    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.WeakestPreconditions.Sum
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Proof of correctness of an imperative summation algorithm, using weakest
    -- preconditions. We investigate a few different invariants and see how
    -- different versions lead to proofs and failures.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.WeakestPreconditions.Sum where

    import Data.SBV
    import Data.SBV.Control

    import Data.SBV.Tools.WeakestPreconditions

    import GHC.Generics (Generic)

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- * Program state

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

    -- | Show instance for 'SumS'. 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 (SumS (SBV a)) where
       show :: SumS (SBV a) -> String
    show (SumS SBV a
    n SBV a
    i SBV a
    s) = 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
    ", s = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SBV a
    s 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)

    -- | 'Fresh' instance for the program state
    instance SymVal a => Fresh IO (SumS (SBV a)) where
      fresh :: QueryT IO (SumS (SBV a))
    fresh = SBV a -> SBV a -> SBV a -> SumS (SBV a)
    forall a. a -> a -> a -> SumS a
    SumS (SBV a -> SBV a -> SBV a -> SumS (SBV a))
    -> QueryT IO (SBV a) -> QueryT IO (SBV a -> SBV a -> SumS (SBV a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO (SBV a)
    forall a. SymVal a => Query (SBV a)
    freshVar_  QueryT IO (SBV a -> SBV a -> SumS (SBV a))
    -> QueryT IO (SBV a) -> QueryT IO (SBV a -> SumS (SBV a))
    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 (SBV a)
    forall a. SymVal a => Query (SBV a)
    freshVar_  QueryT IO (SBV a -> SumS (SBV a))
    -> QueryT IO (SBV a) -> QueryT IO (SumS (SBV a))
    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 (SBV a)
    forall a. SymVal a => Query (SBV a)
    freshVar_

    -- | Helper type synonym
    type S = SumS SInteger

    -- * The algorithm

    -- | The imperative summation algorithm:
    --
    -- @
    --    i = 0
    --    s = 0
    --    while i < n
    --      i = i+1
    --      s = s+i
    -- @
    --
    -- Note that we need to explicitly annotate each loop with its invariant and the termination
    -- measure. For convenience, we take those two as parameters, so we can experiment later.
    algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
    algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
    algorithm Invariant S
    inv Maybe (Measure S)
    msr = [Stmt S] -> Stmt S
    forall st. [Stmt st] -> Stmt st
    Seq [ (S -> S) -> Stmt S
    forall st. (st -> st) -> Stmt st
    Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
    forall a b. (a -> b) -> a -> b
    $ \S
    st -> S
    st{i = 0, s = 0}
                            , String -> Invariant S -> Stmt S
    forall st. String -> (st -> SBool) -> Stmt st
    assert String
    "n >= 0" (Invariant S -> Stmt S) -> Invariant S -> Stmt S
    forall a b. (a -> b) -> a -> b
    $ \SumS{SInteger
    n :: forall a. SumS a -> a
    n :: SInteger
    n} -> SInteger
    n SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0
                            , String
    -> Invariant S
    -> Maybe (Measure S)
    -> Invariant S
    -> Stmt S
    -> Stmt S
    forall st.
    String
    -> Invariant st
    -> Maybe (Measure st)
    -> Invariant st
    -> Stmt st
    -> Stmt st
    While String
    "i < n"
                                    Invariant S
    inv
                                    Maybe (Measure S)
    msr
                                    (\SumS{SInteger
    i :: forall a. SumS a -> a
    i :: SInteger
    i, SInteger
    n :: forall a. SumS a -> a
    n :: SInteger
    n} -> SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< SInteger
    n)
                                    (Stmt S -> Stmt S) -> Stmt S -> Stmt S
    forall a b. (a -> b) -> a -> b
    $ [Stmt S] -> Stmt S
    forall st. [Stmt st] -> Stmt st
    Seq [ (S -> S) -> Stmt S
    forall st. (st -> st) -> Stmt st
    Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
    forall a b. (a -> b) -> a -> b
    $ \st :: S
    st@SumS{SInteger
    i :: forall a. SumS a -> a
    i :: SInteger
    i}    -> S
    st{i = i+1}
                                          , (S -> S) -> Stmt S
    forall st. (st -> st) -> Stmt st
    Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
    forall a b. (a -> b) -> a -> b
    $ \st :: S
    st@SumS{SInteger
    i :: forall a. SumS a -> a
    i :: SInteger
    i, SInteger
    s :: forall a. SumS a -> a
    s :: SInteger
    s} -> S
    st{s = s+i}
                                          ]
                            ]

    -- | Precondition for our program: @n@ must be non-negative. Note that there is
    -- an explicit call to 'Data.SBV.Tools.WeakestPreconditions.abort' in our program to protect against this case, so
    -- if we do not have this precondition, all programs will fail.
    pre :: S -> SBool
    pre :: Invariant S
    pre SumS{SInteger
    n :: forall a. SumS a -> a
    n :: SInteger
    n} = SInteger
    n SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0

    -- | Postcondition for our program: @s@ must be the sum of all numbers up to
    -- and including @n@.
    post :: S -> SBool
    post :: Invariant S
    post SumS{SInteger
    n :: forall a. SumS a -> a
    n :: SInteger
    n, SInteger
    s :: forall a. SumS a -> a
    s :: SInteger
    s} = SInteger
    s SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SInteger
    n SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * (SInteger
    nSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1)) SInteger -> SInteger -> SInteger
    forall a. SDivisible a => a -> a -> a
    `sDiv` SInteger
    2

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

    -- | A program is the algorithm, together with its pre- and post-conditions.
    imperativeSum :: Invariant S -> Maybe (Measure S) -> Program S
    imperativeSum :: Invariant S -> Maybe (Measure S) -> Program S
    imperativeSum Invariant S
    inv Maybe (Measure S)
    msr = Program { setup :: Symbolic ()
    setup         = () -> Symbolic ()
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                    , precondition :: Invariant S
    precondition  = Invariant S
    pre
                                    , program :: Stmt S
    program       = Invariant S -> Maybe (Measure S) -> Stmt S
    algorithm Invariant S
    inv Maybe (Measure S)
    msr
                                    , postcondition :: Invariant S
    postcondition = Invariant S
    post
                                    , stability :: Stable S
    stability     = Stable S
    noChange
                                    }

    -- * Correctness

    -- | Check that the program terminates and @s@ equals @n*(n+1)/2@
    -- upon termination, i.e., the sum of all numbers upto @n@. Note
    -- that this only holds if @n >= 0@ to start with, as guaranteed
    -- by the precondition of our program.
    --
    -- The correct termination measure is @n-i@: It goes down in each
    -- iteration provided we start with @n >= 0@ and it always remains
    -- non-negative while the loop is executing. Note that we do not
    -- need a lexicographic measure in this case, hence we simply return
    -- a list of one element.
    --
    -- The correct invariant is a conjunction of two facts. First, @s@ is
    -- equivalent to the sum of numbers @0@ upto @i@.  This clearly holds at
    -- the beginning when @i = s = 0@, and is maintained in each iteration
    -- of the body. Second, it always holds that @i <= n@ as long as the
    -- loop executes, both before and after each execution of the body.
    -- When the loop terminates, it holds that @i = n@. Since the invariant says
    -- @s@ is the sum of all numbers up to but not including @i@, we
    -- conclude that @s@ is the sum of all numbers up to and including @n@,
    -- as requested.
    --
    -- Note that coming up with this invariant is neither trivial, nor easy
    -- to automate by any means. What SBV provides is a way to check that
    -- your invariant and termination measures are correct, not
    -- a means of coming up with them in the first place.
    --
    -- We have:
    --
    -- >>> :set -XNamedFieldPuns
    -- >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    -- >>> let measure   SumS{n, i}    = [n - i]
    -- >>> correctness invariant (Just measure)
    -- Total correctness is established.
    -- Q.E.D.
    correctness :: Invariant S -> Maybe (Measure S) -> IO (ProofResult (SumS Integer))
    correctness :: Invariant S -> Maybe (Measure S) -> IO (ProofResult (SumS Integer))
    correctness Invariant S
    inv Maybe (Measure S)
    msr = WPConfig -> Program S -> IO (ProofResult (SumS 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} (Invariant S -> Maybe (Measure S) -> Program S
    imperativeSum Invariant S
    inv Maybe (Measure S)
    msr)

    -- * Example proof attempts
    --
    -- $examples

    {- $examples
    It is instructive to look at several proof attempts to see what can go wrong and how
    the weakest-precondition engine behaves.

    == Always false invariant

    Let's see what happens if we have an always false invariant. Clearly, this will not
    do the job, but it is instructive to see the output. For this exercise, we are only
    interested in partial correctness (to see the impact of the invariant only), so we
    will simply use 'Nothing' for the measures.

    >>> import Control.Monad (void)
    >>> let invariant _ = sFalse
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Invariant for loop "i < n" fails upon entry:
        SumS {n = 0, i = 0, s = 0}

    When the invariant is constant false, it fails upon entry to the loop, and thus the
    proof itself fails.

    == Always true invariant

    The invariant must hold prior to entry to the loop, after the loop-body
    executes, and must be strong enough to establish the postcondition. The easiest
    thing to try would be the invariant that always returns true:

    >>> let invariant _ = sTrue
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Postcondition fails:
        Start: SumS {n = 0, i = 0, s = 0}
        End  : SumS {n = 0, i = 0, s = 1}

    In this case, we are told that the end state does not establish the
    post-condition. Indeed when @n=0@, we would expect @s=0@, not @s=1@.

    The natural question to ask is how did SBV come up with this unexpected
    state at the end of the program run? If you think about the program execution, indeed this
    state is unreachable: We know that @s@ represents the sum of all numbers up to @i@,
    so if @i=0@, we would expect @s@ to be @0@. Our invariant is clearly an overapproximation
    of the reachable space, and SBV is telling us that we need to constrain and outlaw
    the state @{n = 0, i = 0, s = 1}@. Clearly, the invariant has to state something
    about the relationship between @i@ and @s@, which we are missing in this case.

    == Failing to maintain the invariant

    What happens if we pose an invariant that the loop actually does not maintain? Here
    is an example:

    >>> let invariant SumS{n, i, s} = s .<= i .&& s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Invariant for loop "i < n" is not maintained by the body:
        Before: SumS {n = 2, i = 1, s = 1}
        After : SumS {n = 2, i = 2, s = 3}

    Here, we posed the extra incorrect invariant that @s <= i@ must be maintained, and SBV found us a reachable state that violates the invariant. The
    /before/ state indeed satisfies @s <= i@, but the /after/ state does not. Note that the proof fails in this case not because the program
    is incorrect, but the stipulated invariant is not valid.

    == Having a bad measure, Part I

    The termination measure must always be non-negative:

    >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> let measure   SumS{n, i}    = [1-i]
    >>> void $ correctness invariant (Just measure)
    Following proof obligation failed:
    ==================================
      Measure for loop "i < n" is negative:
        State  : SumS {n = 3, i = 2, s = 3}
        Measure: -1

    The failure is pretty obvious in this case: Measure produces a negative value.

    == Having a bad measure, Part II

    The other way we can have a bad measure is if it fails to decrease through the loop body:

    >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> let measure   SumS{n, i}    = [n + i]
    >>> void $ correctness invariant (Just measure)
    Following proof obligations failed:
    ===================================
      Measure for loop "i < n" is negative:
        State  : SumS {n = 0, i = -1, s = 0}
        Measure: -1
      Measure for loop "i < n" does not decrease:
        Before : SumS {n = 0, i = -1, s = 0}
        Measure: -1
        After  : SumS {n = 0, i = 0, s = 0}
        Measure: 0

    Clearly, as @i@ increases, so does our bogus measure @n+i@. Note that in this case the counterexample has
    @i@ as a negative value, as the SMT solver finds a counter-example to induction, not
    necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.
    -}