Schanuel's Conjecture and the Semantics of Triton's FPSan
a day ago
- #Floating-Point Verification
- #Compiler Pass
- #Algebraic Equivalence
- FPSan is a tool for verifying algebraic equivalence of Triton programs with floating-point arithmetic, developed with Pawel Szczerbuk.
- It does not preserve functionality, makes programs slower, and was initially undocumented, acting as a non-standard compiler pass.
- The tool transforms floating-point operations into integer operations via a bijective embedding function φ, ensuring algebraically equivalent programs produce identical integer results.
- It relies on Schanuel's conjecture to guarantee correctness for programs with input-independent control flow, constants {-1,0,1}, and operations {-,+,×,exp}, covering many ML kernels like matrix multiplication.
- The implementation maps IEEE-754 floats to integers mod 2³², using operations like multiplication by odd constants and xorshift, preserving properties like φ(-x) = -φ(x).
- FPSan replaces fadd, fsub, fmul, and exp with integer analogs, and supports mixed precision via downcasting and upcasting with integer ring operations.
- The proof leverages Schanuel's conjecture to show equivalence in a free exponential ring, extended to include sine and cosine via complex exponential forms.