Word RAMs

A word RAM is a random-access machine whose registers and memory cells hold w-bit words, and whose every instruction costs one unit of time. The word size must accommodate the input and its addresses; it may exceed O(log n) when input words do Cormen et al., Section 2.2 Fredman and Willard Hagerup. This file chooses an instruction-count model, parameterized by a basis of word operations (Cslib.WordRAM.Basis); the standard basis Cslib.WordRAM.Basis.standard has unit-cost multiplication, division, bitwise operations and shifts. It does not establish a bit-cost simulation.

The existing Cslib.RAM, inspired by Cook and Reckhow Cook and Reckhow, has unbounded natural-number registers and supports both unit and logarithmic cost measures. Cslib.WordRAM instead supplies bounded, faulting operational semantics, a finite named register file with indirect memory, and a different input and halting convention. Changing a cost measure alone does not change these operational choices. No simulation between these models or Turing machines is proved here.

This file defines the machine and its runs. Cslib.WordRAM.DecidableInTime allows width-indexed code of uniformly bounded length, width-dependent encodings and time bounds, and arbitrary admissible input/width pairs. Cslib.WordRAM.UniformDecidableInTime uses one fixed program. Structured programs (Cslib.WordRAM.Code) compile to the flat programs of this file with the same instruction counts.

The model

• A program (Cslib.WordRAM.Program B r) over a basis B is a list of instructions over a finite register file Fin r; besides the registers there is a memory indexed by natural numbers.
• Registers and memory cells hold natural numbers below 2 ^ w (Cslib.WordRAM.Fits).
• The data instructions (Cslib.WordRAM.Op) load a constant, copy a register, apply an operation of the basis to registers, and read or write the memory cell whose address is held in a register. The standard basis has the arithmetic, bitwise and shift operations (Cslib.WordRAM.BinOp, applied by Cslib.WordRAM.Op.bin) and reads the word size w (Cslib.WordRAM.Op.width); the exact basis (Cslib.WordRAM.Basis.exact) has the same operations, with subtraction below zero and division by zero undefined. The control instructions jump, branch on an equality or unsigned comparison of two registers, and halt with the contents of a register as output. Instr.rand is the random-sampling instruction interpreted by Cslib.WordRAM.stepRand and Cslib.WordRAM.runRand. Deterministic Cslib.WordRAM.step faults on Instr.rand.
• A run starts at instruction 0 with all registers 0, the input length at address 0 and the input words at addresses 1, …, n (Cslib.WordRAM.State.init); all other cells hold 0. Installing this initial input and extracting the halting output are uncharged; executing the final halt costs one instruction.
• On a run from an input whose length and words fit a word (Cslib.WordRAM.InputFits), an instruction that would write a number of more than w bits into a register faults, and so do an operation whose value is undefined and running off the end of the program. A fault is not a result: only runs that halt count. Registers and memory hold words throughout such a run (Cslib.WordRAM.Runs.bounded_init), so every address is a word and the memory has 2 ^ w usable cells.

Design notes

The definitions are adapted from the Lean formalization accompanying MIT–ULB CompGeom Group. The modelling choices are these.

• Overflow faults instead of wrapping around modulo 2 ^ w. This formalizes the standard assumption that every value an algorithm computes fits a word Cormen et al., Section 2.2: a run that succeeds never relies on wrapping. Hence a successful run of a program that does not read the word size never depends on it: such a run succeeds identically at every larger word size (Cslib.WordRAM.Executes.mono_width). Algorithms that use arithmetic modulo 2 ^ w Hagerup must reduce explicitly, for instance with the word size and half-word arithmetic; this is not formalized here.
• Words are unsigned Hagerup. In the standard basis subtraction is truncated, and division and remainder by zero follow Lean's conventions x / 0 = 0 and x % 0 = x. In the exact basis these values are undefined, so the operation faults. These are part of this machine's semantics; transfer to a model with other conventions requires a separate simulation.
• The operations form a parameter, as the gates of a circuit do: word-RAM models differ in their instruction sets Hagerup. The standard basis has addition, subtraction, multiplication, bitwise operations and shifts as in Hagerup's multiplication RAM, together with division, remainder and an operation reading the word size, which word-RAM algorithms may use Fredman and Willard. Everything else about the machine is the same for every basis.
• Only constants and operations check that the number they write fits a word. Copies, loads and stores move words already held by the machine, and every address held in a register is a word, so on a run from an input that fits such checks could never fail (Cslib.WordRAM.Runs.bounded_init); omitting them spares every program proof their side conditions.
• Memory starts zeroed beyond the input, so a program may use any cell before writing it.
• The program counter is not required to fit a word. Each execution uses a finite program; the complexity predicates additionally bound code length independently of word size.
• Data instructions have one semantics, Cslib.WordRAM.Op.eval, shared by flat and structured programs; runs are counted with cslib's Relation.RelatesInSteps.

Compared with the source formalization, words are unsigned rather than two's-complement integers; the operations form a basis, whose standard instance adds bitwise operations, shifts and the word size to the source's arithmetic (Cslib.WordRAM.Basis.arithmetic); copies, loads, addresses and the halting output are not checked against the word size; the program counter is unbounded; the time classes of Cslib.WordRAM.LinearTime measure the word size by the number of binary digits of the size rather than by log₂ (size + 2) + 2; and an operation may be undefined, which faults. In particular, the exact basis faults on subtraction below zero and on division and remainder by zero. The source does not reject these cases as such: its signed subtraction may give a negative word, its division and remainder follow Lean's integer conventions x / 0 = 0 and x % 0 = x, and only its usual check that the result fits a signed word applies. The current classes allow width-indexed code; the Uniform variants retain the fixed-program convention.

Main definitions

• Cslib.WordRAM.Fits: a number fits a w-bit word.
• Cslib.WordRAM.Cond, Cslib.WordRAM.Cond.Holds, Cslib.WordRAM.Op, Cslib.WordRAM.Instr, Cslib.WordRAM.Program: conditions, their satisfaction, data instructions, instructions and programs over a basis.
• Cslib.WordRAM.Op.bin, Cslib.WordRAM.Op.width: the data instructions of the standard basis; Cslib.WordRAM.Op.exactBin, Cslib.WordRAM.Op.exactWidth: those of the exact basis.
• Cslib.WordRAM.Data, Cslib.WordRAM.Data.set, Cslib.WordRAM.Data.write, Cslib.WordRAM.Data.put, Cslib.WordRAM.State: registers with memory, register/memory updates, and state with a program counter.
• Cslib.WordRAM.Op.eval: the effect of a data instruction, none on a fault.
• Cslib.WordRAM.Outcome, Cslib.WordRAM.step, Cslib.WordRAM.Next: step outcome, one step of a program, and the single-step transition relation.
• Cslib.WordRAM.Runs, Cslib.WordRAM.Executes: runs of a given number of steps, and runs that halt with a given output after a given number of instructions, the halt included.
• Cslib.WordRAM.Data.init, Cslib.WordRAM.State.init, Cslib.WordRAM.InputFits, Cslib.WordRAM.Data.Bounded: initial data/state on an input, inputs whose length and words fit a word, and word-bounded machine data.
• Cslib.WordRAM.Op.ReadsWidth, Cslib.WordRAM.Instr.ReadsWidth, Cslib.WordRAM.Program.ReadsWidth: predicates for reading the word size w.
• Cslib.WordRAM.Instr.IsRandFree, Cslib.WordRAM.Program.IsRandFree: predicates for programs that do not use Instr.rand.
• Cslib.WordRAM.run: a computable interpreter with a step budget.

Main results

• Cslib.WordRAM.executes_iff_exists_run_eq: the interpreter computes exactly the halting runs.
• Cslib.WordRAM.Executes.unique: output and instruction count are determined by the program, the word size and the state.
• Cslib.WordRAM.Runs.bounded_init: from an input that fits, every reachable register and memory cell holds a w-bit word.
• Cslib.WordRAM.Executes.mono_width: a program that does not read the word size halts in the same way at every larger word size.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms
• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees
• T. Hagerup, Sorting and searching on the word RAM
• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

Words

def Cslib.WordRAM.Fits (w v : ℕ) : Prop

A number fits a w-bit word if it is below 2 ^ w.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableFits (w v : ℕ) : Decidable (Fits w v)

Decidability of Fits w v.

theorem Cslib.WordRAM.fits_iff {w v : ℕ} : Fits w v ↔ v < 2 ^ w

Fits w v unfolds to v < 2 ^ w.

theorem Cslib.WordRAM.Fits.mono {w w' v : ℕ} (h : Fits w v) (hw : w ≤ w') : Fits w' v

A word that fits in w bits also fits in any larger word width w'.

theorem Cslib.WordRAM.Fits.of_le {w u v : ℕ} (h : Fits w v) (huv : u ≤ v) : Fits w u

Any value at most a w-bit word also fits in w bits.

@[simp]

theorem Cslib.WordRAM.fits_zero (w : ℕ) : Fits w 0

Zero fits in every word width w.

theorem Cslib.WordRAM.fits_one {w : ℕ} (hw : w ≠ 0) : Fits w 1

One fits in every nonzero word width w.

theorem Cslib.WordRAM.fits_self (w : ℕ) : Fits w w

The word size fits a word, so that a program may read it.

Instructions

inductive Cslib.WordRAM.Cond (r : ℕ) : Type

The conditions on which a program branches: equality and unsigned comparison of two registers.

• eq {r : ℕ} (i j : Fin r) : Cond r

  Registers i and j hold equal words.

• lt {r : ℕ} (i j : Fin r) : Cond r

  Register i holds a smaller word than register j.

def Cslib.WordRAM.instDecidableEqCond.decEq {r✝ : ℕ} (x✝ x✝¹ : Cond r✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqCond {r✝ : ℕ} : DecidableEq (Cond r✝)

def Cslib.WordRAM.instReprCond.repr {r✝ : ℕ} : Cond r✝ → ℕ → Std.Format

@[instance_reducible]

instance Cslib.WordRAM.instReprCond {r✝ : ℕ} : Repr (Cond r✝)

inductive Cslib.WordRAM.Op (B : Basis) (r : ℕ) : Type

The data instructions over the basis B. Registers are named in the instruction; memory is addressed through the contents of a register.

• const {B : Basis} {r : ℕ} (d : Fin r) (v : ℕ) : Op B r

  const d v sets register d to the constant v.

• copy {B : Basis} {r : ℕ} (d s : Fin r) : Op B r

  copy d s sets register d to the contents of register s.

• alu {B : Basis} {r : ℕ} (f : B.Op) (d : Fin r) (args : Fin (B.Arity f) → Fin r) : Op B r

  alu f d args sets register d to the operation f of the basis applied to the registers args.

• load {B : Basis} {r : ℕ} (d a : Fin r) : Op B r

  load d a sets register d to the memory cell whose address is in register a.

• store {B : Basis} {r : ℕ} (a s : Fin r) : Op B r

  store a s sets the memory cell whose address is in register a to register s.

def Cslib.WordRAM.instDecidableEqOp.decEq {B✝ : Basis} {r✝ : ℕ} (x✝ x✝¹ : Op B✝ r✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqOp {B✝ : Basis} {r✝ : ℕ} : DecidableEq (Op B✝ r✝)

def Cslib.WordRAM.Op.bin {r : ℕ} (f : BinOp) (d i j : Fin r) : Op Basis.standard r

bin f d i j sets register d to the standard binary operation f applied to registers i and j.

def Cslib.WordRAM.Op.width {r : ℕ} (d : Fin r) : Op Basis.standard r

width d sets register d to the word size.

def Cslib.WordRAM.Op.exactBin {r : ℕ} (f : BinOp) (d i j : Fin r) : Op Basis.exact r

exactBin f d i j sets register d to the exact value of the binary operation f applied to registers i and j.

def Cslib.WordRAM.Op.exactWidth {r : ℕ} (d : Fin r) : Op Basis.exact r

exactWidth d sets register d to the word size, over the exact basis.

inductive Cslib.WordRAM.Instr (B : Basis) (r : ℕ) : Type

Instructions over the basis B: data instructions, jumps, conditional branches, halting, and random sampling. Jump and branch targets are instruction indices.

• op {B : Basis} {r : ℕ} (o : Op B r) : Instr B r

  Execute a data instruction and proceed to the next instruction.

• jump {B : Basis} {r : ℕ} (t : ℕ) : Instr B r

  Proceed to instruction t.

• branch {B : Basis} {r : ℕ} (c : Cond r) (t : ℕ) : Instr B r

  Proceed to instruction t if c holds, and to the next instruction otherwise.

• halt {B : Basis} {r : ℕ} (i : Fin r) : Instr B r

  Halt with the contents of register i as output.

• rand {B : Basis} {r : ℕ} (dst src : Fin r) : Instr B r

  Sample uniformly from [0, regs src] into register dst under randomized execution; faults under deterministic step.

def Cslib.WordRAM.instDecidableEqInstr.decEq {B✝ : Basis} {r✝ : ℕ} (x✝ x✝¹ : Instr B✝ r✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqInstr {B✝ : Basis} {r✝ : ℕ} : DecidableEq (Instr B✝ r✝)

@[reducible, inline]

abbrev Cslib.WordRAM.Program (B : Basis) (r : ℕ) : Type

A program over the basis B and r registers is a list of instructions, indexed by the program counter.

Data and states

structure Cslib.WordRAM.Data (r : ℕ) : Type

The data of a machine: register contents and memory.

• regs : Fin r → ℕ

  The contents of the registers.

• mem : ℕ → ℕ

  The contents of memory, by address.

theorem Cslib.WordRAM.Data.ext {r : ℕ} {x y : Data r} (regs : x.regs = y.regs) (mem : x.mem = y.mem) : x = y

theorem Cslib.WordRAM.Data.ext_iff {r : ℕ} {x y : Data r} : x = y ↔ x.regs = y.regs ∧ x.mem = y.mem

def Cslib.WordRAM.Data.set {r : ℕ} (x : Data r) (i : Fin r) (v : ℕ) : Data r

Set register i to v.

def Cslib.WordRAM.Data.write {r : ℕ} (x : Data r) (a v : ℕ) : Data r

Set the memory cell at address a to v.

@[simp]

theorem Cslib.WordRAM.Data.set_regs {r : ℕ} (x : Data r) (i : Fin r) (v : ℕ) : (x.set i v).regs = Function.update x.regs i v

Setting register i updates the register file at i.

@[simp]

theorem Cslib.WordRAM.Data.set_mem {r : ℕ} (x : Data r) (i : Fin r) (v : ℕ) : (x.set i v).mem = x.mem

Setting register i leaves memory unchanged.

@[simp]

theorem Cslib.WordRAM.Data.write_regs {r : ℕ} (x : Data r) (a v : ℕ) : (x.write a v).regs = x.regs

Writing to memory leaves the register file unchanged.

@[simp]

theorem Cslib.WordRAM.Data.write_mem {r : ℕ} (x : Data r) (a v : ℕ) : (x.write a v).mem = Function.update x.mem a v

Writing v at address a updates memory at a.

def Cslib.WordRAM.Data.put {r : ℕ} (w : ℕ) (x : Data r) (i : Fin r) (v : ℕ) : Option (Data r)

Set register i to v if v fits a w-bit word, and fault otherwise.

theorem Cslib.WordRAM.Data.put_of_fits {r w : ℕ} {x : Data r} {i : Fin r} {v : ℕ} (h : Fits w v) : put w x i v = some (x.set i v)

When v fits in w bits, put succeeds and sets register i to v.

theorem Cslib.WordRAM.Data.put_eq_some {r w : ℕ} {x y : Data r} {i : Fin r} {v : ℕ} : put w x i v = some y ↔ Fits w v ∧ x.set i v = y

put returns some y iff v fits in w bits and y = x.set i v.

structure Cslib.WordRAM.State (r : ℕ) : Type

A machine state: the index of the next instruction, and the data.

• pc : ℕ

  The program counter: the index of the next instruction.

• data : Data r

  Register contents and memory.

theorem Cslib.WordRAM.State.ext {r : ℕ} {x y : State r} (pc : x.pc = y.pc) (data : x.data = y.data) : x = y

theorem Cslib.WordRAM.State.ext_iff {r : ℕ} {x y : State r} : x = y ↔ x.pc = y.pc ∧ x.data = y.data

Semantics of instructions

def Cslib.WordRAM.Cond.Holds {r : ℕ} : Cond r → Data r → Prop

Whether a condition holds of the register contents.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableHolds {r : ℕ} (c : Cond r) (x : Data r) : Decidable (c.Holds x)

Decidability of Cond.Holds.

@[simp]

theorem Cslib.WordRAM.Cond.holds_eq {r : ℕ} {i j : Fin r} {x : Data r} : (eq i j).Holds x ↔ x.regs i = x.regs j

Cond.eq i j holds iff registers i and j have equal contents.

@[simp]

theorem Cslib.WordRAM.Cond.holds_lt {r : ℕ} {i j : Fin r} {x : Data r} : (lt i j).Holds x ↔ x.regs i < x.regs j

Cond.lt i j holds iff register i is strictly less than register j.

def Cslib.WordRAM.Op.eval {B : Basis} {r : ℕ} (w : ℕ) : Op B r → Data r → Option (Data r)

The effect of a data instruction at word size w, or none if it faults. Only constants and operations can produce a number that does not fit a word, and they fault when they do; an operation also faults when its value is undefined. Copying, loading and storing need no check: throughout a run from an input that fits, registers and memory hold words (Cslib.WordRAM.Runs.bounded_init), so every address held in a register is a word too.

@[simp]

theorem Cslib.WordRAM.Op.eval_const {B : Basis} {r : ℕ} (w : ℕ) (x : Data r) {d : Fin r} (v : ℕ) : eval w (const d v) x = Data.put w x d v

Evaluating Op.const d v writes v to register d via Data.put.

@[simp]

theorem Cslib.WordRAM.Op.eval_copy {B : Basis} {r : ℕ} (w : ℕ) (x : Data r) {d s : Fin r} : eval w (copy d s) x = some (x.set d (x.regs s))

Evaluating Op.copy d s copies register s into register d.

@[simp]

theorem Cslib.WordRAM.Op.eval_alu {B : Basis} {r : ℕ} (w : ℕ) (x : Data r) {d : Fin r} (f : B.Op) (args : Fin (B.Arity f) → Fin r) : eval w (alu f d args) x = (B.interp w f (x.regs ∘ args)).bind (Data.put w x d)

Evaluating Op.alu f d args interprets f on args and writes the result via Data.put.

@[simp]

theorem Cslib.WordRAM.Op.eval_load {B : Basis} {r : ℕ} (w : ℕ) (x : Data r) {d a : Fin r} : eval w (load d a) x = some (x.set d (x.mem (x.regs a)))

Evaluating Op.load d a loads the memory word at address x.regs a into register d.

@[simp]

theorem Cslib.WordRAM.Op.eval_store {B : Basis} {r : ℕ} (w : ℕ) (x : Data r) {s a : Fin r} : eval w (store a s) x = some (x.write (x.regs a) (x.regs s))

Evaluating Op.store a s stores x.regs s at memory address x.regs a.

theorem Cslib.WordRAM.Op.eval_alu_eq_some {B : Basis} {r w : ℕ} {x y : Data r} {f : B.Op} {d : Fin r} {args : Fin (B.Arity f) → Fin r} : eval w (alu f d args) x = some y ↔ ∃ (v : ℕ), B.interp w f (x.regs ∘ args) = some v ∧ Fits w v ∧ x.set d v = y

An operation succeeds when its value is defined and fits a word.

@[simp]

theorem Cslib.WordRAM.Op.eval_bin {r : ℕ} (w : ℕ) (f : BinOp) (d i j : Fin r) (x : Data r) : eval w (bin f d i j) x = Data.put w x d (f.eval (x.regs i) (x.regs j))

Evaluating a standard binary operation Op.bin f d i j writes f.eval via Data.put.

@[simp]

theorem Cslib.WordRAM.Op.eval_width {r : ℕ} (w : ℕ) (d : Fin r) (x : Data r) : eval w (width d) x = some (x.set d w)

The word size always fits a word, so reading it never faults.

@[simp]

theorem Cslib.WordRAM.Op.eval_exactBin {r : ℕ} (w : ℕ) (f : BinOp) (d i j : Fin r) (x : Data r) : eval w (exactBin f d i j) x = (f.evalExact (x.regs i) (x.regs j)).bind (Data.put w x d)

Evaluating an exact binary operation Op.exactBin f d i j binds f.evalExact to Data.put.

@[simp]

theorem Cslib.WordRAM.Op.eval_exactWidth {r : ℕ} (w : ℕ) (d : Fin r) (x : Data r) : eval w (exactWidth d) x = some (x.set d w)

Reading the word width in the exact basis always succeeds and writes w.

inductive Cslib.WordRAM.Outcome (r : ℕ) : Type

The outcome of a step: the next state, halting with an output, or a fault.

• next {r : ℕ} (s : State r) : Outcome r

  The run continues in the given state.

• halt {r : ℕ} (v : ℕ) : Outcome r

  The run halts with the given output.

• fault {r : ℕ} : Outcome r

  The run faults.

def Cslib.WordRAM.step {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : Outcome r

One step of program p at word size w: execute the instruction at the program counter. Running off the end of the program faults.

theorem Cslib.WordRAM.step_op {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {o : Op B r} {x : Data r} (hp : p[s.pc]? = some (Instr.op o)) (h : Op.eval w o s.data = some x) : step w p s = Outcome.next { pc := s.pc + 1, data := x }

Stepping on a data instruction that evaluates to some x advances pc by 1 with data x.

theorem Cslib.WordRAM.step_op_fault {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {o : Op B r} (hp : p[s.pc]? = some (Instr.op o)) (h : Op.eval w o s.data = none) : step w p s = Outcome.fault

Stepping on a data instruction that evaluates to none faults.

theorem Cslib.WordRAM.step_jump {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {t : ℕ} (hp : p[s.pc]? = some (Instr.jump t)) : step w p s = Outcome.next { pc := t, data := s.data }

Stepping on an unconditional jump sets pc to the target t.

theorem Cslib.WordRAM.step_branch {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {c : Cond r} {t : ℕ} (hp : p[s.pc]? = some (Instr.branch c t)) : step w p s = Outcome.next { pc := if c.Holds s.data then t else s.pc + 1, data := s.data }

Stepping on a conditional branch jumps to t when c holds and advances pc otherwise.

theorem Cslib.WordRAM.step_halt {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {i : Fin r} (hp : p[s.pc]? = some (Instr.halt i)) : step w p s = Outcome.halt (s.data.regs i)

Stepping on halt i halts with output s.data.regs i.

theorem Cslib.WordRAM.step_rand {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {dst src : Fin r} (hp : p[s.pc]? = some (Instr.rand dst src)) : step w p s = Outcome.fault

Stepping deterministically on rand dst src faults.

Runs

def Cslib.WordRAM.Next {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s t : State r) : Prop

One step of p at word size w leads from s to t.

@[reducible, inline]

abbrev Cslib.WordRAM.Runs {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) : State r → State r → ℕ → Prop

Runs w p s t n: running p at word size w leads from s to t in exactly n steps, none of which halts or faults.

def Cslib.WordRAM.Executes {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) (v n : ℕ) : Prop

Executes w p s v n: running p at word size w from s halts with output v after exactly n instructions, the final halt included. A run that faults executes nothing.

def Cslib.WordRAM.run {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) : ℕ → State r → Option (ℕ × ℕ)

Run p at word size w from s for at most fuel steps: some (v, n) if it halts with output v after n instructions, and none if it faults or needs more steps.

theorem Cslib.WordRAM.Executes.halt {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v : ℕ} (h : step w p s = Outcome.halt v) : Executes w p s v 1

A state that immediately halts executes in 1 instruction.

theorem Cslib.WordRAM.Executes.head {B : Basis} {r w : ℕ} {p : Program B r} {s t : State r} {v n : ℕ} (h : Next w p s t) (ht : Executes w p t v n) : Executes w p s v (n + 1)

Prepending a single transition Next w p s t increments the instruction count by 1.

theorem Cslib.WordRAM.Executes.of_runs {B : Basis} {r w : ℕ} {p : Program B r} {s t : State r} {v m n : ℕ} (h : Runs w p s t m) (ht : Executes w p t v n) : Executes w p s v (m + n)

A run followed by a halting run is a halting run.

theorem Cslib.WordRAM.Executes.pos {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} (h : Executes w p s v n) : 0 < n

Every halting execution takes at least one instruction.

theorem Cslib.WordRAM.run_succ {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {n : ℕ} : run w p (n + 1) s = match step w p s with | Outcome.next t => Option.map (fun (vn : ℕ × ℕ) => (vn.1, vn.2 + 1)) (run w p n t) | Outcome.halt v => some (v, 1) | Outcome.fault => none

Unfolding run for n + 1 steps of fuel.

theorem Cslib.WordRAM.Executes.of_run {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n fuel : ℕ} (h : run w p fuel s = some (v, n)) : Executes w p s v n

The interpreter only finds halting runs.

theorem Cslib.WordRAM.Executes.run_eq {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} (h : Executes w p s v n) : run w p n s = some (v, n)

A halting run of n instructions is found by the interpreter with n steps of fuel.

theorem Cslib.WordRAM.run_mono {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {fuel fuel' : ℕ} {vn : ℕ × ℕ} (h : run w p fuel s = some vn) (hle : fuel ≤ fuel') : run w p fuel' s = some vn

More fuel does not change a result of the interpreter.

theorem Cslib.WordRAM.executes_iff_exists_run_eq {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} : Executes w p s v n ↔ ∃ (fuel : ℕ), run w p fuel s = some (v, n)

The interpreter computes exactly the halting runs.

theorem Cslib.WordRAM.Executes.unique {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v v' n n' : ℕ} (h : Executes w p s v n) (h' : Executes w p s v' n') : v = v' ∧ n = n'

A halting run is determined by the program, the word size and the state: its output and its number of instructions are unique.

theorem Cslib.WordRAM.not_executes_of_fault {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} (h : step w p s = Outcome.fault) : ¬Executes w p s v n

A state from which the step faults has no halting run.

Inputs

def Cslib.WordRAM.Data.init {r : ℕ} (input : List ℕ) : Data r

The initial data on an input: all registers 0, the input length at address 0 and the input words at addresses 1, …, n, all other memory 0. Placing the input is the calling convention, not part of the program's cost.

def Cslib.WordRAM.State.init {r : ℕ} (input : List ℕ) : State r

The initial state on an input: the program counter at 0, and Data.init input.

@[simp]

theorem Cslib.WordRAM.Data.init_regs {r : ℕ} (input : List ℕ) (i : Fin r) : (init input).regs i = 0

All registers are initialized to 0 in Data.init.

@[simp]

theorem Cslib.WordRAM.Data.init_mem_zero {r : ℕ} (input : List ℕ) : (init input).mem 0 = input.length

Memory cell 0 holds the input length in Data.init.

@[simp]

theorem Cslib.WordRAM.Data.init_mem_succ {r : ℕ} (input : List ℕ) (a : ℕ) : (init input).mem (a + 1) = input.getD a 0

Memory cell a + 1 holds the a-th input word (or 0 out of bounds) in Data.init.

def Cslib.WordRAM.InputFits (w : ℕ) (input : List ℕ) : Prop

An input fits word size w if its length and all its words do.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableInputFits (w : ℕ) (input : List ℕ) : Decidable (InputFits w input)

Decidability of InputFits w input.

theorem Cslib.WordRAM.InputFits.mono {w w' : ℕ} {input : List ℕ} (h : InputFits w input) (hw : w ≤ w') : InputFits w' input

An input that fits in word size w also fits in any larger word size w'.

Word bounds

The machine holds only w-bit words: from an input that fits, every register and memory cell of every reachable state does.

def Cslib.WordRAM.Data.Bounded {r : ℕ} (w : ℕ) (x : Data r) : Prop

All registers and memory cells hold w-bit words.

theorem Cslib.WordRAM.Data.Bounded.init {r w : ℕ} {input : List ℕ} (h : InputFits w input) : Bounded w (Data.init input)

The initial data on an input that fits in w bits is word-bounded.

theorem Cslib.WordRAM.Data.Bounded.set {r w : ℕ} {x : Data r} (hx : Bounded w x) {i : Fin r} {v : ℕ} (hv : Fits w v) : Bounded w (x.set i v)

Setting a register to a w-bit word preserves Data.Bounded w.

theorem Cslib.WordRAM.Data.Bounded.write {r w : ℕ} {x : Data r} (hx : Bounded w x) {a v : ℕ} (hv : Fits w v) : Bounded w (x.write a v)

Writing a w-bit word to memory preserves Data.Bounded w.

theorem Cslib.WordRAM.Data.Bounded.op {B : Basis} {r w : ℕ} {x y : Data r} (hx : Bounded w x) {o : Op B r} (h : Op.eval w o x = some y) : Bounded w y

Any non-faulting data instruction preserves Data.Bounded w.

theorem Cslib.WordRAM.Next.bounded {B : Basis} {r w : ℕ} {p : Program B r} {s t : State r} (h : Next w p s t) (hs : Data.Bounded w s.data) : Data.Bounded w t.data

A step preserves word bounds.

theorem Cslib.WordRAM.Runs.bounded {B : Basis} {r w : ℕ} {p : Program B r} {s t : State r} {n : ℕ} (h : Runs w p s t n) (hs : Data.Bounded w s.data) : Data.Bounded w t.data

A run preserves word bounds.

theorem Cslib.WordRAM.Runs.bounded_init {B : Basis} {r w : ℕ} {p : Program B r} {input : List ℕ} {t : State r} {n : ℕ} (h : Runs w p (State.init input) t n) (hi : InputFits w input) : Data.Bounded w t.data

Every state reachable from an input that fits holds only w-bit words.

Larger word sizes

Overflow faults, so a program that does not read the word size cannot tell word sizes apart on a run that succeeds: the same run succeeds at every larger word size.

def Cslib.WordRAM.Op.ReadsWidth {B : Basis} {r : ℕ} : Op B r → Prop

The data instruction reads the word size: it applies an operation that the basis marks with Basis.ReadsWidth, such as Op.width in the standard basis.

@[instance_reducible]

instance Cslib.WordRAM.instDecidablePredOpReadsWidth {B : Basis} {r : ℕ} : DecidablePred Op.ReadsWidth

Decidability of Op.ReadsWidth.

@[simp]

theorem Cslib.WordRAM.Op.readsWidth_bin {r : ℕ} (f : BinOp) (d i j : Fin r) : ¬(bin f d i j).ReadsWidth

A binary ALU instruction Op.bin does not read the word width.

@[simp]

theorem Cslib.WordRAM.Op.readsWidth_width {r : ℕ} (d : Fin r) : (width d).ReadsWidth

The instruction Op.width reads the word width.

def Cslib.WordRAM.Instr.ReadsWidth {B : Basis} {r : ℕ} : Instr B r → Prop

The instruction reads the word size.

@[instance_reducible]

instance Cslib.WordRAM.instDecidablePredInstrReadsWidth {B : Basis} {r : ℕ} : DecidablePred Instr.ReadsWidth

Decidability of Instr.ReadsWidth.

def Cslib.WordRAM.Instr.IsRandFree {B : Basis} {r : ℕ} : Instr B r → Prop

An instruction is rand-free if it is not Instr.rand.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableIsRandFree {B : Basis} {r : ℕ} (i : Instr B r) : Decidable i.IsRandFree

Decidability of Instr.IsRandFree.

def Cslib.WordRAM.Program.IsRandFree {B : Basis} {r : ℕ} (p : Program B r) : Prop

A program is rand-free if none of its instructions is Instr.rand.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableIsRandFree_1 {B : Basis} {r : ℕ} (p : Program B r) : Decidable p.IsRandFree

Decidability of Program.IsRandFree.

def Cslib.WordRAM.Program.ReadsWidth {B : Basis} {r : ℕ} (p : Program B r) : Prop

A program reads the word size if one of its instructions does.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableReadsWidth {B : Basis} {r : ℕ} (p : Program B r) : Decidable p.ReadsWidth

Decidability of Program.ReadsWidth.

theorem Cslib.WordRAM.Op.eval_mono_width {B : Basis} {r w w' : ℕ} {o : Op B r} {x y : Data r} (ho : ¬o.ReadsWidth) (h : eval w o x = some y) (hw : w ≤ w') : eval w' o x = some y

A successful evaluation of a data instruction that does not read the word width gives the same result at any larger width.

theorem Cslib.WordRAM.Next.mono_width {B : Basis} {r w w' : ℕ} {p : Program B r} {s t : State r} (hp : ¬p.ReadsWidth) (h : Next w p s t) (hw : w ≤ w') : Next w' p s t

A single step of a program that does not read the word width is preserved at any larger width.

theorem Cslib.WordRAM.step_halt_mono_width {B : Basis} {r w w' : ℕ} {p : Program B r} {s : State r} {v : ℕ} (h : step w p s = Outcome.halt v) : step w' p s = Outcome.halt v

theorem Cslib.WordRAM.Runs.mono_width {B : Basis} {r w w' : ℕ} {p : Program B r} {s t : State r} {n : ℕ} (hp : ¬p.ReadsWidth) (h : Runs w p s t n) (hw : w ≤ w') : Runs w' p s t n

Multi-step runs of a program that does not read the word width lift to any larger width.

theorem Cslib.WordRAM.Executes.mono_width {B : Basis} {r w w' : ℕ} {p : Program B r} {s : State r} {v n : ℕ} (hp : ¬p.ReadsWidth) (h : Executes w p s v n) (hw : w ≤ w') : Executes w' p s v n

Word-size monotonicity. A program that does not read the word size halts in the same way at every larger word size.