Corey Lewis

> I've pushed my first attempt at this [here](https://github.com/corlewis/seL4/commit/2455b4d9235ab2707bdd513a5b9abd8cc2bb173b). I haven't properly tested all of the cases yet, but I think it should handle everything that we have mentioned so...

> > I haven't been able to work out a nice way of calling the invocations that makes use of them having optional parameters. > > From libsel4's point of...

This PR has now been updated with compatibility functions, and I think all existing issues and suggestions have been resolved. Verification is also now mostly complete, as seen at https://github.com/seL4/l4v/pull/505....

> It's possible to add multiple methods for the same id to libsel4/include/interfaces/sel4.xml with the following change: Thank you for the suggestion @Indanz, those changes worked perfectly. The latest commit...

> That's only because the new function doesn't accept a null cap. I think it would work if you change the if check in `updateAndCheckHandlerEP` to: To be precise, the...

> > A small alternative is that we could explicitly allow the combination of a null cap and a 0 badge value. That does start to feel a bit overly...

Rebased the branch, so that it can be tested with the verification changes.

> > Rebased the branch, so that it can be tested with the verification changes. > > You made a mistake with the rebase and modified all merged commits in...

In some sense there's two issues here, there's the new free variables that the schematic precondition doesn't depend on, and there's the fact that `wp` results in a schematic assumption...

> Thanks for tracking down the `wp_comb`! Do you think you'll have any time/willingness post-deadlines to take a look at de-`hoare_vcg_precond_imp`ing? It's not good to have an unsafe rule waiting...