Framed arithmetic on multiword register banks

The bank starts at physical register forty-four. Multiplication uses thirty-six scratch digits in registers eight through forty-three and copies the low eighteen digits into the destination. Subtraction copies its minuend into a fresh destination and clears that destination when a final borrow signals underflow. Both wrappers preserve memory and every other bank entry.

Main definitions

• Bank.multiply: multiplication through a separate full-product scratch area.
• Bank.subtract: copying followed by truncating natural-number subtraction.

Main results

• Bank.exec_multiply: a product smaller than six physical words updates a bank entry in exactly 2484 instructions.
• Bank.exec_subtract: general natural-number subtraction updates a fresh bank entry in at most 151 instructions.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms.

def Cslib.WordRAM.Multiword.Bank.productLow (n : ℕ) : List (Fin (capacity n + 4))

Low eighteen product digits, in physical registers eight through twenty-five.

def Cslib.WordRAM.Multiword.Bank.productHigh (n : ℕ) : List (Fin (capacity n + 4))

High eighteen product digits, in physical registers twenty-six through forty-three.

theorem Cslib.WordRAM.Multiword.Bank.length_productLow (n : ℕ) : (productLow n).length = 18

theorem Cslib.WordRAM.Multiword.Bank.length_productHigh (n : ℕ) : (productHigh n).length = 18

def Cslib.WordRAM.Multiword.Bank.multiply {n : ℕ} (a b d : Fin n) : Code Basis.standard (capacity n + 4)

Compute the full scratch product, then copy its low eighteen digits to a bank entry. The destination may coincide with either source.

theorem Cslib.WordRAM.Multiword.Bank.size_multiply {n : ℕ} (a b d : Fin n) : (multiply a b d).size = 2484

theorem Cslib.WordRAM.Multiword.Bank.size_multiply_le {n : ℕ} (a b d : Fin n) : (multiply a b d).size ≤ 4000

Uniform static code-size bound for multiplication.

theorem Cslib.WordRAM.Multiword.Bank.exec_multiply {n w : ℕ} (hw : 2 ≤ w) (a b d : Fin n) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) (hprod : v a * v b < 2 ^ (6 * w)) : ∃ (y : Data (capacity n + 4)), Exec w (multiply a b d) x y 2484 ∧ Encodes w y (Function.update v d (v a * v b)) ∧ y.mem = x.mem

A six-word-bounded exact product can be placed in any bank entry, including a source entry. The full scratch execution precedes the copy, and all other bank registers survive.

def Cslib.WordRAM.Multiword.Bank.subtract {n : ℕ} (w : ℕ) (a b d : Fin n) : Code Basis.standard (capacity n + 4)

Copy the minuend to a fresh destination, then subtract with underflow cleared to zero.

theorem Cslib.WordRAM.Multiword.Bank.size_subtract {n : ℕ} (w : ℕ) (a b d : Fin n) : (subtract w a b d).size = 153

theorem Cslib.WordRAM.Multiword.Bank.size_subtract_le {n : ℕ} (w : ℕ) (a b d : Fin n) : (subtract w a b d).size ≤ 4000

Uniform static code-size bound for subtraction.

theorem Cslib.WordRAM.Multiword.Bank.exec_subtract {n w : ℕ} (hw : 2 ≤ w) (a b d : Fin n) (hda : d ≠ a) (hdb : d ≠ b) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) : ∃ (y : Data (capacity n + 4)), ExecWithin w (subtract w a b d) x y 151 ∧ Encodes w y (Function.update v d (v a - v b)) ∧ y.mem = x.mem

General subtraction needs no sign hypothesis. Its destination is distinct from the two sources; those sources may coincide. Every other bank entry and all memory are preserved.