Commit 062b5533 authored by Dan Frumin's avatar Dan Frumin
Browse files

Specifications for `vcg_eval_dexpr`.

- Well-formedness and correctness for `vcg_eval_dexpr`
- Get rid of admits in vcgen
parent 1ea712e8
......@@ -37,7 +37,7 @@ Section denv.
| None :: m' => denv_wf_val E m'
end.
Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool :=
Fixpoint denv_wf_len (E: known_locs) (m: denv) {struct m} : bool :=
match E, m with
| _, [] => true
| _ :: E', _ :: m' => denv_wf_len E' m'
......
......@@ -372,6 +372,46 @@ Section vcg_spec.
transitivity (length ms1); eauto.
Qed.
Lemma vcg_eval_dexpr_correct E de dv :
vcg_eval_dexpr de = Some dv
WP dexpr_interp E de {{ v, v = dval_interp E dv }}%I.
Proof.
generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=.
- by iApply wp_value.
- simplify_option_eq.
wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1.
iIntros (? ->).
wp_bind (dexpr_interp E de2). iApply wp_wand; first by iApply IHde2.
iIntros (? ->).
by iApply wp_value.
- destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
destruct dv'; simplify_eq/=.
wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde.
iIntros (? ->). simpl. by wp_proj.
- destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
destruct dv'; simplify_eq/=.
wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde.
iIntros (? ->). simpl. by wp_proj.
Qed.
Lemma vcg_eval_dexpr_wf E de dv :
vcg_eval_dexpr de = Some dv
dexpr_wf E de dval_wf E dv.
Proof.
generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=; eauto.
- simplify_option_eq. naive_solver.
- destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
destruct dv'; simplify_eq/=. intros Hwfde.
specialize (IHde (dPairV dv dv'2) eq_refl Hwfde).
(* THIS IS UGLY AF ^ *) simpl in IHde.
destruct_and!. auto.
- destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
destruct dv'; simplify_eq/=. intros Hwfde.
specialize (IHde (dPairV dv'1 dv) eq_refl Hwfde).
(* THIS IS UGLY AF ^ *) simpl in IHde.
destruct_and!. auto.
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
......@@ -380,8 +420,10 @@ Section vcg_spec.
Proof.
revert ms ms' mNew dv. induction de;
iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
- (* iFrame. iApply denv_stack_interp_intro.
iApply awp_ret. wp_value_head. iSplit; eauto. rewrite /denv_interp //. *) admit.
- simplify_option_eq.
iApply denv_stack_interp_intro.
iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
- specialize (IHde ms).
destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
......@@ -500,7 +542,7 @@ Section vcg_spec.
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
simplify_eq/=; iSplit; eauto.
rewrite -denv_merge_interp. iFrame.
Admitted.
Qed.
Lemma vcg_sp_correct E de m ms mNew dv R :
vcg_sp E [m] de = Some (ms, mNew, dv)
......@@ -542,7 +584,8 @@ Section vcg_spec.
Proof.
revert ms ms' mNew dv. induction de;
intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
- simplify_option_eq. split_and?; auto. by destruct E. admit.
- simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf.
- 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)
......@@ -615,7 +658,7 @@ Section vcg_spec.
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
Admitted.
Qed.
Lemma vcg_sp'_wf E de m m' mNew dv :
denv_wf E m
......@@ -798,8 +841,11 @@ Section vcg_spec.
awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
Proof.
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. *) admit.
- 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 *. 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.
......@@ -1013,7 +1059,7 @@ Section vcg_spec.
rewrite (vcg_wp_continuation_mono E) //.
iFrame.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
Admitted.
Qed.
End vcg_spec.
Arguments vcg_wp_awp_continuation _ _ _ _ _ _ _ /.
......
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