Verified fixed-word division candidates

The radix-2^32 runtime loop is a candidate generator. Its quotient and remainder are accepted when native multiplication and addition confirm the Euclidean division equation and the remainder bound. If that check rejects the candidate, the runtime falls back to a restoring accumulator. This module proves that accumulator equal to the logical recurrence and certifies its result on normalized inputs of precision + 1 bits with 64 < precision ≤ 126.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.CandidateShift.toNat_bounds (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (shift : CandidateShift) : 64 < toNat precision shift ∧ toNat precision shift < 128

Both candidate shifts of an in-range precision lie strictly between one and two words.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.certificate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (quotient remainder : UInt128) (hdecomposition : quotient.toNat * den.toNat + remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift) (hremainder : remainder.toNat < den.toNat) : certificate precision num den shift quotient remainder = true

The executable certificate accepts every representable Euclidean decomposition for the two shifts used by two-limb division.

This is completeness of the independent checker, not of the speculative Algorithm D generator.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.certificate_sound (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (quotient remainder : UInt128) (hvalid : certificate precision num den shift quotient remainder = true) : quotient.toNat * den.toNat + remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift ∧ remainder.toNat < den.toNat

A successful native certificate gives the quotient/remainder decomposition and the Euclidean remainder bound. The proof does not depend on the radix-2^32 candidate generator.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.restoringCandidate_eq_quotientSteps128 (precision : ℕ) (num den : UInt128) (shift : CandidateShift) : restoringCandidate precision num den shift = RestoringQuotient.quotientSteps128 den (CandidateShift.toNat precision shift) (restoringInitial num den)

The allocation-light restoring repair agrees with the logical two-limb recurrence.

Runtime code calls the primitive-word accumulator, and proofs continue from this theorem through quotientSteps128.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.restoringCandidate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : certificate precision num den shift (restoringCandidate precision num den shift).quotient (restoringCandidate precision num den shift).remainder = true

The restoring repair produces a certified candidate for normalized precision + 1-bit significands.

The shift is precision when the numerator is at least the denominator and precision + 1 otherwise, as the two-limb backends choose it.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_eq_repair_of_certificate_false (precision : ℕ) (num den : UInt128) (shift : CandidateShift) (hrejected : certificate precision num den shift (candidate precision num den shift).1 (candidate precision num den shift).2 = false) : checkedCandidate precision num den shift = { quotient := (restoringCandidate precision num den shift).quotient, remainder := (restoringCandidate precision num den shift).remainder }

A rejected Algorithm D candidate selects the restoring repair.

No hypothesis on the operands is needed beyond the failed certificate.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_complete (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : certificate precision num den shift (checkedCandidate precision num den shift).quotient (checkedCandidate precision num den shift).remainder = true

The checked candidate is complete on the normalized two-limb division domain.

Either the fast candidate passes its certificate, or the proved restoring loop supplies the quotient and remainder. Either way the returned pair is certified, with no second runtime check and no unreachable backend fallback.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate_sound (precision : ℕ) (hprecision : 64 < precision ∧ precision ≤ 126) (num den : UInt128) (shift : CandidateShift) (hnum : 2 ^ precision ≤ num.toNat ∧ num.toNat < 2 ^ (precision + 1)) (hden : 2 ^ precision ≤ den.toNat ∧ den.toNat < 2 ^ (precision + 1)) (hshift : shift = if den.toNat ≤ num.toNat then CandidateShift.exact else CandidateShift.extra) : (checkedCandidate precision num den shift).quotient.toNat * den.toNat + (checkedCandidate precision num den shift).remainder.toNat = num.toNat * 2 ^ CandidateShift.toNat precision shift ∧ (checkedCandidate precision num den shift).remainder.toNat < den.toNat

The candidate selected by the fast-check-or-repair runtime path satisfies Euclidean division.

It combines checkedCandidate_complete with certificate_sound, so callers get the equation and the strict remainder bound without unfolding the executable certificate.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.roundQuotient_toNat (den quotient remainder : UInt128) (numerator : ℕ) (hdenFit : den.toNat < 2 ^ 127) (hdecomposition : quotient.toNat * den.toNat + remainder.toNat = numerator) (hremainder : remainder.toNat < den.toNat) (hquotientFit : quotient.toNat + 1 < 2 ^ 128) : (roundQuotient den quotient remainder).toNat = Numerics.roundQuotientEven numerator den.toNat

Native quotient rounding agrees with exact nearest-even rational rounding for a certified Euclidean decomposition.

theorem FloatLib.Numerics.FixedWord.CertifiedDivision.roundQuotient_toNat_eq_or (den quotient remainder : UInt128) (hquotientFit : quotient.toNat + 1 < 2 ^ 128) : (roundQuotient den quotient remainder).toNat = quotient.toNat ∨ (roundQuotient den quotient remainder).toNat = quotient.toNat + 1

Native quotient rounding returns the input quotient or its successor when incrementing fits.