Verified structured RAM last-bit scanner

The typed scanner compiler supplies the implementation, exact execution proof, and resource bounds. This module adds only agreement with the existing Language.lastBitZero and Language.lastBitOne specifications.

@[simp]

theorem Complexity.RAM.Structured.LastBit.stepCount_eq (target : Bool) (inputLength : ℕ) : stepCount target inputLength = 18 + 9 * inputLength

The three-state last-bit scanner takes exactly 18 + 9n transitions.

theorem Complexity.RAM.Structured.LastBit.program_performance (target : Bool) (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program target) (inputStore target bits) final (stepCount target bits.length) cost space ∧ cost ≤ timeBound target bits.length ∧ space ≤ spaceBound target bits.length ∧ final verdictReg = Input.bitValue (decide (bits.getLast? = some target))

Source correctness and explicit resource bounds for the last-bit scanner.

theorem Complexity.RAM.Structured.LastBit.compiled_performance (target : Bool) (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program target) (inputStore target bits) final (stepCount target bits.length) cost space ∧ run (compiled target) (stepCount target bits.length) { pc := 0, regs := inputStore target bits } = { pc := (program target).codeSize, regs := final } ∧ Halted (compiled target) (run (compiled target) (stepCount target bits.length) { pc := 0, regs := inputStore target bits }) ∧ logTimeUpto (compiled target) (stepCount target bits.length) { pc := 0, regs := inputStore target bits } ≤ timeBound target bits.length ∧ spaceUpto (compiled target) (stepCount target bits.length) { pc := 0, regs := inputStore target bits } ≤ spaceBound target bits.length ∧ ((run (compiled target) (stepCount target bits.length) { pc := 0, regs := inputStore target bits }).regs verdictReg = 1 ↔ bits.getLast? = some target)

End-to-end compiled performance and language correctness.

theorem Complexity.RAM.Structured.LastBit.timeBound_bigO_quasilinear (target : Bool) : BigO (timeBound target) (quasilinearBound target)

The explicit time budget is quasilinear.

theorem Complexity.RAM.Structured.LastBit.spaceBound_bigO_quasilinear (target : Bool) : BigO (spaceBound target) (quasilinearBound target)

The explicit peak-space budget is quasilinear.