seL4-L4.verified

History

Rafal Kolanski fa9797948c arm+arm-hyp: remove duplicated ASpec asid bit definitions MiscMachine_A already contains asid_high_bits, asid_low_bits and asid_bits. Other architectures don't duplicate them in Arch_Structs_A, so ARM and ARM_HYP shouldn't either. For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to refer to the MiscMachine_A definitions when needed (CapDL duplicates them again in Types_D, but as they don't import machine theories, those can't be removed). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>		2024-08-08 18:05:03 +10:00
..
adl-spec	Fix refs_valid_procedures definition	2021-03-24 10:47:01 +11:00
cdl-refine	arm+arm-hyp: remove duplicated ASpec asid bit definitions	2024-08-08 18:05:03 +10:00
glue-proofs	license: provide documentation under CC-BY-SA-4.0	2020-03-16 14:19:15 +08:00
glue-spec	all: remove theory import path references	2020-11-02 10:16:17 +10:00
Makefile	Makefiles: remove unused report-regression target	2022-06-03 09:36:43 +10:00
README	licenses: convert license tags to SPDX	2020-03-13 14:38:24 +08:00
ROOT	camkes: ROOT updates	2020-10-27 15:52:31 +10:00
tests.xml	licenses: convert license tags to SPDX	2020-03-13 14:38:24 +08:00

README

<!--
     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: GPL-2.0-only
-->

CAmkES is a component platform for seL4. This directory contains files related
to a formal Isabelle model of CAmkES.

 adl-spec/ - Architectural model.
 glue-proofs/ - AutoCorres-based work (bottom-up approach to glue code).
 glue-spec/ - Behavioural model (top-down approach to glue code).