Control-effect soundness for Aho's machine

Grammar effects of local, close-crossing, and structural control moves.

Local grammar effects in the execution-order denotation

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.plainBinary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B C : g.nt} (haug : AugBinary g A B C) (h : ExecRep g { left := left, focus := WorkSym.plain A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.plain B, right := WorkSym.plain C :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.plainTerminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A : g.nt} {a : T} (haug : AugTerminal g A a) (h : ExecRep g { left := left, focus := WorkSym.plain A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.terminal a, right := next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.plainPushSkip {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B : g.nt} {f : g.flag} (haug : AugPush g A B f) (h : ExecRep g { left := left, focus := WorkSym.plain A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.plain B, right := next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.plainPushUse {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B : g.nt} {f : g.flag} (haug : AugPush g A B f) (h : ExecRep g { left := left, focus := WorkSym.plain A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.live B, right := WorkSym.index (cflagBase g f) IndexMark.firstPending :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.liveBinaryBoth {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B C : g.nt} (haug : AugBinary g A B C) (h : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.live B, right := WorkSym.live C :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.liveBinaryLeft {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B C : g.nt} (haug : AugBinary g A B C) (h : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.live B, right := WorkSym.plain C :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.liveBinaryRight {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B C : g.nt} (haug : AugBinary g A B C) (h : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.plain B, right := WorkSym.live C :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.livePushFresh {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B : g.nt} {f : g.flag} (haug : AugPush g A B f) (h : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.live B, right := WorkSym.index (cflagBase g f) IndexMark.laterPending :: next :: right } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.livePushCompress {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A B : g.nt} {f : g.flag} {R : CFlag g} {d : IndexMark} (haug : AugPush g A B f) (h : ExecRep g { left := left, focus := WorkSym.live A, right := WorkSym.index R d :: next :: right } form) : ∃ (form' : List g.ISym), ExecRep g { left := left, focus := WorkSym.live B, right := WorkSym.index (cflagComp g (cflagBase g f) R) d :: next :: right } form' ∧ g.Derives form form'

Close-crossing pop effects

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.invertLive {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {A : g.nt} (h : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } form) : ∃ (actual : List g.flag) (stack : BlockDenotation.VisibleStack g) (tailForm : List g.ISym), form = ISym.indexed A actual :: tailForm ∧ RightRep g (next :: right) stack ∧ BlockDenotation.LiveDecorates stack actual ∧ ExecRep g { left := left, focus := next, right := right } tailForm

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.popPlain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha beta gamma : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d : IndexMark} {A B : g.nt} (hfree : IndexFree beta) (hedge : R A B = true) (h : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } form) : ∃ (form' : List g.ISym), ExecRep g { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d, WorkSym.dollar], focus := WorkSym.plain B, right := WorkSym.close :: gamma } form' ∧ g.Derives form form'

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.popLive {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha beta gamma : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d : IndexMark} {A B : g.nt} (hfree : IndexFree beta) (hedge : R A B = true) (hlater : d.later = true) (h : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta ++ WorkSym.index R d :: gamma } form) : ∃ (form' : List g.ISym), ExecRep g { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d, WorkSym.dollar], focus := WorkSym.live B, right := WorkSym.close :: gamma } form' ∧ g.Derives form form'

Structural execution effects

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.matchTerminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {a : T} (h : ExecRep g { left := left, focus := WorkSym.terminal a, right := next :: right } form) : ∃ (restForm : List g.ISym), form = ISym.terminal a :: restForm ∧ ExecRep g { left := left, focus := next, right := right } restForm

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.eraseIndex {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d : IndexMark} (h : ExecRep g { left := left, focus := WorkSym.index R d, right := next :: right } form) : ExecRep g { left := left, focus := next, right := right } form

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.invertClose {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left right : List (WorkSym g)} {form : List g.ISym} (h : ExecRep g { left := left, focus := WorkSym.close, right := right } form) : ∃ (alpha : List (WorkSym g)) (beta : List (WorkSym g)) (Z : WorkSym g), DollarFree beta ∧ left = alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar] ∧ ExecRep g { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ right } form

Generic inversion at a close focus.

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.focus_ne_dollar {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cursor : WorkCursor g} {form : List g.ISym} (h : ExecRep g cursor form) : cursor.focus ≠ WorkSym.dollar

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.right_ne_nil_of_plain_focus {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cursor : WorkCursor g} {form : List g.ISym} {A : g.nt} (h : ExecRep g cursor form) (hfocus : cursor.focus = WorkSym.plain A) : cursor.right ≠ []

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.right_ne_nil_of_index_focus {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {cursor : WorkCursor g} {form : List g.ISym} {R : CFlag g} {d : IndexMark} (h : ExecRep g cursor form) (hfocus : cursor.focus = WorkSym.index R d) : cursor.right ≠ []

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.popPlainErase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha gamma : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d : IndexMark} {A B : g.nt} (hedge : R A B = true) (h : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := WorkSym.index R d :: gamma } form) : ∃ (form' : List g.ISym), ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain B, right := gamma } form' ∧ g.Derives form form'

Consume an adjacent compressed block and erase its representation immediately. Unlike the framed pop, no saved index is needed because this block is owned exclusively by the active task.

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.popLiveErase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha gamma : List (WorkSym g)} {form : List g.ISym} {R : CFlag g} {d : IndexMark} {A B : g.nt} (hedge : R A B = true) (hlater : d.later = true) (h : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := WorkSym.index R d :: gamma } form) : ∃ (form' : List g.ISym), ExecRep g { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live B, right := gamma } form' ∧ g.Derives form form'

Live counterpart of popPlainErase for a lower represented stack that remains active.

theorem IndexedGrammar.Aho.ControlDenotation.ExecRep.returnFrameSound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha beta gamma : List (WorkSym g)} {Z : WorkSym g} {form : List g.ISym} (hZ : Z ≠ WorkSym.dollar) (hfree : DollarFree beta) (h : ExecRep g { left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } form) : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } form