NameDateSize

..30-Nov-202017

Arch_DR.thyH A D30-Oct-202094.5 KiB

base/H30-Oct-20203

CNode_DR.thyH A D30-Oct-2020132.4 KiB

Corres_D.thyH A D09-Apr-202027.7 KiB

Finalise_DR.thyH A D30-Oct-2020174 KiB

Intent_DR.thyH A D30-Oct-202096.5 KiB

Interrupt_DR.thyH A D09-Apr-202029.7 KiB

Ipc_DR.thyH A D30-Oct-2020136.3 KiB

KHeap_DR.thyH A D30-Oct-2020167.4 KiB

Lemmas_D.thyH A D09-Apr-2020982

MoreCorres.thyH A D09-Apr-20204.7 KiB

MoreHOL.thyH A D09-Apr-2020347

README.mdH A D30-Nov-20201.1 KiB

Refine_D.thyH A D30-Oct-20202.3 KiB

Schedule_DR.thyH A D30-Oct-202035.8 KiB

StateTranslation_D.thyH A D30-Oct-202048.5 KiB

StateTranslationProofs_DR.thyH A D30-Oct-202012.8 KiB

Syscall_DR.thyH A D30-Oct-202082.5 KiB

Tcb_DR.thyH A D30-Oct-202090.6 KiB

Untyped_DR.thyH A D30-Oct-202087 KiB

README.md

1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7CapDL Refinement Proof
8======================
9
10This proof establishes that seL4's [abstract specification][aspec] is
11a formal *refinement* (i.e. a correct implementation) of its [capDL
12specification][capDL]. It is described as part of an ICFEM '13
13[paper][paper].
14
15  [aspec]: ../../spec/abstract/
16  [capdl]: ../../spec/capDL/
17  [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation"
18
19Building
20--------
21
22To build from the `l4v/` directory, run:
23
24    ./isabelle/bin/isabelle build -d . -v -b DRefine
25
26Important Theories
27------------------
28
29The top-level theory where the refinement statement is established over
30the entire kernel is [`Refine_D`](Refine_D.thy); the state-relation that
31relates the state-spaces of the two specifications is defined in
32[`StateTranslation_D`](StateTranslation_D.thy) and the basic
33correspondence property proved over each kernel function is defined in
34[`Corres_D`](Corres_D.thy).
35
36