sbv 11.3 → 11.4
raw patch · 12 files changed
+437/−56 lines, 12 files
Files
- CHANGES.md +9/−0
- Data/SBV.hs +26/−0
- Data/SBV/Internals.hs +5/−1
- Data/SBV/Tools/KD/KnuckleDragger.hs +59/−40
- Documentation/SBV/Examples/BitPrecise/MergeSort.hs +6/−1
- Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs +309/−0
- Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +4/−8
- Documentation/SBV/Examples/Puzzles/Coins.hs +1/−1
- README.md +12/−0
- SBVTestSuite/GoldFiles/doctest_sanity.gold +2/−2
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- sbv.cabal +2/−1
CHANGES.md view
@@ -1,6 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 11.4, 2025-03-12++ * Generalize the strong-induction principle to use lexicographic order for simultanous+ induction over two lists.++ * Added a proof of correctness for the merge-sort algorithm using KnuckleDragger++ * More exports from Data.SBV.Internals to enable compilation of SBVPlugin.+ ### Version 11.3, 2025-03-10 * Fix various haddock documentation links
Data/SBV.hs view
@@ -33,6 +33,8 @@ -- Functions for checking satisfiability ('sat' and 'allSat') are also -- provided. --+-- __Symbolic Types__+-- -- The sbv library introduces the following symbolic types: -- -- * 'SBool': Symbolic Booleans (bits).@@ -112,6 +114,9 @@ -- return a satisfying assignment, if there is one. The 'allSat' function returns -- all satisfying assignments. --+--+-- __Solvers__+-- -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: -- <https://smt-lib.org> --@@ -143,6 +148,27 @@ -- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included.+--+--+-- __Semi-automated theorem proving__+--+-- While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT+-- solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about+-- any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a+-- style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs.+-- The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion+-- and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle+-- etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can+-- be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT+-- solvers alone. See "Data.SBV.Tools.KnuckleDragger" for the API, and+--+-- - "Documentation.SBV.Examples.KnuckleDragger.InsertionSort"+-- - "Documentation.SBV.Examples.KnuckleDragger.MergeSort"+-- - "Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational"+-- - "Documentation.SBV.Examples.KnuckleDragger.ShefferStroke"+-- - "Documentation.SBV.Examples.KnuckleDragger.Lists"+--+-- for various proofs performed in this style. ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}
Data/SBV/Internals.hs view
@@ -33,6 +33,9 @@ -- * Internal structures useful for low-level programming , module Data.SBV.Core.Data + -- * Is this name reserved?+ , isReserved, UIName(..)+ -- * Operations useful for instantiating SBV type classes , genLiteral, genFromCV, CV(..), genMkSymVar, genParse, showModel, SMTModel(..), liftQRem, liftDMod, registerKind, svToSV , ProvableM(), SatisfiableM(), UICodeKind(..)@@ -74,7 +77,7 @@ import Data.SBV.Core.Kind (BVIsNonZero, ValidFloat) import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod)-import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..))+import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..), UIName(..)) import Data.SBV.Core.Floating (sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord, svFloatingPointAsSWord) @@ -83,6 +86,7 @@ import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen +import Data.SBV.SMT.SMTLibNames import Data.SBV.SMT.SMT (genParse, showModel, SatModel(..)) import Data.SBV.Provers.Prover (ProvableM, SatisfiableM)
Data/SBV/Tools/KD/KnuckleDragger.hs view
@@ -128,6 +128,11 @@ cover = sAnd regulars .&& sNot (sOr [b | (_, b) <- caseSplits]) +-- | Propagate the settings for ribbon/timing from top to current. Because in any subsequent configuration+-- in a lemmaWith, inductWith etc., we just want to change the solver, not the actual settings for KD.+kdMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig+kdMergeCfg cur top = cur{kdOptions = kdOptions top}+ -- | A class for doing equational reasoning style calculational proofs. Use 'calc' to prove a given theorem -- as a sequence of equalities, each step following from the previous. class CalcLemma a steps where@@ -167,10 +172,10 @@ {-# MINIMAL calcSteps #-} calcSteps :: a -> steps -> Symbolic (SBool, CalcStrategy) - calc nm p steps = getKDConfig >>= \cfg -> calcWith cfg nm p steps- calcThm nm p steps = getKDConfig >>= \cfg -> calcThmWith cfg nm p steps- calcWith = calcGeneric False- calcThmWith = calcGeneric True+ calc nm p steps = getKDConfig >>= \cfg -> calcWith cfg nm p steps+ calcThm nm p steps = getKDConfig >>= \cfg -> calcThmWith cfg nm p steps+ calcWith cfg nm p steps = getKDConfig >>= \cfg' -> calcGeneric False (kdMergeCfg cfg cfg') nm p steps+ calcThmWith cfg nm p steps = getKDConfig >>= \cfg' -> calcGeneric True (kdMergeCfg cfg cfg') nm p steps calcGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> KD Proof calcGeneric tagTheorem cfg@SMTConfig{kdOptions = KDOptions{measureTime}} nm result steps = do@@ -376,15 +381,15 @@ -- partial correctness is guaranteed if non-terminating functions are involved. sInductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof - induct nm p steps = getKDConfig >>= \cfg -> inductWith cfg nm p steps- inductThm nm p steps = getKDConfig >>= \cfg -> inductThmWith cfg nm p steps- inductWith = inductGeneric RegularInduction False- inductThmWith = inductGeneric RegularInduction True+ induct nm p steps = getKDConfig >>= \cfg -> inductWith cfg nm p steps+ inductThm nm p steps = getKDConfig >>= \cfg -> inductThmWith cfg nm p steps+ inductWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric RegularInduction False (kdMergeCfg cfg cfg') nm p steps+ inductThmWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric RegularInduction True (kdMergeCfg cfg cfg') nm p steps - sInduct nm p steps = getKDConfig >>= \cfg -> sInductWith cfg nm p steps- sInductThm nm p steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p steps- sInductWith = inductGeneric StrongInduction False- sInductThmWith = inductGeneric StrongInduction True+ sInduct nm p steps = getKDConfig >>= \cfg -> sInductWith cfg nm p steps+ sInductThm nm p steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p steps+ sInductWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric StrongInduction False (kdMergeCfg cfg cfg') nm p steps+ sInductThmWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric StrongInduction True (kdMergeCfg cfg cfg') nm p steps -- | Internal, shouldn't be needed outside the library {-# MINIMAL inductionStrategy #-}@@ -620,11 +625,25 @@ 's':_:_ -> init n _ -> n ++ "Elt" --- | Metric for induction. Currently we simply require the list we're assuming correctness for is shorter in length, which--- is a measure that is guarenteed >= 0. -- Later on, we might want to generalize this to a user given measure.-smaller :: SymVal a => SList a -> SList a -> SBool-smaller xs ys = SL.length xs .<= SL.length ys+-- | Metric for induction over lists. Currently we simply require the list we're assuming correctness for is shorter in length, which+-- is a measure that is guarenteed >= 0. Note that we use .<= here, since when called, the second argument is always the tail+-- of the induction argument. Later on, we might want to generalize this to a user given measure.+lexLeq :: SymVal a => SList a -> SList a -> SBool+lexLeq xs ys = SL.length xs .<= SL.length ys +-- | Metric for induction over two lists. We use lexicographic ordering. Again, we don't expose this directly. The+-- second argument is always the tail of the induction argument, so we use .<=. Later on, we might want to generalize+-- this to a user given measure.+lexLeq2 :: (SymVal a, SymVal b) => (SList a, SList b) -> (SList a, SList b) -> SBool+lexLeq2 (xs', ys') (xs, ys) = lxs' .<= lxs -- tail of the first is the same, i.e., the first went down. So, we're good.+ .|| ( lxs' .== 1 + SL.length xs -- OR, the tail did not grow (note the +1 due to us receiving the tail)+ .&& lys' .<= lys -- and the tail of the second went down. + )+ where lxs = SL.length xs+ lys = SL.length ys+ lxs' = SL.length xs'+ lys' = SL.length ys'+ -- | Induction over 'SList'. instance (KnownSymbol nx, SymVal x, EqSymbolic z) => Inductive (Forall nx [x] -> SBool)@@ -639,8 +658,8 @@ xs <- free nxs let ih = case style of- RegularInduction -> internalAxiom "IH" $ result (Forall xs)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) -> xs' `smaller` xs .=> result (Forall xs')+ RegularInduction -> internalAxiom "IH" $ result (Forall xs)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) -> xs' `lexLeq` xs .=> result (Forall xs') CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs pure InductionStrategy {@@ -667,8 +686,8 @@ a <- free na let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (a' :: Forall na a)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a)+ RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (a' :: Forall na a)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a pure InductionStrategy {@@ -697,8 +716,8 @@ b <- free nb let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b)+ RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b pure InductionStrategy {@@ -729,8 +748,8 @@ c <- free nc let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c pure InductionStrategy {@@ -763,8 +782,8 @@ d <- free nd let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d pure InductionStrategy {@@ -799,8 +818,8 @@ e <- free ne let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' e' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' e' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d e pure InductionStrategy {@@ -830,8 +849,8 @@ ys <- free nys let ih = case style of- RegularInduction -> internalAxiom "IH" $ result (Forall xs) (Forall ys)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys')+ RegularInduction -> internalAxiom "IH" $ result (Forall xs) (Forall ys)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys pure InductionStrategy {@@ -864,8 +883,8 @@ a <- free na let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (Forall ys) (a' :: Forall na a)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a)+ RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (Forall ys) (a' :: Forall na a)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a pure InductionStrategy {@@ -900,8 +919,8 @@ b <- free nb let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b)+ RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b pure InductionStrategy {@@ -938,8 +957,8 @@ c <- free nc let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c pure InductionStrategy {@@ -978,8 +997,8 @@ d <- free nd let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d pure InductionStrategy {@@ -1020,8 +1039,8 @@ e <- free ne let ih = case style of- RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)- StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' e' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' e' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d e pure InductionStrategy {
Documentation/SBV/Examples/BitPrecise/MergeSort.hs view
@@ -6,7 +6,12 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental ----- Symbolic implementation of merge-sort and its correctness.+-- Symbolic implementation of merge-sort and its correctness. Note that this+-- version, while fully push-button, proves merge-sort correct for fixed number+-- of elements, i.e., not in its generality. A general proof would require+-- non-trivial applications of induction and more manual guiding. We do+-- such a proof in "Documentation.SBV.Examples.KnuckleDragger.MergeSort", which+-- shows the full-power of the theorem-proving like aspects of SBV. ----------------------------------------------------------------------------- {-# LANGUAGE TupleSections #-}
+ Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs view
@@ -0,0 +1,309 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.KnuckleDragger.MergeSort+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Proving merge-sort correct.+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.KnuckleDragger.MergeSort where++import Data.SBV+import Data.SBV.Tools.KnuckleDragger++import Prelude hiding (null, length, head, tail, elem, splitAt, (++), take, drop)+import Data.SBV.List++-- * Merge sort++-- | Merge two already sorted lists into another+merge :: SList Integer -> SList Integer -> SList Integer+merge = smtFunction "merge" $ \l r -> ite (null l) r+ $ ite (null r) l+ $ let (a, as) = uncons l+ (b, bs) = uncons r+ in ite (a .<= b) (a .: merge as r) (b .: merge l bs)++-- | Merge sort, using 'merge' above to successively sort halved input+mergeSort :: SList Integer -> SList Integer+mergeSort = smtFunction "mergeSort" $ \l -> ite (length l .<= 1) l+ $ let (h1, h2) = splitAt (length l `sEDiv` 2) l+ in merge (mergeSort h1) (mergeSort h2)+-- * 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 merge-sort.+--+-- We have:+--+-- >>> correctness+-- Lemma: nonDecrInsert Q.E.D.+-- Lemma: nonDecTail Q.E.D.+-- Inductive lemma (strong): mergeKeepsSort+-- Base: mergeKeepsSort.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Asms: 3 Q.E.D.+-- Step: 3 Q.E.D.+-- Asms: 4 Q.E.D.+-- Step: 4 Q.E.D.+-- Asms: 5 Q.E.D.+-- Step: 5 Q.E.D.+-- Asms: 6 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Step: mergeKeepsSort.Step Q.E.D.+-- Inductive lemma (strong): sortNonDecreasing+-- Base: sortNonDecreasing.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: sortNonDecreasing.Step Q.E.D.+-- Inductive lemma (strong): mergeCount+-- Base: mergeCount.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Step: mergeCount.Step Q.E.D.+-- Inductive lemma: countAppend+-- Base: countAppend.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: countAppend.Step Q.E.D.+-- Lemma: take_drop Q.E.D.+-- Lemma: takeDropCount+-- Step : 1 Q.E.D.+-- Step : 2 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): sortIsPermutation+-- Base: sortIsPermutation.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: sortIsPermutation.Step Q.E.D.+-- Lemma: mergeSortIsCorrect Q.E.D.+-- [Proven] mergeSortIsCorrect+correctness :: IO Proof+correctness = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 50}} $ do++ --------------------------------------------------------------------------------------------+ -- Part I. Prove that the output of merge sort is non-decreasing.+ --------------------------------------------------------------------------------------------++ nonDecrIns <- lemma "nonDecrInsert"+ (\(Forall @"x" x) (Forall @"ys" ys) -> nonDecreasing ys .&& sNot (null ys) .&& x .<= head ys+ .=> nonDecreasing (x .: ys))+ []++ nonDecrTail <- lemma "nonDecTail"+ (\(Forall @"x" x) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs)+ []++ mergeKeepsSort <-+ sInductWith cvc5 "mergeKeepsSort"+ (\(Forall @"xs" xs) (Forall @"ys" ys) -> nonDecreasing xs .&& nonDecreasing ys .=> nonDecreasing (merge xs ys)) $+ \ih x xs y ys -> [nonDecreasing (x .: xs), nonDecreasing (y .: ys)]+ |- nonDecreasing (merge (x .: xs) (y .: ys))+ ?? "unfold merge"+ =: nonDecreasing (ite (x .<= y)+ (x .: merge xs (y .: ys))+ (y .: merge (x .: xs) ys))+ ?? "push nonDecreasing down"+ =: ite (x .<= y)+ (nonDecreasing (x .: merge xs (y .: ys)))+ (nonDecreasing (y .: merge (x .: xs) ys))+ ?? [ hprf $ nonDecrIns `at` (Inst @"x" x, Inst @"ys" (merge xs (y .: ys)))+ , hyp $ nonDecreasing (x .: xs)+ , hyp $ nonDecreasing (y .: ys)+ ]+ =: ite (x .<= y)+ (nonDecreasing (merge xs (y .: ys)))+ (nonDecreasing (y .: merge (x .: xs) ys))+ ?? [ hprf $ nonDecrIns `at` (Inst @"x" y, Inst @"ys" (merge (x .: xs) ys))+ , hyp $ nonDecreasing (x .: xs)+ , hyp $ nonDecreasing (y .: ys)+ ]+ =: ite (x .<= y)+ (nonDecreasing (merge xs (y .: ys)))+ (nonDecreasing (merge (x .: xs) ys))+ ?? [ hprf $ ih `at` (Inst @"xs" xs, Inst @"ys" (y .: ys))+ , hprf $ nonDecrTail `at` (Inst @"x" x, Inst @"xs" xs)+ , hyp $ nonDecreasing (y .: ys)+ , hyp $ nonDecreasing (x .: xs)+ ]+ =: ite (x .<= y)+ sTrue+ (nonDecreasing (merge (x .: xs) ys))+ ?? [ hprf $ ih `at` (Inst @"xs" (x .: xs), Inst @"ys" ys)+ , hprf $ nonDecrTail `at` (Inst @"x" y, Inst @"xs" ys)+ , hyp $ nonDecreasing (y .: ys)+ , hyp $ nonDecreasing (x .: xs)+ ]+ =: ite (x .<= y) sTrue sTrue+ ?? "simplify"+ =: sTrue+ =: qed++ sortNonDecreasing <-+ sInduct "sortNonDecreasing"+ (\(Forall @"xs" xs) -> nonDecreasing (mergeSort xs)) $+ \ih x xs -> [] |- nonDecreasing (mergeSort (x .: xs))+ ?? "unfold"+ =: let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs)+ in nonDecreasing (ite (length (x .: xs) .<= 1)+ (x .: xs)+ (merge (mergeSort h1) (mergeSort h2)))+ ?? "push nonDecreasing down"+ =: ite (length (x .: xs) .<= 1)+ (nonDecreasing (x .: xs))+ (nonDecreasing (merge (mergeSort h1) (mergeSort h2)))+ ?? ih `at` Inst @"xs" xs+ =: ite (length (x .: xs) .<= 1)+ sTrue+ (nonDecreasing (merge (mergeSort h1) (mergeSort h2)))+ ?? [ ih `at` Inst @"xs" h1+ , ih `at` Inst @"xs" h2+ , mergeKeepsSort `at` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2))+ ]+ =: sTrue+ =: qed++ --------------------------------------------------------------------------------------------+ -- Part II. Prove that the output of merge sort is a permuation of its input+ --------------------------------------------------------------------------------------------++ mergeCount <-+ sInduct "mergeCount"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"e" e) -> count e (merge xs ys) .== count e xs + count e ys) $+ \ih x xs y ys e -> [] |- count e (merge (x .: xs) (y .: ys))+ ?? "unfold merge"+ =: count e (ite (x .<= y)+ (x .: merge xs (y .: ys))+ (y .: merge (x .: xs) ys))+ ?? "push count inside"+ =: ite (x .<= y)+ (count e (x .: merge xs (y .: ys)))+ (count e (y .: merge (x .: xs) ys))+ ?? "unfold count, twice"+ =: ite (x .<= y)+ (let r = count e (merge xs (y .: ys)) in ite (e .== x) (1+r) r)+ (let r = count e (merge (x .: xs) ys) in ite (e .== y) (1+r) r)+ ?? ih `at` (Inst @"xs" xs, Inst @"ys" (y .: ys), Inst @"e" e)+ =: ite (x .<= y)+ (let r = count e xs + count e (y .: ys) in ite (e .== x) (1+r) r)+ (let r = count e (merge (x .: xs) ys) in ite (e .== y) (1+r) r)+ ?? ih `at` (Inst @"xs" (x .: xs), Inst @"ys" ys, Inst @"e" e)+ =: ite (x .<= y)+ (let r = count e xs + count e (y .: ys) in ite (e .== x) (1+r) r)+ (let r = count e (x .: xs) + count e ys in ite (e .== y) (1+r) r)+ ?? "unfold count in reverse, twice"+ =: ite (x .<= y)+ (count e (x .: xs) + count e (y .: ys))+ (count e (x .: xs) + count e (y .: ys))+ ?? "simplify"+ =: count e (x .: xs) + count e (y .: ys)+ =: qed++ 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++ takeDropCount <- do++ takeDrop <- lemma "take_drop"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList Integer)) -> take n xs ++ drop n xs .== xs)+ []++ calc "takeDropCount"+ (\(Forall @"xs" xs) (Forall @"n" n) (Forall @"e" e) -> count e (take n xs) + count e (drop n xs) .== count e xs) $+ \xs n e -> [] |- count e (take n xs) + count e (drop n xs)+ ?? countAppend `at` (Inst @"xs" (take n xs), Inst @"ys" (drop n xs), Inst @"e" e)+ =: count e (take n xs ++ drop n xs)+ ?? takeDrop+ =: count e xs+ =: qed++ sortIsPermutation <-+ sInduct "sortIsPermutation"+ (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .== count e (mergeSort xs)) $+ \ih x xs e -> [] |- count e (mergeSort (x .: xs))+ ?? "unfold mergeSort"+ =: count e (ite (length (x .: xs) .<= 1)+ (x .: xs)+ (let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs)+ in merge (mergeSort h1) (mergeSort h2)))+ ?? "push count down, simplify, rearrange"+ =: let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs)+ in ite (null xs)+ (count e (singleton x))+ (count e (merge (mergeSort h1) (mergeSort h2)))+ ?? mergeCount `at` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2), Inst @"e" e)+ =: ite (null xs)+ (count e (singleton x))+ (count e (mergeSort h1) + count e (mergeSort h2))+ ?? ih `at` (Inst @"xs" h1, Inst @"e" e)+ =: ite (null xs) (count e (singleton x)) (count e h1 + count e (mergeSort h2))+ ?? ih `at` (Inst @"xs" h2, Inst @"e" e)+ =: ite (null xs)+ (count e (singleton x))+ (count e h1 + count e h2)+ ?? takeDropCount `at` (Inst @"xs" (x .: xs), Inst @"n" (length (x .: xs) `sEDiv` 2), Inst @"e" e)+ =: ite (null xs)+ (count e (singleton x))+ (count e (x .: xs))+ =: qed++ --------------------------------------------------------------------------------------------+ -- Put the two parts together for the final proof+ --------------------------------------------------------------------------------------------+ lemma "mergeSortIsCorrect"+ (\(Forall @"xs" xs) -> let out = mergeSort xs in nonDecreasing out .&& isPermutation xs out)+ [sortNonDecreasing, sortIsPermutation]
Documentation/SBV/Examples/KnuckleDragger/Numeric.hs view
@@ -61,8 +61,6 @@ -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@. ----- Note that z3 (as of mid Feb 2025) can't converge on this quickly, but CVC5 does just fine. We have:--- -- >>> sumProof -- Inductive lemma: sum_correct -- Base: sum_correct.Base Q.E.D.@@ -76,7 +74,7 @@ sumProof :: IO Proof sumProof = runKD $ do let sum :: SInteger -> SInteger- sum = smtFunction "sum" $ \n -> ite (n .== 0) 0 (n + sum (n - 1))+ sum = smtFunction "sum" $ \n -> ite (n .<= 0) 0 (n + sum (n - 1)) spec :: SInteger -> SInteger spec n = (n * (n+1)) `sDiv` 2@@ -84,7 +82,7 @@ p :: SInteger -> SBool p n = sum n .== spec n - inductWith cvc5 "sum_correct"+ induct "sum_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $ \ih n -> [n .>= 0] |- sum (n+1) ?? n .>= 0 =: n+1 + sum n ?? [hprf ih, hyp (n .>= 0)]@@ -94,8 +92,6 @@ -- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@. ----- Note that z3 (as of mid Feb 2025) can't converge on this quickly, but CVC5 does just fine. We have:--- -- >>> sumSquareProof -- Inductive lemma: sumSquare_correct -- Base: sumSquare_correct.Base Q.E.D.@@ -109,7 +105,7 @@ sumSquareProof :: IO Proof sumSquareProof = runKD $ do let sumSquare :: SInteger -> SInteger- sumSquare = smtFunction "sumSquare" $ \n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1))+ sumSquare = smtFunction "sumSquare" $ \n -> ite (n .<= 0) 0 (n * n + sumSquare (n - 1)) spec :: SInteger -> SInteger spec n = (n * (n+1) * (2*n+1)) `sDiv` 6@@ -117,7 +113,7 @@ p :: SInteger -> SBool p n = sumSquare n .== spec n - inductWith cvc5 "sumSquare_correct"+ induct "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $ \ih n -> [n .>= 0] |- sumSquare (n+1) ?? n .>= 0 =: (n+1)*(n+1) + sumSquare n ?? [hprf ih, hyp (n .>= 0)]
Documentation/SBV/Examples/Puzzles/Coins.hs view
@@ -21,7 +21,7 @@ -- you: Really? and these six coins are all US government coins currently in production? -- friend: Yes. -- you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?--- friend: Sorry, I would like to but I cant with the coins I have.+-- friend: Sorry, I would like to but I can't with the coins I have. -- What coins are your friend holding? -- @ --
README.md view
@@ -95,6 +95,18 @@ SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. See `proveWithAny`/`proveWithAll` and `satWithAny`/`satWithAll` functions. The function `sbvAvailableSolvers` can be used to query the available solvers at run-time. +### Semi-automated theorem proving++While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT+solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about+any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a+style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs.+The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion+and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle+etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can+be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT+solvers alone. See the documentation under the `Documentation.SBV.Examples.KnuckleDragger` directory.+ ## Copyright, License The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for details.
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 937; Tried: 937; Skipped: 0; Success: 937; Errors: 0; Failures 0-Examples: 809; Tried: 809; Skipped: 0; Success: 809; Errors: 0; Failures 0+Total: 938; Tried: 938; Skipped: 0; Success: 938; Errors: 0; Failures 0+Examples: 810; Tried: 810; Skipped: 0; Success: 810; Errors: 0; Failures 0 Setup: 128; Tried: 128; Skipped: 0; Success: 128; 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.14.1")+[RECV] (:version "4.14.2") [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.14.1")+[RECV] (:version "4.14.2") [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.3+Version : 11.4 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@@ -158,6 +158,7 @@ , Documentation.SBV.Examples.KnuckleDragger.InsertionSort , Documentation.SBV.Examples.KnuckleDragger.Kleene , Documentation.SBV.Examples.KnuckleDragger.Lists+ , Documentation.SBV.Examples.KnuckleDragger.MergeSort , Documentation.SBV.Examples.KnuckleDragger.Numeric , Documentation.SBV.Examples.KnuckleDragger.ShefferStroke , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational