Correctness of restoring quotient generation

The one-word restoring loop computes the nearest-even rounding of a rational quotient under its capacity bounds. This module also proves the two-limb step and the one-word rational logarithm. Quotient.Restoring128Proof extends the step theorem to the two-limb loop. Floating-point kernels supply their own decoding, exponent handling, and packing.

def FloatLib.Numerics.FixedWord.RestoringQuotient.natQuotientStep (den : ℕ) (state : QuotientState ℕ) : QuotientState ℕ

One restoring-division step in the natural-number proof model.

def FloatLib.Numerics.FixedWord.RestoringQuotient.natQuotientSteps (den : ℕ) : ℕ → QuotientState ℕ → QuotientState ℕ

Iterate the natural-number restoring-division step n times.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.natQuotientStep_spec (den : ℕ) (state : QuotientState ℕ) (hremainder : state.remainder < den) : have next := natQuotientStep den state; next.quotient * den + next.remainder = 2 * (state.quotient * den + state.remainder) ∧ next.remainder < den ∧ state.quotient ≤ next.quotient

One restoring step doubles the represented numerator, preserves a reduced remainder, and never decreases the quotient.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.natQuotientSteps_spec (den n : ℕ) (state : QuotientState ℕ) (hremainder : state.remainder < den) : have result := natQuotientSteps den n state; result.quotient * den + result.remainder = (state.quotient * den + state.remainder) * 2 ^ n ∧ result.remainder < den ∧ state.quotient ≤ result.quotient

After n restoring steps, the state represents the original numerator scaled by 2^n, with a remainder below the denominator.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.natQuotientSteps_div_mod (den n : ℕ) (state : QuotientState ℕ) (hremainder : state.remainder < den) : have numerator := (state.quotient * den + state.remainder) * 2 ^ n; have result := natQuotientSteps den n state; result.quotient = numerator / den ∧ result.remainder = numerator % den

The restoring loop returns the ordinary quotient and remainder of the scaled natural-number numerator.

def FloatLib.Numerics.FixedWord.RestoringQuotient.QuotientState.toNat (state : QuotientState UInt64) : QuotientState ℕ

Convert a native quotient state to its natural-number proof model.

def FloatLib.Numerics.FixedWord.RestoringQuotient.QuotientState.toNat128 (state : QuotientState UInt128) : QuotientState ℕ

Convert a two-limb quotient state to its natural-number proof model.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStep128_toNat (den : UInt128) (state : QuotientState UInt128) (hdenFit : den.toNat < 2 ^ 127) (hremainder : state.remainder.toNat < den.toNat) (hnextFit : (natQuotientStep den.toNat state.toNat128).quotient < 2 ^ 128) : (quotientStep128 den state).toNat128 = natQuotientStep den.toNat state.toNat128

One native two-limb restoring step refines the natural-number recurrence.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.roundQuotientState_toNat (den : UInt64) (state : QuotientState UInt64) (scaled : ℕ) (hden : den ≠ 0) (hdenFit : den.toNat < 2 ^ 63) (hquotient : state.quotient.toNat = scaled / den.toNat) (hremainderEq : state.remainder.toNat = scaled % den.toNat) (hquotientFit : scaled / den.toNat + 1 < 2 ^ 63) : (roundQuotientState den state).toNat = Numerics.roundQuotientEven scaled den.toNat

Nearest-even rounding of an exact quotient state is the reference quotient rounding.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.isFloorQuotient_spec {scaled : UInt128} {den guess : UInt64} (h : isFloorQuotient scaled den guess = true) : guess.toNat = scaled.toNat / den.toNat ∧ (quotientRemainder scaled den guess).lo.toNat = scaled.toNat % den.toNat ∧ guess.toNat + 1 < 2 ^ 63

An accepted quotient candidate is the floor quotient, with its remainder in the low word.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.roundScaledQuotient_toNat (num den : UInt64) (shift : ℕ) (hden : den ≠ 0) (hdenFit : den.toNat < 2 ^ 63) (hquotientFit : num.toNat <<< shift / den.toNat + 1 < 2 ^ 63) : (roundScaledQuotient num den shift).toNat = Numerics.roundQuotientEven (num.toNat <<< shift) den.toNat

Native restoring division computes the nearest-even rounding of the scaled rational quotient.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.floorLog2RatWord_eq (num den : UInt64) (hnum : num ≠ 0) (hden : den ≠ 0) : floorLog2RatWord num den = RationalBinary.floorLog2 num.toNat den.toNat

The native-word rational logarithm selector agrees with the representation-independent floorLog2 specification for nonzero operands.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.floorLog2RatWord_log_bounds (num den : UInt64) : Int.ofNat num.log2.toNat - Int.ofNat den.log2.toNat - 1 ≤ floorLog2RatWord num den ∧ floorLog2RatWord num den ≤ Int.ofNat num.log2.toNat - Int.ofNat den.log2.toNat

The native quotient logarithm differs from the difference of the operand logarithms by at most one.