FPSan is a Triton compiler pass that replaces floating-point ops with integer ring ops, enabling algebraic equivalence checking of GPU kernels contingent on Schanuel’s conjecture.
Key Takeaways
FPSan maps IEEE-754 floats bijectively into integers mod 2^32 via a mixing function φ, preserving ring structure so equivalent programs produce identical outputs.
Correctness depends on the real Schanuel’s conjecture: assuming it, the subring of R generated by {+, ×, exp} is the free exponential ring, making FPSan’s integer quotient a valid homomorphic image.
Covers matrix multiplications and self-attention kernels; control flow must be data-independent and ops restricted to {-, +, ×, exp, sin, cos}.
Mixed-precision support maps j-bit floats into integers mod 2^j, with downcasting via mod reduction and upcasting via sign-extending lift; 2-adic Newton’s method computes modular inverses.
tl.dot (Triton’s matrix multiply primitive) is supported by expanding into scalar ops; only per-element φ/φ^-1 calls are needed around an int32 core.
