Aho scheduler state and invariants

Ghost tasks, cursor invariants, schedule reachability, and canonical endpoints.

Ghost annotations and the global scheduling invariant

inductive IndexedGrammar.Aho.TaskMode {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : Type

Whether a pending parse task must retain the compressed stack to its right. A plain task does not consume the top inherited occurrence; prefix closure then says it consumes no inherited occurrence. A live task does consume the top occurrence and must be scheduled against the next compressed-index token.

• plain {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} (unused : ¬p.ConsumesAt 0) : TaskMode p
• live {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} (used : p.ConsumesAt 0) : TaskMode p

structure IndexedGrammar.Aho.ScheduleTask {T : Type} (g : IndexedGrammar T) (input : List T) : Type

A pending parse task, together with the terminal position which owns its work-tape payload. The scheduler uses the left endpoint of the task's nonempty yield interval as owner.

• A : g.nt
• stack : List g.flag
• yield : List T
• parse : g.NFParse self.A self.stack self.yield
• pre : List T
• post : List T
• input_eq : input = self.pre ++ self.yield ++ self.post
• mode : TaskMode self.parse

def IndexedGrammar.Aho.ScheduleTask.owner {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) : Fin input.length

The first terminal position in a pending task's nonempty yield.

Equations

• task.owner = ⟨task.pre.length, ⋯⟩

def IndexedGrammar.Aho.ScheduleTask.workSym {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) : WorkSym g

Erase the ghost parse and retain the finite work symbol seen by the machine.

Equations

• One or more equations did not get rendered due to their size.

structure IndexedGrammar.Aho.ScheduleIndex {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : Type

A compressed-index occurrence with its concrete denotation and terminal-position owner. Only the finite relation and mark survive ghost erasure.

• flags : List g.flag
• relation : CFlag g
• mark : IndexMark
• denotes : CFlag.Denotes g self.flags self.relation
• owner : Fin (10 * input.length)

inductive IndexedGrammar.Aho.ScheduleAtom {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : Type

Ghost-annotated symbols used by the parse-directed scheduler.

• task {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleTask g input → ScheduleAtom g input
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : Fin input.length → T → ScheduleAtom g input
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleIndex g input → ScheduleAtom g input
• dollar {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input
• close {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : Fin (10 * input.length) → ScheduleAtom g input
• hash {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input

def IndexedGrammar.Aho.ScheduleAtom.workSym {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input → WorkSym g

Erase all scheduler-only data.

Equations

• (IndexedGrammar.Aho.ScheduleAtom.task t).workSym = t.workSym
• (IndexedGrammar.Aho.ScheduleAtom.terminal a a_1).workSym = IndexedGrammar.Aho.WorkSym.terminal a_1
• (IndexedGrammar.Aho.ScheduleAtom.index idx).workSym = IndexedGrammar.Aho.WorkSym.index idx.relation idx.mark
• IndexedGrammar.Aho.ScheduleAtom.dollar.workSym = IndexedGrammar.Aho.WorkSym.dollar
• (IndexedGrammar.Aho.ScheduleAtom.close a).workSym = IndexedGrammar.Aho.WorkSym.close
• IndexedGrammar.Aho.ScheduleAtom.hash.workSym = IndexedGrammar.Aho.WorkSym.hash

def IndexedGrammar.Aho.ScheduleAtom.taskOwner? {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input → Option (Fin input.length)

Owners of task/terminal payloads.

Equations

• (IndexedGrammar.Aho.ScheduleAtom.task t).taskOwner? = some t.owner
• (IndexedGrammar.Aho.ScheduleAtom.terminal owner a).taskOwner? = some owner
• x✝.taskOwner? = none

def IndexedGrammar.Aho.ScheduleAtom.indexOwner? {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input → Option (Fin (10 * input.length))

Owners of compressed-index payloads.

Equations

• (IndexedGrammar.Aho.ScheduleAtom.index idx).indexOwner? = some idx.owner
• x✝.indexOwner? = none

def IndexedGrammar.Aho.ScheduleAtom.closeOwner? {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} : ScheduleAtom g input → Option (Fin (10 * input.length))

The selected persistent-index owner charged by an open frame.

Equations

• (IndexedGrammar.Aho.ScheduleAtom.close owner).closeOwner? = some owner
• x✝.closeOwner? = none

structure IndexedGrammar.Aho.ScheduleCursor {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : Type

A zipper over the ghost-annotated scheduler word.

• left : List (ScheduleAtom g input)
• focus : ScheduleAtom g input
• right : List (ScheduleAtom g input)

def IndexedGrammar.Aho.ScheduleCursor.word {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : List (ScheduleAtom g input)

The complete ghost word.

Equations

• cursor.word = cursor.left ++ cursor.focus :: cursor.right

def IndexedGrammar.Aho.ScheduleCursor.erase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : WorkCursor g

Erase a ghost cursor to the finite machine cursor.

Equations

• cursor.erase = { left := List.map IndexedGrammar.Aho.ScheduleAtom.workSym cursor.left, focus := cursor.focus.workSym, right := List.map IndexedGrammar.Aho.ScheduleAtom.workSym cursor.right }

@[simp]

theorem IndexedGrammar.Aho.ScheduleCursor.erase_word {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : cursor.erase.word = List.map ScheduleAtom.workSym cursor.word

@[simp]

theorem IndexedGrammar.Aho.ScheduleCursor.erase_word_length {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : cursor.erase.word.length = cursor.word.length

def IndexedGrammar.Aho.ScheduleCursor.taskOwners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : List (Fin input.length)

Task/terminal owners present in the cursor.

Equations

• cursor.taskOwners = List.filterMap IndexedGrammar.Aho.ScheduleAtom.taskOwner? cursor.word

def IndexedGrammar.Aho.ScheduleCursor.indexOwners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : List (Fin (10 * input.length))

Compressed-index owners present in the cursor.

Equations

• cursor.indexOwners = List.filterMap IndexedGrammar.Aho.ScheduleAtom.indexOwner? cursor.word

def IndexedGrammar.Aho.ScheduleCursor.frameOwners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : List (Fin (10 * input.length))

Persistent-index owners currently charged by open $/close frames.

Equations

• cursor.frameOwners = List.filterMap IndexedGrammar.Aho.ScheduleAtom.closeOwner? cursor.word

def IndexedGrammar.Aho.ScheduleCursor.frameCount {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : ℕ

Number of currently open $/close frames.

Equations

• cursor.frameCount = cursor.frameOwners.length

structure IndexedGrammar.Aho.ScheduleInvariant {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (cursor : ScheduleCursor g input) : Prop

Global invariant maintained by the compressed scheduler. Tasks are charged to terminal positions, while persistent physical blocks satisfy the 6|input| reusable-owner cap. shape_bound accounts for one task/index square per payload, two delimiters per open frame, and the fixed outer $/# pair.

• taskOwners_nodup : cursor.taskOwners.Nodup
• indexOwners_nodup : cursor.indexOwners.Nodup
• frameOwners_nodup : cursor.frameOwners.Nodup
• frameOwners_subset_indexOwners : cursor.frameOwners ⊆ cursor.indexOwners
• taskCount_le : cursor.taskOwners.length ≤ input.length
• indexCount_le : cursor.indexOwners.length ≤ 6 * input.length
• shape_bound : cursor.word.length ≤ cursor.taskOwners.length + cursor.indexOwners.length + 2 * cursor.frameCount + 2

theorem IndexedGrammar.Aho.ScheduleInvariant.of_owner_nodup {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (htasks : cursor.taskOwners.Nodup) (hindices : cursor.indexOwners.Nodup) (hframes : cursor.frameOwners.Nodup) (hframeSubset : cursor.frameOwners ⊆ cursor.indexOwners) (hindexCount : cursor.indexOwners.length ≤ 6 * input.length) (hshape : cursor.word.length ≤ cursor.taskOwners.length + cursor.indexOwners.length + 2 * cursor.frameCount + 2) : ScheduleInvariant cursor

Construct the global invariant from its qualitative ownership facts, the explicit persistent owner bound, and the delimiter-shape bound. Unlike task owners, persistent owners live in an ambient carrier larger than their reusable bank, so their 6|input| bound is supplied explicitly.

theorem IndexedGrammar.Aho.ScheduleInvariant.frameCount_le_indexCount {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (hinv : ScheduleInvariant cursor) : cursor.frameCount ≤ cursor.indexOwners.length

Distinct open frames inject into the persistent indices which own them.

theorem IndexedGrammar.Aho.ScheduleInvariant.word_length_le_twenty_one_mul {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (hinv : ScheduleInvariant cursor) (hinput : 0 < input.length) : cursor.word.length ≤ 21 * input.length

The accounting invariant implies a uniform twenty-one-squares-per-input-symbol bound.

theorem IndexedGrammar.Aho.ScheduleInvariant.erase_within {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (hinv : ScheduleInvariant cursor) (hinput : 0 < input.length) (inputPos : ℕ) : Config.Within (21 * input.length) { inputPos := inputPos, work := cursor.erase }

Erasing scheduler annotations preserves the bound needed by BoundedReaches.

theorem IndexedGrammar.Aho.ScheduleInvariant.erase_within_max_two {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {cursor : ScheduleCursor g input} (hinv : ScheduleInvariant cursor) (inputPos : ℕ) : Config.Within (max 2 (21 * input.length)) { inputPos := inputPos, work := cursor.erase }

The two fixed boundary cells also cover the vacuous zero-length ambient carrier.

Invariant-carrying schedule witnesses

structure IndexedGrammar.Aho.ScheduleState {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : Type

A scheduler state consists of a ghost cursor, its input position, and the global ownership invariant. Erasing it gives an ordinary composite-machine configuration.

• inputPos : ℕ
• inputPos_le : self.inputPos ≤ input.length
• cursor : ScheduleCursor g input
• invariant : ScheduleInvariant self.cursor

def IndexedGrammar.Aho.ScheduleState.config {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (state : ScheduleState g input) : Config g

Forget all scheduler annotations.

Equations

• state.config = { inputPos := state.inputPos, work := state.cursor.erase }

theorem IndexedGrammar.Aho.ScheduleState.config_within {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (state : ScheduleState g input) (hinput : 0 < input.length) : Config.Within (21 * input.length) state.config

Every scheduler state is inside the target tape bound.

def IndexedGrammar.Aho.ScheduleStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (state state' : ScheduleState g input) : Prop

A scheduler edge erases to one composite-machine edge. Ownership data is carried by the endpoint states, so a schedule is bounded by construction.

Equations

• IndexedGrammar.Aho.ScheduleStep g input state state' = IndexedGrammar.Aho.CompositeStep g input state.config state'.config

def IndexedGrammar.Aho.ScheduleReaches {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (state state' : ScheduleState g input) : Prop

An invariant-carrying finite schedule, recorded extensionally at the erased machine configurations. Ghost-owner relabellings therefore cost no executable step.

Equations

• IndexedGrammar.Aho.ScheduleReaches g input state state' = IndexedGrammar.Aho.BoundedReaches g input (max 2 (21 * input.length)) state.config state'.config

theorem IndexedGrammar.Aho.ScheduleReaches.refl {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (state : ScheduleState g input) : ScheduleReaches g input state state

The empty schedule at an invariant-carrying state.

theorem IndexedGrammar.Aho.ScheduleReaches.single {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {state state' : ScheduleState g input} (step : CompositeStep g input state.config state'.config) : ScheduleReaches g input state state'

Package one verified composite-machine edge between invariant-carrying scheduler states.

theorem IndexedGrammar.Aho.ScheduleReaches.trans {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {state₁ state₂ state₃ : ScheduleState g input} (first : ScheduleReaches g input state₁ state₂) (second : ScheduleReaches g input state₂ state₃) : ScheduleReaches g input state₁ state₃

Concatenate two invariant-carrying schedules at their common scheduler state.

theorem IndexedGrammar.Aho.ScheduleReaches.congr_config {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {state state' relabelled relabelled' : ScheduleState g input} (schedule : ScheduleReaches g input state state') (hstart : relabelled.config = state.config) (hend : relabelled'.config = state'.config) : ScheduleReaches g input relabelled relabelled'

Change either endpoint's ghost annotations without changing its erased configuration.

theorem IndexedGrammar.Aho.ScheduleReaches.toBoundedReaches {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {state state' : ScheduleState g input} (hinput : 0 < input.length) (schedule : ScheduleReaches g input state state') : BoundedReaches g input (21 * input.length) state.config state'.config

Erasing an invariant-carrying schedule produces BoundedReaches directly.

Canonical endpoints

def IndexedGrammar.Aho.initialScheduleTask {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleTask g input

The initial pending task is plain because its inherited stack is empty.

Equations

• IndexedGrammar.Aho.initialScheduleTask parse = { A := g.initial, stack := [], yield := input, parse := parse, pre := [], post := [], input_eq := ⋯, mode := IndexedGrammar.Aho.TaskMode.plain ⋯ }

def IndexedGrammar.Aho.initialScheduleCursor {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleCursor g input

Ghost cursor for Aho's initial $ S # configuration.

Equations

• One or more equations did not get rendered due to their size.

def IndexedGrammar.Aho.finalScheduleCursor {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : ScheduleCursor g input

Ghost cursor for the final $ # configuration.

Equations

• IndexedGrammar.Aho.finalScheduleCursor g input = { left := [IndexedGrammar.Aho.ScheduleAtom.dollar], focus := IndexedGrammar.Aho.ScheduleAtom.hash, right := [] }

theorem IndexedGrammar.Aho.initialScheduleCursor_invariant {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleInvariant (initialScheduleCursor parse)

theorem IndexedGrammar.Aho.finalScheduleCursor_invariant {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) : ScheduleInvariant (finalScheduleCursor g input)

def IndexedGrammar.Aho.initialScheduleState {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleState g input

Canonical invariant-carrying initial state.

Equations

• IndexedGrammar.Aho.initialScheduleState parse = { inputPos := 0, inputPos_le := ⋯, cursor := IndexedGrammar.Aho.initialScheduleCursor parse, invariant := ⋯ }

def IndexedGrammar.Aho.finalScheduleState {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : ScheduleState g input

Canonical invariant-carrying accepting state.

Equations

• IndexedGrammar.Aho.finalScheduleState g input = { inputPos := input.length, inputPos_le := ⋯, cursor := IndexedGrammar.Aho.finalScheduleCursor g input, invariant := ⋯ }

@[simp]

theorem IndexedGrammar.Aho.initialScheduleState_config {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : (initialScheduleState parse).config = initialConfig g

@[simp]

theorem IndexedGrammar.Aho.finalScheduleState_config {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) : (finalScheduleState g input).config = finalConfig g input.length

def IndexedGrammar.Aho.ParseScheduled {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : Prop

The exact remaining semantic obligation: construct an ownership-preserving schedule from a concrete parse.

Equations

• IndexedGrammar.Aho.ParseScheduled parse = IndexedGrammar.Aho.ScheduleReaches g input (IndexedGrammar.Aho.initialScheduleState parse) (IndexedGrammar.Aho.finalScheduleState g input)

theorem IndexedGrammar.Aho.complete_bounded_of_parseScheduled {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) (schedule : ParseScheduled parse) : BoundedReaches g input (21 * input.length) (initialConfig g) (finalConfig g input.length)

Once the parse-directed schedule is constructed, its endpoint and ownership invariants give full bounded completeness without any additional accounting argument.