Commit 9bcba503 authored by Léon Gondelman's avatar Léon Gondelman

fixed and proved vcgen with list of permissions

parent 1621092c
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-05-23.3.7ae0b644") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-31.1.27914f3f") | (= "dev") }
]
......@@ -73,14 +73,14 @@ Section proofs.
wp_let. wp_alloc l as "Hl".
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iExFalso. rewrite (bi.big_sepM_lookup _ σ l _); last eauto.
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'".
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "H Hl'".
- iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+ rewrite bi.big_sepM_insert; eauto. iFrame. eauto.
+ rewrite big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iApply ("H" with "Hl'").
Qed.
......@@ -118,7 +118,7 @@ Section proofs.
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hv" as "[Hv Hl]".
rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
rewrite Qp_mult_1_l.
......@@ -129,7 +129,7 @@ Section proofs.
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -bi.big_sepM_insert_override; eauto.
+ rewrite -big_sepM_insert_override; eauto.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
......@@ -224,7 +224,7 @@ Section proofs.
iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
{ iIntros "Hus". iApply "HΦ". by iFrame. }
{ rewrite -bi.big_sepM_insert_override; eauto. }
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R Φ (f e : expr) :
......
This diff is collapsed.
......@@ -22,7 +22,7 @@ Section contents.
Lemma U_intro P : P U P.
Proof.
iIntros "HP". iExists [].
rewrite !bi.big_sepL_nil. eauto.
rewrite !big_sepL_nil. eauto.
Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
......@@ -31,7 +31,7 @@ Section contents.
iIntros "[HP HQ]".
iDestruct "HP" as (ls1) "[HP1 HP2]".
iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
iExists (ls1++ls2). rewrite !bi.big_sepL_app. iFrame.
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
- by iApply "HP2".
- by iApply "HQ2".
......@@ -44,7 +44,7 @@ Section contents.
Proof.
iDestruct 1 as (ls1) "[HPQ1 HPQ2]".
iDestruct 1 as (ls2) "[HP1 HP2]".
iExists (ls1++ls2). rewrite !bi.big_sepL_app. iFrame.
iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
iIntros "[HPQ1 HP1]".
iApply ("HPQ2" with "HPQ1").
iApply ("HP2" with "HP1").
......
......@@ -131,40 +131,40 @@ Section flock.
(** all_props lemmas *)
Lemma all_props_empty : all_props .
Proof. by rewrite /all_props bi.big_sepM_empty. Qed.
Proof. by rewrite /all_props big_sepM_empty. Qed.
Lemma all_props_singleton s R : all_props {[s := R]} R.
Proof. by rewrite /all_props bi.big_sepM_singleton. Qed.
Proof. by rewrite /all_props big_sepM_singleton. Qed.
Lemma all_props_insert s (R : iProp Σ) f :
f !! s = None
all_props (<[s := R]>f) (R all_props f)%I.
Proof. intros ?. rewrite /all_props bi.big_sepM_insert //. Qed.
Proof. intros ?. rewrite /all_props big_sepM_insert //. Qed.
Lemma all_props_union f g :
all_props f all_props g all_props (f g).
Proof.
revert g.
simple refine (map_ind (fun f => g, all_props f all_props g - all_props (f g)) _ _ f); simpl; rewrite /all_props.
- intros g. by rewrite bi.big_sepM_empty !left_id.
- intros g. by rewrite big_sepM_empty !left_id.
- intros i P f' Hi IH.
intros g. rewrite bi.big_sepM_insert; last done.
intros g. rewrite big_sepM_insert; last done.
iIntros "[[HP Hf] Hg]".
rewrite -insert_union_l.
remember (g !! i) as Z. destruct Z as [R|].
+ assert (g = <[i:=R]>(delete i g)) as Hfoo.
{ rewrite insert_delete insert_id; eauto. }
rewrite {1}Hfoo.
rewrite bi.big_sepM_insert; last first.
rewrite big_sepM_insert; last first.
{ apply lookup_delete. }
iDestruct "Hg" as "[HR Hg]".
iApply (bi.big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
iApply (big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
{ apply lookup_union_Some_raw. right. eauto. }
* iApply (IH g).
rewrite Hfoo bi.big_sepM_insert; last by apply lookup_delete.
rewrite Hfoo big_sepM_insert; last by apply lookup_delete.
rewrite delete_insert; last by apply lookup_delete. iFrame.
* eauto.
+ rewrite bi.big_sepM_insert; last first.
+ rewrite big_sepM_insert; last first.
{ apply lookup_union_None. eauto. }
iFrame. iApply (IH g). iFrame.
Qed.
......@@ -174,14 +174,14 @@ Section flock.
Proof.
intros f. rewrite /all_props. (* rewrite /all_props /big_opM. *)
simple refine (map_ind (fun f => g, f g _ _) _ _ f); simpl.
- intros g. rewrite bi.big_sepM_empty.
- intros g. rewrite big_sepM_empty.
simple refine (map_ind (fun g => g _ _) _ _ g); simpl.
+ by rewrite bi.big_sepM_empty.
+ by rewrite big_sepM_empty.
+ intros j R g' Hj IH Hg'.
exfalso. specialize (Hg' j). revert Hg'.
rewrite lookup_insert lookup_empty. inversion 1.
- intros i P f' Hi IH g Hf'.
rewrite bi.big_sepM_insert; last done.
rewrite big_sepM_insert; last done.
specialize (IH (delete i g)).
assert (f' delete i g) as Hf'g.
{ by rewrite -Hf' delete_insert. }
......@@ -192,7 +192,7 @@ Section flock.
- exfalso. revert Hf'. rewrite lookup_insert. inversion 1.
- exists R. split; auto.
revert Hf'. rewrite lookup_insert. by inversion 1. }
rewrite (bi.big_sepM_delete _ g i R); eauto.
rewrite (big_sepM_delete _ g i R); eauto.
by apply bi.sep_proper.
Qed.
......@@ -556,7 +556,7 @@ Section flock.
intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
simplify_eq/=; exists R''; eauto. }
destruct Hfoo as [R' [HReq Hf]].
rewrite /all_props {1}(bi.big_sepM_lookup_acc _ fa s R'); last done.
rewrite /all_props {1}(big_sepM_lookup_acc _ fa s R'); last done.
iDestruct "Hfa" as "[HR' Hfa]".
assert (( R)%I ( R')%I) as ->. by apply bi.later_proper.
by iFrame.
......
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