Lean native floating-point interoperability

Explicit conversions connect every configured binary format to Lean's runtime Float32 and Float types: toFloat, ofFloat, toFloat32, and ofFloat32 round once in a mode option when the two formats differ, and move the interchange word unchanged between Binary64 and Float and between Binary32 and Float32. Lean names its IEEE binary64 runtime type Float, and there is no core type named Float64.

At the conversion boundary:

• ofBits32, toBits32, ofBits64, and toBits64 transport every interchange word unchanged inside FloatLib.
• The native conversions use Lean's public Float32.ofBits, Float32.toBits, Float.ofBits, and Float.toBits operations.
• Lean's logical model of Float32.ofBits and Float.ofBits canonicalizes NaN payloads, and so do the compiled runtime primitives (a compiled (Float32.ofBits 0x7f800001).toBits is 0x7fc00000). Payload-preserving transport therefore stays in the ofBits32/toBits32 and ofBits64/toBits64 APIs.

The conversions themselves do not choose an arithmetic backend. Configured binary32 and binary64 arithmetic uses proved software kernels by default. Applications may opt into Configured.NativeFPU.Unchecked for guarded host arithmetic, but those functions are outside the proof-carrying planner and depend on the compiler and host runtime.

The companion Native.Integer module connects integer conversion to FloatLib's rounding specifications. Native.AddSub proves agreement for finite operands, and Native.Sqrt covers every input after NaN canonicalization. Import FloatLib.Floats.Formats.IEEE754 or FloatLib to include these proofs alongside the conversions.

References

• IEEE 754-2019, Sections 3.4 and 3.6, defines binary interchange encodings.
• Lean's Init.Data.Float.Float32 and Init.Data.Float.Float modules define the runtime types, their logical models, and the model-based conversion boundary used here.

Exact encoded-word transport

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofBits32 (bits : UInt32) : Binary32

Construct configured IEEE binary32 from an exact 32-bit interchange word.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toBits32 (value : Binary32) : UInt32

Extract the exact 32-bit interchange word from configured IEEE binary32.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toBits32_ofBits32 (bits : UInt32) : toBits32 (ofBits32 bits) = bits

Extracting the word just used to construct binary32 returns that word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofBits32_toBits32 (value : Binary32) : ofBits32 (toBits32 value) = value

Reconstructing binary32 from its exact interchange word returns the original value.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofBits64 (bits : UInt64) : Binary64

Construct configured IEEE binary64 from an exact 64-bit interchange word.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toBits64 (value : Binary64) : UInt64

Extract the exact 64-bit interchange word from configured IEEE binary64.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toBits64_ofBits64 (bits : UInt64) : toBits64 (ofBits64 bits) = bits

Extracting the word just used to construct binary64 returns that word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofBits64_toBits64 (value : Binary64) : ofBits64 (toBits64 value) = value

Reconstructing binary64 from its exact interchange word returns the original value.

Lean runtime types

The general paths of the native conversions: a value of another format crosses through Model.cast to or from the native word. They call the compiled status kernel of the cast and keep its value, which is the value of Model.cast (Model.value_cast), so the conversions of every format share the code of the cast library instead of inlining a copy of it.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.Internal.Native.cast (src dst : Formats.BinaryInterchange.FloatFormat) (value : Formats.BinaryInterchange.Model src) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : Formats.BinaryInterchange.Model dst

The value of Model.cast src dst value (mode := mode).

def FloatLib.Floats.ExecFloat.Binary.Internal.Native.toWord64 {format : Formats.BinaryInterchange.FloatFormat} (value : Formats.BinaryInterchange.Model format) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : UInt64

The binary64 interchange word of value cast to binary64 in mode.

def FloatLib.Floats.ExecFloat.Binary.Internal.Native.toWord32 {format : Formats.BinaryInterchange.FloatFormat} (value : Formats.BinaryInterchange.Model format) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : UInt32

The binary32 interchange word of value cast to binary32 in mode.

def FloatLib.Floats.ExecFloat.Binary.Internal.Native.ofWord64 (format : Formats.BinaryInterchange.FloatFormat) (bits : UInt64) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : Formats.BinaryInterchange.Model format

The binary64 interchange word bits cast to format in mode.

def FloatLib.Floats.ExecFloat.Binary.Internal.Native.ofWord32 (format : Formats.BinaryInterchange.FloatFormat) (bits : UInt32) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : Formats.BinaryInterchange.Model format

The binary32 interchange word bits cast to format in mode.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toFloat {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Float

Convert a configured value to Lean's native binary64 Float, rounding once in mode (nearest-even by default) when the format has values that binary64 cannot hold.

A binary64 value crosses as its interchange word, through Lean's public Float.ofBits. Every other format is cast to binary64 by Model.cast first, which is exact for binary32, binary16, and bfloat16. Both the logical model of Float.ofBits and its compiled primitive canonicalize a noncanonical NaN payload, so a NaN with a payload does not round-trip through this function. Use toBits64 for payload-preserving serialization inside FloatLib.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofFloat {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} (value : Float) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan

Convert Lean's native binary64 Float to a configured value, rounding once in mode (nearest-even by default) when the destination cannot hold every binary64 value. Lean calls its 64-bit IEEE runtime type Float.

The expected type selects the destination, as in (ExecFloat.Binary.ofFloat 0.1 : BFloat16). A binary64 destination receives the word of Lean's public Float.toBits, and every other destination receives Model.cast of that word.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toFloat32 {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Float32

Convert a configured value to Lean's native Float32, rounding once in mode (nearest-even by default) when the format has values that binary32 cannot hold.

A binary32 value crosses as its interchange word, through Lean's public Float32.ofBits. Every other format is cast to binary32 by Model.cast first, which is exact for binary16 and bfloat16. Both the logical model of Float32.ofBits and its compiled primitive canonicalize a noncanonical NaN payload, so a NaN with a payload does not round-trip through this function. Use toBits32 for payload-preserving serialization inside FloatLib.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofFloat32 {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} (value : Float32) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan

Convert Lean's native binary32 Float32 to a configured value, rounding once in mode (nearest-even by default) when the destination cannot hold every binary32 value.

The expected type selects the destination. A binary32 destination receives the word of Lean's public Float32.toBits, whose logical model and compiled primitive agree on every finite value and infinity. A NaN reaches this function already canonicalized by whichever operation produced it. Every other destination receives Model.cast of that word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toBits32_ofFloat32 (value : Float32) : (ofFloat32 value).toBits32 = value.toBits

Converting a native Float32 keeps Lean's public interchange word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat32 (value : Binary32) : (toFloat32 value).toModel = Float32.Model.ofBits (toBits32 value)

The logical model of a converted binary32 value is constructed from the same word.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_toFloat32 (value : Binary32) : ofFloat32 (toFloat32 value) = ofBits32 (Formats.BinaryInterchange.Model.NativeBinary32.toUInt32 (Formats.BinaryInterchange.Model.canonicalizeModel (Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32 (toBits32 value))))

A round trip of configured binary32 through Float32 is the canonical-NaN normalization of the generic Lean-model bridge.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toBits64_ofFloat (value : Float) : (ofFloat value).toBits64 = value.toBits

Converting a native Float keeps Lean's public interchange word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat (value : Binary64) : (toFloat value).toModel = Float.Model.ofBits (toBits64 value)

The logical model of a converted binary64 value is constructed from the same word.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_toFloat (value : Binary64) : ofFloat (toFloat value) = ofBits64 (Formats.BinaryInterchange.Model.NativeBinary64.toUInt64 (Formats.BinaryInterchange.Model.canonicalizeModel (Formats.BinaryInterchange.Model.NativeBinary64.ofUInt64 (toBits64 value))))

A round trip of configured binary64 through Float is the canonical-NaN normalization of the generic Lean-model bridge.

Exact source integration

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.nativeFloat32ExactDecoder : ExactDecoder Float32 Numerics.SignedRat

Lean's native binary32 participates as an exact signed-rational conversion source.

The decoder crosses the native bit boundary and then uses the configured binary32 decoder, so -0.0 decodes to SignedRat.negZero. The caller names the destination through ExecFloat.convert, and native types do not join an implicit promotion lattice.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.nativeFloatExactDecoder : ExactDecoder Float Numerics.SignedRat

Lean's native binary64 participates as an exact signed-rational conversion source.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.nativeFloat32ExactDecoder_run (value : Float32) : ExactDecoder.run value = (ofFloat32 value).decode

Decoding a native Float32 source decodes its binary32 interchange value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.nativeFloatExactDecoder_run (value : Float) : ExactDecoder.run value = (ofFloat value).decode

Decoding a native Float source decodes its binary64 interchange value.