TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Narrow.Base.Proof

Correctness of native binary32 storage operations #

The UInt32 storage conversions are mutual inverses, and native sign-bit negation agrees with the generic binary32 model. Runtime clients can import Base.Runtime without these proofs.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.negate_eq (x : Value) :
negate x = neg x

Word negation is the model sign flip.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_toUInt32 (x : Value) :
ofUInt32 (toUInt32 x) = x

Repacking the stored word returns the value.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toUInt32_ofUInt32 (bits : UInt32) :
toUInt32 (ofUInt32 bits) = bits

Unpacking a freshly packed word returns the word.