Commit cfaef17b authored by Léon Gondelman's avatar Léon Gondelman

finished the vcg_wp for alloc

parent 19fba43f
......@@ -50,6 +50,12 @@ Definition dloc_interp (E : known_locs) (dl : dloc) : loc :=
| dLocUnknown l => l
end.
Lemma dloc_interp_lookup_endl E l :
l = (dloc_interp (E ++ [l]) (dLoc (length E))).
Proof.
induction E; simplify_eq /=; done.
Qed.
Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
match l with
| dLitInt x => LitInt x
......
......@@ -225,7 +225,7 @@ Section denv_spec.
apply denv_singleton_lookup in Hk as [? ->]. omega.
- iIntros "[$ _]".
Qed.
Lemma denv_insert_interp_aux E m i k x q dv :
denv_interp_aux E m k dloc_interp E (dLoc (k+i)) C[x]{q} dval_interp E dv
denv_interp_aux E (denv_insert i x q dv m) k.
......@@ -297,11 +297,11 @@ Section denv_spec.
+ iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
Qed.
Lemma denv_merge_interp E m1 m2 :
denv_interp E m1 denv_interp E m2 denv_interp E (denv_merge m1 m2).
Proof. by rewrite -!denv_interp_aux_0 denv_merge_interp_aux. Qed.
Lemma denv_delete_frac_interp_aux E i k m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
denv_interp_aux E m k
......@@ -606,7 +606,7 @@ Section denv_spec.
eauto with iFrame.
- destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:Hnew; simplify_eq/=.
iApply denv_stack_interp_intro.
rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux; last done.
rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux; last done.
eauto with iFrame.
Qed.
......@@ -660,11 +660,11 @@ Section denv_spec.
- destruct di as [dl df dval]. destruct i.
case_option_guard; simplify_eq/=; try naive_solver.
intros ? ?; destruct_and!.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
split_and!; eauto; eapply IHm; eauto.
- destruct i; first naive_solver.
intros ??.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
eapply IHm; eauto.
Qed.
......@@ -712,4 +712,15 @@ Section denv_spec.
denv_wf E m'
dval_wf E dv.
Proof. Admitted.
Lemma denv_wf_extend E m dv l x q :
denv_wf E m dval_wf E dv
denv_wf (E ++ [l]) (denv_insert (length E) x q dv m).
Proof.
intros.
assert (E `prefix_of` E ++ [l]). by eapply prefix_app_l; done.
assert (dval_wf (E ++ [l]) dv). eapply dval_wf_mono; done.
apply denv_wf_insert; eauto. eapply denv_wf_mono; done.
Qed.
End denv_spec.
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......@@ -21,4 +21,41 @@ Section tests_vcg.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_solver. iIntros "!> !> !>". eauto with iFrame.
Qed.
Definition swap_with_alloc : val := λ: "l1" "l2",
a_bind (λ: "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;;; a_ret #())
(a_alloc (a_ret #0)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
l1 C v1 - l2 C v2 -
awp (swap_with_alloc #l1 #l2) R (λ _, l1 C v2 l2 C v1).
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "Hr".
vcg_solver. repeat iModIntro. eauto with iFrame.
(* Compared with step-by-step proof *) (*
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "Hr".
iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". iModIntro. awp_ret_value. by iFrame. *)
Qed.
End tests_vcg.
......@@ -586,14 +586,18 @@ Section vcg_spec.
iIntros (l) "Hl". iSpecialize ("Hwp" $! l).
unfold vcg_wp_postcondition.
iExists (E' ++ [l]), (dLitV (dLitLoc (dLoc (length E')))), (denv_insert (length E') ULvl 1 dv m').
iSplit. admit. (*TODO: this will require a special lemma *)
iSplit. iPureIntro. compute[dval_interp dbase_lit_interp]. do 2 f_equal.
apply (dloc_interp_lookup_endl E' l).
iSplit. iPureIntro. trans E'; first done. by apply prefix_app_r.
iSplit. admit. (*TODO: this will require another denv_wf monotonicity lemma *)
iSplit. (*TODO: this will require a special lemma *) admit.
iSplit. iPureIntro. by apply denv_wf_extend.
iSplit. iPureIntro. compute[dval_wf].
case_bool_decide; first done. apply H0. apply lookup_lt_is_Some_2.
rewrite app_length. simpl. lia.
iFrame. rewrite -denv_insert_interp.
iSplitL "Hm". iApply (denv_interp_mono with "Hm"); first done.
trans E'; first done. by apply prefix_app_r.
(*TODO: this will require a special lemma *) admit.
trans E'; first done. by apply prefix_app_r.
rewrite -(dloc_interp_lookup_endl E' l).
rewrite (dval_interp_mono E' (E'++[l])) //. by apply prefix_app_r .
- rewrite IHde //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
......
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