-----------------------------------------------------------------------------
-- |
-- 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 CPP                   #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.WeakestPreconditions.Fib where

import Data.SBV
import Data.SBV.Tools.WeakestPreconditions

import GHC.Generics (Generic)

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
-- >>> import Data.SBV.Control
-- >>> import Data.SBV.Tools.WeakestPreconditions
#endif

-- * Program state

-- | The state for the sum program, parameterized over a base type @a@.
data FibS a = FibS { forall a. FibS a -> a
n :: a    -- ^ The input value
                   , forall a. FibS a -> a
i :: a    -- ^ Loop counter
                   , forall a. FibS a -> a
k :: a    -- ^ tracks @fib (i+1)@
                   , forall a. FibS a -> a
m :: a    -- ^ tracks @fib i@
                   }
                   deriving (Int -> FibS a -> ShowS
[FibS a] -> ShowS
FibS a -> String
(Int -> FibS a -> ShowS)
-> (FibS a -> String) -> ([FibS a] -> ShowS) -> Show (FibS a)
forall a. Show a => Int -> FibS a -> ShowS
forall a. Show a => [FibS a] -> ShowS
forall a. Show a => FibS a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> FibS a -> ShowS
showsPrec :: Int -> FibS a -> ShowS
$cshow :: forall a. Show a => FibS a -> String
show :: FibS a -> String
$cshowList :: forall a. Show a => [FibS a] -> ShowS
showList :: [FibS a] -> ShowS
Show, (forall x. FibS a -> Rep (FibS a) x)
-> (forall x. Rep (FibS a) x -> FibS a) -> Generic (FibS a)
forall x. Rep (FibS a) x -> FibS a
forall x. FibS a -> Rep (FibS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FibS a) x -> FibS a
forall a x. FibS a -> Rep (FibS a) x
$cfrom :: forall a x. FibS a -> Rep (FibS a) x
from :: forall x. FibS a -> Rep (FibS a) x
$cto :: forall a x. Rep (FibS a) x -> FibS a
to :: forall x. Rep (FibS a) x -> FibS a
Generic, Bool -> SBool -> FibS a -> FibS a -> FibS a
(Bool -> SBool -> FibS a -> FibS a -> FibS a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [FibS a] -> FibS a -> SBV b -> FibS a)
-> Mergeable (FibS a)
forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[FibS a] -> FibS a -> SBV b -> FibS a
forall a.
Mergeable a =>
Bool -> SBool -> FibS a -> FibS a -> FibS a
forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[FibS a] -> FibS a -> SBV b -> FibS a
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: forall a.
Mergeable a =>
Bool -> SBool -> FibS a -> FibS a -> FibS a
symbolicMerge :: Bool -> SBool -> FibS a -> FibS a -> FibS a
$cselect :: forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[FibS a] -> FibS a -> SBV b -> FibS a
select :: forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[FibS a] -> FibS a -> SBV b -> FibS a
Mergeable, Functor FibS
Foldable FibS
(Functor FibS, Foldable FibS) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> FibS a -> f (FibS b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    FibS (f a) -> f (FibS a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FibS a -> m (FibS b))
-> (forall (m :: * -> *) a. Monad m => FibS (m a) -> m (FibS a))
-> Traversable FibS
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 => FibS (m a) -> m (FibS a)
forall (f :: * -> *) a. Applicative f => FibS (f a) -> f (FibS a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FibS a -> m (FibS b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FibS a -> f (FibS b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FibS a -> f (FibS b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FibS a -> f (FibS b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => FibS (f a) -> f (FibS a)
sequenceA :: forall (f :: * -> *) a. Applicative f => FibS (f a) -> f (FibS a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FibS a -> m (FibS b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FibS a -> m (FibS b)
$csequence :: forall (m :: * -> *) a. Monad m => FibS (m a) -> m (FibS a)
sequence :: forall (m :: * -> *) a. Monad m => FibS (m a) -> m (FibS a)
Traversable, (forall a b. (a -> b) -> FibS a -> FibS b)
-> (forall a b. a -> FibS b -> FibS a) -> Functor FibS
forall a b. a -> FibS b -> FibS a
forall a b. (a -> b) -> FibS a -> FibS 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) -> FibS a -> FibS b
fmap :: forall a b. (a -> b) -> FibS a -> FibS b
$c<$ :: forall a b. a -> FibS b -> FibS a
<$ :: forall a b. a -> FibS b -> FibS a
Functor, (forall m. Monoid m => FibS m -> m)
-> (forall m a. Monoid m => (a -> m) -> FibS a -> m)
-> (forall m a. Monoid m => (a -> m) -> FibS a -> m)
-> (forall a b. (a -> b -> b) -> b -> FibS a -> b)
-> (forall a b. (a -> b -> b) -> b -> FibS a -> b)
-> (forall b a. (b -> a -> b) -> b -> FibS a -> b)
-> (forall b a. (b -> a -> b) -> b -> FibS a -> b)
-> (forall a. (a -> a -> a) -> FibS a -> a)
-> (forall a. (a -> a -> a) -> FibS a -> a)
-> (forall a. FibS a -> [a])
-> (forall a. FibS a -> Bool)
-> (forall a. FibS a -> Int)
-> (forall a. Eq a => a -> FibS a -> Bool)
-> (forall a. Ord a => FibS a -> a)
-> (forall a. Ord a => FibS a -> a)
-> (forall a. Num a => FibS a -> a)
-> (forall a. Num a => FibS a -> a)
-> Foldable FibS
forall a. Eq a => a -> FibS a -> Bool
forall a. Num a => FibS a -> a
forall a. Ord a => FibS a -> a
forall m. Monoid m => FibS m -> m
forall a. FibS a -> Bool
forall a. FibS a -> Int
forall a. FibS a -> [a]
forall a. (a -> a -> a) -> FibS a -> a
forall m a. Monoid m => (a -> m) -> FibS a -> m
forall b a. (b -> a -> b) -> b -> FibS a -> b
forall a b. (a -> b -> b) -> b -> FibS 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 => FibS m -> m
fold :: forall m. Monoid m => FibS m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FibS a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FibS a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FibS a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> FibS a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> FibS a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FibS a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FibS a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FibS a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FibS a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FibS a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FibS a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> FibS a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FibS a -> a
foldr1 :: forall a. (a -> a -> a) -> FibS a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FibS a -> a
foldl1 :: forall a. (a -> a -> a) -> FibS a -> a
$ctoList :: forall a. FibS a -> [a]
toList :: forall a. FibS a -> [a]
$cnull :: forall a. FibS a -> Bool
null :: forall a. FibS a -> Bool
$clength :: forall a. FibS a -> Int
length :: forall a. FibS a -> Int
$celem :: forall a. Eq a => a -> FibS a -> Bool
elem :: forall a. Eq a => a -> FibS a -> Bool
$cmaximum :: forall a. Ord a => FibS a -> a
maximum :: forall a. Ord a => FibS a -> a
$cminimum :: forall a. Ord a => FibS a -> a
minimum :: forall a. Ord a => FibS a -> a
$csum :: forall a. Num a => FibS a -> a
sum :: forall a. Num a => FibS a -> a
$cproduct :: forall a. Num a => FibS a -> a
product :: forall a. Num a => FibS a -> a
Foldable)

-- | Show instance for t'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 (SBV a) -> String
show (FibS SBV a
n SBV a
i SBV a
k SBV a
m) = String
"{n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", k = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", m = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
     where sh :: SBV a -> String
sh SBV a
v = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<symbolic>" a -> String
forall a. Show a => a -> String
show (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
v)

-- | 'Queriable instance for our state
instance Queriable IO (FibS SInteger) where
  type QueryResult (FibS SInteger) = FibS Integer
  create :: QueryT IO F
create = SInteger -> SInteger -> SInteger -> SInteger -> F
forall a. a -> a -> a -> a -> FibS a
FibS (SInteger -> SInteger -> SInteger -> SInteger -> F)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SInteger -> SInteger -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_  QueryT IO (SInteger -> SInteger -> SInteger -> F)
-> QueryT IO SInteger -> QueryT IO (SInteger -> SInteger -> F)
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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> SInteger -> F)
-> QueryT IO SInteger -> QueryT IO (SInteger -> F)
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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> F) -> QueryT IO SInteger -> QueryT IO F
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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
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 :: Stmt F
algorithm = [Stmt F] -> Stmt F
forall st. [Stmt st] -> Stmt st
Seq [ (F -> F) -> Stmt F
forall st. (st -> st) -> Stmt st
Assign ((F -> F) -> Stmt F) -> (F -> F) -> Stmt F
forall a b. (a -> b) -> a -> b
$ \F
st -> F
st{i = 0, k = 1, m = 0}
                , String -> (F -> SBool) -> Stmt F
forall st. String -> (st -> SBool) -> Stmt st
assert String
"n >= 0" ((F -> SBool) -> Stmt F) -> (F -> SBool) -> Stmt F
forall a b. (a -> b) -> a -> b
$ \FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n} -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                , String
-> (F -> SBool)
-> Maybe (Measure F)
-> (F -> SBool)
-> Stmt F
-> Stmt F
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While String
"i < n"
                        (\FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n, SInteger
i :: forall a. FibS a -> a
i :: SInteger
i, SInteger
k :: forall a. FibS a -> a
k :: SInteger
k, SInteger
m :: forall a. FibS a -> a
m :: SInteger
m} -> 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)
                        (Measure F -> Maybe (Measure F)
forall a. a -> Maybe a
Just (\FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n, SInteger
i :: forall a. FibS a -> a
i :: SInteger
i} -> [SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
i]))
                        (\FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n, SInteger
i :: forall a. FibS a -> a
i :: SInteger
i} -> SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
n)
                        (Stmt F -> Stmt F) -> Stmt F -> Stmt F
forall a b. (a -> b) -> a -> b
$ [Stmt F] -> Stmt F
forall st. [Stmt st] -> Stmt st
Seq [ (F -> F) -> Stmt F
forall st. (st -> st) -> Stmt st
Assign ((F -> F) -> Stmt F) -> (F -> F) -> Stmt F
forall a b. (a -> b) -> a -> b
$ \st :: F
st@FibS{SInteger
m :: forall a. FibS a -> a
m :: SInteger
m, SInteger
k :: forall a. FibS a -> a
k :: SInteger
k} -> F
st{m = k, k = m + k}
                              , (F -> F) -> Stmt F
forall st. (st -> st) -> Stmt st
Assign ((F -> F) -> Stmt F) -> (F -> F) -> Stmt F
forall a b. (a -> b) -> a -> b
$ \st :: F
st@FibS{SInteger
i :: forall a. FibS a -> a
i :: SInteger
i}    -> F
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 :: SInteger -> SInteger
fib SInteger
x
 | SInteger -> Bool
forall a. SymVal a => SBV a -> Bool
isSymbolic SInteger
x = String -> SInteger -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"fib" SInteger
x
 | Bool
True         = SInteger -> SInteger
forall {t} {t}. (Mergeable t, EqSymbolic t, Num t, Num t) => t -> t
go SInteger
x
 where go :: t -> t
go t
i = SBool -> t -> t -> t
forall a. Mergeable a => SBool -> a -> a -> a
ite (t
i t -> t -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== t
0) t
0
            (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ SBool -> t -> t -> t
forall a. Mergeable a => SBool -> a -> a -> a
ite (t
i t -> t -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== t
1) t
1
            (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ t -> t
go (t
it -> t -> t
forall a. Num a => a -> a -> a
-t
1) t -> t -> t
forall a. Num a => a -> a -> a
+ t -> t
go (t
it -> t -> t
forall a. Num a => a -> a -> a
-t
2)

-- | Constraints and axioms we need to state explicitly to tell
-- the SMT solver about our specification for fibonacci.
axiomatizeFib :: Symbolic ()
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 <- Symbolic SInteger
sInteger_
                   constrain $ x .== 0 .=> fib x .== 0
                   constrain $ x .== 1 .=> fib x .== 1

                   constrain $ \(Forall SInteger
n) -> SInteger -> SInteger
fib (SInteger
nSInteger -> 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
nSInteger -> 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
n

-- | Precondition for our program: @n@ must be non-negative.
pre :: F -> SBool
pre :: F -> SBool
pre FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n} = SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0

-- | Postcondition for our program: @m = fib n@
post :: F -> SBool
post :: F -> SBool
post FibS{SInteger
n :: forall a. FibS a -> a
n :: SInteger
n, SInteger
m :: forall a. FibS a -> a
m :: SInteger
m} = SInteger
m SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fib SInteger
n

-- | Stability condition: Program must leave @n@ unchanged.
noChange :: Stable F
noChange :: Stable F
noChange = [String -> (F -> SInteger) -> F -> F -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"n" F -> SInteger
forall a. FibS a -> a
n]

-- | A program is the algorithm, together with its pre- and post-conditions.
imperativeFib :: Program F
imperativeFib :: Program F
imperativeFib = Program { setup :: Symbolic ()
setup         = Symbolic ()
axiomatizeFib
                        , precondition :: F -> SBool
precondition  = F -> SBool
pre
                        , program :: Stmt F
program       = Stmt F
algorithm
                        , postcondition :: F -> SBool
postcondition = F -> SBool
post
                        , stability :: Stable F
stability     = Stable F
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 :: IO (ProofResult (FibS Integer))
correctness = WPConfig -> Program F -> IO (ProofResult (FibS Integer))
forall st res.
(Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose=True} Program F
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@.
-}