Shared fixed-word runtime primitives

Fixed-format and fixed-limb backends share a native-integer toolbox for bounded arithmetic. It implements nearest-even shifts and quotients, two-word arithmetic, and restoring square-root state without committing to a floating-point format.

The common case stays in UInt64 or UInt128, so a specialized backend does not pay for arbitrary-precision arithmetic to manipulate a few limbs. Every boundary where truncation or overflow could matter is visible in the code, and Core.Proof relates these routines to their unbounded-natural specifications. Wider inputs use the general numerical kernel rather than an approximate host operation.

@[inline]

def FloatLib.Numerics.FixedWord.finiteScale (exponent : UInt64) : UInt64

Encode a finite exponent as the nonnegative scale used by compact arithmetic kernels.

@[inline]

def FloatLib.Numerics.FixedWord.roundShiftRightEven (value : UInt64) (shift : ℕ) : UInt64

Round a UInt64 divided by 2^shift to nearest, with ties to even.

@[inline]

def FloatLib.Numerics.FixedWord.roundShiftRightEvenNat (value shift : ℕ) : ℕ

Use native nearest-even shifting whenever the input fits in one machine word.

Core.Proof.Rounding registers this dispatcher as the @[csimp] replacement for Numerics.roundShiftRightEven. Wider inputs retain the guard bit with the quotient and reuse those bits to test for a discarded suffix. Only a set guard bit with an even quotient needs that test, and no halfway marker or remainder is constructed.

@[inline]

def FloatLib.Numerics.FixedWord.roundQuotientEven (num den : UInt64) : UInt64

Round the native quotient num / den to nearest, with ties to even.

Since num % den < den, comparing the remainder with den - remainder decides 2 * remainder against den without leaving the word, because the subtraction cannot underflow and nothing is doubled. For den = 0 the kernel returns 0. This differs from Numerics.roundQuotientEven num 0, which inherits Lean's n / 0 = 0 and n % 0 = n and so returns 1 for nonzero num. So roundQuotientEven_toNat assumes den ≠ 0.

@[inline]

def FloatLib.Numerics.FixedWord.roundQuotientEvenNat (num den : ℕ) : ℕ

Use native quotient rounding when the numerator fits in the signed-word range and the denominator is a nonzero machine word.

The numerator bound keeps the incremented quotient below 2^64. Core.Proof.Rounding registers this dispatcher as the @[csimp] replacement for Numerics.roundQuotientEven, so the arbitrary-precision branch repeats the logical definition instead of calling it. A call would make compiler simplification recurse through the replacement theorem.

structure FloatLib.Numerics.FixedWord.RestoringRootState (α : Type u) : Type u

Root and remainder produced by a restoring square-root loop.

The carrier is chosen by capacity. Restoring kernels over one or more native words share this state and the same square/remainder invariant.

• root : α

  Current floor-root prefix.

• remainder : α

  Remainder after the consumed base-four digits.

def FloatLib.Numerics.FixedWord.instDecidableEqRestoringRootState.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : RestoringRootState α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instDecidableEqRestoringRootState {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (RestoringRootState α✝)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instReprRestoringRootState {α✝ : Type u_1} [Repr α✝] : Repr (RestoringRootState α✝)

def FloatLib.Numerics.FixedWord.instReprRestoringRootState.repr {α✝ : Type u_1} [Repr α✝] : RestoringRootState α✝ → ℕ → Std.Format

Representation-independent nearest-even selection

@[inline]

def FloatLib.Numerics.FixedWord.selectNearestEvenNat (comparison : Ordering) (lower upper : ℕ) : ℕ

Select one of two adjacent natural-number codes from a midpoint comparison.

The comparison is target versus midpoint. Equality uses the low bit of the lower code for ties-to-even. Numerical formats share this decision while keeping their own decoders, candidate construction, and exceptional-value semantics.

@[inline]

def FloatLib.Numerics.FixedWord.selectNearestEvenWord (comparison : Ordering) (lower upper : UInt64) : UInt64

Machine-word sibling of selectNearestEvenNat.

The parity test stays in UInt64, so fixed-carrier rounding kernels avoid a conversion to Nat.

Machine-width bit-field primitives

@[inline]

def FloatLib.Numerics.FixedWord.log2WordStep (shift : UInt64) (next : UInt64 → UInt64) (value : UInt64) : UInt64

Select the half containing the leading bit and add its offset to the next stage.

@[inline]

def FloatLib.Numerics.FixedWord.log2Word (value : UInt64) : UInt64

Floor binary logarithm from at most four word stages and a packed lookup, with zero mapped to zero.

Zero and one return immediately. Other four-bit values go straight to the packed lookup, and larger byte-sized values need only the final stage. For larger words, each preceding stage halves the range of possible leading-bit positions. The remaining four-bit value indexes a two-bit entry in the scalar constant 0xffffaa50. All work stays in machine words, with no loop whose length grows with the position of the leading bit. Core.Proof.Word proves equality with UInt64.log2 on the entire word range.

@[inline]

def FloatLib.Numerics.FixedWord.bitAtWord (value index : UInt64) : Bool

Read one bit from a machine word using a machine-word index.

Lean's UInt64 shifts reduce their count modulo 64, so the range check is part of the semantics: an index outside the stored word returns false instead of wrapping to a different bit. Format backends should keep statically bounded field widths in this representation throughout their hot decoder and cross to Nat only at an arbitrary-precision boundary.

@[inline]

def FloatLib.Numerics.FixedWord.lowMaskWord (width : UInt64) : UInt64

Mask the low width bits of a machine word.

The complete-width branch avoids the modulo-64 interpretation of 1 <<< 64.

@[inline]

def FloatLib.Numerics.FixedWord.lowBitsWord (value width : UInt64) : UInt64

Retain the low width bits of a machine word.

@[inline]

def FloatLib.Numerics.FixedWord.countLeadingZerosWord (value width : UInt64) : UInt64

Count leading zeroes in the retained low-width field without crossing through Nat.

Callers establish width ≤ 64. For a nonzero field, log2Word gives its highest set-bit index, so the result is width - bitLength, and under that contract the subtraction cannot underflow.

@[inline]

def FloatLib.Numerics.FixedWord.countLeadingRunWord (value width : UInt64) (bit : Bool) : UInt64

Count a leading equal-bit run in a low-width machine field.

Leading ones are leading zeroes after whole-word complementation. Bits above width are discarded by lowBitsWord, so complementing the whole word gives the fixed-field count.

@[inline]

def FloatLib.Numerics.FixedWord.shiftRightWord (value shift : UInt64) : UInt64

Shift right by a machine-word amount, returning zero at and beyond the carrier width.

@[inline]

def FloatLib.Numerics.FixedWord.jamCombine (sameSign exact : Bool) (A q : UInt64) : UInt64

The sticky quotient shiftRightJam (A * 2^d + B) d, or of A * 2^d - B when the signs differ, from q = B / 2^d and whether that division was exact (jamCombine_toNat).

structure FloatLib.Numerics.FixedWord.UInt128 : Type

A 128-bit unsigned value represented by two native 64-bit limbs.

• hi : UInt64

  Bits 64 through 127.

• lo : UInt64

  Bits 0 through 63.

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instDecidableEqUInt128 : DecidableEq UInt128

def FloatLib.Numerics.FixedWord.instDecidableEqUInt128.decEq (x✝ x✝¹ : UInt128) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.FixedWord.instReprUInt128.repr : UInt128 → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.instReprUInt128 : Repr UInt128

@[irreducible]

def FloatLib.Numerics.FixedWord.UInt128.toNat (value : UInt128) : ℕ

Mathematical value of a two-limb unsigned integer.

The definition is irreducible. Unfolding it during reduction would expand value.hi.toNat * 2 ^ 64 one successor at a time and exhaust the recursion limit, and #eval reduces the type of a two-word storage code, whose bound mentions this function, while it looks for a ToExpr instance. Proofs unfold it with simp [UInt128.toNat], unfold UInt128.toNat, or UInt128.toNat.eq_1, since rfl, change, show, and decide do not unfold it.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.ofNat (value : ℕ) : UInt128

Split the residue of a natural number modulo 2^128 into two native 64-bit limbs.

@[inline]

def FloatLib.Numerics.FixedWord.low32 (value : UInt64) : UInt64

Low 32-bit half of a native word.

@[inline]

def FloatLib.Numerics.FixedWord.high32 (value : UInt64) : UInt64

High 32-bit half of a native word.

@[inline]

def FloatLib.Numerics.FixedWord.mul64 (x y : UInt64) : UInt128

Full 128-bit product of two 64-bit words in native arithmetic.

The same half-word carry decomposition appears in Go 1.23.0, math/bits.Mul64: https://github.com/golang/go/blob/go1.23.0/src/math/bits/bits.go#L470-L483 See also Henry S. Warren, Jr., Hacker's Delight, 2nd ed., §8.2, "High-Order Half of 64-Bit Product".