We use the FPSan.cpp from triton to lift definitions into Lean, along with definitions from opencompl/fp-lean of floating point numbers, to give a formally verified implementation of the FPSan sanitizer in Lean. Then, the bulk of the work was performed by Aristotle, with high-level guidance from me on proof strategies, due to my experience with floating point and bitvector verification in Lean, as well as experience thinking about decision procedures for exponential rings (thanks Ben!).
Axioms
We take as axiom the fact that if two circuits agree on the free exponential ring, which we just take to be the reals, then they agree on agree exponential ring. This is the essential content of Macintyre'91.
Proofs
We prove the following properties of the embedding:
Homomorphism theorems (φ commutes with every operation)
phi_fpsanAdd:φ(fpsanAdd(a, b)) = φ(a) + φ(b)phi_fpsanSub:φ(fpsanSub(a, b)) = φ(a) - φ(b)phi_fpsanMul:φ(fpsanMul(a, b)) = φ(a) * φ(b)phi_fpsanNeg:φ(fpsanNeg(a)) = -φ(a)phi_fpsanZero:φ(fpsanZero) = 0phi_fpsanOne:φ(fpsanOne) = 1phi_fpsanExp:φ(fpsanExp(a)) = exp(φ(a))phi_fpsanSin:φ(fpsanSin(a)) = sin(φ(a))phi_fpsanCos:φ(fpsanCos(a)) = cos(φ(a))
Ring axioms (FPSan operations form a commutative ring)
fpsanAdd_comm,fpsanAdd_assoc— addition is commutative and associativefpsanZero_add,fpsanAdd_zero— zero is the additive identityfpsanNeg_add— negation is the additive inversefpsanSub_eq_add_neg— subtraction equals adding the negationfpsanMul_comm,fpsanMul_assoc— multiplication is commutative and associativefpsanOne_mul,fpsanMul_one— one is the multiplicative identityfpsanMul_add,fpsanAdd_mul— distributivity
Exponential ring axioms
fpsanExp_zero:fpsanExp(0) = 1fpsanExp_add:fpsanExp(a + b) = fpsanExp(a) * fpsanExp(b)
Trigonometric identities
fpsanSin_zero,fpsanCos_zero— sin(0) = 0, cos(0) = 1fpsanCos_add— cosine angle-sum formulafpsanSin_add— sine angle-sum formulafpsanSin_sq_add_cos_sq— Pythagorean identity: sin²(a) + cos²(a) = 1