    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.WeakestPreconditions.Basics
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Some basic aspects of weakest preconditions, demonstrating programs
    -- that do not use while loops. We use a simple increment program as
    -- an example.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.WeakestPreconditions.Basics 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
    -- >>> import Data.SBV.Control
    -- >>> import Data.SBV.Tools.WeakestPreconditions

    -- * Program state

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

    -- | Show instance for 'IncS'. 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 (IncS (SBV a)) where
       show :: IncS (SBV a) -> String
    show (IncS SBV a
    x SBV a
    y) = String
    "{x = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SBV a
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", y = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SBV a
    y 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 (IncS (SBV a)) where
      fresh :: QueryT IO (IncS (SBV a))
    fresh = SBV a -> SBV a -> IncS (SBV a)
    forall a. a -> a -> IncS a
    IncS (SBV a -> SBV a -> IncS (SBV a))
    -> QueryT IO (SBV a) -> QueryT IO (SBV a -> IncS (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 -> IncS (SBV a))
    -> QueryT IO (SBV a) -> QueryT IO (IncS (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 I = IncS SInteger

    -- * The algorithm

    -- | The increment algorithm:
    --
    -- @
    --    y = x+1
    -- @
    --
    -- The point here isn't really that this program is interesting, but we want to
    -- demonstrate various aspects of WP proofs. So, we take a before and after
    -- program to annotate our algorithm so we can experiment later.
    algorithm :: Stmt I -> Stmt I -> Stmt I
    algorithm :: Stmt I -> Stmt I -> Stmt I
    algorithm Stmt I
    before Stmt I
    after = [Stmt I] -> Stmt I
    forall st. [Stmt st] -> Stmt st
    Seq [ Stmt I
    before
                                 , (I -> I) -> Stmt I
    forall st. (st -> st) -> Stmt st
    Assign ((I -> I) -> Stmt I) -> (I -> I) -> Stmt I
    forall a b. (a -> b) -> a -> b
    $ \st :: I
    st@IncS{SInteger
    x :: forall a. IncS a -> a
    x :: SInteger
    x} -> I
    st{y :: SInteger
    y = SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1}
                                 , Stmt I
    after
                                 ]

    -- | Precondition for our program. Strictly speaking, we don't really need any preconditions,
    -- but for example purposes, we'll require @x@ to be non-negative.
    pre :: I -> SBool
    pre :: I -> SBool
    pre IncS{SInteger
    x :: forall a. IncS a -> a
    x :: SInteger
    x} = SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0

    -- | Postcondition for our program: @y@ must equal @x+1@.
    post :: I -> SBool
    post :: I -> SBool
    post IncS{SInteger
    x :: forall a. IncS a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. IncS a -> a
    y :: SInteger
    y} = SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1

    -- | Stability: @x@ must remain unchanged.
    noChange :: Stable I
    noChange :: Stable I
    noChange = [String -> (I -> SInteger) -> I -> I -> (String, SBool)
    forall a st.
    EqSymbolic a =>
    String -> (st -> a) -> st -> st -> (String, SBool)
    stable String
    "x" I -> SInteger
    forall a. IncS a -> a
    x]

    -- | A program is the algorithm, together with its pre- and post-conditions.
    imperativeInc :: Stmt I -> Stmt I -> Program I
    imperativeInc :: Stmt I -> Stmt I -> Program I
    imperativeInc Stmt I
    before Stmt I
    after = Program { setup :: Symbolic ()
    setup         = () -> Symbolic ()
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                         , precondition :: I -> SBool
    precondition  = I -> SBool
    pre
                                         , program :: Stmt I
    program       = Stmt I -> Stmt I -> Stmt I
    algorithm Stmt I
    before Stmt I
    after
                                         , postcondition :: I -> SBool
    postcondition = I -> SBool
    post
                                         , stability :: Stable I
    stability     = Stable I
    noChange
                                         }

    -- * Correctness

    -- | State the correctness with respect to before/after programs. In the simple
    -- case of nothing prior/after, we have the obvious proof:
    --
    -- >>> correctness Skip Skip
    -- Total correctness is established.
    -- Q.E.D.
    correctness :: Stmt I -> Stmt I -> IO (ProofResult (IncS Integer))
    correctness :: Stmt I -> Stmt I -> IO (ProofResult (IncS Integer))
    correctness Stmt I
    before Stmt I
    after = WPConfig -> Program I -> IO (ProofResult (IncS Integer))
    forall st res.
    (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
    WPConfig -> Program st -> IO (ProofResult res)
    wpProveWith WPConfig
    defaultWPCfg{wpVerbose :: Bool
    wpVerbose=Bool
    True} (Stmt I -> Stmt I -> Program I
    imperativeInc Stmt I
    before Stmt I
    after)

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

    {- $examples
    It is instructive to look at how the proof changes as we put in different @pre@ and @post@ values.

    == Violating the post condition

    If we stick in an extra increment for @y@ after, we can easily break the postcondition:

    >>> :set -XNamedFieldPuns
    >>> import Control.Monad (void)
    >>> void $ correctness Skip $ Assign $ \st@IncS{y} -> st{y = y+1}
    Following proof obligation failed:
    ==================================
      Postcondition fails:
        Start: IncS {x = 0, y = 0}
        End  : IncS {x = 0, y = 2}

    We're told that the program ends up in a state where @x=0@ and @y=2@, violating the requirement @y=x+1@, as expected.

    == Using 'assert'

    There are two main use cases for 'assert', which merely ends up being a call to 'Abort'.
    One is making sure the inputs are well formed. And the other is the user putting in their
    own invariants into the code.

    Let's assume that we only want to accept strictly positive values of @x@. We can try:

    >>> void $ correctness (assert "x > 0" (\st@IncS{x} -> x .> 0)) Skip
    Following proof obligation failed:
    ==================================
      Abort "x > 0" condition is satisfiable:
        Before: IncS {x = 0, y = 0}
        After : IncS {x = 0, y = 0}

    Recall that our precondition ('pre') required @x@ to be non-negative. So, we can put in something weaker and it would be fine:

    >>> void $ correctness (assert "x > -5" (\st@IncS{x} -> x .> -5)) Skip
    Total correctness is established.

    In this case the precondition to our program ensures that the 'assert' will always be satisfied.

    As another example, let us put a post assertion that @y@ is even:

    >>> void $ correctness Skip (assert "y is even" (\st@IncS{y} -> y `sMod` 2 .== 0))
    Following proof obligation failed:
    ==================================
      Abort "y is even" condition is satisfiable:
        Before: IncS {x = 0, y = 0}
        After : IncS {x = 0, y = 1}

    It is important to emphasize that you can put whatever invariant you might want:

    >>> void $ correctness Skip (assert "y > x" (\st@IncS{x, y} -> y .> x))
    Total correctness is established.

    == Violating stability

    What happens if our program modifies @x@? After all, we can simply set @x=10@ and @y=11@ and our post condition would be satisfied:

    >>> void $ correctness Skip (Assign $ \st -> st{x = 10, y = 11})
    Following proof obligation failed:
    ==================================
      Stability fails for "x":
        Before: IncS {x = 0, y = 1}
        After : IncS {x = 10, y = 11}

    So, the stability condition prevents programs from cheating!
    -}