add 3 instances of GPS read

.gitignore

@@ -2,6 +2,7 @@
 *.d
 *.glob
 *.vo
+*.vio
 *.log
 *.aux
 *.fdb_latexmk

coq/ra/gps_instances.v

@@ -15,7 +15,8 @@ Section Protocols.
 
   Local Notation iProp := (iProp Σ).
   Context `{ParamDec : ∀ x y : Param, Decision (x = y)}
-           {ParamCount : Countable Param}.
+           {ParamCount : Countable Param}
+           {ParamInhab : Inhabited 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).
 
@@ -39,37 +40,150 @@ Section Protocols.
     ∃ γ, n = Encoder γ x ★ WA s V γ.
 
   Section SW.
-    Context (Np Nl : namespace) (NNpDisj: disjoint N Np).
+    Context (Np Nl : namespace)
+            (NNpDisj: disjoint N Np) (NNlDisj: disjoint N Nl).
 
-    Definition GSP_RP l x s V : iProp :=
+    Definition GPS_RP l x s V : iProp :=
       persisted Np Nl l PrInvRaw (ReaderRaw x s V).
 
-    Definition GSP_WP l x s V : iProp :=
+    Definition GPS_WP l x s V : iProp :=
       persisted Np Nl l PrInvRaw (WriterRaw x s V).
+
+    Lemma GPS_RP_Read (P : vPred) (Q : Z -> vPred) E s Φ π V l x :
+      nclose N ⊆ E → nclose Nl ⊆ E →
+      ▷ (⊩ (∀ s', ■ (s ⊑ s') →
+            (∀ v, F_past x s' v ★ P ={E∖Nl}=★ Q v)%V
+            ∨ (∀ s'' v, ■ (s' ⊑ s'') → F x s'' v ★ P ={E∖Nl}=★ False)))
+      ★ invariants.inv N PSInv ★ Seen π V ★ ▷ (P V) ★ GPS_RP l x s V
+        ★ (∀ v V' s', ■ (V ⊑ V') ★ ■ (s ⊑ s') ★ Seen π V' 
+                      ★ Q v V' ★ GPS_RP l x s' V' -★ Φ (LitV $ LitInt v, π))
+                       ⊢ WP (Load at_hack (Lit $ LitLoc l), π) @ (E) {{ Φ }}.
+    Proof.
+      intros.
+      iIntros "(Hyp & #kI & #kS & oP & oR & Post)".
+      iVs ((persistor_open Np Nl) with "[oR]")
+        as (X) "(PrInvRaw & ReaderRaw & HClose)" => //.
+      iDestruct "ReaderRaw" as (γ) "(% & RA)".
+      iDestruct "PrInvRaw" as (γ' x') "(>% & PrInv)".
+      rewrite H2 in H1. destruct (Encoder_Inj _ _ _ _ H1) as [Eqx Eqγ].
+      subst x γ.
+      iApply ((RawProto_Read N)) => //.
+      - apply ndisj_subseteq_difference => //.
+      - iSplitL "Hyp"; first by iNext.
+        iSplit => //.
+        iSplit => //.
+        iSplitL "oP" => //.
+        iSplitL "RA" => //.
+        iSplitL "PrInv" => //.
+        iIntros (v V' s') "(% & % & #kS' & kQ & kRA & PrInv)".
+        iAssert (GPS_RP l x' s' V' -★ Φ (LitV (LitInt v), π))
+          with "[Post kQ]" as "Post".
+          { iIntros "GPS". iApply ("Post" $! v V' s').
+            iFrame. repeat iSplit => //. }
+        iApply "Post". iApply "HClose".
+        iSplitL "PrInv".
+        + iNext. iExists γ', x'. by iFrame.
+        + iExists γ'. by iFrame.
+    Qed.
   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).
+    Context (Np Nl : namespace)
+            (NNpDisj: disjoint N Np) (NNlDisj: disjoint N Nl).
 
-    Definition GSP_Plain l x s V : iProp :=
+    Definition GPS_Plain l x s V : iProp :=
       persisted Np Nl l PrInvRaw_WShare (ReaderRaw x s V).
 
+    Lemma GPS_Plain_Read (P : vPred) (Q : Z -> vPred) E s Φ π V l x :
+      nclose N ⊆ E → nclose Nl ⊆ E →
+      ▷ (⊩ (∀ s', ■ (s ⊑ s') →
+            (∀ v, F_past x s' v ★ P ={E∖Nl}=★ Q v)%V
+            ∨ (∀ s'' v, ■ (s' ⊑ s'') → F x s'' v ★ P ={E∖Nl}=★ False)))
+      ★ invariants.inv N PSInv ★ Seen π V ★ ▷ (P V) ★ GPS_Plain l x s V
+        ★ (∀ v V' s', ■ (V ⊑ V') ★ ■ (s ⊑ s') ★ Seen π V' 
+                      ★ Q v V' ★ GPS_Plain l x s' V' -★ Φ (LitV $ LitInt v, π))
+                       ⊢ WP (Load at_hack (Lit $ LitLoc l), π) @ (E) {{ Φ }}.
+    Proof.
+      intros.
+      iIntros "(Hyp & #kI & #kS & oP & oR & Post)".
+      iVs ((persistor_open Np Nl) with "[oR]")
+        as (X) "(PrInvRaw & ReaderRaw & HClose)" => //.
+      iDestruct "ReaderRaw" as (γ) "(% & RA)".
+      iDestruct "PrInvRaw" as (γ' x') "(>% & PrInv & Writer)".
+      rewrite H2 in H1. destruct (Encoder_Inj _ _ _ _ H1) as [Eqx Eqγ].
+      subst x γ.
+      iApply ((RawProto_Read N)) => //.
+      - apply ndisj_subseteq_difference => //.
+      - iSplitL "Hyp"; first by iNext.
+        iSplit => //.
+        iSplit => //.
+        iSplitL "oP" => //.
+        iSplitL "RA" => //.
+        iSplitL "PrInv" => //.
+        iIntros (v V' s') "(% & % & #kS' & kQ & kRA & PrInv)".
+        iAssert (GPS_Plain l x' s' V' -★ Φ (LitV (LitInt v), π))
+          with "[Post kQ]" as "Post".
+          { iIntros "GPS". iApply ("Post" $! v V' s').
+            iFrame. repeat iSplit => //. }
+        iApply "Post". iApply "HClose".
+        iSplitL "PrInv Writer".
+        + iNext. iExists γ', x'. by iFrame.
+        + iExists γ'. by iFrame.
+    Qed.
+
   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 (Nl : namespace) (NNlDisj: disjoint N Nl).
     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.
+
+    Lemma GPS_Frac_Read (P : vPred) (Q : Z -> vPred) E s Φ π V l x q :
+      nclose N ⊆ E → nclose Nl ⊆ E →
+      ▷ (⊩ (∀ s', ■ (s ⊑ s') →
+            (∀ v, F_past x s' v ★ P ={E∖Nl}=★ Q v)%V
+            ∨ (∀ s'' v, ■ (s' ⊑ s'') → F x s'' v ★ P ={E∖Nl}=★ False)))
+      ★ invariants.inv N PSInv ★ Seen π V ★ ▷ (P V) ★ GSP_Frac l x s q V
+        ★ (∀ v V' s', ■ (V ⊑ V') ★ ■ (s ⊑ s') ★ Seen π V' 
+                      ★ Q v V' ★ GSP_Frac l x s' q V' -★ Φ (LitV $ LitInt v, π))
+                       ⊢ WP (Load at_hack (Lit $ LitLoc l), π) @ (E) {{ Φ }}.
+    Proof.
+      intros.
+      iIntros "(Hyp & #kI & #kS & oP & oR & Post)".
+      iVs ((fractor_open Nl) with "[oR]")
+        as (X) "(PrInvRaw & FracRaw & HClose)" => //.
+      iDestruct "FracRaw" as (γ) "(% & RA)".
+      iDestruct "PrInvRaw" as (γ' x') "(>% & PrInv & Writer)".
+      rewrite H2 in H1. destruct (Encoder_Inj _ _ _ _ H1) as [Eqx Eqγ].
+      subst x γ.
+      iApply ((RawProto_Read N)) => //.
+      - apply ndisj_subseteq_difference => //.
+      - iSplitL "Hyp"; first by iNext.
+        iSplit => //.
+        iSplit => //.
+        iSplitL "oP" => //.
+        iSplitL "RA" => //.
+        iSplitL "PrInv" => //.
+        iIntros (v V' s') "(% & % & #kS' & kQ & kRA & PrInv)".
+        iAssert (GSP_Frac l x' s' q V' -★ Φ (LitV (LitInt v), π))
+          with "[Post kQ]" as "Post".
+          { iIntros "GPS". iApply ("Post" $! v V' s').
+            iFrame. repeat iSplit => //. }
+        iApply "Post". iApply "HClose".
+        iSplitL "PrInv Writer".
+        + iNext. iExists γ', x'. by iFrame.
+        + iExists γ'. by iFrame.
+    Qed.
   End Frac.
 
 End Protocols.
\ No newline at end of file