-----------------------------------------------------------------------------
-- |
-- 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.Tools.WeakestPreconditions

import qualified Data.SBV.List as L

import GHC.Generics (Generic)

-- * Program state

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

-- | Show instance: A simplified version of what would otherwise be generated.
instance (SymVal a, Show (f a), Show b) => Show (LenS (f a) b) where
  show :: LenS (f a) b -> String
show LenS{f a
xs :: forall a b. LenS a b -> a
xs :: f a
xs, f a
ys :: forall a b. LenS a b -> a
ys :: f a
ys, b
l :: forall a b. LenS a b -> b
l :: b
l} = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f a -> String
forall a. Show a => a -> String
show f a
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f a -> String
forall a. Show a => a -> String
show f a
ys String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", l = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

-- | Injection/projection from concrete and symbolic values.
instance Queriable IO (LenS (SList Integer) SInteger) where
  type QueryResult (LenS (SList Integer) SInteger) = LenS [Integer] Integer

  create :: QueryT IO S
create                 = SList Integer -> SList Integer -> SInteger -> S
forall a b. a -> a -> b -> LenS a b
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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (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 (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  project :: S -> QueryT IO (QueryResult S)
project (LenS SList Integer
xs SList Integer
ys SInteger
l) = [Integer] -> [Integer] -> Integer -> LenS [Integer] Integer
forall a b. a -> a -> b -> LenS a b
LenS ([Integer] -> [Integer] -> Integer -> LenS [Integer] Integer)
-> QueryT IO [Integer]
-> QueryT IO ([Integer] -> Integer -> LenS [Integer] Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SList Integer -> QueryT IO (QueryResult (SList Integer))
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SList Integer
xs QueryT IO ([Integer] -> Integer -> LenS [Integer] Integer)
-> QueryT IO [Integer]
-> QueryT IO (Integer -> LenS [Integer] 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 (QueryResult (SList Integer))
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SList Integer
ys QueryT IO (Integer -> LenS [Integer] Integer)
-> QueryT IO Integer -> QueryT IO (LenS [Integer] 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 (QueryResult SInteger)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project SInteger
l
  embed :: QueryResult S -> QueryT IO S
embed   (LenS [Integer]
xs [Integer]
ys Integer
l) = SList Integer -> SList Integer -> SInteger -> S
forall a b. a -> a -> b -> LenS a b
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
<$> QueryResult (SList Integer) -> QueryT IO (SList Integer)
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   [Integer]
QueryResult (SList Integer)
xs 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
<*> QueryResult (SList Integer) -> QueryT IO (SList Integer)
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   [Integer]
QueryResult (SList Integer)
ys 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
<*> QueryResult SInteger -> QueryT IO SInteger
forall (m :: * -> *) a.
Queriable m a =>
QueryResult a -> QueryT m a
embed   Integer
QueryResult SInteger
l

-- | Helper type synonym
type S = LenS (SList Integer) SInteger

-- * 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 b. LenS a b -> a
xs :: SList Integer
xs} -> S
st{ys = xs, l = 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 b. LenS a b -> 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 b. LenS a b -> b
l :: SInteger
l}  -> S
st{l  = l + 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 b. LenS a b -> a
ys :: SList Integer
ys} -> S
st{ys = L.tail 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 b. LenS a b -> a
xs :: SList Integer
xs, SInteger
l :: forall a b. LenS a b -> b
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 b. LenS a b -> 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 b. LenS a b -> a
xs :: SList Integer
xs, SList Integer
ys :: forall a b. LenS a b -> a
ys :: SList Integer
ys, SInteger
l :: forall a b. LenS a b -> b
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 b. LenS a b -> 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 (LenS [Integer] Integer) -> IO ()
forall a. Show a => a -> IO ()
print (ProofResult (LenS [Integer] Integer) -> IO ())
-> IO (ProofResult (LenS [Integer] Integer)) -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< WPConfig -> Program S -> IO (ProofResult (LenS [Integer] 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
imperativeLength Invariant S
invariant (Measure S -> Maybe (Measure S)
forall a. a -> Maybe a
Just Measure S
measure))