l4v
l4v copied to clipboard
seL4
seL4 specification and proofs
When PR #410 is merged, the proofs will be generic in the number of protection domains. Testing that fact with every CI job is going to be too resource-intensive, but...
Dear， I want to use predicate corres_underlying to prove the correspondence between two whileLoop or two whileLoopE, but I have not found the relevant lemma in the file corresponding_UL.thy. Does...
The PR seL4/seL4#243 fixes an issue in `PageGetAddr` and `SchedContextYield` + `SchedContextConsumed`. The underlying problem in that issue is that in the (already verified) `PageGetAddr` we do not use the...
See discussion on seL4/seL4#443 -- the parser should produce an error message for this case, not just fail silently.
Several proof directories on the rt branch had diverged from master in unexpected ways. This commit manually brings them back in sync. The specific directories are access-control, bisim, dpolicy, drefine,...
This PR solves a bit more than 1/3 of the open proofs for the abstract invariants of the AARCH64 configuration. In particular, it provides all basic lemmas for virtual address...
This is the final significant PR for the Monadic_Rewrite overhaul funded by the seL4 Foundation. There is one item outstanding: re-indenting `Fastpath_Equiv` and `Fastpath_C` but I don't want the noise...
This PR reorders the assumptions of the various `corres_split` rules, finishing the work started in https://github.com/seL4/l4v/pull/218. The changes in this PR were produced first by a sequence of `sed` and...
Currently `cinit lift: x_'` leaves an assumption of the form `x = t` in the assumptions, where `x` is a new parameter (the lifted `x_'`) and `x` occurs in the...