Word RAMs as generic RAMs

Every word-RAM basis determines a GenericRAM.Model. Values, addresses, constants and the configuration are natural numbers, with the configuration interpreted as word width. Operations use the original basis; equality and unsigned comparison are the tests. Only constants and operation results check word fit, exactly as in WordRAM.Defs; existing values and control labels remain unchecked. Address extraction is the identity, including on arbitrary initial states.

The adapter preserves each step, including faults, and every fuel-bounded result and exact instruction count. It does not impose new validity assumptions on existing WordRAM states.

Main definitions

• Basis.genericModel: the generic model associated to a word-RAM operation basis.
• Data.toGeneric, State.toGeneric, Program.toGeneric: the exact representation adapter.

Main results

• step_toGeneric: one step has the identical continuation, halt or fault.
• run_toGeneric, executes_toGeneric_iff: output and exact instruction counts agree.

References

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

@[reducible, inline]

abbrev Cslib.WordRAM.Basis.genericModel (B : Basis) : GenericRAM.Model

Natural word values and addresses, with exactly the existing word-RAM checking policy. The two test symbols are false for equality and true for unsigned comparison.

def Cslib.WordRAM.Data.toGeneric {r : ℕ} (B : Basis) (x : Data r) : GenericRAM.Data B.genericModel r

Identical registers and memory in the generic representation.

def Cslib.WordRAM.State.toGeneric {r : ℕ} (B : Basis) (s : State r) : GenericRAM.State B.genericModel r

Identical control label, registers and memory in the generic representation.

def Cslib.WordRAM.Cond.toGeneric {r : ℕ} (B : Basis) : Cond r → GenericRAM.Cond B.genericModel r

Translate an equality or comparison test.

def Cslib.WordRAM.Op.toGeneric {B : Basis} {r : ℕ} : Op B r → GenericRAM.Op B.genericModel r

Translate a data instruction without changing its registers or operation.

def Cslib.WordRAM.Instr.toGeneric {B : Basis} {r : ℕ} : Instr B r → GenericRAM.Instr B.genericModel r

Translate an instruction without changing its control labels.

def Cslib.WordRAM.Program.toGeneric {B : Basis} {r : ℕ} (p : Program B r) : GenericRAM.Program B.genericModel r

Instruction-for-instruction translation to the generic core.

theorem Cslib.WordRAM.Program.length_toGeneric {B : Basis} {r : ℕ} (p : Program B r) : List.length p.toGeneric = List.length p

Translation preserves the number of instructions.

theorem Cslib.WordRAM.Data.toGeneric_init {r : ℕ} (B : Basis) (input : List ℕ) : toGeneric B (init input) = GenericRAM.Data.init 0 fun (a : B.genericModel.Address) => if a = 0 then input.length else input.getD (a - 1) 0

The original input convention is an explicit generic initialization, with no charged work.

def Cslib.WordRAM.Outcome.toGeneric {r : ℕ} (B : Basis) : Outcome r → GenericRAM.Outcome B.genericModel r

Translate a step outcome without changing its meaning.

theorem Cslib.WordRAM.Op.eval_toGeneric {B : Basis} {r : ℕ} (o : Op B r) (w : ℕ) (x : Data r) : GenericRAM.Op.eval w o.toGeneric (Data.toGeneric B x) = Option.map (Data.toGeneric B) (eval w o x)

Data instructions preserve success and failure, even on unbounded initial data.

theorem Cslib.WordRAM.Cond.eval_toGeneric {B : Basis} {r : ℕ} (c : Cond r) (w : ℕ) (x : Data r) : GenericRAM.Cond.eval w (toGeneric B c) (Data.toGeneric B x) = some (decide (c.Holds x))

Tests have precisely the original truth value and never fail.

theorem Cslib.WordRAM.step_toGeneric {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : GenericRAM.step w p.toGeneric (State.toGeneric B s) = Outcome.toGeneric B (step w p s)

Exact step correspondence, including faults and arbitrary initial states.

theorem Cslib.WordRAM.run_toGeneric {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (fuel : ℕ) (s : State r) : GenericRAM.run w p.toGeneric fuel (State.toGeneric B s) = run w p fuel s

The interpreter returns exactly the original output and instruction count at every fuel.

theorem Cslib.WordRAM.executes_toGeneric_iff {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} : GenericRAM.Executes w p.toGeneric (State.toGeneric B s) v n ↔ Executes w p s v n

Halting executions agree in both directions, with the exact same instruction count.