Commit 312c1b5a authored by Dan Frumin's avatar Dan Frumin
Browse files

Start working on `vcg_sp`

parent c00f7e02
......@@ -8,6 +8,16 @@ From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
Context `{amonadG Σ}.
Lemma test_seq (s l : loc) :
s C[ULvl] #0 - l C[ULvl] #1 -
awp (a_bin_op PlusOp ((a_store (a_ret #l) (a_ret #2));;;;a_load (a_ret #l))
(a_store (a_ret #s) (a_ret #4))) True (λ v, v = #6 s C[LLvl] #4 l C #2).
Proof.
iIntros "Hs Hl".
vcg_solver.
rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma store_load (s l : loc) R :
s C #0 - l C #1 -
awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s C[LLvl] #1 l C #1).
......
......@@ -41,7 +41,6 @@ Section vcg.
(** Deep embedding of formulae used to build the verification condition generator *)
(** TODO: remove Par *)
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| MapstoStar : dloc (frac dval wp_expr) wp_expr
......@@ -104,8 +103,8 @@ Section vcg.
| dCLoad de1 =>
''(mIn, mOut, dl) vcg_sp E m de1;
i is_dloc E dl;
''(mIn1, mOut2, q, dv) denv_delete_frac_2 i mIn mOut;
Some (mIn1, denv_insert i ULvl q dv mOut2, dv)
''(mIn1, mOut1, q, dv) denv_delete_frac_2 i mIn mOut;
Some (mIn1, denv_insert i ULvl q dv mOut1, dv)
| dCStore de1 de2 =>
''(mIn1, mOut1, dl) vcg_sp E m de1;
i is_dloc E dl;
......@@ -127,8 +126,8 @@ Section vcg.
end
| dCSeq de1 de2 =>
''(mIn1, mOut1, _) vcg_sp E m de1;
''(mIn2, mOut2, dv2) vcg_sp E (denv_unlock mIn1) de2;
Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
''(mIn2, mOut2, dv2) vcg_sp E (denv_merge mIn1 (denv_unlock mOut1)) de2;
Some (mIn2, mOut2, dv2)
| dCAlloc _ | dCUnknown _ => None
end.
......@@ -264,23 +263,21 @@ Section vcg_spec.
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. Admitted.
(* revert m mIn mOut dv. induction de;
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 /=.
destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac i mIn1) as [[[mIn1' q] dv1]|] eqn:Hfar; simplify_eq/=.
rewrite IHde; last done. iDestruct "Hm" as "[HmIn1 Hawp]".
rewrite -denv_delete_frac_interp; last done.
iDestruct "HmIn1" as "[HmIn Hl]".
iFrame "HmIn".
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]".
iDestruct (denv_delete_frac_2_interp with "HmIn1") as "[$ Hm]"; first eassumption.
iApply a_load_spec.
iApply (awp_wand with "Hawp").
iIntros (?) "[% HmOut1]". simplify_eq/=. iExists _, _. iSplit; eauto.
iFrame "Hl". iIntros "Hl". iSplit; eauto.
iDestruct ("Hm" with "HmOut1") as "[HmOut2 $]". iIntros "Hl". iSplit; eauto.
rewrite denv_insert_interp.
by iFrame.
- specialize (IHde1 m).
......@@ -327,21 +324,28 @@ Section vcg_spec.
iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu.
- 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 /=.
rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
iApply (a_sequence_spec with "[Hawp1 Hawp2]").
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.
assert (AsVal (λ: <>, dcexpr_interp E de2)).
{ 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.
Qed. *)
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. *)
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