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 merely to manipulate a few limbs. Every boundary where truncation or overflow could matter is kept explicit, 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. The arbitrary-precision branch therefore repeats the logical definition instead of calling it, so compiler simplification cannot recurse through the replacement theorem.

@[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: the subtraction is exact and no doubling can wrap. 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; roundQuotientEven_toNat accordingly 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; compiler simplification must not 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 selected by exact capacity. Restoring kernels over one or more native words share this state and the same square/remainder invariant.

• root : α

  Current floor-root prefix.

• remainder : α

  Exact remainder after the consumed base-four digits.

@[instance_reducible]

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

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

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

@[instance_reducible]

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

Representation-independent nearest-even selection

@[inline]

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

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

The comparison is target versus midpoint. Equality uses the low bit of the lower code for ties-to-even. Numerical formats may share this decision primitive while retaining 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.

Keeping the parity test in UInt64 prevents an otherwise unnecessary arbitrary-precision conversion in fixed-carrier rounding kernels.

Machine-width bit-field primitives

@[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. The explicit range check is therefore 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 exact 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, UInt64.log2 gives its highest set-bit index, so the result is width - bitLength; the subtraction is exact under that capacity contract.

@[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 the complement has exactly the intended fixed-field meaning.

@[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.

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

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

Mathematical value of a two-limb unsigned integer.

@[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

Exact native multiplication of two 64-bit words.

The implementation follows the four-half-word decomposition from Hacker's Delight.