Certified fixed-word division runtime

The radix-2^32 loop generates a quotient and remainder candidate for two normalized two-limb significands of precision + 1 bits, for any precision from 65 to 126. An executable certificate then checks the Euclidean equation and the remainder bound, and a rejected candidate is replaced by the allocation-light restoring accumulator. Soundness, completeness of the repair, and equality between that accumulator and the logical recurrence are proved in CertifiedDivision.Proof.

inductive FloatLib.Numerics.FixedWord.CertifiedDivision.CandidateShift : Type

Scaling distance for a normalized quotient of two precision + 1-bit significands.

Division needs two cases: precision when the numerator is at least the denominator, and precision + 1 otherwise. A closed type keeps an unsupported distance from silently selecting one of the fixed-word layouts.

• exact : CandidateShift

  Scale the numerator by 2^precision.

• extra : CandidateShift

  Scale the numerator by 2^(precision + 1).

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instDecidableEqCandidateShift : DecidableEq CandidateShift

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instReprCandidateShift : Repr CandidateShift

def FloatLib.Numerics.FixedWord.CertifiedDivision.instReprCandidateShift.repr : CandidateShift → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.CandidateShift.toNat (precision : ℕ) : CandidateShift → ℕ

Natural-number exponent represented by a candidate shift for precision + 1-bit operands.

def FloatLib.Numerics.FixedWord.CertifiedDivision.radix32Mask : UInt64

A mask selecting the low radix-2^32 digit of a native word.

def FloatLib.Numerics.FixedWord.CertifiedDivision.radix32Base : UInt64

Radix 2^32 as a native 64-bit word.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.wordDigit32 (value : UInt128) : ℕ → UInt64

Read radix-2^32 digit index for index < 4. Larger indices return digit 3 too.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.wordsOfDigits32 (d0 d1 d2 d3 : UInt64) : UInt128

Pack four little-endian digits, each below 2^32, into a 128-bit word.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.adjustQuotientDigit (qhat rhat v3 v2 nextDigit : UInt64) : UInt64

Apply the at-most-two quotient-digit corrections required by normalized Knuth division and return the corrected digit.

The digit and its remainder stay in separate native words, because a pair of UInt64 values would box both components on every step.

structure FloatLib.Numerics.FixedWord.CertifiedDivision.Radix32StepResult : Type

Result of one radix-2^32 long-division step.

• d0 : UInt64

  Least-significant remainder digit.

• d1 : UInt64

  Second remainder digit.

• d2 : UInt64

  Third remainder digit.

• d3 : UInt64

  Fourth remainder digit.

• d4 : UInt64

  Most-significant remainder digit.

• quotient : UInt64

  Quotient digit selected by this step.

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instDecidableEqRadix32StepResult : DecidableEq Radix32StepResult

def FloatLib.Numerics.FixedWord.CertifiedDivision.instDecidableEqRadix32StepResult.decEq (x✝ x✝¹ : Radix32StepResult) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instReprRadix32StepResult : Repr Radix32StepResult

def FloatLib.Numerics.FixedWord.CertifiedDivision.instReprRadix32StepResult.repr : Radix32StepResult → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.radix32Step (v0 v1 v2 v3 d0 d1 d2 d3 d4 : UInt64) : Radix32StepResult

Consume one radix-2^32 quotient digit from a five-digit partial dividend.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.candidate (precision : ℕ) (num den : UInt128) (shift : CandidateShift) : UInt128 × UInt128

Generate a quotient/remainder candidate for a normalized numerator and denominator of precision + 1 bits, with 64 < precision ≤ 126.

The intended result is (num * 2^(shift.toNat precision)) / den together with the corresponding remainder. Knuth's Algorithm D runs in radix 2^32 after normalizing the divisor by 127 - precision bits so that its leading bit is bit 127. The numerator receives the same normalization, which places the scaled dividend at num * 2^127 or num * 2^128 independently of the precision, so the digit layout below does not depend on the format. The shift argument admits only the two layouts this kernel supports.

Algorithm reference: Donald E. Knuth, The Art of Computer Programming, vol. 2, Seminumerical Algorithms, 3rd ed. (1997), §4.3.1, Algorithm D.

The Algorithm D result is a speculative fast candidate that callers check with certificate. checkedCandidate keeps this hot path and calls a proved restoring divider only after a failed certificate.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.widenLow (value : UInt128) : UInt256

Embed a 128-bit word into the low half of a 256-bit word.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.certificate (precision : ℕ) (num den : UInt128) (shift : CandidateShift) (quotient remainder : UInt128) : Bool

Check a quotient/remainder candidate for the selected scaling distance.

The check is the Euclidean equation quotient * den + remainder = num * 2^(shift.toNat precision), computed in 256 bits without carry, together with remainder < den. For 64 < precision ≤ 126, certificate_sound shows that the check implies that the candidate is the true quotient and remainder.

structure FloatLib.Numerics.FixedWord.CertifiedDivision.CandidateResult : Type

Quotient and remainder selected for normalized two-limb division.

• quotient : UInt128

  Quotient of the scaled numerator.

• remainder : UInt128

  Euclidean remainder of the scaled numerator.

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instDecidableEqCandidateResult : DecidableEq CandidateResult

def FloatLib.Numerics.FixedWord.CertifiedDivision.instDecidableEqCandidateResult.decEq (x✝ x✝¹ : CandidateResult) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.CertifiedDivision.instReprCandidateResult : Repr CandidateResult

def FloatLib.Numerics.FixedWord.CertifiedDivision.instReprCandidateResult.repr : CandidateResult → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.restoringInitial (num den : UInt128) : RestoringQuotient.QuotientState UInt128

Initial quotient and remainder for operands with 0 < den and num < 2 * den.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.restoringCandidate (precision : ℕ) (num den : UInt128) (shift : CandidateShift) : RestoringQuotient.QuotientState UInt128

Recompute a scaled quotient with the allocation-light two-limb restoring loop.

This is a cold repair path. Normalized significands differ by less than a factor of two, so the initial quotient is zero or one and the selected shift generates the required precision + 1 quotient bits. restoringCandidate_eq_quotientSteps128 proves that this accumulator call equals the logical restoring recurrence.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.checkedCandidate (precision : ℕ) (num den : UInt128) (shift : CandidateShift) : CandidateResult

Run the fast Algorithm D candidate and repair a failed certificate with restoring division.

The common path is one Algorithm D candidate plus one certificate. If the check rejects the candidate, the function returns the restoring-division result. The proof module shows that the returned pair is correct on the normalized domain, so the backend needs no failure branch.

@[inline]

def FloatLib.Numerics.FixedWord.CertifiedDivision.roundQuotient (den quotient remainder : UInt128) : UInt128

Round a certified quotient to nearest, ties to even.

roundQuotient_toNat requires den < 2^127, remainder < den, and the incremented quotient below 2^128. The two-word backends satisfy these for their normalized operands.