Gerwin Klein
Gerwin Klein
- Remove remaining use of direct numeral related to `irq_len`. The lemma happened to work for `irq_len >= 8`, but not for smaller `irq_len`. - Improve sys-init example: the example...
We have at least two definitions of `tcbs_of`/`tcbs_of'` on the master branch, one in the fast path, one in Invariants_H (for at least some architectures). We should turn these into...
We made a number of small improvements to the haskell translator on the `rt` branch. We should cherry-pick or back port those that make sense to reduce the diff between...
As decided at the most recent TSC meeting, bump cmake format to the latest version. This will change/break style in many of the existing cmake files, but pinning pyyaml to...
Following on from the discussion in #1435, the PR there fixes most of the yieldTo misbehaviour apart from the issue that the kernel does not store enough information to decide...
We're currently relying on compiler optimisations to remove the function prologue for the idle thread. This does work correctly in the tests so far with the recommended tool chains, but...
Simplify installation and use the `mlton` included in the Isabelle distribution. Needs to be merged after Isabelle2025 (#882), because before that the included `mlton` is too old to support Arm...
We often declare Haskell assertions as `defs` with an immediate `declare x_def[simp]`, which is somewhat ugly. Since `defs` is being defined in this repo anyway, we could just was well...
See discussion on https://github.com/seL4/l4v/pull/846#discussion_r1903570321 -- it would be nice to collect lemmas like ``` lemma virqType_eq[simp]: "virqType = virq_type" ``` into one theory in Refine that is included relatively early....
This is a medium-size cleanup task. The function `get_tcb` defined in ASpec was an early attempt at a nicer accessor function for the heap, specifically for TCBs. It ended up...