Merge pull request tamarin-prover#457 from Hong-Thai/Split-Theory

Split Theory.hs

lib/theory/src/Items/LemmaItem.hs

@@ -0,0 +1,109 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module Items.LemmaItem (
+    module Items.LemmaItem
+) where
+
+import GHC.Generics (Generic)
+import Control.DeepSeq (NFData)
+import Data.Binary (Binary)
+import Theory.Constraint.Solver (GoalRanking)
+import Theory.Model
+import Data.Label as L
+
+------------------------------------------------------------------------------
+-- Lemmas
+------------------------------------------------------------------------------
+
+-- | An attribute for a 'Lemma'.
+data LemmaAttribute =
+         SourceLemma
+       | ReuseLemma
+       | ReuseDiffLemma
+       | InvariantLemma
+       | HideLemma String
+       | LHSLemma
+       | RHSLemma
+       | LemmaHeuristic [GoalRanking]
+--        | BothLemma
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+-- | A 'TraceQuantifier' stating whether we check satisfiability of validity.
+data TraceQuantifier = ExistsTrace | AllTraces
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+-- | A lemma describes a property that holds in the context of a theory
+-- together with a proof of its correctness.
+data ProtoLemma f p = Lemma
+       { _lName            :: String
+       , _lTraceQuantifier :: TraceQuantifier
+       , _lFormula         :: f
+       , _lAttributes      :: [LemmaAttribute]
+       , _lProof           :: p
+       }
+       deriving( Generic)
+$(mkLabels [''ProtoLemma])
+
+type Lemma = ProtoLemma LNFormula
+type SyntacticLemma = ProtoLemma SyntacticLNFormula
+
+deriving instance Eq p => Eq (Lemma p)
+deriving instance Ord p => Ord (Lemma p)
+deriving instance Show p => Show (Lemma p)
+deriving instance NFData p => NFData (Lemma p)
+deriving instance Binary p => Binary  (Lemma p)
+
+
+
+-- | A diff lemma describes a correspondence property that holds in the context of a theory
+-- together with a proof of its correctness.
+data DiffLemma p = DiffLemma
+       { _lDiffName            :: String
+--        , _lTraceQuantifier :: TraceQuantifier
+--        , _lFormula         :: LNFormula
+       , _lDiffAttributes      :: [LemmaAttribute]
+       , _lDiffProof           :: p
+       }
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+$(mkLabels [''DiffLemma])
+
+
+
+-- | An accountability Lemma describes a property that holds in the context
+-- of a theory and some parties with a verdict function
+--data AccLemma v p par = AccLemma
+--       { _acName            :: String
+--       , _acTraceQuantifier :: TraceQuantifier
+--       , _acFormula         :: LNFormula
+--       , _acAttributes      :: [LemmaAttribute]
+--       , _acVerdict         :: v
+--       , _acProof           :: p
+--       , _acParties         :: par
+--       }
+--       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+
+-- Instances
+------------
+
+instance Functor Lemma where
+    fmap f (Lemma n qua fm atts prf) = Lemma n qua fm atts (f prf)
+
+instance Foldable Lemma where
+    foldMap f = f . L.get lProof
+
+instance Traversable Lemma where
+    traverse f (Lemma n qua fm atts prf) = Lemma n qua fm atts <$> f prf
+
+instance Functor DiffLemma where
+    fmap f (DiffLemma n atts prf) = DiffLemma n atts (f prf)
+
+instance Foldable DiffLemma where
+    foldMap f = f . L.get lDiffProof
+
+instance Traversable DiffLemma where
+    traverse f (DiffLemma n atts prf) = DiffLemma n atts <$> f prf

lib/theory/src/Items/OpenTheoryItem.hs

@@ -0,0 +1,32 @@
+module Items.OpenTheoryItem (
+    module Items.OpenTheoryItem
+) where
+
+import Rule
+import Theory.ProofSkeleton
+import Theory.Model
+import TheoryObject
+import Prelude hiding (id, (.))
+
+-- | Open theories can be extended. Invariants:
+--   1. Lemma names are unique.
+type OpenTheory =
+    Theory SignaturePure [IntrRuleAC] OpenProtoRule ProofSkeleton SapicElement
+
+type OpenTheoryItem = TheoryItem OpenProtoRule ProofSkeleton SapicElement
+
+-- | Open theories can be extended. Invariants:
+--   1. Lemma names are unique.
+--   2. All SapicItems are translated
+type OpenTranslatedTheory =
+    Theory SignaturePure [IntrRuleAC] OpenProtoRule ProofSkeleton ()
+
+-- | Open diff theories can be extended. Invariants:
+--   1. Lemma names are unique.
+type OpenDiffTheory =
+    DiffTheory SignaturePure [IntrRuleAC] DiffProtoRule OpenProtoRule DiffProofSkeleton ProofSkeleton
+
+-- | Either Therories can be Either a normal or a diff theory
+
+-- type EitherTheory = Either Theory  DiffTheory
+type EitherOpenTheory = Either OpenTheory OpenDiffTheory

lib/theory/src/Items/OptionItem.hs

@@ -0,0 +1,29 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
+
+module Items.OptionItem (
+    Option(..)
+    ,module Items.OptionItem
+) where
+import GHC.Generics (Generic)
+import Control.DeepSeq (NFData)
+import Data.Binary (Binary)
+import Data.Label as L
+
+------------------------------------------------------------------------------
+-- Options
+------------------------------------------------------------------------------
+-- | Options for translation and, maybe in the future, also msrs itself.
+-- | Note: setOption below assumes all values to be boolean
+data Option = Option
+        {
+          _transAllowPatternMatchinginLookup   :: Bool
+        , _transProgress            :: Bool
+        , _transReliable            :: Bool
+        , _transReport            :: Bool
+        }
+        deriving( Eq, Ord, Show, Generic, NFData, Binary )
+$(mkLabels [''Option])
+-- generate accessors for Option data structure records
+

lib/theory/src/Items/PredicateItem.hs

@@ -0,0 +1,32 @@
+
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+module Items.PredicateItem (
+    module Items.PredicateItem
+) where
+
+import Control.DeepSeq
+import Data.Binary (Binary)
+import Data.Label as L
+import GHC.Generics
+import Term.LTerm
+import Theory.Model
+import Prelude hiding (id, (.))
+
+
+------------------------------------------------------------------------------
+-- Predicates
+------------------------------------------------------------------------------
+
+data Predicate = Predicate
+        { _pFact            :: Fact LVar
+        , _pFormula         :: LNFormula
+        }
+        deriving( Eq, Ord, Show, Generic, NFData, Binary )
+$(mkLabels [''Predicate])
+
+-- generate accessors for Predicate data structure records

lib/theory/src/Items/ProcessItem.hs

@@ -0,0 +1,31 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+module Items.ProcessItem (
+    module Items.ProcessItem
+) where
+
+import Theory.Sapic
+import GHC.Generics
+import Data.Binary (Binary)
+import Data.Label as L
+import           Control.DeepSeq
+
+import           Prelude                             hiding (id, (.))
+
+------------------------------------------------------------------------------
+-- Processes
+------------------------------------------------------------------------------
+
+data ProcessDef = ProcessDef
+        { _pName            :: String
+        , _pBody            :: Process
+        }
+        deriving( Eq, Ord, Show, Generic, NFData, Binary )
+$(mkLabels [''ProcessDef])
+
+-- generate accessors for ProcessDef data structure records

lib/theory/src/Items/RuleItem.hs

@@ -0,0 +1,80 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
+
+module Items.RuleItem (
+    module Items.RuleItem
+) where
+
+import GHC.Generics
+import Control.DeepSeq
+import Data.Binary
+
+import           Prelude                             hiding (id, (.))
+
+
+import qualified Data.Set                            as S
+
+import           Control.Category
+import           Extension.Data.Label                hiding (get)
+import qualified Extension.Data.Label                as L
+
+import           Theory.Model
+import           Theory.Proof
+
+------------------------------------------------------------------------------
+-- Commented sets of rewriting rules
+------------------------------------------------------------------------------
+
+-- | A protocol rewriting rule modulo E together with its possible assertion
+-- soundness proof.
+-- Optionally, the variant(s) modulo AC can be present if they were loaded
+-- or contain additional actions.
+data OpenProtoRule = OpenProtoRule
+       { _oprRuleE  :: ProtoRuleE             -- original rule modulo E
+       , _oprRuleAC :: [ProtoRuleAC]          -- variant(s) modulo AC
+       }
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+-- | A diff protocol rewriting rule modulo E
+-- Optionally, the left and right rules can be present if they were loaded
+-- or contain additional actions.
+data DiffProtoRule = DiffProtoRule
+       { _dprRule       :: ProtoRuleE         -- original rule with diff
+       , _dprLeftRight  :: Maybe (OpenProtoRule, OpenProtoRule)
+                                              -- left and right instances
+       }
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+-- | A closed proto rule lists its original rule modulo E, the corresponding
+-- variant(s) modulo AC, and if required the assertion soundness proof.
+-- When using auto-sources, all non-trivial variants of a ClosedProtoRule are
+-- split up into multiple ClosedProtoRules. Auto-sources also only adds
+-- actions only to closed rules. Opening such rules keeps the AC rules s.t.
+-- they can be exported.
+data ClosedProtoRule = ClosedProtoRule
+       { _cprRuleE         :: ProtoRuleE      -- original rule modulo E
+       , _cprRuleAC        :: ProtoRuleAC     -- variant(s) modulo AC
+       }
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+type OpenRuleCache = [IntrRuleAC]
+
+data ClosedRuleCache = ClosedRuleCache
+       { _crcRules               :: ClassifiedRules
+       , _crcRawSources          :: [Source]
+       , _crcRefinedSources      :: [Source]
+       , _crcInjectiveFactInsts  :: S.Set FactTag
+       }
+       deriving( Eq, Ord, Show, Generic, NFData, Binary )
+
+$(mkLabels [''OpenProtoRule, ''DiffProtoRule, ''ClosedProtoRule, ''ClosedRuleCache])
+
+instance HasRuleName OpenProtoRule where
+    ruleName = ruleName . L.get oprRuleE
+
+instance HasRuleName DiffProtoRule where
+    ruleName = ruleName . L.get dprRule
+
+instance HasRuleName ClosedProtoRule where
+    ruleName = ruleName . L.get cprRuleAC

lib/theory/src/Items/TheoryItem.hs

@@ -0,0 +1,66 @@
+
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module Items.TheoryItem (
+    module Items.TheoryItem
+) where 
+
+import Theory.Sapic
+import GHC.Generics
+import Data.Binary (Binary)
+import Theory.Model.Restriction
+import Theory.Constraint.Solver
+
+import Items.ProcessItem
+import Items.PredicateItem
+import Lemma
+import           Prelude                             hiding (id, (.))
+import           Control.DeepSeq
+import           Prelude                             hiding (id, (.))
+
+------------------------------------------------------------------------------
+-- Theories
+------------------------------------------------------------------------------
+
+-- | A formal comment is a header together with the body of the comment.
+
+type FormalComment = (String, String)
+
+-- | SapicItems can be processes and accountability lemmas
+data SapicElement=
+      ProcessItem Process
+      | ProcessDefItem ProcessDef
+      deriving( Show, Eq, Ord, Generic, NFData, Binary )
+
+-- | A theory item built over the given rule type.
+data TheoryItem r p s =
+       RuleItem r
+     | LemmaItem (Lemma p)
+     | RestrictionItem Restriction
+     | TextItem FormalComment
+     | PredicateItem Predicate
+     | SapicItem s
+     deriving( Show, Eq, Ord, Functor, Generic, NFData, Binary )
+
+-- | A diff theory item built over the given rule type.
+--   This includes
+--   - Diff Rules, which are then decomposed in either rules for both sides
+--   - the Diff Lemmas, stating observational equivalence
+--   - the either lemmas and restrictions, stating properties about either side
+--   - and comments
+data DiffTheoryItem r r2 p p2 =
+       DiffRuleItem r
+     | EitherRuleItem (Side, r2)
+     | DiffLemmaItem (DiffLemma p)
+     | EitherLemmaItem (Side, Lemma p2)
+     | EitherRestrictionItem (Side, Restriction)
+     | DiffTextItem FormalComment
+     deriving( Show, Eq, Ord, Functor, Generic, NFData, Binary )
+
+
+