Structured RAM terminated-unary decoder — proof internals

theorem Complexity.RAM.Structured.UnaryDecode.mainLoop_measured_internal {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

theorem Complexity.RAM.Structured.UnaryDecode.program_measured_internal (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