Add a_store_spec

theories/c_translation/monad.v

@@ -125,12 +125,15 @@ Section a_wp.
     iIntros "Hunfl". wp_seq. iFrame.
   Qed.
 
-  Lemma awp_par (v1 v2 : val) R (Ψ1 Ψ2 Φ : val → iProp Σ) :
-    awp v1 R Ψ1 -∗
-    awp v2 R Ψ2 -∗
+  Lemma awp_par (ve1 ve2 : expr) (v1 v2 : val) R (Ψ1 Ψ2 Φ : val → iProp Σ) :
+    IntoVal ve1 v1 →
+    IntoVal ve2 v2 →
+    awp ve1 R Ψ1 -∗
+    awp ve2 R Ψ2 -∗
     ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
-    awp (a_par v1 v2) R Φ.
+    awp (a_par ve1 ve2) R Φ.
   Proof.
+    intros ? ?. rewrite -(of_to_val ve1 v1); last done. rewrite -(of_to_val ve2 v2); last done.
     iIntros "Hwp1 Hwp2 HΦ" (γ π env l) "#Hlock [Hunfl1 Hunfl2]".
     rewrite /a_par /=. do 4 wp_lam.
     iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I

theories/c_translation/translation.v

@@ -38,9 +38,8 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
 Definition a_seq : val := λ: "env",
   a_atomic_env (λ: "env", mset_clear "env") "env".
 
-
 Section proofs.
-  Context `{locking_heapG Σ, heapG Σ, flockG Σ}.
+  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
 
   Lemma a_load_spec R `{Timeless _ R} (l : loc) (v : val) Φ :
     l ↦U v -∗
@@ -103,4 +102,58 @@ Section proofs.
     - by iApply "HΦ".
   Qed.
 
+  Lemma a_store_spec `{Timeless _ R} (l : loc) (v : val) (w : val) Φ :
+    l ↦U v -∗
+    (l ↦L w -∗ Φ w) -∗
+    awp (a_store (a_ret #l) (a_ret w)) R Φ.
+  Proof.
+    unfold a_store. iIntros "Hv HΦ".
+    rewrite /a_ret.
+    repeat (awp_pure _).
+    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
+    Opaque par. repeat (wp_pure _).
+    wp_bind (_ ||| _)%E.
+    iApply (wp_par (fun v => ⌜v = #l⌝) (fun v => ⌜v = w⌝))%I.
+    { repeat wp_pure _. eauto. }
+    { repeat wp_pure _. eauto. }
+    iIntros (? ?) "[% %]"; simplify_eq/=. iNext.
+    wp_let. wp_let.
+    iRevert "Hflock Hunfl". iRevert (γ π env lk).
+    iApply awp_atomic_env.
+    iIntros (env) "Henv HR".
+    rewrite {2}/env_inv.
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Hlocks" as %Hlocks.
+    iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
+    assert (#l ∉ X).
+    { unfold correct_locks in *. intros Hx. apply Hl.
+      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
+    wp_let. wp_proj.
+    wp_apply (mset_add_spec with "[$HX]"); eauto.
+    iIntros "HX". wp_seq.
+    iAssert (⌜σ !! l = Some ULvl⌝%I) with "[Hσ Hv]" as %?.
+    { rewrite mapsto_eq /mapsto_def.
+      iDestruct "Hv" as "[Hv Hl]".
+      by iDestruct (own_valid_2 with "Hσ Hl")
+        as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
+    iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
+    do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
+    iDestruct "Hv" as "[Hv Hl]".
+    rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
+    iDestruct "Hls" as "[Hl' Hls]".
+    iDestruct "Hl'" as (?) "Hl'".
+    iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
+    iCombine "Hv Hl'" as "Hv".
+    wp_store.
+    iDestruct "Hv" as "[Hv Hl']".
+    iSpecialize ("Hls" with "[Hl']"); eauto.
+    wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
+    - iExists ({[#l]} ∪ X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+      + rewrite -big_sepM_insert_override; eauto.
+      + (* TODO: a separate lemma somewhere *)
+        iPureIntro. rewrite locked_locs_lock.
+        revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
+    - iApply "HΦ". iFrame.
+  Qed.
+
 End proofs.

theories/lib/mset.v

@@ -148,11 +148,14 @@ Section MutableSet_wp.
     iExists s, hd. eauto.
   Qed.
 
-  Lemma mset_add_spec (x: val) (xs: val) (X:  gset val):
+  Lemma mset_add_spec (xe xse: expr) (x xs: val) (X:  gset val):
+    IntoVal xe x →
+    IntoVal xse xs →
     {{{ is_set_mut xs X ∧ ⌜x ∉ X⌝ }}}
-      mset_add x xs
+      mset_add xe xse
     {{{ RET #() ; (is_set_mut xs ({[x]} ∪ X))}}}.
   Proof.
+    intros ??. rewrite -(of_to_val xe x); last done. rewrite -(of_to_val xse xs); last done.
     iIntros (Φ) "[Hmut %] HPost".
     iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
     do 2 wp_lam; wp_load; wp_let.
@@ -162,7 +165,6 @@ Section MutableSet_wp.
     iExists s, v. by iFrame.
   Qed.
 
-
   Lemma mset_clear_spec (xs: val) (X:  gset val):
     {{{ is_set_mut xs X }}}
       mset_clear xs