From 06c31d052cdbc4be7507b9b041b48ecdbb6354b4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 08:38:45 -0700 Subject: [PATCH 01/61] copilot-core: Force evaluation of `Proxy` value in `Copilot.Core.Type.Array`. Refs #767. The module `copilot-core:Copilot.Core.Type.Array` achieves less than full coverage in the two of the three main categories used by `hpc`, namely "Top Level Definitions" and "Expressions". For the former, only 4 out of 6 definitions are covered, and for the latter, only 47 out of 48. To make Copilot ready for use in future missions, we want to achieve maximum coverage possible. The lower coverage of "Expressions" is due to a `Proxy` value not being forced in a call to `natVal`, which only needs the type-level information for the `Proxy` being provided. This commit modifies the code of `copilot-core:Copilot.Core.Type.Array` to force the evaluation of a `Proxy` value being passed to `natVal`. Specifically, it uses `($!)`, which achieves the evaluation of the value at the point where it is being used, making `hpc` mark it as evaluated. Other alternatives (e.g., use of `seq`, use of `Proxy#`) either do not achieve the desired effect or require more extensive changes and the use of language extensions. --- copilot-core/src/Copilot/Core/Type/Array.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs index b11e8949b..07c10ba31 100644 --- a/copilot-core/src/Copilot/Core/Type/Array.hs +++ b/copilot-core/src/Copilot/Core/Type/Array.hs @@ -37,7 +37,7 @@ array xs | datalen == typelen = Array xs | otherwise = error errmsg where datalen = length xs - typelen = fromIntegral $ natVal (Proxy :: Proxy n) + typelen = fromIntegral $ natVal $! (Proxy :: Proxy n) errmsg = "Length of data (" ++ show datalen ++ ") does not match length of type (" ++ show typelen ++ ")." From fa1d30a20a222d551c37a22be7203f71c2a1263e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 08:39:08 -0700 Subject: [PATCH 02/61] copilot-core: Test default functions in `Show` instance for `Array`. Refs #767. The module `copilot-core:Copilot.Core.Type.Array` achieves less than full coverage in the two of the three main categories used by `hpc`, namely "Top Level Definitions" and "Expressions". For the former, only 4 out of 6 definitions are covered, and for the latter, only 47 out of 48. To make Copilot ready for use in future missions, we want to achieve maximum coverage possible. The module `copilot-core:Copilot.Core.Type.Array` includes an instance of the class `Show` for the type `Array`. That instance implicitly declares `showList` and `showsPrec`, set to their default values per the class definition. However, there is no guarantee that the definitions are correct for this specific instance, and `hpc` marks them as not covered unless we explicitly test them, affecting the "Top Level Definitions" score for this library. This commit adds two tests for functions that are implicitly set to their default definitions in the `Show` instance for `Array`. --- .../tests/Test/Copilot/Core/Type/Array.hs | 20 +++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs index e070f138b..0af0ffae9 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs @@ -11,8 +11,9 @@ import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.QuickCheck (Gen, Property, arbitrary, chooseInt, expectFailure, forAll, - getNegative, getNonNegative, oneof, - property, vector, vectorOf) + getNegative, getNonNegative, + listOf, oneof, property, vector, + vectorOf) -- Internal imports: library modules being tested import Copilot.Core.Type.Array (Array, array, arrayElems, arrayUpdate) @@ -31,6 +32,10 @@ tests = testArrayElemsFail , testProperty "Show for arrays" testShowArray + , testProperty "showsPrec for arrays" + testShowsPrecArray + , testProperty "showList for arrays" + testShowListArray , testProperty "arrayElems (arrayUpdate x i v) !! i == v" (testArrayUpdateElem (Proxy :: Proxy 5)) , testProperty "arrayUpdate x i ((arrayElems x) !! i) == x" @@ -70,6 +75,17 @@ testShowArray :: Property testShowArray = forAll (vector 3) $ \l -> property $ show (array l :: Array 3 Int64) == show (l :: [Int64]) +-- | Test 'Show.showsPrec' for 'Array's. +testShowsPrecArray :: Property +testShowsPrecArray = forAll (getNonNegative <$> arbitrary) $ \prec -> + forAll (vector 3) $ \l -> property $ + showsPrec prec (array l :: Array 3 Int64) "" == show (l :: [Int64]) + +-- | Test 'Show.showList' for 'Array's. +testShowListArray :: Property +testShowListArray = forAll (listOf $ vector 3) $ \l -> property $ + showList (map array l :: [Array 3 Int64]) "" == show (l :: [[Int64]]) + -- | Test that updating an array updates the element appropriately (if we -- project that element we get the value we put in). testArrayUpdateElem :: forall n . KnownNat n => Proxy n -> Property From 34cc90741e8b792d8f55ad7e875a3bdcffe4a122 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 11 Oct 2026 17:16:56 -0700 Subject: [PATCH 03/61] copilot-core: Document changes in CHANGELOG. Refs #767. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 1ccbf7db4..33cf7c007 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-11 + * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + 2026-09-07 * Version bump (4.8.1). (#760) From ae91b9ad23ddf0f9313ae9f6e3f5d9352969dfb6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 09:08:19 -0700 Subject: [PATCH 04/61] copilot-core: Fix errors in the documentation of `Copilot.Core.Spec`. Refs #769. The Haddock documentation associated to the type `copilot-core:Copilot.Core.Spec.Stream` contains two grammatical errors. The first is the incorrect use of "in" in the sentence "A stream in an infinite succession of values", which causes the sentence to have no verb, and the second is the use of `Stream` in the second paragraph with no article. To make documentation most useful and in compliance with our style guide, the documentation should have no typos or grammatical errors. This commit fixes both grammatical errors in the documentation of `copilot-core:Copilot.Core.Spec.Stream`, as well as a grammatical error in the top-level documentation of the same module. --- copilot-core/src/Copilot/Core/Spec.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-core/src/Copilot/Core/Spec.hs b/copilot-core/src/Copilot/Core/Spec.hs index 6614d0621..e8972c928 100644 --- a/copilot-core/src/Copilot/Core/Spec.hs +++ b/copilot-core/src/Copilot/Core/Spec.hs @@ -11,9 +11,9 @@ -- and their handling functions, or streams to observe, or a theorem that must -- be proved. -- --- In order to be executed, high-level Copilot Language Spec must be turned --- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core --- representations for Specs and the main types of element in a spec. +-- In order to be executed, a high-level Copilot Language @Spec@ must be +-- turned into a Copilot Core 'Spec'. This module defines the low-level Copilot +-- Core representation for 'Spec' and the main types of element in a spec. module Copilot.Core.Spec ( Stream (..) , Observer (..) @@ -32,9 +32,9 @@ import Data.Typeable (Typeable) import Copilot.Core.Expr (Expr, Id, Name, UExpr) import Copilot.Core.Type (Type, Typed) --- | A stream in an infinite succession of values of the same type. +-- | A stream is an infinite succession of values of the same type. -- --- Stream can carry different types of data. Boolean streams play a special +-- Streams can carry different types of data. Boolean streams play a special -- role: they are used by other parts (e.g., 'Trigger') to detect when the -- properties being monitored are violated. data Stream = forall a . (Typeable a, Typed a) => Stream From ae2dfdb87f54b2288b5e95147830a203bf344382 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 09:09:50 -0700 Subject: [PATCH 05/61] copilot-core: Document changes in CHANGELOG. Refs #769. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 33cf7c007..9e45e6c5b 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,5 +1,6 @@ -2026-10-11 +2026-10-12 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) 2026-09-07 * Version bump (4.8.1). (#760) From d567a73e4f00f126b9ed49b7b6065240fa120014 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:12:14 -0700 Subject: [PATCH 06/61] copilot-core: Replace tab in CHANGELOG. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces a tab in the CHANGELOG of `copilot-core` with spaces. --- copilot-core/CHANGELOG | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 9e45e6c5b..755a52efa 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,5 +1,5 @@ 2026-10-12 - * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) 2026-09-07 From 8f59941cd05980f4c9f4cf8ae77e821e5e1cb03e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:13:31 -0700 Subject: [PATCH 07/61] copilot-bluespec: Replace tabs in `DESIGN.md`. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces tabs in the `DESIGN.md` document of `copilot-bluespec` with spaces. --- copilot-bluespec/DESIGN.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/copilot-bluespec/DESIGN.md b/copilot-bluespec/DESIGN.md index b5a07dd31..6cf5cd610 100644 --- a/copilot-bluespec/DESIGN.md +++ b/copilot-bluespec/DESIGN.md @@ -418,15 +418,15 @@ This generates a Verilog module `mkFibs.v` that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0); + odd_arg0); input CLK; input RST_N; @@ -815,17 +815,17 @@ that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0, + odd_arg0, - fibs); + fibs); input CLK; input RST_N; From de586c06d696053c7d7e5fdd70d99a220aac32c8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:12:42 -0700 Subject: [PATCH 08/61] copilot-interpreter: Replace tab in `Copilot.Interpret.Eval`. Refs #772. Several files across the codebase contain tabs, including the `DESIGN.md` file in `copilot-bluespec`, the `CHANGELOG` for `copilot-core`, and the `Eval` module in `copilot-interpreter`. Per our style guide, we should not use tabs anywhere in code, READMEs or CHANGELOGs, unless strictly necessary. This commit replaces a tab in the module `copilot-interpreter:Copilot.Interpret.Eval` with spaces. --- copilot-interpreter/src/Copilot/Interpret/Eval.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs index 462b5853e..9543806c9 100644 --- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs +++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs @@ -19,7 +19,7 @@ module Copilot.Interpret.Eval import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..), Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..), Trigger (..), Type (..), UExpr (..), Value (..), - arrayElems, arrayUpdate, specObservers, + arrayElems, arrayUpdate, specObservers, specStreams, specTriggers, updateField) import Copilot.Interpret.Error (badUsage) From 9835d834d41bdcea5abc4f83c214af88635c8e0a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:19 -0700 Subject: [PATCH 09/61] copilot-core: Document changes in CHANGELOG. Refs #772. --- copilot-core/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 755a52efa..8ffeafc40 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,6 +1,7 @@ 2026-10-12 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) + * Replace tab in CHANGELOG. (#772) 2026-09-07 * Version bump (4.8.1). (#760) From 1e34f7b0f1e7aadff87c5f77f8ef5042c3e70930 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:30 -0700 Subject: [PATCH 10/61] copilot-bluespec: Document changes in CHANGELOG. Refs #772. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 3b655c5ac..aa122183f 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Replace tabs in `DESIGN.md`. (#772) + 2026-09-07 * Version bump (4.8.1). (#760) * Replace tab in CHANGELOG. (#755) From d00808a471e635c470444edcaaa89478ee9fb0c9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:33:39 -0700 Subject: [PATCH 11/61] copilot-interpreter: Document changes in CHANGELOG. Refs #772. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 3e396d8d4..1b88d8eb7 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Replace tab in `Copilot.Interpreter.Eval`. (#772) + 2026-09-07 * Version bump (4.8.1). (#760) From cfb8974ddb668f047b026241faa50011ed2c5411 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:18:43 -0700 Subject: [PATCH 12/61] copilot: Adjust Travis CI script to flag presence of tabs as an error. Refs #774. The current CI settings do not detect if tabs have been introduced in source code, documentation or CHANGELOGs. That lack of automation makes the accidental introduction of tabs in the code more likely, especially by new users who have not yet configured their editor to replace tabs with spaces. To facilitate keeping Copilot conformant with the style guide, we want to automatically detect when tabs are introduced and warn users accordingly. This commit modifies the Travis CI script to stop with an error if any code, Cabal files, documentation or CHANGELOGs contain any tabs. --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index f157c7aa8..de3f14bb5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,6 +32,9 @@ before_install: - git submodule update --remote script: + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. + - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi + # We explicitly install all libraries so that they are exposed and we can use # them for tests (e.g., with runhaskell). There is no harm in doing this # instead of installing just copilot. From 74a4e39b4e258767a9cea632b0b72e14c44319ee Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 10:34:18 -0700 Subject: [PATCH 13/61] copilot: Document changes in CHANGELOG. Refs #774. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index a838b070a..e7b1e3700 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-12 + * Adjust Travis CI script to flag presence of tabs as an error. (#774) + 2026-09-07 * Version bump (4.8.1). (#760) * Disable secure mode in Cabal in Travis CI. (#753) From 73c31d9de618cb99dd0dfafb47b9db34fec02fa7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 13:54:30 -0700 Subject: [PATCH 14/61] copilot-bluespec: Remove trailing spaces. Refs #775. The module `copilot-bluespec:Copilot.Compile.Bluespec.Expr` contains trailing spaces. It's best to remove them, since those are automatically removed by many editors, leading to PRs containing changes unrelated to the main issues being addressed. In compliance with our coding standard, trailing space should be removed. This commit removes all trailing spaces from `copilot-bluespec:Copilot.Compile.Bluespec.Expr`. --- .../src/Copilot/Compile/Bluespec/Expr.hs | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs index 2b71b3957..84a9ffe7a 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -627,43 +627,43 @@ constInt ty i -- | Translate a Copilot floating-point literal into a Bluespec expression. constFP :: Type ty -> Double -> BS.CExpr constFP ty d - -- Bluespec internally represents all IEEE floating-point values as structs + -- Bluespec internally represents all IEEE floating-point values as structs -- so special symbols have to be called for constructing special values, -- e.g. NaN, inf, and -0.0. See -- https://github.com/B-Lang-org/bsc/blob/main/src/Libraries/Base3-Math/FloatingPoint.bsv#L441 - | isInfinite d = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "infinity") + | isInfinite d = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "infinity") [ if d < 0 - then BS.CCon BS.idTrue [] + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] - - | isNaN d = let - cexpr = BS.CHasType + + | isNaN d = let + cexpr = BS.CHasType ( BS.CLit $ BS.CLiteral BS.NoPos $ BS.LInt $ BS.IntLit Nothing 10 cval ) - ( BS.CQType [] $ BS.TCon $ - BS.TyCon - (BS.mkId BS.NoPos ctype) - Nothing + ( BS.CQType [] $ BS.TCon $ + BS.TyCon + (BS.mkId BS.NoPos ctype) + Nothing BS.TIabstract ) - cval = case ty of - Float -> fromIntegral $ + cval = case ty of + Float -> fromIntegral $ castFloatToWord32 $ uncastDoubleNaNToFloat d - Double -> fromIntegral $ + Double -> fromIntegral $ castDoubleToWord64 d _ -> impossible "constFP" "copilot-bluespec" - ctype = case ty of + ctype = case ty of Float -> "Bit 32" Double -> "Bit 64" _ -> impossible "constFP" "copilot-bluespec" in BS.CApply (BS.CVar $ BS.mkId BS.NoPos "unpack") [cexpr] - | d == 0 = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "zero") - [ if isNegativeZero d - then BS.CCon BS.idTrue [] + | d == 0 = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "zero") + [ if isNegativeZero d + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] | d > 0 = withTypeAnnotation ty $ cLit $ BS.LReal d @@ -676,13 +676,13 @@ constFP ty d [cLit $ BS.LReal $ negate d] -- Because NaNs are specially placed as bit-representations by `constfp` and `constfp` requires Doubles as inputs, --- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload +-- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload -- internals of NaNs so in this case we need a special conversion. uncastDoubleNaNToFloat :: Double -> Float -uncastDoubleNaNToFloat nan = if (isSignaling nan) - then (setPayloadSignaling payload) +uncastDoubleNaNToFloat nan = if (isSignaling nan) + then (setPayloadSignaling payload) else (setPayload payload) - where + where payload = double2Float $ getPayload nan -- | Create a Bluespec expression consisting of a literal. From 78cdf022d05c422358782bcf19fe210d5d69188b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 14:04:03 -0700 Subject: [PATCH 15/61] copilot-bluespec: Document changes in CHANGELOG. Refs #775. --- copilot-bluespec/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index aa122183f..b3cc16e04 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,5 +1,6 @@ 2026-10-12 * Replace tabs in `DESIGN.md`. (#772) + * Remove trailing spaces. (#775) 2026-09-07 * Version bump (4.8.1). (#760) From 64912e909a1023d252e2196eba881fd1e66907dc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 18:29:33 -0700 Subject: [PATCH 16/61] copilot: Adjust Travis CI script to flag trailing space as an error. Refs #777. The current CI settings do not detect if trailing space has been introduced in source code, documentation or CHANGELOGs. That lack of automation makes the accidental introduction of trailing space in the code more likely, especially by new users who have not yet configured their editor to automatically remove trailing spaces. To facilitate keeping Copilot conformant with the style guide, we want to automatically detect when trailing spaces are introduced and warn users accordingly. This commit modifies the Travis CI script to stop with an error if any non-binary files contain any trailing spaces. --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index de3f14bb5..6cf023165 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,6 +32,9 @@ before_install: - git submodule update --remote script: + # Fail if the any non-binary files contain trailing spaces. + - if grep -nIHre ' \+$' * ; then exit 1; fi + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi From 177982b2d4cd653774ceb8fae714126f6a4ce3c9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 12 Oct 2026 18:32:05 -0700 Subject: [PATCH 17/61] copilot: Document changes in CHANGELOG. Refs #777. --- copilot/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index e7b1e3700..f28d79c55 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,5 +1,6 @@ 2026-10-12 * Adjust Travis CI script to flag presence of tabs as an error. (#774) + * Adjust Travis CI script to flag trailing space as an error. (#777) 2026-09-07 * Version bump (4.8.1). (#760) From 2a04a921cff2f492323512fbd9bf6ade6172a7af Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:33 -0700 Subject: [PATCH 18/61] copilot: Use "into" instead of "in" when indicating movement in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit replaces a use of "in" with "into" after a verb that denotes movement or change with direction, which improves the style of the sentence. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 893d6a933..a1f7fd875 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -7,7 +7,7 @@ Copilot is a runtime verification framework for hard real-time systems. Programs can be interpreted for testing, or translated into C99 code to be -incorporated in a project or standalone application. The C99 code generated +incorporated into a project or standalone application. The C99 code generated is constant in memory and time, making it suitable for systems with hard real-time requirements. From e76d6534a876d71075d885678c019bf6d2f7cd93 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:13:31 -0700 Subject: [PATCH 19/61] copilot: Add missing article in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a missing article in a sentence, part of the list of features of Copilot, which is grammatically more correct and reads better. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index a1f7fd875..2d8d4ed5a 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -26,7 +26,7 @@ real-time requirements. - Produce hard real-time C99 runtime monitors that run in constant memory and time. -- Catch errors in specifications early using expressive static type system. +- Catch errors in specifications early using an expressive static type system. - Prove properties about specifications using theorem proving extensions. From e351df801b08221074bb0a65d407b279c86b4faf Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:49 -0700 Subject: [PATCH 20/61] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a comma after the introductory phrase "to use Copilot". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 2d8d4ed5a..49bb8358c 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -98,7 +98,7 @@ ghci> ghci> Leaving GHCi. ### Other Linux distributions On other Linux distributions or older Debian-based distributions, to use -Copilot you must install a Haskell compiler (GHC) and the package manager +Copilot, you must install a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.10 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu, From 73a3444671661c9e83410f8c18aab671c55421ed Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:14:58 -0700 Subject: [PATCH 21/61] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a comma after the introductory phrase "To use Copilot". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 49bb8358c..0cebe449d 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -129,7 +129,7 @@ ghci> ghci> Leaving GHCi. ## Mac installation [(Back to top)](#table-of-contents) -To use Copilot you must have a Haskell compiler (GHC) and the package manager +To use Copilot, you must have a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.6 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/), as well as with Homebrew: From c05161555f1714d1d913ebabde3e87c1373c75fb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 14 Oct 2026 20:21:00 -0700 Subject: [PATCH 22/61] copilot: Fix spelling of Travis CI in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the spelling of "Travis CI". --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 0cebe449d..03ffcf650 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -162,7 +162,7 @@ ghci> ghci> Leaving GHCi. Feel free to open an issue if you are unable to install Copilot following these instructions. -There is a TravisCI file at the root of the repository that may help with +There is a Travis CI file at the root of the repository that may help with troubleshooting the installation. Our issues often include comments with Dockerfiles listing the steps necessary to install Copilot from scratch. From cc42fd662cd6a423f37ffadd892d9c349e5dad5d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:13:37 -0700 Subject: [PATCH 23/61] copilot: Fix discrepancy between pronoun and verb in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes a discrepancy between the number of the pronoun in a sentence ("It") and the verb ("read"). It also adds an article accmpanying temperature, since there is no marker suggesting it refers specifically to the global C variable by that name. --- copilot/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/copilot/README.md b/copilot/README.md index 03ffcf650..ec2c3723b 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -176,8 +176,9 @@ of the main repository. ```haskell -- This example implements a simple home heating system. The system heats --- when the temperature gets too low, and stops when it is high enough. It read --- temperature as a byte (range -50C to 100C) and translates this to Celsius. +-- when the temperature gets too low, and stops when it is high enough. It +-- reads the temperature as a byte (range -50C to 100C) and translates it to +-- Celsius. module Heater where From f32cf04d3e4b9af0ea875c1402b476061143aaa2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:18:34 -0700 Subject: [PATCH 24/61] copilot: Fix capitalization of Copilot in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the capitalization of Copilot referring to the project. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index ec2c3723b..66060e7ca 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -239,7 +239,7 @@ does not constitute any form of endorsement._ built using NASA's Core Flight System or the Robot Operating System (ROS 2). - [arduino-copilot](https://hackage.haskell.org/package/arduino-copilot) - facilitates building copilot applications that run on Arduino. + facilitates building Copilot applications that run on Arduino. - [sketch-frp-copilot](https://hackage.haskell.org/package/sketch-frp-copilot) extends Copilot with an FRP-like interface. From 5d879d850d14d1e8c263cffa6a2759bdd68f7a35 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:18:43 -0700 Subject: [PATCH 25/61] copilot: Fix capitalization of Copilot in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit fixes the capitalization of Copilot referring to the project. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 66060e7ca..7332fd7da 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -245,7 +245,7 @@ does not constitute any form of endorsement._ extends Copilot with an FRP-like interface. - [zephyr-copilot](https://hackage.haskell.org/package/zephyr-copilot) - facilitates building copilot applications that run on boards supported by the + facilitates building Copilot applications that run on boards supported by the Zephyr project. # Documentation From dc3ac33be460111f241e3bec7d3870c791f5e173 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 14 Oct 2026 20:27:36 -0700 Subject: [PATCH 26/61] copilot: Add missing comma in README. Refs #779. The README contains several typos, missing commas, issues with capitalization, and poor wording in some sentences. For example, Copilot is written as `Copilot` in some places, but `copilot` in others, even when referring to the project (as opposed to the library). The sentence "It read temperature as a byte", which accompanies a code example, is grammatically incorrect. To make the README useful and easy to read, we should fix all syntactic and grammatical errors wherever possible. This commit adds a missing comma after an introductory adverb. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 7332fd7da..536665d87 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -391,5 +391,5 @@ https://github.com/Copilot-Language/copilot/graphs/contributors We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work. -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported +Additionally, NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported further development of Copilot. From 12024c6efe5d80bb09d52eebfb78d23b8536a4ee Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 15 Oct 2026 22:12:30 -0700 Subject: [PATCH 27/61] copilot: Document changes in CHANGELOG. Refs #779. --- copilot/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f28d79c55..4758ed15b 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,6 +1,7 @@ -2026-10-12 +2026-10-15 * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) + * Update README to correct typos and improve readability. (#779) 2026-09-07 * Version bump (4.8.1). (#760) From 7c2cbbd99c2bf3d476c2b493f0127a61252a4566 Mon Sep 17 00:00:00 2001 From: Kaveh Zare Date: Fri, 16 Oct 2026 13:30:21 -0500 Subject: [PATCH 28/61] copilot-core: Fix comments for two tests in `Test.Copilot.Core.Type`. Refs #781. The Haddock comments that accompany the properties `testUpdateStruct` and `testUpdateStruct`, included in the test module `copilot-core:Test.Copilot.Core.Type` are incorrect. The comments indicate that the properties test showing a struct, when they are related to updates instead. All Haddock comments should correctly document the functionality implemented in Copilot. This commit fixes the Haddock comments for the aforementioned test properties. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 9f9cb6d5e..128cdea67 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -350,7 +350,7 @@ testShowStruct = forAll arbitrary $ \k1 -> forAll arbitrary $ \k2 -> show (S (Field k1) (Field k2)) == "" --- | Test showing a struct. +-- | Test updating a struct. testUpdateStruct :: Property testUpdateStruct = forAll arbitrary $ \k1 -> @@ -364,7 +364,7 @@ testUpdateStruct = where unField (Field x) = x --- | Test showing a struct. +-- | Test updating a struct (should fail). testUpdateStructFail :: Property testUpdateStructFail = expectFailure $ forAll arbitrary $ \k1 -> From 54f18ef8b755704082929a374ab8700c61eaeb9c Mon Sep 17 00:00:00 2001 From: Kaveh Zare Date: Fri, 16 Oct 2026 13:35:12 -0500 Subject: [PATCH 29/61] copilot-core: Document changes in CHANGELOG. Refs #781. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 8ffeafc40..ad519557c 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,7 +1,8 @@ -2026-10-12 +2026-10-16 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) + * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) 2026-09-07 * Version bump (4.8.1). (#760) From 570cda7fa751149911d0e69f6ab1d9a57b48ccb2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 17 Oct 2026 08:20:18 -0700 Subject: [PATCH 30/61] copilot-core: Fix typo in Haddock comment of test property. Refs #783. The Haddock comment for the property `copilot-core:Test.Copilot.Core.Type.testTypeLength2` states that it tests "that the length of an multi-dimensional array is as expected", which is grammatically incorrect. To make documentation most useful and in compliance with our style guide, the documentation should have no typos or grammatical errors. This commit fixes the aforementioned typo. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 128cdea67..979f87d88 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -165,7 +165,7 @@ testTypeLength1 = property $ typeLength a == 3 a :: Type (Array 3 Int8) a = Array Int8 --- | Test that the length of an multi-dimensional array is as expected. +-- | Test that the length of a multi-dimensional array is as expected. testTypeLength2 :: Property testTypeLength2 = property $ typeLength a == 3 where From 7c9c43fe28bd2cf4d311547fcadf372c646f134e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 18 Oct 2026 09:28:29 -0700 Subject: [PATCH 31/61] copilot-core: Document changes in CHANGELOG. Refs #783. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index ad519557c..b2d405f95 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,8 +1,9 @@ -2026-10-16 +2026-10-17 * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) + * Fix typo in Haddock comment of test property. (#783) 2026-09-07 * Version bump (4.8.1). (#760) From 6046703392ad20ea306b16ab03a7d604a68c0af6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 17 Oct 2026 08:30:23 -0700 Subject: [PATCH 32/61] copilot-core: Fix test to use `typeSize` instead of `typeLength`. Refs #784. The test property `copilot-core:Test.Copilot.Core.Type.testTypeSize1` claims, in its name, in the Haddock comment that accompanies it, and in the property description as part of the property group, that it tests `typeSize`. However, its implementation tests `typeLength`. The property should test the function it is expected to be testing. This commit modifies `copilot-core:Test.Copilot.Core.Type.testTypeSize1` to use `typeSize` instead of `typeLength`. --- copilot-core/tests/Test/Copilot/Core/Type.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 979f87d88..47d8c5940 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -174,7 +174,7 @@ testTypeLength2 = property $ typeLength a == 3 -- | Test that the size of an array is as expected. testTypeSize1 :: Property -testTypeSize1 = property $ typeLength a == 3 +testTypeSize1 = property $ typeSize a == 3 where a :: Type (Array 3 Int8) a = Array Int8 From 1aac617ad5ac27e167ff755e5905c1b0e1c507e6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 18 Oct 2026 11:43:35 -0700 Subject: [PATCH 33/61] copilot-core: Document changes in CHANGELOG. Refs #784. --- copilot-core/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index b2d405f95..c8a3f790d 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -4,6 +4,7 @@ * Replace tab in CHANGELOG. (#772) * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) * Fix typo in Haddock comment of test property. (#783) + * Fix test to use `typeSize` instead of `typeLength` (#784). 2026-09-07 * Version bump (4.8.1). (#760) From 5c32631cb72d51ce8b91802f58b840e2f482d05f Mon Sep 17 00:00:00 2001 From: James Todd Gloyd Date: Fri, 23 Oct 2026 20:54:08 +0000 Subject: [PATCH 34/61] copilot-libraries: Add random stream generation module. Refs #766. Copilot does not currently contain any capability to produce a random stream of values. Randomization is useful for a lot of applications, from testing to fault injection. To make Copilot more versatile and useful for the use cases we want to support, we want to add a module to `copilot-libraries` with randomization primitives. This commit adds a new module that provides functions to produce random streams of different types and with different properties. --- copilot-libraries/copilot-libraries.cabal | 1 + .../src/Copilot/Library/Random.hs | 145 ++++++++++++++++++ 2 files changed, 146 insertions(+) create mode 100644 copilot-libraries/src/Copilot/Library/Random.hs diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index aa5c8e61b..b34020a57 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -51,6 +51,7 @@ library , Copilot.Library.PTLTL , Copilot.Library.StateMachines , Copilot.Library.Statistics + , Copilot.Library.Random , Copilot.Library.RegExp , Copilot.Library.Utils , Copilot.Library.Voting diff --git a/copilot-libraries/src/Copilot/Library/Random.hs b/copilot-libraries/src/Copilot/Library/Random.hs new file mode 100644 index 000000000..d4828e12b --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/Random.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +-- | +-- Basic pseudo-random number generation. +-- +-- Information on performance of a selection of pseudo-random number generation +-- algorithms, including those implemented below, can be found at: +-- https://prng.di.unimi.it/ +-- +-- Important: these pseudo-random number generators are NOT cryptographically +-- secure generators. +module Copilot.Library.Random + ( randomW32 + , randomW64 + , boundedRandomIntegral + , proportionalRandomBool + , weightedRandomSelection + ) + where + +-- External imports +import Copilot.Language (Array, Stream, Typed, Word32, Word64, arrayElems, + constant, mod, mux, (!), (++), (.<<.), (.>>.), (.^.), + (<), (<=)) +import GHC.TypeLits (KnownNat, type (<=)) +import Prelude hiding (mod, (++), (<), (<=)) + +-- | Given two Word32 seeds, produce a pseudo-random stream of Word32 numbers, +-- which has a period of 2^32 - 1. Neither of the seeds should be zero, since +-- the underlying randomization algorithm maps zero to itself. +-- +-- This function uses an Xorshift+ algorithm. +randomW32 :: Word32 -> Word32 -> Stream Word32 +randomW32 0 _ = error "randomW32: seed cannot be zero." +randomW32 _ 0 = error "randomW32: seed cannot be zero." +randomW32 seed1 seed2 = s1 + s2 + + where + + s1 :: Stream Word32 + s1 = [seed1] ++ (xorshift32 s1) + + s2 :: Stream Word32 + s2 = [seed2] ++ (xorshift32 s2) + + -- This is a simple implementation of an Xorshift algorithm + xorshift32 :: Stream Word32 -> Stream Word32 + xorshift32 x1 = x4 -- Note: 0 maps to itself with this + where + x4 = x3 .^. (x3 .<<. (5 :: Stream Word32)) + x3 = x2 .^. (x2 .>>. (17 :: Stream Word32)) + x2 = x1 .^. (x1 .<<. (13 :: Stream Word32)) + +-- | Given two Word64 seeds, produce a pseudo-random stream of Word64 numbers, +-- which has a period of 2^128 - 1. Neither of the seeds should be zero, as +-- doing so will negatively impact the quality of the randomness. +-- +-- This function uses an Xorshiftrplus algorithm. +randomW64 :: Word64 -> Word64 -> Stream Word64 +randomW64 0 _ = error "randomW64: seed cannot be zero." +randomW64 _ 0 = error "randomW64: seed cannot be zero." +randomW64 seed1 seed2 = x + + where + + s0 :: Stream Word64 + s0 = [seed1] ++ s1 + + s1 :: Stream Word64 + s1 = [seed2] ++ (x + s1) + + x :: Stream Word64 + x = xorshiftr128plus s0 s1 + + xorshiftr128plus :: Stream Word64 -> Stream Word64 -> Stream Word64 + xorshiftr128plus x1 y = x4 + where + x4 = x3 .^. y + x3 = x2 .^. (x2 .>>. (17 :: Stream Word64)) + x2 = x1 .^. (x1 .<<. (23 :: Stream Word64)) + +-- | Given a stream of random integral numbers, a minimum value, and a maximum +-- value, produce a stream of random values greater than or equal to the +-- minimum and less than the maximum value, i.e., [@mN@, @mX@). +boundedRandomIntegral :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream a +boundedRandomIntegral gen mN mX = (gen `mod` constant (mX - mN)) + constant mN + +-- | Given a stream of random integral numbers and two integers defining the +-- numerator and denominator of a rational probability, produce a boolean +-- stream that is randomly @True@ with the given probability. That is to say, +-- given a numerator @n@ and denominator @d@, then, over a sufficiently large +-- sample size, the resulting stream @s@ is @True@ @n@ out of @d@ times. +proportionalRandomBool :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream Bool +proportionalRandomBool gen n d = (gen `mod` constant d) < constant n + +-- | Given a stream of random integral numbers, an array of values, and an +-- equal length array of weights, produce a stream of random values from the +-- given array with probabilities proportional to the given weights. +weightedRandomSelection :: forall a b s + . (KnownNat s, s <= MaxWord32, Typed a, Typed b, + Integral a, Bounded a) + => Stream a -> Array s b -> Array s a -> Stream b +weightedRandomSelection gen values weights + | overflow + = error "weightedRandomSelection: sum of weights overflows type" + + | signedType + = error "weightedRandomSelection: type of weights array must be unsigned" + + | otherwise + = constant values ! idx + + where + + -- Check if cumulativeSum decreases at any point. For unsigned integral + -- types, a decreasing element in this cumulative sequence corresponds to + -- an overflow. + overflow = or (zipWith (>) cumulativeSum (drop 1 cumulativeSum)) + + signedType = 0 > (minBound :: a) + + idx :: Stream Word32 + idx = countLeq cumulativeSum (gen `mod` constant totalSum) + + countLeq :: [a] -> Stream a -> Stream Word32 + countLeq xs v = sum [ mux (constant x <= v) 1 0 | x <- xs ] + -- ^ get number of elements in @xs@ less than or equal to @v@. + -- For non-decreasing @xs@, this is equal to the index of the first + -- element greater than @v@. + + cumulativeSum :: [a] + cumulativeSum = scanl1 (+) (arrayElems weights) + + totalSum :: a + totalSum = last cumulativeSum + +-- | Type-level representation of the upper bound on an unsigned 32-bit +-- integer. +type MaxWord32 = 4294967295 -- 2^32 - 1 From 39548759d483719d4554bf8cd2e21adf5a8b21aa Mon Sep 17 00:00:00 2001 From: James Todd Gloyd Date: Fri, 23 Oct 2026 21:04:47 +0000 Subject: [PATCH 35/61] copilot-libraries: Document changes in CHANGELOG. Refs #766. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 0e8dcc83f..b95a2cd3f 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-10-23 + * Add random stream generation module. (#766) + 2026-09-07 * Version bump (4.8.1). (#760) From e6d4b6450f8c90247d7d9f5b105d1cbb9217901d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 May 2026 14:56:02 +0000 Subject: [PATCH 36/61] copilot: Add Github Actions workflow file. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. This commit adds a Github Actions workflow file that replicates the steps executed by Travis CI. --- .github/workflows/build.yml | 66 +++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 000000000..21e929e6c --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,66 @@ +name: build + +# Trigger the workflow on push or pull request +on: + - pull_request + - push + +jobs: + cabal: + name: ${{ matrix.os }} / ghc ${{ matrix.ghc }} / cabal ${{ matrix.cabal }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-26.04] + cabal: ["2.4", "3.2", "3.4"] + ghc: + - "8.6.5" + - "8.8.4" + - "8.10.4" + - "9.0.1" + + steps: + + - uses: haskell-actions/setup@main + id: setup-haskell-cabal + name: Setup Haskell + continue-on-error: true + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Prepare environment + run: | + echo "$HOME/.ghcup/bin" >> $GITHUB_PATH + echo "$HOME/.cabal/bin" >> $GITHUB_PATH + sed -i -e "s;-- \(secure.\) True;\1 False;g" $HOME/.cabal/config + cabal update + + - uses: actions/checkout@v7 + + - name: Install dependencies + run: | + sudo apt-get install -y cppcheck z3 + + - name: Format check + run: | + # Fail if the any non-binary files contain trailing spaces. + if grep -nIHre ' \+$' * ; then exit 1; fi + + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. + if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi + + - name: Install copilot + run: | + cabal v2-install --lib copilot/ copilot-core/ copilot-c99/ copilot-language/ copilot-libraries/ copilot-theorem/ copilot-interpreter/ copilot-prettyprinter/ + + - name: Test packages + if: matrix.ghc == '8.10.4' + run: | + cabal v2-test -j1 copilot-core/ copilot-language/ copilot-interpreter/ copilot-c99/ copilot-theorem/ copilot-libraries/ + + - name: Check cpp + if: matrix.ghc == '8.10.4' + run: | + export GHC_ENVIRONMENT=~/.ghc/x86_64-linux-8.10.4/environments/default + runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c From a39952269a8545c7e71002b53f632336794c4be3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 8 May 2026 14:56:13 +0000 Subject: [PATCH 37/61] copilot: Remove Travis CI file. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. A prior commit added a Github Actions workflow file that replicates the steps executed by Travis CI, thus making the Travis CI setup redundant. This commit removes the Travis CI script from the repository. --- .travis.yml | 58 ----------------------------------------------------- 1 file changed, 58 deletions(-) delete mode 100644 .travis.yml diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 6cf023165..000000000 --- a/.travis.yml +++ /dev/null @@ -1,58 +0,0 @@ -# dist should be at least focal because we need cppcheck >= 1.88. -dist: focal - -# NB: don't set `language: haskell` here - -# The following enables several GHC versions to be tested; often it's enough to -# test only against the last release in a major GHC version. Feel free to omit -# lines listings versions you don't need/want testing for. -env: - - CABALVER=2.4 GHCVER=8.6.5 - - CABALVER=3.2 GHCVER=8.8.4 - - CABALVER=3.2 GHCVER=8.10.4 - - CABALVER=3.4 GHCVER=9.0.1 -# - CABALVER=head GHCVER=head # see section about GHC HEAD snapshots - -# Note: the distinction between `before_install` and `install` is not important. -before_install: - - travis_retry sudo add-apt-repository -y ppa:hvr/ghc - - travis_retry sudo apt-get update - - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex - - # We install z3 and cppcheck only for the tests, since they are not needed - # for normal compilation. - - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3 cppcheck; fi - - - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - - cabal --version - - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]" - - cabal user-config init - - sed -i -e "s;-- \(secure.\) True;\1 False;g" ${HOME}/.cabal/config - - travis_retry cabal update - - git submodule update --remote - -script: - # Fail if the any non-binary files contain trailing spaces. - - if grep -nIHre ' \+$' * ; then exit 1; fi - - # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. - - if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi - - # We explicitly install all libraries so that they are exposed and we can use - # them for tests (e.g., with runhaskell). There is no harm in doing this - # instead of installing just copilot. - - travis_wait 30 cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language copilot-libraries copilot-theorem copilot-interpreter copilot-prettyprinter - - # Run tests only on GHC 8.10.4 - # - # Only libraries with tests are listed below or the v2-test command fails. - # - # Testing copilot-theorem and copilot-libraries requires z3. See above - # conditional installation, and keep GHC version numbers in both places in - # sync. - - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem copilot-libraries; fi - - # Check that the code produced by Copilot complies with MISRA C 2012. We - # explicitly make cppcheck produce a non-zero exit code on non-compliance - # with the standard to make the CI build fail. - - if [ "${GHCVER}" == "8.10.4" ]; then runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c; fi From b0e6e698ded581bdb49c7d7e0ac6196e39cab2b8 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 21:01:56 +0000 Subject: [PATCH 38/61] copilot: Replace Travis CI badge with Github Actions badge in README. Refs #790. CI jobs are being automatically cancelled by Travis CI mid-build. Travis CI is reporting the plan as being out of credits, when the organization have plenty of credits to run jobs to completion. Prior commits replaced the Travis CI-based setup with one based on Github Actions. This commit updates the Travis CI build status badge in the `README.md` to reflect the build status of the `master` branch on Github Actions, and to point to the corresponding workflow file. --- copilot/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot/README.md b/copilot/README.md index 536665d87..63a2459ef 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -2,7 +2,7 @@ # Copilot -[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) +[![Build Status](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml/badge.svg?branch=master)](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml) [![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](https://hackage.haskell.org/package/copilot) Copilot is a runtime verification framework for hard real-time systems. From 701880b127fadd9d94f9f8c73ec44ba791d42775 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 21:27:02 +0000 Subject: [PATCH 39/61] copilot: Document changes in CHANGELOG. Refs #790. --- copilot/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 4758ed15b..c350ec33a 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,7 +1,8 @@ -2026-10-15 +2026-11-07 * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) * Update README to correct typos and improve readability. (#779) + * Replace Travis CI with Github Actions. (#790) 2026-09-07 * Version bump (4.8.1). (#760) From 1a137a86d5a8459750d3092e28679cb326e868d2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 40/61] copilot-core: Version bump (4.8.2). Refs #792. --- 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 57f92d703..288399a9c 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.8.1 +version: 4.8.2 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From c666b71483eaf5889f53fa82d588d991bc123e35 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 41/61] copilot-bluespec: Version bump (4.8.2). Refs #792. --- copilot-bluespec/copilot-bluespec.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index e8f29e4d7..1d8f7b3af 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.8.1 +version : 4.8.2 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,7 +51,7 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From fd210f80474c58044014aaa8bf5014aeffa1ef16 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 42/61] copilot-c99: Version bump (4.8.2). Refs #792. --- 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 ea2e233dc..7e1e3d17a 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.8.1 +version : 4.8.2 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.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From c2b0269f9838f21e08e040e4bcb39635fd683eb0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 43/61] copilot-prettyprinter: Version bump (4.8.2). Refs #792. --- 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 d6c2bcc11..35c5c7d7c 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: From d17de87e12bc1a7ba2f4bf4e26ec83e03d768c81 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 44/61] copilot-interpreter: Version bump (4.8.2). Refs #792. --- 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 538237a10..60152a66a 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: From 8e714c714950405f568b5e2ebb2f1a3e15ebc04e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 45/61] copilot-theorem: Version bump (4.8.2). Refs #792. --- 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 cf3e8c44c..da29f566a 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.8.1 +version : 4.8.2 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.8.1 && < 4.9 - , copilot-prettyprinter >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 1f67ea0f33b69c775f25dd21d48c540d95e0ac45 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 46/61] copilot-language: Version bump (4.8.2). Refs #792. --- 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 b30c29db6..40ba65f2c 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 - , copilot-interpreter >= 4.8.1 && < 4.9 - , copilot-theorem >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-interpreter >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From c97769b18999b8be9b673726817123466bf1c4e9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 47/61] copilot-libraries: Version bump (4.8.2). Refs #792. --- 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 b34020a57..6e18aba84 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.8.1 +version: 4.8.2 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.8.1 && < 4.9 + , copilot-language >= 4.8.2 && < 4.9 exposed-modules: Copilot.Library.Analysis From dabb5562b912ae11074e2db5a3610c5a9c296bb6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 48/61] copilot-verifier: Version bump (4.8.2). Refs #792. --- 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 4052ee006..bcf1061bf 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.8.1 +Version: 4.8.2 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.8.1 && < 4.9, - copilot-core >= 4.8.1 && < 4.9, - copilot-theorem >= 4.8.1 && < 4.9, + copilot-c99 >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-theorem >= 4.8.2 && < 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.8.1 && < 4.9, - copilot-language >= 4.8.1 && < 4.9, - copilot-libraries >= 4.8.1 && < 4.9, - copilot-prettyprinter >= 4.8.1 && < 4.9, + copilot >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9, + copilot-libraries >= 4.8.2 && < 4.9, + copilot-prettyprinter >= 4.8.2 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples From a9847388d62d2b725acf1c521ce5b31efc9af989 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 49/61] copilot-visualizer: Version bump (4.8.2). Refs #792. --- copilot-visualizer/copilot-visualizer.cabal | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index 3b1d539eb..34d2289bd 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.8.1 +version: 4.8.2 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.8.1 && < 4.9, - copilot-core >= 4.8.1 && < 4.9, - copilot-interpreter >= 4.8.1 && < 4.9, - copilot-language >= 4.8.1 && < 4.9 + copilot >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-interpreter >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.8.1 && < 4.9, + copilot >= 4.8.2 && < 4.9, copilot-visualizer if flag(examples) From 82d2e07f507e688a8ab5415a9b469787f84fa904 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:38:42 -0800 Subject: [PATCH 50/61] copilot: Version bump (4.8.2). Refs #792. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 5fa90035e..00a495e3f 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.8.1 +version: 4.8.2 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.8.1 && < 4.9 - , copilot-theorem >= 4.8.1 && < 4.9 - , copilot-language >= 4.8.1 && < 4.9 - , copilot-libraries >= 4.8.1 && < 4.9 - , copilot-c99 >= 4.8.1 && < 4.9 - , copilot-prettyprinter >= 4.8.1 && < 4.9 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 + , copilot-language >= 4.8.2 && < 4.9 + , copilot-libraries >= 4.8.2 && < 4.9 + , copilot-c99 >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main From 9a6a2d4ebc52fa54fb7f090624c44b7ca6c8797e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 51/61] copilot-core: Document changes in CHANGELOG. Refs #792. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index c8a3f790d..033129dbc 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-17 +2026-11-07 + * Version bump (4.8.2). (#792) * Increase test coverage for `Copilot.Core.Type.Array`. (#767) * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) * Replace tab in CHANGELOG. (#772) From 8511f4801141ff2773a1787cb9d51e97e6523b33 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 52/61] copilot-bluespec: Document changes in CHANGELOG. Refs #792. --- copilot-bluespec/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index b3cc16e04..b5130fa0b 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-12 +2026-11-07 + * Version bump (4.8.2). (#792) * Replace tabs in `DESIGN.md`. (#772) * Remove trailing spaces. (#775) From 3096f9356cc298409b2c2beb909f5cbdff38458b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 53/61] copilot-c99: Document changes in CHANGELOG. Refs #792. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 2caf70ef2..b53dcc838 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From c8e5d846f393ff4c60c079c510a6e4ca3cbb7ec3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 54/61] copilot-prettyprinter: Document changes in CHANGELOG. Refs #792. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 799783ce8..bbe715c47 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 3b79a5b0213f85ca0dd3a904afa474a00f9562d3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 55/61] copilot-interpreter: Document changes in CHANGELOG. Refs #792. --- copilot-interpreter/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 1b88d8eb7..55cdec51c 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-12 +2026-11-07 + * Version bump (4.8.2). (#792) * Replace tab in `Copilot.Interpreter.Eval`. (#772) 2026-09-07 From c6dcc87d50db4d3d33ecc7755d4fc4476413401c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 56/61] copilot-theorem: Document changes in CHANGELOG. Refs #792. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 251b49484..0207c5446 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) * Remove unnecessary extension. (#733) From 184eaeaa68300f3a303cb92d678ead8ae89acc2b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 57/61] copilot-language: Document changes in CHANGELOG. Refs #792. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 49162ceb0..4aacc9e2e 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 1efa2d78fd4f4d40cadd36e0721b9020806cc202 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 58/61] copilot-libraries: Document changes in CHANGELOG. Refs #792. --- copilot-libraries/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index b95a2cd3f..f84c75a48 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,4 +1,5 @@ -2026-10-23 +2026-11-07 + * Version bump (4.8.2). (#792) * Add random stream generation module. (#766) 2026-09-07 From 090ff4e6dd4914cd10497452de6970d23f84c5b5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 59/61] copilot-verifier: Document changes in CHANGELOG. Refs #792. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 1dec1cfd0..c69ccd708 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) From 11c0601e795f40db74538cc0d52c41f2810ebdf3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 60/61] copilot-visualizer: Document changes in CHANGELOG. Refs #792. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 9d772eca0..b578bedb9 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + 2026-09-07 * Version bump (4.8.1). (#760) * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) From 8049dbb1e8aea3b123ca54be5a285bd1950ea2c6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 7 Nov 2026 17:41:22 -0800 Subject: [PATCH 61/61] copilot: Document changes in CHANGELOG. Refs #792. --- copilot/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index c350ec33a..8b691705e 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,4 +1,5 @@ 2026-11-07 + * Version bump (4.8.2). (#792) * Adjust Travis CI script to flag presence of tabs as an error. (#774) * Adjust Travis CI script to flag trailing space as an error. (#777) * Update README to correct typos and improve readability. (#779)