Configured binary-interchange conversion proofs

Configured conversion inherits the descriptor's default IEEE nearest-value contract and preserves the complete outcome for every context.

It is the final transport layer between descriptor-level conversion semantics and the public packed carrier. Storage selection is intentionally absent from the statement: any configured backend must decode to the same converted value and status, so changing from a native word to arbitrary-width storage cannot change the numerical contract.

@[simp]

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

Finite observations are handled by the configured binary finite quantizer.

@[simp]

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

Infinity observations are handled only by the explicit infinity policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.run_exceptional {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.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 exceptional policy.

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

The configured carrier inherits the descriptor's nearest-value and complete-outcome clauses.

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

The semantic contract retains the exact configured word and every status field.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.nearestFinite_of_spec {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (context : Context) (exact : Numerics.SignedRat) (rounded : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (indicators : ConversionStatus) (hpolicy : context.quantization = Numerics.QuantizationPolicy.nearestEven) (hformat : format.isIEEE = true) (h : spec context (Numerics.NumericalValue.finite exact) (ConversionOutcome.success rounded indicators)) : NearestFinite exact.value (toModel rounded)

A successful default IEEE conversion satisfies the nearest-value predicate after decoding.

@[simp]

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

The installed exact decoder is the public signed-rational decoder.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.run_default_finite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (exact : Numerics.SignedRat) : run Context.default (Numerics.NumericalValue.finite exact) = ConversionOutcome.success (ofModel (Formats.BinaryInterchange.Model.roundRat format exact.negative exact.value.num.natAbs exact.value.den)) (finiteStatus Context.default exact.value (Formats.BinaryInterchange.Model.roundRat format exact.negative exact.value.num.natAbs exact.value.den))

A default-context finite conversion is the canonical nearest-even rational rounder applied to the sign bit and magnitude of the signed rational.

The delivered value is Model.roundRat. For conventional IEEE destinations and finite results, Model.toReal_roundRatScaled_eq_roundAt relates that rounder to nearest-even rounding over ℝ.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.run_default_negZero_value? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : (run Context.default (Numerics.NumericalValue.finite Numerics.SignedRat.negZero)).value? = some (zero true)

Converting an exact negative zero preserves its sign when the destination supports negative zero.

For an encoding with one unsigned zero, zero true is that encoding's positive zero, so the statement also covers FNUZ destinations.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.run_infinity_reject {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (negative : Bool) : run { infinity := InfinityPolicy.reject } (Numerics.NumericalValue.infinity negative) = ConversionOutcome.failure (ConversionFailure.infinity InputPosition.source negative)

Rejecting infinity produces the corresponding explicit failure.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.run_exceptional_reject {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (exceptional : Numerics.ExceptionalValue) : run { exceptional := ExceptionalPolicy.reject } (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.failure (ConversionFailure.exceptional InputPosition.source exceptional)

Rejecting an exceptional observation preserves its complete common classification.