Shared fixed-carrier guard-and-sticky Posit rounding

One-word and two-limb posit kernels round the same normalized exponent/fraction stream. They differ only in the carrier that holds the significand and the packed code, so everything from tail inspection through candidate packing to the round-to-nearest-even decision is written once here and instantiated by each carrier.

• TailCarrier records the two operations that reading the discarded tail needs: one bit, and whether a low-bit suffix is nonzero. tailBit and tailHasNonzeroAfter are the readers.
• CandidateCarrier extends it with the arithmetic that packing needs: shifts, an addition that callers keep from overflowing, a low-ones mask, the successor, the parity test, and the leading bit. fractionPrefix, tailPrefix, lowerCandidateFromFields, roundInterior, and roundNormalizedPositive form the shared kernel.

Both records are passed explicitly to always-inlined functions. The UInt64 and UInt128 instances are transparent constants, allowing specialization to their primitive operations. The sibling proof module states the natural-number meaning of every operation (LawfulTailCarrier, LawfulCandidateCarrier) and proves the shared kernel against the arbitrary-width rounder DirectDyadicPacking.roundPositiveCode.

The two exponent bits are always stored in UInt64, so this module reads them through neutral fixed-word primitives and depends on neither posit storage backend. Underflow detection, the zero test, and sign restoration stay in the specialized kernels: they use carrier-specific comparison and complement primitives with their own contracts.

structure FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.TailCarrier (α : Type) : Type

Operations needed to inspect the finite tail of a packed significand.

The structure contains executable data only. LawfulTailCarrier in the sibling proof module states how these operations represent natural-number bit streams.

• bitAt : α → ℕ → Bool

  Read one bit using least-significant-bit numbering.

• hasLowBits : α → ℕ → Bool

  Test whether any of the low width bits is set.

structure FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.CandidateCarrier (α : Type) extends FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.TailCarrier α : Type

Operations needed to pack and round a positive normalized posit candidate inside one fixed-width carrier.

Every operation is total. Its natural-number meaning, stated by LawfulCandidateCarrier, is guaranteed only under the bounds the shared rounder establishes: add and increment are exact when the mathematical result fits the carrier, shiftLeft when the shifted value fits, lowOnes below the carrier width, and fractionBelow on a significand whose leading one sits at the given index. The structure contains executable data only.

• bitAt : α → ℕ → Bool
• hasLowBits : α → ℕ → Bool
• ofWord : UInt64 → α

  Embed a machine word; used for the two-bit exponent field and the constants zero and one.

• shiftLeft : α → ℕ → α

  Shift left, returning zero once the shift reaches the carrier width.

• shiftRight : α → ℕ → α

  Shift right, returning zero once the shift reaches the carrier width.

• fractionBelow : α → ℕ → α

  Remove the leading one, at the given bit index, from a normalized significand.

• add : α → α → α

  Addition; exact whenever the mathematical sum fits the carrier.

• lowOnes : ℕ → α

  A mask whose low width bits are one.

• increment : α → α

  Successor; exact whenever it fits the carrier.

• isOdd : α → Bool

  Whether the least significant bit is set.

• log2 : α → ℕ

  Index of the leading one of a nonzero value.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailBit {α : Type} (carrier : TailCarrier α) (exponentField : UInt64) (significand : α) (leading index : ℕ) : Bool

Read one bit of the two-bit exponent followed by the finite fraction.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailHasNonzeroAfter {α : Type} (carrier : TailCarrier α) (exponentField : UInt64) (significand : α) (leading consumed : ℕ) : Bool

Test whether the exact exponent/fraction suffix after consumed contains a one.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.fractionPrefix {α : Type} (carrier : CandidateCarrier α) (significand : α) (leading count : ℕ) : α

First count normalized fraction bits after the leading one at index leading.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailPrefix {α : Type} (carrier : CandidateCarrier α) (exponentField : UInt64) (significand : α) (leading count : ℕ) : α

Prefix of the standard two-bit exponent followed by the normalized fraction.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.lowerCandidateFromFields {α : Type} (carrier : CandidateCarrier α) (format : Format) (regime : ℤ) (exponentField : UInt64) (significand : α) (leading : ℕ) : α

Pack normalized regime, exponent, and significand fields into the unsigned lower posit candidate.

Regimes that consume the whole payload saturate to maxPos or truncate to zero. Interior regimes place the run, its terminator, and the retained tail prefix.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.roundInterior {α : Type} (carrier : CandidateCarrier α) (format : Format) (regime : ℤ) (exponentField : UInt64) (significand : α) (leading regimeFieldBits : ℕ) : α

Round an interior normalized target to nearest even from its retained prefix, guard bit, and sticky suffix.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.roundNormalizedPositive {α : Type} (carrier : CandidateCarrier α) (format : Format) (significand : α) (exponent : ℤ) : α

Round the nonzero positive value significand * 2 ^ exponent, known not to underflow, to its unsigned posit code.

Regimes that consume the payload map directly to maxPos or minPos; interior values use the field-oriented guard/sticky rule. For a lawful carrier whose capacity is strictly greater than the format's payload width, the result is the carrier image of DirectDyadicPacking.roundPositiveCode (roundNormalizedPositive_toNat_eq_direct).