Lang.Crucible.Backend.ProofGoals

This module defines a data strucutre for storing a collection of proof obligations, and the current state of assumptions.

Goals

data ProofGoal asmp goal

A proof goal consists of a collection of assumptions that were in scope when an assertion was made, together with the given assertion.

Constructors

ProofGoal

Fields

• proofAssumptions :: asmp
• proofGoal :: goal

data Goals asmp goal

A collection of goals, which can represent shared assumptions.

Constructors

Assuming asmp !(Goals asmp goal)

Make an assumption that is in context for all the contained goals.

Prove goal

A proof obligation, to be proved in the context of all previously-made assumptions.

ProveConj !(Goals asmp goal) !(Goals asmp goal)

A conjunction of two goals.

Instances

(Show asmp, Show goal) => Show (Goals asmp goal)

Defined in Lang.Crucible.Backend.ProofGoals

Methods

showsPrec :: Int -> Goals asmp goal -> ShowS

show :: Goals asmp goal -> String

showList :: [Goals asmp goal] -> ShowS

goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]

Render the tree of goals as a list instead, duplicating shared assumptions over each goal as necessary.

proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)

Construct a Goals object from a collection of subgoals, all of which are to be proved. This yields Nothing if the collection of goals is empty, and otherwise builds a conjunction of all the goals. Note that there is no new sharing in the resulting structure.

goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)

Helper to conjoin two possibly trivial Goals objects.

traversals

traverseGoals :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp' goal'))

Traverse the structure of a Goals data structure. The function for visiting goals my decide to remove the goal from the structure. If no goals remain after the traversal, the resulting value will be a Nothing.

In a call to 'traverseGoals assumeAction transformer goals', the arguments are used as follows:

• traverseGoals is an action is called every time we encounter an Assuming constructor. The first argument is the original sequence of assumptions. The second argument is a continuation action. The result is a sequence of transformed assumptions and the result of the continuation action.
• assumeAction is a transformer action on goals. Return Nothing if you wish to remove the goal from the overall tree.

traverseOnlyGoals :: (Applicative f, Monoid asmp) => (goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal'))

traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) => (asmp -> goal -> f (Maybe goal')) -> Goals asmp goal -> f (Maybe (Goals asmp goal'))

Visit every goal in a Goals structure, remembering the sequence of assumptions along the way to that goal.

traverseGoalsSeq :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))

Traverse a sequence of Goals data structures. See traverseGoals for an explanation of the action arguments. The resulting sequence may be shorter than the original if some Goals become trivial.

Goal collector

newtype FrameIdentifier

A FrameIdentifier is a value that identifies an an assumption frame. These are expected to be unique when a new frame is pushed onto the stack. This is primarily a debugging aid, to ensure that stack management remains well-bracketed.

Constructors

FrameIdentifier Word64

Instances

Eq FrameIdentifier

Defined in Lang.Crucible.Backend.ProofGoals

Methods

(==) :: FrameIdentifier -> FrameIdentifier -> Bool

(/=) :: FrameIdentifier -> FrameIdentifier -> Bool

Ord FrameIdentifier

Defined in Lang.Crucible.Backend.ProofGoals

Methods

compare :: FrameIdentifier -> FrameIdentifier -> Ordering

(<) :: FrameIdentifier -> FrameIdentifier -> Bool

(<=) :: FrameIdentifier -> FrameIdentifier -> Bool

(>) :: FrameIdentifier -> FrameIdentifier -> Bool

(>=) :: FrameIdentifier -> FrameIdentifier -> Bool

max :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier

min :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier

data GoalCollector asmp goal

A data-strucutre that can incrementally collect goals in context. It keeps track both of the collection of assumptions that lead to the current state, as well as any proof obligations incurred along the way.

emptyGoalCollector :: GoalCollector asmp goal

A collector with no goals and no context.

traversals

traverseGoalCollector :: (Applicative f, Monoid asmp') => (forall a. asmp -> f a -> f (asmp', a)) -> (goal -> f (Maybe goal')) -> GoalCollector asmp goal -> f (GoalCollector asmp' goal')

Traverse the goals in a 'GoalCollector. See traverseGoals for an explaination of the action arguments.

traverseGoalCollectorWithAssumptions :: (Applicative f, Monoid asmp) => (asmp -> goal -> f (Maybe goal')) -> GoalCollector asmp goal -> f (GoalCollector asmp goal')

Traverse the goals in a GoalCollector, keeping track, for each goal, of the assumptions leading to that goal.

Context management

gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector asmp goal

Add a sequence of extra assumptions to the current context.

gcProve :: goal -> GoalCollector asmp goal -> GoalCollector asmp goal

Add a new proof obligation to the current context.

gcPush :: FrameIdentifier -> GoalCollector asmp goal -> GoalCollector asmp goal

Mark the current frame. Using gcPop will unwind to here.

gcPop :: Monoid asmp => GoalCollector asmp goal -> Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal) (Maybe (Goals asmp goal))

Pop to the last push, or all the way to the top, if there were no more pushes. If the result is Left, then we popped until an explicitly marked push; in that case we return:

1. the frame identifier of the popped frame,
2. the assumptions that were forgotten,
3. any proof goals that were generated since the frame push, and
4. the state of the collector before the push.

If the result is Right, then we popped all the way to the top, and the result is the goal tree, or Nothing if there were no goals.

gcAddGoals :: Goals asmp goal -> GoalCollector asmp goal -> GoalCollector asmp goal

Global operations on context

gcRemoveObligations :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal

Remove all collected proof obligations, but keep the current set of assumptions.

gcRestore

Arguments

:: Monoid asmp

=> GoalCollector asmp goal

The assumption state to restore

-> GoalCollector asmp goal

The assumptions state to overwrite

-> GoalCollector asmp goal

This operation restores the assumption state of the first given GoalCollector, overwriting the assumptions state of the second collector. However, all proof obligations in the second collector are retained and placed into the the first goal collector in the base assumption level.

The end result is a goal collector that maintains all the active proof obligations of both collectors, and has the same assumption context as the first collector.

gcReset :: Monoid asmp => GoalCollector asmp goal -> GoalCollector asmp goal

Reset the goal collector to the empty assumption state; but first collect all the pending proof goals and stash them.

gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal)

Get all currently collected goals.

Viewing the assumption state

data AssumptionFrames asmp

The AssumptionFrames data structure captures the current state of assumptions made inside a GoalCollector.

Constructors

AssumptionFrames

Fields

• baseFrame :: !asmp

  Assumptions made at the top level of a solver.

• pushedFrames :: !(Seq (FrameIdentifier, asmp))

  A sequence of pushed frames, together with the assumptions that were made in each frame. The sequence is organized with newest frames on the end (right side) of the sequence.

gcFrames :: forall asmp goal. Monoid asmp => GoalCollector asmp goal -> AssumptionFrames asmp

Return a list of all the assumption frames in this goal collector. The first element of the pair is a collection of assumptions made unconditionaly at top level. The remaining list is a sequence of assumption frames, each consisting of a collection of assumptions made in that frame. Frames closer to the front of the list are older. A gcPop will remove the newest (rightmost) frame from the list.