LanglibCanonical executable reachability witnesses #
Every member of a bounded reachable layer has an exactly fuel-indexed padded path. This module turns that path into an executable sequence of protocol actions, both in an inductive-counting inner scan and in the final all-nonfinal scan.
theorem
CertifiedRowSystem.Complement.reachableWitness_run
{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}
{input : List I}
{old : ProtocolRow A}
{depth oldCount newCount outerIndex innerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : ChooseInnerInvariant D input old depth oldCount newCount outerIndex innerIndex selected)
(hreachable : ⟨innerIndex, ⋯⟩ ∈ protocolReached D input depth)
:
∃ (new : ProtocolRow A),
Relation.ReflTransGen (ProtocolStep D) old new ∧ (innerIndex + 1 < Fintype.card A ^ input.length ∧ ChooseInnerInvariant D input new depth oldCount newCount outerIndex (innerIndex + 1)
(insert ⟨innerIndex, ⋯⟩ selected) ∨ innerIndex + 1 = Fintype.card A ^ input.length ∧ FinishOuterInvariant D input new depth oldCount newCount outerIndex (insert ⟨innerIndex, ⋯⟩ selected))
A reachable current inner rank has a complete executable witness run. The run
starts the bounded witness, realizes an exactly depth-step padded path, and commits
the current rank to the inner-scan transcript.
theorem
CertifiedRowSystem.Complement.finalReachableWitness_run
{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}
{input : List I}
{old : ProtocolRow A}
{depth count innerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : FinalChooseInvariant D input old depth count innerIndex selected)
(hreachable : ⟨innerIndex, ⋯⟩ ∈ protocolReached D input depth)
(hnonfinal : ¬rankFinal D input.length ⟨innerIndex, ⋯⟩)
:
∃ (new : ProtocolRow A),
Relation.ReflTransGen (ProtocolStep D) old new ∧ (innerIndex + 1 < Fintype.card A ^ input.length ∧ FinalChooseInvariant D input new depth count (innerIndex + 1) (insert ⟨innerIndex, ⋯⟩ selected) ∨ innerIndex + 1 = Fintype.card A ^ input.length ∧ FinalFinishInvariant D input new depth count (insert ⟨innerIndex, ⋯⟩ selected))
The final scan has the analogous complete executable witness run. Its final completion action additionally checks the current reachable row is nonfinal.