TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Representation theorems for configured OCP MX values #

Complete E8M0 bytes and joint MX block codes round-trip through their configured wrappers.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.E8M0.toCode_ofCode (code : Formats.OCP.MX.E8M0) :
(ofCode code).toCode = code

Unwrapping a freshly wrapped E8M0 code returns the original code.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofCode_toCode (value : E8M0) :
ofCode value.toCode = value

Rewrapping the code of an E8M0 value returns the original value.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.E8M0.ofNatBits_toNatBits (value : E8M0) :
ofNatBits value.toNatBits = value

Reconstructing an E8M0 scale from its complete byte preserves the value.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.E8M0.toNatBits_ofNatBits_of_lt (bits : ℕ) (bits_lt : bits < 2 ^ 8) :
(ofNatBits bits).toNatBits = bits

An in-range byte is unchanged by E8M0 encoding and decoding.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.toCode_ofCode {format : Formats.BinaryInterchange.FloatFormat} (code : Formats.OCP.MX.BlockCode format) :
(ofCode code).toCode = code

Unwrapping a freshly wrapped MX block returns the original code.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.ofCode_toCode {format : Formats.BinaryInterchange.FloatFormat} (value : Block format) :
ofCode value.toCode = value

Rewrapping the code of an MX block returns the original value.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.scale_ofComponents {format : Formats.BinaryInterchange.FloatFormat} (scaleValue : E8M0) (elementValues : Array (Formats.BinaryInterchange.Model format)) :
(ofComponents scaleValue elementValues).scale = scaleValue

ofComponents preserves the supplied shared scale.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.values_ofComponents {format : Formats.BinaryInterchange.FloatFormat} (scaleValue : E8M0) (elementValues : Array (Formats.BinaryInterchange.Model format)) :
(ofComponents scaleValue elementValues).values = elementValues

ofComponents preserves the supplied binary element words.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.OCP.MX.Block.values_ofElements {F : Type u} [Formats.BinaryInterchange.StaticByte.Family F] (scaleValue : E8M0) (elementValues : Array (ExecFloat F)) :
(ofElements scaleValue elementValues).values = Array.map (fun (value : ExecFloat F) => Formats.BinaryInterchange.StaticByte.toModel value) elementValues

Building from nominal elements stores exactly their corresponding proof-model values.