Verified structured RAM pair validator

This table-driven RAM program reimplements the same five-state automaton as TM.pairValidateTM. Its proof gives an exact transition count, explicit logarithmic-cost time and peak-space budgets, and an end-to-end compiled-RAM correctness theorem for the canonical pair-encoding language.

@[simp]

theorem Complexity.RAM.Structured.PairValidate.stepCount_eq (inputLength : ℕ) : stepCount inputLength = 24 + 9 * inputLength

The five-state pair validator takes exactly 24 + 9n transitions.

theorem Complexity.RAM.Structured.PairValidate.program_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits.length) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ final lengthReg = Input.bitValue (TM.pairValidateAccept (List.foldl TM.pairValidateStep TM.PairValidateState.next bits))

Source-level correctness and explicit resource bounds.

theorem Complexity.RAM.Structured.PairValidate.compiled_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits.length) cost space ∧ run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits }) ∧ logTimeUpto compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } ≤ timeBound bits.length ∧ spaceUpto compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } ≤ spaceBound bits.length ∧ (run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits }).regs lengthReg = Input.bitValue (TM.pairValidateAccept (List.foldl TM.pairValidateStep TM.PairValidateState.next bits)) ∧ ((run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits }).regs lengthReg = 1 ↔ bits ∈ validPairEncoding)

End-to-end compiled performance and language correctness.

theorem Complexity.RAM.Structured.PairValidate.timeBound_bigO_quasilinear : BigO timeBound quasilinearBound

The explicit logarithmic-cost time budget is quasilinear.

theorem Complexity.RAM.Structured.PairValidate.spaceBound_bigO_quasilinear : BigO spaceBound quasilinearBound

The explicit peak-space budget is quasilinear.