start work on the auth construction

_CoqProject

@@ -64,6 +64,7 @@ program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
 program_logic/tests.v
+program_logic/auth.v
 program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v

algebra/auth.v

@@ -146,6 +146,8 @@ Proof.
 Qed.
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
+Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
+Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 Lemma auth_update a a' b b' :
   (∀ n af, ✓{S n} a → a ≡{S n}≡ a' ⋅ af → b ≡{S n}≡ b' ⋅ af ∧ ✓{S n} b) →

program_logic/auth.v

 Require Export algebra.auth algebra.functor.
-Require Import program_logic.language program_logic.weakestpre.
-Import uPred.
-
-(* RJ: This is a work-in-progress playground.
-   FIXME: Finish or remove. *)
+Require Export program_logic.invariants program_logic.ghost_ownership.
+Import uPred ghost_ownership.
 
 Section auth.
-  (* TODO what should be implicit, what explicit? *)
-  Context {Λ : language}.
-  Context {C : nat → cmraT}.
-  Context (i : nat).
-  Context {A : cmraT}.
-
-  Hypothesis Ci : C i = authRA A.
-  Let Σ : iFunctor := iprodF (mapF positive ∘ constF ∘ C).
-
-  Definition tr (a : authRA A) : C i.
-  rewrite Ci. exact a. Defined.
-  Definition tr' (c : C i) : authRA A.
-  rewrite -Ci. exact c. Defined.
-
-  Lemma tr'_tr a :
-    tr' $ tr a = a.
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma tr_tr' c :
-    tr $ tr' c = c.
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma tr_proper : Proper ((≡) ==> (≡)) tr.
-  Proof.
-    move=>a1 a2 Heq. rewrite /tr. by destruct Ci.
-  Qed.
-
-  Lemma Ci_op (c1 c2: C i) :
-    c1 ⋅ c2 = tr (tr' c1 ⋅ tr' c2).
-  Proof.
-    rewrite /tr' /tr. by destruct Ci.
-  Qed.
-
-  Lemma A_val a :
-    ✓a = ✓(tr a).
-  Proof.
-    rewrite /tr. by destruct Ci.
-  Qed.
-
-  (* FIXME RJ: I'd rather not have to specify Σ by hand here. *)
-  Definition A2m (p : positive) (a : authRA A) : iGst Λ Σ :=
-    iprod_singleton i (<[p:=tr a]>∅).
-  Definition ownA (p : positive) (a : authRA A) : iProp Λ Σ :=
-    ownG (Σ:=Σ) (A2m p a).
-
-  Lemma ownA_op p a1 a2 :
-    (ownA p a1 ★ ownA p a2)%I ≡ ownA p (a1 ⋅ a2).
+  Context {A : cmraT} `{Empty A, !CMRAIdentity A}.
+  Context {Λ : language} {Σ : gid → iFunctor} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
+  (* TODO: Come up with notation for "iProp Λ (globalC Σ)". *)
+  Context (N : namespace) (φ : A → iProp Λ (globalC Σ)).
+  Implicit Types P Q R : iProp Λ (globalC Σ).
+  Implicit Types a b : A.
+  Implicit Types γ : gname.
+
+  (* TODO: Need this to be proven somewhere. *)
+  (* FIXME ✓ binds too strong, I need parenthesis here. *)
+  Hypothesis auth_valid :
+    forall a b, (✓(Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
+
+  (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
+  Local Instance auth_inhabited : Inhabited A.
+  Proof. split. exact ∅. Qed.
+
+  Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
+    (∃ a, own AuthI γ (●a) ★ φ a)%I.
+  Definition auth_own (γ : gname) (a : A) := own AuthI γ (◯a).
+  Definition auth_ctx (γ : gname) := inv N (auth_inv γ).
+
+  Lemma auth_alloc a :
+    ✓a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ ∧ auth_own γ a).
   Proof.
-    rewrite /ownA /A2m /iprod_singleton /iprod_insert -ownG_op. apply ownG_proper=>j /=.
-    rewrite iprod_lookup_op. destruct (decide (i = j)).
-    - move=>q. destruct e. rewrite lookup_op /=.
-      destruct (decide (p = q)); first subst q.
-      + rewrite !lookup_insert.
-        rewrite /op /cmra_op /=. f_equiv.
-        rewrite Ci_op. apply tr_proper.
-        rewrite !tr'_tr. reflexivity.
-      + by rewrite !lookup_insert_ne //.
-    - by rewrite left_id.
+    intros Ha. rewrite -(right_id True%I (★)%I (φ _)).
+    rewrite (own_alloc AuthI (Auth (Excl a) a) N) //; [].
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
+    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
+    transitivity (▷auth_inv γ ★ auth_own γ a)%I.
+    { rewrite /auth_inv -later_intro -(exist_intro a).
+      rewrite (commutative _ _ (φ _)) -associative. apply sep_mono; first done.
+      rewrite /auth_own -own_op auth_both_op. done. }
+    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
+    by rewrite always_and_sep_l'.
   Qed.
 
-  (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
-     assertion. However, the map_updateP_alloc does not suffice to show this. *)
-  Lemma ownA_alloc E a :
-    ✓a → True ⊑ pvs E E (∃ p, ownA p a).
+  Lemma auth_opened a γ :
+    (▷auth_inv γ ★ auth_own γ a) ⊑ (▷∃ a', φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
-    intros Ha. set (P m := ∃ p, m = A2m p a).
-    set (a' := tr a).
-    rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
-    - rewrite -pvs_updateP_empty //; [].
-      subst P. eapply (iprod_singleton_updateP_empty i).
-      + eapply map_updateP_alloc' with (x:=a'). subst a'.
-        by rewrite -A_val.
-      + simpl. move=>? [p [-> ?]]. exists p. done.
-    - apply exist_elim=>m. apply const_elim_l.
-      move=>[p ->] {P}. by rewrite -(exist_intro p).
-  Qed.      
-    
+    rewrite /auth_inv. rewrite [auth_own _ _]later_intro -later_sep.
+    apply later_mono. rewrite sep_exist_r. apply exist_elim=>b.
+    rewrite /auth_own [(_ ★ φ _)%I]commutative -associative -own_op.
+    rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
+    rewrite [∅ ⋅ _]left_id -(exist_intro a').
+  Abort.
 End auth.
 

program_logic/invariants.v

@@ -8,6 +8,7 @@ Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
 Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
+
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
 Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
@@ -91,7 +92,7 @@ Qed.
 
 Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) :
   atomic e → nclose N ⊆ E →
-  (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)))%I ⊑ wp E e Q.
+  (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
 Proof.
   move=>He HN.
   rewrite /inv and_exist_r. apply exist_elim=>i.
@@ -108,7 +109,7 @@ Proof.
   apply pvs_mask_frame'; solve_elem_of.
 Qed.
 
-Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
+Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
 
 End inv.

program_logic/pviewshifts.v

@@ -132,6 +132,8 @@ Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
 Proof. apply pvs_trans; solve_elem_of. Qed.
+Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q.
+Proof. move=>->. by rewrite pvs_trans'. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
 Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed.
 Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :

program_logic/viewshifts.v

@@ -100,7 +100,7 @@ Proof.
 Qed.
 
 Lemma vs_alloc (N : namespace) P : ▷ P ={N}=> inv N P.
-Proof. by intros; apply vs_alt, pvs_alloc. Qed.
+Proof. by intros; apply vs_alt, inv_alloc. Qed.
 
 End vs.
 

program_logic/weakestpre.v

@@ -206,6 +206,8 @@ Proof. by apply wp_mask_frame_mono. Qed.
 Global Instance wp_mono' E e :
   Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
+Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q.
+Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).