bump gpfsl

_CoqProject

@@ -16,7 +16,6 @@ theories/lifetime/at_borrow.v
 theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
 theories/logic/gps.v
-theories/logic/gps_view_inv.v
 theories/lang/notation.v
 theories/lang/memcpy.v
 theories/lang/new_delete.v

opam

@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-02-11.0.2fd09d18") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-02-15.1.400540d7") | (= "dev") }
 ]

theories/lang/spawn.v

@@ -3,8 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import notation.
 From gpfsl.logic Require Import view_invariants.
-From gpfsl.gps Require Import middleware protocols escrows.
-From lrust.logic Require Import gps_view_inv.
+From gpfsl.gps Require Import surface protocols escrows.
 
 Set Default Proof Using "Type".
 

theories/logic/gps_view_inv.v

-From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
-From lrust.lang Require Import notation.
-From gpfsl.logic Require Import view_invariants.
-From gpfsl.gps Require Import middleware.
-
-Section gps_view_SP.
-Context `{!noprolG Σ, !gpsG Σ Prtcl, !view_invG Σ} (N: namespace).
-
-Local Notation vProp := (vProp Σ).
-
-Implicit Types (IP : interpC Σ Prtcl) (IPC: interpCasC Σ Prtcl) (l : loc)
-               (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
-               (γ : gname).
-
-Definition GPS_vSP_Reader IP IPC l t s v γ γi : vProp :=
-  (GPS_SWReader l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
-Definition GPS_vSP_Writer IP IPC l t s v γ γi: vProp :=
-  (GPS_SWWriter l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
-Definition GPS_vSP_SharedReader IP IPC l t s v q γ γi : vProp :=
-  (GPS_SWSharedReader l t s v q γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
-Definition GPS_vSP_SharedWriter IP IPC l t s v γ γi : vProp :=
-  (GPS_SWSharedWriter l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
-
-Global Instance GPS_vSP_Writer_contractive IPC l t s v γ γi :
-  Contractive (λ IP, GPS_vSP_Writer IP IPC l t s v γ γi).
-Proof.
-  move => n ???. apply bi.sep_ne; [done|]. apply view_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
-Qed.
-
-Global Instance GPS_vSP_Writer_ne IPC l t s v γ γi :
-  NonExpansive (λ IP, GPS_vSP_Writer IP IPC l t s v γ γi).
-Proof. apply contractive_ne. by apply _. Qed.
-
-
-Lemma GPS_vSP_SWWriter_Reader IP IPC l t s v γ γi:
-  GPS_vSP_Writer IP IPC l t s v γ γi -∗ GPS_vSP_Reader IP IPC l t s v γ γi.
-Proof.
-  iDestruct 1 as "[W $]". iDestruct (GPS_SWWriter_Reader with "W") as "$".
-Qed.
-
-Lemma GPS_vSP_Init (IP: gname → interpC Σ Prtcl) IPC l s v E:
-  l ↦ v -∗ (∀ γi t γ, ▷ IP γi true l γ t s v) ={E}=∗
-  ∃ γi γ t, view_tok γi 1 ∗ GPS_vSP_Writer (IP γi) IPC l t s v γ γi.
-Proof.
-  iIntros "Hl IP".
-  iMod (view_inv_alloc N _) as (γi) "VI".
-  iMod (GPS_SWRaw_Init_vs (IP γi) _ IPC true s with "Hl IP") as (γ t) "[SW gpsI]".
-  iMod ("VI" $! (GPS_INV (IP γi) l IPC γ) with "gpsI") as "[#Inv tok]".
-  iIntros "!>". iExists γi, γ, t. by iFrame.
-Qed.
-
-Lemma GPS_vSP_SWWrite_rel IP IPC l q Q Q1 Q2 t s s' v v' γ γi tid E
-  (Exts: s ⊑ s') (DISJ: histN ## N) (SUB1: ↑histN ⊆ E) (SUB2: ↑N ⊆ E):
-  let WVS: vProp :=
-  (∀ t', ⌜(t < t')%positive⌝ -∗ GPS_SWWriter l t' s' v' γ -∗ Q2 -∗ view_tok γi q
-              ={E ∖ ↑N}=∗ (<obj> (Q1 ={E ∖ ↑N}=∗ IPC l γ t s v)) ∗
-                     |={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
-  {{{ view_tok γi q ∗ GPS_vSP_Writer IP IPC l t s v γ γi
-      ∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
-    #l <-ʳᵉˡ v' in tid @ E
-  {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_vSP_Reader IP IPC l t' s' v' γ γi
-      ∗ Q t' }}}.
-Proof.
-  iIntros (WVS Φ) "(Htok & [W #Inv] & WVS & IP) Post".
-  iMod (view_inv_acc_base γi N with "[$Inv $Htok]") as "[Htok VI]"; [done|].
-  iDestruct "VI" as (Vb) "[HInv Closed]".
-  iApply (GPS_SWRaw_SWWrite_rel_view IP _ IPC Q Q1 Q2 (view_tok γi q)%I t s s'
-           v v' γ tid Vb with "[$W $HInv $Htok $WVS $IP]"); [done|solve_ndisj|..].
-  iIntros "!>" (t' V') "(Ext & R & In & tok & HInv)".
-  rewrite bi.and_elim_r bi.and_elim_l.
-  iMod ("Closed" $! _ (Q t') with "tok HInv") as "Q".
-  by iApply ("Post" $! t' with "[$Ext $R $Q $Inv]").
-Qed.
-
-Lemma GPS_vSP_SWRead_acq_dealloc IP IPC l P Q R q t s v vd γ γi tid E
-  (DISJ: histN ## N) (SUB1: ↑histN ⊆ E) (SUB2: ↑N ⊆ E):
-  let RVS: vProp :=
-    (∀ t' s' v', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
-         <obj> ((IP false l γ t' s' v' ={E ∖ ↑N}=∗ IP false l γ t' s' v' ∗ R t' s' v') ∧
-                (IP true l γ t' s' v' ={E ∖ ↑N}=∗ IP true l γ t' s' v' ∗ R t' s' v') ∧
-                (IPC l γ t' s' v' ={E ∖ ↑N}=∗ IPC l γ t' s' v' ∗ R t' s' v')))%I in
-  let DVS: vProp :=
-    (∀ t' s', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗ P -∗ view_tok γi q -∗ R t' s' vd ={E ∖ ↑N}=∗
-      view_tok γi 1 ∗ Q t' s')%I in
-  {{{ view_tok γi q ∗ GPS_vSP_Reader IP IPC l t s v γ γi
-      ∗ ▷ RVS ∗ ▷ DVS ∗ P }}}
-    !ᵃᶜ#l in tid @ E
-  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗
-      GPS_vSP_Reader IP IPC l t' s' v' γ γi ∗
-      if (decide (v' = vd)) then ▷ GPS_INV IP l IPC γ ∗ Q t' s'
-      else view_tok γi q ∗ R t' s' v' ∗ P }}}.
-Proof.
-  iIntros (RVS DVS Φ) "(Htok & [R #Inv] & RVS & DVS & P) Post".
-  iMod (view_inv_acc_base γi N with "[$Inv $Htok]") as "[Htok VI]"; [done|].
-  iDestruct "VI" as (Vb) "[HInv Closed]".
-  iApply (GPS_SWRaw_Read IP _ IPC R _ t s v _ _ Vb with "[$R $HInv $RVS]");
-    [solve_ndisj|by right|..].
-  iIntros "!>" (t' s' v') "(#Ext & R & HInv & HR)".
-  case (decide (v' = vd)) as [Eq|NEq]; last first.
-  - rewrite bi.and_elim_l. iMod ("Closed" with "Htok HInv") as "Htok".
-    iIntros "!>". iApply ("Post" with "[$Ext $R $Inv HR Htok P]").
-    rewrite (decide_False _ _ NEq). by iFrame.
-  - subst v'. iMod ("DVS" $! t' s' with "Ext P Htok HR") as "[Htok Q]".
-    rewrite bi.and_elim_r bi.and_elim_r.
-    iDestruct ("Closed" with "Htok") as "[In >_]".
-    iSpecialize ("HInv" with "In"). iModIntro.
-    iApply ("Post" $! t' s' vd with "[$Ext $R $Inv HInv Q]").
-    rewrite decide_True; [by iFrame|done].
-Qed.
-
-End gps_view_SP.