-----------------------------------------------------------------------------
-- |
-- 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        #-}

{-# 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 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
$cto :: forall a x. Rep (LenS a) x -> LenS a
$cfrom :: forall a x. LenS a -> Rep (LenS a) x
Generic, 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
select :: forall b.
(Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
$cselect :: forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
symbolicMerge :: Bool -> SBool -> LenS a -> LenS a -> LenS a
$csymbolicMerge :: forall a. SymVal a => Bool -> SBool -> LenS a -> LenS a -> 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 = " forall a. [a] -> [a] -> [a]
++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
xs forall a. [a] -> [a] -> [a]
++ String
", ys = " forall a. [a] -> [a] -> [a]
++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ys forall a. [a] -> [a] -> [a]
++ String
", l = " forall a. [a] -> [a] -> [a]
++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SInteger
l forall a. [a] -> [a] -> [a]
++ String
"}"
    where sh :: SBV a -> String
sh SBV a
v = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<symbolic>" forall a. Show a => a -> String
show (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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
xs forall a. [a] -> [a] -> [a]
++ String
", ys = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
ys forall a. [a] -> [a] -> [a]
++ String
", l = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
l 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) (LenC Integer) where
  create :: QueryT IO S
create                 = forall a. SList a -> SList a -> SInteger -> LenS a
LenS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => Query (SBV a)
freshVar_   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Query (SBV a)
freshVar_   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Query (SBV a)
freshVar_
  project :: S -> QueryT IO (LenC Integer)
project (LenS SList Integer
xs SList Integer
ys SInteger
l) = forall a. [a] -> [a] -> Integer -> LenC a
LenC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SList Integer
xs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Query a
getValue SList Integer
ys forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Query a
getValue SInteger
l
  embed :: LenC Integer -> QueryT IO S
embed   (LenC [Integer]
xs [Integer]
ys Integer
l) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SList a -> SList a -> SInteger -> LenS a
LenS (forall a. SymVal a => a -> SBV a
literal [Integer]
xs) (forall a. SymVal a => a -> SBV a
literal [Integer]
ys) (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 = forall st. [Stmt st] -> Stmt st
Seq [ forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SList Integer
xs :: SList Integer
xs :: forall a. LenS a -> SList a
xs} -> S
st{ys :: SList Integer
ys = SList Integer
xs, l :: SInteger
l = SInteger
0}
                        , 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 :: SList Integer
ys :: forall a. LenS a -> SList a
ys} -> SBool -> SBool
sNot (forall a. SymVal a => SList a -> SBool
L.null SList Integer
ys))
                                forall a b. (a -> b) -> a -> b
$ forall st. [Stmt st] -> Stmt st
Seq [ forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SInteger
l :: SInteger
l :: forall a. LenS a -> SInteger
l}  -> S
st{l :: SInteger
l  = SInteger
l forall a. Num a => a -> a -> a
+ SInteger
1  }
                                      , forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SList Integer
ys :: SList Integer
ys :: forall a. LenS a -> SList a
ys} -> S
st{ys :: SList Integer
ys = 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 :: SList Integer
xs :: forall a. LenS a -> SList a
xs, SInteger
l :: SInteger
l :: forall a. LenS a -> SInteger
l} = SInteger
l forall a. EqSymbolic a => a -> a -> SBool
.== 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 = [forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" 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         = 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 :: SList Integer
xs :: forall a. LenS a -> SList a
xs, SList Integer
ys :: SList Integer
ys :: forall a. LenS a -> SList a
ys, SInteger
l :: SInteger
l :: forall a. LenS a -> SInteger
l} = forall a. SymVal a => SList a -> SInteger
L.length SList Integer
xs forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
l forall a. Num a => a -> a -> a
+ 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 :: SList Integer
ys :: forall a. LenS a -> SList a
ys} = [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 = forall a. Show a => a -> IO ()
print forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall st res.
(Show res, Mergeable st, Queriable IO st res) =>
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 (forall a. a -> Maybe a
Just Measure S
measure))