Path actions for the certified-row complement protocol #

def CertifiedRowSystem.Complement.noteBit :

Option Bool → Bool → Option Bool

Extend a possibly-unset replicated bit, rejecting a disagreement.

Equations

CertifiedRowSystem.Complement.noteBit none x✝ = some x✝
CertifiedRowSystem.Complement.noteBit (some expected) x✝ = if x✝ = expected then some expected else none

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.noteBit_none (bit : Bool) :

noteBit none bit = some bit

def CertifiedRowSystem.Complement.notePhase :

Option ProtocolPhase → ProtocolPhase → Option ProtocolPhase

Extend a possibly-unset replicated phase, rejecting a disagreement.

Equations

CertifiedRowSystem.Complement.notePhase none x✝ = some x✝
CertifiedRowSystem.Complement.notePhase (some expected) x✝ = if x✝ = expected then some expected else none

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.notePhase_none (phase : ProtocolPhase) :

notePhase none phase = some phase

inductive CertifiedRowSystem.Complement.UniformScan (X : Type u_5) :

Type u_5

State of a uniform-value scan. bad is distinct from the initially unset state, so a disagreement cannot be erased by a later matching cell.

start {X : Type u_5} : UniformScan X
value {X : Type u_5} (expected : X) : UniformScan X
bad {X : Type u_5} : UniformScan X

Instances For

def CertifiedRowSystem.Complement.instDecidableEqUniformScan.decEq {X✝ : Type u_5} [DecidableEq X✝] (x✝ x✝¹ : UniformScan X✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

instance CertifiedRowSystem.Complement.instDecidableEqUniformScan {X✝ : Type u_5} [DecidableEq X✝] :

DecidableEq (UniformScan X✝)

Equations

CertifiedRowSystem.Complement.instDecidableEqUniformScan = CertifiedRowSystem.Complement.instDecidableEqUniformScan.decEq

instance CertifiedRowSystem.Complement.instFintypeUniformScan {X✝ : Type u_5} [Fintype X✝] :

Fintype (UniformScan X✝)

Equations

CertifiedRowSystem.Complement.instFintypeUniformScan = Fintype.ofEquiv (Unit ⊕ X✝ ⊕ Unit) (CertifiedRowSystem.Complement.UniformScan.proxyTypeEquiv X✝)

def CertifiedRowSystem.Complement.UniformScan.step {X : Type u_5} [DecidableEq X] :

UniformScan X → X → UniformScan X

Extend a uniform-value scan by one element.

Equations

One or more equations did not get rendered due to their size.
CertifiedRowSystem.Complement.UniformScan.start.step x✝ = CertifiedRowSystem.Complement.UniformScan.value x✝
CertifiedRowSystem.Complement.UniformScan.bad.step x✝ = CertifiedRowSystem.Complement.UniformScan.bad

Instances For

def CertifiedRowSystem.Complement.scanBits :

UniformScan Bool → List Bool → UniformScan Bool

Scan a replicated Boolean track.

Equations

CertifiedRowSystem.Complement.scanBits x✝ [] = x✝
CertifiedRowSystem.Complement.scanBits x✝ (bit :: bits) = CertifiedRowSystem.Complement.scanBits (x✝.step bit) bits

Instances For

def CertifiedRowSystem.Complement.scanPhases :

UniformScan ProtocolPhase → List ProtocolPhase → UniformScan ProtocolPhase

Scan a replicated phase track.

Equations

CertifiedRowSystem.Complement.scanPhases x✝ [] = x✝
CertifiedRowSystem.Complement.scanPhases x✝ (phase :: phases) = CertifiedRowSystem.Complement.scanPhases (x✝.step phase) phases

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.scanBits_bad (bits : List Bool) :

scanBits UniformScan.bad bits = UniformScan.bad

@[simp]

theorem CertifiedRowSystem.Complement.scanPhases_bad (phases : List ProtocolPhase) :

scanPhases UniformScan.bad phases = UniformScan.bad

@[simp]

theorem CertifiedRowSystem.Complement.scanBits_mismatch (expected bit : Bool) (bits : List Bool) (h : bit ≠ expected) :

scanBits (UniformScan.value expected) (bit :: bits) = UniformScan.bad

A disagreement is an absorbing rejection for the replicated-bit scanner.

@[simp]

theorem CertifiedRowSystem.Complement.scanPhases_mismatch (expected phase : ProtocolPhase) (phases : List ProtocolPhase) (h : phase ≠ expected) :

scanPhases (UniformScan.value expected) (phase :: phases) = UniformScan.bad

A disagreement is an absorbing rejection for the replicated-phase scanner.

@[simp]

theorem CertifiedRowSystem.Complement.scanBits_true_false_true :

scanBits UniformScan.start [true , false , true ] = UniformScan.bad

Regression test: a later matching bit cannot erase an earlier disagreement.

scanPhases UniformScan.start [ProtocolPhase.path , ProtocolPhase.chooseInner , ProtocolPhase.path ] = UniformScan.bad

@[simp]

theorem CertifiedRowSystem.Complement.scanPhases_path_choose_path :

Regression test: a later matching phase cannot erase an earlier disagreement.

def CertifiedRowSystem.Complement.noteEq {A : Type u_2} [DecidableEq A] (ok : Bool) (old new : A) :

Equality accumulator for an aligned pair of tracks.

Equations

CertifiedRowSystem.Complement.noteEq ok old new = (ok && decide (old = new))

Instances For

def CertifiedRowSystem.Complement.checkPairs {α : Type u_5} {β : Type u_6} (p : α → β → Bool) :

List α → List β → Bool

Boolean scan of a cell-local relation on two aligned lists.

Equations

CertifiedRowSystem.Complement.checkPairs p [] [] = true
CertifiedRowSystem.Complement.checkPairs p (x_2 :: xs) (y :: ys) = (p x_2 y && CertifiedRowSystem.Complement.checkPairs p xs ys)
CertifiedRowSystem.Complement.checkPairs p x✝¹ x✝ = false

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.checkPairs_eq_true_iff {α : Type u_5} {β : Type u_6} (p : α → β → Bool) (xs : List α) (ys : List β) :

checkPairs p xs ys = true ↔ List.Forall₂ (fun (x : α) (y : β) => p x y = true) xs ys

theorem CertifiedRowSystem.Complement.unitList_eq_replicate (cert : List Unit) :

cert = List.replicate cert.length ()

Every list of unit certificates is the canonical replicated unit list.

theorem CertifiedRowSystem.Complement.rowStep_iff_evalUnit {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (old new : List A) :

D.RowStep old new ↔ ∃ (q : Q), D.evalStep D.stepStart old new (List.replicate old.length ()) = some q ∧ D.stepDone q = true

For a unit-certified system there is only one certificate row of a given length.

theorem CertifiedRowSystem.Complement.exists_evalStep_unit_of_length {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (q : Q) (old new : List A) (hlen : old.length = new.length) :

∃ (out : Q), D.evalStep q old new (List.replicate old.length ()) = some out

A deterministic unit-certified verifier has a unique run on every aligned pair.

Starting a path #

noncomputable def CertifiedRowSystem.Complement.startPathLocalOK {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (old new : ProtocolCell A) :

Cell-local part of path initialization. All persistent tracks are copied, the path is reset to the immutable source row, and fuel is reset to zero.

Equations

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

Instances For

@[reducible, inline]

abbrev CertifiedRowSystem.Complement.StartPathVerifier :

Type

State of a path-initialization scan.

Equations

CertifiedRowSystem.Complement.StartPathVerifier = Bool

Instances For

noncomputable def CertifiedRowSystem.Complement.startPathStepCell {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (ok : StartPathVerifier) (old new : ProtocolCell A) :

StartPathVerifier

One cell of a path-initialization scan.

Equations

CertifiedRowSystem.Complement.startPathStepCell oldPhase newPhase ok old new = (ok && CertifiedRowSystem.Complement.startPathLocalOK oldPhase newPhase old new)

Instances For

def CertifiedRowSystem.Complement.startPathDone (q : StartPathVerifier) :

Successful terminal state for path initialization.

Equations

CertifiedRowSystem.Complement.startPathDone q = q

Instances For

noncomputable def CertifiedRowSystem.Complement.evalStartPath {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) :

StartPathVerifier → ProtocolRow A → ProtocolRow A → Option StartPathVerifier

Run a path-initialization scanner on aligned protocol rows.

Equations

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

Instances For

def CertifiedRowSystem.Complement.StartsPath {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (old new : ProtocolRow A) :

Exact list-level specification of path initialization.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.evalStartPath_done_iff {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (old new : ProtocolRow A) :

evalStartPath oldPhase newPhase true old new = some true ↔ StartsPath oldPhase newPhase old new

The finite scanner accepts exactly the list-level path-initialization relation.

@[simp]

theorem CertifiedRowSystem.Complement.startPathLocalOK_eq_true_iff {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (old new : ProtocolCell A) :

startPathLocalOK oldPhase newPhase old new = true ↔ old.phase = oldPhase ∧ new.phase = newPhase ∧ new.vertex.source = old.vertex.source ∧ new.vertex.depth = old.vertex.depth ∧ new.vertex.outer = old.vertex.outer ∧ new.vertex.inner = old.vertex.inner ∧ new.vertex.path = old.vertex.source ∧ new.vertex.fuel = (vertexCodec A).zero ∧ new.counter.oldCount = old.counter.oldCount ∧ new.counter.newCount = old.counter.newCount ∧ new.counter.seenCount = old.counter.seenCount ∧ new.found = old.found

theorem CertifiedRowSystem.Complement.StartsPath.spec {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] {oldPhase newPhase : ProtocolPhase} {old new : ProtocolRow A} (h : StartsPath oldPhase newPhase old new) :

List.length old = List.length new ∧ HasPhase oldPhase old ∧ HasPhase newPhase new ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ innerTrack new = innerTrack old ∧ pathTrack new = sourceTrack old ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ seenCountTrack new = seenCountTrack old ∧ foundTrack new = foundTrack old

Track/phase projection of the list-level path initialization relation.

@[reducible, inline]

noncomputable abbrev CertifiedRowSystem.Complement.startPathCell {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (ok : StartPathVerifier) (old new : ProtocolCell A) :

StartPathVerifier

Ordinary counting-round path initialization.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev CertifiedRowSystem.Complement.finalStartPathCell {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (ok : StartPathVerifier) (old new : ProtocolCell A) :

StartPathVerifier

Final-rejection path initialization.

Equations

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

Instances For

Extending a bounded path #

structure CertifiedRowSystem.Complement.PathStepVerifier (Q : Type u_5) :

Type u_5

Finite state of the synchronous bounded-path scanner.

sourceState : Q
samePath : Bool
fuelSucc : RowNumeral.CarryState
fuelDepth : Ordering
localOK : Bool

Instances For

def CertifiedRowSystem.Complement.instDecidableEqPathStepVerifier.decEq {Q✝ : Type u_5} [DecidableEq Q✝] (x✝ x✝¹ : PathStepVerifier Q✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance CertifiedRowSystem.Complement.instDecidableEqPathStepVerifier {Q✝ : Type u_5} [DecidableEq Q✝] :

DecidableEq (PathStepVerifier Q✝)

Equations

CertifiedRowSystem.Complement.instDecidableEqPathStepVerifier = CertifiedRowSystem.Complement.instDecidableEqPathStepVerifier.decEq

noncomputable instance CertifiedRowSystem.Complement.PathStepVerifier.instFintype {Q : Type u_3} [Fintype Q] :

Fintype (PathStepVerifier Q)

Equations

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

def CertifiedRowSystem.Complement.pathStepStart {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) :

Initial state for a bounded path-extension scan.

Equations

CertifiedRowSystem.Complement.pathStepStart D = { sourceState := D.stepStart, samePath := true, fuelSucc := RowNumeral.CarryState.carry, fuelDepth := Ordering.eq, localOK := true }

Instances For

def CertifiedRowSystem.Complement.pathStepLocalOK {A : Type u_2} [Fintype A] [DecidableEq A] (phase : ProtocolPhase) (old new : ProtocolCell A) :

Persistent cell-local conditions of a path extension.

Equations

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

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.pathStepLocalOK_eq_true_iff {A : Type u_2} [Fintype A] [DecidableEq A] (phase : ProtocolPhase) (old new : ProtocolCell A) :

pathStepLocalOK phase old new = true ↔ old.phase = phase ∧ new.phase = phase ∧ new.vertex.source = old.vertex.source ∧ new.vertex.depth = old.vertex.depth ∧ new.vertex.outer = old.vertex.outer ∧ new.vertex.inner = old.vertex.inner ∧ new.counter.oldCount = old.counter.oldCount ∧ new.counter.newCount = old.counter.newCount ∧ new.counter.seenCount = old.counter.seenCount ∧ new.found = old.found

noncomputable def CertifiedRowSystem.Complement.pathStepCell {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (phase : ProtocolPhase) (q : PathStepVerifier Q) (old new : ProtocolCell A) :

One cell of a path extension. It simultaneously runs the deterministic source edge verifier, the stuttering check, the fuel successor, and fuel < depth.

Equations

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

Instances For

def CertifiedRowSystem.Complement.pathStepDone {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (q : PathStepVerifier Q) :

A path extension succeeds exactly for a proper bounded fuel increment and either a stutter or a source edge.

Equations

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

Instances For

noncomputable def CertifiedRowSystem.Complement.evalPathStep {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (phase : ProtocolPhase) :

PathStepVerifier Q → ProtocolRow A → ProtocolRow A → Option (PathStepVerifier Q)

Run the path-extension scanner on aligned rows.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.evalPathStep_eq_some_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (phase : ProtocolPhase) (q out : PathStepVerifier Q) (old new : ProtocolRow A) :

evalPathStep D phase q old new = some out ↔ D.evalStep q.sourceState (pathTrack old) (pathTrack new) (List.replicate (List.length old) ()) = some out.sourceState ∧ out.samePath = (q.samePath && decide (pathTrack old = pathTrack new)) ∧ (vertexCodec A).evalSucc q.fuelSucc (fuelTrack old) (fuelTrack new) = some out.fuelSucc ∧ (vertexCodec A).evalCompare q.fuelDepth (fuelTrack old) (depthTrack old) = some out.fuelDepth ∧ out.localOK = (q.localOK && checkPairs (pathStepLocalOK phase) old new)

Exact componentwise behavior of the path-extension scan. This theorem is the bridge from the finite product state to the list-level source, counter, comparison, and preservation checks.

def CertifiedRowSystem.Complement.IsPathStep {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (phase : ProtocolPhase) (old new : ProtocolRow A) :

List-level semantics of one bounded path extension.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.IsPathStep.persistent_spec {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {phase : ProtocolPhase} {old new : ProtocolRow A} (h : IsPathStep D phase old new) :

List.length old = List.length new ∧ HasPhase phase old ∧ HasPhase phase new ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ innerTrack new = innerTrack old ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ seenCountTrack new = seenCountTrack old ∧ foundTrack new = foundTrack old

Phase and persistent-track projection of a bounded path step.

theorem CertifiedRowSystem.Complement.evalPathStep_done_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (phase : ProtocolPhase) (old new : ProtocolRow A) :

(∃ (out : PathStepVerifier Q), evalPathStep D phase (pathStepStart D) old new = some out ∧ pathStepDone D out = true) ↔ IsPathStep D phase old new

The path scanner accepts exactly a persistent, proper fuel increment whose path component either stutters or follows one determinized source edge.

@[reducible, inline]

noncomputable abbrev CertifiedRowSystem.Complement.countingPathStepCell {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q : PathStepVerifier Q) (old new : ProtocolCell A) :

Counting-round path extension.

Equations

CertifiedRowSystem.Complement.countingPathStepCell D = CertifiedRowSystem.Complement.pathStepCell D CertifiedRowSystem.Complement.ProtocolPhase.path

Instances For

@[reducible, inline]

noncomputable abbrev CertifiedRowSystem.Complement.finalPathStepCell {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q : PathStepVerifier Q) (old new : ProtocolCell A) :

Final-rejection path extension.

Equations

CertifiedRowSystem.Complement.finalPathStepCell D = CertifiedRowSystem.Complement.pathStepCell D CertifiedRowSystem.Complement.ProtocolPhase.finalPath

Instances For

Completing a counting-round witness #

structure CertifiedRowSystem.Complement.FinishWitnessVerifier (Q : Type u_5) :

Type u_5

Finite state for completing a reachability witness in a counting round.

edgeState : Q
pathInner : Bool
fuelDepth : Bool
innerOuter : Bool
seenSucc : RowNumeral.CarryState
innerSucc : RowNumeral.CarryState
oldFound : UniformScan Bool
newFound : UniformScan Bool
newPhase : UniformScan ProtocolPhase
localOK : Bool

Instances For

instance CertifiedRowSystem.Complement.instDecidableEqFinishWitnessVerifier {Q✝ : Type u_5} [DecidableEq Q✝] :

DecidableEq (FinishWitnessVerifier Q✝)

Equations

CertifiedRowSystem.Complement.instDecidableEqFinishWitnessVerifier = CertifiedRowSystem.Complement.instDecidableEqFinishWitnessVerifier.decEq

def CertifiedRowSystem.Complement.instDecidableEqFinishWitnessVerifier.decEq {Q✝ : Type u_5} [DecidableEq Q✝] (x✝ x✝¹ : FinishWitnessVerifier Q✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

noncomputable instance CertifiedRowSystem.Complement.FinishWitnessVerifier.instFintype {Q : Type u_3} [Fintype Q] :

Fintype (FinishWitnessVerifier Q)

Equations

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

def CertifiedRowSystem.Complement.finishWitnessStart {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) :

FinishWitnessVerifier Q

Initial state of the witness-completion scan.

Equations

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

Instances For

noncomputable def CertifiedRowSystem.Complement.finishWitnessLocalOK {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolCell A) :

Persistent and reset conditions of counting-round witness completion.

Equations

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

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.finishWitnessLocalOK_eq_true_iff {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolCell A) :

finishWitnessLocalOK old new = true ↔ old.phase = ProtocolPhase.path ∧ new.vertex.source = old.vertex.source ∧ new.vertex.depth = old.vertex.depth ∧ new.vertex.outer = old.vertex.outer ∧ new.vertex.path = (vertexCodec A).zero ∧ new.vertex.fuel = (vertexCodec A).zero ∧ new.counter.oldCount = old.counter.oldCount ∧ new.counter.newCount = old.counter.newCount

noncomputable def CertifiedRowSystem.Complement.finishWitnessCell {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q : FinishWitnessVerifier Q) (old new : ProtocolCell A) :

FinishWitnessVerifier Q

One cell of witness completion.

Equations

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

Instances For

def CertifiedRowSystem.Complement.finishWitnessDone {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (q : FinishWitnessVerifier Q) :

Successful witness completion. The phase is determined by whether advancing the canonical inner enumeration overflows.

Equations

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

Instances For

noncomputable def CertifiedRowSystem.Complement.evalFinishWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) :

FinishWitnessVerifier Q → ProtocolRow A → ProtocolRow A → Option (FinishWitnessVerifier Q)

Run counting-round witness completion on aligned rows.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.evalFinishWitness_eq_some_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q out : FinishWitnessVerifier Q) (old new : ProtocolRow A) :

evalFinishWitness D q old new = some out ↔ D.evalStep q.edgeState (innerTrack old) (outerTrack old) (List.replicate (List.length old) ()) = some out.edgeState ∧ out.pathInner = (q.pathInner && decide (pathTrack old = innerTrack old)) ∧ out.fuelDepth = (q.fuelDepth && decide (fuelTrack old = depthTrack old)) ∧ out.innerOuter = (q.innerOuter && decide (innerTrack old = outerTrack old)) ∧ (countCodec A).evalSucc q.seenSucc (seenCountTrack old) (seenCountTrack new) = some out.seenSucc ∧ (vertexCodec A).evalSucc q.innerSucc (innerTrack old) (innerTrack new) = some out.innerSucc ∧ out.oldFound = scanBits q.oldFound (List.map (fun (x : ProtocolCell A) => x.found) old) ∧ out.newFound = scanBits q.newFound (List.map (fun (x : ProtocolCell A) => x.found) new) ∧ out.newPhase = scanPhases q.newPhase (List.map (fun (x : ProtocolCell A) => x.phase) new) ∧ out.localOK = (q.localOK && checkPairs finishWitnessLocalOK old new)

Exact componentwise behavior of counting-round witness completion.

def CertifiedRowSystem.Complement.IsFinishWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :

List-level specification of completing a counting-round reachability witness.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.IsFinishWitness.persistent_spec {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {old new : ProtocolRow A} (h : IsFinishWitness D old new) :

List.length old = List.length new ∧ HasPhase ProtocolPhase.path old ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ pathTrack new = (vertexCodec A).zeroRow (List.length new) ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old

Persistent/reset-track projection of counting-round witness completion.

theorem CertifiedRowSystem.Complement.evalFinishWitness_done_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :

(∃ (out : FinishWitnessVerifier Q), evalFinishWitness D (finishWitnessStart D) old new = some out ∧ finishWitnessDone D out = true) ↔ IsFinishWitness D old new

The finite scanner accepts exactly the list-level witness-completion action.

Completing a final-rejection witness #

structure CertifiedRowSystem.Complement.FinalWitnessVerifier (F : Type u_5) :

Type u_5

Finite state for completing one witness in the final all-nonfinal scan.

finalState : F
pathInner : Bool
fuelDepth : Bool
seenSucc : RowNumeral.CarryState
innerSucc : RowNumeral.CarryState
newPhase : UniformScan ProtocolPhase
localOK : Bool

Instances For

instance CertifiedRowSystem.Complement.instDecidableEqFinalWitnessVerifier {F✝ : Type u_5} [DecidableEq F✝] :

DecidableEq (FinalWitnessVerifier F✝)

Equations

CertifiedRowSystem.Complement.instDecidableEqFinalWitnessVerifier = CertifiedRowSystem.Complement.instDecidableEqFinalWitnessVerifier.decEq

def CertifiedRowSystem.Complement.instDecidableEqFinalWitnessVerifier.decEq {F✝ : Type u_5} [DecidableEq F✝] (x✝ x✝¹ : FinalWitnessVerifier F✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

noncomputable instance CertifiedRowSystem.Complement.FinalWitnessVerifier.instFintype {F : Type u_4} [Fintype F] :

Fintype (FinalWitnessVerifier F)

Equations

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

def CertifiedRowSystem.Complement.finalWitnessStart {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) :

FinalWitnessVerifier F

Initial state for final witness completion.

Equations

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

Instances For

noncomputable def CertifiedRowSystem.Complement.finalWitnessLocalOK {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolCell A) :

Persistent/reset conditions for final witness completion.

Equations

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

Instances For

@[simp]

theorem CertifiedRowSystem.Complement.finalWitnessLocalOK_eq_true_iff {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolCell A) :

finalWitnessLocalOK old new = true ↔ old.phase = ProtocolPhase.finalPath ∧ new.vertex.source = old.vertex.source ∧ new.vertex.depth = old.vertex.depth ∧ new.vertex.outer = old.vertex.outer ∧ new.vertex.path = (vertexCodec A).zero ∧ new.vertex.fuel = (vertexCodec A).zero ∧ new.counter.oldCount = old.counter.oldCount ∧ new.counter.newCount = old.counter.newCount ∧ new.found = old.found

noncomputable def CertifiedRowSystem.Complement.finalWitnessCell {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q : FinalWitnessVerifier F) (old new : ProtocolCell A) :

FinalWitnessVerifier F

One cell of final witness completion.

Equations

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

Instances For

def CertifiedRowSystem.Complement.finalWitnessDone {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (q : FinalWitnessVerifier F) :

Successful final witness completion also requires the witnessed source row to be nonfinal.

Equations

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

Instances For

noncomputable def CertifiedRowSystem.Complement.evalFinalWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) :

FinalWitnessVerifier F → ProtocolRow A → ProtocolRow A → Option (FinalWitnessVerifier F)

Run final witness completion on aligned rows.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.evalFinalWitness_eq_some_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (q out : FinalWitnessVerifier F) (old new : ProtocolRow A) :

evalFinalWitness D q old new = some out ↔ D.evalFinal q.finalState (innerTrack old) = out.finalState ∧ out.pathInner = (q.pathInner && decide (pathTrack old = innerTrack old)) ∧ out.fuelDepth = (q.fuelDepth && decide (fuelTrack old = depthTrack old)) ∧ (countCodec A).evalSucc q.seenSucc (seenCountTrack old) (seenCountTrack new) = some out.seenSucc ∧ (vertexCodec A).evalSucc q.innerSucc (innerTrack old) (innerTrack new) = some out.innerSucc ∧ out.newPhase = scanPhases q.newPhase (List.map (fun (x : ProtocolCell A) => x.phase) new) ∧ out.localOK = (q.localOK && checkPairs finalWitnessLocalOK old new)

Exact componentwise behavior of final witness completion.

def CertifiedRowSystem.Complement.IsFinalWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :

List-level specification of completing one final all-nonfinal witness.

Equations

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

Instances For

theorem CertifiedRowSystem.Complement.IsFinalWitness.persistent_spec {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {old new : ProtocolRow A} (h : IsFinalWitness D old new) :

List.length old = List.length new ∧ HasPhase ProtocolPhase.finalPath old ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ pathTrack new = (vertexCodec A).zeroRow (List.length new) ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ foundTrack new = foundTrack old

Persistent/reset-track projection of final witness completion.