Commit 644307d8 authored by Léon Gondelman's avatar Léon Gondelman

a_run proof restored

parent c0d31e02
......@@ -77,17 +77,20 @@ Section a_wp.
WP a_run v {{ Φ }}.
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.
*) Admitted.
Lemma awp_atomic (v : val) R Φ :
(R - R', R' awp v R' (λ w, R' - R Φ w)) -
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment