diff --git a/_CoqProject b/_CoqProject index 6f18679ede63cf8188fd34628bd7404382ced25c..1e919b355c4136038e8ade6bab57d9a8754106b3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -78,7 +78,6 @@ program_logic/ectxi_language.v program_logic/ectx_lifting.v program_logic/ghost_ownership.v program_logic/saved_prop.v -program_logic/auth.v program_logic/sts.v program_logic/namespaces.v program_logic/boxes.v diff --git a/algebra/auth.v b/algebra/auth.v index d831c60814efde52431787db4ea8e2c133ffbe50..94b0cabf32ea6be24817610fec86a9b1d34a0757 100644 --- a/algebra/auth.v +++ b/algebra/auth.v @@ -200,26 +200,20 @@ Proof. by rewrite /op /auth_op /= left_id. Qed. Lemma auth_auth_valid a : ✓ a → ✓ (◠a). Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed. -Lemma auth_update a af b : - a ~l~> b @ Some af → ◠(a ⋅ af) ⋅ ◯ a ~~> ◠(b ⋅ af) ⋅ ◯ b. +Lemma auth_update a b a' b' : + (a,b) ~l~> (a',b') → ◠a ⋅ ◯ b ~~> ◠a' ⋅ ◯ b'. Proof. - intros [Hab Hab']; apply cmra_total_update. - move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. - move: Ha; rewrite !left_id=> Hm; split; auto. - exists bf2. rewrite -assoc. - apply (Hab' _ (Some _)); auto. by rewrite /= assoc. + intros Hup; apply cmra_total_update. + move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *. + move: Ha; rewrite !left_id -assoc=> Ha. + destruct (Hup n (Some (bf1 ⋅ bf2))); auto. + split; last done. exists bf2. by rewrite -assoc. Qed. -Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ◠a ⋅ ◯ a ~~> ◠b ⋅ ◯ b. -Proof. - intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b). - by apply auth_update. -Qed. -Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ◠af ~~> ◠(b ⋅ af) ⋅ ◯ b. -Proof. - intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (◠_)). - by apply auth_update. -Qed. +Lemma auth_update_alloc a a' b' : (a,∅) ~l~> (a',b') → ◠a ~~> ◠a' ⋅ ◯ b'. +Proof. intros. rewrite -(right_id _ _ (◠a)). by apply auth_update. Qed. +Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',∅) → ◠a ⋅ ◯ b ~~> ◠a'. +Proof. intros. rewrite -(right_id _ _ (◠a')). by apply auth_update. Qed. End cmra. Arguments authR : clear implicits. diff --git a/algebra/coPset.v b/algebra/coPset.v index f90ff8e5ab8c4f0773f6ff3cbc823631734ccc60..722d95b09484e4f8ce29eacc285b6b92e189d795 100644 --- a/algebra/coPset.v +++ b/algebra/coPset.v @@ -48,11 +48,11 @@ Section coPset. Lemma coPset_update X Y : X ~~> Y. Proof. done. Qed. - Lemma coPset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf. + Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X'). Proof. intros (Z&->&?)%subseteq_disjoint_union_L. - intros; apply local_update_total; split; [done|]; simpl. - intros mZ _. rewrite !coPset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. + rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->. + split. done. rewrite coPset_op_union. set_solver. Qed. End coPset. diff --git a/algebra/csum.v b/algebra/csum.v index 13e8e30f54910759b9682ec6a1a480bdc689bf4a..27066a1d8410d78a871a2d19744dfcfd152653e5 100644 --- a/algebra/csum.v +++ b/algebra/csum.v @@ -300,31 +300,22 @@ Proof. eauto using csum_updateP_l. Qed. Lemma csum_updateP'_r (P : B → Prop) b : b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'. Proof. eauto using csum_updateP_r. Qed. -Lemma csum_local_update_l (a1 a2 : A) af : - (∀ af', af = Cinl <$> af' → a1 ~l~> a2 @ af') → Cinl a1 ~l~> Cinl a2 @ af. + +Lemma csum_local_update_l (a1 a2 a1' a2' : A) : + (a1,a2) ~l~> (a1',a2') → (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2'). Proof. - intros Ha. split; destruct af as [[af'| |]|]=>//=. - - by eapply (Ha (Some af')). - - by eapply (Ha None). - - destruct (Ha (Some af') (reflexivity _)) as [_ Ha']. - intros n [[mz|mz|]|] ?; inversion 1; subst; constructor. - by apply (Ha' n (Some mz)). by apply (Ha' n None). - - destruct (Ha None (reflexivity _)) as [_ Ha']. - intros n [[mz|mz|]|] ?; inversion 1; subst; constructor. - by apply (Ha' n (Some mz)). by apply (Ha' n None). + intros Hup n mf ? Ha1; simpl in *. + destruct (Hup n (mf ≫= maybe Cinl)); auto. + { by destruct mf as [[]|]; inversion_clear Ha1. } + split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor. Qed. -Lemma csum_local_update_r (b1 b2 : B) bf : - (∀ bf', bf = Cinr <$> bf' → b1 ~l~> b2 @ bf') → Cinr b1 ~l~> Cinr b2 @ bf. +Lemma csum_local_update_r (b1 b2 b1' b2' : B) : + (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2'). Proof. - intros Hb. split; destruct bf as [[|bf'|]|]=>//=. - - by eapply (Hb (Some bf')). - - by eapply (Hb None). - - destruct (Hb (Some bf') (reflexivity _)) as [_ Hb']. - intros n [[mz|mz|]|] ?; inversion 1; subst; constructor. - by apply (Hb' n (Some mz)). by apply (Hb' n None). - - destruct (Hb None (reflexivity _)) as [_ Hb']. - intros n [[mz|mz|]|] ?; inversion 1; subst; constructor. - by apply (Hb' n (Some mz)). by apply (Hb' n None). + intros Hup n mf ? Ha1; simpl in *. + destruct (Hup n (mf ≫= maybe Cinr)); auto. + { by destruct mf as [[]|]; inversion_clear Ha1. } + split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor. Qed. End cmra. diff --git a/algebra/gmap.v b/algebra/gmap.v index c679e97819295b1b8429daf3f58334ca94646aad..42f430f56ce5976c42b24ee1e1bdf3bbbd5f620f 100644 --- a/algebra/gmap.v +++ b/algebra/gmap.v @@ -378,50 +378,63 @@ Section freshness. Qed. End freshness. -Lemma insert_local_update m i x y mf : - x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf. +Lemma alloc_local_update m1 m2 i x : + m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2). Proof. - intros [Hxy Hxy']; split. - - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy. - + by rewrite !lookup_opM !lookup_insert_ne. - - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j). - destruct (decide (i = j)); subst. - + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'. - + by rewrite !lookup_opM !lookup_insert_ne. -Qed. - -Lemma singleton_local_update i x y mf : - x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf. -Proof. apply insert_local_update. Qed. - -Lemma alloc_singleton_local_update m i x mf : - (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf. + rewrite cmra_valid_validN=> Hi ?. + apply local_update_unital=> n mf Hmv Hm; simpl in *. + split; auto using insert_validN. + intros j; destruct (decide (i = j)) as [->|]. + - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj]. + by rewrite lookup_op !lookup_insert Hj. + - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //. +Qed. + +Lemma alloc_singleton_local_update m i x : + m !! i = None → ✓ x → (m,∅) ~l~> (<[i:=x]>m, {[ i:=x ]}). +Proof. apply alloc_local_update. Qed. + +Lemma insert_local_update m1 m2 i x y x' y' : + m1 !! i = Some x → m2 !! i = Some y → + (x, y) ~l~> (x', y') → + (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2). Proof. - rewrite lookup_opM op_None=> -[Hi Hif] ?. - rewrite insert_singleton_op // comm. apply alloc_local_update. - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi. - by apply cmra_valid_validN. - - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id. + intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *. + destruct (Hup n (mf !! i)) as [? Hx']; simpl in *. + { move: (Hmv i). by rewrite Hi1. } + { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). } + split; auto using insert_validN. + rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|]. + - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM. + - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne. +Qed. + +Lemma singleton_local_update m i x y x' y' : + m !! i = Some x → + (x, y) ~l~> (x', y') → + (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}). +Proof. + intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y). + eapply insert_local_update; eauto using lookup_insert. Qed. -Lemma alloc_unit_singleton_local_update i x mf : - mf ≫= (!! i) = None → ✓ x → (∅:gmap K A) ~l~> {[ i := x ]} @ mf. +Lemma delete_local_update m1 m2 i x `{!Exclusive x} : + m2 !! i = Some x → (m1, m2) ~l~> (delete i m1, delete i m2). Proof. - intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi. + intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *. + split; auto using delete_validN. + rewrite Hm=> j; destruct (decide (i = j)) as [<-|]. + - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None. + apply eq_None_not_Some=> -[y Hi']. + move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l. + - by rewrite lookup_op !lookup_delete_ne // lookup_op. Qed. -Lemma delete_local_update m i x `{!Exclusive x} mf : - m !! i = Some x → m ~l~> delete i m @ mf. +Lemma delete_singleton_local_update m i x `{!Exclusive x} : + (m, {[ i := x ]}) ~l~> (delete i m, ∅). Proof. - intros Hx; split; [intros n; apply delete_update|]. - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j). - destruct (decide (i = j)); subst. - + rewrite !lookup_opM !lookup_delete Hx=> ? Hj. - rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //. - by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj. - + by rewrite !lookup_opM !lookup_delete_ne. + rewrite -(delete_singleton i x). + eapply delete_local_update; eauto using lookup_singleton. Qed. End properties. diff --git a/algebra/gset.v b/algebra/gset.v index 8cc7816168cf6413cd6407b2b2068420272a5766..5fa902142b87cbf38668e4f52e6f0a6b19c555f2 100644 --- a/algebra/gset.v +++ b/algebra/gset.v @@ -47,16 +47,15 @@ Section gset. Lemma gset_update X Y : X ~~> Y. Proof. done. Qed. - Lemma gset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf. + Lemma gset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X'). Proof. intros (Z&->&?)%subseteq_disjoint_union_L. - intros; apply local_update_total; split; [done|]; simpl. - intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. + rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->. + split. done. rewrite gset_op_union. set_solver. Qed. Global Instance gset_persistent X : Persistent X. Proof. by apply persistent_total; rewrite gset_core_self. Qed. - End gset. Arguments gsetR _ {_ _}. @@ -72,6 +71,8 @@ Arguments GSetBot {_ _ _}. Section gset_disj. Context `{Countable K}. Arguments op _ _ !_ !_ /. + Arguments cmra_op _ !_ !_ /. + Arguments ucmra_op _ !_ !_ /. Canonical Structure gset_disjC := leibnizC (gset_disj K). @@ -174,35 +175,45 @@ Section gset_disj. Proof. eauto using gset_disj_alloc_empty_updateP. Qed. End fresh_updates. - Lemma gset_disj_dealloc_local_update X Y Xf : - GSet X ~l~> GSet (X ∖ Y) @ Some (GSet Xf). + Lemma gset_disj_dealloc_local_update X Y : + (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), ∅). + Proof. + apply local_update_total_valid=> _ _ /gset_disj_included HYX. + rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=. + rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done]. + by rewrite difference_union_distr_l_L + difference_diag_L !left_id_L difference_disjoint_L. + Qed. + Lemma gset_disj_dealloc_empty_local_update X Z : + (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X,∅). Proof. - apply local_update_total; split; simpl. - { rewrite !gset_disj_valid_op; set_solver. } - intros mZ ?%gset_disj_valid_op. rewrite gset_disj_union //. - destruct mZ as [[Z|]|]; simpl; try done. - - rewrite {1}/op {1}/cmra_op /=. destruct (decide _); simpl; try done. - intros [=]. do 2 f_equal. by apply union_cancel_l_L with X. - - intros [=]. assert (Xf = ∅) as -> by set_solver. by rewrite right_id. + apply local_update_total_valid=> /gset_disj_valid_op HZX _ _. + assert (X = (Z ∪ X) ∖ Z) as HX by set_solver. + rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update. Qed. - Lemma gset_disj_dealloc_empty_local_update X Xf : - GSet X ~l~> GSet ∅ @ Some (GSet Xf). + Lemma gset_disj_dealloc_op_local_update X Y Z : + (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y) ~l~> (GSet X,GSet Y). Proof. - rewrite -(difference_diag_L X). apply gset_disj_dealloc_local_update. + rewrite -{2}(left_id ∅ _ (GSet Y)). + apply op_local_update_frame, gset_disj_dealloc_empty_local_update. Qed. - Lemma gset_disj_alloc_local_update X i Xf : - i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf). + Lemma gset_disj_alloc_op_local_update X Y Z : + Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y). + Proof. + intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op. + Qed. + Lemma gset_disj_alloc_local_update X Y Z : + Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet (Z ∪ X), GSet (Z ∪ Y)). Proof. - intros ??; apply local_update_total; split; simpl. - - rewrite !gset_disj_valid_op; set_solver. - - intros mZ ?%gset_disj_valid_op HXf. - rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. + intros. apply local_update_total_valid=> _ _ /gset_disj_included ?. + rewrite -!gset_disj_union //; last set_solver. + auto using gset_disj_alloc_op_local_update. Qed. - Lemma gset_disj_alloc_empty_local_update i Xf : - i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf). + Lemma gset_disj_alloc_empty_local_update X Z : + Z ⊥ X → (GSet X, GSet ∅) ~l~> (GSet (Z ∪ X), GSet Z). Proof. - intros. rewrite -(right_id_L _ _ {[i]}). + intros. rewrite -{2}(right_id_L _ union Z). apply gset_disj_alloc_local_update; set_solver. Qed. End gset_disj. diff --git a/algebra/list.v b/algebra/list.v index b37c75a3fa0f678507355f2aee651136a9850198..c9bd4bfcf242c7c0937b4ad3ad7409397cbc4a38 100644 --- a/algebra/list.v +++ b/algebra/list.v @@ -398,6 +398,7 @@ Section properties. rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst. Qed. +(* FIXME Lemma list_middle_local_update l1 l2 x y ml : x ~l~> y @ ml ≫= (!! length l1) → l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml. @@ -421,6 +422,7 @@ Section properties. Lemma list_singleton_local_update i x y ml : x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml. Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. +*) End properties. (** Functor *) diff --git a/algebra/local_updates.v b/algebra/local_updates.v index efc3df3dec8179042bec984ca195b669491d3e8f..7ed0d5d35d4e991d981bf12cbc2fe553f8270058 100644 --- a/algebra/local_updates.v +++ b/algebra/local_updates.v @@ -1,100 +1,159 @@ From iris.algebra Require Export cmra. (** * Local updates *) -Record local_update {A : cmraT} (mz : option A) (x y : A) := { - local_update_valid n : ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz); - local_update_go n mz' : - ✓{n} (x ⋅? mz) → x ⋅? mz ≡{n}≡ x ⋅? mz' → y ⋅? mz ≡{n}≡ y ⋅? mz' -}. -Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70). +Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz, + ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz. Instance: Params (@local_update) 1. +Infix "~l~>" := local_update (at level 70). Section updates. -Context {A : cmraT}. -Implicit Types x y : A. + Context {A : cmraT}. + Implicit Types x y : A. -Global Instance local_update_proper : - Proper ((≡) ==> (≡) ==> (≡) ==> iff) (@local_update A). -Proof. - cut (Proper ((≡) ==> (≡) ==> (≡) ==> impl) (@local_update A)). - { intros Hproper; split; by apply Hproper. } - intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto. -Qed. + Global Instance local_update_proper : + Proper ((≡) ==> (≡) ==> iff) (@local_update A). + Proof. unfold local_update. by repeat intro; setoid_subst. Qed. -Global Instance local_update_preorder mz : PreOrder (@local_update A mz). -Proof. - split. - - intros x; by split. - - intros x1 x2 x3 [??] [??]; split; eauto. -Qed. + Global Instance local_update_preorder : PreOrder (@local_update A). + Proof. split; unfold local_update; red; naive_solver. Qed. -Lemma exclusive_local_update `{!Exclusive x} y mz : ✓ y → x ~l~> y @ mz. -Proof. - split; intros n. - - move=> /exclusiveN_opM ->. by apply cmra_valid_validN. - - intros mz' ? Hmz. - by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz. -Qed. + Lemma exclusive_local_update `{!Exclusive y} x x' : ✓ x' → (x,y) ~l~> (x',x'). + Proof. + intros ? n mz Hxv Hx; simpl in *. + move: Hxv; rewrite Hx; move=> /exclusiveN_opM=> ->; split; auto. + by apply cmra_valid_validN. + Qed. -Lemma op_local_update x1 x2 y mz : - x1 ~l~> x2 @ Some (y ⋅? mz) → x1 ⋅ y ~l~> x2 ⋅ y @ mz. -Proof. - intros [Hv1 H1]; split. - - intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto. - - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto. -Qed. + Lemma op_local_update x y z : + (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y). + Proof. + intros Hv n mz Hxv Hx; simpl in *; split; [by auto|]. + by rewrite Hx -cmra_opM_assoc. + Qed. + Lemma op_local_update_discrete `{!CMRADiscrete A} x y z : + (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y). + Proof. + intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n). + Qed. -Lemma alloc_local_update x y mz : - (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ~l~> x ⋅ y @ mz. -Proof. - split; first done. - intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->. -Qed. + Lemma op_local_update_frame x y x' y' yf : + (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf). + Proof. + intros Hup n mz Hxv Hx; simpl in *. + destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_opM_assoc|]. + by rewrite cmra_opM_assoc. + Qed. -Lemma local_update_total `{CMRADiscrete A} x y mz : - x ~l~> y @ mz ↔ - (✓ (x ⋅? mz) → ✓ (y ⋅? mz)) ∧ - (∀ mz', ✓ (x ⋅? mz) → x ⋅? mz ≡ x ⋅? mz' → y ⋅? mz ≡ y ⋅? mz'). -Proof. - split. - - destruct 1. split; intros until 0; - rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto. - - intros [??]; split; intros until 0; - rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto. -Qed. + Lemma local_update_discrete `{!CMRADiscrete A} (x y x' y' : A) : + (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz. + Proof. + rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff. + setoid_rewrite <-(λ n, timeless_iff n x). + setoid_rewrite <-(λ n, timeless_iff n x'). naive_solver eauto using 0. + Qed. + + Lemma local_update_valid0 x y x' y' : + (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) → + (x,y) ~l~> (x',y'). + Proof. + intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto. + - by apply (cmra_validN_le n); last lia. + - apply (cmra_validN_le n); last lia. + move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l. + - destruct mz as [z|]. + + right. exists z. apply dist_le with n; auto with lia. + + left. apply dist_le with n; auto with lia. + Qed. + Lemma local_update_valid `{!CMRADiscrete A} x y x' y' : + (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y'). + Proof. + rewrite !(cmra_discrete_valid_iff 0) + (cmra_discrete_included_iff 0) (timeless_iff 0). + apply local_update_valid0. + Qed. + + Lemma local_update_total_valid0 `{!CMRATotal A} x y x' y' : + (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y'). + Proof. + intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto. + by rewrite Hx. + Qed. + Lemma local_update_total_valid `{!CMRATotal A, !CMRADiscrete A} x y x' y' : + (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y'). + Proof. + rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0). + apply local_update_total_valid0. + Qed. End updates. +Section updates_unital. + Context {A : ucmraT}. + Implicit Types x y : A. + + Lemma local_update_unital x y x' y' : + (x,y) ~l~> (x',y') ↔ ∀ n z, + ✓{n} x → x ≡{n}≡ y ⋅ z → ✓{n} x' ∧ x' ≡{n}≡ y' ⋅ z. + Proof. + split. + - intros Hup n z. apply (Hup _ (Some z)). + - intros Hup n [z|]; simpl; [by auto|]. + rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto. + Qed. + + Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) : + (x,y) ~l~> (x',y') ↔ ∀ z, ✓ x → x ≡ y ⋅ z → ✓ x' ∧ x' ≡ y' ⋅ z. + Proof. + rewrite local_update_discrete. split. + - intros Hup z. apply (Hup (Some z)). + - intros Hup [z|]; simpl; [by auto|]. + rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto. + Qed. +End updates_unital. + (** * Product *) -Lemma prod_local_update {A B : cmraT} (x y : A * B) mz : - x.1 ~l~> y.1 @ fst <$> mz → x.2 ~l~> y.2 @ snd <$> mz → - x ~l~> y @ mz. +Lemma prod_local_update {A B : cmraT} (x y x' y' : A * B) : + (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) → + (x,y) ~l~> (x',y'). Proof. - intros [Hv1 H1] [Hv2 H2]; split. - - intros n [??]; destruct mz; split; auto. - - intros n mz' [??] [??]. - specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')). - destruct mz, mz'; split; naive_solver. + intros Hup1 Hup2 n mz [??] [??]; simpl in *. + destruct (Hup1 n (fst <$> mz)); [done|by destruct mz|]. + destruct (Hup2 n (snd <$> mz)); [done|by destruct mz|]. + by destruct mz. Qed. +Lemma prod_local_update' {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) : + (x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') → + ((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')). +Proof. intros. by apply prod_local_update. Qed. +Lemma prod_local_update_1 {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 : B) : + (x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)). +Proof. intros. by apply prod_local_update. Qed. +Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) : + (x2,y2) ~l~> (x2',y2') → ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')). +Proof. intros. by apply prod_local_update. Qed. + (** * Option *) -Lemma option_local_update {A : cmraT} (x y : A) mmz : - x ~l~> y @ mjoin mmz → - Some x ~l~> Some y @ mmz. +Lemma option_local_update {A : cmraT} (x y x' y' : A) : + (x, y) ~l~> (x',y') → + (Some x, Some y) ~l~> (Some x', Some y'). Proof. - intros [Hv H]; split; first destruct mmz as [[?|]|]; auto. - intros n mmz'. specialize (H n (mjoin mmz')). - destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto. + intros Hup n mmz Hxv Hx; simpl in *. + destruct (Hup n (mjoin mmz)); first done. + { destruct mmz as [[?|]|]; inversion_clear Hx; auto. } + split; first done. destruct mmz as [[?|]|]; constructor; auto. Qed. (** * Natural numbers *) -Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz. +Lemma nat_local_update (x y x' y' : nat) : + x + y' = x' + y → (x,y) ~l~> (x',y'). Proof. - split; first done. - compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia. + intros ??; apply local_update_unital_discrete=> z _. + compute -[minus plus]; lia. Qed. -Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ~l~> y @ mz. +Lemma mnat_local_update (x y x' : mnatUR) : + x ≤ x' → (x,y) ~l~> (x',x'). Proof. - split; first done. - compute -[max]; destruct mz as [z|]; intros n [z'|]; lia. + intros ??; apply local_update_unital_discrete=> z _. + compute -[max]; lia. Qed. diff --git a/algebra/updates.v b/algebra/updates.v index 012b53aaf66606f877c73f55928fbf253fc5b368..cdb1fc2d9fc1c00ab0f4de2a2918975f6f4db987 100644 --- a/algebra/updates.v +++ b/algebra/updates.v @@ -76,8 +76,7 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 Proof. rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. Qed. -Lemma cmra_update_valid0 x y : - (✓{0} x → x ~~> y) → x ~~> y. +Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y. Proof. intros H n mz Hmz. apply H, Hmz. apply (cmra_validN_le n); last lia. diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v index a5c116b0b47b4a442b3e5a154962cea0449f9f31..a5e84e8d0a15c643fa9c741bd741ad4a8f0234fe 100644 --- a/heap_lang/adequacy.v +++ b/heap_lang/adequacy.v @@ -1,18 +1,28 @@ From iris.program_logic Require Export weakestpre adequacy. From iris.heap_lang Require Export heap. -From iris.program_logic Require Import auth ownership. +From iris.algebra Require Import auth. +From iris.program_logic Require Import ownership. From iris.heap_lang Require Import proofmode notation. From iris.proofmode Require Import tactics. -Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang]. +Class heapPreG Σ := HeapPreG { + heap_preG_iris :> irisPreG heap_lang Σ; + heap_preG_heap :> inG Σ (authR heapUR) +}. -Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ : +Definition heapΣ : gFunctors := + #[irisΣ heap_lang; GFunctor (constRF (authR heapUR))]. +Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ. +Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed. + +Definition heap_adequacy Σ `{heapPreG Σ} e σ φ : (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■φ v }}) → adequate e σ φ. Proof. intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ". - iVs (auth_alloc (ownP ∘ of_heap) heapN _ (to_heap σ) with "[Hσ]") as (γ) "[??]". - - auto using to_heap_valid. - - rewrite /= (from_to_heap σ); auto. - - iApply (Hwp (HeapG _ _ _ γ)). by rewrite /heap_ctx. + iVs (own_alloc (◠to_heap σ)) as (γ) "Hh". + { apply (auth_auth_valid (to_heap _)), to_heap_valid. } + set (Hheap := HeapG _ _ _ γ). + iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|]. + iApply (Hwp _). by rewrite /heap_ctx. Qed. \ No newline at end of file diff --git a/heap_lang/heap.v b/heap_lang/heap.v index 11f538b90a1df728df488309130a7f3fed1b236e..5401d24f4bfbf2f8c7cac3a47e8bfcc9ab5f6e71 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -1,7 +1,7 @@ From iris.heap_lang Require Export lifting. -From iris.algebra Require Import upred_big_op gmap frac dec_agree. +From iris.algebra Require Import auth gmap frac dec_agree. From iris.program_logic Require Export invariants ghost_ownership. -From iris.program_logic Require Import ownership auth. +From iris.program_logic Require Import ownership. From iris.proofmode Require Import tactics. Import uPred. (* TODO: The entire construction could be generalized to arbitrary languages that have @@ -14,32 +14,24 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)). (** The CMRA we need. *) Class heapG Σ := HeapG { heapG_iris_inG :> irisG heap_lang Σ; - heap_inG :> authG Σ heapUR; + heap_inG :> inG Σ (authR heapUR); heap_name : gname }. (** The Functor we need. *) Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)). -Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd). Section definitions. Context `{heapG Σ}. Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := - auth_own heap_name {[ l := (q, DecAgree v) ]}. + own heap_name (◯ {[ l := (q, DecAgree v) ]}). Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed. Definition heap_mapsto := proj1_sig heap_mapsto_aux. Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := proj2_sig heap_mapsto_aux. - Definition heap_inv (h : heapUR) : iProp Σ := - ownP (of_heap h). - Definition heap_ctx : iProp Σ := - auth_ctx heap_name heapN heap_inv. - - Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv. - Proof. solve_proper. Qed. - Global Instance heap_ctx_persistent : PersistentP heap_ctx. - Proof. apply _. Qed. + Definition heap_inv : iProp Σ := (∃ σ, ownP σ ★ own heap_name (◠to_heap σ))%I. + Definition heap_ctx : iProp Σ := inv heapN heap_inv. End definitions. Typeclasses Opaque heap_ctx heap_mapsto. @@ -57,57 +49,38 @@ Section heap. Implicit Types h g : heapUR. (** Conversion to heaps and back *) - Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap. - Proof. solve_proper. Qed. - Lemma from_to_heap σ : of_heap (to_heap σ) = σ. - Proof. - apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l). - Qed. Lemma to_heap_valid σ : ✓ to_heap σ. Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed. - Lemma of_heap_insert l v h : - of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h). - Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed. - Lemma of_heap_singleton_op l q v h : - ✓ ({[l := (q, DecAgree v)]} ⋅ h) → - of_heap ({[l := (q, DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h). + Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None. + Proof. by rewrite /to_heap lookup_fmap=> ->. Qed. + Lemma heap_singleton_included σ l q v : + {[l := (q, DecAgree v)]} ≼ to_heap σ → σ !! l = Some v. Proof. - intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|]. - - move: (Hv l). rewrite /of_heap lookup_insert - lookup_omap (lookup_op _ h) lookup_singleton. - case _:(h !! l)=>[[q' [v'|]]|] //=; last by move=> [??]. - move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp. - - rewrite /of_heap lookup_insert_ne // !lookup_omap. - by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L. + rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]]. + move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst. + by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->]. Qed. - Lemma to_heap_insert l v σ : - to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ). - Proof. by rewrite /to_heap -fmap_insert. Qed. - Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None. + Lemma heap_singleton_included' σ l q v : + {[l := (q, DecAgree v)]} ≼ to_heap σ → to_heap σ !! l = Some (1%Qp,DecAgree v). Proof. - move=> /(_ l). rewrite /of_heap lookup_omap. - by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto. + intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl. Qed. - Lemma heap_store_valid l h v1 v2 : - ✓ ({[l := (1%Qp, DecAgree v1)]} ⋅ h) → - ✓ ({[l := (1%Qp, DecAgree v2)]} ⋅ h). - Proof. - intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|]. - - rewrite !lookup_op !lookup_singleton. - by case: (h !! l)=> [x|] // /Some_valid/exclusive_l. - - by rewrite !lookup_op !lookup_singleton_ne. - Qed. - Hint Resolve heap_store_valid. + Lemma to_heap_insert l v σ : + to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ). + Proof. by rewrite /to_heap fmap_insert. Qed. Context `{heapG Σ}. (** General properties of mapsto *) + Global Instance heap_ctx_persistent : PersistentP heap_ctx. + Proof. rewrite /heap_ctx. apply _. Qed. Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v). Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed. Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v. Proof. - by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. + by rewrite heap_mapsto_eq + -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp. Qed. Lemma heap_mapsto_op l q1 q2 v1 v2 : @@ -115,11 +88,10 @@ Section heap. Proof. destruct (decide (v1 = v2)) as [->|]. { by rewrite heap_mapsto_op_eq pure_equiv // left_id. } - rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //. apply (anti_symm (⊢)); last by apply pure_elim_l. - rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton. - rewrite option_validI prod_validI !discrete_valid /=. - by apply pure_elim_r. + rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. + eapply pure_elim; [done|]=> /auth_own_valid /=. + rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros []. Qed. Lemma heap_mapsto_op_1 l q1 q2 v1 v2 : @@ -140,15 +112,14 @@ Section heap. heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}. Proof. iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx. - iVs (auth_empty heap_name) as "Hh". - iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto. - rewrite left_id_L /heap_inv. iDestruct "Hv" as %?. - iApply wp_alloc_pst. iFrame "Hh". iNext. - iIntros (l) "[% Hh] !==>". - iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]"). - { rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None. - iFrame "Hh". iPureIntro. - by apply alloc_unit_singleton_local_update; first apply of_heap_None. } + iInv heapN as (σ) ">[Hσ Hh] " "Hclose". + iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>". + iVs (own_update with "Hh") as "[Hh H]". + { apply auth_update_alloc, + (alloc_singleton_local_update _ l (1%Qp,DecAgree v)); + by auto using lookup_to_heap_None. } + iVs ("Hclose" with "[Hσ Hh]") as "_". + { iNext. iExists (<[l:=v]> σ). rewrite to_heap_insert. by iFrame. } iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def. Qed. @@ -157,14 +128,13 @@ Section heap. heap_ctx ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}. Proof. - iIntros (?) "[#Hinv [Hl HΦ]]". + iIntros (?) "[#Hinv [>Hl HΦ]]". rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. - iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto. - rewrite /heap_inv. - iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert. - rewrite of_heap_singleton_op //. iFrame "Hl". - iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]"). - { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. } + iInv heapN as (σ) ">[Hσ Hh] " "Hclose". + iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2. + iApply (wp_load_pst _ σ); first eauto using heap_singleton_included. + iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_". + { iNext. iExists σ. by iFrame. } by iApply "HΦ". Qed. @@ -173,17 +143,18 @@ Section heap. heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit)) ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. Proof. - iIntros (<-%of_to_val ?) "[#Hinv [Hl HΦ]]". + iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]". rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. - iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto. - rewrite /heap_inv. - iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. - rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". - iIntros "!> Hl !==>". - iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]"). - { iSplit. - - iPureIntro; by apply singleton_local_update, exclusive_local_update. - - rewrite of_heap_singleton_op //; eauto. } + iInv heapN as (σ) ">[Hσ Hh] " "Hclose". + iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2. + iApply (wp_store_pst _ σ); first eauto using heap_singleton_included. + iIntros "{$Hσ} !> Hσ !==>". + iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]". + { eapply auth_update, singleton_local_update, + (exclusive_local_update _ (1%Qp, DecAgree v)); last done. + by eapply heap_singleton_included'. } + iVs ("Hclose" with "[Hσ Hh]") as "_". + { iNext. iExists (<[l:=v]>σ). rewrite to_heap_insert. iFrame. } by iApply "HΦ". Qed. @@ -192,14 +163,13 @@ Section heap. heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false))) ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. Proof. - iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]". + iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]". rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. - iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto. - rewrite /heap_inv. - iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. - rewrite of_heap_singleton_op //. iFrame "Hl". - iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]"). - { iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. } + iInv heapN as (σ) ">[Hσ Hh] " "Hclose". + iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2. + iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|]. + iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_". + { iNext. iExists σ. by iFrame. } by iApply "HΦ". Qed. @@ -208,17 +178,18 @@ Section heap. heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true))) ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. Proof. - iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]". + iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]". rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. - iVs (auth_open with "[Hl]") as (h) "[% [Hl Hclose]]"; eauto. - rewrite /heap_inv. - iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //. - rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". - iIntros "!> Hl !==>". - iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]"). - { iSplit. - - iPureIntro; by apply singleton_local_update, exclusive_local_update. - - rewrite of_heap_singleton_op //; eauto. } + iInv heapN as (σ) ">[Hσ Hh] " "Hclose". + iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2. + iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included. + iIntros "{$Hσ} !> Hσ !==>". + iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]". + { eapply auth_update, singleton_local_update, + (exclusive_local_update _ (1%Qp, DecAgree v2)); last done. + by eapply heap_singleton_included'. } + iVs ("Hclose" with "[Hσ Hh]") as "_". + { iNext. iExists (<[l:=v2]>σ). rewrite to_heap_insert. iFrame. } by iApply "HΦ". Qed. End heap. diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 96769c478f0c081dcbdfdb10937bdeb72ed18f20..2b8c7575b376d95bf36af8ac98d07010f99760c3 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -1,7 +1,7 @@ From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang. From iris.proofmode Require Import tactics. -From iris.program_logic Require Import auth. +From iris.algebra Require Import frac auth. From iris.heap_lang Require Import proofmode notation. Definition newcounter : val := λ: <>, ref #0. @@ -12,76 +12,160 @@ Definition inc : val := Definition read : val := λ: "l", !"l". Global Opaque newcounter inc get. -(** The CMRA we need. *) -Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }. -Definition counterΣ : gFunctors := #[authΣ mnatUR]. - -Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ. -Proof. intros [? _]%subG_inv. split; apply _. Qed. - -Section proof. -Context `{!heapG Σ, !counterG Σ} (N : namespace). - -Definition counter_inv (l : loc) (n : mnat) : iProp Σ := (l ↦ #n)%I. - -Definition counter (l : loc) (n : nat) : iProp Σ := - (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ - auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I. - -(** The main proofs. *) -Global Instance counter_persistent l n : PersistentP (counter l n). -Proof. apply _. Qed. - -Lemma newcounter_spec (R : iProp Σ) Φ : - heapN ⊥ N → - heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}. -Proof. - iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". - iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]") - as (γ) "[#? Hγ]"; try by auto. - iVsIntro. iApply "HΦ". rewrite /counter; eauto 10. -Qed. - -Lemma inc_spec l j (Φ : val → iProp Σ) : - counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}. -Proof. - iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. - iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)". - wp_bind (! _)%E. - iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto. - rewrite {2}/counter_inv. - wp_load. iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto. - iVsIntro. wp_let; wp_op. wp_bind (CAS _ _ _). - iVs (auth_open (counter_inv l) with "[Hγf]") as (j'') "(% & Hl & Hclose)"; auto. - rewrite {2}/counter_inv. - destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj]. - - wp_cas_suc; first (by do 3 f_equal). - iVs ("Hclose" $! (1 + j `max` j')%nat with "[Hl]") as "Hγf". - { iSplit; [iPureIntro|iNext]. - { apply mnat_local_update. abstract lia. } - rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia. - by rewrite Nat2Z.inj_succ -Z.add_1_l. } - iVsIntro. wp_if. - iVsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto. - iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia. - - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]). - iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto. - iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10. -Qed. - -Lemma read_spec l j (Φ : val → iProp Σ) : - counter l j ★ (∀ i, ■(j ≤ i)%nat → counter l i -★ Φ #i) - ⊢ WP read #l {{ Φ }}. -Proof. - iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)". - rewrite /read /=. wp_let. - iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto. - wp_load. - iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf". - { iSplit; [iPureIntro|iNext]. - { apply mnat_local_update; abstract lia. } - by rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent. } - iVsIntro. rewrite !mnat_op_max. - iApply ("HΦ" with "[%]"); first abstract lia. rewrite /counter; eauto 10. -Qed. -End proof. +(** Monotone counter *) +Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }. +Definition mcounterΣ : gFunctors := #[GFunctor (constRF (authR mnatUR))]. + +Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ. +Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. + +Section mono_proof. + Context `{!heapG Σ, !mcounterG Σ} (N : namespace). + + Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ := + (∃ n, own γ (◠(n : mnat)) ★ l ↦ #n)%I. + + Definition mcounter (l : loc) (n : nat) : iProp Σ := + (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ + inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I. + + (** The main proofs. *) + Global Instance mcounter_persistent l n : PersistentP (mcounter l n). + Proof. apply _. Qed. + + Lemma newcounter_mono_spec (R : iProp Σ) Φ : + heapN ⊥ N → + heap_ctx ★ (∀ l, mcounter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}. + Proof. + iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". + iVs (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done. + iVs (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]"). + { iNext. iExists 0%nat. by iFrame. } + iVsIntro. iApply "HΦ". rewrite /mcounter; eauto 10. + Qed. + + Lemma inc_mono_spec l n (Φ : val → iProp Σ) : + mcounter l n ★ (mcounter l (S n) -★ Φ #()) ⊢ WP inc #l {{ Φ }}. + Proof. + iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. + iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)". + wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose". + wp_load. iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. + iVsIntro. wp_let. wp_op. + wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose". + destruct (decide (c' = c)) as [->|]. + - iDestruct (own_valid_2 with "[$Hγ $Hγf]") + as %[?%mnat_included _]%auth_valid_discrete_2. + iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". + { apply auth_update, (mnat_local_update _ _ (S c)); auto. } + wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]") as "_". + { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } + iVsIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto. + iApply (own_mono with "Hγf"). apply: auth_frag_mono. + by apply mnat_included, le_n_S. + - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). + iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|]. + iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). + rewrite {3}/mcounter; eauto 10. + Qed. + + Lemma read_mono_spec l j (Φ : val → iProp Σ) : + mcounter l j ★ (∀ i, ■(j ≤ i)%nat → mcounter l i -★ Φ #i) + ⊢ WP read #l {{ Φ }}. + Proof. + iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)". + rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + iDestruct (own_valid_2 with "[$Hγ $Hγf]") + as %[?%mnat_included _]%auth_valid_discrete_2. + iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". + { apply auth_update, (mnat_local_update _ _ c); auto. } + iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. + iApply ("HΦ" with "[%]"); rewrite /mcounter; eauto 10. + Qed. +End mono_proof. + +(** Counter with contributions *) +Class ccounterG Σ := + CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }. +Definition ccounterΣ : gFunctors := + #[GFunctor (constRF (authR (optionUR (prodR fracR natR))))]. + +Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ. +Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. + +Section contrib_spec. + Context `{!heapG Σ, !ccounterG Σ} (N : namespace). + + Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ := + (∃ n, own γ (◠Some (1%Qp, n)) ★ l ↦ #n)%I. + + Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ := + (heapN ⊥ N ∧ heap_ctx ∧ inv N (ccounter_inv γ l))%I. + + Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ := + own γ (◯ Some (q, n)). + + (** The main proofs. *) + Lemma ccounter_op γ q1 q2 n1 n2 : + ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1★ ccounter γ q2 n2. + Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed. + + Lemma newcounter_contrib_spec (R : iProp Σ) Φ : + heapN ⊥ N → + heap_ctx ★ (∀ γ l, ccounter_ctx γ l ★ ccounter γ 1 0 -★ Φ #l) + ⊢ WP newcounter #() {{ Φ }}. + Proof. + iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". + iVs (own_alloc (◠(Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat)))) + as (γ) "[Hγ Hγ']"; first done. + iVs (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]"). + { iNext. iExists 0%nat. by iFrame. } + iVsIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10. + Qed. + + Lemma inc_contrib_spec γ l q n (Φ : val → iProp Σ) : + ccounter_ctx γ l ★ ccounter γ q n ★ (ccounter γ q (S n) -★ Φ #()) + ⊢ WP inc #l {{ Φ }}. + Proof. + iIntros "(#(%&?&?) & Hγf & HΦ)". iLöb as "IH". wp_rec. + wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose". + wp_load. iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. + iVsIntro. wp_let. wp_op. + wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose". + destruct (decide (c' = c)) as [->|]. + - iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". + { apply auth_update, option_local_update, prod_local_update_2. + apply (nat_local_update _ _ (S c) (S n)); omega. } + wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]") as "_". + { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } + iVsIntro. wp_if. by iApply "HΦ". + - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). + iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|]. + iVsIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ"). + Qed. + + Lemma read_contrib_spec γ l q n (Φ : val → iProp Σ) : + ccounter_ctx γ l ★ ccounter γ q n ★ + (∀ c, ■(n ≤ c)%nat → ccounter γ q n -★ Φ #c) + ⊢ WP read #l {{ Φ }}. + Proof. + iIntros "(#(%&?&?) & Hγf & HΦ)". + rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + iDestruct (own_valid_2 with "[$Hγ $Hγf]") + as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2. + iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. + iApply ("HΦ" with "[%]"); rewrite /ccounter; eauto 10. + Qed. + + Lemma read_contrib_spec_1 γ l n (Φ : val → iProp Σ) : + ccounter_ctx γ l ★ ccounter γ 1 n ★ (ccounter γ 1 n -★ Φ #n) + ⊢ WP read #l {{ Φ }}. + Proof. + iIntros "(#(%&?&?) & Hγf & HΦ)". + rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2. + apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done. + iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. + by iApply "HΦ". + Qed. +End contrib_spec. diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v index 157b85465214314825309b46187a2e4b925500fa..2858a093dfbf5ae2f99bb487a928838277f9ece9 100644 --- a/heap_lang/lib/ticket_lock.v +++ b/heap_lang/lib/ticket_lock.v @@ -101,8 +101,7 @@ Section proof. iVsIntro. wp_let. wp_op=>[_|[]] //. wp_if. iVsIntro. iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto. - + iExFalso. iCombine "Ht" "Haown" as "Haown". - iDestruct (own_valid with "Haown") as % [_ ?%gset_disj_valid_op]. + + iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op]. set_solver. - iVs ("Hclose" with "[Hlo Hln Ha]"). { iNext. iExists o, n. by iFrame. } @@ -123,12 +122,10 @@ Section proof. iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose". destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq]. - wp_cas_suc. - iVs (own_update with "Hauth") as "Hauth". - { eapply (auth_update_no_frag _ (∅, _)), prod_local_update, - (gset_disj_alloc_empty_local_update n); [done|]. - rewrite elem_of_seq_set. omega. } - rewrite pair_op left_id_L. iDestruct "Hauth" as "[Hauth Hofull]". - rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0). + iVs (own_update with "Hauth") as "[Hauth Hofull]". + { eapply auth_update_alloc, prod_local_update_2. + eapply (gset_disj_alloc_empty_local_update _ {[ n ]}). + apply (seq_set_S_disjoint 0). } rewrite -(seq_set_S_union_L 0). iVs ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_". { iNext. iExists o', (S n). @@ -137,7 +134,7 @@ Section proof. iApply (wait_loop_spec γ (#lo, #ln)). iFrame "HΦ". rewrite /issued; eauto 10. - wp_cas_fail. - iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]"). + iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_". { iNext. iExists o', n'. by iFrame. } iVsIntro. wp_if. by iApply "IH". Qed. @@ -151,28 +148,20 @@ Section proof. rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E. iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". wp_load. - iAssert (o' = o)%I with "[#]" as "%"; subst. - { iCombine "Hγo" "Hauth" as "Hγo". - by iDestruct (own_valid with "Hγo") (* FIXME: this is horrible *) - as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. } + iDestruct (own_valid_2 with "[$Hauth $Hγo]") as + %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2. iVs ("Hclose" with "[Hlo Hln Hauth Haown]") as "_". { iNext. iExists o, n. by iFrame. } iVsIntro. wp_op. iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". wp_store. - iAssert (o' = o)%I with "[#]" as "%"; subst. - { iCombine "Hγo" "Hauth" as "Hγo". - by iDestruct (own_valid with "Hγo") - as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. } + iDestruct (own_valid_2 with "[$Hauth $Hγo]") as + %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2. iDestruct "Haown" as "[[Hγo' _]|?]". - { iCombine "Hγo" "Hγo'" as "Hγo". - iDestruct (own_valid with "Hγo") as %[[] ?]. } - iCombine "Hauth" "Hγo" as "Hauth". - iVs (own_update with "Hauth") as "Hauth". - { rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *) - apply prod_local_update, reflexivity; simpl. - by apply option_local_update, exclusive_local_update. } - rewrite -pair_split_L. iDestruct "Hauth" as "[Hauth Hγo]". + { iDestruct (own_valid_2 with "[$Hγo $Hγo']") as %[[] ?]. } + iVs (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]". + { apply auth_update, prod_local_update_1. + by apply option_local_update, (exclusive_local_update _ (Excl (S o))). } iVs ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto. iNext. iExists (S o), n'. rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame. diff --git a/program_logic/auth.v b/program_logic/auth.v deleted file mode 100644 index d8a586dbee791e35334a1a899001c7581c64ebf6..0000000000000000000000000000000000000000 --- a/program_logic/auth.v +++ /dev/null @@ -1,109 +0,0 @@ -From iris.program_logic Require Export invariants. -From iris.algebra Require Export auth. -From iris.algebra Require Import gmap. -From iris.proofmode Require Import tactics. -Import uPred. - -(* The CMRA we need. *) -Class authG Σ (A : ucmraT) := AuthG { - auth_inG :> inG Σ (authR A); - auth_discrete :> CMRADiscrete A; -}. -Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ]. - -Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A. -Proof. intros ?%subG_inG ?. by split. Qed. - -Section definitions. - Context `{irisG Λ Σ, authG Σ A} (γ : gname). - Definition auth_own (a : A) : iProp Σ := - own γ (◯ a). - Definition auth_inv (φ : A → iProp Σ) : iProp Σ := - (∃ a, own γ (◠a) ★ φ a)%I. - Definition auth_ctx (N : namespace) (φ : A → iProp Σ) : iProp Σ := - inv N (auth_inv φ). - - Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own. - Proof. solve_proper. Qed. - Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own. - Proof. solve_proper. Qed. - Global Instance auth_own_timeless a : TimelessP (auth_own a). - Proof. apply _. Qed. - Global Instance auth_inv_ne n : - Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv). - Proof. solve_proper. Qed. - Global Instance auth_ctx_ne n N : - Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N). - Proof. solve_proper. Qed. - Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ). - Proof. apply _. Qed. -End definitions. - -Typeclasses Opaque auth_own auth_ctx. -Instance: Params (@auth_inv) 6. -Instance: Params (@auth_own) 6. -Instance: Params (@auth_ctx) 7. - -Section auth. - Context `{irisG Λ Σ, authG Σ A}. - Context (φ : A → iProp Σ) {φ_proper : Proper ((≡) ==> (⊣⊢)) φ}. - Implicit Types N : namespace. - Implicit Types P Q R : iProp Σ. - Implicit Types a b : A. - Implicit Types γ : gname. - - Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b. - Proof. by rewrite /auth_own -own_op auth_frag_op. Qed. - - Global Instance from_sep_own_authM γ a b : - FromSep (auth_own γ (a ⋅ b)) (auth_own γ a) (auth_own γ b) | 90. - Proof. by rewrite /FromSep auth_own_op. Qed. - - Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a. - Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed. - - Global Instance auth_own_persistent γ a : - Persistent a → PersistentP (auth_own γ a). - Proof. rewrite /auth_own. apply _. Qed. - - Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a. - Proof. by rewrite /auth_own own_valid auth_validI. Qed. - - Lemma auth_alloc_strong N E a (G : gset gname) : - ✓ a → ▷ φ a ={E}=> ∃ γ, ■(γ ∉ G) ∧ auth_ctx γ N φ ∧ auth_own γ a. - Proof. - iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. - iVs (own_alloc_strong (Auth (Excl' a) a) G) as (γ) "[% Hγ]"; first done. - iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']". - iVs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"). - { iNext. iExists a. by iFrame. } - iVsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame. - Qed. - - Lemma auth_alloc N E a : - ✓ a → ▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a. - Proof. - iIntros (?) "Hφ". - iVs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; eauto. - Qed. - - Lemma auth_empty γ : True =r=> auth_own γ ∅. - Proof. by rewrite /auth_own -own_empty. Qed. - - Lemma auth_open E N γ a : - nclose N ⊆ E → - auth_ctx γ N φ ★ ▷ auth_own γ a ={E,E∖N}=> ∃ af, - ■✓ (a ⋅ af) ★ ▷ φ (a ⋅ af) ★ ∀ b, - ■(a ~l~> b @ Some af) ★ ▷ φ (b ⋅ af) ={E∖N,E}=★ auth_own γ b. - Proof. - iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own. - iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ". - iDestruct (own_valid with "Hγ") as % [[af Ha'] ?]%auth_valid_discrete. - simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst. - iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done. - iIntros (b) "[% Hφ]". - iVs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto. - iVs ("Hclose" with "[Hφ Hγ]") as "_"; auto. - iNext. iExists (b ⋅ af). by iFrame. - Qed. -End auth. diff --git a/program_logic/boxes.v b/program_logic/boxes.v index f5ea2bb994f955b475c3c54ba75f0c93cd932ca5..57c21b86515ad3f18907f2733943cbdf320fb810 100644 --- a/program_logic/boxes.v +++ b/program_logic/boxes.v @@ -65,10 +65,8 @@ Lemma box_own_auth_update γ b1 b2 b3 : box_own_auth γ (◠Excl' b1) ★ box_own_auth γ (◯ Excl' b2) =r=> box_own_auth γ (◠Excl' b3) ★ box_own_auth γ (◯ Excl' b3). Proof. - rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]". - iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete. - iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity. - by apply auth_update_no_frame, option_local_update, exclusive_local_update. + rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. + by apply auth_update, option_local_update, exclusive_local_update. Qed. Lemma box_own_agree γ Q1 Q2 : diff --git a/program_logic/ownership.v b/program_logic/ownership.v index 6af5bfac1e4b633a7e89222bc4f7c63495042be9..6f3c7fa9bebd445aafc8006748661255f0393f20 100644 --- a/program_logic/ownership.v +++ b/program_logic/ownership.v @@ -67,8 +67,8 @@ Proof. Qed. Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 =r=> ownP_auth σ2 ★ ownP σ2. Proof. - rewrite /ownP -!own_op. by apply own_update, auth_update_no_frame, - option_local_update, exclusive_local_update. + rewrite /ownP -!own_op. + by apply own_update, auth_update, option_local_update, exclusive_local_update. Qed. (* Invariants *) @@ -161,8 +161,8 @@ Proof. as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. } iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?). iVs (own_update with "Hw") as "[Hw HiP]". - { apply (auth_update_no_frag _ {[ i := invariant_unfold P ]}). - apply alloc_unit_singleton_local_update; last done. + { eapply auth_update_alloc, + (alloc_singleton_local_update _ i (invariant_unfold P)); last done. by rewrite /= lookup_fmap HIi. } iVsIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP". iExists (<[i:=P]>I); iSplitL "Hw". diff --git a/tests/barrier_client.v b/tests/barrier_client.v index dac3e09c35a59dce6faa957713e42acca4a7f0ff..abbfe8cbffcb61eadb58e32e62c5acf0e0511a7c 100644 --- a/tests/barrier_client.v +++ b/tests/barrier_client.v @@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang. From iris.heap_lang.lib.barrier Require Import proof. From iris.heap_lang Require Import par. -From iris.program_logic Require Import auth sts saved_prop hoare ownership. From iris.heap_lang Require Import adequacy proofmode. Definition worker (n : Z) : val :=