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.
• 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.Op, Cslib.WordRAM.Instr, Cslib.WordRAM.Program: conditions, 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.State: registers with memory, and with a program counter.
• Cslib.WordRAM.Op.eval: the effect of a data instruction, none on a fault.
• Cslib.WordRAM.step: one step of a program, which continues, halts with an output, or faults.
• 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.State.init, Cslib.WordRAM.InputFits: the initial state on an input, and inputs whose length and words fit a word.
• 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)

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

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

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

@[simp]

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

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

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.

@[instance_reducible]

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

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

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 and halting. 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.

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_iff {r : ℕ} {x y : Data r} : x = y ↔ x.regs = y.regs ∧ x.mem = y.mem

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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)

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

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_iff {r : ℕ} {x y : State r} : x = y ↔ x.pc = y.pc ∧ x.data = y.data

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

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)

@[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

@[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

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

@[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))

@[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)

@[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)))

@[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))

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))

@[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)

@[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)

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 }

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

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 }

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 }

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)

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

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)

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

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

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

@[simp]

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

@[simp]

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

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)

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

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)

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)

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)

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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.