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.
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!
It seems to me that one could maliciously construct a failure. For example:
phi(1.0) * 2^32 = 0
So:
1.0 + … + 1.0 (2^32 terms added)
Will turn into zero in the embedding. (I bet other, dramatically smaller zeros could be found by other operations. phi^-1(2^16) could be a good starting point, but you don’t necessarily need a shorter one — see below.)
Now you find a floating point expression tree that has only 1.0, 0, and -1.0 at the leaves and generates this spurious zero. (For example, 1.0 + 1.0, squared five times.)
Now you maliciously transform a program by adding one of these spurious zero expressions somewhere. Am I missing something?
More generally, what is the multiply-xorshift-multiply sequence accomplishing? I feel like it might make non-malicious collisions unlikely, but I feel like it would be mildly surprising if it does much in the setting of trying to prove something without any probability of error. And it seems a bit unfortunate that no choice of the scrambling constants has any effect on the expressions that start with 1.0 and use only multiplication and addition to get to zero.
Also, how does floating point infinity fit in? It seems like it doesn’t act very infinite in the integer embedding.
(I could be totally wrong here. I only read the definitions twice, and I didn’t try to write anything down.)
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.
Now you find a floating point expression tree that has only 1.0, 0, and -1.0 at the leaves and generates this spurious zero. (For example, 1.0 + 1.0, squared five times.)
Now you maliciously transform a program by adding one of these spurious zero expressions somewhere. Am I missing something?
More generally, what is the multiply-xorshift-multiply sequence accomplishing? I feel like it might make non-malicious collisions unlikely, but I feel like it would be mildly surprising if it does much in the setting of trying to prove something without any probability of error. And it seems a bit unfortunate that no choice of the scrambling constants has any effect on the expressions that start with 1.0 and use only multiplication and addition to get to zero.
Also, how does floating point infinity fit in? It seems like it doesn’t act very infinite in the integer embedding.
(I could be totally wrong here. I only read the definitions twice, and I didn’t try to write anything down.)