Direct one-word guard-and-sticky Posit rounding

The shared field-oriented posit rounder is instantiated with the UInt64 carrier. candidateCarrier maps every shared operation to a native-word primitive, and the generic kernel in GuardStickyCarrier keeps the candidate code in UInt64 during packing and rounding. Only steps with carrier-specific contracts live here: the exact minimum-positive comparison, the zero test, and sign restoration.

The kernel is selected by intermediate capacity, not by a named Posit width. Operations that continue in a two-limb intermediate import the separate WordLimb adapter at that boundary; this scalar rounder does not depend on or re-export a second implementation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.shiftLeft (value : UInt64) (shift : ℕ) : UInt64

Shift left in the one-word bitstream, returning zero at and beyond 64 positions.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.hasLowBits (value : UInt64) (width : ℕ) : Bool

Whether the discarded low-bit suffix is nonzero.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.isOdd (value : UInt64) : Bool

Parity of the packed candidate used to break a midpoint tie.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.candidateCarrier : GuardStickyCarrier.CandidateCarrier UInt64

One-word implementation of the shared candidate carrier.

This transparent record is consumed only by always-inlined helpers, leaving the generated hot path in primitive UInt64 operations. Shifts return zero at and beyond the word width instead of using the native modular shift amount; addition and the successor are the wrapping machine operations, which the shared rounder applies only to values it has bounded.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.isLessMinPositive (format : Format) (significand : UInt64) (exponent : ℤ) : Bool

Test a positive scalar target against the format's exact minimum-positive value.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundPositiveCodeWord (format : Format) (_heligible : NativeWord.Eligible format) (significand : UInt64) (exponent : ℤ) : UInt64

Round the nonnegative value significand * 2 ^ exponent to its complete unsigned code in one word.

Zero maps to code zero and targets below minPos to code one; every other target uses the shared normalized rounder at the UInt64 carrier.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundPositiveCode (format : Format) (heligible : NativeWord.Eligible format) (significand : UInt64) (exponent : ℤ) : ℕ

Natural-number view of positive native-field rounding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundCodeWord (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : UInt64

Round signed native dyadic fields and retain the complete code in one word.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundCodeNat (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : ℕ

Natural-number view of complete signed native-field rounding.