TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.Configured.Conversion.Proof

Proof contracts for configured OCP MX decoding #

OCP MX values reach generic algorithms through the shared ExactDecoder capability. The bridge lemmas below show that decoding an E8M0 scale or a shared-scale block is exactly the corresponding numerical-system denotation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.E8M0.Conversion.exactDecoder_run (value : E8M0) :
ExactDecoder.run value = Formats.OCP.MX.E8M0.numericalSystem.denote value.toCode

The installed decoder is the E8M0 numerical-system denotation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.Conversion.exactDecoder_run {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) :
ExactDecoder.run value = (Formats.OCP.MX.blockSystem format).denote value.toCode

The installed block decoder is the joint block denotation.