copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594.

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)

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

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

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
 

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
 

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
@@ -51,11 +53,12 @@ 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
-  , 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.

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

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)
@@ -139,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