README.md
1Design Spec Refinement Proof
2============================
3
4This proof establishes that seL4's [design specification](../../spec/design/)
5is a formal *refinement* (i.e. a correct implementation) of its
6[abstract specification](../../spec/abstract/). This proof also
7interweaves the definition and proofs of the global invariant for the
8design specification, and builds on the [Abstract Spec Invariant
9Proof](../invariant-abstract/). It is described in the TPHOLS '08
10[paper][1].
11
12 [1]: http://nicta.com.au/pub?id=483 "Secure Microkernels, State Monads and Scalable Refinement"
13
14Building
15--------
16
17Make sure that the `L4V_ARCH` environment variable is set to the desired
18target architecture. If in doubt, use `L4V_ARCH=ARM`.
19
20To build from the `l4v/` directory, run:
21
22 ./isabelle/bin/isabelle build -d . -v -b Refine
23
24Important Theories
25------------------
26
27The top-level theory where the refinement statement is established over
28the entire kernel is [`Refine`](ARM/Refine.thy); the state-relation that
29relates the state-spaces of the two specifications is defined in
30[`StateRelation`](ARM/StateRelation.thy) and the basic correspondence
31property proved over each kernel function is defined in
32[`Corres`](ARM/Corres.thy).
33
34
35