    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.WeakestPreconditions.Length
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Proof of correctness of an imperative list-length algorithm, using weakest
    -- preconditions. Illustrates the use of SBV's symbolic lists together with
    -- the WP algorithm.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.WeakestPreconditions.Length where

    import Data.SBV
    import Data.SBV.Control

    import qualified Data.SBV.List as L

    import Data.SBV.Tools.WeakestPreconditions

    import GHC.Generics (Generic)

    -- * Program state

    -- | The state of the length program, paramaterized over the element type @a@
    data LenS a = LenS { forall a. LenS a -> SList a
    xs :: SList a  -- ^ The input list
                       , forall a. LenS a -> SList a
    ys :: SList a  -- ^ Copy of input
                       , forall a. LenS a -> SInteger
    l  :: SInteger -- ^ Running length
                       }
                       deriving ((forall x. LenS a -> Rep (LenS a) x)
    -> (forall x. Rep (LenS a) x -> LenS a) -> Generic (LenS a)
    forall x. Rep (LenS a) x -> LenS a
    forall x. LenS a -> Rep (LenS a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (LenS a) x -> LenS a
    forall a x. LenS a -> Rep (LenS a) x
    $cfrom :: forall a x. LenS a -> Rep (LenS a) x
    from :: forall x. LenS a -> Rep (LenS a) x
    $cto :: forall a x. Rep (LenS a) x -> LenS a
    to :: forall x. Rep (LenS a) x -> LenS a
    Generic, Bool -> SBool -> LenS a -> LenS a -> LenS a
    (Bool -> SBool -> LenS a -> LenS a -> LenS a)
    -> (forall b.
        (Ord b, SymVal b, Num b) =>
        [LenS a] -> LenS a -> SBV b -> LenS a)
    -> Mergeable (LenS a)
    forall b.
    (Ord b, SymVal b, Num b) =>
    [LenS a] -> LenS a -> SBV b -> LenS a
    forall a. SymVal a => Bool -> SBool -> LenS a -> LenS a -> LenS a
    forall a b.
    (SymVal a, Ord b, SymVal b, Num b) =>
    [LenS a] -> LenS a -> SBV b -> LenS 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. SymVal a => Bool -> SBool -> LenS a -> LenS a -> LenS a
    symbolicMerge :: Bool -> SBool -> LenS a -> LenS a -> LenS a
    $cselect :: forall a b.
    (SymVal a, Ord b, SymVal b, Num b) =>
    [LenS a] -> LenS a -> SBV b -> LenS a
    select :: forall b.
    (Ord b, SymVal b, Num b) =>
    [LenS a] -> LenS a -> SBV b -> LenS a
    Mergeable)

    -- | The concrete counterpart to 'LenS'. Note that we can no longer use the duality
    -- between @SBV a@ and @a@ as in other examples and just use one datatype for both.
    -- This is because @SList a@ and @[a]@ are fundamentally different types. This can
    -- be a bit confusing at first, but the point is that it is the list that is symbolic
    -- in case of an @SList a@, not that we have a concrete list with symbolic elements
    -- in it. Subtle difference, but it is important to keep these two separate.
    data LenC a = LenC [a] [a] Integer

    -- | Show instance: A simplified version of what would otherwise be generated.
    instance (SymVal a, Show a) => Show (LenS a) where
      show :: LenS a -> String
    show (LenS SList a
    xs SList a
    ys SInteger
    l) = String
    "{xs = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SList a -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SList a
    xs String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", ys = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SList a -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SList a
    ys String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", l = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SInteger -> String
    forall {a}. (Show a, SymVal a) => SBV a -> String
    sh SInteger
    l 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)

    -- | Show instance: Similarly, we want to be a bit more concise here.
    instance Show a => Show (LenC a) where
      show :: LenC a -> String
    show (LenC [a]
    xs [a]
    ys Integer
    l) = String
    "{xs = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [a] -> String
    forall a. Show a => a -> String
    show [a]
    xs String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", ys = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [a] -> String
    forall a. Show a => a -> String
    show [a]
    ys String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", l = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"

    -- | We have to write the bijection between 'LenS' and 'LenC' explicitly. Luckily, the
    -- definition is more or less boilerplate.
    instance Queriable IO (LenS Integer) where
      type QueryResult (LenS Integer) = LenC Integer
      create :: QueryT IO S
    create                 = SList Integer -> SList Integer -> SInteger -> S
    forall a. SList a -> SList a -> SInteger -> LenS a
    LenS (SList Integer -> SList Integer -> SInteger -> S)
    -> QueryT IO (SList Integer)
    -> QueryT IO (SList Integer -> SInteger -> S)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO (SList Integer)
    forall a. SymVal a => Query (SBV a)
    freshVar_   QueryT IO (SList Integer -> SInteger -> S)
    -> QueryT IO (SList Integer) -> QueryT IO (SInteger -> S)
    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 (SList Integer)
    forall a. SymVal a => Query (SBV a)
    freshVar_   QueryT IO (SInteger -> S) -> QueryT IO SInteger -> QueryT IO S
    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_
      project :: S -> QueryT IO (QueryResult S)
    project (LenS SList Integer
    xs SList Integer
    ys SInteger
    l) = [Integer] -> [Integer] -> Integer -> LenC Integer
    forall a. [a] -> [a] -> Integer -> LenC a
    LenC ([Integer] -> [Integer] -> Integer -> LenC Integer)
    -> QueryT IO [Integer]
    -> QueryT IO ([Integer] -> Integer -> LenC Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SList Integer -> QueryT IO [Integer]
    forall a. SymVal a => SBV a -> Query a
    getValue SList Integer
    xs QueryT IO ([Integer] -> Integer -> LenC Integer)
    -> QueryT IO [Integer] -> QueryT IO (Integer -> LenC Integer)
    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
    <*> SList Integer -> QueryT IO [Integer]
    forall a. SymVal a => SBV a -> Query a
    getValue SList Integer
    ys QueryT IO (Integer -> LenC Integer)
    -> QueryT IO Integer -> QueryT IO (LenC Integer)
    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
    <*> SInteger -> QueryT IO Integer
    forall a. SymVal a => SBV a -> Query a
    getValue SInteger
    l
      embed :: QueryResult S -> QueryT IO S
    embed   (LenC [Integer]
    xs [Integer]
    ys Integer
    l) = S -> QueryT IO S
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (S -> QueryT IO S) -> S -> QueryT IO S
    forall a b. (a -> b) -> a -> b
    $ SList Integer -> SList Integer -> SInteger -> S
    forall a. SList a -> SList a -> SInteger -> LenS a
    LenS ([Integer] -> SList Integer
    forall a. SymVal a => a -> SBV a
    literal [Integer]
    xs) ([Integer] -> SList Integer
    forall a. SymVal a => a -> SBV a
    literal [Integer]
    ys) (Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    l)

    -- | Helper type synonym
    type S = LenS Integer

    -- * The algorithm

    -- | The imperative length algorithm:
    --
    -- @
    --    ys = xs
    --    l  = 0
    --    while not (null ys)
    --      l  = l+1
    --      ys = tail ys
    -- @
    --
    -- 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
    $ \st :: S
    st@LenS{SList Integer
    xs :: forall a. LenS a -> SList a
    xs :: SList Integer
    xs} -> S
    st{ys :: SList Integer
    ys = SList Integer
    xs, l :: SInteger
    l = 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
    "! (null ys)"
                                    Invariant S
    inv
                                    Maybe (Measure S)
    msr
                                    (\LenS{SList Integer
    ys :: forall a. LenS a -> SList a
    ys :: SList Integer
    ys} -> SBool -> SBool
    sNot (SList Integer -> SBool
    forall a. SymVal a => SList a -> SBool
    L.null SList Integer
    ys))
                                    (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@LenS{SInteger
    l :: forall a. LenS a -> SInteger
    l :: SInteger
    l}  -> S
    st{l :: SInteger
    l  = SInteger
    l SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    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@LenS{SList Integer
    ys :: forall a. LenS a -> SList a
    ys :: SList Integer
    ys} -> S
    st{ys :: SList Integer
    ys = SList Integer -> SList Integer
    forall a. SymVal a => SList a -> SList a
    L.tail SList Integer
    ys}
                                          ]
                            ]

    -- | Precondition for our program. Nothing! It works for all lists.
    pre :: S -> SBool
    pre :: Invariant S
    pre S
    _ = SBool
    sTrue

    -- | Postcondition for our program: @l@ must be the length of the input list.
    post :: S -> SBool
    post :: Invariant S
    post LenS{SList Integer
    xs :: forall a. LenS a -> SList a
    xs :: SList Integer
    xs, SInteger
    l :: forall a. LenS a -> SInteger
    l :: SInteger
    l} = SInteger
    l SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SList Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList Integer
    xs

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

    -- | A program is the algorithm, together with its pre- and post-conditions.
    imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S
    imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S
    imperativeLength 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
                                       }

    -- | The invariant simply relates the length of the input to the length of the
    -- current suffix and the length of the prefix traversed so far.
    invariant :: Invariant S
    invariant :: Invariant S
    invariant LenS{SList Integer
    xs :: forall a. LenS a -> SList a
    xs :: SList Integer
    xs, SList Integer
    ys :: forall a. LenS a -> SList a
    ys :: SList Integer
    ys, SInteger
    l :: forall a. LenS a -> SInteger
    l :: SInteger
    l} = SList Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList Integer
    xs SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    l SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SList Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList Integer
    ys

    -- | The measure is obviously the length of @ys@, as we peel elements off of it through the loop.
    measure :: Measure S
    measure :: Measure S
    measure LenS{SList Integer
    ys :: forall a. LenS a -> SList a
    ys :: SList Integer
    ys} = [SList Integer -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList Integer
    ys]

    -- * Correctness

    -- | We check that @l@ is the length of the input list @xs@ upon termination.
    -- Note that even though this is an inductive proof, it is fairly easy to prove with our SMT based
    -- technology, which doesn't really handle induction at all!  The usual inductive proof steps are baked
    -- into the invariant establishment phase of the WP proof. We have:
    --
    -- >>> correctness
    -- Total correctness is established.
    -- Q.E.D.
    correctness :: IO ()
    correctness :: IO ()
    correctness = ProofResult (LenC Integer) -> IO ()
    forall a. Show a => a -> IO ()
    print (ProofResult (LenC Integer) -> IO ())
    -> IO (ProofResult (LenC Integer)) -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< WPConfig -> Program S -> IO (ProofResult (LenC 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} (Invariant S -> Maybe (Measure S) -> Program S
    imperativeLength Invariant S
    invariant (Measure S -> Maybe (Measure S)
    forall a. a -> Maybe a
    Just Measure S
    measure))