Certified row checker for Aho's machine

The packed rows in Aho.Machine.PaddedRows retain the active work-head bit. Consequently every composite move is a regular relation on two aligned rows. Insertions and deletions only shift the remaining suffix by at most two slots: the checker below remembers the preceding two old and new slots.

The per-cell certificate chooses the finite composite rule and the phase reached after each of the twenty-one logical slots in that cell. Phase choices only resolve regular-expression boundaries; all grammar predicates, symbols, active bits, input-consumption bits, and delayed suffix equalities are checked by the finite control.

Logical-slot verifier

inductive IndexedGrammar.Aho.WorkPhase : Type

Finite phases shared by the fourteen composite-certificate cases.

• prefix : WorkPhase
• marked : WorkPhase
• stage1 : WorkPhase
• stage2 : WorkPhase
• stage3 : WorkPhase
• popBeta : WorkPhase
• returnBeta : WorkPhase
• minus1First : WorkPhase
• suffixSame : WorkPhase
• suffixPlus1 : WorkPhase
• suffixPlus2 : WorkPhase
• suffixMinus1 : WorkPhase
• suffixMinus2 : WorkPhase
• dead : WorkPhase

instance IndexedGrammar.Aho.instDecidableEqWorkPhase : DecidableEq WorkPhase

Equations

• IndexedGrammar.Aho.instDecidableEqWorkPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance IndexedGrammar.Aho.instFintypeWorkPhase : Fintype WorkPhase

Equations

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

structure IndexedGrammar.Aho.WorkHistory {T : Type} (g : IndexedGrammar T) : Type

Two slots of lookbehind on each aligned work track. The outer option distinguishes "no slot has been read" from a previously read padding blank.

• old1 : Option (Option (WorkSlot g))
• old2 : Option (Option (WorkSlot g))
• new1 : Option (Option (WorkSlot g))
• new2 : Option (Option (WorkSlot g))

noncomputable instance IndexedGrammar.Aho.WorkHistory.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (WorkHistory g)

Equations

• IndexedGrammar.Aho.WorkHistory.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.WorkHistory g)

noncomputable instance IndexedGrammar.Aho.WorkHistory.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] : Fintype (WorkHistory g)

Equations

• IndexedGrammar.Aho.WorkHistory.instFintype = Fintype.ofInjective (fun (h : IndexedGrammar.Aho.WorkHistory g) => (h.old1, h.old2, h.new1, h.new2)) ⋯

structure IndexedGrammar.Aho.WorkScanState {T : Type} (g : IndexedGrammar T) : Type

State of the logical-slot scan. oldEnded and newEnded enforce the canonical some* none* padding shape.

• phase : WorkPhase
• history : WorkHistory g
• oldEnded : Bool
• newEnded : Bool

noncomputable instance IndexedGrammar.Aho.WorkScanState.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (WorkScanState g)

Equations

• IndexedGrammar.Aho.WorkScanState.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.WorkScanState g)

noncomputable instance IndexedGrammar.Aho.WorkScanState.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] : Fintype (WorkScanState g)

Equations

• IndexedGrammar.Aho.WorkScanState.instFintype = Fintype.ofInjective (fun (s : IndexedGrammar.Aho.WorkScanState g) => (s.phase, s.history, s.oldEnded, s.newEnded)) ⋯

def IndexedGrammar.Aho.initialWorkScan {T : Type} (g : IndexedGrammar T) : WorkScanState g

Equations

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

def IndexedGrammar.Aho.inactive {T✝ : Type} {g : IndexedGrammar T✝} (z : WorkSym g) : Option (WorkSlot g)

Equations

• IndexedGrammar.Aho.inactive z = some { active := false, symbol := z }

def IndexedGrammar.Aho.active {T✝ : Type} {g : IndexedGrammar T✝} (z : WorkSym g) : Option (WorkSlot g)

Equations

• IndexedGrammar.Aho.active z = some { active := true, symbol := z }

def IndexedGrammar.Aho.InactiveOpt {T✝ : Type} {g : IndexedGrammar T✝} : Option (WorkSlot g) → Prop

Equations

• IndexedGrammar.Aho.InactiveOpt none = True
• IndexedGrammar.Aho.InactiveOpt (some s) = (s.active = false)

def IndexedGrammar.Aho.InactiveSome {T✝ : Type} {g : IndexedGrammar T✝} (x : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.InactiveSome x = ∃ (z : IndexedGrammar.Aho.WorkSym g), x = IndexedGrammar.Aho.inactive z

def IndexedGrammar.Aho.InactiveNonIndex {T✝ : Type} {g : IndexedGrammar T✝} (x : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.InactiveNonIndex x = ∃ (z : IndexedGrammar.Aho.WorkSym g), x = IndexedGrammar.Aho.inactive z ∧ z.isIndex = false

def IndexedGrammar.Aho.SameInactiveSome {T✝ : Type} {g : IndexedGrammar T✝} (x y : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.SameInactiveSome x y = ∃ (z : IndexedGrammar.Aho.WorkSym g), x = IndexedGrammar.Aho.inactive z ∧ y = IndexedGrammar.Aho.inactive z

def IndexedGrammar.Aho.ProductiveMarked {T✝ : Type} {g : IndexedGrammar T✝} (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.ProductiveBoundaryOK {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) : Prop

Equations

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

def IndexedGrammar.Aho.Boundary {T✝ : Type} {g : IndexedGrammar T✝} (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.Boundary old new = (old = IndexedGrammar.Aho.inactive IndexedGrammar.Aho.WorkSym.dollar ∧ new = IndexedGrammar.Aho.inactive IndexedGrammar.Aho.WorkSym.dollar)

def IndexedGrammar.Aho.sameSuffix {T✝ : Type} {g : IndexedGrammar T✝} (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.sameSuffix old new = (old = new ∧ IndexedGrammar.Aho.InactiveOpt old)

def IndexedGrammar.Aho.plus1Suffix {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.plus1Suffix h old new = (IndexedGrammar.Aho.InactiveOpt old ∧ IndexedGrammar.Aho.InactiveOpt new ∧ h.old1 = some new)

def IndexedGrammar.Aho.plus2Suffix {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.plus2Suffix h old new = (IndexedGrammar.Aho.InactiveOpt old ∧ IndexedGrammar.Aho.InactiveOpt new ∧ h.old2 = some new)

def IndexedGrammar.Aho.minus1Suffix {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.minus1Suffix h old new = (IndexedGrammar.Aho.InactiveOpt old ∧ IndexedGrammar.Aho.InactiveOpt new ∧ h.new1 = some old)

def IndexedGrammar.Aho.minus2Suffix {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.minus2Suffix h old new = (IndexedGrammar.Aho.InactiveOpt old ∧ IndexedGrammar.Aho.InactiveOpt new ∧ h.new2 = some old)

def IndexedGrammar.Aho.sameSymbolFirstMinus1 {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.prefixEdge {T✝ : Type} {g : IndexedGrammar T✝} (productive : Bool) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.prefixEdge productive IndexedGrammar.Aho.WorkPhase.prefix IndexedGrammar.Aho.WorkPhase.prefix h old new = IndexedGrammar.Aho.SameInactiveSome old new
• IndexedGrammar.Aho.prefixEdge productive IndexedGrammar.Aho.WorkPhase.prefix IndexedGrammar.Aho.WorkPhase.marked h old new = (productive = true ∧ IndexedGrammar.Aho.ProductiveMarked old new)
• IndexedGrammar.Aho.prefixEdge productive IndexedGrammar.Aho.WorkPhase.marked IndexedGrammar.Aho.WorkPhase.stage1 h old new = (productive = true ∧ IndexedGrammar.Aho.Boundary old new)
• IndexedGrammar.Aho.prefixEdge productive phase next h old new = False

def IndexedGrammar.Aho.insertOneEdge {T✝ : Type} {g : IndexedGrammar T✝} (productive : Bool) (oldFocus newFocus inserted : WorkSym g) (needOldSome : Bool) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.replaceOneEdge {T✝ : Type} {g : IndexedGrammar T✝} (productive : Bool) (oldFocus newFocus : WorkSym g) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.replaceTwoEdge {T✝ : Type} {g : IndexedGrammar T✝} (oldFocus newFocus oldNext newNext : WorkSym g) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.deleteOneEdge {T✝ : Type} {g : IndexedGrammar T✝} (focusOK : Option (WorkSlot g) → Prop) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

Equations

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

def IndexedGrammar.Aho.WorkEdge {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) : Prop

The finite aligned-slot edge relation for one Aho composite certificate.

Equations

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

def IndexedGrammar.Aho.CertEnabled {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : CompositeCert g → Prop

The grammar-side side condition carried by a composite certificate.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.plainBinary A B C) = IndexedGrammar.Aho.AugBinary g A B C
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.plainTerminal A a) = IndexedGrammar.Aho.AugTerminal g A a
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.plainPushSkip A B f) = IndexedGrammar.Aho.AugPush g A B f
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.plainPushUse A B f) = IndexedGrammar.Aho.AugPush g A B f
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.liveBinaryBoth A B C) = IndexedGrammar.Aho.AugBinary g A B C
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.liveBinaryLeft A B C) = IndexedGrammar.Aho.AugBinary g A B C
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.liveBinaryRight A B C) = IndexedGrammar.Aho.AugBinary g A B C
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.livePushFresh A B f) = IndexedGrammar.Aho.AugPush g A B f
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.popPlain R d A B) = (R A B = true)
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.popLive R d A B) = (R A B = true ∧ d.later = true)
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.matchTerminal a) = True
• IndexedGrammar.Aho.CertEnabled g (IndexedGrammar.Aho.CompositeCert.eraseIndex R d) = (d.erasable = true)
• IndexedGrammar.Aho.CertEnabled g IndexedGrammar.Aho.CompositeCert.returnFrame = True

def IndexedGrammar.Aho.CompositeCert.productive {T✝ : Type} {g : IndexedGrammar T✝} : CompositeCert g → Bool

Composite rules whose alpha prefix is changed by Aho's productive mark operation.

Equations

• (IndexedGrammar.Aho.CompositeCert.plainBinary a a_1 a_2).productive = true
• (IndexedGrammar.Aho.CompositeCert.plainTerminal a a_1).productive = true
• (IndexedGrammar.Aho.CompositeCert.liveBinaryBoth a a_1 a_2).productive = true
• (IndexedGrammar.Aho.CompositeCert.liveBinaryLeft a a_1 a_2).productive = true
• (IndexedGrammar.Aho.CompositeCert.liveBinaryRight a a_1 a_2).productive = true
• x✝.productive = false

theorem IndexedGrammar.Aho.workEdge_prefix_iff {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (phase next : WorkPhase) (h : WorkHistory g) (old new : Option (WorkSlot g)) (hphase : phase = WorkPhase.prefix ∨ phase = WorkPhase.marked) : WorkEdge g cert phase next h old new ↔ CertEnabled g cert ∧ prefixEdge cert.productive phase next h old new

def IndexedGrammar.Aho.paddingOK {T✝ : Type} {g : IndexedGrammar T✝} (ended : Bool) (slot : Option (WorkSlot g)) : Prop

Equations

• IndexedGrammar.Aho.paddingOK ended slot = (ended = false ∨ slot = none)

def IndexedGrammar.Aho.updateHistory {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (old new : Option (WorkSlot g)) : WorkHistory g

Equations

• IndexedGrammar.Aho.updateHistory h old new = { old1 := some old, old2 := h.old1, new1 := some new, new2 := h.new1 }

noncomputable def IndexedGrammar.Aho.workSlotStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : Option (WorkSlot g)) (next : WorkPhase) : WorkScanState g

Execute one aligned logical-slot check.

Equations

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

theorem IndexedGrammar.Aho.workSlotStep_prefix_same {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (z : WorkSym g) (henabled : CertEnabled g cert) : workSlotStep g cert { phase := WorkPhase.prefix, history := h, oldEnded := false, newEnded := false } (inactive z) (inactive z) WorkPhase.prefix = { phase := WorkPhase.prefix, history := updateHistory h (inactive z) (inactive z), oldEnded := false, newEnded := false }

theorem IndexedGrammar.Aho.workSlotStep_prefix_mark {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (R : CFlag g) (d : IndexMark) (henabled : CertEnabled g cert) (hproductive : cert.productive = true) : workSlotStep g cert { phase := WorkPhase.prefix, history := h, oldEnded := false, newEnded := false } (inactive (WorkSym.index R d)) (inactive (WorkSym.index R d.markUsed)) WorkPhase.marked = { phase := WorkPhase.marked, history := updateHistory h (inactive (WorkSym.index R d)) (inactive (WorkSym.index R d.markUsed)), oldEnded := false, newEnded := false }

theorem IndexedGrammar.Aho.workSlotStep_prefix_boundary {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (henabled : CertEnabled g cert) (hboundary : cert.productive = false ∨ ProductiveBoundaryOK h) : workSlotStep g cert { phase := WorkPhase.prefix, history := h, oldEnded := false, newEnded := false } (inactive WorkSym.dollar) (inactive WorkSym.dollar) WorkPhase.stage1 = { phase := WorkPhase.stage1, history := updateHistory h (inactive WorkSym.dollar) (inactive WorkSym.dollar), oldEnded := false, newEnded := false }

theorem IndexedGrammar.Aho.workSlotStep_marked_boundary {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (henabled : CertEnabled g cert) (hproductive : cert.productive = true) : workSlotStep g cert { phase := WorkPhase.marked, history := h, oldEnded := false, newEnded := false } (inactive WorkSym.dollar) (inactive WorkSym.dollar) WorkPhase.stage1 = { phase := WorkPhase.stage1, history := updateHistory h (inactive WorkSym.dollar) (inactive WorkSym.dollar), oldEnded := false, newEnded := false }

noncomputable def IndexedGrammar.Aho.evalWorkSlots {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) : WorkScanState g → List (Option (WorkSlot g)) → List (Option (WorkSlot g)) → List WorkPhase → WorkScanState g

Run a list of aligned logical slots and phase choices.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.evalWorkSlots g cert x✝ [] [] [] = x✝
• IndexedGrammar.Aho.evalWorkSlots g cert x✝³ x✝² x✝¹ x✝ = { phase := IndexedGrammar.Aho.WorkPhase.dead, history := x✝³.history, oldEnded := x✝³.oldEnded, newEnded := x✝³.newEnded }

def IndexedGrammar.Aho.historySame {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) (xs : List (WorkSym g)) : WorkHistory g

Equations

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

theorem IndexedGrammar.Aho.evalWorkSlots_prefix_same {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (xs : List (WorkSym g)) (henabled : CertEnabled g cert) : evalWorkSlots g cert { phase := WorkPhase.prefix, history := h, oldEnded := false, newEnded := false } (List.map inactive xs) (List.map inactive xs) (List.replicate xs.length WorkPhase.prefix) = { phase := WorkPhase.prefix, history := historySame h xs, oldEnded := false, newEnded := false }

noncomputable def IndexedGrammar.Aho.evalWorkBlock {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old new : WorkBlock g) (choices : Fin workWidth → WorkPhase) : WorkScanState g

Run the twenty-one logical slots packed in one physical row cell.

Equations

• IndexedGrammar.Aho.evalWorkBlock g cert state old new choices = IndexedGrammar.Aho.evalWorkSlots g cert state (List.ofFn old) (List.ofFn new) (List.ofFn choices)

theorem IndexedGrammar.Aho.evalWorkSlots_append {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (state : WorkScanState g) (old₁ old₂ new₁ new₂ : List (Option (WorkSlot g))) (choices₁ choices₂ : List WorkPhase) (h₁ : old₁.length = new₁.length) (h₂ : old₁.length = choices₁.length) : evalWorkSlots g cert state (old₁ ++ old₂) (new₁ ++ new₂) (choices₁ ++ choices₂) = evalWorkSlots g cert (evalWorkSlots g cert state old₁ new₁ choices₁) old₂ new₂ choices₂

noncomputable def IndexedGrammar.Aho.evalWorkBlocks {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) : WorkScanState g → List (WorkBlock g) → List (WorkBlock g) → List (Fin workWidth → WorkPhase) → WorkScanState g

Fold a list of physical blocks; useful for relating the cell checker to one flat slot scan.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.evalWorkBlocks g cert x✝ [] [] [] = x✝
• IndexedGrammar.Aho.evalWorkBlocks g cert x✝³ x✝² x✝¹ x✝ = { phase := IndexedGrammar.Aho.WorkPhase.dead, history := x✝³.history, oldEnded := x✝³.oldEnded, newEnded := x✝³.newEnded }

def IndexedGrammar.Aho.runBlocks {T : Type} {g : IndexedGrammar T} : List (RowCell g) → Option (List (WorkBlock g))

Extract all work blocks when every cell is in running form.

Equations

• IndexedGrammar.Aho.runBlocks [] = some []
• IndexedGrammar.Aho.runBlocks (IndexedGrammar.Aho.RowCell.run cell :: row) = Option.map (fun (x : List (IndexedGrammar.Aho.WorkBlock g)) => cell.block :: x) (IndexedGrammar.Aho.runBlocks row)
• IndexedGrammar.Aho.runBlocks (IndexedGrammar.Aho.RowCell.input a :: tail) = none

def IndexedGrammar.Aho.packedBlockList {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (cell n : ℕ) : List (WorkBlock g)

The consecutive packed blocks beginning at logical cell offset cell.

Equations

• IndexedGrammar.Aho.packedBlockList g work cell n = List.ofFn fun (i : Fin n) => packedCell IndexedGrammar.Aho.workWidth work (cell + ↑i)

@[simp]

theorem IndexedGrammar.Aho.runBlocks_encodeRunRowFrom {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) (w : List T) : runBlocks (encodeRunRowFrom g work inputPos cell w) = some (packedBlockList g work cell w.length)

def IndexedGrammar.Aho.phaseBlockList (n : ℕ) (phases : Fin (n * workWidth) → WorkPhase) : List (Fin workWidth → WorkPhase)

Reblock a flat phase function into one twenty-one-phase certificate per physical row cell.

Equations

• IndexedGrammar.Aho.phaseBlockList n phases = List.ofFn fun (i : Fin n) (j : Fin IndexedGrammar.Aho.workWidth) => phases ⟨↑i * IndexedGrammar.Aho.workWidth + ↑j, ⋯⟩

@[simp]

theorem IndexedGrammar.Aho.phaseBlockList_length (n : ℕ) (phases : Fin (n * workWidth) → WorkPhase) : (phaseBlockList n phases).length = n

theorem IndexedGrammar.Aho.phaseBlockList_flatten (n : ℕ) (phases : Fin (n * workWidth) → WorkPhase) : List.flatMap List.ofFn (phaseBlockList n phases) = List.ofFn phases

def IndexedGrammar.Aho.paddedWork {T✝ : Type} {g : IndexedGrammar T✝} (n : ℕ) (work : List (WorkSlot g)) : List (Option (WorkSlot g))

The full aligned slot stream of a bounded logical work word.

Equations

• IndexedGrammar.Aho.paddedWork n work = List.ofFn fun (k : Fin (n * IndexedGrammar.Aho.workWidth)) => work[↑k]?

@[simp]

theorem IndexedGrammar.Aho.paddedWork_length {T✝ : Type} {g : IndexedGrammar T✝} (n : ℕ) (work : List (WorkSlot g)) : (paddedWork n work).length = n * workWidth

theorem IndexedGrammar.Aho.paddedWork_eq_append {T✝ : Type} {g : IndexedGrammar T✝} (n : ℕ) (work : List (WorkSlot g)) (hwork : work.length ≤ n * workWidth) : paddedWork n work = List.map some work ++ List.replicate (n * workWidth - work.length) none

def IndexedGrammar.Aho.lastOldNone {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) : Prop

Equations

• IndexedGrammar.Aho.lastOldNone h = (h.old1 = some none)

def IndexedGrammar.Aho.lastTwoOldNone {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) : Prop

Equations

• IndexedGrammar.Aho.lastTwoOldNone h = (h.old1 = some none ∧ h.old2 = some none)

def IndexedGrammar.Aho.lastNewNone {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) : Prop

Equations

• IndexedGrammar.Aho.lastNewNone h = (h.new1 = some none)

def IndexedGrammar.Aho.lastTwoNewNone {T✝ : Type} {g : IndexedGrammar T✝} (h : WorkHistory g) : Prop

Equations

• IndexedGrammar.Aho.lastTwoNewNone h = (h.new1 = some none ∧ h.new2 = some none)

noncomputable def IndexedGrammar.Aho.workScanDone {T✝ : Type} {g : IndexedGrammar T✝} (state : WorkScanState g) : Bool

Successful terminal phases, including the padding needed to prevent truncated insertions.

Equations

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

Physical-row verifier

inductive IndexedGrammar.Aho.InputPhase : Type

• prefix : InputPhase
• tail : InputPhase
• matched : InputPhase
• dead : InputPhase

instance IndexedGrammar.Aho.instDecidableEqInputPhase : DecidableEq InputPhase

Equations

• IndexedGrammar.Aho.instDecidableEqInputPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance IndexedGrammar.Aho.instFintypeInputPhase : Fintype InputPhase

Equations

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

noncomputable def IndexedGrammar.Aho.inputStep {T✝ : Type} {g : IndexedGrammar T✝} (cert : CompositeCert g) (phase : InputPhase) (old new : RunCell g) : InputPhase

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.inputStep cert✝ IndexedGrammar.Aho.InputPhase.prefix old new = if old.input ≠ new.input then IndexedGrammar.Aho.InputPhase.dead else IndexedGrammar.Aho.InputPhase.prefix
• IndexedGrammar.Aho.inputStep cert✝ IndexedGrammar.Aho.InputPhase.prefix old new = if old.input ≠ new.input then IndexedGrammar.Aho.InputPhase.dead else IndexedGrammar.Aho.InputPhase.tail
• IndexedGrammar.Aho.inputStep cert✝ IndexedGrammar.Aho.InputPhase.tail old new = if old.input ≠ new.input then IndexedGrammar.Aho.InputPhase.dead else IndexedGrammar.Aho.InputPhase.tail
• IndexedGrammar.Aho.inputStep cert✝ phase✝ old new = if old.input ≠ new.input then IndexedGrammar.Aho.InputPhase.dead else IndexedGrammar.Aho.InputPhase.dead

noncomputable def IndexedGrammar.Aho.inputDone {T✝ : Type} {g : IndexedGrammar T✝} (cert : CompositeCert g) : InputPhase → Bool

Equations

• IndexedGrammar.Aho.inputDone (IndexedGrammar.Aho.CompositeCert.matchTerminal a) IndexedGrammar.Aho.InputPhase.prefix = decide False
• IndexedGrammar.Aho.inputDone cert IndexedGrammar.Aho.InputPhase.prefix = decide True
• IndexedGrammar.Aho.inputDone (IndexedGrammar.Aho.CompositeCert.matchTerminal a) IndexedGrammar.Aho.InputPhase.tail = decide False
• IndexedGrammar.Aho.inputDone cert IndexedGrammar.Aho.InputPhase.tail = decide True
• IndexedGrammar.Aho.inputDone (IndexedGrammar.Aho.CompositeCert.matchTerminal a) IndexedGrammar.Aho.InputPhase.matched = decide True
• IndexedGrammar.Aho.inputDone cert IndexedGrammar.Aho.InputPhase.matched = decide False
• IndexedGrammar.Aho.inputDone cert IndexedGrammar.Aho.InputPhase.dead = false

noncomputable def IndexedGrammar.Aho.evalInputBlocks {T✝ : Type} {g : IndexedGrammar T✝} (cert : CompositeCert g) : InputPhase → List (RunCell g) → List (RunCell g) → InputPhase

Fold the independent immutable-input/consumption-bit check over running cells.

Equations

• IndexedGrammar.Aho.evalInputBlocks cert x✝ [] [] = x✝
• IndexedGrammar.Aho.evalInputBlocks cert x✝ (old :: olds) (new :: news) = IndexedGrammar.Aho.evalInputBlocks cert (IndexedGrammar.Aho.inputStep cert x✝ old new) olds news
• IndexedGrammar.Aho.evalInputBlocks cert x✝² x✝¹ x✝ = IndexedGrammar.Aho.InputPhase.dead

inductive IndexedGrammar.Aho.RowCert {T : Type} (g : IndexedGrammar T) : Type

One physical-row certificate. The same composite certificate must be repeated along the row; the phase block may vary from cell to cell.

• init {T : Type} {g : IndexedGrammar T} : RowCert g
• composite {T : Type} {g : IndexedGrammar T} : CompositeCert g → (Fin workWidth → WorkPhase) → RowCert g

noncomputable instance IndexedGrammar.Aho.RowCert.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (RowCert g)

Equations

• IndexedGrammar.Aho.RowCert.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.RowCert g)

noncomputable instance IndexedGrammar.Aho.RowCert.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] [Fintype g.flag] : Fintype (RowCert g)

Equations

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

inductive IndexedGrammar.Aho.RowState {T : Type} (g : IndexedGrammar T) : Type

• start {T : Type} {g : IndexedGrammar T} : RowState g
• init {T : Type} {g : IndexedGrammar T} : BoundaryScanState → RowState g
• composite {T : Type} {g : IndexedGrammar T} : CompositeCert g → InputPhase → WorkScanState g → RowState g
• dead {T : Type} {g : IndexedGrammar T} : RowState g

noncomputable instance IndexedGrammar.Aho.RowState.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (RowState g)

Equations

• IndexedGrammar.Aho.RowState.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.RowState g)

noncomputable instance IndexedGrammar.Aho.RowState.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] [Fintype g.flag] : Fintype (RowState g)

Equations

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

noncomputable def IndexedGrammar.Aho.compositeCell {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (input : InputPhase) (work : WorkScanState g) (old new : RowCell g) (phases : Fin workWidth → WorkPhase) : RowState g

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.compositeCell g cert input work old new phases = IndexedGrammar.Aho.RowState.dead

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

One physical-cell transition of the complete row verifier.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.rowStepCell g (IndexedGrammar.Aho.RowState.init q) x✝¹ x✝ IndexedGrammar.Aho.RowCert.init = IndexedGrammar.Aho.RowState.init (IndexedGrammar.Aho.initScanCell g q x✝¹ x✝)
• IndexedGrammar.Aho.rowStepCell g x✝³ x✝² x✝¹ x✝ = IndexedGrammar.Aho.RowState.dead

@[simp]

theorem IndexedGrammar.Aho.rowStepCell_composite_same {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (input : InputPhase) (work : WorkScanState g) (old new : RunCell g) (phases : Fin workWidth → WorkPhase) : rowStepCell g (RowState.composite cert input work) (RowCell.run old) (RowCell.run new) (RowCert.composite cert phases) = RowState.composite cert (inputStep cert input old new) (evalWorkBlock g cert work old.block new.block phases)

@[simp]

theorem IndexedGrammar.Aho.rowStepCell_composite_start {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (old new : RunCell g) (phases : Fin workWidth → WorkPhase) : rowStepCell g RowState.start (RowCell.run old) (RowCell.run new) (RowCert.composite cert phases) = RowState.composite cert (inputStep cert InputPhase.prefix old new) (evalWorkBlock g cert (initialWorkScan g) old.block new.block phases)

noncomputable def IndexedGrammar.Aho.rowStepDone {T✝ : Type} {g : IndexedGrammar T✝} : RowState g → Bool

Equations

• IndexedGrammar.Aho.rowStepDone (IndexedGrammar.Aho.RowState.init IndexedGrammar.Aho.BoundaryScanState.tail) = true
• IndexedGrammar.Aho.rowStepDone (IndexedGrammar.Aho.RowState.composite cert input work) = (IndexedGrammar.Aho.inputDone cert input && IndexedGrammar.Aho.workScanDone work)
• IndexedGrammar.Aho.rowStepDone x✝ = false

noncomputable def IndexedGrammar.Aho.ahoRowSystem {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : CertifiedRowSystem T (RowCell g) (RowCert g) (RowState g) BoundaryScanState

The certified row system implementing initialized and composite Aho steps.

Equations

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

@[simp]

theorem IndexedGrammar.Aho.ahoRowSystem_stepCell {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (q : RowState g) (old new : RowCell g) (cert : RowCert g) : (ahoRowSystem g).stepCell q old new cert = rowStepCell g q old new cert

def IndexedGrammar.Aho.RowState.Closed {T✝ : Type} {g : IndexedGrammar T✝} : RowState g → Prop

Equations

• (IndexedGrammar.Aho.RowState.composite a a_1 a_2).Closed = True
• IndexedGrammar.Aho.RowState.dead.Closed = True
• x✝.Closed = False

theorem IndexedGrammar.Aho.rowStepCell_closed {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {state : RowState g} (hstate : state.Closed) (old new : RowCell g) (cert : RowCert g) : (rowStepCell g state old new cert).Closed

theorem IndexedGrammar.Aho.evalStep_closed {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {state : RowState g} (hstate : state.Closed) (old new : List (RowCell g)) (certs : List (RowCert g)) {result : RowState g} (h : (ahoRowSystem g).evalStep state old new certs = some result) : result.Closed

theorem IndexedGrammar.Aho.evalStep_init_from {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (q : BoundaryScanState) (old new : List (RowCell g)) (hlen : old.length = new.length) : (ahoRowSystem g).evalStep (RowState.init q) old new (List.replicate old.length RowCert.init) = some (RowState.init (evalInitScan g q old new))

theorem IndexedGrammar.Aho.evalStep_init_start {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (old new : List (RowCell g)) (hne : old ≠ []) (hlen : old.length = new.length) : (ahoRowSystem g).evalStep RowState.start old new (List.replicate old.length RowCert.init) = some (RowState.init (evalInitScan g BoundaryScanState.first old new))

theorem IndexedGrammar.Aho.evalStep_init_sound {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (old new : List (RowCell g)) (certs : List (RowCert g)) (q : BoundaryScanState) (h : (ahoRowSystem g).evalStep RowState.start old new certs = some (RowState.init q)) : evalInitScan g BoundaryScanState.first old new = q

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

Every semantic initialization step has a certified-row witness.

theorem IndexedGrammar.Aho.paddedInitStep_of_evalStep_init {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {old new : List (RowCell g)} {certs : List (RowCert g)} {q : BoundaryScanState} (heval : (ahoRowSystem g).evalStep RowState.start old new certs = some (RowState.init q)) (hdone : rowStepDone (RowState.init q) = true) : PaddedInitStep g old new

If a successful certified scan finishes in initialization mode, it is exactly an initialization row step.

theorem IndexedGrammar.Aho.evalFinal_ahoRowSystem {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (q : BoundaryScanState) (row : List (RowCell g)) : (ahoRowSystem g).evalFinal q row = evalFinalScan g q row

theorem IndexedGrammar.Aho.final_ahoRowSystem_iff {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (row : List (RowCell g)) : (ahoRowSystem g).Final row ↔ FinalRow g row

The target component of the certified system is exactly Aho's final padded row.