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 kernelhttps://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