diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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 - * 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 @@ -1,89 +1,183 @@ -# Copilot: Stream DSL for hard real-time runtime verification +
-[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) -[![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](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. +[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) +[![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 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: +
-* 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 +[(Back to top)](#table-of-contents) - ```bash - git clone https://github.com/Copilot-Language/copilot.git - cd copilot - ``` +## Linux installation +[(Back to top)](#table-of-contents) - 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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) -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 `#` 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 +[(Back to top)](#table-of-contents) -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 +[(Back to top)](#table-of-contents) +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) -## 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 #.` + 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)*. -## 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 +[(Back to top)](#table-of-contents) + +## The Copilot team +[(Back to top)](#table-of-contents) + +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 +[(Back to top)](#table-of-contents) + +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. diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -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 . +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 diff --git a/examples/AddMult.hs b/examples/AddMult.hs --- a/examples/AddMult.hs +++ b/examples/AddMult.hs @@ -1,6 +1,4 @@ --------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- -- | Another small example that calculates a constant value using a recursive -- function. diff --git a/examples/Array.hs b/examples/Array.hs --- a/examples/Array.hs +++ b/examples/Array.hs @@ -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 () diff --git a/examples/Cast.hs b/examples/Cast.hs --- a/examples/Cast.hs +++ b/examples/Cast.hs @@ -1,6 +1,4 @@ --------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- -- | Examples of casting types. diff --git a/examples/Clock.hs b/examples/Clock.hs --- a/examples/Clock.hs +++ b/examples/Clock.hs @@ -1,6 +1,4 @@ --------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- -- | Example showing usage of clocks to generate periodically recurring truth -- values. diff --git a/examples/Counter.hs b/examples/Counter.hs --- a/examples/Counter.hs +++ b/examples/Counter.hs @@ -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] diff --git a/examples/Engine.hs b/examples/Engine.hs --- a/examples/Engine.hs +++ b/examples/Engine.hs @@ -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) diff --git a/examples/Heater.hs b/examples/Heater.hs --- a/examples/Heater.hs +++ b/examples/Heater.hs @@ -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 diff --git a/examples/Structs.hs b/examples/Structs.hs --- a/examples/Structs.hs +++ b/examples/Structs.hs @@ -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 diff --git a/examples/StructsUpdateField.hs b/examples/StructsUpdateField.hs new file mode 100644 --- /dev/null +++ b/examples/StructsUpdateField.hs @@ -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' diff --git a/examples/Voting.hs b/examples/Voting.hs --- a/examples/Voting.hs +++ b/examples/Voting.hs @@ -1,6 +1,4 @@ --------------------------------------------------------------------------------- -- Copyright © 2019 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- -- | Fault-tolerant voting examples. diff --git a/examples/WCV.hs b/examples/WCV.hs --- a/examples/WCV.hs +++ b/examples/WCV.hs @@ -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 diff --git a/examples/what4/Arithmetic.hs b/examples/what4/Arithmetic.hs --- a/examples/what4/Arithmetic.hs +++ b/examples/what4/Arithmetic.hs @@ -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 diff --git a/examples/what4/ArithmeticCounterExamples.hs b/examples/what4/ArithmeticCounterExamples.hs new file mode 100644 --- /dev/null +++ b/examples/what4/ArithmeticCounterExamples.hs @@ -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 diff --git a/examples/what4/Propositional.hs b/examples/what4/Propositional.hs --- a/examples/what4/Propositional.hs +++ b/examples/what4/Propositional.hs @@ -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 diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs --- a/examples/what4/Structs.hs +++ b/examples/what4/Structs.hs @@ -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 diff --git a/src/Language/Copilot/Main.hs b/src/Language/Copilot/Main.hs --- a/src/Language/Copilot/Main.hs +++ b/src/Language/Copilot/Main.hs @@ -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