[ondrik]

Draft: exploration. Stacked on #46. This makes f128 build on arm64 macOS, which has no 128-bit floating-point type at all, by using Berkeley SoftFloat 3e. SoftFloat setup and install instructions apply only to the Mac; Linux builds neither need it nor change.

How it's switched on

• SOFTFLOAT=1 selects it. That's the default on macOS only, so make there builds f128 on SoftFloat.
• One-time setup: make init-softfloat fetches SoftFloat at a pinned commit and builds it, the same way make init-sylvan works. If it's missing, the link stops early with that hint.
• Install steps: the README gets a short macOS (Apple Silicon) section with the Mac-only steps.

Code changes

leaf_f128_soft.h (new, ~120 lines)	The f128 scalar becomes SoftFloat's float128_t. The header implements the same *_generic API and snap() on SoftFloat calls. Native builds keep their existing code unchanged.
~30 call sites (leaf_reim_double.c, norm_track.c, mtbdd.c, tests)	A struct can't use + - * ==, so the few raw scalar operations outside the leaf primitives go through LEAF_S_* macros. On native builds these are plain operators.
prob_t	double in SoftFloat mode, which affects measurement probabilities and --norm-csv.
printing	to_str prints %.30g exactly as glibc's strfromf128 does, via exact integer conversion with round-half-even. It matched on 2 million random and edge-case values (subnormals, extremes).

Verified on x86_64 Linux, against native __float128

• Same results. Over 613 benchmark runs (all of no-measure, plus --symbolic for LP-*), every classic run gives a bit-identical res.dot.
• The 39 --symbolic runs that differ do so for one reason: (1/√2)^k.
  • SoftFloat builds it exactly, as 2^(−⌊k/2⌋), times 1/√2 when k is odd.
  • Native uses powf128(fl(1/√2), k), a power of the rounded constant. That's off in the last bits for 399 of 401 exponents; even k = −200 gives 2^100 + 0.017.
  • With the exact construction on native as well, all 39 match. Native's powf128 path is the less accurate one, and switching it to the exact construction is worth a separate small PR.
• Faster, not slower. SoftFloat runs at about 0.7× native time (geometric mean over runs longer than 0.5 s; 0.76× in total).
• Tests: make test and make test-grover-f128 pass with SOFTFLOAT=1. The native suites still pass after the macro changes.

CI (this PR)

• macOS job: runs make init-softfloat and is expected to pass every f128 step.
• New Ubuntu 24.04, SoftFloat job: runs the same suites on SoftFloat f128 where native f128 also runs, so a regression on either side shows up next to the other.

Open questions

• (1/√2)^k on native: whether to switch native to the exact construction too. That would make Mac and Linux bit-identical and native more accurate, but it changes the last digits of some --symbolic outputs.
• prob_t as double: whether that's acceptable on macOS, or worth carrying through as float128_t (about 17 more call sites).

🤖 Generated with Claude Code

https://claude.ai/code/session_012q87VyzNBV8gtH2ntMeKoM

[github-actions]

Claude Code review (CERIT, model coder) of a3fc08f

I reviewed the PR description and the full diff (all 15 changed files are shown; the diff does not end with any "files not shown" note), then read the surrounding sources (leaf_primitive_double.h/.c, leaf_f128_soft.h, leaf_reim_double.c, mtbdd.h/.c, norm_track.c, sim.c, the Makefile, platforms.yml, platform-probe.sh, and the touched tests). I verified the SoftFloat constant bit patterns (LEAF_SQRT2INV, LEAF_ABS_EPS, LEAF_INV_ABS_EPS) and the leaf_s_to_str digit/rounding logic against glibc %.30g semantics; both check out. Findings, most severe first:

• src/interface_implementations/leaf_primitives/leaf_f128_soft.h:64 (leaf_sqrt2inv_pow) - the 2^-q bit-pattern construction (uint64_t)(16383 - q) << 48 is only valid for 16383 - q in [0, 0x7FFE], i.e. |k| ≲ 32767. Outside that it silently produces wrong values instead of overflow/underflow: for k ≤ -32769 (e.g. k = -32770, q = -16385, 16383 - q = 0x8000) the shift sets bit 63 and zeroes the exponent field, so the function returns -0.0 where the true value (1/√2)^k = 2^16385 overflows to +inf (powf128 on native returns +inf); for k ≥ 32766 the exponent field becomes 0 with a zero significand, i.e. +0.0, where 2^-16383 is a representable subnormal that native powf128 returns. Both mul_inv_sqrt2_pow_generic and inv_sqrt2_pow_generic (leaf_primitive_double.c:35-46) feed this into leaves. Scenario: a --symbolic run whose circuit accumulates ≥ ~32767 powers of 1/√2 (≈33k H/rotation-type gates) — the SoftFloat build emits −0/+0 where the native build emits inf/subnormal, so macOS and Linux outputs diverge with no diagnostic. Caveat: I could not construct a benchmark in the repo that reaches |k| ≥ 32767 (in classic mode snap() would zero such amplitudes anyway), so this may be unreachable in practice — but if it is reachable, it is a silent wrong result rather than an error.

• Makefile:191-195 - CLIBS += $(SOFTFLOAT_LIB) is applied unconditionally at parse time whenever LEAF_FLOAT_TYPE=3 (the default) and SOFTFLOAT=1 (the macOS default), and CLIBS is used by every link rule, including buddy_gmp (Makefile:909), the GMP/MPFR test binaries and the Sylvan targets, none of which use f128. Scenario: on a fresh macOS checkout, make init && make buddy_gmp (no make init-softfloat) fails at the link step with "file not found: lib/softfloat/build/Linux-x86_64-GCC/softfloat.a" — a target that needs no SoftFloat at all is broken, and the intended hint rule ($(SOFTFLOAT_LIB): error) never fires because F128_DEPS is only an order-only prerequisite of buddy_doubles (Makefile:926), not of these targets. (The CI jobs don't hit this because they always run init-softfloat first.)

• src/mtbdd.h:28-29 / src/interface_implementations/inc/interface_prob.h:32-36 - in the SoftFloat build prob_t is double, so all probability accumulation, not just printing, is downgraded from 113-bit to 53-bit precision. Scenario: measure_all (src/sim.c:788-800) compares random <= p_qt_is_one where p_qt_is_one is now a double sum of up to 2^n leaf probabilities; a state whose probability lies within ~1e-16 relative of the rand() draw samples the opposite outcome compared with the native-f128 build of the same circuit and seed, so sampled distributions and --norm-csv total_prob/norm_dev columns differ between macOS/SoftFloat and Linux/native. The PR description flags this as an open question, but as written it is a silent results change on every SoftFloat build (macOS and the new Ubuntu SoftFloat CI job), not just a display precision change.

• src/interface_implementations/leaf_primitives/leaf_f128_soft.h:32-34 - LEAF_ABS_EPS/LEAF_REL_EPS are defined unconditionally, but the Makefile still supports overriding them (Makefile:245-246, make LEAF_ABS_EPS=...), which works on every native leaf type via the #ifndef guards. Scenario: make SOFTFLOAT=1 LEAF_ABS_EPS=1e-40 emits a "redefined" warning and the command-line override is silently discarded — the same invocation on a native build changes the snap grid. A user tuning the epsilon gets different behaviour depending on the backend with no error. (The header comment acknowledges this; LEAF_REL_EPS is currently unused by any code, only LEAF_ABS_EPS matters.)

• src/interface_implementations/leaf_primitives/leaf_primitive_double.c:53-116 (leaf_s_to_str) - the ~90-line reimplementation of glibc's %.30g (decimal-exponent estimate plus correction loop, round-half-even via mpz_odd_p(q), subnormal handling, the four %g layout branches) has no test anywhere in tests/: the claim of digit-for-digit agreement with strfromf128 is verified only outside the repo. Scenario: a regression in any of these branches (e.g. the E++/E-- correction loop, or the E < -4 || E >= P style threshold) changes the last digits of every amplitude in res.dot without failing make test — the circuit/grover tests parse res.dot terminals numerically with tolerance rather than comparing strings, so a wrong-but-parseable digit ships unnoticed on the macOS and Ubuntu-SoftFloat CI jobs. A small direct test pinning to_str_generic output for a handful of values (normal, subnormal, E = -4/-5 boundary, E = 29/30 boundary, trailing-zero stripping) would close this.

I am unsure whether the first finding is reachable with the current benchmark suite (|k| would have to exceed ~32767); everything else I could trace concretely through the code.
_{Automated and advisory: it may be wrong, and it does not block merging. Run.}