copilot 3.7 → 4.8
raw patch · 19 files changed
Files
- CHANGELOG +130/−7
- README.md +315/−115
- copilot.cabal +39/−11
- examples/AddMult.hs +0/−2
- examples/Array.hs +16/−4
- examples/Cast.hs +0/−2
- examples/Clock.hs +0/−2
- examples/Counter.hs +3/−4
- examples/Engine.hs +5/−8
- examples/Heater.hs +2/−4
- examples/Structs.hs +28/−26
- examples/StructsUpdateField.hs +161/−0
- examples/Voting.hs +0/−2
- examples/WCV.hs +3/−19
- examples/what4/Arithmetic.hs +6/−7
- examples/what4/ArithmeticCounterExamples.hs +110/−0
- examples/what4/Propositional.hs +46/−22
- examples/what4/Structs.hs +33/−27
- src/Language/Copilot/Main.hs +18/−12
CHANGELOG view
@@ -1,3 +1,126 @@+2026-07-07+ * Version bump (4.8). (#745)++2026-05-07+ * Version bump (4.7.1). (#730)++2026-03-07+ * Version bump (4.7). (#714)++2026-01-07+ * Version bump (4.6.1). (#705)+ * Relax version constraint on optparse-applicative. (#603)++2025-11-07+ * Version bump (4.6). (#679)++2025-09-07+ * Version bump (4.5.1). (#666)+ * Add hello world example for FPGA. (#657)++2025-07-07+ * Version bump (4.5). (#642)++2025-05-07+ * Version bump (4.4). (#618)+ * Update build status badge URL. (#612)++2025-03-07+ * Version bump (4.3). (#604)+ * Include missing dependencies in installation instructions. (#591)+ * Update version of GHC in README. (#590)+ * Add example of how to use proveWithCounterExample. (#589)+ * List all Copilot packages in installation command in README. (#597)++2025-01-07+ * Version bump (4.2). (#577)+ * Bump upper version constraint on filepath. (#570)+ * Update struct examples to use generic method implementations. (#564)++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)+ * Update example to demonstrate array update support. (#36)++2024-07-07+ * Version bump (3.20). (#522)+ * Update README to reflect support for GHC 9.8. (#518)++2024-05-07+ * Version bump (3.19.1). (#512)++2024-03-07+ * Version bump (3.19). (#504)++2024-01-07+ * Version bump (3.18.1). (#493)+ * Update README to reflect support for GHC 9.6. (#491)++2024-01-07+ * Version bump (3.18). (#487)+ * Enable tests for copilot-theorem in CI script. (#474)+ * Enable tests for copilot-libraries in CI script. (#475)+ * Replace uses of forall with forAll. (#470)+ * Update CI job to check for MISRA compliance with cppcheck. (#472)+ * Relax version constraint on optparse-applicative. (#488)++2023-11-07+ * Version bump (3.17). (#466)+ * Replace uses of deprecated functions. (#457)++2023-11-03+ * Fix typo in README. (#459)++2023-09-07+ * Version bump (3.16.1). (#455)++2023-07-07+ * Version bump (3.16). (#448)++2023-05-07+ * Version bump (3.15). (#438)++2023-03-07+ * Version bump (3.14). (#422)+ * Replace import of Copilot.Language.prettyPrint. (#412)+ * Re-structure README. (#415)+ * Update README to reflect support for GHC 9.4. (#423)++2023-01-07+ * Version bump (3.13). (#406)++2022-11-07+ * Version bump (3.12). (#389)++2022-09-07+ * Version bump (3.11). (#376)++2022-07-07+ * Version bump (3.10). (#356)+ * Run tests in CI. (#329)+ * Remove duplicated compiler option. (#328)+ * Fix typos in README and Heater example. (#352)+ * Relax version bounds of dependencies. (#335)+ * Update repo info in cabal file. (#333)++2022-05-06+ * Version bump (3.9). (#320)+ * Compliance with style guide (partial). (#316)+ * Add support for GHC 9.0. (#294)++2022-03-07+ * Version bump (3.8). (#298)+ * Mark package as uncurated to avoid modification. (#288)+ 2022-01-07 * Version bump (3.7). (#287) * Add example with nested structs. (#275)@@ -42,11 +165,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
@@ -1,89 +1,183 @@-# Copilot: Stream DSL for hard real-time runtime verification+<div align="center"> -[](https://app.travis-ci.com/github/Copilot-Language/copilot)-[](https://hackage.haskell.org/package/copilot)+# Copilot -Copilot is a runtime verification framework written in Haskell. It allows the-user to write programs in a simple but powerful way using a stream-based-approach.+[](https://app.travis-ci.com/github/Copilot-Language/copilot)+[](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 as a standalone application. The C99 backend-output is constant in memory and time, making it suitable for systems with hard-realtime requirements.+incorporated in 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. +[Installation](#installation) •+[Examples](#examples) •+[Related projects](#related-projects) •+[Documentation](#documentation) •+[Contributions](#contributions) •+[Acknowledgements](#acknowledgements) -## Using Copilot-Assuming you have GHC and cabal already installed (see [Haskell-Platform](http://hackage.haskell.org/platform/) or-[ghcup](https://www.haskell.org/ghcup/)), there are several ways to use-Copilot:+</div> -* Adding Copilot to your project+## Features - Copilot is available from- [Hackage](https://hackage.haskell.org/package/copilot). Adding `copilot`- to your project's cabal file should be enough to get going.+- Write simple, high-level specifications using a stream-based language. -* Adding Copilot to the default GHC environment+- Produce hard real-time C99 runtime monitors that run in constant memory and time. - ```bash- cabal v2-install --lib copilot- ```+- Catch errors in specifications early using expressive static type system. - After which Copilot will be available from ghci.+- Prove properties about specifications using theorem proving extensions. -* Launching a repl with Copilot+- Interpret specifications for testing and debugging purposes. - Another quick solution is to cabal to launch a repl with Copilot- available.+- Obtain proofs of correctness of the generated code. - ```bash- cabal v2-repl --build-depends copilot- ```+## Table of Contents - Cabal will download and build Copilot only to make it available in the- launched repl. The global GHC environment will not be affected.+- [Installation](#installation)+ - [Linux installation](#linux-installation)+ - [Mac installation](#mac-installation)+ - [Troubleshooting](#troubleshooting)+- [Examples](#examples)+- [Related projects](#related-projects)+- [Documentation](#documentation)+ - [API documentation and tutorials](#api-documentation-and-tutorials)+ - [Publications](#publications)+ - [Website](#website)+- [Contributions](#contributions)+- [Acknowledgements](#acknowledgements)+ - [The Copilot team](#the-copilot-team)+ - [Institutional support](#institutional-support) -* Building from source (typically done for development):+# Installation+<sup>[(Back to top)](#table-of-contents)</sup> - ```bash- git clone https://github.com/Copilot-Language/copilot.git- cd copilot- ```+## Linux installation+<sup>[(Back to top)](#table-of-contents)</sup> - Compiling can either be done in a Nix-style build, or a traditional one:+### Debian Bookworm / Ubuntu 23.04 - _Nix-Style build (Cabal >= 2.x)_+On Debian Bookworm / Ubuntu 23.04 or newer, Copilot can be installed directly+from the package repositories with: - ```bash- cabal build copilot-*/ # For Cabal 3.x- cabal v2-build copilot-*/ # For Cabal 2.x- ```+```sh+$ sudo apt-get install libghc-copilot-dev+``` - _Traditional build (Cabal 1.x)_- ```bash- cd copilot- cabal install --dependencies-only . ../copilot-*/- cabal install ../copilot-*/- cabal build- ```+To test that Copilot is available, execute the following:+```sh+$ ghci <<< 'import Language.Copilot'+``` -Note there is a TravisCI build (linked to at the top of this README) if you-have trouble building/installing.+It should end with a line like the following and not print any error messages:+```sh+ghci> ghci> Leaving GHCi.+``` +### Fedora 40 -## Example-Here follows a simple example of a heating system. Other examples can be found+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+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,+you can use `apt-get` to install all dependencies as follows:++```sh+$ sudo apt-get install ghc cabal-install alex happy pkg-config libz-dev+```++Once the compiler is installed, install Copilot from+[Hackage](https://hackage.haskell.org/package/copilot) with:++```sh+cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language \+ copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter+```++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.+```++## Mac installation+<sup>[(Back to top)](#table-of-contents)</sup>++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:++```sh+$ brew install ghc cabal-install+```++Once the compiler is installed, install Copilot from+[Hackage](https://hackage.haskell.org/package/copilot) with:++```sh+$ cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language \+ copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter+```++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.+```++## Troubleshooting+<sup>[(Back to top)](#table-of-contents)</sup>++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+troubleshooting the installation. Our issues often include comments with+Dockerfiles listing the steps necessary to install Copilot from scratch.++## Examples+<sup>[(Back to top)](#table-of-contents)</sup>++Here follows a simple example of a heating system. More examples can be found in the [examples directory](https://github.com/Copilot-Language/copilot/tree/master/copilot/examples) of the main repository. ```haskell--- This is a simple example with basic usage. It implements a simple home--- heating system: It heats when temp gets too low, and stops when it is high--- enough. It read temperature as a byte (range -50C to 100C) and translates--- this to Celcius.+-- 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. module Heater where @@ -92,12 +186,13 @@ import Prelude hiding ((>), (<), div) --- External temperature as a byte, range of -50C to 100C+-- External temperature as a byte, ranging from -50C to 100C. temp :: Stream Word8 temp = extern "temperature" Nothing --- Calculate temperature in Celcius.--- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there+-- Temperature in Celsius.+--+-- We need to cast the Word8 to a Float. This is an unsafeCast, as there -- is no direct relation between Word8 and Float. ctemp :: Stream Float ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0@@ -112,83 +207,188 @@ main = reify spec >>= compile "heater" ``` -The examples located in the `examples/` directory can be run from the root of-the project. Each example has a name. As a rule of thumb, the examples are-named after the filename (without extension) in lowercase letters, and-directory seperators replaced with a '-'. For example:+If you save this example in a file `Heater.hs` and run:+```sh+$ runhaskell Heater.hs+```+it will produce the files `heater.c`, `heater.h` and `heater_types.h`,+containing, respectively, the implementation of the monitors, the interface,+and a declaration of any types declared in the specification (empty in this+case). +If you clone the repository, the examples in the `examples/` directory can be+run from the root of the project. As a rule of thumb, each example is named+after the filename (without extension) in lowercase letters, and directory+separators replaced with a '-'. For example:+ ```sh-cabal run addmult -f examples-cabal run counter -f examples-cabal run what4-arithmetic -f examples+$ cabal run addmult -f examples+$ cabal run counter -f examples+$ cabal run what4-arithmetic -f examples ``` -## Contributions-Feel free to open new issues and send pull requests.+# Related projects+<sup>[(Back to top)](#table-of-contents)</sup> -In order to contribute to Copilot, please use the following steps which will-make the process of evaluating and including your changes much easier:+_Disclaimer: The following projects are not part of Copilot. Their mention here+does not constitute any form of endorsement._ -* Create an issue for every individual change or problem with Copilot. Document- the issue well.+- [Ogma](https://github.com/nasa/ogma) is a NASA tool to facilitate the+ integration of safe runtime monitors into other systems, including those+ built using NASA's Core Flight System or the Robot Operating System (ROS 2). -* Always comment on the issues you are addressing in every commit. Be- descriptive, and use the syntax `#<issue_number>` so that we can track- changes and issues easily.+- [arduino-copilot](https://hackage.haskell.org/package/arduino-copilot)+ facilitates building copilot applications that run on Arduino. -* Every commit should mention one issue and, ideally, only one.+- [sketch-frp-copilot](https://hackage.haskell.org/package/sketch-frp-copilot)+ extends Copilot with an FRP-like interface. -* Do not send a PR or commit that addresses multiple problems, unless they are- related and cannot be separated.+- [zephyr-copilot](https://hackage.haskell.org/package/zephyr-copilot)+ facilitates building copilot applications that run on boards supported by the+ Zephyr project. -* Do not commit to master directly, except for branch merges. Make sure you- always merge onto master using `--no-ff` so that we can tell that features- were addressed separately, completed, tested, and then merged. If you are a- Copilot developer, create a branch for every issue you are addressing, complete- it, and then merge onto master. Document every commit in every branch,- including the last merge commit, stating the issues it addresses or closes.+# Documentation+<sup>[(Back to top)](#table-of-contents)</sup> -This process is similar to [Git-Flow](http://nvie.com/posts/a-successful-git-branching-model/). The equivalent-of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's-develop branch is our master.+## API documentation and tutorials+<sup>[(Back to top)](#table-of-contents)</sup> +A tutorial on Copilot can be found+[here](https://copilot-language.github.io/downloads/copilot_tutorial.pdf). -## Further information-For further information, including documentation and a tutorial, please visit-the Copilot website:+The API is documented throughout the different libraries and published on+Hackage:++- [copilot](https://hackage.haskell.org/package/copilot)+- [copilot-c99](https://hackage.haskell.org/package/copilot-c99)+- [copilot-core](https://hackage.haskell.org/package/copilot-core)+- [copilot-interpreter](https://hackage.haskell.org/package/copilot-interpreter)+- [copilot-language](https://hackage.haskell.org/package/copilot-language)+- [copilot-libraries](https://hackage.haskell.org/package/copilot-libraries)+- [copilot-prettyprinter](https://hackage.haskell.org/package/copilot-prettyprinter)+- [copilot-theorem](https://hackage.haskell.org/package/copilot-theorem)++## Publications+<sup>[(Back to top)](#table-of-contents)</sup>++The best introduction to the fundamentals of Copilot apart from the tutorial+is:++- [Copilot 3](https://ntrs.nasa.gov/citations/20200003164)++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)++- [Copilot: monitoring embedded systems](https://link.springer.com/article/10.1007/s11334-013-0223-x)++- [From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project](https://arxiv.org/abs/2012.03745)++- [Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors](https://ntrs.nasa.gov/citations/20220000049)++- [Monitoring Distributed Real-Time Systems: A Survey and Future Directions](https://ntrs.nasa.gov/citations/20100027427)++- [Monitoring ROS2: from Requirements to Autonomous Robots](https://arxiv.org/abs/2209.14030)++## Website+<sup>[(Back to top)](#table-of-contents)</sup>++For further information, including links to more documentation and the+tutorial, please visit the Copilot website: [https://copilot-language.github.io](https://copilot-language.github.io). +# Contributions+<sup>[(Back to top)](#table-of-contents)</sup> -## Acknowledgements-We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National-Institute of Aerospace, which partially supported this work.+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. -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported-further development of Copilot.+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. -## License-Copilot is distributed under the BSD-3-Clause license, which can be found-[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot/LICENSE).+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)*. -## The Copilot Team-The development of Copilot spans across several years. During these years-the following people have helped develop Copilot (in no particular order):+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. -* Lee Pike-* Alwyn Goodloe (maintainer)-* Robin Morisset-* Sebastian Niller-* Nis Wegmann+# Acknowledgements+<sup>[(Back to top)](#table-of-contents)</sup>++## The Copilot team+<sup>[(Back to top)](#table-of-contents)</sup>++Copilot is currently maintained by:++* Alwyn Goodloe+* Ivan Perez++Past and current team members also include (in alphabetical order):++* Macallan Cruff+* Frank Dedden * Chris Hathhorn-* Eli Mendelson-* Jonathan Laurent-* Laura Titolo * Georges-Axel Jolayan-* Macallan Cruff-* Ryan Spring+* Jonathan Laurent+* Eli Mendelson+* Robin Morisset+* Sebastian Niller * Lauren Pick-* Frank Dedden (maintainer: contact at dev@dedden.net)-* Ivan Perez (maintainer)+* Lee Pike+* Will Pogge+* Ryan Spring+* Laura Titolo+* Nis Wegmann++For a complete list of contributors, including external contributors, see:+https://github.com/Copilot-Language/copilot/graphs/contributors++## Institutional support+<sup>[(Back to top)](#table-of-contents)</sup>++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+further development of Copilot.
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 3.7+version: 4.8 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -24,6 +24,8 @@ A tutorial, examples, and other information are available at <https://copilot-language.github.io>. +x-curation: uncurated+ extra-source-files: README.md CHANGELOG@@ -31,6 +33,7 @@ source-repository head type: git location: https://github.com/Copilot-Language/copilot.git+ subdir: copilot flag examples description: Enable examples@@ -42,19 +45,19 @@ default-language: Haskell2010 ghc-options: -Wall- -fwarn-tabs -fno-warn-orphans build-depends:- base >= 4.9 && < 5- , optparse-applicative >= 0.14 && < 0.16- , directory >= 1.3 && < 1.4- , filepath >= 1.4 && < 1.5+ base >= 4.9 && < 5+ , optparse-applicative >= 0.14 && < 0.20+ , directory >= 1.3 && < 1.4+ , filepath >= 1.4 && < 1.6 - , copilot-core >= 3.7 && < 3.8- , copilot-theorem >= 3.7 && < 3.8- , copilot-language >= 3.7 && < 3.8- , copilot-libraries >= 3.7 && < 3.8- , copilot-c99 >= 3.7 && < 3.8+ , copilot-core >= 4.8 && < 4.9+ , copilot-theorem >= 4.8 && < 4.9+ , copilot-language >= 4.8 && < 4.9+ , copilot-libraries >= 4.8 && < 4.9+ , copilot-c99 >= 4.8 && < 4.9+ , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main@@ -83,6 +86,19 @@ else buildable: False +executable what4-arithmetic-counterexamples+ main-is: ArithmeticCounterExamples.hs+ hs-source-dirs: examples/what4+ build-depends: base+ , containers+ , copilot+ , copilot-theorem+ default-language: Haskell2010+ if flag(examples)+ buildable: True+ else+ buildable: False+ executable what4-structs main-is: Structs.hs hs-source-dirs: examples/what4@@ -194,6 +210,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/AddMult.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Another small example that calculates a constant value using a recursive -- function.
examples/Array.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | This is a simple example for arrays. As a program, it does not make much -- sense, however it shows of the features of arrays nicely.@@ -8,8 +6,8 @@ -- | Enable compiler extension for type-level data, necesary for the array -- length. -{-# LANGUAGE RebindableSyntax #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE RebindableSyntax #-} module Main where @@ -28,7 +26,21 @@ -- It passes the current value of arr as an argument. -- The prototype of 'func' would be: -- void func (int8_t arg[3]);- trigger "func" (arr .!! 0) [arg arr]+ trigger "func" (arr ! 0) [arg arr]++ -- A trigger that fires 'func2' every time.+ -- It passes the current value of arr as an argument, but updating the first+ -- element of the array to always be True.+ -- The prototype of 'func2' would be:+ -- void func2 (int8_t arg[3]);+ trigger "func2" true [arg (arr !! 0 =: true)]++ -- A trigger that fires 'func2' every time.+ -- It passes the current value of arr as an argument, but negating the second+ -- element of the array.+ -- The prototype of 'func3' would be:+ -- void func3 (int8_t arg[3]);+ trigger "func3" true [arg (arr !! 1 =$ not)] -- Compile the spec main :: IO ()
examples/Cast.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Examples of casting types.
examples/Clock.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example showing usage of clocks to generate periodically recurring truth -- values.
examples/Counter.hs view
@@ -1,6 +1,4 @@-------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example showing an implementation of a resettable counter. @@ -22,8 +20,9 @@ -- Counter that resets when it reaches 256 bytecounter :: Stream Int32-bytecounter = counter true reset where- reset = counter true false `mod` 256 == 0+bytecounter = counter true reset+ where+ reset = counter true false `mod` 256 == 0 spec :: Spec spec = trigger "counter" true [arg $ bytecounter]
examples/Engine.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Example implementing an engine cooling control system. @@ -11,11 +9,10 @@ import Language.Copilot import qualified Prelude as P -{- If the majority of the engine temperature probes exeeds 250 degrees, then- - the cooler is engaged and remains engaged until the majority of the engine- - temperature probes drop to 250 or below. Otherwise, trigger an immediate- - shutdown of the engine.--}+-- If the majority of the engine temperature probes exeeds 250 degrees, then+-- the cooler is engaged and remains engaged until the majority of the engine+-- temperature probes drop to 250 or below. Otherwise, trigger an immediate+-- shutdown of the engine. engineMonitor :: Spec engineMonitor = do@@ -28,7 +25,7 @@ exceed = map (> 250) vals maj = majority exceed checkMaj = aMajority exceed maj- ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) + ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) two51 = Just $ [251, 251] P.++ repeat (250 :: Word8) zero = Just $ repeat (0 :: Word8)
examples/Heater.hs view
@@ -1,11 +1,9 @@--------------------------------------------------------------------------------- -- Copyright 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- This is a simple example with basic usage. It implements a simple home -- heating system: It heats when temp gets too low, and stops when it is high -- enough. It read temperature as a byte (range -50C to 100C) and translates--- this to Celcius.+-- this to Celsius. module Main where @@ -18,7 +16,7 @@ temp :: Stream Word8 temp = extern "temperature" Nothing --- Calculate temperature in Celcius.+-- Calculate temperature in Celsius. -- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there -- is no direct relation between Word8 and Float. ctemp :: Stream Float
examples/Structs.hs view
@@ -1,53 +1,56 @@ -- | An example showing how specifications involving structs (in particular, -- nested structs) are compiled to C using copilot-c99. -{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-} module Main where import qualified Prelude as P import Control.Monad (void, forM_)+import GHC.Generics (Generic) import Language.Copilot import Copilot.Compile.C99 - -- | Definition for `Volts`. data Volts = Volts- { numVolts :: Field "numVolts" Word16- , flag :: Field "flag" Bool- }+ { numVolts :: Field "numVolts" Word16+ , flag :: Field "flag" Bool+ }+ deriving Generic -- | `Struct` instance for `Volts`. instance Struct Volts where- typename _ = "volts"- toValues volts = [ Value Word16 (numVolts volts)- , Value Bool (flag volts)- ]+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- 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- typeOf = Struct (Volts (Field 0) (Field False))+ typeOf = typeOfDefault data Battery = Battery- { temp :: Field "temp" Word16- , volts :: Field "volts" (Array 10 Volts)- , other :: Field "other" (Array 10 (Array 5 Word32))- }+ { temp :: Field "temp" Word16+ , volts :: Field "volts" (Array 10 Volts)+ , other :: Field "other" (Array 10 (Array 5 Word32))+ }+ deriving Generic -- | `Battery` instance for `Struct`. instance Struct Battery where- typename _ = "battery"- toValues battery = [ Value typeOf (temp battery)- , Value typeOf (volts battery)- , Value typeOf (other battery)- ]+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- 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--- throw an error.+-- | `Battery` instance for `Typed`. instance Typed Battery where- typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))+ typeOf = typeOfDefault spec :: Spec spec = do@@ -57,15 +60,14 @@ -- 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))+ ((((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))+ ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)) [arg battery]- main :: IO () main = do
+ examples/StructsUpdateField.hs view
@@ -0,0 +1,161 @@+-- | 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 DeriveGeneric #-}+{-# 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.Generics (Generic)+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+ }+ deriving Generic++-- | `Struct` instance for `Volts`.+instance Struct Volts where+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- 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`.+ -- (Alternatively, we could define this as @updateField = updateFieldDefault@,+ -- but we demonstrate how to manually implement it below for educational+ -- purposes.)+ 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 = typeOfDefault++data Battery = Battery+ { temp :: Field "temp" Word16+ , volts :: Field "volts" (Array 10 Volts)+ , other :: Field "other" (Array 10 (Array 5 Word32))+ }+ deriving Generic++-- | `Battery` instance for `Struct`.+instance Struct Battery where+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- We implement `updateField` similarly to how we implement it in the+ -- `Struct Volts` instance above. (Alternatively, we could define this as+ -- @updateField = updateFieldDefault@, but we demonstrate how to manually+ -- implement it below for educational purposes.)+ 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`.+instance Typed Battery where+ typeOf = typeOfDefault++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/Voting.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Fault-tolerant voting examples.
examples/WCV.hs view
@@ -3,7 +3,7 @@ -- Well-Clear Bounday Models for the Integration of UAS in the NAS', -- https://ntrs.nasa.gov/citations/20140010078. -{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE RebindableSyntax #-} module Main where@@ -14,7 +14,6 @@ import Data.Foldable (forM_) import qualified Control.Monad as Monad - -- | `dthr` is the horizontal distance threshold. dthr :: Stream Double dthr = extern "dthr" Nothing@@ -33,10 +32,7 @@ type Vect2 = (Stream Double, Stream Double) ---------------------------------- -- External streams for relative position and velocity.--------------------------------- -- | The relative x velocity between ownship and the intruder. vx :: Stream Double@@ -54,7 +50,6 @@ v :: (Stream Double, Stream Double) v = (vx, vy) - -- | The relative x position between ownship and the intruder. sx :: Stream Double sx = extern "relative_position_x" Nothing@@ -71,10 +66,7 @@ s :: (Stream Double, Stream Double) s = (sx, sy) -------------------- -- The following section contains basic libraries for working with vectors.------------------- -- | Multiply two Vectors. (|*|) :: Vect2 -> Vect2 -> Stream Double@@ -101,11 +93,8 @@ neg :: Vect2 -> Vect2 neg (x, y) = (negate x, negate y) ---------------------- -- From here on the algorithm, as described by the paper mentioned on the top -- of this file, is implemented. Please refer to the paper for details.--------------------- tau :: Vect2 -> Vect2 -> Stream Double tau s v = if s |*| v < 0@@ -134,7 +123,6 @@ theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v) - tcoa :: Stream Double -> Stream Double -> Stream Double tcoa sz vz = if (sz * vz) < 0 then (-sz) / vz@@ -143,10 +131,7 @@ dcpa :: Vect2 -> Vect2 -> Stream Double dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy) ---------------------------- -- Well clear Violation ----------------------------- -- | Determines if the well clear property is violated or not. wcv :: (Vect2 -> Vect2 -> Stream Double) ->@@ -166,9 +151,8 @@ (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr)) spec = do- Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))- -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz)))-+ Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))+ -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz))) main :: IO () main = do
examples/what4/Arithmetic.hs view
@@ -21,23 +21,22 @@ efloat = extern "efloat" Nothing -- The simplest example involving numbers: equality on constant values.- void $ prop "Example 1" (forall ((constant (1 :: Int8)) == (constant 1)))+ void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1))) -- Testing "a < a + 1". This should fail, because it isn't true.- void $ prop "Example 2" (forall (eint8 < (eint8 + 1)))+ void $ prop "Example 2" (forAll (eint8 < (eint8 + 1))) -- Adding another condition to the above property to make it true.- void $ prop "Example 3" (forall ((eint8 < (eint8 + 1)) || (eint8 == 127)))+ void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127))) -- Just like the previous example, but with words.- void $ prop "Example 4" (forall ((eword8 < (eword8 + 1)) || (eword8 == 255)))+ void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255))) -- An example with floats.- void $ prop "Example 5" (forall ((2 * efloat) == (efloat + efloat)))+ void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat))) -- Another example with floats. This fails, because it isn't true.- void $ prop "Example 6" (forall ((efloat + 1) /= efloat))-+ void $ prop "Example 6" (forAll ((efloat + 1) /= efloat)) main :: IO () main = do
+ examples/what4/ArithmeticCounterExamples.hs view
@@ -0,0 +1,110 @@+-- | An example showing the usage of the What4 backend in copilot-theorem for+-- simple arithmetic. This example uses the 'proveWithCounterExamples' function+-- to demonstrate counterexamples in the event of invalid properties.++module Main where++import qualified Prelude as P+import Control.Monad (void, forM_)+import qualified Data.Map as Map++import Language.Copilot+import Copilot.Theorem.What4++spec :: Spec+spec = do+ -- Define some external streams. Their values are not important, so external+ -- streams suffice.+ let eint8 :: Stream Int8+ eint8 = extern "eint8" Nothing+ eword8 :: Stream Word8+ eword8 = extern "eword8" Nothing+ efloat :: Stream Float+ efloat = extern "efloat" Nothing++ -- The simplest example involving numbers: equality on constant values.+ void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))++ -- Testing "a < a + 1". This should fail, because it isn't true.+ void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))++ -- Adding another condition to the above property to make it true.+ void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))++ -- Just like the previous example, but with words.+ void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))++ -- An example with floats.+ void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))++ -- Another example with floats. This fails, because it isn't true.+ void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))++main :: IO ()+main = do+ spec' <- reify spec++ -- Use Z3 to prove the properties.+ results <- proveWithCounterExample Z3 spec'++ -- Print the results.+ forM_ results $ \(nm, res) -> do+ putStr $ nm <> ": "+ case res of+ ValidCex -> putStrLn "valid"+ InvalidCex cex -> do+ putStrLn "invalid"+ putStrLn $ ppCounterExample cex+ UnknownCex -> putStrLn "unknown"++-- | Pretty-print a counterexample for user display.+ppCounterExample :: CounterExample -> String+ppCounterExample cex+ | any P.not (baseCases cex)+ = if Map.null baseCaseVals+ then+ " All possible extern values during the base case(s) " P.+++ "constitute a counterexample."+ else+ unlines $+ " The base cases failed with the following extern values:" :+ map+ (\((name, _), val) -> " " P.++ name P.++ ": " P.++ show val)+ (Map.toList baseCaseVals)++ | P.not (inductionStep cex)+ = if Map.null inductionStepVals+ then+ " All possible extern values during the induction step " P.+++ "constitute a counterexample."+ else+ unlines $+ " The induction step failed with the following extern values:" :+ map+ (\((name, _), val) -> " " P.++ name P.++ ": " P.++ show val)+ (Map.toList inductionStepVals)++ | otherwise+ = error $+ "ppCounterExample: " P.+++ "Counterexample without failing base cases or induction step"+ where+ allExternVals = concreteExternValues cex++ baseCaseVals =+ Map.filterWithKey+ (\(_, offset) _ ->+ case offset of+ AbsoluteOffset {} -> True+ RelativeOffset {} -> False+ )+ allExternVals++ inductionStepVals =+ Map.filterWithKey+ (\(_, offset) _ ->+ case offset of+ AbsoluteOffset {} -> False+ RelativeOffset {} -> True+ )+ allExternVals
examples/what4/Propositional.hs view
@@ -11,41 +11,65 @@ spec :: Spec spec = do+ -- * Non-inductive propositions+ -- The constant value true, which is translated as the corresponding SMT- -- boolean literal.- void $ prop "Example 1" (forall true)+ -- 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.- void $ prop "Example 2" (forall false)+ -- 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
@@ -2,53 +2,56 @@ -- structs and arrays. Particular focus is on nested structs. -- For general usage of structs, refer to the general structs example. -{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-} module Main where import qualified Prelude as P import Control.Monad (void, forM_)+import GHC.Generics (Generic) import Language.Copilot import Copilot.Theorem.What4 - -- | Definition for `Volts`. data Volts = Volts- { numVolts :: Field "numVolts" Word16- , flag :: Field "flag" Bool- }+ { numVolts :: Field "numVolts" Word16+ , flag :: Field "flag" Bool+ }+ deriving Generic -- | `Struct` instance for `Volts`. instance Struct Volts where- typename _ = "volts"- toValues volts = [ Value Word16 (numVolts volts)- , Value Bool (flag volts)- ]+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- 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- typeOf = Struct (Volts (Field 0) (Field False))+ typeOf = typeOfDefault data Battery = Battery- { temp :: Field "temp" Word16- , volts :: Field "volts" (Array 10 Volts)- , other :: Field "other" (Array 10 (Array 5 Word32))- }+ { temp :: Field "temp" Word16+ , volts :: Field "volts" (Array 10 Volts)+ , other :: Field "other" (Array 10 (Array 5 Word32))+ }+ deriving Generic -- | `Battery` instance for `Struct`. instance Struct Battery where- typename _ = "battery"- toValues battery = [ Value typeOf (temp battery)- , Value typeOf (volts battery)- , Value typeOf (other battery)- ]+ typeName = typeNameDefault+ toValues = toValuesDefault+ -- 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--- throw an error.+-- | `Battery` instance for `Typed`. instance Typed Battery where- typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))+ typeOf = typeOfDefault spec :: Spec spec = do@@ -57,14 +60,17 @@ -- Check equality, indexing into nested structs and arrays. Note that this is -- trivial by equality.- void $ prop "Example 1" $ forall $- (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)+ void $ prop "Example 1" $ forAll $+ (((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts) -- Same as previous example, but get a different array index (so should be -- false).- void $ prop "Example 2" $ forall $- (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)+ void $ prop "Example 2" $ forAll $+ (((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4) + -- Update a struct field, then check it for equality.+ void $ prop "Example 3" $ forAll $+ ((battery ## temp =$ (+1))#temp == (battery#temp + 1)) main :: IO () main = do
src/Language/Copilot/Main.hs view
@@ -3,9 +3,10 @@ module Language.Copilot.Main ( copilotMain, defaultMain ) where import qualified Copilot.Core as C (Spec)-import Copilot.Language (interpret, prettyPrint)+import Copilot.Language (interpret) import Copilot.Language.Reify (reify) import Copilot.Language (Spec)+import qualified Copilot.PrettyPrint as PP import Options.Applicative import Data.Semigroup ((<>))@@ -44,7 +45,6 @@ <> metavar "INT" <> showDefault <> help "Interpret specification and write result to output") - -- | Create a main to either compile or interpret a copilot specification. -- -- This function must be provided an auxiliary function capable of compiling@@ -63,18 +63,19 @@ -- * @--interpret/-i NUM@: interpret the specification for a given number -- of steps. copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()-copilotMain interp pretty comp spec = main =<< execParser opts where- opts = info (cmdargs <**> helper) fullDesc+copilotMain interp pretty comp spec = main =<< execParser opts+ where+ opts = info (cmdargs <**> helper) fullDesc - main :: CmdArgs -> IO ()- main args = do- let iters = ainterpret args- when (apretty args) $ pretty spec- when (iters Prelude.> 0) $ interp (fromIntegral iters) spec+ main :: CmdArgs -> IO ()+ main args = do+ let iters = ainterpret args+ when (apretty args) $ pretty spec+ when (iters Prelude.> 0) $ interp (fromIntegral iters) spec - when (not $ acompile args) $ do- spec' <- reify spec- comp (aoutput args) spec'+ when (not $ acompile args) $ do+ spec' <- reify spec+ comp (aoutput args) spec' -- | Create a main function with a default interpreter and pretty printer. --@@ -86,3 +87,8 @@ -- command line options. defaultMain :: Compiler -> Spec -> IO () defaultMain = copilotMain interpret prettyPrint+ where+ -- Transform a high-level Copilot Language specification into a low-level+ -- Copilot Core specification and pretty-print it to stdout.+ prettyPrint :: Spec -> IO ()+ prettyPrint e = fmap PP.prettyPrint (reify e) >>= putStr