Commit 148d00ca authored by Dan Frumin's avatar Dan Frumin
Browse files

Get rid of some admits

parent cab3db52
......@@ -296,6 +296,48 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
| dCUnknown e1 => W.to_expr e1
end.
(** ** Substitution *)
Fixpoint de_subst
(E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
match de with
| dEVal _ => de
| dEVar y => if decide (x = y) then dEVal dv else de
| dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
| dEFst de1 => dEFst (de_subst E x dv de1)
| dESnd de1 => dESnd (de_subst E x dv de1)
| dEUnknown we =>
dEUnknown (W.subst x
(W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
end.
Fixpoint dce_subst (E: known_locs)
(x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
match dce with
| dCRet de1 => dCRet (de_subst E x dv de1)
| dCBind y de1 de2 =>
if decide (x = y)
then dCBind y (dce_subst E x dv de1) de2
else dCBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCLoad de1 => dCLoad (dce_subst E x dv de1)
| dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCBinOp op de1 de2 =>
dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPreBinOp op de1 de2 =>
dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCUnOp op de1 => dCUnOp op (dce_subst E x dv de1)
| dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
| dCUnknown we => dCUnknown (W.subst x (W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
end.
(** Well-formedness of dcexpr w.r.t. known_locs *)
Definition dloc_wf (E: known_locs) (dl : dloc) : bool :=
match dl with
......@@ -330,6 +372,74 @@ Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
| dCUnknown e => W.is_closed X e
end.
(** Substitution properties *)
(* We need to be able to simplify subst in the following lemma *)
Arguments subst _ _ !_ /.
Lemma de_subst_subst_comm E x de dv :
(dexpr_interp E (de_subst E x dv de)) =
subst x (dval_interp E dv) (dexpr_interp E de).
Proof.
induction de; simplify_eq /=.
- by simpl_subst.
- by destruct (decide (x = s)).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- by rewrite! W.to_expr_subst.
Qed.
Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
dcexpr_interp E (dce_subst E x dv de) =
(subst x (dval_interp E dv) (dcexpr_interp E de))%E.
Proof.
induction de; simplify_eq /=; simpl_subst;
try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- by rewrite de_subst_subst_comm.
- destruct (decide (x = s)); simplify_eq /=; rewrite IHde1.
+ rewrite decide_False; naive_solver.
+ rewrite IHde2 decide_True; naive_solver.
Qed.
(* Turn the simplification in subst OFF again *)
Arguments subst : simpl never.
Lemma de_subst_dexpr_wf X E s dv1 de2 :
dval_wf E dv1
dexpr_wf (s::X) E de2
dexpr_wf X E (de_subst E s dv1 de2).
Proof.
revert X. induction de2; intros X Hdv1 Hwf2;
simplify_eq/=; try naive_solver.
- case_match; eauto. simpl.
apply bool_decide_pack.
apply bool_decide_unpack in Hwf2.
set_solver.
- apply W.is_closed_correct in Hwf2.
admit.
Admitted.
Lemma dce_subst_dcexpr_wf X E s dv1 de2 :
dval_wf E dv1
dcexpr_wf (s::X) E de2
dcexpr_wf X E (dce_subst E s dv1 de2).
Proof.
revert X. induction de2; intros X Hdv1 Hwf2;
simplify_eq/=; try naive_solver.
- by apply de_subst_dexpr_wf.
- destruct_and!. case_match; simpl; split_and; eauto.
+ subst.
(* use H0 *)
admit.
+ eapply IHde2_2; eauto.
admit.
- apply W.is_closed_correct in Hwf2.
admit. (* Need W.is_closed_correct in the opposite direction *)
Admitted.
(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
......
......@@ -55,48 +55,6 @@ Section vcg.
| dEUnknown _ => None
end.
(** substitution *)
Fixpoint de_subst
(E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
match de with
| dEVal _ => de
| dEVar y => if decide (x = y) then dEVal dv else de
| dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
| dEFst de1 => dEFst (de_subst E x dv de1)
| dESnd de1 => dESnd (de_subst E x dv de1)
| dEUnknown we =>
dEUnknown (W.subst x
(W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
end.
Fixpoint dce_subst (E: known_locs)
(x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
match dce with
| dCRet de1 => dCRet (de_subst E x dv de1)
| dCBind y de1 de2 =>
if decide (x = y)
then dCBind y (dce_subst E x dv de1) de2
else dCBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCLoad de1 => dCLoad (dce_subst E x dv de1)
| dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCBinOp op de1 de2 =>
dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPreBinOp op de1 de2 =>
dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCUnOp op de1 => dCUnOp op (dce_subst E x dv de1)
| dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
| dCUnknown we => dCUnknown (W.subst x (W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
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`. *)
......@@ -363,45 +321,6 @@ End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Arguments subst _ _ !_ /.
Lemma de_subst_subst_comm E x de dv :
(dexpr_interp E (de_subst E x dv de)) =
subst x (dval_interp E dv) (dexpr_interp E de).
Proof.
induction de; simplify_eq /=.
- by simpl_subst.
- by destruct (decide (x = s)).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- by rewrite! W.to_expr_subst.
Qed.
Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
dcexpr_interp E (dce_subst E x dv de) =
(subst x (dval_interp E dv) (dcexpr_interp E de))%E.
Proof.
induction de; simplify_eq /=; simpl_subst;
try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- by rewrite de_subst_subst_comm.
- destruct (decide (x = s)); simplify_eq /=; rewrite IHde1.
+ rewrite decide_False; naive_solver.
+ rewrite IHde2 decide_True; naive_solver.
Qed.
Lemma dce_subst_dcexpr_wf E s dv1 de2 :
dval_wf E dv1
dcexpr_wf [s] E de2
dcexpr_wf [] E (dce_subst E s dv1 de2).
Proof. Admitted.
Arguments subst : simpl never.
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
......@@ -500,6 +419,142 @@ Section vcg_spec.
+ done.
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_wf' E de ms ms' mNew dv n:
Forall (denv_wf E) ms
dcexpr_wf [] E de
vcg_sp E ms de n = Some (ms', mNew, dv)
Forall (denv_wf E) ms' denv_wf E mNew dval_wf E dv .
Proof.
revert de ms ms' mNew dv. induction n as [|n IH];
intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
{ destruct de; simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf. }
destruct de; simplify_eq /=.
- simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2))
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct ms2 as [|t ms2]; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
assert (Forall (denv_wf E) (mNew1 :: ms1)) as Hwfms2.
{ apply Forall_cons. split; eauto. }
assert (dcexpr_wf [] E (dce_subst E s dv1 de2)) as Hwfsubst.
by apply dce_subst_dcexpr_wf.
destruct (IH (dce_subst E s dv1 de2) _ _ _ _ Hwfms2 Hwfsubst Hsp2) as (Hall&?&?).
apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge.
- 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)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
eapply denv_wf_delete_frac_2 in Hout1; eauto.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert.
- 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] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
eapply denv_wf_delete_full_2 in Hout1; try eassumption.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert.
eauto using denv_wf_merge.
- 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/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
- 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] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
eapply denv_wf_delete_full_2 in Hout1; try eassumption.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert, denv_wf_merge.
eapply denv_wf_insert; eauto.
eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
by eapply denv_wf_merge.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
repeat split; eauto.
eapply dun_op_eval_Some_wf; eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct ms2 as [|t ms2]; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2.
{ apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
destruct (IH de2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge.
- 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/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
Qed.
Lemma vcg_sp'_wf E de m m' mNew dv :
denv_wf E m
dcexpr_wf [] E de
vcg_sp' E m de = Some (m', mNew, dv)
denv_wf E m' denv_wf E mNew dval_wf E dv.
Proof.
rewrite /vcg_sp'. intros Hm Hde Hsp'.
assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto).
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). simpl in Hsp'.
inversion Hsp'. subst.
destruct (vcg_sp_wf' E de [m] [m'] mNew _ _ Hms Hde Hsp) as (Hm'&?&?).
repeat split; eauto. by inversion Hm'.
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.
......@@ -522,31 +577,9 @@ Section vcg_spec.
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_dval_wf E de ms ms' mNew dv n :
vcg_sp E ms de n = Some (ms', mNew, dv)
dval_wf E dv.
Proof. Admitted.
Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
vcg_sp E ms de n = Some (ms', mNew, dv)
Forall (denv_wf E) ms
dcexpr_wf [] E de
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R
......@@ -554,12 +587,12 @@ 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 Hwfms 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 (de ms ms' mNew dv Hsp Hwfms Hwf).
destruct de; simplify_option_eq.
- iApply denv_stack_interp_intro; iApply awp_ret;
iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
......@@ -571,10 +604,20 @@ Section vcg_spec.
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
iPoseProof (IH de1 ms) as "Hawp1"; first done. done.
iPoseProof (IH de1 ms) as "Hawp1"; eauto.
assert (Forall (denv_wf E) ms1
denv_wf E mNew1 dval_wf E dv1).
{ eapply vcg_sp_wf'; eauto. }
destruct_and!.
assert (Forall (denv_wf E) (mNew1 :: ms1)).
{ econstructor; eauto. }
assert (Forall (denv_wf E) (t :: ms')
denv_wf E mNew2 dval_wf E dv).
{ eapply (vcg_sp_wf' _ (dce_subst E s dv1 de2)); eauto.
apply dce_subst_dcexpr_wf; eauto. }
iPoseProof (IH (dce_subst E s dv1 de2) (mNew1 :: ms1))
as "Hawp2"; first done.
apply dce_subst_dcexpr_wf. eapply vcg_sp_dval_wf. eassumption. done.
as "Hawp2"; eauto.
{ apply dce_subst_dcexpr_wf; eauto. }
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
......@@ -596,7 +639,7 @@ Section vcg_spec.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
specialize (IH de ms).
iPoseProof IH as "Hawp"; first done. done.
iPoseProof IH as "Hawp"; eauto.
iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
iClear "Hawp Hm".
......@@ -618,8 +661,9 @@ Section vcg_spec.
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 (IH de1) as "Hawp1"; destruct_and!; eauto.
iPoseProof (IH de2) as "Hawp2"; eauto.
{ eapply (vcg_sp_wf' _ de1); eauto. }
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".
......@@ -639,8 +683,9 @@ Section vcg_spec.
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.
iPoseProof (IH de1 ms) as "Hawp1"; eauto.
iPoseProof (IH de2 ms1) as "Hawp2"; eauto.
{ eapply (vcg_sp_wf' _ de1); eauto. }
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
......@@ -660,7 +705,8 @@ Section vcg_spec.
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 (IH de2 ms1) as "Hawp2"; eauto.
{ eapply (vcg_sp_wf' _ de1); eauto. }
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".
......@@ -691,8 +737,10 @@ Section vcg_spec.
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.
iPoseProof (IH de1 ms) as "Hawp1"; eauto.
iPoseProof (IH de2 (denv_unlock mNew1 :: ms1)) as "Hawp2"; eauto.
{ econstructor; [eapply denv_wf_unlock |];
eapply (vcg_sp_wf' _ de1); eauto. }
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
......@@ -711,7 +759,8 @@ Section vcg_spec.
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.
iPoseProof (IH de2) as "Hawp2"; eauto.
{ eapply (vcg_sp_wf' _ de1); eauto. }
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
......@@ -723,14 +772,15 @@ Section vcg_spec.
Lemma vcg_sp_correct E de m ms mNew dv R n:
vcg_sp E [m] de n = Some (ms, mNew, dv)
denv_wf E m
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 Hwf) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; first eassumption; first done.
iIntros (Hsp Hwfm Hwf) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; eauto.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen;
assert ( m', ms = [m']) as [m' ->]=>/=.
{ destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
......@@ -739,6 +789,7 @@ Section vcg_spec.
Lemma vcg_sp'_correct E de m m' mNew dv R :
vcg_sp' E m de = Some (m', mNew, dv)
denv_wf E m
dcexpr_wf [] E de
denv_interp E m -
denv_interp E m'
......@@ -746,133 +797,16 @@ Section vcg_spec.
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
rewrite /vcg_sp'.
iIntros (Hsp' Hwf) "Hm".
iIntros (Hsp' Hwfm 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 vcg_sp_correct; eauto. simpl.
rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=.
by iFrame.
Qed.