docs: add debugging tips for vcg goals

docs/README.md

@@ -18,13 +18,17 @@ Current topics are:
 
 - [Setup](setup.md) for doing seL4 proofs
 - [Naming conventions](conventions.md) in this repository
+- [Commit message](commit-messages.md) conventions in this repository
+- [Proof style](Style.thy) rules for this repository
 - Using [`find_theorems`](find-theorems.md) effectively
 - Using [`find_consts`](find-consts.md) effectively
 - [De-duplicating proofs](de-duplicating-proofs.md)
 - [Compacting proofs](compacting-proofs.md)
 - [Architecture Split](arch-split.md) Why and How-To
 - [Haskell Assertions](haskell-assertions.md): how to use assertions in Haskell to use information from AInvs on Haskell and C levels
-- [CRefine Notes](crefine-notes.md)
+- General [CRefine Notes](crefine-notes.md)
+- [Debugging VCG](vcg-debugging.md) goals and failures in CRefine
+- [Platform branches](platform-branches.md) -- what they are and how to update them
 
 ## Plans
 

docs/crefine-notes.md

@@ -229,45 +229,40 @@ These are some things that may happen and some hints do deal with it:
 
 ## Proving the Hoare triple
 
-Mostly every time, this phase is just a sequence of application of `wp` and `vcg` tactics.
+Mostly, this phase is just a sequence of application of `wp` and `vcg` tactics.
 
-However here are some tricks when it could go wrong:
+However here are some tips for when things go wrong:
 
-* if the vcg is expanding all the state, then
+* if `vcg` is expanding all the state, see the [VCG debugging guide](vcg-debugging.md#vcg-takes-very-long).
 
-
-  ```
-  apply (rule conseqPre)
-
-  ```
-  just before
-
-
-* sometimes the precondition generated by `wp` or `vcg` contains False somewhere (we figure it out while trying to prove the 'last big subgoal')
-so a simplification before the `wp`/`vcg` is needed...
+* sometimes the precondition generated by `vcg` contains `False` somewhere or leaves an unprovable
+  goal (we figure it out while trying to prove the 'last big subgoal') so a modification before
+  `vcg` is needed. See the [VCG debugging
+  guide](vcg-debugging.md#unprovable-goals-and-false-in-the-post-condition) for these cases.
 
 ## Proving the 'last big subgoal'
 
 This 'last big subgoal' is where we prove that the `P` and `P'` appearing in the lemma statement imply the `?Q` and `?Q'` that have, at that point, been instantiated to a big conjunction of all the preconditions computed to fulfil the Hoare triple for each instruction of the program.
 
-The first thing that may happen here is that you end up needing to prove False. This is due to a simplification along the proof that instantiated a schematic precondition to 'False' to fulfil the goal (e.g. `?Q ⟹ bla`). The only thing to do here is to go back into the proof to see where it is generated and try to avoid it (sorry, not better clue...)
+The first thing that may happen here is that you end up needing to prove `False` or get an
+unprovable goal from the C `vcg`. See the [VCG debugging guide](vcg-debugging.md) for more
+information.
 
 Another problem is to deal with sometimes 40 goals after expansion of this last goal, and usually very similar goals. So this idea is to 'generate' the more useful premises as possible before expanding (by `subgoal_tac` or `frule`).
 
 In this context, a trick that helped me is that if some subgoals depend on an equality (e.g. one subgoal being `a = b ⟶ P`), then try to formulate the lemma you want to use as frule (before expansion) as
 
 
-```
+```isabelle
 ⟦ bla ⟧ ⟹ a = b ⟶ P
-
 ```
-instead of
 
+instead of
 
-```
+```isabelle
 ⟦ bla; a = b ⟧ ⟹ P
-
 ```
+
 (because if not you will need first to expand and then to do `impI` and then to apply the lemma, whereas in the first case, you can do frule before expansion and hopefully even have the subgoal proved automatically).
 
 ## Some other hints
@@ -295,14 +290,8 @@ instead of
 
 
 
-* if the `vcg` takes too long, then it is probably expanding the state (see above). Usually it is when the precondition is an intersection...
-So just before the `vcg`, just do `apply (rule conseqPre)`
-* You can turn off (some) of the hoare package's funky syntax translations using
-
-
-  ```
-  ML {* HoareSyntax.use_call_tr' := false *}
-  ```
+* if the `vcg` takes too long, see the [VCG debugging guide](vcg-debugging.md)
+  for strategies.
 
 
 

docs/vcg-debugging.md

@@ -0,0 +1,125 @@
+<!--
+     Copyright 2024, Proofcraft Pty Ltd
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# VCG debugging techniques for CRefine
+
+## Unprovable goals and `False` in the post condition
+
+When using `vcg`, situations arise where schematic instantiation to `False` can
+happen due to unification failure -- mostly during simplification. This is
+usually hard to find because `False` itself does not necessarily show up, for
+example you may get something like this:
+
+```isabelle
+   ∀cte cap.
+      ccap_relation (cteCap cte) cap ⟶
+      cap_get_tag cap ≠ signed cap_vspace_cap ∧ ...
+```
+
+Which is obviously not provable, because we don't have any information about
+`cap` to work with. What it should have generated is something like:
+
+```isabelle
+   ∀cte cap.
+       ccap_relation (cteCap cte) cap ⟶
+       (∀t. cap_get_tag cap = signed cap_vspace_cap ⟶ ...)
+```
+
+This means that some conjunct in the `...` above got resolved to `False`, which
+got simplified to the unsolvable goal.
+
+The way to track down these issues is to go over the `vcg` steps to see which
+ones introduced the unexpected result. However, with large goals this is very
+difficult to work with. What else can help?
+
+First, try removing `(P ⟶ False) = (¬ P)` from the simpset, so we can look for
+`False` in the goals:
+
+```isabelle
+  supply simp_thms(19)[simp del]
+```
+
+Second, if you do have identified a suspicious `vcg` invocation that could
+result in a bad instantiation, try the following instead of only `vcg`:
+
+```isabelle
+  apply (rule conseqPre, vcg, rule subset_refl)
+```
+
+For a "good" goal, this sequence will succeed and leave a goal to prove which
+has no schematic variables in the assumptions (ideally also not in the
+conclusion, but those should be harmless for this purpose). If this sequence
+fails, then there most likely is a problem with the parameters of the schematic
+precondition the goal is allowed to depend on, e.g. you have `?P x` in the
+precondition, but `vcg` is generating a goal that depends on add additional
+parameter `y`.
+
+This can happen when new parameters are introduced by `exE`, `clarsimp`, case
+distinctions, or other tactics. For instance you might have `x = Some y` in the
+assumptions and `?P (Some y)` as the schematic precondition, but the `vcg` needs
+`?P y`. Unification is generally not smart enough to figure out that `P (the
+(Some y))` would be a solution. The following strategies may help:
+
+* try using the tactic `wpfix`. It can sometimes resolve the problem by
+  replacing `?P` with a new `?P` that is allowed to depend on more parameters.
+
+* go back to the place where the schematic `?P` is introduced and introduce the
+  parameter before the schematic, so `?P` can depend on the parameter. This could
+  happen for instance by using a better case distinction rule that manages
+  schematics, or by performing the relevant `exE`, `clarsimp` etc before the
+  schematic is introduced (not always possible).
+
+* go back to the place where the parameter `y` is introduced and prevent it from
+  being introduced. E.g. instead of using `clarsimp` to generate `x = Some y`
+  and using `y`, be careful to keep the form `∃y. x = Some y` in your
+  assumptions (or prevent it from even occurring when possible, e.g. by blocking
+  a `x ≠ None` rewrite or using `Lib.not_None`). Then use `the x` instead to
+  access the content of `x`. This is not necessarily nice, but should always be
+  available in principle.
+
+* it is sometimes possible to use `wpc` in `ccorres` goals to produce sub goals
+  that provide access to the correct set of parameters (e.g. a `None` case and
+  `Some y` case, where `y` is fine to access). This can also be used when one of
+  the cases is impossible by showing a contradiction for that branch.
+
+In summary, beware not only of `simp`, which might instantiate schematics, but
+also of otherwise safe tactics like `clarsimp` and `exE` when working with `vcg`
+goals that still have schematic variables.
+
+## VCG takes very long
+
+Sometimes the `vcg` invocation takes very long for simple goals. There are two
+potential reasons for this.
+
+* `vcg` might be expanding the state record into its many constituents. While
+  this is a good tactic for the `vcg` for making progress in smaller state
+  spaces, the C state in `l4v` is too large for this, and even printing the goal
+  state will take a long time in expanded form with hundreds of state variables.
+
+  To avoid this, use `conseqPre` before you apply `vcg` so that there is no
+  concrete state the `vcg` can split on. You can resolve the generated
+  implication immediately with `subset_refl`, so the full form is the same
+  as for avoiding instantiation to `False`:
+
+  ```isabelle
+  apply (rule conseqPre, vgc, rule subset_refl)
+  ```
+
+* `vcg` might be trying to inline multiple function definitions and the goal is
+  then not actually as small as it looked. When this happens the `vcg` prints
+  info messages about this unfolding. Prove specification lemmas for the
+  functions instead to avoid unfolding.
+
+If you do get a legitimate goal that is very large, you can try to at least
+speed up printing at the cost of not expanding syntax and syntax translations:
+
+* Use `supply [[goals_limit = 1]]` if you have more than one goal
+* Use the `Quick print` option in jEdit to turn off translations
+* Turn off some of the Hoare package's funky syntax translations using
+
+  ```isabelle
+  ML {* HoareSyntax.use_call_tr' := false *}
+  ```