Tighter version of c_call

theories/c_translation/translation.v

@@ -146,8 +146,10 @@ Notation "'λᶜ' x , e" := (c_fun (λ: x, e)%V)
 
 Definition c_call : val := λ: "f" "arg",
   (* sequence point before a function call *)
-  "fa" ←ᶜ ("f" |||ᶜ "arg");ᶜ
-  c_atomic (λ: <>, (Fst "fa") (Snd "fa")).
+  "fa" ←ᶜ ("f" |||ᶜ "arg") ;;ᶜ
+  c_atomic (λ: <>,
+    c_atomic_env mset_clear ;;ᶜ
+    (Fst "fa") (Snd "fa")).
 Notation "'callᶜ' f a" :=
   (c_call f a)%E
   (at level 10, f, a at level 9,
@@ -382,30 +384,39 @@ Section proofs.
     iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
   Qed.
 
-  (* Internal spec: breaks the abstraction/notation *)
-  Lemma cwp_seq_bind' R Φ e (f: val) :
-    CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -∗
-    CWP c_seq_bind e f @ R {{ Φ }}.
+  (** Helper lemma *)
+  Lemma cwp_mset_clear R Φ :
+    ▷ U (Φ #()) -∗
+    CWP c_atomic_env mset_clear @ 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"). iIntros (w) "H".
-    cwp_pures. iApply cwp_bind.
-    iApply cwp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
-    iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
+    iIntros "HΦ". iApply cwp_atomic_env.
+    iIntros (env). iDestruct (1) as (X σ _) "[Hlocks Hσ]".
+    iIntros "$". iApply wp_fupd.
     wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
-    rewrite U_eq. iDestruct "H" as (us) "[Hus H]".
+    rewrite U_eq. iDestruct "HΦ" as (us) "[Hus H]".
     iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
-    - iModIntro. iSplitR "H".
+    - iModIntro. iNext. iSplitR "H Hus".
       + iExists ∅, σ. by iFrame.
-      + iNext. cwp_lam. by iApply "H".
+      + iFrame. by iApply "H".
     - iDestruct "Hus" as "[Hu Hus]".
       iDestruct (full_locking_heap_locked_present with "Hu Hσ") as %[z Hz].
       iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
-      iApply ("IH" with "Hus [H Hu] Hσ Hlocks").
+      iApply ("IH" with "Hus [Hu H] Hσ Hlocks").
       iIntros "Hus". iApply "H". by iFrame.
   Qed.
 
+  (* Internal spec: breaks the abstraction/notation *)
+  Lemma cwp_seq_bind' R Φ e (f: val) :
+    CWP e @ R {{ v, U (CWP f v @ R {{ Φ }}) }} -∗
+    CWP c_seq_bind e f @ 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"). iIntros (w) "H".
+    cwp_pures. iApply cwp_bind. iApply cwp_mset_clear.
+    iNext. iModIntro. by cwp_lam.
+  Qed.
+
   Lemma cwp_seq_bind R Φ x e1 e2 :
     CWP e1 @ R {{ v, U (CWP subst' x v e2 @ R {{ Φ }}) }} -∗
     CWP x ←ᶜ e1 ;ᶜ e2 @ R {{ Φ }}.
@@ -535,11 +546,12 @@ Section proofs.
     cwp_apply (cwp_wp with "H2"); iIntros (vf) "H2".
     cwp_apply (cwp_wp with "H1"); iIntros (va) "H1".
     cwp_lam. cwp_pures.
-    iApply cwp_seq_bind'. iApply (cwp_par with "H1 H2").
-    iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"); iModIntro.
-    cwp_pures.
-    iApply cwp_atomic. iIntros "HR". iSpecialize ("H" with "HR").
-    iExists True%I. iModIntro; iSplit; first done. cwp_pures.
+    iApply cwp_bind. iApply (cwp_par with "H1 H2").
+    iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2").
+    cwp_pures. iApply cwp_atomic. iIntros "HR". iNext.
+    iExists True%I. iSplitR; first done. cwp_pures.
+    iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro.
+    iSpecialize ("H" with "HR"). cwp_pures.
     iApply (cwp_wand with "H"); eauto.
   Qed.