Input-head safety for Aho's machine

Every certified composite transition preserves the invariant that the input position remains within the supplied input.

Input-head safety

def IndexedGrammar.Aho.Config.InputWithin {T : Type} {g : IndexedGrammar T} (input : List T) (c : Config g) : Prop

The input cursor has not moved beyond the fixed input word.

Equations

• IndexedGrammar.Aho.Config.InputWithin input c = (c.inputPos ≤ input.length)

theorem IndexedGrammar.Aho.initialConfig_inputWithin {T : Type} (g : IndexedGrammar T) (input : List T) : Config.InputWithin input (initialConfig g)

theorem IndexedGrammar.Aho.certStep_preserves_inputWithin {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) (cert : CompositeCert g) {c c' : Config g} (hstep : CertStep g input cert c c') (hin : Config.InputWithin input c) : Config.InputWithin input c'

Every certified move preserves input-head safety. The sole advancing move carries a successful getElem? check, which proves that the old cursor is strictly inside the input.

theorem IndexedGrammar.Aho.compositeStep_preserves_inputWithin {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {c c' : Config g} (hstep : CompositeStep g input c c') (hin : Config.InputWithin input c) : Config.InputWithin input c'