Limb arrays: value semantics of the accessors

The accessors of Core.Runtime have value-level contracts in terms of the natural number toNat of a limb array. The contracts use three groups of lemmas.

• segment lemmas: segment_eq_ofDigits and toNat_eq_ofDigits identify the denotation with Mathlib's little-endian base-2^32 evaluation. Its append, bound, prefix, and injectivity theorems apply to limb segments, including zero padding beyond the stored size.
• Digit and bit extraction: limb_toNat_eq reads limb i as a base-2^32 digit of toNat, and limb_testBit reads a bit of a limb as a bit of toNat. Together with Nat.eq_of_testBit_eq these turn every bitwise accessor into a statement about Nat bits.
• The accessor theorems: toNat_ofNat, ofNat_toNat, testBit_eq, bitsAt32_toNat, toNat_lowBits, toNat_resize, anyBelow_eq_true_iff, toNat_orLowBit, compare_eq, isZero_eq_true_iff, and log2_eq.

The compiler certificate toNat_eq_toNatImpl replaces the proof-facing toNat by its Horner loop. limb_toNat_eq and limb_testBit connect limb access to value-level proofs.

Limbs and segments

theorem FloatLib.Numerics.LimbArray.limb_eq_zero_of_size_le (v : LimbArray) {i : ℕ} (h : v.size ≤ i) : v.limb i = 0

Limbs beyond the stored size read as zero.

theorem FloatLib.Numerics.LimbArray.limb_eq_getElem (v : LimbArray) {i : ℕ} (h : i < v.limbs.size) : v.limb i = v.limbs[i]

A stored limb is the corresponding array element.

theorem FloatLib.Numerics.LimbArray.limb_toNat_lt (v : LimbArray) (i : ℕ) : (v.limb i).toNat < radix

Every limb is below the radix.

theorem FloatLib.Numerics.LimbArray.radix_eq : radix = 2 ^ 32

The radix is 2^32.

theorem FloatLib.Numerics.LimbArray.radix_pow (n : ℕ) : radix ^ n = 2 ^ (32 * n)

A power of the radix is a power of two.

@[simp]

theorem FloatLib.Numerics.LimbArray.segment_zero (v : LimbArray) (s : ℕ) : v.segment s 0 = 0

An empty segment denotes zero.

theorem FloatLib.Numerics.LimbArray.segment_succ (v : LimbArray) (s n : ℕ) : v.segment s (n + 1) = (v.limb s).toNat + radix * v.segment (s + 1) n

A segment is its first limb plus the radix times the rest, Horner's rule read from the low end.

theorem FloatLib.Numerics.LimbArray.segment_eq_ofDigits (v : LimbArray) (s n : ℕ) : v.segment s n = Nat.ofDigits radix (List.map (fun (i : ℕ) => (v.limb i).toNat) (List.range' s n))

A segment evaluates its zero-padded limb digits in Mathlib's little-endian convention.

theorem FloatLib.Numerics.LimbArray.segment_add (v : LimbArray) (s m n : ℕ) : v.segment s (m + n) = v.segment s m + radix ^ m * v.segment (s + m) n

Splitting a segment.

theorem FloatLib.Numerics.LimbArray.segment_succ_back (v : LimbArray) (s n : ℕ) : v.segment s (n + 1) = v.segment s n + (v.limb (s + n)).toNat * radix ^ n

Adding a limb at the top of a segment.

theorem FloatLib.Numerics.LimbArray.segment_lt (v : LimbArray) (s n : ℕ) : v.segment s n < radix ^ n

A segment of n limbs is below radix ^ n.

theorem FloatLib.Numerics.LimbArray.segment_congr {a b : LimbArray} {s n : ℕ} (h : ∀ i < n, a.limb (s + i) = b.limb (s + i)) : a.segment s n = b.segment s n

Segments depend only on the limbs they cover.

theorem FloatLib.Numerics.LimbArray.segment_eq_zero_of_limb_eq_zero {v : LimbArray} {s n : ℕ} (h : ∀ i < n, v.limb (s + i) = 0) : v.segment s n = 0

A segment of zero limbs is zero.

theorem FloatLib.Numerics.LimbArray.segment_eq_of_limb_eq_zero {v : LimbArray} {s m n : ℕ} (hmn : m ≤ n) (h : ∀ (i : ℕ), m ≤ i → i < n → v.limb (s + i) = 0) : v.segment s n = v.segment s m

Trailing zero limbs do not change a segment.

theorem FloatLib.Numerics.LimbArray.segment_eq_zero_iff {v : LimbArray} {s n : ℕ} : v.segment s n = 0 ↔ ∀ i < n, v.limb (s + i) = 0

A segment is zero exactly when every covered limb is zero.

The value

theorem FloatLib.Numerics.LimbArray.toNat_eq_ofDigits (v : LimbArray) : v.toNat = Nat.ofDigits radix (List.map UInt32.toNat v.limbs.toList)

A limb array's value is the base-2^32 evaluation of its stored digits.

theorem FloatLib.Numerics.LimbArray.toNat_eq_segment_of_size_le {v : LimbArray} {n : ℕ} (h : v.size ≤ n) : v.toNat = v.segment 0 n

toNat may be read from any limb count at or above the stored size.

theorem FloatLib.Numerics.LimbArray.toNat_lt (v : LimbArray) : v.toNat < radix ^ v.size

The value is below radix ^ size.

theorem FloatLib.Numerics.LimbArray.toNat_lt_of_size_le {v : LimbArray} {n : ℕ} (h : v.size ≤ n) : v.toNat < radix ^ n

The value is below radix ^ n for every n at or above the stored size.

theorem FloatLib.Numerics.LimbArray.toNat_lt_two_pow_of_size_le {v : LimbArray} {n : ℕ} (h : v.size ≤ n) : v.toNat < 2 ^ (32 * n)

The value is below 2^(32 n) for every n at or above the stored size.

theorem FloatLib.Numerics.LimbArray.segment_zero_eq_mod (v : LimbArray) (n : ℕ) : v.segment 0 n = v.toNat % radix ^ n

A segment starting at limb zero is a prefix of the value.

theorem FloatLib.Numerics.LimbArray.limb_toNat_eq (v : LimbArray) (i : ℕ) : (v.limb i).toNat = v.toNat / radix ^ i % radix

Limb i is the base-2^32 digit i of the value.

theorem FloatLib.Numerics.LimbArray.limb_testBit (v : LimbArray) (i j : ℕ) (hj : j < 32) : (v.limb i).toNat.testBit j = v.toNat.testBit (32 * i + j)

Bit j of limb i is bit 32 i + j of the value, for j < 32.

theorem FloatLib.Numerics.LimbArray.limb_testBit_eq_false (v : LimbArray) (i j : ℕ) (hj : 32 ≤ j) : (v.limb i).toNat.testBit j = false

A limb has no bits at or above position 32.

theorem FloatLib.Numerics.LimbArray.ext_of_toNat {a b : LimbArray} (hsize : a.size = b.size) (h : a.toNat = b.toNat) : a = b

Limb arrays with equal size and value are equal.

theorem FloatLib.Numerics.LimbArray.limb_eq_of_toNat_eq {a b : LimbArray} (h : a.toNat = b.toNat) (i : ℕ) : a.limb i = b.limb i

Limbs of two arrays with the same value agree.

theorem FloatLib.Numerics.LimbArray.segment_eq_mod_of_digits (v : LimbArray) (n c : ℕ) : (∀ j < c, (v.limb j).toNat = n / radix ^ j % radix) → v.segment 0 c = n % radix ^ c

A value determined digit by digit.

Horner evaluation

theorem FloatLib.Numerics.LimbArray.hornerFrom_eq (v : LimbArray) (n acc : ℕ) : v.hornerFrom n acc = acc * radix ^ n + v.segment 0 n

The compiled Horner loop computes the segment denotation from an accumulator.

theorem FloatLib.Numerics.LimbArray.toNatImpl_eq (v : LimbArray) : v.toNatImpl = v.toNat

The Horner loop computes the value.

@[csimp]

theorem FloatLib.Numerics.LimbArray.toNat_eq_toNatImpl : toNat = toNatImpl

Compile the proof-facing front recursion of toNat as its tail-recursive Horner loop.

Construction from a natural number

theorem FloatLib.Numerics.LimbArray.size_ofNatLoop (count n : ℕ) (acc : Array UInt32) : (ofNatLoop count n acc).size = acc.size + count

The ofNat loop appends exactly count limbs to its accumulator.

theorem FloatLib.Numerics.LimbArray.getElem_ofNatLoop (count n : ℕ) (acc : Array UInt32) (j : ℕ) (hj : j < (ofNatLoop count n acc).size) : (ofNatLoop count n acc)[j] = if h : j < acc.size then acc[j] else UInt32.ofNat (n / radix ^ (j - acc.size))

The ofNat loop keeps the accumulator's prefix and appends the base-2^32 digits of n.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_ofNat (n count : ℕ) : (ofNat n count).size = count

ofNat n count has exactly count limbs.

theorem FloatLib.Numerics.LimbArray.limb_ofNat (n count j : ℕ) (hj : j < count) : (ofNat n count).limb j = UInt32.ofNat (n / radix ^ j)

Limb j of ofNat n count is the j-th base-2^32 digit of n.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_ofNat (n count : ℕ) : (ofNat n count).toNat = n % radix ^ count

The constructed array holds n modulo radix ^ count.

theorem FloatLib.Numerics.LimbArray.toNat_ofNat_of_lt {n count : ℕ} (h : n < radix ^ count) : (ofNat n count).toNat = n

The constructed array holds n when n fits count limbs.

theorem FloatLib.Numerics.LimbArray.ofNat_toNat (v : LimbArray) : ofNat v.toNat v.size = v

Rebuilding an array from its value and size is the identity.

Zero

@[simp]

theorem FloatLib.Numerics.LimbArray.size_zero (count : ℕ) : (zero count).size = count

The zero array has the requested limb count.

theorem FloatLib.Numerics.LimbArray.limb_zero (count i : ℕ) : (zero count).limb i = 0

Every limb of the zero array is zero, also beyond its size.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_zero (count : ℕ) : (zero count).toNat = 0

The zero array denotes zero.

Leading limb, zero test, and logarithm

theorem FloatLib.Numerics.LimbArray.topLimb_eq_zero_iff (v : LimbArray) (n : ℕ) : v.topLimb n = 0 ↔ ∀ i < n, v.limb i = 0

The top-limb search returns zero exactly when every scanned limb is zero.

theorem FloatLib.Numerics.LimbArray.topLimb_le (v : LimbArray) (n : ℕ) : v.topLimb n ≤ n

The top-limb search never returns an index beyond the scanned prefix.

theorem FloatLib.Numerics.LimbArray.topLimb_spec (v : LimbArray) (n i : ℕ) (h : v.topLimb n = i + 1) : v.limb i ≠ 0 ∧ i < n ∧ ∀ (j : ℕ), i < j → j < n → v.limb j = 0

When the search returns i + 1, limb i is the highest nonzero limb of the scanned prefix.

theorem FloatLib.Numerics.LimbArray.isZero_eq_true_iff (v : LimbArray) : v.isZero = true ↔ v.toNat = 0

The zero test decides whether the value is zero.

theorem FloatLib.Numerics.LimbArray.isZero_eq (v : LimbArray) : v.isZero = decide (v.toNat = 0)

The zero test as a decision.

@[simp]

theorem FloatLib.Numerics.LimbArray.uint32_log2_toNat (x : UInt32) : x.log2.toNat = x.toNat.log2

Native UInt32.log2 has the natural-number value of Nat.log2.

theorem FloatLib.Numerics.LimbArray.log2_eq (v : LimbArray) (h : v.toNat ≠ 0) : v.log2 = v.toNat.log2

The leading-bit position of a nonzero array is the natural-number logarithm of its value.

Bit access

theorem FloatLib.Numerics.LimbArray.testBit_eq (v : LimbArray) (k : ℕ) : v.testBit k = v.toNat.testBit k

testBit reads the bit of the value.

theorem FloatLib.Numerics.LimbArray.lowMask32_toNat (r : ℕ) (hr : r < 32) : (lowMask32 r).toNat = 2 ^ r - 1

The mask of the low r bits.

theorem FloatLib.Numerics.LimbArray.testBit_and_lowMask32 (x : UInt32) (r j : ℕ) (hr : r < 32) : (x &&& lowMask32 r).toNat.testBit j = (x.toNat.testBit j && decide (j < r))

A masked limb keeps exactly the bits below r.

@[simp]

theorem FloatLib.Numerics.LimbArray.bitsAt32_toNat (v : LimbArray) (lo : ℕ) : (v.bitsAt32 lo).toNat = v.toNat / 2 ^ lo % radix

The 32-bit window at lo is the value shifted down by lo, modulo the radix.

Masking and resizing

@[simp]

theorem FloatLib.Numerics.LimbArray.size_lowBits (v : LimbArray) (k : ℕ) : (v.lowBits k).size = v.size

Masking to the low bits keeps the limb count.

theorem FloatLib.Numerics.LimbArray.limb_lowBits (v : LimbArray) (k i : ℕ) : (v.lowBits k).limb i = if i < k / 32 then v.limb i else if i = k / 32 then v.limb i &&& lowMask32 (k % 32) else 0

lowBits keeps whole limbs below the cut, masks the limb at the cut, and zeroes the rest.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_lowBits (v : LimbArray) (k : ℕ) : (v.lowBits k).toNat = v.toNat % 2 ^ k

Masking keeps the value modulo 2^k.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_resize (v : LimbArray) (count : ℕ) : (v.resize count).size = count

resize has exactly the requested limb count.

theorem FloatLib.Numerics.LimbArray.limb_resize (v : LimbArray) (count i : ℕ) : (v.resize count).limb i = if i < count then v.limb i else 0

resize keeps the limbs inside the new size and reads zero above it.

@[simp]

theorem FloatLib.Numerics.LimbArray.toNat_resize (v : LimbArray) (count : ℕ) : (v.resize count).toNat = v.toNat % radix ^ count

Resizing keeps the value modulo radix ^ count.

theorem FloatLib.Numerics.LimbArray.toNat_resize_of_size_le (v : LimbArray) {count : ℕ} (h : v.size ≤ count) : (v.resize count).toNat = v.toNat

Resizing to at least the stored size keeps the value.

Sticky bits

theorem FloatLib.Numerics.LimbArray.anyLimbBelow_eq_true_iff (v : LimbArray) (q : ℕ) : v.anyLimbBelow q = true ↔ ∃ i < q, v.limb i ≠ 0

The sticky scan reports true exactly when some limb below the cut is nonzero.

theorem FloatLib.Numerics.LimbArray.anyBelow_eq_true_iff (v : LimbArray) (k : ℕ) : v.anyBelow k = true ↔ v.toNat % 2 ^ k ≠ 0

anyBelow detects a nonzero suffix below bit k.

theorem FloatLib.Numerics.LimbArray.anyBelow_eq (v : LimbArray) (k : ℕ) : v.anyBelow k = decide (v.toNat % 2 ^ k ≠ 0)

anyBelow as a decision.

@[simp]

theorem FloatLib.Numerics.LimbArray.size_orLowBit (v : LimbArray) (sticky : Bool) : (v.orLowBit sticky).size = v.size

Setting the sticky bit keeps the limb count.

theorem FloatLib.Numerics.LimbArray.limb_orLowBit_true (v : LimbArray) (hsize : 0 < v.size) (i : ℕ) : (v.orLowBit true).limb i = if i = 0 then v.limb 0 ||| 1 else v.limb i

Setting the sticky bit ors 1 into limb zero and leaves every other limb unchanged.

theorem FloatLib.Numerics.LimbArray.toNat_orLowBit (v : LimbArray) (hsize : 0 < v.size) (sticky : Bool) : (v.orLowBit sticky).toNat = if sticky = true then v.toNat ||| 1 else v.toNat

Jamming a sticky bit sets bit zero of the value.

Comparison

theorem FloatLib.Numerics.LimbArray.compareFrom_eq (a b : LimbArray) (n : ℕ) : a.compareFrom b n = Ord.compare (a.segment 0 n) (b.segment 0 n)

Lexicographic comparison from the top limb down agrees with comparing the denoted segments.

theorem FloatLib.Numerics.LimbArray.compare_eq (a b : LimbArray) : a.compare b = Ord.compare a.toNat b.toNat

Limb comparison compares the values.