Schanuel's Conjecture and the Semantics of Triton's FPSan

Wow, that's pretty cool. Translating (almost) arbitrary floating point programs into weird integer programs while also preserving equivalence under non-strict floating point semantics? Mathematics can be surprisingly wonderful.

> if f and g are algebraically equivalent programs then FPSan(f) and FPSan(g) produce identical results when given identical inputs

Ok, but we want the other direction. If FPSan(f) & FPSan(g) produce identical results for identical inputs then we want to conclude that f & g are also equivalent. If g is an "optimized" version of f then this would allow checking equivalence but that's not what they are proving or maybe they are but it looks like the converse is contingent on an unproven conjecture.