Logical-slot traces for Aho's row checker

This module gives the proof-relevant trace relation behind the finite checker. A trace records every aligned old/new logical slot and scan phase, enforces canonical some* none* padding on both tracks, and connects accepting traces to the executable slot evaluator.

Logical-slot traces

def IndexedGrammar.Aho.advanceWorkState {T✝ : Type} {g : IndexedGrammar T✝} (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) : WorkScanState g

Equations

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

def IndexedGrammar.Aho.ValidWorkEdge {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) : Prop

Equations

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

@[simp]

theorem IndexedGrammar.Aho.workSlotStep_of_valid {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) (h : ValidWorkEdge g cert state old new next) : workSlotStep g cert state old new next = advanceWorkState state old new next

theorem IndexedGrammar.Aho.valid_of_workSlotStep_phase_ne_dead {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) (h : (workSlotStep g cert state old new next).phase ≠ WorkPhase.dead) : ValidWorkEdge g cert state old new next

@[simp]

theorem IndexedGrammar.Aho.workSlotStep_phase_dead {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) (h : state.phase = WorkPhase.dead) : (workSlotStep g cert state old new next).phase = WorkPhase.dead

theorem IndexedGrammar.Aho.evalWorkSlots_phase_dead {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : state.phase = WorkPhase.dead) : (evalWorkSlots g cert state (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.2) rows)).phase = WorkPhase.dead

inductive IndexedGrammar.Aho.PaddingStream {T : Type} (g : IndexedGrammar T) : Bool → List (Option (WorkSlot g)) → Prop

The exact some* none* discipline enforced independently on each padded work track.

• nil {T : Type} {g : IndexedGrammar T} (ended : Bool) : PaddingStream g ended []
• cons {T : Type} {g : IndexedGrammar T} {ended : Bool} {x : Option (WorkSlot g)} {xs : List (Option (WorkSlot g))} (hhead : paddingOK ended x) (htail : PaddingStream g (ended || x.isNone) xs) : PaddingStream g ended (x :: xs)

theorem IndexedGrammar.Aho.paddingStream_replicate_none {T : Type} (g : IndexedGrammar T) (ended : Bool) (k : ℕ) : PaddingStream g ended (List.replicate k none)

theorem IndexedGrammar.Aho.paddingStream_inactive_append_none {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) (k : ℕ) : PaddingStream g false (List.map inactive xs ++ List.replicate k none)

theorem IndexedGrammar.Aho.PaddingStream.tail {T : Type} {g : IndexedGrammar T} {ended : Bool} {x : Option (WorkSlot g)} {xs : List (Option (WorkSlot g))} (h : PaddingStream g ended (x :: xs)) : PaddingStream g (ended || x.isNone) xs

theorem IndexedGrammar.Aho.PaddingStream.head {T : Type} {g : IndexedGrammar T} {ended : Bool} {x : Option (WorkSlot g)} {xs : List (Option (WorkSlot g))} (h : PaddingStream g ended (x :: xs)) : paddingOK ended x

theorem IndexedGrammar.Aho.PaddingStream.append_none {T : Type} {g : IndexedGrammar T} {ended : Bool} {xs : List (Option (WorkSlot g))} (h : PaddingStream g ended xs) : PaddingStream g ended (xs ++ [none])

inductive IndexedGrammar.Aho.WorkTrace {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) : WorkScanState g → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) → WorkScanState g → Prop

A successful aligned slot trace, retaining every local edge fact needed for inversion.

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} (state : WorkScanState g) : WorkTrace g cert state [] state
• cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} {state : WorkScanState g} {old new : Option (WorkSlot g)} {next : WorkPhase} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} {result : WorkScanState g} (hedge : ValidWorkEdge g cert state old new next) (htail : WorkTrace g cert (advanceWorkState state old new next) rows result) : WorkTrace g cert state ((old, new, next) :: rows) result

theorem IndexedGrammar.Aho.evalWorkSlots_of_trace {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) {state result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (h : WorkTrace g cert state rows result) : evalWorkSlots g cert state (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.2) rows) = result

theorem IndexedGrammar.Aho.trace_of_evalWorkSlots_phase_ne_dead {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (hne : (evalWorkSlots g cert state (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.2) rows)).phase ≠ WorkPhase.dead) : WorkTrace g cert state rows (evalWorkSlots g cert state (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.2) rows))

def IndexedGrammar.Aho.WorkTraceAccepts {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (old new : List (Option (WorkSlot g))) : Prop

Acceptance of two already-aligned logical-slot streams.

Equations

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

theorem IndexedGrammar.Aho.evalWorkSlots_of_accepts {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g cert old new) : ∃ (phases : List WorkPhase) (result : WorkScanState g), phases.length = old.length ∧ new.length = old.length ∧ evalWorkSlots g cert (initialWorkScan g) old new phases = result ∧ workScanDone result = true