From 4193161c07fdc6e14605e03ffe95a15e01304891 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Gondelman?= Date: Thu, 4 Oct 2018 18:14:47 +0200 Subject: [PATCH] vcgen and dcexpr correctness fixed (vcg_solver remains) --- theories/vcgen/dcexpr.v | 16 ++-- theories/vcgen/vcgen.v | 190 +++++++++++++++++++++++++--------------- 2 files changed, 128 insertions(+), 78 deletions(-) diff --git a/theories/vcgen/dcexpr.v b/theories/vcgen/dcexpr.v index 270c93f..7c533e5 100644 --- a/theories/vcgen/dcexpr.v +++ b/theories/vcgen/dcexpr.v @@ -383,11 +383,17 @@ Qed. Global Instance dcexpr_closed X E de : dcexpr_wf X E de → - Closed X (cdexpr_interp E de). -Proof. Admitted. -(* induction de; simpl; try solve_closed. rewrite /Closed /=. - split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d). -Qed. *) + Closed X (dcexpr_interp E de). +Proof. + revert X. induction de; intros; unfold Closed in *; simplify_eq /=; + try (destruct_and!; split_and; first split_and; [ apply is_closed_of_val | by apply IHde2 | by apply IHde1]); + 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 *) (** ** LocLookup *) diff --git a/theories/vcgen/vcgen.v b/theories/vcgen/vcgen.v index fbd28ea..ee9b11a 100644 --- a/theories/vcgen/vcgen.v +++ b/theories/vcgen/vcgen.v @@ -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 | dCSeq de1 de2, S p => 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 => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => @@ -724,14 +724,12 @@ Section vcg_spec. (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew). Proof. iIntros (Hsp Hwf) "Hm". - iPoseProof vcg_sp_correct' as "Hawp"; first eassumption. - pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. + iPoseProof vcg_sp_correct' as "Hawp"; first eassumption; first done. + pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen; assert (∃ m', ms = [m']) as [m' ->]=>/=. { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. } - { done. } - Admitted. - (* rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]". - Qed.*) + rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]". + Qed. Lemma vcg_sp'_correct E de m m' mNew dv R : vcg_sp' E m de = Some (m', mNew, dv) → @@ -748,24 +746,41 @@ Section vcg_spec. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen); simplify_eq. rewrite vcg_sp_correct; last eassumption; simplify_eq; last done. simpl. - rewrite denv_merge_nil_r. iFrame. eauto 422 with iFrame. simplify_option_eq. - Admitted. + rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=. + by iFrame. + Qed. Lemma vcg_sp_wf' E de ms ms' mNew dv n: Forall (denv_wf E) ms → - dcexpr_wf E de → + dcexpr_wf [] E de → vcg_sp E ms de n = Some (ms', mNew, dv) → Forall (denv_wf E) ms' ∧ denv_wf E mNew ∧ dval_wf E dv . - Proof. Admitted. -(* revert ms ms' mNew dv. induction de; - intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto. - - simplify_option_eq. split_and?; auto; first by destruct E. - by eapply vcg_eval_dexpr_wf. + Proof. + revert de ms ms' mNew dv. induction n as [|n IH]; + intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto. + { destruct de; simplify_option_eq. split_and?; auto; first by destruct E. + 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 (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; 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 (?&?&?). + destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?). eapply denv_wf_delete_frac_2 in Hout1; eauto. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert. @@ -777,8 +792,8 @@ Section vcg_spec. 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 (?&?&?). + destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). + destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). eapply denv_wf_delete_full_2 in Hout1; try eassumption. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert. @@ -789,8 +804,8 @@ Section vcg_spec. simplify_eq/=. destruct (dcbin_op_eval E c 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). - destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). + destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). + destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). repeat split; eauto. apply denv_wf_merge; eauto. eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; @@ -802,8 +817,8 @@ Section vcg_spec. as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. - destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). - destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). + destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). + destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). eapply denv_wf_delete_full_2 in Hout1; try eassumption. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert, denv_wf_merge. @@ -811,7 +826,7 @@ Section vcg_spec. eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto. by eapply denv_wf_merge. - 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/=. repeat split; eauto. eapply dun_op_eval_Some_wf; eauto. @@ -820,36 +835,37 @@ Section vcg_spec. 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). + destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2. { 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. 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 (?&?&?). + destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). + destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). repeat split; eauto. apply denv_wf_merge; eauto. - Qed. *) + Qed. Lemma vcg_sp'_wf E de m m' mNew dv : denv_wf E m → - dcexpr_wf E de → + dcexpr_wf [] E de → vcg_sp' E m de = Some (m', mNew, dv) → - denv_wf E m' ∧ denv_wf E mNew ∧ dval_wf E dv . - Proof. Admitted. -(* rewrite /vcg_sp'. intros Hm Hde Hsp'. + denv_wf E m' ∧ denv_wf E mNew ∧ dval_wf E dv. + Proof. + rewrite /vcg_sp'. intros Hm Hde Hsp'. 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 ms as [|?m' ms]; simplify_eq/=. - pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen. - assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen). - destruct (vcg_sp_wf' E de [m] [m'] mNew _ Hms Hde Hsp) as (Hm'&?&?). + destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq. + destruct ms as [|?m' ms]; simplify_eq. + pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. + assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen). simpl in Hsp'. + inversion Hsp'. subst. + destruct (vcg_sp_wf' E de [m] [m'] mNew _ _ Hms Hde Hsp) as (Hm'&?&?). repeat split; eauto. by inversion Hm'. - Qed. *) + Qed. Lemma vcg_wp_awp_continuation_correct R E m de Φ : denv_wf E m → @@ -1008,47 +1024,75 @@ Section vcg_spec. iSplit. iPureIntro. by trans E'. eauto with iFrame. Qed. - Lemma vcg_wp_correct R E m de Φ : - dcexpr_wf E de → + Lemma vcg_wp_correct R E m de Φ n: + dcexpr_wf [] E de → denv_wf 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 Φ). Proof. - Admitted. (* - revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp". + revert de Φ E m. induction n as [|n IH]; intros de Φ 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. + 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"). + - 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]. 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. + iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done. 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). iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". rewrite (dval_interp_mono E E') //. rewrite /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'". 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Φ". + 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. + try done. clear Heqsp. + iDestruct (IH de2 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 /vcg_wp_alloc mapsto_wand_list_spec. iCombine "HmNew Hm'" as "Hm'". rewrite (denv_interp_mono E E') // denv_merge_interp. 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Φ". - - rewrite IHde //. iRename "Hm" into "Hawp". + - rewrite (IH de) //. iRename "Hm" into "Hawp". iSpecialize ("Hawp" with "Hwp"); simpl. iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp"). @@ -1068,9 +1112,9 @@ Section vcg_spec. + 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. + iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done. 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). iDestruct 1 as (E' dw m'' ? Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". rewrite (dval_interp_mono E E') //. subst v1. @@ -1082,8 +1126,8 @@ Section vcg_spec. 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 (IHde2 with "Hm' Hwp") as "Hde2"; try done. + try done. clear Heqsp. + iDestruct (IH de2 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)". rewrite (dval_interp_mono E E') //. subst v2. @@ -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 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. + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done. 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"). + rewrite (IH de1); [| 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)"; @@ -1112,10 +1156,10 @@ Section vcg_spec. eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. { iApply (denv_interp_mono with "HmNew"); eauto. } 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 (?&?&?). 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". iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "(-> & HmNew) Hex". @@ -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 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. + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done. 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"). + rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iApply (a_pre_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)"; @@ -1149,10 +1193,10 @@ Section vcg_spec. iExists l, v, w. iFrame. repeat iSplit; eauto. * iPureIntro. rewrite (dval_interp_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 (?&?&?). 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". iApply (a_pre_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "(-> & HmNew) Hex $". @@ -1167,19 +1211,19 @@ Section vcg_spec. iExists l, v, w. iFrame. repeat iSplit; eauto. * iPureIntro. rewrite (dval_interp_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". iDestruct "Hex" as (E' dv m' -> Hpre' Hm'wf) "(% & Hm & Hwp)". iDestruct (vcg_wp_un_op_correct with "Hm Hwp") as (w ?) "Hcont"; auto. iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono. - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. - rewrite IHde1 //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. - iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. + rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. + iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. by apply dcexpr_closed. iNext. iApply (awp_wand with "Hm"). iIntros (v) "Hex". iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl. rewrite denv_unlock_interp. - iModIntro. rewrite IHde2 //. iSpecialize ("Hm" with "Hwp"). - specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre'). + iModIntro. rewrite (IH de2) //. iSpecialize ("Hm" with "Hwp"). + specialize (dcexpr_interp_mono [] E Enew de2 Hwf2 Hpre'). 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. @@ -1193,11 +1237,11 @@ Section vcg_spec. 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. + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done. 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"). + rewrite (IH de1); [| 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)"; @@ -1209,10 +1253,10 @@ Section vcg_spec. 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. + + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption. done. 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"). + rewrite (IH de2); [| 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 !>". @@ -1225,7 +1269,7 @@ Section vcg_spec. eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge). iFrame. rewrite (denv_interp_mono E) //. iApply denv_merge_interp. iFrame. - - simpl. rewrite IHde //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. + - simpl. rewrite (IH de) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. iApply (a_invoke_spec with "Hm"). iIntros (arg) "Hf !> HR". iDestruct "Hf" as (E' dv1 m' Heq Hpre Hm'wf) "(% & Hm' & Hwp)". unfold vcg_wp_awp_continuation. @@ -1235,7 +1279,7 @@ Section vcg_spec. rewrite (vcg_wp_continuation_mono E) //. iFrame. - by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). - Qed.*) + Qed. End vcg_spec. Arguments vcg_wp_awp_continuation _ _ _ _ _ _ _ /. -- GitLab