Executable direct posit quotient packing

A quotient of two dyadics need not itself be dyadic. This algorithm avoids constructing a rational. Instead this module normalizes both significands, generates the leading quotient window required by the destination format, and folds every ungenerated one into the low sticky bit. The resulting finite stream is consumed by the same direct regime/exponent/fraction rounder used for exact dyadics.

The execution path is uniform at every arbitrary width: one integer division, one exact remainder test, and one guard/sticky packing pass. Its equality to exact quotient rounding is proved in Direct.Proof.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.prefixLeading (format : Format) : ℕ

Number of the quotient's normalized leading position.

A Posit has payloadBits bits below its sign. Retaining a quotient through that leading position leaves enough exponent/fraction stream for every possible guard bit; the jammed low bit records whether any later quotient digit is nonzero.

structure FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.NormalizedSignificands : Type

Normalize two positive significands to the same leading position.

The operands are shifted by different amounts to reach a common leading position. Their ratio changes by a power of two determined by the original leading positions; the result exponent compensates for this change.

• numerator : ℕ

  Numerator shifted so its leading bit reaches the common position.

• denominator : ℕ

  Denominator shifted so its leading bit reaches the common position.

• numeratorLeading : ℕ

  Leading-bit position of the original numerator.

• denominatorLeading : ℕ

  Leading-bit position of the original denominator.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.normalizeSignificands (numerator denominator : ℕ) : NormalizedSignificands

Shift two positive significands to their shared leading-bit position.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.prefixAtLeading (leading : ℕ) (numerator denominator : Numerics.Dyadic) : Numerics.Dyadic

Generate a normalized quotient prefix at an explicit leading position.

For nonzero input significands, normalized ratios below one emit one extra digit; ratios at least one begin with their known leading one. In both branches the quotient prefix has leading position leading, and the Euclidean remainder determines its exact sticky bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientPrefix (format : Format) (numerator denominator : Numerics.Dyadic) : Numerics.Dyadic

Generate the destination-width normalized quotient prefix.

The policy depends only on representable precision, not on a named storage backend or special format width.

Complete direct quotient rounding

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositiveCode (format : Format) (numerator denominator : Numerics.Dyadic) : ℕ

Round a positive quotient directly from its normalized prefix and exact sticky bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositive (format : Format) (numerator denominator : Numerics.Dyadic) : Model format

Pack the directly selected positive quotient code.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.round (format : Format) (numerator denominator : Numerics.Dyadic) : Model format

Round a signed quotient using the direct positive packer and shared special-value rules.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundCode (format : Format) (numerator denominator : Numerics.Dyadic) : ℕ

Complete signed quotient encoding for storage kernels that keep codes rather than models.

Division by zero emits the NaR code, a zero numerator emits zero, and the sign of a finite quotient is restored on the positive code. roundCode_eq_toNatBits identifies this with round.