Gerwin Klein
Gerwin Klein
Currently, `vppi_event` is defined as ```isabelle "vppi_event irq = do cur_vcpu ← gets (arm_current_vcpu ∘ arch_state); case cur_vcpu of Some (vcpu_ptr, True) ⇒ do do_machine_op $ maskInterrupt True irq; vppi...
The "Orphanage" theory in the Refine session was added to make sure that thread states correspond to the scheduler queues, i.e. that no running threads can become orphaned by being...
We have lots of custom commands and automation available in `lib/` but they are hard to discover, some are undocumented, and are therefore in danger of falling out of use...
[AddUpdSimps.thy](https://github.com/seL4/l4v/blob/master/lib/AddUpdSimps.thy) should probably be used more, but has no documentation, is hard to discover and has no examples/test cases. This issue is for rectifying docs, examples, and tests.
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...
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.
We should check for minimum `gcc` and `clang` versions in the cmake files to avoid hard-to-debug messages at some late point in the build. See for instance #574 The current...
Add a trigger via label for starting a sel4bench run on seL4 repo PRs (similar to running the hw tests or proofs).
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...