Completeness of Aho's certified row system

This is the semantic-to-physical direction. It combines the input-track and work-track trace constructors, packs them into physical cells, and proves that every semantic PaddedRowStep is accepted as a CertifiedRowSystem.RowStep.

@[simp]

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

@[simp]

theorem IndexedGrammar.Aho.encodeRunCellsFrom_length {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) (input : List T) : (encodeRunCellsFrom g work inputPos cell input).length = input.length

@[simp]

theorem IndexedGrammar.Aho.encodeRunCells_length {T : Type} (g : IndexedGrammar T) (input : List T) (c : Config g) : (encodeRunCells g input c).length = input.length

@[simp]

theorem IndexedGrammar.Aho.encodeRunCells_map_block {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.evalStep_composite_from {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (inputState : InputPhase) (workState : WorkScanState g) (old new : List (RunCell g)) (choices : List (Fin workWidth → WorkPhase)) (hnew : new.length = old.length) (hchoices : choices.length = old.length) : (ahoRowSystem g).evalStep (RowState.composite cert inputState workState) (List.map RowCell.run old) (List.map RowCell.run new) (List.map (RowCert.composite cert) choices) = some (RowState.composite cert (evalInputBlocks cert inputState old new) (evalWorkBlocks g cert workState (List.map RunCell.block old) (List.map RunCell.block new) choices))

theorem IndexedGrammar.Aho.evalStep_composite_start {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (old new : List (RunCell g)) (choices : List (Fin workWidth → WorkPhase)) (hne : old ≠ []) (hnew : new.length = old.length) (hchoices : choices.length = old.length) : (ahoRowSystem g).evalStep RowState.start (List.map RowCell.run old) (List.map RowCell.run new) (List.map (RowCert.composite cert) choices) = some (RowState.composite cert (evalInputBlocks cert InputPhase.prefix old new) (evalWorkBlocks g cert (initialWorkScan g) (List.map RunCell.block old) (List.map RunCell.block new) choices))

theorem IndexedGrammar.Aho.exists_phaseBlocks_of_workTraceAccepts {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (n : ℕ) (old new : List (WorkSlot g)) (h : WorkTraceAccepts g cert (paddedWork n old) (paddedWork n new)) : ∃ (choices : List (Fin workWidth → WorkPhase)) (result : WorkScanState g), choices.length = n ∧ evalWorkBlocks g cert (initialWorkScan g) (packedBlockList g old 0 n) (packedBlockList g new 0 n) choices = result ∧ workScanDone result = true

theorem IndexedGrammar.Aho.rowStep_of_certStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (cert : CompositeCert g) (old new : Config g) (hne : input ≠ []) (holdPos : Config.InputWithin input old) (hnewPos : Config.InputWithin input new) (holdWork : Config.Within (input.length * workWidth) old) (hnewWork : Config.Within (input.length * workWidth) new) (hstep : CertStep g input cert old new) : (ahoRowSystem g).RowStep (encodeRunRow g input old) (encodeRunRow g input new)

One bounded semantic Aho certificate is accepted by the physical certified-row checker.

theorem IndexedGrammar.Aho.rowStep_of_paddedCompositeStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {old new : List (RowCell g)} (h : PaddedCompositeStep g old new) : (ahoRowSystem g).RowStep old new

Every semantic composite padded-row edge is accepted by the certified row system; initialization is handled separately by rowStep_of_paddedRowStep.

theorem IndexedGrammar.Aho.rowStep_of_paddedRowStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {old new : List (RowCell g)} (h : PaddedRowStep g old new) : (ahoRowSystem g).RowStep old new

Every semantic padded-row edge has a finite certificate row.

theorem IndexedGrammar.Aho.rowReachLanguage_of_paddedReachLanguage {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : input ∈ paddedReachLanguage g → input ∈ (ahoRowSystem g).rowReachLanguage

Semantic padded reachability embeds into the executable finite row system.