Input-track soundness for Aho's padded rows

The work-track checker is independent of the immutable input letters and their consumed-prefix bits. This file isolates the latter component. It shows that the finite input scan accepts exactly a stationary input head for every structural certificate, and exactly one checked input advance for matchTerminal.

def IndexedGrammar.Aho.encodeRunCellsFrom {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) : List T → List (RunCell g)

The running cells underlying encodeRunRowFrom, before applying RowCell.run.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.encodeRunCellsFrom g work inputPos cell [] = []

def IndexedGrammar.Aho.encodeRunCells {T : Type} (g : IndexedGrammar T) (w : List T) (c : Config g) : List (RunCell g)

The running cells underlying a packed configuration row.

Equations

• IndexedGrammar.Aho.encodeRunCells g w c = IndexedGrammar.Aho.encodeRunCellsFrom g c.work.slots c.inputPos 0 w

@[simp]

theorem IndexedGrammar.Aho.encodeRunRowFrom_eq_map_run {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) (w : List T) : encodeRunRowFrom g work inputPos cell w = List.map RowCell.run (encodeRunCellsFrom g work inputPos cell w)

@[simp]

theorem IndexedGrammar.Aho.encodeRunRow_eq_map_run {T : Type} (g : IndexedGrammar T) (w : List T) (c : Config g) : encodeRunRow g w c = List.map RowCell.run (encodeRunCells g w c)

def IndexedGrammar.Aho.inputPositionCells {T : Type} (g : IndexedGrammar T) (inputPos : ℕ) : List T → List (RunCell g)

A block-independent presentation of a running input track whose first inputPos cells have their consumed bit set.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.inputPositionCells g inputPos [] = []

theorem IndexedGrammar.Aho.evalInputBlocks_encodeRunCells_eq_positionCells {T : Type} (g : IndexedGrammar T) (cert : CompositeCert g) (phase : InputPhase) (input : List T) (old new : Config g) : evalInputBlocks cert phase (encodeRunCells g input old) (encodeRunCells g input new) = evalInputBlocks cert phase (inputPositionCells g old.inputPos input) (inputPositionCells g new.inputPos input)

The input scan of an encoded row depends only on the input word and the two head positions, not on either packed work word.

def IndexedGrammar.Aho.CompositeCert.InputAction {T : Type} {g : IndexedGrammar T} (cert : CompositeCert g) (input : List T) (oldPos newPos : ℕ) : Prop

The input-position effect prescribed by a composite certificate.

Equations

• (IndexedGrammar.Aho.CompositeCert.matchTerminal a).InputAction input oldPos newPos = (input[oldPos]? = some a ∧ newPos = oldPos + 1)
• cert.InputAction input oldPos newPos = (newPos = oldPos)

theorem IndexedGrammar.Aho.certStep_inputAction {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) (cert : CompositeCert g) {old new : Config g} (hstep : CertStep g input cert old new) : cert.InputAction input old.inputPos new.inputPos

Every semantic certificate step has the input-head action checked by the independent input track.

Decoding arbitrary accepted physical input tracks

def IndexedGrammar.Aho.RunCell.clearBlock {T : Type} (g : IndexedGrammar T) (cell : RunCell g) : RunCell g

Erase the packed work block while retaining exactly the input letter and consumed bit.

Equations

• IndexedGrammar.Aho.RunCell.clearBlock g cell = { input := cell.input, consumed := cell.consumed, block := IndexedGrammar.Aho.blankBlock g }

def IndexedGrammar.Aho.clearInputBlocks {T : Type} (g : IndexedGrammar T) (row : List (RunCell g)) : List (RunCell g)

Block-independent view of a physical running row.

Equations

• IndexedGrammar.Aho.clearInputBlocks g row = List.map (IndexedGrammar.Aho.RunCell.clearBlock g) row

@[simp]

theorem IndexedGrammar.Aho.clearInputBlocks_length {T : Type} (g : IndexedGrammar T) (row : List (RunCell g)) : (clearInputBlocks g row).length = row.length

@[simp]

theorem IndexedGrammar.Aho.inputPositionCells_length {T : Type} (g : IndexedGrammar T) (pos : ℕ) (input : List T) : (inputPositionCells g pos input).length = input.length

theorem IndexedGrammar.Aho.clearInputBlocks_encodeRunCellsFrom {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (pos cell : ℕ) (input : List T) : clearInputBlocks g (encodeRunCellsFrom g work pos cell input) = inputPositionCells g (pos - cell) input

Clearing blocks from a genuine encoded row gives its canonical input-position track.

@[simp]

theorem IndexedGrammar.Aho.clearInputBlocks_encodeRunCells {T : Type} (g : IndexedGrammar T) (input : List T) (c : Config g) : clearInputBlocks g (encodeRunCells g input c) = inputPositionCells g c.inputPos input

@[simp]

theorem IndexedGrammar.Aho.runBlocks_map_runCells {T✝ : Type} {g : IndexedGrammar T✝} (cells : List (RunCell g)) : runBlocks (List.map RowCell.run cells) = some (List.map RunCell.block cells)

theorem IndexedGrammar.Aho.map_block_encodeRunCellsFrom {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (pos cell : ℕ) (input : List T) : List.map RunCell.block (encodeRunCellsFrom g work pos cell input) = packedBlockList g work cell input.length

Packed work blocks underlying an encoded list of running cells.

theorem IndexedGrammar.Aho.map_block_encodeRunCells {T : Type} (g : IndexedGrammar T) (input : List T) (c : Config g) : List.map RunCell.block (encodeRunCells g input c) = packedBlockList g c.work.slots 0 input.length

theorem IndexedGrammar.Aho.runCells_eq_of_clearInputBlocks_eq_of_map_block_eq {T : Type} (g : IndexedGrammar T) {old new : List (RunCell g)} (hclear : clearInputBlocks g old = clearInputBlocks g new) (hblocks : List.map RunCell.block old = List.map RunCell.block new) : old = new

Running rows are determined by their input/consumption projection and their packed blocks.

theorem IndexedGrammar.Aho.eq_encodeRunCellsFrom_of_clear_of_blocks {T : Type} (g : IndexedGrammar T) (row : List (RunCell g)) (work : List (WorkSlot g)) (pos cell : ℕ) (input : List T) (hclear : clearInputBlocks g row = inputPositionCells g (pos - cell) input) (hblocks : List.map RunCell.block row = packedBlockList g work cell input.length) : row = encodeRunCellsFrom g work pos cell input

Combine an input-track decoder with a packed-block decoder to reconstruct the exact running cells of an encoded work cursor.

theorem IndexedGrammar.Aho.evalInputBlocks_decode {T : Type} (g : IndexedGrammar T) (cert : CompositeCert g) (old new : List (RunCell g)) (haccept : inputDone cert (evalInputBlocks cert InputPhase.prefix old new) = true) : ∃ (input : List T) (oldPos : ℕ) (newPos : ℕ), oldPos ≤ input.length ∧ newPos ≤ input.length ∧ clearInputBlocks g old = inputPositionCells g oldPos input ∧ clearInputBlocks g new = inputPositionCells g newPos input ∧ cert.InputAction input oldPos newPos

Soundness decoder for arbitrary physical running rows. An accepted input scan reconstructs a common immutable input word, canonical consumed-prefix positions, and exactly the input action named by its certificate. Packed work blocks are intentionally erased from the row equalities.

theorem IndexedGrammar.Aho.evalInputBlocks_encodeRunCells_accepts_iff {T : Type} (g : IndexedGrammar T) (cert : CompositeCert g) (input : List T) (old new : Config g) (hold : old.inputPos ≤ input.length) (hnew : new.inputPos ≤ input.length) : inputDone cert (evalInputBlocks cert InputPhase.prefix (encodeRunCells g input old) (encodeRunCells g input new)) = true ↔ cert.InputAction input old.inputPos new.inputPos

Exact input-track correctness for encoded configurations.

theorem IndexedGrammar.Aho.evalInputBlocks_encodeRunCells_complete {T : Type} (g : IndexedGrammar T) (cert : CompositeCert g) (input : List T) (old new : Config g) (hold : old.inputPos ≤ input.length) (hnew : new.inputPos ≤ input.length) (haction : cert.InputAction input old.inputPos new.inputPos) : inputDone cert (evalInputBlocks cert InputPhase.prefix (encodeRunCells g input old) (encodeRunCells g input new)) = true

Completeness direction of evalInputBlocks_encodeRunCells_accepts_iff.

theorem IndexedGrammar.Aho.evalInputBlocks_encodeRunCells_sound {T : Type} (g : IndexedGrammar T) (cert : CompositeCert g) (input : List T) (old new : Config g) (hold : old.inputPos ≤ input.length) (hnew : new.inputPos ≤ input.length) (haccept : inputDone cert (evalInputBlocks cert InputPhase.prefix (encodeRunCells g input old) (encodeRunCells g input new)) = true) : cert.InputAction input old.inputPos new.inputPos

Soundness direction of evalInputBlocks_encodeRunCells_accepts_iff.