l4v
l4v copied to clipboard
seL4
seL4 specification and proofs
This PR adds verification for the SGISignalCap API of [RFC-17](https://sel4.github.io/rfcs/active/0170-multikernel-ipi-api.html) (seL4/seL4#1222). Specs and proofs are updated for all architectures (affects mostly ARM, ARM_HYP, and AARCH64), including all affected parts of...
This generally follows the structure and naming conventions of the existing rule set for Hoare logic, in `Trace_VCG.thy` and `Trace_More_VCG.thy` (and the very similar ruleset and files in the nondet...
This makes two improvements for tracing rules applied by `wp_pre`. The first is that the resulting trace will be shown when `wp_pre` is called directly, not just when called from...
In a ccorres or wp proof with a `∃val. x = Some val` or anything like that, an accidental clarsimp will introduce new free variable, and if the schematic only...
As seen in https://github.com/seL4/l4v/issues/729 if wp or some other tool gets you into a bad situation, e.g. schematic assumption, `simp` will happily unify that with `False` which will result in...
When we try to make a rule to match a complex goal, we often want something like `epptr` in the rule, but we have `PTR(endpoint_C) (capEPPtr (projr luRet)))` or whatever....
As seen in this rambly gist https://gist.github.com/Xaphiosis/2fa2b51b65e05c3addda1576f90a31ed One way of getting around schematic unification disaster with the `vcg` method is via `subset_refl`. @lsf37 suggested we do this: `method svcg =...
Pulls in license change and content update of the Simpl session from the AFP. The license changes from LGPL to BSD-3-Clause. Flow-on breakage seems to be low, the main things...
This updates the TCB cap slots in the CapDL specification to match the output of the CapDL-tool. It also provides a new definition to hide these details and improve maintainability.
The specific case is `monadic_rewrite_symb_exec_r` which will attempt to automatically discharge, for example, the `no_fail` side condition. When it works, this is great, but when it fails there is no...