Get rid of the unnecessary update modalityin logrel_binary

F_mu_ref_conc/examples/counter.v

@@ -284,7 +284,7 @@ Section CG_Counter.
     iIntros "#H".
     iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     iModIntro. iApply wp_value; auto.
-    iModIntro. iExists (RecV e'). 
+    iExists (RecV e'). 
     rewrite Hclosed Hclosed'. simpl.
     iFrame "Hj". iAlways. iIntros (vv) "Hvv".
     iSpecialize ("H" $! Δ vv with "Hvv").

F_mu_ref_conc/examples/stack/refinement.v

@@ -94,7 +94,7 @@ Section Stack_refinement.
       iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
       iApply fupd_wp. iMod "Hff". iModIntro.
       iApply (wp_wand with "Hff").
-      iIntros (v). iMod 1 as (v2) "[Hj [% %]]".
+      iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
       tp_normalise j. asimpl.
       iApply fupd_wp. tp_rec j; auto using to_of_val.
       asimpl.
@@ -200,7 +200,7 @@ Section Stack_refinement.
       iApply wp_case_inl; auto. iNext.
       iApply wp_value; auto. 
       iExists (InjLV ())%V. iFrame "Hj".
-      iLeft. iExists (_,_). iModIntro. iSplit; auto.
+      iLeft. iExists (_,_). iSplit; auto.
     + close_sinv "Hclose" "[Hoe Hst' Hst Hl]".
       wp_bind (Unfold _). iApply wp_fold; first auto. iNext.
       iApply wp_rec; first auto. iNext. asimpl.
@@ -252,7 +252,7 @@ Section Stack_refinement.
         iModIntro.
         iApply wp_value; try by rewrite /= ?to_of_val /=.
         iExists (InjRV zn1). iFrame "Hj".
-        iRight. iExists (_,_). simpl. iModIntro. iSplit; auto.
+        iRight. iExists (_,_). simpl. iSplit; auto.
       * (* CAS fails *)
         iApply (wp_cas_fail with "Hst"); try by (rewrite /= ?to_of_val /=).
         congruence.        
@@ -280,7 +280,7 @@ Section Stack_refinement.
            (TArrow (TVar 0) TUnit)
            (TArrow TUnit (TSum TUnit (TVar 0))))
            (TArrow (TArrow (TVar 0) TUnit) TUnit))).
-    clear j K. iModIntro. iAlways. iIntros (τi) "%". 
+    clear j K. iAlways. iIntros (τi) "%". 
     iIntros (j K) "Hj /=".
     iApply fupd_wp.
     tp_tlam j.
@@ -326,7 +326,7 @@ Section Stack_refinement.
     iApply wp_value; first by eauto. 
     iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)).
     simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".   
-    iExists (_, _), (_, _); iModIntro; iSplit; eauto.
+    iExists (_, _), (_, _); iSplit; eauto.
     iSplit.
     (* refinement of push and pop *)
     - iExists (_, _), (_, _); iSplit; eauto. iSplit.

F_mu_ref_conc/fundamental_binary.v

@@ -290,7 +290,7 @@ Section fundamental.
     iSpecialize ("IH" with "* Hj").
     iApply fupd_wp. iApply "IH".
     iIntros (w).
-    iMod 1 as (w') "[Hw Hiw]".
+    iDestruct 1 as (w') "[Hw Hiw]".
     iExists _; rewrite -interp_subst; eauto.
   Qed.
 
@@ -367,7 +367,8 @@ Section fundamental.
     { iApply interp_env_cons. iFrame "Hτi".
       iApply interp_env_ren. auto. }
     iSpecialize ("IH2" with "* Hs [HΓ'] * Hj"); auto.
-    iApply fupd_wp. iApply "IH2". iIntros (v). iMod 1 as (v') "[Hj Hvv']".
+    iApply fupd_wp. iApply "IH2". iIntros (v).
+    iDestruct 1 as (v') "[Hj Hvv']".
     rewrite (interp_weaken [] [τi] Δ τ2). simpl.
     eauto.
   Qed.
@@ -477,7 +478,7 @@ Section fundamental.
       tp_normalise j.
       iMod ("Hclose" with "[Hv1 Hv2]").
       { iNext; iExists (_, _); by iFrame. }
-      iExists (#♭v true). iModIntro. iModIntro. eauto. 
+      iExists (#♭v true). iModIntro. eauto. 
     - iAssert (▷ ⌜v' ≠ w'⌝)%I as ">%".
       { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
       simpl. iApply (wp_cas_fail with "Hv1"); eauto.

F_mu_ref_conc/logrel_binary.v

@@ -35,7 +35,7 @@ Section logrel.
   Definition interp_expr (E1 E2 : coPset) (τi : listC D -n> D) (Δ : listC D)
       (ee : expr * expr) : iProp Σ := (∀ j K,
     j ⤇ fill K (ee.2) -∗
-    |={E1,E2}=> WP ee.1 @ E2 {{ v, |={E2}=> ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
+    |={E1,E2}=> WP ee.1 @ E2 {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
   Global Instance interp_expr_ne n E1 E2:
     Proper (dist n ==> dist n ==> (=) ==> dist n) (interp_expr E1 E2).
   Proof. solve_proper. Qed.       

F_mu_ref_conc/relational_properties.v

@@ -45,7 +45,7 @@ Section properties.
     iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     rewrite Hclosed Hclosed'.
     iModIntro. iApply wp_value; eauto.
-    iModIntro. iExists v'. rewrite (of_to_val e' v' _); auto.
+    iExists v'. rewrite (of_to_val e' v' _); auto.
     iFrame. iApply ("IH" $! Δ).
   Qed.
 
@@ -278,29 +278,62 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_atomic K Γ E1 E2 e1 e2 τ
-    (Hatomic : atomic e1)
-    (Hclosed1 : ∀ f, e1.[f] = e1) :
-    (|={E1,E2}=> {E2,E1;Γ} ⊨ fill K e1 ≤log≤ e2 : τ) -∗
-    {E1,E1;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
+  Lemma bin_log_related_atomic_l K Γ E1 E2 e1 e2 τ
+   (Hatomic : atomic e1)
+   (Hclosed1 : ∀ f, e1.[f] = e1) :
+   (|={E1,E2}=> WP e1 @ E2 {{ v,
+     ⌜∀ f, (of_val v).[f] = of_val v⌝ ∗
+     |={E2,E1}=>{E1,E1;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ }})%I -∗
+   {E1,E1;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
   Proof.
-    iIntros "Hlog".
+    iIntros "He".
     iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
     rewrite fill_subst /=.
     rewrite Hclosed1.
-    iApply wp_bind.
+    iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K)).
     iApply wp_atomic; auto.
-    iMod ("Hlog"). 
-    iSpecialize ("Hlog" with "* Hs [HΓ]"); auto.
-    iSpecialize ("Hlog" with "* Hj").
-    rewrite fill_subst /= Hclosed1.
-    iMod "Hlog". iModIntro.
-    iApply wp_mono.
-    {  iIntros (v) "Hp". iModIntro. iExact "Hp". }
-    iApply wp_bind_inv.
+    iMod "He".
+    iApply (wp_wand with "He").
+    iIntros (v) "[% Hv]".
+    iMod "Hv".
+    iSpecialize ("Hv" with "* Hs [HΓ] * Hj"); auto.
+    iMod "Hv". simpl.
+    rewrite fill_subst /=. rewrite H1.
     done.
-  Qed.    
+  Qed.
+
+  Lemma bin_log_related_alloc_l_alt Γ E1 E2 K e v t τ
+    (Heval : to_val e = Some v)
+    (Hclosed : ∀ f, e.[f] = e) :
+    (|={E1,E2}=> ∀ (l : loc), l ↦ᵢ v -∗
+           |={E2,E1}=>{E1,E1;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ)%I
+    -∗ {E1,E1;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hsafe".
+    iApply bin_log_related_atomic_l; auto.
+    { intro f. asimpl. by rewrite Hclosed. }
+    iMod "Hsafe". iModIntro.
+    iApply wp_alloc.  apply Heval.
+    iNext. iIntros (l) "Hl".
+    iSpecialize ("Hsafe" with "* Hl").
+    iSplitR; eauto.
+  Qed.
 
+  Lemma bin_log_related_load_l_alt E1 E2 Γ K l t τ :
+    (|={E1,E2}=> ∃ v', ⌜∀ f, (of_val v').[f] = of_val v'⌝ ∗
+    ▷(l ↦ᵢ v') ∗
+    (l ↦ᵢ v' -∗ (|={ E2,E1}=> {E1,E1;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ)))%I
+    -∗ {E1,E1;Γ} ⊨ fill K (Load (Loc l)) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hsafe".
+    iApply bin_log_related_atomic_l; auto.
+    iMod "Hsafe" as (v') "[% [Hl Hsafe]]". iModIntro.    
+    iApply (wp_load with "Hl").  
+    iNext. iIntros "Hl".
+    iSpecialize ("Hsafe" with "* Hl").
+    iSplitR; eauto.
+  Qed.
+  
   Lemma bin_log_related_step_atomic_l {A} (Φ : A → val → iProp Σ) K Γ E1 E2 e1 e2 τ
     (Hatomic : atomic e1)
     (Hclosed1 : ∀ f, e1.[f] = e1) :

F_mu_ref_conc/soundness_binary.v

@@ -38,7 +38,7 @@ Proof.
   { rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
   iApply fupd_wp. iApply "Hrel"; auto.
   iIntros (v1).
-  iMod 1 as (v2) "[Hj #Hinterp]". 
+  iDestruct 1 as (v2) "[Hj #Hinterp]". 
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
   rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
   iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.