Evaluation lemmas for Aho's packed row checker

Physical input cells contain blocks of twenty-one logical work slots. This module bridges the certified row system's cell-by-cell evaluator to the flattened input and work-track evaluators used by the completeness and soundness proofs.

noncomputable def IndexedGrammar.Aho.evalRowTriples {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : RowState g → List (RowCell g × RowCell g × RowCert g) → RowState g

Equations

• IndexedGrammar.Aho.evalRowTriples g x✝ [] = x✝
• IndexedGrammar.Aho.evalRowTriples g x✝ ((old, new, cert) :: rows) = IndexedGrammar.Aho.evalRowTriples g (IndexedGrammar.Aho.rowStepCell g x✝ old new cert) rows

theorem IndexedGrammar.Aho.evalStep_rowTriples {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (state : RowState g) (rows : List (RowCell g × RowCell g × RowCert g)) : (ahoRowSystem g).evalStep state (List.map (fun (r : RowCell g × RowCell g × RowCert g) => r.1) rows) (List.map (fun (r : RowCell g × RowCell g × RowCert g) => r.2.1) rows) (List.map (fun (r : RowCell g × RowCell g × RowCert g) => r.2.2) rows) = some (evalRowTriples g state rows)

theorem IndexedGrammar.Aho.packedBlockList_flatten {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (n : ℕ) : List.flatMap List.ofFn (packedBlockList g work 0 n) = paddedWork n work

Flattening the consecutive physical work blocks recovers the fixed-width padded slot row.

theorem IndexedGrammar.Aho.evalWorkBlocks_eq_evalWorkSlots {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : List (WorkBlock g)) (choices : List (Fin workWidth → WorkPhase)) (hnew : new.length = old.length) (hchoices : choices.length = old.length) : evalWorkBlocks g cert state old new choices = evalWorkSlots g cert state (List.flatMap List.ofFn old) (List.flatMap List.ofFn new) (List.flatMap List.ofFn choices)

Folding physical blocks is the same computation as folding their flattened slot streams.