GitLab

The wp_store and wp_load tactics appear to be very sensitive to the order of points to assumptions in the context. Consider the following snippet, placed after heap_e_spec in tests/heap_lang.v

  Definition heap_e2  : expr [] :=
    let: "x" := ref #1 in
    let: "y" := ref #1 in
    '"x" <- !'"x" + #1 ;; !'"x".
  Lemma heap_e2_spec E N :
     nclose N ⊆ E → heap_ctx N ⊢ WP heap_e2 @ E {{ v, v = #2 }}.
  Proof.
    iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
    wp_alloc l. wp_let.
    wp_alloc l'. wp_let.
    time wp_load.
  Abort.

The wp_load takes 109 seconds to complete on my machine. The problem appears to be in the call to iAssumptionCore in wp_load, which tries to find an assumption l |-> ?v in the context. Because of the order of assumptions, it will first try to unify with l' |-> 1. For some reason, this does not fail instantaneously. You can check that this is the source of delay with the following example:

Remark bad_unify (l l': loc): True.
Proof.
(evar (v: Z );
  let v0 := eval unfold v in v in
unify (l ↦ #v0)%I (l' ↦ #1)%I).
Abort.

The obvious work-around is to just re-order the two points to facts in the context, or use "remember" to "hide" one of them temporarily, but this is obviously brittle. I am not an expert on how unification works under the hood, so it is hard for me to diagnose why it's so slow here.

First, does this occur for others? I am using coq 8.5pl1 and ssreflect ad273277ab38b. If so, is there some more robust work-around?