Two-limb restoring quotient refinement #
Each step doubles quotient * denominator + remainder while keeping the remainder below the
denominator. Iterating the step theorem from Quotient.Proof gives the scaled quotient and
remainder, provided the denominator and quotient prefixes fit in two limbs.
theorem
FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStep128_spec
(den : UInt128)
(state : QuotientState UInt128)
(hdenFit : den.toNat < 2 ^ 127)
(hremainder : state.remainder.toNat < den.toNat)
(hquotientFit : 2 * state.quotient.toNat + 1 < 2 ^ 128)
:
have result := quotientStep128 den state;
result.quotient.toNat * den.toNat + result.remainder.toNat = 2 * (state.quotient.toNat * den.toNat + state.remainder.toNat) ∧ result.remainder.toNat < den.toNat ∧ state.quotient.toNat ≤ result.quotient.toNat ∧ result.quotient.toNat + 1 ≤ 2 * (state.quotient.toNat + 1)
One two-limb restoring step preserves the exact scaled numerator and keeps the quotient within the capacity required by the remaining loop.
theorem
FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128_spec
(den : UInt128)
(n : ℕ)
(state : QuotientState UInt128)
(hdenFit : den.toNat < 2 ^ 127)
(hremainder : state.remainder.toNat < den.toNat)
(hcapacity : (state.quotient.toNat + 1) * 2 ^ n ≤ 2 ^ 128)
:
The two-limb restoring loop preserves the exact scaled numerator without ever overflowing the quotient carrier.
theorem
FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128_div_mod
(den : UInt128)
(n : ℕ)
(state : QuotientState UInt128)
(hdenFit : den.toNat < 2 ^ 127)
(hremainder : state.remainder.toNat < den.toNat)
(hcapacity : (state.quotient.toNat + 1) * 2 ^ n ≤ 2 ^ 128)
:
The final two-limb restoring state is the exact quotient and remainder of its scaled numerator.