Why the RAM must use logarithmic cost: a formal soundness theorem

This module turns the model's central design decision into a theorem. A RAM stores unbounded natural numbers in each register. Under the unit-cost measure (one time unit per instruction, RAM.unitTimeUpto) a program can repeatedly square a register, reaching 2 ^ (2 ^ k) in k + 1 steps. That number has 2 ^ k + 1 binary digits, so any Turing machine needs at least 2 ^ k steps merely to write it: unit-cost RAM time is super-polynomially stronger than Turing time, and the two models are not polynomially equivalent.

RAM.logGap_squaring proves exactly this gap for the concrete squaring program family RAM.sqProg, whose only literal is the constant 2: on the same run from the all-zero configuration RAM.sqStart, register 1 reaches 2 ^ (2 ^ k) and the unit time is k + 1, while the logarithmic time (RAM.logTimeUpto, which charges each instruction the bit-length of the numbers it manipulates) is at least 2 ^ k. This is why the library adopts the logarithmic cost measure and never the unit-cost one — the difference is not a convention but the boundary between a sound Turing-equivalent model and a "reward-hacked" one that decides more than it should in polynomial time.

def Complexity.RAM.sqProg (k : ℕ) : Program

The k-fold squaring program: load 2 into register 1, then square register 1 a total of k times. After j + 1 steps register 1 holds 2 ^ (2 ^ j).

Equations

• Complexity.RAM.sqProg k = Complexity.RAM.Instr.imm 1 2 :: List.replicate k (Complexity.RAM.Instr.mul 1 1 1)

def Complexity.RAM.sqStart : Cfg

The start configuration for the squaring family: program counter 0, all registers 0.

Equations

• Complexity.RAM.sqStart = { pc := 0, regs := fun (x : ℕ) => 0 }

theorem Complexity.RAM.logGap_squaring (k : ℕ) : Halted (sqProg k) (run (sqProg k) (k + 1) sqStart) ∧ (run (sqProg k) (k + 1) sqStart).regs 1 = 2 ^ 2 ^ k ∧ unitTimeUpto (sqProg k) (k + 1) sqStart = k + 1 ∧ 2 ^ k ≤ logTimeUpto (sqProg k) (k + 1) sqStart

The unit-vs-logarithmic gap for the squaring family. On the run of the k-fold squaring program sqProg k from the all-zero configuration sqStart for k + 1 steps:

• the machine halts;
• register 1 holds 2 ^ (2 ^ k), a number with 2 ^ k + 1 bits;
• the unit time is k + 1 (linear in k);
• the logarithmic time is at least 2 ^ k (exponential in k).

The only literal in sqProg k is the constant 2 of its first imm, so the large value is produced by the k multiplications rather than loaded. Hence any complexity measure based on unit cost differs super-polynomially from logarithmic cost, and only the logarithmic measure is polynomially related to Turing-machine time. This is the formal justification for the library's cost convention.