Limb arrays: representation and field access

A LimbArray stores a natural number as a little-endian array of 32-bit limbs: limb i carries weight 2^(32 i), and reading beyond the stored limbs yields zero, so an array denotes the same number after zero limbs are appended. The value of an array is toNat; Core.Proof relates the accessors to this value, and the arithmetic and shift modules provide their own value theorems.

Using UInt32 limbs lets each limb product, plus an accumulator limb and a carry, fit in a UInt64: (2^32 - 1)^2 + 2 * (2^32 - 1) = 2^64 - 1. Array updates can also reuse storage when the array is uniquely referenced.

This module defines the representation and the non-arithmetic accessors: reading bits and 32-bit windows, masking to a bit count, resizing, comparing, and locating the leading set bit. Each loop is structural recursion over a limb count so its invariant can be stated by induction. The arithmetic kernels live in Arithmetic.Runtime and the shifts in Shift.Runtime.

structure FloatLib.Numerics.LimbArray : Type

A natural number stored as little-endian 32-bit limbs.

• limbs : Array UInt32

  Little-endian limbs; limb i has weight 2^(32 i).

def FloatLib.Numerics.instDecidableEqLimbArray.decEq (x✝ x✝¹ : LimbArray) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqLimbArray : DecidableEq LimbArray

@[instance_reducible]

instance FloatLib.Numerics.instReprLimbArray : Repr LimbArray

def FloatLib.Numerics.instReprLimbArray.repr : LimbArray → Nat → Std.Format

@[reducible, inline]

abbrev FloatLib.Numerics.LimbArray.radix : Nat

The limb radix 2^32.

@[inline]

def FloatLib.Numerics.LimbArray.size (v : LimbArray) : Nat

Number of stored limbs.

@[inline]

def FloatLib.Numerics.LimbArray.limb (v : LimbArray) (i : Nat) : UInt32

Limb i, or zero beyond the stored limbs.

def FloatLib.Numerics.LimbArray.segment (v : LimbArray) (start : Nat) : Nat → Nat

Value of the count limbs starting at index start, in units of 2^(32 start).

The recursion places the first limb below the remaining segment, which gives the arithmetic loops a common induction invariant.

def FloatLib.Numerics.LimbArray.toNat (v : LimbArray) : Nat

The natural number denoted by a limb array.

def FloatLib.Numerics.LimbArray.hornerFrom (v : LimbArray) : Nat → Nat → Nat

Horner evaluation from the most significant of count limbs down to limb zero.

def FloatLib.Numerics.LimbArray.toNatImpl (v : LimbArray) : Nat

Executable evaluation of toNat.

Core.Proof.toNat_eq_toNatImpl registers this tail-recursive Horner loop as the compiled form of toNat, whose front recursion is convenient for proofs but not tail recursive.

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

Append the count low base-2^32 digits of n to an accumulator array.

def FloatLib.Numerics.LimbArray.ofNat (n count : Nat) : LimbArray

The count-limb array holding n modulo 2^(32 count).

def FloatLib.Numerics.LimbArray.zero (count : Nat) : LimbArray

The count-limb array holding zero.

def FloatLib.Numerics.LimbArray.topLimb (v : LimbArray) : Nat → Nat

One more than the index of the highest nonzero limb below count, or zero if there is none.

@[inline]

def FloatLib.Numerics.LimbArray.isZero (v : LimbArray) : Bool

Whether the array denotes zero.

def FloatLib.Numerics.LimbArray.log2 (v : LimbArray) : Nat

Position of the leading set bit; zero for the zero array.

@[inline]

def FloatLib.Numerics.LimbArray.testBit (v : LimbArray) (k : Nat) : Bool

Bit k of the denoted number.

@[inline]

def FloatLib.Numerics.LimbArray.bitsAt32 (v : LimbArray) (lo : Nat) : UInt32

The 32-bit window of the denoted number starting at bit lo.

@[inline]

def FloatLib.Numerics.LimbArray.lowMask32 (r : Nat) : UInt32

The mask of the low r bits of a limb, for r < 32.

def FloatLib.Numerics.LimbArray.lowBits (v : LimbArray) (k : Nat) : LimbArray

The denoted number modulo 2^k, keeping the stored limb count.

def FloatLib.Numerics.LimbArray.resize (v : LimbArray) (count : Nat) : LimbArray

The denoted number modulo 2^(32 count), stored in exactly count limbs.

def FloatLib.Numerics.LimbArray.anyLimbBelow (v : LimbArray) : Nat → Bool

Whether any of the limbs below index count is nonzero.

@[inline]

def FloatLib.Numerics.LimbArray.anyBelow (v : LimbArray) (k : Nat) : Bool

Whether any bit below position k is set.

@[inline]

def FloatLib.Numerics.LimbArray.orLowBit (v : LimbArray) (sticky : Bool) : LimbArray

Set the low bit when sticky holds; an empty array remains empty.

def FloatLib.Numerics.LimbArray.compareFrom (a b : LimbArray) : Nat → Ordering

Compare the limbs below index count, most significant first.

@[inline]

def FloatLib.Numerics.LimbArray.compare (a b : LimbArray) : Ordering

Compare the denoted numbers.