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 logical and accumulator forms of the one- and two-limb loops equal and registers the accumulator direction with @[csimp].

The compiled scaled quotient also tries a floating-point candidate, checked in exact integer arithmetic, before the loop. Its certificate uses the loop's arithmetic specification from Quotient.Proof, imported here privately so executable clients get the rewrite without re-exporting that 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.Internal.quotientSteps_eq (den : UInt64) (n : ℕ) (state : QuotientState UInt64) : quotientSteps den n state = RestoringQuotient.quotientSteps den n state

The one-word accumulator agrees with the logical loop for every state and iteration count.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps_eq_internal : quotientSteps = Internal.quotientSteps

Compile one-word restoring division through primitive accumulators.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.roundScaledQuotient_eq_internal : roundScaledQuotient = Internal.roundScaledQuotient

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.Internal.quotientSteps128_eq (den : UInt128) (n : ℕ) (state : QuotientState UInt128) : quotientSteps128 den n state = RestoringQuotient.quotientSteps128 den n state

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

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128_eq_internal : quotientSteps128 = Internal.quotientSteps128

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