Missing inverse lemmas for Float.ofBits / Float.toBits

[kjsdesigns]

Summary

Float.ofBits and Float.toBits are declared as @[extern] opaque primitives in Init.Data.Float but have no accompanying lemmas establishing their inverse relationship:

@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 → Float
@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64

There are currently zero theorems about these functions in the standard library.

Requested additions

axiom Float.ofBits_toBits (f : Float) : Float.ofBits f.toBits = f
axiom Float.toBits_ofBits (u : UInt64) : (Float.ofBits u).toBits = u

Both hold by the C implementation (lean_float_of_bits / lean_float_to_bits are memcpy-based reinterpret casts between double and uint64_t, which are exact inverses on all IEEE 754 platforms).

Motivating use case

I maintain a production Lean 4 codebase that uses a typed data model with a positional JSON codec. The codec serializes Float values via their exact IEEE-754 bit pattern (Float.toBits → UInt64 → Nat → Json.num) and decodes the reverse path. Proving the round-trip property (fromPositionalJson dm (toPositionalJson v) = .ok v) requires knowing that Float.ofBits f.toBits = f.

Without upstream support, I had to introduce a project-local axiom:

-- lean/Spec/Trusted/FloatBits.lean
axiom float_ofBits_toBits (f : Float) : Float.ofBits f.toBits = f

This is the only axiom in the project (714+ sorry-free theorems otherwise). Having this in the standard library would eliminate the need for downstream projects to each introduce their own trusted axiom for the same fact.

Implementation question

Would the Lean team prefer these as:

1. axiom declarations in Init.Data.Float (simplest, matches the opaque status of the functions), or
2. Some other mechanism (e.g. native_decide-backed, or @[implemented_by])?

Happy to open a PR once there's alignment on the approach.

[Rob23oba]

I'll just mention that they are not exact inverses but

(ofBits x).toBits = if (ofBits x).isNaN then 0x7ff8_0000_0000_0000 else x

lean4/src/runtime/object.cpp

Lines 1870 to 1877 in 41ab492

	extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
	{
	uint64_t ret;
	if (isnan(d))
	d = std::numeric_limits<double>::quiet_NaN();
	std::memcpy(&ret, &d, sizeof(double));
	return ret;
	}

This is just to say that this may not be as obvious as it seems. Otherwise, I can't speak on behalf of the FRO, but I don't think we would add a new axiom to the Lean codebase for something this specific. We are already very strict regarding safe axioms, the only ones in the codebase are propext, Quot.sound, Classical.choice, sorryAx and Lean.trustCompiler, Lean.ofReduceNat, Lean.ofReduceBool, the last three of which may be deprecated soon.

That being said, I don't see a problem with asserting this as an axiom in your project. In contrast to Float.toBits_ofBits, Float.ofBits_toBits is true (note that we consider all NaNs equal even if this is not stated anywhere).