From 9743faef83ea8d04722c1a215410b71968ab3340 Mon Sep 17 00:00:00 2001 From: Trevor Kann Date: Fri, 19 Dec 2025 12:06:37 -0500 Subject: [PATCH 01/32] copilot-bluespec: Fix translation of special Float values to Bluespec. Refs #697. `copilot-bluespec`'s translation from Copilot to Bluespec up-casts `Float` values to `Double` values using the `realToFrac` function. `realToFrac` incorrectly handles special floating-point values such as negative zero, infinity, and NaN values, causing `copilot-bluespec` to generate the wrong `Float` values on the Bluespec end. This commit removes the use of `realToFrac` in favor of an alternative approach based on `GHC.Float.float2Double`, which correctly handles most special floating-point values. A notable exception is NaN values, as `float2Double` does not reliably preserve the payload of a NaN value. As such, we include a special case for NaN values that takes care to preserve payloads. Co-authored-by: Ryan Scott --- .../src/Copilot/Compile/Bluespec/Expr.hs | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs index 39ff1ad2..2b71b395 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -18,7 +18,7 @@ import Data.String (IsString (..)) import qualified Language.Bluespec.Classic.AST as BS import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload) -import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64) +import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64, float2Double) -- Internal imports: Copilot import Copilot.Core @@ -535,7 +535,7 @@ constTy ty = Word16 -> constInt ty . toInteger Word32 -> constInt ty . toInteger Word64 -> constInt ty . toInteger - Float -> constFP ty . realToFrac + Float -> constFP ty . nanSafeFloat2Double Double -> constFP ty -- Translating a Copilot array literal to a Bluespec Vector is somewhat @@ -563,6 +563,20 @@ constTy ty = , constTy ty'' val )) (toValues v)) + where + -- Convert a Float to a Double. This function takes care to preserve + -- special floating-point values, such as negative zero, infinity, and NaN + -- values. + nanSafeFloat2Double :: Float -> Double + nanSafeFloat2Double x + -- float2Double does not preserve the payloads of NaN values, so we + -- include special cases for translating NaNs. + | isNaN x && isSignaling x = setPayloadSignaling payload + | isNaN x = setPayload payload + | otherwise = float2Double x + where + payload :: Double + payload = float2Double $ getPayload x -- | Transform a list of Copilot Core expressions of a given 'Type' into a -- Bluespec @Vector@ expression. From caafd778b32a0ca2ed6638daee8e008f403a6261 Mon Sep 17 00:00:00 2001 From: Trevor Kann Date: Fri, 19 Dec 2025 14:23:42 -0500 Subject: [PATCH 02/32] copilot-theorem: Handle special Float values correctly for counterexamples. Refs #697. `copilot-theorem`'s counterexample-reporting machinery up-casts `Float` values to `Double` values using the `realToFrac` function. `realToFrac` incorrectly handles special floating-point values such as negative zero, infinity, and NaN values, causing `copilot-theorem` to generate incorrect counterexamples when these special values are involved. This commit removes the use of `realToFrac` in favor of an alternative approach based on `GHC.Float.double2Float`, which correctly handles most special floating-point values. A notable exception is NaN values, as `double2Float` does not reliably preserve the payload of a NaN value. As such, we include a special case for NaN values that takes care to preserve payloads. Co-authored-by: Ryan Scott --- copilot-theorem/copilot-theorem.cabal | 1 + copilot-theorem/src/Copilot/Theorem/What4.hs | 19 +++++++++++++++++-- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index f8b4ff57..87f53807 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 + , fp-ieee >= 0.1 && < 0.2 , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.4 , panic >= 0.4.0 && < 0.5 diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 51ed6e8f..97e55a85 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -77,8 +77,9 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Nonce import Data.Parameterized.Some import qualified Data.Parameterized.Vector as V -import GHC.Float (castWord32ToFloat, castWord64ToDouble) +import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float) import LibBF (BigFloat, bfToDouble, pattern NearEven) +import Numeric.Floating.IEEE.NaN (getPayload, isSignaling, setPayload, setPayloadSignaling) import qualified Panic as Panic import Copilot.Theorem.What4.Translate @@ -707,7 +708,7 @@ valFromExpr ge xe = case xe of XFloat e -> Some . CopilotValue CT.Float <$> iFloatGroundEval WFP.SingleFloatRepr e - (realToFrac . fst . bfToDouble NearEven) + (nanSafeDoubleToFloat . fst . bfToDouble NearEven) fromRational (castWord32ToFloat . fromInteger . BV.asUnsigned) XDouble e -> @@ -757,3 +758,17 @@ valFromExpr ge xe = case xe of WB.FloatIEEERepr -> ieeeK <$> WG.groundEval ge e WB.FloatRealRepr -> realK <$> WG.groundEval ge e WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e + + -- Convert a Double to a Float. This function takes care to preserve + -- special floating-point values, such as negative zero, infinity, and NaN + -- values. + nanSafeDoubleToFloat :: Double -> Float + nanSafeDoubleToFloat x + -- double2Float does not preserve the payloads of NaN values, so we + -- include a special case for translating NaNs. + | isNaN x && isSignaling x = setPayloadSignaling payload + | isNaN x = setPayload payload + | otherwise = double2Float x + where + payload :: Float + payload = double2Float $ getPayload x From b2d81f6b64ffcb6a0e5e445736c7a8aae36f1f5d Mon Sep 17 00:00:00 2001 From: Trevor Kann Date: Tue, 31 Mar 2026 09:53:19 -0400 Subject: [PATCH 03/32] copilot-bluespec: Document changes in CHANGELOG. Refs #697. Co-authored-by: Ryan Scott --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 9072a0a4..c0ab51bc 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-31 + * Fix translation of special Float values to Bluespec. (#697) + 2026-03-07 * Version bump (4.7). (#714) From 6e2fed247bbf8b1a878306b8c0227c3629266ffb Mon Sep 17 00:00:00 2001 From: Trevor Kann Date: Tue, 31 Mar 2026 09:56:01 -0400 Subject: [PATCH 04/32] copilot-theorem: Document changes in CHANGELOG. Refs #697. Co-authored-by: Ryan Scott --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 4aaf2cf9..2f521a85 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-31 + * Handle special Float values correctly for counterexamples. (#697) + 2026-03-07 * Version bump (4.7). (#714) From c854b5ff70a1ef99bf34137a186fe63a6ad5eb6a Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 31 Mar 2026 11:46:52 -0500 Subject: [PATCH 05/32] copilot-theorem: Update examples to compile with copilot-theorem >= 3.0. Refs #692. Some example programs in the copilot-theorem/example subdirectory have bitrotted, as they depend on a Copilot.Theorem.Prover.Z3 module that is no longer included in copilot-theorem.cabal (as of 6a67d89). Attempting to build any of these examples results in compilation failures. This commit fixes the examples so they will compile using the current version of copilot-theorem. --- copilot-theorem/examples/BoyerMoore.hs | 4 ++-- copilot-theorem/examples/Grey.hs | 6 +++--- copilot-theorem/examples/Incr.hs | 4 ++-- copilot-theorem/examples/SerialBoyerMoore.hs | 6 +++--- copilot-theorem/examples/SphericalWCV.hs | 6 +++--- copilot-theorem/examples/WCV.hs | 6 +++--- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs index d4cebf63..47fe790a 100644 --- a/copilot-theorem/examples/BoyerMoore.hs +++ b/copilot-theorem/examples/BoyerMoore.hs @@ -5,7 +5,7 @@ module BoyerMoore where import Copilot.Language hiding (length) import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (debug, def, induction, z3) import Copilot.Core.Type @@ -71,7 +71,7 @@ spec = do maj = majorityVote ss induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 -- | Initial value for a given type. -- diff --git a/copilot-theorem/examples/Grey.hs b/copilot-theorem/examples/Grey.hs index 9a1ca431..91500ba1 100644 --- a/copilot-theorem/examples/Grey.hs +++ b/copilot-theorem/examples/Grey.hs @@ -4,7 +4,7 @@ module Grey where import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (Options (..), def, induction, kInduction, z3) import Prelude () import Data.String (fromString) @@ -32,7 +32,7 @@ spec = do r = extern "reset" Nothing induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 kinduct :: Word32 -> Proof Universal -kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False } +kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3 diff --git a/copilot-theorem/examples/Incr.hs b/copilot-theorem/examples/Incr.hs index 3c39a008..dd6ccdc4 100644 --- a/copilot-theorem/examples/Incr.hs +++ b/copilot-theorem/examples/Incr.hs @@ -4,7 +4,7 @@ import Prelude () import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (debug, def, induction, z3) spec = do bounds <- prop "bounds" (forAll $ x < 255) @@ -16,4 +16,4 @@ spec = do x = [2] ++ (1 + x) induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = True } +induct = induction def { debug = True } z3 diff --git a/copilot-theorem/examples/SerialBoyerMoore.hs b/copilot-theorem/examples/SerialBoyerMoore.hs index 5f0d4209..eb858a6a 100644 --- a/copilot-theorem/examples/SerialBoyerMoore.hs +++ b/copilot-theorem/examples/SerialBoyerMoore.hs @@ -4,7 +4,7 @@ module SerialBoyerMoore where import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (Options (..), def, induction, kInduction, z3) import Prelude () import Data.String (fromString) @@ -56,7 +56,7 @@ spec = do (p, s, j) = majority input induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 kinduct :: Word32 -> Proof Universal -kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False } +kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3 diff --git a/copilot-theorem/examples/SphericalWCV.hs b/copilot-theorem/examples/SphericalWCV.hs index 74b89958..06d203ad 100644 --- a/copilot-theorem/examples/SphericalWCV.hs +++ b/copilot-theorem/examples/SphericalWCV.hs @@ -8,7 +8,7 @@ import Prelude () import Copilot.Language import Copilot.Language.Reify import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (debug, def, onlySat, onlyValidity, z3) import qualified Copilot.Language.Operators.Propositional as P @@ -241,7 +241,7 @@ localConvexity = do theorem "6" (P.not (forAll $ locallyConvex tau)) arithSat arith :: Proof Universal -arith = onlyValidity def { nraNLSat = True, debug = False } +arith = onlyValidity def { debug = False } z3 arithSat :: Proof Existential -arithSat = onlySat def { nraNLSat = True, debug = False } +arithSat = onlySat def { debug = False } z3 diff --git a/copilot-theorem/examples/WCV.hs b/copilot-theorem/examples/WCV.hs index 62c27f28..c0f267c6 100644 --- a/copilot-theorem/examples/WCV.hs +++ b/copilot-theorem/examples/WCV.hs @@ -5,7 +5,7 @@ import Prelude () import Copilot.Language import Copilot.Language.Reify import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (debug, def, onlySat, onlyValidity, z3) import qualified Copilot.Language.Operators.Propositional as P @@ -165,7 +165,7 @@ localConvexity = do theorem "6" (P.not (forAll $ locallyConvex tau)) arithSat arith :: Proof Universal -arith = onlyValidity def { nraNLSat = True, debug = False } +arith = onlyValidity def { debug = False } z3 arithSat :: Proof Existential -arithSat = onlySat def { nraNLSat = True, debug = False } +arithSat = onlySat def { debug = False } z3 From 579b124a56146f563e620ca9df5d9b1c70640a84 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 31 Mar 2026 12:31:53 -0500 Subject: [PATCH 06/32] copilot-theorem: Document changes in CHANGELOG. Refs #692. --- copilot-theorem/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 2f521a85..90964353 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,5 +1,6 @@ 2026-03-31 * Handle special Float values correctly for counterexamples. (#697) + * Update examples to compile with copilot-theorem >= 3.0. (#692) 2026-03-07 * Version bump (4.7). (#714) From a4126bbed39662575daf0fd4ecdca80ce7476ffb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 18 May 2025 04:45:39 +0000 Subject: [PATCH 07/32] copilot-libraries: Add stream analysis module. Refs #726. There is a need to have in Copilot a module that includes stream and spec analysis functions. Such functions have been useful in other projects, and they could be added as part of Copilot's standard library so that they are available to all users. This commit adds a new module that provides functions to determine if a stream is always true or always false. --- copilot-libraries/copilot-libraries.cabal | 3 ++- .../src/Copilot/Library/Analysis.hs | 23 +++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) create mode 100644 copilot-libraries/src/Copilot/Library/Analysis.hs diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index e194daf7..14588731 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -44,7 +44,8 @@ library , copilot-language >= 4.7 && < 4.8 exposed-modules: - Copilot.Library.Libraries + Copilot.Library.Analysis + , Copilot.Library.Libraries , Copilot.Library.Clocks , Copilot.Library.LTL , Copilot.Library.PTLTL diff --git a/copilot-libraries/src/Copilot/Library/Analysis.hs b/copilot-libraries/src/Copilot/Library/Analysis.hs new file mode 100644 index 00000000..240addd7 --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/Analysis.hs @@ -0,0 +1,23 @@ +-- | Formally analyze streams. +module Copilot.Library.Analysis + ( triviallyTrue + , triviallyFalse + ) + where + +-- External imports. +import Prelude hiding (not) + +-- Internal imports. +import Copilot.Language (Stream, forAll, not) +import Copilot.Language.Spec (Prop, Universal) + +-- | Property that captures whether a stream is trivially true, meaning that +-- there is no way to make it false. +triviallyTrue :: Stream Bool -> Prop Universal +triviallyTrue = forAll + +-- | Property that captures whether a stream is trivially false, meaning that +-- there is no way to make it true. +triviallyFalse :: Stream Bool -> Prop Universal +triviallyFalse = triviallyTrue . not From fb249d239ed3722b1cbe03e2c6be86e112a2afb4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 20:28:02 -0700 Subject: [PATCH 08/32] copilot-libraries: Document changes in CHANGELOG. Refs #726. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 171b9b7d..49779ea5 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Add stream analysis module. (#726) + 2026-03-07 * Version bump (4.7). (#714) From 4b5225ee46f9d1ab2c832a043c5ccc7b73c5377f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:55 -0700 Subject: [PATCH 09/32] copilot-libraries: Add state machine module. Refs #728. There is a need to have in Copilot a module that implements state machines. Such functions have been useful in other projects, and they could be added as part of Copilot's standard library so that they are available to all users. This commit adds a state machine module that enables simulating a state machine using simple notation to describe the state machine. --- copilot-libraries/copilot-libraries.cabal | 1 + .../src/Copilot/Library/StateMachines.hs | 45 +++++++++++++++++++ 2 files changed, 46 insertions(+) create mode 100644 copilot-libraries/src/Copilot/Library/StateMachines.hs diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 14588731..e59ff32f 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -49,6 +49,7 @@ library , Copilot.Library.Clocks , Copilot.Library.LTL , Copilot.Library.PTLTL + , Copilot.Library.StateMachines , Copilot.Library.Statistics , Copilot.Library.RegExp , Copilot.Library.Utils diff --git a/copilot-libraries/src/Copilot/Library/StateMachines.hs b/copilot-libraries/src/Copilot/Library/StateMachines.hs new file mode 100644 index 00000000..37121b1a --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/StateMachines.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE ScopedTypeVariables #-} +-- | Simulate state machines using streams. +module Copilot.Library.StateMachines where + +import Copilot.Language (Stream, Typed, constant, ifThenElse, (&&), (++), (==)) +import Prelude hiding ((&&), (++), (==)) + +-- | A definition of a state machine where some elements are defined +-- as streams. +-- +-- A state machine is defined by an initial state, a final state, a no +-- transition stream (true when tere is no input coming in), a list of +-- transitions, and a bad state. +type StateMachine a = (a, a, Stream Bool, [(a, Stream Bool, a)], a) + +-- | Produce a stream that, at any given time, contains the current state of +-- the state machine. +stateMachine :: forall a . (Eq a, Typed a) => StateMachine a -> Stream a +stateMachine (initial, final, noInputData, transitions, bad) = state + where + state = ifThenElses transitions + previousState = [initial] ++ state + + ifThenElses :: [(a, Stream Bool, a)] -> Stream a + ifThenElses [] = + ifThenElse (previousState == constant final && noInputData) + (constant final) + (constant bad) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse + (previousState == constant s1 && i) + (constant s2) + (ifThenElses ss) + +-- | Produce a stream that, at any given time, contains the current state of +-- the state machine as the numeric representation of an enum. +stateMachineEnum :: (Eq b, Typed b, Num b, Enum a) + => StateMachine a + -> Stream b +stateMachineEnum (initial, final, noInputData, transitions, bad) = + stateMachine (fe initial, fe final, noInputData, transitionsE, fe bad) + where + transitionsE = map (\(s1, t, s2) -> (fe s1, t, fe s2)) transitions + fe = fromIntegral . fromEnum From 32704d9c8ebb7bbed0a8c7d4a5bc9aeb15554079 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:55 -0700 Subject: [PATCH 10/32] copilot-libraries: Document changes in CHANGELOG. Refs #728. --- copilot-libraries/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 49779ea5..745bb1b6 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,5 +1,6 @@ 2026-05-07 * Add stream analysis module. (#726) + * Add state machine module. (#728) 2026-03-07 * Version bump (4.7). (#714) From 2d3d84540473667029e696be9b42c19c2fe1d565 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 11/32] copilot-core: Version bump (4.7.1). Refs #730. --- 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 6d99e77d..ee463977 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 +version: 4.7.1 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 8cb85bbdd90e983572e673de469de4673d46f3dc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 12/32] copilot-bluespec: Version bump (4.7.1). Refs #730. --- 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 3ac0839c..ffaadaca 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 +version : 4.7.1 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 && < 4.8 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.7.1 && < 4.8 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From 7818e6c1404f62e3bcff10eca35983320746758e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 13/32] copilot-c99: Version bump (4.7.1). Refs #730. --- 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 0567e941..d9802bd4 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 +version : 4.7.1 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 && < 4.8 + , copilot-core >= 4.7.1 && < 4.8 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 4b1fa514a3a6f3185fdda5bcaacbd6cecb609478 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 14/32] copilot-prettyprinter: Version bump (4.7.1). Refs #730. --- 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 f6f5fcc5..c40511c4 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 +version: 4.7.1 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 && < 4.8 + copilot-core >= 4.7.1 && < 4.8 exposed-modules: From 7752221d3e0be7414bf915bd2bbc401464acffef Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 15/32] copilot-interpreter: Version bump (4.7.1). Refs #730. --- 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 9ef09f11..0303bf17 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 +version: 4.7.1 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 && < 4.8 + copilot-core >= 4.7.1 && < 4.8 exposed-modules: From 02defe133e9e2ce434b542eeedd4e7ba01e543e4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 16/32] copilot-theorem: Version bump (4.7.1). Refs #730. --- 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 87f53807..cd9d2e00 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.7 +version : 4.7.1 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.7 && < 4.8 - , copilot-prettyprinter >= 4.7 && < 4.8 + , copilot-core >= 4.7.1 && < 4.8 + , copilot-prettyprinter >= 4.7.1 && < 4.8 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 8eac0cac7a0bb24082f0a137c7da0ea5845889ce Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 17/32] copilot-language: Version bump (4.7.1). Refs #730. --- 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 740bb2b8..2cfab8eb 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 +version: 4.7.1 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 && < 4.8 - , copilot-interpreter >= 4.7 && < 4.8 - , copilot-theorem >= 4.7 && < 4.8 + , copilot-core >= 4.7.1 && < 4.8 + , copilot-interpreter >= 4.7.1 && < 4.8 + , copilot-theorem >= 4.7.1 && < 4.8 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From dad3ad411fce1d1db711fb9be0ffff7722557d94 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 18/32] copilot-libraries: Version bump (4.7.1). Refs #730. --- 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 e59ff32f..85b117f6 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 +version: 4.7.1 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 && < 4.8 + , copilot-language >= 4.7.1 && < 4.8 exposed-modules: Copilot.Library.Analysis From 9af5f1194a388f79e2a80b73e660b7b518ab2461 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 19/32] copilot-verifier: Version bump (4.7.1). Refs #730. --- 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 c7bf36a1..339892ec 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 +Version: 4.7.1 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 && < 4.8, - copilot-core >= 4.7 && < 4.8, - copilot-theorem >= 4.7 && < 4.8, + copilot-c99 >= 4.7.1 && < 4.8, + copilot-core >= 4.7.1 && < 4.8, + copilot-theorem >= 4.7.1 && < 4.8, 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 && < 4.8, - copilot-language >= 4.7 && < 4.8, - copilot-libraries >= 4.7 && < 4.8, - copilot-prettyprinter >= 4.7 && < 4.8, + 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-verifier exposed-modules: Copilot.Verifier.Examples From a932329dec110e8d0ed00893c33b649f879df311 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 20/32] copilot-visualizer: Version bump (4.7.1). Refs #730. --- 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 0500c1b4..5e8735ea 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 +version: 4.7.1 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 && < 4.8, - copilot-core >= 4.7 && < 4.8, - copilot-interpreter >= 4.7 && < 4.8, - copilot-language >= 4.7 && < 4.8 + 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 exposed-modules: From 4df77d15f74ea237c08e957ab52ec3f954cbdaed Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 21/32] copilot: Version bump (4.7.1). Refs #730. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 68ff811e..ace61023 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.7 +version: 4.7.1 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 && < 4.8 - , copilot-theorem >= 4.7 && < 4.8 - , copilot-language >= 4.7 && < 4.8 - , copilot-libraries >= 4.7 && < 4.8 - , copilot-c99 >= 4.7 && < 4.8 - , copilot-prettyprinter >= 4.7 && < 4.8 + , 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 exposed-modules: Language.Copilot, Language.Copilot.Main From df290fb3f4945c3b8a0283d612f9299ff4f84007 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 22/32] copilot-core: Document changes in CHANGELOG. Refs #730. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 671e39ef..4a019a35 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) From 4c5a53a6c53882fe57f3efb1dd6b8095abb7fbf7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 23/32] copilot-bluespec: Document changes in CHANGELOG. Refs #730. --- copilot-bluespec/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index c0ab51bc..63ea6878 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,4 +1,5 @@ -2026-03-31 +2026-05-07 + * Version bump (4.7.1). (#730) * Fix translation of special Float values to Bluespec. (#697) 2026-03-07 From 77b3a64b58554751393eeb200f467a495e41a922 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 24/32] copilot-c99: Document changes in CHANGELOG. Refs #730. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 856d5149..74c6c1dd 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) * Raise error when compiling empty arrays or structs. (#695) From d1943d58127e39f62a365065f877adf34b3a3b12 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 25/32] copilot-prettyprinter: Document changes in CHANGELOG. Refs #730. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index efa6ccf5..a8e6d3e1 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) From 00b1fa10a39c967935844275ad054f0baa8b034b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 26/32] copilot-interpreter: Document changes in CHANGELOG. Refs #730. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index c2920d17..53984488 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) From c09bb16c44ea425544192f21d88225b9f1339711 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 27/32] copilot-theorem: Document changes in CHANGELOG. Refs #730. --- copilot-theorem/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 90964353..03facaf3 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ -2026-03-31 +2026-05-07 + * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697) * Update examples to compile with copilot-theorem >= 3.0. (#692) From d1547de8018afe6469b6b3afd0d15e65ea32c1b2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 28/32] copilot-language: Document changes in CHANGELOG. Refs #730. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 4751f706..069d20f5 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) From 3b6e1b2d68177346ce6af788dbc82bc9fd60b3e6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 29/32] copilot-libraries: Document changes in CHANGELOG. Refs #730. --- copilot-libraries/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 745bb1b6..19b510a6 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,4 +1,5 @@ 2026-05-07 + * Version bump (4.7.1). (#730) * Add stream analysis module. (#726) * Add state machine module. (#728) From 2c11c9b25101bd57a7b317eaf9d9ae5b8190905c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 30/32] copilot-verifier: Document changes in CHANGELOG. Refs #730. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 049ec224..a2b4dd53 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) * Relax version constraints on what4. (#716) From 9921f52eacd65f310438cef2f170f01ae42bb1f6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 31/32] copilot-visualizer: Document changes in CHANGELOG. Refs #730. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 402ec34d..0735d51a 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714) * Relax version constraints on ogma-extra. (#716) From fce6bdfb3104aadd8af9eb978dfb2b9a75b82aca Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 7 May 2026 23:59:48 -0700 Subject: [PATCH 32/32] copilot: Document changes in CHANGELOG. Refs #730. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index dd34bc70..f58dd30e 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-05-07 + * Version bump (4.7.1). (#730) + 2026-03-07 * Version bump (4.7). (#714)