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. A separate executable certificate checks the exact Euclidean equation and remainder bound. Rejected candidates select the allocation-light restoring accumulator. Mathematical soundness, completeness of the repair, and equality between that accumulator and the logical recurrence are isolated in CertifiedDivision.Proof.

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

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

Division needs exactly these two cases: precision when the numerator is at least the denominator, and precision + 1 otherwise. Keeping the choice closed prevents 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

The radix 2^32, represented in 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 also return digit 3.

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

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

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 has only the two layouts supported by this kernel.

The Algorithm D result remains a speculative fast candidate: callers independently check it with certificate. checkedCandidate retains this exact hot path and invokes 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

Independently certify a quotient/remainder candidate for the selected scaling distance.

The check is the exact 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 direct 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 that check rejects the candidate, the function selects the restoring-division result instead. The proof module shows that this selected pair is exact on the normalized domain, so the backend does not need an additional 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.