Random access machines: operational metatheory (proof internals)

This module proves the structural facts about RAM.run, RAM.logTimeUpto, RAM.unitTimeUpto, and register support that the surface theorems rely on:

• Unfolding lemmas and the fixed-point behaviour of a halted configuration (step_halted, run_halted, logTimeUpto_halted, unitTimeUpto_halted).
• Run/cost algebra: run_one, run_succ_step, and the additive decompositions run_add, logTimeUpto_add, unitTimeUpto_add, giving stationarity of the run and cost once halted, and monotonicity of the cost in the fuel.
• Cost lower bounds: every executed step costs at least one time unit (Instr.one_le_logCost), so the step count never exceeds the logarithmic time (unitTimeUpto_le_logTimeUpto).
• Finite support: the register file has finite support along any run from a finitely-supported start (run_finiteSupport), which is what makes the finsum-based space measure RAM.Cfg.space a genuine finite sum.

Not intended for human audit: the definitions in Defs.lean and the theorem statements in the surface module carry the mathematical content.

Unfolding lemmas

@[simp]

theorem Complexity.RAM.run_zero (P : Program) (c : Cfg) : run P 0 c = c

@[simp]

theorem Complexity.RAM.logTimeUpto_zero (P : Program) (c : Cfg) : logTimeUpto P 0 c = 0

@[simp]

theorem Complexity.RAM.unitTimeUpto_zero (P : Program) (c : Cfg) : unitTimeUpto P 0 c = 0

theorem Complexity.RAM.run_succ (P : Program) (fuel : ℕ) (c : Cfg) : run P (fuel + 1) c = if Halted P c then c else run P fuel (step P c)

theorem Complexity.RAM.logTimeUpto_succ (P : Program) (fuel : ℕ) (c : Cfg) : logTimeUpto P (fuel + 1) c = if Halted P c then 0 else stepLogCost P c + logTimeUpto P fuel (step P c)

theorem Complexity.RAM.unitTimeUpto_succ (P : Program) (fuel : ℕ) (c : Cfg) : unitTimeUpto P (fuel + 1) c = if Halted P c then 0 else 1 + unitTimeUpto P fuel (step P c)

Halted configurations are fixed points

theorem Complexity.RAM.step_halted (P : Program) {c : Cfg} (h : Halted P c) : step P c = c

Stepping a halted configuration is a no-op: halt leaves everything fixed.

theorem Complexity.RAM.run_halted (P : Program) {c : Cfg} (h : Halted P c) (fuel : ℕ) : run P fuel c = c

Running a halted configuration for any amount of fuel leaves it fixed.

theorem Complexity.RAM.logTimeUpto_halted (P : Program) {c : Cfg} (h : Halted P c) (fuel : ℕ) : logTimeUpto P fuel c = 0

A halted configuration accumulates no logarithmic time.

theorem Complexity.RAM.unitTimeUpto_halted (P : Program) {c : Cfg} (h : Halted P c) (fuel : ℕ) : unitTimeUpto P fuel c = 0

A halted configuration accumulates no unit time.

Run/cost algebra

theorem Complexity.RAM.run_one (P : Program) (c : Cfg) : run P 1 c = step P c

One unit of fuel performs exactly one step (a no-op if already halted).

theorem Complexity.RAM.run_add (P : Program) (a b : ℕ) (c : Cfg) : run P (a + b) c = run P b (run P a c)

The run decomposes additively: a + b steps is b steps after a steps.

theorem Complexity.RAM.run_succ_step (P : Program) (n : ℕ) (c : Cfg) : run P (n + 1) c = step P (run P n c)

Running n + 1 steps is one step after running n steps.

theorem Complexity.RAM.logTimeUpto_add (P : Program) (a b : ℕ) (c : Cfg) : logTimeUpto P (a + b) c = logTimeUpto P a c + logTimeUpto P b (run P a c)

Logarithmic time decomposes additively along the run.

theorem Complexity.RAM.unitTimeUpto_add (P : Program) (a b : ℕ) (c : Cfg) : unitTimeUpto P (a + b) c = unitTimeUpto P a c + unitTimeUpto P b (run P a c)

Unit time decomposes additively along the run.

theorem Complexity.RAM.run_eq_of_halted_le (P : Program) {c : Cfg} {f f' : ℕ} (hle : f ≤ f') (h : Halted P (run P f c)) : run P f' c = run P f c

Once halted after f steps, extra fuel does not change the configuration.

theorem Complexity.RAM.logTimeUpto_eq_of_halted_le (P : Program) {c : Cfg} {f f' : ℕ} (hle : f ≤ f') (h : Halted P (run P f c)) : logTimeUpto P f' c = logTimeUpto P f c

Once halted after f steps, extra fuel does not change the logarithmic time.

theorem Complexity.RAM.logTimeUpto_mono (P : Program) {c : Cfg} {f f' : ℕ} (hle : f ≤ f') : logTimeUpto P f c ≤ logTimeUpto P f' c

Logarithmic time is monotone in the fuel.

theorem Complexity.RAM.unitTimeUpto_mono (P : Program) {c : Cfg} {f f' : ℕ} (hle : f ≤ f') : unitTimeUpto P f c ≤ unitTimeUpto P f' c

Unit time is monotone in the fuel.

Cost lower bounds

theorem Complexity.RAM.Instr.one_le_logCost (i : Instr) (c : Cfg) : 1 ≤ i.logCost c

Every instruction costs at least one time unit under the logarithmic measure (the base cost).

theorem Complexity.RAM.one_le_stepLogCost (P : Program) (c : Cfg) : 1 ≤ stepLogCost P c

Every executed step costs at least one time unit.

theorem Complexity.RAM.unitTimeUpto_le_logTimeUpto (P : Program) (fuel : ℕ) (c : Cfg) : unitTimeUpto P fuel c ≤ logTimeUpto P fuel c

The number of steps taken never exceeds the logarithmic time: each step costs at least one time unit, so log-time dominates the step count.

theorem Complexity.RAM.unitTimeUpto_eq_of_not_halted (P : Program) (c : Cfg) (fuel : ℕ) (h : ∀ j < fuel, ¬Halted P (run P j c)) : unitTimeUpto P fuel c = fuel

If no halt occurs in the first fuel steps, the unit time is exactly the fuel (every step is counted).

Finite support of the register file

theorem Complexity.RAM.support_update_subset (f : ℕ → ℕ) (i v : ℕ) : Function.support (Function.update f i v) ⊆ insert i (Function.support f)

The support of an updated function is contained in the support of the original with the written index inserted.

theorem Complexity.RAM.initRegs_finiteSupport (x : List Bool) : (Function.support (initRegs x)).Finite

The initial register file has finite support: only registers 0 … |x| can be nonzero.

theorem Complexity.RAM.stepInstr_finiteSupport (i : Instr) (c : Cfg) (h : (Function.support c.regs).Finite) : (Function.support (stepInstr i c).regs).Finite

One instruction preserves finite support of the register file: each instruction writes at most one register.

theorem Complexity.RAM.step_finiteSupport (P : Program) (c : Cfg) (h : (Function.support c.regs).Finite) : (Function.support (step P c).regs).Finite

One step preserves finite support of the register file.

theorem Complexity.RAM.run_finiteSupport (P : Program) (fuel : ℕ) (c : Cfg) (h : (Function.support c.regs).Finite) : (Function.support (run P fuel c).regs).Finite

Finite support of the register file is a run invariant.

theorem Complexity.RAM.run_initCfg_finiteSupport (P : Program) (fuel : ℕ) (x : List Bool) : (Function.support (run P fuel (initCfg x)).regs).Finite

Finite support along any run started from an initial configuration. This guarantees RAM.Cfg.space is a genuine finite sum, not the finsum fallback value 0.