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.

▲

measurablefunc 5 hours ago | parent | prev [-]

> 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.

	▲	simonreiff 4 hours ago \| parent [-]
		Right. Put differently, we have that FPSan() is a well-defined function, so [ f = g ] => [ FPSan(f) = FPSan(g)], but we need to show that FPSan() is injective, i.e., [ FPSan(f) = FPSan(g) ] => [ f = g ]. I confess I haven't looked very closely but it should not be so hard. We can prove injectibility in the alternative by analyzing ker(FPSan()), the set of all inputs in the domain of functions mapping to the identity element in the co-domain. If the kernel is trivial and only consists of the identity map, the injectibility is established, but I am not immediately seeing the proof. Fun!