diff --git a/.ghci b/.ghci --- a/.ghci +++ b/.ghci @@ -2,4 +2,4 @@ -- :set -ilib/term/src -- :set -ilib/utils/src :set -isrc -:set -Wall +:set -Wall -fwarn-tabs diff --git a/data/CHANGES b/data/CHANGES --- a/data/CHANGES +++ b/data/CHANGES @@ -1,3 +1,21 @@ +* 0.8.1.0 + - enabled parallelization by default when compiling `tamarin-prover` with + GHC 7.4 and higher. It uses as many threads as there are CPU cores on + the system. Use `tamarin-prover +RTS -N1 -RTS` to use only one thread. + + - fixed: lemmas proven for some trace ('exists-trace') and marked with + the [reuse] attribute were wrongly used in the proof of other lemmas. + - fixed: axioms that are not safety formulas were not transformed + properly when applying induction. + - fixed: fresh name generation was not always handled properly when + applying a precomputed case distinction to a goal that uses + DH-exponentiation. Security protocol models that use DH-exponentiation + should be checked again. Some of our case studies were indeed missing + a few cases, but no property changed its validity. + - fixed: no more case names containing spaces, + when solving deconstruction chains. + - fixed: avoid solving KU-goals for nullary function symbols + * 0.8.0.0 - new homepage: http://www.infsec.ethz.ch/research/software/tamarin - mailing list: https://groups.google.com/group/tamarin-prover diff --git a/data/examples/loops/TESLA_Scheme1.spthy b/data/examples/loops/TESLA_Scheme1.spthy --- a/data/examples/loops/TESLA_Scheme1.spthy +++ b/data/examples/loops/TESLA_Scheme1.spthy @@ -60,17 +60,18 @@ // Setup phase ////////////// -// We choose a fresh start key and provide facts for sending and answering -// receiver connection requests. +// A sender knows is own identity $S. He chooses a fresh key to start sending +// a new authenticated stream. We provide facts for sending the stream and for +// answering receiver connection requests. rule Sender_Setup: [ Fr(~k1) ] --> - [ Sender1(~k1), !Sender0a(~k1) ] + [ Sender1($S, ~k1), !Sender0a($S, ~k1) ] // Everybody can listen in by sending a request for the commitment to the // first key. rule Sender0a: - [ !Sender0a(k1) + [ !Sender0a(S, k1) , In( < R, S, nR> ) , !Ltk(S, ltkS) ] @@ -78,73 +79,64 @@ [ Out( ) ] // Receivers start by requesting the commitment to the first key and verifying -// the signature on this commitment. +// the signature on this commitment. We use the receiver nonce to identify +// receivers. rule Receiver0a: - [ Fr( ~nR ) ] + [ Fr( ~rid ) ] --> - [ Out( < $R, $S, ~nR > ) - , Receiver0b( $R, $S, ~nR ) ] + [ Out( < $R, $S, ~rid > ) + , Receiver0b( ~rid, $R, $S ) ] rule Receiver0b: - [ Receiver0b ( R, S, nR ) + [ Receiver0b ( rid, R, S ) , !Pk( S, pkS) - , In( ) + , In( ) ] --> - [ Receiver0b_check(S, k2, verify(signature, , pkS)) ] + [ Receiver0b_check( rid, S, commit_k1 + , verify(signature, , pkS)) ] rule Receiver0b_check: - [ Receiver0b_check(S, k2, true) ] + [ Receiver0b_check(rid, S, commit_k1, true) ] --> - [ Receiver1( S, k2 ) ] + [ Receiver1( rid, S, commit_k1 ) ] -/* The following setup-phase allows for a simpler proof. - -rule Setup: - [ Fr(~k1) ] - --> - [ Sender1(~k1) - , Receiver1(f(~k1)) - ] - -*/ - // Authenticated broadcasting rule Send1: let data1 = <'1', ~m1, f(~k2)> in - [ Sender1(~k1) + [ Sender1(S, ~k1) , Fr(~m1) , Fr(~k2) ] - --[ Sent(data1) + --[ Sent(S, data1) ]-> - [ Sender(~k1, ~k2) + [ Sender(S, ~k1, ~k2) , Out( < data1, MAC{data1}~k1 > ) ] rule Recv1: let data1 = <'1', m1, commit_k2> in - [ Receiver1(S, commit_k1) + [ Receiver1(rid, S, commit_k1) , In( ) ] - --[ AssumeCommitNotExpired(commit_k1) + --[ AssumeCommitNotExpired(rid, commit_k1) ]-> - [ Receiver(S, data1, mac1, commit_k1, commit_k2) ] + [ Receiver(rid, S, data1, mac1, commit_k1, commit_k2) ] rule SendN: let data = <'N', ~m, f(~kNew), ~kOld> in - [ Sender(~kOld, ~k) + [ Sender(S, ~kOld, ~k) , Fr(~m) , Fr(~kNew) ] - --[ Sent(data) + --[ Sent(S, data) , CommitExpired(f(~kOld)) ]-> - [ Sender(~k, ~kNew) + [ Sender(S, ~k, ~kNew) , Out( ) ] @@ -152,31 +144,32 @@ let data = <'N', m, commit_kNew, kOld> in [ In(< data, mac >) - , Receiver(S, dataOld, MAC{dataOld}kOld, f(kOld), commit_k) + , Receiver(rid, S, dataOld, MAC{dataOld}kOld, f(kOld), commit_k) ] - --[ FromSender(S, dataOld) - , AssumeCommitNotExpired(commit_k) + --[ FromSender(rid, S, dataOld) + , AssumeCommitNotExpired(rid, commit_k) ]-> - [ Receiver(S, data, mac, commit_k, commit_kNew) ] + [ Receiver(rid, S, data, mac, commit_k, commit_kNew) ] -// The desired security property: if all commits expired after all asumptions -// that they are not expired, then we have message authentication provided the -// long-term key of the server was not revealed. -// -// Note that we could strengthen this property such that only expiredness of -// commits in this broadcasting session before the 'FromSender'-claim is -// required. +/* +The desired security property: if all expiredness assumptions of the test +thread are given and the server that is sending was not compromised before, +then received data was sent by the server. +*/ lemma authentic [use_induction]: - "(All commit #i #j . - AssumeCommitNotExpired(commit) @ i - & CommitExpired(commit) @ j - ==> i < j - ) - ==> - (All S m #i. FromSender(S, m) @ i ==> - ( (Ex #j. Sent(m) @ j & j < i) + /* For every reciever claiming that it received data 'm' from the server, */ + "(All rid S m #i. FromSender(rid, S, m) @ i ==> + /* the server actually sent that data */ + ( (Ex #j. Sent(S, m) @ j & j < i) + /* or the server's longterm key was compromised before the claim */ | (Ex #j. RevealLtk(S) @ j & j < i) + /* or one of the receivers expiredness assumptions before the claim + was not met. */ + | (Ex commit #ne #e. AssumeCommitNotExpired(rid, commit) @ ne + & CommitExpired(commit) @ e + & e < ne + & ne < i) ) ) " @@ -184,14 +177,12 @@ // Ensure that the above lemma is not vacuous due to the filtering condition. lemma authentic_reachable [use_induction]: exists-trace - "(All commit #i #j . - AssumeCommitNotExpired(commit) @ i + "(All rid commit #i #j . + AssumeCommitNotExpired(rid, commit) @ i & CommitExpired(commit) @ j ==> i < j - ) - & - (Ex S m #i. FromSender(S, m) @ i) - " + ) & + (Ex rid S m #i. FromSender(rid, S, m) @ i) " end diff --git a/data/examples/loops/Typing_and_Destructors.spthy b/data/examples/loops/Typing_and_Destructors.spthy new file mode 100644 --- /dev/null +++ b/data/examples/loops/Typing_and_Destructors.spthy @@ -0,0 +1,122 @@ +theory Typing_and_Destructors +begin + +/* + Protocol: Demonstration of the interaction between typing and + destructors + Modeler: Simon Meier + Date: July 2012 + + Status: working / misses theory extension (see issue #104) + + This protocol is a variant of 'Minimal_Typing_Example' that uses explicit + destructors. Its verification does not yet work out of the box, as the + implemented definition of guarded trace properties is too restrictive to + allow formalizing the required type invariant. + + NOTE that it seems that the best option is to explicitly state in a rule + that it does not continue in case the application of a deconstructor was + not successful using an axiom like 'No_failure_terms'. This considerably + simplifies the verification. +*/ + + +builtins: symmetric-encryption, hashing + +// Shared keys that can be compromised. +rule Setup_Key: + [ Fr(~k) ] --[ IsKey(~k) ]-> [ !Key(~k) ] + +rule Reveal_Key: + [ !Key(k) ] --[ Rev(k) ]-> [ Out(k) ] + +rule Initiator: + let msg = senc{~sec,~pub}k + in + [ !Key(k), Fr(~sec), Fr(~pub) ] + --[ Out_Initiator(msg) + , Public(~pub) + ]-> + [ Out( msg ) ] + +rule Responder: + // We use explicit destructors instead of the pattern matching + // + // msg = senc{sec,pub}key + // + // This explicit use of destructors is more permissive (i.e., allows more + // traces), as it allows the rule to fire even if an failure term is sent. + // + let body = sdec{msg}key + sec = fst(body) + pub = snd(body) + in + [ !Key(key), In( msg ) + ] + --[ In_Responder(msg, pub) + , Secret(sec, key) + // We can simulate pattern matching by logging that the 'pub' term must + // not be an failure term. + , NoFailureTerm(pub) + ]-> + [ Out( pub ) ] + +// Commented out to test the type assertion. +// +// // This axiom then filters all traces with disallowed failure terms. +// // Note that we interpret its formula modulo AC. +// axiom No_failure_terms: +// "(All x #i. NoFailureTerm(snd(x)) @ i ==> F)" +// // Here we should also exclude all other possible shapes of failure terms. + +// This type assertion does not hold, as 'pub' could be an failure term. See the +// case marked below for the missing piece of the puzzle. +// Note that we interpret its formula modulo AC. +lemma type_assertion [typing]: + /* For all messages received by the responder */ + "(All m pub #i. In_Responder(m, pub) @ i ==> + /* they either came from the adversary and he therefore knows the + * contained 'k' variable before it was instantiated */ + ( (Ex #j. KU(pub) @ j & j < i) + /* or there is an initiator that sent 'm'. */ + | (Ex #j. Out_Initiator(m) @ j) + // These two cases cover the failure cases and make the type assertion + // valid. They are also sufficient to prove the statements below. + // They are currently not wellformed because 'snd' and 'sdec' are not + // allowed in formulas. + | (Ex body #j. KU(body) @ j + & pub = snd(body) & j < i) + | (Ex body key #j #k. IsKey(key)@k & KU(body) @ j + & pub = snd(sdec{body}key) & j < i) + // Note that I thinkg that these two cases might be sufficient. They + // would however require that equalities can also be guarding. + // | (Ex body. pub = snd(body)) + // | (Ex body key. pub = snd(sdec{body}key)) + ) + ) + " + +/* The secret part of the message received by Responder is secret provided the + * key has not been compromised. + */ +lemma Responder_secrecy: + " All sec key #i #j. + Secret(sec, key) @ #i + & K(sec) @ #j + ==> + (Ex #r. Rev(key) @ r) + " + +/* Sanity check: the public part is accessible to the adversary without + * performing a key reveal. + */ +lemma Public_part_public: + exists-trace + " /* No key reveal has been performed */ + not (Ex k #i. Rev(k) @ i) + /* and the public part of a message is known to the adversary. */ + & (Ex pub #i #j. Public(pub) @ i & K(pub) @ j ) + " + + +end diff --git a/data/js/tamarin-prover-ui.js b/data/js/tamarin-prover-ui.js --- a/data/js/tamarin-prover-ui.js +++ b/data/js/tamarin-prover-ui.js @@ -186,15 +186,15 @@ }); // Enable context menu - $("#proof a.proof-step").contextMenu( - { menu: "contextMenu" }, - function(action, el, pos) { - var theoryPath = theory.extractTheoryPath($(el).attr("href")); - mainDisplay.loadTarget( - theory.absolutePath(action,theoryPath), - null - ); - }); + // $("#proof a.proof-step").contextMenu( + // { menu: "contextMenu" }, + // function(action, el, pos) { + // var theoryPath = theory.extractTheoryPath($(el).attr("href")); + // mainDisplay.loadTarget( + // theory.absolutePath(action,theoryPath), + // null + // ); + // }); // Click handler for save link events.installAbsoluteClickHandler("a.save-link", server.handleJson); @@ -249,26 +249,27 @@ // Install handlers on plain internal links events.installRelativeClickHandler( "div#proof a.internal-link", - "main", + null, null); + // FIXME: delete is disabled // Install handlers on delete links - events.installRelativeClickHandler( - "div#proof a.internal-link.delete-link", - "del/path", - null); + // events.installRelativeClickHandler( + // "div#proof a.internal-link.delete-link", + // "del/path", + // null); // Install handlers on proof-step links events.installRelativeClickHandler( "div#proof a.internal-link.proof-step", - "main", + null, null ); // Install click handlers on main events.installRelativeClickHandler( "div#ui-main-display a.internal-link", - "main", + null, null); // Install handlers on removal links @@ -335,7 +336,7 @@ // callback function and pass keycode if(map[key]) { // Hide context menu - $("ul#contextMenu").hide(); + // $("ul#contextMenu").hide(); // Call callback var callback = map[key]; callback(key); @@ -379,7 +380,7 @@ installScrollHandler: function(name, selector) { $(selector).scroll(function(ev) { // Hide context menu - $("ul#contextMenu").hide(); + // $("ul#contextMenu").hide(); // Record position in cookie var pos = $(this).scrollTop(); $.cookie(name + "-position", pos, { path: "/" }); @@ -419,10 +420,19 @@ // Add new click handler $(selector).click(function(ev) { ev.preventDefault(); - var element = $(this); + + // FIXME: always set the right link on the Haskell side + // and get rid of section + path = $(this).attr("href"); + if(section) { + // replace section in path + elementPath = $(this).attr("href").split("/"); + elementPath[3] = section; + path = elementPath.join("/"); + } + mainDisplay.loadTarget( - // section, - element.attr("href"), + path, function() { if(callback) callback(element); }); @@ -665,7 +675,7 @@ // Re-install click handlers on main events.installRelativeClickHandler( "div#ui-main-display a.internal-link", - "main", + null, null); }, diff --git a/interactive-only-src/Paths_tamarin_prover.hs b/interactive-only-src/Paths_tamarin_prover.hs --- a/interactive-only-src/Paths_tamarin_prover.hs +++ b/interactive-only-src/Paths_tamarin_prover.hs @@ -12,7 +12,7 @@ version :: Version -version = Version {versionBranch = [0,8,0,0], versionTags = []} +version = Version {versionBranch = [0,8,1,0], versionTags = []} bindir, libdir, datadir, libexecdir :: FilePath bindir = "./" diff --git a/src/Main/Mode/Batch.hs b/src/Main/Mode/Batch.hs --- a/src/Main/Mode/Batch.hs +++ b/src/Main/Mode/Batch.hs @@ -12,6 +12,8 @@ ) where import Control.Basics +import Control.DeepSeq (force) +import Control.Exception (evaluate) import Data.List import Data.Maybe import System.Console.CmdArgs.Explicit as CmdArgs @@ -142,7 +144,8 @@ (thySummary, t) <- timed $ do thy <- load writeFileWithDirs outFile $ renderDoc $ fullDoc thy - return $ summaryDoc thy + -- ensure that the summary is in normal form + evaluate $ force $ summaryDoc thy let summary = Pretty.vcat [ ppAnalyzed , Pretty.text $ "" diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs --- a/src/Main/TheoryLoader.hs +++ b/src/Main/TheoryLoader.hs @@ -105,30 +105,37 @@ where (loadOpen, close) = loadThy as -loadClosedThyString :: Arguments -> String -> IO ClosedTheory -loadClosedThyString = uncurry (>=>) . loadThyString +loadClosedThyString :: Arguments -> String -> IO (Either String ClosedTheory) +loadClosedThyString as file = do + let (loader, closer) = loadThyString as + openThy <- loader file + case openThy of + Right thy -> Right <$> closer thy + Left err -> return $ Left err -- | Load an open/closed theory from a file. loadThy :: Arguments -> (FilePath -> IO OpenTheory, OpenTheory -> IO ClosedTheory) loadThy as = loadGenericThy (parseOpenTheory (defines as)) as -- | Load an open/closed theory from a string. -loadThyString :: Arguments -> (String -> IO OpenTheory, OpenTheory -> IO ClosedTheory) +loadThyString :: Arguments -> ( String -> IO (Either String OpenTheory) + , OpenTheory -> IO ClosedTheory) loadThyString as = loadGenericThy loader as where loader str = case parseOpenTheoryString (defines as) str of - Right thy -> return thy - Left err -> error $ show err + Right thy -> return $ Right thy + Left err -> return $ Left $ "parse error: " ++ show err -- | The defined pre-processor flags in the argument. defines :: Arguments -> [String] defines = findArg "defines" +-- FIXME: SM: This naming, tupling, blah is a mess and can be done more +-- cleanly. DO IT! + -- | Load an open/closed theory given a loader function. -loadGenericThy :: (a -> IO OpenTheory) - -> Arguments - -> (a -> IO OpenTheory, OpenTheory -> IO ClosedTheory) +loadGenericThy :: a -> Arguments -> (a, OpenTheory -> IO ClosedTheory) loadGenericThy loader as = (loader, (closeThy as) <=< addMessageDeductionRuleVariants) diff --git a/src/Theory.hs b/src/Theory.hs --- a/src/Theory.hs +++ b/src/Theory.hs @@ -38,6 +38,7 @@ , thyCache , thyItems , theoryRules + , theoryLemmas , theoryAxioms , addAxiom , addLemma @@ -201,11 +202,10 @@ -- soundness sequent, if required. closeProtoRule :: MaudeHandle -> OpenProtoRule -> ClosedProtoRule closeProtoRule hnd ruE = ClosedProtoRule ruE (variantsProtoRule hnd ruE) - -- | Close a rule cache. Hower, note that the -- requires case distinctions are not computed here. -closeRuleCache :: [LNFormula] -- ^ Axioms to use. - -> [LNFormula] -- ^ Typing lemmas to use. +closeRuleCache :: [LNGuarded] -- ^ Axioms to use. + -> [LNGuarded] -- ^ Typing lemmas to use. -> SignatureWithMaude -- ^ Signature of theory. -> [ClosedProtoRule] -- ^ Protocol rules with variants. -> OpenRuleCache -- ^ Intruder rules modulo AC. @@ -222,8 +222,11 @@ injFactInstances = simpleInjectiveFactInstances $ L.get cprRuleE <$> protoRules - -- precomputing the case distinctions - untypedCaseDists = precomputeCaseDistinctions ctxt0 axioms + -- precomputing the case distinctions: we make sure to only add safety + -- axioms. Otherwise, it wouldn't be sound to use the precomputed case + -- distinctions for properties proven using induction. + safetyAxioms = filter isSafetyFormula axioms + untypedCaseDists = precomputeCaseDistinctions ctxt0 safetyAxioms typedCaseDists = refineWithTypingAsms typAsms ctxt0 untypedCaseDists -- classifying the rules @@ -608,10 +611,11 @@ TextItem -- extract typing axioms and lemmas - axioms = [ L.get axFormula ax | AxiomItem ax <- items ] + axioms = do AxiomItem ax <- items + return $ formulaToGuarded_ $ L.get axFormula ax typAsms = do LemmaItem lem <- items guard (isTypingLemma lem) - return $ L.get lFormula lem + return $ formulaToGuarded_ $ L.get lFormula lem -- extract protocol rules rules = theoryRules (Theory errClose errClose errClose items) @@ -689,21 +693,26 @@ add prf = fromMaybe prf $ runProver prover ctxt 0 sys prf -- | Construct a constraint system for verifying the given formula. -mkSystem :: ProofContext -> [Axiom] -> [TheoryItem r p] -> LNFormula -> System -mkSystem ctxt axioms preItems = - addAxiomsAndLemmasToSystem - . formulaToSystem (L.get pcCaseDistKind ctxt) (L.get pcTraceQuantifier ctxt) +mkSystem :: ProofContext -> [Axiom] -> [TheoryItem r p] + -> LNFormula -> System +mkSystem ctxt axioms previousItems = + -- Note that it is OK to add reusable lemmas directly to the system, as + -- they do not change the considered set of traces. This is the key + -- difference between lemmas and axioms. + addLemmas + . formulaToSystem (map (formulaToGuarded_ . L.get axFormula) axioms) + (L.get pcCaseDistKind ctxt) + (L.get pcTraceQuantifier ctxt) where - addAxiomsAndLemmasToSystem sys = - (`insertLemmas` sys) $ - map (L.get axFormula) axioms ++ - gatherReusableLemmas (L.get sCaseDistKind sys) + addLemmas sys = + insertLemmas (gatherReusableLemmas $ L.get sCaseDistKind sys) sys gatherReusableLemmas kind = do - LemmaItem lem <- preItems - guard $ lemmaCaseDistKind lem <= kind && - ReuseLemma `elem` L.get lAttributes lem - return $ L.get lFormula lem + LemmaItem lem <- previousItems + guard $ lemmaCaseDistKind lem <= kind + && ReuseLemma `elem` L.get lAttributes lem + && AllTraces == L.get lTraceQuantifier lem + return $ formulaToGuarded_ $ L.get lFormula lem ------------------------------------------------------------------------------ @@ -780,7 +789,10 @@ prettyAxiom :: HighlightDocument d => Axiom -> d prettyAxiom ax = kwAxiom <-> text (L.get axName ax) <> colon $-$ - (nest 2 $ doubleQuotes $ prettyLNFormula $ L.get axFormula ax) + (nest 2 $ doubleQuotes $ prettyLNFormula $ L.get axFormula ax) $-$ + (nest 2 $ if safety then lineComment_ "safety formula" else emptyDoc) + where + safety = isSafetyFormula $ formulaToGuarded_ $ L.get axFormula ax -- | Pretty print a lemma. prettyLemma :: HighlightDocument d => (p -> d) -> Lemma p -> d diff --git a/src/Theory/Constraint/Solver/CaseDistinctions.hs b/src/Theory/Constraint/Solver/CaseDistinctions.hs --- a/src/Theory/Constraint/Solver/CaseDistinctions.hs +++ b/src/Theory/Constraint/Solver/CaseDistinctions.hs @@ -67,7 +67,7 @@ -- given typing assumptions are justified. initialCaseDistinction :: ProofContext - -> [LNFormula] -- ^ Axioms. + -> [LNGuarded] -- ^ Axioms. -> Goal -> CaseDistinction initialCaseDistinction ctxt axioms goal = @@ -111,9 +111,8 @@ solveAllSafeGoals ths = solve [] where - -- safeGoal _ _ = False - safeGoal _ (_, (_, Useless)) = False - safeGoal doSplit (goal, _ ) = + safeGoal _ (_, (_, LoopBreaker)) = False + safeGoal doSplit (goal, _ ) = case goal of ChainG _ _ -> True ActionG _ fa -> not (isKUFact fa) @@ -158,9 +157,13 @@ :: ProofContext -- ^ Proof context used for refining the case distinction. -> CaseDistinction -- ^ Case distinction to use. -> Goal -- ^ Goal to match - -> Maybe CaseDistinction - -- ^ An adapted version of the case distinction and a matcher of the case - -- distinction goal to the substitution goal. + -> Maybe (Reduction [String]) + -- ^ A constraint reduction step to apply the resulting case distinction. + -- Note that this step assumes that the theorem has been imported using + -- 'someInst' into the context that this reduction is executed in. + -- + -- FIXME: This is a mess. Factor code such that this inter-dependency + -- between 'applyCaseDistinction' and 'matchToGoal' goes away. matchToGoal ctxt th goalTerm = case (goalTerm, get cdGoal th) of ( PremiseG (iTerm, premIdxTerm) faTerm @@ -168,27 +171,26 @@ let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of [] -> Nothing - subst:_ -> - let refine = do - modM sEdges (substNodePrem pPat (iPat, premIdxTerm)) - void (solveSubstEqs SplitNow subst) - return ((), []) - in Just $ snd $ refineCaseDistinction ctxt refine th + subst:_ -> Just $ genericApply subst $ + -- add the missing edge to each case of the theorem + modify sEdges (substNodePrem pPat (iPat, premIdxTerm)) (ActionG iTerm faTerm, ActionG iPat faPat) -> let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of [] -> Nothing - subst:_ -> - let refine = do - void (solveSubstEqs SplitNow subst) - return ((), []) - in Just $ snd $ refineCaseDistinction ctxt refine th + subst:_ -> Just $ genericApply subst id -- No other matches possible, as we only precompute case distinctions for -- premises and KU-actions. _ -> Nothing where + genericApply subst systemModifier = do + void (solveSubstEqs SplitNow subst) + (names, sysTh) <- disjunctionOfList $ getDisj $ get cdCases th + conjoinSystem (systemModifier sysTh) + return names + substNodePrem from to = S.map (\ e@(Edge c p) -> if p == from then Edge c to else e) @@ -211,11 +213,8 @@ | isJust $ matchToGoal ctxt th goal = Just $ do markGoalAsSolved "precomputed" goal thRenamed <- rename th - let thInst = fromJustNote "applyCaseDistinction: impossible" $ - matchToGoal ctxt thRenamed goal - (names, sysTh) <- disjunctionOfList $ getDisj $ get cdCases thInst - conjoinSystem sysTh - return names + fromJustNote "applyCaseDistinction: impossible" $ + matchToGoal ctxt thRenamed goal | otherwise = Nothing @@ -240,7 +239,7 @@ -- | Precompute a saturated set of case distinctions. precomputeCaseDistinctions :: ProofContext - -> [LNFormula] -- ^ Axioms. + -> [LNGuarded] -- ^ Axioms. -> [CaseDistinction] precomputeCaseDistinctions ctxt axioms = map cleanupCaseNames $ saturateCaseDistinctions ctxt rawCaseDists @@ -294,17 +293,15 @@ -- | Refine a set of case distinction by exploiting additional typing -- assumptions. refineWithTypingAsms - :: [LNFormula] -- ^ Typing assumptions to use. + :: [LNGuarded] -- ^ Typing assumptions to use. -> ProofContext -- ^ Proof context to use. -> [CaseDistinction] -- ^ Original, untyped case distinctions. -> [CaseDistinction] -- ^ Refined, typed case distinctions. -refineWithTypingAsms assumptions0 ctxt cases0 = +refineWithTypingAsms assumptions ctxt cases0 = fmap (modifySystems removeFormulas) $ saturateCaseDistinctions ctxt $ modifySystems updateSystem <$> cases0 where - assumptions = - map (either (error . render) id . formulaToGuarded) assumptions0 modifySystems = modify cdCases . fmap . second updateSystem se = modify sFormulas (S.union (S.fromList assumptions)) $ diff --git a/src/Theory/Constraint/Solver/Goals.hs b/src/Theory/Constraint/Solver/Goals.hs --- a/src/Theory/Constraint/Solver/Goals.hs +++ b/src/Theory/Constraint/Solver/Goals.hs @@ -26,6 +26,7 @@ import qualified Data.DAG.Simple as D (cyclic) import qualified Data.Map as M +import qualified Data.Set as S import Control.Basics import Control.Category @@ -45,7 +46,15 @@ -- Extracting Goals ------------------------------------------------------------------------------ -data Usefulness = Useful | Useless +data Usefulness = + Useful + -- ^ A goal that is likely to result in progress. + | LoopBreaker + -- ^ A goal that is delayed to avoid immediate termination. Needs to be + -- handled fairly. + | ProbablySolvable + -- ^ A goal that is very likely to be solvable without introducing further + -- interesting constraints. These goals are delayed until the very end. deriving (Show, Eq) -- | Goals annotated with their number and usefulness. @@ -60,13 +69,16 @@ compare a b = check a b where - check Useful Useful = EQ - check Useless Useless = EQ - check x y = compare (tag x) (tag y) - tag (Useful) = 0 :: Int - tag (Useless) = 1 :: Int + check Useful Useful = EQ + check LoopBreaker LoopBreaker = EQ + check ProbablySolvable ProbablySolvable = EQ + check x y = compare (tag x) (tag y) + tag (Useful) = 0 :: Int + tag (LoopBreaker) = 1 + tag (ProbablySolvable) = 2 + -- | The list of goals that must be solved before a solution can be extracted. -- Each goal is annotated with its age and an indicator for its usefulness. openGoals :: System -> [AnnotatedGoal] @@ -80,6 +92,7 @@ || isMsgVar m || sortOfLNTerm m == LSortPub -- handled by 'insertAction' || isPair m || isInverse m || isProduct m + || isNullaryFunction m ActionG _ _ -> not solved PremiseG _ _ -> not solved -- Technically the 'False' disj would be a solvable goal. However, we @@ -97,17 +110,20 @@ -- explicitly if they still exist. SplitG idx -> splitExists (get sEqStore sys) idx - let useful = case goal of - -- Note that 'solveAllSafeGoals' in "CaseDistinctions" relies on - -- looping goals being classified as 'Useless'. - _ | get gsLoopBreaker status -> Useless + let + useful = case goal of + _ | get gsLoopBreaker status -> LoopBreaker ActionG i (kFactView -> Just (UpK, m)) - | isSimpleTerm m || deducible i m -> Useless + -- if there are KU-guards then all knowledge goals are useful + | hasKUGuards -> Useful + | isSimpleTerm m || deducible i m -> ProbablySolvable _ -> Useful return (goal, (get gsNr status, useful)) where existingDeps = rawLessRel sys + hasKUGuards = + any ((KUFact `elem`) . guardFactTags) $ S.toList $ get sFormulas sys -- We use the following heuristic for marking KU-actions as useful (worth -- solving now) or useless (to be delayed until no more useful goals @@ -216,7 +232,7 @@ let m = case kFactView faConc of Just (DnK, m') -> m' _ -> error $ "solveChain: impossible" - caseName (viewTerm -> FApp o _) = show o + caseName (viewTerm -> FApp o _) = showFunSymName o caseName t = show t return $ caseName m `disjunction` diff --git a/src/Theory/Constraint/Solver/ProofMethod.hs b/src/Theory/Constraint/Solver/ProofMethod.hs --- a/src/Theory/Constraint/Solver/ProofMethod.hs +++ b/src/Theory/Constraint/Solver/ProofMethod.hs @@ -258,8 +258,9 @@ solveGoalMethod (goal, (nr, usefulness)) = ( SolveGoal goal , "nr. " ++ show nr ++ case usefulness of - Useful -> "" - Useless -> " (marked useless)" + Useful -> "" + LoopBreaker -> " (loop breaker)" + ProbablySolvable -> " (probably solvable)" ) newtype Heuristic = Heuristic [GoalRanking] @@ -320,9 +321,9 @@ -> System -> [AnnotatedGoal] -> [AnnotatedGoal] smartRanking allowPremiseGLoopBreakers sys = - delayUseless . unmark . sortDecisionTree solveFirst . goalNrRanking + sortOnUsefulness . unmark . sortDecisionTree solveFirst . goalNrRanking where - delayUseless = sortOn (snd . snd) + sortOnUsefulness = sortOn (snd . snd) unmark | allowPremiseGLoopBreakers = map unmarkPremiseG | otherwise = id @@ -338,10 +339,16 @@ , isFreshKnowsGoal . fst , isSplitGoalSmall . fst , isDoubleExpGoal . fst - , isLoopBreakerGoal ] - -- prefer knowledge goals and loop-breaker premises - -- before expensive equation splits + , isNoLargeSplitGoal . fst ] + -- move the rest (mostly more expensive KU-goals) before expensive + -- equation splits + -- FIXME: This small split goal preferral is quite hacky when using + -- induction. The problem is that we may end up solving message premise + -- goals all the time instead performing a necessary split. We should make + -- sure that a split does not get too old. + smallSplitGoalSize = 3 + isNonLoopBreakerProtoFactGoal (PremiseG _ fa, (_, Useful)) = not $ isKFact fa isNonLoopBreakerProtoFactGoal _ = False @@ -356,14 +363,13 @@ Just (viewTerm2 -> FExp _ (viewTerm2 -> FMult _)) -> True _ -> False - isLoopBreakerGoal (ActionG _ fa, _ ) = isKUFact fa - isLoopBreakerGoal (PremiseG _ _, (_, Useless)) = True - isLoopBreakerGoal _ = False - -- Be conservative on splits that don't exist. isSplitGoalSmall (SplitG sid) = - maybe False (< 3) $ splitSize (L.get sEqStore sys) sid + maybe False (<= smallSplitGoalSize) $ splitSize (L.get sEqStore sys) sid isSplitGoalSmall _ = False + + isNoLargeSplitGoal goal@(SplitG _) = isSplitGoalSmall goal + isNoLargeSplitGoal _ = True -- | @sortDecisionTree xs ps@ returns a reordering of @xs@ -- such that the sublist satisfying @ps!!0@ occurs first, diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs --- a/src/Theory/Constraint/Solver/Reduction.hs +++ b/src/Theory/Constraint/Solver/Reduction.hs @@ -76,6 +76,7 @@ import qualified Data.Foldable as F import qualified Data.Map as M import qualified Data.Set as S +import Data.List (mapAccumL) import Safe import Control.Basics @@ -266,7 +267,7 @@ modM sEdges (\es -> foldr S.insert es [ Edge c p | (c,_,_,p) <- edges]) -- | Insert an 'Action' atom. Ensures that (almost all) trivial *KU* actions --- are solved immediatly using rule *S_{at,u,triv}*. We currently avoid +-- are solved immediately using rule *S_{at,u,triv}*. We currently avoid -- adding intermediate products. Indicates whether nodes other than the given -- action have been added to the constraint system. -- @@ -292,7 +293,7 @@ where goal = ActionG i fa -- Here we rely on the fact that the action is new. Otherwise, we might - -- loop due to generating new KU-nodes that are merged immediatly. + -- loop due to generating new KU-nodes that are merged immediately. requiresKU t = do j <- freshLVar "vk" LSortNode let faKU = kuFact t @@ -558,12 +559,17 @@ joinSets sEdges F.mapM_ insertLast $ get sLastAtom sys F.mapM_ (uncurry insertLess) $ get sLessAtoms sys - mapM_ (uncurry insertGoalStatus) $ M.toList $ get sGoals sys + -- split-goals are not valid anymore + mapM_ (uncurry insertGoalStatus) $ filter (not . isSplitGoal . fst) $ M.toList $ get sGoals sys F.mapM_ insertFormula $ get sFormulas sys -- update nodes _ <- (setNodes . (M.toList (get sNodes sys) ++) . M.toList) =<< getM sNodes -- conjoin equation store - modM sConjDisjEqs (`mappend` get sConjDisjEqs sys) + eqs <- getM sEqStore + let (eqs',splitIds) = (mapAccumL addDisj eqs (map snd . getConj $ get sConjDisjEqs sys)) + setM sEqStore eqs' + -- add split-goals for all disjunctions of sys + mapM_ (`insertGoal` False) $ SplitG <$> splitIds void (solveSubstEqs SplitNow $ get sSubst sys) -- Propagate substitution changes. Ignore change indicator, as it is -- assumed to be 'Changed' by default. @@ -571,8 +577,6 @@ where joinSets :: Ord a => (System :-> S.Set a) -> Reduction () joinSets proj = modM proj (`S.union` get proj sys) - - -- Unification via the equation store ------------------------------------- diff --git a/src/Theory/Constraint/System.hs b/src/Theory/Constraint/System.hs --- a/src/Theory/Constraint/System.hs +++ b/src/Theory/Constraint/System.hs @@ -100,7 +100,7 @@ import Data.Binary import qualified Data.DAG.Simple as D import Data.DeriveTH -import Data.List (foldl') +import Data.List (foldl', partition) import qualified Data.Map as M import Data.Maybe (fromMaybe) import Data.Monoid (Monoid(..)) @@ -134,12 +134,18 @@ -- | Case dinstinction kind that are allowed. The order of the kinds -- corresponds to the subkinding relation: untyped < typed. data CaseDistKind = UntypedCaseDist | TypedCaseDist - deriving( Eq, Ord ) + deriving( Eq ) instance Show CaseDistKind where show UntypedCaseDist = "untyped" show TypedCaseDist = "typed" +instance Ord CaseDistKind where + compare UntypedCaseDist UntypedCaseDist = EQ + compare UntypedCaseDist TypedCaseDist = LT + compare TypedCaseDist UntypedCaseDist = GT + compare TypedCaseDist TypedCaseDist = EQ + -- | The status of a 'Goal'. Use its 'Semigroup' instance to combine the -- status info of goals that collapse. data GoalStatus = GoalStatus @@ -203,25 +209,35 @@ -- | Returns the constraint system that has to be proven to show that given -- formula holds in the context of the given theory. -formulaToSystem :: CaseDistKind -> SystemTraceQuantifier -> LNFormula -> System -formulaToSystem kind traceQuantifier fm = - L.set sFormulas (S.singleton gf) (emptySystem kind) +formulaToSystem :: [LNGuarded] -- ^ Axioms to add + -> CaseDistKind -- ^ Case distinction kind + -> SystemTraceQuantifier -- ^ Trace quantifier + -> LNFormula + -> System +formulaToSystem axioms kind traceQuantifier fm = + insertLemmas safetyAxioms + $ L.set sFormulas (S.singleton gf2) + $ (emptySystem kind) where - adapt = case traceQuantifier of - ExistsSomeTrace -> id - ExistsNoTrace -> gnot - gf = either (error . render) id (adapt <$> formulaToGuarded fm) + (safetyAxioms, otherAxioms) = partition isSafetyFormula axioms + gf0 = formulaToGuarded_ fm + gf1 = case traceQuantifier of + ExistsSomeTrace -> gf0 + ExistsNoTrace -> gnot gf0 + -- Non-safety axioms must be added to the formula, as they render the set + -- of traces non-prefix-closed, which makes the use of induction unsound. + gf2 = gconj $ gf1 : otherAxioms -- | Add a lemma / additional assumption to a constraint system. -insertLemma :: LNFormula -> System -> System -insertLemma fm0 = - go (either (error . render) id $ formulaToGuarded fm0) +insertLemma :: LNGuarded -> System -> System +insertLemma = + go where go (GConj conj) = foldr (.) id $ map go $ getConj conj go fm = L.modify sLemmas (S.insert fm) -- | Add lemmas / additional assumptions to a constraint system. -insertLemmas :: [LNFormula] -> System -> System +insertLemmas :: [LNGuarded] -> System -> System insertLemmas fms sys = foldl' (flip insertLemma) sys fms ------------------------------------------------------------------------------ diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs --- a/src/Theory/Constraint/System/Guarded.hs +++ b/src/Theory/Constraint/System/Guarded.hs @@ -1,5 +1,6 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -29,6 +30,7 @@ , ginduct , formulaToGuarded + , formulaToGuarded_ -- ** Transformation , simplifyGuarded @@ -40,7 +42,10 @@ , isDisjunction , isAllGuarded , isExGuarded + , isSafetyFormula + , guardFactTags + -- ** Conversions to non-bound representations , bvarToLVar , openGuarded @@ -70,6 +75,7 @@ import Data.Either (partitionEithers) import Data.Foldable (Foldable(..), foldMap) import Data.List +import qualified Data.DList as D import Data.Monoid (Monoid(..)) import Data.Traversable hiding (mapM, sequence) @@ -94,26 +100,50 @@ -- f@i atoms in as. deriving (Eq, Ord, Show) -isConjunction :: Guarded t t1 t2 -> Bool +isConjunction :: Guarded s c v -> Bool isConjunction (GConj _) = True isConjunction _ = False -isDisjunction :: Guarded t t1 t2 -> Bool +isDisjunction :: Guarded s c v -> Bool isDisjunction (GDisj _) = True isDisjunction _ = False -isExGuarded :: Guarded t t1 t2 -> Bool +isExGuarded :: Guarded s c v -> Bool isExGuarded (GGuarded Ex _ _ _) = True isExGuarded _ = False -isAllGuarded :: Guarded t t1 t2 -> Bool +isAllGuarded :: Guarded s c v -> Bool isAllGuarded (GGuarded All _ _ _) = True isAllGuarded _ = False +-- | Check whether the guarded formula is closed and does not contain an +-- existential quantifier. This under-approximates the question whether the +-- formula is a safety formula. A safety formula @phi@ has the property that a +-- trace violating it can never be extended to a trace satisfying it. +isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> Bool +isSafetyFormula gf0 = + null (frees [gf0]) && noExistential gf0 + where + noExistential (GAto _ ) = True + noExistential (GGuarded Ex _ _ _) = False + noExistential (GGuarded All _ _ gf) = noExistential gf + noExistential (GDisj disj) = all noExistential $ getDisj disj + noExistential (GConj conj) = all noExistential $ getConj conj + +-- | All 'FactTag's that are used in guards. +guardFactTags :: Guarded s c v -> [FactTag] +guardFactTags = + D.toList . + foldGuarded mempty (mconcat . getDisj) (mconcat . getConj) getTags + where + getTags _qua _ss atos inner = + mconcat [ D.singleton tag | Action _ (Fact tag _) <- atos ] <> inner + ------------------------------------------------------------------------------ -- Folding ------------------------------------------------------------------------------ + -- | Fold a guarded formula. foldGuarded :: (Atom (VTerm c (BVar v)) -> b) -> (Disj b -> b) @@ -355,6 +385,13 @@ instance Document d => Error (ErrorDoc d) where noMsg = emptyDoc strMsg = text + + +-- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is +-- equivalent to @fm@ under the assumption that this is possible. +-- If not, then 'error' is called. +formulaToGuarded_ :: LNFormula -> LNGuarded +formulaToGuarded_ = either (error . render) id . formulaToGuarded -- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is -- equivalent to @fm@ if possible. diff --git a/src/Theory/Text/Parser/Token.hs b/src/Theory/Text/Parser/Token.hs --- a/src/Theory/Text/Parser/Token.hs +++ b/src/Theory/Text/Parser/Token.hs @@ -149,7 +149,7 @@ -- | Parse a symbol. symbol :: String -> Parser String -symbol = try . T.symbol spthy +symbol sym = try (T.symbol spthy sym) ("\"" ++ sym ++ "\"") -- | Parse a symbol without returning the parsed string. symbol_ :: String -> Parser () diff --git a/src/Theory/Tools/EquationStore.hs b/src/Theory/Tools/EquationStore.hs --- a/src/Theory/Tools/EquationStore.hs +++ b/src/Theory/Tools/EquationStore.hs @@ -32,6 +32,7 @@ -- ** Adding equalities , addEqs , addRuleVariants + , addDisj -- ** Case splitting , performSplit @@ -157,7 +158,7 @@ splits eqs = map fst $ nub $ sortOn snd [ (idx, S.size conj) | (idx, conj) <- getConj $ L.get eqsConj eqs ] --- | Returns the number of cases for a given 'SplitId'. +-- | Returns 'True' if the 'SplitId' is valid. splitExists :: EqStore -> SplitId -> Bool splitExists eqs = isJust . splitSize eqs diff --git a/src/Theory/Tools/Wellformedness.hs b/src/Theory/Tools/Wellformedness.hs --- a/src/Theory/Tools/Wellformedness.hs +++ b/src/Theory/Tools/Wellformedness.hs @@ -341,6 +341,17 @@ atomTerms (Less i j) = [i, j] atomTerms (Last i) = [i] +-- TODO: Perhaps a lot of errors would be captured when making the signature +-- of facts, term, and atom constructors explicit. +lemmaAttributeReport :: OpenTheory -> WfErrorReport +lemmaAttributeReport thy = do + lem <- theoryLemmas thy + guard $ get lTraceQuantifier lem == ExistsTrace + && ReuseLemma `elem` get lAttributes lem + return ( "attributes" + , text "lemma" <-> (text $ quote $ get lName lem) <> colon <-> + text "cannot reuse 'exists-trace' lemmas" + ) -- | Check for mistakes in lemmas. -- @@ -490,6 +501,7 @@ , ruleSortsReport , factReports , formulaReports + , lemmaAttributeReport , multRestrictedReport ] diff --git a/src/Web/Dispatch.hs b/src/Web/Dispatch.hs --- a/src/Web/Dispatch.hs +++ b/src/Web/Dispatch.hs @@ -70,7 +70,8 @@ -> Bool -- ^ Load last proof state if present -> Bool -- ^ Automatically save proof state -> (FilePath -> IO ClosedTheory) -- ^ Theory loader (from file). - -> (String -> IO ClosedTheory) -- ^ Theory loader (from string). + -> (String -> IO (Either String ClosedTheory)) + -- ^ Theory loader (from string). -> (OpenTheory -> IO ClosedTheory) -- ^ Theory closer. -> Bool -- ^ Show debugging messages? -> FilePath -- ^ Path to static content directory diff --git a/src/Web/Handler.hs b/src/Web/Handler.hs --- a/src/Web/Handler.hs +++ b/src/Web/Handler.hs @@ -337,12 +337,17 @@ case result of Nothing -> setMessage "Post request failed." - Just fileinfo -> do - yesod <- getYesod - closedThy <- liftIO $ parseThy yesod (BS.unpack $ fileContent fileinfo) - void $ putTheory Nothing - (Just $ Upload $ T.unpack $ fileName fileinfo) closedThy - setMessage "Loaded new theory!" + Just fileinfo + | BS.null $ fileContent fileinfo -> setMessage "No theory file given." + | otherwise -> do + yesod <- getYesod + closedThy <- liftIO $ parseThy yesod (BS.unpack $ fileContent fileinfo) + case closedThy of + Left err -> setMessage $ "Theory loading failed:\n" <> toHtml err + Right thy -> do + void $ putTheory Nothing + (Just $ Upload $ T.unpack $ fileName fileinfo) thy + setMessage "Loaded new theory!" theories <- getTheories defaultLayout $ do setTitle "Welcome to the Tamarin prover" diff --git a/src/Web/Theory.hs b/src/Web/Theory.hs --- a/src/Web/Theory.hs +++ b/src/Web/Theory.hs @@ -133,14 +133,15 @@ where ppCase step = markStatus (fst $ psInfo step) - ppStep step = case fst $ psInfo step of - (Nothing, _) -> superfluousStep - (_, Nothing) -> stepLink ["sorry-step"] <> - case psMethod step of - Sorry _ -> emptyDoc - _ -> removeStep - (_, Just True) -> stepLink ["hl_good"] - (_, Just False) -> stepLink ["hl_bad"] + ppStep step = + case fst $ psInfo step of + (Nothing, _) -> superfluousStep + (_, Nothing) -> stepLink ["sorry-step"] + (_, Just True) -> stepLink ["hl_good"] + (_, Just False) -> stepLink ["hl_bad"] + <> case psMethod step of + Sorry _ -> emptyDoc + _ -> removeStep where ppMethod = prettyProofMethod $ psMethod step stepLink cls = linkToPath renderUrl @@ -218,8 +219,12 @@ bold = withTag "strong" [] . text overview n info p = linkToPath renderUrl (TheoryPathMR tidx p) [] (bold n <-> info) messageLink = overview "Message theory" (text "") TheoryMessage - ruleLink = overview "Multiset rewriting rules and axioms" rulesInfo TheoryRules + ruleLink = overview ruleLinkMsg rulesInfo TheoryRules + ruleLinkMsg = "Multiset rewriting rules" ++ + if null(theoryAxioms thy) then "" else " and axioms" + reqCasesLink name k = overview name (casesInfo k) (TheoryCaseDist k 0 0) + {- -- | A snippet that explains a sequent using a rendered graph and the pretty diff --git a/src/Web/Types.hs b/src/Web/Types.hs --- a/src/Web/Types.hs +++ b/src/Web/Types.hs @@ -101,7 +101,7 @@ , workDir :: FilePath -- ^ The working directory (for storing/loading theories). -- , parseThy :: MonadIO m => String -> GenericHandler m ClosedTheory - , parseThy :: String -> IO ClosedTheory + , parseThy :: String -> IO (Either String ClosedTheory) -- ^ Parse a closed theory according to command-line arguments. , closeThy :: OpenTheory -> IO ClosedTheory -- ^ Close an open theory according to command-line arguments. diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal --- a/tamarin-prover.cabal +++ b/tamarin-prover.cabal @@ -1,7 +1,7 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover -version: 0.8.0.0 +version: 0.8.1.0 license: GPL license-file: LICENSE category: Theorem Provers @@ -80,6 +80,7 @@ examples/loops/Minimal_Create_Use_Destroy.spthy examples/loops/Minimal_Typing_Example.spthy examples/loops/Minimal_Loop_Example.spthy + examples/loops/Typing_and_Destructors.spthy examples/loops/JCS12_Typing_Example.spthy examples/loops/TESLA_Scheme1.spthy @@ -165,6 +166,13 @@ ghc-options: -Wall -fwarn-tabs -rtsopts ghc-prof-options: -auto-all + + -- Parallelize by default. Only activated for GHC 7.4, as this flag was + -- unstable in earlier -- versions; i.e., it resulted in command-line + -- parsing errors. + if impl(ghc >= 7.4) + ghc-options: -with-rtsopts=-N + hs-source-dirs: src main-is: Main.hs @@ -204,6 +212,7 @@ , deepseq == 1.3.* , array >= 0.3 && < 0.5 , containers >= 0.4.2 && < 0.5 + , dlist == 0.5.* , mtl == 2.0.* , cmdargs == 0.9.* , filepath >= 1.1 && < 1.4 @@ -221,8 +230,8 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils == 0.8.* - , tamarin-prover-term == 0.8.* + , tamarin-prover-utils >= 0.8.1 && < 0.9 + , tamarin-prover-term >= 0.8.1 && < 0.9 other-modules: