Fixed-word restoring quotient generation

One- and two-limb unsigned restoring-division state machines share a quotient/remainder recurrence, alongside a one-word rational-logarithm kernel. Quotient.Proof proves the one-word loop and the two-limb step; Quotient.Restoring128Proof proves the two-limb loop.

structure FloatLib.Numerics.FixedWord.RestoringQuotient.QuotientState (α : Type u) : Type u

Quotient and remainder state shared by the native loop and its natural-number proof model.

• quotient : α

  Binary quotient prefix generated so far.

• remainder : α

  Exact remainder after the generated quotient prefix.

def FloatLib.Numerics.FixedWord.RestoringQuotient.instDecidableEqQuotientState.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : QuotientState α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.RestoringQuotient.instDecidableEqQuotientState {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (QuotientState α✝)

@[instance_reducible]

instance FloatLib.Numerics.FixedWord.RestoringQuotient.instReprQuotientState {α✝ : Type u_1} [Repr α✝] : Repr (QuotientState α✝)

def FloatLib.Numerics.FixedWord.RestoringQuotient.instReprQuotientState.repr {α✝ : Type u_1} [Repr α✝] : QuotientState α✝ → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStep (den : UInt64) (state : QuotientState UInt64) : QuotientState UInt64

Generate one additional binary quotient digit.

Callers keep den < 2^63 and remainder < den, so the doubled remainder fits one word, and keep the generated quotient prefix below 2^63 so that its doubling fits as well.

@[inline]

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

Generate n binary quotient digits, under the same capacity contract as quotientStep.

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

Generate quotient digits with unboxed quotient and remainder accumulators.

Only the final result constructs a QuotientState. The arithmetic is identical to quotientSteps, including word wraparound outside its exact-arithmetic capacity bounds.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStepsImpl (den : UInt64) (n : ℕ) (state : QuotientState UInt64) : QuotientState UInt64

Run the one-word restoring loop without allocating a state for each quotient bit.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.quotientStep128 (den : UInt128) (state : QuotientState UInt128) : QuotientState UInt128

Generate one binary quotient digit in a two-limb carrier.

Callers maintain remainder < den < 2^127 and quotient < 2^127. These bounds keep the doubled remainder and the next quotient prefix in UInt128, so the step agrees with the natural-number restoring recurrence.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128Words (denHi denLo : UInt64) : ℕ → UInt64 → UInt64 → UInt64 → UInt64 → QuotientState UInt128

Generate two-limb quotient digits using four primitive machine-word accumulators.

The preconditions are the same as quotientStep128: callers keep the denominator below 2^127, the remainder below the denominator, and the generated quotient in range.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.quotientSteps128Impl (den : UInt128) (n : ℕ) (state : QuotientState UInt128) : QuotientState UInt128

Compiled two-limb quotient loop.

The implementation keeps quotient and remainder in four primitive machine-word accumulators. It constructs the public state only once, after the final digit, avoiding per-step structure and addition-result allocation.

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

Generate n binary quotient digits in a two-limb carrier.

The logical body is the shared restoring recurrence, and it is the only definition the kernel sees. With Quotient.Compiler imported, compiled code runs quotientSteps128Impl instead: that module proves the two extensionally equal and registers the equation with @[csimp], so the substitution is checked rather than asserted through implemented_by. Modules that import only this runtime compile the logical recursion.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.roundQuotientState (den : UInt64) (state : QuotientState UInt64) : UInt64

Round a restoring-division state to nearest, with ties to even.

Callers keep 0 < den < 2^63, remainder < den, and the quotient below 2^63, so the doubled remainder and the incremented quotient fit one word.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.roundScaledQuotient (num den : UInt64) (shift : ℕ) : UInt64

Round (num / den) * 2^shift to nearest even using native restoring division.

roundScaledQuotient_toNat requires 0 < den < 2^63 and (num <<< shift) / den + 1 < 2^63, which keep every intermediate of the restoring loop inside one word.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.roundScaledQuotientImpl (num den : UInt64) (shift : ℕ) : UInt64

Nearest-even quotient rounding through the primitive-word accumulator.

@[inline]

def FloatLib.Numerics.FixedWord.RestoringQuotient.floorLog2RatWord (num den : UInt64) : ℤ

Compute floor (log2 (num / den)) for nonzero operands, using native-word alignment.