Commit 4592361e authored by Léon Gondelman 's avatar Léon Gondelman

wip

parent 6c3ed7ff
......@@ -351,6 +351,13 @@ End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
dcexpr_interp E (dce_subst E x dv de) =
(let: x := (dval_interp E dv) in (dcexpr_interp E de))%E.
Proof.
Admitted.
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
......@@ -387,7 +394,7 @@ Section vcg_spec.
destruct de; by simplify_option_eq.
(*Induction case*)
- intros ms ms' mNew dv de Hsp;
destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout.
destruct (vcg_sp E ms de (S n)) as [[[ms1 mNew1] dv1]|] eqn:Hout.
destruct de; simplify_eq /=; try by simplify_option_eq.
+ (*bind case*)
destruct (vcg_sp E ms de1 n)
......@@ -494,13 +501,63 @@ Section vcg_spec.
(awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew)))%I.
Proof.
Admitted. (*
revert ms ms' mNew dv. induction de;
iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
- simplify_option_eq.
revert de ms ms' mNew dv. induction n.
(* Base Case *)
- iIntros (de ms ms' mNew dv Hsp); 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).
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 //.
+ 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 /=.
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
(* specialize (IHn (mNew1 :: ms1)). *)
(* specialize (IHn de1). *)
iPoseProof (IHn de1 ms) as "Hawp1"; first done.
iPoseProof (IHn (dce_subst E s dv1 de2) (mNew1 :: ms1))
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_bind.
* admit.
* iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
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)
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/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
specialize (IHn de ms).
iPoseProof IHn 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.
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/=.
......
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