complete lock

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.2018-05-23.3.3e9b81e3") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-05-23.5.2f8996b5") | (= "dev") }
 ]

theories/lang/lock.v

@@ -129,20 +129,27 @@ Section proof.
   Proof.
     iIntros (??) "#Hproto !# * HP HΦ".
     wp_rec. iMod ("Hproto" with "HP") as (γ Vb) "(#[Eq lc] & inv & Hclose)".
+    iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
     iApply (GPS_PPRaw_CAS_simple (lock_interp R0) _ _ _
                 (Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I
-            with "[$lc $inv]"); [done|by right|by left|..].
-    { iSplitL ""; [|iSplitL ""]; iNext; iModIntro.
+            with "[$lc $inv rTrue]"); [done|by right|by left|..].
+    { iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
       - iIntros (?? _). by iApply lock_interp_comparable.
       - by iIntros (??)"_ #$".
-      - simpl. admit. }
+      - iNext. rewrite /= -(bi.True_sep' (∀ _, _)%I).
+        iApply (rel_sep_objectively with "[$rTrue]").
+        iModIntro. iIntros ([] _). iSplit; [|by iIntros (?) "??"].
+        iIntros "F _". iModIntro. rewrite /lock_interp /=.
+        iExists (). iSplitL ""; [done|]. iDestruct "F" as (b) "[Eq R0]".
+        iDestruct "Eq" as %Eq. destruct b; [by inversion Eq|].
+        iFrame "R0". iSplit; by iExists true. }
     iNext. iIntros (b v' s') "(_ & inv & _ & CASE)"; simpl.
     iMod ("Hclose" with "inv") as "P".
     iModIntro. iApply "HΦ". iFrame "P".
     iDestruct "CASE" as "[[[% _] ?]|[[% _]_]]"; by subst b.
-  Admitted.
+  Qed.
 
-  Lemma acquire_specl l (R0 R P: vProp) tid E1 E2 :
+  Lemma acquire_spec l (R0 R P: vProp) tid E1 E2 :
     ↑histN ⊆ E1 → E1 ⊆ E2 →
     □ (P ={E2,E1}=∗ ∃ γ Vb, lock_proto_lc l γ R0 R
                   ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)