----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.WeakestPreconditions.Fib -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Proof of correctness of an imperative fibonacci algorithm, using weakest -- preconditions. Note that due to the recursive nature of fibonacci, we -- cannot write the spec directly, so we use an uninterpreted function -- and proper axioms to complete the proof. ----------------------------------------------------------------------------- {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} module Documentation.SBV.Examples.WeakestPreconditions.Fib where import Data.SBV import Data.SBV.Control import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) -- * Program state -- | The state for the sum program, parameterized over a base type @a@. data FibS a = FibS { n :: a -- ^ The input value , i :: a -- ^ Loop counter , k :: a -- ^ tracks @fib (i+1)@ , m :: a -- ^ tracks @fib i@ } deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable) -- | Show instance for 'FibS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (FibS (SBV a)) where show (FibS n i k m) = "{n = " ++ sh n ++ ", i = " ++ sh i ++ ", k = " ++ sh k ++ ", m = " ++ sh m ++ "}" where sh v = case unliteral v of Nothing -> "<symbolic>" Just l -> show l -- | 'Fresh' instance for the program state instance (SymVal a, SMTValue a) => Fresh IO (FibS (SBV a)) where fresh = FibS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_ -- | Helper type synonym type F = FibS SInteger -- * The algorithm -- | The imperative fibonacci algorithm: -- -- @ -- i = 0 -- k = 1 -- m = 0 -- while i < n: -- m, k = k, m + k -- i++ -- @ -- -- When the loop terminates, @m@ contains @fib(n)@. algorithm :: Stmt F algorithm = Seq [ Assign $ \st -> st{i = 0, k = 1, m = 0} , assert "n >= 0" $ \FibS{n} -> n .>= 0 , While "i < n" (\FibS{n, i, k, m} -> i .<= n .&& k .== fib (i+1) .&& m .== fib i) (Just (\FibS{n, i} -> [n-i])) (\FibS{n, i} -> i .< n) $ Seq [ Assign $ \st@FibS{m, k} -> st{m = k, k = m + k} , Assign $ \st@FibS{i} -> st{i = i+1} ] ] -- | Symbolic fibonacci as our specification. Note that we cannot -- really implement the fibonacci function since it is not -- symbolically terminating. So, we instead uninterpret and -- axiomatize it below. -- -- NB. The concrete part of the definition is only used in calls to 'traceExecution' -- and is not needed for the proof. If you don't need to call 'traceExecution', you -- can simply ignore that part and directly uninterpret. fib :: SInteger -> SInteger fib x | isSymbolic x = uninterpret "fib" x | True = go x where go i = ite (i .== 0) 0 $ ite (i .== 1) 1 $ go (i-1) + go (i-2) -- | Constraints and axioms we need to state explicitly to tell -- the SMT solver about our specification for fibonacci. axiomatizeFib :: Symbolic () axiomatizeFib = do -- Base cases. -- Note that we write these in forms of implications, -- instead of the more direct: -- -- constrain $ fib 0 .== 0 -- constrain $ fib 1 .== 1 -- -- As otherwise they would be concretely evaluated and -- would not be sent to the SMT solver! x <- sInteger_ constrain $ x .== 0 .=> fib x .== 0 constrain $ x .== 1 .=> fib x .== 1 -- The inductive case. Unfortunately; SBV does not support -- adding quantified constraints in the query mode. So we -- have to write this axiom directly in SMT-Lib. Note also how -- carefully we've chosen this axiom to work with our proof! addAxiom "fib_n" [ "(assert (forall ((x Int))" , " (= (fib (+ x 2)) (+ (fib (+ x 1)) (fib x)))))" ] -- | Precondition for our program: @n@ must be non-negative. pre :: F -> SBool pre FibS{n} = n .>= 0 -- | Postcondition for our program: @m = fib n@ post :: F -> SBool post FibS{n, m} = m .== fib n -- | Stability condition: Program must leave @n@ unchanged. noChange :: Stable F noChange = [stable "n" n] -- | A program is the algorithm, together with its pre- and post-conditions. imperativeFib :: Program F imperativeFib = Program { setup = axiomatizeFib , precondition = pre , program = algorithm , postcondition = post , stability = noChange } -- * Correctness -- | With the axioms in place, it is trivial to establish correctness: -- -- >>> correctness -- Total correctness is established. -- Q.E.D. -- -- Note that I found this proof to be quite fragile: If you do not get the algorithm right -- or the axioms aren't in place, z3 simply goes to an infinite loop, instead of providing -- counter-examples. Of course, this is to be expected with the quantifiers present. correctness :: IO (ProofResult (FibS Integer)) correctness = wpProveWith defaultWPCfg{wpVerbose=True} imperativeFib -- * Concrete execution -- $concreteExec {- $concreteExec Example concrete run. As we mentioned in the definition for 'fib', the concrete-execution function cannot deal with uninterpreted functions and axioms for obvious reasons. In those cases we revert to the concrete definition. Here's an example run: >>> traceExecution imperativeFib $ FibS {n = 3, i = 0, k = 0, m = 0} *** Precondition holds, starting execution: {n = 3, i = 0, k = 0, m = 0} ===> [1.1] Assign {n = 3, i = 0, k = 1, m = 0} ===> [1.2] Conditional, taking the "then" branch {n = 3, i = 0, k = 1, m = 0} ===> [1.2.1] Skip {n = 3, i = 0, k = 1, m = 0} ===> [1.3] Loop "i < n": condition holds, executing the body {n = 3, i = 0, k = 1, m = 0} ===> [1.3.{1}.1] Assign {n = 3, i = 0, k = 1, m = 1} ===> [1.3.{1}.2] Assign {n = 3, i = 1, k = 1, m = 1} ===> [1.3] Loop "i < n": condition holds, executing the body {n = 3, i = 1, k = 1, m = 1} ===> [1.3.{2}.1] Assign {n = 3, i = 1, k = 2, m = 1} ===> [1.3.{2}.2] Assign {n = 3, i = 2, k = 2, m = 1} ===> [1.3] Loop "i < n": condition holds, executing the body {n = 3, i = 2, k = 2, m = 1} ===> [1.3.{3}.1] Assign {n = 3, i = 2, k = 3, m = 2} ===> [1.3.{3}.2] Assign {n = 3, i = 3, k = 3, m = 2} ===> [1.3] Loop "i < n": condition fails, terminating {n = 3, i = 3, k = 3, m = 2} *** Program successfully terminated, post condition holds of the final state: {n = 3, i = 3, k = 3, m = 2} Program terminated successfully. Final state: {n = 3, i = 3, k = 3, m = 2} As expected, @fib 3@ is @2@. -}