Structured logarithmic-cost RAM programs — proof internals

This file proves that absolute-jump lowering preserves the independent source semantics exactly: final registers, logarithmic cost, and peak register space.

theorem Complexity.RAM.Structured.Cmd.length_compileAt (cmd : Cmd) (start : ℕ) : List.length (compileAt start cmd) = cmd.codeSize

theorem Complexity.RAM.Structured.compileAt_correct_internal {cmd : Cmd} {initial final : Store} {steps cost space : ℕ} (hexec : Exec cmd initial final steps cost space) (pre suffix : Program) : have P := pre ++ Cmd.compileAt (List.length pre) cmd ++ suffix; have start := { pc := List.length pre, regs := initial }; run P steps start = { pc := List.length pre + cmd.codeSize, regs := final } ∧ logTimeUpto P steps start = cost ∧ spaceUpto P steps start = space