Rafal Kolanski

Some mods can't be found at all despite supporting current version

1

### Operating System Linux ### Version of PolyMC PolyMC 1.4.1 ### Version of Qt Qt 5.12.8 ### Description of bug I'm running MC 1.19.2 with Fabric loader. Doing a search...

Monadic_Rewrite overhaul

2

This is the final significant PR for the Monadic_Rewrite overhaul funded by the seL4 Foundation. There is one item outstanding: re-indenting `Fastpath_Equiv` and `Fastpath_C` but I don't want the noise...

Have wp warn when resulting in a goal with a schematic assumption.

15

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...

Some way of blocking `simp` from unifying schematics

1

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 =...

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...

There is this comment, in `CSpace_C`: ``` (* Useful: apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *}) *) ``` This...

There are a number of comments left over from past X64 verification efforts. Now that these have succeeded, removing them would be a good idea. Example: `(* FIXME x64: ucast?...

During work on AArch64 CRefine, we identified the following aspects of cleanup in `Wellformed_C.thy` which should be applied across all platforms once AARCH64 CRefine theories make their way into master:...