Commit 0c261f6f authored by Dan Frumin's avatar Dan Frumin

Clean up vcgen.v

parent 0fc880d8
......@@ -7,6 +7,8 @@ From iris_c.c_translation Require Import monad translation proofmode.
Section vcg.
Context `{amonadG Σ}.
(** `mapsto_wand_list E [l1:=v1,l2:=v2,...ln:=vn] Φ`
= `l1 ↦C v1 -∗ l2 ↦C v2 -∗ ... -∗ ln ↦C vn -∗ Φ` *)
Fixpoint mapsto_wand_list_aux
(E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
match m with
......@@ -29,6 +31,7 @@ Section vcg.
end.
Global Arguments popstack !_ /.
(** Evaluation of simple expressions *)
Fixpoint vcg_eval_dexpr (de : dexpr) : option dval :=
match de with
| dEVal dv => Some dv
......@@ -51,6 +54,9 @@ Section vcg.
| dEUnknown _ => None
end.
(** Computes the framing for the resources, necessary for the safety of the
expression, and simulatenously computes the strongest postcondition based on that.
See `vcg_sp_correct` and `vcg_sp'_correct`. *)
Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
: option (list denv * denv * dval) :=
match de with
......@@ -441,7 +447,7 @@ Section vcg_spec.
iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
iIntros "Hl". iSplit; eauto.
rewrite -denv_insert_interp. by iFrame.
- specialize (IHde1 ms).
- specialize (IHde1 ms).
destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
specialize (IHde2 ms1).
......@@ -697,19 +703,19 @@ Section vcg_spec.
cl C{q} w (cl C{q} w - vcg_wp_continuation E Φ w).
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 /=.
* destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
- destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
+ destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ".
apply is_dloc_Some in Hdloc. simplify_eq/=.
iExists (dloc_interp E (dLoc i 0)), q, (dval_interp E dv');
iSplit; first done. iFrame. iIntros "Hl".
iExists E, dv', m; repeat (iSplit; first done). iFrame.
rewrite Hm0. eapply denv_lookup_wf in Hlkp; eauto with iFrame.
* rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"). simpl.
iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_Some in Hdloc. subst.
iExists (dloc_interp E (dLoc i 0)), q, v'; iSplit; first done. iFrame.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
- rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
iExists l, q, v'. iSplit; first done. iFrame.
......@@ -726,11 +732,11 @@ Section vcg_spec.
Proof.
iIntros (Hwf Hwf2) "Hm Hwp". rewrite /vcg_wp_un_op.
destruct (dun_op_eval E b dv) as [dw|] eqn:Hbin.
* iExists (dval_interp E dw); iSplit.
- iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dun_op_eval_correct. by rewrite Hbin. }
iExists E, dw, m.
apply dun_op_eval_Some_wf in Hbin; try done. eauto with iFrame.
* rewrite mapsto_wand_list_spec.
- rewrite mapsto_wand_list_spec.
iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Qed.
......@@ -746,12 +752,12 @@ Section vcg_spec.
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dcbin_op_eval E b dv1 dv2) as [dw|] eqn:Hbin.
* iExists (dval_interp E dw); iSplit.
- iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
apply dcbin_op_eval_Some_wf in Hbin; try done.
rewrite -denv_merge_interp //. eauto with iFrame.
* iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
- iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
rewrite mapsto_wand_list_spec.
iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Qed.
......@@ -991,7 +997,7 @@ 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 IHde //. 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.
......@@ -1051,13 +1057,13 @@ Section vcg_spec.
iApply denv_merge_interp. iFrame.
- simpl. rewrite IHde //. 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.
rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm'").
simplify_eq /=. iExists R. iFrame.
iApply (awp_wand with "Hwp"). iIntros (v) "Hc Hr".
rewrite (vcg_wp_continuation_mono E) //.
iFrame.
iDestruct "Hf" as (E' dv1 m' Heq Hpre Hm'wf) "(% & Hm' & Hwp)".
unfold vcg_wp_awp_continuation.
rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm'").
simplify_eq /=. iExists R. iFrame.
iApply (awp_wand with "Hwp"). iIntros (v) "Hc Hr".
rewrite (vcg_wp_continuation_mono E) //.
iFrame.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
Qed.
End vcg_spec.
......
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