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 diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index f157c7aa8..000000000 --- a/.travis.yml +++ /dev/null @@ -1,52 +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: - # 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 diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 3b655c5ac..b5130fa0b 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,8 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Replace tabs in `DESIGN.md`. (#772) + * Remove trailing spaces. (#775) + 2026-09-07 * Version bump (4.8.1). (#760) * Replace tab in CHANGELOG. (#755) 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; 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 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. 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) 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 diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 1ccbf7db4..033129dbc 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,12 @@ +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) + * 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) 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. 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 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 ++ ")." diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 9f9cb6d5e..47d8c5940 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 @@ -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 @@ -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 -> 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 diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 3e396d8d4..55cdec51c 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,7 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Replace tab in `Copilot.Interpreter.Eval`. (#772) + 2026-09-07 * Version bump (4.8.1). (#760) 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: 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) 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) 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 diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 0e8dcc83f..f84c75a48 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,7 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Add random stream generation module. (#766) + 2026-09-07 * Version bump (4.8.1). (#760) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index aa5c8e61b..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 @@ -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 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) 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: 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) 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 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) 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 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) 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) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index a838b070a..8b691705e 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,10 @@ +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) + * Replace Travis CI with Github Actions. (#790) + 2026-09-07 * Version bump (4.8.1). (#760) * Disable secure mode in Cabal in Travis CI. (#753) diff --git a/copilot/README.md b/copilot/README.md index 893d6a933..63a2459ef 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -2,12 +2,12 @@ # 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. 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. @@ -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. @@ -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, @@ -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: @@ -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. @@ -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 @@ -238,13 +239,13 @@ 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. - [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 @@ -390,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. 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