Verified finite-state structured RAM scanners #

This module exposes a reusable compiler from numeric finite automata to the structured RAM frontend. Its correctness theorem includes an exact transition count and explicit logarithmic-time and peak-space bounds, all transferred to the concrete compiled RAM.

source

theorem Complexity.RAM.Structured.Scanner.program_performance (spec : Spec) (bits : List Bool) :

∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program spec) (inputStore spec bits) final (stepCount spec bits.length) cost space ∧ cost ≤ timeBound spec bits.length ∧ space ≤ spaceBound spec bits.length ∧ final lengthReg = Input.bitValue (spec.accept (List.foldl spec.step spec.initial bits))

Source-level correctness and explicit resource bounds.

source

theorem Complexity.RAM.Structured.Scanner.compiled_performance (spec : Spec) (bits : List Bool) :

∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program spec) (inputStore spec bits) final (stepCount spec bits.length) cost space ∧ run (compiled spec) (stepCount spec bits.length) { pc := 0, regs := inputStore spec bits } = { pc := (program spec).codeSize, regs := final } ∧ Halted (compiled spec) (run (compiled spec) (stepCount spec bits.length) { pc := 0, regs := inputStore spec bits }) ∧ logTimeUpto (compiled spec) (stepCount spec bits.length) { pc := 0, regs := inputStore spec bits } ≤ timeBound spec bits.length ∧ spaceUpto (compiled spec) (stepCount spec bits.length) { pc := 0, regs := inputStore spec bits } ≤ spaceBound spec bits.length ∧ (run (compiled spec) (stepCount spec bits.length) { pc := 0, regs := inputStore spec bits }).regs lengthReg = Input.bitValue (spec.accept (List.foldl spec.step spec.initial bits))

End-to-end performance and correctness of the compiled concrete RAM.

source

theorem Complexity.RAM.Structured.Scanner.typed_program_performance {State : Type} [FinEnum State] (typed : TypedSpec State) (bits : List Bool) :

∃ (final : Store) (cost : ℕ) (space : ℕ), Exec typed.program (typed.inputStore bits) final (typed.stepCount bits.length) cost space ∧ cost ≤ typed.timeBound bits.length ∧ space ≤ typed.spaceBound bits.length ∧ final lengthReg = Input.bitValue (typed.accept (List.foldl typed.step typed.initial bits))

Source-level correctness and resource bounds for a typed scanner.

source

theorem Complexity.RAM.Structured.Scanner.typed_compiled_performance {State : Type} [FinEnum State] (typed : TypedSpec State) (bits : List Bool) :

∃ (final : Store) (cost : ℕ) (space : ℕ), Exec typed.program (typed.inputStore bits) final (typed.stepCount bits.length) cost space ∧ run typed.compiled (typed.stepCount bits.length) { pc := 0, regs := typed.inputStore bits } = { pc := typed.program.codeSize, regs := final } ∧ Halted typed.compiled (run typed.compiled (typed.stepCount bits.length) { pc := 0, regs := typed.inputStore bits }) ∧ logTimeUpto typed.compiled (typed.stepCount bits.length) { pc := 0, regs := typed.inputStore bits } ≤ typed.timeBound bits.length ∧ spaceUpto typed.compiled (typed.stepCount bits.length) { pc := 0, regs := typed.inputStore bits } ≤ typed.spaceBound bits.length ∧ (run typed.compiled (typed.stepCount bits.length) { pc := 0, regs := typed.inputStore bits }).regs lengthReg = Input.bitValue (typed.accept (List.foldl typed.step typed.initial bits))

End-to-end concrete RAM correctness for a typed scanner.

source

theorem Complexity.RAM.Structured.Scanner.timeBound_bigO_quasilinear (spec : Spec) :

BigO (timeBound spec) (quasilinearBound spec)

For each fixed scanner, its explicit time budget is quasilinear.

source

theorem Complexity.RAM.Structured.Scanner.spaceBound_bigO_quasilinear (spec : Spec) :

BigO (spaceBound spec) (quasilinearBound spec)

For each fixed scanner, its explicit peak-space budget is quasilinear.

source