Parameters: Issue#419 and tamarin-prover#292 (tamarin-prover#475)

* [ADD] checkIfLemmasInTheory in TheoryLoader  and Temporary putStrLn in one case

* Aesthetic

* Issue#419: [UPD] Put check function in Wellformedness + Adjustement of `checkWellformedness` calls

* [ADD] _thyParams Options in Theory and Options in DiffTheory with _diffThyParams

* [DEL] Useless boolean

* Issue#419: [ADD] params in _thyParams AND load them in checkWellformedness from HTML

* Issue#419: [FIX] in Web/Theory.hs + [ADD] Diff version

* [DEL] DiffOption -> Option

* Issue#419: [UPD] Option (delete DiffOption)

* Issue#419: [UPD] Changing Wellfordness Check and [FIX] issue when loading file

* Issue#419: [ADD] Comments

* Issue#419: [UPD] add to OpenTheory rather than in between on TransThy

* [ADD] Option and parameter : OpenChainLimit and SaturationLimit

* [ADD] readMaybe for OCL and SL parameters

* [UPD] LoadDiff -> add Options  + loadClosedDiffThyWfReport + Comments

* [UPD] Changements addParamOptions instead of just the lemmasToProve
++ minors changes

* [ADD] Comments

* [UPD] Putting flagOpt --> flagReq : because the default value already exist if no values are specified

* [ADD] Readibility and change flag names

* [Renaming]

* [REVERT] flagReq -> flagOpt

* [FIX] Merge issue - Forgot case with empty args

Co-authored-by: Nicolas Beaudouin <nicolas.beaudouin@telecomnancy.eu>

lib/theory/src/ClosedTheory.hs

@@ -398,7 +398,8 @@ prettyClosedDiffTheory thy = if containsManualRuleVariantsDiff mergedRules
             ,_diffThyCacheRight=(L.get diffThyCacheRight thy)
             ,_diffThyDiffCacheLeft=(L.get diffThyDiffCacheLeft thy)
             ,_diffThyDiffCacheRight=(L.get diffThyDiffCacheRight thy)
-            ,_diffThyItems = mergedRules}
+            ,_diffThyItems = mergedRules
+            ,_diffThyOptions =(L.get diffThyOptions thy)}
     ppInjectiveFactInsts crc =
         case S.toList $ L.get crcInjectiveFactInsts crc of
             []   -> emptyDoc

lib/theory/src/Items/OptionItem.hs

@@ -28,8 +28,10 @@ data Option = Option
         , _asynchronousChannels       :: Bool
         , _compressEvents       :: Bool
         , _forcedInjectiveFacts :: S.Set FactTag
+        , _lemmasToProve        :: [String]
+        , _openChainsLimit      :: Integer
+        , _saturationLimit      :: Integer
         }
         deriving( Eq, Ord, Show, Generic, NFData, Binary )
 $(mkLabels [''Option])
--- generate accessors for Option data structure records
-
+-- generate accessors for Option data structure records

lib/theory/src/OpenTheory.hs

@@ -383,7 +383,8 @@ addAutoSourcesLemma hnd lemmaName (ClosedRuleCache _ raw _ _) items =
 -- Open theory construction / modification
 ------------------------------------------------------------------------------
 defaultOption :: Option
-defaultOption = Option False False False False False False False S.empty
+defaultOption = Option False False False False False False False S.empty [] 10 5
+
 
 
 -- | Default theory
@@ -392,7 +393,7 @@ defaultOpenTheory flag = Theory "default" [] (emptySignaturePure flag) [] [] def
 
 -- | Default diff theory
 defaultOpenDiffTheory :: Bool -> OpenDiffTheory
-defaultOpenDiffTheory flag = DiffTheory "default" [] (emptySignaturePure flag) [] [] [] [] []
+defaultOpenDiffTheory flag = DiffTheory "default" [] (emptySignaturePure flag) [] [] [] [] [] defaultOption
 
 -- Add the default Diff lemma to an Open Diff Theory
 addDefaultDiffLemma:: OpenDiffTheory -> OpenDiffTheory

lib/theory/src/Prover.hs

@@ -26,10 +26,12 @@ import           Theory.Proof
 import           Theory.Text.Pretty
 import           Theory.Tools.AbstractInterpretation
 import           Theory.Tools.LoopBreakers
-import Lemma
-import ClosedTheory
-import TheoryObject
-import OpenTheory
+import           Lemma
+import           ClosedTheory
+import           TheoryObject
+import           OpenTheory
+
+import           Theory.Constraint.Solver.Sources     as Sources (IntegerParameters(..))
 
 
 -- | Close a theory by closing its associated rule set and checking the proof
@@ -69,16 +71,18 @@ closeDiffTheoryWithMaude sig thy0 autoSources =
   if autoSources && (containsPartialDeconstructions (cacheLeft items) || containsPartialDeconstructions (cacheRight items))
     then
       proveDiffTheory (const True) checkProof checkDiffProof
-        (DiffTheory (L.get diffThyName thy0) h sig (cacheLeft items') (cacheRight items') (diffCacheLeft items') (diffCacheRight items') items')
+        (DiffTheory (L.get diffThyName thy0) h sig (cacheLeft items') (cacheRight items') (diffCacheLeft items') (diffCacheRight items') items' (L.get diffThyOptions thy0))
     else
       proveDiffTheory (const True) checkProof checkDiffProof
-        (DiffTheory (L.get diffThyName thy0) h sig (cacheLeft items) (cacheRight items) (diffCacheLeft items) (diffCacheRight items) items)
+        (DiffTheory (L.get diffThyName thy0) h sig (cacheLeft items) (cacheRight items) (diffCacheLeft items) (diffCacheRight items) items (L.get diffThyOptions thy0))
+
   where
+    parameters = Sources.IntegerParameters (L.get (openChainsLimit.diffThyOptions) thy0) (L.get (saturationLimit.diffThyOptions) thy0)
     h              = L.get diffThyHeuristic thy0
-    diffCacheLeft  its = closeRuleCache restrictionsLeft  (typAsms its) S.empty sig (leftClosedRules its)  (L.get diffThyDiffCacheLeft  thy0) True
-    diffCacheRight its = closeRuleCache restrictionsRight (typAsms its) S.empty sig (rightClosedRules its) (L.get diffThyDiffCacheRight thy0) True
-    cacheLeft  its = closeRuleCache restrictionsLeft  (typAsms its) S.empty sig (leftClosedRules its)  (L.get diffThyCacheLeft  thy0) False
-    cacheRight its = closeRuleCache restrictionsRight (typAsms its) S.empty sig (rightClosedRules its) (L.get diffThyCacheRight thy0) False
+    diffCacheLeft  its = closeRuleCache parameters restrictionsLeft  (typAsms its) S.empty sig (leftClosedRules its)  (L.get diffThyDiffCacheLeft  thy0) True
+    diffCacheRight its = closeRuleCache parameters restrictionsRight (typAsms its) S.empty sig (rightClosedRules its) (L.get diffThyDiffCacheRight thy0) True
+    cacheLeft  its = closeRuleCache parameters restrictionsLeft  (typAsms its) S.empty sig (leftClosedRules its)  (L.get diffThyCacheLeft  thy0) False
+    cacheRight its = closeRuleCache parameters restrictionsRight (typAsms its) S.empty sig (rightClosedRules its) (L.get diffThyCacheRight thy0) False
 
     checkProof = checkAndExtendProver (sorryProver Nothing)
     checkDiffProof = checkAndExtendDiffProver (sorryDiffProver Nothing)
@@ -137,9 +141,9 @@ closeDiffTheoryWithMaude sig thy0 autoSources =
 
     -- extract protocol rules
     leftClosedRules  :: [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof s] -> [ClosedProtoRule]
-    leftClosedRules its = leftTheoryRules  (DiffTheory errClose errClose errClose errClose errClose errClose errClose its)
+    leftClosedRules its = leftTheoryRules  (DiffTheory errClose errClose errClose errClose errClose errClose errClose its errClose)
     rightClosedRules :: [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof s] -> [ClosedProtoRule]
-    rightClosedRules its = rightTheoryRules (DiffTheory errClose errClose errClose errClose errClose errClose errClose its)
+    rightClosedRules its = rightTheoryRules (DiffTheory errClose errClose errClose errClose errClose errClose errClose its errClose)
     errClose  = error "closeDiffTheory"
 
     addSolvingLoopBreakers = useAutoLoopBreakersAC
@@ -169,9 +173,10 @@ closeTheoryWithMaude sig thy0 autoSources =
         proveTheory (const True) checkProof
       $ Theory (L.get thyName thy0) h sig (cache items) items (L.get thyOptions thy0)
   where
+    parameters = Sources.IntegerParameters (L.get (openChainsLimit.thyOptions) thy0) (L.get (saturationLimit.thyOptions) thy0)
     h          = L.get thyHeuristic thy0
     forcedInjFacts = L.get forcedInjectiveFacts $ L.get thyOptions thy0
-    cache its = closeRuleCache restrictions (typAsms its) forcedInjFacts sig (rules its) (L.get thyCache thy0) False
+    cache its = closeRuleCache parameters restrictions (typAsms its) forcedInjFacts sig (rules its) (L.get thyCache thy0) False
     checkProof = checkAndExtendProver (sorryProver Nothing)
 
     -- Maude / Signature handle
@@ -437,11 +442,11 @@ openTheory  (Theory n h sig c items opts) = openTranslatedTheory(
 -- | Open a theory by dropping the closed world assumption and values whose
 -- soundness depends on it.
 openDiffTheory :: ClosedDiffTheory -> OpenDiffTheory
-openDiffTheory  (DiffTheory n h sig c1 c2 c3 c4 items) =
+openDiffTheory  (DiffTheory n h sig c1 c2 c3 c4 items opts) =
     -- We merge duplicate rules if they were split into variants
     DiffTheory n h (toSignaturePure sig) (openRuleCache c1) (openRuleCache c2) (openRuleCache c3) (openRuleCache c4)
       (mergeOpenProtoRulesDiff $ map (mapDiffTheoryItem id (\(x, y) -> (x, (openProtoRule y))) (\(DiffLemma s a p) -> (DiffLemma s a (incrementalToSkeletonDiffProof p))) (\(x, Lemma a b c d e) -> (x, Lemma a b c d (incrementalToSkeletonProof e)))) items)
-
+      opts
 
 ------------------------------------------------------------------------------
 -- References to lemmas

lib/theory/src/Rule.hs

@@ -27,6 +27,7 @@ import           Theory.Tools.RuleVariants
 import           Theory.Tools.IntruderRules
 
 import           Term.Positions
+import Theory.Constraint.Solver.Sources (IntegerParameters)
 
 
 
@@ -113,15 +114,16 @@ closeIntrRule _   ir                                        = [ir]
 
 -- | Close a rule cache. Hower, note that the
 -- requires case distinctions are not computed here.
-closeRuleCache :: [LNGuarded]        -- ^ Restrictions to use.
+closeRuleCache :: IntegerParameters  -- ^ Parameters for open chains and saturation limits
+               -> [LNGuarded]        -- ^ Restrictions to use.
                -> [LNGuarded]        -- ^ Source lemmas to use.
                -> S.Set FactTag      -- ^ Fact tags forced to be injective
                -> SignatureWithMaude -- ^ Signature of theory.
                -> [ClosedProtoRule]  -- ^ Protocol rules with variants.
                -> OpenRuleCache      -- ^ Intruder rules modulo AC.
                -> Bool               -- ^ Diff or not
                -> ClosedRuleCache    -- ^ Cached rules and case distinctions.
-closeRuleCache restrictions typAsms forcedInjFacts sig protoRules intrRules isdiff = -- trace ("closeRuleCache: " ++ show classifiedRules) $
+closeRuleCache parameters restrictions typAsms forcedInjFacts sig protoRules intrRules isdiff = -- trace ("closeRuleCache: " ++ show classifiedRules) $
     ClosedRuleCache
         classifiedRules rawSources refinedSources injFactInstances
   where
@@ -139,8 +141,8 @@ closeRuleCache restrictions typAsms forcedInjFacts sig protoRules intrRules isdi
     -- restrictions. Otherwise, it wouldn't be sound to use the precomputed case
     -- distinctions for properties proven using induction.
     safetyRestrictions = filter isSafetyFormula restrictions
-    rawSources         = precomputeSources ctxt0 safetyRestrictions
-    refinedSources     = refineWithSourceAsms typAsms ctxt0 rawSources
+    rawSources         = precomputeSources parameters ctxt0 safetyRestrictions
+    refinedSources     = refineWithSourceAsms parameters typAsms ctxt0 rawSources
 
     -- Maude handle
     hnd = L.get sigmMaudeHandle sig

lib/theory/src/Theory/Constraint/Solver/Sources.hs

@@ -1,3 +1,6 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
 -- |
 -- Copyright   : (c) 2011,2012 Simon Meier
 -- License     : GPL v3 (see LICENSE)
@@ -22,6 +25,11 @@ module Theory.Constraint.Solver.Sources (
   -- ** Redundant cases
   , removeRedundantCases
 
+  -- Paramters type
+  , IntegerParameters(..)
+  , paramOpenChainsLimit
+  , paramSaturationLimit
+
   ) where
 
 import           Prelude                                 hiding (id, (.))
@@ -58,6 +66,17 @@ import           Theory.Model
 import           Control.Monad.Bind
 
 import           Debug.Trace
+import qualified GHC.Generics as G
+import qualified Data.Binary  as B
+
+
+-- | Parameters
+data IntegerParameters = IntegerParameters 
+    {
+      _paramOpenChainsLimit :: Integer
+    , _paramSaturationLimit :: Integer
+    } deriving( Eq, Ord, Show, G.Generic, NFData, B.Binary )
+$(mkLabels [''IntegerParameters])
 
 ------------------------------------------------------------------------------
 -- Precomputing case distinctions
@@ -122,9 +141,9 @@ refineSource ctxt proofStep th =
 -- repeatedly simplifying the proof state.
 --
 -- Returns the names of the steps applied.
-solveAllSafeGoals :: [Source] -> Reduction [String]
-solveAllSafeGoals ths' =
-    solve ths' [] Nothing 10
+solveAllSafeGoals :: [Source] -> Integer -> Reduction [String]
+solveAllSafeGoals ths' openChainsLimit =
+    solve ths' [] Nothing openChainsLimit
   where
 --    extensiveSplitting = unsafePerformIO $
 --      (getEnv "TAMARIN_EXTENSIVE_SPLIT" >> return True) `catchIOError` \_ -> return False
@@ -133,7 +152,7 @@ solveAllSafeGoals ths' =
       case goal of
         ChainG _ _    -> if (chainsLeft > 0)
                             then True
-                            else (trace "Stopping precomputation, too many chain goals." False)
+                            else trace ("[Open Chains] Too many chain goals, stopping precomputation. Open Chains limits (can be changed with -c=): "++ show openChainsLimit) False
         ActionG _ fa  -> not (isKUFact fa)
         -- we do not solve KD goals for Xor facts as insertAction inserts
         -- these goals directly. This prevents loops in the precomputations
@@ -334,35 +353,35 @@ applySource ctxt th0 goal = case matchToGoal ctxt th0 goal of
   where
     keepVarBindings = M.fromList (map (\v -> (v, v)) (frees goal))
 
-
 -- | Saturate the sources with respect to each other such that no
 -- additional splitting is introduced; i.e., only rules with a single or no
 -- conclusion are used for the saturation.
 saturateSources
-    :: ProofContext -> [Source] -> [Source]
-saturateSources ctxt thsInit =
+    :: IntegerParameters -> ProofContext -> [Source] -> [Source]
+saturateSources parameters ctxt thsInit  =
     (go thsInit 1)
   where
     go :: [Source] -> Integer -> [Source]
     go ths n =
-        if (any or (changes `using` parList rdeepseq)) && (n <= 5)
-          then go ths' (n + 1)
-          else if (n > 5)
-            then trace "saturateSources: Saturation aborted, more than 5 iterations." ths'
-            else ths'
+        if (any or (changes `using` parList rdeepseq)) && (n <= get paramSaturationLimit parameters)
+          then trace("[Saturating Sources] Step " ++ show n ++ "/" ++ show (get paramSaturationLimit parameters)) $ go ths' (n + 1)
+          else if (n > get paramSaturationLimit parameters)
+            then trace ("[Saturating Sources] Saturation aborted, more than " ++ (show (get paramSaturationLimit parameters)) ++ " iterations. (Limit can be change with -s=)") ths'
+            else trace("[Saturating Sources] Step " ++ show n ++ "/" ++ show (get paramSaturationLimit parameters)) ths'
       where
         (changes, ths') = unzip $ map (refineSource ctxt solver) ths
         goodTh th  = length (getDisj (get cdCases th)) <= 1
-        solver     = do names <- solveAllSafeGoals (filter goodTh ths)
+        solver     = do names <- solveAllSafeGoals (filter goodTh ths) (get paramOpenChainsLimit parameters) 
                         return (not $ null names, names)
 
 -- | Precompute a saturated set of case distinctions.
 precomputeSources
-    :: ProofContext
+    :: IntegerParameters
+    -> ProofContext
     -> [LNGuarded]       -- ^ Restrictions.
     -> [Source]
-precomputeSources ctxt restrictions =
-    map cleanupCaseNames (saturateSources ctxt rawSources)
+precomputeSources parameters ctxt restrictions =
+    map cleanupCaseNames (saturateSources parameters ctxt rawSources)
   where
     cleanupCaseNames = modify cdCases $ fmap $ first $
         filter (not . null)
@@ -416,15 +435,16 @@ precomputeSources ctxt restrictions =
 -- | Refine a set of sources by exploiting additional source
 -- assumptions.
 refineWithSourceAsms
-    :: [LNGuarded]    -- ^ Source assumptions to use.
+    :: IntegerParameters -- ^ Parameters for openChains and Saturation limits
+    -> [LNGuarded]    -- ^ Source assumptions to use.
     -> ProofContext   -- ^ Proof context to use.
     -> [Source]       -- ^ Original, raw sources.
     -> [Source]       -- ^ Manipulated, refined sources.
-refineWithSourceAsms [] _ cases0 =
+refineWithSourceAsms _ [] _ cases0 =
     fmap ((modify cdCases . fmap . second) (set sSourceKind RefinedSource)) $ cases0
-refineWithSourceAsms assumptions ctxt cases0 =
+refineWithSourceAsms parameters assumptions ctxt cases0 =
     fmap (modifySystems removeFormulas) $
-    saturateSources ctxt $
+    saturateSources parameters ctxt $
     modifySystems updateSystem <$> cases0
   where
     modifySystems   = modify cdCases . fmap . second

lib/theory/src/Theory/Tools/Wellformedness.hs

@@ -75,7 +75,7 @@ import           Control.Category
 import           Data.Char
 import           Data.Generics.Uniplate.Data (universeBi)
 import           Data.Label
-import           Data.List                   (intersperse,(\\))
+import           Data.List                   (intersperse,(\\), intercalate, isPrefixOf)
 import           Data.Maybe
 -- import           Data.Monoid                 (mappend, mempty)
 import qualified Data.Set                    as S
@@ -90,6 +90,9 @@ import           Theory
 import           Theory.Text.Pretty
 import           Theory.Sapic
 import           Theory.Tools.RuleVariants
+import           Safe                        (lastMay)
+import           Items.OptionItem            (lemmasToProve)
+import           TheoryObject                (diffThyOptions)
 
 ------------------------------------------------------------------------------
 -- Types for error reports
@@ -954,6 +957,63 @@ multRestrictedReportDiff thy = do
 -- multicombine2 xs0 = do (x,xs) <- zip xs0 $ tails xs0; (,) x <$> xs
 
 
+--------------------
+-- Check if lemmas from "--prove" / "--lemma" args are in the theory
+--------------------
+
+-- | A fold to check if the lemmas are proper
+findNotProvedLemmas :: [String] -> [String] -> [String]
+findNotProvedLemmas lemmaArgsNames lemmasInTheory = foldl (\acc x -> if not (argFilter x) then  x:acc else acc ) [] lemmaArgsNames
+  where
+      -- Check a lemma against a prefix* pattern or the name of a lemma 
+      lemmaChecker :: String -> String -> Bool
+      lemmaChecker argLem lemFromThy
+        | lastMay argLem == Just '*' = init argLem `isPrefixOf` lemFromThy
+        | otherwise = argLem == lemFromThy
+
+      -- A filter to check if a lemma (str) is in the list of lemmas from the theory
+      argFilter :: String -> Bool
+      argFilter str = any (lemmaChecker str) lemmasInTheory
+
+
+-- | Check that all the lemmas in the arguments are lemmas of the theory and return an error if not
+  -----------------------
+checkIfLemmasInTheory :: Theory sig c r p s  -> WfErrorReport
+checkIfLemmasInTheory thy 
+        | null notProvedLemmas = []
+        | otherwise = 
+            [(topic, vcat
+            [ text $ "--> '" ++ intercalate "', '" notProvedLemmas ++ "'"  ++ " from arguments "
+              ++ "do(es) not correspond to a specified lemma in the theory "
+            -- , text $ "List of lemmas from the theory: " ++ show (map _lName (theoryLemmas thy))
+            ])]
+
+    where
+      lemmaArgsNames = get (lemmasToProve.thyOptions) thy
+      topic = "Check presence of the --prove/--lemma arguments in theory"
+      lemmasInTheory = map _lName (theoryLemmas thy)
+      notProvedLemmas = findNotProvedLemmas lemmaArgsNames lemmasInTheory
+
+
+-- | Check that all the lemmas in the arguments are lemmas of the diffTheory and return an error if not
+  -----------------------
+checkIfLemmasInDiffTheory :: DiffTheory sig c r r2 p p2  -> WfErrorReport
+checkIfLemmasInDiffTheory thy 
+        | null notProvedLemmas = []
+        | otherwise = 
+            [(topic, vcat
+            [ text $ "--> '" ++ intercalate "', '"  notProvedLemmas ++ "'"  ++ " from arguments "
+              ++ "do(es) not correspond to a specified lemma in the theory "
+            -- , text $ "List of lemmas from the theory: " ++ show (map _lName (theoryLemmas thy))
+            ])]
+
+    where
+      lemmaArgsNames = get (lemmasToProve.diffThyOptions) thy
+      topic = "Check presence of the --prove/--lemma arguments in theory"
+      lemmasInTheory = map (_lName.snd) (diffTheoryLemmas thy)
+      notProvedLemmas = findNotProvedLemmas lemmaArgsNames lemmasInTheory
+
+
 ------------------------------------------------------------------------------
 -- Theory
 ------------------------------------------------------------------------------
@@ -963,7 +1023,8 @@ checkWellformednessDiff :: OpenDiffTheory -> SignatureWithMaude
                     -> WfErrorReport
 checkWellformednessDiff thy sig = -- trace ("checkWellformednessDiff: " ++ show thy) $
   concatMap ($ thy)
-    [ unboundReportDiff
+    [ checkIfLemmasInDiffTheory
+    , unboundReportDiff
     , freshNamesReportDiff
     , publicNamesReportDiff
     , ruleSortsReportDiff
@@ -981,7 +1042,8 @@ checkWellformednessDiff thy sig = -- trace ("checkWellformednessDiff: " ++ show
 checkWellformedness :: OpenTranslatedTheory -> SignatureWithMaude
                     -> WfErrorReport
 checkWellformedness thy sig = concatMap ($ thy)
-    [ unboundReport
+    [ checkIfLemmasInTheory
+    , unboundReport
     , freshNamesReport
     , publicNamesReport
     , ruleSortsReport
@@ -990,4 +1052,5 @@ checkWellformedness thy sig = concatMap ($ thy)
     , formulaReports
     , lemmaAttributeReport
     , multRestrictedReport
-    ]
+    ]
+