Commit 4193161c authored by Léon Gondelman 's avatar Léon Gondelman

vcgen and dcexpr correctness fixed (vcg_solver remains)

parent d3b68845
...@@ -383,11 +383,17 @@ Qed. ...@@ -383,11 +383,17 @@ Qed.
Global Instance dcexpr_closed X E de : Global Instance dcexpr_closed X E de :
dcexpr_wf X E de dcexpr_wf X E de
Closed X (cdexpr_interp E de). Closed X (dcexpr_interp E de).
Proof. Admitted. Proof.
(* induction de; simpl; try solve_closed. rewrite /Closed /=. revert X. induction de; intros; unfold Closed in *; simplify_eq /=;
split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d). try (destruct_and!; split_and; first split_and; [ apply is_closed_of_val | by apply IHde2 | by apply IHde1]);
Qed. *) try (destruct_and!; split_and; first split_and; [ apply is_closed_of_val | by apply IHde1 | by apply IHde2]).
- split_and; eauto using is_closed_of_val. by apply dexpr_closed.
- split_and; [ apply is_closed_of_val | by apply IHde].
- split_and; [ apply is_closed_of_val | by apply IHde].
- split_and; first split_and; [ apply is_closed_of_val | apply is_closed_of_val | by apply IHde].
- by apply W.is_closed_correct.
Qed.
(** * Reification of C syntax *) (** * Reification of C syntax *)
(** ** LocLookup *) (** ** LocLookup *)
......
...@@ -332,7 +332,7 @@ Section vcg. ...@@ -332,7 +332,7 @@ Section vcg.
| dCUnOp op de, S p => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ) p | dCUnOp op de, S p => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ) p
| dCSeq de1 de2, S p => | dCSeq de1 de2, S p =>
vcg_wp E m de1 R (λ E m _, vcg_wp E m de1 R (λ E m _,
U (vcg_wp E (denv_unlock m) de2 R Φ p)) p U (vcg_wp E (denv_unlock m) de2 R Φ p)) p
| dCPar de1 de2, S p => | dCPar de1 de2, S p =>
match vcg_sp' E m de1 with match vcg_sp' E m de1 with
| Some (m', mNew, dv1) => | Some (m', mNew, dv1) =>
...@@ -724,14 +724,12 @@ Section vcg_spec. ...@@ -724,14 +724,12 @@ Section vcg_spec.
(λ v, v = dval_interp E dv denv_interp E mNew). (λ v, v = dval_interp E dv denv_interp E mNew).
Proof. Proof.
iIntros (Hsp Hwf) "Hm". iIntros (Hsp Hwf) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; first eassumption. iPoseProof vcg_sp_correct' as "Hawp"; first eassumption; first done.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen;
assert ( m', ms = [m']) as [m' ->]=>/=. assert ( m', ms = [m']) as [m' ->]=>/=.
{ destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. } { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
{ done. } rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
Admitted. Qed.
(* rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
Qed.*)
Lemma vcg_sp'_correct E de m m' mNew dv R : Lemma vcg_sp'_correct E de m m' mNew dv R :
vcg_sp' E m de = Some (m', mNew, dv) vcg_sp' E m de = Some (m', mNew, dv)
...@@ -748,24 +746,41 @@ Section vcg_spec. ...@@ -748,24 +746,41 @@ Section vcg_spec.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen); simplify_eq. assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen); simplify_eq.
rewrite vcg_sp_correct; last eassumption; simplify_eq; last done. simpl. rewrite vcg_sp_correct; last eassumption; simplify_eq; last done. simpl.
rewrite denv_merge_nil_r. iFrame. eauto 422 with iFrame. simplify_option_eq. rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=.
Admitted. by iFrame.
Qed.
Lemma vcg_sp_wf' E de ms ms' mNew dv n: Lemma vcg_sp_wf' E de ms ms' mNew dv n:
Forall (denv_wf E) ms Forall (denv_wf E) ms
dcexpr_wf E de dcexpr_wf [] E de
vcg_sp E ms de n = Some (ms', mNew, dv) vcg_sp E ms de n = Some (ms', mNew, dv)
Forall (denv_wf E) ms' denv_wf E mNew dval_wf E dv . Forall (denv_wf E) ms' denv_wf E mNew dval_wf E dv .
Proof. Admitted. Proof.
(* revert ms ms' mNew dv. induction de; revert de ms ms' mNew dv. induction n as [|n IH];
intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto. intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
- simplify_option_eq. split_and?; auto; first by destruct E. { destruct de; simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf. by eapply vcg_eval_dexpr_wf. }
destruct de; simplify_eq /=.
- simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 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 (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
assert (Forall (denv_wf E) (mNew1 :: ms1)) as Hwfms2.
{ apply Forall_cons. split; eauto. }
assert (dcexpr_wf [] E (dce_subst E s dv1 de2)) as Hwfsubst.
by apply dce_subst_dcexpr_wf.
destruct (IH (dce_subst E s dv1 de2) _ _ _ _ Hwfms2 Hwfsubst Hsp2) as (Hall&?&?).
apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1) destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=. as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?). destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
eapply denv_wf_delete_frac_2 in Hout1; eauto. eapply denv_wf_delete_frac_2 in Hout1; eauto.
destruct Hout1 as (?&?&?). destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert. repeat split; eauto using denv_wf_insert.
...@@ -777,8 +792,8 @@ Section vcg_spec. ...@@ -777,8 +792,8 @@ Section vcg_spec.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
eapply denv_wf_delete_full_2 in Hout1; try eassumption. eapply denv_wf_delete_full_2 in Hout1; try eassumption.
destruct Hout1 as (?&?&?). destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert. repeat split; eauto using denv_wf_insert.
...@@ -789,8 +804,8 @@ Section vcg_spec. ...@@ -789,8 +804,8 @@ Section vcg_spec.
simplify_eq/=. simplify_eq/=.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto. repeat split; eauto. apply denv_wf_merge; eauto.
eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto. eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
...@@ -802,8 +817,8 @@ Section vcg_spec. ...@@ -802,8 +817,8 @@ Section vcg_spec.
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
eapply denv_wf_delete_full_2 in Hout1; try eassumption. eapply denv_wf_delete_full_2 in Hout1; try eassumption.
destruct Hout1 as (?&?&?). destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert, denv_wf_merge. repeat split; eauto using denv_wf_insert, denv_wf_merge.
...@@ -811,7 +826,7 @@ Section vcg_spec. ...@@ -811,7 +826,7 @@ Section vcg_spec.
eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto. eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
by eapply denv_wf_merge. by eapply denv_wf_merge.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=. destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
repeat split; eauto. repeat split; eauto.
eapply dun_op_eval_Some_wf; eauto. eapply dun_op_eval_Some_wf; eauto.
...@@ -820,36 +835,37 @@ Section vcg_spec. ...@@ -820,36 +835,37 @@ Section vcg_spec.
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct ms2 as [|t ms2]; simplify_eq/=. destruct ms2 as [|t ms2]; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2. assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2.
{ apply Forall_cons. split; eauto. by apply denv_wf_unlock. } { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?). destruct (IH de2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
apply Forall_cons in Hall. destruct Hall. apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge. 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 ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
simplify_eq/=. simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto. repeat split; eauto. apply denv_wf_merge; eauto.
Qed. *) Qed.
Lemma vcg_sp'_wf E de m m' mNew dv : Lemma vcg_sp'_wf E de m m' mNew dv :
denv_wf E m denv_wf E m
dcexpr_wf E de dcexpr_wf [] E de
vcg_sp' E m de = Some (m', mNew, dv) vcg_sp' E m de = Some (m', mNew, dv)
denv_wf E m' denv_wf E mNew dval_wf E dv . denv_wf E m' denv_wf E mNew dval_wf E dv.
Proof. Admitted. Proof.
(* rewrite /vcg_sp'. intros Hm Hde Hsp'. rewrite /vcg_sp'. intros Hm Hde Hsp'.
assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto). assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto).
destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=. destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq.
destruct ms as [|?m' ms]; simplify_eq/=. destruct ms as [|?m' ms]; simplify_eq.
pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen). assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen). simpl in Hsp'.
destruct (vcg_sp_wf' E de [m] [m'] mNew _ Hms Hde Hsp) as (Hm'&?&?). inversion Hsp'. subst.
destruct (vcg_sp_wf' E de [m] [m'] mNew _ _ Hms Hde Hsp) as (Hm'&?&?).
repeat split; eauto. by inversion Hm'. repeat split; eauto. by inversion Hm'.
Qed. *) Qed.
Lemma vcg_wp_awp_continuation_correct R E m de Φ : Lemma vcg_wp_awp_continuation_correct R E m de Φ :
denv_wf E m denv_wf E m
...@@ -1008,47 +1024,75 @@ Section vcg_spec. ...@@ -1008,47 +1024,75 @@ Section vcg_spec.
iSplit. iPureIntro. by trans E'. eauto with iFrame. iSplit. iPureIntro. by trans E'. eauto with iFrame.
Qed. Qed.
Lemma vcg_wp_correct R E m de Φ : Lemma vcg_wp_correct R E m de Φ n:
dcexpr_wf E de dcexpr_wf [] E de
denv_wf E m denv_wf E m
denv_interp E m - denv_interp E m -
vcg_wp E m de R Φ 1024 (*TODO: Fix this *) - vcg_wp E m de R Φ n -
awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ). awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
Proof. Proof.
Admitted. (* revert de Φ E m. induction n as [|n IH]; intros de Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp". { simpl; case_match; eauto with iFrame.
simpl. case_match.
+ iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
iIntros (? ->). iExists E,_,m. repeat iSplit; eauto with iFrame.
iPureIntro. by eapply vcg_eval_dexpr_wf.
+ by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
destruct de; eauto with iFrame.
- simpl. case_match. - simpl. case_match.
+ iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct. + iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
iIntros (? ->). iExists E,_,m. repeat iSplit; eauto with iFrame. iIntros (? ->). iExists E,_,m. repeat iSplit; eauto with iFrame.
iPureIntro. by eapply vcg_eval_dexpr_wf. iPureIntro. by eapply vcg_eval_dexpr_wf.
+ by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). + by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
- simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
assert (Closed [s] (dcexpr_interp E de2)).
{ by apply dcexpr_closed. }
iApply (awp_bind with "[Hm]"); fold dcexpr_interp.
{ exists (λ: s, dcexpr_interp E de2)%V. by unlock. }
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
awp_let.
iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)".
assert (dcexpr_wf [] Enew (dce_subst Enew s dv de2)) as Hwfs.
{ apply dce_subst_dcexpr_wf; first done. by eapply dcexpr_wf_mono. }
rewrite (IH (dce_subst Enew s dv de2)) //.
iSpecialize ("Hm" with "Hwp").
rewrite (dcexpr_interp_mono _ E Enew _ Hwf2 Hpre').
rewrite Hpre -dce_subst_subst_comm.
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.
iSplit; first done.
iFrame. iPureIntro; done.
- simpl in *. apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. - 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 de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first.
+ destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; 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"). } { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; first done. iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done.
clear Heqsp2 Heqsp. clear Heqsp2 Heqsp.
iDestruct (IHde1 with "Hm' Hwp") as "Hde1"; try done. iDestruct (IH de1 with "Hm' Hwp") as "Hde1"; try done.
iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]".
rewrite (dval_interp_mono E E') //. rewrite (dval_interp_mono E E') //.
rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'". rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'".
rewrite (denv_interp_mono E E') // denv_merge_interp. rewrite (denv_interp_mono E E') // denv_merge_interp.
iDestruct ("H" with "Hm'") as (n ->) "HΦ". iExists n; iSplit; first done. iDestruct ("H" with "Hm'") as (n' ->) "HΦ". iExists n'; iSplit; first done.
iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ". iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
+ specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]";
first done. clear Heqsp. try done. clear Heqsp.
iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done. iDestruct (IH de2 with "Hm' Hwp") as "Hde2"; try done.
iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 -> ???) "[Hm' H]". iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 -> ???) "[Hm' H]".
rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'". rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'".
rewrite (denv_interp_mono E E') // denv_merge_interp. rewrite (denv_interp_mono E E') // denv_merge_interp.
rewrite !(dval_interp_mono E E') // . rewrite !(dval_interp_mono E E') // .
iDestruct ("H" with "Hm'") as (n ->) "HΦ". iExists n; iSplit; first done. iDestruct ("H" with "Hm'") as (n' ->) "HΦ". iExists n'; iSplit; first done.
iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ". iIntros (l) "Hl". by iApply vcg_wp_continuation_mono; last by iApply "HΦ".
- rewrite IHde //. iRename "Hm" into "Hawp". - rewrite (IH de) //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl. iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (a_load_spec_exists_frac with "[Hawp]").
iApply (awp_wand with "Hawp"). iApply (awp_wand with "Hawp").
...@@ -1068,9 +1112,9 @@ Section vcg_spec. ...@@ -1068,9 +1112,9 @@ Section vcg_spec.
+ destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; 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"). } { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; first done. iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done.
clear Heqsp2 Heqsp. clear Heqsp2 Heqsp.
iDestruct (IHde1 with "Hm' Hwp") as "Hde1"; try done. iDestruct (IH de1 with "Hm' Hwp") as "Hde1"; try done.
iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iDestruct 1 as (E' dw m'' ? Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". iDestruct 1 as (E' dw m'' ? Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]".
rewrite (dval_interp_mono E E') //. subst v1. rewrite (dval_interp_mono E E') //. subst v1.
...@@ -1082,8 +1126,8 @@ Section vcg_spec. ...@@ -1082,8 +1126,8 @@ Section vcg_spec.
iApply vcg_wp_continuation_mono; last by iApply "H". done. iApply vcg_wp_continuation_mono; last by iApply "H". done.
+ specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]";
first done. clear Heqsp. try done. clear Heqsp.
iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done. iDestruct (IH de2 with "Hm' Hwp") as "Hde2"; try done.
iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? ? ?) "(% & Hm' & H)". iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? ? ?) "(% & Hm' & H)".
rewrite (dval_interp_mono E E') //. subst v2. rewrite (dval_interp_mono E E') //. subst v2.
...@@ -1098,11 +1142,11 @@ Section vcg_spec. ...@@ -1098,11 +1142,11 @@ Section vcg_spec.
destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. 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. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first.
{ by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]". iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]".
iClear "Hsp"; clear Heqsp2 Heqsp. iClear "Hsp"; clear Heqsp2 Heqsp.
rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp"). rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp").
iApply (a_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp. iApply (a_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmNew)". iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
...@@ -1112,10 +1156,10 @@ Section vcg_spec. ...@@ -1112,10 +1156,10 @@ Section vcg_spec.
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
{ iApply (denv_interp_mono with "HmNew"); eauto. } { iApply (denv_interp_mono with "HmNew"); eauto. }
iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono. iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono.
+ iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp. iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp.
rewrite IHde2; [| done | done]. iSpecialize ("Hm'" with "Hwp"). rewrite (IH de2); [| done | done]. iSpecialize ("Hm'" with "Hwp").
iRename "Hm'" into "Hde2". iRename "Hm'" into "Hde2".
iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmNew) Hex". iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
...@@ -1131,11 +1175,11 @@ Section vcg_spec. ...@@ -1131,11 +1175,11 @@ Section vcg_spec.
destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. 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. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first.
{ by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]". iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]".
iClear "Hsp"; clear Heqsp2 Heqsp. iClear "Hsp"; clear Heqsp2 Heqsp.
rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp"). rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp").
iApply (a_pre_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp. iApply (a_pre_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmNew) $". iNext. iIntros (v1 v2) "Hex (-> & HmNew) $".
iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
...@@ -1149,10 +1193,10 @@ Section vcg_spec. ...@@ -1149,10 +1193,10 @@ Section vcg_spec.
iExists l, v, w. iFrame. repeat iSplit; eauto. iExists l, v, w. iFrame. repeat iSplit; eauto.
* iPureIntro. rewrite (dval_interp_mono E E'); auto. * iPureIntro. rewrite (dval_interp_mono E E'); auto.
* rewrite (vcg_wp_continuation_mono E E'); auto. * rewrite (vcg_wp_continuation_mono E E'); auto.
+ iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp. iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp.
rewrite IHde2; [| done | done]. iSpecialize ("Hm'" with "Hwp"). rewrite (IH de2); [| done | done]. iSpecialize ("Hm'" with "Hwp").
iRename "Hm'" into "Hde2". iRename "Hm'" into "Hde2".
iApply (a_pre_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iApply (a_pre_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmNew) Hex $". iNext. iIntros (v1 v2) "(-> & HmNew) Hex $".
...@@ -1167,19 +1211,19 @@ Section vcg_spec. ...@@ -1167,19 +1211,19 @@ Section vcg_spec.
iExists l, v, w. iFrame. repeat iSplit; eauto. iExists l, v, w. iFrame. repeat iSplit; eauto.
* iPureIntro. rewrite (dval_interp_mono E E'); auto. * iPureIntro. rewrite (dval_interp_mono E E'); auto.
* rewrite (vcg_wp_continuation_mono E E'); auto. * rewrite (vcg_wp_continuation_mono E E'); auto.
- rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp"). - rewrite (IH de) //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex". iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (E' dv m' -> Hpre' Hm'wf) "(% & Hm & Hwp)". iDestruct "Hex" as (E' dv m' -> Hpre' Hm'wf) "(% & Hm & Hwp)".
iDestruct (vcg_wp_un_op_correct with "Hm Hwp") as (w ?) "Hcont"; auto. iDestruct (vcg_wp_un_op_correct with "Hm Hwp") as (w ?) "Hcont"; auto.
iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono. iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono.
- simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
rewrite IHde1 //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. by apply dcexpr_closed.
iNext. iApply (awp_wand with "Hm"). iIntros (v) "Hex". iNext. iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl. iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl.
rewrite denv_unlock_interp. rewrite denv_unlock_interp.
iModIntro. rewrite IHde2 //. iSpecialize ("Hm" with "Hwp"). iModIntro. rewrite (IH de2) //. iSpecialize ("Hm" with "Hwp").
specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre'). specialize (dcexpr_interp_mono [] E Enew de2 Hwf2 Hpre').
intro Heq; rewrite Heq. iApply (awp_wand with "Hm"). intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v1) "Hex". iIntros (v1) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl. iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl.
...@@ -1193,11 +1237,11 @@ Section vcg_spec. ...@@ -1193,11 +1237,11 @@ Section vcg_spec.
destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first.