Multiword arithmetic on the checked word RAM

An elementary schoolbook multiplication update uses half-word digits. For radix β = 2 ^ (w / 2), four digits a, b, d, c < β satisfy a * b + d + c < β ^ 2 ≤ 2 ^ w. Thus the product and both partial sums fit the physical word, and division and remainder recover an exact digit and carry.

Main definitions

• Cslib.WordRAM.Multiword.radix: the half-word radix.
• Cslib.WordRAM.Multiword.LimbUpdate.program: five standard RAM instructions implementing one schoolbook multiply-add update.
• Cslib.WordRAM.Multiword.LimbUpdate.initializedProgram: compute the half-word radix and perform the update in ten instructions, with no preloaded radix.

Main results

• Cslib.WordRAM.Multiword.LimbUpdate.exec: checked execution, exact reconstruction, and bounded output digit and carry in five instructions, independently of the word size.

This module supplies the elementary update. WordRAM.Multiword.Mul assembles the full schoolbook routine for arbitrary fixed operand lengths.

References

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

def Cslib.WordRAM.Multiword.radix (w : ℕ) : ℕ

Radix for digits whose multiply-add updates fit a single physical word.

theorem Cslib.WordRAM.Multiword.radix_eq_one_of_lt_two {w : ℕ} (hw : w < 2) : radix w = 1

Widths below two have a degenerate floor-half radix, so nonzero inputs require a different representation and routine. The schoolbook routines explicitly assume 2 ≤ w.

theorem Cslib.WordRAM.Multiword.one_lt_radix {w : ℕ} (hw : 2 ≤ w) : 1 < radix w

theorem Cslib.WordRAM.Multiword.radix_sq_le (w : ℕ) : radix w ^ 2 ≤ 2 ^ w

theorem Cslib.WordRAM.Multiword.radix_fits {w : ℕ} (hw : 2 ≤ w) : Fits w (radix w)

theorem Cslib.WordRAM.Multiword.exists_six_word_digits {w v : ℕ} (hw : 2 ≤ w) (hv : v < 2 ^ (6 * w)) : ∃ (x : Fin 18 → ℕ), (∀ (i : Fin 18), x i < radix w) ∧ Nat.ofDigits (radix w) (List.ofFn x) = v

Eighteen half-word digits suffice for a value occupying at most six physical words, including odd word sizes. This is a representation bound, not a multiplication algorithm.

theorem Cslib.WordRAM.Multiword.limb_update_lt_sq {β a b d c : ℕ} (ha : a < β) (hb : b < β) (hd : d < β) (hc : c < β) : a * b + d + c < β ^ 2

The sharp bound for a schoolbook multiply-add: the maximum is β ^ 2 - 1.

theorem Cslib.WordRAM.Multiword.limb_update_fits {w a b d c : ℕ} (ha : a < radix w) (hb : b < radix w) (hd : d < radix w) (hc : c < radix w) : Fits w (a * b + d + c)

Every intermediate arithmetic result of the update fits the physical word.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.left : Fin 7

First multiplicand digit (preserved).

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.right : Fin 7

Second multiplicand digit (preserved).

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.addend : Fin 7

Previous destination digit (preserved).

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.carry : Fin 7

Input carry, replaced by the output carry.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.base : Fin 7

Radix (preserved).

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.total : Fin 7

Product and partial-sum workspace.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.LimbUpdate.digit : Fin 7

Output digit.

def Cslib.WordRAM.Multiword.LimbUpdate.program : Code Basis.standard 7

One schoolbook update, using only checked single-word arithmetic.

theorem Cslib.WordRAM.Multiword.LimbUpdate.size_program : program.size = 5

def Cslib.WordRAM.Multiword.LimbUpdate.setup : Code Basis.standard 7

Compute the radix from the physical word size, using only the two output registers as workspace. The four input digits are preserved.

def Cslib.WordRAM.Multiword.LimbUpdate.setupResult (w : ℕ) (x : Data 7) : Data 7

The result of radix setup.

theorem Cslib.WordRAM.Multiword.LimbUpdate.exec_setup {w : ℕ} (x : Data 7) (hw : 2 ≤ w) : Exec w setup x (setupResult w x) 5

Radix setup costs five instructions for every physical word size at least two.

def Cslib.WordRAM.Multiword.LimbUpdate.initializedProgram : Code Basis.standard 7

Fixed code computing the radix and then executing a schoolbook update.

theorem Cslib.WordRAM.Multiword.LimbUpdate.size_initializedProgram : initializedProgram.size = 10

def Cslib.WordRAM.Multiword.LimbUpdate.result (x : Data 7) : Data 7

The mathematical result of the five instructions, including the workspace.

theorem Cslib.WordRAM.Multiword.LimbUpdate.exec_exact {w : ℕ} (x : Data 7) (ha : x.regs left < radix w) (hb : x.regs right < radix w) (hd : x.regs addend < radix w) (hc : x.regs carry < radix w) : Exec w program x (result x) 5

Checked execution of the elementary update. All three intermediate results are justified from the digit bounds; no high-product primitive or enlarged physical word is assumed.

theorem Cslib.WordRAM.Multiword.LimbUpdate.exec {w : ℕ} (x : Data 7) (hw : 2 ≤ w) (hbase : x.regs base = radix w) (ha : x.regs left < radix w) (hb : x.regs right < radix w) (hd : x.regs addend < radix w) (hc : x.regs carry < radix w) : ∃ (y : Data 7), ExecWithin w program x y 5 ∧ y.regs digit < radix w ∧ y.regs carry < radix w ∧ x.regs left * x.regs right + x.regs addend + x.regs carry = y.regs digit + radix w * y.regs carry ∧ y.mem = x.mem ∧ y.regs left = x.regs left ∧ y.regs right = x.regs right ∧ y.regs addend = x.regs addend ∧ y.regs base = x.regs base

In five instructions the elementary update returns an exact low digit and carry, both strictly below the radix. Memory and the two operands, addend, and radix are preserved. For globally bounded input data, ExecWithin.bounded also gives globally bounded output data.

theorem Cslib.WordRAM.Multiword.LimbUpdate.exec_initialized {w : ℕ} (x : Data 7) (hw : 2 ≤ w) (ha : x.regs left < radix w) (hb : x.regs right < radix w) (hd : x.regs addend < radix w) (hc : x.regs carry < radix w) : ∃ (y : Data 7), ExecWithin w initializedProgram x y 10 ∧ y.regs digit < radix w ∧ y.regs carry < radix w ∧ x.regs left * x.regs right + x.regs addend + x.regs carry = y.regs digit + radix w * y.regs carry ∧ y.mem = x.mem ∧ y.regs left = x.regs left ∧ y.regs right = x.regs right ∧ y.regs addend = x.regs addend ∧ y.regs base = radix w

The update with charged radix setup, in ten instructions at any word size at least two. The initial radix and workspace registers may contain arbitrary words.