Translating signed RAM data operations and tests

All five operations of GenericRAM.Signed.Arithmetic (addition, subtraction, multiplication, Euclidean division and Euclidean remainder), together with constants, copies, memory operations and signed comparisons, are translated to unsigned word-RAM code. The existing source interpreter, including its signed range and address checks, determines successful source steps. The target blocks operate on the separate register bank and encode every memory value.

Main definitions

• ToWordRAM.arithmeticCode, ToWordRAM.compileOp: unsigned instruction blocks.
• ToWordRAM.compileCond: comparison returning a Boolean word and a constant one.

Main results

• ToWordRAM.exec_compileOp: successful source data operations transfer within twenty-three steps.
• ToWordRAM.exec_compileCond: signed comparisons transfer with a preserved source state.

References

The translation is an original implementation using the existing signed RAM semantics.

def Cslib.GenericRAM.Signed.ToWordRAM.arithmeticCode {r : ℕ} : Arithmetic → WordRAM.Code WordRAM.Basis.standard (r + 9)

Unsigned instruction block implementing each of the five signed arithmetic operations.

def Cslib.GenericRAM.Signed.ToWordRAM.addressCode {r : ℕ} (a : Fin r) : WordRAM.Code WordRAM.Basis.standard (r + 9)

Decode a nonnegative signed address into scratch register left.

def Cslib.GenericRAM.Signed.ToWordRAM.operandsCode {r : ℕ} (a b : Fin r) : WordRAM.Code WordRAM.Basis.standard (r + 9)

Copy both operands to scratch before updating any source register.

def Cslib.GenericRAM.Signed.ToWordRAM.compileOp {r : ℕ} : Op model r → WordRAM.Code WordRAM.Basis.standard (r + 9)

Translate one data operation, retaining source memory addresses.

def Cslib.GenericRAM.Signed.ToWordRAM.compileCond {r : ℕ} : Cond model r → WordRAM.Code WordRAM.Basis.standard (r + 9)

Translate equality or signed ordering. result holds zero or one and two holds one.

theorem Cslib.GenericRAM.Signed.ToWordRAM.exec_address {r w : ℕ} {s : Data model r} {x : WordRAM.Data (r + 9)} (hx : Represents w s x) (a : Fin r) (ha : 0 ≤ s.regs a) : ∃ (y : WordRAM.Data (r + 9)), WordRAM.ExecWithin (w + 2) (addressCode a) x y 2 ∧ y.regs WordRAM.Signed.left = Int.toNat (s.regs a) ∧ Represents w s y

Nonnegative signed addresses are decoded in two instructions without changing source data.

theorem Cslib.GenericRAM.Signed.ToWordRAM.exec_operands {r w : ℕ} {s : Data model r} {x : WordRAM.Data (r + 9)} (hx : Represents w s x) (a b : Fin r) : ∃ (y : WordRAM.Data (r + 9)), WordRAM.ExecWithin (w + 2) (operandsCode a b) x y 2 ∧ y.regs WordRAM.Signed.left = WordRAM.Signed.encode (s.regs a) ∧ y.regs WordRAM.Signed.right = WordRAM.Signed.encode (s.regs b) ∧ Represents w s y

Copy the operands to the arithmetic workspace without changing represented source data.

theorem Cslib.GenericRAM.Signed.ToWordRAM.exec_compileOp {r w : ℕ} {s t : Data model r} {x : WordRAM.Data (r + 9)} (o : Op model r) (hx : Represents w s x) (he : Op.eval w o s = some t) : ∃ (y : WordRAM.Data (r + 9)), WordRAM.ExecWithin (w + 2) (compileOp o) x y 23 ∧ Represents w t y

Every successful source data operation has an unsigned implementation in at most twenty-three instructions at width w + 2. Aliased source/destination registers are allowed.

theorem Cslib.GenericRAM.Signed.ToWordRAM.exec_compileCond {r w : ℕ} {s : Data model r} {x : WordRAM.Data (r + 9)} (c : Cond model r) (hx : Represents w s x) {b : Bool} (he : Cond.eval w c s = some b) : ∃ (y : WordRAM.Data (r + 9)), WordRAM.ExecWithin (w + 2) (compileCond c) x y 14 ∧ (y.regs WordRAM.Signed.result = if b = true then 1 else 0) ∧ y.regs WordRAM.Signed.two = 1 ∧ Represents w s y

Every successful source test is implemented within fourteen instructions, returning its Boolean result and preserving the source data. Scratch register two is set to one.