Gerwin Klein
Gerwin Klein
So I might be a bit late to the game, but this trick we're using to force an enum to be `long` does not seem to be legal C according...
I think this discussion has come up before, but I'd like to document it and make sure we're on the same page. Currently it looks like it is possible that...
This is a follow-up issue for PR #636, where we fixed a potential use of scheduling contexts after deletion (after finalisation, really), leading to an assertion failure. sel4/sel4test#56 triggers this...
The manual currently talks about untyped objects, which is not really accurate and a source of confusion. I've tried to make some of that more precise in the tutorials in...
Raf's idea: one thing that is annoying to type in `crunches` is longer lambda expressions in `crunches`, e.g. the common pattern "%s. P (machine_state s)" We could add syntax for...
We currently have multiple word types in the abstract spec (and others) that are type synonyms with `machine_word` (`obj_ref`, `paddr`, `vspace_ref` etc). This means we get different names in input,...
We're currently attempting to build `SimplExportAndRefine` and `CKernel` for the MCS config of seL4 from the master branch of l4v. This was convenient because it kept the CI workflow simple....
The [Eval_Bool](https://github.com/seL4/l4v/blob/0f633ce3872b6b8748150c93da447e6dab89b261/lib/Eval_Bool.thy) theory defines a simp_proc and a proof method for reducing bool terms to values via the code generator. This is not a bad idea, but despite it being...
ASpec and ExecSpec were written before the "new" datatype package existed, which introduced selectors (named fields) and discriminators (`is_Cons`) for data types. In a number of places, we still have...
The MCS proofs for AInvs and Refine produced a number of enhancements and additional lemmas in the `Lib` session. We should backport these to `master` to reduce merge effort later...