Commit a21fb68f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of

parents bde0ad00 3a86d2ff
Require Export algebra.excl.
Require Import algebra.functor.
Require Import algebra.functor algebra.option.
Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
......@@ -169,6 +169,18 @@ Qed.
Lemma auth_update_op_r a a' b :
(a b) a a' ~~> (a b) (a' b).
Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
Lemma auth_local_update (L : LocalUpdate A) `{!LocalUpdateSpec L} a a' b :
L a = Some b (b a')
(a a') a ~~> (b a') b.
intros Hlv Hv. apply auth_update=>n af Hab EQ.
split; last done.
apply (injective (R:=()) Some).
rewrite !Some_op -Hlv.
rewrite -!local_update_spec //; eauto; last by rewrite -EQ; [].
by rewrite EQ.
End cmra.
Arguments authRA : clear implicits.
......@@ -384,6 +384,7 @@ Section cmra_monotone.
Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
Require Export algebra.cmra.
Require Import algebra.functor.
Require Import algebra.functor algebra.option.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......@@ -143,6 +143,18 @@ Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
Proof. by destruct y; intros ? [?| |]. Qed.
Lemma excl_updateP (P : excl A Prop) x y : y P y Excl x ~~>: P.
Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
Definition excl_local_update_to (b : A) : LocalUpdate exclRA :=
λ a, if a is Excl _ then Some (Excl b) else None.
Global Instance excl_local_update_to_spec b :
LocalUpdateSpec (excl_local_update_to b).
- move=>? a a' EQ. destruct EQ; done.
- move=>a a' n [b' Hlv] Hv /=. destruct a; try discriminate Hlv; [].
destruct a'; try contradiction Hv; []. reflexivity.
End excl.
Arguments exclC : clear implicits.
......@@ -263,6 +263,7 @@ Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A → Prop) i
~~>: P ~~>: λ m, y, m = {[ i y ]} P y.
Proof. eauto using map_singleton_updateP_empty. Qed.
Section freshness.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma map_updateP_alloc (Q : gmap K A Prop) m x :
x ( i, m !! i = None Q (<[i:=x]>m)) m ~~>: Q.
......@@ -277,6 +278,49 @@ Qed.
Lemma map_updateP_alloc' m x :
x m ~~>: λ m', i, m' = <[i:=x]>m m !! i = None.
Proof. eauto using map_updateP_alloc. Qed.
End freshness.
Section local.
Definition map_local_alloc i x : LocalUpdate (mapRA K A) :=
local_update_op {[ i x ]}.
(* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
then the frame could always own "unit x", and prevent deallocation. *)
Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
Definition map_local_update i : LocalUpdate (mapRA K A) :=
λ m, x m !! i; y L x; Some (<[i:=y]>m).
Global Instance map_local_update_spec i : LocalUpdateSpec (map_local_update i).
rewrite /map_local_update. split.
- (* FIXME Oh wow, this is harder than expected... *)
move=>n f g EQ. move:(EQ i).
case _:(f !! i)=>[fi|]; case _:(g !! i)=>[gi|]; move=>EQi;
inversion EQi; subst; simpl; last done.
assert (EQL : L fi {n} L gi) by (by apply local_update_ne). move: EQL.
case _:(L fi)=>[Lfi|] /=; case _:(L gi)=>[Lgi|]; move=>EQL;
inversion EQL; subst; simpl; last done.
apply Some_ne, insert_ne; done.
- move=>f g n [b Hlv] Hv. rewrite lookup_op. move:Hlv.
case EQf:(f !! i)=>[fi|]; simpl; last discriminate.
case EQL:(L fi)=>[Lfi|]; simpl; last discriminate.
case=>?. subst b.
case EQg:(g !! i)=>[gi|]; simpl.
+ assert (L (fi gi) {n} L fi Some gi) as EQLi.
{ apply local_update_spec; first by eauto.
move:(Hv i). rewrite lookup_op EQf EQg -Some_op. done. }
rewrite EQL -Some_op in EQLi.
destruct (L (fi gi)) as [Lfgi|]; inversion EQLi; subst; simpl.
rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
rewrite EQg -Some_op. apply Some_ne. done.
+ rewrite EQL /=.
rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
by rewrite EQg.
End local.
End properties.
(** Functor *)
......@@ -314,3 +358,4 @@ Next Obligation.
intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
......@@ -82,6 +82,7 @@ Lemma None_includedN n (mx : option A) : None ≼{n} mx.
Proof. rewrite option_includedN; auto. Qed.
Lemma Some_Some_includedN n (x y : A) : x {n} y Some x {n} Some y.
Proof. rewrite option_includedN; eauto 10. Qed.
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Definition option_cmra_mixin : CMRAMixin (option A).
......@@ -186,3 +187,28 @@ Next Obligation.
intros Σ A B C f g x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
(** * Local CMRA Updates *)
(* FIXME: These need the CMRA structure on option, hence they are defined here. Or maybe moe option to cmra.v? *)
(* TODO: Probably needs some more magic flags. What about notation? *)
Section local_update.
Context {A : cmraT}.
(* Do we need more step-indexing here? *)
Definition LocalUpdate := A option A.
Class LocalUpdateSpec (L : LocalUpdate) := {
local_update_ne n :> Proper ((dist n) ==> (dist n)) L;
local_update_spec a b n : is_Some (L a) {n}(a b) L (a b) {n} (L a) Some b
Definition local_update_op (b : A) : LocalUpdate
:= λ a, Some (b a).
Global Instance local_update_op_spec b : LocalUpdateSpec (local_update_op b).
rewrite /local_update_op. split.
- move=>? ? ? EQ /=. by rewrite EQ.
- move=>a a' n Hlv Hv /=. by rewrite associative.
End local_update.
Arguments LocalUpdate : clear implicits.
......@@ -58,16 +58,17 @@ Section auth.
by rewrite sep_elim_l.
Lemma auth_closing a a' b γ :
auth_step (a a') a (b a') b
Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
Lemma auth_closing a a' b γ :
L a = Some b (b a')
(φ (b a') own AuthI γ ( (a a') a))
pvs N N (auth_inv γ auth_own γ b).
intros Hstep. rewrite /auth_inv /auth_own -(exist_intro (b a')).
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (b a')).
rewrite [(_ φ _)%I]commutative -associative.
rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite -own_op. apply own_update.
by apply auth_update.
by apply (auth_local_update L).
End auth.
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