-----------------------------------------------------------------------------
-- |
-- 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 #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE TypeOperators    #-}

{-# 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, 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, 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, a) -> String
forall a. Show a => a -> String
show (a, 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 ~ QueryResult st)
       => 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 -> SBool)              -- ^ 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 :: forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct = SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> [(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 ~ QueryResult st)
           => SMTConfig
           -> Bool
           -> Symbolic ()
           -> (st -> SBool)
           -> (st -> st -> SBool)
           -> [(String, st -> SBool)]
           -> (st -> SBool)
           -> (st -> (SBool, SBool))
           -> IO (InductionResult res)
inductWith :: forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith SMTConfig
cfg Bool
chatty Symbolic ()
setup st -> SBool
initial st -> st -> SBool
trans [(String, st -> SBool)]
strengthenings st -> SBool
inv st -> (SBool, SBool)
goal =
     String
-> (st -> st -> SBool)
-> ((res, res) -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving initiation"
         (\st
s st
_ -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
inv st
s)
         (InductionStep -> (res, res) -> InductionResult res
forall a. InductionStep -> (a, 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)
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 -> st -> SBool)
-> ((res, res) -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving consecution"
               (\st
s st
s' -> [SBool] -> SBool
sAnd (st -> SBool
inv st
s SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: st
s st -> st -> SBool
`trans` 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
inv st
s')
               (InductionStep -> (res, res) -> InductionResult res
forall a. InductionStep -> (a, 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 -> st -> SBool)
-> ((res, res) -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving partial correctness"
                     (\st
s st
_ -> 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, res) -> InductionResult res
forall a. InductionStep -> (a, a) -> InductionResult a
Failed InductionStep
PartialCorrectness)
                     (String -> IO ()
msg String
"Done" IO () -> IO (InductionResult res) -> IO (InductionResult res)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InductionResult res -> IO (InductionResult res)
forall a. a -> IO a
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
-> (st -> st -> SBool)
-> ((res, res) -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
m st -> st -> SBool
p (res, res) -> InductionResult res
wrap IO (InductionResult res)
cont = do String -> IO ()
msg String
m
                               res <- (st -> st -> SBool) -> IO (Maybe (res, res))
check st -> st -> SBool
p
                               case res of
                                 Just (res, res)
ex -> InductionResult res -> IO (InductionResult res)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InductionResult res -> IO (InductionResult res))
-> InductionResult res -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ (res, res) -> InductionResult res
wrap (res, res)
ex
                                 Maybe (res, res)
Nothing -> IO (InductionResult res)
cont

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

                                   cs <- checkSat
                                   case cs of
                                     CheckSatResult
Unk    -> String -> Query (Maybe (res, res))
forall a. HasCallStack => String -> a
error String
"Solver said unknown"
                                     DSat{} -> String -> Query (Maybe (res, res))
forall a. HasCallStack => String -> a
error String
"Solver returned a delta-sat result"
                                     CheckSatResult
Unsat  -> Maybe (res, res) -> Query (Maybe (res, res))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (res, res)
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 in state:"
                                                  exS  <- st -> QueryT IO (QueryResult st)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project st
s
                                                  io $ msg $ show exS
                                                  io $ msg "Transitioning to:"
                                                  exS' <- project s'
                                                  io $ msg $ show exS'
                                                  return $ Just (exS, exS')

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