Verified structured RAM terminated-unary decoder

This module exposes a reusable cursor decoder for the unary fields used by the serialized-circuit format. The source proof covers both successful termination and input exhaustion, and compilation preserves its exact transition count, logarithmic cost, peak space, decoded value, and suffix cursor.

theorem Complexity.RAM.Structured.UnaryDecode.mainLoop_performance {remaining : List Bool} {inputLength offset value : ℕ} {store : Store} (hready : CursorReady inputLength remaining offset value store) (hbound : Internal.StoreEnvelope (inputLength + inputBase) (inputLength + inputBase) store) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec mainLoop store final (loopStepCount remaining) cost space ∧ cost ≤ timeBound inputLength ∧ space ≤ spaceBound inputLength ∧ (match CircuitCode.NatCode.decodePrefix? remaining with | none => final verdictReg = 0 ∧ final valueReg = value + remaining.length ∧ final pointerReg = inputBase + inputLength ∧ final remainingReg = 0 | some (decoded, rest) => final verdictReg = 1 ∧ final valueReg = value + decoded ∧ final pointerReg = inputBase + offset + decoded + 1 ∧ final remainingReg = rest.length) ∧ final activeReg = 0 ∧ final oneReg = 1 ∧ (∀ (index : ℕ), inputBase ≤ index → final index = store index) ∧ Internal.StoreEnvelope (inputLength + inputBase) (inputLength + inputBase) final

Invoke the decoder loop as a resource-bounded cursor routine.

Unlike program_performance, this theorem does not require the standalone input initializer. It can therefore be sequenced after another parser step. The loop preserves every data register at or above inputBase.

theorem Complexity.RAM.Structured.UnaryDecode.program_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ match CircuitCode.NatCode.decodePrefix? bits with | none => final verdictReg = 0 ∧ final valueReg = bits.length ∧ final pointerReg = inputBase + bits.length ∧ final remainingReg = 0 | some (value, rest) => final verdictReg = 1 ∧ final valueReg = value ∧ final pointerReg = inputBase + value + 1 ∧ final remainingReg = rest.length

Source-level correctness with exact transitions and explicit resources.

theorem Complexity.RAM.Structured.UnaryDecode.compiled_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits) cost space ∧ run compiled (stepCount bits) { pc := 0, regs := inputStore bits } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount bits) { pc := 0, regs := inputStore bits }) ∧ logTimeUpto compiled (stepCount bits) { pc := 0, regs := inputStore bits } ≤ timeBound bits.length ∧ spaceUpto compiled (stepCount bits) { pc := 0, regs := inputStore bits } ≤ spaceBound bits.length ∧ match CircuitCode.NatCode.decodePrefix? bits with | none => final verdictReg = 0 ∧ final valueReg = bits.length ∧ final pointerReg = inputBase + bits.length ∧ final remainingReg = 0 | some (value, rest) => final verdictReg = 1 ∧ final valueReg = value ∧ final pointerReg = inputBase + value + 1 ∧ final remainingReg = rest.length

End-to-end concrete RAM performance and terminated-unary correctness.

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

The explicit logarithmic-cost time budget is quasilinear.

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

The explicit peak-space budget is quasilinear.