Structured RAM last-bit scanner — definitions

This is a second consumer of the typed finite-state scanner API. Its state is Option Bool: none before any input and some bit thereafter.

@[implicit_reducible]

instance Complexity.RAM.Structured.LastBit.optionBoolFinEnum : FinEnum (Option Bool)

Equations

• Complexity.RAM.Structured.LastBit.optionBoolFinEnum = FinEnum.ofList [none, some false, some true] Complexity.RAM.Structured.LastBit.optionBoolFinEnum._proof_1

def Complexity.RAM.Structured.LastBit.spec (target : Bool) : Scanner.TypedSpec (Option Bool)

Typed scanner for whether the final input bit equals target.

Equations

• Complexity.RAM.Structured.LastBit.spec target = { initial := none, step := fun (x : Option Bool) (bit : Bool) => some bit, accept := fun (state : Option Bool) => decide (state = some target) }

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.verdictReg : ℕ

Final verdict register inherited from the scanner layout.

Equations

• Complexity.RAM.Structured.LastBit.verdictReg = Complexity.RAM.Structured.Scanner.lengthReg

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.inputStore (target : Bool) : List Bool → Store

Reserved-prefix input store for the last-bit scanner.

Equations

• Complexity.RAM.Structured.LastBit.inputStore target = (Complexity.RAM.Structured.LastBit.spec target).inputStore

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.program (target : Bool) : Cmd

Structured RAM last-bit program.

Equations

• Complexity.RAM.Structured.LastBit.program target = (Complexity.RAM.Structured.LastBit.spec target).program

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.compiled (target : Bool) : Program

Concrete compiled RAM last-bit program.

Equations

• Complexity.RAM.Structured.LastBit.compiled target = (Complexity.RAM.Structured.LastBit.spec target).compiled

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.stepCount (target : Bool) : ℕ → ℕ

Exact compiled transition count.

Equations

• Complexity.RAM.Structured.LastBit.stepCount target = (Complexity.RAM.Structured.LastBit.spec target).stepCount

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.timeBound (target : Bool) : ℕ → ℕ

Explicit logarithmic-time budget.

Equations

• Complexity.RAM.Structured.LastBit.timeBound target = (Complexity.RAM.Structured.LastBit.spec target).timeBound

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.spaceBound (target : Bool) : ℕ → ℕ

Explicit peak-space budget.

Equations

• Complexity.RAM.Structured.LastBit.spaceBound target = (Complexity.RAM.Structured.LastBit.spec target).spaceBound

@[reducible, inline]

abbrev Complexity.RAM.Structured.LastBit.quasilinearBound (target : Bool) : ℕ → ℕ

Shifted quasilinear comparison function.

Equations

• Complexity.RAM.Structured.LastBit.quasilinearBound target = (Complexity.RAM.Structured.LastBit.spec target).quasilinearBound