Strength the CAS rule

F_mu_ref_conc/examples/counter.v

@@ -180,20 +180,20 @@ Section CG_Counter.
     destruct (decide (n = n')); subst.
     - iExists (#nv n'). iFrame.
       iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
-      iIntros "_ Hx". simpl.
+      iIntros "_ !> Hx". simpl.
       rewrite ->uPred.and_elim_r.
       iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
       iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.   
     - iExists (#nv n'). iFrame. 
       iSplitL; eauto; last first.
       { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
-      iIntros "_ Hx". simpl.
+      iIntros "_ !> Hx". simpl.
       iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.   
       rewrite ->uPred.and_elim_l.
       iMod ("HQ" with "[Hx HR]").
-      { iExists _; iFrame. }      
+      { iExists _; iFrame. }
       iApply "IH".
-  Qed.    
+  Qed.
 
   (* A similar atomic specification for the counter_read fn *)
   Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :

F_mu_ref_conc/rel_tactics.v

@@ -360,8 +360,8 @@ Lemma tac_rel_cas_l `{heapIG Σ, !cfgSG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l
   nam_cl ≠ nam →
   Δ2 = envs_snoc (envs_snoc Δ1 false nam (▷ P)%I) false nam_cl (▷ P ={E1 ∖ ↑N,E1}=∗ True)%I →
   (Δ2 ⊢ |={E2}=> ∃ v, ▷ (l ↦ᵢ v) ∗
-     ((⌜v ≠ v1⌝ ∗ (l ↦ᵢ v  -∗ {E2,E1;Γ} ⊨ fill K' (#♭ false) ≤log≤ t : τ)) ∨
-      (⌜v = v1⌝ ∗ (l ↦ᵢ v2 -∗ {E2,E1;Γ} ⊨ fill K' (#♭ true) ≤log≤ t : τ)))) →
+     ((⌜v ≠ v1⌝ ∗ ▷ (l ↦ᵢ v  -∗ {E2,E1;Γ} ⊨ fill K' (#♭ false) ≤log≤ t : τ)) ∨
+      (⌜v = v1⌝ ∗ ▷ (l ↦ᵢ v2 -∗ {E2,E1;Γ} ⊨ fill K' (#♭ true) ≤log≤ t : τ)))) →
   (Δ1 ⊢ bin_log_related E1 E1 Γ e t τ).
 Proof.
   intros ???????????.

F_mu_ref_conc/relational_properties.v

@@ -479,8 +479,8 @@ Section properties.
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (|={E1,E2}=> ∃ v', ▷ (l ↦ᵢ v') ∗ 
-     (⌜v' ≠ v1⌝ -∗ l ↦ᵢ v' -∗ {E2,E1;Γ} ⊨ fill K (#♭ false) ≤log≤ t : τ) ∗
-     (⌜v' = v1⌝ -∗ l ↦ᵢ v2 -∗ {E2,E1;Γ} ⊨ fill K (#♭ true) ≤log≤ t : τ))
+     (⌜v' ≠ v1⌝ -∗ ▷ (l ↦ᵢ v' -∗ {E2,E1;Γ} ⊨ fill K (#♭ false) ≤log≤ t : τ)) ∗
+     (⌜v' = v1⌝ -∗ ▷ (l ↦ᵢ v2 -∗ {E2,E1;Γ} ⊨ fill K (#♭ true) ≤log≤ t : τ)))
     -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
   Proof.
     iIntros (??) "Hlog".
@@ -488,11 +488,11 @@ Section properties.
     iMod "Hlog" as (v') "[Hl [Hlog_fail Hlog_suc]]". iModIntro. 
     destruct (decide (v' = v1)).
     - (* CAS successful *) subst.      
-      iApply (wp_cas_suc with "Hl"); eauto. 
-      iNext. by iApply "Hlog_suc".
+      iApply (wp_cas_suc with "Hl"); eauto.
+      iSpecialize ("Hlog_suc" with "[]"); eauto.
     - (* CAS failed *)
       iApply (wp_cas_fail with "Hl"); eauto. 
-      iNext. by iApply "Hlog_fail".
+      iSpecialize ("Hlog_fail" with "[]"); eauto.
   Qed.
 
   Lemma bin_log_related_cas_fail_l Γ E1 E2 K l e1 e2 v1 v2 t τ :