From ab8063db9a49192e671d7c89c8a0a75b4db174af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Oct 2016 10:45:06 +0200
Subject: [PATCH] the resurrection of program_logic/auth

---
 _CoqProject          |   1 +
 heap_lang/heap.v     |  70 +++++++++--------------
 program_logic/auth.v | 131 +++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 160 insertions(+), 42 deletions(-)
 create mode 100644 program_logic/auth.v

diff --git a/_CoqProject b/_CoqProject
index 1e919b355..6f18679ed 100644
--- a/_CoqProject
+++ b/_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
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 5401d24f4..8951c875a 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 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.
diff --git a/program_logic/auth.v b/program_logic/auth.v
new file mode 100644
index 000000000..57c311e92
--- /dev/null
+++ b/program_logic/auth.v
@@ -0,0 +1,131 @@
+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.
-- 
GitLab