Lean native floating-point interoperability

Explicit conversions connect ExecFloat.Binary (exponentBits := 8) (fractionBits := 23) and ExecFloat.Binary (exponentBits := 11) (fractionBits := 52) to Lean's runtime Float32 and Float types. Lean names its IEEE binary64 runtime type Float; there is no separate core type named Float64.

The conversion boundary is explicit:

• ofBits32, toBits32, ofBits64, and toBits64 transport every interchange word exactly 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 the compiled runtime primitives do the same (a compiled (Float32.ofBits 0x7f800001).toBits is 0x7fc00000); exact 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 call Configured.NativeFPU.Unchecked explicitly for guarded host arithmetic, but those functions are outside the proof-carrying planner and depend on the compiler and host runtime.

Lean 4.34 exposes more definitions in its logical float model. 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) : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4

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

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toBits32 (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4) : UInt32

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

@[simp]

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

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofBits32_toBits32 (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4) : ofBits32 value.toBits32 = value

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

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofBits64 (bits : UInt64) : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4

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

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toBits64 (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4) : UInt64

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

@[simp]

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

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofBits64_toBits64 (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4) : ofBits64 value.toBits64 = value

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

Lean runtime types

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofFloat32 (value : Float32) : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4

Convert Lean's native binary32 value to configured ExecFloat binary32.

The definition uses Lean's public interchange conversion Float32.toBits. Its logical model and the compiled primitive agree on every finite value and infinity; a NaN reaches this function already canonicalized by whichever operation produced it.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toFloat32 (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4) : Float32

Convert configured ExecFloat binary32 to Lean's native Float32.

Both the logical model of Float32.ofBits and its compiled primitive canonicalize a noncanonical NaN payload, so a configured NaN with a payload does not round-trip through this function. Use toBits32 for payload-preserving serialization inside FloatLib.

@[simp]

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

Native binary32 conversion exposes exactly Lean's public interchange word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat32 (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4) : value.toFloat32.toModel = Float32.Model.ofBits value.toBits32

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

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_toFloat32 (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ofBits32._proof_1 ofBits32._proof_2 ofBits32._proof_3 ofBits32._proof_4) : ofFloat32 value.toFloat32 = ofBits32 (Formats.BinaryInterchange.Model.NativeBinary32.toUInt32 (Formats.BinaryInterchange.Model.canonicalizeModel (Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32 value.toBits32)))

Converting configured binary32 through Lean's native model performs exactly the canonical-NaN normalization already defined by the generic Lean-model bridge.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.ofFloat (value : Float) : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4

Convert Lean's native binary64 Float to configured ExecFloat binary64.

Lean calls its 64-bit IEEE runtime type Float.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toFloat (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4) : Float

Convert configured ExecFloat binary64 to Lean's native binary64 Float.

Both the logical model of Float.ofBits and its compiled primitive canonicalize a noncanonical NaN payload, so a configured NaN with a payload does not round-trip through this function. Use toBits64 for payload-preserving serialization inside FloatLib.

@[simp]

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

Native binary64 conversion exposes exactly Lean's public interchange word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4) : value.toFloat.toModel = Float.Model.ofBits value.toBits64

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

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_toFloat (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) ofBits64._proof_1 ofBits64._proof_2 ofBits64._proof_3 ofBits64._proof_4) : ofFloat value.toFloat = ofBits64 (Formats.BinaryInterchange.Model.NativeBinary64.toUInt64 (Formats.BinaryInterchange.Model.canonicalizeModel (Formats.BinaryInterchange.Model.NativeBinary64.ofUInt64 value.toBits64)))

Converting configured binary64 through Lean's native model performs exactly the canonical-NaN normalization already defined by 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 already documented native bit boundary and then uses the configured binary32 decoder, so -0.0 decodes to SignedRat.negZero. Destination selection remains explicit through ExecFloat.convert; native types are not placed in 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 = decode (ofFloat32 value)

The native binary32 source capability uses exact interchange decoding.

@[simp]

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

The native binary64 source capability uses exact interchange decoding.