add abstract view read rules

coq/ra/gps/fractional.v

+From iris.proofmode Require Import tactics.
 From ra.gps Require Export inst_shared.
+From ra Require Import abs_view.
 
 Section Fractional.
-  Context {Σ : gFunctors} {Prtcl : protocolT} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
+  Context `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
           `{persG : persistorG Σ}
           `{agreeG : gps_agreeG Σ Prtcl}
           `{CInvG : cinvG Σ}
@@ -146,6 +148,46 @@ Section Fractional.
       iPureIntro. do 3 (etrans; eauto).
   Qed.
 
+  Lemma GPS_FP_Read_abs `{absG : absViewG Σ}
+      l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
+      s (E : coPset) β (HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E):
+    {{{{ (▷ ∀ s', ■ (s ⊑ s') →
+                  (∀ v, F_past l s' v ∗ P ={E ∖ ↑fracN .@ l}=∗ Q s' v)
+                  ∨ (∀ s'' v, ■ (s' ⊑ s'') → F l s'' v ∗ P ={E ∖ ↑fracN .@ l}=∗ False))
+           ∗ ▷ ɐ (∀ s' v, ■ (s ⊑ s') ∗ F_past l s' v
+                          ={E ∖ ↑fracN .@ l}=∗ F_past l s' v ∗ F_past l s' v )
+           ∗ P ∗ ⌞vGPS_FP l s q⌟ β ∗ aSeen β }}}}
+      ([ #l ]_at) @ E
+      {{{{ s' v, RET #v ;
+           ■ (s ⊑ s') ∗ ⌞vGPS_FP l s q⌟ β ∗ Q s' v }}}}%C.
+  Proof.
+    intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR & Seen) Post".
+    iDestruct "oR" as (V0) "(abs & oR)".
+    iDestruct "Seen" as (V1) "(% & abs2)".
+    iDestruct (absView_agree with "[$abs $abs2]") as "%". subst V1.
+    iMod (fractor_open with "[$oR]")
+      as (X) "(gpsRaw & RRaw & HClose)"; first exact HNl.
+
+    iDestruct "RRaw" as (γ γ_x e_x) "(% & Hex & RA)".
+    iDestruct "gpsRaw" as (γ' γ_x' ζ) "(>% & oI & Writer)".
+    subst X. apply encode_inj in H1. inversion H1. subst γ' γ_x'.
+
+    iDestruct "RA" as (V_r v_r) "(% & % & #oR)".
+
+    iApply (RawProto_Read IP l P Q s _ _ V_r v_r γ γ_x
+            with "[$VS $oI $kI $kS $oP $oR VSDup]"); [solve_ndisj|by etrans|..].
+    { iNext. by iSpecialize ("VSDup" $! _). }
+    iNext.
+    iIntros (s' v Vr V') "(#HV' & kS' & #Hs' & oI & oQ & #oR' & % & %)".
+    iApply ("Post" $! V' with "HV' * kS'"). iFrame "Hs' oQ".
+    iExists V0. iFrame "abs".
+    iApply "HClose". iSplitL "oI Writer".
+    + iNext. iExists γ, γ_x, ζ. by iFrame "oI Writer".
+    + iExists γ, γ_x, e_x. iFrame "Hex".
+      iSplit; first done.
+      iExists V_r, v_r. iFrame (H0 H2) "oR".
+  Qed.
+
   Lemma GPS_FP_Write l q s s' v (E : coPset)
         (P: vPred) (Q : pr_state Prtcl → vPred) 
         (HN : ↑physN ⊆ E) (HNl: ↑fracN .@ l ⊆ E) (HFinal : final_st s'):

coq/ra/na.v

@@ -2,7 +2,7 @@ From iris.program_logic Require Import weakestpre.
 From iris.base_logic Require Import lib.invariants.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode weakestpre fractor.
+From ra Require Import viewpred proofmode weakestpre fractor abs_view.
 From ra Require Export notation.
 From ra.base Require Export ghosts na_read na_write.
 
@@ -10,7 +10,7 @@ Section Helpers.
   Context {Σ : gFunctors}.
   Set Default Proof Using "Type".
   Definition valloc_local_aux h V: iProp Σ := ⌜alloc_local h V⌝%I.
-  
+
   Definition vPred_valloc_local h :
     @vPred_Mono Σ (valloc_local_aux h).
   Proof.
@@ -25,21 +25,21 @@ End Helpers.
 Section Exclusive.
   Context {Σ : gFunctors} `{fG : foundationG Σ}.
   Set Default Proof Using "Type".
-  
+
   Definition own_loc_prim l h: @vPred Σ
     := (∃ i, valloc_local h ∧ (☐ Hist l h) ∗ (☐ Info l 1%Qp i)).
-  
+
   Definition own_loc_na l v: @vPred Σ
     := ∃ V, own_loc_prim l {[v, V]}.
 
   Definition own_loc l : @vPred Σ :=
     (∃ h, own_loc_prim l h).
-  
+
   Global Instance From_own_loc_prim_exist:
     ∀ V, FromExist (own_loc_prim l h V) 
                    (λ i, (valloc_local h ∧ (☐ Hist l h) ∗ (☐ Info l 1%Qp i)) V)%VP.
   Proof. apply _. Qed.
-  
+
   Global Instance Into_own_loc_prim_exist:
     ∀ V, IntoExist (own_loc_prim l h V) 
                    (λ i, (valloc_local h ∧ (☐ Hist l h) ∗ (☐ Info l 1%Qp i)) V)%VP.
@@ -71,7 +71,7 @@ Section Exclusive.
   Global Instance own_loc_prim_timeless l h V 
     : TimelessP (own_loc_prim l h V).
   Proof. apply _. Qed.
-  
+
   Global Instance own_loc_timeless l V : TimelessP (own_loc l V).
   Proof. apply _. Qed.
 
@@ -88,7 +88,7 @@ Typeclasses Opaque own_loc_prim own_loc_na own_loc.
 Section Fractional.
   Context {Σ : gFunctors} `{fG : foundationG Σ} `{cG : cinvG Σ}.
   Set Default Proof Using "Type".
-  
+
   Notation frac_inv h := (λ l _, Hist l h)%I.
   Notation frac_local v := (λ _ _ X, ⌜X = encode v⌝)%I.
 
@@ -117,6 +117,22 @@ Proof.
   destruct 1 as (vx & Vx & ? & ?). abstract set_solver.
 Qed.
 
+Lemma alloc_local_singleton_na_safe l v V V':
+  alloc_local {[v, V]} V' → na_safe l {[v, V]} V'.
+Proof.
+  move => [v1 [V1 [H1 [H2 _]]]].
+  exists (v1, V1). repeat split; [auto|abstract set_solver+H1|auto].
+Qed.
+
+Lemma alloc_local_singleton_value_init v V V':
+  alloc_local {[VInj v, V]} V' → init_local {[VInj v, V]} V'.
+Proof.
+  move => [v1 [V1 [H1 [H2 _]]]].
+  exists v1, V1. repeat split; [auto|auto|].
+  apply elem_of_singleton_1 in H1. by inversion H1.
+Qed.
+
+
 Section ExclusiveRules.
   Context `{foundationG Σ}.
   Set Default Proof Using "Type".
@@ -137,11 +153,11 @@ Section ExclusiveRules.
   Proof.
     intros. iViewUp; iIntros "#kI kS oNA Post".
     iDestruct "oNA" as (V_0 i) "(% & oH & oI)".
-    iApply wp_mask_mono; last (iApply (f_read_na with "[$kI $kS $oH]")); first auto.
-    - destruct H1 as (v1 & V1 & H1 & H2 & H3). iSplit; iPureIntro.
-      + exists (v1, V1). repeat split; [auto|abstract set_solver+H1|auto].
-      + exists v1, V1. repeat split; [auto|auto|].
-        apply elem_of_singleton_1 in H1. by inversion H1.
+    iApply wp_mask_mono;
+      last (iApply (f_read_na with "[$kI $kS $oH]")); first auto.
+    - iSplit; iPureIntro;
+      by [apply alloc_local_singleton_na_safe|
+          apply alloc_local_singleton_value_init].
     - iNext. iIntros (v_r V') "(% & kS' & oH & % & H)".
       iDestruct "H" as (V_1) "(% & % & %)".
       move: H6 => /value_at_hd_singleton [[->] ->].
@@ -231,18 +247,17 @@ Section FractionalRules.
     ↑ physN ⊆ E →
     ↑fracN .@ l ⊆ E →
     {{{{ l ↦{q} v }}}}
-      ([ #l]_na) @ E 
-    {{{{ z, RET (#z); ■ (z = v) ∗ (l ↦{q} v)  }}}}.
+      [ #l ]_na @ E 
+    {{{{ z, RET (#z); ■ (z = v) ∗ l ↦{q} v }}}}.
   Proof.
     intros. iViewUp; iIntros "#kI kS oNA Post".
     iDestruct "oNA" as (V_0) "(% & oNA)".
     iMod (fractor_open with "oNA") as (X) "(oH & HX & HClose)"; [solve_ndisj|].
     iApply wp_mask_mono; last (iApply (f_read_na with "[$kI $kS $oH]"));
       first solve_ndisj.
-    - destruct H1 as (v1 & V1 & H1 & H2 & H3). iSplit; iPureIntro.
-      + exists (v1, V1). repeat split; [auto|abstract set_solver+H1|auto].
-      + exists v1, V1. repeat split; [auto|auto|].
-        apply elem_of_singleton_1 in H1. by inversion H1.
+    - iSplit; iPureIntro;
+      by [apply alloc_local_singleton_na_safe|
+          apply alloc_local_singleton_value_init].
     - iNext. iIntros (v_r V') "(% & kS' & oH & % & H)".
       iDestruct "H" as (V_1) "(% & % & %)".
       move: H6 => /value_at_hd_singleton [[->] ->].
@@ -254,6 +269,35 @@ Section FractionalRules.
       exists (VInj v_r), V_1. by rewrite elem_of_singleton.
   Qed.
 
+  Lemma na_read_abs_frac `{absG : absViewG Σ} (E : coPset) l q v β :
+    ↑ physN ⊆ E →
+    ↑fracN .@ l ⊆ E →
+    {{{{ ⌞l ↦{q} v⌟ β ∗ aSeen β }}}}
+      [ #l ]_na @ E 
+    {{{{ z, RET (#z); ■ (z = v) ∗ ⌞l ↦{q} v⌟ β }}}}.
+  Proof.
+    intros. iViewUp; iIntros "#kI kS (ol & Seen) Post".
+    iDestruct "ol" as (V0) "(abs & ol)".
+    iDestruct "Seen" as (V1) "(% & abs2)".
+    iDestruct (absView_agree with "[$abs $abs2]") as "%". subst V0.
+    iDestruct "ol" as (V0) "[% ol]".
+    iMod (fractor_open with "ol") as (X) "(oH & HX & HClose)"; [solve_ndisj|].
+    iApply wp_mask_mono; last (iApply (f_read_na with "[$kI $kS $oH]"));
+      first solve_ndisj.
+    - iSplit; iPureIntro;
+       [apply alloc_local_singleton_na_safe|
+          apply alloc_local_singleton_value_init];
+       by apply (alloc_local_Mono _ _ V1).
+    - iNext. iIntros (v_r V') "(% & kS' & oH & % & H)".
+      iDestruct "H" as (V_1) "(% & % & %)".
+      move: H7 => /value_at_hd_singleton [[?] ?]. subst v_r V_1.
+      iApply ("Post" with "[%] * kS'"); [done|].
+      iMod ("HClose" $! (λ _ _ X, ⌜X = encode (VInj v)⌝)%I with "[$oH $HX]")
+        as "ol".
+      iModIntro. iSplitL ""; first done.
+      iExists _. iFrame "abs". iExists _. by iFrame "ol".
+  Qed.
+
   Lemma na_frac_from_non (E: coPset) l v:
     ↑ physN ⊆ E →
     (☐ PSCtx ∗ l ↦ v ={E}=> l ↦{1} v)%VP.
@@ -307,5 +351,6 @@ Section FractionalRules.
 
 End FractionalRules.
 
+
 Arguments na_read [_ _ _ _ _] _ [_ _ _].
 Arguments na_write [_ _ _ _ _] _ [_ _ _].
\ No newline at end of file