Corey Lewis

> The line you linked to (https://github.com/seL4/l4v/blob/master/proof/invariant-abstract/Syscall_AI.thy#L1149) also declares `hoare_seq_ext` as `[wp]`, which is at least strange. Have you tried removing that one as well? I did try removing that...

> I've started having a look at this and while removing it doesn't affect too many lemmas, it does break more than I expected. So far it's only lemmas that...

I like the idea of `wp (once)` doing `wp_pre`, either as an explicit step on its own or as an implicit step as part of applying a different rule, but...

> I guess we could make it so that `wp (once)` is roughly `(wp_pre | wp_fix | resolve_ruleset_tac | cleanup_tac)` and depend on `wp_pre`, `wp_fix`, and `cleanup_tac` only being able...

I was more thinking to make `wp (once)` only do a single step, no matter which of the sub-tactics that step is actually doing. So with a 'standard' goal, the...

> This looks good to me. I'm not too worried about the performance impact -- it's not like this runs in a tight inner loop somewhere. We do use it...

> I just remembered that I wrote that benchmarking script. I agree that the performance impact should be negligible but now I'm curious if we'll be able to even see...

For completeness, these lemmas are ``` "(if P then 1 else 0) = (0 :: 'a :: zero_neq_one) ⟷ ¬P" ```

Sorry, just noticed that I never replied. No concerns from my side and I think it is a good idea to minimise the dependencies.

> This might have verification impact for the system initialiser. @corlewis do we need to do anything special in the tools or is this just excluded in spec wellformedness for...