1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7The Abstract Specification of seL4
8==================================
9
10    l4v/spec/abstract/
11
12This directory contains the main Isabelle sources of the seL4 abstract
13specification. The specification draws in additional interface files from
14`design` and `machine`.
15
16The specification is written in monadic style. See
17`l4v/lib/Monad_WP/NonDetMonad` for the definition of this monad.
18
19Top-Level Theory
20----------------
21
22The top-level theory file that draws the whole specification together is
23`Syscall_A`, the top-level function in that theory is `call_kernel`.
24
25This top-level function defines in-kernel behaviour. Later in the proof,
26in particular in `invariant-abstract`, this function is further wrapped
27in an automaton that describes system behaviour.
28
29Entry Points
30------------
31
32Two useful entry points for browsing the abstract specification are the
33theories `Structures_A` and `ARM_Structs_A`. They define the state space
34of the kernel model, including what capabilities and kernel objects are.
35
36The theories `Invocations_A` and `ArchInvocation_A` define datatypes for
37the capability invocations/operations the kernel understands.
38
39Most theories are named after the subsystem of the kernel they specify.
40
41Building
42--------
43
44The corresponding Isabelle session is `ASpec`. It is set up to build a
45human-readable PDF document. `Glossary_Doc` contains definitions of common
46seL4 terms.
47
48To build, run in directory `l4v/spec`:
49
50    make ASpec
51
52Remarks
53-------
54
55 * Note that this specification is actually an extensible _family_ of
56   specifications, with predefined extension points. These points can
57   either be left generic, as for most of the abstract invariant proofs,
58   or they can be instantiated to more precise behaviour, such as in
59   the theory `Deterministic_A`, which is used for the information flow
60   proofs.
61
62 * The theory `Init_A` *does not* define real kernel initialisation.
63   Instead it is a dummy initial state for the kernel to demonstrate
64   non-emptiness of abstract kernel invariants.
65
66 * `KernelInit_A` is a paused project and not currently included in
67   the rest of the specification.
68
69