From 5de4a7bb82e9671b7961b8b0b4c222e0738a1bc3 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:53:43 -0500 Subject: [PATCH 01/25] 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 modern releases of Kind2. It has been tested with Kind2 v2.3, the latest at the time of this commit. --- copilot-theorem/copilot-theorem.cabal | 2 +- .../src/Copilot/Theorem/Kind2/AST.hs | 51 +++++-- .../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 +++++------------- 6 files changed, 196 insertions(+), 179 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index cd9d2e00e..1c809e3c9 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 diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs index e69cda8d0..efd493a6d 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs @@ -1,27 +1,54 @@ {-# 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 +-- ([nativeInput.ml] +-- (https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml)), +-- which includes a sketch of the grammar in a comment near the end of the +-- file) and the example file +-- [two_counters.kind2] +-- (https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.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 8258eb4968490d46bcb651c870b64d73398c7adb Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Mon, 22 Jun 2026 14:26:39 -0500 Subject: [PATCH 02/25] copilot-theorem: Update README for Kind2 backend changes. 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 copilot-theorem's README to reflect updates required to the Kind2 backend for supporting newer versions of Kind2 (e.g., the renaming Kind2's "--bmc_max" flag to "--unroll_max"). --- copilot-theorem/README.md | 40 +++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 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 From b8ff2fbaa16abac1441d172fa557e727d4380e66 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:54:17 -0500 Subject: [PATCH 03/25] 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..fd4dea25b 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-06-09 + * Extend range of versions of Kind2. (#734) + 2026-05-07 * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697) From 423e4bd95130c1148a0a8ab826d732892ee25468 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 04/25] copilot-core: Version bump (4.8). Refs #745. --- copilot-core/copilot-core.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index ee463977c..541cad1e3 100644 --- a/copilot-core/copilot-core.cabal +++ b/copilot-core/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 4.7.1 +version: 4.8 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 068fb4dd5f9f4be6457b722666674fd8d1ee0ad4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 05/25] copilot-bluespec: Version bump (4.8). Refs #745. --- copilot-bluespec/copilot-bluespec.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index ffaadaca2..2cff39b37 100644 --- a/copilot-bluespec/copilot-bluespec.cabal +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec -version : 4.7.1 +version : 4.8 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,8 +51,8 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.7.1 && < 4.8 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.8 && < 4.9 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From e89270da21a828c45ddb39d73c02931f4973ffa2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 06/25] copilot-c99: Version bump (4.8). Refs #745. --- copilot-c99/copilot-c99.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index d9802bd42..d3defea3f 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 4.7.1 +version : 4.8 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ library , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 2d8b28ad156c1546b39aa8cbef83468ba3c545b4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 07/25] copilot-prettyprinter: Version bump (4.8). Refs #745. --- copilot-prettyprinter/copilot-prettyprinter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index c40511c43..393ae9b37 100644 --- a/copilot-prettyprinter/copilot-prettyprinter.cabal +++ b/copilot-prettyprinter/copilot-prettyprinter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-prettyprinter -version: 4.7.1 +version: 4.8 synopsis: A prettyprinter of Copilot Specifications. description: A prettyprinter of Copilot specifications. @@ -45,7 +45,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.7.1 && < 4.8 + copilot-core >= 4.8 && < 4.9 exposed-modules: From 792d6d9bff09ecec03538e7d82e72779c7596397 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 08/25] copilot-interpreter: Version bump (4.8). Refs #745. --- copilot-interpreter/copilot-interpreter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 0303bf17b..255d0400d 100644 --- a/copilot-interpreter/copilot-interpreter.cabal +++ b/copilot-interpreter/copilot-interpreter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-interpreter -version: 4.7.1 +version: 4.8 synopsis: Interpreter for Copilot. description: Interpreter for Copilot. @@ -44,7 +44,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.7.1 && < 4.8 + copilot-core >= 4.8 && < 4.9 exposed-modules: From bce90b0d81f566d61a0b4e136e4f2ee480217823 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 09/25] copilot-theorem: Version bump (4.8). Refs #745. --- copilot-theorem/copilot-theorem.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 1c809e3c9..28127ebd0 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.7.1 +version : 4.8 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , transformers >= 0.5 && < 0.7 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 40b284454e23c9c15963eeba2447e9e6f9c0ea55 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 10/25] copilot-language: Version bump (4.8). Refs #745. --- copilot-language/copilot-language.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 2cfab8eb8..ca5232a8c 100644 --- a/copilot-language/copilot-language.cabal +++ b/copilot-language/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 4.7.1 +version: 4.8 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ library , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 4.7.1 && < 4.8 - , copilot-interpreter >= 4.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-interpreter >= 4.8 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From 27e4a4988ae552850ac4c9227a74fc682af14482 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 11/25] copilot-libraries: Version bump (4.8). Refs #745. --- copilot-libraries/copilot-libraries.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 85b117f63..dd96c07d4 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 4.7.1 +version: 4.8 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.9 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.7.1 && < 4.8 + , copilot-language >= 4.8 && < 4.9 exposed-modules: Copilot.Library.Analysis From 766bf4f787fde14e88d6cf32e1e28c848b7b93c0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 12/25] copilot-verifier: Version bump (4.8). Refs #745. --- copilot-verifier/copilot-verifier.cabal | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 339892ec9..aed3a0f10 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.7.1 +Version: 4.8 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ common bldflags bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-theorem >= 4.7.1 && < 4.8, + copilot-c99 >= 4.8 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-theorem >= 4.8 && < 4.9, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8, - copilot-libraries >= 4.7.1 && < 4.8, - copilot-prettyprinter >= 4.7.1 && < 4.8, + copilot >= 4.8 && < 4.9, + copilot-language >= 4.8 && < 4.9, + copilot-libraries >= 4.8 && < 4.9, + copilot-prettyprinter >= 4.8 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples From cb850da8408028c9628697e87c7c81ef6a385e81 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 13/25] copilot-visualizer: Version bump (4.8). Refs #745. --- copilot-visualizer/copilot-visualizer.cabal | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index 5e8735ea4..1bd88608a 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -1,6 +1,6 @@ cabal-version: >= 1.10 name: copilot-visualizer -version: 4.7.1 +version: 4.8 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -65,10 +65,10 @@ library text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-interpreter >= 4.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8 + copilot >= 4.8 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-interpreter >= 4.8 && < 4.9, + copilot-language >= 4.8 && < 4.9 exposed-modules: From 2eabea860dbc45ec2b6f406d6484a15f854e6762 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:20:12 -0700 Subject: [PATCH 14/25] copilot: Version bump (4.8). Refs #745. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index ace61023d..85dd95ab0 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.7.1 +version: 4.8 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ library , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 - , copilot-language >= 4.7.1 && < 4.8 - , copilot-libraries >= 4.7.1 && < 4.8 - , copilot-c99 >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 + , copilot-language >= 4.8 && < 4.9 + , copilot-libraries >= 4.8 && < 4.9 + , copilot-c99 >= 4.8 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main From 254abaa94f82bc8fd0b7b05d047c197f6c5c55d3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 15/25] copilot-core: Document changes in CHANGELOG. Refs #745. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 4a019a359..e37d60585 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 88d7cf5abd9b1ff4171ca9635e5549bffddb2749 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 16/25] copilot-bluespec: Document changes in CHANGELOG. Refs #745. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 63ea6878b..1145b7a83 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Fix translation of special Float values to Bluespec. (#697) From ad9bce157314386f729048cdc9143414f40be55a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 17/25] copilot-c99: Document changes in CHANGELOG. Refs #745. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 74c6c1dd4..ba43b631d 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 310c80ddf67e8dc10401da6a305189e54ba91575 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 18/25] copilot-prettyprinter: Document changes in CHANGELOG. Refs #745. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index a8e6d3e12..7ffd6c90d 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From e27694855d0c8a8ff6aa6ca1c106615da9266509 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 19/25] copilot-interpreter: Document changes in CHANGELOG. Refs #745. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 53984488e..d97f4575e 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From f45759c245e82df5095071acf926b41bf046f514 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 20/25] copilot-theorem: Document changes in CHANGELOG. Refs #745. --- copilot-theorem/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index fd4dea25b..ec8dafd5a 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ -2026-06-09 +2026-07-07 + * Version bump (4.8). (#745) * Extend range of versions of Kind2. (#734) 2026-05-07 From d67b8c87f752bc326d270801cad35c3afdde1ac7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 21/25] copilot-language: Document changes in CHANGELOG. Refs #745. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 069d20f5d..b162f316a 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 2fddcea36646277ce88ce1f1719144156019b64e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 22/25] copilot-libraries: Document changes in CHANGELOG. Refs #745. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 19b510a63..b09286048 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Add stream analysis module. (#726) From d081479e1d86a9fc7479cb233d5c2b84b2c3ff17 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 23/25] copilot-verifier: Document changes in CHANGELOG. Refs #745. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index a2b4dd530..81d2534f7 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 8d17366634029cb76a13d0a42f0622cf168a9192 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 24/25] copilot-visualizer: Document changes in CHANGELOG. Refs #745. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 0735d51ab..e4a74c508 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) From 88a6761537c5d7ae0b0efcd48e6ce59bcae22788 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 7 Jul 2026 23:21:58 -0700 Subject: [PATCH 25/25] copilot: Document changes in CHANGELOG. Refs #745. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f58dd30e6..f46d51f91 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730)