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
242 stars 34 forks source link

Mergeable instance for symbolic Either elimination #453

Closed bts closed 5 years ago

bts commented 5 years ago

Hi Levent,

It seems that just as ite, the symbolic eliminator for the Bool sum type, symbolicMerges amongst its possible outcomes, that we should probably similarly have a Mergeable constraint on the symbolic eliminator either? (Disclaimer: I have not yet played with the this new Either functionality firsthand -- I may be failing to take something into account.)

Thoughts? Brian

LeventErkok commented 5 years ago

Possibly! Would be great to play around with these a bit and see what sort of extra functionality needed. An actual use-case would be good too if you can contribute that as an example file that we can ship with SBV.

LeventErkok commented 5 years ago

@bts

The following works just fine

Prelude Data.SBV Data.SBV.Either> prove $ \x y z -> ite x y (z::SEither Bool Integer) .== z
Falsifiable. Counter-example:
  s0 =       True :: Bool
  s1 = Left False :: Either Bool Integer
  s2 =    Right 0 :: Either Bool Integer

This works because of the default SBV instance for mergeable: Note that if a type directly maps to an SMTLib type, then we get mergeable for free: SMTLib does it for us!

Is this what you were worried about? Is there some other scenario that might go wrong?

bts commented 5 years ago

Ah perfect! Yeah, the instance SymVal a => Mergeable (SBV a) does the trick for us. That makes sense. Thanks!