sbv 11.6 → 11.7
raw patch · 54 files changed
+880/−123 lines, 54 filesdep +tree-view
Dependencies added: tree-view
Files
- CHANGES.md +8/−0
- Data/SBV.hs +3/−1
- Data/SBV/Char.hs +3/−1
- Data/SBV/Either.hs +3/−1
- Data/SBV/Internals.hs +3/−1
- Data/SBV/List.hs +3/−1
- Data/SBV/Maybe.hs +3/−1
- Data/SBV/RegExp.hs +3/−1
- Data/SBV/Set.hs +4/−1
- Data/SBV/String.hs +3/−1
- Data/SBV/Tools/BVOptimize.hs +4/−1
- Data/SBV/Tools/KD/Kernel.hs +18/−15
- Data/SBV/Tools/KD/KnuckleDragger.hs +14/−6
- Data/SBV/Tools/KD/Utils.hs +79/−10
- Data/SBV/Tools/KnuckleDragger.hs +3/−0
- Data/SBV/Tools/Overflow.hs +3/−1
- Data/SBV/Tools/Range.hs +3/−1
- Data/SBV/Tuple.hs +3/−1
- Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs +1/−1
- Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs +1/−2
- Documentation/SBV/Examples/BitPrecise/PrefixSum.hs +1/−2
- Documentation/SBV/Examples/CodeGeneration/GCD.hs +1/−2
- Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs +1/−2
- Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs +1/−2
- Documentation/SBV/Examples/Crypto/AES.hs +1/−2
- Documentation/SBV/Examples/Crypto/Prince.hs +1/−2
- Documentation/SBV/Examples/KnuckleDragger/Basics.hs +7/−2
- Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs +1/−1
- Documentation/SBV/Examples/KnuckleDragger/Lists.hs +1/−2
- Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +1/−2
- Documentation/SBV/Examples/KnuckleDragger/QuickSort.hs +661/−0
- Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs +7/−9
- Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +1/−2
- Documentation/SBV/Examples/Misc/Floating.hs +1/−2
- Documentation/SBV/Examples/Misc/Newtypes.hs +1/−2
- Documentation/SBV/Examples/Misc/SetAlgebra.hs +1/−2
- Documentation/SBV/Examples/Optimization/ExtField.hs +1/−2
- Documentation/SBV/Examples/Optimization/LinearOpt.hs +1/−2
- Documentation/SBV/Examples/Optimization/Production.hs +1/−2
- Documentation/SBV/Examples/Optimization/VM.hs +1/−2
- Documentation/SBV/Examples/ProofTools/AddHorn.hs +1/−2
- Documentation/SBV/Examples/Puzzles/Orangutans.hs +1/−2
- Documentation/SBV/Examples/Queries/Interpolants.hs +1/−2
- Documentation/SBV/Examples/Uninterpreted/AUF.hs +1/−2
- Documentation/SBV/Examples/Uninterpreted/Function.hs +1/−2
- Documentation/SBV/Examples/Uninterpreted/Multiply.hs +1/−2
- Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs +1/−2
- Documentation/SBV/Examples/WeakestPreconditions/Basics.hs +1/−2
- Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +1/−2
- Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +1/−2
- Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +1/−2
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- sbv.cabal +7/−5
CHANGES.md view
@@ -1,6 +1,14 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 11.7, 2025-05-16++ * KnuckleDragger: Add a proof of correctness for the quick-sort algorithm.++ * KnuckleDragger: Add methods 'getProofTree' and 'kdShowDepsHTML' to collect and render+ the proof as a dependency tree, unicode or as HTML. Useful for programming+ methods/tactics on top of knuckle-dragger provided facilities.+ ### Version 11.6, 2025-05-10 * Make SBV compile cleanly with GHC 9.8.4. This is really as far back a GHC you should be using,
Data/SBV.hs view
@@ -178,6 +178,7 @@ -- used in the property are terminating. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-}@@ -542,10 +543,11 @@ import Data.Char (isSpace, isPunctuation) +#ifdef DOCTEST --- $setup---- >>> -- For doctest purposes only: --- >>> :set -XDataKinds -XFlexibleContexts -XTypeApplications -XRankNTypes --- >>> import Data.Proxy+#endif -- | Show a value in detailed (cracked) form, if possible. -- This makes most sense with numbers, and especially floating-point types.
Data/SBV/Char.hs view
@@ -21,6 +21,7 @@ -- we will provide full unicode versions as well. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -53,12 +54,13 @@ import Data.SBV.String (isInfixOf, singleton) +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.String (isInfixOf, singleton) -- >>> import Prelude hiding(elem, notElem) -- >>> :set -XOverloadedStrings+#endif -- | Is the character in the string? --
Data/SBV/Either.hs view
@@ -10,6 +10,7 @@ -- Symbolic coproduct, symbolic version of Haskell's 'Either' type. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -35,10 +36,11 @@ import Data.SBV.Core.Data import Data.SBV.Core.Model () -- instances only +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Prelude hiding(either) -- >>> import Data.SBV+#endif -- | Construct an @SEither a b@ from an @SBV a@ --
Data/SBV/Internals.hs view
@@ -17,6 +17,7 @@ -- is a very good but also a very difficult question to answer!) ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-}@@ -102,10 +103,11 @@ import Data.SBV.Lambda +#ifdef DOCTEST --- $setup---- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables --- >>> import Data.SBV+#endif -- | Send an arbitrary string to the solver in a query. -- Note that this is inherently dangerous as it can put the solver in an arbitrary
Data/SBV/List.hs view
@@ -14,6 +14,7 @@ -- be used as symbolic-lists. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -65,14 +66,15 @@ import Data.Proxy +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem, notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, all, any) -- >>> import qualified Prelude as P(map) -- >>> import Data.SBV -- >>> :set -XDataKinds -- >>> :set -XOverloadedLists -- >>> :set -XScopedTypeVariables+#endif -- | Length of a list. --
Data/SBV/Maybe.hs view
@@ -10,6 +10,7 @@ -- Symbolic option type, symbolic version of Haskell's 'Maybe' type. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-}@@ -37,10 +38,11 @@ import Data.SBV.Core.Data import Data.SBV.Core.Model (ite) +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Prelude hiding (maybe, map) -- >>> import Data.SBV+#endif -- | The symbolic 'Nothing'. --
Data/SBV/RegExp.hs view
@@ -14,6 +14,7 @@ -- this module. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-}@@ -66,14 +67,15 @@ -- For testing only import Data.SBV.Char +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Char -- >>> import Data.SBV.String -- >>> import Prelude hiding (length, take, elem, notElem, head) -- >>> :set -XOverloadedStrings -- >>> :set -XScopedTypeVariables+#endif -- | Matchable class. Things we can match against a 'RegExp'. --
Data/SBV/Set.hs view
@@ -21,6 +21,7 @@ -- it into a list or necessarily enumerate its elements. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -56,11 +57,13 @@ import Data.SBV.Core.Kind +#ifdef DOCTEST -- $setup -- >>> -- For doctest purposes only: -- >>> import Prelude hiding(null) -- >>> import Data.SBV hiding(complement) -- >>> :set -XScopedTypeVariables+#endif -- | Empty set. --@@ -496,7 +499,7 @@ ka = kindOf (Proxy @a) -- | Synonym for 'Data.SBV.Set.difference'.-infixl 9 \\+infixl 9 \\ -- This comment avoids CPP to eat up the trailing backspace in this line Do not remove! (\\) :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a (\\) = difference
Data/SBV/String.hs view
@@ -15,6 +15,7 @@ -- used as symbolic-strings. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -51,11 +52,12 @@ import Data.Proxy +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Prelude hiding (head, tail, init, length, take, drop, concat, null, reverse, (++), (!!)) -- >>> :set -XOverloadedStrings+#endif -- | Length of a string. --
Data/SBV/Tools/BVOptimize.hs view
@@ -16,6 +16,8 @@ -- This implementation is based on an idea by Nikolaj Bjorner, see <https://github.com/Z3Prover/z3/issues/7156>. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-}+ {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Tools.BVOptimize (@@ -32,10 +34,11 @@ import Data.SBV import Data.SBV.Control +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XDataKinds -- >>> import Data.SBV+#endif {- $maxBVEx
Data/SBV/Tools/KD/Kernel.hs view
@@ -69,22 +69,24 @@ -- | Internal axiom generator; so we can keep truck of KnuckleDrugger's trusted axioms, vs. user given axioms. internalAxiom :: Proposition a => String -> a -> Proof-internalAxiom nm p = Proof { rootOfTrust = None- , isUserAxiom = False- , getProof = label nm (quantifiedBool p)- , getProp = toDyn p- , proofName = nm+internalAxiom nm p = Proof { rootOfTrust = None+ , dependencies = []+ , isUserAxiom = False+ , getProof = label nm (quantifiedBool p)+ , getProp = toDyn p+ , proofName = nm } -- | A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver -- cannot deal with, or if we want to postpone the proof for the time being. KnuckleDragger will keep -- track of the uses of 'sorry' and will print them appropriately while printing proofs. sorry :: Proof-sorry = Proof { rootOfTrust = Self- , isUserAxiom = False- , getProof = label "sorry" (quantifiedBool p)- , getProp = toDyn p- , proofName = "sorry"+sorry = Proof { rootOfTrust = Self+ , dependencies = []+ , isUserAxiom = False+ , getProof = label "sorry" (quantifiedBool p)+ , getProp = toDyn p+ , proofName = "sorry" } where -- ideally, I'd rather just use -- p = sFalse@@ -106,11 +108,12 @@ -- What to do if all goes well good mbStart d = do mbElapsed <- getElapsedTime mbStart liftIO $ finishKD cfg ("Q.E.D." ++ modulo) d $ catMaybes [mbElapsed]- pure Proof { rootOfTrust = ros- , isUserAxiom = False- , getProof = label nm (quantifiedBool inputProp)- , getProp = toDyn inputProp- , proofName = nm+ pure Proof { rootOfTrust = ros+ , dependencies = by+ , isUserAxiom = False+ , getProof = label nm (quantifiedBool inputProp)+ , getProp = toDyn inputProp+ , proofName = nm } where (ros, modulo) = calculateRootOfTrust nm by
Data/SBV/Tools/KD/KnuckleDragger.hs view
@@ -29,7 +29,7 @@ {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Tools.KD.KnuckleDragger (- Proposition, Proof, Instantiatable(..), Inst(..)+ Proposition, Proof, Instantiatable(..), Inst(..), getProofTree, kdShowDepsHTML, KDProofDeps(..) , axiom , lemma, lemmaWith , theorem, theoremWith@@ -295,11 +295,12 @@ let (ros, modulo) = calculateRootOfTrust nm (concatMap getHelperProofs (getAllHelpers calcProofTree)) finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed]) - pure Proof { rootOfTrust = ros- , isUserAxiom = False- , getProof = label nm (quantifiedBool result)- , getProp = toDyn result- , proofName = nm+ pure Proof { rootOfTrust = ros+ , dependencies = getDependencies calcProofTree+ , isUserAxiom = False+ , getProof = label nm (quantifiedBool result)+ , getProp = toDyn result+ , proofName = nm } -- Helper data-type for calc-step below@@ -955,6 +956,13 @@ -- | A proof, as processed by KD. Producing a boolean result and each step is a boolean. Helpers on branches dispersed down, only strings are left for printing type KDProof = KDProofGen SBool [String] SBool++-- | Collect dependencies for a KDProof+getDependencies :: KDProof -> [Proof]+getDependencies = collect+ where collect (ProofStep _ hs next) = concatMap getHelperProofs hs ++ collect next+ collect (ProofBranch _ _ bs) = concatMap (collect . snd) bs+ collect (ProofEnd _ hs) = concatMap getHelperProofs hs -- | Class capturing giving a proof-step helper type family Hinted a where
Data/SBV/Tools/KD/Utils.hs view
@@ -21,6 +21,7 @@ KD, runKD, runKDWith, Proof(..) , startKD, finishKD, getKDState, getKDConfig, KDState(..), KDStats(..) , RootOfTrust(..), KDProofContext(..), calculateRootOfTrust, message, updStats+ , KDProofDeps(..), getProofTree, kdShowDepsHTML ) where import Control.Monad.Reader (ReaderT, runReaderT, MonadReader, ask, liftIO)@@ -28,7 +29,11 @@ import Data.Time (NominalDiffTime) -import Data.List (intercalate, nub, sort)+import Data.Tree+import Data.Tree.View++import Data.Char (isSpace)+import Data.List (intercalate, nub, sort, isInfixOf) import System.IO (hFlush, stdout) import Data.SBV.Core.Data (SBool)@@ -142,19 +147,83 @@ -- is still large: The underlying solver, SBV, and KnuckleDragger kernel itself. But this -- mechanism ensures we can't create proven things out of thin air, following the standard LCF -- methodology.)-data Proof = Proof { rootOfTrust :: RootOfTrust -- ^ Root of trust, described above.- , isUserAxiom :: Bool -- ^ Was this an axiom given by the user?- , getProof :: SBool -- ^ Get the underlying boolean- , getProp :: Dynamic -- ^ The actual proposition- , proofName :: String -- ^ User given name+data Proof = Proof { rootOfTrust :: RootOfTrust -- ^ Root of trust, described above.+ , dependencies :: [Proof] -- ^ Immediate dependencies of this proof. (Not transitive)+ , isUserAxiom :: Bool -- ^ Was this an axiom given by the user?+ , getProof :: SBool -- ^ Get the underlying boolean+ , getProp :: Dynamic -- ^ The actual proposition+ , proofName :: String -- ^ User given name } -- | NFData ignores the getProp field instance NFData Proof where- rnf (Proof rootOfTrust isUserAxiom getProof _getProp proofName) = rnf rootOfTrust- `seq` rnf isUserAxiom- `seq` rnf getProof- `seq` rnf proofName+ rnf (Proof rootOfTrust dependencies isUserAxiom getProof _getProp proofName) = rnf rootOfTrust+ `seq` rnf dependencies+ `seq` rnf isUserAxiom+ `seq` rnf getProof+ `seq` rnf proofName++-- | Dependencies of a proof, in a tree format.+data KDProofDeps = KDProofDeps Proof [KDProofDeps]++-- | Return all the proofs this particular proof depends on, transitively+getProofTree :: Proof -> KDProofDeps+getProofTree p = KDProofDeps p $ map getProofTree (dependencies p)++-- | Turn dependencies to a container tree, for display purposes+depsToTree :: [String] -> (String -> Int -> Int -> a) -> (Int, KDProofDeps) -> ([String], Tree a)+depsToTree visited xform (cnt, KDProofDeps top ds) = (nVisited, Node (xform nTop cnt (length chlds)) chlds)+ where nTop = shortName top++ (nVisited, chlds) | nTop `elem` visited = (visited, [])+ | True = walk (nTop : visited) (compress (filter interesting ds))++ walk v [] = (v, [])+ walk v (c:cs) = let (v', t) = depsToTree v xform c+ (v'', ts) = walk v' cs+ in (v'', t : ts)++ -- Don't show IH's, just not interesting+ interesting (KDProofDeps p _) = not ("IH" `isInfixOf` proofName p)++ -- If a proof is used twice in the same proof, compress it+ compress :: [KDProofDeps] -> [(Int, KDProofDeps)]+ compress [] = []+ compress (p : ps) = (1 + length [() | (_, True) <- filtered], p) : compress [d | (d, False) <- filtered]+ where filtered = [(d, shortName p' == curName) | d@(KDProofDeps p' _) <- ps]+ curName = case p of+ KDProofDeps curProof _ -> shortName curProof++ -- Drop the instantiation part+ shortName :: Proof -> String+ shortName p | "@" `isInfixOf` s = reverse . dropWhile isSpace . reverse . takeWhile (/= '@') $ s+ | True = s+ where s = proofName p++-- | Display the dependencies as a tree+instance Show KDProofDeps where+ show d = showTree $ snd $ depsToTree [] sh (1, d)+ where sh nm 1 _ = nm+ sh nm x _= nm ++ " (x" ++ show x ++ ")"++-- | Display the tree as an html doc for rendering purposes.+-- The first argument is Path (or URL) to external CSS file, if needed.+kdShowDepsHTML :: Maybe FilePath -> KDProofDeps -> String+kdShowDepsHTML mbCSS deps = htmlTree mbCSS $ snd $ depsToTree [] nodify (1, deps)+ where nodify :: String -> Int -> Int -> NodeInfo+ nodify nm cnt dc = NodeInfo { nodeBehavior = InitiallyExpanded+ , nodeName = nm+ , nodeInfo = spc (used cnt) ++ depCount dc+ }+ used 1 = ""+ used n = "Used " ++ show n ++ " times."++ spc "" = ""+ spc s = s ++ " "++ depCount 0 = ""+ depCount 1 = "Has one dependency."+ depCount n = "Has " ++ show n ++ " dependencies." -- | Show instance for t'Proof' instance Show Proof where
Data/SBV/Tools/KnuckleDragger.hs view
@@ -19,6 +19,9 @@ -- * Propositions and their proofs Proposition, Proof + -- * Getting the proof tree+ , KDProofDeps(), getProofTree, kdShowDepsHTML+ -- * Adding axioms/definitions , axiom
Data/SBV/Tools/Overflow.hs view
@@ -10,6 +10,7 @@ -- Based on: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf> ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}@@ -48,9 +49,10 @@ import Data.Word import Data.Proxy +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV+#endif -- | Detecting overflow. Each function here will return 'sTrue' if the result will not fit in the target -- type, i.e., if it overflows or underflows.
Data/SBV/Tools/Range.hs view
@@ -9,6 +9,7 @@ -- Single variable valid range detection. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -32,10 +33,11 @@ import Data.SBV.Internals hiding (Range, free_) +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> :set -XScopedTypeVariables -XDataKinds+#endif -- | A boundary value data Boundary a = Unbounded -- ^ Unbounded
Data/SBV/Tuple.hs view
@@ -10,6 +10,7 @@ -- Accessing symbolic tuple fields and deconstruction. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}@@ -42,10 +43,11 @@ import Prelude hiding (fst, snd) +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XTypeApplications -- >>> import Data.SBV+#endif -- | Field access, inspired by the lens library. This is merely reverse -- application, but allows us to write things like @(1, 2)^._1@ which is
Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs view
@@ -19,7 +19,7 @@ import Data.SBV import Data.SBV.Tools.Overflow -#ifndef HADDOCK+#ifdef DOCTEST -- $setup -- >>> import Data.SBV -- >>> import Data.Int
Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs view
@@ -48,9 +48,8 @@ import Data.SBV import GHC.TypeLits (KnownNat) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> :set -XDataKinds -XTypeApplications #endif
Documentation/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -22,9 +22,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/CodeGeneration/GCD.hs view
@@ -22,9 +22,8 @@ import Data.SBV import Data.SBV.Tools.CodeGen -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Tools.CodeGen #endif
Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -19,9 +19,8 @@ import Data.SBV import Data.SBV.Tools.CodeGen -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs view
@@ -25,9 +25,8 @@ import Data.SBV import Data.SBV.Tools.CodeGen -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Crypto/AES.hs view
@@ -52,9 +52,8 @@ import Test.QuickCheck hiding (verbose) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Crypto/Prince.hs view
@@ -24,9 +24,8 @@ import Data.SBV import Data.SBV.Tools.CodeGen -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/KnuckleDragger/Basics.hs view
@@ -25,13 +25,14 @@ import Data.SBV import Data.SBV.Tools.KnuckleDragger -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception #endif +-- * Truth and falsity+ -- | @sTrue@ is provable. -- -- We have:@@ -55,6 +56,8 @@ _won'tGoThrough <- lemma "sFalse" sFalse [] pure () +-- * Quantification+ -- | Basic quantification example: For every integer, there's a larger integer. -- -- We have:@@ -69,6 +72,8 @@ -- | Use an uninterpreted type for the domain data T mkUninterpretedSort ''T++-- * Basic connectives -- | Pushing a universal through conjunction. We have: --
Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs view
@@ -194,7 +194,7 @@ ] -- Prove the case when the target is in the array- bsearchPresent <- sInductWith cvc5 "bsearchPresent"+ bsearchPresent <- sInduct "bsearchPresent" (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"x" x) -> nonDecreasing arr (lo, hi) .&& inArray arr (lo, hi) x .=> arr `readArray` fromJust (bsearch arr (lo, hi) x) .== x) (\(_arr :: Arr) (lo :: SInteger) (hi :: SInteger) (_x :: SInteger) -> abs (hi - lo + 1)) $
Documentation/SBV/Examples/KnuckleDragger/Lists.hs view
@@ -35,9 +35,8 @@ import Control.Monad (void) import Data.Proxy -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> :set -XTypeApplications -- >>> import Data.SBV
Documentation/SBV/Examples/KnuckleDragger/Numeric.hs view
@@ -24,9 +24,8 @@ import Data.SBV import Data.SBV.Tools.KnuckleDragger -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception #endif
+ Documentation/SBV/Examples/KnuckleDragger/QuickSort.hs view
@@ -0,0 +1,661 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.KnuckleDragger.QuickSort+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Proving quick sort correct. The proof here closely follows the development+-- given by Tobias Nipkow, in his paper "Term Rewriting and Beyond -- Theorem+-- Proving in Isabelle," published in Formal Aspects of Computing 1: 320-338+-- back in 1989.+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.KnuckleDragger.QuickSort where++import Prelude hiding (null, length, (++), tail, all, fst, snd, elem)+import Control.Monad.Trans (liftIO)++import Data.SBV+import Data.SBV.List hiding (partition)+import Data.SBV.Tuple+import Data.SBV.Tools.KnuckleDragger++-- * Quick sort++-- | Quick-sort, using the first element as pivot.+quickSort :: SList Integer -> SList Integer+quickSort = smtFunction "quickSort" $ \l -> ite (null l)+ nil+ (let (x, xs) = uncons l+ (lo, hi) = untuple (partition x xs)+ in quickSort lo ++ singleton x ++ quickSort hi)++-- | We define @partition@ as an explicit function. Unfortunately, we can't just replace this+-- with @\pivot xs -> Data.List.SBV.partition (.< pivot) xs@ because that would create a firstified version of partition+-- with a free-variable captured, which isn't supported due to higher-order limitations in SMTLib.+partition :: SInteger -> SList Integer -> STuple [Integer] [Integer]+partition = smtFunction "partition" $ \pivot xs -> ite (null xs)+ (tuple (nil, nil))+ (let (a, as) = uncons xs+ (lo, hi) = untuple (partition pivot as)+ in ite (a .< pivot)+ (tuple (a .: lo, hi))+ (tuple (lo, a .: hi)))++-- * Helper functions++-- | A predicate testing whether a given list is non-decreasing.+nonDecreasing :: SList Integer -> SBool+nonDecreasing = smtFunction "nonDecreasing" $ \l -> null l .|| null (tail l)+ .|| let (x, l') = uncons l+ (y, _) = uncons l'+ in x .<= y .&& nonDecreasing l'++-- | Count the number of occurrences of an element in a list+count :: SInteger -> SList Integer -> SInteger+count = smtFunction "count" $ \e l -> ite (null l)+ 0+ (let (x, xs) = uncons l+ cxs = count e xs+ in ite (e .== x) (1 + cxs) cxs)++-- | Are two lists permutations of each other?+isPermutation :: SList Integer -> SList Integer -> SBool+isPermutation xs ys = quantifiedBool (\(Forall @"x" x) -> count x xs .== count x ys)++-- * Correctness proof++-- | Correctness of quick-sort.+--+-- We have:+--+-- >>> correctness+-- Inductive lemma: lltCorrect+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: lgeCorrect+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: countNonNegative+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: countElem+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: elemCount+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: sublistCorrect+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Lemma: sublistElem+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Lemma: sublistTail Q.E.D.+-- Lemma: permutationImpliesSublist Q.E.D.+-- Inductive lemma: lltSublist+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- Lemma: lltPermutation+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: lgeSublist+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- Lemma: lgePermutation+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: partitionFstLT+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (push llt down) Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: partitionSndGE+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (push lge down) Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): partitionNotLongerFst+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 (simplify) Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): partitionNotLongerSnd+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 (simplify) Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: countAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (unfold count) Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 (simplify) Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: countPartition+-- Step: Base Q.E.D.+-- Step: 1 (expand partition) Q.E.D.+-- Step: 2 (push countTuple down) Q.E.D.+-- Step: 3 (2 way case split)+-- Step: 3.1.1 Q.E.D.+-- Step: 3.1.2 (simplify) Q.E.D.+-- Step: 3.1.3 Q.E.D.+-- Step: 3.2.1 Q.E.D.+-- Step: 3.2.2 (simplify) Q.E.D.+-- Step: 3.2.3 Q.E.D.+-- Step: 3.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): sortCountsMatch+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 (expand quickSort) Q.E.D.+-- Step: 1.2.3 (push count down) Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.2.5 Q.E.D.+-- Step: 1.2.6 (IH on lo) Q.E.D.+-- Step: 1.2.7 (IH on hi) Q.E.D.+-- Step: 1.2.8 Q.E.D.+-- Result: Q.E.D.+-- Lemma: sortIsPermutation Q.E.D.+-- Inductive lemma: nonDecreasingMerge+-- Step: Base Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): sortIsNonDecreasing+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 (expand quickSort) Q.E.D.+-- Step: 1.2.3 (push nonDecreasing down) Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Result: Q.E.D.+-- Lemma: quickSortIsCorrect Q.E.D.+-- == Dependencies:+-- quickSortIsCorrect+-- ├╴sortIsPermutation+-- │ └╴sortCountsMatch+-- │ ├╴countAppend (x2)+-- │ ├╴partitionNotLongerFst+-- │ ├╴partitionNotLongerSnd+-- │ └╴countPartition+-- └╴sortIsNonDecreasing+-- ├╴partitionNotLongerFst+-- ├╴partitionNotLongerSnd+-- ├╴partitionFstLT+-- ├╴partitionSndGE+-- ├╴sortIsPermutation (x2)+-- ├╴lltPermutation+-- │ ├╴lltSublist+-- │ │ ├╴sublistElem+-- │ │ │ └╴sublistCorrect+-- │ │ │ ├╴countElem+-- │ │ │ │ └╴countNonNegative+-- │ │ │ └╴elemCount+-- │ │ ├╴lltCorrect+-- │ │ └╴sublistTail+-- │ └╴permutationImpliesSublist+-- ├╴lgePermutation+-- │ ├╴lgeSublist+-- │ │ ├╴sublistElem+-- │ │ ├╴lgeCorrect+-- │ │ └╴sublistTail+-- │ └╴permutationImpliesSublist+-- └╴nonDecreasingMerge+-- [Proven] quickSortIsCorrect+correctness :: IO Proof+correctness = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 60}} $ do++ ---------------------------------------------------------------------------------------------------+ -- Part I. Formalizing less-than/greater-than-or-equal over lists and relationship to permutations+ ---------------------------------------------------------------------------------------------------+ -- llt: list less-than: all the elements are < pivot+ -- lge: list greater-equal: all the elements are >= pivot+ let llt, lge :: SInteger -> SList Integer -> SBool+ llt = smtFunction "llt" $ \pivot l -> null l .|| let (x, xs) = uncons l in x .< pivot .&& llt pivot xs+ lge = smtFunction "lge" $ \pivot l -> null l .|| let (x, xs) = uncons l in x .>= pivot .&& lge pivot xs++ -- Sublist relationship+ sublist :: SList Integer -> SList Integer -> SBool+ sublist xs ys = quantifiedBool (\(Forall @"e" e) -> count e xs .> 0 .=> count e ys .> 0)++ -- llt correctness+ lltCorrect <-+ induct "lltCorrect"+ (\(Forall @"xs" xs) (Forall @"e" e) (Forall @"pivot" pivot) -> llt pivot xs .&& e `elem` xs .=> e .< pivot) $+ \ih x xs e pivot -> [llt pivot (x .: xs), e `elem` (x .: xs)]+ |- e .< pivot+ ?? ih+ =: sTrue+ =: qed++ -- lge correctness+ lgeCorrect <-+ induct "lgeCorrect"+ (\(Forall @"xs" xs) (Forall @"e" e) (Forall @"pivot" pivot) -> lge pivot xs .&& e `elem` xs .=> e .>= pivot) $+ \ih x xs e pivot -> [lge pivot (x .: xs), e `elem` (x .: xs)]+ |- e .>= pivot+ ?? ih+ =: sTrue+ =: qed++ -- count is always non-negative+ countNonNegative <- induct "countNonNegative"+ (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .>= 0) $+ \ih x xs e -> [] |- count e (x .: xs) .>= 0+ =: cases [ e .== x ==> 1 + count e xs .>= 0+ ?? ih+ =: sTrue+ =: qed+ , e ./= x ==> count e xs .>= 0+ ?? ih+ =: sTrue+ =: qed+ ]++ -- relationship between count and elem, forward direction+ countElem <- induct "countElem"+ (\(Forall @"xs" xs) (Forall @"e" e) -> e `elem` xs .=> count e xs .> 0) $+ \ih x xs e -> [e `elem` (x .: xs)]+ |- count e (x .: xs) .> 0+ =: cases [ e .== x ==> 1 + count e xs .> 0+ ?? countNonNegative+ =: sTrue+ =: qed+ , e ./= x ==> count e xs .> 0+ ?? ih+ =: sTrue+ =: qed+ ]++ -- relationship between count and elem, backwards direction+ elemCount <- induct "elemCount"+ (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .> 0 .=> e `elem` xs) $+ \ih x xs e -> [count e xs .> 0]+ |- e `elem` (x .: xs)+ =: cases [ e .== x ==> trivial+ , e ./= x ==> e `elem` xs+ ?? ih+ =: sTrue+ =: qed+ ]++ -- sublist correctness+ sublistCorrect <- calc "sublistCorrect"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"x" x) -> xs `sublist` ys .&& x `elem` xs .=> x `elem` ys) $+ \xs ys x -> [xs `sublist` ys, x `elem` xs]+ |- x `elem` ys+ ?? [ countElem `at` (Inst @"xs" xs, Inst @"e" x)+ , elemCount `at` (Inst @"xs" ys, Inst @"e" x)+ ]+ =: sTrue+ =: qed++ -- If one list is a sublist of another, then its head is an elem+ sublistElem <- calc "sublistElem"+ (\(Forall @"x" x) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) `sublist` ys .=> x `elem` ys) $+ \x xs ys -> [(x .: xs) `sublist` ys]+ |- x `elem` ys+ ?? sublistCorrect `at` (Inst @"xs" (x .: xs), Inst @"ys" ys, Inst @"x" x)+ =: sTrue+ =: qed++ -- If one list is a sublist of another so is its tail+ sublistTail <- lemma "sublistTail"+ (\(Forall @"x" x) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) `sublist` ys .=> xs `sublist` ys)+ []++ -- Permutation implies sublist+ permutationImpliesSublist <- lemma "permutationImpliesSublist"+ (\(Forall @"xs" xs) (Forall @"ys" ys) -> isPermutation xs ys .=> xs `sublist` ys)+ []++ -- If a value is less than all the elements in a list, then it is also less than all the elements of any sublist of it+ lltSublist <-+ inductWith cvc5 "lltSublist"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"ys" ys) -> llt pivot ys .&& xs `sublist` ys .=> llt pivot xs) $+ \ih x xs pivot ys -> [llt pivot ys, (x .: xs) `sublist` ys]+ |- llt pivot (x .: xs)+ =: x .< pivot .&& llt pivot xs+ ?? [ -- To establish x .< pivot, observe that x is in ys, and together+ -- with llt pivot ys, we get that x is less than pivot+ sublistElem `at` (Inst @"x" x, Inst @"xs" xs, Inst @"ys" ys)+ , lltCorrect `at` (Inst @"xs" ys, Inst @"e" x, Inst @"pivot" pivot)++ -- Use induction hypothesis to get rid of the second conjunct. We need to tell+ -- the prover that xs is a sublist of ys too so it can satisfy its precondition+ , sublistTail `at` (Inst @"x" x, Inst @"xs" xs, Inst @"ys" ys)+ , ih `at` (Inst @"pivot" pivot, Inst @"ys" ys)+ ]+ =: sTrue+ =: qed++ -- Variant of the above for the permutation case+ lltPermutation <-+ calc "lltPermutation"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"ys" ys) -> llt pivot ys .&& isPermutation xs ys .=> llt pivot xs) $+ \xs pivot ys -> [llt pivot ys, isPermutation xs ys]+ |- llt pivot xs+ ?? [ lltSublist `at` (Inst @"xs" xs, Inst @"pivot" pivot, Inst @"ys" ys)+ , permutationImpliesSublist `at` (Inst @"xs" xs, Inst @"ys" ys)+ ]+ =: sTrue+ =: qed++ -- If a value is greater than or equal to all the elements in a list, then it is also less than all the elements of any sublist of it+ lgeSublist <-+ inductWith cvc5 "lgeSublist"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"ys" ys) -> lge pivot ys .&& xs `sublist` ys .=> lge pivot xs) $+ \ih x xs pivot ys -> [lge pivot ys, (x .: xs) `sublist` ys]+ |- lge pivot (x .: xs)+ =: x .>= pivot .&& lge pivot xs+ ?? [ -- To establish x .>= pivot, observe that x is in ys, and together+ -- with lge pivot ys, we get that x is greater than equal to the pivot+ sublistElem `at` (Inst @"x" x, Inst @"xs" xs, Inst @"ys" ys)+ , lgeCorrect `at` (Inst @"xs" ys, Inst @"e" x, Inst @"pivot" pivot)++ -- Use induction hypothesis to get rid of the second conjunct. We need to tell+ -- the prover that xs is a sublist of ys too so it can satisfy its precondition+ , sublistTail `at` (Inst @"x" x, Inst @"xs" xs, Inst @"ys" ys)+ , ih `at` (Inst @"pivot" pivot, Inst @"ys" ys)+ ]+ =: sTrue+ =: qed++ -- Variant of the above for the permutation case+ lgePermutation <-+ calc "lgePermutation"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"ys" ys) -> lge pivot ys .&& isPermutation xs ys .=> lge pivot xs) $+ \xs pivot ys -> [lge pivot ys, isPermutation xs ys]+ |- lge pivot xs+ ?? [ lgeSublist `at` (Inst @"xs" xs, Inst @"pivot" pivot, Inst @"ys" ys)+ , permutationImpliesSublist `at` (Inst @"xs" xs, Inst @"ys" ys)+ ]+ =: sTrue+ =: qed++ --------------------------------------------------------------------------------------------+ -- Part II. Helper lemmas for partition+ --------------------------------------------------------------------------------------------++ -- The first element of the partition produces all smaller elements+ partitionFstLT <- inductWith cvc5 "partitionFstLT"+ (\(Forall @"l" l) (Forall @"pivot" pivot) -> llt pivot (fst (partition pivot l))) $+ \ih a as pivot -> [] |- llt pivot (fst (partition pivot (a .: as)))+ =: llt pivot (ite (a .< pivot)+ (a .: fst (partition pivot as))+ ( fst (partition pivot as)))+ ?? "push llt down"+ =: ite (a .< pivot)+ (a .< pivot .&& llt pivot (fst (partition pivot as)))+ ( llt pivot (fst (partition pivot as)))+ ?? ih+ =: sTrue+ =: qed++ -- The second element of the partition produces all greater-than-or-equal to elements+ partitionSndGE <- inductWith cvc5 "partitionSndGE"+ (\(Forall @"l" l) (Forall @"pivot" pivot) -> lge pivot (snd (partition pivot l))) $+ \ih a as pivot -> [] |- lge pivot (snd (partition pivot (a .: as)))+ =: lge pivot (ite (a .< pivot)+ ( snd (partition pivot as))+ (a .: snd (partition pivot as)))+ ?? "push lge down"+ =: ite (a .< pivot)+ (a .< pivot .&& lge pivot (snd (partition pivot as)))+ ( lge pivot (snd (partition pivot as)))+ ?? ih+ =: sTrue+ =: qed++ -- The first element of partition does not increase in size+ partitionNotLongerFst <- sInduct "partitionNotLongerFst"+ (\(Forall @"l" l) (Forall @"pivot" pivot) -> length (fst (partition pivot l)) .<= length l)+ (\l (_ :: SInteger) -> length @Integer l) $+ \ih l pivot -> [] |- length (fst (partition pivot l)) .<= length l+ =: split l trivial+ (\a as -> let lo = fst (partition pivot as)+ in ite (a .< pivot)+ (length (a .: lo) .<= length (a .: as))+ (length lo .<= length (a .: as))+ ?? "simplify"+ =: ite (a .< pivot)+ (length lo .<= length as)+ (length lo .<= 1 + length as)+ ?? ih `at` (Inst @"l" as, Inst @"pivot" pivot)+ =: sTrue+ =: qed)++ -- The second element of partition does not increase in size+ partitionNotLongerSnd <- sInduct "partitionNotLongerSnd"+ (\(Forall @"l" l) (Forall @"pivot" pivot) -> length (snd (partition pivot l)) .<= length l)+ (\l (_ :: SInteger) -> length @Integer l) $+ \ih l pivot -> [] |- length (snd (partition pivot l)) .<= length l+ =: split l trivial+ (\a as -> let hi = snd (partition pivot as)+ in ite (a .< pivot)+ (length hi .<= length (a .: as))+ (length (a .: hi) .<= length (a .: as))+ ?? "simplify"+ =: ite (a .< pivot)+ (length hi .<= 1 + length as)+ (length hi .<= length as)+ ?? ih `at` (Inst @"l" as, Inst @"pivot" pivot)+ =: sTrue+ =: qed)++ --------------------------------------------------------------------------------------------+ -- Part III. Helper lemmas for count+ --------------------------------------------------------------------------------------------++ -- Count distributes over append+ countAppend <-+ induct "countAppend"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"e" e) -> count e (xs ++ ys) .== count e xs + count e ys) $+ \ih x xs ys e -> [] |- count e ((x .: xs) ++ ys)+ =: count e (x .: (xs ++ ys))+ ?? "unfold count"+ =: (let r = count e (xs ++ ys) in ite (e .== x) (1+r) r)+ ?? ih `at` (Inst @"ys" ys, Inst @"e" e)+ =: (let r = count e xs + count e ys in ite (e .== x) (1+r) r)+ ?? "simplify"+ =: count e (x .: xs) + count e ys+ =: qed++ -- Count is preserved over partition+ let countTuple :: SInteger -> STuple [Integer] [Integer] -> SInteger+ countTuple e xsys = count e xs + count e ys+ where (xs, ys) = untuple xsys++ countPartition <-+ induct "countPartition"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"e" e) -> countTuple e (partition pivot xs) .== count e xs) $+ \ih a as pivot e ->+ [] |- countTuple e (partition pivot (a .: as))+ ?? "expand partition"+ =: countTuple e (let (lo, hi) = untuple (partition pivot as)+ in ite (a .< pivot)+ (tuple (a .: lo, hi))+ (tuple (lo, a .: hi)))+ ?? "push countTuple down"+ =: let (lo, hi) = untuple (partition pivot as)+ in ite (a .< pivot)+ (count e (a .: lo) + count e hi)+ (count e lo + count e (a .: hi))+ =: cases [e .== a ==> ite (a .< pivot)+ (1 + count e lo + count e hi)+ (count e lo + 1 + count e hi)+ ?? "simplify"+ =: 1 + count e lo + count e hi+ ?? ih+ =: 1 + count e as+ =: qed+ , e ./= a ==> ite (a .< pivot)+ (count e lo + count e hi)+ (count e lo + count e hi)+ ?? "simplify"+ =: count e lo + count e hi+ ?? ih+ =: count e as+ =: qed+ ]+ --------------------------------------------------------------------------------------------+ -- Part IV. Prove that the output of quick sort is a permutation of its input+ --------------------------------------------------------------------------------------------++ sortCountsMatch <-+ sInduct "sortCountsMatch"+ (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .== count e (quickSort xs))+ (\xs (_ :: SInteger) -> length @Integer xs) $+ \ih xs e ->+ [] |- count e (quickSort xs)+ =: split xs trivial+ (\a as -> count e (quickSort (a .: as))+ ?? "expand quickSort"+ =: count e (let (lo, hi) = untuple (partition a as)+ in quickSort lo ++ singleton a ++ quickSort hi)+ ?? "push count down"+ =: let (lo, hi) = untuple (partition a as)+ in count e (quickSort lo ++ singleton a ++ quickSort hi)+ ?? countAppend `at` (Inst @"xs" (quickSort lo), Inst @"ys" (singleton a ++ quickSort hi), Inst @"e" e)+ =: count e (quickSort lo) + count e (singleton a ++ quickSort hi)+ ?? countAppend `at` (Inst @"xs" (singleton a), Inst @"ys" (quickSort hi), Inst @"e" e)+ =: count e (quickSort lo) + count e (singleton a) + count e (quickSort hi)+ ?? [ hprf $ ih `at` (Inst @"xs" lo, Inst @"e" e)+ , hprf $ partitionNotLongerFst `at` (Inst @"l" as, Inst @"pivot" a)+ , hasm $ xs .== a .: as+ , hcmnt "IH on lo"+ ]+ =: count e lo + count e (singleton a) + count e (quickSort hi)+ ?? [ hprf $ ih `at` (Inst @"xs" hi, Inst @"e" e)+ , hprf $ partitionNotLongerSnd `at` (Inst @"l" as, Inst @"pivot" a)+ , hasm $ xs .== a .: as+ , hcmnt "IH on hi"+ ]+ =: count e lo + count e (singleton a) + count e hi+ ?? countPartition `at` (Inst @"xs" as, Inst @"pivot" a, Inst @"e" e)+ =: count e xs+ =: qed)++ sortIsPermutation <- lemma "sortIsPermutation" (\(Forall @"xs" xs) -> isPermutation xs (quickSort xs)) [sortCountsMatch]++ --------------------------------------------------------------------------------------------+ -- Part V. Helper lemmas for nonDecreasing+ --------------------------------------------------------------------------------------------+ nonDecreasingMerge <-+ inductWith cvc5 "nonDecreasingMerge"+ (\(Forall @"xs" xs) (Forall @"pivot" pivot) (Forall @"ys" ys) ->+ nonDecreasing xs .&& llt pivot xs+ .&& nonDecreasing ys .&& lge pivot ys .=> nonDecreasing (xs ++ singleton pivot ++ ys)) $+ \ih x xs pivot ys ->+ [nonDecreasing (x .: xs), llt pivot xs, nonDecreasing ys, lge pivot ys]+ |- nonDecreasing (x .: xs ++ singleton pivot ++ ys)+ =: split xs trivial+ (\a as -> nonDecreasing (x .: a .: as ++ singleton pivot ++ ys)+ =: x .<= a .&& nonDecreasing (a .: as ++ singleton pivot ++ ys)+ ?? ih+ =: sTrue+ =: qed)++ --------------------------------------------------------------------------------------------+ -- Part VI. Prove that the output of quick sort is non-decreasing+ --------------------------------------------------------------------------------------------+ sortIsNonDecreasing <-+ sInductWith cvc5 "sortIsNonDecreasing"+ (\(Forall @"xs" xs) -> nonDecreasing (quickSort xs))+ (length @Integer) $+ \ih xs ->+ [] |- nonDecreasing (quickSort xs)+ =: split xs trivial+ (\a as -> nonDecreasing (quickSort (a .: as))+ ?? "expand quickSort"+ =: nonDecreasing (let (lo, hi) = untuple (partition a as)+ in quickSort lo ++ singleton a ++ quickSort hi)+ ?? "push nonDecreasing down"+ =: let (lo, hi) = untuple (partition a as)+ in nonDecreasing (quickSort lo ++ singleton a ++ quickSort hi)+ ?? [ -- Deduce that lo/hi is not longer than as, and hence, shorter than xs+ partitionNotLongerFst `at` (Inst @"l" as, Inst @"pivot" a)+ , partitionNotLongerSnd `at` (Inst @"l" as, Inst @"pivot" a)++ -- Use the inductive hypothesis twice to deduce quickSort of lo and hi are nonDecreasing+ , ih `at` Inst @"xs" lo -- nonDecreasing (quickSort lo)+ , ih `at` Inst @"xs" hi -- nonDecreasing (quickSort hi)++ -- Deduce that lo is all less than a, and hi is all greater than or equal to a+ , partitionFstLT `at` (Inst @"l" as, Inst @"pivot" a)+ , partitionSndGE `at` (Inst @"l" as, Inst @"pivot" a)++ -- Deduce that quickSort lo is all less than a+ , sortIsPermutation `at` Inst @"xs" lo+ , lltPermutation `at` (Inst @"xs" (quickSort lo), Inst @"pivot" a, Inst @"ys" lo)++ -- Deduce that quickSort hi is all greater than or equal to a+ , sortIsPermutation `at` Inst @"xs" hi+ , lgePermutation `at` (Inst @"xs" (quickSort hi), Inst @"pivot" a, Inst @"ys" hi)++ -- Finally conclude that the whole reconstruction is non-decreasing+ , nonDecreasingMerge `at` (Inst @"xs" (quickSort lo), Inst @"pivot" a, Inst @"ys" (quickSort hi))+ ]+ =: sTrue+ =: qed)++ --------------------------------------------------------------------------------------------+ -- Part VII. Putting it together+ --------------------------------------------------------------------------------------------++ qs <- lemma "quickSortIsCorrect"+ (\(Forall @"xs" xs) -> let out = quickSort xs in isPermutation xs out .&& nonDecreasing out)+ [sortIsPermutation, sortIsNonDecreasing]++ -- | We can display the dependencies in a proof+ liftIO $ do putStrLn "== Dependencies:"+ putStr $ show $ getProofTree qs++ pure qs
Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs view
@@ -26,9 +26,8 @@ import Data.SBV.Tuple import Data.SBV.Tools.KnuckleDragger -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception #endif@@ -64,13 +63,12 @@ sInductWith cvc5 "oddSequence" (\(Forall @"n" n) -> n .>= 0 .=> sNot (2 `sDivides` s n)) (abs @SInteger) $ \ih n -> [n .>= 0] |- 2 `sDivides` s n- =: cases [ n .== 0 ==> sFalse =: qed- , n .== 1 ==> sFalse =: qed- , n .>= 2 ==> 2 `sDivides` (s (n-2) + 2 * s (n-1))- =: 2 `sDivides` s (n-2)- ?? ih `at` Inst @"n" (n - 2)- =: sFalse- =: qed+ =: cases [ n .== 0 ==> contradiction+ , n .== 1 ==> contradiction+ , n .>= 2 ==> 2 `sDivides` (s (n-2) + 2 * s (n-1))+ =: 2 `sDivides` s (n-2)+ ?? ih `at` Inst @"n" (n - 2)+ =: contradiction ] -- | Prove that the sequence @1@, @3@, @2 S_{k-1} - S_{k-2}@ generates sequence of odd numbers.
Documentation/SBV/Examples/Misc/FirstOrderLogic.hs view
@@ -29,9 +29,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only, ignore. -- >>> import Data.SBV -- >>> :set -XDataKinds -XScopedTypeVariables #endif
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -27,9 +27,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Misc/Newtypes.hs view
@@ -23,9 +23,8 @@ import Data.SBV import qualified Data.SBV.Internals as SI -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Misc/SetAlgebra.hs view
@@ -18,9 +18,8 @@ import Data.SBV hiding (complement) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV hiding (complement) -- >>> import Data.SBV.Set -- >>> :set -XScopedTypeVariables
Documentation/SBV/Examples/Optimization/ExtField.hs view
@@ -16,9 +16,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Optimization/LinearOpt.hs view
@@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Optimization/Production.hs view
@@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Optimization/VM.hs view
@@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/ProofTools/AddHorn.hs view
@@ -33,9 +33,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Puzzles/Orangutans.hs view
@@ -25,9 +25,8 @@ import Data.SBV import GHC.Generics (Generic) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Queries/Interpolants.hs view
@@ -23,9 +23,8 @@ import Data.SBV import Data.SBV.Control -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Control #endif
Documentation/SBV/Examples/Uninterpreted/AUF.hs view
@@ -36,9 +36,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Uninterpreted/Function.hs view
@@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Uninterpreted/Multiply.hs view
@@ -19,9 +19,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs view
@@ -22,9 +22,8 @@ import Data.SBV -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
Documentation/SBV/Examples/WeakestPreconditions/Basics.hs view
@@ -29,9 +29,8 @@ import GHC.Generics (Generic) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Control -- >>> import Data.SBV.Tools.WeakestPreconditions
Documentation/SBV/Examples/WeakestPreconditions/Fib.hs view
@@ -30,9 +30,8 @@ import GHC.Generics (Generic) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Control -- >>> import Data.SBV.Tools.WeakestPreconditions
Documentation/SBV/Examples/WeakestPreconditions/GCD.hs view
@@ -36,9 +36,8 @@ import Prelude hiding (gcd) import qualified Prelude as P (gcd) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV -- >>> import Data.SBV.Control -- >>> import Data.SBV.Tools.WeakestPreconditions
Documentation/SBV/Examples/WeakestPreconditions/Sum.hs view
@@ -29,9 +29,8 @@ import GHC.Generics (Generic) -#ifndef HADDOCK+#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 949; Tried: 949; Skipped: 0; Success: 949; Errors: 0; Failures 0-Examples: 818; Tried: 818; Skipped: 0; Success: 818; Errors: 0; Failures 0-Setup: 131; Tried: 131; Skipped: 0; Success: 131; Errors: 0; Failures 0+Total: 908; Tried: 908; Skipped: 0; Success: 908; Errors: 0; Failures 0+Examples: 819; Tried: 819; Skipped: 0; Success: 819; Errors: 0; Failures 0+Setup: 89; Tried: 89; Skipped: 0; Success: 89; Errors: 0; Failures 0
SBVTestSuite/GoldFiles/query1.gold view
@@ -73,7 +73,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version)-[RECV] (:version "4.15.0")+[RECV] (:version "4.15.1") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -104,7 +104,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.15.0")+[RECV] (:version "4.15.1") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 11.6+Version : 11.7 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT@@ -21,8 +21,8 @@ Tested-With : GHC==9.10.1 -flag haddock_is_running- description: Define this flag during Haddock generation+flag doctest_is_running+ description: Define this flag during doctest run default : False manual : True @@ -88,8 +88,8 @@ Library import : common-settings - if flag(haddock_is_running)- CPP-Options: -DHADDOCK+ if flag(doctest_is_running)+ CPP-Options: -DDOCTEST default-language: Haskell2010 build-depends : QuickCheck@@ -112,6 +112,7 @@ , text , time , transformers+ , tree-view , uniplate Exposed-modules : Data.SBV , Data.SBV.Control@@ -170,6 +171,7 @@ , Documentation.SBV.Examples.KnuckleDragger.Lists , Documentation.SBV.Examples.KnuckleDragger.MergeSort , Documentation.SBV.Examples.KnuckleDragger.Numeric+ , Documentation.SBV.Examples.KnuckleDragger.QuickSort , Documentation.SBV.Examples.KnuckleDragger.ShefferStroke , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational , Documentation.SBV.Examples.KnuckleDragger.StrongInduction