Portability	GHC only
Maintainer	Simon Meier <iridcode@gmail.com>
Safe Haskell	None

Theory.Constraint.Solver

Contents

Constraint systems
Proof contexts
Constraint reduction rules
- Contradictions
- Precomputed case distinctions
Proof methods
- Convenience export

Description

The public interface of the constraint solver, which implements all constraint reduction rules and together with a rule application heuristic.

Synopsis

Constraint systems

module Theory.Constraint.System

Proof contexts

The proof context captures all relevant information about the context in which we are using the constraint solver. These are things like the signature of the message theory, the multiset rewriting rules of the protocol, the available precomputed case distinctions, whether induction should be applied or not, whether typed or untyped case distinctions are used, and whether we are looking for the existence of a trace or proving the absence of any trace satisfying the constraint system.

data ProofContext Source

A proof context contains the globally fresh facts, classified rewrite rules and the corresponding precomputed premise case distinction theorems.

Constructors

ProofContext
Fields _pcSignature :: SignatureWithMaude _pcRules :: ClassifiedRules _pcInjectiveFactInsts :: Set FactTag _pcCaseDistKind :: CaseDistKind _pcCaseDists :: [CaseDistinction] _pcUseInduction :: InductionHint _pcTraceQuantifier :: SystemTraceQuantifier

Instances

Eq ProofContext
Ord ProofContext
Show ProofContext

pcSignature :: forall arr. Arrow arr => Lens arr ProofContext SignatureWithMaude Source

pcRules :: forall arr. Arrow arr => Lens arr ProofContext ClassifiedRules Source

pcCaseDists :: forall arr. Arrow arr => Lens arr ProofContext [CaseDistinction]Source

pcUseInduction :: forall arr. Arrow arr => Lens arr ProofContext InductionHint Source

pcCaseDistKind :: forall arr. Arrow arr => Lens arr ProofContext CaseDistKind Source

pcTraceQuantifier :: forall arr. Arrow arr => Lens arr ProofContext SystemTraceQuantifier Source

pcInjectiveFactInsts :: forall arr. Arrow arr => Lens arr ProofContext (Set FactTag)Source

data InductionHint Source

Constructors

UseInduction
AvoidInduction

Instances

Eq InductionHint
Ord InductionHint
Show InductionHint
Binary InductionHint
NFData InductionHint

data ClassifiedRules Source

Constructors

ClassifiedRules
Fields _crProtocol :: [RuleAC] _crDestruct :: [RuleAC] _crConstruct :: [RuleAC]

Instances

Eq ClassifiedRules
Ord ClassifiedRules
Show ClassifiedRules
Binary ClassifiedRules
NFData ClassifiedRules

joinAllRules :: ClassifiedRules -> [RuleAC]Source

joinAllRules rules computes the union of all rules classified in rules.

crProtocol :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

crConstruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

crDestruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

Constraint reduction rules

Contradictions

All rules that reduce a constraint system to the empty set of constraint systems. The Contradiction datatype stores the information about the contradiction for later display to the user.

data Contradiction Source

Reasons why a constraint System can be contradictory.

Instances

Eq Contradiction
Ord Contradiction
Show Contradiction
Binary Contradiction
NFData Contradiction
HasFrees Contradiction

contradictions :: ProofContext -> System -> [Contradiction]Source

All CR-rules reducing a constraint system to *⟂* represented as a list of trivial contradictions. Note that some constraint systems are also removed because they have no unifier. This is part of unification. Note also that *S_{¬@}* is handled as part of *S_∀*.

Precomputed case distinctions

For better speed, we precompute case distinctions. This is especially important for getting rid of all chain constraints before actually starting to verify security properties.

data CaseDistinction Source

A big-step case distinction.

Instances

Eq CaseDistinction
Ord CaseDistinction
Show CaseDistinction
Binary CaseDistinction
NFData CaseDistinction
HasFrees CaseDistinction

cdGoal :: forall arr. Arrow arr => Lens arr CaseDistinction Goal Source

cdCases :: forall arr. Arrow arr => Lens arr CaseDistinction (Disj ([String], System))Source

precomputeCaseDistinctions Source

Arguments

:: ProofContext
-> [LNGuarded]	Axioms.
-> [CaseDistinction]

Precompute a saturated set of case distinctions.

refineWithTypingAsms Source

Arguments

:: [LNGuarded]	Typing assumptions to use.
-> ProofContext	Proof context to use.
-> [CaseDistinction]	Original, untyped case distinctions.
-> [CaseDistinction]	Refined, typed case distinctions.

Refine a set of case distinction by exploiting additional typing assumptions.

unsolvedChainConstraints :: CaseDistinction -> [Int]Source

The number of remaining chain constraints of each case.

Proof methods

Proof methods are the external to the constraint solver. They allow its small step execution. This module also provides the heuristics for selecting the best proof method to apply to a constraint system.

module Theory.Constraint.Solver.ProofMethod

Convenience export

module Logic.Connectives