scyther-proof-0.10.0.1: src/Scyther/Equalities.hs
{-# LANGUAGE DeriveDataTypeable #-}
module Scyther.Equalities (
-- * Single Equalities
TIDEq
, TIDRoleEq
, RoleEq
, ArbMsgEq
, AVarEq
, MVarEq
, MsgEq
, AnyEq(..)
, Inequality(..)
, arbmEqToMsgEq
, mvarEqToMsgEq
-- * Compound Equalities
, Equalities
-- ** Construction
, empty
, solve
, trimTIDEqs
, trimArbMsgEqs
-- ** Destruction
, getTIDEqs
, getTIDRoleEqs
, getArbMsgEqs
, getAVarEqs
, getMVarEqs
, getPostEqs
, toAnyEqs
, anyEqTIDs
, anyEqAMIDs
, inequalityTIDs
, inequalityAMIDs
-- ** Substitution
, substTID
, substLocalId
, substAVar
, substMVar
, substAMID
, substMsg
, substAnyEq
, substInequality
-- ** Additional Queries
, threadRole
, maxMappedTID
, maxMappedArbMsgId
, reflexive
, falseIneq
, null
-- * Mapping Logical Variables
, Mapping(..)
, emptyMapping
, mkMapping
, addTIDMapping
, addArbMsgIdMapping
, addTIDRoleMapping
, deleteTIDMapping
, deleteArbMsgIdMapping
-- * Pretty Printing
, sptAnyEq
, sptInequality
) where
import Prelude hiding (null)
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.UnionFind as U
import Data.Data
import Control.Arrow ( (***) )
import Control.Monad
import Text.Isar
import Scyther.Protocol
import Scyther.Message
------------------------------------------------------------------------------
-- Equalities
------------------------------------------------------------------------------
-- | Equalities over thread identifers.
--
-- Logically these are equalities between logical thread identifier variables.
type TIDEq = (TID, TID)
type TIDEqs = M.Map TID TID
-- | A thread to role assignment.
type TIDRoleEq = (TID, Role)
type TIDRoleEqs = M.Map TID Role
-- | The role equalities serve a double function:
type RoleEq = (Role, Role)
-- | An equality on an arbitrar-message id (a logical message variable).
type ArbMsgEq = (ArbMsgId, Message)
-- | Like role equalities, the agent equalities specify both quantification and
-- equalities.
type ArbMsgEqs = M.Map ArbMsgId Message
-- | 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 AVarEq = (AVar, AVar)
type AVarEqs = M.Map AVar AVar
-- | Equalities between message variables and arbitrary messages.
type MVarEq = (MVar, Message)
type MVarEqs = M.Map MVar Message
-- | Equalities between messages.
type MsgEq = (Message, Message)
type MsgEqs = U.UnionFind Message
-- | Some representable equality.
data AnyEq =
TIDEq !TIDEq
| TIDRoleEq !TIDRoleEq
| RoleEq !RoleEq
| ArbMsgEq !ArbMsgEq
| AVarEq !AVarEq
| MVarEq !MVarEq
| MsgEq !MsgEq
deriving( Eq, Ord, Show, Data, Typeable )
-- | An inequality. Bound logical variables are universally quantified.
newtype Inequality = Inequality { getInequality :: AnyEq }
deriving( Eq, Ord, Show, Data, Typeable )
-- | A conjunction of equality facts.
--
-- Invariants for a value @eqs = Equalities tideqs roleeqs avareqs mvareqs arbmeqs@:
--
-- 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(arbmeqs). substAMID eqs aid = MArbMsg aid
--
-- 2. Origin always greater than image for symmetric eqs.
--
-- forall (tid, tid') : tideqs. tid > tid'
-- forall (lid, lid') : avareqs. lid > lid'
--
-- 3. Range of message variable equalities normalized with respect to key inversion.
--
-- forall m : ran(mvareqs). normMsg m = m
--
-- 4. All thread identifiers are in the domain of roleeqs.
--
-- 5. All agent identifiers are in the domain of arbmeqs.
--
-- 6. No cycles.
--
data Equalities = Equalities {
tidEqs :: TIDEqs -- ^ Thread identifier equalities.
, roleEqs :: TIDRoleEqs -- ^ Thread to role assignments.
, avarEqs :: AVarEqs -- ^ Equalities between agent variables.
, mvarEqs :: MVarEqs -- ^ Equalities between message variables and arbitrary messages.
, arbmEqs :: ArbMsgEqs -- ^ Equalities between logical message variables and other messages.
, postEqs :: MsgEqs -- ^ Postponed equalities that stem from equalities involving
-- bi-directional keys and cannot be solved without
-- splitting in their most general form @KShr a b = KShr c d@. We
-- try to exploit these postponed equalities after
-- every regular unification.
}
deriving( Eq, Ord, Show, Data, Typeable {-! NFData !-} )
-- | Empty equality premises.
empty :: Equalities
empty = Equalities M.empty M.empty M.empty M.empty M.empty U.empty
-- | True if no equalities are present.
null :: Equalities -> Bool
null = (==) empty
-- Substitution
---------------
-- NOTE: Here we exploit that range of equalities does not contain any
-- identifier from the domain.
-- | Substitute a thread identifier according to thread identifier equalities.
substTID :: Equalities -> TID -> TID
substTID eqs tid = M.findWithDefault tid tid (tidEqs eqs)
-- | Substitute a local identifier according to thread identifier equalities.
substLocalId :: Equalities -> LocalId -> LocalId
substLocalId eqs (LocalId (i, tid)) = (LocalId (i, substTID eqs tid))
-- | Substitute a local identifier belonging to an agent variable.
substAVar :: Equalities -> AVar -> AVar
substAVar eqs av = M.findWithDefault av' av' (avarEqs eqs)
where av' = mapAVar (substLocalId eqs) av
-- | Substitute a local identifier belonging to a message variable.
substMVar :: Equalities -> MVar -> Message
substMVar eqs mv = M.findWithDefault (MMVar mv') mv' (mvarEqs eqs)
where mv' = mapMVar (substLocalId eqs) mv
-- | Substitute an agent id representing an arbitrary agent name.
substAMID :: Equalities -> ArbMsgId -> Message
substAMID eqs aid = M.findWithDefault (MArbMsg aid) aid (arbmEqs eqs)
-- | Substitute message constituents according to equalities.
--
-- POST: Message normalized w.r.t. 'normMsg'.
substMsg :: Equalities -> Message -> Message
substMsg eqs = normMsg . go
where
go m@(MConst _) = m
go (MFresh fr) = MFresh (mapFresh (substLocalId eqs) fr)
go (MAVar av) = MAVar (substAVar eqs av)
go (MMVar mv) = substMVar eqs mv
go (MArbMsg aid) = substAMID eqs aid
go (MHash m) = MHash (go m)
go (MTup m1 m2) = MTup (go m1) (go m2)
go (MEnc m1 m2) = MEnc (go m1) (go m2)
go (MSymK m1 m2) = MSymK (go m1) (go m2)
go (MShrK m1 m2) =
U.findWithDefault m' m' $ postEqs eqs
where
m' = MShrK (go m1) (go m2)
go (MAsymPK m) = MAsymPK (go m)
go (MAsymSK m) = MAsymSK (go m)
go (MInvKey m) = MInvKey (go m)
-- | Substitute a thread id equalitiy.
substTIDEq :: Equalities -> TIDEq -> TIDEq
substTIDEq eqs = substTID eqs *** substTID eqs
-- | Substitute a thread id to role equality.
substTIDRoleEq :: Equalities -> TIDRoleEq -> AnyEq
substTIDRoleEq eqs (tid, role) = case threadRole tid' eqs of
Just role' -> RoleEq (role, role')
Nothing -> TIDRoleEq (tid', role)
where
tid' = substTID eqs tid
-- | Substitute an agent equality.
substArbMsgEq :: Equalities -> ArbMsgEq -> MsgEq
substArbMsgEq eqs = substAMID eqs *** substMsg eqs
-- | Substitute an agent variable equality.
substAVarEq :: Equalities -> AVarEq -> AVarEq
substAVarEq eqs = substAVar eqs *** substAVar eqs
-- | Substitute a message variable equality.
substMVarEq :: Equalities -> MVarEq -> MsgEq
substMVarEq eqs = substMVar eqs *** substMsg eqs
-- | Substitute a message equality.
substMsgEq :: Equalities -> MsgEq -> MsgEq
substMsgEq eqs = substMsg eqs *** substMsg eqs
-- | Substitute both sides of a representable equality.
substAnyEq :: Equalities -> AnyEq -> AnyEq
substAnyEq eqs eq0 = case eq0 of
TIDEq eq -> TIDEq $ substTIDEq eqs eq
TIDRoleEq eq -> substTIDRoleEq eqs eq
RoleEq _ -> eq0
ArbMsgEq eq -> MsgEq $ substArbMsgEq eqs eq
AVarEq eq -> AVarEq $ substAVarEq eqs eq
MVarEq eq -> MsgEq $ substMVarEq eqs eq
MsgEq eq -> MsgEq $ substMsgEq eqs eq
-- | Substitute both sides of an inequality.
substInequality :: Equalities -> Inequality -> Inequality
substInequality eqs = Inequality . substAnyEq eqs . getInequality
-- Checking for reflexivity
---------------------------
-- | Convert an agent equality to a message equality.
arbmEqToMsgEq :: ArbMsgEq -> MsgEq
arbmEqToMsgEq (aid, rhs) = (MArbMsg aid, rhs)
-- | Convert a message variable equallity to a message equality.
mvarEqToMsgEq :: MVarEq -> MsgEq
mvarEqToMsgEq (v, m) = (MMVar v, m)
-- | Check if an equality is reflexive.
reflexive :: AnyEq -> Bool
reflexive eq0 = case eq0 of
TIDEq eq -> uncurry (==) eq
TIDRoleEq _ -> False
RoleEq eq -> uncurry (==) eq
ArbMsgEq eq -> reflexive . MsgEq $ arbmEqToMsgEq eq
AVarEq eq -> uncurry (==) eq
MVarEq eq -> reflexive . MsgEq $ mvarEqToMsgEq eq
MsgEq eq -> uncurry (==) eq
-- Deconstruction
-----------------
-- | The list of thread identifier equalities.
getTIDEqs :: Equalities -> [TIDEq]
getTIDEqs = M.toList . tidEqs
-- | The list of role equalities.
getTIDRoleEqs :: Equalities -> [TIDRoleEq]
getTIDRoleEqs = M.toList . roleEqs
-- | The list of agent variable equalities.
getArbMsgEqs :: Equalities -> [ArbMsgEq]
getArbMsgEqs = M.toList . arbmEqs
-- | The list of agent variable equalities.
getAVarEqs :: Equalities -> [AVarEq]
getAVarEqs = M.toList . avarEqs
-- | The list of message variable equalities.
getMVarEqs :: Equalities -> [MVarEq]
getMVarEqs = M.toList . mvarEqs
-- | The list of postponed message equalities.
getPostEqs :: Equalities -> [MsgEq]
getPostEqs = U.toList . postEqs
-- | Convert a set of equalities ot the tuple with lists for each individual
-- equality type.
toLists :: Equalities -> ([TIDEq], [TIDRoleEq], [ArbMsgEq], [AVarEq], [MVarEq], [MsgEq])
toLists eqs =
(getTIDEqs eqs, getTIDRoleEqs eqs, getArbMsgEqs eqs
, getAVarEqs eqs, getMVarEqs eqs, getPostEqs eqs)
-- | Convert a set of equalities to a list of equalities.
--
-- POST: Order of equalities equal to order in result of 'toLists'.
toAnyEqs :: Equalities -> [AnyEq]
toAnyEqs eqs =
map TIDEq a ++ map TIDRoleEq b ++ map ArbMsgEq c ++ map AVarEq d ++
map MVarEq e ++ map MsgEq f
where (a, b, c, d, e, f) = toLists eqs
-- | The threads occurring in an equality.
anyEqTIDs :: AnyEq -> [TID]
anyEqTIDs eq = case eq of
TIDEq (tid, _) -> return tid
TIDRoleEq (tid, _) -> return tid
RoleEq (_, _) -> mzero
ArbMsgEq (_, m) -> msgTIDs m
AVarEq (a1, a2) -> return (avarTID a1) `mplus` return (avarTID a2)
MVarEq (v, m) -> return (mvarTID v) `mplus` msgTIDs m
MsgEq (m1, m2) -> msgTIDs m1 `mplus` msgTIDs m2
-- | The logical message variables occuring in an equality.
anyEqAMIDs :: AnyEq -> [ArbMsgId]
anyEqAMIDs eq = case eq of
TIDEq _ -> mzero
TIDRoleEq _ -> mzero
RoleEq _ -> mzero
ArbMsgEq (a, m) -> a : msgAMIDs m
AVarEq _ -> mzero
MVarEq (_, m) -> msgAMIDs m
MsgEq (m1, m2) -> msgAMIDs m1 `mplus` msgAMIDs m2
-- | The threads occurring in an inequality.
inequalityTIDs :: Inequality -> [TID]
inequalityTIDs = anyEqTIDs . getInequality
-- | The logical message variables occuring in an inequality.
inequalityAMIDs :: Inequality -> [ArbMsgId]
inequalityAMIDs = anyEqAMIDs . getInequality
-- Unification
--------------
-- | Substitute and normalize the postponed equalities with respect to the
-- other equalities.
normPostEqs :: Equalities -> Equalities
normPostEqs eqs0 =
eqs { postEqs = U.map (substMsg eqs) (postEqs eqs0) }
where
eqs = eqs0 { postEqs = U.empty }
-- | 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.
solve :: Monad m => [AnyEq] -> Equalities -> m Equalities
solve ueqs eqs =
-- trace ("SOLVE: " ++ render (fsep $ punctuate comma $ map sptAnyEq ueqs)) $
fst `liftM` solveRepeated ueqs eqs False
-- | Repeatedly solve unification equations until the solution doesn't change
-- anymore. Postponed equations are tried to be solved again after each full
-- iteration.
--
-- A return value @(neweqs, improvedsolution)@ is to be interpreted such that
-- @improvedsolution@ denotes that something apart from the postponed
-- equalities has changed.
solveRepeated :: Monad m => [AnyEq] -> Equalities -> Bool -> m (Equalities, Bool)
solveRepeated [] eqs False = return (eqs, False)
solveRepeated [] eqs True =
solveRepeated (map MsgEq $ getPostEqs eqs) (eqs { postEqs = U.empty }) False
solveRepeated (ueq:ueqs) eqs improved = do
(ueqs', eqs', improved') <- solve1 ueq eqs
solveRepeated (ueqs ++ ueqs') (normPostEqs eqs') (improved || improved')
-- | Solve a single unification equation.
solve1 :: Monad m => AnyEq -> Equalities -> m ([AnyEq], Equalities, Bool)
solve1 ueq eqs@(Equalities tideqs roleeqs aveqs mveqs arbmeqs posteqs) =
-- trace ("solve1: " ++ show (sptAnyEq ueq)) $
case ueq of
TIDEq (tid1, tid2) ->
let tid1' = substTID eqs tid1
tid2' = substTID eqs tid2
elimTID x y = return
( mkAnyEqs TIDRoleEq roleeqs ++ mkAnyEqs ArbMsgEq arbmeqs ++
mkAnyEqs AVarEq aveqs ++ mkAnyEqs MVarEq mveqs ++
map MsgEq (U.toList posteqs)
, empty { tidEqs = M.insert x y tideqs }
, True
)
where
mkAnyEqs :: ((k, v) -> AnyEq) -> M.Map k v -> [AnyEq]
mkAnyEqs constr = map constr . M.toList
in
elimVarEqVar elimTID (tid1', tid1') (tid2', tid2')
TIDRoleEq (tid, role) ->
let tid' = substTID eqs tid
in
case M.lookup tid' roleeqs of
Just role' | role' /= role -> different "role" role role'
_ ->
updateSolution (eqs { roleEqs = M.insert tid' role roleeqs })
RoleEq (role1, role2)
| role1 == role2 -> skipEq
| otherwise -> different "role" role1 role2
AVarEq (av1, av2) ->
let av1' = substAVar eqs av1
av2' = substAVar eqs av2
elimAVar x y = updateSolution (eqs {
mvarEqs = M.map (substMsg elimEqs) mveqs
, arbmEqs = M.map (substMsg elimEqs) arbmeqs
, avarEqs = M.insert x y $ M.map (substAVar elimEqs) aveqs
})
where elimEqs = empty { avarEqs = M.singleton x y }
in
elimVarEqVar elimAVar (av1', av1') (av2', av2')
ArbMsgEq (lhs, rhs) ->
let elimArbMsgId x y
| x `elem` msgAMIDs y = case y of
MInvKey _ -> postpone (MArbMsg x) y
-- Here, we have to postpone the equality as 'x = inv(x)'
-- has a solution.
--
-- This is a hacky solution. The real solution is to
-- implement an occurs check strong enough to deal with the
-- 'inv(inv(x)) = x' cancellation rule.
--
-- FIXME: Implement proper equational unification, as done
-- in the tamarin-prover.
_ -> noUnifier $ "occurs check failed for '" ++ show x ++
"' in '" ++ show y ++ "'"
| otherwise =
updateSolution (eqs {
mvarEqs = M.map (substMsg elimEqs) mveqs
, arbmEqs = M.insert x y $ M.map (substMsg elimEqs) arbmeqs
})
where elimEqs = empty { arbmEqs = M.singleton x y }
in
case (substAMID eqs lhs, substMsg eqs rhs) of
(lhs'@(MArbMsg aid1), rhs'@(MArbMsg aid2)) ->
elimVarEqVar elimArbMsgId (aid1, lhs') (aid2, rhs')
(lhs' , (MArbMsg aid2)) -> elimArbMsgId aid2 lhs'
((MArbMsg aid1), rhs' ) -> elimArbMsgId aid1 rhs'
(lhs' , rhs' ) -> newEqs [MsgEq (lhs', rhs')]
MVarEq (lhs, rhs) ->
let elimMVar x y
| x `elem` msgFMV y = case y of
MInvKey _ -> postpone (MMVar x) y
-- Here, we have to postpone the equality as 'x = inv(x)'
-- has a solution.
--
-- This is a hacky solution. The real solution is to
-- implement an occurs check strong enough to deal with the
-- 'inv(inv(x)) = x' cancellation rule.
_ -> noUnifier $ "occurs check failed for '" ++ show x ++
"' in '" ++ show y ++ "'"
| otherwise =
updateSolution (eqs {
mvarEqs = M.insert x y $ M.map (substMsg elimEqs) mveqs
})
where elimEqs = empty { mvarEqs = M.singleton x y }
in
case (substMVar eqs lhs, substMsg eqs rhs) of
(lhs'@(MMVar mv1), rhs'@(MMVar mv2)) ->
elimVarEqVar elimMVar (mv1, lhs') (mv2, rhs')
(lhs' , (MMVar mv2)) -> elimMVar mv2 lhs'
( (MMVar mv1), rhs' ) -> elimMVar mv1 rhs'
(lhs' , rhs' ) -> newEqs [MsgEq (lhs', rhs')]
MsgEq eq -> case (substMsg eqs *** substMsg eqs) eq of
-- The order of pattern matches ensures that message variables are always
-- substituted by arbitrary-message ids.
(MMVar mv1, rhs) -> newEqs [MVarEq (mv1, rhs)]
(lhs, MMVar mv2) -> newEqs [MVarEq (mv2, lhs)]
(MArbMsg aid1, rhs) -> newEqs [ArbMsgEq (aid1, rhs)]
(lhs, MArbMsg aid2) -> newEqs [ArbMsgEq (aid2, lhs)]
(MInvKey x, MInvKey y ) -> newEqs [MsgEq (x, y)]
(MInvKey x, MAsymPK m1) -> newEqs [MsgEq (x, MAsymSK m1)]
(MAsymPK m1, MInvKey x ) -> newEqs [MsgEq (x, MAsymSK m1)]
(MInvKey x, MAsymSK m1) -> newEqs [MsgEq (x, MAsymPK m1)]
(MAsymSK m1, MInvKey x ) -> newEqs [MsgEq (x, MAsymPK m1)]
-- We postpone equalities between messages and inversions if both of
-- them may still be an asymmetric key. Otherwise, the inversion can be
-- eliminated as it is applied to a symmetric key.
(m1, m2@(MInvKey x)) | mayBeAsymKeys [m1, x] -> postpone m1 m2
| otherwise -> newEqs [MsgEq (x, m1)]
(m1@(MInvKey x), m2) | mayBeAsymKeys [x, m2] -> postpone m1 m2
| otherwise -> newEqs [MsgEq (x, m2)]
(MAVar av1, MAVar av2) -> newEqs [AVarEq (av1, av2)]
(MFresh (Fresh fr1), MFresh (Fresh fr2))
| lidId fr1 == lidId fr2 -> newEqs [TIDEq (lidTID fr1, lidTID fr2)]
| otherwise -> different "nonce" fr1 fr2
(MHash m1, MHash m2 ) -> newEqs [MsgEq (m1, m2)]
(MTup m11 m12, MTup m21 m22 ) -> newEqs [MsgEq (m11, m21), MsgEq (m12, m22)]
(MEnc m11 m12, MEnc m21 m22 ) -> newEqs [MsgEq (m11, m21), MsgEq (m12, m22)]
(MAsymPK m1, MAsymPK m2 ) -> newEqs [MsgEq (m1, m2)]
(MAsymSK m1, MAsymSK m2 ) -> newEqs [MsgEq (m1, m2)]
(MSymK m11 m12, MSymK m21 m22) -> newEqs [MsgEq (m11, m21), MsgEq (m12, m22)]
(m1@(MShrK m11 m12), m2@(MShrK m21 m22))
| m11 == m21 -> newEqs [MsgEq (m12, m22)]
| m11 == m22 -> newEqs [MsgEq (m12, m21)]
| m12 == m21 -> newEqs [MsgEq (m11, m22)]
| m12 == m22 -> newEqs [MsgEq (m11, m21)]
| m11 == m12 -> newEqs [MsgEq (m11, m21), MsgEq (m11, m22)]
| m21 == m22 -> newEqs [MsgEq (m11, m21), MsgEq (m12, m21)]
| (m1, m2) `U.equiv` posteqs -> skipEq
| otherwise -> postpone m1 m2
(MConst c1, MConst c2)
| c1 == c2 -> skipEq
| otherwise -> different "constant" c1 c2
(m1, m2) -> different "message" m1 m2
where
skipEq = return ([], eqs , False)
newEqs ueqs = return (ueqs, eqs , False)
updateSolution eqs' = return ([], eqs', True)
noUnifier = fail . ("solve1: " ++)
different ty x y = noUnifier $ ty ++ " '" ++ show x ++ "' /= '" ++ show y ++ "'"
postpone m1 m2 = return ([], eqs { postEqs = U.equate m1 m2 $ posteqs }, False)
elimVarEqVar elim (vl, lhs) (vr, rhs) =
case compare vl vr of
EQ -> skipEq
LT -> elim vr lhs
GT -> elim vl rhs
mayBeAsymKeys = any (not . mustBeSymKey)
-- | 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.
trimTIDEqs :: Equalities -> ([TID], Equalities) -- ^ Dropped TIDs plus updated equalities
trimTIDEqs eqs = (M.keys . tidEqs $ eqs, eqs { tidEqs = M.empty })
-- | 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.
trimArbMsgEqs :: Equalities -> ([ArbMsgId], Equalities) -- ^ Dropped ArbMsgIds plus updated equalities
trimArbMsgEqs eqs = (M.keys . arbmEqs $ eqs, eqs { arbmEqs = M.empty })
-- | The maximal mapped thread identifier.
maxMappedTID :: Equalities -> Maybe TID
maxMappedTID = fmap (fst . fst) . M.maxViewWithKey . tidEqs
-- | The maximal mapped agent identifier.
maxMappedArbMsgId :: Equalities -> Maybe ArbMsgId
maxMappedArbMsgId = fmap (fst . fst) . M.maxViewWithKey . arbmEqs
-- | Retrieve the role of a thread.
threadRole :: TID -> Equalities -> Maybe Role
threadRole tid eqs = M.lookup (substTID eqs tid) $ roleEqs eqs
-- | Test whether the equalities impose constraints on bound variables only.
onlyLocalConstraints :: Equalities -> Bool
onlyLocalConstraints eqs =
M.null (tidEqs eqs) &&
M.null (roleEqs eqs) &&
M.null (avarEqs eqs) &&
all isBoundVarMsg (map snd $ M.toList $ mvarEqs eqs) &&
all isBoundVarEq (M.toList $ arbmEqs eqs) &&
L.null (U.toList (postEqs eqs))
where
isBoundVar (BoundVarId _) = True
isBoundVar _ = False
isBoundVarMsg (MArbMsg v) = isBoundVar v
isBoundVarMsg _ = False
isBoundVarEq (lhs, rhs) = isBoundVar lhs || isBoundVarMsg rhs
-- | Check if an inequality is trivially false, i.e., there exists an
-- substitution of bound logical variables which makes it reflexive.
falseIneq :: Inequality -> Bool
falseIneq ineq = maybe False onlyLocalConstraints $ solve [getInequality ineq] empty
-------------------------------------------------------------------------------
-- Abusing equalities to represent mappings of logical variables
-------------------------------------------------------------------------------
newtype Mapping = Mapping { getMappingEqs :: Equalities }
deriving( Eq, Ord, Show, Data, Typeable )
-- | Map the equalities inside a mapping.
mapMapping :: (Equalities -> Equalities) -> Mapping -> Mapping
mapMapping f = Mapping . f . getMappingEqs
-- | An empty mapping.
emptyMapping :: Mapping
emptyMapping = Mapping empty
-- | 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.
mkMapping :: M.Map TID TID -> M.Map ArbMsgId ArbMsgId -> Mapping
mkMapping tideqs arbmeqs = Mapping $
empty {tidEqs = tideqs , arbmEqs = M.map MArbMsg arbmeqs}
-- | Add a mapping from one thread identifier to another one, possibly
-- overriding an existing mapping.
addTIDMapping :: TID -> TID -> Mapping -> Mapping
addTIDMapping from to = mapMapping $ \eqs ->
eqs { tidEqs = M.insert from to $ tidEqs eqs }
-- | Add a mapping from one arbitrary-message id to another arbitrary-message
-- id, possibly overriding an existing mapping.
addArbMsgIdMapping :: ArbMsgId -> ArbMsgId -> Mapping -> Mapping
addArbMsgIdMapping from to = mapMapping $ \eqs ->
eqs { arbmEqs = M.insert from (MArbMsg to) $ arbmEqs eqs }
-- | Add a mapping from one thread identifier to an other role, possibly
-- overriding an existing mapping.
addTIDRoleMapping :: TID -> Role -> Mapping -> Mapping
addTIDRoleMapping tid role = mapMapping $ \eqs ->
let tid' = substTID eqs tid
in eqs { roleEqs = M.insert tid' role $ roleEqs eqs }
-- | Delete the mapping of the given thread identifier.
deleteTIDMapping :: TID -> Mapping -> Mapping
deleteTIDMapping tid = mapMapping $ \eqs ->
eqs { tidEqs = M.delete tid $ tidEqs eqs }
-- | Delete the mapping of the given agent identifier.
deleteArbMsgIdMapping :: ArbMsgId -> Mapping -> Mapping
deleteArbMsgIdMapping aid = mapMapping $ \eqs ->
eqs { arbmEqs = M.delete aid $ arbmEqs eqs }
------------------------------------------------------------------------------
-- Pretty Printing
------------------------------------------------------------------------------
-- Helper functions for pretty printing
---------------------------------------
ppEq :: Doc -> (a -> Doc) -> (b -> Doc) -> (a, b) -> Doc
ppEq sym pp1 pp2 (x1, x2) = pp1 x1 <-> sym <-> pp2 x2
ppEq' :: Doc -> (a -> Doc) -> (a, a) -> Doc
ppEq' sym pp = ppEq sym pp pp
filterBoundVars :: [ArbMsgId] -> [ArbMsgId]
filterBoundVars = filter p
where
p (BoundVarId _) = True
p (FreeVarId _) = False
-- Isar
-------
ppIsarEq :: Doc -> IsarConf -> AnyEq -> Doc
ppIsarEq sym conf eq0 = case eq0 of
TIDEq eq -> ppEq' sym ppIsar eq
RoleEq eq -> ppEq' sym (text . roleName) eq
TIDRoleEq (tid, role) ->
text "roleMap r" <-> ppIsar tid <-> sym <-> text ("Some " ++ roleName role)
ArbMsgEq eq -> ppEq sym ppIsar ppIsar eq
AVarEq eq -> ppEq' sym ppIsar eq
MVarEq eq -> ppEq sym ppIsar ppIsar eq
MsgEq eq -> ppEq' sym ppIsar eq
where
ppIsar :: Isar a => a -> Doc
ppIsar = isar conf
instance Isar AnyEq where
isar = ppIsarEq (char '=')
instance Isar Inequality where
isar conf eq = if L.null boundVars
then ineq
else parens $ quantifiers <-> ineq
where
boundVars = map (isar conf) $ filterBoundVars $ inequalityAMIDs eq
ineq = ppIsarEq (isaNotEq conf) conf (getInequality eq)
quantifiers = foldl (<->) (isaForall conf) boundVars <> char '.'
-- SP Theory
------------
ppSPTEq :: Doc -> AnyEq -> Doc
ppSPTEq sym eq0 = case eq0 of
TIDEq eq -> ppEq' sym sptTID eq
RoleEq eq -> ppEq' sym (text . roleName) eq
TIDRoleEq (tid, role) ->
text "role(" <-> sptTID tid <-> char ')' <-> sym <-> text (roleName role)
ArbMsgEq eq -> ppEq sym sptArbMsgId sptMessage eq
AVarEq eq -> ppEq' sym sptAVar eq
MVarEq eq -> ppEq sym sptMVar sptMessage eq
MsgEq eq -> ppEq' sym sptMessage eq
sptAnyEq :: AnyEq -> Doc
sptAnyEq = ppSPTEq (char '=')
sptInequality :: Inequality -> Doc
sptInequality eq = if L.null boundVars
then ineq
else parens $ quantifiers <-> ineq
where
boundVars = map sptArbMsgId $ filterBoundVars $ inequalityAMIDs eq
ineq = ppSPTEq (text "!=") (getInequality eq)
quantifiers = foldl (<->) (char '!') boundVars <> char '.'
{-
-- | Convert the equalities for pretty printing.
sptEqualities :: Equalities ->
([Doc], [Doc], [Doc]) -- ^ quantified variables, representable
-- equalities, non-representable equalities
sptEqualities (Equalities tideqs roleeqs aveqs mveqs arbmeqs) =
( map sptTID (M.keys roleeqs) ++
[ sptArbMsgId aid | (aid, Nothing) <- M.toList arbmeqs]
, ppMapMaybe ppTIDRoleEq roleeqs ++
ppVarEqs ppAVar ppAVar aveqs ++
ppVarEqs ppMVar sptMessage mveqs ++
ppVarEqs ppAgent (maybe emptyDoc (either ppAgent ppAVar)) arbmeqs
, ppMap ppTIDEq tideqs ++
ppMapMaybe ppArbMsgEq arbmeqs
)
where
ppAVar = sptMessage . MAVar
ppMVar = sptMessage . MMVar
ppAgent = sptMessage . MArbMsg
ppMap ppElem = map ppElem . M.toList
ppMapMaybe ppElem m = map ppElem [(k,v) | (k, Just v) <- M.toList m]
ppTIDEq (tid1,tid2) = sptTID tid1 <-> text "->" <-> sptTID tid2
ppTIDRoleEq (tid, role) = text "role(" <> sptTID tid <> text ") =" <-> text (roleName role)
ppArbMsgEq (aid, rhs) = sptArbMsgId aid <-> text "->" <-> either sptArbMsgId sptLocalId rhs
ppVarEqs dom ran = ppMap ppVarEq . equalityChains
where
ppVarEq (r,ds) = fsep . intersperse (char '=') $ ran r : map dom (S.toList ds)
-- | Compute the equality classes given wrto a partial function.
equalityChains :: (Ord a, Ord b) => M.Map a b -> M.Map b (S.Set a)
equalityChains = foldl' insertEdge M.empty . M.toList
where
insertEdge m (from,to) = M.insertWith' S.union to (S.singleton from) m
-}