1The C Semantics of seL4
2=======================
3
4    l4v/spec/cspec/
5
6This directory contains the entry point for the automatic translation of
7the seL4 source code into Isabelle/HOL.
8
9The C semantics of the kernel is produced by first configuring and
10preprocessing the C sources for a specific platform and then parsing it into
11Isabelle using the C parser in `l4v/tools/c-parser`.
12
13To inspect the output of this translation, build the image `CSpec` and
14interactively inspect the constants the parser has defined.
15
16
17Top-Level Theory
18----------------
19
20The top-level theory file for this module is `Kernel_C` for the bare
21translation of seL4 into Isabelle, and `KernelInc_C` for additional automatic
22proofs about generated bitfield functions.
23
24
25Building
26--------
27
28The corresponding Isabelle sessions for this module are `CKernel` and `CSpec`.
29`CSpec` contains `CKernel` plus automated bitfield proofs.
30
31To build the image, run the corresponding session in directory `l4v/spec`,
32e.g.:
33
34    make CSpec
35
36This will also configure and preprocess the kernel sources.
37
38Expect this build to take about 30 min on a modern machine and to require
39close to 4GB of memory. For further sessions building on top of `CSpec`,
40usually at least 16GB of main memory are required together with a 64-bit setup
41of Isabelle.
42
43The target architecture may be specified by setting the `L4V_ARCH` environment
44variable. It determines both which configuration of seL4 is used, as well as
45indicating the architecture-specific definitions and proofs to use. The default
46architecture is `ARM` and will be selected if none is provided. See
47`l4v/spec/cspec/c/Makefile` for seL4 configuration details.
48
49
50Remarks
51-------
52
53To speed up interactive development, the bitfield code generator can be
54configured to skip the corresponding proofs and produce sorried
55(unproven) property statements only. To achieve this, set the
56environment variable `SORRY_BITFIELD_PROOFS` to `TRUE`.
57
58