Compiler certificates for restoring quotient loops

The logical restoring loop is convenient for proofs, while the primitive-word accumulator avoids allocating a state at every generated quotient bit. This module proves the one- and two-limb loops extensionally equal and registers the optimized direction with @[csimp].

Keeping this certificate separate from Quotient.Proof matters for executable clients: they can enable the verified compiler rewrite without importing the much larger rational-arithmetic proof development.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStepsWords_eq (den : UInt64) (n : ℕ) (quotient remainder : UInt64) : quotientStepsWords den n quotient remainder = quotientSteps den n { quotient := quotient, remainder := remainder }

The unboxed one-word accumulators preserve every step of the restoring recurrence.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStepsImpl_eq_quotientSteps (den : UInt64) (n : ℕ) (state : QuotientState UInt64) : quotientStepsImpl den n state = quotientSteps den n state

The one-word implementation agrees for every state and iteration count.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps_eq_quotientStepsImpl : quotientSteps = quotientStepsImpl

Compile one-word restoring division through primitive accumulators.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.roundScaledQuotient_eq_roundScaledQuotientImpl : roundScaledQuotient = roundScaledQuotientImpl

Compile scaled quotient rounding through the same accumulator.

This equation also replaces calls whose original body was compiled before the loop certificate was imported.

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128Impl_eq_quotientSteps128 (den : UInt128) (n : ℕ) (state : QuotientState UInt128) : quotientSteps128Impl den n state = quotientSteps128 den n state

The primitive-word accumulator implements the logical two-limb restoring recurrence.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128_eq_quotientSteps128Impl : quotientSteps128 = quotientSteps128Impl

Compile the logical two-limb quotient loop through its verified word accumulator.