1[![Build Status](https://api.travis-ci.org/NICTA/cogent.svg?branch=master)](https://travis-ci.org/NICTA/cogent) 2[![Documentation Status](https://readthedocs.org/projects/cogent/badge/?version=latest)](https://cogent.readthedocs.io/en/latest/?badge=latest) 3 4# Cogent: Code and Proof Co-Generation 5 6## Project homepage 7 8For general context of this project, motivation, an overview, and published papers, see 9our [project homepage](http://ts.data61.csiro.au/projects/TS/cogent.pml). 10 11## Online documentation 12 13https://cogent.readthedocs.io 14 15## Installation 16 17Instructions tested on Debian GNU/Linux 9.8 ("stretch") and Ubuntu 18.04 ("bionic"). Similar distributions may also work. 18 19Install dependencies from the Debian repository. 20``` 21sudo apt-get install git # git 22sudo apt-get install python-lxml python-psutil python-pycparser # regression tester 23``` 24 25To install the Cogent compiler, consult file [cogent/README.md](./cogent/README.md) for details. 26 27The Cogent framework depends on [Isabelle-2019](https://isabelle.in.tum.de/). 28If you already have them on your machine, you can use your local copy. 29Otherwise you can either obtain it from their website or from the `isabelle` submodule, via 30`git submodule update --init --recursive -- isabelle`. 31 32Add `isabelle/bin` to your PATH: `export PATH="$(pwd)/isabelle/bin:$PATH"` 33If you have an existing Isabelle install, you may want to set `ISABELLE_IDENTIFIER` instead of `PATH`. 34 35Initialise Isabelle and install components: 36``` 37isabelle components -I 38isabelle components -a 39``` 40Consult [Isabelle manual](https://isabelle.in.tum.de/documentation.html) for more information. 41 42For more customised settings to run proofs and regression tests, modify [`build-env.sh`](build-env.sh). 43 44Note: also see [Proofs](#proofs) and [Regression tests](#regression-tests) below. 45 46 47## Compiler 48 49See [cogent/README.md](./cogent/README.md) for more information. 50 51 52## File systems 53 54See [impl/fs/ext2/README](./impl/fs/ext2/README) and [impl/fs/bilby/README](./impl/fs/bilby/README) for more information on how to build the kernel modules. 55 56 57## Proofs 58 59Firstly, download the AutoCorres release from [http://ts.data61.csiro.au/projects/TS/autocorres/](http://ts.data61.csiro.au/projects/TS/autocorres/), 60move the extracted folder to this directory, and rename the folder to `autocorres`. 61 62To build the proofs, it is recommended that your machine (or virtual machine) 63provides 32G of memory and 4���8 CPU threads. 64 65``` 66# Build compilation correctness proof for ext2. (ETA: 120 CPU hours) 67(cd impl/fs/ext2/cogent; 68 make verification; 69 export L4V_ARCH="ARM"; 70 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b Ext2_AllRefine) 71 72# Build compilation correctness proof for BilbyFs. (ETA: 120 CPU hours) 73(cd impl/fs/bilby/cogent; 74 make verification; 75 patch -d plat/verification < ../../../../BilbyFs_CorresProof.patch; 76 export L4V_ARCH="ARM"; 77 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b -o process_output_limit=999 BilbyFs_AllRefine) 78 79# View end-to-end theorems. Each theory has a "print_theorems" command for this. 80# For ext2: 81L4V_ARCH="ARM" isabelle jedit -d impl/ext2/cogent/plat/verification -d cogent/isa -d autocorres -l Ext2_CorresProof impl/fs/ext2/cogent/plat/verification/Ext2_AllRefine.thy 82# For BilbyFs: 83L4V_ARCH="ARM" isabelle jedit -d impl/fs/bilby/cogent/plat/verification -d cogent/isa -d autocorres -l BilbyFs_CorresProof impl/fs/bilby/cogent/plat/verification/BilbyFs_AllRefine.thy 84``` 85 86The functional correctness proofs for BilbyFs's `sync` and `iget` operations are in 87`impl/fs/bilby/proof/`. 88They are built as part of the [regression tests](#regression-tests), and can be rebuilt with 89 90``` 91regression/run_tests.py -x autocorres -x isabelle -v sync iget 92``` 93 94 95## Regression tests (for developers; ETA: 2���3 CPU hours) 96 97For testing the compiler, refer to [travis.yml](./travis.yml) for commands. 98 99Run `./run_tests` to test systems implementations and parts of their Isabelle proofs. 100 101For C-refinement proofs, which are excluded from the regression tests because of 102their size, follow instructions in [Proofs](#proofs) section. 103 104 105## Directory 106 107* `cogent`: Cogent compiler 108* `c-refinement`: Isabelle/HOL theories and proof procedures for Cogent-C refinement 109 * `tests`: Cogent test programs for proof procedures 110* `isa-parser`: Haskell library for parsing and pretty-printing Isabelle/HOL 111* `impl`: Systems implemented in Cogent 112 * `fs`: File systems 113 * `bilby`: Bilby file system 114 * `cogent`: Cogent code for BilbyFs 115 * `c`: C implementation for BilbyFs 116 * `proof`: Functional correctness specs and proofs for BilbyFs 117 * `ext2`: ext2 file system 118 * `cogent`: Cogent code for ext2 119* `regression`: Regression test script 120 121 122## The Gencot Tool 123 124Gencot is a tool for translating C code to Cogent. It's developed by our collaborators. 125The repository is hosted on [Github](https://github.com/F1-C0D3/gencot). See the 126README file and the documentation for more details. 127 128