-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Formally prove properties of Haskell programs using SBV/SMT
--   
--   GHC plugin for proving properties over Haskell functions using SMT
--   solvers, based on the <a>SBV</a> package.
--   
--   See <a>Data.SBV.Plugin</a> for a quick example, or the modules under
--   <a>Data.SBV.Plugin.Examples</a> for more details.
@package sbvPlugin
@version 9.2.2


-- | Internal data-structures for the sbvPlugin
module Data.SBV.Plugin.Data

-- | Plugin options. Note that we allow picking multiple solvers, which
--   will all be run in parallel. You can pick and choose any number of
--   them, or if you want to run all available solvers, then use the option
--   <a>AnySolver</a>. The default behavior is to error-out on failure,
--   using the default-SMT solver picked by SBV, which is currently Z3.
data SBVOption

-- | Continue even if proof fails
IgnoreFailure :: SBVOption

-- | Skip the proof. Can be handy for properties that we currently do not
--   want to focus on.
Skip :: String -> SBVOption

-- | Produce verbose output, good for debugging
Verbose :: SBVOption

-- | Produce really verbose output, use only when things go really wrong!
Debug :: SBVOption

-- | Perform quickCheck
QuickCheck :: SBVOption

-- | Uninterpret this binding for proof purposes
Uninterpret :: SBVOption

-- | Use these names for the arguments; need not be exhaustive
Names :: [String] -> SBVOption

-- | If a list-input is found, use this length. If not specified, we will
--   complain!
ListSize :: Int -> SBVOption

-- | Use Z3
Z3 :: SBVOption

-- | Use Yices
Yices :: SBVOption

-- | Use Boolector
Boolector :: SBVOption

-- | Use CVC4
CVC4 :: SBVOption

-- | Use MathSAT
MathSAT :: SBVOption

-- | Use ABC
ABC :: SBVOption

-- | Run all installed solvers in parallel, and report the result from the
--   first to finish
AnySolver :: SBVOption

-- | The actual annotation.
newtype SBVAnnotation
SBV :: [SBVOption] -> SBVAnnotation
[options] :: SBVAnnotation -> [SBVOption]

-- | A property annotation, using default options.
sbv :: SBVAnnotation

-- | Synonym for sbv really, just looks cooler
theorem :: SBVAnnotation

-- | Importable type as an annotation alternative
type Proved a = a
instance Data.Data.Data Data.SBV.Plugin.Data.SBVOption
instance GHC.Classes.Eq Data.SBV.Plugin.Data.SBVOption
instance GHC.Show.Show Data.SBV.Plugin.Data.SBVOption
instance Data.Data.Data Data.SBV.Plugin.Data.SBVAnnotation
instance GHC.Classes.Eq Data.SBV.Plugin.Data.SBVAnnotation


-- | (The sbvPlugin is hosted at
--   <a>http://github.com/LeventErkok/sbvPlugin</a>. Comments, bug reports,
--   and patches are always welcome.)
--   
--   <h2>SBVPlugin: A GHC Plugin for SBV, SMT Based Verification</h2>
--   
--   <a>SBV</a> is a library for express properties about Haskell programs
--   and automatically proving them using SMT solvers. The SBVPlugin allows
--   simple annotations on Haskell functions to prove them directly during
--   GHC compilation time.
--   
--   <h3><i>Example</i></h3>
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
--   
--   module Test where
--   
--   import Data.SBV.Plugin
--   
--   {-# ANN test theorem #-}
--   test :: Integer -&gt; Integer -&gt; Bool
--   test x y = x + y &gt;= x - y
--   </pre>
--   
--   When compiled via GHC or loaded into GHCi, we get:
--   
--   <pre>
--   [SBV] Test.hs:9:1-4 Proving "test", using Z3.
--   [Z3] Falsifiable. Counter-example:
--     x =  0 :: Integer
--     y = -1 :: Integer
--   [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
--   </pre>
--   
--   Note that the compilation will be aborted, since the theorem doesn't
--   hold. As shown in the hint, GHC can be instructed to continue in that
--   case, using an annotation of the form:
--   
--   <pre>
--   {-# ANN test theorem {options = [IgnoreFailure]} #-}
--   </pre>
--   
--   <h3><i>Using the plugin from GHCi</i></h3>
--   
--   The plugin should work from GHCi with no changes. Note that when run
--   from GHCi, the plugin will behave as if the <tt>IgnoreFailure</tt>
--   option is given on all annotations, so that failures do not stop the
--   load process.
--   
--   <h3><i>Plugin order</i></h3>
--   
--   By default, sbvPlugin runs before GHCs optimizer passes. While the
--   order of the run should not matter in general, the simplifier can
--   rearrange the core in various ways that can have an impact on the
--   verification conditions generated by the plugin. As an experiment, you
--   can pass the argument <tt>runLast</tt> to the plugin to see if it
--   makes any difference, using the following argument to GHC:
--   
--   <pre>
--   -fplugin-opt Data.SBV.Plugin:runLast
--   </pre>
--   
--   Please report if you find any crucial differences when the plugin is
--   run first or last, especially if the outputs are different.
module Data.SBV.Plugin

-- | Entry point to the plugin
plugin :: Plugin

-- | The actual annotation.
newtype SBVAnnotation
SBV :: [SBVOption] -> SBVAnnotation
[options] :: SBVAnnotation -> [SBVOption]

-- | A property annotation, using default options.
sbv :: SBVAnnotation

-- | Synonym for sbv really, just looks cooler
theorem :: SBVAnnotation

-- | Plugin options. Note that we allow picking multiple solvers, which
--   will all be run in parallel. You can pick and choose any number of
--   them, or if you want to run all available solvers, then use the option
--   <a>AnySolver</a>. The default behavior is to error-out on failure,
--   using the default-SMT solver picked by SBV, which is currently Z3.
data SBVOption

-- | Continue even if proof fails
IgnoreFailure :: SBVOption

-- | Skip the proof. Can be handy for properties that we currently do not
--   want to focus on.
Skip :: String -> SBVOption

-- | Produce verbose output, good for debugging
Verbose :: SBVOption

-- | Produce really verbose output, use only when things go really wrong!
Debug :: SBVOption

-- | Perform quickCheck
QuickCheck :: SBVOption

-- | Uninterpret this binding for proof purposes
Uninterpret :: SBVOption

-- | Use these names for the arguments; need not be exhaustive
Names :: [String] -> SBVOption

-- | If a list-input is found, use this length. If not specified, we will
--   complain!
ListSize :: Int -> SBVOption

-- | Use Z3
Z3 :: SBVOption

-- | Use Yices
Yices :: SBVOption

-- | Use Boolector
Boolector :: SBVOption

-- | Use CVC4
CVC4 :: SBVOption

-- | Use MathSAT
MathSAT :: SBVOption

-- | Use ABC
ABC :: SBVOption

-- | Run all installed solvers in parallel, and report the result from the
--   first to finish
AnySolver :: SBVOption

-- | Importable type as an annotation alternative
type Proved a = a


-- | A transcription of Anthony Cowley's MicroController example, using the
--   SBV plugin. For the original, see:
--   <a>http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf</a>
module Data.SBV.Plugin.Examples.MicroController

-- | The range detector must output if the range is larger than this
--   amount.
safetyDistance :: Int

-- | The range detector must have sent an output before this many cycles
--   have past.
maxTimeSince :: Int

-- | Given a last-signal-time calculator, named <tt>calculate</tt>, check
--   that it satisfies the following three requirements: We must've just
--   sent a signal if:
--   
--   <ul>
--   <li><i>minRate</i>: The last-time we sent is strictly less than the
--   <a>maxTimeSince</a> amount</li>
--   <li><i>minRange</i>: We must've just sent a signal if the range is
--   beyond <a>safetyDistance</a></li>
--   <li><i>manualOverride</i>: We must've just sent a signal if the
--   manual-override is specified</li>
--   </ul>
checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool

-- | A "bad" implementation, see if you can spot the problem with it,
--   before looking at the failed theorem below!
computeLastBad :: Int -> Bool -> Int -> Int

-- | Using SBV, prove that the <a>computeLastBad</a> is indeed a bad
--   implementation. Here's the output we get from the plugin:
--   
--   <pre>
--   [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3.
--   [Z3] Falsifiable. Counter-example:
--     range     =     0 :: Int64
--     manual    = False :: Bool
--     timeSince =     9 :: Int64
--   </pre>
--   
--   We're being told that if the range is 0, and manual override is off,
--   and time-since last is 9, then our "calculator" returns 10. But that
--   violates the <tt>minRate</tt> requirement, since we never want to go
--   <a>maxTimeSince</a> cycles without sending a signal!
checkBad :: Int -> Bool -> Int -> Bool

-- | A "good" implementation, properly handling the off-by-one error of the
--   original.
computeLastGood :: Int -> Bool -> Int -> Int

-- | We now verify that the good variant is indeed good. We have:
--   
--   <pre>
--   [SBV] MicroController.hs:108:1-9 Proving "checkGood", using Z3.
--   [Z3] Q.E.D.
--   </pre>
checkGood :: Proved (Int -> Bool -> Int -> Bool)


-- | An implementation of merge-sort and its correctness.
module Data.SBV.Plugin.Examples.MergeSort

-- | Merging two given sorted lists, preserving the order.
merge :: Ord a => [a] -> [a] -> [a]

-- | Simple merge-sort implementation.
mergeSort :: Ord a => [a] -> [a]

-- | Check whether a given sequence is non-decreasing.
nonDecreasing :: Ord a => [a] -> Bool

-- | Check whether two given sequences are permutations. We simply check
--   that each sequence is a subset of the other, when considered as a set.
--   The check is slightly complicated for the need to account for possibly
--   duplicated elements.
isPermutationOf :: Eq a => [a] -> [a] -> Bool

-- | Asserting correctness of merge-sort for a list of the given size. Note
--   that we can only check correctness for fixed-size lists. Also, the
--   proof will get more and more complicated for the backend SMT solver as
--   <tt>n</tt> increases. Here we try it with 4.
--   
--   We have:
--   
--   <pre>
--   [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3.
--   [Z3] Q.E.D.
--   </pre>
mergeSortCorrect :: [Int] -> Bool


-- | Shows that a naive definition of maximum doing bit-vector arithmetic
--   is incorrect.
module Data.SBV.Plugin.Examples.Maximum

-- | Compute the maximum of three integers, which is intuitively correct
--   for unbounded values, but not for bounded bit-vectors.
myMax :: Int -> Int -> Int -> Int

-- | Show that this function fails to compute maximum correctly. We have:
--   
--   <pre>
--   [SBV] a.hs:11:1-7 Proving "correct", using Z3.
--   [Z3] Falsifiable. Counter-example:
--     x = -2816883406898309583 :: Int64
--     y = -2816883406898309583 :: Int64
--     z =  6694719001794338309 :: Int64
--   </pre>
correct :: Proved (Int -> Int -> Int -> Bool)


-- | Checks the correctness of a few tricks from the large collection found
--   in: <a>https://graphics.stanford.edu/~seander/bithacks.html</a>
module Data.SBV.Plugin.Examples.BitTricks

-- | SBVPlugin can only see definitions in the current module. So we define
--   <a>elem</a> ourselves.
elem :: Eq a => a -> [a] -> Bool

-- | Returns 1 if bool is <tt>True</tt>
oneIf :: Num a => Bool -> a

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax</a>
fastMinCorrect :: Proved (Int -> Int -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax</a>
fastMaxCorrect :: Proved (Int -> Int -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns</a>
oppositeSignsCorrect :: Proved (Int -> Int -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching</a>
conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2</a>
powerOfTwoCorrect :: Proved (Word32 -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge</a>
maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2</a>
roundPowerOfTwoCorrect :: Proved (Word32 -> Bool)

-- | Formalizes
--   <a>https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord</a>
zeroInWord :: Proved (Word32 -> Bool)