Add opaque types for Double and Float

[mario-bucev]

No description provided.

[samarion]

I'm pretty sure Z3 and CVC4 support floating-point arithmetic. Why not add solver support?

[mario-bucev]

For context, there is a project that would require converting between FP and their bits representation (for serialization & deserialization). @vkuncak and I settled on this first approach towards adding some FP support in Stainless. But maybe doing that in this way is not the best way (another approach would be by extracting these methods and handle them separately).

[samarion]

The SMT standard [1] has support for FP <-> BV conversions but it seems like the -> direction is not injective (which might break your doubleToRawLongBits post-condition). They recommend using

(declare-fun b () (_ BitVec m))
(assert (= ((_ to_fp eb sb) b) f))

Note that it shouldn't be too much work to add FP support throughout the stack, just need to

1. define some new trees in Inox and the corresponding embeddings, and
2. adapt the extraction logic.

Maybe a useful first step in the project?

[1] http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

[mario-bucev]

Yes, this looks like a good direction, thank you for the research! I will discuss it with @vkuncak