add gps instances definition

coq/ra/_CoqProject

@@ -20,3 +20,4 @@
 ./persistor.v
 ./fractor.v
 ./gps.v
+./gps_instances.v

coq/ra/gps_instances.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
+From iris.program_logic Require Import cancelable_invariants.
+
+Import uPred.
+
+From ra Require Import persistor fractor.
+From ra Require Export gps.
+
+Section Protocols.
+  Context `{!gpsG Prtcl Σ} `{PrInhab : Inhabited (Pr_state Prtcl)}
+          `{PrDec : ∀ s1 s2 : Pr_state Prtcl, Decision (s1 = s2)}
+          `{!persistorG Σ}.
+  Context (N: namespace).
+
+  Local Notation iProp := (iProp Σ).
+  Context `{ParamDec : ∀ x y : Param, Decision (x = y)}
+           {ParamCount : Countable Param}.
+  Variables (F F_past : Param -> Pr_state Prtcl -> Z -> @vPred Σ).
+  Hypothesis (PastDup : ∀ x s v V, F_past x s v V ⊢ F_past x s v V ★ F_past x s v V).
+
+  Implicit Type
+           (l : loc)
+           (s : Pr_state Prtcl)
+           (ζ : sts.sts.state (gps_sts Prtcl))
+           (V : View).
+
+  Context (Encoder: gname → Param → val) 
+          (Encoder_Inj: ∀ x1 γ1 x2 γ2, Encoder γ1 x1 = Encoder γ2 x2
+                                       → x1 = x2 ∧ γ1 = γ2).
+
+  Definition PrInvRaw l n : iProp :=
+    ∃ γ x, n = Encoder γ x ★ PrInv F F_past l γ x.
+
+  Definition ReaderRaw x s V l n : iProp :=
+    ∃ γ, n = Encoder γ x ★ RA s V γ.
+
+  Definition WriterRaw x s V l n : iProp :=
+    ∃ γ, n = Encoder γ x ★ WA s V γ.
+
+  Section SW.
+    Context (Np Nl : namespace) (NNpDisj: disjoint N Np).
+
+    Definition GSP_RP l x s V : iProp :=
+      persisted Np Nl l PrInvRaw (ReaderRaw x s V).
+
+    Definition GSP_WP l x s V : iProp :=
+      persisted Np Nl l PrInvRaw (WriterRaw x s V).
+  End SW.
+
+  Definition PrInvRaw_WShare l n : iProp :=
+    ∃ γ x, n = Encoder γ x ★ PrInv F F_past l γ x ★ ∃ ζ, Writer γ ζ.
+
+  Section Plain.
+    Context (Np Nl : namespace) (NNpDisj: disjoint N Np).
+
+    Definition GSP_Plain l x s V : iProp :=
+      persisted Np Nl l PrInvRaw_WShare (ReaderRaw x s V).
+
+  End Plain.
+
+  Section Frac.
+    Context (Encoder': val → gname → val) 
+            (Encoder_Inj': ∀ X1 γ1 X2 γ2, Encoder' X1 γ1 = Encoder' X2 γ2
+                                           → X1 = X2 ∧ γ1 = γ2).
+    Context (Nl : namespace).
+    Context `{!cinvG Σ}.
+    Definition FracRaw x s V l (q: frac) n : iProp :=
+      ∃ γ, n = Encoder γ x ★ RA s V γ.
+
+    Definition GSP_Frac l x s (q: frac) V : iProp :=
+      fractored Nl Encoder' l PrInvRaw_WShare (FracRaw x s V) q.
+  End Frac.
+
+End Protocols.
\ No newline at end of file