Copyright	(c) Galois Inc 2024
License	BSD3
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Backend.Prove

Contents

Strategy
- Combiner
- Prover
  - Offline
  - Online
Proving goals

Description

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 (Assertion) that we are trying to prove.
Attempt to prove the conjunction of the assumptions and the negated goal.

If this goal is satisfiable (Sat), then there exists a counterexample that makes the original goal false, so we have disproven the goal. If the negated goal is unsatisfiable (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).

Synopsis

data ProofResult sym t
- = Proved
- | Disproved (GroundEvalFn t) (Maybe (ExprRangeBindings t))
- | Unknown
newtype ProofConsumer sym t r = ProofConsumer (ProofObligation sym -> ProofResult sym t -> IO r)
data ProofStrategy sym m t r = ProofStrategy {
- stratProver :: !(Prover sym m t r)
- stratCombine :: Combiner m r
}
data SubgoalResult r = SubgoalResult {
- subgoalWasProved :: !Bool
- subgoalResult :: !r
}
newtype Combiner m r = Combiner {
- getCombiner :: m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
}
keepGoing :: Monad m => Semigroup r => Combiner m r
failFast :: Monad m => Semigroup r => Combiner m r
data Prover sym m t r = Prover {
- proverProve :: Assumptions sym -> Assertion sym -> ProofConsumer sym t r -> m (SubgoalResult r)
- proverAssume :: Assumptions sym -> m (SubgoalResult r) -> m (SubgoalResult r)
}
offlineProve :: MonadIO m => sym ~ ExprBuilder t st fs => IsSymExprBuilder sym => sym -> LogData -> SolverAdapter st -> Assumptions sym -> Assertion sym -> ProofConsumer sym t r -> m (SubgoalResult r)
offlineProveWithTimeout :: 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)
offlineProver :: MonadError TimedOut m => MonadIO m => sym ~ ExprBuilder t st fs => Timeout -> IsSymExprBuilder sym => sym -> LogData -> SolverAdapter st -> Prover sym m t r
onlineProve :: 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)
onlineProver :: MonadIO m => MonadMask m => SMTReadWriter solver => sym ~ ExprBuilder t st fs => IsSymExprBuilder sym => sym -> SolverProcess t solver -> Prover sym m t r
proveGoals :: Functor m => ProofStrategy sym m t r -> Goals (Assumptions sym) (Assertion sym) -> ProofConsumer sym t r -> m r
proveObligations :: Applicative m => Monoid r => sym ~ ExprBuilder t st fs => ProofStrategy sym m t r -> ProofObligations sym -> ProofConsumer sym t r -> m r
proveCurrentObligations :: MonadIO m => Monoid r => sym ~ ExprBuilder t st fs => IsSymBackend sym bak => bak -> ProofStrategy sym m t r -> ProofConsumer sym t r -> m r

Strategy

data ProofResult sym t Source #

The result of attempting to prove a goal with an SMT solver.

The constructors of this type correspond to those of SatResult.

sym is the symbolic backend, usually ExprBuilder
t is the "brand" parameter to Expr (not a base type)

Constructors

Proved

The goal was proved.

Corresponds to Unsat.

Disproved (GroundEvalFn t) (Maybe (ExprRangeBindings t))

The goal was disproved, and a model that falsifies it is available.

The GroundEvalFn is only available for use during the execution of a ProofConsumer. See SolverAdapter.

The Maybe ExprRangeBindings are Just when using offlineProve and Nothing when using onlineProve.

Corresponds to Sat.

Unknown

The SMT solver returned "unknown".

Corresponds to Unknown.

newtype ProofConsumer sym t r Source #

A callback used to consume a ProofResult.

If the result is Disproved, then this function must consume the GroundEvalFn before returning. See SolverAdapter.

sym is the symbolic backend, usually ExprBuilder
t is the "brand" parameter to Expr (not a base type)
r is the return type of the callback

Constructors

ProofConsumer (ProofObligation sym -> ProofResult sym t -> IO r)

data ProofStrategy sym m t r Source #

A ProofStrategy dictates how results are proved.

sym is the symbolic backend, usually ExprBuilder
m is the monad in which the Prover and Combiner run
t is the "brand" parameter to Expr (not a base type)
r is the return type of the eventual ProofConsumer

Constructors

ProofStrategy
Fields stratProver :: !(Prover sym m t r) Generally `offlineProver` or `onlineProver` stratCombine :: Combiner m r

Combiner

data SubgoalResult r Source #

Whether or not a subgoal was proved, together with the result from a ProofConsumer.

Constructors

SubgoalResult
Fields subgoalWasProved :: !Bool subgoalResult :: !r

Instances

Instances details

Functor SubgoalResult Source #
Instance details Defined in Lang.Crucible.Backend.Prove Methods fmap :: (a -> b) -> SubgoalResult a -> SubgoalResult b # (<$) :: a -> SubgoalResult b -> SubgoalResult a #

newtype Combiner m r Source #

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

Constructors

Combiner
Fields getCombiner :: m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)

keepGoing :: Monad m => Semigroup r => Combiner m r Source #

Combine SubgoalResults using the <> operator. Keep going when subgoals fail.

failFast :: Monad m => Semigroup r => Combiner m r Source #

Combine SubgoalResults using the <> operator. After the first subgoal fails, stop trying to prove further goals.

Prover

data Prover sym m t r Source #

A collection of functions used to prove goals as part of a ProofStrategy.

Constructors

Prover
Fields proverProve :: Assumptions sym -> Assertion sym -> ProofConsumer sym t r -> m (SubgoalResult r) Prove a single goal under some `Assumptions`. proverAssume :: Assumptions sym -> m (SubgoalResult r) -> m (SubgoalResult r) Assume some `Assumptions` in the scope of a subgoal.