module Theory.Tools.IntruderRules (
subtermIntruderRules
, dhIntruderRules
, bpIntruderRules
, multisetIntruderRules
, mkDUnionRule
, specialIntruderRules
, isDExpRule
, isDEMapRule
, isDPMultRule
) where
import Control.Basics
import Control.Monad.Reader
import Data.List
import qualified Data.Set as S
import Data.ByteString (ByteString)
import Extension.Data.Label
import Utils.Misc
import Term.Maude.Signature
import Term.Narrowing.Variants.Compute
import Term.Rewriting.Norm
import Term.SubtermRule
import Term.Positions
import Term.Subsumption
import Theory.Model
specialIntruderRules :: [IntrRuleAC]
specialIntruderRules =
[ kuRule CoerceRule [kdFact x_var] (x_var)
, kuRule PubConstrRule [] (x_pub_var)
, kuRule FreshConstrRule [Fact FreshFact [x_fresh_var]] (x_fresh_var)
, Rule ISendRule [kuFact x_var] [Fact InFact [x_var]] [kLogFact x_var]
, Rule IRecvRule [Fact OutFact [x_var]] [Fact KDFact [x_var]] []
]
where
kuRule name prems t = Rule name prems [kuFact t] [kuFact t]
x_var = varTerm (LVar "x" LSortMsg 0)
x_pub_var = varTerm (LVar "x" LSortPub 0)
x_fresh_var = varTerm (LVar "x" LSortFresh 0)
destructionRules :: StRule -> [IntrRuleAC]
destructionRules (StRule lhs@(viewTerm -> FApp (NoEq (f,_)) _) (RhsPosition pos)) =
go [] lhs pos
where
rhs = lhs `atPos` pos
go _ _ [] = []
go _ (viewTerm -> FApp _ _) (_:[]) = []
go uprems (viewTerm -> FApp _ as) (i:p) =
irule ++ go uprems' t' p
where
uprems' = uprems++[ t | (j, t) <- zip [0..] as, i /= j ]
t' = as!!i
irule = if (t' /= rhs && rhs `notElem` uprems')
then [ Rule (DestrRule f)
((kdFact t'):(map kuFact uprems'))
[kdFact rhs] [] ]
else []
go _ (viewTerm -> Lit _) (_:_) =
error "IntruderRules.destructionRules: impossible, position invalid"
destructionRules _ = []
minimizeIntruderRules :: [IntrRuleAC] -> [IntrRuleAC]
minimizeIntruderRules rules =
go [] rules
where
go checked [] = reverse checked
go checked (r@(Rule _ prems concs _):unchecked) = go checked' unchecked
where
checked' = if any (\(Rule _ prems' concs' _)
-> concs' == concs && prems' `subsetOf` prems)
(checked++unchecked)
then checked
else r:checked
subtermIntruderRules :: MaudeSig -> [IntrRuleAC]
subtermIntruderRules maudeSig =
minimizeIntruderRules $ concatMap destructionRules (S.toList $ stRules maudeSig)
++ constructionRules (stFunSyms maudeSig)
constructionRules :: NoEqFunSig -> [IntrRuleAC]
constructionRules fSig =
[ createRule s k | (s,(k,Public)) <- S.toList fSig ]
where
createRule s k = Rule (ConstrRule s) (map kuFact vars) [concfact] [concfact]
where vars = take k [ varTerm (LVar "x" LSortMsg i) | i <- [0..] ]
m = fAppNoEq (s,(k,Public)) vars
concfact = kuFact m
dhIntruderRules :: WithMaude [IntrRuleAC]
dhIntruderRules = reader $ \hnd -> minimizeIntruderRules $
[ expRule ConstrRule kuFact return
, invRule ConstrRule kuFact return
] ++
concatMap (variantsIntruder hnd id)
[ expRule DestrRule kdFact (const [])
, invRule DestrRule kdFact (const [])
]
where
x_var_0 = varTerm (LVar "x" LSortMsg 0)
x_var_1 = varTerm (LVar "x" LSortMsg 1)
expRule mkInfo kudFact mkAction =
Rule (mkInfo expSymString) [bfact, efact] [concfact] (mkAction concfact)
where
bfact = kudFact x_var_0
efact = kuFact x_var_1
conc = fAppExp (x_var_0, x_var_1)
concfact = kudFact conc
invRule mkInfo kudFact mkAction =
Rule (mkInfo invSymString) [bfact] [concfact] (mkAction concfact)
where
bfact = kudFact x_var_0
conc = fAppInv x_var_0
concfact = kudFact conc
variantsIntruder :: MaudeHandle -> ([LNSubstVFresh] -> [LNSubstVFresh]) -> IntrRuleAC -> [IntrRuleAC]
variantsIntruder hnd minimizeVariants ru = do
let ruleTerms = concatMap factTerms
(get rPrems ru++get rConcs ru++get rActs ru)
fsigma <- minimizeVariants $ computeVariants (fAppList ruleTerms) `runReader` hnd
let sigma = freshToFree fsigma `evalFreshAvoiding` ruleTerms
ruvariant = normRule' (apply sigma ru) `runReader` hnd
guard (frees (get rConcs ruvariant) /= [] &&
ruvariant /= ru &&
(get rConcs ruvariant) \\ (get rPrems ruvariant) /= []
)
case concatMap factTerms $ get rConcs ruvariant of
[viewTerm -> FApp (AC Mult) _] ->
fail "Rules with product conclusion are redundant"
_ -> return ruvariant
normRule' :: IntrRuleAC -> WithMaude IntrRuleAC
normRule' (Rule i ps cs as) = reader $ \hnd ->
let normFactTerms = map (fmap (\t -> norm' t `runReader` hnd)) in
Rule i (normFactTerms ps) (normFactTerms cs) (normFactTerms as)
multisetIntruderRules :: [IntrRuleAC]
multisetIntruderRules = [mkDUnionRule [x_var, y_var] x_var]
where x_var = varTerm (LVar "x" LSortMsg 0)
y_var = varTerm (LVar "y" LSortMsg 0)
mkDUnionRule :: [LNTerm] -> LNTerm -> IntrRuleAC
mkDUnionRule t_prems t_conc =
Rule (DestrRule unionSymString)
[kdFact $ fAppAC Union t_prems]
[kdFact t_conc] []
bpIntruderRules :: WithMaude [IntrRuleAC]
bpIntruderRules = reader $ \hnd -> minimizeIntruderRules $
[ pmultRule ConstrRule kuFact return
, emapRule ConstrRule kuFact return
]
++
(variantsIntruder hnd id $ pmultRule DestrRule kdFact (const []))
++
(bpVariantsIntruder hnd $ emapRule DestrRule kdFact (const []) )
where
x_var_0 = varTerm (LVar "x" LSortMsg 0)
x_var_1 = varTerm (LVar "x" LSortMsg 1)
pmultRule mkInfo kudFact mkAction =
Rule (mkInfo pmultSymString) [bfact, efact] [concfact] (mkAction concfact)
where
bfact = kudFact x_var_0
efact = kuFact x_var_1
conc = fAppPMult (x_var_1, x_var_0)
concfact = kudFact conc
emapRule mkInfo kudFact mkAction =
Rule (mkInfo emapSymString) [bfact, efact] [concfact] (mkAction concfact)
where
bfact = kudFact x_var_0
efact = kudFact x_var_1
conc = fAppEMap (x_var_0, x_var_1)
concfact = kudFact conc
bpVariantsIntruder :: MaudeHandle -> IntrRuleAC -> [IntrRuleAC]
bpVariantsIntruder hnd ru = do
ruvariant <- variantsIntruder hnd minimizeVariants ru
case ruvariant of
Rule i [Fact KDFact args@[viewTerm -> Lit (Var _)], yfact] concs actions ->
return $ Rule i [Fact KUFact args, yfact] concs actions
Rule i [yfact, Fact KDFact args@[viewTerm -> Lit (Var _)]] concs actions ->
return $ Rule i [yfact, Fact KUFact args] concs actions
_ -> return ruvariant
where
minimizeVariants = nub . map canonize
canonize subst = canonizeSubst . substFromListVFresh $ zip doms (sort rngs)
where
mappings = substToListVFresh subst
doms = map fst mappings
rngs = map snd mappings
isDRule :: ByteString -> Rule (RuleInfo t IntrRuleACInfo) -> Bool
isDRule ruString ru = case get rInfo ru of
IntrInfo (DestrRule n) | n == ruString -> True
_ -> False
isDExpRule, isDPMultRule, isDEMapRule
:: Rule (RuleInfo t IntrRuleACInfo) -> Bool
isDExpRule = isDRule expSymString
isDPMultRule = isDRule pmultSymString
isDEMapRule = isDRule emapSymString