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

wip

parent 0f2dec86
......@@ -548,17 +548,17 @@ Section vcg_spec.
Proof.
revert de ms ms' mNew dv. induction n as [|n IH].
(* Base Case *)
- iIntros (de ms ms' mNew dv Hsp Hwf); simplify_eq/=.
{ iIntros (de ms ms' mNew dv Hsp Hwf); simplify_eq/=.
destruct de; 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 //.
- iIntros (de ms ms' mNew dv Hsp Hwf).
iIntros (? ->). iSplit; eauto. rewrite /denv_interp //. }
{ iIntros (de ms ms' mNew dv Hsp Hwf).
destruct de; simplify_option_eq.
+ iApply denv_stack_interp_intro; iApply awp_ret;
- iApply denv_stack_interp_intro; iApply awp_ret;
iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
+ destruct (vcg_sp E ms de1 n)
- destruct (vcg_sp E ms de1 n)
as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
......@@ -583,7 +583,7 @@ Section vcg_spec.
rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2").
iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto.
rewrite- denv_merge_interp. iFrame.
+ destruct (vcg_sp E ms de n)
- destruct (vcg_sp E ms de n)
as [[[ms1 mNew1] dv1]|] eqn:Hsp'; simplify_eq /=.
destruct (is_dloc _ _)
as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
......@@ -603,161 +603,153 @@ Section vcg_spec.
iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
iIntros "Hl". iSplit; eauto.
rewrite -denv_insert_interp. by iFrame.
Admitted.
(*
- 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/=.
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
iPoseProof IHde as "Hawp"; first done.
iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
iClear "Hawp Hm".
iApply (denv_stack_interp_mono with "Hawp'").
iIntros "[Hawp Hm]".
iApply a_load_spec.
iApply (awp_wand with "Hawp").
iIntros (?) "[% HmNew1]". simplify_eq/=.
iExists _, _. iSplit; eauto.
iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
iIntros "Hl". iSplit; eauto.
rewrite -denv_insert_interp. by iFrame.
- 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).
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv3] |] eqn:Hfar; simplify_eq/=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
iPoseProof denv_delete_full_2_interp as "Hl"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
iClear "Hawp1 Hawp2 Hl Hawp'".
iApply (denv_stack_interp_mono with "Hawp").
iIntros "[[Hawp1 Hawp2] Hl]".
iApply (a_store_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=.
iExists _, _; iSplit; eauto.
iCombine "HmNew1 HmNew2" as "HmNew".
rewrite denv_merge_interp -denv_insert_interp.
iDestruct ("Hl" with "HmNew") as "[HmNew3 $]".
iIntros "Hl". by iFrame.
- specialize (IHde1 ms).
destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
specialize (IHde2 ms1).
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply (a_bin_op_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
iExists (dval_interp E dv). repeat iSplit; eauto.
+ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
+ rewrite -denv_merge_interp. iFrame.
- 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).
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=.
destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
iPoseProof denv_delete_full_2_interp as "Hl"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
iClear "Hawp1 Hawp2 Hawp' Hl".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[[Hawp1 Hawp2] Hl]".
iApply (a_pre_bin_op_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] HR"; simplify_eq/=.
iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp.
iExists (dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d).
iDestruct ("Hl" with "HmNew") as "[HmNew $]".
repeat iSplit; eauto.
+ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
+ iIntros "Hl". iFrame. iSplit; first done.
rewrite -denv_insert_interp. by iFrame.
- specialize (IHde ms).
destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
iPoseProof IHde as "Hawp"; first done.
iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
iIntros "Hawp".
iApply a_un_op_spec.
iApply (awp_wand with "Hawp"). iIntros (v) "[% H]". simplify_eq/=.
iExists (dval_interp E dv). repeat iSplit; eauto.
iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu.
- specialize (IHde1 ms).
destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
specialize (IHde2 (denv_unlock mNew1 :: ms1)).
destruct (vcg_sp E _ de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec'.
iNext. iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
rewrite (denv_unlock_interp E mNew1).
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
rewrite -denv_merge_interp. iSplit; eauto with iFrame.
- specialize (IHde1 ms).
destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
specialize (IHde2 ms1).
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
iPoseProof IHde1 as "Hawp1"; first done.
iPoseProof IHde2 as "Hawp2"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply (awp_par with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
simplify_eq/=; iSplit; eauto.
rewrite -denv_merge_interp. iFrame.
Qed. *)
- destruct (vcg_sp E ms de1)
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 (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv3] |] eqn:Hfar; simplify_eq/=.
iPoseProof (IH de1) as "Hawp1"; destruct_and!; try done.
iPoseProof (IH de2) as "Hawp2"; try done.
iPoseProof denv_delete_full_2_interp as "Hl"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
iClear "Hawp1 Hawp2 Hl Hawp'".
iApply (denv_stack_interp_mono with "Hawp").
iIntros "[[Hawp1 Hawp2] Hl]".
iApply (a_store_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=.
iExists _, _; iSplit; eauto.
iCombine "HmNew1 HmNew2" as "HmNew".
rewrite denv_merge_interp -denv_insert_interp.
iDestruct ("Hl" with "HmNew") as "[HmNew3 $]".
iIntros "Hl". by iFrame.
- 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 /=.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe;
simplify_eq/=; destruct_and!.
iPoseProof (IH de1 ms) as "Hawp1"; try done.
iPoseProof (IH de2 ms1) as "Hawp2"; try done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply (a_bin_op_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
iExists (dval_interp E dv). repeat iSplit; eauto.
+ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
+ rewrite -denv_merge_interp. iFrame.
- destruct (vcg_sp E ms de1)
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 (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=.
destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe;
simplify_eq/=; destruct_and!.
iPoseProof (IH de1 ms) as "Hawp1"; try done.
iPoseProof (IH de2 ms1) as "Hawp2"; try done.
iPoseProof denv_delete_full_2_interp as "Hl"; first done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
iClear "Hawp1 Hawp2 Hawp' Hl".
iApply (denv_stack_interp_mono with "Hawp").
iIntros "[[Hawp1 Hawp2] Hl]".
iApply (a_pre_bin_op_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] HR"; simplify_eq/=.
iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp.
iExists
(dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d).
iDestruct ("Hl" with "HmNew") as "[HmNew $]".
repeat iSplit; eauto.
+ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
+ iIntros "Hl". iFrame. iSplit; first done.
rewrite -denv_insert_interp. by iFrame.
- destruct (vcg_sp E ms de)
as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
iPoseProof (IH de ms) as "Hawp"; try done.
iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
iIntros "Hawp".
iApply a_un_op_spec.
iApply (awp_wand with "Hawp"). iIntros (v) "[% H]". simplify_eq/=.
iExists (dval_interp E dv). repeat iSplit; eauto.
iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu.
- destruct (vcg_sp E ms de1)
as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct (vcg_sp E _ de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=; destruct_and!.
iPoseProof (IH de1 ms) as "Hawp1"; try done.
iPoseProof (IH de2 (denv_unlock mNew1 :: ms1)) as "Hawp2"; try done.
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec'.
{ by apply dcexpr_closed. }
iNext. iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
rewrite (denv_unlock_interp E mNew1).
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
rewrite -denv_merge_interp. iSplit; eauto with iFrame.
- 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 /=; destruct_and!.
iPoseProof (IH de1) as "Hawp1"; try done.
iPoseProof (IH de2) as "Hawp2"; try done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply (awp_par with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
simplify_eq/=; iSplit; eauto.
rewrite -denv_merge_interp. iFrame. }
Qed.
Lemma vcg_sp_correct E de m ms mNew dv R n:
vcg_sp E [m] de n = Some (ms, mNew, dv)
dcexpr_wf [] E de
denv_interp E m -
denv_interp E (denv_stack_merge ms)
awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
iIntros (Hsp) "Hm".
iIntros (Hsp Hwf) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
assert ( m', ms = [m']) as [m' ->]=>/=.
{ destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
Qed.
{ done. }
Admitted.
(* 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)
dcexpr_wf [] E de
denv_interp E m -
denv_interp E m'
awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof. Admitted.
(* rewrite /vcg_sp'.
iIntros (Hsp') "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).
rewrite vcg_sp_correct; last eassumption. simpl.
rewrite denv_merge_nil_r. iFrame.
Qed. *)
Proof.
rewrite /vcg_sp'.
iIntros (Hsp' Hwf) "Hm".
destruct (vcg_sp E [m] de 1024) 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); 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.
Lemma vcg_sp_wf' E de ms ms' mNew dv n:
Forall (denv_wf E) ms
......
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