Can we verify `f32` and `f64` behavior?

Some relevant papers and docs for this issue:

- https://inria.hal.science/hal-01534533v1/document
- https://people.mpi-sws.org/~rosaabbasi/key_float.pdf
- https://www.acsel-lab.com/arithmetic/arith18/papers/ARITH18_Boldo.pdf
- https://why3.org/stdlib/floating_point.html

Since we have floating point types in the Why3 standard library I think this is doable.