Configured posit conversion proofs

The conversion relation specifies finite results through real posit rounding and the complete decoded model. Its implementation proof uses the rational-to-real rounding bridge and codec inverse laws. The exponent size is fixed at two bits by the Posit Standard (2022), so width is the only descriptor parameter.

Conversion to an equally wide or wider descriptor appends zero bits to the source word. The configured results follow from exact model widening and the codec inverse laws. Complete decoding and default conversion preserve zero and NaR as well as finite values.

theorem FloatLib.Floats.ExecFloat.Posit.decode_ofModel_widen {source target : Formats.Posit.Format} {sourcePlan : Formats.Posit.Configured.StoragePlan source} {targetPlan : Formats.Posit.Configured.StoragePlan target} {sourceCode targetCode : Type} [ModelCodec sourcePlan (Formats.Posit.Model source) sourceCode] [ModelCodec targetPlan (Formats.Posit.Model target) targetCode] (hw : source.bits ≤ target.bits) (value : ExecFloat (Formats.Posit.Configured.Family source sourceCode sourcePlan)) : decode (ofModel (Formats.Posit.Model.ofNatBits (toNatBits value * 2 ^ (target.bits - source.bits)))) = decode value

Appending zero bits preserves the complete configured observation, including zero and NaR.

def FloatLib.Floats.ExecFloat.Posit.Conversion.spec {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : Numerics.Quantization.Spec Context (Numerics.NumericalValue ℚ) (ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan)))

Finite conversion follows real posit rounding, with exact status for the delivered model.

The real rounder uses the standard appended-bit boundary, minPos underflow, and maxPos saturation. Model equality retains the complete word. Infinity and exceptional observations obey their explicit policies. This proof-facing relation needs no real-number evaluation at runtime.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_finite {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (exact : ℚ) : run context (Numerics.NumericalValue.finite exact) = quantizeFinite exact

Finite observations use the exact arbitrary-width posit rounder.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_infinity {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (negative : Bool) : run context (Numerics.NumericalValue.infinity negative) = quantizeInfinity context negative

Infinity observations are handled only by the explicit posit infinity policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_exceptional {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (exceptional : Numerics.ExceptionalValue) : run context (Numerics.NumericalValue.exceptional exceptional) = quantizeExceptional context exceptional

Exceptional observations are handled only by the explicit posit exceptional policy.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.implements_run {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : spec.Implements run

The real rounding bridge and the codec inverse law establish the finite contract.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.spec_iff_eq_run {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (context : Context) (input : Numerics.NumericalValue ℚ) (outcome : ConversionOutcome (ExecFloat (Formats.Posit.Configured.Family format code plan))) : spec context input outcome ↔ outcome = run context input

Real rounding plus the codec law determines the complete original outcome and status.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.exactDecoder_run {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : ExactDecoder.run value = decode value

The installed exact decoder is the public configured posit decoder.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_default_infinity {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (negative : Bool) : run Context.default (Numerics.NumericalValue.infinity negative) = ConversionOutcome.success nar { mappedSpecial := true }

Default conversion maps either infinity to NaR, as required by Posit Standard (2022), §6.5.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_default_exceptional {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (exceptional : Numerics.ExceptionalValue) : run Context.default (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.success nar { mappedSpecial := true }

Default conversion maps exceptional observations to NaR, including IEEE NaNs and posit NaR.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.quantizeFinite_widen {source target : Formats.Posit.Format} {sourcePlan : Formats.Posit.Configured.StoragePlan source} {targetPlan : Formats.Posit.Configured.StoragePlan target} {sourceCode targetCode : Type} [ModelCodec sourcePlan (Formats.Posit.Model source) sourceCode] [ModelCodec targetPlan (Formats.Posit.Model target) targetCode] (hw : source.bits ≤ target.bits) (value : ExecFloat (Formats.Posit.Configured.Family source sourceCode sourcePlan)) (exact : ℚ) (hfinite : decode value = Numerics.NumericalValue.finite exact) : (quantizeFinite exact).value? = some (ofModel (Formats.Posit.Model.ofNatBits (toNatBits value * 2 ^ (target.bits - source.bits))))

Quantizing a decoded finite source into a wider codec appends exactly the additional zero bits. The statement concerns the successful value, not the conversion status.

theorem FloatLib.Floats.ExecFloat.Posit.Conversion.run_default_widen {source target : Formats.Posit.Format} {sourcePlan : Formats.Posit.Configured.StoragePlan source} {targetPlan : Formats.Posit.Configured.StoragePlan target} {sourceCode targetCode : Type} [ModelCodec sourcePlan (Formats.Posit.Model source) sourceCode] [ModelCodec targetPlan (Formats.Posit.Model target) targetCode] (hw : source.bits ≤ target.bits) (value : ExecFloat (Formats.Posit.Configured.Family source sourceCode sourcePlan)) : (run Context.default (decode value)).value? = some (ofModel (Formats.Posit.Model.ofNatBits (toNatBits value * 2 ^ (target.bits - source.bits))))

Default conversion into a wider codec returns the source word with appended zero bits. This includes the unique zero and NaR words; the default exceptional-value policy preserves NaR.