For general context of this project, motivation, an overview, and published papers, see our project homepage.
Instructions tested on Debian GNU/Linux 8.2 ("jessie") and Ubuntu 16.04 ("xenial"). May need to be adapted for other systems.
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.
l4v, isabelle and z3
are submodules that the Cogent framework depends on. To get them: git submodule update --init --recursive.
If you already have them on your machine, you can use your local copies, by checking out the compatible revisions:
l4v:ecc84ffc6ead5a4d80aac7dabacf4b010c05dfcaisabelle: any Isabelle2018 revisionz3: see cogent/INSTALL.md for more information
Add isabelle/bin to your PATH: export PATH="$(pwd)/isabelle/bin:$PATH"
If you have an existing Isabelle install, you may want to set ISABELLE_IDENTIFIER instead of PATH.
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 build-env.sh.
Note: also see Proofs and Regression tests below.
Run build system and regression tests. (ETA: 2–3 CPU hours)
This also builds the Cogent compiler and Isabelle theories.
If this works, your install is probably ok.
Run ./run_tests.
For C-refinement proofs, which are excluded from the regression tests because of their size, follow instructions in Proofs section.
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;
isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../l4v -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;
isabelle build -d . -d ../../../../cogent/isa -d ../../../../l4v -b -o process_output_limit=999 BilbyFs_AllRefine)
# View end-to-end theorems. Each theory has a "print_theorems" command for this.
# For ext2:
isabelle jedit -d impl/ext2/cogent/plat/verification -d cogent/isa -d l4v -l Ext2_CorresProof impl/fs/ext2/cogent/plat/verification/Ext2_AllRefine.thy
# For BilbyFs:
isabelle jedit -d impl/fs/bilby/cogent/plat/verification -d cogent/isa -d l4v -l BilbyFs_CorresProof impl/fs/bilby/cogent/plat/verification/BilbyFs_AllRefine.thy
The functional correctness proofs for BilbyFs's sync and iget operations are in
impl/fs/bilby/proof/.
They are built as part of the regression tests, and can be rebuilt with
regression/run_tests.py -x l4v -x isabelle -v sync iget
See impl/fs/ext2/README and impl/fs/bilby/README for more information on how to build the kernel modules
cogent: Cogent compilerc-refinement: Isabelle/HOL theories and proof procedures for Cogent-C refinementtests: Cogent test programs for proof procedures
isa-parser: Haskell library for parsing and pretty-printing Isabelle/HOLimpl: Systems implemented in Cogentfs: File systemsbilby: Bilby file systemcogent: Cogent code for BilbyFsc: C implementation for BilbyFsproof: Functional correctness specs and proofs for BilbyFs
ext2: ext2 file systemcogent: Cogent code for ext2
regression: Regression test script