# sbvPlugin

Formally prove properties of Haskell programs using SBV/SMT http://github.com/LeventErkok/sbvPlugin

Latest on Hackage: | 0.8 |

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

**Levent Erkok**

**Levent Erkok (erkokl@gmail.com)**

## SBVPlugin: SBV Plugin for GHC

[] (http://hackage.haskell.org/package/sbvPlugin) [] (http://travis-ci.org/LeventErkok/sbvPlugin)

### Example

```
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
module Test where
import Data.SBV.Plugin
test :: Proved (Integer -> Integer -> Bool)
test x y = x + y >= x - y
```

*Note the GHC option on the very first line. Either add this to your file, or pass -fplugin=Data.SBV.Plugin as an
argument to GHC, either on the command line or via cabal. Same trick also works for GHCi.*

The `Proved`

type simply wraps over the type of the predicate you are trying to prove, typically a function
returning a `Bool`

value. It tells the plugin to treat the input as a theorem that needs to be proved.
When compiled, we get:

```
$ ghc -c Test.hs
[SBV] Test.hs:8:1-4 Proving "test", using Z3.
[Z3] Falsifiable. Counter-example:
x = 0 :: Integer
y = -1 :: Integer
[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
```

Note that the compilation will be aborted, since the theorem doesn't hold. If you load this file in GHCi, it will simply fail and drop you back to the GHCi prompt.

### Annotation style

While the `Proved`

type should suffice for simple uses, the plugin takes a number of arguments to modify
options and pick underlying solvers. In this case, an explicit annotation can be provided:

```
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
module Test where
import Data.SBV.Plugin
{-# ANN test theorem {options = [IgnoreFailure]} #-}
test :: Integer -> Integer -> Bool
test x y = x == y -- clearly not True!
```

The above, for instance, tells the plugin to ignore failed commands (`IgnoreFailure`

). This would be useful when you
have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping at
that point.

### Available options

The plugin currently understands the following options. Multiple options can be given at the same time by comma separating them.

```
data SBVOption =
IgnoreFailure -- ^ Continue even if proof fails
| Skip String -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on.
| Verbose -- ^ Produce verbose output, good for debugging
| Debug -- ^ Produce really verbose output, use only when things go really wrong!
| QuickCheck -- ^ Perform quickCheck
| Uninterpret -- ^ Uninterpret this binding for proof purposes
| Names [String] -- ^ Use these names for the arguments; need not be exhaustive
| ListSize Int -- ^ If a list-input is found, use this length. If not specified, we will complain!
| Z3 -- ^ Use Z3
| Yices -- ^ Use Yices
| Boolector -- ^ Use Boolector
| CVC4 -- ^ Use CVC4
| MathSAT -- ^ Use MathSAT
| ABC -- ^ Use ABC
| AnySolver -- ^ Run all installed solvers in parallel, and report the result from the first to finish
```

### Using SBVPlugin from GHCi

The plugin should work from GHCi with no changes. Note that when run from GHCi, the plugin will
behave as if the `IgnoreFailure`

argument is given on all annotations, so that failures do not stop
the load process.

### Thanks

The following people reported bugs, provided comments/feedback, or contributed to the development of SBVPlugin in various ways: Nickolas Fotopoulos and Stephan Renatus.

## Changes

- Hackage: http://hackage.haskell.org/package/sbvPlugin
- GitHub: http://github.com/LeventErkok/sbvPlugin
- Latest Hackage released version: 0.8, 2017-01-12

### Version 0.8, 2017-01-12

- Fix broken links, thanks to Stephan Renatus for the patch.
- Add the 'Proved' type, which allows for easily tagging a type for proof, without the need for an explicit annotation. Thanks to Nickolas Fotopoulos for the patch.
- Bump up sbv dependence to >5.14

### Version 0.7, 2016-06-06

- Compile with GHC-8.0. Plugin at least requires GHC-8.0.1 and SBV 5.12
- Fix a few dead links

### Version 0.6, 2016-01-01

- Support for list expressions of the form [x .. y] and [x, y .. z]; so long as the x, y, and z are all concrete.
- Simplify some of the expressions in BitTricks using the new list-construction support.
- Added more proofs to the BitTricks example

### Version 0.5, 2015-12-26

- Allow higher-order (i.e., function) arguments to theorems.
- Rework uninterpreted functions, generalize types
- Simplify cabal file; no need to ship gold-files for tests
- Add merge-sort example "Data/SBV/Plugin/Examples/MergeSort.hs"
- Add bit-tricks example "Data/SBV/Plugin/Examples/BitTricks.hs"

### Version 0.4, 2015-12-24

- Support for case-alternatives producing lists/tuples and functions. In the list case, we require that both alternatives produce equal-length lists, as otherwise there is no way to merge the two results.
- More test cases.

### Version 0.3, 2015-12-21

- Added the micro-controller example, adapted from the original SBV variant by Anthony Cowley: http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf
- Add the "skip" option for the plugin itself. Handy when compiling the plugin itself!

### Version 0.2, 2015-12-21

- Further fleshing of internals
- Support for case-expressions
- Support for uninterpreted types/functions
- Lots of test cases, refactoring.

### Version 0.1, 2015-12-06

- Basic functionality. Initial design exploration.
- The plugin functional on base values, but there are a lot of rough edges around the details. Please report any issues you might find!