Verified single-word primitives for executable numerical arithmetic

Native-word shifts, bit operations, and restoring square-root state have exact natural-number interpretations. Nearest-even rounding is proved in Core.Proof.Rounding; wider two-limb values and exact 64 × 64 → 128 multiplication are proved in Core.Proof.UInt128.

theorem FloatLib.Numerics.FixedWord.uint64_add_toNat_of_lt (x y : UInt64) (hfit : x.toNat + y.toNat < 2 ^ 64) : (x + y).toNat = x.toNat + y.toNat

A native-word sum has its ordinary natural-number value when that sum does not overflow the word.

theorem FloatLib.Numerics.FixedWord.uint64_mul_toNat_of_lt (x y : UInt64) (hfit : x.toNat * y.toNat < 2 ^ 64) : (x * y).toNat = x.toNat * y.toNat

A native-word product has its natural-number value when it does not overflow the word.

def FloatLib.Numerics.FixedWord.RestoringRootState.Represents {α : Type} (toNat : α → ℕ) (state : RestoringRootState α) (value : ℕ) : Prop

Mathematical meaning of a restoring square-root state, independent of the native carrier used by the executable loop.

theorem FloatLib.Numerics.FixedWord.RestoringRootState.root_lt_two_pow {α : Type} (toNat : α → ℕ) (precision : ℕ) {state : RestoringRootState α} {value : ℕ} (hrep : Represents toNat state value) (hvalue : value < 2 ^ (2 * precision)) : toNat state.root < 2 ^ precision

The root component of a valid restoring state fits in the requested precision whenever the processed radicand fits in twice that precision.

theorem FloatLib.Numerics.FixedWord.RestoringRootState.root_eq_sqrt {α : Type} (toNat : α → ℕ) {state : RestoringRootState α} {value : ℕ} (hrep : Represents toNat state value) : toNat state.root = value.sqrt

The root component of a valid restoring state is the exact floor square root, independently of the machine-word carrier used by the executable loop.

theorem FloatLib.Numerics.FixedWord.RestoringRootState.sqrt_spec {α : Type} (toNat : α → ℕ) {state : RestoringRootState α} {value : ℕ} (hrep : Represents toNat state value) : toNat state.root = value.sqrt ∧ toNat state.remainder = value - value.sqrt * value.sqrt

A valid restoring state contains the exact floor square root and its square remainder.

theorem FloatLib.Numerics.FixedWord.maskedBaseFourDigit_lt (value : UInt64) : (value &&& 3).toNat < 4

Masking a native word to one base-four digit always produces a value below four.

theorem FloatLib.Numerics.FixedWord.lowBitIsZero_eq_even (code : UInt64) : (code &&& 1 == 0) = decide (code.toNat % 2 = 0)

Native low-bit inspection is exactly natural-number parity.

theorem FloatLib.Numerics.FixedWord.lowBitIsNonzero_eq_odd (code : UInt64) : (code &&& 1 != 0) = (code.toNat % 2 != 0)

Native low-bit nonzero inspection is exactly odd natural-number parity.

theorem FloatLib.Numerics.FixedWord.UInt128.lowBitIsZero_eq_even (code : UInt128) : (code.lo &&& 1 == 0) = decide (code.toNat % 2 = 0)

Inspecting the low bit of a two-limb word is natural-number parity.

theorem FloatLib.Numerics.FixedWord.UInt128.lowBitIsNonzero_eq_odd (code : UInt128) : (code.lo &&& 1 != 0) = (code.toNat % 2 != 0)

Two-limb low-bit nonzero inspection is exactly odd natural-number parity.

@[simp]

theorem FloatLib.Numerics.FixedWord.selectNearestEvenWord_toNat (comparison : Ordering) (lower upper : UInt64) : (selectNearestEvenWord comparison lower upper).toNat = selectNearestEvenNat comparison lower.toNat upper.toNat

Machine-word nearest-even selection has the same natural-number code as the shared scalar selector.

@[simp]

theorem FloatLib.Numerics.FixedWord.log2_toNat (value : UInt64) : value.log2.toNat = value.toNat.log2

Native UInt64.log2 has the same natural-number value as Nat.log2.

theorem FloatLib.Numerics.FixedWord.log2_low_add_high_mul_pow (low high offset : ℕ) (hlow : low < 2 ^ offset) (hhigh : high ≠ 0) : (low + high * 2 ^ offset).log2 = offset + high.log2

When the high part is nonzero, the low bits do not change its leading-bit position.

theorem FloatLib.Numerics.FixedWord.log2_toNat_lt_of_toNat_lt_two_pow (value : UInt64) (width : ℕ) (hvalue : value ≠ 0) (hfit : value.toNat < 2 ^ width) : value.log2.toNat < width

If a nonzero native word fits below 2 ^ width, then its leading-bit position is smaller than width.

theorem FloatLib.Numerics.FixedWord.two_pow_le_shiftLeft_sub_log2 (precision value : ℕ) (hvalue : value ≠ 0) (hleading : value.log2 ≤ precision) : 2 ^ precision ≤ value <<< (precision - value.log2)

Moving a nonzero value's leading bit to precision puts it at or above 2 ^ precision.

theorem FloatLib.Numerics.FixedWord.shiftLeft_sub_log2_lt_two_pow (precision value : ℕ) (hleading : value.log2 ≤ precision) : value <<< (precision - value.log2) < 2 ^ (precision + 1)

Moving the leading bit to precision keeps the value below the next power of two.

theorem FloatLib.Numerics.FixedWord.shiftLeft_toNat (value : UInt64) (shift : ℕ) (hshift : shift < 64) (hfit : value.toNat <<< shift < 2 ^ 64) : (value <<< UInt64.ofNat shift).toNat = value.toNat <<< shift

A native left shift has its mathematical natural-number value when the shift amount and result fit.

theorem FloatLib.Numerics.FixedWord.shiftLeft_toNat_mod (value : UInt64) (shift : ℕ) (hshift : shift < 64) : (value <<< UInt64.ofNat shift).toNat = value.toNat * 2 ^ shift % 2 ^ 64

An in-range native left shift is multiplication modulo the word size.

theorem FloatLib.Numerics.FixedWord.uint64_powTwo_toNat (exponent : ℕ) (hexponent : exponent < 64) : (1 <<< UInt64.ofNat exponent).toNat = 2 ^ exponent

Shifting the native word 1 within range represents the corresponding power of two.

theorem FloatLib.Numerics.FixedWord.shiftLeftLowBits_toNat (value : UInt64) (inner : ℕ) (hpositive : 0 < inner) (hinner : inner < 64) : (value <<< UInt64.ofNat (64 - inner)).toNat = value.toNat % 2 ^ inner * 2 ^ (64 - inner)

Moving the low inner bits of a word to the high end has the expected natural-number value.

This is the wrapped half of a cross-limb right shift. Keeping it in the fixed-word core lets every multi-limb backend share the same machine-word argument.

theorem FloatLib.Numerics.FixedWord.shiftRight_toNat (value : UInt64) (shift : ℕ) (hshift : shift < 64) : (value >>> UInt64.ofNat shift).toNat = value.toNat >>> shift

A native right shift by an in-range natural has the expected mathematical value.

theorem FloatLib.Numerics.FixedWord.shiftedPair_toNat (low high : UInt64) (inner : ℕ) (hpositive : 0 < inner) (hinner : inner < 64) : (low >>> UInt64.ofNat inner ||| high <<< UInt64.ofNat (64 - inner)).toNat = low.toNat / 2 ^ inner + high.toNat % 2 ^ inner * 2 ^ (64 - inner)

Joining the two halves of a cross-limb right shift has the expected natural-number value.

def FloatLib.Numerics.FixedWord.BaseFour.place (index : ℕ) : ℕ

Positional weight of one base-four digit.

def FloatLib.Numerics.FixedWord.BaseFour.digitsValue {α : Type} (digitAt : α → ℕ → UInt64) (source : α) : ℕ → ℕ

Value reconstructed from the first steps digits of any machine-word base-four source.

Concrete radicand layouts provide only their digit reader; the positional recurrence and loop proof are shared across one-word and multi-word square-root kernels.

def FloatLib.Numerics.FixedWord.BaseFour.wordDigit (value : UInt64) (index : ℕ) : ℕ

Base-four digit selected from a machine word; indices below 32 avoid shift-count wraparound.

def FloatLib.Numerics.FixedWord.BaseFour.wordDigits (value : UInt64) : ℕ → ℕ

Value reconstructed from the first steps base-four digits of a machine word.

theorem FloatLib.Numerics.FixedWord.BaseFour.wordDigit_eq (value : UInt64) (index : ℕ) (hindex : index < 32) : wordDigit value index = value.toNat / place index % 4

Machine extraction agrees with natural-number base-four digit selection.

theorem FloatLib.Numerics.FixedWord.BaseFour.place_succ (index : ℕ) : place (index + 1) = place index * 4

Advancing one base-four position multiplies its weight by four.

theorem FloatLib.Numerics.FixedWord.BaseFour.loop_represents {α β : Type} (toNat : α → ℕ) (digitAt : β → ℕ → UInt64) (step : UInt64 → RestoringRootState α → RestoringRootState α) (loop : β → ℕ → RestoringRootState α → RestoringRootState α) (bound : ℕ) (hloopZero : ∀ (source : β) (state : RestoringRootState α), loop source 0 state = state) (hloopSucc : ∀ (source : β) (steps : ℕ) (state : RestoringRootState α), loop source (steps + 1) state = loop source steps (step (digitAt source steps) state)) (hdigit : ∀ (source : β) (index : ℕ), (digitAt source index).toNat < 4) (hstep : ∀ (state : RestoringRootState α) (digit : UInt64) (value : ℕ), RestoringRootState.Represents toNat state value → value < bound → digit.toNat < 4 → RestoringRootState.Represents toNat (step digit state) (value * 4 + digit.toNat)) (source : β) (steps : ℕ) (state : RestoringRootState α) (value : ℕ) (hrep : RestoringRootState.Represents toNat state value) (hfit : value * place steps + digitsValue digitAt source steps < bound) : RestoringRootState.Represents toNat (loop source steps state) (value * place steps + digitsValue digitAt source steps)

Generic refinement of a restoring loop from a proved digit step.

Only the carrier-specific step theorem and recursive equations are supplied by a backend. The base-four accumulation and induction are independent of word width.

theorem FloatLib.Numerics.FixedWord.BaseFour.place_add (left right : ℕ) : place (left + right) = place left * place right

Base-four positional weights multiply when their indices add.

theorem FloatLib.Numerics.FixedWord.BaseFour.wordDigits_eq_mod (value : UInt64) (steps : ℕ) (hsteps : steps ≤ 32) : wordDigits value steps = value.toNat % place steps

Reconstructing the low base-four digits is reduction modulo their total width.

@[simp]

theorem FloatLib.Numerics.FixedWord.bitAtWord_eq_testBit (value index : UInt64) : bitAtWord value index = value.toNat.testBit index.toNat

Machine-indexed bit inspection agrees with natural-number bit inspection.

theorem FloatLib.Numerics.FixedWord.lowMaskWord_toNat (width : UInt64) (hwidth : width < 64) : (lowMaskWord width).toNat = 2 ^ width.toNat - 1

Natural value of a machine-indexed low-bit mask below the carrier width.

theorem FloatLib.Numerics.FixedWord.lowBitsWord_toNat (value width : UInt64) (hwidth : width ≤ 64) : (lowBitsWord value width).toNat = value.toNat % 2 ^ width.toNat

Machine-indexed low-bit extraction is exact through the complete carrier width.

theorem FloatLib.Numerics.FixedWord.uint64_lowBits_toNat (value : UInt64) (shift : ℕ) (hshift : shift < 64) : (value &&& 1 <<< UInt64.ofNat shift - 1).toNat = value.toNat % 2 ^ shift

Masking a native word to a Nat-indexed low-bit field agrees with reduction modulo the corresponding power of two.

This theorem bridges kernels whose control flow uses Nat to the shared machine-indexed lowBitsWord primitive; the executable data path remains on unboxed UInt64 values.

theorem FloatLib.Numerics.FixedWord.shiftRightWord_toNat (value shift : UInt64) (hshift : shift < 64) : (shiftRightWord value shift).toNat = value.toNat >>> shift.toNat

Machine-indexed right shift agrees with natural-number right shift in range.

theorem FloatLib.Numerics.FixedWord.countLeadingZerosWord_toNat (value width : UInt64) (hwidth : width ≤ 64) : (countLeadingZerosWord value width).toNat = have truncated := lowBitsWord value width; if (truncated == 0) = true then width.toNat else width.toNat - (truncated.log2.toNat + 1)

Machine-width leading-zero counting has the corresponding natural-number value.

The nonzero branch proves that log2 + 1 is at most the retained field width before interpreting the machine subtraction. This is the capacity invariant that rules out unsigned wraparound.

theorem FloatLib.Numerics.FixedWord.countLeadingRunWord_toNat (value width : UInt64) (bit : Bool) (hwidth : width ≤ 64) : (countLeadingRunWord value width bit).toNat = have source := if bit = true then ~~~value else value; have truncated := lowBitsWord source width; if (truncated == 0) = true then width.toNat else width.toNat - (truncated.log2.toNat + 1)

Machine-width equal-bit run counting reduces to the shared leading-zero primitive.