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 2.x. (#734)
+
 2026-05-07
         * Version bump (4.7.1). (#730)
         * Handle special Float values correctly for counterexamples. (#697)

copilot-theorem/README.md

@@ -95,7 +95,7 @@ It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prov
 ```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,51 +335,25 @@ 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 2.x 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` funtion,
+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
 `Misc.Renaming` monad. Some code complexity has been added so variable names
 remain as clear as possible after merging two nodes.
 
-The function `removeCycles` computes the strongly connected components of the
-dependency graph and merge each one into a single node. The complexity of this
-process is high in the worst case (the square of the total size of the system
-times the size of the biggest node) but good in practice as few nodes are to be
-merged in most practical cases.
-
-After the cycles have been removed, it is useful to apply another
-transformation which makes the translation from `TransSys.Spec` to `Kind2.AST`
-easier. This transformation is implemented in the `complete` function. In a
-nutshell, it transforms a system such that:
-
-* If a node depends on another, it imports *all* its variables.
-* The dependency graph is transitive, that is if *A* depends of *B* which
-  depends of *C* then *A* depends on *C*.
-
 After this transformation, the translation from `TransSys.Spec` to `Kind2.AST`
 is almost only a matter of syntax.
 
-###### Bonus track
-
-Thanks to the `mergeNodes` function, we can get for free the function
-
-```haskell
-inline :: Spec -> Spec
-inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec
-```
-
-which discards all the structure of a *modular transition system* and turns it
-into a *non-modular transition system* with only one node. In fact, when
-translating a Copilot specification to a Kind2 file, two styles are available:
-the `Kind2.toKind2` function takes a `Style` argument which can take the value
-`Inlined` or `Modular`. The only difference is that in the first case, a call
-to `removeCycles` is replaced by a call to `inline`.
-
 ### Limitations of copilot-theorem
 
 Now, we will discuss some limitations of the *copilot-theorem* tool. These
@@ -516,10 +490,11 @@ 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. 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 +544,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
@@ -60,7 +65,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 +141,40 @@ test-suite unit-tests
 
   ghc-options:
     -Wall
+
+-- Tests of the Kind2 backend, which require the kind2 executable (version
+-- 2.x) 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,35 +1,38 @@
 {-# 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 2.x (@--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.
 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 series of
+-- propositions about the last (top) node.
 data File = File
-  { filePreds     :: [PredDef]
+  { fileNodes     :: [Node]
   , fileProps     :: [Prop] }
 
 -- | 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.
-data StateVarDef = StateVarDef
-  { varId         :: String           -- ^ Name of the variable.
-  , varType       :: Type             -- ^ Type of the variable.
-  , varFlags      :: [StateVarFlag] } -- ^ Flags for the variable.
-
 -- | Types used in Kind2 files to represent Copilot types.
 --
 -- The Kind2 backend provides functions to, additionally, constrain the range
@@ -39,14 +42,15 @@ data Type = Int | Real | Bool
 -- | Possible flags for a state variable.
 data StateVarFlag = FConst
 
--- | Type of the predicate, either belonging to an initial state or a pair of
--- states with a transition.
-data PredType = Init | Trans
-
 -- | Datatype to describe a term in the Kind language.
 data Term =
     ValueLiteral  String
   | PrimedStateVar String
   | StateVar       String
   | FunApp         String [Term]
-  | PredApp        String PredType [Term]
+
+-- | A definition of a state variable.
+data StateVarDef = StateVarDef
+  { varId         :: String           -- ^ Name of the variable.
+  , varType       :: Type             -- ^ Type of the variable.
+  , varFlags      :: [StateVarFlag] } -- ^ Options for the variable.