Commit 94f431da authored by Léon Gondelman's avatar Léon Gondelman
Browse files

extend vcgen with par.

parent 97c0d2c3
......@@ -43,4 +43,23 @@ Section test.
Proof.
iIntros "**". vcg_solver. auto.
Qed.
Lemma test_par_1 (l1 l2 : loc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
awp ( ∗ᶜ l1 ||| ∗ᶜ l2) True
(λ w, w = (v1, v2)%V l1 C v1 l2 C v2).
Proof.
iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma test_par_2 (l1 l2 : loc) (v1 v2: val) :
l1 C v1 - l2 C v2 -
awp ( (l1 = a_ret v2) ||| (l2 = a_ret v1) ) True
(λ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1).
Proof.
iIntros "**". vcg_solver. eauto with iFrame.
Qed.
(*TODO: test function call with multiple arguments *)
End test.
......@@ -5,47 +5,22 @@ From iris_c.vcgen Require Import dcexpr denv.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
(*
TODO
[DONE] Fix all the unknown cases, introduce a function for that (which should be
simpl never)
- Write more tests with unknown stuff in it
add tests like `!(l := 10;ᶜ l)`
[DONE] Support alloc in `vcg_wp`
- Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case
- Finish the proofs
[DONE] Maybe drop `wp_expr`? We are not taking it as an input of anything anymore
Less urgent TODO
- Symbolic fractions
- Support bind
- Support conditional
- Write examples with R
- Deal with functions
*)
(*
TODO:
Inductive dfrac :=
| dFrac : frac → dfrac
| dFracUnknown : nat → nat → frac → dfrac.
*)
Section vcg.
Context `{amonadG Σ}.
Fixpoint mapsto_wand_list_aux (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
Fixpoint mapsto_wand_list_aux
(E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
match m with
| [] => Φ
| None :: m' => mapsto_wand_list_aux E m' Φ (S i)
| Some (DenvItem x q dv) :: m' =>
dloc_interp E (dLoc i) C[x]{q} dval_interp E dv - mapsto_wand_list_aux E m' Φ (S i)
dloc_interp E (dLoc i) C[x]{q} dval_interp E dv -
mapsto_wand_list_aux E m' Φ (S i)
end%I.
Definition mapsto_wand_list (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
Definition mapsto_wand_list
(E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
mapsto_wand_list_aux E m Φ O.
Definition popstack (ms : list denv) : option (list denv * denv) :=
......@@ -87,10 +62,15 @@ Section vcg.
''(ms2, mNew2, dv2) vcg_sp E (denv_unlock mNew1 :: ms1) de2;
''(ms3, mNew3) popstack ms2;
Some (ms3, denv_merge mNew2 mNew3, dv2)
| dCAlloc _ | dCUnknown _ | dCPar _ _ => None
| dCPar de1 de2 =>
''(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 _ => None
end.
Definition vcg_sp' (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Definition vcg_sp'
(E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
''(ms,mNew,dv) vcg_sp E [m] de;
''(_, m') popstack ms;
Some (m', mNew, dv).
......@@ -105,8 +85,8 @@ Section vcg.
denv_interp E' m'
Φ E' m' dv)%I.
Definition vcg_wp_awp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
Definition vcg_wp_awp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr)
(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_load (E : known_locs) (dv : dval) (m : denv)
......@@ -151,7 +131,8 @@ Section vcg.
(m : denv) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match dbin_op_eval E op dv1 dv2 with
| dSome dw => Φ E m dw
| mdw => dw, doption_interp mdw = Some dw vcg_wp_continuation E Φ (dval_interp E dw)
| mdw => dw, doption_interp mdw = Some dw
vcg_wp_continuation E Φ (dval_interp E dw)
end%I.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
......@@ -195,6 +176,19 @@ Section vcg.
| dCSeq de1 de2 =>
vcg_wp E m de1 R (λ E m _,
U (vcg_wp E (denv_unlock m) de2 R Φ))
| dCPar de1 de2 =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| _ => vcg_wp_awp_continuation R E de m Φ
end%I.
End vcg.
......@@ -206,14 +200,19 @@ Section vcg_spec.
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
default 1%positive
(E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
Proof.
iIntros "H". iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
iIntros "H".
iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
- iIntros "[H1 H2]". rewrite -plus_n_O. iSpecialize ("H" with "H1").
iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2").
iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega.
- iIntros "[_ H2]". iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2").
iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega.
iIntros "!>" (n y ?) "/= H".
by replace (k + S n)%nat with (S k + n)%nat by omega.
- iIntros "[_ H2]". iApply ("IH" with "H [H2]").
iApply (big_sepL_impl with "H2").
iIntros "!>" (n y ?) "/= H".
by replace (k + S n)%nat with (S k + n)%nat by omega.
Qed.
Lemma mapsto_wand_list_spec E m Φ :
......@@ -232,38 +231,46 @@ Section vcg_spec.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=.
destruct dv1 as [ dv1| | dv1 ]; try destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
transitivity (length ms1).
+ by eapply IHde.
+ by eapply denv_delete_frac_2_length.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1;
simplify_eq /=.
destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
transitivity (length ms1).
+ by eapply IHde1.
+ transitivity (length ms2). by eapply IHde2.
by eapply denv_delete_full_2_length.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
simplify_eq/=.
destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
transitivity (length ms1); eauto.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
destruct (dun_op_eval E u dv1); simplify_eq/=.
by eapply IHde.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct ms2; simplify_eq/=.
transitivity (length ms1).
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct ms2; simplify_eq/=. transitivity (length ms1).
+ by eapply IHde1.
+ apply IHde2 in Hde2. by simplify_eq/=.
+ apply IHde2 in Hde2; by simplify_eq/=.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
transitivity (length ms1); eauto.
Qed.
Lemma vcg_sp_correct' E de ms ms' mNew dv R :
vcg_sp E ms de = Some (ms', mNew, dv)
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew)))%I.
(awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew)))%I.
Proof.
revert ms ms' mNew dv. induction de;
iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
......@@ -273,7 +280,8 @@ Section vcg_spec.
destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
iPoseProof IHde as "Hawp"; first done.
iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
......@@ -283,7 +291,8 @@ Section vcg_spec.
iApply a_load_spec.
iApply (awp_wand with "Hawp").
iIntros (?) "[% HmNew1]". simplify_eq/=.
iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
iExists _, _. iSplit; eauto.
iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
iIntros "Hl". iSplit; eauto.
rewrite -denv_insert_interp.
by iFrame.
......@@ -352,12 +361,26 @@ Section vcg_spec.
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
rewrite -denv_merge_interp. iSplit; eauto with iFrame.
- specialize (IHde1 ms).
destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
specialize (IHde2 ms1).
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply (awp_par with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>"; simplify_eq/=; iSplit; eauto.
rewrite -denv_merge_interp. iFrame.
Qed.
Lemma vcg_sp_correct E de m ms mNew dv R :
vcg_sp E [m] de = Some (ms, mNew, dv)
denv_interp E m -
denv_interp E (denv_stack_merge ms) awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew).
denv_interp E (denv_stack_merge ms)
awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
iIntros (Hsp) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
......@@ -370,7 +393,9 @@ Section vcg_spec.
Lemma vcg_sp'_correct E de m m' mNew dv R :
vcg_sp' E m de = Some (m', mNew, dv)
denv_interp E m -
denv_interp E m' awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew).
denv_interp E m'
awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
rewrite /vcg_sp'.
iIntros (Hsp') "Hm".
......@@ -393,16 +418,20 @@ Section vcg_spec.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
eapply denv_wf_delete_frac_2 in Hout1; eauto.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
simplify_eq /=.
destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as
[[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
......@@ -411,7 +440,8 @@ Section vcg_spec.
repeat split; eauto using denv_wf_insert.
eauto using denv_wf_merge.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
simplify_eq/=.
destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
......@@ -424,7 +454,8 @@ Section vcg_spec.
repeat split; eauto.
eapply dun_op_eval_dSome_wf; eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct ms2 as [|t ms2]; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
......@@ -433,6 +464,13 @@ Section vcg_spec.
destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
Qed.
Lemma vcg_sp'_wf E de m m' mNew dv :
......@@ -474,7 +512,8 @@ Section vcg_spec.
rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
+ destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
* destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ".
apply is_dloc_some in Hdloc. simplify_eq/=.
iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv');
iSplit; first done. iFrame. iIntros "Hl".
iExists E, dv', m; repeat (iSplit; first done). iFrame.
......@@ -519,17 +558,20 @@ Section vcg_spec.
vcg_wp_store E dv1 dv2 m Φ -
(l : loc) (w : val),
dval_interp E dv1 = #l
l C w
(l C[LLvl] dval_interp E dv2 - vcg_wp_continuation E Φ (dval_interp E dv2)).
l C w (l C[LLvl] dval_interp E dv2 -
vcg_wp_continuation E Φ (dval_interp E dv2)).
Proof.
iIntros (Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
- apply is_dloc_some in Hdloc; rewrite Hdloc.
destruct (denv_delete_full i m) as [[m' dv_old]|] eqn:Hdel.
+ iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old); iSplit; first done.
+ iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old);
iSplit; first done.
iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
iSpecialize ("Hdel" with "[$Hm]"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
iSpecialize ("Hdel" with "[$Hm]").
iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m');
repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_insert; last done.
by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
rewrite -denv_insert_interp. eauto with iFrame.
......@@ -563,10 +605,12 @@ Section vcg_spec.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
- rewrite IHde //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
iApply (a_load_spec_exists_frac with "[Hawp]").
iApply (awp_wand with "Hawp").
iIntros (v) "H".
iDestruct "H" as (E' dv m' Heq Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done.
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload";
first done.
iDestruct "Hload" as (l q w) "(% & Hl & Hwp)". rewrite Heq.
iExists l, q, w. iSplit; first done. iFrame. iIntros "Hl".
iSpecialize ("Hwp" with "Hl").
......@@ -592,7 +636,8 @@ Section vcg_spec.
iExists l, w. iSplit; first done. iIntros "{$Hl} Hl".
iApply vcg_wp_continuation_mono; last by iApply "H". done.
+ specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; first done. clear Heqsp.
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]";
first done. clear Heqsp.
iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done.
iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? ? ?) "(% & Hm' & H)".
......@@ -615,7 +660,8 @@ Section vcg_spec.
rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp").
iApply (a_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
simplify_eq /=.
rewrite (dval_interp_mono E E' dv2); eauto.
iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H";
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
......@@ -628,7 +674,8 @@ Section vcg_spec.
iRename "Hm'" into "Hde2".
iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)";
simplify_eq /=.
iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H";
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
{ iApply (denv_interp_mono with "HmNew"); eauto. }
......@@ -659,11 +706,48 @@ Section vcg_spec.
intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v1) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl.
iExists Ef, dvf, mf; iSplit; first done. iSplit. iPureIntro. trans Enew ; done.
iExists Ef, dvf, mf; iSplit; first done. iSplit.
iPureIntro. trans Enew ; done.
iSplit; first done.
iFrame. iPureIntro; done. eapply dcexpr_wf_mono in Hwf2.
done. done. by apply denv_wf_unlock.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
- rewrite{1} /vcg_wp; fold vcg_wp.
simpl in Hwf; apply andb_prop_elim in Hwf; destruct 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"). }
iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]".
iClear "Hsp"; clear Heqsp2 Heqsp.
rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp").
iApply (awp_par with "Hm' Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
simplify_eq /=. rewrite (dval_interp_mono E E' dv2); eauto. iNext.
iApply vcg_wp_continuation_mono;
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iExists E', (dPairV dv1 dv2), (denv_merge mNew m'');
repeat (iSplit; try iPureIntro; simpl;
eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge).
iFrame. rewrite (denv_interp_mono E) //.
iApply denv_merge_interp. iFrame.
+ iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp.
rewrite IHde2; [| done | done]. iSpecialize ("Hm'" with "Hwp").
iRename "Hm'" into "Hde2".
iApply (awp_par with "Hde1 Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmNew) Hex !>".
iDestruct "Hex" as (E' dv2 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
simplify_eq /=. rewrite (dval_interp_mono E E' dv1); eauto.
iApply vcg_wp_continuation_mono;
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iExists E', (dPairV dv1 dv2), (denv_merge mNew m'');
repeat (iSplit; try iPureIntro; simpl;
eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge).
iFrame. rewrite (denv_interp_mono E) //.
iApply denv_merge_interp. iFrame.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
Qed.
End vcg_spec.
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