Commit 6ce58f78 authored by Dan Frumin's avatar Dan Frumin

Simplify a_run

parent d1ce91a5
......@@ -24,10 +24,7 @@ Notation "y ;;ᶜ z" := (a_bind y (λ: <>, z))%E
Definition a_run : val := λ: "x",
let: "env" := mset_create #() in
let: "l" := newlock #() in
let: "v" := "x" "env" "l"
in "v". (* TODO: we have a dummy step here :(
but potentially we would have a free(l) operation here
*)
"x" "env" "l".
(* M A → M A *)
Definition a_atomic : val := λ: "x" "env" "l",
......@@ -312,7 +309,6 @@ Section a_wp_run.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
iMod (wp_value_inv with "Hwp") as "Hwp".
wp_bind (ev env k).
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[s := LockRes _ 1 ρ]} with "Hlock [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
......@@ -320,7 +316,6 @@ Section a_wp_run.
- iIntros (w) "[HΦ Hres]".
rewrite /flock_resources big_sepM_singleton /=.
iMod (flock_res_dealloc with "Hlock Hres") as "[Henv HR]"; try done.
wp_let.
iApply "HΦ". iFrame.
Qed.
End a_wp_run.
......
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