Configured posit conversions for fixed-width signed integers

These adapters preserve the Section 6.4 MSB-only sentinel through any lawful posit model codec. The integer width is independent of the posit width. Integer-to-posit conversion rounds the exact signed value once using Section 4.1; posit-to-integer conversion uses nearest integer with ties to even, checking the signed range after rounding.

The signed minimum shares the sentinel word. These explicit adapters therefore differ from generic numerical conversion through an ordinary FixedInt decoder, which treats that word as a finite integer.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.ofFixedInt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (value : Numerics.Representations.FixedInt width) (hwidth : 0 < width := by decide) : ExecFloat (Formats.Posit.Configured.Family format code plan)

Convert a signed integer to a configured posit, reserving the MSB-only input for NaR.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.toFixedInt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width := by decide) : Numerics.Representations.FixedInt width

Convert a configured posit to a signed integer with nearest-even rounding. NaR and a rounded value outside the signed range produce the MSB-only sentinel.