Theory

Theory datatype and transformations on it.

Axioms

data Axiom

An axiom describes a property that must hold for all traces. Axioms are always used as lemmas in proofs.

Constructors

Axiom

Fields

_axName :: String

_axFormula :: LNFormula

Instances

Eq Axiom

Ord Axiom

Show Axiom

Binary Axiom

NFData Axiom

axName :: forall arr. Arrow arr => Lens arr Axiom String

axFormula :: forall arr. Arrow arr => Lens arr Axiom LNFormula

Lemmas

data LemmaAttribute

An attribute for a Lemma.

Constructors

TypingLemma

ReuseLemma

InvariantLemma

Instances

Eq LemmaAttribute

Ord LemmaAttribute

Show LemmaAttribute

Binary LemmaAttribute

NFData LemmaAttribute

data TraceQuantifier

A TraceQuantifier stating whether we check satisfiability of validity.

Constructors

ExistsTrace

AllTraces

Instances

Eq TraceQuantifier

Ord TraceQuantifier

Show TraceQuantifier

Binary TraceQuantifier

NFData TraceQuantifier

data Lemma p

A lemma describes a property that holds in the context of a theory together with a proof of its correctness.

Instances

Functor Lemma

Foldable Lemma

Traversable Lemma

Eq p => Eq (Lemma p)

Ord p => Ord (Lemma p)

Show p => Show (Lemma p)

Binary p_1628398076 => Binary (Lemma p_1628398076)

NFData p_1628398076 => NFData (Lemma p_1628398076)

lName :: forall arr p. Arrow arr => Lens arr (Lemma p) String

lTraceQuantifier :: forall arr p. Arrow arr => Lens arr (Lemma p) TraceQuantifier

lFormula :: forall arr p. Arrow arr => Lens arr (Lemma p) LNFormula

lAttributes :: forall arr p. Arrow arr => Lens arr (Lemma p) [LemmaAttribute]

lProof :: forall arr p. Arrow arr => Lens arr (Lemma p) p

unprovenLemma :: String -> [LemmaAttribute] -> TraceQuantifier -> LNFormula -> Lemma ProofSkeleton

Create a new unproven lemma from a formula modulo E.

skeletonLemma :: String -> [LemmaAttribute] -> TraceQuantifier -> LNFormula -> ProofSkeleton -> Lemma ProofSkeleton

Theories

data Theory sig c r p

A theory contains a single set of rewriting rules modeling a protocol and the lemmas that

Constructors

Theory

Fields

_thyName :: String

_thySignature :: sig

_thyCache :: c

_thyItems :: [TheoryItem r p]

Instances

(Eq sig, Eq c, Eq r, Eq p) => Eq (Theory sig c r p)

(Ord sig, Ord c, Ord r, Ord p) => Ord (Theory sig c r p)

(Show sig, Show c, Show r, Show p) => Show (Theory sig c r p)

(Binary sig_1628398556, Binary c_1628398557, Binary r_1628398558, Binary p_1628398559) => Binary (Theory sig_1628398556 c_1628398557 r_1628398558 p_1628398559)

(NFData sig_1628398556, NFData c_1628398557, NFData r_1628398558, NFData p_1628398559) => NFData (Theory sig_1628398556 c_1628398557 r_1628398558 p_1628398559)

data TheoryItem r p

A theory item built over the given rule type.

Constructors

RuleItem r

LemmaItem (Lemma p)

AxiomItem Axiom

TextItem FormalComment

Instances

Functor (TheoryItem r)

(Eq r, Eq p) => Eq (TheoryItem r p)

(Ord r, Ord p) => Ord (TheoryItem r p)

(Show r, Show p) => Show (TheoryItem r p)

(Binary r_1628398560, Binary p_1628398561) => Binary (TheoryItem r_1628398560 p_1628398561)

(NFData r_1628398560, NFData p_1628398561) => NFData (TheoryItem r_1628398560 p_1628398561)

thyName :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) String

thySignature :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) sig

thyCache :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) c

thyItems :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) [TheoryItem r p]

theoryRules :: Theory sig c r p -> [r]

All rules of a theory.

theoryLemmas :: Theory sig c r p -> [Lemma p]

All lemmas of a theory.

theoryAxioms :: Theory sig c r p -> [Axiom]

All axioms of a theory.

addAxiom :: Axiom -> Theory sig c r p -> Maybe (Theory sig c r p)

Add a new axiom. Fails, if axiom with the same name exists.

addLemma :: Lemma p -> Theory sig c r p -> Maybe (Theory sig c r p)

Add a new lemma. Fails, if a lemma with the same name exists.

removeLemma :: String -> Theory sig c r p -> Maybe (Theory sig c r p)

Remove a lemma by name. Fails, if the lemma does not exist.

lookupLemma :: String -> Theory sig c r p -> Maybe (Lemma p)

Find the lemma with the given name.

addComment :: Doc -> Theory sig c r p -> Theory sig c r p

Add a comment to the theory.

addStringComment :: String -> Theory sig c r p -> Theory sig c r p

Add a comment represented as a string to the theory.

addFormalComment :: FormalComment -> Theory sig c r p -> Theory sig c r p

cprRuleE :: forall arr. Arrow arr => Lens arr ClosedProtoRule ProtoRuleE

Open theories

type OpenTheory = Theory SignaturePure [IntrRuleAC] OpenProtoRule ProofSkeleton

Open theories can be extended. Invariants: 1. Lemma names are unique.

defaultOpenTheory :: OpenTheory

Default theory

addProtoRule :: ProtoRuleE -> OpenTheory -> Maybe OpenTheory

Add a new protocol rules. Fails, if a protocol rule with the same name exists.

applyPartialEvaluation :: EvaluationStyle -> ClosedTheory -> ClosedTheory

Apply partial evaluation.

addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheory

Add intruder proof rules.

normalizeTheory :: OpenTheory -> OpenTheory

Normalize the theory representation such that they remain semantically equivalent. Use this function when you want to compare two theories (quite strictly) for semantic equality; e.g., when testing the parser.

Closed theories

type ClosedTheory = Theory SignatureWithMaude ClosedRuleCache ClosedProtoRule IncrementalProof

Closed theories can be proven. Invariants: 1. Lemma names are unique 2. All proof steps with annotated sequents are sound with respect to the closed rule set of the theory. 3. Maude is running under the given handle.

data ClosedRuleCache

Constructors

ClosedRuleCache

Fields

_crcRules :: ClassifiedRules

_crcUntypedCaseDists :: [CaseDistinction]

_crcTypedCaseDists :: [CaseDistinction]

_crcInjectiveFactInsts :: Set FactTag

Instances

Eq ClosedRuleCache

Ord ClosedRuleCache

Show ClosedRuleCache

Binary ClosedRuleCache

NFData ClosedRuleCache

closeTheory

Arguments

:: FilePath

Path to the Maude executable.

-> OpenTheory

-> IO ClosedTheory

Close a theory by closing its associated rule set and checking the proof skeletons and caching AC variants as well as precomputed case distinctions.

This function initializes the relation to the Maude process with the correct signature. This is the right place to do that because in a closed theory the signature may not change any longer.

openTheory :: ClosedTheory -> OpenTheory

Open a theory by dropping the closed world assumption and values whose soundness dependens on it.

data ClosedProtoRule

A closed proto rule lists its original rule modulo E, the corresponding variant modulo AC, and if required the assertion soundness proof.

Constructors

ClosedProtoRule

Fields

_cprRuleE :: ProtoRuleE

_cprRuleAC :: ProtoRuleAC

Instances

Eq ClosedProtoRule

Ord ClosedProtoRule

Show ClosedProtoRule

Binary ClosedProtoRule

NFData ClosedProtoRule

HasRuleName ClosedProtoRule

getLemmas :: ClosedTheory -> [Lemma IncrementalProof]

All lemmas.

getIntrVariants :: ClosedTheory -> [IntrRuleAC]

The variants of the intruder rules.

getProtoRuleEs :: ClosedTheory -> [ProtoRuleE]

All protocol rules modulo E.

getProofContext :: Lemma a -> ClosedTheory -> ProofContext

Get the proof context for a lemma of the closed theory.

getClassifiedRules :: ClosedTheory -> ClassifiedRules

The classified set of rules modulo AC in this theory.

getInjectiveFactInsts :: ClosedTheory -> Set FactTag

The facts with injective instances in this theory

getCaseDistinction :: CaseDistKind -> ClosedTheory -> [CaseDistinction]

The precomputed case distinctions.

Proving

type ProofSkeleton = Proof ()

Proof skeletons are used to represent proofs in open theories.

proveTheory

Arguments

:: (Lemma IncrementalProof -> Bool)

Lemma selector.

-> Prover

-> ClosedTheory

-> ClosedTheory

Prove both the assertion soundness as well as all lemmas of the theory. If the prover fails on a lemma, then its proof remains unchanged.

Lemma references

lookupLemmaProof :: LemmaRef -> ClosedTheory -> Maybe IncrementalProof

Resolve a path in a theory.

modifyLemmaProof :: Prover -> LemmaRef -> ClosedTheory -> Maybe ClosedTheory

Modify the proof at the given lemma ref, if there is one. Fails if the path is not present or if the prover fails.

Pretty printing

prettyFormalComment :: HighlightDocument d => String -> String -> d

Pretty print a formal comment

prettyLemmaName :: HighlightDocument d => Lemma p -> d

Pretty print the lemma name together with its attributes.

prettyAxiom :: HighlightDocument d => Axiom -> d

Pretty print an axiom.

prettyLemma :: HighlightDocument d => (p -> d) -> Lemma p -> d

Pretty print a lemma.

prettyClosedTheory :: HighlightDocument d => ClosedTheory -> d

Pretty print a closed theory.

prettyOpenTheory :: HighlightDocument d => OpenTheory -> d

Pretty print an open theory.

prettyClosedSummary :: Document d => ClosedTheory -> d

prettyIntruderVariants :: HighlightDocument d => [IntrRuleAC] -> d

Pretty-print a non-empty bunch of intruder rules.

prettyTraceQuantifier :: Document d => TraceQuantifier -> d

Pretty print a TraceQuantifier.

Convenience exports

module Theory.Model

module Theory.Proof