Lang.Crucible.Backend.Prove

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).

Strategy

data ProofResult sym t

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

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

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

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

Constructors

SubgoalResult

Fields

• subgoalWasProved :: !Bool
• subgoalResult :: !r

Instances

Functor SubgoalResult

Defined in Lang.Crucible.Backend.Prove

Methods

fmap :: (a -> b) -> SubgoalResult a -> SubgoalResult b

(<$) :: a -> SubgoalResult b -> SubgoalResult a

newtype Combiner m r

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

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

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

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

Prover

data Prover sym m t r

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.

Offline

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)

Prove a goal using an "offline" solver (i.e., one process per goal).

See offlineProveWithTimeout for a version that integrates Timeouts.

See the module-level documentation for further discussion of offline vs. online solving.

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)

Prove a goal using an "offline" solver, with a timeout.

See offlineProveWithTimeout for a version without Timeouts.

See the module-level documentation for further discussion of offline vs. online solving.

offlineProver :: MonadError TimedOut m => MonadIO m => sym ~ ExprBuilder t st fs => Timeout -> IsSymExprBuilder sym => sym -> LogData -> SolverAdapter st -> Prover sym m t r

Prove goals using offlineProveWithTimeout.

See the module-level documentation for further discussion of offline vs. online solving.

Online

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)

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.

onlineProver :: MonadIO m => MonadMask m => SMTReadWriter solver => sym ~ ExprBuilder t st fs => IsSymExprBuilder sym => sym -> SolverProcess t solver -> Prover sym m t r

Prove goals using onlineProve and onlineAssume.

See the module-level documentation for further discussion of offline vs. online solving.

Proving goals

proveGoals :: Functor m => ProofStrategy sym m t r -> Goals (Assumptions sym) (Assertion sym) -> ProofConsumer sym t r -> m r

Prove a collection of Goals using the specified ProofStrategy.

proveObligations :: Applicative m => Monoid r => sym ~ ExprBuilder t st fs => ProofStrategy sym m t r -> ProofObligations sym -> ProofConsumer sym t r -> m r

Prove a collection of ProofObligations using a ProofStrategy.

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

Prove a the current collection of ProofObligations associated with the symbolic backend (retrieved via getProofObligations).