Schanuel’s conjecture and the semantics of FPSan | Complex Projective 4-Space
Complex Projective 4-Space
Where exciting things happen
Skip to content
Home<br>About
Cipher solvers
Season IV
Solved cipher 71
Season III
Solved cipher 70
Solved cipher 69
Solved cipher 68
Solved cipher 67
Solved cipher 66
Solved cipher 65
Solved cipher 64
Solved cipher 63
Solved cipher 62
Solved cipher 61
Solved cipher 60
Solved cipher 59
Solved cipher 58
Solved cipher 57
Solved cipher 56
Solved cipher 55
Solved cipher 54
Solved cipher 53
Solved cipher 52
Solved cipher 51
Season II
Solved cipher 50
Solved cipher 49
Solved cipher 48
Solved cipher 47
Solved cipher 46
Solved cipher 45
Solved cipher 44
Solved cipher 43
Solved cipher 42
Solved cipher 41
Solved cipher 40
Solved cipher 39
Solved cipher 38
Solved cipher 37
Solved cipher 36
Solved cipher 35
Solved cipher 34
Solved cipher 33
Solved cipher 32
Solved cipher 31
Season I
Solved cipher 30
Solved cipher 29
Solved cipher 28
Solved cipher 27
Solved cipher 26
Solved cipher 25
Solved cipher 24
Solved cipher 23
Solved cipher 22
Solved cipher 21
Solved cipher 20
Solved cipher 19
Solved cipher 18
Solved cipher 17
Solved cipher 16
Solved cipher 15
Solved cipher 14
Solved cipher 13
Solved cipher 12
Solved cipher 11
Solved cipher 10
Solved cipher 9
Solved cipher 8
Solved cipher 7
Solved cipher 6
Solved cipher 5
Solved cipher 4
Contact
Publications
Revision
IA revision
IB revision
Skydive
← Charles Corderman’s computer
Schanuel’s conjecture and the semantics of FPSan
Posted on May 3, 2026 by apgoucher
I’ve been spending some of my time recently developing a tool called FPSan in collaboration with Pawel Szczerbuk. It’s implemented as a Triton compiler pass, but has none of the desirable properties expected of a compiler pass: in particular, it doesn’t preserve functionality, it makes things slower, and it’s hitherto completely undocumented. (On the latter point, Pawel has an open PR adding documentation.)
Its purpose is to make it easier to verify algebraic equivalence of programs written in Triton that involve floating-point arithmetic. The key problem is that, in floating-point arithmetic, algebraic laws such as associativity do not hold exactly: in general, (a + b) + c need not equal a + (b + c). As such, if you rewrite a program to take advantage of this, e.g. to replace a sequential summation loop with a parallel tree-shaped reduction, the program will no longer behave completely identically.
FPSan can be viewed as an idempotent function on the space of programs that replaces all floating-point operations with (completely different!) integer operations, such that if f and g are algebraically equivalent programs then FPSan(f) and FPSan(g) produce identical results when given identical inputs.
More formally, conditional on the real version of Schanuel’s conjecture, this holds provided that the programs f and g have the following properties:
each program implements an arithmetic circuit on its floating-point inputs, and the control flow is independent of those floating-point inputs;
the arithmetic circuit only consists of inputs, outputs, the constants {-1.0, 0.0, +1.0}, the ring operations {−, +, ×}, and the exponential function exp.
These operations may seem somewhat restrictive, but it already encompasses a vast range of the more common GPU kernels involved in machine learning: matrix multiplications and [the bulk of] self-attention are covered by FPSan’s guarantees.
The proof is deferred to the end of this article to avoid derailing the discussion. This is quite possibly the only compiler sanitiser whose correctness depends on an extremely difficult unsolved problem in transcendental number theory.
Implementation
Specifically, FPSan constructs a bijective ’embedding function’ φ from the set of IEEE-754 single-precision floats (there are 2^32 of them) to the ring of integers modulo 2^32. The function φ is implemented as follows:
encode the float as a 32-bit word using the IEEE-754 encoding;
the uppermost bit (sign bit) is preserved;
for the remaining 31 bits, we apply a mod-2^31 multiplication by an odd constant, then a xorshift, then another mod-2^31 multiplication by an odd constant, and finally (if the sign bit was set) take the two’s complement;
interpret the 32-bit word as an integer modulo 2^32.
It’s designed to mix the bits reasonably well whilst having the properties that φ(−x) = −φ(x) for all nonzero x, φ(0.0) = 0, and φ(1.0) = 1. The ‘negative zero’ float gets mapped to 2^31, which is the other additively self-inverse element of the ring of integers modulo 2^32.
With this function, FPSan replaces:
floating-point addition fadd(x, y) with φ^-1(φ(x) + φ(y));
floating-point subtraction fsub(x, y) with φ^-1(φ(x) − φ(y));
floating-point multiplication fmul(x, y) with φ^-1(φ(x) × φ(y));
floating-point exponentiation exp(x) with φ^-1(C^φ(x)) where C is a particular constant...