Limb arrays: value semantics of the arithmetic kernels

Every loop of Arithmetic.Runtime is specified by a segment invariant: processing the limbs from index onward changes the segment starting at index by the intended amount and leaves the limbs below index untouched. The invariants are proved by induction on the loop's remaining count, and the toNat statements follow by splitting toNat into the segment below index, the segment the loop wrote, and the untouched segment above it.

• toNat_addWordAt and toNat_addAt: adding a word at a limb or bit position, provided the result still fits the stored limbs;
• toNat_add: add a b carry denotes toNat a + toNat b + carry, with no side condition because the result has one limb more than the wider operand;
• toNat_sub: sub a b borrow denotes toNat a - toNat b - borrow whenever that difference is nonnegative and the borrow is at most one;
• toNat_mul: mul a b denotes toNat a * toNat b.

limb_setIfInBounds describes array updates; uint64_low_toNat and uint64_high_toNat split each intermediate into a result limb and a carry.

Array updates and machine-word digits

theorem FloatLib.Numerics.LimbArray.limb_setIfInBounds (arr : Array UInt32) (i : ℕ) (x : UInt32) (j : ℕ) : { limbs := arr.setIfInBounds i x }.limb j = if i = j ∧ i < arr.size then x else { limbs := arr }.limb j

The limb view of an in-bounds array update.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_setIfInBounds' (arr : Array UInt32) (i : ℕ) (x : UInt32) : { limbs := arr.setIfInBounds i x }.size = { limbs := arr }.size

Writing one limb in bounds keeps the limb count.

theorem FloatLib.Numerics.LimbArray.segment_setIfInBounds_of_le (arr : Array UInt32) (i : ℕ) (x : UInt32) (s n : ℕ) (h : s + n ≤ i ∨ i < s) : { limbs := arr.setIfInBounds i x }.segment s n = { limbs := arr }.segment s n

Segments away from an updated limb are unchanged.

theorem FloatLib.Numerics.LimbArray.uint64_low_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % radix

The low word of a UInt64 is its value modulo the radix.

theorem FloatLib.Numerics.LimbArray.uint64_high_toNat (x : UInt64) : (x >>> 32).toUInt32.toNat = x.toNat / radix

The high word of a UInt64 is its value divided by the radix.

theorem FloatLib.Numerics.LimbArray.uint32_toNat_lt (x : UInt32) : x.toNat < radix

Every limb value is below the radix 2^32.

theorem FloatLib.Numerics.LimbArray.toNat_split (v : LimbArray) (i c : ℕ) (h : i + c ≤ v.size) : v.toNat = v.segment 0 i + radix ^ i * v.segment i c + radix ^ (i + c) * v.segment (i + c) (v.size - (i + c))

The three-way split of a value around a written segment.

Carry propagation

theorem FloatLib.Numerics.LimbArray.size_carryLoop (count index : ℕ) (carry : UInt32) (out : Array UInt32) : (carryLoop count index carry out).size = out.size

The carry loop writes into the output array without resizing it.

theorem FloatLib.Numerics.LimbArray.carryLoop_spec (count index : ℕ) (carry : UInt32) (out : Array UInt32) (hsize : index + count ≤ out.size) (hfit : { limbs := out }.segment index count + carry.toNat < radix ^ count) : { limbs := carryLoop count index carry out }.segment index count = { limbs := out }.segment index count + carry.toNat ∧ ∀ (i : ℕ), i < index ∨ index + count ≤ i → { limbs := carryLoop count index carry out }.limb i = { limbs := out }.limb i

The carry loop adds its carry to the segment it processes and leaves the other limbs unchanged, provided the sum fits the processed limbs.

theorem FloatLib.Numerics.LimbArray.toNat_addWordAt (v : LimbArray) (index : ℕ) (w : UInt32) (hindex : index ≤ v.size) (hfit : v.toNat + w.toNat * radix ^ index < radix ^ v.size) : (v.addWordAt index w).toNat = v.toNat + w.toNat * radix ^ index

Adding a word at a limb position, when the sum fits the stored limbs.

theorem FloatLib.Numerics.LimbArray.size_addWordAt (v : LimbArray) (index : ℕ) (w : UInt32) : (v.addWordAt index w).size = v.size

Adding a word at an index keeps the limb count.

theorem FloatLib.Numerics.LimbArray.shifted_word_toNat (w : UInt32) (r : ℕ) (hr : r < 32) : (w.toUInt64 <<< UInt64.ofNat r).toNat = w.toNat * 2 ^ r

The 64-bit shifted word splits into a low and a high limb.

theorem FloatLib.Numerics.LimbArray.toNat_addAt (v : LimbArray) (k : ℕ) (w : UInt32) (hk : k / 32 + 1 ≤ v.size) (hfit : v.toNat + w.toNat * 2 ^ k < radix ^ v.size) : (v.addAt k w).toNat = v.toNat + w.toNat * 2 ^ k

Adding w * 2^k, when the sum fits the stored limbs and bit k lies within the array.

theorem FloatLib.Numerics.LimbArray.size_addAt (v : LimbArray) (k : ℕ) (w : UInt32) : (v.addAt k w).size = v.size

Adding a word at a bit offset keeps the limb count.

Addition

theorem FloatLib.Numerics.LimbArray.size_addLoop (a b : LimbArray) (count index : ℕ) (carry : UInt32) (out : Array UInt32) : (a.addLoop b count index carry out).size = out.size

The addition loop keeps the size of its accumulator.

theorem FloatLib.Numerics.LimbArray.addLoop_spec (a b : LimbArray) (count index : ℕ) (carry : UInt32) (out : Array UInt32) (hsize : index + count < out.size) : { limbs := a.addLoop b count index carry out }.segment index (count + 1) = a.segment index count + b.segment index count + carry.toNat ∧ ∀ i < index, { limbs := a.addLoop b count index carry out }.limb i = { limbs := out }.limb i

The addition loop writes the sum of the processed segments and the carry.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_add (a b : LimbArray) (carry : UInt32) : (a.add b carry).size = max a.size b.size + 1

A sum has one limb more than the wider operand, room for the final carry.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_add (a b : LimbArray) (carry : UInt32) : (a.add b carry).toNat = a.toNat + b.toNat + carry.toNat

add denotes the sum of its operands and the incoming carry.

Subtraction

theorem FloatLib.Numerics.LimbArray.size_subLoop (a b : LimbArray) (count index : ℕ) (borrow : UInt32) (out : Array UInt32) : (a.subLoop b count index borrow out).size = out.size

The subtraction loop keeps the size of its accumulator.

theorem FloatLib.Numerics.LimbArray.subLoop_spec (a b : LimbArray) (count index : ℕ) (borrow : UInt32) (out : Array UInt32) (hsize : index + count ≤ out.size) (hborrow : borrow.toNat ≤ 1) (hle : b.segment index count + borrow.toNat ≤ a.segment index count) : { limbs := a.subLoop b count index borrow out }.segment index count + b.segment index count + borrow.toNat = a.segment index count ∧ ∀ i < index, { limbs := a.subLoop b count index borrow out }.limb i = { limbs := out }.limb i

The subtraction loop writes the difference of the processed segments when it is nonnegative.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_sub (a b : LimbArray) (borrow : UInt32) : (a.sub b borrow).size = max a.size b.size

A difference has as many limbs as the wider operand.

theorem FloatLib.Numerics.LimbArray.toNat_sub (a b : LimbArray) (borrow : UInt32) (hborrow : borrow.toNat ≤ 1) (hle : b.toNat + borrow.toNat ≤ a.toNat) : (a.sub b borrow).toNat = a.toNat - b.toNat - borrow.toNat

sub denotes the difference when it is nonnegative and the borrow is at most one.

Multiplication

theorem FloatLib.Numerics.LimbArray.size_mulRow (b : LimbArray) (m : UInt32) (offset count j : ℕ) (carry : UInt32) (out : Array UInt32) : (b.mulRow m offset count j carry out).size = out.size

One schoolbook row keeps the size of its accumulator.

theorem FloatLib.Numerics.LimbArray.mulRow_spec (b : LimbArray) (m : UInt32) (offset count j : ℕ) (carry : UInt32) (out : Array UInt32) (hsize : offset + j + count < out.size) (hslot : { limbs := out }.limb (offset + j + count) = 0) : { limbs := b.mulRow m offset count j carry out }.segment (offset + j) (count + 1) = { limbs := out }.segment (offset + j) count + m.toNat * b.segment j count + carry.toNat ∧ ∀ (i : ℕ), i < offset + j ∨ offset + j + count < i → { limbs := b.mulRow m offset count j carry out }.limb i = { limbs := out }.limb i

A row of the schoolbook product adds m times a segment of b at its offset.

theorem FloatLib.Numerics.LimbArray.size_mulRows (a b : LimbArray) (count i : ℕ) (out : Array UInt32) : (a.mulRows b count i out).size = out.size

The schoolbook row loop writes into the output array without resizing it.

theorem FloatLib.Numerics.LimbArray.mulRows_spec (a b : LimbArray) (count i : ℕ) (out : Array UInt32) (hsize : out.size = a.size + b.size) (hrows : i + count = a.size) (hvalue : { limbs := out }.toNat = a.segment 0 i * b.toNat) (hzero : ∀ (k : ℕ), i + b.size ≤ k → { limbs := out }.limb k = 0) : { limbs := a.mulRows b count i out }.toNat = a.segment 0 (i + count) * b.toNat

The row loop maintains the partial product and the zero limbs above it.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_mul (a b : LimbArray) : (a.mul b).size = a.size + b.size

A product has as many limbs as the two operands together.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_mul (a b : LimbArray) : (a.mul b).toNat = a.toNat * b.toNat

mul denotes the product of its operands.