Hello,
I am from Lin Zhong’s group at Yale University and I am currently looking at
the seL4 specifications and proofs.
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 ?
- 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<https://dl.acm.org/doi/10.1145/1629575.1629596> ?
- Is there any textual artifact that lists the invariants in prose that could
help me ?
- 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 ?
Thank you for your help,
Thanasis Typaldos
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
