Replacement and prefix soundness for Aho's row checker

Inversion of nonproductive and productive prefixes, one-symbol replacement, and two-symbol replacement.

Nonproductive replacement

theorem IndexedGrammar.Aho.workTraceAccepts_plainPushSkip_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g (CompositeCert.plainPushSkip A B f) old new) : ∃ (oldCursor : WorkCursor g) (newCursor : WorkCursor g) (kOld : ℕ) (kNew : ℕ), old = List.map some oldCursor.slots ++ List.replicate kOld none ∧ new = List.map some newCursor.slots ++ List.replicate kNew none ∧ CertWorkStep g (CompositeCert.plainPushSkip A B f) oldCursor newCursor

Soundness of the logical checker for the skipped-push replacement.

Productive prefix inversion

def IndexedGrammar.Aho.CopiedHistory {T✝ : Type} {g : IndexedGrammar T✝} (alpha : List (WorkSym g)) (hist : WorkHistory g) : Prop

The scan history agrees with the last copied symbol of a prefix, when one exists.

Equations

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

def IndexedGrammar.Aho.ProductivePrefixInv {T✝ : Type} {g : IndexedGrammar T✝} (alpha : List (WorkSym g)) (state : WorkScanState g) : Prop

Invariant carried while a productive prefix is copied and selectively marked.

Equations

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

theorem IndexedGrammar.Aho.productivePrefixInv_initial {T : Type} (g : IndexedGrammar T) : ProductivePrefixInv [] (initialWorkScan g)

The initial work scan satisfies the productive-prefix invariant for the empty prefix.

theorem IndexedGrammar.Aho.WorkTrace.splitProductivePrefix {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} (hproductive : cert.productive = true) {alpha : List (WorkSym g)} {state result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (hinv : ProductivePrefixInv alpha state) (h : WorkTrace g cert state rows result) (hdone : workScanDone result = true) : ∃ (delta : List (WorkSym g)) (newDelta : List (WorkSym g)) (rest : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (stage : WorkScanState g), CertEnabled g cert ∧ markProductivePrefix (alpha ++ delta) = alpha ++ newDelta ∧ oldProjection rows = List.map inactive delta ++ [inactive WorkSym.dollar] ++ oldProjection rest ∧ newProjection rows = List.map inactive newDelta ++ [inactive WorkSym.dollar] ++ newProjection rest ∧ stage.phase = WorkPhase.stage1 ∧ WorkTrace g cert stage rest result

Split a productive scan immediately after its $ boundary, retaining the exact markProductivePrefix relation on the scanned prefix.

theorem IndexedGrammar.Aho.workTraceAccepts_plainTerminal_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {a : T} {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g (CompositeCert.plainTerminal A a) old new) : ∃ (oldCursor : WorkCursor g) (newCursor : WorkCursor g) (kOld : ℕ) (kNew : ℕ), old = List.map some oldCursor.slots ++ List.replicate kOld none ∧ new = List.map some newCursor.slots ++ List.replicate kNew none ∧ CertWorkStep g (CompositeCert.plainTerminal A a) oldCursor newCursor

Soundness of the logical checker for a productive terminal replacement.

Shared nonproductive-prefix split

theorem IndexedGrammar.Aho.WorkTrace.splitNonproductivePrefix {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} (hproductive : cert.productive = false) {state result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (hphase : state.phase = WorkPhase.prefix) (h : WorkTrace g cert state rows result) (hdone : workScanDone result = true) : ∃ (alpha : List (WorkSym g)) (rest : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (stage : WorkScanState g), CertEnabled g cert ∧ oldProjection rows = List.map inactive alpha ++ [inactive WorkSym.dollar] ++ oldProjection rest ∧ newProjection rows = List.map inactive alpha ++ [inactive WorkSym.dollar] ++ newProjection rest ∧ stage.phase = WorkPhase.stage1 ∧ WorkTrace g cert stage rest result

Split a nonproductive scan at its $ boundary, preserving the copied prefix exactly.

Two-symbol replacement

theorem IndexedGrammar.Aho.workTraceAccepts_livePushCompress_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {R : CFlag g} {d : IndexMark} {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g (CompositeCert.livePushCompress A B f R d) old new) : ∃ (oldCursor : WorkCursor g) (newCursor : WorkCursor g) (kOld : ℕ) (kNew : ℕ), old = List.map some oldCursor.slots ++ List.replicate kOld none ∧ new = List.map some newCursor.slots ++ List.replicate kNew none ∧ CertWorkStep g (CompositeCert.livePushCompress A B f R d) oldCursor newCursor