Padded Aho machine rows

The fixed-width row encoding and semantic padded transition relation used by the LBA compiler.

Twenty-one-slot padded rows

@[irreducible]

def IndexedGrammar.Aho.workWidth : ℕ

The fixed number of logical work squares per input position used by the scheduler bound. Aho proves the sharper constant six; the persistent scheduler invariant currently uses twenty-one.

Equations

• IndexedGrammar.Aho.workWidth = 21

theorem IndexedGrammar.Aho.workWidth_eq : workWidth = 21

@[reducible, inline]

abbrev IndexedGrammar.Aho.WorkBlock {T : Type} (g : IndexedGrammar T) : Type

One packed work block. none is a blank logical work square.

Equations

• IndexedGrammar.Aho.WorkBlock g = PackedBlock (IndexedGrammar.Aho.WorkSlot g) IndexedGrammar.Aho.workWidth

def IndexedGrammar.Aho.blankBlock {T : Type} (g : IndexedGrammar T) : WorkBlock g

The completely unused packed work block.

Equations

• IndexedGrammar.Aho.blankBlock g x✝ = none

theorem IndexedGrammar.Aho.packedCell_eq_blankBlock_of_length_le {T : Type} (g : IndexedGrammar T) (xs : List (WorkSlot g)) (cell : ℕ) (h : xs.length ≤ cell * workWidth) : packedCell workWidth xs cell = blankBlock g

Once a packed-cell offset lies beyond the logical word, that whole block is blank.

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

A running row cell retains its immutable input letter, whether that input position has already been compared, and twenty-one logical work squares.

• input : T
• consumed : Bool
• block : WorkBlock g

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

Equations

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

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

Equations

• IndexedGrammar.Aho.RunCell.instFintype = Fintype.ofInjective (fun (c : IndexedGrammar.Aho.RunCell g) => (c.input, c.consumed, c.block)) ⋯

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

Row cells are raw input cells before initialization or packed running cells afterwards.

• input {T : Type} {g : IndexedGrammar T} : T → RowCell g
• run {T : Type} {g : IndexedGrammar T} : RunCell g → RowCell g

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

Equations

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

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

Equations

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

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

Read the packed block of a running row cell.

Equations

• (IndexedGrammar.Aho.RowCell.input a).block? = none
• (IndexedGrammar.Aho.RowCell.run c).block? = some c.block

def IndexedGrammar.Aho.RowCell.consumed? {T : Type} {g : IndexedGrammar T} : RowCell g → Option Bool

Read the consumed-input bit of a running row cell.

Equations

• (IndexedGrammar.Aho.RowCell.input a).consumed? = none
• (IndexedGrammar.Aho.RowCell.run c).consumed? = some c.consumed

def IndexedGrammar.Aho.RowCell.inputLetter {T : Type} {g : IndexedGrammar T} : RowCell g → T

Recover the immutable input letter from either presentation of a row cell.

Equations

• (IndexedGrammar.Aho.RowCell.input a).inputLetter = a
• (IndexedGrammar.Aho.RowCell.run c).inputLetter = c.input

@[simp]

theorem IndexedGrammar.Aho.RowCell.inputLetter_input {T : Type} {g : IndexedGrammar T} (a : T) : (input a).inputLetter = a

@[simp]

theorem IndexedGrammar.Aho.RowCell.inputLetter_run {T : Type} {g : IndexedGrammar T} (c : RunCell g) : (run c).inputLetter = c.input

@[simp]

theorem IndexedGrammar.Aho.RowCell.input_ne_run {T : Type} {g : IndexedGrammar T} (a : T) (c : RunCell g) : input a ≠ run c

def IndexedGrammar.Aho.inputRow {T : Type} (g : IndexedGrammar T) (w : List T) : List (RowCell g)

The row presented to the certified-row system by an input word.

Equations

• IndexedGrammar.Aho.inputRow g w = List.map IndexedGrammar.Aho.RowCell.input w

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

Encode a running configuration, starting at physical input-cell offset cell.

Equations

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

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

Pack a composite configuration into one width-twenty-one row cell per input letter.

Equations

• IndexedGrammar.Aho.encodeRunRow g w c = IndexedGrammar.Aho.encodeRunRowFrom g c.work.slots c.inputPos 0 w

def IndexedGrammar.Aho.initialBlock {T : Type} (g : IndexedGrammar T) : WorkBlock g

The only nonblank block in an initialized running row.

Equations

• IndexedGrammar.Aho.initialBlock g = packedCell IndexedGrammar.Aho.workWidth (IndexedGrammar.Aho.initialConfig g).work.slots 0

def IndexedGrammar.Aho.finalBlock {T : Type} (g : IndexedGrammar T) : WorkBlock g

The only nonblank block in a final running row.

Equations

• IndexedGrammar.Aho.finalBlock g = packedCell IndexedGrammar.Aho.workWidth (IndexedGrammar.Aho.finalConfig g 0).work.slots 0

theorem IndexedGrammar.Aho.encodeRunRow_initial_cons {T : Type} (g : IndexedGrammar T) (a : T) (w : List T) : encodeRunRow g (a :: w) (initialConfig g) = RowCell.run { input := a, consumed := false, block := initialBlock g } :: List.map (fun (b : T) => RowCell.run { input := b, consumed := false, block := blankBlock g }) w

Canonical cellwise shape of a nonempty initialization row.

theorem IndexedGrammar.Aho.encodeRunRow_final_cons {T : Type} (g : IndexedGrammar T) (a : T) (w : List T) : encodeRunRow g (a :: w) (finalConfig g (a :: w).length) = RowCell.run { input := a, consumed := true, block := finalBlock g } :: List.map (fun (b : T) => RowCell.run { input := b, consumed := true, block := blankBlock g }) w

Canonical cellwise shape of a nonempty final row.

@[simp]

theorem IndexedGrammar.Aho.inputRow_length {T : Type} (g : IndexedGrammar T) (w : List T) : (inputRow g w).length = w.length

@[simp]

theorem IndexedGrammar.Aho.inputRow_map_inputLetter {T : Type} (g : IndexedGrammar T) (w : List T) : List.map RowCell.inputLetter (inputRow g w) = w

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

@[simp]

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

theorem IndexedGrammar.Aho.encodeRunRowFrom_getElem?_block {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) (w : List T) (k : ℕ) (hk : k < w.length) : (encodeRunRowFrom g work inputPos cell w)[k]?.bind RowCell.block? = some (packedCell workWidth work (cell + k))

theorem IndexedGrammar.Aho.encodeRunRowFrom_getElem?_consumed {T : Type} (g : IndexedGrammar T) (work : List (WorkSlot g)) (inputPos cell : ℕ) (w : List T) (k : ℕ) (hk : k < w.length) : (encodeRunRowFrom g work inputPos cell w)[k]?.bind RowCell.consumed? = some (decide (cell + k < inputPos))

@[simp]

theorem IndexedGrammar.Aho.encodeRunRow_length {T : Type} (g : IndexedGrammar T) (w : List T) (c : Config g) : (encodeRunRow g w c).length = w.length

@[simp]

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

theorem IndexedGrammar.Aho.encodeRunRow_input_eq {T : Type} {g : IndexedGrammar T} {w w' : List T} {c d : Config g} (h : encodeRunRow g w c = encodeRunRow g w' d) : w = w'

Equal running rows necessarily carry the same immutable input word.

theorem IndexedGrammar.Aho.encodeRunRow_injective_of_bounds {T : Type} (g : IndexedGrammar T) (w : List T) (c d : Config g) (hcpos : c.inputPos ≤ w.length) (hdpos : d.inputPos ≤ w.length) (hcwork : c.work.word.length ≤ w.length * workWidth) (hdwork : d.work.word.length ≤ w.length * workWidth) (hrow : encodeRunRow g w c = encodeRunRow g w d) : c = d

On a fixed input row, bounded marked encodings are injective in the full configuration, including both the input position and the active work-head position.

theorem IndexedGrammar.Aho.encodeRunRow_pair_injective_of_bounds {T : Type} (g : IndexedGrammar T) (w w' : List T) (c d : Config g) (hcpos : c.inputPos ≤ w.length) (hdpos : d.inputPos ≤ w'.length) (hcwork : c.work.word.length ≤ w.length * workWidth) (hdwork : d.work.word.length ≤ w'.length * workWidth) (hrow : encodeRunRow g w c = encodeRunRow g w' d) : w = w' ∧ c = d

Bounded marked rows recover both the immutable input word and the complete configuration.

def IndexedGrammar.Aho.PaddedInitStep {T : Type} (g : IndexedGrammar T) (x y : List (RowCell g)) : Prop

The initialization row step.

Equations

• IndexedGrammar.Aho.PaddedInitStep g x y = ∃ (w : List T), w ≠ [] ∧ x = IndexedGrammar.Aho.inputRow g w ∧ y = IndexedGrammar.Aho.encodeRunRow g w (IndexedGrammar.Aho.initialConfig g)

def IndexedGrammar.Aho.PaddedCompositeStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (x y : List (RowCell g)) : Prop

A bounded packed-row image of one Aho composite move.

Equations

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

def IndexedGrammar.Aho.PaddedRowStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (x y : List (RowCell g)) : Prop

Semantic padded-row relation: initialize once, then perform a bounded composite move.

Equations

• IndexedGrammar.Aho.PaddedRowStep g x y = (IndexedGrammar.Aho.PaddedInitStep g x y ∨ IndexedGrammar.Aho.PaddedCompositeStep g x y)

def IndexedGrammar.Aho.FinalRow {T : Type} (g : IndexedGrammar T) (row : List (RowCell g)) : Prop

A final row has consumed the whole frozen input and contains Aho's final $ # work word.

Equations

• IndexedGrammar.Aho.FinalRow g row = ∃ (w : List T), w ≠ [] ∧ row = IndexedGrammar.Aho.encodeRunRow g w (IndexedGrammar.Aho.finalConfig g w.length)