Certified configured standard MX conversion

The common destination capability is backed by the numerical nearest-even and shared-scale contracts. SAT is the default specified by this implementation of the recommendation in §6.3; the explicit context also permits FP8 OVF conversion.

theorem FloatLib.Floats.ExecFloat.OCP.MX.Standard.exactDecoder_eq_denote {profile : Formats.OCP.MX.Standard.Profile} (value : Standard profile) : ExactDecoder.decode value = Numerics.FormatSemantics.denote value.toCode

The configured source decoder agrees with the format's exact finite-block denotation.

theorem FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.implements_run {profile : Formats.OCP.MX.Standard.Profile} : Numerics.Quantization.Spec.Implements spec run

Configured conversion satisfies the numerical block contract for both explicit modes.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.quantizer {profile : Formats.OCP.MX.Standard.Profile} : Quantizer (Standard profile) (Vector Numerics.SignedRat 32)

The standard block destination quantizer has an explicit FP8 overflow policy context.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.defaultQuantizer {profile : Formats.OCP.MX.Standard.Profile} : DefaultQuantizer (Standard profile) (Vector Numerics.SignedRat 32)

Standard max-binade block conversion defaults to nearest-even with finite saturation.