Retrofit GPS with AtomicPtsTo

theories/base_logic/base_lifting.v

@@ -599,12 +599,12 @@ Lemma iwp_cas l vr vw orf or ow C q
                         ={E,E'}=∗ ▷|={E', (El l')}=> ∃ q C', hist l' q C'))
            | _, _ => emp
           end) ∗
-    (⌜if b then v' = vr else true⌝ -∗
-      P ={E}[E']▷=∗
+    ( ⌜if b then v' = vr else true⌝ -∗
+      P -∗
       seen 𝓥' -∗
       hist l 1 C' -∗ atread l q (rsa ∪ {[tr]}) -∗ naread l 1 rsn -∗
       (if b then atwrite l 1 (ws ∪ {[t]}) else atwrite l 1 ws) -∗
-      ⌜good_hist C'⌝ -∗
+      ⌜good_hist C'⌝ ={E}[E']▷=∗
       Φ (mkVal #b 𝓥')))
   -∗ WP CAS #l #vr vw orf or ow at 𝓥 @ E {{ Φ }}.
 Proof.
@@ -634,13 +634,13 @@ Proof.
       - repeat split; auto.
         eapply (atw_local_mono _ ws ws); [done| |apply ATW]. by solve_lat. }
     iDestruct "HΦ" as (P) "(P & _ & HΦ)".
-    iSpecialize ("HΦ" with "[%] P"); [done|]. iMod "HΦ".
-    iIntros "!> !>". iMod "HΦ".
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iMod ("VS" with "Hσ") as "[Hσ' [seen' ar]]". rewrite decide_True; [|done].
-    iMod ("HClose" with "Hσ'") as "$". iModIntro. iSplitL "";[done|].
-    by iApply ("HΦ" with "seen' hist ar na aw").
+    iMod ("HClose" with "Hσ'") as "$".
+    (* done accessing hist_ctx *)
+    iMod ("HΦ" with "[%//] P seen' hist ar na aw [%//]") as "HΦ".
+    iIntros "!> !>". by iMod "HΦ" as "$".
   - iClear "VSR".
     assert (∃ tr 𝑚, ot = Some tr ∧ 𝑚s = [𝑚]) as [tr [𝑚 [? ?]]].
     { inversion_clear DRFPost. by do 2 eexists. } subst ot 𝑚s.
@@ -662,26 +662,22 @@ Proof.
     match goal with
     | H : lit_eq _ _ _ |- _ => inversion H as [| |lr|lr]; clear H
     end.
-    + iMod ("HΦ" with "[%//] P") as "HΦ".
-      iIntros "!> !>". iMod "HΦ".
-      (* accessing hist_ctx *)
+    + (* accessing hist_ctx *)
       iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
       iMod ("VS" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
       iDestruct (hist_ctx_hist_good with "Hσ' hist'") as %WFC'.
-      iMod ("HClose" with "Hσ'") as "$".
+      iMod ("HClose" with "Hσ'") as "$". rewrite EQT.
       (* done accessing hist_ctx *)
-      iModIntro. iSplit; [done|]. rewrite EQT.
-      by iApply ("HΦ" with "seen' hist' at' na aw' [%]").
-    + iMod ("HΦ" with "[%] P") as "HΦ"; [done|].
-      iIntros "!> !>". iMod "HΦ".
-      (* accessing hist_ctx *)
+      iMod ("HΦ" with "[%//] P seen' hist' at' na aw' [%//]") as "HΦ".
+      iIntros "!> !>". by iMod "HΦ" as "$".
+    + (* accessing hist_ctx *)
       iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
       iMod ("VS" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
       iDestruct (hist_ctx_hist_good with "Hσ' hist'") as %WFC'.
-      iMod ("HClose" with "Hσ'") as "$".
+      iMod ("HClose" with "Hσ'") as "$". rewrite EQT.
       (* done accessing hist_ctx *)
-      iModIntro. iSplit; [done|]. rewrite EQT.
-      by iApply ("HΦ" with "seen' hist' at' na aw' [%]").
+      iMod ("HΦ" with "[%//] P seen' hist' at' na aw' [%//]") as "HΦ".
+      iIntros "!> !>". by iMod "HΦ" as "$".
     + subst. iClear "HΦ seen".
       rewrite bi.and_elim_l.
       iMod ("HP" with "P") as "Hl". iDestruct "Hl" as (??) "Hl".