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

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone




Types to represent proofs.



data LTree l a Source

Trees with uniquely labelled edges.




root :: a
children :: Map l (LTree l a)


Functor (LTree l) 
Foldable (LTree l) 
Traversable (LTree l) 
(Eq l, Eq a) => Eq (LTree l a) 
(Ord l, Ord a) => Ord (LTree l a) 
(Show l, Show a) => Show (LTree l a) 
(Ord l, Binary l, Binary a) => Binary (LTree l a) 
(Ord l, NFData l, NFData a) => NFData (LTree l a) 

mergeMapsWith :: Ord k => (a -> c) -> (b -> c) -> (a -> b -> c) -> Map k a -> Map k b -> Map k cSource

O(n+m). A generalized union operator for maps with differing types.


data ProofStep a Source

A proof steps is a proof method together with additional context-dependent information.




psMethod :: ProofMethod
psInfo :: a


Functor ProofStep 
Foldable ProofStep 
Traversable ProofStep 
Eq a => Eq (ProofStep a) 
Ord a => Ord (ProofStep a) 
Show a => Show (ProofStep a) 
Binary a_1628259371 => Binary (ProofStep a_1628259371) 
NFData a_1628259371 => NFData (ProofStep a_1628259371) 
HasFrees a => HasFrees (ProofStep a) 

type Proof a = LTree CaseName (ProofStep a)Source

A proof is a tree of proof steps whose edges are labelled with case names.

Paths inside proofs

type ProofPath = [CaseName]Source

A path to a subproof.

atPath :: Proof a -> ProofPath -> Maybe (Proof a)Source

prf atPath path returns the subproof at the path in prf.

insertPaths :: Proof a -> Proof (a, ProofPath)Source

insertPaths prf inserts the path to every proof node.

Folding/modifying proofs

mapProofInfo :: (a -> b) -> Proof a -> Proof bSource

Apply a function to the information of every proof step.

foldProof :: Monoid m => (ProofStep a -> m) -> Proof a -> mSource

Fold a proof.

annotateProof :: (ProofStep a -> [b] -> b) -> Proof a -> Proof bSource

Annotate a proof in a bottom-up fashion.

data ProofStatus Source

The status of a Proof.



All steps are unannotated


The proof is complete: no annotated sorry, no annotated solved step


There is a annotated sorry, but no annotatd solved step.


There is an annotated solved step

Unfinished proofs

sorry :: Maybe String -> a -> Proof aSource

A proof using the sorry proof method.

unproven :: a -> Proof aSource

A proof denoting an unproven part of the proof.

Incremental proof construction

type IncrementalProof = Proof (Maybe System)Source

Incremental proofs are used to represent intermediate results of proof checking/construction.

data Prover Source

Provers whose sequencing is handled via the Monoid instance.

 p1 `mappend` p2

Is a prover that first runs p1 and then p2 on the resulting proof.


mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> ProverSource

Map the proof generated by the prover.

orelse :: Prover -> Prover -> ProverSource

Resorts to the second prover, if the first one is not successful.

tryProver :: Prover -> ProverSource

Try to apply a prover. If it fails, just return the original proof.

sorryProver :: Maybe String -> ProverSource

Replace the current proof with a sorry step and the given reason.

oneStepProver :: ProofMethod -> ProverSource

Try to execute one proof step using the given proof method.

focus :: ProofPath -> Prover -> ProverSource

Apply a prover only to a sub-proof, fails if the subproof doesn't exist.

checkAndExtendProver :: Prover -> ProverSource

Check the proof and handle new cases using the given prover.

replaceSorryProver :: Prover -> ProverSource

Replace all annotated sorry steps using the given prover.

contradictionProver :: ProverSource

Prover that does one contradiction step.

Explicit representation of a fully automatic prover

Pretty Printing



:: HighlightDocument d 
=> (ProofStep a -> d)

Make proof step pretty

-> (ProofStep a -> d -> d)

Make whole case pretty

-> Proof a

The proof to prettify

-> d 

showProofStatus :: SystemTraceQuantifier -> ProofStatus -> StringSource

Convert a proof status to a redable string.

Parallel Strategy for exploring a proof

parLTreeDFS :: Strategy (LTree l a)Source

A parallel evaluation strategy well-suited for DFS traversal: As soon as a node is forced it sparks off the computation of the number of case-maps of all its children. This way most of the data is already evaulated, when the actual DFS traversal visits it.

NOT used for now. It sometimes required too much memory.

Small-step interface to the constraint solver