Strengthen some rules.

This commits makes some λMC rules atomic, in the sense that the user
can use the shared resources for the duration of the rule.

theories/c_translation/translation.v

@@ -267,15 +267,16 @@ Section proofs.
   Qed.
 
   Lemma cwp_free R Φ e :
-    CWP e @ R {{ v, ∃ cl ws, ⌜ v = cloc_to_val cl ⌝ ∧
-                             block_info cl true (length ws) ∗ cl ↦C∗ ws ∗ Φ #() }} -∗
+    CWP e @ R {{ v, R ={⊤}=∗ ∃ cl ws, ⌜ v = cloc_to_val cl ⌝ ∧
+                        block_info cl true (length ws) ∗ cl ↦C∗ ws ∗ R ∗ Φ #() }} -∗
     CWP freeᶜ(e) @ R {{ Φ }}.
   Proof.
     iIntros "H".
     cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
     iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
-    iIntros (v). iDestruct 1 as (cl ws ->) "(Hinfo & Hcl & HΦ)". cwp_pures.
+    iIntros (v) "H". cwp_pures.
     iApply cwp_atomic_env. iIntros (env) "Henv HR". wp_pures.
+    iMod ("H" with "HR") as (cl ws ->) "(Hinfo & Hcl & $ & HΦ)". cwp_pures.
     rewrite cloc_to_val_eq. wp_pures.
     iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
     iAssert ⌜ ∀ i : nat, is_Some (ws !! i) → (cl +∗ i) ∉ locked_locs σ⌝%I as %Hlocked.
@@ -302,7 +303,7 @@ Section proofs.
       wp_op. iSplit; first done. iNext; wp_pures.
       iApply ("IH" with "[%] Hlocks HΨ"). lia. }
     wp_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
-    iIntros "!> {$HΦ $HR}". iExists X, _.
+    iIntros "!> {$HΦ}". iExists X, _.
     iFrame "Hlock". iSplit; last by iApply "Hclose".
     iPureIntro; intros w Hw. destruct (HX _ Hw) as (cl'&Hcl&Hin).
     exists cl';  split; first done. apply locked_locs_free_heap; first done.
@@ -315,8 +316,8 @@ Section proofs.
   Lemma cwp_store R Φ Ψ1 Ψ2 e1 e2 :
     CWP e1 @ R {{ Ψ1 }} -∗
     CWP e2 @ R {{ Ψ2 }} -∗
-    (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ cl w,
-              ⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] v2 -∗ Φ v2)) -∗
+    (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R ={⊤}=∗ ∃ cl w,
+        ⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] v2 ={⊤}=∗ R ∗ Φ v2)) -∗
     CWP e1 =ᶜ e2 @ R {{ Φ }}.
   Proof.
     iIntros "H1 H2 HΦ".
@@ -325,9 +326,9 @@ Section proofs.
     cwp_lam. cwp_pures.
     iApply cwp_bind. iApply (cwp_par with "H1 H2").
     iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
-    iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
     iApply cwp_atomic_env.
     iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
+    iMod ("HΦ" with "H1 H2 HR") as (cl w ->) "[Hl HΦ]".
     iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
     iDestruct (mapsto_offset_non_neg with "Hl") as %?.
     assert ((#(cloc_base cl), #(cloc_offset cl))%V ∉ X) as HclX.
@@ -341,22 +342,24 @@ Section proofs.
     wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
     iApply wp_fupd. wp_store.
     iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
-    iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
+    iMod ("HΦ" with "Hl") as "HΦ".
+    iIntros "!> !>". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
     iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} ∪ X), _.
     iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
   Qed.
 
   Lemma cwp_load_exists_frac R Φ e :
-    CWP e @ R {{ v, ∃ cl q w, ⌜ v = cloc_to_val cl ⌝ ∧
-                              cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) }} -∗
+    CWP e @ R {{ v, R ={⊤}=∗ ∃ cl q w, ⌜ v = cloc_to_val cl ⌝ ∧
+                        cl ↦C{q} w ∗ (cl ↦C{q} w ={⊤}=∗ R ∗ Φ w) }} -∗
     CWP ∗ᶜe @ R {{ Φ }}.
   Proof.
     iIntros "H".
     cwp_apply (cwp_wp with "H"); iIntros (v) "H". cwp_lam. cwp_pures.
     iApply cwp_bind. iApply (cwp_wand with "H"). clear v.
-    iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". cwp_pures.
-    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
+    iIntros (v) "H". cwp_pures.
     iApply cwp_atomic_env. iIntros (env) "Henv HR".
+    iMod ("H" with "HR")  as (cl q w ->) "[Hl HΦ]".
+    iDestruct (mapsto_offset_non_neg with "Hl") as %?.
     iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
     iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
     assert ((#(cloc_base cl), #(cloc_offset cl))%V ∉ X) as HclX.
@@ -368,20 +371,22 @@ Section proofs.
     wp_op. iSplit; first done. iNext; wp_seq.
     wp_load; wp_match.
     iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
+    iApply wp_fupd.
     wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
     iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
-    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
-    iExists X, _. by iFrame.
+    iMod ("HΦ" with "Hl") as "[$ $]".
+    iIntros "!> !>". iExists X, _. by iFrame.
   Qed.
 
   Lemma cwp_load R Φ q e :
-    CWP e @ R {{ v, ∃ cl w, ⌜ v = cloc_to_val cl ⌝ ∧
-                            cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) }} -∗
+    CWP e @ R {{ v, R ={⊤}=∗ ∃ cl w, ⌜ v = cloc_to_val cl ⌝ ∧
+                      cl ↦C{q} w ∗ (cl ↦C{q} w ={⊤}=∗ R ∗ Φ w) }} -∗
     CWP ∗ᶜe @ R {{ Φ }}.
   Proof.
     iIntros "H". iApply cwp_load_exists_frac.
     cwp_apply (cwp_wand with "H").
-    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
+    iIntros (v). iIntros "H HR".
+    iMod ("H" with "HR") as (cl w ->) "[H1 H2]". eauto 100 with iFrame.
   Qed.
 
   (** Helper lemma *)
@@ -656,8 +661,8 @@ Section proofs.
     iIntros (v1 v2) "Hv1 Hv2 !>". cwp_pures.
     iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
     iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
-    iExists cl, v; iFrame. iSplit; first done.
-    iIntros "Hl". cwp_pures. iApply cwp_bind.
+    iIntros "HR !>". iExists cl, v; iFrame. iSplit; first done.
+    iIntros "Hl !>". cwp_pures. iApply cwp_bind.
     iApply (cwp_store _ _
       (λ v', ⌜v' = cloc_to_val cl⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]").
     - cwp_proj. iApply cwp_ret; by wp_value_head.
@@ -665,8 +670,8 @@ Section proofs.
         try (try cwp_proj; iApply cwp_ret; by wp_value_head).
       iIntros (? ? -> ->); eauto.
     - iIntros (? ? -> ->).
-      iExists _, _; iFrame. iSplit; first done.
-      iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ".
+      iIntros "HR !>". iExists _, _; iFrame. iSplit; first done.
+      iIntros "? !>". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ".
   Qed.
 End proofs.
 

theories/vcgen/forward.v

@@ -226,8 +226,8 @@ Section forward_spec.
       iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
       iApply cwp_load. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
       iDestruct ("H2" with "Hm") as "[Hm2 Hi]".
-      iExists _, _. iFrame "Hi". iSplit; first by eauto.
-      iIntros "Hi"; iSplit; first done.
+      iIntros "$ !>". iExists _, _. iFrame "Hi". iSplit; first by eauto.
+      iIntros "Hi !>"; iSplit; first done.
       iApply denv_insert_interp; eauto with iFrame.
     - (* assign *)
       destruct (forward_aux _ _ _ _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
@@ -244,8 +244,8 @@ Section forward_spec.
       iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
       iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
       { iApply denv_merge_interp; eauto with iFrame. }
-      iExists _, _. iFrame "Hi". iSplit; first by eauto.
-      iIntros "Hi"; iSplit; first done.
+      iIntros "$ !>". iExists _, _. iFrame "Hi". iSplit; first by eauto.
+      iIntros "Hi !>"; iSplit; first done.
       iApply denv_insert_interp; eauto 10 with iFrame.
     - (* bin op *)
       destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.

theories/vcgen/vcg.v

@@ -514,7 +514,7 @@ Section vcg_spec.
       { iApply ("IH" with "[] [] Hm H"); eauto. }
       iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]".
       iDestruct (vcg_load_correct with "Hm H") as (cl q w ?) "[Hi H]"; eauto.
-      iExists _, _, _; iSplit; first done. iIntros "{$Hi} Hi".
+      iIntros "$ !>". iExists _, _, _; iSplit; first done. iIntros "{$Hi} Hi".
       by iApply vcg_continuation_mono; last by iApply "H".
     - (* assign *)
       destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
@@ -528,7 +528,7 @@ Section vcg_spec.
           eauto using denv_wf_mono, dval_wf_mono.
         { iApply denv_merge_interp; eauto using denv_wf_mono.
           iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
-        iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
+        iIntros "$ !>". iExists _, _; iSplit; first done. iIntros "{$Hi} Hi !>".
         rewrite (dval_interp_mono E E'); eauto.
         by iApply vcg_continuation_mono; last by iApply "H".
       + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
@@ -540,7 +540,7 @@ Section vcg_spec.
         { iApply denv_merge_interp; eauto using denv_wf_mono.
           iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
         rewrite (dval_interp_mono E E'); eauto.
-        iExists _, _; iSplit; first done. iIntros "{$Hi} Hi".
+        iIntros "$ !>". iExists _, _; iSplit; first done. iIntros "{$Hi} Hi !>".
         by iApply vcg_continuation_mono; last by iApply "H".
     - (* bin op *)
       destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.