Make EqType more realistic

theories/logrel/F_mu_ref_conc/context_refinement.v

@@ -187,7 +187,9 @@ Proof.
 Qed.
 
 Definition ctx_refines (Γ : list type)
-    (e e' : expr) (τ : type) := ∀ K thp σ v,
+    (e e' : expr) (τ : type) :=
+  typed Γ e τ ∧ typed Γ e' τ ∧
+  ∀ K thp σ v,
   typed_ctx K Γ τ [] TUnit →
   rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) →
   ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ').

theories/logrel/F_mu_ref_conc/examples/counter.v

@@ -366,6 +366,6 @@ Theorem counter_ctx_refinement :
 Proof.
   set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]).
   set (HG := soundness_unary.HeapPreIG Σ _ _).
-  eapply (binary_soundness Σ _); auto.
+  eapply (binary_soundness Σ _); auto using FG_counter_type, CG_counter_type.
   intros. apply FG_CG_counter_refinement.
 Qed.

theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v

@@ -3,11 +3,14 @@ From iris_examples.logrel.F_mu_ref_conc Require Import  typing.
 Definition FG_StackType τ :=
   TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
 
+Definition FG_Stack_Ref_Type τ :=
+  Tref (TSum TUnit (TProd τ (FG_StackType τ))).
+
 Definition FG_push (st : expr) : expr :=
   Rec (App (Rec
               (* try push *)
               (If (CAS (st.[ren (+4)]) (Var 1)
-                       (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+                       (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
                   )
                   Unit (* push succeeds we return unit *)
                   (App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -19,7 +22,7 @@ Definition FG_pushV (st : expr) : val :=
   RecV (App (Rec
               (* try push *)
               (If (CAS (st.[ren (+4)]) (Var 1)
-                       (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+                       (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
                   )
                   Unit (* push succeeds we return unit *)
                   (App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -39,8 +42,8 @@ Definition FG_pop (st : expr) : expr :=
                              If
                                (CAS
                                   (st.[ren (+7)])
-                                  (Fold (Var 4))
-                                  (Snd (Var 0))
+                                  (Var 4)
+                                  (Unfold (Snd (Var 0)))
                                )
                                (InjR (Fst (Var 0))) (* pop succeeds *)
                                (App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -52,7 +55,7 @@ Definition FG_pop (st : expr) : expr :=
                  )
               )
            )
-           (Unfold (Load st.[ren (+ 2)]))
+           (Load st.[ren (+ 2)])
       ).
 Definition FG_popV (st : expr) : val :=
   RecV
@@ -67,8 +70,8 @@ Definition FG_popV (st : expr) : val :=
                           If
                             (CAS
                                (st.[ren (+7)])
-                               (Fold (Var 4))
-                               (Snd (Var 0))
+                               (Var 4)
+                               (Unfold (Snd (Var 0)))
                             )
                             (InjR (Fst (Var 0))) (* pop succeeds *)
                             (App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -80,7 +83,7 @@ Definition FG_popV (st : expr) : val :=
               )
           )
        )
-       (Unfold (Load st.[ren (+ 2)]))
+       (Load st.[ren (+ 2)])
     ).
 
 Definition FG_iter (f : expr) : expr :=
@@ -100,14 +103,14 @@ Definition FG_iterV (f : expr) : val :=
           )
     ).
 Definition FG_read_iter (st : expr) : expr :=
-  Rec (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
+  Rec (App (FG_iter (Var 1)) (Fold (Load st.[ren (+2)]))).
 
 Definition FG_stack_body (st : expr) : expr :=
   Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
 
 Definition FG_stack : expr :=
   TLam (App (Rec (FG_stack_body (Var 1)))
-                (Alloc (Fold (Alloc (InjL Unit))))).
+                (Alloc (Alloc (InjL Unit)))).
 
 Section FG_stack.
   (* Fine-grained push *)
@@ -116,7 +119,7 @@ Section FG_stack.
     Rec (App (Rec
                 (* try push *)
                 (If (CAS (st.[ren (+4)]) (Var 1)
-                         (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+                         (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
                     )
                     Unit (* push succeeds we return unit *)
                     (App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -127,20 +130,19 @@ Section FG_stack.
   Proof. trivial. Qed.
 
   Section FG_push_type.
-    (* The following assumption is simply ** WRONG ** *)
-    (* We assume it though to just be able to prove that the
-       stack we are implementing is /type-sane/ so to speak! *)
-    Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
-
     Lemma FG_push_type st Γ τ :
-      typed Γ st (Tref (FG_StackType τ)) →
+      typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
       typed Γ (FG_push st) (TArrow τ TUnit).
     Proof.
-      intros H1. repeat (econstructor; eauto using HEQTP).
+      intros HTst.
+      repeat match goal with
+               |- typed _ _ _ => econstructor; eauto
+             end; repeat econstructor; eauto.
       - eapply (context_weakening [_; _; _; _]); eauto.
       - by asimpl.
-      - eapply (context_weakening [_; _]); eauto.
+      -  eapply (context_weakening [_; _]); eauto.
     Qed.
+
   End FG_push_type.
 
   Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st).
@@ -173,8 +175,8 @@ Section FG_stack.
                                 If
                                   (CAS
                                      (st.[ren (+7)])
-                                     (Fold (Var 4))
-                                     (Snd (Var 0))
+                                     (Var 4)
+                                     (Unfold (Snd (Var 0)))
                                   )
                                   (InjR (Fst (Var 0))) (* pop succeeds *)
                                   (App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -186,24 +188,28 @@ Section FG_stack.
                     )
                 )
              )
-             (Unfold (Load st.[ren (+ 2)]))
+             (Load st.[ren (+ 2)])
         ).
   Proof. trivial. Qed.
 
   Section FG_pop_type.
-    (* The following assumption is simply ** WRONG ** *)
-    (* We assume it though to just be able to prove that the
-       stack we are implementing is /type-sane/ so to speak! *)
-    Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
 
     Lemma FG_pop_type st Γ τ :
-      typed Γ st (Tref (FG_StackType τ)) →
+      typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
       typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)).
     Proof.
-      intros H1. repeat (econstructor; eauto using HEQTP).
-      - eapply (context_weakening [_; _; _; _; _; _; _]); eauto.
-      - asimpl; trivial.
+      replace (FG_Stack_Ref_Type τ) with
+          (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).[FG_StackType τ/];
+        last first.
+      { by asimpl. }
+      intros HTst.
+      repeat match goal with
+               |- typed _ _ _ => econstructor; eauto
+             end; repeat econstructor; eauto; last first.
       - eapply (context_weakening [_; _]); eauto.
+      - by asimpl.
+      - eapply (context_weakening [_; _; _; _; _; _; _]); eauto.
+      - econstructor.
     Qed.
   End FG_pop_type.
 
@@ -270,13 +276,13 @@ Section FG_stack.
   Global Opaque FG_iter.
 
   Lemma FG_read_iter_type st Γ τ :
-    typed Γ st (Tref (FG_StackType τ)) →
+    typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
     typed Γ (FG_read_iter st)
           (TArrow (TArrow τ TUnit) TUnit).
   Proof.
     intros H1; repeat econstructor.
     - eapply FG_iter_type; by constructor.
-    - by eapply (context_weakening [_;_]).
+    - by eapply (context_weakening [_;_]); asimpl.
   Qed.
 
   Transparent FG_iter.
@@ -296,13 +302,9 @@ Section FG_stack.
   Global Opaque FG_iter.
 
   Section FG_stack_body_type.
-    (* The following assumption is simply ** WRONG ** *)
-    (* We assume it though to just be able to prove that the
-       stack we are implementing is /type-sane/ so to speak! *)
-    Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
 
     Lemma FG_stack_body_type st Γ τ :
-      typed Γ st (Tref (FG_StackType τ)) →
+      typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
       typed Γ (FG_stack_body st)
             (TProd
                (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ)))
@@ -328,10 +330,6 @@ Section FG_stack.
   Qed.
 
   Section FG_stack_type.
-    (* The following assumption is simply ** WRONG ** *)
-    (* We assume it though to just be able to prove that the
-       stack we are implementing is /type-sane/ so to speak! *)
-    Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
 
     Lemma FG_stack_type Γ :
       typed Γ FG_stack
@@ -348,7 +346,6 @@ Section FG_stack.
       - eapply FG_push_type; try constructor; simpl; eauto.
       - eapply FG_pop_type; try constructor; simpl; eauto.
       - eapply FG_read_iter_type; constructor; by simpl.
-      - asimpl. repeat constructor.
     Qed.
   End FG_stack_type.
 

theories/logrel/F_mu_ref_conc/examples/stack/refinement.v

@@ -41,7 +41,7 @@ Section Stack_refinement.
     simpl.
     rewrite CG_locked_push_subst CG_locked_pop_subst
             CG_iter_subst CG_snap_subst. simpl. asimpl.
-    iApply (wp_bind (fill [FoldCtx; AllocCtx; AppRCtx (RecV _)]));
+    iApply (wp_bind (fill [AllocCtx; AppRCtx (RecV _)]));
       iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
     iApply wp_alloc; first done. iNext; iIntros (istk) "Histk".
     iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -64,7 +64,7 @@ Section Stack_refinement.
       iFrame "Hls". iLeft. iSplit; trivial. }
     iAssert ((∃ istk v h, (stack_owns h)
                          ∗ stk' ↦ₛ v
-                         ∗ stk ↦ᵢ (FoldV (LocV istk))
+                         ∗ stk ↦ᵢ (LocV istk)
                          ∗ StackLink τi (LocV istk, v)
                          ∗ l ↦ₛ (#♭v false)
              )%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
@@ -98,8 +98,8 @@ Section Stack_refinement.
         clear v h.
         iApply wp_pure_step_later; auto using to_of_val.
         iModIntro. iNext. asimpl.
-        iApply (wp_bind (fill [FoldCtx;
-                               CasRCtx (LocV _) (FoldV (LocV _)); IfCtx _ _]));
+
+        iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
           iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
         iApply wp_alloc; simpl; trivial.
         iNext. iIntros (ltmp) "Hltmp".
@@ -140,7 +140,7 @@ Section Stack_refinement.
         iApply wp_pure_step_later; auto. iNext.
         rewrite -(FG_pop_folding (Loc stk)).
         asimpl.
-        iApply (wp_bind (fill [UnfoldCtx; AppRCtx (RecV _)]));
+        iApply (wp_bind (fill [AppRCtx (RecV _)]));
           iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
         iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
         iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
@@ -153,10 +153,7 @@ Section Stack_refinement.
              as "[Hj [Hstk' Hl]]"; first solve_ndisj.
           iMod ("Hclose" with "[-Hj Hmpt]") as "_".
           { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
-          iApply (wp_bind (fill [AppRCtx (RecV _)]));
-            iApply wp_wand_l; iSplitR; [iModIntro; iIntros (w) "Hw"; iExact "Hw"|].
-          iApply wp_pure_step_later; simpl; auto using to_of_val.
-          iModIntro. iNext. iApply wp_value.
+          iModIntro.
           iApply wp_pure_step_later; auto. iNext. asimpl.
           clear h.
           iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -176,10 +173,7 @@ Section Stack_refinement.
         * (* The stack is not empty *)
           iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
           { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
-          iApply (wp_bind (fill [AppRCtx (RecV _)]));
-            iApply wp_wand_l; iSplitR; [iModIntro; iIntros (w') "Hw"; iExact "Hw"|].
-          iApply wp_pure_step_later; simpl; auto.
-          iModIntro. iNext. iApply wp_value. iApply wp_pure_step_later; auto.
+          iModIntro. iApply wp_pure_step_later; auto.
           iNext. asimpl.
           clear h.
           iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -195,8 +189,12 @@ Section Stack_refinement.
           iModIntro. iNext. asimpl.
           iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl.
           iApply wp_pure_step_later; [simpl; by rewrite ?to_of_val |].
-          iNext.
-          iApply (wp_bind (fill [CasRCtx (LocV _) (FoldV (LocV _)); IfCtx _ _]));
+          iNext. asimpl.
+          iApply (wp_bind (fill [UnfoldCtx; CasRCtx (LocV _) (LocV _); IfCtx _ _]));
+            iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
+          asimpl. iApply wp_pure_step_later; auto.
+          simpl. iNext. iApply wp_value.
+          iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
             iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
           asimpl. iApply wp_pure_step_later; auto.
           simpl. iNext. iApply wp_value.
@@ -249,7 +247,7 @@ Section Stack_refinement.
         by (by rewrite FG_iter_of_val).
       replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
         by (by rewrite CG_iter_of_val).
-      iApply (wp_bind (fill [AppRCtx _])); iApply wp_wand_l;
+      iApply (wp_bind (fill [FoldCtx; AppRCtx _])); iApply wp_wand_l;
         iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
       iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose".
       iMod (steps_CG_snap _ _ _ (AppRCtx _ :: K)
@@ -337,6 +335,6 @@ Theorem stack_ctx_refinement :
 Proof.
   set (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR); GFunctor (authR stackUR)]).
   set (HG := soundness_unary.HeapPreIG Σ _ _).
-  eapply (binary_soundness Σ); eauto using FG_stack_closed, CG_stack_closed.
+  eapply (binary_soundness Σ); eauto using FG_stack_type, CG_stack_type.
   intros; apply FG_CG_counter_refinement.
 Qed.

theories/logrel/F_mu_ref_conc/fundamental_binary.v

@@ -356,8 +356,8 @@ Section fundamental.
     iApply wp_atomic; eauto.
     iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
     iModIntro.
-    iApply (wp_store with "Hv1"); auto using to_of_val. 
-    iNext. iIntros "Hw2". 
+    iApply (wp_store with "Hv1"); auto using to_of_val.
+    iNext. iIntros "Hw2".
     iMod (step_store with "[$Hs Hw Hv2]") as "[Hw Hv2]"; eauto;
     [solve_ndisj | by iFrame|].
     iMod ("Hclose" with "[Hw2 Hv2]").
@@ -381,30 +381,31 @@ Section fundamental.
       ('`IHHtyped3 _ _ _  j ((CasRCtx _ _) :: K)).
     iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
     iApply wp_atomic; eauto.
-    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
+    iMod (interp_ref_open' _ _ l l' with "[]") as
+        (v v') "(>Hl & >Hl' & #Hiv & Heq & Hcl)"; eauto.
+    { iExists (_, _); eauto. }
     iModIntro.
-    iPoseProof ("Hv") as "Hv'".
-    rewrite {2}[⟦ τ ⟧ Δ (v, v')]interp_EqType_agree; trivial.
-    iMod "Hv'" as %Hv'; subst.
-    destruct (decide (v' = w)) as [|Hneq]; subst.
-    - iAssert (▷ ⌜w' = w⌝)%I as ">%".
-      { rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
-      simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
-      iNext. iIntros "Hv1".
+    destruct (decide (v = w)) as [|Hneq]; subst.
+    - iApply (wp_cas_suc with "Hl"); eauto using to_of_val; eauto.
+      iNext. iIntros "Hl".
+      iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
+      iDestruct "Heq" as %[-> _]; last trivial.
       iMod (step_cas_suc
-            with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
-      iFrame. iFrame "Hs".
-      iMod ("Hclose" with "[Hv1 Hv2]").
+            with "[Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
+      { iFrame. iFrame "Hs". }
+      iMod ("Hcl" with "[Hl Hl']").
       { iNext; iExists (_, _); by iFrame. }
       iExists (#♭v true); iFrame; eauto.
-    - iAssert (▷ ⌜v' ≠ w'⌝)%I as ">%".
-      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
-      simpl. iApply (wp_cas_fail with "Hv1"); eauto.
-      iNext. iIntros "Hv1". 
+    - iApply (wp_cas_fail with "Hl"); eauto using to_of_val; eauto.
+      iNext. iIntros "Hl".
+      iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
+      iDestruct "Heq" as %[_ Heq].
+      assert (v' ≠ w').
+      { by intros ?; apply Hneq; rewrite Heq. }
       iMod (step_cas_fail
-            with "[$Hs Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
+            with "[$Hs Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
       iFrame.
-      iMod ("Hclose" with "[Hv1 Hv2]").
+      iMod ("Hcl" with "[Hl Hl']").
       { iNext; iExists (_, _); by iFrame. }
       iExists (#♭v false); eauto.
   Qed.

theories/logrel/F_mu_ref_conc/logrel_binary.v

@@ -231,25 +231,149 @@ Section logrel.
     apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
   Qed.
 
-  Lemma interp_EqType_agree τ v v' Δ :
-    env_Persistent Δ → EqType τ → interp τ Δ (v, v') ⊢ ⌜v = v'⌝.
+  Lemma interp_ref_pointsto_neq E Δ τ l w (l1 l2 l3 l4 : loc) :
+    ↑logN.@(l1, l2) ⊆ E →
+    l2 ≠ l4 →
+    l ↦ᵢ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
+      |={E ∖ ↑logN.@(l3, l4)}=> l ↦ᵢ w ∗ ⌜l ≠ l1⌝.
   Proof.
-    intros ? Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
-    - by iDestruct "H1" as "[% %]"; subst.
-    - by iDestruct "H1" as (n) "[% %]"; subst.
-    - by iDestruct "H1" as (b) "[% %]"; subst.
-    - iDestruct "H1" as ([??] [??]) "[% [H1 H2]]"; simplify_eq/=.
-      rewrite IHHτ1 IHHτ2.
-      by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
-    - iDestruct "H1" as "[H1|H1]".
-      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
-        rewrite IHHτ1. by iDestruct "H1" as "%"; subst.
-      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
-        rewrite IHHτ2. by iDestruct "H1" as "%"; subst.
+    intros Hnin Hneq.
+    destruct (decide (l = l1)); subst; last auto.
+    iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
+    iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
+    iDestruct "Hi" as ((v1, v2))  "(Hl3 & Hl2' & ?)".
+    iMod "Hl3".
+    by iDestruct (@mapsto_valid_2 with "Hl1 Hl3") as %?.
   Qed.
+
+  Lemma interp_ref_pointsto_neq' E Δ τ l w (l1 l2 l3 l4 : loc) :
+    ↑logN.@(l1, l2) ⊆ E →
+    l1 ≠ l3 →
+    l ↦ₛ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
+      |={E ∖ ↑logN.@(l3, l4)}=> l ↦ₛ w ∗ ⌜l ≠ l2⌝.
+  Proof.
+    intros Hnin Hneq.
+    destruct (decide (l = l2)); subst; last auto.
+    iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
+    iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
+    iDestruct "Hi" as ((v1, v2))  "(Hl3 & Hl2' & ?)".
+    iMod "Hl2'"; simpl.
+    unfold heapS_mapsto.
+    iDestruct (@own_valid_2 _ _ _ cfg_name with "Hl1 Hl2'") as %[_ Hvl].
+    exfalso.
+    specialize (Hvl l6); revert Hvl. simpl.
+    rewrite /= gmap.lookup_op !lookup_singleton -Some_op. by intros [? _].
+  Qed.
+
+  Lemma interp_ref_open' Δ τ l l' :
+    env_Persistent Δ → EqType τ →
+    ⟦ Tref τ ⟧ Δ (LocV l, LocV l') -∗
+               |={⊤, ⊤ ∖ ↑logN.@(l, l')}=>
+  ∃ w w', ▷ l ↦ᵢ w ∗ ▷ l' ↦ₛ w' ∗ ▷ ⟦ τ ⟧ Δ (w, w') ∗
+            ▷ (∀ z z' u u' v v',
+                  l ↦ᵢ z -∗ l' ↦ₛ z' -∗ ⟦ τ ⟧ Δ (u, u') -∗ ⟦ τ ⟧ Δ (v, v') -∗
+                    |={⊤ ∖ ↑logN.@(l, l')}=> l ↦ᵢ z ∗
+                                              l' ↦ₛ z' ∗ ⌜v = u ↔ v' = u'⌝)
+            ∗ (▷ (∃ vv : val * val, l ↦ᵢ vv.1 ∗ l' ↦ₛ vv.2 ∗ ⟦ τ ⟧ Δ vv)
+          ={⊤ ∖ ↑logN.@(l, l'), ⊤}=∗ True).
+  Proof.
+    iIntros (HΔ Heqt); simpl.
+    iDestruct 1 as ((l1, l1')) "[% H1]"; simplify_eq.
+    iInv (logN.@(l1, l1')) as "Hi" "$"; simpl. iClear "H1".
+    iDestruct "Hi" as ((v1, v2))  "(Hl1 & Hl1' & Hrl)"; simpl in *.
+    destruct Heqt; simpl in *.
+    - iModIntro; iExists _, _; iFrame.
+      iNext. iIntros (??????) "? ?". iIntros ([??] [??]); subst.
+      by iModIntro; iFrame.
+    - iModIntro; iExists _, _; iFrame.
+      iNext. iIntros (??????) "? ?".
+      iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
+      simplify_eq. by iModIntro; iFrame.
+    - iModIntro; iExists _, _; iFrame.
+      iNext. iIntros (??????) "? ?".
+      iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
+      simplify_eq. by iModIntro; iFrame.
+    - iModIntro; iExists _, _; iFrame; iFrame "#". iNext.
+      iIntros (z z' u u' v v') "Hl1 Hl1' Huu". iDestruct 1 as ((l2, l2')) "[% #Hl2]";
+        simplify_eq; simpl in *.
+      iDestruct "Huu" as ((l3, l3')) "[% #Hl3]";
+        simplify_eq; simpl in *.
+      destruct (decide ((l1, l1') = (l2, l2'))); simplify_eq.
+      + destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq; first by iFrame.
+        destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
+        * iMod (interp_ref_pointsto_neq with "Hl1 []")
+               as "[Hl1 %]"; simpl; eauto.
+             { by iExists (_, _); iFrame "#". }
+             by iFrame.
+        * iMod (interp_ref_pointsto_neq with "Hl1 []")
+               as "[Hl1 %]"; simpl; eauto.
+             { by iExists (_, _); iFrame "#". }
+             by iFrame.
+        * iMod (interp_ref_pointsto_neq' with "Hl1' []")
+               as "[Hl1' %]";
+               simpl; eauto.
+             { by iExists (_, _); iFrame "#". }
+             by iFrame.
+        * iFrame; iModIntro; iPureIntro; split; by inversion 1.
+      + destruct (decide ((l1, l1') = (l3, l3'))); simplify_eq.
+        * destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
+          -- iMod (interp_ref_pointsto_neq with "Hl1 []")
+              as "[Hl1 %]"; simpl; eauto.
+             { by iExists (_, _); iFrame "#". }
+             by iFrame.
+          -- iMod (interp_ref_pointsto_neq with "Hl1 []")
+               as "[Hl1 %]"; simpl; eauto.
+             { iExists (_, _); iSplit; first eauto. iFrame "#". }
+             by iFrame.
+          -- iMod (interp_ref_pointsto_neq' with "Hl1' []")
+               as "[Hl1' %]";
+               simpl; eauto.
+             { iExists (_, _); iSplit; first eauto. iFrame "#". }
+             by iFrame.
+          -- iFrame; iModIntro; iPureIntro; split; by inversion 1.
+        * destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq.
+          -- destruct (decide (l1 = l3)); destruct (decide (l1' = l3')); subst.
+             ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
+                 as "[Hl1 %]"; simpl; eauto.
+                { by iExists (_, _); iFrame "#". }
+                  by iFrame.
+             ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
+               as "[Hl1 %]"; simpl; eauto.
+                { by iExists (_, _); iFrame "#". }
+                  by iFrame.
+             ++ iMod (interp_ref_pointsto_neq' with "Hl1' []")
+                 as "[Hl1' %]";
+                  simpl; eauto.
+                { by iExists (_, _); iFrame "#". }
+                  by iFrame.
+             ++ iFrame; iModIntro; iPureIntro; split; by inversion 1.
+          -- iFrame.
+             { destruct (decide (l2 = l3)); destruct (decide (l2' = l3'));
+                 simplify_eq; auto.
+               + iInv (logN.@(l3, l2')) as "Hib1" "Hcl1".
+                 iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
+                 iDestruct "Hib1" as ((v11, v12)) "(Hlx1' & Hlx2 & Hr1)".
+                 iDestruct "Hib2" as ((v11', v12')) "(Hl1'' & Hl2' & Hr2)".
+                 simpl.
+                 iMod "Hlx1'"; iMod "Hl1''".
+                   by iDestruct (@mapsto_valid_2 with "Hlx1' Hl1''") as %?.