Schoolbook multiplication on the checked word RAM

The code is unrolled for fixed operand lengths. Each row adds one shifted digit product to the accumulator and appends its final carry. Leading zero updates make the active accumulator and shifted operand have the same length.

Main definitions

• Cslib.WordRAM.Multiword.Schoolbook.cell, Cslib.WordRAM.Multiword.Schoolbook.row: one multiply-add cell and one complete multiply-add row.
• Cslib.WordRAM.Multiword.Schoolbook.rows, Cslib.WordRAM.Multiword.Schoolbook.rowCost, Cslib.WordRAM.Multiword.Schoolbook.clear, Cslib.WordRAM.Multiword.Schoolbook.program: the unrolled schoolbook rows, their instruction cost, accumulator clearing, and full multiplication routine.
• Cslib.WordRAM.Multiword.Schoolbook.registers, Cslib.WordRAM.Multiword.Schoolbook.leftRegs, Cslib.WordRAM.Multiword.Schoolbook.rightRegs, Cslib.WordRAM.Multiword.Schoolbook.outputRegs, Cslib.WordRAM.Multiword.Schoolbook.lowRegs, Cslib.WordRAM.Multiword.Schoolbook.highRegs, Cslib.WordRAM.Multiword.Schoolbook.fixedProgram, Cslib.WordRAM.Multiword.Schoolbook.input: a concrete register allocation and input encoding for arbitrary fixed operand lengths.

Main results

• Cslib.WordRAM.Multiword.Schoolbook.exec_fixedProgram: exact multiplication, bounded digits, preservation of operands and memory, and an exact width-independent instruction count.
• Cslib.WordRAM.Multiword.Schoolbook.exec_eighteen: 18-digit operands, 36 result digits, 76 registers, and 2465 instructions for every physical word width at least two.

Inputs and outputs use little-endian half-word digits. Conversion from other representations is not part of the routine. Odd widths use the same floor-half radix. Widths zero and one are excluded: their floor-half radix is one and cannot represent a nonzero integer.

References

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

def Cslib.WordRAM.Multiword.Schoolbook.cell {r : ℕ} (a b d : Fin (r + 4)) : Code Basis.standard (r + 4)

The in-place form of LimbUpdate.program: five ordinary instructions for one multiply-add, overwriting the destination digit after reading it.

def Cslib.WordRAM.Multiword.Schoolbook.row {r : ℕ} (a : Fin (r + 4)) : List (Fin (r + 4)) → List (Fin (r + 4)) → Code Basis.standard (r + 4)

Update a full row. The final self-copy gives the empty row a one-instruction execution.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_row {r : ℕ} (a : Fin (r + 4)) (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) : (row a bs ds).size = 5 * ds.length + 1

A row has one five-instruction cell per digit and one final self-copy.

def Cslib.WordRAM.Multiword.Schoolbook.rows {r : ℕ} : List (Fin (r + 4)) → List (Fin (r + 4)) → List (Fin (r + 4)) → List (Fin (r + 4)) → Code Basis.standard (r + 4)

Unrolled schoolbook rows. ds is the current accumulator and os supplies one fresh high digit per remaining multiplicand digit. The multiplier gains a leading zero each row.

def Cslib.WordRAM.Multiword.Schoolbook.rowCost : ℕ → ℕ → ℕ

Exact instruction count of the unrolled rows, including empty-row self-copies.

theorem Cslib.WordRAM.Multiword.Schoolbook.rowCost_eq (m n : ℕ) : rowCost m n = 5 * (m * n + m * (m - 1) / 2) + 3 * m + 1

The extra cells are the leading-zero updates in successive shifted rows.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_rows {r : ℕ} (as bs ds os : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hos : os.length = as.length) : (rows as bs ds os).size = rowCost as.length bs.length

The instruction count of rows equals rowCost on the operand lengths.

theorem Cslib.WordRAM.Multiword.Schoolbook.rowCost_le (m n : ℕ) : rowCost m n ≤ 5 * m * (n + m) + 3 * m + 1

The runtime is constant for fixed operand lengths, independently of the physical width.

def Cslib.WordRAM.Multiword.Schoolbook.clear {r : ℕ} : List (Fin (r + 4)) → Code Basis.standard (r + 4)

Clear the initial accumulator; the empty clear uses one carry self-copy.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_clear {r : ℕ} (ds : List (Fin (r + 4))) : (clear ds).size = ds.length + 1

Clearing ds takes one constant instruction per digit plus one final self-copy.

def Cslib.WordRAM.Multiword.Schoolbook.program {r : ℕ} (as bs ds os : List (Fin (r + 4))) : Code Basis.standard (r + 4)

Complete multiplication: initialize the radix and zero, clear the initial accumulator, and execute all rows. Operand and output register lists are fixed at code construction time.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_program {r : ℕ} (as bs ds os : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hos : os.length = as.length) : (program as bs ds os).size = 7 + bs.length + rowCost as.length bs.length

Exact code size, which is also the exact execution time on valid inputs.

theorem Cslib.WordRAM.Multiword.Schoolbook.exec {r w : ℕ} (hw : 2 ≤ w) (as bs ds os : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hos : os.length = as.length) (hin : ∀ i ∈ as ++ bs, Workspace.IsDigit i) (hout : ∀ i ∈ ds ++ os, Workspace.IsDigit i) (hnd : (ds ++ os).Nodup) (hdis : (ds ++ os).Disjoint (as ++ bs)) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hb : Bounded (radix w) x bs) : ∃ (y : Data (r + 4)), Exec w (program as bs ds os) x y (7 + bs.length + rowCost as.length bs.length) ∧ Bounded (radix w) y (ds ++ os) ∧ value (radix w) y (ds ++ os) = value (radix w) x as * value (radix w) x bs ∧ y.mem = x.mem ∧ ∀ i ∈ as ++ bs, y.regs i = x.regs i

Multiplication of two arbitrary fixed-length little-endian digit lists. All outputs start arbitrary: initialization is part of the charged code. Every arithmetic operation uses the original physical width and checked overflow. The complete product occupies ds ++ os. The layout assumptions express only nonaliasing and reserved-register separation.

def Cslib.WordRAM.Multiword.Schoolbook.registers {r : ℕ} (start len : ℕ) (h : start + len ≤ r) : List (Fin (r + 4))

A contiguous list of digit registers, after the four reserved workspace registers.

def Cslib.WordRAM.Multiword.Schoolbook.leftRegs (m n : ℕ) : List (Fin (2 * (m + n) + 4))

The first operand occupies the first m digit registers.

def Cslib.WordRAM.Multiword.Schoolbook.rightRegs (m n : ℕ) : List (Fin (2 * (m + n) + 4))

The second operand follows the first.

def Cslib.WordRAM.Multiword.Schoolbook.outputRegs (m n : ℕ) : List (Fin (2 * (m + n) + 4))

The m + n result digits follow both operands.

def Cslib.WordRAM.Multiword.Schoolbook.lowRegs (m n : ℕ) : List (Fin (2 * (m + n) + 4))

Initial zero accumulator, with the second operand's length.

def Cslib.WordRAM.Multiword.Schoolbook.highRegs (m n : ℕ) : List (Fin (2 * (m + n) + 4))

One fresh high digit for each schoolbook row.

def Cslib.WordRAM.Multiword.Schoolbook.fixedProgram (m n : ℕ) : Code Basis.standard (2 * (m + n) + 4)

A concrete schoolbook program with 2 * (m + n) + 4 registers and no address words. The code and register count depend only on the limb counts, not on the physical word width.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_fixedProgram (m n : ℕ) : (fixedProgram m n).size = 7 + n + rowCost m n

Exact code size of the fixed-register schoolbook multiplication program.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_fixedProgram_eq (m n : ℕ) : (fixedProgram m n).size = 5 * (m * n + m * (m - 1) / 2) + 3 * m + n + 8

Closed form of the exact instruction count, including setup and initialization.

theorem Cslib.WordRAM.Multiword.Schoolbook.size_fixedProgram_le {m n : ℕ} (hm : m ≤ 18) (hn : n ≤ 18) : (fixedProgram m n).size ≤ 2465

The same constant bounds every choice of operand lengths up to eighteen digits.

theorem Cslib.WordRAM.Multiword.Schoolbook.exec_fixedProgram {w : ℕ} (hw : 2 ≤ w) (m n : ℕ) (x : Data (2 * (m + n) + 4)) (ha : Bounded (radix w) x (leftRegs m n)) (hb : Bounded (radix w) x (rightRegs m n)) : ∃ (y : Data (2 * (m + n) + 4)), Exec w (fixedProgram m n) x y (7 + n + rowCost m n) ∧ Bounded (radix w) y (outputRegs m n) ∧ value (radix w) y (outputRegs m n) = value (radix w) x (leftRegs m n) * value (radix w) x (rightRegs m n) ∧ y.mem = x.mem ∧ ∀ i ∈ leftRegs m n ++ rightRegs m n, y.regs i = x.regs i

The concrete fixed-register schoolbook program multiplies all bounded operands, including zero-length operands, at every physical width at least two. The output has m + n bounded digits, reconstructs the exact product, and preserves memory and both operands.

theorem Cslib.WordRAM.Multiword.Schoolbook.exec_eighteen {w : ℕ} (hw : 2 ≤ w) (x : Data 76) (ha : Bounded (radix w) x (leftRegs 18 18)) (hb : Bounded (radix w) x (rightRegs 18 18)) : ∃ (y : Data (2 * (18 + 18) + 4)), Exec w (fixedProgram 18 18) x y 2465 ∧ Bounded (radix w) y (outputRegs 18 18) ∧ value (radix w) y (outputRegs 18 18) = value (radix w) x (leftRegs 18 18) * value (radix w) x (rightRegs 18 18) ∧ y.mem = x.mem ∧ ∀ i ∈ leftRegs 18 18 ++ rightRegs 18 18, y.regs i = x.regs i

Eighteen digits per operand give a fixed 76-register, 2465-instruction program. This accommodates six physical words per operand even at odd widths, including width three.

def Cslib.WordRAM.Multiword.Schoolbook.input (m n : ℕ) (a : Fin m → ℕ) (b : Fin n → ℕ) : Data (2 * (m + n) + 4)

Encode two fixed digit tuples into the concrete layout, with zero workspace and memory. This is an input encoding, not a RAM conversion routine.

theorem Cslib.WordRAM.Multiword.Schoolbook.six_word_product {w a b : ℕ} (hw : 2 ≤ w) (ha : a < 2 ^ (6 * w)) (hb : b < 2 ^ (6 * w)) : ∃ (x : Data 76) (y : Data 76), Data.Bounded w x ∧ Data.Bounded w y ∧ Exec w (fixedProgram 18 18) x y 2465 ∧ value (radix w) x (leftRegs 18 18) = a ∧ value (radix w) x (rightRegs 18 18) = b ∧ Bounded (radix w) y (outputRegs 18 18) ∧ value (radix w) y (outputRegs 18 18) = a * b

Any two values smaller than six physical words have a globally bounded digit encoding on which the concrete checked program computes their full product in 2465 instructions. The encoding is specified separately; the runtime starts with the encoded operands.