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.
2 comments
[ 3.8 ms ] story [ 12.4 ms ] threadOk, 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.