the resurrection of program_logic/auth

_CoqProject

@@ -78,6 +78,7 @@ 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

heap_lang/heap.v

 From iris.heap_lang Require Export lifting.
 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.
+From iris.program_logic Require Import ownership auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
@@ -14,28 +14,26 @@ 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 :> inG Σ (authR heapUR);
+  heap_inG :> authG Σ heapUR;
   heap_name : gname
 }.
-(** The Functor we need. *)
+
 Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
 
 Section definitions.
   Context `{heapG Σ}.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    own heap_name (◯ {[ l := (q, DecAgree v) ]}).
+    auth_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 : iProp Σ := (∃ σ, ownP σ ★ own heap_name (● to_heap σ))%I.
-  Definition heap_ctx : iProp Σ := inv heapN heap_inv.
+  Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
 End definitions.
 
 Typeclasses Opaque heap_ctx heap_mapsto.
-Instance: Params (@heap_inv) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -79,8 +77,7 @@ Section heap.
 
   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
-      -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
+    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
   Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
@@ -89,8 +86,8 @@ Section heap.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
     apply (anti_symm (⊢)); last by apply pure_elim_l.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
-    eapply pure_elim; [done|]=> /auth_own_valid /=.
+    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
+    eapply pure_elim; [done|] =>  /=.
     rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
   Qed.
 
@@ -112,14 +109,13 @@ 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.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iVs auth_empty as "Ha".
+    (* TODO: Why do I have to give to_heap here? *)
+    iVs (auth_open to_heap with "[Ha]") as (σ) "(%&Hσ&Hcl)"; [done|by iFrame|].
     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. }
+    iVs ("Hcl" $! _ _ with "[Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
     iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
@@ -130,11 +126,10 @@ Section heap.
   Proof.
     iIntros (?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open to_heap with "[Hl]") as (σ) "(%&Hσ&Hcl)"; [done|by iFrame|].
     iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists σ. by iFrame. }
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" $! _ _ with "[Hσ]") as "Ha".
+    { iFrame. iPureIntro. done. }
     by iApply "HΦ".
   Qed.
 
@@ -145,16 +140,12 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open to_heap with "[Hl]") as (σ) "(%&Hσ&Hcl)"; [done|by iFrame|].
     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.
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" $! _ _ with "[Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply singleton_local_update, exclusive_local_update; 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.
 
@@ -165,11 +156,10 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open to_heap with "[Hl]") as (σ) "(%&Hσ&Hcl)"; [done|by iFrame|].
     iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
-    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists σ. by iFrame. }
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" $! _ _ with "[Hσ]") as "Ha".
+    { iFrame. iPureIntro. done. }
     by iApply "HΦ".
   Qed.
 
@@ -180,16 +170,12 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open to_heap with "[Hl]") as (σ) "(%&Hσ&Hcl)"; [done|by iFrame|].
     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.
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" $! _ _ with "[Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply singleton_local_update, exclusive_local_update; 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.

program_logic/auth.v

+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).
+  Context {T : Type}.
+  Definition auth_own (a : A) : iProp Σ :=
+    own γ (◯ a).
+  Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
+    (∃ t, own γ (● f t) ★ φ t)%I.
+  Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
+    inv N (auth_inv f φ).
+
+  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: 
+    Proper (pointwise_relation T (≡) ==>
+            pointwise_relation T (≡) ==> (≡)) (auth_inv).
+  Proof. solve_proper. Qed.
+  Global Instance auth_ctx_ne N :
+    Proper (pointwise_relation T (≡) ==>
+            pointwise_relation T (≡) ==> (≡)) (auth_ctx N).
+  Proof. solve_proper. Qed.
+  Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
+  Proof. apply _. Qed.
+End definitions.
+
+Typeclasses Opaque auth_own auth_inv auth_ctx.
+(* TODO: Not sure what to put here. *)
+Instance: Params (@auth_inv) 5.
+Instance: Params (@auth_own) 4.
+Instance: Params (@auth_ctx) 7.
+
+Section auth.
+  Context `{irisG Λ Σ, authG Σ A}.
+  Context {T : Type} `{!Inhabited T}.
+  Context (f : T → A) (φ : T → iProp Σ).
+  Implicit Types N : namespace.
+  Implicit Types P Q R : iProp Σ.
+  Implicit Types a b : A.
+  Implicit Types t u : T.
+  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 t (G : gset gname) :
+    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+  Proof.
+    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
+    iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
+    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']").
+    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
+    iVsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
+  Qed.
+
+  Lemma auth_alloc N E t :
+    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
+  Proof.
+    iIntros (?) "Hφ".
+    iVs (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
+  Qed.
+
+  Lemma auth_empty γ : True =r=> auth_own γ ∅.
+  Proof. by rewrite /auth_own -own_empty. Qed.
+
+  Lemma auth_acc E γ a :
+    ▷ auth_inv γ f φ ★ auth_own γ a ={E}=> ∃ t,
+      ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
+      ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b.
+  Proof.
+    iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
+    iDestruct "Hinv" as (t) "[>Hγa Hφ]". iVsIntro.
+    iExists t. iCombine "Hγa" "Hγf" as "Hγ".
+    iDestruct (own_valid with "Hγ") as % [? ?]%auth_valid_discrete_2.
+    iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
+    iVs (own_update with "Hγ") as "[Hγa Hγf]".
+    { eapply auth_update. eassumption. }
+    iVsIntro. iFrame. iExists u. iFrame.
+  Qed.
+
+  Lemma auth_open E N γ a :
+    nclose N ⊆ E →
+    auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=> ∃ t,
+      ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
+      ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b.
+  Proof.
+    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
+    (* The following is essentially a very trivial composition of the accessors
+       [auth_acc] and [inv_open] -- but since we don't have any good support
+       for that currently, this gets more tedious than it should, with us having
+       to unpack and repack various proofs.
+       TODO: Make this mostly automatic, by supporting "opening accessors
+       around accessors". *)
+    iVs (auth_acc with "[Hinv Hγf]") as (t) "(?&?&HclAuth)"; first by iFrame.
+    iVsIntro. iExists t. iFrame. iIntros (u b) "H".
+    iVs ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
+  Qed.
+End auth.