build: f128 on Berkeley SoftFloat for macOS (exploration)

.github/workflows/platforms.yml

@@ -34,7 +34,7 @@ concurrency:
 
 jobs:
   ubuntu:
-    name: Ubuntu ${{ matrix.release }}${{ matrix.cc == 'clang' && ', clang' || '' }}
+    name: Ubuntu ${{ matrix.release }}${{ matrix.cc == 'clang' && ', clang' || '' }}${{ matrix.softfloat && ', SoftFloat' || '' }}
     runs-on: ubuntu-24.04
     container: ubuntu:${{ matrix.release }}
     timeout-minutes: 45
@@ -48,12 +48,21 @@ jobs:
         #   26.04 GCC 15, CMake 4.2, GMP 6.3.0
         release: ['22.04', '24.04', '26.04']
         cc: [gcc]
+        # An axis of its own, so the SoftFloat entry below is added as a new
+        # job rather than merged into the plain 24.04 one.
+        softfloat: [false]
         include:
           - release: '24.04'
             cc: clang
+          # The macOS f128 implementation, on a platform where it can be
+          # compared with native __float128 (same suites, same expectations).
+          - release: '24.04'
+            cc: gcc
+            softfloat: true
     env:
       DEBIAN_FRONTEND: noninteractive
-      PLATFORM: Ubuntu ${{ matrix.release }}, ${{ matrix.cc }}
+      PLATFORM: Ubuntu ${{ matrix.release }}, ${{ matrix.cc }}${{ matrix.softfloat && ', SoftFloat f128' || '' }}
+      MAKE_EXTRA: ${{ matrix.softfloat && 'SOFTFLOAT=1' || '' }}
     steps:
       - name: Install dependencies
         run: |
@@ -75,14 +84,18 @@ jobs:
       - name: Build MoToBuddy
         run: make init
 
+      - name: Build SoftFloat
+        if: matrix.softfloat
+        run: make init-softfloat
+
       - name: Probe
         run: bash .github/scripts/platform-probe.sh
 
       - name: Upload logs
         if: always()
         uses: actions/upload-artifact@v7
         with:
-          name: probe-logs-ubuntu-${{ matrix.release }}-${{ matrix.cc }}
+          name: probe-logs-ubuntu-${{ matrix.release }}-${{ matrix.cc }}${{ matrix.softfloat && '-softfloat' || '' }}
           path: probe-logs/
           if-no-files-found: ignore
 
@@ -91,10 +104,9 @@ jobs:
     runs-on: macos-15
     timeout-minutes: 45
     env:
-      PLATFORM: macOS 15 arm64, Apple clang
-      # arm64 macOS has no binary128 type (neither __float128 nor a 128-bit
-      # long double).
-      EXPECT_FAIL: build-f128
+      # f128 on SoftFloat (SOFTFLOAT=1 is the default on macOS): arm64 macOS
+      # has no binary128 type.
+      PLATFORM: macOS 15 arm64, Apple clang, SoftFloat f128
     steps:
       - uses: actions/checkout@v7
 
@@ -109,8 +121,10 @@ jobs:
           echo "CPATH=${p}/include" >> "${GITHUB_ENV}"
           echo "LIBRARY_PATH=${p}/lib" >> "${GITHUB_ENV}"
 
-      - name: Build MoToBuddy
-        run: make init
+      - name: Build MoToBuddy and SoftFloat
+        run: |
+          make init
+          make init-softfloat
 
       - name: Probe
         run: bash .github/scripts/platform-probe.sh

Makefile

@@ -84,6 +84,18 @@ ifeq ($(MEDUSA_DEBUG), 1)
   OBJ_TAG := $(OBJ_TAG)-dbglog
 endif
 
+# f128 on Berkeley SoftFloat (src/.../leaf_f128_soft.h), for targets with no
+# binary128 type. On by default only on macOS, where it needs
+# `make init-softfloat` once; Linux builds neither need nor use it.
+ifeq ($(shell uname -s),Darwin)
+  SOFTFLOAT ?= 1
+else
+  SOFTFLOAT ?= 0
+endif
+ifeq ($(SOFTFLOAT), 1)
+  OBJ_TAG := $(OBJ_TAG)-softfloat
+endif
+
 OBJ_DIR := $(OBJ_ROOT)/$(OBJ_TAG)
 
 SRCS             := $(wildcard $(SRC_DIR)/*.c)
@@ -120,6 +132,14 @@ CC     := gcc
 CXX    := g++
 CLIBS  := -lgmp -lpthread -lm
 
+# SoftFloat 3e, pinned. Its build directory is named Linux-x86_64-GCC, but it is
+# SoftFloat's generic 64-bit little-endian configuration and builds with any
+# GCC or clang (8086-SSE only selects NaN encodings, which MEDUSA never uses).
+SOFTFLOAT_REPO   := https://github.com/ucb-bar/berkeley-softfloat-3.git
+SOFTFLOAT_COMMIT := a0c6494cdc11865811dec815d5c0049fba9d82a8
+SOFTFLOAT_DIR    := $(LIB_DIR)/softfloat
+SOFTFLOAT_LIB    := $(SOFTFLOAT_DIR)/build/Linux-x86_64-GCC/softfloat.a
+
 # Fat LTO objects carry ordinary code beside the IR, so an LTO=0 link can reuse
 # them. Only where the compiler accepts the flag: Apple clang rejects it, but
 # only alongside -flto, so the check has to pass both.
@@ -168,6 +188,11 @@ else ifeq ($(LEAF_FLOAT_TYPE), 2)
   FLOAT_SUFFIX := f80
 else ifeq ($(LEAF_FLOAT_TYPE), 3)
   FLOAT_SUFFIX := f128
+  ifeq ($(SOFTFLOAT), 1)
+    CFLAGS += -DLEAF_F128_SOFTFLOAT -I $(SOFTFLOAT_DIR)/source/include
+    CLIBS  += $(SOFTFLOAT_LIB)
+    F128_DEPS := $(SOFTFLOAT_LIB)
+  endif
 else
   $(error Unknown LEAF_FLOAT_TYPE=$(LEAF_FLOAT_TYPE))
 endif
@@ -243,7 +268,7 @@ BSCRIPT_PATH       := benchmark-utils/scripts
 .PHONY: all help clean clean-all clean-artifacts clean-deps clean-benchmark \
         plot benchmarks                                                     \
         init init-motobuddy make-motobuddy download-motobuddy               \
-        init-sylvan make-sylvan download-sylvan                             \
+        init-sylvan make-sylvan download-sylvan init-softfloat              \
         make-sliqsim                                                        \
         sylvan_gmp sylvan_doubles buddy_mpfr                                \
         buddy_gmp                                                           \
@@ -281,6 +306,7 @@ help:
 	@echo "  make LTO=0 ...        release without link-time optimisation"
 	@echo "  make init             clone/pin MoToBuddy @ $(MOTOBUDDY_COMMIT) and build"
 	@echo "  make init-sylvan      clone and build lib/sylvan (optional; Lace via CMake)"
+	@echo "  make init-softfloat   clone and build lib/softfloat (macOS only: f128 there)"
 	@echo "  make sylvan_gmp       algebraic GMP leaves on Sylvan (C path, no MOSF)"
 	@echo "  make sylvan_doubles   float leaves on Sylvan (LEAF_FLOAT_TYPE, default f128)"
 	@echo "  make test             MoToBuddy unit + circuits + benchmarks + metamorphic"
@@ -897,7 +923,7 @@ buddy_doubles: $(SIM_MOSF_OBJ) \
                $(INTERFACE_OBJ_buddy_doubles) \
                $(LEAF_OBJ_double) \
                $(LEAF_OBJ_reim) \
-               $(LIB_DIR)/MoToBuddy/build/src/libbuddy.a | $(BIN_DIR)
+               $(LIB_DIR)/MoToBuddy/build/src/libbuddy.a | $(BIN_DIR) $(F128_DEPS)
 	$(LINKER) $(INC_DIRS_BUDDY_DOUBLES) $(CFLAGS) \
 	    -o $(BIN_DIR)/MEDUSA_buddy_doubles_$(FLOAT_SUFFIX) $^ $(CLIBS)
 ifeq ($(LEAF_FLOAT_TYPE),3)
@@ -1035,6 +1061,16 @@ benchmarks:
 
 init: init-motobuddy
 
+# Only for f128 on macOS (SOFTFLOAT=1); see SOFTFLOAT_COMMIT above.
+init-softfloat:
+	rm -rf $(SOFTFLOAT_DIR)
+	git clone -q $(SOFTFLOAT_REPO) $(SOFTFLOAT_DIR)
+	git -C $(SOFTFLOAT_DIR) checkout -q $(SOFTFLOAT_COMMIT)
+	$(MAKE) -C $(dir $(SOFTFLOAT_LIB)) SPECIALIZE_TYPE=8086-SSE
+
+$(SOFTFLOAT_LIB):
+	@echo >&2 "error: f128 with SOFTFLOAT=1 needs SoftFloat. Run: make init-softfloat"; exit 1
+
 init-motobuddy: make-motobuddy
 	mkdir -p $(LIB_DIR) && rm -rf $(LIB_DIR)/MoToBuddy && mv MoToBuddy $(LIB_DIR)
 

README.md

@@ -31,6 +31,23 @@ make
 ```
 `make help` lists all targets.
 
+### macOS (Apple Silicon)
+
+Apple's toolchain has no 128-bit floating-point type, so on macOS the default
+f128 leaves are computed with [Berkeley SoftFloat](https://github.com/ucb-bar/berkeley-softfloat-3)
+(`SOFTFLOAT=1`, the default there). Install the dependencies and build it once, next to MoToBuddy:
+```
+brew install gmp
+export CPATH="$(brew --prefix)/include" LIBRARY_PATH="$(brew --prefix)/lib"
+make init
+make init-softfloat
+make
+```
+Results are bit-identical to f128 on Linux, except that (1/√2)^k is computed
+exactly rather than with `powf128` (last-digit differences under `--symbolic`),
+and probabilities (measurement, `--norm-csv`) are computed in `double`.
+Linux needs none of this: there f128 uses the compiler's binary128 type.
+
 ### Build types
 
 | | flags | object tree | use |

src/interface_implementations/inc/interface_prob.h

@@ -29,7 +29,11 @@ leaf_scalar_t qBDD_calculateProb(qBDD);
  * @param n          Total number of variables
  * @return           The probability contribution from paths matching curr_state
  */
+#ifdef LEAF_SCALAR_IS_SOFT    /* prob_t (mtbdd.h) is double there */
+double interface_prob_sum(qBDD t, uint32_t xt, char* curr_state, int n);
+#else
 leaf_scalar_t interface_prob_sum(qBDD t, uint32_t xt, char* curr_state, int n);
+#endif
 
 #ifdef __cplusplus
 }

src/interface_implementations/leaf_primitives/leaf_f128_soft.h

@@ -0,0 +1,122 @@
+/* leaf_f128_soft.h - f128 leaves on Berkeley SoftFloat 3e.
+ *
+ * For targets with no IEEE binary128 type at all (arm64 macOS: no __float128,
+ * and long double is a double). Included by leaf_primitive_double.h when
+ * LEAF_F128_SOFTFLOAT is defined (make SOFTFLOAT=1, the default on macOS).
+ *
+ * SoftFloat's operations are correctly rounded IEEE binary128, like the
+ * compiler's __float128 soft-float routines, so results match native f128
+ * bit for bit. float128_t is a struct, so C operators do not apply: this
+ * header provides the *_generic API and snap() on top of SoftFloat calls, and
+ * the LEAF_S_* macros that the few call sites outside it use instead of
+ * operators. Probabilities (prob_t) are double in this mode.
+ */
+#ifndef LEAF_F128_SOFT_H
+#define LEAF_F128_SOFT_H
+
+#include <string.h>
+#define SOFTFLOAT_FAST_INT64   /* what lib/softfloat is built with: pass-by-value API */
+#include <softfloat.h>
+
+#define LEAF_SCALAR_IS_SOFT 1
+
+typedef float128_t      leaf_primitive_t[1];
+typedef float128_t      leaf_scalar_t;
+
+/* Constants as binary128 bit patterns {low, high} (little-endian, as
+ * SoftFloat stores them), equal to the q-suffixed literals of the
+ * __float128 build. LEAF_REL_EPS / LEAF_ABS_EPS cannot be overridden here. */
+#define LEAF_F128_BITS(lo, hi) ((float128_t){ { (lo), (hi) } })
+#define LEAF_ZERO        LEAF_F128_BITS(0, 0)
+#define LEAF_ONE         LEAF_F128_BITS(0, 0x3fff000000000000ULL)
+#define LEAF_REL_EPS     LEAF_F128_BITS(0x941b17953adc3111ULL, 0x3fa1fb0f6be50601ULL) /* 1e-28 */
+#define LEAF_ABS_EPS     LEAF_F128_BITS(0x2974cfbc31db4b03ULL, 0x3f949f623d5a8a73ULL) /* 1e-32 */
+#define LEAF_INV_ABS_EPS LEAF_F128_BITS(0x6b3be04000000000ULL, 0x40693b8b5b5056e1ULL) /* 1/fl(1e-32) */
+#define LEAF_SQRT2INV    LEAF_F128_BITS(0xc908b2fb1366ea95ULL, 0x3ffe6a09e667f3bcULL) /* 1/sqrt(2) */
+
+static inline float128_t leaf_s_from_d(double d) {
+    float64_t f; memcpy(&f, &d, sizeof d); return f64_to_f128(f);
+}
+static inline double leaf_s_to_d(float128_t x) {
+    float64_t f = f128_to_f64(x); double d; memcpy(&d, &f, sizeof d); return d;
+}
+static inline float128_t leaf_s_neg(float128_t x) { x.v[1] ^= (uint64_t)1 << 63; return x; }
+static inline float128_t leaf_s_abs(float128_t x) { x.v[1] &= ~((uint64_t)1 << 63); return x; }
+
+#define LEAF_ISNAN(x)    (!f128_eq((x), (x)))
+#define LEAF_ABS(x)      leaf_s_abs(x)
+#define LEAF_SQRT(x)     f128_sqrt(x)
+#define LEAF_ROUND(x)    f128_roundToInt((x), softfloat_round_near_maxMag, false)
+
+/* Operators for the call sites outside this header. */
+#define LEAF_S_ADD(a, b)     f128_add((a), (b))
+#define LEAF_S_SUB(a, b)     f128_sub((a), (b))
+#define LEAF_S_MUL(a, b)     f128_mul((a), (b))
+#define LEAF_S_LT(a, b)      f128_lt((a), (b))
+#define LEAF_S_LE(a, b)      f128_le((a), (b))
+#define LEAF_S_IS_ZERO(x)    f128_eq((x), LEAF_ZERO)
+#define LEAF_S_TO_DOUBLE(x)  leaf_s_to_d(x)
+#define LEAF_S_FROM_DOUBLE(d) leaf_s_from_d(d)
+#define LEAF_S_TO_PROB(x)    leaf_s_to_d(x)
+#define LEAF_S_FROM_PROB(p)  leaf_s_from_d(p)
+
+/* (1/sqrt 2)^k, exactly rounded: 2^-q, times 1/sqrt 2 when k is odd. */
+static inline float128_t leaf_sqrt2inv_pow(long k) {
+    long q = k >= 0 ? k / 2 : -((-k + 1) / 2);       /* floor(k / 2) */
+    float128_t r = LEAF_F128_BITS(0, (uint64_t)(16383 - q) << 48);
+    return (k - 2 * q) ? f128_mul(r, LEAF_SQRT2INV) : r;
+}
+
+#define LEAF_SCALAR_HASH_BYTES sizeof(leaf_scalar_t)
+#define LEAF_PRIMITIVE_OPS_INLINED 1
+
+static inline int cmp_generic(leaf_primitive_t a, leaf_primitive_t b) {
+    return !f128_eq(a[0], b[0]);
+}
+static inline void init_generic(leaf_primitive_t x) { x[0] = LEAF_ZERO; }
+static inline void init_set_generic(leaf_primitive_t dst, leaf_primitive_t src) { dst[0] = src[0]; }
+static inline void clear_generic(leaf_primitive_t x) { x[0] = LEAF_ZERO; }
+static inline void mul_ui_generic(leaf_primitive_t r, leaf_primitive_t x, unsigned long c) {
+    r[0] = f128_mul(x[0], ui64_to_f128(c));
+}
+static inline void neg_generic(leaf_primitive_t r, leaf_primitive_t x) { r[0] = leaf_s_neg(x[0]); }
+static inline void add_generic(leaf_primitive_t r, leaf_primitive_t a, leaf_primitive_t b) {
+    r[0] = f128_add(a[0], b[0]);
+}
+static inline void init_set_ui_generic(leaf_primitive_t x, unsigned long v) { x[0] = ui64_to_f128(v); }
+static inline int sgn_generic(leaf_primitive_t x) {
+    if (f128_lt(LEAF_ZERO, x[0])) return 1;
+    if (f128_lt(x[0], LEAF_ZERO)) return -1;
+    return 0;
+}
+static inline void set_ui_generic(leaf_primitive_t x, unsigned long v) { x[0] = ui64_to_f128(v); }
+static inline void set_generic(leaf_primitive_t dst, leaf_primitive_t src) { dst[0] = src[0]; }
+static inline void mul_generic(leaf_primitive_t r, leaf_primitive_t a, leaf_primitive_t b) {
+    r[0] = f128_mul(a[0], b[0]);
+}
+static inline void set_d_generic(leaf_primitive_t x, double v) { x[0] = leaf_s_from_d(v); }
+static inline void sub_generic(leaf_primitive_t r, leaf_primitive_t a, leaf_primitive_t b) {
+    r[0] = f128_sub(a[0], b[0]);
+}
+static inline void div_generic(leaf_primitive_t r, leaf_primitive_t a, leaf_primitive_t b) {
+    r[0] = f128_div(a[0], b[0]);
+}
+static inline void mul_d_generic(leaf_primitive_t r, leaf_primitive_t x, double s) {
+    r[0] = f128_mul(x[0], leaf_s_from_d(s));
+}
+static inline void mul_sqrt2inv_generic(leaf_primitive_t r, leaf_primitive_t x) {
+    r[0] = f128_mul(x[0], LEAF_SQRT2INV);
+}
+static inline double to_double_generic(leaf_primitive_t x) { return leaf_s_to_d(x[0]); }
+
+/* Same grid snap as the native header (see the comment there). */
+static inline leaf_scalar_t snap(leaf_scalar_t x) {
+    if (LEAF_ISNAN(x)) {
+        printf("ERROR: NaN detected. Possible numerical instability.\n");
+        exit(1);
+    }
+    if (f128_lt(LEAF_ABS(x), LEAF_ABS_EPS)) return LEAF_ZERO;
+    return f128_mul(LEAF_ROUND(f128_mul(x, LEAF_INV_ABS_EPS)), LEAF_ABS_EPS);
+}
+
+#endif /* LEAF_F128_SOFT_H */