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

add well-foundness as premise for vcg_wp_correct and fix the case for sequence

parent 006364e6
......@@ -4,10 +4,6 @@ From iris_c.c_translation Require Import monad translation proofmode.
Definition known_locs := list loc.
Lemma prefix_trans (E E' E'': known_locs) :
E `prefix_of` E' E' `prefix_of` E'' E `prefix_of` E''.
Proof. intros. eapply PreOrder_Transitive; eauto. Qed.
Inductive dloc :=
| dLoc : nat dloc
| dLocUnknown : loc dloc.
......
......@@ -372,8 +372,9 @@ Section vcg_spec.
Lemma vcg_wp_unknown_correct R E m de Φ :
denv_interp E m -
wp_interp E (vcg_wp_unknown R E de m Φ) -
awp (dcexpr_interp E de) R
(λ v, E' dv m', E `prefix_of` E' dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v
denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
rewrite /vcg_wp_unknown mapsto_wand_list_spec.
iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm").
......@@ -387,7 +388,8 @@ Section vcg_spec.
denv_interp E m -
wp_interp E (vcg_wp_load E dv m (Φ E)) -
(l:loc) q w, dval_interp E dv = #l l C{q} w (l C{q} w -
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w denv_interp E' m' wp_interp E' (Φ E' m' dv')).
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w
denv_interp E' m' wp_interp E' (Φ E' m' dv')).
Proof.
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 /=.
......@@ -410,25 +412,27 @@ Section vcg_spec.
Qed.
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf E de
denv_interp E m -
wp_interp E (vcg_wp E m de R Φ) -
awp (dcexpr_interp E de) R
(λ v, E' dv m', E `prefix_of` E' dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v
denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
revert Φ E m. induction de; intros Φ E m; iIntros "Hm Hwp".
revert Φ E m. induction de; intros Φ E m Hwf; iIntros "Hm Hwp".
- iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; by iFrame.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
- rewrite IHde. iSpecialize ("Hm" with "Hwp"); simpl.
- rewrite IHde; last done. iSpecialize ("Hm" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hm]"). iApply (awp_wand with "Hm").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <-) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload".
iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
iSpecialize ("Hwp" with "Hl"). iDestruct "Hwp" as (Ef dvf mf Hpre' <-) "(Hmf & Hwp)".
iExists Ef, dvf, mf. iSplit. iPureIntro. eapply prefix_trans; done. eauto with iFrame.
iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done.
- admit.
- admit.
- rewrite IHde. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
- 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 & Hwp)".
destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
......@@ -440,20 +444,23 @@ Section vcg_spec.
iExists (dval_interp E' w). iSplit. iPureIntro.
apply dun_op_eval_correct. by rewrite Hop.
iExists E', w, m'; eauto with iFrame.
- rewrite IHde1. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
- rewrite IHde1; last first.
{ simpl in Hwf. apply andb_prop_elim in Hwf. by destruct Hwf. }
iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' Hpre <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
iDestruct "Hex" as (Enew dv m' Hpre <-) "(Hm & Hwp)". simpl.
rewrite denv_unlock_interp.
iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
assert (dcexpr_wf E de2). admit.
(*TODO: fix this by extending statement of the correctness *)
specialize (dcexpr_interp_mono E Enew de2 H0 Hpre).
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
specialize (dcexpr_interp_mono E Enew de2 H1 Hpre).
intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
iExists Ef, dvf, mf. iSplit. iPureIntro. eapply prefix_trans; done. iSplit; first done.
iFrame.
iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
iFrame. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
by eapply dcexpr_wf_mono in Hpre.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
......
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