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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
