introduce a notion oflocal updates (up for discussion) and use it to formulate the auth rules

algebra/auth.v

 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.
+Proof.
+  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.
+Qed.
 End cmra.
 
 Arguments authRA : clear implicits.

algebra/cmra.v

@@ -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.

algebra/excl.v

 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).
+Proof.
+  split.
+  - 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.
+Qed.
+
 End excl.
 
 Arguments exclC : clear implicits.

algebra/fin_maps.v

@@ -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).
+Proof.
+  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.
+Qed.
+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.
 Qed.
+

algebra/option.v

@@ -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).
 Proof.
@@ -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.
 Qed.
+
+(** * 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).
+  Proof.
+    rewrite /local_update_op. split.
+    - move=>? ? ? EQ /=. by rewrite EQ.
+    - move=>a a' n Hlv Hv /=. by rewrite associative.
+  Qed.
+End local_update.
+Arguments LocalUpdate : clear implicits.
+
+

program_logic/auth.v

@@ -58,16 +58,17 @@ Section auth.
     by rewrite sep_elim_l.
   Qed.
 
-  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).
   Proof.
-    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).
   Qed.
 
 End auth.