47119bf43e
The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+
- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.
- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.
|
||
|---|---|---|
| .. | ||
| AbstractSeparationHelpers_SD.thy | ||
| AbstractSeparation_SD.thy | ||
| Frame_SD.thy | ||
| Helpers_SD.thy | ||
| Lookups_D.thy | ||
| README.md | ||
| Sep_Tactic_Helper.thy | ||
| Separation_SD.thy | ||
| Types_SD.thy | ||
README.md
CapDL Separation Logic Proof
This proof defines a separation logic for the capDL kernel specification. It builds on a generic separation algebra, described in the ITP 2012 paper.
The separation logic is defined on a lifted heap where we lift the object heap and IRQ table into an object-component heap and an IRQ table heap. This gives us a separation algebra with a capability-level of granularity.
This separation logic is used by the CapDL API Proofs and the system initialiser specification.
This separation logic is described in the ICFEM '13 paper and Andrew Boyton's PhD thesis.
Building
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b SepDSpec
Important Theories
-
The definitions of heap disjunction, heap addition and showing that they produce a separation algebra is found in
AbstractSeparation_SD. -
The "arrows" are defined in
Separation_SD. -
The "frame rule" for specific leaf functions is defined in
Frame_SD. This "frame rule" is different from the traditional frame rule as we use a shallow embedding.