search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Unsound term simplification for ite with SFloatingPoint #702

Closed lsrcz closed 2 months ago

lsrcz commented 2 months ago

The following code demonstrates the problem. It is falsifiable with the counter-example x = False.

ghci> prove $ \x -> ite x (-infinity :: SFloatingPoint 8 24) infinity .== -infinity
Q.E.D.
LeventErkok commented 2 months ago

Yeah, that’s no good. I’ll take a look tomorrow AM.

lsrcz commented 2 months ago

I believe that I’ve understood what’s happening.

https://github.com/LeventErkok/sbv/blob/720255d2a843b146d248720036a986917ee62041/Data/SBV/Core/SizedFloats.hs#L226-L233

The newly added arbFPIsEqualObjectH function has a clause that tests whether the lhs is inf, and if so, return whether the rhs is inf. This will make +/-inf equal.

I believe that we don’t need to handle inf specially, but we can just use the == operator. What do you think? I can send a fix for it, but no hurry to review it.