Floating point determinism

Currently, the floating point semantics of all CakeML ILs just delegates to `machine_ieee`, which uses a @ term to select a NaN to return in cases where that is the result. This makes the behavior of basic floating point operations dependent on the HOL model. While it is philosophically unsatisfactory for a physical value which is subjectable to experiment to not be model-theoretically absolute, it's not problematic for program verification: any statement you can prove about fp64 math is true for all models, including the model which agrees with ARM VFP semantics.

If native floats are added for any other architecture, this breaks down, as different architectures have different rules for NaN propagation, invalid float-to-int conversions, and probably other things. It would also be unsuitable for hardware verification, as hardware cannot simultaneously match all HOL models.

I believe we need to either pick a deterministic semantics for floating point and commit to emulating it on all platforms, or somehow make the semantics explicitly nondeterministic.