diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,14 @@ * Hackage: * GitHub: +### 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, diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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. diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -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? -- diff --git a/Data/SBV/Either.hs b/Data/SBV/Either.hs --- a/Data/SBV/Either.hs +++ b/Data/SBV/Either.hs @@ -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@ -- diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -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 diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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. -- diff --git a/Data/SBV/Maybe.hs b/Data/SBV/Maybe.hs --- a/Data/SBV/Maybe.hs +++ b/Data/SBV/Maybe.hs @@ -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'. -- diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -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'. -- diff --git a/Data/SBV/Set.hs b/Data/SBV/Set.hs --- a/Data/SBV/Set.hs +++ b/Data/SBV/Set.hs @@ -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 diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -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. -- diff --git a/Data/SBV/Tools/BVOptimize.hs b/Data/SBV/Tools/BVOptimize.hs --- a/Data/SBV/Tools/BVOptimize.hs +++ b/Data/SBV/Tools/BVOptimize.hs @@ -16,6 +16,8 @@ -- This implementation is based on an idea by Nikolaj Bjorner, see . ----------------------------------------------------------------------------- +{-# 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 diff --git a/Data/SBV/Tools/KD/Kernel.hs b/Data/SBV/Tools/KD/Kernel.hs --- a/Data/SBV/Tools/KD/Kernel.hs +++ b/Data/SBV/Tools/KD/Kernel.hs @@ -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 diff --git a/Data/SBV/Tools/KD/KnuckleDragger.hs b/Data/SBV/Tools/KD/KnuckleDragger.hs --- a/Data/SBV/Tools/KD/KnuckleDragger.hs +++ b/Data/SBV/Tools/KD/KnuckleDragger.hs @@ -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 diff --git a/Data/SBV/Tools/KD/Utils.hs b/Data/SBV/Tools/KD/Utils.hs --- a/Data/SBV/Tools/KD/Utils.hs +++ b/Data/SBV/Tools/KD/Utils.hs @@ -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 diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs --- a/Data/SBV/Tools/KnuckleDragger.hs +++ b/Data/SBV/Tools/KnuckleDragger.hs @@ -19,6 +19,9 @@ -- * Propositions and their proofs Proposition, Proof + -- * Getting the proof tree + , KDProofDeps(), getProofTree, kdShowDepsHTML + -- * Adding axioms/definitions , axiom diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -10,6 +10,7 @@ -- Based on: ----------------------------------------------------------------------------- +{-# 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. diff --git a/Data/SBV/Tools/Range.hs b/Data/SBV/Tools/Range.hs --- a/Data/SBV/Tools/Range.hs +++ b/Data/SBV/Tools/Range.hs @@ -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 diff --git a/Data/SBV/Tuple.hs b/Data/SBV/Tuple.hs --- a/Data/SBV/Tuple.hs +++ b/Data/SBV/Tuple.hs @@ -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 diff --git a/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs b/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs --- a/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs +++ b/Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs @@ -19,7 +19,7 @@ import Data.SBV import Data.SBV.Tools.Overflow -#ifndef HADDOCK +#ifdef DOCTEST -- $setup -- >>> import Data.SBV -- >>> import Data.Int diff --git a/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs b/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs --- a/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs +++ b/Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs @@ -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 diff --git a/Documentation/SBV/Examples/BitPrecise/PrefixSum.hs b/Documentation/SBV/Examples/BitPrecise/PrefixSum.hs --- a/Documentation/SBV/Examples/BitPrecise/PrefixSum.hs +++ b/Documentation/SBV/Examples/BitPrecise/PrefixSum.hs @@ -22,9 +22,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/CodeGeneration/GCD.hs b/Documentation/SBV/Examples/CodeGeneration/GCD.hs --- a/Documentation/SBV/Examples/CodeGeneration/GCD.hs +++ b/Documentation/SBV/Examples/CodeGeneration/GCD.hs @@ -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 diff --git a/Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs b/Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs --- a/Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs +++ b/Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs @@ -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 diff --git a/Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs b/Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs --- a/Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs +++ b/Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs @@ -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 diff --git a/Documentation/SBV/Examples/Crypto/AES.hs b/Documentation/SBV/Examples/Crypto/AES.hs --- a/Documentation/SBV/Examples/Crypto/AES.hs +++ b/Documentation/SBV/Examples/Crypto/AES.hs @@ -52,9 +52,8 @@ import Test.QuickCheck hiding (verbose) -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Crypto/Prince.hs b/Documentation/SBV/Examples/Crypto/Prince.hs --- a/Documentation/SBV/Examples/Crypto/Prince.hs +++ b/Documentation/SBV/Examples/Crypto/Prince.hs @@ -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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/Basics.hs b/Documentation/SBV/Examples/KnuckleDragger/Basics.hs --- a/Documentation/SBV/Examples/KnuckleDragger/Basics.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Basics.hs @@ -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: -- diff --git a/Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs b/Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs --- a/Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs @@ -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)) $ diff --git a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs --- a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs @@ -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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs b/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs --- a/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs @@ -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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/QuickSort.hs b/Documentation/SBV/Examples/KnuckleDragger/QuickSort.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/KnuckleDragger/QuickSort.hs @@ -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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs b/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs --- a/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs @@ -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. diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs --- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs @@ -29,9 +29,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only, ignore. -- >>> import Data.SBV -- >>> :set -XDataKinds -XScopedTypeVariables #endif diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -27,9 +27,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Misc/Newtypes.hs b/Documentation/SBV/Examples/Misc/Newtypes.hs --- a/Documentation/SBV/Examples/Misc/Newtypes.hs +++ b/Documentation/SBV/Examples/Misc/Newtypes.hs @@ -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 diff --git a/Documentation/SBV/Examples/Misc/SetAlgebra.hs b/Documentation/SBV/Examples/Misc/SetAlgebra.hs --- a/Documentation/SBV/Examples/Misc/SetAlgebra.hs +++ b/Documentation/SBV/Examples/Misc/SetAlgebra.hs @@ -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 diff --git a/Documentation/SBV/Examples/Optimization/ExtField.hs b/Documentation/SBV/Examples/Optimization/ExtField.hs --- a/Documentation/SBV/Examples/Optimization/ExtField.hs +++ b/Documentation/SBV/Examples/Optimization/ExtField.hs @@ -16,9 +16,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Optimization/LinearOpt.hs b/Documentation/SBV/Examples/Optimization/LinearOpt.hs --- a/Documentation/SBV/Examples/Optimization/LinearOpt.hs +++ b/Documentation/SBV/Examples/Optimization/LinearOpt.hs @@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Optimization/Production.hs b/Documentation/SBV/Examples/Optimization/Production.hs --- a/Documentation/SBV/Examples/Optimization/Production.hs +++ b/Documentation/SBV/Examples/Optimization/Production.hs @@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Optimization/VM.hs b/Documentation/SBV/Examples/Optimization/VM.hs --- a/Documentation/SBV/Examples/Optimization/VM.hs +++ b/Documentation/SBV/Examples/Optimization/VM.hs @@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/ProofTools/AddHorn.hs b/Documentation/SBV/Examples/ProofTools/AddHorn.hs --- a/Documentation/SBV/Examples/ProofTools/AddHorn.hs +++ b/Documentation/SBV/Examples/ProofTools/AddHorn.hs @@ -33,9 +33,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Puzzles/Orangutans.hs b/Documentation/SBV/Examples/Puzzles/Orangutans.hs --- a/Documentation/SBV/Examples/Puzzles/Orangutans.hs +++ b/Documentation/SBV/Examples/Puzzles/Orangutans.hs @@ -25,9 +25,8 @@ import Data.SBV import GHC.Generics (Generic) -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Queries/Interpolants.hs b/Documentation/SBV/Examples/Queries/Interpolants.hs --- a/Documentation/SBV/Examples/Queries/Interpolants.hs +++ b/Documentation/SBV/Examples/Queries/Interpolants.hs @@ -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 diff --git a/Documentation/SBV/Examples/Uninterpreted/AUF.hs b/Documentation/SBV/Examples/Uninterpreted/AUF.hs --- a/Documentation/SBV/Examples/Uninterpreted/AUF.hs +++ b/Documentation/SBV/Examples/Uninterpreted/AUF.hs @@ -36,9 +36,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Uninterpreted/Function.hs b/Documentation/SBV/Examples/Uninterpreted/Function.hs --- a/Documentation/SBV/Examples/Uninterpreted/Function.hs +++ b/Documentation/SBV/Examples/Uninterpreted/Function.hs @@ -17,9 +17,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs --- a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs +++ b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs @@ -19,9 +19,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs --- a/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs +++ b/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -22,9 +22,8 @@ import Data.SBV -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs @@ -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 diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs @@ -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 diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs @@ -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 diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs @@ -29,9 +29,8 @@ import GHC.Generics (Generic) -#ifndef HADDOCK +#ifdef DOCTEST -- $setup --- >>> -- For doctest purposes only: -- >>> import Data.SBV #endif diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -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) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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