Trace foundations for Aho's logical-slot checker

The work-cursor semantics, canonical-padding inversion, and shared suffix decoder used by the certificate-specific soundness proofs.

noncomputable def IndexedGrammar.Aho.CertWorkStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : CompositeCert g → WorkCursor g → WorkCursor g → Prop

The work-cursor component of CertStep, with input-head metadata omitted.

Equations

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

Canonical padding extracted from a valid trace

theorem IndexedGrammar.Aho.WorkTrace.projections_canonical {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} {result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (h : WorkTrace g cert (initialWorkScan g) rows result) : ∃ (oldSlots : List (WorkSlot g)) (newSlots : List (WorkSlot g)) (kOld : ℕ) (kNew : ℕ), List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows = List.map some oldSlots ++ List.replicate kOld none ∧ List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows = List.map some newSlots ++ List.replicate kNew none

Both projections of a trace from the initial work state have canonical some* none* form.

Generic suffix inversions

def IndexedGrammar.Aho.oldProjection {T✝ : Type} {g : IndexedGrammar T✝} (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) : List (Option (WorkSlot g))

Old-track cells projected from synchronized trace rows.

Equations

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

def IndexedGrammar.Aho.newProjection {T✝ : Type} {g : IndexedGrammar T✝} (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) : List (Option (WorkSlot g))

New-track cells projected from synchronized trace rows.

Equations

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

theorem IndexedGrammar.Aho.WorkTrace.decodeSuffixSame {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} {state result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (hphase : state.phase = WorkPhase.suffixSame) (hsuffix : ∀ (next : WorkPhase) (hist : WorkHistory g) (old new : Option (WorkSlot g)), WorkEdge g cert WorkPhase.suffixSame next hist old new → next = WorkPhase.suffixSame ∧ sameSuffix old new) (h : WorkTrace g cert state rows result) (hdone : workScanDone result = true) : ∃ (beta : List (WorkSym g)) (k : ℕ), oldProjection rows = List.map inactive beta ++ List.replicate k none ∧ newProjection rows = List.map inactive beta ++ List.replicate k none

In the equal-suffix phase, the remaining non-padding symbols are the same inactive word on both tracks.