sbvPlugin: Formally prove properties of Haskell programs using SBV/SMT

[ bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ] [ Propose Tags ]

GHC plugin for proving properties over Haskell functions using SMT solvers, based on the SBV package.

See Data.SBV.Plugin for a quick example, or the modules under Data.SBV.Plugin.Examples for more details.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 0.10, 0.11, 0.12, 9.0.1, 9.2.2, 9.4.4, 9.6.1, 9.8.1, 9.8.2 (info)
Change log CHANGES.md
Dependencies base (>=4.19 && <5), containers, ghc (>=9.8.2), ghc-prim, mtl, sbv (>=10.7), template-haskell [details]
License BSD-3-Clause
Author Levent Erkok
Maintainer Levent Erkok (erkokl@gmail.com)
Category Formal methods, Theorem provers, Math, SMT, Symbolic Computation
Home page http://github.com/LeventErkok/sbvPlugin
Bug tracker http://github.com/LeventErkok/sbvPlugin/issues
Source repo head: git clone git://github.com/LeventErkok/sbvPlugin.git
Uploaded by LeventErkok at 2024-03-23T21:48:42Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 6098 total (52 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for sbvPlugin-9.8.2

[back to package description]

SBVPlugin: SBV Plugin for GHC

On Hackage: http://hackage.haskell.org/package/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 proofs (IgnoreFailure). This is useful when you have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping compilation and erroring out 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.