prove sts_alloc; play around with modules and namespaces for sts

algebra/cmra.v

@@ -466,7 +466,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
 
 Section discrete.
   Context {A : cofeT} `{∀ x : A, Timeless x}.
-  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
+  Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -487,6 +487,8 @@ Section discrete.
   Lemma discrete_update (x y : discreteRA) :
     (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
   Proof. intros Hvalid z n; apply Hvalid. Qed.
+  Lemma discrete_valid (x : discreteRA) : v x → validN_valid x.
+  Proof. move=>Hx n. exact Hx. Qed.
 End discrete.
 
 (** ** CMRA for the unit type *)

algebra/upred.v

@@ -320,13 +320,13 @@ Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
 Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
-Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
+Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
 Proof.
   by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
     [rewrite -(dist_le _ _ _ _ Ha); last lia
     |rewrite (dist_le _ _ _ _ Ha); last lia].
 Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
+Global Instance ownM_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
 Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
 Proof. unfold uPred_iff; solve_proper. Qed.
 Global Instance iff_proper :
@@ -899,7 +899,7 @@ Qed.
 Global Instance eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed.
-Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
+Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
 Proof.
   intros ?; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
     cmra_timeless_included_l; eauto using cmra_validN_le.
@@ -929,7 +929,7 @@ Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I
 Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
 Global Instance later_always_stable P : AS P → AS (▷ P).
 Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
-Global Instance own_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
+Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
 Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
 Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) :
   AS P → (∀ x, AS (Q x)) → AS (default P mx Q).

program_logic/ownership.v

@@ -22,7 +22,7 @@ Implicit Types m : iGst Λ Σ.
 Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
 Proof.
   intros n P Q HPQ. rewrite /ownI.
-  apply uPred.own_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
+  apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
   by apply Next_contractive=> j ?; rewrite (HPQ j).
 Qed.
 Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.

program_logic/sts.v

 From algebra Require Export sts.
+From algebra Require Import dra.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-Class StsInG Λ Σ (i : gid) {A B} (R : relation A) (tok : A → set B) := {
-  sts_inG :> InG Λ Σ i (stsRA R tok);
+Local Arguments valid _ _ !_ /.
+Local Arguments op _ _ !_ !_ /.
+Local Arguments unit _ _ !_ /.
+
+Module sts.
+Record Sts {A B} := {
+  st : relation A;
+  tok    : A → set B;
+}.
+Arguments Sts : clear implicits.
+
+Class InG Λ Σ (i : gid) {A B} (sts : Sts A B) := {
+  inG :> ghost_ownership.InG Λ Σ i (stsRA sts.(st) sts.(tok));
 }.
 
 Section definitions.
-  Context {Λ Σ A B} (i : gid) (R : relation A) (tok : A → set B)
-          `{!StsInG Λ Σ i R tok} (γ : gname).
-  Definition sts_inv  (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-    (∃ s, own i γ (sts_auth R tok s set_all) ★ φ s)%I.
-  Definition sts_states (S : set A) (T: set B) : iPropG Λ Σ :=
-    (■ sts.closed R tok S T ∧ own i γ (sts_frag R tok S T))%I.
-  Definition sts_state (s : A) (T: set B) : iPropG Λ Σ :=
-    own i γ (sts_frag R tok (sts.up R tok s T) T).
-  Definition sts_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-    inv N (sts_inv φ).
+  Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ i sts} (γ : gname).
+  Definition inv  (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    (∃ s, own i γ (sts_auth sts.(st) sts.(tok) s set_empty) ★ φ s)%I.
+  Definition states (S : set A) (T: set B) : iPropG Λ Σ :=
+    (■ sts.closed sts.(st) sts.(tok) S T ∧
+     own i γ (sts_frag sts.(st) sts.(tok) S T))%I.
+  Definition state (s : A) (T: set B) : iPropG Λ Σ :=
+    own i γ (sts_frag sts.(st) sts.(tok) (sts.up sts.(st) sts.(tok) s T) T).
+  Definition ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    invariants.inv N (inv φ).
 End definitions.
-Instance: Params (@sts_inv) 9.
-Instance: Params (@sts_states) 9.
-Instance: Params (@sts_ctx) 10.
+Instance: Params (@inv) 8.
+Instance: Params (@states) 8.
+Instance: Params (@ctx) 9.
 
 Section sts.
-  Context `{StsInG Λ Σ StsI (A:=A) R tok}.
+  Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ StsI sts}.
   Context (φ : A → iPropG Λ Σ).
   Implicit Types N : namespace.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types γ : gname.
 
+  Lemma alloc N s :
+    φ s ⊑ pvs N N (∃ γ, ctx StsI sts γ N φ ∧ state StsI sts γ s (set_all ∖ sts.(tok) s)).
+  Proof.
+    eapply sep_elim_True_r.
+    { eapply (own_alloc StsI (sts_auth sts.(st) sts.(tok) s (set_all ∖ sts.(tok) s)) N).
+      apply discrete_valid=>/=. solve_elem_of. }
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
+    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
+    transitivity (▷ inv StsI sts γ φ ★ state StsI sts γ s (set_all ∖ sts.(tok) s))%I.
+    { rewrite /inv -later_intro -(exist_intro s).
+      rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
+      rewrite -own_op. apply equiv_spec, own_proper.
+      split; first split; simpl.
+      - intros; solve_elem_of-.
+      - intros _. split_ands; first by solve_elem_of-.
+        + apply sts.closed_up. solve_elem_of-.
+        + constructor; last solve_elem_of-. apply sts.elem_of_up. 
+      - intros _. constructor. solve_elem_of-. }
+    rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono.
+    by rewrite always_and_sep_l.
+  Qed.
+
+End sts.
+
 End sts.