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