-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.Induction
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Induction engine for state transition systems. See the following examples
-- for details:
--
--   * "Documentation.SBV.Examples.ProofTools.Strengthen": Use of strengthening
--     to establish inductive invariants.
--
--   * "Documentation.SBV.Examples.ProofTools.Sum": Proof for correctness of
--     an algorithm to sum up numbers,
--
--   * "Documentation.SBV.Examples.ProofTools.Fibonacci": Proof for correctness of
--     an algorithm to fast-compute fibonacci numbers, using axiomatization.
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.Induction (
         InductionResult(..), InductionStep(..), induct, inductWith
       ) where

import Data.SBV
import Data.SBV.Control

import Data.List     (intercalate)
import Control.Monad (when)

-- | A step in an inductive proof. If the tag is present (i.e., @Just nm@), then
-- the step belongs to the subproof that establishes the strengthening named @nm@.
data InductionStep = Initiation  (Maybe String)
                   | Consecution (Maybe String)
                   | PartialCorrectness

-- | Show instance for 'InductionStep', diagnostic purposes only.
instance Show InductionStep where
   show :: InductionStep -> String
show (Initiation  Maybe String
Nothing)  = String
"initiation"
   show (Initiation  (Just String
s)) = String
"initiation for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
   show (Consecution Maybe String
Nothing)  = String
"consecution"
   show (Consecution (Just String
s)) = String
"consecution for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
   show InductionStep
PartialCorrectness     = String
"partial correctness"

-- | Result of an inductive proof, with a counter-example in case of failure.
--
-- If a proof is found (indicated by a 'Proven' result), then the invariant holds
-- and the goal is established once the termination condition holds. If it fails, then
-- it can fail either in an initiation step or in a consecution step:
--
--    * A 'Failed' result in an 'Initiation' step means that the invariant does /not/ hold for
--      the initial state, and thus indicates a true failure.
--
--    * A 'Failed' result in a 'Consecution' step will return a state /s/. This state is known as a
--      CTI (counterexample to inductiveness): It will lead to a violation of the invariant
--      in one step. However, this does not mean the property is invalid: It could be the
--      case that it is simply not inductive. In this case, human intervention---or a smarter
--      algorithm like IC3 for certain domains---is needed to see if one can strengthen the
--      invariant so an inductive proof can be found. How this strengthening can be done remains
--      an art, but the science is improving with algorithms like IC3.
--
--    * A 'Failed' result in a 'PartialCorrectness' step means that the invariant holds, but assuming the
--      termination condition the goal still does not follow. That is, the partial correctness
--      does not hold.
data InductionResult a = Failed InductionStep a
                       | Proven

-- | Show instance for 'InductionResult', diagnostic purposes only.
instance Show a => Show (InductionResult a) where
  show :: InductionResult a -> String
show InductionResult a
Proven       = String
"Q.E.D."
  show (Failed InductionStep
s a
e) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"Failed while establishing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InductionStep -> String
forall a. Show a => a -> String
show InductionStep
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
                                       , String
"Counter-example to inductiveness:"
                                       , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (a -> String
forall a. Show a => a -> String
show a
e)]
                                       ]

-- | Induction engine, using the default solver. See "Documentation.SBV.Examples.ProofTools.Strengthen"
-- and "Documentation.SBV.Examples.ProofTools.Sum" for examples.
induct :: (Show res, Queriable IO st res)
       => Bool                             -- ^ Verbose mode
       -> Symbolic ()                      -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.)
       -> (st -> SBool)                    -- ^ Initial condition
       -> (st -> [st])                     -- ^ Transition relation
       -> [(String, st -> SBool)]          -- ^ Strengthenings, if any. The @String@ is a simple tag.
       -> (st -> SBool)                    -- ^ Invariant that ensures the goal upon termination
       -> (st -> (SBool, SBool))           -- ^ Termination condition and the goal to establish
       -> IO (InductionResult res)         -- ^ Either proven, or a concrete state value that, if reachable, fails the invariant.
induct :: Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct = SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
forall res st.
(Show res, Queriable IO st res) =>
SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith SMTConfig
defaultSMTCfg

-- | Induction engine, configurable with the solver
inductWith :: (Show res, Queriable IO st res)
           => SMTConfig
           -> Bool
           -> Symbolic ()
           -> (st -> SBool)
           -> (st -> [st])
           -> [(String, st -> SBool)]
           -> (st -> SBool)
           -> (st -> (SBool, SBool))
           -> IO (InductionResult res)
inductWith :: SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith SMTConfig
cfg Bool
chatty Symbolic ()
setup st -> SBool
initial st -> [st]
trans [(String, st -> SBool)]
strengthenings st -> SBool
inv st -> (SBool, SBool)
goal =
     String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try String
"Proving initiation"
         (\st
s -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
inv st
s)
         (InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Initiation Maybe String
forall a. Maybe a
Nothing))
         (IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ [(String, st -> SBool)]
-> IO (InductionResult res) -> IO (InductionResult res)
forall a.
(Queriable IO st a, Show a) =>
[(String, st -> SBool)]
-> IO (InductionResult a) -> IO (InductionResult a)
strengthen [(String, st -> SBool)]
strengthenings
         (IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try String
"Proving consecution"
               (\st
s -> [SBool] -> SBool
sAnd (st -> SBool
inv st
s SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [st -> SBool
st st
s | (String
_, st -> SBool
st) <- [(String, st -> SBool)]
strengthenings]) SBool -> SBool -> SBool
.=> (st -> SBool) -> [st] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll st -> SBool
inv (st -> [st]
trans st
s))
               (InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Consecution Maybe String
forall a. Maybe a
Nothing))
               (IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try String
"Proving partial correctness"
                     (\st
s -> let (SBool
term, SBool
result) = st -> (SBool, SBool)
goal st
s in st -> SBool
inv st
s SBool -> SBool -> SBool
.&& SBool
term SBool -> SBool -> SBool
.=> SBool
result)
                     (InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed InductionStep
PartialCorrectness)
                     (String -> IO ()
msg String
"Done" IO () -> IO (InductionResult res) -> IO (InductionResult res)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InductionResult res -> IO (InductionResult res)
forall (m :: * -> *) a. Monad m => a -> m a
return InductionResult res
forall a. InductionResult a
Proven)

  where msg :: String -> IO ()
msg = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
chatty (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn

        try :: String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try String
m a -> SBool
p t -> b
wrap IO b
cont = do String -> IO ()
msg String
m
                               Maybe t
res <- (a -> SBool) -> IO (Maybe t)
forall a a.
(Queriable IO a a, Show a) =>
(a -> SBool) -> IO (Maybe a)
check a -> SBool
p
                               case Maybe t
res of
                                 Just t
ex -> b -> IO b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> IO b) -> b -> IO b
forall a b. (a -> b) -> a -> b
$ t -> b
wrap t
ex
                                 Maybe t
Nothing -> IO b
cont

        check :: (a -> SBool) -> IO (Maybe a)
check a -> SBool
p = SMTConfig -> Symbolic (Maybe a) -> IO (Maybe a)
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith SMTConfig
cfg (Symbolic (Maybe a) -> IO (Maybe a))
-> Symbolic (Maybe a) -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
                        Symbolic ()
setup
                        Query (Maybe a) -> Symbolic (Maybe a)
forall a. Query a -> Symbolic a
query (Query (Maybe a) -> Symbolic (Maybe a))
-> Query (Maybe a) -> Symbolic (Maybe a)
forall a b. (a -> b) -> a -> b
$ do a
st <- QueryT IO a
forall (m :: * -> *) a b. Queriable m a b => QueryT m a
create
                                   SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (a -> SBool
p a
st)

                                   CheckSatResult
cs <- Query CheckSatResult
checkSat
                                   case CheckSatResult
cs of
                                     CheckSatResult
Unk    -> String -> Query (Maybe a)
forall a. HasCallStack => String -> a
error String
"Solver said unknown"
                                     DSat{} -> String -> Query (Maybe a)
forall a. HasCallStack => String -> a
error String
"Solver returned a delta-sat result"
                                     CheckSatResult
Unsat  -> Maybe a -> Query (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
                                     CheckSatResult
Sat    -> do IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
msg String
"Failed:"
                                                  a
ex <- a -> QueryT IO a
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project a
st
                                                  IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
msg (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
ex
                                                  Maybe a -> Query (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Query (Maybe a)) -> Maybe a -> Query (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
ex

        strengthen :: [(String, st -> SBool)]
-> IO (InductionResult a) -> IO (InductionResult a)
strengthen []             IO (InductionResult a)
cont = IO (InductionResult a)
cont
        strengthen ((String
nm, st -> SBool
st):[(String, st -> SBool)]
sts) IO (InductionResult a)
cont = String
-> (st -> SBool)
-> (a -> InductionResult a)
-> IO (InductionResult a)
-> IO (InductionResult a)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try (String
"Proving strengthening initiation  : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
                                             (\st
s -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
st st
s)
                                             (InductionStep -> a -> InductionResult a
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Initiation (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)))
                                             (IO (InductionResult a) -> IO (InductionResult a))
-> IO (InductionResult a) -> IO (InductionResult a)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (a -> InductionResult a)
-> IO (InductionResult a)
-> IO (InductionResult a)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try (String
"Proving strengthening consecution: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
                                                   (\st
s -> st -> SBool
st st
s SBool -> SBool -> SBool
.=> (st -> SBool) -> [st] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll st -> SBool
st (st -> [st]
trans st
s))
                                                   (InductionStep -> a -> InductionResult a
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Consecution (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)))
                                                   ([(String, st -> SBool)]
-> IO (InductionResult a) -> IO (InductionResult a)
strengthen [(String, st -> SBool)]
sts IO (InductionResult a)
cont)