Yes, this is correct, and indeed injectivity is impossible from a counting argument: for example, there are only (2^32)^(2^32) unary functions in this finite ring, but infinitely many polynomials with integer coefficients, so we cannot hope to distinguish them all.
> More generally, what is the multiply-xorshift-multiply sequence accomplishing? I feel like it might make non-malicious collisions unlikely
Exactly this. One issue with the bitcast embedding (other than not mapping {-1.0, 0.0, 1.0} to {-1, 0, 1}) is that 'round numbers' such as 42.0 have floating-point representations (such as 0x42280000) that end in very many trailing zero bits. This is particularly problematic because multiplying two such numbers gives 0.
In general, FPSan isn't designed for an adversarial regime. There are ways that it could be hardened in this direction: for example, instead of using the ring of integers modulo 2^32, choose a prime-power modulus using a large prime derived from a cryptographic hash of the source code of the two programs that you're trying to compare. But I'm not confident that even that guarantees adversarial robustness: for instance, there may be some clever way to efficiently implement a nonzero polynomial that vanishes at every small integer (say, every integer with absolute value < 10^100) and that would break this hardened variant.
The motivation behind FPSan is to protect against accidental implementation bugs: for example, someone writes a complicated fused kernel that improves the runtime of model inference, but makes an honest mistake whilst doing so. Bitwise floating-point matching is too strict; approximate matching is too messy (what should the error tolerances be?); symbolic methods are too unscalable.
