search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

Add opaque types for Double and Float #1413

Open mario-bucev opened 1 year ago

samarion commented 1 year ago

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

mario-bucev commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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