6418bda962
findVSpaceForASIDAssert is needed for modeling the hardware ASID lookup on ARM. None of AARCH64, RISCV64, X64 use that mechanism and the function is unused. There are some proof about it, but those are unused as well. This commit removes all of these. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| ARM | ||
| ARM_HYP | ||
| RISCV64 | ||
| X64 | ||
| autocorres-test | ||
| base | ||
| intermediate | ||
| lib | ||
| Move_C.thy | ||
| README.md | ||
README.md
C Refinement Proof
This proof establishes that seL4's C code, once translated into Isabelle/HOL using Michael Norrish's C parser, is a formal refinement (i.e. a correct implementation) of its design specification and, transitively (using the results of the Design Spec Refinement Proof) seL4's C code is also a formal refinement of its abstract specification. In other words, this proof establishes that seL4's C code correctly implements its abstract specification.
The approach used for the proof is described in the TPHOLS '09 [paper][5].
Building
To build from the l4v/proof directory, run:
make CRefine
If you wish to build for a specific architecture other than the default, set
your L4V_ARCH environment variable accordingly, as documented for the C code
translation.
Important Theories
The top-level theory where the refinement statement is established over
the entire kernel is Refine_C; the state-relation that
relates the state-spaces of the two specifications is defined in
StateRelation_C.
Note that this proof deals with two C-level semantics of seL4: one
produced directly by the C parser from the kernel's C code, and another
produced by the C spec's Substitute
theory. These proofs largely operate on the latter, proving that it
corresponds to the design spec. Refinement between the two C-level specs
is proved in the CToCRefine theory.
The top-level Refine_C theory quotes both refinement
properties.