Synchronous scanners for enumeration actions

The state below combines the constant-memory scanners needed by one canonical enumeration action. It carries at most one source-radix successor, one count-radix successor, one comparison result, and a Boolean conjunction of cell-local checks.

inductive CertifiedRowSystem.Complement.EnumerationMode : Type

Whether the scanner is waiting for its first cell, processing a row, or irrecoverably bad.

• start : EnumerationMode
• scan : EnumerationMode
• bad : EnumerationMode

instance CertifiedRowSystem.Complement.instDecidableEqEnumerationMode : DecidableEq EnumerationMode

Equations

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

instance CertifiedRowSystem.Complement.instFintypeEnumerationMode : Fintype EnumerationMode

Equations

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

instance CertifiedRowSystem.Complement.instReprEnumerationMode : Repr EnumerationMode

Equations

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

def CertifiedRowSystem.Complement.instReprEnumerationMode.repr : EnumerationMode → ℕ → Std.Format

Equations

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

structure CertifiedRowSystem.Complement.EnumerationAccumulator : Type

Constant-size accumulator shared by all enumeration actions.

• action : ProtocolAction
• overflow : Bool
• found : Bool
• vertexSucc : RowNumeral.CarryState
• countSucc : RowNumeral.CarryState
• comparison : Ordering
• ok : Bool

def CertifiedRowSystem.Complement.instDecidableEqEnumerationAccumulator.decEq (x✝ x✝¹ : EnumerationAccumulator) : Decidable (x✝ = x✝¹)

Equations

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

instance CertifiedRowSystem.Complement.instDecidableEqEnumerationAccumulator : DecidableEq EnumerationAccumulator

Equations

• CertifiedRowSystem.Complement.instDecidableEqEnumerationAccumulator = CertifiedRowSystem.Complement.instDecidableEqEnumerationAccumulator.decEq

def CertifiedRowSystem.Complement.instReprEnumerationAccumulator.repr : EnumerationAccumulator → ℕ → Std.Format

Equations

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

instance CertifiedRowSystem.Complement.instReprEnumerationAccumulator : Repr EnumerationAccumulator

Equations

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

noncomputable instance CertifiedRowSystem.Complement.EnumerationAccumulator.instFintype : Fintype EnumerationAccumulator

Equations

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

structure CertifiedRowSystem.Complement.EnumerationVerifier : Type

Complete finite-state verifier state for enumeration actions.

• mode : EnumerationMode
• acc : EnumerationAccumulator

instance CertifiedRowSystem.Complement.instDecidableEqEnumerationVerifier : DecidableEq EnumerationVerifier

Equations

• CertifiedRowSystem.Complement.instDecidableEqEnumerationVerifier = CertifiedRowSystem.Complement.instDecidableEqEnumerationVerifier.decEq

def CertifiedRowSystem.Complement.instDecidableEqEnumerationVerifier.decEq (x✝ x✝¹ : EnumerationVerifier) : Decidable (x✝ = x✝¹)

Equations

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

def CertifiedRowSystem.Complement.instReprEnumerationVerifier.repr : EnumerationVerifier → ℕ → Std.Format

Equations

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

instance CertifiedRowSystem.Complement.instReprEnumerationVerifier : Repr EnumerationVerifier

Equations

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

noncomputable instance CertifiedRowSystem.Complement.EnumerationVerifier.instFintype : Fintype EnumerationVerifier

Equations

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

def CertifiedRowSystem.Complement.initialEnumerationAccumulator : EnumerationAccumulator

Dummy accumulator used before the first cell and after rejection.

Equations

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

def CertifiedRowSystem.Complement.enumerationStart : EnumerationVerifier

Initial scanner state.

Equations

• CertifiedRowSystem.Complement.enumerationStart = { mode := CertifiedRowSystem.Complement.EnumerationMode.start, acc := CertifiedRowSystem.Complement.initialEnumerationAccumulator }

def CertifiedRowSystem.Complement.enumerationBad : EnumerationVerifier

Absorbing bad scanner state.

Equations

• CertifiedRowSystem.Complement.enumerationBad = { mode := CertifiedRowSystem.Complement.EnumerationMode.bad, acc := CertifiedRowSystem.Complement.initialEnumerationAccumulator }

def CertifiedRowSystem.Complement.startEnumerationAccumulator {A : Type u_1} [Fintype A] (action : ProtocolAction) (old new : ProtocolCell A) : EnumerationAccumulator

Initialize an accumulator for an action, using the first cell only to remember which of the two canonical successor outcomes the target phase claims.

Equations

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

noncomputable def CertifiedRowSystem.Complement.beginRoundLocalOK {A : Type u_1} [Fintype A] [DecidableEq A] (old new : ProtocolCell A) : Bool

Cell-local checks for entering an inner scan.

Equations

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

noncomputable def CertifiedRowSystem.Complement.skipInnerLocalOK {A : Type u_1} [Fintype A] [DecidableEq A] (overflow : Bool) (old new : ProtocolCell A) : Bool

Cell-local checks for skipping an inner vertex. The successor itself is checked by the vertexSucc component.

Equations

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

noncomputable def CertifiedRowSystem.Complement.finishOuterLocalOK {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (overflow found : Bool) (old new : ProtocolCell A) : Bool

Cell-local checks for finishing one outer vertex.

Equations

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

noncomputable def CertifiedRowSystem.Complement.finishRoundLocalOK {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (plateau : Bool) (old new : ProtocolCell A) : Bool

Cell-local checks at a complete count-round boundary.

Equations

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

noncomputable def CertifiedRowSystem.Complement.finalSkipLocalOK {A : Type u_1} [Fintype A] [DecidableEq A] (overflow : Bool) (old new : ProtocolCell A) : Bool

Cell-local checks for skipping a vertex in the final scan.

Equations

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

noncomputable def CertifiedRowSystem.Complement.finalFinishLocalOK {A : Type u_1} [Fintype A] [DecidableEq A] (old new : ProtocolCell A) : Bool

Cell-local checks for the accepting transition after the final scan.

Equations

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

noncomputable def CertifiedRowSystem.Complement.scanEnumerationCell {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (acc : EnumerationAccumulator) (old new : ProtocolCell A) : EnumerationAccumulator

Process one cell after an enumeration action has been selected.

Equations

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

noncomputable def CertifiedRowSystem.Complement.enumerationStepCell {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] : EnumerationVerifier → ProtocolCell A → ProtocolCell A → ProtocolAction → EnumerationVerifier

One cell of the enumeration-action verifier.

Equations

• One or more equations did not get rendered due to their size.
• CertifiedRowSystem.Complement.enumerationStepCell { mode := CertifiedRowSystem.Complement.EnumerationMode.bad, acc := acc } x✝² x✝¹ x✝ = CertifiedRowSystem.Complement.enumerationBad

def CertifiedRowSystem.Complement.enumerationDone : EnumerationVerifier → Bool

Terminal check for one enumeration action.

Equations

• One or more equations did not get rendered due to their size.
• CertifiedRowSystem.Complement.enumerationDone x✝ = false

noncomputable def CertifiedRowSystem.Complement.evalEnumeration {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] : EnumerationVerifier → ProtocolRow A → ProtocolRow A → List ProtocolAction → Option EnumerationVerifier

Run an enumeration-action scanner over three aligned rows.

Equations

• One or more equations did not get rendered due to their size.
• CertifiedRowSystem.Complement.evalEnumeration x✝ [] [] [] = some x✝
• CertifiedRowSystem.Complement.evalEnumeration x✝³ x✝² x✝¹ x✝ = none