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, and
Quotient.Restoring128Proof proves the two-limb loop.
Quotient and remainder state shared by the native loop and its natural-number proof model.
- quotient : α
Binary quotient prefix generated so far.
- remainder : α
Remainder after the generated quotient prefix.
Instances For
Instances For
Instances For
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.
Instances For
Generate n binary quotient digits, under the same capacity contract as quotientStep.
Instances For
Generate quotient digits with unboxed quotient and remainder accumulators.
Only the final result constructs a QuotientState. The arithmetic is that of quotientSteps,
including word wraparound outside its capacity bounds.
Instances For
Run the one-word restoring loop without allocating a state for each quotient bit.
Instances For
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.
Instances For
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.
Instances For
Compiled two-limb quotient loop, on the accumulators of quotientSteps128Words.
It constructs the public state once, after the final digit, so no step allocates a structure or an addition result.
Instances For
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 Internal.quotientSteps128 instead.
That module proves the two equal and registers the equation with @[csimp], so the substitution
carries a proof, which implemented_by would not. Modules that import only this runtime compile
the logical recursion.
Instances For
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.
Instances For
Floating-point candidate for (num <<< shift) / den when shift < 64. Its accuracy is never
assumed, because isFloorQuotient checks every candidate.
Instances For
Remainder of scaled after subtracting guess * den, as a two-word value.
Instances For
Whether guess is the floor quotient of scaled by den with room to round up, decided from
the two-word product and remainder.
Instances For
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.
Instances For
Compiled roundScaledQuotient. When shift < 64 and 0 < den < 2^63, the floating-point
candidate or a neighbour that passes isFloorQuotient replaces the restoring loop. Otherwise the
loop runs on primitive-word accumulators. The checked state is never materialized, so the fast path
allocates nothing. Quotient.Compiler proves it equal to roundScaledQuotient.
Instances For
Compute floor (log2 (num / den)) for nonzero operands, using native-word alignment.