Hi Thanasis,
I am interested in finding the invariants at the abstract level regarding the capability management (CNode and CSpace). I would need some help with navigating the repository, because I am relatively new to interactive theorem proving in general.
- I think what I am looking for is in the `l4v/proof/invariant-abstract` directory inside the `{CNode, CSpace}*_AI.thy` files. Is this correct ?
You're in the correct directory, but the files you're looking at are the invariant proofs themselves, not the invariant statements. For just the statements, the following files are the most relevant:
InvariantsPre_AI.thy $L4V_ARCH/ArchInvariants_AI.thy Invariants_AI.thy
where $L4V_ARCH is one of ARM, ARM_HYP, X64, RISCV64, AARCH64. The latter two have more recent, slightly nicer formulations than the older files.
It might make sense to read these in reverse order, i.e. starting at the definition of "invs" in "Invariants_AI" and using jump-to-definition in Isabelle/jEdit for the conjuncts in that statement to see more detail.
As is usual in invariant proofs, these invariants are almost all interrelated in the sense that you usually cannot prove any of these in isolation -- you need to prove all of them simultaneously. There are sone small exceptions, but as a rule of thumb, they're one large invariant. That means, even if some of these don't look like they are related to capability management, they ultimately all are. (That said, we do apply a lot of proof engineering effort to prove things separately for as long as we possibly can before they all merge, so that small invariant changes still lead to small proof changes as often as possible).
As a first order approximation, anything that mentions "cap" in its name or definition will be fairly closely related to capability management. Not all of these are just about generic management functions alone, e.g. there are some interesting capability invariants in the architecture files.
- How can I distinguish between helper lemmas and the invariants that you state for example in your paper: SeL4: formal verification of an OS kernel ?
The invariants themselves are usually stated as definitions, the top-level statements are lemmas like "{| invs |} some_function {| _. invs |}". The invariant is "invs", the lemma shows that it is indeed invariant.
- Is there any textual artifact that lists the invariants in prose that could help me ?
No, not really, sorry. People request that from time to time, but apart form the work it would take, it is not without drawbacks to do this. The prose statements would have all the problems of natural language (not machine-checkable, either imprecise or harder to understand than the formula, danger of misunderstanding, etc) and they would be very quickly out of date. That means, people would prefer to read those over the formulas, because they would look easier to understand, but they would be almost guaranteed to be wrong after some time.
The high-level list in the paper is as close as we were comfortable doing as a separate document -- I hope we kept it high-level enough to have some time resilience while still being useful.
- Can you clarify me the relationship between the specifications in `l4v/spec/abstract` and the proofs in `l4v/proof/invariant-abstract` ? According to my understanding, the abstract specification defines the system in the abstract level, whereas the proofs use these definitions from the specifications to prove properties and invariants about them. So, the invariants are the statements that the proofs prove. Am I on the right track ?
Yes, that is right. In the example lemma statement above, you would find the definition of "invs" in Invariants_AI, the definition of "some_function" in spec/abstract, and the lemma statement in e.g. CSpace_AI.
Cheers, Gerwin