Cogent: Code and Proof Co-Generation
For general context of this project, motivation, an overview, and published papers, see our project homepage.
Instructions tested on Debian GNU/Linux 9.8 ("stretch") and Ubuntu 18.04 ("bionic"). Similar distributions may also work.
Install dependencies from the Debian repository.
sudo apt-get install git # git sudo apt-get install python-lxml python-psutil python-pycparser # regression tester
To install the Cogent compiler, consult file cogent/README.md for details.
The Cogent framework depends on Isabelle-2019.
If you already have them on your machine, you can use your local copy.
Otherwise you can either obtain it from their website or from the
isabelle submodule, via
git submodule update --init --recursive -- isabelle.
isabelle/bin to your PATH:
If you have an existing Isabelle install, you may want to set
ISABELLE_IDENTIFIER instead of
Initialise Isabelle and install components:
isabelle components -I isabelle components -a
Consult Isabelle manual for more information.
For more customised settings to run proofs and regression tests, modify
See cogent/README.md for more information.
Firstly, download the AutoCorres release v1.6.1 from https://ts.data61.csiro.au/projects/TS/autocorres.html,
move the extracted folder to this directory, and rename the folder to
To build the proofs, it is recommended that your machine (or virtual machine) provides 32G of memory and 4–8 CPU threads.
# Build compilation correctness proof for ext2. (ETA: 120 CPU hours) (cd impl/fs/ext2/cogent; make verification; export L4V_ARCH="ARM"; isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b Ext2_AllRefine) # Build compilation correctness proof for BilbyFs. (ETA: 120 CPU hours) (cd impl/fs/bilby/cogent; make verification; patch -d plat/verification < ../../../../BilbyFs_CorresProof.patch; export L4V_ARCH="ARM"; isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b -o process_output_limit=999 BilbyFs_AllRefine) # View end-to-end theorems. Each theory has a "print_theorems" command for this. # For ext2: L4V_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 # For BilbyFs: L4V_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
The functional correctness proofs for BilbyFs's
iget operations are in
They are built as part of the regression tests, and can be rebuilt with
regression/run_tests.py -x autocorres -x isabelle -v sync iget
Regression tests (for developers; ETA: 2–3 CPU hours)
For testing the compiler, refer to travis.yml for commands.
./run_tests to test systems implementations and parts of their Isabelle proofs.
For C-refinement proofs, which are excluded from the regression tests because of their size, follow instructions in Proofs section.
cogent: Cogent compiler
c-refinement: Isabelle/HOL theories and proof procedures for Cogent-C refinement
tests: Cogent test programs for proof procedures
isa-parser: Haskell library for parsing and pretty-printing Isabelle/HOL
impl: Systems implemented in Cogent
fs: File systems
bilby: Bilby file system
cogent: Cogent code for BilbyFs
c: C implementation for BilbyFs
proof: Functional correctness specs and proofs for BilbyFs
ext2: ext2 file system
cogent: Cogent code for ext2
regression: Regression test script
The Gencot Tool
Gencot is a tool for translating C code to Cogent. It's developed by our collaborators. The repository is hosted on Github. See the README file and the documentation for more details.