Common tactic machinery for symbolic execution of pure reductions

The goal of this merge request is to unify some machinery used for performing pure symbolic reductions in a way that would allow for better code reuse between WP and e.g. sequential WP or WP for total program correctness.

Overview

The way that symbolic execution for the WP-calculus (for heap_lang) is implemented right now is basically as follows. For each possible reduction in the language there is a Coq tactic lemma (that can be iApplied) and a corresponding Ltac code that

• Tries to find the place where this lemma can be applied
• Applies the lemma
• Gets rid of some clutter (e.g. reduces #();; e to e).

If one wants to implement tactics for symbolic execution for WP for total program correctness or for if-convergence, then essentially all this effort has to be duplicated.

These sort of issues arose in the formalisation of logical relations that we were working on with @robbertkrebbers. There we had several layers of tactics for symbolic execution: in the weakest precondition, in the ghost threadpool, and on both sides of the logical relation. After having troubles maintaining 4*n tactics and tactic lemmas we decided to abstract it away as follows.

Implementation and advantages

For each "layer" of symbolic execution you have an "open ended" tactic/lemma that is parameterized over a typeclass:

Lemma wp_pure' `{Inhabited state} K E e1 e2 φ Φ :
  PureExec φ e1 e2 →
  φ →
  (▷ WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.

The typeclass PureExec φ e1 e2 says that there is a pure (and deterministic) reduction from e1 to e2 in the language under some (pure) assumption φ.

The instances for the PureExec typeclass are declared separately and can be reused for symbolic execution lemmas for constructs other than WP.

Then, there is a single Ltac tactic wp_pure for applying the said lemma. All the other tactics for pure reductions are defined in terms of it (see proofmode.v for examples).

Another advantage of having a single tactic is that you can use it to perform as much pure reductions as possible, as in this example (tests/heap_lang.v):

  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

  Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, ⌜v = #1⌝ }}%I.
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

Issues

1. Should the pure premises for PureExec be split into those that should be solve automatically and those that should be solved manually?
2. wp_binop/wp_op does not behave as it used to be. Previously the wp_op tactic for the BinOp Eq case was specialized in such a way that it would generate two different goals. E.g. proving WP #a = #b {{ Φ }} could be reduced to proving #a = #b → Φ #true and #a ≠ #b → Φ #true. Right now, wp_op reduces the goal to Φ #(bool_decide (#a = #b)). Not sure if that's an important issue.

Thanks for this MR!

I see you have TODOs left for the wp_op changes, do you intend to do anything about them?

@jjourdan do you think it will be a problem to use this in lambdaRust?

I tried definition wp_match as a composition of two wp_pure reductions, but that does not work in some corner cases. For instance match: InjL v with InjL <> => e1 | InjR x => e2 is reduced to App (Lam <> e1) v == v ;; e1 by wp_pure; however, wp_finish is designed to already take care of that Seq and reduces to expression further to just e1.

What is the problem here?

@jjourdan do you think it will be a problem to use this in lambdaRust?

I don't think so. Someone has just to do the work :)

However, there are plenty of impure operations in lambdarust (even comparison is impure!). So I am unsure how much simplification we will get out of this.

However, there are plenty of impure operations in lambdarust (even comparison is impure!). So I am unsure how much simplification we will get out of this.

I think we should also figure out a way to reduce the redundancy of all these wp_ tactics for stateful steps, but it is not so clear what the general pattern would be there. IMHO, this should be a story for a future MR.

@jung,

I see you have TODOs left for the wp_op changes, do you intend to do anything about them?

Those are related to the wp_op issue that I've described in the OP. Ideally, I would like all the new tactics to have the exact same behaviour, so that all the old examples could be compiled without any changes.

What is the problem here?

Sorry if I wasn't clear enough. What I want to achieve is the behaviour of the original wp_match. I tried to things:

1. Define wp_match to be just wp_pure (Case _ _ _). In that case, match: InjL v with InjL <> => e1 | InjR x => e2 is reduced to e1, and match: InjR v with InjL <> => e1 | InjR x => e2 is reduced to App e2 v (I want it to be reduced to subst' x v e2.
2. Define wp_match to be wp_pure (Case _ _ _); wp_let. In this case, reducing match: InjL v with InjL <> => e1 | InjR x => e2 produces an error, as it tried to run wp_let on e1.

match: InjL v with InjL <> => e1 | InjR x => e2 is reduced to e1

Why isn't that reduced to App (Lam <> e1) v?

Why isn't that reduced to App (Lam <> e1) v?

Because this is equal to v ;; e1 and wp_finish is eager to reduce it to e1.

Oh, I forgot that wp_finish is also used. Do we still need it?

changed the description

added 1 commit

• e20d278d - Get rid of the unnecessary instances

Compare with previous version

The problem there is that we need an instance PureExec ?P (Seq e1 e2) e2. Although pure_rec matches up to conversion, conversion is going the wrong way. In order to apply pure_rec, Coq has to expand e2 to make the subst appear, which it will not do. You can prove this lemma as follows:

  by rewrite -(wp_pure' []); last eauto.

This way, it will look for PureExec ?P (Seq e1 e2) ?e with ?e an evar, which will succeed.

@jung There seems to be a Gitlab bug; when posting comments under the theories/heap_lang/lifting.v discussion above, they just disappear.

added 1 commit

• 14245102 - A bit of cleanup

Compare with previous version

I think we need to make the type of PureExec a bit more general. Currently it is:

  Class PureExec (P : Prop) (e1 e2 : expr)

Now, the tactic wp_pure solves P automatically using wp_pure_done, and if it cannot, the tactic fails. However, I think there should be two kinds of premises:

  Class PureExec (P Q : Prop) (e1 e2 : expr)

• P: Those that should be solved automatically, and if it cannot be, the tactic should fail. Here, you should think of stuff like to_val ? = ? and Closed ? ?.
• Q: Those that should be become additional goals, if they cannot be solved automatically. Here, you should think of things like bin_op_eval op v1 v2 = Some v'.

The reason that the you want some premises to become goals is that they may require non-trivial manual proof work. For example, when considering a language like C, you need to show that addition of integers does not overflow.

There seems to be a Gitlab bug; when posting comments under the theories/heap_lang/lifting.v discussion above, they just disappear.

Hm, indeed. Strange. No idea what is going on. I informed IST.

Oh, I forgot that wp_finish is also used. Do we still need it?

I got rid of it, it was a total hack anyway. See 88c69906 in the branch pure_exec. wp_match is now defined as wp_case; wp_let.

Apart from that, I changed the following:

• Write the wp_ tactics for stateful steps in the same style as wp_pure, i.e. by taking the context into account.
• Make use of the context K in wp_pure.

Remaining TODOs:

• Get a consensus on where to put the new class and rules, and how to name it.
• Figure out how to deal with premises that should be solved automatically and that may become goals.
• Generalize the class to language.
• Decide whether we mind that wp_binop/wp_op behave differently. I am fine with them behaving differently. The old behavior was kind of weird, since it produced an arrow in Coq, instead of an arrow on the RHS of the Iris turnstyle.