-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.ProofTools.Strengthen
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- An example showing how traditional state-transition invariance problems
-- can be coded using SBV, using induction. We also demonstrate the use of
-- invariant strengthening.
--
-- This example comes from Bradley's [Understanding IC3](http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf) paper,
-- which considers the following two programs:
--
-- @
--      x, y := 1, 1                    x, y := 1, 1
--      while *:                        while *:
--        x, y := x+1, y+x                x, y := x+y, y+x
-- @
--
-- Where @*@ stands for non-deterministic choice. For each program we try to prove that @y >= 1@ is an invariant.
--
-- It turns out that the property @y >= 1@ is indeed an invariant, but is
-- not inductive for either program. We proceed to strengten the invariant
-- and establish it for the first case. We then note that the same strengthening
-- doesn't work for the second program, and find a further strengthening to
-- establish that case as well. This example follows the introductory example
-- in Bradley's paper quite closely.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.ProofTools.Strengthen where

import Data.SBV
import Data.SBV.Tools.Induction
import Data.SBV.Control

-- * System state

-- | System state. We simply have two components, parameterized
-- over the type so we can put in both concrete and symbolic values.
data S a = S { forall a. S a -> a
x :: a, forall a. S a -> a
y :: a }
         deriving (Int -> S a -> ShowS
forall a. Show a => Int -> S a -> ShowS
forall a. Show a => [S a] -> ShowS
forall a. Show a => S a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [S a] -> ShowS
$cshowList :: forall a. Show a => [S a] -> ShowS
show :: S a -> String
$cshow :: forall a. Show a => S a -> String
showsPrec :: Int -> S a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> S a -> ShowS
Show, forall a b. a -> S b -> S a
forall a b. (a -> b) -> S a -> S b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> S b -> S a
$c<$ :: forall a b. a -> S b -> S a
fmap :: forall a b. (a -> b) -> S a -> S b
$cfmap :: forall a b. (a -> b) -> S a -> S b
Functor, forall a. Eq a => a -> S a -> Bool
forall a. Num a => S a -> a
forall a. Ord a => S a -> a
forall m. Monoid m => S m -> m
forall a. S a -> Bool
forall a. S a -> Int
forall a. S a -> [a]
forall a. (a -> a -> a) -> S a -> a
forall m a. Monoid m => (a -> m) -> S a -> m
forall b a. (b -> a -> b) -> b -> S a -> b
forall a b. (a -> b -> b) -> b -> S 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
product :: forall a. Num a => S a -> a
$cproduct :: forall a. Num a => S a -> a
sum :: forall a. Num a => S a -> a
$csum :: forall a. Num a => S a -> a
minimum :: forall a. Ord a => S a -> a
$cminimum :: forall a. Ord a => S a -> a
maximum :: forall a. Ord a => S a -> a
$cmaximum :: forall a. Ord a => S a -> a
elem :: forall a. Eq a => a -> S a -> Bool
$celem :: forall a. Eq a => a -> S a -> Bool
length :: forall a. S a -> Int
$clength :: forall a. S a -> Int
null :: forall a. S a -> Bool
$cnull :: forall a. S a -> Bool
toList :: forall a. S a -> [a]
$ctoList :: forall a. S a -> [a]
foldl1 :: forall a. (a -> a -> a) -> S a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> S a -> a
foldr1 :: forall a. (a -> a -> a) -> S a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> S a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
foldl :: forall b a. (b -> a -> b) -> b -> S a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> S a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
foldr :: forall a b. (a -> b -> b) -> b -> S a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> S a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
fold :: forall m. Monoid m => S m -> m
$cfold :: forall m. Monoid m => S m -> m
Foldable, Functor S
Foldable S
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 => S (m a) -> m (S a)
forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
sequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
$csequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
$cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
sequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> S a -> f (S b)
Traversable)

-- | 'Fresh' instance for our state
instance Fresh IO (S SInteger) where
  fresh :: QueryT IO (S SInteger)
fresh = forall a. a -> a -> S a
S 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_

-- * Encoding the problem

-- | We parameterize over the transition relation and the strengthenings to
-- investigate various combinations.
problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer))
problem :: (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
trans [(String, S SInteger -> SBool)]
strengthenings = forall res st.
(Show res, Queriable IO st res) =>
Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct Bool
chatty Symbolic ()
setup S SInteger -> SBool
initial S SInteger -> [S SInteger]
trans [(String, S SInteger -> SBool)]
strengthenings S SInteger -> SBool
inv S SInteger -> (SBool, SBool)
goal
  where -- Set this to True for SBV to print steps as it proceeds
        -- through the inductive proof
        chatty :: Bool
        chatty :: Bool
chatty = Bool
False

        -- This is where we would put solver options, typically via
        -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
        -- so we simply do nothing.
        setup :: Symbolic ()
        setup :: Symbolic ()
setup = forall (m :: * -> *) a. Monad m => a -> m a
return ()

        -- Initially, @x@ and @y@ are both @1@
        initial :: S SInteger -> SBool
        initial :: S SInteger -> SBool
initial S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = SInteger
x forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> SBool -> SBool
.&& SInteger
y forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1

        -- Invariant to prove:
        inv :: S SInteger -> SBool
        inv :: S SInteger -> SBool
inv S{SInteger
y :: SInteger
y :: forall a. S a -> a
y} = SInteger
y forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
1

        -- We're not interested in termination/goal for this problem, so just pass trivial values
        goal :: S SInteger -> (SBool, SBool)
        goal :: S SInteger -> (SBool, SBool)
goal S SInteger
_ = (SBool
sTrue, SBool
sTrue)

-- | The first program, coded as a transition relation:
pgm1 :: S SInteger -> [S SInteger]
pgm1 :: S SInteger -> [S SInteger]
pgm1 S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = [S{x :: SInteger
x = SInteger
xforall a. Num a => a -> a -> a
+SInteger
1, y :: SInteger
y = SInteger
yforall a. Num a => a -> a -> a
+SInteger
x}]

-- | The second program, coded as a transition relation:
pgm2 :: S SInteger -> [S SInteger]
pgm2 :: S SInteger -> [S SInteger]
pgm2 S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} = [S{x :: SInteger
x = SInteger
xforall a. Num a => a -> a -> a
+SInteger
y, y :: SInteger
y = SInteger
yforall a. Num a => a -> a -> a
+SInteger
x}]

-- * Examples

-- | Example 1: First program, with no strengthenings. We have:
--
-- >>> ex1
-- Failed while establishing consecution.
-- Counter-example to inductiveness:
--   S {x = -1, y = 1}
ex1 :: IO (InductionResult (S Integer))
ex1 :: IO (InductionResult (S Integer))
ex1 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm1 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = []

-- | Example 2: First program, strengthened with @x >= 0@. We have:
--
-- >>> ex2
-- Q.E.D.
ex2 :: IO (InductionResult (S Integer))
ex2 :: IO (InductionResult (S Integer))
ex2 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm1 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [(String
"x >= 0", \S{SInteger
x :: SInteger
x :: forall a. S a -> a
x} -> SInteger
x forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]

-- | Example 3: Second program, with no strengthenings. We have:
--
-- >>> ex3
-- Failed while establishing consecution.
-- Counter-example to inductiveness:
--   S {x = -1, y = 1}
ex3 :: IO (InductionResult (S Integer))
ex3 :: IO (InductionResult (S Integer))
ex3 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm2 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = []

-- | Example 4: Second program, strengthened with @x >= 0@. We have:
--
-- >>> ex4
-- Failed while establishing consecution for strengthening "x >= 0".
-- Counter-example to inductiveness:
--   S {x = 0, y = -1}
ex4 :: IO (InductionResult (S Integer))
ex4 :: IO (InductionResult (S Integer))
ex4 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm2 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [(String
"x >= 0", \S{SInteger
x :: SInteger
x :: forall a. S a -> a
x} -> SInteger
x forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]

-- | Example 5: Second program, strengthened with @x >= 0@ and @y >= 1@ separately. We have:
--
-- >>> ex5
-- Failed while establishing consecution for strengthening "x >= 0".
-- Counter-example to inductiveness:
--   S {x = 0, y = -1}
--
-- Note how this was sufficient in 'ex2' to establish the invariant for the first
-- program, but fails for the second.
ex5 :: IO (InductionResult (S Integer))
ex5 :: IO (InductionResult (S Integer))
ex5 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm2 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [ (String
"x >= 0", \S{SInteger
x :: SInteger
x :: forall a. S a -> a
x} -> SInteger
x forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
                         , (String
"y >= 1", \S{SInteger
y :: SInteger
y :: forall a. S a -> a
y} -> SInteger
y forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
1)
                         ]

-- | Example 6: Second program, strengthened with @x >= 0 \/\\ y >= 1@ simultaneously. We have:
--
-- >>> ex6
-- Q.E.D.
--
-- Compare this to 'ex5'. As pointed out by Bradley, this shows that
-- /a conjunction of assertions can be inductive when none of its components, on its own, is inductive./
-- It remains an art to find proper loop invariants, though the science is improving!
ex6 :: IO (InductionResult (S Integer))
ex6 :: IO (InductionResult (S Integer))
ex6 = (S SInteger -> [S SInteger])
-> [(String, S SInteger -> SBool)]
-> IO (InductionResult (S Integer))
problem S SInteger -> [S SInteger]
pgm2 [(String, S SInteger -> SBool)]
strengthenings
  where strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [(String
"x >= 0 /\\ y >= 1", \S{SInteger
x :: SInteger
x :: forall a. S a -> a
x, SInteger
y :: SInteger
y :: forall a. S a -> a
y} -> SInteger
x forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
1)]