Finite-state scanners for the structured RAM frontend

Scanner.Spec describes a finite automaton using numeric state codes. The compiler below realizes it as a table-driven structured RAM program. The state bound and transition-closure fields are the complete trusted interface needed by the generic correctness and resource proof.

structure Complexity.RAM.Structured.Scanner.Spec : Type

A total finite-state Boolean scanner with contiguous numeric state codes.

• stateCount : ℕ

  Number of valid state codes.

• initial : ℕ

  Initial state code.

• initial_lt : self.initial < self.stateCount

  The initial code is valid.

• step : ℕ → Bool → ℕ

  One state transition.

• step_lt (state : ℕ) : state < self.stateCount → ∀ (bit : Bool), self.step state bit < self.stateCount

  Transitions preserve valid state codes.

• accept : ℕ → Bool

  Final Boolean verdict.

structure Complexity.RAM.Structured.Scanner.TypedSpec (State : Type) [FinEnum State] : Type

A scanner specification over an explicitly enumerable Lean state type.

FinEnum retains a concrete equivalence with an initial segment of natural numbers, so lowering remains executable while consumers reason using their domain-specific state type.

• initial : State

  Initial typed state.

• step : State → Bool → State

  One typed state transition.

• accept : State → Bool

  Final Boolean verdict.

def Complexity.RAM.Structured.Scanner.TypedSpec.code {State : Type} [FinEnum State] (state : State) : ℕ

Numeric state code chosen by the explicit enumeration.

Equations

• Complexity.RAM.Structured.Scanner.TypedSpec.code state = ↑(FinEnum.equiv state)

def Complexity.RAM.Structured.Scanner.TypedSpec.numeric {State : Type} [FinEnum State] (typed : TypedSpec State) : Spec

Lower a typed scanner to the verified numeric scanner interface.

Equations

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

def Complexity.RAM.Structured.Scanner.lengthReg : ℕ

Remaining input length and final verdict register.

Equations

• Complexity.RAM.Structured.Scanner.lengthReg = 0

def Complexity.RAM.Structured.Scanner.stateReg : ℕ

Current numeric automaton state.

Equations

• Complexity.RAM.Structured.Scanner.stateReg = 1

def Complexity.RAM.Structured.Scanner.pointerReg : ℕ

Address of the next input bit.

Equations

• Complexity.RAM.Structured.Scanner.pointerReg = 2

def Complexity.RAM.Structured.Scanner.oneReg : ℕ

Constant-one register.

Equations

• Complexity.RAM.Structured.Scanner.oneReg = 3

def Complexity.RAM.Structured.Scanner.bitReg : ℕ

Current input bit.

Equations

• Complexity.RAM.Structured.Scanner.bitReg = 4

def Complexity.RAM.Structured.Scanner.addressReg : ℕ

Scratch address used for table lookups.

Equations

• Complexity.RAM.Structured.Scanner.addressReg = 5

def Complexity.RAM.Structured.Scanner.twoReg : ℕ

Constant-two register.

Equations

• Complexity.RAM.Structured.Scanner.twoReg = 6

def Complexity.RAM.Structured.Scanner.transitionBaseReg : ℕ

Register containing the transition-table base address.

Equations

• Complexity.RAM.Structured.Scanner.transitionBaseReg = 7

def Complexity.RAM.Structured.Scanner.acceptBaseReg : ℕ

Register containing the verdict-table base address.

Equations

• Complexity.RAM.Structured.Scanner.acceptBaseReg = 8

def Complexity.RAM.Structured.Scanner.transitionBase : ℕ

First transition-table register.

Equations

• Complexity.RAM.Structured.Scanner.transitionBase = 9

def Complexity.RAM.Structured.Scanner.acceptBase (spec : Spec) : ℕ

First verdict-table register.

Equations

• Complexity.RAM.Structured.Scanner.acceptBase spec = Complexity.RAM.Structured.Scanner.transitionBase + 2 * spec.stateCount

def Complexity.RAM.Structured.Scanner.inputBase (spec : Spec) : ℕ

First input register.

Equations

• Complexity.RAM.Structured.Scanner.inputBase spec = Complexity.RAM.Structured.Scanner.transitionBase + 3 * spec.stateCount

def Complexity.RAM.Structured.Scanner.transitionAddress (state : ℕ) (bit : Bool) : ℕ

Address of one transition-table entry.

Equations

• Complexity.RAM.Structured.Scanner.transitionAddress state bit = Complexity.RAM.Structured.Scanner.transitionBase + 2 * state + Complexity.RAM.Structured.Input.bitValue bit

def Complexity.RAM.Structured.Scanner.acceptAddress (spec : Spec) (state : ℕ) : ℕ

Address of one verdict-table entry.

Equations

• Complexity.RAM.Structured.Scanner.acceptAddress spec state = Complexity.RAM.Structured.Scanner.acceptBase spec + state

def Complexity.RAM.Structured.Scanner.inputStore (spec : Spec) (bits : List Bool) : Store

Reserved-prefix input layout for a scanner.

Equations

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

def Complexity.RAM.Structured.Scanner.fixedSetupIndices : List ℕ

The six fixed setup destinations below the tables.

Equations

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

def Complexity.RAM.Structured.Scanner.tableIndices (spec : Spec) : List ℕ

Every table destination, in increasing order.

Equations

• Complexity.RAM.Structured.Scanner.tableIndices spec = List.range' Complexity.RAM.Structured.Scanner.transitionBase (3 * spec.stateCount)

def Complexity.RAM.Structured.Scanner.setupIndices (spec : Spec) : List ℕ

Every setup destination.

Equations

• Complexity.RAM.Structured.Scanner.setupIndices spec = Complexity.RAM.Structured.Scanner.fixedSetupIndices ++ Complexity.RAM.Structured.Scanner.tableIndices spec

def Complexity.RAM.Structured.Scanner.setupValue (spec : Spec) (index : ℕ) : ℕ

Value written to one setup destination.

Equations

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

def Complexity.RAM.Structured.Scanner.setupWrites (spec : Spec) : List (ℕ × ℕ)

Constant and table writes performed before scanning.

Equations

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

def Complexity.RAM.Structured.Scanner.setupOps (spec : Spec) : List Basic

Straight-line setup instruction list.

Equations

• Complexity.RAM.Structured.Scanner.setupOps spec = List.map (fun (write : ℕ × ℕ) => Complexity.RAM.Structured.Basic.imm write.1 write.2) (Complexity.RAM.Structured.Scanner.setupWrites spec)

def Complexity.RAM.Structured.Scanner.setup (spec : Spec) : Cmd

Initialize constants and transition/verdict tables.

Equations

• Complexity.RAM.Structured.Scanner.setup spec = Complexity.RAM.Structured.Cmd.basics (Complexity.RAM.Structured.Scanner.setupOps spec)

def Complexity.RAM.Structured.Scanner.bodyOps : List Basic

Seven-instruction scanner body, independent of the particular automaton.

Equations

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

def Complexity.RAM.Structured.Scanner.body : Cmd

Consume one input bit and update the encoded automaton state.

Equations

• Complexity.RAM.Structured.Scanner.body = Complexity.RAM.Structured.Cmd.basics Complexity.RAM.Structured.Scanner.bodyOps

def Complexity.RAM.Structured.Scanner.mainLoop : Cmd

Scan all input bits.

Equations

• Complexity.RAM.Structured.Scanner.mainLoop = Complexity.RAM.Structured.Cmd.whileNonzero Complexity.RAM.Structured.Scanner.lengthReg Complexity.RAM.Structured.Scanner.body

def Complexity.RAM.Structured.Scanner.finalizeOps : List Basic

Two-instruction final verdict lookup.

Equations

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

def Complexity.RAM.Structured.Scanner.finalize : Cmd

Write the final verdict to R₀.

Equations

• Complexity.RAM.Structured.Scanner.finalize = Complexity.RAM.Structured.Cmd.basics Complexity.RAM.Structured.Scanner.finalizeOps

def Complexity.RAM.Structured.Scanner.program (spec : Spec) : Cmd

Complete structured scanner.

Equations

• Complexity.RAM.Structured.Scanner.program spec = (Complexity.RAM.Structured.Scanner.setup spec).seq (Complexity.RAM.Structured.Scanner.mainLoop.seq Complexity.RAM.Structured.Scanner.finalize)

def Complexity.RAM.Structured.Scanner.compiled (spec : Spec) : Program

Concrete compiled RAM scanner.

Equations

• Complexity.RAM.Structured.Scanner.compiled spec = (Complexity.RAM.Structured.Scanner.program spec).compile

def Complexity.RAM.Structured.Scanner.stepCount (spec : Spec) (inputLength : ℕ) : ℕ

Exact compiled transition count.

Equations

• Complexity.RAM.Structured.Scanner.stepCount spec inputLength = 9 + 3 * spec.stateCount + 9 * inputLength

def Complexity.RAM.Structured.Scanner.timeBound (spec : Spec) (inputLength : ℕ) : ℕ

Explicit logarithmic-cost time budget.

Equations

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

def Complexity.RAM.Structured.Scanner.spaceBound (spec : Spec) (inputLength : ℕ) : ℕ

Explicit peak-space budget.

Equations

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

def Complexity.RAM.Structured.Scanner.quasilinearBound (spec : Spec) (inputLength : ℕ) : ℕ

Shifted quasilinear comparison function.

Equations

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

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.inputStore {State : Type} [FinEnum State] (typed : TypedSpec State) : List Bool → Store

Input store for a typed scanner.

Equations

• typed.inputStore = Complexity.RAM.Structured.Scanner.inputStore typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.program {State : Type} [FinEnum State] (typed : TypedSpec State) : Cmd

Structured RAM program generated from a typed scanner.

Equations

• typed.program = Complexity.RAM.Structured.Scanner.program typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.compiled {State : Type} [FinEnum State] (typed : TypedSpec State) : Program

Concrete RAM program generated from a typed scanner.

Equations

• typed.compiled = Complexity.RAM.Structured.Scanner.compiled typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.stepCount {State : Type} [FinEnum State] (typed : TypedSpec State) : ℕ → ℕ

Exact transition count for a typed scanner.

Equations

• typed.stepCount = Complexity.RAM.Structured.Scanner.stepCount typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.timeBound {State : Type} [FinEnum State] (typed : TypedSpec State) : ℕ → ℕ

Explicit logarithmic-time budget for a typed scanner.

Equations

• typed.timeBound = Complexity.RAM.Structured.Scanner.timeBound typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.spaceBound {State : Type} [FinEnum State] (typed : TypedSpec State) : ℕ → ℕ

Explicit peak-space budget for a typed scanner.

Equations

• typed.spaceBound = Complexity.RAM.Structured.Scanner.spaceBound typed.numeric

@[reducible, inline]

abbrev Complexity.RAM.Structured.Scanner.TypedSpec.quasilinearBound {State : Type} [FinEnum State] (typed : TypedSpec State) : ℕ → ℕ

Shifted quasilinear comparison function for a typed scanner.

Equations

• typed.quasilinearBound = Complexity.RAM.Structured.Scanner.quasilinearBound typed.numeric