Merge branch 'master' of gitlab.science.ru.nl:lgg/iris-c-monad

theories/c_translation/monad.v

@@ -78,17 +78,20 @@ Section a_wp.
     WP a_run v {{ Φ }}.
   Proof.
     iIntros "HR Hwp". rewrite /a_run /=. wp_let.
-    wp_let. wp_alloc env. wp_let.
-
-(*
-    wp_apply (newlock_cancel_spec R with "[$]").
-    iIntros (k γ') "Hlock". wp_let. iApply wp_fupd.
-    iApply (wp_wand with "[Hwp Hlock]"); first by iApply "Hwp".
+    wp_bind (newset #()).
+    iApply set_newset_spec. done.
+    iNext. iIntros (v0) "%".
+    wp_alloc env as "H". wp_let.
+    wp_apply (newlock_cancel_spec (env_inv #env ∗ R)%I with "[H HR]").
+    iFrame. iExists ∅. iExists env, v0. iFrame. done.
+    iIntros (k γ') "Hlock". wp_let. rewrite- wp_fupd.
+    iApply (wp_wand with "[Hwp Hlock]").
+    unfold awp. iApply ("Hwp" with "Hlock").
     iIntros (w) "[HΦ Hlock]".
-    iMod (cancel_lock with "Hlock") as "HR".
-    by iApply "HΦ".
+    iApply "HΦ".
+    iMod (cancel_lock with "Hlock") as "[HEnv HR]".  done.
   Qed.
-*) Admitted.
+
 
   Lemma awp_atomic (v : val) R Φ `{Timeless _ R} :
     (R -∗ ∃ R', ⌜Timeless R'⌝ ∧ R' ∗ awp v R' (λ w, R' -∗ R ∗ Φ w)) -∗