Right-shift soundness for Aho's row checker

One-slot insertions and the binary and push certificates implemented by them.

One-slot right shifts

theorem IndexedGrammar.Aho.WorkTrace.decodePlus1None {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.suffixPlus1) (hcarry : state.history.old1 = some none) (holdEnded : state.oldEnded = true) (hsuffix : ∀ (next : WorkPhase) (hist : WorkHistory g) (old new : Option (WorkSlot g)), WorkEdge g cert WorkPhase.suffixPlus1 next hist old new → next = WorkPhase.suffixPlus1 ∧ plus1Suffix 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-input case of a one-slot right-shift suffix.

theorem IndexedGrammar.Aho.WorkTrace.decodePlus1Some {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.suffixPlus1) (hcarry : state.history.old1 = some (inactive z)) (holdEnded : state.oldEnded = false) (hsuffix : ∀ (next : WorkPhase) (hist : WorkHistory g) (old new : Option (WorkSlot g)), WorkEdge g cert WorkPhase.suffixPlus1 next hist old new → next = WorkPhase.suffixPlus1 ∧ plus1Suffix hist 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 + 1) none ∧ newProjection rows = inactive z :: List.map inactive beta ++ List.replicate k none

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

Completed one-slot insertion inversions

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

theorem IndexedGrammar.Aho.workTraceAccepts_plainPushUse_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.plainPushUse 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.plainPushUse A B f) oldCursor newCursor

theorem IndexedGrammar.Aho.workTraceAccepts_livePushFresh_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.livePushFresh 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.livePushFresh A B f) oldCursor newCursor

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

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

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