make the ElimAcc instance for WP add a view shift

theories/heap_lang/lib/counter.v

@@ -48,7 +48,7 @@ Section mono_proof.
     iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
     iDestruct "Hl" as (γ) "[#? Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
-    wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     wp_let. wp_op.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
@@ -56,12 +56,12 @@ Section mono_proof.
         as %[?%mnat_included _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cas_suc. iSplitL "Hl Hγ".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf"). apply: auth_frag_mono.
       by apply mnat_included, le_n_S.
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
@@ -72,7 +72,7 @@ Section mono_proof.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
-    iApply wp_fupd. wp_load.
+    wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[?%mnat_included _]%auth_valid_discrete_2.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
@@ -125,17 +125,17 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
-    wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     wp_let. wp_op.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
-      wp_cas_suc. iSplitL "Hl Hγ".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_if. by iApply "HΦ".
     - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
@@ -146,7 +146,7 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
-    iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
 
@@ -157,7 +157,7 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
-    iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.
 End contrib_spec.

theories/heap_lang/lib/spawn.v

@@ -56,7 +56,7 @@ Proof.
   - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]".
-    wp_store. iSplit; last done. iNext. iExists (SOMEV v). iFrame. eauto.
+    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :
@@ -65,10 +65,10 @@ Proof.
   iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
+  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
     wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
-    + iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
+    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
       wp_match. by iApply "HΦ".
     + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.

theories/heap_lang/lib/spin_lock.v

@@ -62,10 +62,10 @@ Section proof.
   Proof.
     iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
     wp_rec. iInv N as ([]) "[Hl HR]".
-    - wp_cas_fail. iSplitL "Hl"; first (iNext; iExists true; eauto).
+    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
       iApply ("HΦ" $! false). done.
     - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
-      iSplitL "Hl"; first (iNext; iExists true; eauto).
+      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
       rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
 
@@ -85,7 +85,7 @@ Section proof.
     iDestruct "Hlock" as (l ->) "#Hinv".
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
     wp_store. iSplitR "HΦ"; last by iApply "HΦ".
-    iNext. iExists false. by iFrame.
+    iModIntro. iNext. iExists false. by iFrame.
   Qed.
 End proof.
 

theories/heap_lang/lib/ticket_lock.v

@@ -91,13 +91,13 @@ Section proof.
     iInv N as (o n) "(Hlo & Hln & Ha)".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iSplitL "Hlo Hln Hainv Ht".
+      + iModIntro. iSplitL "Hlo Hln Hainv Ht".
         { iNext. iExists o, n. iFrame. }
         wp_let. wp_op. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
-    - iSplitL "Hlo Hln Ha".
+    - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
       wp_let. wp_op. case_bool_decide; [simplify_eq |].
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
@@ -109,7 +109,7 @@ Section proof.
     iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]".
-    wp_load. iSplitL "Hlo Hln Ha".
+    wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
     wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
@@ -119,14 +119,14 @@ Section proof.
         eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
         apply (seq_set_S_disjoint 0). }
       rewrite -(seq_set_S_union_L 0).
-      wp_cas_suc. iSplitL "Hlo' Hln' Haown Hauth".
+      wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
       + by iNext.
-    - wp_cas_fail.
+    - wp_cas_fail. iModIntro.
       iSplitL "Hlo' Hln' Hauth Haown".
       { iNext. iExists o', n'. by iFrame. }
       wp_if. by iApply "IH"; auto.
@@ -142,7 +142,7 @@ Section proof.
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
-    iSplitL "Hlo Hln Hauth Haown".
+    iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
     wp_op.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
@@ -155,7 +155,7 @@ Section proof.
     { apply auth_update, prod_local_update_1.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
     iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
-    iNext. iExists (S o), n'.
+    iIntros "!> !>". iExists (S o), n'.
     rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
 End proof.

theories/program_logic/weakestpre.v

@@ -408,23 +408,23 @@ Section proofmode_classes.
   Global Instance acc_elim_wp {X} E1 E2 α β γ e s Φ :
     Atomic (stuckness_to_atomicity s) e →
     AccElim (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
-            (λ x, WP e @ s; E2 {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     intros ?. rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
-    iIntros (v) "[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 
   Global Instance acc_elim_wp_nonatomic {X} E α β γ e s Φ :
     AccElim (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
-            (λ x, WP e @ s; E {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
-    iIntros (v) "[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 
 End proofmode_classes.

theories/tests/one_shot.v

@@ -53,7 +53,7 @@ Proof.
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
       wp_cas_suc. iSplitL; last eauto.
-      iNext; iRight; iExists n; by iFrame.
+      iModIntro. iNext; iRight; iExists n; by iFrame.
     + wp_cas_fail. iSplitL; last eauto.
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_seq. wp_bind (! _)%E.
@@ -70,7 +70,7 @@ Proof.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    wp_let. iIntros "!#". wp_seq.
+    iModIntro. wp_let. iIntros "!#". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.
@@ -78,7 +78,7 @@ Proof.
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
-    iSplitL "Hl".
+    iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
     wp_match. iApply wp_assert.
     wp_op. by case_bool_decide.