feat: add `Float.toBits` and `Float.fromBits` This PR adds raw transmutation of floating-point numbers to and from `UInt64`. Floats and UInts share the same endianness across all supported platforms. The IEEE 754 standard precisely specifies the bit layout of floats. Note that `Float.toBits` is distinct from `Float.toUInt64`, which attempts to preserve the numeric value rather than the bitwise value.

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index eb7d66d..f8e384b 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean

@@ -47,6 +47,25 @@
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
+/--
+Raw transmutation from `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+
+/--
+Raw transmutation to `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float.toUInt64`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
+
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 90b4b84..a0b83c7 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h

@@ -2691,6 +2691,8 @@
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
+LEAN_EXPORT double lean_float_from_bits(uint64_t u);
+LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }
 static inline double lean_float_mul(double a, double b) { return a * b; }

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index b23a291..2634445 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp

@@ -1620,6 +1620,21 @@
     return r;
 }
 
+extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
+{
+    static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
+    double ret;
+    std::memcpy(&ret, &u, sizeof(double));
+    return ret;
+}
+
+extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
+{
+    uint64_t ret;
+    std::memcpy(&ret, &d, sizeof(double));
+    return ret;
+}
+
 // =======================================
 // Strings
 

diff --git a/tests/lean/run/floatBits.lean b/tests/lean/run/floatBits.lean
new file mode 100644
index 0000000..1904df8
--- /dev/null
+++ b/tests/lean/run/floatBits.lean

@@ -0,0 +1,13 @@
+def d : Float := 1.245
+
+/--
+info: 4608285800708723180
+-/
+#guard_msgs in
+#eval d.toBits
+
+/--
+info: true
+-/
+#guard_msgs in
+#eval Float.fromBits d.toBits == d