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) = 0
• phi_fpsanOne: φ(fpsanOne) = 1
• phi_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 associative
• fpsanZero_add, fpsanAdd_zero — zero is the additive identity
• fpsanNeg_add — negation is the additive inverse
• fpsanSub_eq_add_neg — subtraction equals adding the negation
• fpsanMul_comm, fpsanMul_assoc — multiplication is commutative and associative
• fpsanOne_mul, fpsanMul_one — one is the multiplicative identity
• fpsanMul_add, fpsanAdd_mul — distributivity

Exponential ring axioms

• fpsanExp_zero: fpsanExp(0) = 1
• fpsanExp_add: fpsanExp(a + b) = fpsanExp(a) * fpsanExp(b)

Trigonometric identities

• fpsanSin_zero, fpsanCos_zero — sin(0) = 0, cos(0) = 1
• fpsanCos_add — cosine angle-sum formula
• fpsanSin_add — sine angle-sum formula
• fpsanSin_sq_add_cos_sq — Pythagorean identity: sin²(a) + cos²(a) = 1