Primitive carriers for fixed-word posit kernels

The four built-in posit carriers differ only in how they widen to and narrow from UInt64. Carrier records that relationship once. It is passed only to always-inlined helpers; the public raw kernels remain monomorphic so their native calling conventions are unchanged.

structure FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.Carrier (α : Type) (capacity : ℕ) : Type

Arithmetic view of one primitive unsigned carrier.

• toNat : α → ℕ

  Observe the encoded natural number.

• toUInt64 : α → UInt64

  Zero-extend the carrier to the packed arithmetic word.

• narrow : UInt64 → α

  Narrow a packed arithmetic result back to the carrier.

• ofNat : ℕ → α

  Construct the carrier from a natural number.

• toNat_injective : Function.Injective self.toNat

  Natural-number observation determines the primitive carrier.

• toNat_toUInt64 (value : α) : (self.toUInt64 value).toNat = self.toNat value

  Widening preserves the represented natural number.

• toNat_narrow (word : UInt64) : self.toNat (self.narrow word) = word.toNat % 2 ^ capacity

  Narrowing is reduction modulo the carrier capacity.

• toNat_ofNat (value : ℕ) : self.toNat (self.ofNat value) = value % 2 ^ capacity

  Natural construction is reduction modulo the carrier capacity.

• capacity_le : capacity ≤ 64

  Fixed-word carriers fit in the packed UInt64 arithmetic word.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.uint8Carrier : Carrier UInt8 8

UInt8 as a packed posit carrier.

This is an abbreviation so monomorphic raw kernels reduce its projections at compile time instead of loading conversion closures from a runtime record.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.uint16Carrier : Carrier UInt16 16

UInt16 as a packed posit carrier.

Keeping the carrier transparent preserves the native UInt16 calling convention after the generic fixed-word kernel specializes.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.uint32Carrier : Carrier UInt32 32

UInt32 as a packed posit carrier.

Keeping the carrier transparent lets widening and narrowing compile to primitive operations.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.uint64Carrier : Carrier UInt64 64

UInt64 as the full packed arithmetic carrier.

Keeping the carrier transparent reduces both conversion projections to id.