Scyther.Equalities

Single Equalities

type TIDEq = (TID, TID)

Equalities over thread identifers.

Logically these are equalities between logical thread identifier variables.

type TIDRoleEq = (TID, Role)

A thread to role assignment.

type RoleEq = (Role, Role)

The role equalities serve a double function:

type AgentEqRHS = Either AgentId AVar

type AgentEq = (AgentId, AgentEqRHS)

type AVarEq = (AVar, AVar)

Equalities between different agent variables.

We do not have to reason about equalities between an agent variable and some other message because our semantics guarantees that agent variables are only instantiated with agent names. Hence, they can only be equal to other agent variables or message variables. In the latter case, we store the equality the other way round; assigning the agent variable to the message variable.

type MVarEq = (MVar, Message)

Equalities between message variables and arbitrary messages.

type MsgEq = (Message, Message)

Equalities between messages.

data AnyEq

Some representable equality.

Constructors

TIDEq !TIDEq

TIDRoleEq !TIDRoleEq

RoleEq !RoleEq

AgentEq !AgentEq

AVarEq !AVarEq

MVarEq !MVarEq

MsgEq !MsgEq

Instances

Eq AnyEq

Data AnyEq

Ord AnyEq

Show AnyEq

Typeable AnyEq

Isar AnyEq

agentEqToMsgEq :: AgentEq -> MsgEq

Convert an agent equality to a message equality.

mvarEqToMsgEq :: MVarEq -> MsgEq

Convert a message variable equallity to a message equality.

Compound Equalities

data Equalities

A conjunction of equality facts.

Invariants for a value eqs = Equalities tideqs roleeqs avareqs mvareqs agnteqs:

1. Domain and range normalized with respect to equalities. Note that this implies substitution must always consider TID substitution first.

forall tid : ran(tideqs). substTID eqs tid = tid forall tid : dom(roleeqs). substTID eqs tid = tid forall (lid, lid') : avareqs. substLocalId eqs lid = lid & substAVar eqs lid' = lid' forall (lid, m) : mvareqs. substLocalId eqs lid = lid & substMsg eqs m = m

TODO: Complete properties for Agent ID's

forall aid : dom(agnteqs). substAgentId eqs aid = Just (Left aid) forall : dom(agnteqs). substAgentId eqs aid = Just (Left aid)

1. Origin always greater than image for symmetric eqs.

forall (tid, tid') : tideqs. tid > tid' forall (lid, lid') : avareqs. lid > lid'

1. Range of message variable equalities normalized with respect to key inversion.

forall m : ran(mvareqs). normMsg m = m

1. All thread identifiers are in the domain of roleeqs.
2. All agent identifiers are in the domain of agnteqs.
3. No cycles.

Instances

Eq Equalities

Data Equalities

Ord Equalities

Show Equalities

Typeable Equalities

Construction

empty :: Equalities

Empty equality premises.

solve :: Monad m => [AnyEq] -> Equalities -> m Equalities

Solve a list of unification equations.

The unification is performed modulo key inversion and thread identifier equalities. Additional thread identifier equalities may result from equalities over fresh messages. Bidirectional keys are handled by delaying their solution until only one solution is possible.

trimTIDEqs

Arguments

:: Equalities

-> ([TID], Equalities)

Dropped TIDs plus updated equalities

Remove the thread identifier equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped thread identifiers.

trimAgentEqs

Arguments

:: Equalities

-> ([AgentId], Equalities)

Dropped AgentIds plus updated equalities

Remove the agent identifiers equalities. This is logically safe iff there is no fact outside the equalities that still refers to the dropped agent identifiers.

Destruction

getTIDEqs :: Equalities -> [TIDEq]

The list of thread identifier equalities.

getTIDRoleEqs :: Equalities -> [TIDRoleEq]

The list of role equalities.

getAgentEqs :: Equalities -> [AgentEq]

The list of agent variable equalities.

getAVarEqs :: Equalities -> [AVarEq]

The list of agent variable equalities.

getMVarEqs :: Equalities -> [MVarEq]

The list of message variable equalities.

getPostEqs :: Equalities -> [MsgEq]

The list of postponed message equalities.

toAnyEqs :: Equalities -> [AnyEq]

Convert a set of equalities to a list of equalities.

POST: Order of equalities equal to order in result of toLists.

anyEqTIDs :: AnyEq -> [TID]

The threads occurring in an equality.

Substitution

substTID :: Equalities -> TID -> TID

Substitute a thread identifier according to thread identifier equalities.

substLocalId :: Equalities -> LocalId -> LocalId

Substitute a local identifier according to thread identifier equalities.

substAVar :: Equalities -> AVar -> AVar

Substitute a local identifier belonging to an agent variable.

substMVar :: Equalities -> MVar -> Message

Substitute a local identifier belonging to a message variable.

substAgentId :: Equalities -> AgentId -> AgentEqRHS

Substitute an agent id representing an arbitrary agent name.

substAgentEqRHS :: Equalities -> AgentEqRHS -> AgentEqRHS

Substitute the right-hand-side of an agent id equality.

substMsg :: Equalities -> Message -> Message

Substitute message constituents according to equalities.

POST: Message normalized w.r.t. normMsg.

substAnyEq :: Equalities -> AnyEq -> AnyEq

Substitute both sides of a representable equality.

Additional Queries

threadRole :: TID -> Equalities -> Maybe Role

Retrieve the role of a thread.

maxMappedTID :: Equalities -> Maybe TID

The maximal mapped thread identifier.

maxMappedAgentId :: Equalities -> Maybe AgentId

The maximal mapped agent identifier.

reflexive :: AnyEq -> Bool

Check if an equality is reflexive.

null :: Equalities -> Bool

True if no equalities are present.

Mapping Logical Variables

newtype Mapping

Constructors

Mapping

Fields

getMappingEqs :: Equalities

Instances

Eq Mapping

Data Mapping

Ord Mapping

Show Mapping

Typeable Mapping

emptyMapping :: Mapping

An empty mapping.

mkMapping :: Map TID TID -> Map AgentId AgentId -> Mapping

A mapping of logical variables and the corresponding substitution can be represented as an abstract Equalities value. However, it violates the invariant that the domain of the equalities must be invariant under substitution. This is OK, as domain and range of a mapping are from different logical contexts.

addTIDMapping :: TID -> TID -> Mapping -> Mapping

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

addAgentIdMapping :: AgentId -> AgentId -> Mapping -> Mapping

Add a mapping from one thread identifier to another one, possibly overriding an existing mapping.

addTIDRoleMapping :: TID -> Role -> Mapping -> Mapping

Add a mapping from one thread identifier to an other role, possibly overriding an existing mapping.

deleteTIDMapping :: TID -> Mapping -> Mapping

Delete the mapping of the given thread identifier.

deleteAgentIdMapping :: AgentId -> Mapping -> Mapping

Delete the mapping of the given agent identifier.

Pretty Printing

sptAnyEq :: AnyEq -> Doc