Left-shift soundness for Aho's row checker

One-slot deletion and the terminal-match and erasable-index certificates implemented by it.

One-slot left shifts

theorem IndexedGrammar.Aho.WorkTrace.decodeMinus1None {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.suffixMinus1) (hcarry : state.history.new1 = some none) (hnewEnded : state.newEnded = true) (hsuffix : ∀ (next : WorkPhase) (hist : WorkHistory g) (old new : Option (WorkSlot g)), WorkEdge g cert WorkPhase.suffixMinus1 next hist old new → next = WorkPhase.suffixMinus1 ∧ minus1Suffix hist old new) (h : WorkTrace g cert state rows result) : oldProjection rows = List.replicate rows.length none ∧ newProjection rows = List.replicate rows.length none

Decode the exhausted-output case of a one-slot left-shift suffix.

theorem IndexedGrammar.Aho.WorkTrace.decodeMinus1Some {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cert : CompositeCert g} (z : WorkSym g) {state result : WorkScanState g} {rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (hphase : state.phase = WorkPhase.suffixMinus1) (hcarry : state.history.new1 = some (inactive z)) (hnewEnded : state.newEnded = false) (hsuffix : ∀ (next : WorkPhase) (hist : WorkHistory g) (old new : Option (WorkSlot g)), WorkEdge g cert WorkPhase.suffixMinus1 next hist old new → next = WorkPhase.suffixMinus1 ∧ minus1Suffix hist old new) (h : WorkTrace g cert state rows result) (hdone : workScanDone result = true) : ∃ (beta : List (WorkSym g)) (k : ℕ), oldProjection rows = inactive z :: List.map inactive beta ++ List.replicate k none ∧ newProjection rows = List.map inactive beta ++ List.replicate (k + 1) none

Decode the carried-symbol case of a one-slot left-shift suffix.

theorem IndexedGrammar.Aho.workTraceAccepts_matchTerminal_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {a : T} {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g (CompositeCert.matchTerminal 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.matchTerminal a) oldCursor newCursor

theorem IndexedGrammar.Aho.workTraceAccepts_eraseIndex_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {R : CFlag g} {d : IndexMark} {old new : List (Option (WorkSlot g))} (h : WorkTraceAccepts g (CompositeCert.eraseIndex 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.eraseIndex R d) oldCursor newCursor