Commit 450428f7 authored by Robbert Krebbers's avatar Robbert Krebbers

Support alloc in the vcgen; memcpy remains to be fixed... :(

parent 561a7cde
......@@ -32,10 +32,10 @@ Section derived.
( l: cloc, l C replicate n ev2 - Φ (cloc_to_val l)) -
awp (a_alloc (a_ret e1) (a_ret e2)) R Φ.
Proof.
iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I).
iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I (λ v, v = ev2)%I).
- iApply awp_ret. by iApply wp_value.
- iApply awp_ret. wp_value_head.
iNext. iIntros (? ->). iExists n; iSplit; eauto.
- iApply awp_ret. by iApply wp_value.
- iIntros "!>" (?? -> ->). iExists n; iSplit; eauto.
Qed.
Lemma a_store_ret (cl:cloc) (e: expr) `{Closed [] e} R Φ :
......
......@@ -174,19 +174,20 @@ Notation "e1 +∗=ᶜ e2" := (a_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) :
Section proofs.
Context `{amonadG Σ}.
Lemma a_alloc_spec R Φ Ψ1 e1 e2 :
Lemma a_alloc_spec R Φ Ψ1 Ψ2 e1 e2 :
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ v2, ( v1, Ψ1 v1 - n : nat,
v1 = #n
l, l C replicate n v2 - Φ (cloc_to_val l)) }} -
AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - n : nat,
v1 = #n
l, l C replicate n v2 - Φ (cloc_to_val l)) -
AWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 HΦ".
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
awp_apply (a_wp_awp with "HΦ"); iIntros (v2) "H2". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
iDestruct ("H2" with "H1") as (n ->) "HΦ".
iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
iApply awp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
......
......@@ -212,6 +212,11 @@ Section properties.
Lemma mapsto_downgrade lv cl q v : cl C{q} v - cl C[lv]{q} v.
Proof. apply mapsto_downgrade'. by apply lvl_included. Qed.
Lemma cloc_add_0 cl : cloc_add cl 0 = cl.
Proof. rewrite /cloc_add Nat.add_0_r. by destruct cl. Qed.
Lemma cloc_add_add cl i j : cloc_add (cloc_add cl i) j = cloc_add cl (i + j).
Proof. by rewrite /cloc_add /= Nat.add_assoc. Qed.
Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
Proof. destruct cl. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
Lemma cloc_to_of_val v cl : cloc_of_val v = Some cl cloc_to_val cl = v.
......
......@@ -254,8 +254,8 @@ Qed.
(** DCexpr *)
Inductive dcexpr : Type :=
| dCRet : dval dcexpr
| dCAlloc : dcexpr dcexpr
| dCRet : dval dcexpr
| dCAlloc : dcexpr dcexpr dcexpr
| dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr
| dCBinOp : cbin_op dcexpr dcexpr dcexpr
......@@ -269,7 +269,7 @@ Inductive dcexpr : Type :=
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with
| dCRet dv => a_ret (dval_interp E dv)
| dCAlloc de1 => a_alloc (dcexpr_interp E de1)
| dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCLoad de1 => a_load (dcexpr_interp E de1)
| dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
......@@ -294,8 +294,8 @@ Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet dv => dval_wf E dv
| dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
| dCStore de1 de2 | dCBinOp _ de1 de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2
| dCUnknown _ => true
......@@ -319,11 +319,7 @@ Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof.
induction de; simplify_eq /=; try eauto; [ apply dval_wf_mono | | | | |];
naive_solver.
Qed.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dun_op_eval_dSome_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = dSome dw dval_wf E dw.
......@@ -463,10 +459,10 @@ Global Instance into_dcexpr_ret E v dv:
IntoDCexpr E (a_ret v) (dCRet dv).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_alloc E e de:
IntoDCexpr E e de
IntoDCexpr E (a_alloc e) (dCAlloc de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_alloc E e1 e2 de1 de2 :
IntoDCexpr E e1 de1 IntoDCexpr E e2 de2
IntoDCexpr E (a_alloc e1 e2) (dCAlloc de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_load E e de:
IntoDCexpr E e de
......
......@@ -16,12 +16,10 @@ Section memcpy.
"p" ←ᶜ a_alloc 1 (a_ret (Fst "arg"));;
"q" ←ᶜ a_alloc 1 (a_ret (Fst (Snd "arg")));;
let: "n" := Snd (Snd "arg") in
"pend" ←ᶜ ∗ᶜ(a_ret "p") +∗ᶜ (a_ret "n");;
while (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend"))
{ ((a_ret "p")+=ᶜ♯1) = (∗ᶜ((a_ret "q")+=ᶜ♯1)) }.
Lemma cloc_add_0 cl : cloc_add cl 0 = cl.
Proof. destruct cl; cbv[cloc_add]. simpl. by rewrite Nat.add_0_r. Qed.
"pend" ←ᶜ ∗ᶜ (a_ret "p") +∗ᶜ (a_ret "n");;
while (∗ᶜ (a_ret "p") <∗ᶜ a_ret "pend") {
(a_ret "p" += 1) = ∗ᶜ(a_ret "q" += 1)
}.
Lemma memcpy_body_spec (* (i: nat) *) (pp qq p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
......@@ -97,10 +95,11 @@ Section memcpy.
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Hp Hq".
iApply a_invoke_simpl.
vcg_solver. iModIntro.
awp_lam. iApply awp_bind.
iApply (a_alloc_spec _ _ (λ v, v = #1))%I; first by (iApply awp_ret; wp_value_head).
iApply a_invoke_simpl. vcg_solver. iModIntro.
awp_lam. iApply awp_bind. vcg_solver. repeat awp_proj. iApply awp_ret; wp_value_head.
vcg_continue. iExists 1%nat; iSplit; first done.
iIntros ([pp ppi]) "[Hpp _]". vcg_continue. iIntros "Hll". awp_let.
iApply awp_bind. vcg_solver. (*
awp_proj. iApply awp_ret; wp_value_head.
iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto.
iIntros (pp) "[Hpp _]". rewrite {3}/cloc_add. etaprod pp.
......@@ -118,6 +117,5 @@ Section memcpy.
{ iPureIntro. repeat (case_option_guard; last omega). simpl.
repeat f_equal. rewrite !Nat2Z.id //. }
awp_let. iApply (memcpy_body_spec with "Hp Hq Hpp Hqq"); auto.
Qed.
Qed. *) Admitted.
End memcpy.
......@@ -32,13 +32,11 @@ Section tests_vcg.
Lemma test2 (k : cloc) :
k C #10 - awp (alloc (2,11) = ∗ᶜ♯ₗk + 2) True (λ v, v = #12).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk". iApply (a_alloc_ret 2).
iIntros "Hk". vcg_solver. iExists 2%nat. iSplit; first done.
iIntros (l) "[Hl1 [Hl2 _]]". etaprod l.
vcg_continue. eauto 42 with iFrame.
Qed.
Lemma test6 (l k : cloc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
( Φ, Φ #11 - awp e1 True Φ) -
( Φ, Φ #12 - awp e2 True Φ) -
......@@ -54,5 +52,4 @@ Section tests_vcg.
iApply "He2".
vcg_continue. iIntros "Hk Hl". eauto with iFrame.
Qed.
End tests_vcg.
......@@ -79,7 +79,8 @@ End vcg_continue.
Arguments vcg_wp_continuation {_ _ _ _}.
Declare Reduction vcg_cbv :=
cbv [ vcg_wp vcg_wp_bin_op vcg_wp_pre_bin_op vcg_wp_store vcg_wp_load vcg_wp_awp_continuation mapsto_wand_list].
cbv [ vcg_wp vcg_wp_bin_op vcg_wp_pre_bin_op vcg_wp_alloc vcg_wp_store
vcg_wp_load vcg_wp_awp_continuation mapsto_wand_list].
Ltac vcg_compute :=
match goal with
......
......@@ -74,7 +74,7 @@ Section vcg.
''(ms1, mNew1, dv1) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2;
Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
| dCAlloc _ | dCUnknown _ | dCInvoke _ _ => None
| dCAlloc _ _ | dCUnknown _ | dCInvoke _ _ => None
end.
Definition vcg_sp'
......@@ -97,6 +97,12 @@ Section vcg.
(m: denv) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
( n : nat,
dval_interp E dv1 = #n
l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I.
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match is_dloc E dv with
......@@ -174,6 +180,19 @@ Section vcg.
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match de with
| dCRet dv => Φ E m dv
| dCAlloc de1 de2 =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCLoad de1 =>
vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ)
| dCStore de1 de2 =>
......@@ -615,10 +634,10 @@ Section vcg_spec.
iSpecialize ("Hwp" with "Hm"). simpl.
iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
iExists (dloc_interp E (dLoc i)), q, v'; iSplit; first done. iFrame.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
iExists l, q, v'. iSplit; first done. iFrame.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
iExists l, q, v'. iSplit; first done. iFrame.
Qed.
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
......@@ -726,7 +745,6 @@ Section vcg_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
Qed.
Lemma vcg_wp_continuation_mono E E' Φ w:
E `prefix_of` E' vcg_wp_continuation E' Φ w - vcg_wp_continuation E Φ w.
Proof.
......@@ -746,7 +764,28 @@ Section vcg_spec.
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- iApply awp_ret. wp_value_head.
iExists E, d, m. iSplit; first done; by iFrame.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
- simpl in *. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first.
+ destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first.
{ by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; first done.
clear Heqsp2 Heqsp.
iDestruct (IHde1 with "Hm' Hwp") as "Hde1"; try done.
iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]".
rewrite (dval_interp_mono E E') //.
iDestruct "H" as (n ->) "HΦ". iExists n; iSplit; first done.
iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
+ specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]";
first done. clear Heqsp.
iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done.
iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 -> ???) "[Hm' H]".
rewrite (dval_interp_mono E E') //.
iDestruct "H" as (n ->) "HΦ". iExists n; iSplit; first done.
iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
- rewrite IHde //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]").
......
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