{-|
Module      : Lang.Crucible.Backend.Prove
Description : Proving goals under assumptions
Copyright   : (c) Galois, Inc 2024
License     : BSD3

This module contains helpers to dispatch the proof obligations arising from
symbolic execution using SMT solvers. There are several dimensions of
configurability, encapsulated in a 'ProofStrategy':

* Offline vs. online: Offline solvers ('offlineProver') are simpler to manage
  and more easily parallelized, but starting processes adds overhead, and online
  solvers ('onlineProver') can share state as assumptions are added. See the
  top-level README for What4 for further discussion of this choice.
* Failing fast ('failFast') vs. keeping going ('keepGoing')
* Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without
  ('offlineProve')
* Parallelism: Not yet available via helpers in this module, but may be added to
  a 'ProofStrategy' by clients.

Once an appropriate strategy has been selected, it can be passed to entrypoints
such as 'proveObligations' to dispatch proof obligations.

When proving a single goal, the overall approach is:

* Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
  from branch conditions).
* Negate the goal ('CB.Assertion') that we are trying to prove.
* Attempt to prove the conjunction of the assumptions and the negated goal.

If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample
that makes the original goal false, so we have disproven the goal. If the
negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the
original goal is proven.

Another way to think of this is as the negated material conditional
(implication) @not (assumptions -> assertion)@. This formula is equivalent
to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not
assertion)@.
-}

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lang.Crucible.Backend.Prove
  ( -- * Strategy
    ProofResult(..)
  , ProofConsumer(..)
  , ProofStrategy(..)
    -- ** Combiner
  , SubgoalResult(..)
  , Combiner(..)
  , keepGoing
  , failFast
    -- ** Prover
  , Prover(..)
    -- *** Offline
  , offlineProve
  , offlineProveWithTimeout
  , offlineProver
    -- *** Online
  , onlineProve
  , onlineProver
    -- * Proving goals
  , proveGoals
  , proveObligations
  , proveCurrentObligations
  ) where

import           Control.Lens ((^.))
import           Control.Monad.Catch (MonadMask)
import           Control.Monad.Error.Class (MonadError, liftEither)
import           Control.Monad.IO.Class (MonadIO(liftIO))
import qualified Control.Monad.Reader as Reader

import qualified What4.Interface as W4
import qualified What4.Expr as WE
import qualified What4.Protocol.Online as WPO
import qualified What4.Protocol.SMTWriter as W4SMT
import qualified What4.SatResult as W4R
import qualified What4.Solver.Adapter as WSA

import qualified Lang.Crucible.Backend as CB
import           Lang.Crucible.Backend.Assumptions (Assumptions)
import           Lang.Crucible.Utils.Timeout (Timeout, TimedOut)
import qualified Lang.Crucible.Utils.Timeout as CTO

-- | Local helper
consumeGoals ::
  -- | Consume an 'Assuming'
  (asmp -> a -> a) ->
  -- | Consume a 'Prove'
  (goal -> a) ->
  -- | Consume a 'ProveConj'
  (a -> a -> a) ->
  CB.Goals asmp goal ->
  a
consumeGoals :: forall asmp a goal.
(asmp -> a -> a)
-> (goal -> a) -> (a -> a -> a) -> Goals asmp goal -> a
consumeGoals asmp -> a -> a
onAssumption goal -> a
onGoal a -> a -> a
onConj = Goals asmp goal -> a
go
  where
  go :: Goals asmp goal -> a
go (CB.Prove goal
gl) = goal -> a
onGoal goal
gl
  go (CB.Assuming asmp
as Goals asmp goal
gl) = asmp -> a -> a
onAssumption asmp
as (Goals asmp goal -> a
go Goals asmp goal
gl)
  go (CB.ProveConj Goals asmp goal
g1 Goals asmp goal
g2) = a -> a -> a
onConj (Goals asmp goal -> a
go Goals asmp goal
g1) (Goals asmp goal -> a
go Goals asmp goal
g2)

-- | Local helper
consumeGoalsWithAssumptions ::
  forall asmp goal a.
  Monoid asmp =>
  -- | Consume a 'Prove'
  (asmp -> goal -> a) ->
  -- | Consume a 'ProveConj'
  (a -> a -> a) ->
  CB.Goals asmp goal ->
  a
consumeGoalsWithAssumptions :: forall asmp goal a.
Monoid asmp =>
(asmp -> goal -> a) -> (a -> a -> a) -> Goals asmp goal -> a
consumeGoalsWithAssumptions asmp -> goal -> a
onGoal a -> a -> a
onConj Goals asmp goal
goals =
  Reader asmp a -> asmp -> a
forall r a. Reader r a -> r -> a
Reader.runReader (Goals asmp goal -> Reader asmp a
go Goals asmp goal
goals) asmp
forall a. Monoid a => a
mempty
  where
  go :: CB.Goals asmp goal -> Reader.Reader asmp a
  go :: Goals asmp goal -> Reader asmp a
go =
    (asmp -> Reader asmp a -> Reader asmp a)
-> (goal -> Reader asmp a)
-> (Reader asmp a -> Reader asmp a -> Reader asmp a)
-> Goals asmp goal
-> Reader asmp a
forall asmp a goal.
(asmp -> a -> a)
-> (goal -> a) -> (a -> a -> a) -> Goals asmp goal -> a
consumeGoals
      (\asmp
asmp Reader asmp a
gl -> (asmp -> asmp) -> Reader asmp a -> Reader asmp a
forall a.
(asmp -> asmp)
-> ReaderT asmp Identity a -> ReaderT asmp Identity a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
Reader.local (asmp -> asmp -> asmp
forall a. Semigroup a => a -> a -> a
<> asmp
asmp) Reader asmp a
gl)
      (\goal
gl -> (asmp -> a) -> Reader asmp a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
Reader.asks (\asmp
asmps -> asmp -> goal -> a
onGoal asmp
asmps goal
gl))
      (\Reader asmp a
g1 Reader asmp a
g2 -> a -> a -> a
onConj (a -> a -> a) -> Reader asmp a -> ReaderT asmp Identity (a -> a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Reader asmp a
g1 ReaderT asmp Identity (a -> a) -> Reader asmp a -> Reader asmp a
forall a b.
ReaderT asmp Identity (a -> b)
-> ReaderT asmp Identity a -> ReaderT asmp Identity b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Reader asmp a
g2)

---------------------------------------------------------------------
-- * Strategy

-- | The result of attempting to prove a goal with an SMT solver.
--
-- The constructors of this type correspond to those of 'W4R.SatResult'.
--
-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
data ProofResult sym t
   = -- | The goal was proved.
     --
     -- Corresponds to 'W4R.Unsat'.
     Proved
     -- | The goal was disproved, and a model that falsifies it is available.
     --
     -- The 'WE.GroundEvalFn' is only available for use during the execution of
     -- a 'ProofConsumer'. See 'WSA.SolverAdapter'.
     --
     -- The @'Maybe' 'WE.ExprRangeBindings'@ are 'Just' when using
     -- 'offlineProve' and 'Nothing' when using 'onlineProve'.
     --
     -- Corresponds to 'W4R.Sat'.
   | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
     -- | The SMT solver returned \"unknown\".
     --
     -- Corresponds to 'W4R.Unknown'.
   | Unknown

-- | A 'ProofStrategy' dictates how results are proved.
--
-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
-- * @r@ is the return type of the eventual 'ProofConsumer'
data ProofStrategy sym m t r
  = ProofStrategy
    { -- | Generally 'offlineProver' or 'onlineProver'
      forall sym (m :: Type -> Type) t r.
ProofStrategy sym m t r -> Prover sym m t r
stratProver :: {-# UNPACK #-} !(Prover sym m t r)
    , forall sym (m :: Type -> Type) t r.
ProofStrategy sym m t r -> Combiner m r
stratCombine :: Combiner m r
    }

-- | A callback used to consume a 'ProofResult'.
--
-- If the result is 'Disproved', then this function must consume the
-- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.
--
-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
-- * @r@ is the return type of the callback
newtype ProofConsumer sym t r
  = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)

---------------------------------------------------------------------
-- *** Combiner

-- | Whether or not a subgoal was proved, together with the result from a
-- 'ProofConsumer'.
data SubgoalResult r
  = SubgoalResult
    { forall r. SubgoalResult r -> Bool
subgoalWasProved :: !Bool
    , forall r. SubgoalResult r -> r
subgoalResult :: !r
    }
  deriving (forall a b. (a -> b) -> SubgoalResult a -> SubgoalResult b)
-> (forall a b. a -> SubgoalResult b -> SubgoalResult a)
-> Functor SubgoalResult
forall a b. a -> SubgoalResult b -> SubgoalResult a
forall a b. (a -> b) -> SubgoalResult a -> SubgoalResult b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SubgoalResult a -> SubgoalResult b
fmap :: forall a b. (a -> b) -> SubgoalResult a -> SubgoalResult b
$c<$ :: forall a b. a -> SubgoalResult b -> SubgoalResult a
<$ :: forall a b. a -> SubgoalResult b -> SubgoalResult a
Functor

-- | How to combine results of proofs, used as part of a 'ProofStrategy'.
--
-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
-- * @r@ is the return type of the eventual 'ProofConsumer'
newtype Combiner m r
  = Combiner
    { forall (m :: Type -> Type) r.
Combiner m r
-> m (SubgoalResult r)
-> m (SubgoalResult r)
-> m (SubgoalResult r)
getCombiner ::
        m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
    }

-- | Combine 'SubgoalResult's using the '<>' operator. Keep going when subgoals
-- fail.
keepGoing :: Monad m => Semigroup r => Combiner m r
keepGoing :: forall (m :: Type -> Type) r.
(Monad m, Semigroup r) =>
Combiner m r
keepGoing = (m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
forall (m :: Type -> Type) r.
(m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
Combiner ((m (SubgoalResult r)
  -> m (SubgoalResult r) -> m (SubgoalResult r))
 -> Combiner m r)
-> (m (SubgoalResult r)
    -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
forall a b. (a -> b) -> a -> b
$ \m (SubgoalResult r)
a1 m (SubgoalResult r)
a2 -> SubgoalResult r -> SubgoalResult r -> SubgoalResult r
forall r.
Semigroup r =>
SubgoalResult r -> SubgoalResult r -> SubgoalResult r
subgoalAnd (SubgoalResult r -> SubgoalResult r -> SubgoalResult r)
-> m (SubgoalResult r) -> m (SubgoalResult r -> SubgoalResult r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m (SubgoalResult r)
a1 m (SubgoalResult r -> SubgoalResult r)
-> m (SubgoalResult r) -> m (SubgoalResult r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> m (SubgoalResult r)
a2
  where
  subgoalAnd ::
    Semigroup r =>
    SubgoalResult r ->
    SubgoalResult r ->
    SubgoalResult r
  subgoalAnd :: forall r.
Semigroup r =>
SubgoalResult r -> SubgoalResult r -> SubgoalResult r
subgoalAnd (SubgoalResult Bool
ok1 r
r1) (SubgoalResult Bool
ok2 r
r2) =
    Bool -> r -> SubgoalResult r
forall r. Bool -> r -> SubgoalResult r
SubgoalResult (Bool
ok1 Bool -> Bool -> Bool
&& Bool
ok2) (r
r1 r -> r -> r
forall a. Semigroup a => a -> a -> a
<> r
r2)

-- | Combine 'SubgoalResult's using the '<>' operator. After the first subgoal
-- fails, stop trying to prove further goals.
failFast :: Monad m => Semigroup r => Combiner m r
failFast :: forall (m :: Type -> Type) r.
(Monad m, Semigroup r) =>
Combiner m r
failFast = (m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
forall (m :: Type -> Type) r.
(m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
Combiner ((m (SubgoalResult r)
  -> m (SubgoalResult r) -> m (SubgoalResult r))
 -> Combiner m r)
-> (m (SubgoalResult r)
    -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Combiner m r
forall a b. (a -> b) -> a -> b
$ \m (SubgoalResult r)
sr1 m (SubgoalResult r)
sr2 -> do
  SubgoalResult Bool
ok1 r
r1 <- m (SubgoalResult r)
sr1
  if Bool
ok1
  then do
    SubgoalResult Bool
ok2 r
r2 <- m (SubgoalResult r)
sr2
    SubgoalResult r -> m (SubgoalResult r)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> r -> SubgoalResult r
forall r. Bool -> r -> SubgoalResult r
SubgoalResult Bool
ok2 (r
r1 r -> r -> r
forall a. Semigroup a => a -> a -> a
<> r
r2))
  else SubgoalResult r -> m (SubgoalResult r)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> r -> SubgoalResult r
forall r. Bool -> r -> SubgoalResult r
SubgoalResult Bool
False r
r1)

isProved :: ProofResult sym t -> Bool
isProved :: forall sym t. ProofResult sym t -> Bool
isProved =
  \case
    Proved {} -> Bool
True
    Disproved {} -> Bool
False
    Unknown {} -> Bool
False

---------------------------------------------------------------------
-- ** Prover

-- | A collection of functions used to prove goals as part of a 'ProofStrategy'.
data Prover sym m t r
  = Prover
    { -- | Prove a single goal under some 'Assumptions'.
      forall sym (m :: Type -> Type) t r.
Prover sym m t r
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
proverProve ::
        Assumptions sym ->
        CB.Assertion sym ->
        ProofConsumer sym t r ->
        m (SubgoalResult r)
      -- | Assume some 'Assumptions' in the scope of a subgoal.
    , forall sym (m :: Type -> Type) t r.
Prover sym m t r
-> Assumptions sym -> m (SubgoalResult r) -> m (SubgoalResult r)
proverAssume ::
        Assumptions sym ->
        m (SubgoalResult r) ->
        m (SubgoalResult r)
    }

---------------------------------------------------------------------
-- *** Offline

-- Not exported
offlineProveIO ::
  (sym ~ WE.ExprBuilder t st fs) =>
  W4.IsSymExprBuilder sym =>
  sym ->
  WSA.LogData ->
  WSA.SolverAdapter st ->
  Assumptions sym ->
  CB.Assertion sym ->
  ProofConsumer sym t r ->
  IO (SubgoalResult r)
offlineProveIO :: forall sym t (st :: Type -> Type) fs r.
(sym ~ ExprBuilder t st fs, IsSymExprBuilder sym) =>
sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> IO (SubgoalResult r)
offlineProveIO sym
sym LogData
ld SolverAdapter st
adapter Assumptions sym
asmps Assertion sym
goal (ProofConsumer ProofObligation sym -> ProofResult sym t -> IO r
k) = do
  let goalPred :: Expr t BaseBoolType
goalPred = Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
goal LabeledPred (Expr t BaseBoolType) SimError
-> Getting
     (Expr t BaseBoolType)
     (LabeledPred (Expr t BaseBoolType) SimError)
     (Expr t BaseBoolType)
-> Expr t BaseBoolType
forall s a. s -> Getting a s a -> a
^. Getting
  (Expr t BaseBoolType)
  (LabeledPred (Expr t BaseBoolType) SimError)
  (Expr t BaseBoolType)
forall pred msg pred' (f :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
CB.labeledPred
  Expr t BaseBoolType
asmsPred <- sym -> Assumptions sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
CB.assumptionsPred sym
sym Assumptions sym
asmps
  Expr t BaseBoolType
notGoal <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym Pred sym
Expr t BaseBoolType
goalPred
  SolverAdapter st
-> forall t fs a.
   ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
forall (st :: Type -> Type).
SolverAdapter st
-> forall t fs a.
   ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]
   -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
       -> IO a)
   -> IO a
WSA.solver_adapter_check_sat SolverAdapter st
adapter sym
ExprBuilder t st fs
sym LogData
ld [Expr t BaseBoolType
asmsPred, Expr t BaseBoolType
notGoal] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO (SubgoalResult r))
 -> IO (SubgoalResult r))
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (SubgoalResult r))
-> IO (SubgoalResult r)
forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
r ->
    let r' :: ProofResult sym t
r' =
          case SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
r of
            W4R.Sat (GroundEvalFn t
gfn, Maybe (ExprRangeBindings t)
binds) -> GroundEvalFn t -> Maybe (ExprRangeBindings t) -> ProofResult sym t
forall sym t.
GroundEvalFn t -> Maybe (ExprRangeBindings t) -> ProofResult sym t
Disproved GroundEvalFn t
gfn Maybe (ExprRangeBindings t)
binds
            W4R.Unsat () -> ProofResult sym t
forall sym t. ProofResult sym t
Proved
            SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
W4R.Unknown -> ProofResult sym t
forall sym t. ProofResult sym t
Unknown
    in Bool -> r -> SubgoalResult r
forall r. Bool -> r -> SubgoalResult r
SubgoalResult (ProofResult sym t -> Bool
forall sym t. ProofResult sym t -> Bool
isProved ProofResult sym t
r') (r -> SubgoalResult r) -> IO r -> IO (SubgoalResult r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofObligation sym -> ProofResult sym t -> IO r
k (CrucibleAssumptions (Expr t)
-> LabeledPred (Expr t BaseBoolType) SimError
-> ProofGoal
     (CrucibleAssumptions (Expr t))
     (LabeledPred (Expr t BaseBoolType) SimError)
forall asmp goal. asmp -> goal -> ProofGoal asmp goal
CB.ProofGoal Assumptions sym
CrucibleAssumptions (Expr t)
asmps Assertion sym
LabeledPred (Expr t BaseBoolType) SimError
goal) ProofResult sym t
r'

-- | Prove a goal using an \"offline\" solver (i.e., one process per goal).
--
-- See 'offlineProveWithTimeout' for a version that integrates 'Timeout's.
--
-- See the module-level documentation for further discussion of offline vs.
-- online solving.
offlineProve ::
  MonadIO m =>
  (sym ~ WE.ExprBuilder t st fs) =>
  W4.IsSymExprBuilder sym =>
  sym ->
  WSA.LogData ->
  WSA.SolverAdapter st ->
  Assumptions sym ->
  CB.Assertion sym ->
  ProofConsumer sym t r ->
  m (SubgoalResult r)
offlineProve :: forall (m :: Type -> Type) sym t (st :: Type -> Type) fs r.
(MonadIO m, sym ~ ExprBuilder t st fs, IsSymExprBuilder sym) =>
sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
offlineProve sym
sym LogData
ld SolverAdapter st
adapter Assumptions sym
asmps Assertion sym
goal ProofConsumer sym t r
k =
  IO (SubgoalResult r) -> m (SubgoalResult r)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> IO (SubgoalResult r)
forall sym t (st :: Type -> Type) fs r.
(sym ~ ExprBuilder t st fs, IsSymExprBuilder sym) =>
sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> IO (SubgoalResult r)
offlineProveIO sym
sym LogData
ld SolverAdapter st
adapter Assumptions sym
asmps Assertion sym
goal ProofConsumer sym t r
k)

-- | Prove a goal using an \"offline\" solver, with a timeout.
--
-- See 'offlineProveWithTimeout' for a version without 'Timeout's.
--
-- See the module-level documentation for further discussion of offline vs.
-- online solving.
offlineProveWithTimeout ::
  MonadError TimedOut m =>
  MonadIO m =>
  (sym ~ WE.ExprBuilder t st fs) =>
  W4.IsSymExprBuilder sym =>
  Timeout ->
  sym ->
  WSA.LogData ->
  WSA.SolverAdapter st ->
  Assumptions sym ->
  CB.Assertion sym ->
  ProofConsumer sym t r ->
  m (SubgoalResult r)
offlineProveWithTimeout :: forall (m :: Type -> Type) sym t (st :: Type -> Type) fs r.
(MonadError TimedOut m, MonadIO m, sym ~ ExprBuilder t st fs,
 IsSymExprBuilder sym) =>
Timeout
-> sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
offlineProveWithTimeout Timeout
to sym
sym LogData
ld SolverAdapter st
adapter Assumptions sym
asmps Assertion sym
goal ProofConsumer sym t r
k = do
  Either TimedOut (SubgoalResult r)
r <- IO (Either TimedOut (SubgoalResult r))
-> m (Either TimedOut (SubgoalResult r))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Timeout
-> IO (SubgoalResult r) -> IO (Either TimedOut (SubgoalResult r))
forall a. Timeout -> IO a -> IO (Either TimedOut a)
CTO.withTimeout Timeout
to (sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> IO (SubgoalResult r)
forall sym t (st :: Type -> Type) fs r.
(sym ~ ExprBuilder t st fs, IsSymExprBuilder sym) =>
sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> IO (SubgoalResult r)
offlineProveIO sym
sym LogData
ld SolverAdapter st
adapter Assumptions sym
asmps Assertion sym
goal ProofConsumer sym t r
k))
  Either TimedOut (SubgoalResult r) -> m (SubgoalResult r)
forall e (m :: Type -> Type) a. MonadError e m => Either e a -> m a
liftEither Either TimedOut (SubgoalResult r)
r

-- | Prove goals using 'offlineProveWithTimeout'.
--
-- See the module-level documentation for further discussion of offline vs.
-- online solving.
offlineProver ::
  MonadError TimedOut m =>
  MonadIO m =>
  (sym ~ WE.ExprBuilder t st fs) =>
  Timeout ->
  W4.IsSymExprBuilder sym =>
  sym ->
  WSA.LogData ->
  WSA.SolverAdapter st ->
  Prover sym m t r
offlineProver :: forall (m :: Type -> Type) sym t (st :: Type -> Type) fs r.
(MonadError TimedOut m, MonadIO m, sym ~ ExprBuilder t st fs) =>
Timeout
-> IsSymExprBuilder sym =>
   sym -> LogData -> SolverAdapter st -> Prover sym m t r
offlineProver Timeout
to sym
sym LogData
ld SolverAdapter st
adapter =
  Prover
  { proverProve :: Assumptions sym
-> Assertion sym -> ProofConsumer sym t r -> m (SubgoalResult r)
proverProve = Timeout
-> sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
forall (m :: Type -> Type) sym t (st :: Type -> Type) fs r.
(MonadError TimedOut m, MonadIO m, sym ~ ExprBuilder t st fs,
 IsSymExprBuilder sym) =>
Timeout
-> sym
-> LogData
-> SolverAdapter st
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
offlineProveWithTimeout Timeout
to sym
sym LogData
ld SolverAdapter st
adapter
  , proverAssume :: Assumptions sym -> m (SubgoalResult r) -> m (SubgoalResult r)
proverAssume = \Assumptions sym
_asmps m (SubgoalResult r)
a -> m (SubgoalResult r)
a
  }

---------------------------------------------------------------------
-- *** Online

-- | Prove a goal using an \"online\" solver (i.e., one process for all goals).
--
-- See the module-level documentation for further discussion of offline vs.
-- online solving.
onlineProve ::
  MonadIO m =>
  W4SMT.SMTReadWriter solver =>
  (sym ~ WE.ExprBuilder t st fs) =>
  W4.IsSymExprBuilder sym =>
  WPO.SolverProcess t solver ->
  Assumptions sym ->
  CB.Assertion sym ->
  ProofConsumer sym t r ->
  m (SubgoalResult r)
onlineProve :: forall (m :: Type -> Type) solver sym t (st :: Type -> Type) fs r.
(MonadIO m, SMTReadWriter solver, sym ~ ExprBuilder t st fs,
 IsSymExprBuilder sym) =>
SolverProcess t solver
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
onlineProve SolverProcess t solver
sProc Assumptions sym
asmps Assertion sym
goal (ProofConsumer ProofObligation sym -> ProofResult sym t -> IO r
k) =
  IO (SubgoalResult r) -> m (SubgoalResult r)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SubgoalResult r) -> m (SubgoalResult r))
-> IO (SubgoalResult r) -> m (SubgoalResult r)
forall a b. (a -> b) -> a -> b
$ SolverProcess t solver
-> String
-> BoolExpr t
-> (SatResult (GroundEvalFn t) () -> IO (SubgoalResult r))
-> IO (SubgoalResult r)
forall solver scope a.
SMTReadWriter solver =>
SolverProcess scope solver
-> String
-> BoolExpr scope
-> (SatResult (GroundEvalFn scope) () -> IO a)
-> IO a
WPO.checkSatisfiableWithModel SolverProcess t solver
sProc String
"prove" (Assertion sym
LabeledPred (BoolExpr t) SimError
goal LabeledPred (BoolExpr t) SimError
-> Getting
     (BoolExpr t) (LabeledPred (BoolExpr t) SimError) (BoolExpr t)
-> BoolExpr t
forall s a. s -> Getting a s a -> a
^. Getting
  (BoolExpr t) (LabeledPred (BoolExpr t) SimError) (BoolExpr t)
forall pred msg pred' (f :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
CB.labeledPred) ((SatResult (GroundEvalFn t) () -> IO (SubgoalResult r))
 -> IO (SubgoalResult r))
-> (SatResult (GroundEvalFn t) () -> IO (SubgoalResult r))
-> IO (SubgoalResult r)
forall a b. (a -> b) -> a -> b
$ \SatResult (GroundEvalFn t) ()
r ->
    let r' :: ProofResult sym t
r' =
          case SatResult (GroundEvalFn t) ()
r of
            W4R.Sat GroundEvalFn t
gfn -> GroundEvalFn t -> Maybe (ExprRangeBindings t) -> ProofResult sym t
forall sym t.
GroundEvalFn t -> Maybe (ExprRangeBindings t) -> ProofResult sym t
Disproved GroundEvalFn t
gfn Maybe (ExprRangeBindings t)
forall a. Maybe a
Nothing
            W4R.Unsat () -> ProofResult sym t
forall sym t. ProofResult sym t
Proved
            SatResult (GroundEvalFn t) ()
W4R.Unknown -> ProofResult sym t
forall sym t. ProofResult sym t
Unknown
    in Bool -> r -> SubgoalResult r
forall r. Bool -> r -> SubgoalResult r
SubgoalResult (ProofResult sym t -> Bool
forall sym t. ProofResult sym t -> Bool
isProved ProofResult sym t
r') (r -> SubgoalResult r) -> IO r -> IO (SubgoalResult r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofObligation sym -> ProofResult sym t -> IO r
k (CrucibleAssumptions (Expr t)
-> LabeledPred (BoolExpr t) SimError
-> ProofGoal
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall asmp goal. asmp -> goal -> ProofGoal asmp goal
CB.ProofGoal Assumptions sym
CrucibleAssumptions (Expr t)
asmps Assertion sym
LabeledPred (BoolExpr t) SimError
goal) ProofResult sym t
r'

-- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame').
onlineAssume :: 
  MonadIO m =>
  MonadMask m =>
  W4SMT.SMTReadWriter solver =>
  W4.IsSymExprBuilder sym =>
  (W4.SymExpr sym ~ WE.Expr t) =>
  sym ->
  WPO.SolverProcess t solver ->
  Assumptions sym ->
  m r ->
  m r
onlineAssume :: forall (m :: Type -> Type) solver sym t r.
(MonadIO m, MonadMask m, SMTReadWriter solver,
 IsSymExprBuilder sym, SymExpr sym ~ Expr t) =>
sym -> SolverProcess t solver -> Assumptions sym -> m r -> m r
onlineAssume sym
sym SolverProcess t solver
sProc Assumptions sym
asmps m r
a =
  SolverProcess t solver -> m r -> m r
forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess t solver
sProc (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      let conn :: WriterConn t solver
conn = SolverProcess t solver -> WriterConn t solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
WPO.solverConn SolverProcess t solver
sProc
      BoolExpr t
asmpsPred <- sym -> Assumptions sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
CB.assumptionsPred sym
sym Assumptions sym
asmps
      Term solver
term <- WriterConn t solver -> BoolExpr t -> IO (Term solver)
forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
W4SMT.mkFormula WriterConn t solver
conn BoolExpr t
asmpsPred
      WriterConn t solver -> Term solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Term h -> IO ()
W4SMT.assumeFormula WriterConn t solver
conn Term solver
term
      () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    m r
a

-- | Prove goals using 'onlineProve' and 'onlineAssume'.
--
-- See the module-level documentation for further discussion of offline vs.
-- online solving.
onlineProver ::
  MonadIO m =>
  MonadMask m =>
  W4SMT.SMTReadWriter solver =>
  (sym ~ WE.ExprBuilder t st fs) =>
  W4.IsSymExprBuilder sym =>
  sym ->
  WPO.SolverProcess t solver ->
  Prover sym m t r
onlineProver :: forall (m :: Type -> Type) solver sym t (st :: Type -> Type) fs r.
(MonadIO m, MonadMask m, SMTReadWriter solver,
 sym ~ ExprBuilder t st fs, IsSymExprBuilder sym) =>
sym -> SolverProcess t solver -> Prover sym m t r
onlineProver sym
sym SolverProcess t solver
sProc =
  Prover
  { proverProve :: Assumptions sym
-> Assertion sym -> ProofConsumer sym t r -> m (SubgoalResult r)
proverProve = SolverProcess t solver
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
forall (m :: Type -> Type) solver sym t (st :: Type -> Type) fs r.
(MonadIO m, SMTReadWriter solver, sym ~ ExprBuilder t st fs,
 IsSymExprBuilder sym) =>
SolverProcess t solver
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
onlineProve SolverProcess t solver
sProc
  , proverAssume :: Assumptions sym -> m (SubgoalResult r) -> m (SubgoalResult r)
proverAssume = sym
-> SolverProcess t solver
-> Assumptions sym
-> m (SubgoalResult r)
-> m (SubgoalResult r)
forall (m :: Type -> Type) solver sym t r.
(MonadIO m, MonadMask m, SMTReadWriter solver,
 IsSymExprBuilder sym, SymExpr sym ~ Expr t) =>
sym -> SolverProcess t solver -> Assumptions sym -> m r -> m r
onlineAssume sym
sym SolverProcess t solver
sProc
  }

---------------------------------------------------------------------
-- * Proving goals

-- | Prove a collection of 'CB.Goals' using the specified 'ProofStrategy'.
proveGoals ::
  Functor m =>
  ProofStrategy sym m t r ->
  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
  ProofConsumer sym t r ->
  m r
proveGoals :: forall (m :: Type -> Type) sym t r.
Functor m =>
ProofStrategy sym m t r
-> Goals (Assumptions sym) (Assertion sym)
-> ProofConsumer sym t r
-> m r
proveGoals (ProofStrategy Prover sym m t r
prover (Combiner m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
comb)) Goals (CrucibleAssumptions (SymExpr sym)) (Assertion sym)
goals ProofConsumer sym t r
k =
  (SubgoalResult r -> r) -> m (SubgoalResult r) -> m r
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap SubgoalResult r -> r
forall r. SubgoalResult r -> r
subgoalResult (m (SubgoalResult r) -> m r) -> m (SubgoalResult r) -> m r
forall a b. (a -> b) -> a -> b
$
    (CrucibleAssumptions (SymExpr sym)
 -> Assertion sym -> m (SubgoalResult r))
-> (m (SubgoalResult r)
    -> m (SubgoalResult r) -> m (SubgoalResult r))
-> Goals (CrucibleAssumptions (SymExpr sym)) (Assertion sym)
-> m (SubgoalResult r)
forall asmp goal a.
Monoid asmp =>
(asmp -> goal -> a) -> (a -> a -> a) -> Goals asmp goal -> a
consumeGoalsWithAssumptions
      (\CrucibleAssumptions (SymExpr sym)
asmps Assertion sym
gl -> Prover sym m t r
-> CrucibleAssumptions (SymExpr sym)
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
forall sym (m :: Type -> Type) t r.
Prover sym m t r
-> Assumptions sym
-> Assertion sym
-> ProofConsumer sym t r
-> m (SubgoalResult r)
proverProve Prover sym m t r
prover CrucibleAssumptions (SymExpr sym)
asmps Assertion sym
gl ProofConsumer sym t r
k)
      m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
comb
      Goals (CrucibleAssumptions (SymExpr sym)) (Assertion sym)
goals

-- | Prove a collection of 'CB.ProofObligations' using a 'ProofStrategy'.
proveObligations ::
  Applicative m =>
  Monoid r =>
  (sym ~ WE.ExprBuilder t st fs) =>
  ProofStrategy sym m t r ->
  CB.ProofObligations sym ->
  ProofConsumer sym t r ->
  m r
proveObligations :: forall (m :: Type -> Type) r sym t (st :: Type -> Type) fs.
(Applicative m, Monoid r, sym ~ ExprBuilder t st fs) =>
ProofStrategy sym m t r
-> ProofObligations sym -> ProofConsumer sym t r -> m r
proveObligations ProofStrategy sym m t r
strat ProofObligations sym
obligations ProofConsumer sym t r
k =
  case ProofObligations sym
obligations of
    ProofObligations sym
Nothing -> r -> m r
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure r
forall a. Monoid a => a
mempty
    Just Goals (Assumptions sym) (Assertion sym)
goals -> ProofStrategy sym m t r
-> Goals (Assumptions sym) (Assertion sym)
-> ProofConsumer sym t r
-> m r
forall (m :: Type -> Type) sym t r.
Functor m =>
ProofStrategy sym m t r
-> Goals (Assumptions sym) (Assertion sym)
-> ProofConsumer sym t r
-> m r
proveGoals ProofStrategy sym m t r
strat Goals (Assumptions sym) (Assertion sym)
goals ProofConsumer sym t r
k

-- | Prove a the current collection of 'CB.ProofObligations' associated with the
-- symbolic backend (retrieved via 'CB.getProofObligations').
proveCurrentObligations ::
  MonadIO m =>
  Monoid r =>
  (sym ~ WE.ExprBuilder t st fs) =>
  CB.IsSymBackend sym bak =>
  bak ->
  ProofStrategy sym m t r ->
  ProofConsumer sym t r ->
  m r
proveCurrentObligations :: forall (m :: Type -> Type) r sym t (st :: Type -> Type) fs bak.
(MonadIO m, Monoid r, sym ~ ExprBuilder t st fs,
 IsSymBackend sym bak) =>
bak -> ProofStrategy sym m t r -> ProofConsumer sym t r -> m r
proveCurrentObligations bak
bak ProofStrategy sym m t r
strat ProofConsumer sym t r
k = do
  Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
obligations <- IO
  (Maybe
     (Goals
        (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
        (LabeledPred
           (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)))
-> m (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
CB.getProofObligations bak
bak)
  ProofStrategy sym m t r
-> ProofObligations sym -> ProofConsumer sym t r -> m r
forall (m :: Type -> Type) r sym t (st :: Type -> Type) fs.
(Applicative m, Monoid r, sym ~ ExprBuilder t st fs) =>
ProofStrategy sym m t r
-> ProofObligations sym -> ProofConsumer sym t r -> m r
proveObligations ProofStrategy sym m t r
strat ProofObligations sym
Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
obligations ProofConsumer sym t r
k