Atomic protected-block execution

A protected task whose current parse has no productive event at depth zero may consume its entire first represented block at once. The exact continuation transport then supplies a strictly smaller residual parse; opening and closing the corresponding scheduler frame preserves both the ghost ownership invariant and the resource credit equality.

theorem IndexedGrammar.Aho.ScheduleBlockLayout.input_ne_nil_of_flags_ne {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {flags : List g.flag} {blocks : List (List g.flag)} {owners : List (Fin (10 * input.length))} {word used : List (ScheduleAtom g input)} (layout : ScheduleBlockLayout g input flags blocks owners word used) (hne : flags ≠ []) : word ≠ []

A nonempty concrete layout prefix exposes at least one input atom.

theorem IndexedGrammar.Aho.ScheduleBlockLayout.output_ne_nil_of_flags_ne {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {flags : List g.flag} {blocks : List (List g.flag)} {owners : List (Fin (10 * input.length))} {word used : List (ScheduleAtom g input)} (layout : ScheduleBlockLayout g input flags blocks owners word used) (hne : flags ≠ []) : used ≠ []

Marking the selected blocks of a nonempty layout likewise leaves a nonempty output word.

theorem IndexedGrammar.Aho.protectedScheduleRun_atomicPop {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (hpositive : ∀ d ∈ parse.eventDepths, 0 < d) (ih : ∀ {B : g.nt} {residualStack : List g.flag} (residual : g.NFParse B residualStack w), residual.nodeCount < parse.nodeCount → OrdinaryScheduleRuns residual) : ProtectedScheduleRun parse

Execute the first protected block whenever depth zero is not a productive event. This is the common protected-mode step used after structural pops (and after unary normalization): it does not depend on the syntactic constructor at the root of the parse.

theorem IndexedGrammar.Aho.protectedScheduleRun_pushFresh {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (hparentZero : 0 ∈ (NFParse.push hr hlhs hc hrhs rest).eventDepths) (restOverlay : OverlayScheduleRun rest) : ProtectedScheduleRun (NFParse.push hr hlhs hc hrhs rest)

A push above a protected stack starts a fresh adjacent overlay block. The protected layout remains unchanged below it, while the overlay runner owns and eventually erases the singleton.

theorem IndexedGrammar.Aho.protectedScheduleRun_terminal_false {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) : ProtectedScheduleRun (NFParse.terminal hr hlhs hc hrhs)

A terminal parse never enters protected mode.