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.

Intermediate capacity selects the kernel, and no named Posit width is special. Operations that continue in a two-limb intermediate import the WordLimb adapter at that boundary, so this scalar rounder neither depends on nor re-exports 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, where the native shift would reduce the amount modulo 64. 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, a power of two, by comparing the exponent of its leading bit.

@[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.