Commit 38d65e8a authored by Dan Frumin's avatar Dan Frumin

Add multiple assignment through functions test

parent 9c4c7f6d
......@@ -73,4 +73,94 @@ Section test.
awp_let. awp_load_ret l.
Qed.
Definition assignF : val := λ: "lv",
let: "l" := Fst "lv" in
let: "v" := Snd "lv" in
a_store (a_ret "l") (a_ret "v") ;;;; a_ret "v".
(* Better a_par spec.
But it uses proofmode.v, and cannot be proved from awp_par. *)
Lemma a_par_spec (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
awp e1 R Ψ1 -
awp e2 R Ψ2 -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
awp (a_par e1 e2) R Φ.
Proof.
iIntros "Hwp1 Hwp2 HΦ".
rewrite /a_par /=.
awp_apply (a_wp_awp with "Hwp1"); iIntros (ev1) "Hwp1".
awp_lam.
awp_apply (a_wp_awp with "Hwp2"); iIntros (ev2) "Hwp2".
awp_lam.
rewrite /awp /=. wp_value_head.
iIntros (γ π env l) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam.
iApply (par_spec (λ v, Ψ1 v unflocked _ (π/2))%I
(λ v, Ψ2 v unflocked _ (π/2))%I
with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
- wp_lam. wp_apply (wp_wand with "Hwp1").
iIntros (v) "Hwp1". by iApply "Hwp1".
- wp_lam. wp_apply (wp_wand with "Hwp2").
iIntros (v) "Hwp2". by iApply "Hwp2".
- iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
iApply ("HΦ" with "[$] [$]").
Qed.
Lemma invoke_assignF_1 l (v v' : val) R :
l U v -
awp (a_invoke assignF (a_par (a_ret #l) (a_ret v'))) R
(λ w, l U v' w = v').
Proof.
iIntros "Hl".
iApply (a_invoke_simpl _ _ _ (λ v, v = (#l,v')%V)%I).
- iApply (a_par_spec (λ v, v = #l)%I (λ v, v = v')%I).
+ iApply awp_ret. by wp_value_head.
+ iApply awp_ret. by wp_value_head.
+ iNext. iIntros (? ? -> ->); done.
- iIntros (? ->). iModIntro.
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iExists _; iFrame. iIntros "Hl".
iModIntro. awp_lam.
iApply awp_ret; wp_value_head. eauto.
Qed.
Lemma invoke_assignF_2 (l : loc) (v' : val) R :
awp (a_invoke assignF (a_par (a_ret #l) (a_ret v')))
(l U - R)%I (λ w, w = v')%I.
Proof.
iApply (a_invoke_spec _ _ _ (λ v, v = (#l,v')%V)%I).
- iApply (a_par_spec (λ v, v = #l)%I (λ v, v = v')%I).
+ iApply awp_ret. by wp_value_head.
+ iApply awp_ret. by wp_value_head.
+ iNext. iIntros (? ? -> ->); done.
- iIntros (? ->). iModIntro.
iIntros "[Hl HR]". iExists R%I. iFrame.
unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
iApply a_sequence_spec.
iApply a_store_ret.
iApply awp_ret; wp_value_head.
iDestruct "Hl" as (?) "Hl".
iExists _; iFrame. iIntros "Hl".
iModIntro. awp_lam. iApply awp_ret; wp_value_head.
iIntros "$". iSplit; eauto.
Qed.
Lemma invoke_test (l : loc) (z0 z1 z2: Z) R :
l U #z0 -
awp (a_bin_op PlusOp
(a_invoke assignF (a_par (a_ret #l) (a_ret #z1)))
(a_invoke assignF (a_par (a_ret #l) (a_ret #z2)))) R
(λ v, v = #(z1 + z2))%I.
Proof.
iIntros "Hl".
iApply (awp_insert_res _ _ (l U -)%I with "[Hl]").
{ iNext. by iExists #z0. }
iApply a_bin_op_spec.
- iApply invoke_assignF_2.
- iApply invoke_assignF_2.
- iIntros (? ? -> ->). iExists #(z1+z2). 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