Commit c9f47674 authored by Dan Frumin's avatar Dan Frumin

Fix a_store_spec & add another test

parent 77f7d02d
......@@ -149,12 +149,14 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_store_spec `{Timeless _ R} (l : loc) (v : val) (w : val) Φ :
Lemma a_store_spec `{Timeless _ R} (l : loc) (v : val) (we : expr) (w : val) Φ :
IntoVal we w
l U v -
(l L w - Φ w) -
awp (a_store (a_ret #l) (a_ret w)) R Φ.
awp (a_store (a_ret (#l)%E) (a_ret we)) R Φ.
Proof.
unfold a_store. iIntros "Hv HΦ".
intros <-%of_to_val. unfold a_store.
iIntros "Hv HΦ".
rewrite /a_ret. do 4 awp_lam.
iApply awp_bind.
iApply (awp_par (fun v => v = #l) (fun v => v = w))%I.
......
......@@ -19,4 +19,20 @@ Section test.
iIntros "Hl". awp_pure _.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
Lemma test2 (l : loc) R `{Timeless _ R}:
l U #3 -
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l))%E R (fun v => v = #1).
Proof.
iIntros "Hl".
iApply awp_bind.
iApply (a_store_spec with "Hl"). iIntros "Hl".
awp_lam.
iApply awp_bind.
iApply a_seq_spec.
rewrite U_unlock. iRevert "Hl". rewrite -(U_mono (l U #1) (awp _ _ _))%I. eauto.
iIntros "Hl". awp_pure _.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
End test.
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