diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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 - * 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) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 [(Back to top)](#table-of-contents) -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 #.` + at the end of the subject line of each commit message, in *every commit*. + Replace `` 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 [(Back to top)](#table-of-contents) diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -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 diff --git a/examples/Structs.hs b/examples/Structs.hs --- a/examples/Structs.hs +++ b/examples/Structs.hs @@ -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 diff --git a/examples/StructsUpdateField.hs b/examples/StructsUpdateField.hs new file mode 100644 --- /dev/null +++ b/examples/StructsUpdateField.hs @@ -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' diff --git a/examples/what4/Propositional.hs b/examples/what4/Propositional.hs --- a/examples/what4/Propositional.hs +++ b/examples/what4/Propositional.hs @@ -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 diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs --- a/examples/what4/Structs.hs +++ b/examples/what4/Structs.hs @@ -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