-----------------------------------------------------------------------------
-- |
-- 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 DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
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 { x :: a, y :: a }
deriving (Show, Functor, Foldable, Traversable)
-- | 'Fresh' instance for our state
instance Fresh IO (S SInteger) where
fresh = S <$> freshVar_ <*> 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 trans strengthenings = induct chatty setup initial trans strengthenings inv goal
where -- Set this to True for SBV to print steps as it proceeds
-- through the inductive proof
chatty :: Bool
chatty = 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 = return ()
-- Initially, @x@ and @y@ are both @1@
initial :: S SInteger -> SBool
initial S{x, y} = x .== 1 .&& y .== 1
-- Invariant to prove:
inv :: S SInteger -> SBool
inv S{y} = y .>= 1
-- We're not interested in termination/goal for this problem, so just pass trivial values
goal :: S SInteger -> (SBool, SBool)
goal _ = (sTrue, sTrue)
-- | The first program, coded as a transition relation:
pgm1 :: S SInteger -> [S SInteger]
pgm1 S{x, y} = [S{x = x+1, y = y+x}]
-- | The second program, coded as a transition relation:
pgm2 :: S SInteger -> [S SInteger]
pgm2 S{x, y} = [S{x = x+y, y = y+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 = problem pgm1 strengthenings
where 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 = problem pgm1 strengthenings
where strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [("x >= 0", \S{x} -> x .>= 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 = problem pgm2 strengthenings
where 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 = problem pgm2 strengthenings
where strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [("x >= 0", \S{x} -> x .>= 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 = problem pgm2 strengthenings
where strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [ ("x >= 0", \S{x} -> x .>= 0)
, ("y >= 1", \S{y} -> y .>= 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 = problem pgm2 strengthenings
where strengthenings :: [(String, S SInteger -> SBool)]
strengthenings = [("x >= 0 /\\ y >= 1", \S{x, y} -> x .>= 0 .&& y .>= 1)]