RAMs with arbitrary data values

The control labels of a RAM are natural numbers; its memory addresses and data values need not be. Model specifies operations and tests by signatures, a separate type of constant symbols, admissible produced values, and an explicit partial interpretation of values as addresses. Neither a real nor a field element is implicitly converted into an integer address. The configuration parameter has no prescribed meaning in the core; an instance may use a natural address-word width, or a singleton configuration type.

Operations, tests, constant interpretation and address extraction may fail. Constants and operations check admissibility of their result; moves and halts have a separate configurable validity check. Control labels are checked before instructions and after continuing steps. A successful run costs one per instruction, including its final halt. Interpretations are mathematical functions: executable instances require executable interpretations. No bit-cost bound or simulation of real arithmetic by a Turing machine is claimed.

This factors the finite-register, indirect-memory semantics of Cslib.WordRAM, adapted from MIT–ULB CompGeom Group. Cslib.WordRAM.Basis.genericModel represents the word semantics exactly in this core, and the word RAM's interpreter properties, such as Cslib.WordRAM.Executes.unique, are the results below transported along that representation.

Main definitions

• Model: data values, constant symbols, operation/test signatures and their semantics.
• Op, Cond, Instr, Program: data instructions, tests and flat programs.
• Data, State, Outcome: machine data, control state and step outcomes.
• step, run, Executes: single steps, fuel-bounded interpretation and exact halting cost.
• Data.init: an input convention with explicit default registers and initial memory.

Main results

• executes_iff_exists_run_eq: the interpreter characterizes exact halting executions.
• Executes.unique: a halting output and its instruction count are unique.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

structure Cslib.GenericRAM.Model : Type (max (max (max (a + 1) (c + 1)) (u + 1)) (v + 1))

The data and primitive operations of a RAM. The parameter is an external configuration, not an implicit conversion between values and addresses.

• Value : Type u

  Values stored in registers and memory.

• Address : Type a

  Memory addresses, distinct from natural control labels and from data values.

• decAddress : DecidableEq self.Address

  Addresses support functional updates.

• Config : Type c

  External machine configuration (for example a word width).

• Const : Type v

  Literal symbols permitted in a finite program, separately from arbitrary data values.

• operations : Circuits.Signature

  The operation symbols and their arities.

• tests : Circuits.Signature

  The test symbols and their arities.

• constant : self.Config → self.Const → Option self.Value

  Interpret a constant symbol, possibly failing.

• evalOp : self.Config → (f : self.operations.Op) → (Fin (self.operations.Arity f) → self.Value) → Option self.Value

  Interpret an operation on its register arguments, possibly failing.

• evalTest : self.Config → (f : self.tests.Op) → (Fin (self.tests.Arity f) → self.Value) → Option Bool

  Interpret a test on its register arguments, possibly failing.

• admissible : self.Config → self.Value → Bool

  Check a newly produced constant or operation result.

• address : self.Config → self.Value → Option self.Address

  Explicitly extract an address. Failure causes a load or store to fault.

• validMove : self.Config → self.Value → Bool

  Check existing values moved by copy/load/store or returned by halt.

• validPC : self.Config → ℕ → Bool

  Check control labels before an instruction and after a continuing step.

structure Cslib.GenericRAM.Data (M : Model) (r : ℕ) : Type (max u_1 u_3)

Register contents and indirectly addressed memory.

• regs : Fin r → M.Value

  The finite register file.

• mem : M.Address → M.Value

  Memory uses the address type chosen by the model.

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

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

def Cslib.GenericRAM.Data.set {M : Model} {r : ℕ} (x : Data M r) (i : Fin r) (v : M.Value) : Data M r

Replace a register.

def Cslib.GenericRAM.Data.write {M : Model} {r : ℕ} (x : Data M r) (a : M.Address) (v : M.Value) : Data M r

Replace a memory cell.

def Cslib.GenericRAM.Data.put {M : Model} {r : ℕ} (k : M.Config) (x : Data M r) (i : Fin r) (v : M.Value) : Option (Data M r)

Store a produced value if it is admissible.

def Cslib.GenericRAM.Data.init {M : Model} {r : ℕ} (default : M.Value) (memory : M.Address → M.Value) : Data M r

Initialize registers with an explicit default and memory with an explicit function. Input layout and any length header are conventions supplied by the caller.

def Cslib.GenericRAM.Data.move {M : Model} {r : ℕ} (k : M.Config) (x : Data M r) (i : Fin r) (v : M.Value) : Option (Data M r)

Move an existing value when allowed by the model.

inductive Cslib.GenericRAM.Cond (M : Model) (r : ℕ) : Type

A test applied to named registers.

• test {M : Model} {r : ℕ} (f : M.tests.Op) (args : Fin (M.tests.Arity f) → Fin r) : Cond M r

  Apply a test symbol to its register arguments.

inductive Cslib.GenericRAM.Op (M : Model) (r : ℕ) : Type u_2

A data instruction. Operations and constants are supplied by the model.

• const {M : Model} {r : ℕ} (d : Fin r) (c : M.Const) : Op M r

  Interpret a literal into a register.

• copy {M : Model} {r : ℕ} (d s : Fin r) : Op M r

  Copy a register.

• alu {M : Model} {r : ℕ} (f : M.operations.Op) (d : Fin r) (args : Fin (M.operations.Arity f) → Fin r) : Op M r

  Apply a primitive operation.

• load {M : Model} {r : ℕ} (d a : Fin r) : Op M r

  Read the address extracted from register a.

• store {M : Model} {r : ℕ} (a s : Fin r) : Op M r

  Write to the address extracted from register a.

inductive Cslib.GenericRAM.Instr (M : Model) (r : ℕ) : Type u_2

Flat instructions, with natural control labels.

• op {M : Model} {r : ℕ} (o : Op M r) : Instr M r

  Perform a data instruction and advance.

• jump {M : Model} {r : ℕ} (target : ℕ) : Instr M r

  Jump to a label.

• branch {M : Model} {r : ℕ} (c : Cond M r) (target : ℕ) : Instr M r

  Jump when the test returns true; advance on false; fault on test failure.

• halt {M : Model} {r : ℕ} (i : Fin r) : Instr M r

  Return a register's value.

@[reducible, inline]

abbrev Cslib.GenericRAM.Program (M : Model) (r : ℕ) : Type u_2

A finite instruction sequence.

structure Cslib.GenericRAM.State (M : Model) (r : ℕ) : Type (max u_1 u_3)

A natural control label and machine data.

• pc : ℕ

  The next instruction index.

• data : Data M r

  Registers and memory.

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

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

inductive Cslib.GenericRAM.Outcome (M : Model) (r : ℕ) : Type (max u_1 u_3)

A step continues, halts with a data value, or faults.

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

  Continue in a state.

• halt {M : Model} {r : ℕ} (v : M.Value) : Outcome M r

  Halt with an output value.

• fault {M : Model} {r : ℕ} : Outcome M r

  Undefined instruction, primitive, test, address, or inadmissible result.

def Cslib.GenericRAM.Cond.eval {M : Model} {r : ℕ} (k : M.Config) : Cond M r → Data M r → Option Bool

Evaluate a test; a failed test is distinct from false.

def Cslib.GenericRAM.Op.eval {M : Model} {r : ℕ} (k : M.Config) : Op M r → Data M r → Option (Data M r)

Evaluate a data instruction. Loads/stores require explicit successful address extraction.

def Cslib.GenericRAM.Outcome.continue {M : Model} {r : ℕ} (k : M.Config) (s : State M r) : Outcome M r

Continue only if the destination control label is valid.

def Cslib.GenericRAM.step {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : State M r) : Outcome M r

Execute one instruction. Validate the current control label and every continuation label.

def Cslib.GenericRAM.Next {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s t : State M r) : Prop

A nonhalting, nonfaulting transition.

@[reducible, inline]

abbrev Cslib.GenericRAM.Runs {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) : State M r → State M r → ℕ → Prop

Exactly the stated number of nonhalting transitions.

def Cslib.GenericRAM.Executes {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : State M r) (v : M.Value) (n : ℕ) : Prop

A halting execution, counting the final halt as one instruction.

def Cslib.GenericRAM.run {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) : ℕ → State M r → Option (M.Value × ℕ)

Run with an instruction budget. none means a fault or exhausted fuel, never a halting output. On success, retain the output and exact number of executed instructions.

theorem Cslib.GenericRAM.Executes.halt {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} (h : step w p s = Outcome.halt v) : Executes w p s v 1

theorem Cslib.GenericRAM.Executes.head {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s t : State M r} {v : M.Value} {n : ℕ} (h : Next w p s t) (ht : Executes w p t v n) : Executes w p s v (n + 1)

theorem Cslib.GenericRAM.Executes.of_runs {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s t : State M r} {v : M.Value} {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.GenericRAM.Executes.pos {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} {n : ℕ} (h : Executes w p s v n) : 0 < n

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

theorem Cslib.GenericRAM.Executes.of_run {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} {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.GenericRAM.Executes.run_eq {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} {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.GenericRAM.run_mono {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {fuel fuel' : ℕ} {vn : M.Value × ℕ} (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.GenericRAM.executes_iff_exists_run_eq {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} {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.GenericRAM.Executes.unique {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v v' : M.Value} {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 configuration and the state: its output and its number of instructions are unique.

theorem Cslib.GenericRAM.not_executes_of_fault {M : Model} {r : ℕ} {w : M.Config} {p : Program M r} {s : State M r} {v : M.Value} {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.