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