This directory contains markdown and theory files with conventions and other documentation for the l4v repository.
This is work in progress and contributions are welcome. Feel encouraged to raise pull requests for more material and/or corrections.
Current topics are:
- Setup for doing seL4 proofs
- Naming conventions in this repository
- Commit message conventions in this repository
- Proof style rules for this repository
- Using
find_theoremseffectively - Using
find_constseffectively - De-duplicating proofs
- Compacting proofs
- Architecture Split Why and How-To
- Haskell Assertions: how to use assertions in Haskell to use information from AInvs on Haskell and C levels
- General CRefine Notes
- Debugging VCG goals and failures in CRefine
- Platform branches -- what they are and how to update them
The directory plans/ contains ideas and plans for proof-engineering improvements in this repo. They are at the idea stage, not fully worked out yet. Feel free to contribute new ideas, to make an existing one more concrete, or to pick one up and work on it.