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. An explicit adapter relates the original word semantics to this core without changing its public API.

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.