Direct two-limb posit candidate decoding

The two-limb posit decoder reads encodings stored in native words. Regime scans stay in fixed-width words, and conversion to Nat is delayed until exact dyadic fields are constructed. Refinement theorems live in Decode.Proof.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.isZero (value : Numerics.FixedWord.UInt128) : Bool

Test whether both limbs of a two-word encoding are zero.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.bitAt (value : Numerics.FixedWord.UInt128) (index : ℕ) : Bool

Read one bit from a two-word value using least-significant-bit numbering.

Each branch delegates to the native-word reader, keeping the executable path to a shift, mask, and comparison instead of constructing a BitVec view.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.lowBits (value : Numerics.FixedWord.UInt128) (width : ℕ) : Numerics.FixedWord.UInt128

Retain the low width bits of a two-limb value.

The value is zero-extended outside its 128-bit carrier, so requesting at least 128 bits returns the complete value.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.complement (value : Numerics.FixedWord.UInt128) : Numerics.FixedWord.UInt128

Bitwise complement of both native limbs.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.countLeadingZeros (value : Numerics.FixedWord.UInt128) (width : ℕ) : ℕ

Count leading zeroes in the low width bits of a two-limb value.

The executable path masks once and uses the native logarithm of the high or low nonzero limb.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.countLeadingRun (value : Numerics.FixedWord.UInt128) (width : ℕ) (bit : Bool) : ℕ

Count a leading run in the low width bits of a two-limb value.

Zero runs use one masked native logarithm at every width. One runs use the complemented carrier through width 128; at wider widths the zero extension makes the leading bit zero immediately.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.withNonnegativeFields {α : Type} (format : Format) (code : Numerics.FixedWord.UInt128) (continuation : Numerics.FixedWord.UInt128 → ℤ → α) : α

Eliminate a nonnegative candidate into native significand and exact exponent fields.

The full significand remains in two machine limbs. Only the at-most-two-bit stored exponent is converted to Nat, matching the standardized posit descriptor without constructing an intermediate dyadic record.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.nonnegativeDyadicAt (format : Format) (code : Numerics.FixedWord.UInt128) : Numerics.Dyadic

Decode a nonnegative candidate into the shared exact-dyadic carrier.

This proof-facing view is defined through withNonnegativeFields; optimized arithmetic consumes the same decoder through its native continuation interface.

Direct decoding of complete stored words

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.isNegative (format : Format) (code : Numerics.FixedWord.UInt128) : Bool

Test the stored sign bit without reconstructing the mathematical code.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.magnitudeWord (format : Format) (code : Numerics.FixedWord.UInt128) : Numerics.FixedWord.UInt128

Unsigned magnitude of one complete two-limb posit encoding.

Negative posit codes use exact-width two's complement. Complementation and increment stay in the two native limbs; lowBits removes the carrier bits above narrower formats. The result crosses to Nat only once, when nonnegativeDyadicAt constructs the shared exact significand.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.decodeFinite (format : Format) (code : Numerics.FixedWord.UInt128) : Numerics.Dyadic

Decode a known finite, nonzero posit code through the two-limb field decoder.

The caller handles exceptional values. Sign extraction, magnitude extraction, and regime inspection use the two native limbs; the result stores the significand in the shared dyadic carrier.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.withDyadicFields {α : Type} (format : Format) (code : Numerics.FixedWord.UInt128) (onNaR : α) (continuation : Bool → Numerics.FixedWord.UInt128 → ℤ → α) : α

Eliminate a complete stored posit word into native dyadic fields.

NaR selects onNaR; zero and every finite value call the continuation. Sign extraction, two's-complement magnitude recovery, regime decoding, and significand construction all remain inside the two-limb carrier.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.withTwoDyadicFields {α : Type} (format : Format) (left right : Numerics.FixedWord.UInt128) (onNaR : α) (continuation : Bool → Numerics.FixedWord.UInt128 → ℤ → Bool → Numerics.FixedWord.UInt128 → ℤ → α) : α

Eliminate two stored posit words through one shared native-field interface.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.withThreeDyadicFields {α : Type} (format : Format) (left right addend : Numerics.FixedWord.UInt128) (onNaR : α) (continuation : Bool → Numerics.FixedWord.UInt128 → ℤ → Bool → Numerics.FixedWord.UInt128 → ℤ → Bool → Numerics.FixedWord.UInt128 → ℤ → α) : α

Eliminate three stored posit words through one shared native-field interface.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimb.toDyadic? (format : Format) (code : Numerics.FixedWord.UInt128) : Option Numerics.Dyadic

Total direct decoder for one stored two-limb posit word.

NaR becomes none, the unique zero becomes exact dyadic zero, and every ordinary word uses the fixed-limb decoder.