-----------------------------------------------------------------------------
-- |
-- 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 { LenS a -> SList a
xs :: SList a  -- ^ The input list
                   , LenS a -> SList a
ys :: SList a  -- ^ Copy of input
                   , 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
$cto :: forall a x. Rep (LenS a) x -> LenS a
$cfrom :: forall a x. LenS a -> Rep (LenS a) x
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
select :: [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 = " 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) (LenC Integer) where
  create :: QueryT IO (LenS Integer)
create                 = SList Integer -> SList Integer -> SInteger -> LenS Integer
forall a. SList a -> SList a -> SInteger -> LenS a
LenS (SList Integer -> SList Integer -> SInteger -> LenS Integer)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SInteger -> LenS Integer)
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 -> LenS Integer)
-> QueryT IO (SList Integer)
-> QueryT IO (SInteger -> LenS Integer)
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 -> LenS Integer)
-> QueryT IO SInteger -> QueryT IO (LenS Integer)
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 :: LenS Integer -> QueryT IO (LenC Integer)
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 (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 (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 :: LenC Integer -> QueryT IO (LenS Integer)
embed   (LenC [Integer]
xs [Integer]
ys Integer
l) = LenS Integer -> QueryT IO (LenS Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (LenS Integer -> QueryT IO (LenS Integer))
-> LenS Integer -> QueryT IO (LenS Integer)
forall a b. (a -> b) -> a -> b
$ SList Integer -> SList Integer -> SInteger -> LenS Integer
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 (LenS Integer)
-> Maybe (Measure (LenS Integer)) -> Stmt (LenS Integer)
algorithm Invariant (LenS Integer)
inv Maybe (Measure (LenS Integer))
msr = [Stmt (LenS Integer)] -> Stmt (LenS Integer)
forall st. [Stmt st] -> Stmt st
Seq [ (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall st. (st -> st) -> Stmt st
Assign ((LenS Integer -> LenS Integer) -> Stmt (LenS Integer))
-> (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall a b. (a -> b) -> a -> b
$ \st :: LenS Integer
st@LenS{SList Integer
xs :: SList Integer
xs :: forall a. LenS a -> SList a
xs} -> LenS Integer
st{ys :: SList Integer
ys = SList Integer
xs, l :: SInteger
l = SInteger
0}
                        , String
-> Invariant (LenS Integer)
-> Maybe (Measure (LenS Integer))
-> Invariant (LenS Integer)
-> Stmt (LenS Integer)
-> Stmt (LenS Integer)
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While String
"! (null ys)"
                                Invariant (LenS Integer)
inv
                                Maybe (Measure (LenS Integer))
msr
                                (\LenS{SList Integer
ys :: SList Integer
ys :: forall a. LenS a -> SList a
ys} -> SBool -> SBool
sNot (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
L.null SList Integer
ys))
                                (Stmt (LenS Integer) -> Stmt (LenS Integer))
-> Stmt (LenS Integer) -> Stmt (LenS Integer)
forall a b. (a -> b) -> a -> b
$ [Stmt (LenS Integer)] -> Stmt (LenS Integer)
forall st. [Stmt st] -> Stmt st
Seq [ (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall st. (st -> st) -> Stmt st
Assign ((LenS Integer -> LenS Integer) -> Stmt (LenS Integer))
-> (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall a b. (a -> b) -> a -> b
$ \st :: LenS Integer
st@LenS{SInteger
l :: SInteger
l :: forall a. LenS a -> SInteger
l}  -> LenS Integer
st{l :: SInteger
l  = SInteger
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1  }
                                      , (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall st. (st -> st) -> Stmt st
Assign ((LenS Integer -> LenS Integer) -> Stmt (LenS Integer))
-> (LenS Integer -> LenS Integer) -> Stmt (LenS Integer)
forall a b. (a -> b) -> a -> b
$ \st :: LenS Integer
st@LenS{SList Integer
ys :: SList Integer
ys :: forall a. LenS a -> SList a
ys} -> LenS Integer
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 (LenS Integer)
pre LenS Integer
_ = SBool
sTrue

-- | Postcondition for our program: @l@ must be the length of the input list.
post :: S -> SBool
post :: Invariant (LenS Integer)
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 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 (LenS Integer)
noChange = [String
-> (LenS Integer -> SList Integer)
-> LenS Integer
-> LenS Integer
-> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" LenS Integer -> 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 (LenS Integer)
-> Maybe (Measure (LenS Integer)) -> Program (LenS Integer)
imperativeLength Invariant (LenS Integer)
inv Maybe (Measure (LenS Integer))
msr = Program :: forall st.
Symbolic ()
-> (st -> SBool)
-> Stmt st
-> (st -> SBool)
-> Stable st
-> Program st
Program { setup :: Symbolic ()
setup         = () -> Symbolic ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                   , precondition :: Invariant (LenS Integer)
precondition  = Invariant (LenS Integer)
pre
                                   , program :: Stmt (LenS Integer)
program       = Invariant (LenS Integer)
-> Maybe (Measure (LenS Integer)) -> Stmt (LenS Integer)
algorithm Invariant (LenS Integer)
inv Maybe (Measure (LenS Integer))
msr
                                   , postcondition :: Invariant (LenS Integer)
postcondition = Invariant (LenS Integer)
post
                                   , stability :: Stable (LenS Integer)
stability     = Stable (LenS Integer)
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 (LenS Integer)
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} = 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 (LenS Integer)
measure LenS{SList Integer
ys :: SList Integer
ys :: forall a. LenS a -> SList a
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 (LenS Integer) -> IO (ProofResult (LenC Integer))
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 (LenS Integer)
-> Maybe (Measure (LenS Integer)) -> Program (LenS Integer)
imperativeLength Invariant (LenS Integer)
invariant (Measure (LenS Integer) -> Maybe (Measure (LenS Integer))
forall a. a -> Maybe a
Just Measure (LenS Integer)
measure))