    -----------------------------------------------------------------------------
    -- |
    -- 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  Nothing)  = "initiation"
       show (Initiation  (Just s :: String
    s)) = "initiation for strengthening " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s
       show (Consecution Nothing)  = "consecution"
       show (Consecution (Just s :: String
    s)) = "consecution for strengthening " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s
       show PartialCorrectness     = "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 Proven       = "Q.E.D."
      show (Failed s :: InductionStep
    s e :: a
    e) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [ "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]
    ++ "."
                                           , "Counter-example to inductiveness:"
                                           , String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ["  " 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 cfg :: SMTConfig
    cfg chatty :: Bool
    chatty setup :: Symbolic ()
    setup initial :: st -> SBool
    initial trans :: st -> [st]
    trans strengthenings :: [(String, st -> SBool)]
    strengthenings inv :: st -> SBool
    inv goal :: 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 "Proving initiation"
             (\s :: 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 "Proving consecution"
                   (\s :: st
    s -> [SBool] -> SBool
    sAnd (st -> SBool
    inv st
    s SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : [st -> SBool
    st st
    s | (_, st :: 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 "Proving partial correctness"
                         (\s :: st
    s -> let (term :: SBool
    term, result :: 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 "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 m :: String
    m p :: a -> SBool
    p wrap :: t -> b
    wrap cont :: 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 ex :: 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
                                     Nothing -> IO b
    cont

            check :: (a -> SBool) -> IO (Maybe a)
    check p :: 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
                                         Unk   -> String -> Query (Maybe a)
    forall a. HasCallStack => String -> a
    error "Solver said unknown"
                                         Unsat -> Maybe a -> Query (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
                                         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 "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 []             cont :: IO (InductionResult a)
    cont = IO (InductionResult a)
    cont
            strengthen ((nm :: String
    nm, st :: st -> SBool
    st):sts :: [(String, st -> SBool)]
    sts) cont :: 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 ("Proving strengthening initation  : " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm)
                                                 (\s :: 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 ("Proving strengthening consecution: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    nm)
                                                       (\s :: 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)