Representing signed RAM states by unsigned words

Source registers occupy target registers nine and above. The arithmetic workspace is disjoint from them. Source memory addresses are unchanged; each stored integer is encoded in one word.

Main definitions

• ToWordRAM.bank: the target register representing a source register.
• ToWordRAM.Represents: signed register bounds and the register/memory representation.

Main results

• ToWordRAM.Represents.set, ToWordRAM.Represents.write: representation after writes.
• ToWordRAM.Represents.of_frame: arithmetic blocks preserve represented source data.

References

This representation is an original implementation choice for the existing signed RAM.

def Cslib.GenericRAM.Signed.ToWordRAM.bank {r : ℕ} (i : Fin r) : Fin (r + 9)

Source registers follow the nine unsigned arithmetic registers.

theorem Cslib.GenericRAM.Signed.ToWordRAM.bank_injective {r : ℕ} : Function.Injective bank

Distinct source registers have distinct target registers.

theorem Cslib.GenericRAM.Signed.ToWordRAM.bank_ne_scratch {r : ℕ} (i : Fin r) {j : Fin (r + 9)} (hj : ↑j < 9) : bank i ≠ j

Source register cells are disjoint from the arithmetic workspace.

structure Cslib.GenericRAM.Signed.ToWordRAM.Represents {r : ℕ} (w : ℕ) (x : Data model r) (y : WordRAM.Data (r + 9)) : Prop

The source registers fit their signed width; target registers and memory encode the source data. Scratch values are unconstrained at instruction boundaries.

• fits (i : Fin r) : Fits w (x.regs i)

  Every source register is a signed word.

• regs (i : Fin r) : y.regs (bank i) = WordRAM.Signed.encode (x.regs i)

  The register bank stores canonical signed encodings.

• mem (a : ℕ) : y.mem a = WordRAM.Signed.encode (x.mem a)

  Memory uses unchanged addresses and encoded values.

theorem Cslib.GenericRAM.Signed.ToWordRAM.Represents.scratch {r w : ℕ} {x : Data model r} {y : WordRAM.Data (r + 9)} (h : Represents w x y) {i : Fin (r + 9)} (hi : ↑i < 9) (v : ℕ) : Represents w x (y.set i v)

Arithmetic scratch writes do not change the represented signed state.

theorem Cslib.GenericRAM.Signed.ToWordRAM.Represents.of_frame {r w : ℕ} {x : Data model r} {y z : WordRAM.Data (r + 9)} (h : Represents w x y) (hf : WordRAM.Signed.Frame y z) : Represents w x z

Framed arithmetic preserves all represented source registers and memory.

theorem Cslib.GenericRAM.Signed.ToWordRAM.Represents.set {r w : ℕ} {x : Data model r} {y : WordRAM.Data (r + 9)} (h : Represents w x y) (i : Fin r) {v : ℤ} (hv : Fits w v) : Represents w (x.set i v) (y.set (bank i) (WordRAM.Signed.encode v))

A fitting signed register update is represented by a single bank update.

theorem Cslib.GenericRAM.Signed.ToWordRAM.Represents.write {r w : ℕ} {x : Data model r} {y : WordRAM.Data (r + 9)} (h : Represents w x y) (a : ℕ) (v : ℤ) : Represents w (x.write a v) (y.write a (WordRAM.Signed.encode v))

A signed memory update uses the same address and the encoded value.