Executable direct exact-dyadic posit packing

Direct posit packing rounds the normalized exact-dyadic bit stream in one pass:

• the exact binary scale determines the standard two-bit-exponent regime;
• the regime, exponent, and normalized fraction are emitted most-significant bit first;
• one shared guard-and-sticky kernel performs nearest-even rounding at every width.

Direct packing avoids the reference rounder's search. Its equality to the exact model is proved in Direct.Proof.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositiveCode (format : Format) (target : Numerics.Dyadic) : ℕ

Round a positive exact dyadic directly from its normalized bit stream.

Interior values use one general guard/sticky kernel for every width. Regimes that consume the entire payload map directly to maxPos or minPos.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositive (format : Format) (target : Numerics.Dyadic) : Model format

Pack a positive exact dyadic with the direct guard-and-sticky constructor.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundCode (format : Format) (value : Numerics.Dyadic) : ℕ

Return the complete signed Posit encoding of an exact dyadic.

The positive magnitude is packed by the shared arbitrary-width guard/sticky kernel. Sign restoration is the standard whole-word two's complement, with exact zero kept unique.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.round (format : Format) (value : Numerics.Dyadic) : Model format

Round any exact dyadic through the direct positive packer and whole-word sign restoration.

Exact zero remains the unique unsigned zero. A negative nonzero result uses the Posit Standard (2022)'s whole-word two's-complement symmetry.