copilot-theorem: Extend range of versions of kind2. Refs #734.

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2026-06-09
+        * Update Kind2 backend to support Kind2 1.0 and newer. (#734)
+
 2026-05-07
         * Version bump (4.7.1). (#730)
         * Handle special Float values correctly for counterexamples. (#697)

copilot-theorem/README.md

@@ -31,7 +31,8 @@ properties on Copilot programs. It includes:
 * The *copilot-core* and *copilot-prettyprinter* Haskell libraries
 * The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH`
 * The *Z3* SMT-solver: `z3` must be in your `$PATH`
-* The *Kind2* model checker: `kind2` must be in your `$PATH`
+* The *Kind2* model checker (version 1.0 or newer): `kind2` must be in your
+  `$PATH`
 
 To build it, just install the Copilot library as described in the top-level
 README.
@@ -87,15 +88,17 @@ configuration.
 The *Kind2* prover uses the model checker with the same name, from the
 University of Iowa. It translates the Copilot specification into a *modular
 transition system* (the Kind2 native format) and then calls the `kind2`
-executable.
+executable. Kind2 version 1.0 or newer is required: the native input format
+and the command-line options used by this prover were introduced in Kind2
+1.0, and remain supported as of Kind2 3.0.
 
 It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover
 :: Options -> Prover` where the `Options` type is defined as
 
 ```haskell
 data Options = Options { bmcMax :: Int }
 ```
-and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is
+and where `bmcMax` corresponds to the `--unroll_max` option of *kind2* and is
 equivalent to the `maxK` option of the K-Induction prover. Its default value is
 0, which stands for infinity.
 
@@ -335,11 +338,16 @@ process.
 
 The transition system obtained by the `TransSys.Translate` module is perfectly
 consistent. However, it can't be directly translated into the *Kind2 native
-file format*. Indeed, it is natural to bind each node to a predicate but the
-Kind2 file format requires that each predicate only uses previously defined
-predicates. However, some nodes in our transition system could be mutually
-recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function,
-defined in `TransSys.Transform`, is to remove such dependency cycles.
+file format*. The native input format of Kind2 (version 1.0 and newer) does
+not support predicate calls inside the initial state and transition relation
+predicates of a node, so the modular structure of the transition system cannot
+be expressed directly in it. Therefore, the system is first turned into an
+equivalent non-modular transition system with only one node by the
+`inline :: Spec -> Spec` function, defined in `TransSys.Transform`:
+```haskell
+inline :: Spec -> Spec
+inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec
+```
 
 This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function,
 whose signature is self-explicit. The latter solves name conflicts by using the
@@ -516,10 +524,14 @@ in the Kind2 SMT solver.
 #### Displaying counterexamples
 
 Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't
-support XML output of counterexamples. If the last feature is provided, it
-should be easy to implement displaying of counterexamples in *copilot-theorem*.
-For this, we recommend keeping some information about *observers* in
-`TransSys.Spec` and to add one variable per observer in the Kind2 output file.
+support the output of counterexamples for systems expressed in its native input
+format (the counterexample printing functions in Kind2's
+[`src/inputSystem.ml`](https://github.com/kind2-mc/kind2/blob/v3.0.0/src/inputSystem.ml)
+fail with an internal error for native input). If Kind2 adds this feature, it
+should be easy to implement displaying of counterexamples in
+*copilot-theorem*.  For this, we recommend keeping some information about
+*observers* in `TransSys.Spec` and to add one variable per observer in the
+Kind2 output file.
 
 #### Bad handling of non-linear operators and external functions
 
@@ -569,14 +581,14 @@ architecture of Kind2.
 
 It is true that the code of `TransSys` is quite complex. In fact, it would be
 really straightforward to produce a flattened transition system and then a
-Kind2 file with just a single *top* predicate. In fact, It would be as easy as
+Kind2 file with just a single *top* node. In fact, It would be as easy as
 producing an *IL* specification.
 
 To be honest, I'm not sure producing a modular *Kind2* output is worth the
 complexity added. It's especially true at the time I write this in the sense
 that:
 
-* Each predicate introduced is used only one time (which is true because
+* Each node introduced is used only one time (which is true because
   Copilot doesn't handle functions or parameterized streams like Lustre does
   and everything is inlined during the reification process).
 * A similar form of structure could be obtained from a flattened Kind2 native

copilot-theorem/copilot-theorem.cabal

@@ -35,6 +35,11 @@ source-repository head
     location:   https://github.com/Copilot-Language/copilot.git
     subdir:     copilot-theorem
 
+flag test-kind2
+    description: Enable tests that require the Kind2 model checker (kind2)
+    default: False
+    manual: True
+
 library
   default-language        : Haskell2010
   hs-source-dirs          : src
@@ -51,6 +56,7 @@ library
                           , containers            >= 0.4 && < 0.9
                           , data-default          >= 0.7 && < 0.9
                           , directory             >= 1.3 && < 1.4
+                          , extra                 >= 1.7 && < 1.9
                           , fp-ieee               >= 0.1 && < 0.2
                           , libBF                 >= 0.6.2 && < 0.7
                           , mtl                   >= 2.0 && < 2.4
@@ -60,7 +66,6 @@ library
                           , process               >= 1.6 && < 1.7
                           , random                >= 1.1 && < 1.4
                           , transformers          >= 0.5 && < 0.7
-                          , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.8
 
                           , copilot-core          >= 4.7.1 && < 4.8
@@ -137,3 +142,40 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+
+-- Tests of the Kind2 backend, which require the kind2 executable (version
+-- 1.0 or newer) to be in the PATH. They must be explicitly enabled with the
+-- flag test-kind2.
+test-suite kind2-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Kind2Main.hs
+
+  other-modules:
+    Test.Copilot.Theorem.Kind2
+
+  build-depends:
+      base
+    , HUnit
+    , mtl
+    , test-framework
+    , test-framework-hunit
+
+    , copilot-core
+    , copilot-theorem
+
+  hs-source-dirs:
+    tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
+
+  if flag(test-kind2)
+    buildable: True
+  else
+    buildable: False

copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs

@@ -1,27 +1,53 @@
 {-# LANGUAGE Safe #-}
 
--- | Abstract syntax tree of Kind2 files.
+-- | Abstract syntax tree of Kind2 native input files.
+--
+-- This represents the native transition system input format supported by
+-- Kind2 1.0 and newer (@--input_format native@), in which a file is a
+-- sequence of @define-node@ forms, each declaring a state transition system
+-- by means of an initial state predicate and a transition relation predicate.
+-- The last node defined in a file is the top system analyzed by Kind2, and
+-- the properties to check are attached to it.
+--
+-- The native input format is largely undocumented, and Kind2's user
+-- documentation only covers its Lustre frontend. The best available
+-- references for the native format are the parser in the Kind2 sources
+-- (<https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml nativeInput.ml>,
+-- which includes a sketch of the grammar in a comment near the end of the
+-- file) and the example file
+-- <https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.kind2 two_counters.kind2>
+-- distributed with Kind2.
 module Copilot.Theorem.Kind2.AST where
 
--- | A file is a sequence of predicates and propositions.
+-- | A file is a sequence of node definitions, together with a distinguished
+-- top node and a series of propositions about the top node.
+--
+-- Kind2 analyzes the last node defined in a file as the top system, so the
+-- top node is always printed after all the other nodes.
 data File = File
-  { filePreds     :: [PredDef]
-  , fileProps     :: [Prop] }
+  { fileNodes   :: [Node]  -- ^ Nodes other than the top node, in dependency
+                           --   order (a node may only refer to nodes defined
+                           --   before it).
+  , fileTopNode :: Node    -- ^ The top node, which the propositions are
+                           --   attached to.
+  , fileProps   :: [Prop]  -- ^ Propositions about the top node.
+  }
 
 -- | A proposition is defined by a term.
 data Prop = Prop
   { propName      :: String
   , propTerm      :: Term }
 
--- | A predicate definition.
-data PredDef = PredDef
-  { predId        :: String         -- ^ Identifier for the predicate.
-  , predStateVars :: [StateVarDef]  -- ^ Variables identifying the states in the
-                                    -- underlying state transition system.
-  , predInit      :: Term           -- ^ Predicate that holds for initial
+-- | A node definition.
+data Node = Node
+  { nodeId        :: String         -- ^ Identifier for the node.
+  , nodeStateVars :: [StateVarDef]  -- ^ Variables identifying the states in
+                                    -- the underlying state transition system.
+  , nodeInit      :: Term           -- ^ Predicate that holds for initial
                                     -- states.
-  , predTrans     :: Term           -- ^ Predicate that holds for two states, if
-                                    -- there is state transition between them.
+  , nodeTrans     :: Term           -- ^ Predicate that holds for two states,
+                                    -- if there is a state transition between
+                                    -- them.
   }
 
 -- | A definition of a state variable.

copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs

@@ -4,66 +4,97 @@
 -- | Parse output of Kind2.
 module Copilot.Theorem.Kind2.Output (parseOutput) where
 
-import Text.XML.Light       hiding (findChild)
-import Copilot.Theorem.Prove  as P
-import Data.Maybe           (fromJust)
+import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim)
+import Data.Maybe      (mapMaybe)
+
+import Copilot.Theorem.Prove as P
 
 import qualified Copilot.Core as C
 
 import qualified Copilot.Theorem.Misc.Error as Err
 
-simpleName s = QName s Nothing Nothing
-
 -- | Parse output of Kind2.
+--
+-- The output is expected to be in XML format, as produced by Kind2's @-xml@
+-- flag and documented at
+-- <https://kind.cs.uiowa.edu/kind2_user_doc/3_output/2_machine_readable.html>.
+-- Note that this function does not parse the output as XML: when given a
+-- system in the native transition system format, Kind2 produces output that
+-- is not always well-formed XML (e.g., counterexamples to invariant
+-- properties cannot be printed for systems in that format -- the
+-- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with
+-- an internal error for native input -- and Kind2 reports the error in the
+-- middle of the XML output). Instead, this function looks for the
+-- @\<Property\>@ tag for the given property and extracts the answers in the
+-- @\<Answer\>@ tags it contains.
 parseOutput :: String    -- ^ Property whose validity is being checked.
             -> C.Prop    -- ^ The property's quantifier.
             -> String    -- ^ XML output of Kind2
             -> P.Output
-parseOutput propId propQuantifier xml = fromJust $ do
-  root <- parseXMLDoc xml
-  case findAnswer . findPropTag $ root of
-    "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
+parseOutput propId propQuantifier xml
+    | "valid"       `elem` answers = quantified (Output Valid   [])
+                                                (Output Invalid [])
+    | "falsifiable" `elem` answers = quantified (Output Invalid [])
+                                                (Output Valid   [])
+    | "unknown"     `elem` answers = Output Unknown []
+    | null answers = err $ "Answer for property " ++ propId ++ " not found"
+    | otherwise    = err $ "Unrecognized status : " ++ unwords answers
 
   where
 
-    searchForRuntimeError = undefined
+    -- Pick an output based on the quantifier of the property. The first
+    -- argument is returned when the property Kind2 was asked about is valid,
+    -- and the second one when it is invalid.
+    --
+    -- 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.
+    --
+    -- 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.
+    quantified ifValid ifInvalid = case propQuantifier of
+      C.Forall {} -> ifValid
+      C.Exists {} -> ifInvalid
+
+    -- All the answers reported for the property, in the order in which they
+    -- appear in the output. A conclusive answer (valid or falsifiable), if
+    -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may
+    -- also report when the analysis terminates without an answer for all
+    -- properties.
+    answers = mapMaybe answerText
+            $ filter isRightProperty
+            $ propertyElems xml
 
-    findPropTag root =
-      let rightElement elt =
-            qName (elName elt) == "Property"
-            && lookupAttr (simpleName "name") (elAttribs elt)
-                == Just propId
-      in case filterChildren rightElement root of
-           tag : _ -> tag
-           _ -> err $ "Tag for property " ++ propId ++ " not found"
+    -- Substrings of the output following a @\<Property @ opening tag, each
+    -- extending to the next such tag (or to the end of the output).
+    propertyElems = drop 1 . splitOn "<Property "
 
-    findAnswer tag =
-      case findChildren (simpleName "Answer") tag of
-        answTag : _ ->
-          case onlyText (elContent answTag) of
-            answ : _ -> cdData answ
-            _ -> err "Invalid 'Answer' attribute"
-        _ -> err "Attribute 'Answer' not found"
+    -- True if the given property element has the name of the property this
+    -- function looks for.
+    isRightProperty elem' =
+      ("name=\"" ++ escapeAttr propId ++ "\"") `isInfixOf` openingTag
+      where
+        openingTag = takeWhile (/= '>') elem'
+
+    -- The contents of the first @\<Answer\>@ tag in the given element, if
+    -- any.
+    answerText elem' = do
+      (_, rest)  <- stripInfix "<Answer" elem'
+      (_, rest') <- stripInfix ">" rest
+      let answer = trim $ takeWhile (/= '<') rest'
+      if null answer then Nothing else Just answer
 
     err :: forall a . String -> a
     err msg = Err.fatal $
       "Parse error while reading the Kind2 XML output : \n"
       ++ msg ++ "\n\n" ++ xml
+
+-- | Escape a string for use as an XML attribute value.
+escapeAttr :: String -> String
+escapeAttr = concatMap escapeChar
+  where
+    escapeChar '&' = "&amp;"
+    escapeChar '<' = "&lt;"
+    escapeChar '>' = "&gt;"
+    escapeChar '"' = "&quot;"
+    escapeChar c   = [c]