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, where 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

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

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.Internal.toNat (v : LimbArray) : Nat

Executable evaluation of toNat.

Core.Proof.toNat_eq_internal 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, or 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

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, scanning only stored limbs.

@[inline]

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

Set the low bit when sticky holds. An empty array stays 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.