0cf64b5498
Avoid mixing `isabelle`, `make`, and `run_tests` invocations. Standardise on `run_tests` and mention `L4V_ARCH` each time to indicate that you can and should set `L4V_ARCH`. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
---|---|---|
.. | ||
Decode_SA.thy | ||
Ipc_SA.thy | ||
README.md | ||
Syscall_SA.thy |
README.md
Static Separation Kernel API
This specification is a cut-down version of the seL4 abstract specification that removes all system calls apart from notifications. The resulting kernel is a classic static separation kernel without any dynamism.
A proof that seL4 is equivalent to this cut-down version if configured
appropriately can be found in the proof
directory under
bisim
.
Building
To build from the l4v/
directory for the ARM architecture, run:
L4V_ARCH=ARM ./run_tests ASepSpec
Important Theories
Theory Syscall_SA
contains the top-level definition. The
specification directly includes parts of the 'normal' abstract specification
of seL4 from directory abstract
.