Finite configurations for RAM simulation

A configuration stores a finite register tuple, a natural control label, an explicit default value, and a distinct-key sparse memory. Its denotation is a generic RAM state. Denotation need not be injective: recording a default-valued cell and omitting that cell have the same semantics.

Dispatch walks a fixed finite program, comparing the current label with fixed instruction positions. Successor labels are fixed by those positions. This decomposition supports a native machine for each fixed program without requiring a uniform interpreter for encoded programs.

Main definitions

• FiniteState: finite configurations with a uniform, explicitly supplied memory default.
• FiniteState.step: one finite-state step, including every generic RAM check and fault.

Main results

• FiniteState.denote_step: exact one-step refinement, including continuation, halt and fault.

References

Uses the generic RAM semantics and Mathlib's association-list memory representation.

structure Cslib.GenericRAM.FiniteState (M : Model) (r : ℕ) : Type

Finite data from which a total RAM state is interpreted.

• pc : ℕ

  Current instruction label.

• regs : Fin r → M.Value

  Fixed finite register tuple.

• default : M.Value

  Value returned by an absent memory binding.

• memory : SparseMemory M.Address M.Value

  Distinct stored addresses, including explicitly stored default-valued cells.

theorem Cslib.GenericRAM.FiniteState.ext {M : Model} {r : ℕ} {x y : FiniteState M r} (pc : x.pc = y.pc) (regs : x.regs = y.regs) (default : x.default = y.default) (memory : x.memory = y.memory) : x = y

theorem Cslib.GenericRAM.FiniteState.ext_iff {M : Model} {r : ℕ} {x y : FiniteState M r} : x = y ↔ x.pc = y.pc ∧ x.regs = y.regs ∧ x.default = y.default ∧ x.memory = y.memory

def Cslib.GenericRAM.FiniteState.denote {M : Model} {r : ℕ} (s : FiniteState M r) : State M r

Interpret sparse memory using the supplied default. This map is not required to be injective.

def Cslib.GenericRAM.FiniteState.set {M : Model} {r : ℕ} (s : FiniteState M r) (d : Fin r) (v : M.Value) : FiniteState M r

Replace one register, preserving control and memory.

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

Replace one memory binding, preserving control, registers and the default.

@[simp]

theorem Cslib.GenericRAM.FiniteState.denote_set {M : Model} {r : ℕ} (s : FiniteState M r) (d : Fin r) (v : M.Value) : (s.set d v).denote = { pc := s.pc, data := s.denote.data.set d v }

@[simp]

theorem Cslib.GenericRAM.FiniteState.denote_write {M : Model} {r : ℕ} (s : FiniteState M r) (a : M.Address) (v : M.Value) : (s.write a v).denote = { pc := s.pc, data := s.denote.data.write a v }

def Cslib.GenericRAM.FiniteState.move {M : Model} {r : ℕ} (k : M.Config) (s : FiniteState M r) (d : Fin r) (v : M.Value) : Option (FiniteState M r)

Validate an existing value before moving it into a register.

def Cslib.GenericRAM.FiniteState.evalOp {M : Model} {r : ℕ} (k : M.Config) (o : Op M r) (s : FiniteState M r) : Option (FiniteState M r)

Finite execution of a fixed data instruction. Checked producers include admissibility.

theorem Cslib.GenericRAM.FiniteState.denote_move {M : Model} {r : ℕ} (k : M.Config) (s : FiniteState M r) (d : Fin r) (v : M.Value) : Option.map (fun (t : FiniteState M r) => t.denote.data) (move k s d v) = Data.move k s.denote.data d v

Moving a value commutes with interpretation, including invalid moves.

theorem Cslib.GenericRAM.FiniteState.denote_evalOp {M : Model} {r : ℕ} (k : M.Config) (o : Op M r) (s : FiniteState M r) : Option.map (fun (t : FiniteState M r) => t.denote.data) (evalOp k o s) = Op.eval k o s.denote.data

Finite data execution has exactly the generic data semantics, including failure.

@[reducible, inline]

abbrev Cslib.GenericRAM.FiniteState.Result (M : Model) (r : ℕ) : Type

The three finite outcomes use ordinary option and sum encodings.

def Cslib.GenericRAM.FiniteState.denoteResult {M : Model} {r : ℕ} : Result M r → Outcome M r

Interpret all three outcomes; none is a fault, not a halted state.

def Cslib.GenericRAM.FiniteState.resume {M : Model} {r : ℕ} (k : M.Config) (pc : ℕ) (s : FiniteState M r) : Result M r

Check the continuation label before returning the updated configuration.

@[simp]

theorem Cslib.GenericRAM.FiniteState.denote_resume {M : Model} {r : ℕ} (k : M.Config) (pc : ℕ) (s : FiniteState M r) : denoteResult (resume k pc s) = Outcome.continue k { pc := pc, data := s.denote.data }

def Cslib.GenericRAM.FiniteState.evalInstr {M : Model} {r : ℕ} (k : M.Config) (nextPC : ℕ) (i : Instr M r) (s : FiniteState M r) : Result M r

Execute a fixed instruction with a fixed ordinary successor label.

def Cslib.GenericRAM.FiniteState.dispatch {M : Model} {r : ℕ} (k : M.Config) : Program M r → ℕ → FiniteState M r → Result M r

Search fixed instruction positions. The successor is fixed at the matching position.

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

A finite-state step checks the current label before fixed-program dispatch.

theorem Cslib.GenericRAM.FiniteState.dispatch_eq_getElem? {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (pc : ℕ) (s : FiniteState M r) (h : pc ≤ s.pc) : dispatch k p pc s = do let i ← p[s.pc - pc]? evalInstr k (s.pc + 1) i s

Dispatch agrees with indexed lookup wherever the current label is at or above the offset.

theorem Cslib.GenericRAM.FiniteState.denote_step {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : FiniteState M r) : denoteResult (step k p s) = GenericRAM.step k p s.denote

Exact one-step refinement for arbitrary finite configurations, including all faults. No validity premise on the memory default or the initial registers is hidden in the theorem.