From 3d5a9d7adadd991eb32699f4aee60b28693efd5f Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:53:43 -0500 Subject: [PATCH 1/3] copilot-theorem: Extend range of versions of Kind2. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit updates the copilot-theorem Kind2 native-format backend to produce output targeting the latest release of Kind2 (v2.3), but it should also work with any version of Kind2 from v1.0 to v3.0. --- copilot-theorem/README.md | 40 +++-- copilot-theorem/copilot-theorem.cabal | 39 ++++- .../src/Copilot/Theorem/Kind2/AST.hs | 50 +++++-- .../src/Copilot/Theorem/Kind2/Output.hs | 117 +++++++++------ .../src/Copilot/Theorem/Kind2/PrettyPrint.hs | 49 ++++-- .../src/Copilot/Theorem/Kind2/Prover.hs | 16 +- .../src/Copilot/Theorem/Kind2/Translate.hs | 140 +++++------------- 7 files changed, 258 insertions(+), 193 deletions(-) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 64cce8995..47a4b6081 100644 --- a/copilot-theorem/README.md +++ b/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,7 +88,9 @@ 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 @@ -95,7 +98,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,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 diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index cd9d2e00e..7bc1314b1 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -51,6 +51,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 +61,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 +137,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 diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs index e69cda8d0..2ced67ca9 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/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 +-- (, +-- which includes a sketch of the grammar in a comment near the end of the +-- file) and the example file +-- +-- 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. diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index f80b8170b..8a1d29c28 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/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 +-- . +-- 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 +-- @\@ tag for the given property and extracts the answers in the +-- @\@ 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 @\ - 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 @\@ tag in the given element, if + -- any. + answerText elem' = do + (_, 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 '&' = "&" + escapeChar '<' = "<" + escapeChar '>' = ">" + escapeChar '"' = """ + escapeChar c = [c] diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs index 6851d46fa..92d158a1c 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -1,6 +1,8 @@ {-# LANGUAGE Safe #-} --- | Pretty print a Kind2 file defining predicates and propositions. +-- | Pretty print a Kind2 file defining nodes and propositions, in the native +-- transition system input format supported by Kind2 1.0 and newer (see +-- "Copilot.Theorem.Kind2.AST" for pointers to references on the format). module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -15,6 +17,14 @@ type SSExpr = SExpr String -- | Reserved keyword prime. kwPrime = "prime" +-- | Dummy position attached to the properties of the file. +-- +-- Kind2 requires a position (in the format @file:row-col@) for properties +-- declared with the @:user@ source annotation, and reports that position back +-- in its output. +propPosition :: String +propPosition = "copilot:1-1" + -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint = @@ -29,30 +39,41 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True -- | Convert a file into a sequence of expressions. +-- +-- The top node is printed last, since Kind2 analyzes the last node of the +-- file as the top system. The properties of the file are attached to it. ppFile :: File -> [SSExpr] -ppFile (File preds props) = map ppPredDef preds ++ ppProps props +ppFile (File nodes top props) = + map (`ppNode` []) nodes ++ [ppNode top (ppProps props)] --- | Convert a sequence of propositions into command to check each of them. +-- | Convert a sequence of propositions into a props field. ppProps :: [Prop] -> [SSExpr] -ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +ppProps [] = [] +ppProps ps = [ node "props" [ list $ map ppProp ps ] ] -- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr -ppProp (Prop n t) = list [atom n, ppTerm t] +ppProp (Prop n t) = list [atom n, ppTerm t, atom ":user", atom propPosition] --- | Convert a predicate into an expression. -ppPredDef :: PredDef -> SSExpr -ppPredDef pd = - list [ atom "define-pred" - , atom (predId pd) - , list . map ppStateVarDef . predStateVars $ pd - , node "init" [ppTerm $ predInit pd] - , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a node, together with optional extra fields, into an expression. +ppNode :: Node -> [SSExpr] -> SSExpr +ppNode n extraFields = + list $ [ atom "define-node" + , atom (nodeId n) + , list . map ppStateVarDef . nodeStateVars $ n + , node "init" [ppTerm $ nodeInit n] + , node "trans" [ppTerm $ nodeTrans n] ] + ++ extraFields -- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd = - list [atom (varId svd), ppType (varType svd)] + list $ [atom (varId svd), ppType (varType svd)] + ++ map ppStateVarFlag (varFlags svd) + +-- | Convert a state variable option into an expression. +ppStateVarFlag :: StateVarFlag -> SSExpr +ppStateVarFlag FConst = atom ":const" -- | Convert a type into an expression. ppType :: Type -> SSExpr diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 4bb52322e..a79ede4f6 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -28,7 +28,8 @@ import qualified Copilot.Theorem.TransSys as TS -- | Options for Kind2 data Options = Options { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and - -- step will perform. A value of 0 means /unlimited/. + -- step will perform (passed to Kind2 via its + -- @--unroll_max@ option). A value of 0 means /unlimited/. } -- | Default options with unlimited unrolling for base and step. @@ -41,7 +42,10 @@ data ProverST = ProverST -- | A prover backend based on Kind2. -- --- The executable @kind2@ must exist and its location be in the @PATH@. +-- The executable @kind2@ must exist and its location be in the @PATH@. Kind2 +-- version 1.0 or newer is required: the native input format and the +-- command-line options this prover uses were introduced in Kind2 1.0, and +-- remain supported as of Kind2 3.0. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" @@ -50,24 +54,22 @@ kind2Prover opts = Prover , closeProver = const $ return () } kind2Prog = "kind2" -kind2BaseOptions = ["--input-format", "native", "-xml"] +kind2BaseOptions = ["--input_format", "native", "-xml"] askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do - let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec + let kind2Input = prettyPrint . toKind2 assumptions toCheck $ spec (tempName, tempHandle) <- openTempFile "." "out" "kind" hPutStr tempHandle kind2Input hClose tempHandle let kind2Options = - kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName] + kind2BaseOptions ++ ["--unroll_max", show $ bmcMax opts, tempName] (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options "" - putStrLn kind2Input - removeFile tempName let propId = head toCheck diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index 123f6ed64..d59aaae24 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -1,68 +1,44 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE Safe #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications. module Copilot.Theorem.Kind2.Translate ( toKind2 - , Style (..) ) where import Copilot.Theorem.TransSys import qualified Copilot.Theorem.Kind2.AST as K -import Control.Exception.Base (assert) - import Data.Function (on) import Data.Maybe (fromJust) -import Data.List (sort, sortBy) -import Data.Map (Map, (!)) +import Data.List (partition, sort, sortBy) +import Data.Map ((!)) import qualified Data.Map as Map import qualified Data.Bimap as Bimap --- The following properties MUST hold for the given transition system : --- * Nodes are sorted by topological order --- * Nodes are `completed`, which means the dependency graph is transitive --- and each node imports all the local variables of its dependencies --- - -type DepGraph = Map NodeId [NodeId] - --- | Style of the Kind2 files produced: modular (with multiple separate nodes), --- or all inlined (with only one node). --- --- In the modular style, the graph is simplified to remove cycles by collapsing --- all nodes participating in a strongly connected components. --- --- In the inlined style, the structure of the modular transition system is --- discarded and the graph is first turned into a /non-modular transition/ --- /system/ with only one node, which can be then converted into a Kind2 file. -data Style = Inlined | Modular - -- | Produce a Kind2 file that checks the properties specified. -toKind2 :: Style -- ^ Style of the file (modular or inlined). - -> [PropId] -- ^ Assumptions +toKind2 :: [PropId] -- ^ Assumptions -> [PropId] -- ^ Properties to be checked -> TransSys -- ^ Modular transition system holding the system spec -> K.File -toKind2 style assumptions checkedProps spec = - addAssumptions spec assumptions - $ trSpec (complete spec') predCallsGraph assumptions checkedProps +toKind2 assumptions checkedProps spec = + addAssumptions spec' assumptions $ trSpec spec' checkedProps where - predCallsGraph = specDependenciesGraph spec' - spec' = case style of - Inlined -> inline spec - Modular -> removeCycles spec + spec' = inline spec -trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File -trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props +trSpec :: TransSys -> [PropId] -> K.File +trSpec spec checkedProps = K.File otherNodes topNode props where - preds = map (trNode spec predCallsGraph) (specNodes spec) + (topNode, otherNodes) = + case partition ((== specTopNodeId spec) . K.nodeId) nodes of + ([top], others) -> (top, others) + _ -> error $ "Kind2.Translate: top node " + ++ specTopNodeId spec ++ " not found" + nodes = map (trNode spec) (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ Map.toList $ Map.map fst $ specProps spec @@ -70,37 +46,30 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) -trNode :: TransSys -> DepGraph -> Node -> K.PredDef -trNode spec predCallsGraph node = - K.PredDef { K.predId, K.predStateVars, K.predInit, K.predTrans } - where - predId = nodeId node - predStateVars = gatherPredStateVars spec node - predInit = mkConj $ initLocals node - ++ map (trExpr False) (nodeConstrs node) - ++ predCalls True spec predCallsGraph node - predTrans = mkConj $ transLocals node - ++ map (trExpr True) (nodeConstrs node) - ++ predCalls False spec predCallsGraph node - +trNode :: TransSys -> Node -> K.Node +trNode spec node = K.Node + { K.nodeId = nodeId node + , K.nodeStateVars = gatherPredStateVars spec node + , K.nodeInit = mkConj $ initLocals node + ++ map (trExpr False) (nodeConstrs node) + , K.nodeTrans = mkConj $ transLocals node + ++ map (trExpr True) (nodeConstrs node) + } + +-- | Add the assumptions to the top node of the file by conjoining the +-- corresponding property variables to its initial state and transition +-- relation predicates. addAssumptions :: TransSys -> [PropId] -> K.File -> K.File -addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = - K.File (changeTail aux filePreds) fileProps +addAssumptions spec assumptions file = + file { K.fileTopNode = aux (K.fileTopNode file) } where - changeTail f (reverse -> l) = case l of - [] -> error "impossible" - x : xs -> reverse $ f x : xs - - aux pred = - let init' = mkConj ( K.predInit pred : map K.StateVar vars ) - trans' = mkConj ( K.predTrans pred : map K.PrimedStateVar vars ) - in pred { K.predInit = init', K.predTrans = trans' } + aux node = + let init' = mkConj ( K.nodeInit node : map K.StateVar vars ) + trans' = mkConj ( K.nodeTrans node : map K.PrimedStateVar vars ) + in node { K.nodeInit = init', K.nodeTrans = trans' } - vars = - let bindings = nodeImportedVars (specTopNode 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 + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec + vars = map (varName . extVarLocalPart . toExtVar) assumptions -- The ordering really matters here because the variables -- have to be given in this order in a pred call @@ -169,39 +138,6 @@ transLocals node = Expr e -> [mkEquality (trPrimedVar v) (trExpr True e)] Constrs cs -> map (trExpr True) cs -predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term] -predCalls isInitCall spec predCallsGraph node = - map mkCall toCall - where - nid = nodeId node - toCall = predCallsGraph ! nid - nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] - - nodeLocals n = - map (ExtVar n) . sort . Map.keys - . nodeLocalVars $ (nodesMap ! n) - - mkCall callee - | isInitCall = - K.PredApp callee K.Init (argsSeq trVar) - | otherwise = - K.PredApp callee K.Trans (argsSeq trVar ++ argsSeq trPrimedVar) - where - - calleeLocals = nodeLocals callee - calleeImported = - (concatMap nodeLocals . sort . nodeDependencies) $ nodesMap ! callee - - localAlias trVarF ev = - case Bimap.lookupR ev $ nodeImportedVars node of - Nothing -> error $ - "This spec is not complete : " - ++ show ev ++ " should be imported in " ++ nid - Just v -> trVarF v - - argsSeq trVarF = - map (localAlias trVarF) (calleeLocals ++ calleeImported) - trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr where From fdb9622d22116024c9863b564c71e213fa23b594 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:28:35 -0500 Subject: [PATCH 2/3] copilot-theorem: tests for the Kind2 backend. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit adds a testsuite for the Kind2 copilot-theorem native-format backend. It requires Kind2 (version >1.0) to be installed and can be activated using the `test-kind2` `cabal` flag (e.g., `cabal test -ftest-kind2`). --- copilot-theorem/copilot-theorem.cabal | 5 + copilot-theorem/tests/Kind2Main.hs | 21 ++ .../tests/Test/Copilot/Theorem/Kind2.hs | 301 ++++++++++++++++++ 3 files changed, 327 insertions(+) create mode 100644 copilot-theorem/tests/Kind2Main.hs create mode 100644 copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 7bc1314b1..28cbbba38 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/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 diff --git a/copilot-theorem/tests/Kind2Main.hs b/copilot-theorem/tests/Kind2Main.hs new file mode 100644 index 000000000..657033de9 --- /dev/null +++ b/copilot-theorem/tests/Kind2Main.hs @@ -0,0 +1,21 @@ +-- | Test the Kind2 backend of copilot-theorem. +-- +-- These tests require the @kind2@ executable (version 1.0 or newer) to be in +-- the @PATH@. +module Main where + +-- External imports +import Test.Framework (Test, defaultMain) + +-- Internal imports +import qualified Test.Copilot.Theorem.Kind2 + +-- | Run all unit tests on the Kind2 backend of copilot-theorem. +main :: IO () +main = defaultMain tests + +-- | All unit tests on the Kind2 backend of copilot-theorem. +tests :: [Test.Framework.Test] +tests = + [ Test.Copilot.Theorem.Kind2.tests + ] diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs b/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs new file mode 100644 index 000000000..bca62dba6 --- /dev/null +++ b/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs @@ -0,0 +1,301 @@ +-- | Test copilot-theorem:Copilot.Theorem.Kind2. +-- +-- These tests require the @kind2@ executable (version 1.0 or newer) to be in +-- the @PATH@. +module Test.Copilot.Theorem.Kind2 where + +-- External imports +import Control.Monad.Writer (tell) +import Data.Int (Int32) +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.HUnit (testCase) +import Test.HUnit (Assertion, assertEqual) + +-- External imports: Copilot +import Copilot.Core.Expr (Expr (Const, Drop, ExternVar, Op1, + Op2), Id) +import Copilot.Core.Operators (Op1 (..), Op2 (..)) +import Copilot.Core.Spec (Spec (..), Stream (..)) +import qualified Copilot.Core.Spec as Copilot +import Copilot.Core.Type (Typed (typeOf)) + +-- Internal imports: Modules being tested +import Copilot.Theorem.Kind2.Prover (def, kind2Prover) +import Copilot.Theorem.Prove (Action (..), PropId, prove) + +-- * Constants + +-- | Unit tests for copilot-theorem:Copilot.Theorem.Kind2. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Theorem.Kind2" + [ testCase "Prove that true is valid" + testTrueValid + , testCase "Prove that false is invalid" + testFalseInvalid + , testCase "Prove that an existentially quantified true is valid" + testExistsTrueValid + , testCase "Prove that an existentially quantified false is invalid" + testExistsFalseInvalid + , testCase "Prove a valid property of a recursive stream" + testCounterGt1 + , testCase "Disprove an invalid property of a recursive stream" + testCounterLt255 + , testCase "Prove a valid existential property of a recursive stream" + testCounterExistsGt3 + , testCase "Prove a valid property of an external stream" + testExternEq + , testCase "Prove a property using an assumption" + testAssumption + , testCase "Disprove a property when its assumption is not used" + testNoAssumption + , testCase "Prove a valid property of a real-valued stream" + testRealValued + , testCase "Prove a valid property of a boolean stream" + testBoolStream + ] + +-- * Individual tests + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- constant True +-- @ +testTrueValid :: Assertion +testTrueValid = + checkProve True propName spec + where + propName = "prop" + spec = forallPropSpec propName [] $ Const typeOf True + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- constant False +-- @ +testFalseInvalid :: Assertion +testFalseInvalid = + checkProve False propName spec + where + propName = "prop" + spec = forallPropSpec propName [] $ Const typeOf False + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- exists: constant True +-- @ +-- +-- Existentially quantified properties are encoded by asking Kind2 to check +-- the negation of the property, so this test exercises the case in which +-- Kind2 reports that a property is falsifiable. +testExistsTrueValid :: Assertion +testExistsTrueValid = + checkProve True propName spec + where + propName = "prop" + spec = existsPropSpec propName [] $ Const typeOf True + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- exists: constant False +-- @ +testExistsFalseInvalid :: Assertion +testExistsFalseInvalid = + checkProve False propName spec + where + propName = "prop" + spec = existsPropSpec propName [] $ Const typeOf False + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x > 1) +-- @ +testCounterGt1 :: Assertion +testCounterGt1 = + checkProve True propName spec + where + propName = "gt1" + spec = forallPropSpec propName [counterStream] $ + Op2 (Gt typeOf) counterExpr (constI32 1) + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x < 255) +-- @ +-- +-- This test exercises the case in which Kind2 reports that a property is +-- falsifiable, which, for systems in Kind2's native input format, also makes +-- Kind2 produce output that is not well-formed XML. +testCounterLt255 :: Assertion +testCounterLt255 = + checkProve False propName spec + where + propName = "lt255" + spec = forallPropSpec propName [counterStream] $ + Op2 (Lt typeOf) counterExpr (constI32 255) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let x = [2] ++ (x + 1) +-- in exists (x > 3) +-- @ +testCounterExistsGt3 :: Assertion +testCounterExistsGt3 = + checkProve True propName spec + where + propName = "gt3" + spec = existsPropSpec propName [counterStream] $ + Op2 (Gt typeOf) counterExpr (constI32 3) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let e = extern "ext" Nothing +-- in forAll (e == e) +-- @ +testExternEq :: Assertion +testExternEq = + checkProve True propName spec + where + propName = "eq" + extECopy = ExternVar typeOf "ext" Nothing :: Expr Int32 + spec = forallPropSpec propName [] $ Op2 (Eq typeOf) extECopy extECopy + +-- | Test that Kind2 is able to prove the property @lt20@ valid when assuming +-- the property @lt10@, in the following specification: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x < 10) -- lt10 +-- forAll (x < 20) -- lt20 +-- @ +testAssumption :: Assertion +testAssumption = do + result <- prove spec "lt20" $ + tell [Assume "lt10", Check (kind2Prover def)] + assertEqual "proof result for lt20 (assuming lt10)" True result + where + spec = assumptionSpec + +-- | Test that Kind2 is able to prove the property @lt20@ invalid when the +-- assumption @lt10@ is not used, in the same specification as +-- 'testAssumption'. +testNoAssumption :: Assertion +testNoAssumption = do + result <- prove spec "lt20" $ + tell [Check (kind2Prover def)] + assertEqual "proof result for lt20 (without assumptions)" False result + where + spec = assumptionSpec + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let y = [0.5] ++ y +-- in forAll (y > 0.0) +-- @ +testRealValued :: Assertion +testRealValued = + checkProve True propName spec + where + propName = "pos" + + streamId' :: Id + streamId' = 0 + + stream :: Stream + stream = Stream + { streamId = streamId' + , streamBuffer = [0.5 :: Double] + , streamExpr = Drop typeOf 0 streamId' + , streamExprType = typeOf + } + + spec = forallPropSpec propName [stream] $ + Op2 (Gt typeOf) (Drop typeOf 0 streamId' :: Expr Double) + (Const typeOf (0.0 :: Double)) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let b = [True] ++ (b && constant True) +-- in forAll (not (not b)) +-- @ +testBoolStream :: Assertion +testBoolStream = + checkProve True propName spec + where + propName = "tt" + + streamId' :: Id + streamId' = 0 + + stream :: Stream + stream = Stream + { streamId = streamId' + , streamBuffer = [True] + , streamExpr = Op2 And (Drop typeOf 0 streamId') (Const typeOf True) + , streamExprType = typeOf + } + + spec = forallPropSpec propName [stream] $ + Op1 Not (Op1 Not (Drop typeOf 0 streamId')) + +-- * Auxiliary + +-- | Check that proving the given property of the given spec with the Kind2 +-- prover produces the expected result. +checkProve :: Bool -> PropId -> Spec -> Assertion +checkProve expectation propName spec = do + result <- prove spec propName $ tell [Check (kind2Prover def)] + assertEqual ("proof result for property " ++ propName) expectation result + +-- | A stream of 'Int32' defined by: +-- @ +-- x = [2] ++ (x + 1) +-- @ +counterStream :: Stream +counterStream = Stream + { streamId = counterStreamId + , streamBuffer = [2 :: Int32] + , streamExpr = Op2 (Add typeOf) counterExpr (constI32 1) + , streamExprType = typeOf + } + +-- | Id of 'counterStream'. +counterStreamId :: Id +counterStreamId = 0 + +-- | The current value of 'counterStream'. +counterExpr :: Expr Int32 +counterExpr = Drop typeOf 0 counterStreamId + +-- | A constant 'Int32' expression. +constI32 :: Int32 -> Expr Int32 +constI32 = Const typeOf + +-- | A specification with the 'counterStream' and two properties, @lt10@ and +-- @lt20@, stating that the values of the stream are smaller than 10 and 20, +-- respectively. Both properties are invalid on their own, but @lt20@ holds +-- if @lt10@ is assumed. +assumptionSpec :: Spec +assumptionSpec = Spec + [counterStream] + [] + [] + [ Copilot.Property "lt10" $ Copilot.Forall $ + Op2 (Lt typeOf) counterExpr (constI32 10) + , Copilot.Property "lt20" $ Copilot.Forall $ + Op2 (Lt typeOf) counterExpr (constI32 20) + ] + +-- | Build a 'Spec' that contains one property with the given name, which +-- contains the given streams, and is defined by the given boolean expression, +-- which is universally quantified. +forallPropSpec :: String -> [Stream] -> Expr Bool -> Spec +forallPropSpec propName propStreams propExpr = + Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall propExpr)] + +-- | Build a 'Spec' that contains one property with the given name, which +-- contains the given streams, and is defined by the given boolean expression, +-- which is existentially quantified. +existsPropSpec :: String -> [Stream] -> Expr Bool -> Spec +existsPropSpec propName propStreams propExpr = + Spec propStreams [] [] [Copilot.Property propName (Copilot.Exists propExpr)] From fe2fcd5dcc8fb4cfc9e49092fb107ea472582e9d Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:54:17 -0500 Subject: [PATCH 3/3] copilot-theorem: Document changes in CHANGELOG. Refs #734. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf36..f2a31ba76 100644 --- a/copilot-theorem/CHANGELOG +++ b/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)