Complementing certified row systems

This module implements the inductive-counting construction used to complement the reachability language of a finite CertifiedRowSystem.

The source system is first determinized by CertifiedRowSystem.determinize. Its certificate alphabet is then Unit, and its verifier state after an aligned row scan is the exact set of every source-verifier state reachable by a certificate prefix. Thus an edge and the absence of an edge are both synchronous finite-state checks.

The complement protocol stores a constant number of tracks in each row cell. Vertex and fuel tracks use the source row alphabet; count tracks use radix Fintype.card A + 1, so a nonempty width-n row can represent every count up to (Fintype.card A) ^ n. All tracks are least-significant-cell first and are scanned using RowNumeral.

The semantic finite graph

@[reducible, inline]

abbrev CertifiedRowSystem.Complement.FixedRow (A : Type u_6) (n : ℕ) : Type u_6

A fixed-width source row, represented without a length proof in every operation.

Equations

• CertifiedRowSystem.Complement.FixedRow A n = (Fin n → A)

def CertifiedRowSystem.Complement.FixedRow.toList {A : Type u_2} {n : ℕ} (row : FixedRow A n) : List A

Convert a fixed-width row to the list representation used by a certified row system.

Equations

• row.toList = List.ofFn row

@[simp]

theorem CertifiedRowSystem.Complement.FixedRow.length_toList {A : Type u_2} {n : ℕ} (row : FixedRow A n) : row.toList.length = n

def CertifiedRowSystem.Complement.rowEdge {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) {n : ℕ} (old new : FixedRow A n) : Prop

The finite directed graph on width-n rows induced by the source row relation.

Equations

• CertifiedRowSystem.Complement.rowEdge S old new = S.RowStep old.toList new.toList

def CertifiedRowSystem.Complement.rowFinal {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) {n : ℕ} (row : FixedRow A n) : Prop

The source final predicate on a fixed-width row.

Equations

• CertifiedRowSystem.Complement.rowFinal S row = S.Final row.toList

def CertifiedRowSystem.Complement.inputRow {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) {n : ℕ} (input : FixedRow I n) : FixedRow A n

The fixed-width source row obtained from an input row.

Equations

• CertifiedRowSystem.Complement.inputRow S input = S.inputCell ∘ input

theorem CertifiedRowSystem.Complement.no_final_iff_abstract_counting_certificate {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype A] [DecidableEq A] (S : CertifiedRowSystem I A C Q F) {n : ℕ} (input : FixedRow I n) : (¬∃ (row : FixedRow A n), Relation.ReflTransGen (rowEdge S) (inputRow S input) row ∧ rowFinal S row) ↔ ∃ (count : ℕ), FiniteReachabilityCounting.CertifiedCount (rowEdge S) (inputRow S input) (Fintype.card (FixedRow A n)) count ∧ Nonempty (FiniteReachabilityCounting.FinalRejection (rowEdge S) (inputRow S input) (Fintype.card (FixedRow A n)) count (rowFinal S))

The abstract counting certificate characterizes absence of a reachable final row in the finite graph of width-n source rows. This theorem is the semantic target of the streaming certified-row protocol below.

Streaming protocol storage

noncomputable def CertifiedRowSystem.Complement.vertexCodec (A : Type u_6) [Fintype A] [Nonempty A] : RowNumeral.DigitCodec A

Canonical numbering of an arbitrary nonempty finite source alphabet.

Equations

• CertifiedRowSystem.Complement.vertexCodec A = { toFin := Fintype.equivFin A }

@[reducible, inline]

abbrev CertifiedRowSystem.Complement.CountDigit (A : Type u_6) [Fintype A] : Type

Counter digits have one more value than the source alphabet. Consequently a width-n > 0 counter can store the number of all width-n source rows.

Equations

• CertifiedRowSystem.Complement.CountDigit A = Fin (Fintype.card A + 1)

def CertifiedRowSystem.Complement.countCodec (A : Type u_6) [Fintype A] : RowNumeral.DigitCodec (CountDigit A)

Canonical codec for count digits.

Equations

• CertifiedRowSystem.Complement.countCodec A = RowNumeral.orderedCodec (CertifiedRowSystem.Complement.CountDigit A)

theorem CertifiedRowSystem.Complement.countRadix_gt_one (A : Type u_6) [Fintype A] [Nonempty A] : 1 < (countCodec A).radix

The count radix is genuinely larger than one whenever the source alphabet is nonempty.

inductive CertifiedRowSystem.Complement.ProtocolPhase : Type

Control phases of the streaming inductive-counting protocol.

chooseInner performs the canonical scan over possible old-reachable vertices. A positive choice enters path, which guesses a source path bounded by depth. Once every inner vertex has been considered, finishOuter classifies the current outer vertex and updates the next count. finishRound advances the depth enumeration. The last two phases perform the all-nonfinal scan justified by the final exact count.

• input : ProtocolPhase
• roundStart : ProtocolPhase
• chooseInner : ProtocolPhase
• path : ProtocolPhase
• finishWitness : ProtocolPhase
• finishOuter : ProtocolPhase
• finishRound : ProtocolPhase
• finalChoose : ProtocolPhase
• finalPath : ProtocolPhase
• finalWitness : ProtocolPhase
• finalFinish : ProtocolPhase
• accept : ProtocolPhase

instance CertifiedRowSystem.Complement.instDecidableEqProtocolPhase : DecidableEq ProtocolPhase

Equations

• CertifiedRowSystem.Complement.instDecidableEqProtocolPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CertifiedRowSystem.Complement.instFintypeProtocolPhase : Fintype ProtocolPhase

Equations

• One or more equations did not get rendered due to their size.

def CertifiedRowSystem.Complement.instReprProtocolPhase.repr : ProtocolPhase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance CertifiedRowSystem.Complement.instReprProtocolPhase : Repr ProtocolPhase

Equations

• CertifiedRowSystem.Complement.instReprProtocolPhase = { reprPrec := CertifiedRowSystem.Complement.instReprProtocolPhase.repr }

structure CertifiedRowSystem.Complement.VertexTracks (A : Type u_6) [Fintype A] : Type u_6

Source-alphabet tracks grouped to keep finite-instance synthesis shallow.

• source : A
• depth : A
• outer : A
• inner : A
• path : A
• fuel : A

instance CertifiedRowSystem.Complement.instDecidableEqVertexTracks {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] : DecidableEq (VertexTracks A✝)

Equations

• CertifiedRowSystem.Complement.instDecidableEqVertexTracks = CertifiedRowSystem.Complement.instDecidableEqVertexTracks.decEq

def CertifiedRowSystem.Complement.instDecidableEqVertexTracks.decEq {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] (x✝ x✝¹ : VertexTracks A✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CertifiedRowSystem.Complement.VertexTracks.instFintype {A : Type u_6} [Fintype A] : Fintype (VertexTracks A)

Equations

• CertifiedRowSystem.Complement.VertexTracks.instFintype = Fintype.ofInjective (fun (x : CertifiedRowSystem.Complement.VertexTracks A) => (x.source, x.depth, x.outer, x.inner, x.path, x.fuel)) ⋯

structure CertifiedRowSystem.Complement.CounterTracks (A : Type u_6) [Fintype A] : Type

Larger-radix counter tracks.

• oldCount : CountDigit A
• newCount : CountDigit A
• seenCount : CountDigit A

def CertifiedRowSystem.Complement.instDecidableEqCounterTracks.decEq {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] (x✝ x✝¹ : CounterTracks A✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance CertifiedRowSystem.Complement.instDecidableEqCounterTracks {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] : DecidableEq (CounterTracks A✝)

Equations

• CertifiedRowSystem.Complement.instDecidableEqCounterTracks = CertifiedRowSystem.Complement.instDecidableEqCounterTracks.decEq

noncomputable instance CertifiedRowSystem.Complement.CounterTracks.instFintype {A : Type u_6} [Fintype A] : Fintype (CounterTracks A)

Equations

• CertifiedRowSystem.Complement.CounterTracks.instFintype = Fintype.ofInjective (fun (x : CertifiedRowSystem.Complement.CounterTracks A) => (x.oldCount, x.newCount, x.seenCount)) ⋯

structure CertifiedRowSystem.Complement.ProtocolCell (A : Type u_6) [Fintype A] : Type u_6

One physical cell of the complement protocol.

source is immutable. depth, outer, inner, path, and fuel are source-radix row numerals. oldCount, newCount, and seenCount use the strictly larger count radix. The phase and Boolean flag are replicated; the verifier enforces uniformity on every scan.

• vertex : VertexTracks A
• counter : CounterTracks A
• found : Bool
• phase : ProtocolPhase

def CertifiedRowSystem.Complement.instDecidableEqProtocolCell.decEq {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] (x✝ x✝¹ : ProtocolCell A✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance CertifiedRowSystem.Complement.instDecidableEqProtocolCell {A✝ : Type u_6} {inst✝ : Fintype A✝} [DecidableEq A✝] : DecidableEq (ProtocolCell A✝)

Equations

• CertifiedRowSystem.Complement.instDecidableEqProtocolCell = CertifiedRowSystem.Complement.instDecidableEqProtocolCell.decEq

noncomputable instance CertifiedRowSystem.Complement.ProtocolCell.instFintype {A : Type u_6} [Fintype A] : Fintype (ProtocolCell A)

Equations

• CertifiedRowSystem.Complement.ProtocolCell.instFintype = Fintype.ofInjective (fun (x : CertifiedRowSystem.Complement.ProtocolCell A) => (x.vertex, x.counter, x.found, x.phase)) ⋯

@[reducible, inline]

abbrev CertifiedRowSystem.Complement.ProtocolRow (A : Type u_6) [Fintype A] : Type u_6

A protocol row has one cell per source/input cell.

Equations

• CertifiedRowSystem.Complement.ProtocolRow A = List (CertifiedRowSystem.Complement.ProtocolCell A)

def CertifiedRowSystem.Complement.HasPhase {A : Type u_6} [Fintype A] (phase : ProtocolPhase) (row : ProtocolRow A) : Prop

The phase is replicated across the complete row.

Equations

• CertifiedRowSystem.Complement.HasPhase phase row = ∀ cell ∈ row, cell.phase = phase

def CertifiedRowSystem.Complement.sourceTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the immutable source track.

Equations

• CertifiedRowSystem.Complement.sourceTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.source) row

def CertifiedRowSystem.Complement.depthTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the current counting depth.

Equations

• CertifiedRowSystem.Complement.depthTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.depth) row

def CertifiedRowSystem.Complement.oldCountTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List (CountDigit A)

Extract the exact count from the preceding round.

Equations

• CertifiedRowSystem.Complement.oldCountTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.counter.oldCount) row

def CertifiedRowSystem.Complement.newCountTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List (CountDigit A)

Extract the accumulating next-round count.

Equations

• CertifiedRowSystem.Complement.newCountTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.counter.newCount) row

def CertifiedRowSystem.Complement.seenCountTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List (CountDigit A)

Extract the number of old-reachable vertices selected in the current canonical scan.

Equations

• CertifiedRowSystem.Complement.seenCountTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.counter.seenCount) row

def CertifiedRowSystem.Complement.outerTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the outer vertex being classified.

Equations

• CertifiedRowSystem.Complement.outerTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.outer) row

def CertifiedRowSystem.Complement.innerTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the old vertex currently considered by the inner scan.

Equations

• CertifiedRowSystem.Complement.innerTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.inner) row

def CertifiedRowSystem.Complement.pathTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the current row of a guessed source path.

Equations

• CertifiedRowSystem.Complement.pathTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.path) row

def CertifiedRowSystem.Complement.fuelTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List A

Extract the length of the guessed path.

Equations

• CertifiedRowSystem.Complement.fuelTrack row = List.map (fun (cell : CertifiedRowSystem.Complement.ProtocolCell A) => cell.vertex.fuel) row

def CertifiedRowSystem.Complement.foundTrack {A : Type u_6} [Fintype A] (row : ProtocolRow A) : List Bool

Extract the replicated inclusion flag.

Equations

• CertifiedRowSystem.Complement.foundTrack row = List.map CertifiedRowSystem.Complement.ProtocolCell.found row

def CertifiedRowSystem.Complement.HasFound {A : Type u_6} [Fintype A] (found : Bool) (row : ProtocolRow A) : Prop

All replicated found flags have the specified value.

Equations

• CertifiedRowSystem.Complement.HasFound found row = ∀ cell ∈ row, cell.found = found

structure CertifiedRowSystem.Complement.WellFormedRow {A : Type u_6} [Fintype A] (width : ℕ) (row : ProtocolRow A) : Prop

Shape invariant shared by every protocol phase.

• length_eq : List.length row = width
• uniform_phase : ∃ (phase : ProtocolPhase), HasPhase phase row
• uniform_found : ∃ (found : Bool), HasFound found row

noncomputable def CertifiedRowSystem.Complement.inputProtocolCell {I : Type u_6} {A : Type u_7} [Fintype A] [Nonempty A] (sourceCell : I → A) (input : I) : ProtocolCell A

The input image stores the source row and initializes every work track to zero. The first protocol transition changes oldCount from the all-zero input image to the LSD-first numeral one; doing this in a transition lets the finite verifier identify the first cell.

Equations

• One or more equations did not get rendered due to their size.

def CertifiedRowSystem.Complement.IsInitialized {A : Type u_6} [Fintype A] [Nonempty A] (source : List A) (row : ProtocolRow A) : Prop

Predicate describing the canonical initialized row after the boot transition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CertifiedRowSystem.Complement.initializedProtocolCell {A : Type u_6} [Fintype A] [Nonempty A] (first : Bool) (source : A) : ProtocolCell A

One initialized protocol cell. The first cell stores the least-significant digit one of the initial reachable count; every later count digit is zero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CertifiedRowSystem.Complement.initializedProtocolRow {A : Type u_6} [Fintype A] [Nonempty A] : List A → ProtocolRow A

Canonical initialized protocol row for a nonempty source row.

Equations

• One or more equations did not get rendered due to their size.
• CertifiedRowSystem.Complement.initializedProtocolRow [] = []

@[simp]

theorem CertifiedRowSystem.Complement.length_initializedProtocolRow {A : Type u_6} [Fintype A] [Nonempty A] (source : List A) : List.length (initializedProtocolRow source) = source.length

theorem CertifiedRowSystem.Complement.isInitialized_initializedProtocolRow {A : Type u_6} [Fintype A] [Nonempty A] {source : List A} (hne : source ≠ []) : IsInitialized source (initializedProtocolRow source)

The canonical initialized row satisfies every initialization invariant.

inductive CertifiedRowSystem.Complement.ProtocolAction : Type

A transition label is repeated in the certificate row. The finite verifier rejects if different cells request different actions.

• boot : ProtocolAction
• beginRound : ProtocolAction
• beginFinal : ProtocolAction
• skipInner : ProtocolAction
• startPath : ProtocolAction
• pathStep : ProtocolAction
• finishWitness : ProtocolAction
• finishOuter : ProtocolAction
• finishRound : ProtocolAction
• finalSkip : ProtocolAction
• finalStartPath : ProtocolAction
• finalPathStep : ProtocolAction
• finalFinishWitness : ProtocolAction
• finalFinish : ProtocolAction

instance CertifiedRowSystem.Complement.instDecidableEqProtocolAction : DecidableEq ProtocolAction

Equations

• CertifiedRowSystem.Complement.instDecidableEqProtocolAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CertifiedRowSystem.Complement.instFintypeProtocolAction : Fintype ProtocolAction

Equations

• One or more equations did not get rendered due to their size.

instance CertifiedRowSystem.Complement.instReprProtocolAction : Repr ProtocolAction

Equations

• CertifiedRowSystem.Complement.instReprProtocolAction = { reprPrec := CertifiedRowSystem.Complement.instReprProtocolAction.repr }

def CertifiedRowSystem.Complement.instReprProtocolAction.repr : ProtocolAction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.