simpler corres and corressimp methods

[lsf37]

Dan built two fairly sophisticated proof methods for refinement proofs, corres and corressimp, but we don't use them a lot.

One reason for that is that we're currently mostly updating existing corres proofs and not writing very many new ones. The other reason is that they don't fail in very useful ways. I.e. when they succeed, it's great, but when the methods fail it is very hard to understand why and where, and even harder to figure out how to make progress from there.

My guess is that if we simplify these methods so that they do much less, it will be easier to form a mental model of what they are doing and therefore to use them more productively. They'll probably solve a lot fewer goals automatically, but if it's clear how to make progress on the goals that they leave over, I think they'll be used a lot more.

Similar (but but not equal) to how clarsimp is a lot easier to use incrementally than force or blast, because it makes incremental progress and one can usually understand how to add things to make more progress.

For instance, one thing that Dan did for these methods is to change the underlying corres calculus such that it better supports automation. That new calculus definitely is better for automation, but since we don't use it manually, we don't really understand its subtleties.

My proposal would be as first step to write a completely naive corres method that only know how to split off bind with functions it already has rules for. Maybe, as a plus, it can attempt to immediately solve the wp goals that it produces, but that is already advanced.

Opinions and discussions welcome!

[Xaphiosis]

Some extra thoughts:

corres has issues with single-sided rules, e.g. dealing with an assert on either side

Best-guess automation as with crunch really benefits from tracing and feedback, especially with a two-stage cascade of corres rules + wp[simp]. Things could go wrong at either stage, and being able to trace which corres rules were used is invaluable.

The way wpsimp et al only split off a chunk (bind) if they can do something with it is nice, we should keep that.

Graceful degradation is helpful, i.e. being able to get dumped in the middle of a failed wp discharging after the corres. For bonus points, being able to resume after human assistance would also be helpful, but that can get really weird given that corres can spit out combinations of corres and wp goals, and we wouldn't want the tactic to just keep eating away at goals as long as they are of either form. I guess one could limit the number of goals, but by that argument one could also do (my_tactic+)[n_goals].

It sucks to have to specify corres_split_eqr[OF my_corres_rule] and similar. Would be nice to be able to only give it my_corres_rule. This would necessitate some kind of basic mechanism to go from user-specified, to most specific, to more generic rules?

[lsf37]

Ok, here a first few lines for discussion:

method corres_cleanup = assumption | rule refl
method corres_split declares corres = ((rule corres_split, (rule corres; corres_cleanup?))+)[1]
method corres_split_simp uses simp declares corres = ((corres_split corres: corres | clarsimp simp: simp)+)[1]

As @Xaphiosis pointed out on chat, this needs a bit more refinement and thinking. In particular:

• we should add something like wp_pre, e.g. a corres_pre method
• it should not just be the specific corres_split rule. Probably should be a corres_splits set.
• is the cleanup step safe?
• is the ; safe?
• should it really iterate with + or is there a better, more controlled method
• is the clarsimp a good idea?
• should there be a wpsimp step?

I think we should constrain the focus of this method somewhat. The 3 lines above are definitely not the final method, but they are already pretty useful in the example I tried and do almost all I wanted for it.

As I see it, there are roughly 3 kinds of corres rules:

• split rules that produce new corres goals. They usually produce wp goals as well.
• terminal rules that solve a corres goal. They often have side conditions.
• everything else, in particular symbolic execution such as for assert, but also guard crossing rules, rewriting etc

What I think is easily automatable:

• solving terminal corres goals with simple side conditions that already exist in the goal
• splitting off a new head goal that is terminal and immediately solving that with the previous method, leaving a new head goal and some wp conditions to be solved later.

What I don't think is easily automatable:

• side conditions that need further proof
• symbolic execution and/or asserts

Leaving out symb_exec rules is easy, we can just not provide them. The other point is almost impossible, because terminal corres rules might have side conditions that look simple (e.g. asid' = asid or asid_pool_relation pool pool') or are usually in the goal, but sometimes they only follow after further reasoning, and which of these is the case depends on the goal, not necessarily on the rule.

The usual way to deal with this kind of problem is to move the verification of such side conditions to later. In the current corres calculus this is not possible -- you can't put asid' = asid into the guards of the corres rule, because it mentions both abstract and concrete values (you can put them into the rule, but the rule will never unify with the goal, because in the goal, the abstract guard can only depend on abstract values and the concrete guard only on concrete values). This is why Dan changed the calculus into corresK where that is possible. It turns out that while this is technically the better way, it is not being used, because it's too hard to understand what is going on (I don't think the corresK calculus is too hard to understand in general, it's just that we don't use it and having two is too much -- if we changed everything into corresK it might work just fine, but that is a huge amount of work).

So, the best we can do when we apply a terminal corres rule is to apply the rule and attempt to solve the side conditions, and either stop and hand over to the user in this unsolved state or give up and stop completely. I think that's Ok, this entire argument was just to map out expectations.

For these two questions:

• is the cleanup step safe?
• is the ; safe?

corres_cleanup is only used for those terminal rules. In general, when apply a terminal corres rule, we expect that terminal rule to instantiate all schematics. So when we resolve the side conditions of the rule, there should be no schematics left in the goal. This means the cleanup step and the ; operator for it should be safe. In fact, instead of just assumption | rule refl in corres_cleanup, we should probably make that a bit stronger and at least add a clarsimp.

• should it really iterate with + or is there a better, more controlled method

I'm not sure there is, but I'm open to ideas. The idea is that the terminal step might fail to resolve all side conditions, in which case we want the tactic to stop and not attempt to work on any goals further down in the chain.

• should there be a wpsimp step?

The wp goals that are created by split rules will only have non-schematic post conditions when we are fully done with the corres part. If we can detect that scenario, then a wpsimp+ would make sense and could add some power for simple things. I would not usually expect the method to get that far, because it's rare that everything can be solved without manual reasoning in between, but it could be useful for really simple cases.

[Xaphiosis]

I'll think some more, but meanwhile point out that I would encourage a browse of the Monadic_Rewrite tech I developed, to try not have to duplicate some of the pain that that evolution experienced. For example, the absence of solves anywhere is ok now, because your cleanup is only rule refl | assumption, but will fall apart the moment that gets extended with another tactic, and needs reading all the way down to understand (and I already noticed you want to add clarsimp, so you see my concern is not entirely unfounded).

[Xaphiosis]

I do not agree with closing off symbolic execution early. That kind of approach results in someone doing another approach later, or using your method for hammers like (your_method | rule corres_assert | whatever)+
With asserts, I'm thinking you want one of a few basic behaviours:

• on the left, you can't do anything with it if it didn't simplify away, need to fold into the wp goals
• on the right, you can either fold the condition into the wp goals, or you can try cross it from the abstract side
• when both on the right and the left, you can try demonstrate they are the same assertion and only put it into wp on the abstract side
  Maybe I'm misunderstanding the corres flags involved here, or over-engineering.

There are other situations like when we're dealing with machine ops that I don't really remember, but while the tactic doesn't have to deal with that now, it would be nice to be able to expand it to deal with some of those situations (such as a chain of provably identical machine ops on both sides).

My initial thought was also that some rules are used with corres_split_eqr and others, more specific rule modifiers. Being able to override / tweak / add to those is what makes for a scalable method. Same with adding to the cleanup.

I guess if I were to summarise what bothers me about the current approach is exactly that "they are already pretty useful in the example I tried and do almost all I wanted for it":

• the highest method will clarsimp goals when it didn't successfully split (if_split warning)
• there's no way to add to the cleanup operation
• an "obvious" assert will stop things dead with no visible way to give it a rule/strategy to get over it
• corres_cleanup gets invoked without a solves and is attempted on all goals it can reach, including the tail of the corres (we made tactics to pattern match goals, also if_split warning)
• if you want to take these and build something bigger with them, they aren't stable or extensible
• (minor) no doc strings indicating intent of methods

My vision for how this should go is that for a braindead linear corres proof, we should be able to one-line it, go as far as being able to handle a matching if on both sides, and being able to dump in a rule or two for almost-braindead corres and be able to extend to other situations like machine ops, bindE, or something we haven't thought of yet.

[Xaphiosis]

From MM: I apologise for sounding overly critical, but for the monadic rewrite stuff I hammered out a lot of edge cases to make sub-methods and sub-tactics stable and therefore being able to be assembled into bigger steps/tactics (extending monadic_rewrite to wp_pre, configurable action and finalise, using determ, solves, fwd_all_new, repeat_unless, if_then_else, no_name_eta) ... and then this new approach completely ignores all of that and goes back to the oldschool (rule my_rule | clarsimp | rule refl | assumption)+ approach.

I really don't want to see those approaches immediately forgotten by default :/

[Xaphiosis]

Ok, here are some draft features I think we want

• generalise wp_pre's code to be generic over some pattern (pre_tac?)
• make sure the above pre_tac-like can initialise corres_guard_imp when not already schematic
• deploy no_name_eta before any split rule for more stable names
• expand list of split rules (at minimum corres_splitE)
• think very hard about doing that clarsimp on a corres goal and just leaving it when we aren't able to split - an approach like wpsimp is better: try clarsimp first, and abort it if we can't split
• consider allowing user-supplied split rule(s) (carefully, as with wp some rules should go ahead of user's rules, some after)
• remove if_split from any clarsimps that target corres goals in the tactic
• add clarsimp of some kind to corres_cleanup
• allow user-supplied method to try in corres_cleanup
• have corres_cleanup fail on corres goals
• add solves to the invocation of corres_cleanup (but not to corres_cleanup) (see next point)
• consider something like fwd_all_new for application of solves <corres_cleanup?>, in order to leave only unsolved goals instead of stopping on first unsolved goal (that was what I meant with thinking about + before) ... note that using fwd_all_new benefits from pattern match to avoid trying to solve the generated corres goal
• add method docstrings to let people know the goals of each method
• consider handling of assert (probably needs user-supplied rule to handle both cases of what to do with RHS: cross vs. wp)
• examine what can be done with machine ops wrapped in doMachineOp
• consider deployment on wp goals and wpsimp

That's what I thought of for the time being. Additions and comments welcome.

edit: remove wp_pre abuse

[lsf37]

The checklist is looking pretty good. Esp agree that the clarsimp needs more finesse (and all the bits not mentioned below).

There are some bits where don't seem to be quite on the same page yet:

• think very hard about doing that clarsimp on a corres goal and just leaving it when we aren't able to split - an approach like wpsimp is better: try clarsimp first, and abort it if we can't split

The clarsimp is specifically there to run on corres goals, I was actually thinking about guarding it so that it applies to only corres goals. The idea is that you often want to be able to tweak the corres goal slightly, i.e. unfold some function to inline it or unfold a liftM or something like that, and you want to be able to inspect the proof goal when it has done that but has not successfully split off anything yet, so you can tweak what you're doing there. wpsimp is actually implemented precisely like this -- it first tries wpfix | wp | wpc before it tries the clarsimps, and then loops. That's the same it does here and I think that is the right way around.

Having said that, corres is more subtle and fragile than wp goals, so I definitely agree that we need to be more careful. In addition to the if_split removal, I propose to use a cong rule that makes it rewrite only in the monad part and that protects return relation and predicates (with option to override the cong rule).

Because of the outer + the clarsimp will only ever be applied to the head goal. If we additionally guard it such that it only applies to corres, we get that it is only ever applied to the head goal when that is a corres goal, which I think is what I want it to do.

• have corres_cleanup fail on corres goals

corres_cleanup is only ever applied to the side conditions of terminal corres rules. By definition, these cannot be corres goals (otherwise that would have to be a split rule).

Edit: I'm arguing above that having cores_cleain fail on corres goals is not necessary. Thinking further: so what if we do it anyway, do we gain anything? I think we might: we could then allow terminal corres rules that are not really terminal, e.g. transformation rules that turn one corres form into another one. I had initially excluded that, because it's not safe -- it would make a split applicable where the next step is just a transformation and not a terminal rule that will solve something. I still think that such rules should never be declared [corres] globally, but one could imagine a situation where such a rule will only apply at a specific place inside a function and where we supply in manually for that case. That would be fine. A (conceptual) corres_split, corres_terminal chain would then just do the split and that transformation rule, but in the next iteration we'd presumably solve the (then hopefully) terminal case without further splitting. I think that'd be Ok.

• add solves to the invocation of corres_cleanup (but not to corres_cleanup) (see next point)
• consider something like fwd_all_new for application of solves <corres_cleanup?>, in order to leave only unsolved goals instead of stopping on first unsolved goal (that was what I meant with thinking about + before) ... note that using fwd_all_new benefits from pattern match to avoid trying to solve the generated corres goal

I agree with you about the + here, but it currently isn't actually using that :-). corres_cleanup is applied with ; which does not stop at the first side condition, but applies to all of then. Remember, the cleanup is only called for the side conditions of terminal corres rules -- at terminal rules there can't be any schematics in the goal any more (if there are we have already screwed up earlier or in the rule itself), so the order doesn't matter, which is why it's using ; instead of fwd_all_new.

The solves part needs more thinking. Initially I was agreeing with you (I think you mean (solves <corres_cleanup>)? unless I'm missing a subtlety), and the simple 3-liner I posted does actually have that property.

We might still go that way, but after thinking more about it, I have more doubts. The side conditions of terminal rules is where we spend the actual manual proof time of the corres part (apart from wsimp and the final two implication goals). I'm having trouble imagining one where I wouldn't want to say clarsimp first or where that is at least not safe to do. It does have the disadvantage of leaving a goal that is not precisely in the form we get after just corres rule applications, but it is extremely similar to what we get out of wpsimp as final implication goal, which also always has clarsimp applied to it.

Maybe we need to experiment with this one a bit, I currently can't tell what is more useful. I'd want to avoid the situation where we always call apply (corres_simp, clarsimp).

(Not entirely by thoughtful design the 3-liner does actually always apply clarsimp to those side conditions that aren't solved, because if the side condition proof fails, it will be left in the goal, the corres split will fail, and the clarsimp will be called, which will end the outer loop. For the admittedly few goals that I played with, that clarsimp on the terminal-rule side condition worked very nicely).

• consider handling of assert (probably needs user-supplied rule to handle both cases of what to do with RHS: cross vs. wp)

This is an interesting one. I don't see asserts working as a general capability of the method that it always tries, because they cannot be made safe in general, but as potentially user-supplied rules or maybe even a method that you put in when you know what you want to do, that is a different situation. It could even be a built-in capability that usually gets an empty lemma set (and therefore fails/does nothing), but you can put switch it on by providing the right rule when you want to use the capability. Something like that.

I'd build the rest first and then see how we can add this before we deploy the method more widely.

• examine what can be done with machine ops wrapped in doMachineOp

That could probably be done as a separate extension, because it's unlikely to break anything or change fundamental behaviour of existing applications of the method. I'm not sure we actually need to change anything in the method, it's possible that just providing the right split rule and potentially simp rules does make that bit work (for simple doMachineOp corres goals, the 3-liner already worked, so this would be those case where they are wrapped differently in ASpec vs Haskell).

[lsf37]

Ok, here is a larger new draft for further discussion (untested and still incomplete -- imagine all the parameters properly passed through from the top instead of just simp/cong).

method corres_rel = (WP_pre.pre_tac corres_rel_imp)?

method is_corres = rule corres_inst
method is_wp = rule hoare_triv (* add validE + variations; also no_fail? *)

named_theorems corres_splits
method corres_split declares corres_splits = no_name_eta, rule corres_splits

method corres_cleanup methods m uses simp simp_del split split_del cong intro =
    m
  | assumption
  | rule refl
  | clarsimp simp: simp split: split split_del: split_del cong: cong intro!: intro
  (* enables passing in conjI for terminal goals: *)
  | (rule intro;
     corres_cleanup m simp: simp simp_del: simp_del split: split
                      split_del: split_del cong: cong intro: intro)

named_theorems corres
method corres_terminal methods m uses simp cong declares corres =
  (rule corres | corres_rel, rule corres);
  (fails ‹is_corres›, fails ‹is_wp›, solves ‹corres_cleanup m simp: simp cong: cong›)?

method corres' methods m uses simp cong fallback declares corres corres_splits =
  ((wpfix
    | corres_pre
    | corres_terminal m simp: simp cong: cong corres: corres
    | corres_split corres_splits: corres_splits,
      corres_terminal m simp: simp cong: cong corres: corres
    | corres_terminal m simp: simp cong: cong corres: fallback
    | wpc
    | succeeds ‹is_corres›,
      clarsimp cong: corres_weaker_cong simp: simp cong: cong split del: if_split
    | succeeds ‹is_wp›, (wpsimp simp: simp cong: cong)+
   )+)[1]

method corres uses simp cong declares corres fallback corres_splits =
  corres' ‹fail› simp: simp cong: cong corres: corres fallback: fallback corres_splits: corres_splits

This is now a version that will not leave an unfinished clarsimp for the side conditions of terminal corres rules. Still not sure that's what we want, but happy to experiment. It'd be relatively easy to change this into using clarsimp in the outer loop for fails ‹is_wp› instead of succeeds ‹is_corres›.

Another question is if the whole thing should be prefixed by an succeeds ‹is_corres›, so that we don't start using the corres tactic as a wpsimp call. On the other hand, maybe that is allowable, so that (corres ..)+ does solve wpsimp goals left over from previous (maybe manual) corres steps.

Edit: updated this with a fallback parameter for asserts and similar. Rules supplied with corres get tried first, so if we were to say

apply (corres corres: corres_assert_gen_asm_l)

then corres_assert_gen_asm_l would take always precedence over situations where there is an assert on both sides, which we don't want, but applying supplied corres rules always late would mean that you can't force your own rules for special situations. With this version you can say

apply (corres fallback: corres_assert_gen_asm_l)

which will apply the safe standard rules first, and the supplied rules when neither terminal nor split step succeed.

[lsf37]

• add method docstrings to let people know the goals of each method

Sadly, Eisbach methods don't have doc strings. Comment is the best we can do currently.

[Xaphiosis]

This is much more thorough. More inline comments would be good as well to walk the reader through intent, there are a lot of stages going on. Would like to discuss and go through this, it'll be very easy for me to miss something otherwise.