From 007e80aabd893a3fa2b57c17f58f6530b00530bf Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 21 Feb 2025 16:22:12 -0500 Subject: [PATCH 1/3] copilot-theorem: Add Props to specProps. Refs #594. `copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove that it is valid at all possible time steps. Currently, this happens regardless of whether the proposition is universally or existentially quantified. This is unsound, and it can lead to valid, existentially quantified properties being incorrectly labeled as invalid. This commit adds information about propositions' quantifiers to the Kind2 backend's implementation so that it may use the quantifiers when translating the properties to Kind2. This is accomplished by updating `specProps` to map each proposition's identifier to its corresponding `copilot-core` `Prop`. --- copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs | 4 ++-- .../src/Copilot/Theorem/TransSys/PrettyPrint.hs | 3 ++- copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs | 4 +++- copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs | 3 ++- copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs | 8 +++++--- 5 files changed, 14 insertions(+), 8 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index d8115e893..123f6ed64 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -65,7 +65,7 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props 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 @@ addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = 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 diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs index 89fdc5787..3debe552c 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs @@ -27,7 +27,8 @@ pSpec spec = items $$ props 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 diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs index d2a953387..e0a297535 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs @@ -24,6 +24,8 @@ module Copilot.Theorem.TransSys.Spec , specDependenciesGraph , specTopNode ) where +import qualified Copilot.Core as C + import Copilot.Theorem.TransSys.Type import Copilot.Theorem.TransSys.Operators import Copilot.Theorem.TransSys.Invariants @@ -55,7 +57,7 @@ type PropId = String 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. diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs index 79edd2828..e59058496 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs @@ -42,7 +42,8 @@ mergeNodes toMergeIds spec = 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 diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs index 68ddb8806..f15162e49 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs @@ -96,10 +96,12 @@ translate cspec = 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) From a007efad3207b6603e46da408ebbd3d60e61018b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 24 Feb 2025 05:41:21 -0500 Subject: [PATCH 2/3] copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove that it is valid at all possible time steps. Currently, this happens regardless of whether the proposition is universally or existentially quantified. This is unsound, and it can lead to valid, existentially quantified properties being incorrectly labeled as invalid. This commit fixes the translations of propositions to Kind2 (via Kind2's TransSys backend) such that the translated properties respect quantifier information. Specifically, this replaces an unsound use of the `extractProp` function with an analysis that translates the property differently depending on whether it is universally or existentially quantified. Because all TransSys propositions use universal quantification, we convert an existentially quantified property `∃x.P(x)` as `¬(∀x.¬(P(x)))` during the translation to TransSys. --- .../src/Copilot/Theorem/Kind2/Output.hs | 29 +++++++++++++++---- .../src/Copilot/Theorem/Kind2/Prover.hs | 18 +++++++++--- .../src/Copilot/Theorem/TransSys/Spec.hs | 3 +- .../src/Copilot/Theorem/TransSys/Translate.hs | 10 ++++++- 4 files changed, 49 insertions(+), 11 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index 42a2f60dc..f80b8170b 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -8,19 +8,38 @@ import Text.XML.Light hiding (findChild) 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 @@ parseOutput prop xml = fromJust $ do 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 diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 3931c615b..66db2c346 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -19,10 +19,12 @@ import Copilot.Theorem.Misc.Utils (openTempFile) 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 @@ askKind2 (ProverST opts spec) assumptions toCheck = do 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 diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs index e0a297535..b68181ae0 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs @@ -53,7 +53,8 @@ type NodeId = String 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 diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs index f15162e49..2659fa6cb 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs @@ -141,7 +141,15 @@ streamOfProp :: C.Property -> C.Stream 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 From 3b51c969d863755431cb628de80bc02e0c243a8d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 7 Mar 2025 07:08:02 -0500 Subject: [PATCH 3/3] copilot-theorem: Document changes in CHANGELOG. Refs #594. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index d3c2bd464..8416d3a75 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2025-04-17 + * Translate quantifiers correctly in Kind2 backend. (#594) + 2025-03-07 * Version bump (4.3). (#604) * Fix multiple typos in README. (#560)