tamarin-prover-theory-0.8.5.0: Term manipulation library for the tamarin prover.

Portability GHC only Simon Meier None

Theory.Constraint.System

Description

This is the public interface for constructing and deconstructing constraint systems. The interface for performing constraint solving provided by Theory.Constraint.Solver.

Synopsis

# Constraint systems

data System Source

A constraint system.

Instances

 Eq System Ord System Show System Binary System NFData System HasFrees System

## Construction

The empty constraint system, which is logically equivalent to true.

Whether we are checking for the existence of a trace satisfiying a the current constraint system or whether we're checking that no traces satisfies the current constraint system.

Constructors

 ExistsSomeTrace ExistsNoTrace

Arguments

 :: [LNGuarded] Axioms to add -> CaseDistKind Case distinction kind -> SystemTraceQuantifier Trace quantifier -> LNFormula -> System

Returns the constraint system that has to be proven to show that given formula holds in the context of the given theory.

## Node constraints

sNodes :: forall arr. Arrow arr => Lens arr System (Map NodeId RuleACInst)Source

allKDConcs :: System -> [(NodeId, RuleACInst, LNTerm)]Source

A list of all KD-conclusions in the `System`.

`nodeRule v` accesses the rule label of node `v` under the assumption that it is present in the sequent.

`nodeConcNode` `c` compute the node-id of the node conclusion `c`.

`nodePremNode prem` is the node that this premise is referring to.

`nodePremFact prem se` computes the fact associated to premise `prem` in sequent `se` under the assumption that premise `prem` is a a premise in `se`.

`nodeConcFact (NodeConc (v, i))` accesses the `i`-th conclusion of the rule associated with node `v` under the assumption that `v` is labeled with a rule that has an `i`-th conclusion.

All facts associated to this node premise.

The fact associated with this node conclusion, if there is one.

## Actions

allActions :: System -> [(NodeId, LNFact)]Source

All actions that hold in a sequent.

allKUActions :: System -> [(NodeId, LNFact, LNTerm)]Source

All actions that hold in a sequent.

All actions that hold in a sequent.

kuActionAtoms :: System -> [(NodeId, LNFact, LNTerm)]Source

All KU-actions.

The standard actions, i.e., non-KU-actions.

## Edge and chain constraints

sEdges :: forall arr. Arrow arr => Lens arr System (Set Edge)Source

All unsolved destruction chains in the constraint system.

## Temporal ordering

sLessAtoms :: forall arr. Arrow arr => Lens arr System (Set (NodeId, NodeId))Source

rawLessRel :: System -> [(NodeId, NodeId)]Source

`(from,to)` is in `rawLessRel se` iff we can prove that there is a path (possibly using the `Less` relation) from `from` to `to` in `se` without appealing to transitivity.

rawEdgeRel :: System -> [(NodeId, NodeId)]Source

`(from,to)` is in `rawEdgeRel se` iff we can prove that there is an edge-path from `from` to `to` in `se` without appealing to transitivity.

Returns a predicate that is `True` iff the first argument happens before the second argument in all models of the sequent.

`True` iff the given node id is guaranteed to be instantiated to an index in the trace.

## The last node

sLastAtom :: forall arr. Arrow arr => Lens arr System (Maybe NodeId)Source

`True` iff the given node id is guaranteed to be instantiated to the last index of the trace.

## Equations

sEqStore :: forall arr. Arrow arr => Lens arr System EqStoreSource

Label to access the free substitution of the equation store.

Label to access the conjunction of disjunctions of fresh substutitution in the equation store.

## Formulas

sFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

sSolvedFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

## Lemmas

sLemmas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

insertLemmas :: [LNGuarded] -> System -> SystemSource

## Keeping track of typing assumptions

Case dinstinction kind that are allowed. The order of the kinds corresponds to the subkinding relation: untyped < typed.

Constructors

 UntypedCaseDist TypedCaseDist

## Goals

data GoalStatus Source

The status of a `Goal`. Use its `Semigroup` instance to combine the status info of goals that collapse.

Constructors

 GoalStatus Fields_gsSolved :: Bool _gsNr :: Integer _gsLoopBreaker :: Bool

gsSolved :: forall arr. Arrow arr => Lens arr GoalStatus BoolSource

gsLoopBreaker :: forall arr. Arrow arr => Lens arr GoalStatus BoolSource

gsNr :: forall arr. Arrow arr => Lens arr GoalStatus IntegerSource

sGoals :: forall arr. Arrow arr => Lens arr System (Map Goal GoalStatus)Source

sNextGoalNr :: forall arr. Arrow arr => Lens arr System IntegerSource

# Pretty-printing

Pretty print a sequent

Pretty print the non-graph part of the sequent; i.e. equation store and clauses.