Commit 756fb75f authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix `vcg_sp` for Seq

Generalize `vcg_sp` to take two environments instead of one.
parent 312c1b5a
......@@ -97,36 +97,36 @@ Section vcg.
Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
mapsto_wand_list_aux m Φ O.
Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Fixpoint vcg_sp (E: known_locs) (mIn mOut : denv) (de : dcexpr) : option (denv * denv * dval) :=
match de with
| dCRet dv => Some (m, nil, dv)
| dCRet dv => Some (mIn, mOut, dv)
| dCLoad de1 =>
''(mIn, mOut, dl) vcg_sp E m de1;
i is_dloc E dl;
''(mIn1, mOut1, q, dv) denv_delete_frac_2 i mIn mOut;
Some (mIn1, denv_insert i ULvl q dv mOut1, dv)
''(mIn1, mOut1, dl) vcg_sp E mIn mOut de1;
i is_dloc E dl;
''(mIn2, mOut2, q, dv) denv_delete_frac_2 i mIn1 mOut1;
Some (mIn2, denv_insert i ULvl q dv mOut2, dv)
| dCStore de1 de2 =>
''(mIn1, mOut1, dl) vcg_sp E m de1;
''(mIn1, mOut1, dl) vcg_sp E mIn mOut de1;
i is_dloc E dl;
''(mIn2, mOut2, dv) vcg_sp E mIn1 de2;
''(mIn2, mOut2, dv) vcg_sp E mIn1 [] de2;
''(mIn3, mOut3, _) denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2);
Some (mIn3, denv_insert i LLvl 1 dv mOut3, dv)
| dCBinOp op de1 de2 =>
''(mIn1, mOut1, dv1) vcg_sp E m de1;
''(mIn2, mOut2, dv2) vcg_sp E mIn1 de2;
''(mIn1, mOut1, dv1) vcg_sp E mIn mOut de1;
''(mIn2, mOut2, dv2) vcg_sp E mIn1 [] de2;
match dbin_op_eval E op dv1 dv2 with
| dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
| dNone | dUnknown _ => None
end
| dCUnOp op de =>
''(mIn, mOut, dv) vcg_sp E m de;
''(mIn1, mOut1, dv) vcg_sp E mIn mOut de;
match dun_op_eval E op dv with
| dSome dv' => Some (mIn, mOut, dv')
| dSome dv' => Some (mIn1, mOut1, dv')
| dNone | dUnknown _ => None
end
| dCSeq de1 de2 =>
''(mIn1, mOut1, _) vcg_sp E m de1;
''(mIn2, mOut2, dv2) vcg_sp E (denv_merge mIn1 (denv_unlock mOut1)) de2;
''(mIn1, mOut1, _) vcg_sp E mIn mOut de1;
''(mIn2, mOut2, dv2) vcg_sp E mIn1 (denv_unlock mOut1) de2;
Some (mIn2, mOut2, dv2)
| dCAlloc _ | dCUnknown _ => None
end.
......@@ -189,12 +189,12 @@ Section vcg.
| dCLoad de1 =>
vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E))
| dCStore de1 de2 =>
match vcg_sp E m de1 with
match vcg_sp E m [] de1 with
| Some (mIn, mOut, dv1) =>
vcg_wp E mIn de2 R (λ E mIn dv2,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
| None =>
match vcg_sp E m de2 with
match vcg_sp E m [] de2 with
| Some (mIn, mOut, dv2) =>
vcg_wp E mIn de1 R (λ E mIn dv1,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
......@@ -202,12 +202,12 @@ Section vcg.
end
end
| dCBinOp op de1 de2 =>
match vcg_sp E m de1 with
match vcg_sp E m [] de1 with
| Some (mIn, mOut, dv1) =>
vcg_wp E mIn de2 R (λ E mIn dv2,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
| None =>
match vcg_sp E m de2 with
match vcg_sp E m [] de2 with
| Some (mIn, mOut, dv2) =>
vcg_wp E mIn de1 R (λ E mIn dv1,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
......@@ -258,40 +258,43 @@ Section vcg_spec.
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed. *)
Lemma vcg_sp_correct E m de mIn mOut dv R :
vcg_sp E m de = Some (mIn, mOut, dv)
denv_interp E m -
denv_interp E mIn
awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mOut).
Lemma vcg_sp_correct' E de mIn mOut mIn' mOut' dv R :
vcg_sp E mIn mOut de = Some (mIn', mOut', dv)
denv_interp E mIn -
denv_interp E mIn'
(denv_interp E mOut - awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mOut')).
Proof.
revert m mIn mOut dv. induction de;
iIntros (m mIn mOut dv Hsp) "Hm"; simplify_eq/=.
- iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold denv_interp. done.
- specialize (IHde m).
destruct (vcg_sp E m de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
revert mIn mOut mIn' mOut' dv. induction de;
iIntros (mIn mOut mIn' mOut' dv Hsp) "HmIn"; simplify_eq/=.
- iFrame. iIntros "HmOut". iApply awp_ret. wp_value_head. iSplit; eauto.
- specialize (IHde mIn mOut).
destruct (vcg_sp E mIn mOut de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac_2 i mIn1 mOut1) as [[[[mIn2 mOut2] q] dv1]|] eqn:Hfar; simplify_eq/=.
rewrite IHde; last done. iDestruct "Hm" as "[HmIn1 Hawp]".
rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]".
iDestruct (denv_delete_frac_2_interp with "HmIn1") as "[$ Hm]"; first eassumption.
iIntros "HmOut". iSpecialize ("Hawp" with "HmOut").
iApply a_load_spec.
iApply (awp_wand with "Hawp").
iIntros (?) "[% HmOut1]". simplify_eq/=. iExists _, _. iSplit; eauto.
iDestruct ("Hm" with "HmOut1") as "[HmOut2 $]". iIntros "Hl". iSplit; eauto.
rewrite denv_insert_interp.
by iFrame.
- specialize (IHde1 m).
destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
- specialize (IHde1 mIn mOut).
destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
specialize (IHde2 mIn1).
destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
specialize (IHde2 mIn1 []).
destruct (vcg_sp E mIn1 [] de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
destruct (denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2))
as [[[mIn3 mOut3 ] dv3] |] eqn:Hfar; simplify_eq/=.
rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2' Hawp2]".
rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2 Hawp2]".
rewrite denv_delete_full_2_interp; last done.
iDestruct "HmIn2'" as "[$ Hl]".
iDestruct "HmIn2" as "[$ Hl]". iIntros "HmOut".
iSpecialize ("Hawp2" with "[]"). rewrite /denv_interp; done.
iSpecialize ("Hawp1" with "HmOut").
iApply (a_store_spec _ _
(λ j, j = dloc_interp E (dLoc i) denv_interp E mOut1)%I with "[Hawp1] Hawp2").
{ iApply (awp_wand with "Hawp1").
......@@ -302,50 +305,54 @@ Section vcg_spec.
iIntros "Hl". iSplit; eauto.
rewrite denv_insert_interp.
iFrame "Hl HmOut3".
- specialize (IHde1 m).
destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
specialize (IHde2 mIn1).
destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
- specialize (IHde1 mIn mOut).
destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
specialize (IHde2 mIn1 []).
destruct (vcg_sp E mIn1 [] de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
iIntros "HmOut". iSpecialize ("Hawp1" with "HmOut").
iSpecialize ("Hawp2" with "[]"). by rewrite /denv_interp.
iApply (a_bin_op_spec with "Hawp1 Hawp2").
iNext. iIntros (? ?) "[% HmOut1] [% HmOut2]"; simplify_eq/=.
iExists (dval_interp E dv). repeat iSplit; eauto.
+ iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
+ rewrite -denv_merge_interp. iFrame.
- specialize (IHde m).
destruct (vcg_sp E m de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
- specialize (IHde mIn mOut).
destruct (vcg_sp E mIn mOut de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
rewrite IHde; last done. iDestruct "Hm" as "[$ Hawp]".
rewrite IHde; last done. iDestruct "HmIn" as "[$ Hawp]".
iIntros "HmOut". iSpecialize ("Hawp" with "HmOut").
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 m).
destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
specialize (IHde2 (denv_merge mIn1 (denv_unlock mOut1))).
destruct (vcg_sp E _ de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
iPoseProof (IHde2) as "H"; first done.
- specialize (IHde1 mIn mOut).
destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
specialize (IHde2 mIn1 (denv_unlock mOut1)).
destruct (vcg_sp E mIn1 (denv_unlock mOut1) de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
iIntros "HmOut". iSpecialize ("Hawp1" with "HmOut").
(* TODO: wtf? *)
assert (AsVal (λ: <>, dcexpr_interp E de2)).
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
rewrite -a_sequence_spec.
admit.
(* specialize (IHde2 mIn1). *)
(* destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=. *)
(* rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]". *)
(* iApply (a_sequence_spec with "[Hawp1 Hawp2]"). *)
(* { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. } *)
(* iApply (awp_wand with "Hawp1"). *)
(* iIntros (?) "[-> HmOut1]"; simplify_eq/=. *)
(* rewrite (denv_unlock_interp E mOut1). *)
(* iModIntro. awp_seq. *)
(* iApply (awp_wand with "Hawp2"). *)
(* iIntros (v) "[-> HmOut2]". *)
(* iSplit; first done. *)
(* rewrite -denv_merge_interp. iFrame. *) Admitted.
(* Qed. *)
iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
iIntros (?) "[_ HmOut1]". rewrite (denv_unlock_interp E mOut1).
iModIntro. iSpecialize ("Hawp2" with "HmOut1").
awp_seq. iApply "Hawp2".
Qed.
Lemma vcg_sp_correct E de m mIn mOut dv R :
vcg_sp E m [] de = Some (mIn, mOut, dv)
denv_interp E m -
denv_interp E mIn awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mOut).
Proof.
iIntros (?) "Hm".
iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
iApply "Hawp". by rewrite /denv_interp.
Qed.
Lemma vcg_wp_correct R E m de Φ :
denv_interp E m -
......
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