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

finished the binop case for vcg_wp correctness

parent aa42c811
......@@ -425,7 +425,31 @@ Section vcg_spec.
iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp, denv_wf. eauto.
Qed.
Lemma vcg_wp_correct R E m de Φ :
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
E0 `prefix_of` E
denv_wf E (denv_merge mOut m)
denv_interp E m -
wp_interp E (vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E)) -
denv_interp E mOut -
w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
( E' dv m', E0 `prefix_of` E' dval_interp E' dv = w
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
iIntros (Hpre Hwf) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
rewrite -denv_merge_interp. repeat (iSplit; first done); iFrame.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw1); iSplit.
iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
iExists E, dw1, (denv_merge mOut m).
rewrite -denv_merge_interp. repeat (iSplit; first done). iFrame.
Qed.
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf E de
denv_wf E m
denv_interp E m -
......@@ -449,37 +473,35 @@ Section vcg_spec.
iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done. done.
- admit.
- 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 [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
+ destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
{ by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (H1 & H2 & Hwf).
iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde2]"; iClear "Hsp"; clear Heqsp2 Heqsp.
rewrite IHde1; [| done |]. iSpecialize ("HmIn" with "Hwp").
rewrite IHde1; [| done | done]. iSpecialize ("HmIn" with "Hwp").
iApply (a_bin_op_spec with "[$HmIn] [$Hde2]"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmOut)".
iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E' b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* iExists (dval_interp E' dw); iSplit.
{ iPureIntro.
rewrite (dval_interp_mono _ _ _ Hwf Hpre).
apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E', dw, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_merge. by eapply denv_wf_mono; done. done.
iApply (denv_interp_mono with "HmOut"); done.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E' dw1); iSplit.
{ iPureIntro. rewrite (dval_interp_mono _ _ _ Hwf Hpre).
apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E', dw1, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_merge. by eapply denv_wf_mono; done. done.
iApply (denv_interp_mono with "HmOut"); done.
* done.
+ admit.
specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
+ iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (H1 & H2 & Hwf).
iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde1]"; iClear "Hsp"; clear Heqsp.
rewrite IHde2; [| done | done]. iSpecialize ("HmIn" with "Hwp").
iRename "HmIn" into "Hde2".
iApply (a_bin_op_spec with "[$Hde1] [$Hde2]"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmOut) Hex".
iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
- rewrite IHde; last done. 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)".
......
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