LanglibPop soundness for Aho's row checker #
Two-slot right shifts and inversion of framed and unframed pop certificates.
Two-slot right shifts used by pop #
The unframed implementation of a pop replaces the focus and erases the immediately
adjacent index. It deliberately uses minus1First, distinct from the framed pop's stage2,
so an accepting scan cannot splice the two implementations.
theorem
IndexedGrammar.Aho.workTraceAccepts_popPlain_sound
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{R : CFlag g}
{d : IndexMark}
{A B : g.nt}
{old new : List (Option (WorkSlot g))}
(h : WorkTraceAccepts g (CompositeCert.popPlain R d A B) 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.popPlain R d A B) oldCursor newCursor
theorem
IndexedGrammar.Aho.workTraceAccepts_popLive_sound
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{R : CFlag g}
{d : IndexMark}
{A B : g.nt}
{old new : List (Option (WorkSlot g))}
(h : WorkTraceAccepts g (CompositeCert.popLive R d A B) 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.popLive R d A B) oldCursor newCursor