copilot-theorem 4.3 → 4.4

raw patch · 9 files changed

+70/−22 lines, 9 filesdep ~copilot-coredep ~copilot-prettyprinterPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core, copilot-prettyprinter

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• copilot-theorem.cabal +3/−3
• src/Copilot/Theorem/Kind2/Output.hs +24/−5
• src/Copilot/Theorem/Kind2/Prover.hs +14/−4
• src/Copilot/Theorem/Kind2/Translate.hs +2/−2
• src/Copilot/Theorem/TransSys/PrettyPrint.hs +2/−1
• src/Copilot/Theorem/TransSys/Spec.hs +5/−2
• src/Copilot/Theorem/TransSys/Transform.hs +2/−1
• src/Copilot/Theorem/TransSys/Translate.hs +14/−4

@@ -1,3 +1,7 @@+2025-05-07+        * Version bump (4.4). (#618)+        * Translate quantifiers correctly in Kind2 backend. (#594)+ 2025-03-07         * Version bump (4.3). (#604)         * Fix multiple typos in README. (#560)

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 4.3+version                   : 4.4 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -63,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.7 -                          , copilot-core          >= 4.3 && < 4.4-                          , copilot-prettyprinter >= 4.3 && < 4.4+                          , copilot-core          >= 4.4 && < 4.5+                          , copilot-prettyprinter >= 4.4 && < 4.5    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

@@ -8,19 +8,38 @@ import Copilot.Theorem.Prove  as P import Data.Maybe           (fromJust) +import qualified Copilot.Core as C+ import qualified Copilot.Theorem.Misc.Error as Err  simpleName s = QName s Nothing Nothing  -- | Parse output of Kind2. parseOutput :: String    -- ^ Property whose validity is being checked.+            -> C.Prop    -- ^ The property's quantifier.             -> String    -- ^ XML output of Kind2             -> P.Output-parseOutput prop xml = fromJust $ do+parseOutput propId propQuantifier xml = fromJust $ do   root <- parseXMLDoc xml   case findAnswer . findPropTag $ root of-    "valid"       -> return (Output Valid   [])-    "falsifiable" -> return (Output Invalid [])+    "valid"       -> case propQuantifier of+                       -- We encode a universally quantified property P as+                       -- ∀x.P(x) in Kind2, so the original property is valid+                       -- iff the Kind2 property is valid.+                       C.Forall {} -> return (Output Valid   [])+                       -- We encode an existentially quantified property P as+                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is+                       -- invalid iff the Kind2 property is valid.+                       C.Exists {} -> return (Output Invalid [])+    "falsifiable" -> case propQuantifier of+                       -- We encode a universally quantified property P as+                       -- ∀x.P(x) in Kind2, so the original property is invalid+                       -- iff the Kind2 property is invalid.+                       C.Forall {} -> return (Output Invalid [])+                       -- We encode an existentially quantified property P as+                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is+                       -- valid iff the Kind2 property is invalid.+                       C.Exists {} -> return (Output Valid   [])     s             -> err $ "Unrecognized status : " ++ s    where@@ -31,10 +50,10 @@       let rightElement elt =             qName (elName elt) == "Property"             && lookupAttr (simpleName "name") (elAttribs elt)-                == Just prop+                == Just propId       in case filterChildren rightElement root of            tag : _ -> tag-           _ -> err $ "Tag for property " ++ prop ++ " not found"+           _ -> err $ "Tag for property " ++ propId ++ " not found"      findAnswer tag =       case findChildren (simpleName "Answer") tag of

@@ -19,10 +19,12 @@  import System.Process -import System.Directory-import Data.Default+import           System.Directory+import           Data.Default+import qualified Data.Map         as Map -import qualified Copilot.Theorem.TransSys as TS+import qualified Copilot.Theorem.Misc.Error as Err+import qualified Copilot.Theorem.TransSys   as TS  -- | Options for Kind2 data Options = Options@@ -68,4 +70,12 @@   putStrLn kind2Input    removeFile tempName-  return $ parseOutput (head toCheck) output++  let propId         = head toCheck+      propQuantifier = case Map.lookup propId (TS.specProps spec) of+                         Just (_, quantifier) ->+                           quantifier+                         Nothing ->+                           Err.impossible $+                             "askKind2: " ++ propId ++ " not in specProps"+  return $ parseOutput propId propQuantifier output

@@ -65,7 +65,7 @@     preds = map (trNode spec predCallsGraph) (specNodes spec)     props = map trProp $       filter ((`elem` checkedProps) . fst) $-      Map.toList (specProps spec)+        Map.toList $ Map.map fst $ specProps spec  trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var)@@ -98,7 +98,7 @@      vars =       let bindings   = nodeImportedVars (specTopNode spec)-          toExtVar a = fromJust $ Map.lookup a (specProps spec)+          toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec           toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v       in map (varName . toTopVar . toExtVar) assumptions 

@@ -27,7 +27,8 @@     items = foldr (($$) . pNode) empty (specNodes spec)     props = text "PROPS" $$       Map.foldrWithKey (\k -> ($$) . pProp k)-        empty (specProps spec)+        empty+        (Map.map fst (specProps spec))  pProp pId extvar = quotes (text pId) <+> text "is" <+> pExtVar extvar 

@@ -24,6 +24,8 @@   , specDependenciesGraph   , specTopNode ) where +import qualified Copilot.Core as C+ import Copilot.Theorem.TransSys.Type import Copilot.Theorem.TransSys.Operators import Copilot.Theorem.TransSys.Invariants@@ -51,11 +53,12 @@ type PropId = String  -- | A modular transition system is defined by a graph of nodes and a series--- of properties, each mapped to a variable.+-- of properties, each mapped to a variable and a 'C.Prop' describing how the+-- property is quantified. data TransSys = TransSys   { specNodes         :: [Node]   , specTopNodeId     :: NodeId-  , specProps         :: Map PropId ExtVar }+  , specProps         :: Map PropId (ExtVar, C.Prop) }  -- | A node is a set of variables living in a local namespace and corresponding -- to the 'Var' type.

@@ -42,7 +42,8 @@   spec     { specNodes = newNode :         map (updateOtherNode newNodeId toMergeIds renamingExtF) otherNodes-    , specProps = Map.map renamingExtF (specProps spec) }+    , specProps =+        Map.map (\(ev, prop) -> (renamingExtF ev, prop)) (specProps spec) }    where     nodes = specNodes spec

@@ -96,10 +96,12 @@     cprops :: [C.Property]     cprops = C.specProperties cspec -    propBindings :: Map PropId ExtVar+    propBindings :: Map PropId (ExtVar, C.Prop)     propBindings = Map.fromList $ do-      pid <- map C.propertyName cprops-      return (pid, mkExtVar topNodeId pid)+      cprop <- cprops+      let pid  = C.propertyName cprop+          prop = C.propertyProp cprop+      return (pid, (mkExtVar topNodeId pid, prop))      ((modelNodes, propNodes), extvarNodesNames) = runTrans $       liftM2 (,) (mapM stream (C.specStreams cspec)) (mkPropNodes cprops)@@ -139,7 +141,15 @@ streamOfProp prop =   C.Stream { C.streamId = 42            , C.streamBuffer = []-           , C.streamExpr = C.extractProp (C.propertyProp prop)+             -- TransSys encodes all properties using universal quantification.+             -- Therefore, in order to encode an existentially quantified+             -- property ∃x.P(x), we must first convert it to ¬(∀x.¬(P(x))).+             -- The `Exists` case below handles the ∀x.¬(P(x)) part by adding+             -- an `Op1 Not` around the property. The outermost negation is+             -- handled elsewhere (e.g., in Copilot.Theorem.Kind2.Output.parse).+           , C.streamExpr = case C.propertyProp prop of+                              C.Forall p -> p+                              C.Exists p -> C.Op1 C.Not p            , C.streamExprType = C.Bool }  stream :: C.Stream -> Trans Node