copilot 4.0 → 4.1
raw patch · 7 files changed
+321/−39 lines, 7 filesdep ~copilot-c99dep ~copilot-coredep ~copilot-languagenew-component:exe:structs-update-fieldPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +16/−7
- README.md +68/−5
- copilot.cabal +19/−7
- examples/Structs.hs +7/−0
- examples/StructsUpdateField.hs +159/−0
- examples/what4/Propositional.hs +45/−20
- examples/what4/Structs.hs +7/−0
CHANGELOG view
@@ -1,3 +1,12 @@+2024-11-07+ * Version bump (4.1). (#561)+ * Update contribution guidelines. (#476)+ * Update README with missing publications. (#544)+ * Make the what4-propositional example's comments match results. (#535)+ * Add example describing how to implement updateField. (#525)+ * Standardize changelog format. (#550)+ * Add installation instructions for Fedora 40 and up. (#542)+ 2024-09-07 * Version bump (4.0). (#532) * Update example to demonstrate struct update support. (#524)@@ -117,11 +126,11 @@ 2020-12-06 * Update optparse-applicative dependency version for newer base- versions. (#61).- * Add Ivan Perez as co-maintainer (#51).- * Update description in cabal file to match copilot-core (#50).+ versions. (#61)+ * Add Ivan Perez as co-maintainer. (#51)+ * Update description in cabal file to match copilot-core. (#50) -2019-11-22 Ivan Perez <ivan.perez@nianet.org>- * Version bump (3.1).- * Update multiple examples (#41).- * Update instructions to match new repositry name (#45).+2019-11-22+ * Version bump (3.1). (#46)+ * Update multiple examples. (#41)+ * Update instructions to match new repositry name. (#45)
README.md view
@@ -76,6 +76,25 @@ ghci> ghci> Leaving GHCi. ``` +### Fedora 40++On Fedora 40 or newer, Copilot can be installed directly from the package+repositories with:++```sh+$ sudo dnf install ghc-copilot-devel+```++To test that Copilot is available, execute the following:+```sh+$ ghci <<< 'import Language.Copilot'+```++It should end with a line like the following and not print any error messages:+```sh+ghci> ghci> Leaving GHCi.+```+ ### Other Linux distributions On other Linux distributions or older Debian-based distributions, to use@@ -257,6 +276,28 @@ Other relevant papers include: +- [Runtime Verification in Real-Time with the Copilot Language: A Tutorial](https://link.springer.com/chapter/10.1007/978-3-031-71177-0_27)++- [Trustworthy Runtime Verification via Bisimulation (Experience Report)](https://dl.acm.org/doi/abs/10.1145/3607841)++- [An Introduction to Copilot](https://copilot-language.github.io/downloads/copilot_tutorial.pdf)++- [Assuring the Guardians](https://link.springer.com/chapter/10.1007/978-3-319-23820-3_6)++- [Experience report: a do-it-yourself high-assurance compiler](https://dl.acm.org/doi/abs/10.1145/2364527.2364553)++- [Compiling an Haskell EDSL to C: A new C back-end for the Copilot runtime verification framework](https://studenttheses.uu.nl/handle/20.500.12932/29176)++- [Challenges in High-Assurance Runtime Verification](https://link.springer.com/chapter/10.1007/978-3-319-47166-2_31)++- [Runtime Monitoring On Hard Real-Time Operating Systems](http://hdl.handle.net/10342/4999)++- [Design and Testing of an Approach to Automated In-Flight Safety Risk Management for sUAS Operations](https://ntrs.nasa.gov/citations/20220005948)++- [The Essence of Reactivity](https://dl.acm.org/doi/10.1145/3609026.3609727)++- [Types that Change: The Extensible Type Design Pattern](https://dl.acm.org/doi/abs/10.1145/3609025.3609475)+ - [Automated Translation of Natural Language Requirements to Runtime Monitors](https://link.springer.com/chapter/10.1007/978-3-030-99524-9_21) - [Copilot: A Hard Real-Time Runtime Monitor](https://link.springer.com/chapter/10.1007/978-3-642-16612-9_26)@@ -281,12 +322,34 @@ # Contributions <sup>[(Back to top)](#table-of-contents)</sup> -Copilot cannot accept pull requests or code contributions from developers-outside the development team at this point.+We'd love to receive your contributions, be it code fixes, new features, bug+reports, discussions, or anything else that can help the Copilot project. -If you have a question, find a bug, or would like to request a change, please-file an issue adding as much information as you can to help us reproduce the-error or identify the use case. Please file the issue with no labels.+If you have any comments, questions, ideas, or other topics that you think may+be of interest, start a new discussion+[here](https://github.com/Copilot-Language/copilot/discussions).++If you would like to contribute a fix for an issue, please comment on the issue+indicating that you want to fix it so that we can assign it to you and track+the status on our end. If the issue does not exist, create it first or ask that+an existing discussion be promoted to an issue.++If you are unsure about whether your submission should be filed as an issue or+as a discussion, file it as a discussion. We can always move it later.++To facilitate merging any pull requests that you send, please:+- Reference the issue you are addressing with the text `Refs #<ISSUENUMBER>.`+ at the end of the subject line of each commit message, in *every commit*.+ Replace `<ISSUENUMBER>` with the number of the specific issue that your pull+ request is addressing.+- Describe what each commit does individually *in the commit's message*. It's+ best to err on the side of being more descriptive than less.+- Update the CHANGELOGs in the *last commit(s)*.++You can take a look at the repository's [commit+history](https://github.com/Copilot-Language/copilot/commits/master/) to better+understand the process we follow. Click on each commit to see how we write+commit messages. # Acknowledgements <sup>[(Back to top)](#table-of-contents)</sup>
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 4.0+version: 4.1 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -52,12 +52,12 @@ , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 - , copilot-core >= 4.0 && < 4.1- , copilot-theorem >= 4.0 && < 4.1- , copilot-language >= 4.0 && < 4.1- , copilot-libraries >= 4.0 && < 4.1- , copilot-c99 >= 4.0 && < 4.1- , copilot-prettyprinter >= 4.0 && < 4.1+ , copilot-core >= 4.1 && < 4.2+ , copilot-theorem >= 4.1 && < 4.2+ , copilot-language >= 4.1 && < 4.2+ , copilot-libraries >= 4.1 && < 4.2+ , copilot-c99 >= 4.1 && < 4.2+ , copilot-prettyprinter >= 4.1 && < 4.2 exposed-modules: Language.Copilot, Language.Copilot.Main@@ -197,6 +197,18 @@ executable structs main-is: Structs.hs+ hs-source-dirs: examples+ build-depends: base >= 4.9 && < 5+ , copilot+ , copilot-c99+ default-language: Haskell2010+ if flag(examples)+ buildable: True+ else+ buildable: False++executable structs-update-field+ main-is: StructsUpdateField.hs hs-source-dirs: examples build-depends: base >= 4.9 && < 5 , copilot
examples/Structs.hs view
@@ -23,6 +23,11 @@ toValues volts = [ Value Word16 (numVolts volts) , Value Bool (flag volts) ]+ -- Note that we do not implement `updateField` here. `updateField` is only+ -- needed to make updates to structs work in the Copilot interpreter, and we+ -- do not use the interpreter in this example. (See+ -- `examples/StructsUpdateField.hs` for an example that does implement+ -- `updateField`.) -- | `Volts` instance for `Typed`. instance Typed Volts where@@ -41,6 +46,8 @@ , Value typeOf (volts battery) , Value typeOf (other battery) ]+ -- Note that we do not implement `updateField` here for the same reasons as in+ -- the `Struct Volts` instance above. -- | `Battery` instance for `Typed`. Note that `undefined` is used as an -- argument to `Field`. This argument is never used, so `undefined` will never
+ examples/StructsUpdateField.hs view
@@ -0,0 +1,159 @@+-- | An example showing how specifications involving structs (in particular,+-- nested structs) are interpreted and how they are compiled to C using+-- copilot-c99.++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Main where++import qualified Prelude as P+import Control.Monad (void, forM_)+import Data.Proxy (Proxy(..))+import Data.Type.Equality (TestEquality(..), (:~:)(..))+import GHC.TypeLits (sameSymbol)++import Language.Copilot+import Copilot.Compile.C99++-- | Definition for `Volts`.+data Volts = Volts+ { numVolts :: Field "numVolts" Word16+ , flag :: Field "flag" Bool+ }++-- | `Struct` instance for `Volts`.+instance Struct Volts where+ typeName _ = "volts"+ toValues volts = [ Value Word16 (numVolts volts)+ , Value Bool (flag volts)+ ]+ -- In order to run struct updates (as used in the "equalityStructUpdate"+ -- trigger below) in the Copilot interpreter, we must implement the+ -- `updateField` method. To do so, we must check to see if the supplied+ -- `Value` has a `Field` with the same name and type as a field in `Volts`.+ updateField volts (Value fieldTy (field :: Field fieldName a))+ -- For each field in `Volts`, we must:+ --+ -- 1. Check that the field names match using `sameSymbol`. Here,+ -- "numVolts" is the expected name, and `fieldName` is the actual name+ -- that is supplied as an argument to `updateField`. If the check+ -- succeeds, then the `sameSymbol` function will return `Just p`, where+ -- `p` is proof that the two names are the same.+ | Just Refl <- sameSymbol (Proxy @"numVolts") (Proxy @fieldName)+ -- 2. Check that the field types match using `testEquality`. Here,+ -- `Word16` is the expected type, and `fieldTy` is the actual type that+ -- is supplied as an argument. Again, `testEquality` will return `Just+ -- p` (where `p` is a proof) if the two are the same.+ , Just Refl <- testEquality Word16 fieldTy+ -- 3. If both of the checks above succeed, then we can update the field's+ -- value using a record update.+ = volts { numVolts = field }++ -- It is possible that the `Value` passed as an argument could correspond+ -- to any of the fields in `Volts`, so we must repeat this process for+ -- the `flag` field as well.+ | Just Refl <- sameSymbol (Proxy @fieldName) (Proxy @"flag")+ , Just Refl <- testEquality fieldTy Bool+ = volts { flag = field }++ -- If the supplied `Value` does not correspond to any field in `Volts`,+ -- then something went wrong in the Copilot interpreter. This case reports+ -- this as an error.+ | otherwise+ = error $ "Unexpected field: " P.++ show field++-- | `Volts` instance for `Typed`.+instance Typed Volts where+ typeOf = Struct (Volts (Field 0) (Field False))++data Battery = Battery+ { temp :: Field "temp" Word16+ , volts :: Field "volts" (Array 10 Volts)+ , other :: Field "other" (Array 10 (Array 5 Word32))+ }++-- | `Battery` instance for `Struct`.+instance Struct Battery where+ typeName _ = "battery"+ toValues battery = [ Value typeOf (temp battery)+ , Value typeOf (volts battery)+ , Value typeOf (other battery)+ ]+ -- We implement `updateField` similarly to how we implement it in the+ -- `Struct Volts` instance above.+ updateField battery (Value fieldTy (field :: Field fieldName a))+ | Just Refl <- sameSymbol (Proxy @fieldName) (Proxy @"temp")+ , Just Refl <- testEquality fieldTy Word16+ = battery { temp = field }++ | Just Refl <- sameSymbol (Proxy @fieldName) (Proxy @"volts")+ -- Note that writing out the full `Type` for `Volts` is somewhat verbose,+ -- so we make use of the `Typed Volts` instance and write `typeOf @Volts`+ -- instead.+ , Just Refl <- testEquality fieldTy (Array @10 (typeOf @Volts))+ = battery { volts = field }++ | Just Refl <- sameSymbol (Proxy @fieldName) (Proxy @"other")+ , Just Refl <- testEquality fieldTy (Array @10 (Array @5 Word32))+ = battery { other = field }++ | otherwise+ = error $ "Unexpected field: " P.++ show field++-- | `Battery` instance for `Typed`. Note that `undefined` is used as an+-- argument to `Field`. This argument is never used, so `undefined` will never+-- throw an error.+instance Typed Battery where+ typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))++spec :: Spec+spec = do+ let voltsValue :: Volts+ voltsValue =+ Volts+ { numVolts = Field 42+ , flag = Field True+ }++ batteryValue :: Battery+ batteryValue =+ Battery+ { temp = Field 0+ , volts = Field (array (replicate 10 voltsValue))+ , other = Field (array (replicate 10 (array (replicate 5 0))))+ }++ battery :: Stream Battery+ battery = extern "battery" (Just [batteryValue])++ -- Check equality, indexing into nested structs and arrays. Note that this is+ -- trivial by equality.+ trigger "equalitySameIndex"+ ((((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts))+ [arg battery]++ -- Same as previous example, but get a different array index (so should be+ -- false).+ trigger "equalityDifferentIndices"+ ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4))+ [arg battery]++ -- Update a struct field, then check it for equality.+ let batteryTemp1, batteryTemp2 :: Stream Word16+ batteryTemp1 = (battery ## temp =$ (+1))#temp+ batteryTemp2 = battery#temp + 1+ trigger "equalityStructUpdate"+ (batteryTemp1 == batteryTemp2)+ [arg battery, arg batteryTemp1, arg batteryTemp2]++main :: IO ()+main = do+ -- Run the specification using the Copilot interpreter.+ interpret 1 spec++ -- Compile the specification to C.+ spec' <- reify spec+ compile "structs" spec'
examples/what4/Propositional.hs view
@@ -11,40 +11,65 @@ spec :: Spec spec = do+ -- * Non-inductive propositions+ -- The constant value true, which is translated as the corresponding SMT- -- boolean literal.+ -- boolean literal (and is therefore provable). void $ prop "Example 1" (forAll true) -- The constant value false, which is translated as the corresponding SMT- -- boolean literal.+ -- boolean literal (and is therefore not provable). void $ prop "Example 2" (forAll false) - -- An inductively defined flavor of true, which requires induction to prove,- -- and hence is found to be invalid by the SMT solver (since no inductive- -- hypothesis is made).+ -- An "a or not a" proposition which does not require any sort of inductive+ -- argument (but see examples 5 and 6 below for versions that do require+ -- induction to solve). This is easily proven.+ let a = [False] ++ b+ b = not a+ void $ prop "Example 3" (forAll (a || b))++ -- An "a or not a" proposition using external streams, which is also provable.+ let a = extern "a" Nothing+ void $ prop "Example 4" (forAll (a || not a))++ -- * Simple inductive propositions+ --+ -- While Copilot.Theorem.What4 is not able to solve all inductive propositions+ -- in general (see the "Complex inductive propositions" section below), the+ -- following inductive propositions are simple enough that the heuristics in+ -- Copilot.Theorem.What4 can solve them without issue.++ -- An inductively defined flavor of true. let a = [True] ++ a- void $ prop "Example 3" (forAll a)+ void $ prop "Example 5" (forAll a) - -- An inductively defined "a or not a" proposition, which is unprovable by- -- the SMT solver.+ -- An inductively defined "a or not a" proposition (i.e., a more complex+ -- version of example 3 above). let a = [False] ++ b b = [True] ++ a- void $ prop "Example 4" (forAll (a || b))-- -- A version of "a or not a" proposition which does not require any sort of- -- inductive argument, and hence is provable.- let a = [False] ++ b- b = not a- void $ prop "Example 5" (forAll (a || b))+ void $ prop "Example 6" (forAll (a || b)) - -- A bit more convoluted version of Example 5, which is provable.+ -- A bit more convoluted version of example 6. let a = [True, False] ++ b b = [False] ++ not (drop 1 a)- void $ prop "Example 6" (forAll (a || b))+ void $ prop "Example 7" (forAll (a || b)) - -- An example using external streams.- let a = extern "a" Nothing- void $ prop "Example 7" (forAll (a || not a))+ -- * Complex induction propositions+ --+ -- The heuristics in Copilot.Theorem.What4 are not able to prove these+ -- inductive propositions, so these will be reported as unprovable, even+ -- though each proposition is actually provable.++ -- An inductively defined flavor of true (i.e., a more complex version of+ -- example 5 above).+ let a = [True] ++ ([True] ++ ([True] ++ a))+ void $ prop "Example 8" (forAll a)++ -- An inductively defined "a or not a" proposition (i.e., a more complex+ -- version of example 6 above).+ let a = [False] ++ ([False] ++ ([False] ++ b))+ b = [True] ++ ([True] ++ ([True] ++ a))+ void $ prop "Example 9" (forAll (a || b)) main :: IO () main = do
examples/what4/Structs.hs view
@@ -24,6 +24,11 @@ toValues volts = [ Value Word16 (numVolts volts) , Value Bool (flag volts) ]+ -- Note that we do not implement `updateField` here. `updateField` is only+ -- needed to make updates to structs work in the Copilot interpreter, and we+ -- do not use the interpreter in this example. (See+ -- `examples/StructsUpdateField.hs` for an example that does implement+ -- `updateField`.) -- | `Volts` instance for `Typed`. instance Typed Volts where@@ -42,6 +47,8 @@ , Value typeOf (volts battery) , Value typeOf (other battery) ]+ -- Note that we do not implement `updateField` here for the same reasons as in+ -- the `Struct Volts` instance above. -- | `Battery` instance for `Typed`. Note that `undefined` is used as an -- argument to `Field`. This argument is never used, so `undefined` will never