From ecbaeff24b2cb36d5c218f4ed6c92d6d55524048 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 15 Nov 2024 20:45:19 +0100
Subject: [PATCH] feat: add `Float.toBits` and `Float.fromBits` (#6094)

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.

closes #6071
---
 src/Init/Data/Float.lean      | 19 +++++++++++++++++++
 src/include/lean/lean.h       |  2 ++
 src/runtime/object.cpp        | 15 +++++++++++++++
 tests/lean/run/floatBits.lean | 13 +++++++++++++
 4 files changed, 49 insertions(+)
 create mode 100644 tests/lean/run/floatBits.lean

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index eb7d66df1d..f8e384b5e2 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -47,6 +47,25 @@ def Float.lt : Float → Float → Prop := fun a b =>
 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 25b0416500..fb093d76df 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -2691,6 +2691,8 @@ static inline size_t lean_float_to_usize(double a) {
     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 b23a29177d..2634445fed 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1620,6 +1620,21 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     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 0000000000..1904df8fd1
--- /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