Signed arithmetic implemented by unsigned word-RAM instructions

The input registers hold the encodings of two signed integers. The routines use only ordinary unsigned arithmetic, comparisons and branches; no signed operation is added to the machine. The bounds exclude the final halt; Exec.executes adds exactly one instruction. Registers left (index 0) and right (index 1) are inputs, result (index 2) is the output, and indices 3 through 8 are scratch, including two (index 3). Memory and all other registers are preserved. Code.rename can place the routines in a larger register file.

The source semantics are GenericRAM.Signed.Arithmetic.eval, covering all five operations: addition, subtraction, multiplication, Euclidean division and Euclidean remainder, including Lean's total zero-divisor conventions (a / 0 = 0 and a % 0 = a). The common w + 2 allowance covers exact out-of-range sums, differences and minimum/-1 quotients; it is not a minimal-width claim for results that fit the source range.

Main definitions

• Signed.add, Signed.subtract, Signed.multiply, Signed.divide, Signed.modulo: fixed unsigned instruction blocks.
• Signed.Frame: preservation of memory, operands and registers outside the workspace.

Main results

• Signed.exec_add, Signed.exec_subtract, Signed.exec_multiply, Signed.exec_divide, Signed.exec_modulo: charged executions with two extra unsigned bits, independent of the operands and source width.

References

The instruction blocks and their representation are original implementation choices.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.left {r : ℕ} : Fin (r + 9)

First encoded operand.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.right {r : ℕ} : Fin (r + 9)

Second encoded operand.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.result {r : ℕ} : Fin (r + 9)

Encoded result.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.two {r : ℕ} : Fin (r + 9)

Constant two, used to extract magnitudes and signs.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.magA {r : ℕ} : Fin (r + 9)

Decoded magnitude of the first operand.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.magB {r : ℕ} : Fin (r + 9)

Decoded magnitude of the second operand.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.signA {r : ℕ} : Fin (r + 9)

First operand sign, later reused for the result sign.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.signB {r : ℕ} : Fin (r + 9)

Second operand sign.

@[reducible, inline]

abbrev Cslib.WordRAM.Signed.zero {r : ℕ} : Fin (r + 9)

Constant zero, used to normalize the result.

def Cslib.WordRAM.Signed.unpack {r : ℕ} : Code Basis.standard (r + 9)

Decode the two input words into four scratch registers in six instructions.

def Cslib.WordRAM.Signed.finish {r : ℕ} : Code Basis.standard (r + 9)

Encode a magnitude and sign, setting the sign of zero to zero.

def Cslib.WordRAM.Signed.addMagnitudes {r : ℕ} : Code Basis.standard (r + 9)

Add equal-sign magnitudes, or subtract the smaller opposite-sign magnitude.

def Cslib.WordRAM.Signed.addCore {r : ℕ} : Code Basis.standard (r + 9)

Combine decoded operands and encode their sum.

def Cslib.WordRAM.Signed.add {r : ℕ} : Code Basis.standard (r + 9)

Add two sign-and-magnitude words, normalizing the sign of zero.

def Cslib.WordRAM.Signed.flipRightSign {r : ℕ} : Code Basis.standard (r + 9)

Reverse the right sign bit; the result register temporarily holds the constant one.

def Cslib.WordRAM.Signed.subtract {r : ℕ} : Code Basis.standard (r + 9)

Subtract by reversing the second operand's sign before the addition block. The temporary sign of zero is immaterial and the result is normalized.

def Cslib.WordRAM.Signed.multiplyMagnitudes {r : ℕ} : Code Basis.standard (r + 9)

Multiply the decoded magnitudes and set the product sign.

def Cslib.WordRAM.Signed.multiply {r : ℕ} : Code Basis.standard (r + 9)

Multiply the magnitudes and compare the signs, normalizing the sign of zero.

def Cslib.WordRAM.Signed.divideMagnitudes {r : ℕ} : Code Basis.standard (r + 9)

Compute the Euclidean quotient magnitude and sign from decoded operands.

def Cslib.WordRAM.Signed.divide {r : ℕ} : Code Basis.standard (r + 9)

Signed Euclidean division on sign-and-magnitude words, matching Lean's a / 0 = 0 convention and, for b ≠ 0, Lean's Euclidean Int.ediv: the quotient for which a % b lies in [0, |b|) (rounding toward -∞ when b > 0 and toward +∞ when b < 0).

def Cslib.WordRAM.Signed.moduloCore {r : ℕ} : Code Basis.standard (r + 9)

Compute the encoded Euclidean remainder from decoded operands, preserving a % 0 = a.

def Cslib.WordRAM.Signed.modulo {r : ℕ} : Code Basis.standard (r + 9)

Signed Euclidean remainder on sign-and-magnitude words, matching Lean's a % 0 = a convention and returning a nonnegative remainder below |b| when b ≠ 0.

def Cslib.WordRAM.Signed.Frame {r : ℕ} (x y : Data (r + 9)) : Prop

Memory and registers outside the output and six scratch registers are unchanged.

theorem Cslib.WordRAM.Signed.exec_add {r w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : Data (r + 9)) (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin (w + 2) add x y 15 ∧ y.regs result = encode (GenericRAM.Signed.Arithmetic.add.eval a b) ∧ Frame x y

Signed addition runs within fifteen instructions at unsigned width w + 2. The result is exact even when the sum does not fit the source signed range.

theorem Cslib.WordRAM.Signed.exec_subtract {r w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : Data (r + 9)) (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin (w + 2) subtract x y 17 ∧ y.regs result = encode (GenericRAM.Signed.Arithmetic.sub.eval a b) ∧ Frame x y

Signed subtraction runs within seventeen instructions at unsigned width w + 2. The result is exact even when the difference does not fit the source signed range.

theorem Cslib.WordRAM.Signed.exec_multiply {r w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (hp : GenericRAM.Signed.Fits w (a * b)) (x : Data (r + 9)) (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin (w + 2) multiply x y 14 ∧ y.regs result = encode (GenericRAM.Signed.Arithmetic.mul.eval a b) ∧ Frame x y

Signed multiplication runs within fourteen instructions at unsigned width w + 2, provided the mathematical product fits the source signed range. No double-width unsigned product is needed: the magnitudes' product equals the magnitude of the signed result.

theorem Cslib.WordRAM.Signed.exec_divide {r w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : Data (r + 9)) (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin (w + 2) divide x y 20 ∧ y.regs result = encode (GenericRAM.Signed.Arithmetic.div.eval a b) ∧ Frame x y

Signed Euclidean division runs within twenty instructions at unsigned width w + 2, including Lean's a / 0 = 0 convention. The result is exact even at the minimum/-1 signed overflow (-2 ^ (w - 1)) / (-1) = 2 ^ (w - 1), where GenericRAM.Signed.model faults and the compiled block returns encode (2 ^ (w - 1)) without fault reflection.

theorem Cslib.WordRAM.Signed.exec_modulo {r w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : Data (r + 9)) (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin (w + 2) modulo x y 13 ∧ y.regs result = encode (GenericRAM.Signed.Arithmetic.mod.eval a b) ∧ Frame x y

Signed Euclidean remainder runs within thirteen instructions at unsigned width w + 2, including Lean's a % 0 = a convention.