Limb arrays: addition, subtraction, and multiplication

The carry-propagating loops of multiple-precision integer arithmetic over LimbArray. Each loop recurses on the number of limbs still to process and writes its result with Array.setIfInBounds. The 32-bit limbs leave room for the addition and multiplication intermediates in UInt64.

• carryLoop adds one word at a limb position and propagates the carry upward. It is the primitive behind addWordAt, addAt, and the increment used by rounding.
• add and sub are the schoolbook sum and difference with an incoming carry or borrow; sub assumes its result is nonnegative and the incoming borrow is at most one.
• mul is the schoolbook product; each row adds one limb of the left operand times the right operand at the row's offset.

Arithmetic.Proof states each kernel's effect on toNat, including the required capacity, borrow, and accumulator invariants.

Carry propagation

def FloatLib.Numerics.LimbArray.carryLoop : Nat → Nat → UInt32 → Array UInt32 → Array UInt32

Add carry at limb index and propagate upward through count limbs.

The loop stops as soon as the carry vanishes, so the common case touches one limb.

@[inline]

def FloatLib.Numerics.LimbArray.addWordAt (v : LimbArray) (index : Nat) (w : UInt32) : LimbArray

Add the word w at limb index, discarding any carry beyond the stored array.

def FloatLib.Numerics.LimbArray.addAt (v : LimbArray) (k : Nat) (w : UInt32) : LimbArray

Add w * 2^k to the array.

The word is split at the limb boundary containing bit k; both halves are added with carry propagation. The result is meaningful when the sum still fits the stored limbs.

Addition and subtraction

def FloatLib.Numerics.LimbArray.addLoop (a b : LimbArray) : Nat → Nat → UInt32 → Array UInt32 → Array UInt32

Add limbs index, index + 1, ... of two arrays into out, then store the final carry.

def FloatLib.Numerics.LimbArray.add (a b : LimbArray) (carry : UInt32 := 0) : LimbArray

The sum of two arrays and an incoming carry, in one limb more than the wider operand.

def FloatLib.Numerics.LimbArray.subLoop (a b : LimbArray) : Nat → Nat → UInt32 → Array UInt32 → Array UInt32

Subtract limbs index, index + 1, ... of b and a borrow from those of a into out.

def FloatLib.Numerics.LimbArray.sub (a b : LimbArray) (borrow : UInt32 := 0) : LimbArray

The difference a - b - borrow, in as many limbs as the wider operand.

The result is exact when borrow ≤ 1 and b + borrow ≤ a; Arithmetic.Proof.toNat_sub states that contract.

Multiplication

def FloatLib.Numerics.LimbArray.mulRow (b : LimbArray) (m : UInt32) (offset : Nat) : Nat → Nat → UInt32 → Array UInt32 → Array UInt32

Add m times count limbs of b, starting at limb j, into out at offset offset + j. Store the final carry at offset + j + count; that slot must initially be zero.

Every intermediate m * b_j + out_(offset + j) + carry is below 2^64.

def FloatLib.Numerics.LimbArray.mulRows (a b : LimbArray) : Nat → Nat → Array UInt32 → Array UInt32

Accumulate count rows, starting with row i, each contributing a_i * b * 2^(32 i).

def FloatLib.Numerics.LimbArray.mul (a b : LimbArray) : LimbArray

The schoolbook product, in a.size + b.size limbs.