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.row: one complete multiply-add row.Cslib.WordRAM.Multiword.Schoolbook.rows: the schoolbook multiplication routine.Cslib.WordRAM.Multiword.Schoolbook.fixedProgram: a concrete register allocation for arbitrary fixed operand lengths, including radix setup and accumulator clearing.
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 #
The in-place form of LimbUpdate.program: five ordinary instructions for one multiply-add,
overwriting the destination digit after reading it.
Instances For
Execute an entire row, with exact reconstruction including its final carry.
I is any set of preserved input registers, disjoint from the destination registers.
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.
Instances For
Exact instruction count of the unrolled rows, including empty-row self-copies.
Instances For
Complete schoolbook multiplication with an arbitrary initial accumulator. The theorem constructs an execution and proves its product equation; no multiplication specification is assumed. The accumulator grows by one carry digit per row.
Clear the initial accumulator; the empty clear uses one carry self-copy.
Instances For
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.
Instances For
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.
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.
Instances For
The same constant bounds every choice of operand lengths up to eighteen digits.
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.
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.
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.