-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.ProofTools.Fibonacci
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example inductive proof to show partial correctness of the for-loop
-- based fibonacci algorithm:
--
-- @
--     i = 0
--     k = 1
--     m = 0
--     while i < n:
--        m, k = k, m + k
--        i++
-- @
--
-- We do the proof against an axiomatized fibonacci implementation using an
-- uninterpreted function.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.ProofTools.Fibonacci where

import Data.SBV
import Data.SBV.Tools.Induction
import Data.SBV.Control

import GHC.Generics hiding (S)

-- * System state

-- | System state. We simply have two components, parameterized
-- over the type so we can put in both concrete and symbolic values.
data S a = S { forall a. S a -> a
i :: a, forall a. S a -> a
k :: a, forall a. S a -> a
m :: a, forall a. S a -> a
n :: a }
         deriving (Int -> S a -> ShowS
[S a] -> ShowS
S a -> String
(Int -> S a -> ShowS)
-> (S a -> String) -> ([S a] -> ShowS) -> Show (S a)
forall a. Show a => Int -> S a -> ShowS
forall a. Show a => [S a] -> ShowS
forall a. Show a => S a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> S a -> ShowS
showsPrec :: Int -> S a -> ShowS
$cshow :: forall a. Show a => S a -> String
show :: S a -> String
$cshowList :: forall a. Show a => [S a] -> ShowS
showList :: [S a] -> ShowS
Show, Bool -> SBool -> S a -> S a -> S a
(Bool -> SBool -> S a -> S a -> S a)
-> (forall b.
    (Ord b, SymVal b, Num b) =>
    [S a] -> S a -> SBV b -> S a)
-> Mergeable (S a)
forall b. (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a
forall a. Mergeable a => Bool -> SBool -> S a -> S a -> S a
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[S a] -> S a -> SBV b -> S a
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: forall a. Mergeable a => Bool -> SBool -> S a -> S a -> S a
symbolicMerge :: Bool -> SBool -> S a -> S a -> S a
$cselect :: forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[S a] -> S a -> SBV b -> S a
select :: forall b. (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a
Mergeable, (forall x. S a -> Rep (S a) x)
-> (forall x. Rep (S a) x -> S a) -> Generic (S a)
forall x. Rep (S a) x -> S a
forall x. S a -> Rep (S a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (S a) x -> S a
forall a x. S a -> Rep (S a) x
$cfrom :: forall a x. S a -> Rep (S a) x
from :: forall x. S a -> Rep (S a) x
$cto :: forall a x. Rep (S a) x -> S a
to :: forall x. Rep (S a) x -> S a
Generic, (forall a b. (a -> b) -> S a -> S b)
-> (forall a b. a -> S b -> S a) -> Functor S
forall a b. a -> S b -> S a
forall a b. (a -> b) -> S a -> S b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> S a -> S b
fmap :: forall a b. (a -> b) -> S a -> S b
$c<$ :: forall a b. a -> S b -> S a
<$ :: forall a b. a -> S b -> S a
Functor, (forall m. Monoid m => S m -> m)
-> (forall m a. Monoid m => (a -> m) -> S a -> m)
-> (forall m a. Monoid m => (a -> m) -> S a -> m)
-> (forall a b. (a -> b -> b) -> b -> S a -> b)
-> (forall a b. (a -> b -> b) -> b -> S a -> b)
-> (forall b a. (b -> a -> b) -> b -> S a -> b)
-> (forall b a. (b -> a -> b) -> b -> S a -> b)
-> (forall a. (a -> a -> a) -> S a -> a)
-> (forall a. (a -> a -> a) -> S a -> a)
-> (forall a. S a -> [a])
-> (forall a. S a -> Bool)
-> (forall a. S a -> Int)
-> (forall a. Eq a => a -> S a -> Bool)
-> (forall a. Ord a => S a -> a)
-> (forall a. Ord a => S a -> a)
-> (forall a. Num a => S a -> a)
-> (forall a. Num a => S a -> a)
-> Foldable S
forall a. Eq a => a -> S a -> Bool
forall a. Num a => S a -> a
forall a. Ord a => S a -> a
forall m. Monoid m => S m -> m
forall a. S a -> Bool
forall a. S a -> Int
forall a. S a -> [a]
forall a. (a -> a -> a) -> S a -> a
forall m a. Monoid m => (a -> m) -> S a -> m
forall b a. (b -> a -> b) -> b -> S a -> b
forall a b. (a -> b -> b) -> b -> S a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => S m -> m
fold :: forall m. Monoid m => S m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> S a -> b
foldr :: forall a b. (a -> b -> b) -> b -> S a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> S a -> b
foldl :: forall b a. (b -> a -> b) -> b -> S a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> S a -> a
foldr1 :: forall a. (a -> a -> a) -> S a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> S a -> a
foldl1 :: forall a. (a -> a -> a) -> S a -> a
$ctoList :: forall a. S a -> [a]
toList :: forall a. S a -> [a]
$cnull :: forall a. S a -> Bool
null :: forall a. S a -> Bool
$clength :: forall a. S a -> Int
length :: forall a. S a -> Int
$celem :: forall a. Eq a => a -> S a -> Bool
elem :: forall a. Eq a => a -> S a -> Bool
$cmaximum :: forall a. Ord a => S a -> a
maximum :: forall a. Ord a => S a -> a
$cminimum :: forall a. Ord a => S a -> a
minimum :: forall a. Ord a => S a -> a
$csum :: forall a. Num a => S a -> a
sum :: forall a. Num a => S a -> a
$cproduct :: forall a. Num a => S a -> a
product :: forall a. Num a => S a -> a
Foldable, Functor S
Foldable S
(Functor S, Foldable S) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> S a -> f (S b))
-> (forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> S a -> m (S b))
-> (forall (m :: * -> *) a. Monad m => S (m a) -> m (S a))
-> Traversable S
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
sequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
$cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
$csequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
sequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
Traversable)

-- | 'Fresh' instance for our state
instance Fresh IO (S SInteger) where
   fresh :: QueryT IO (S SInteger)
fresh = SInteger -> SInteger -> SInteger -> SInteger -> S SInteger
forall a. a -> a -> a -> a -> S a
S (SInteger -> SInteger -> SInteger -> SInteger -> S SInteger)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SInteger -> SInteger -> S SInteger)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SInteger -> SInteger -> SInteger -> S SInteger)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SInteger -> S SInteger)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SInteger -> SInteger -> S SInteger)
-> QueryT IO SInteger -> QueryT IO (SInteger -> S SInteger)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SInteger -> S SInteger)
-> QueryT IO SInteger -> QueryT IO (S SInteger)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_

-- | Encoding partial correctness of the sum algorithm. We have:
--
-- >>> fibCorrect
-- Q.E.D.
--
-- NB. In my experiments, I found that this proof is quite fragile due
-- to the use of quantifiers: If you make a mistake in your algorithm
-- or the coding, z3 pretty much spins forever without finding a counter-example.
-- However, with the correct coding, the proof is almost instantaneous!
fibCorrect :: IO (InductionResult (S Integer))
fibCorrect :: IO (InductionResult (S Integer))
fibCorrect = Bool
-> Symbolic ()
-> (S SInteger -> SBool)
-> (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> (S SInteger -> SBool)
-> (S SInteger -> (SBool, SBool))
-> IO (InductionResult (S Integer))
forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct Bool
chatty Symbolic ()
setup S SInteger -> SBool
initial S SInteger -> [S SInteger]
trans [(String, S SInteger -> SBool)]
strengthenings S SInteger -> SBool
inv S SInteger -> (SBool, SBool)
goal
  where -- Set this to True for SBV to print steps as it proceeds
        -- through the inductive proof
        chatty :: Bool
        chatty :: Bool
chatty = Bool
False

        -- Declare fib as un uninterpreted function:
        fib :: SInteger -> SInteger
        fib :: SInteger -> SInteger
fib = String -> SInteger -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"fib"

        -- We setup to axiomatize the textbook definition of fib in SMT-Lib
        setup :: Symbolic ()
        setup :: Symbolic ()
setup = do SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger
fib SInteger
0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
                   SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger
fib SInteger
1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1
                   (Forall Any Integer -> SBool) -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any Integer -> SBool) -> Symbolic ())
-> (Forall Any Integer -> SBool) -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
x) -> SInteger -> SInteger
fib (SInteger
xSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fib (SInteger
xSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fib SInteger
x

        -- Initialize variables
        initial :: S SInteger -> SBool
        initial :: S SInteger -> SBool
initial S{SInteger
i :: forall a. S a -> a
i :: SInteger
i, SInteger
k :: forall a. S a -> a
k :: SInteger
k, SInteger
m :: forall a. S a -> a
m :: SInteger
m, SInteger
n :: forall a. S a -> a
n :: SInteger
n} = SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> SBool -> SBool
.&& SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0

        -- We code the algorithm almost literally in SBV notation:
        trans :: S SInteger -> [S SInteger]
        trans :: S SInteger -> [S SInteger]
trans st :: S SInteger
st@S{SInteger
i :: forall a. S a -> a
i :: SInteger
i, SInteger
k :: forall a. S a -> a
k :: SInteger
k, SInteger
m :: forall a. S a -> a
m :: SInteger
m, SInteger
n :: forall a. S a -> a
n :: SInteger
n} = [SBool -> S SInteger -> S SInteger -> S SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
n)
                                      S SInteger
st { i = i + 1, k = m + k, m = k }
                                      S SInteger
st
                                 ]

        -- No strengthenings needed for this problem!
        strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = []

        -- Loop invariant: @i@ remains at most @n@, @k@ is @fib (i+1)@
        -- and @m@ is fib(i)@:
        inv :: S SInteger -> SBool
        inv :: S SInteger -> SBool
inv S{SInteger
i :: forall a. S a -> a
i :: SInteger
i, SInteger
k :: forall a. S a -> a
k :: SInteger
k, SInteger
m :: forall a. S a -> a
m :: SInteger
m, SInteger
n :: forall a. S a -> a
n :: SInteger
n} =    SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n
                           SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fib (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                           SBool -> SBool -> SBool
.&& SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fib SInteger
i

        -- Final goal. When the termination condition holds, the value @m@
        -- holds the @n@th fibonacc number. Note that SBV does not prove the
        -- termination condition; it simply is the indication that the loop
        -- has ended as specified by the user.
        goal :: S SInteger -> (SBool, SBool)
        goal :: S SInteger -> (SBool, SBool)
goal S{SInteger
i :: forall a. S a -> a
i :: SInteger
i, SInteger
m :: forall a. S a -> a
m :: SInteger
m, SInteger
n :: forall a. S a -> a
n :: SInteger
n} = (SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
n, SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fib SInteger
n)