Certified configured standard MX conversion

The numerical nearest-even and shared-scale contracts back the common destination capability. SAT is the default in this implementation of the recommendation in §6.3, and the 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 in both overflow 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)

Standard block destination quantizer, with the FP8 overflow mode as its 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.