Structured logarithmic-cost RAM programs

This module exposes a minimal imperative authoring language above the concrete logarithmic-cost RAM. Source commands have independent register-store semantics; Cmd.compile lowers structured conditionals and loops to absolute RAM jumps.

The main transfer theorem, Exec.compile_correct, is exact in all three dimensions carried by Exec: final registers, operand-sensitive logarithmic time, and peak register space. Thus source proofs can remain at the structured level without weakening the concrete RAM resource statement.

Switch.select supplies the verified finite numeric case split used by the Turing-machine transition compiler. Its branch selection has exact step accounting and preserves explicit logarithmic-cost and space envelopes.

theorem Complexity.RAM.Structured.Cmd.length_compile (cmd : Cmd) : List.length cmd.compile = cmd.codeSize + 1

A closed compiled command consists of its generated code followed by one halt instruction.

theorem Complexity.RAM.Structured.Exec.compile_correct {cmd : Cmd} {initial final : Store} {steps cost space : ℕ} (hexec : Exec cmd initial final steps cost space) : run cmd.compile steps { pc := 0, regs := initial } = { pc := cmd.codeSize, regs := final } ∧ logTimeUpto cmd.compile steps { pc := 0, regs := initial } = cost ∧ spaceUpto cmd.compile steps { pc := 0, regs := initial } = space

Exact semantic and resource preservation for closed compilation.

theorem Complexity.RAM.Structured.Exec.compile_halted {cmd : Cmd} {initial final : Store} {steps cost space : ℕ} (hexec : Exec cmd initial final steps cost space) : Halted cmd.compile (run cmd.compile steps { pc := 0, regs := initial })

A source execution reaches the halt instruction appended by Cmd.compile.