srv client side with minor admit

misc.v

@@ -20,8 +20,13 @@ Section lemmas.
     eapply cmra_update_exclusive.
     done.
   Qed.
-
+  
   Lemma pair_l_frac_op (g g': val):
     ((((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g'))) ~~> (1%Qp, DecAgree g').
   Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
+
+  Lemma pair_l_frac_op' (g g': val):
+     (1%Qp, DecAgree g') ~~> ((((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g'))).
+  Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
+
 End lemmas.

srv.v

@@ -60,23 +60,23 @@ Section proof.
   Context `{!heapG Σ, !lockG Σ, !srvG Σ} (N : namespace).
 
   Definition srv_inv
-             (γx γ1 γ2: gname) (p: loc)
+             (γx γ1 γ2 γ3: gname) (p: loc)
              (Q: val → val → Prop): iProp Σ :=
     ((∃ (x: val),   p ↦ InjRV x ★ own γ1 (Excl ())) ∨
-     (∃ (x: val),   p ↦ InjLV x ★ own γx ((1/2)%Qp, DecAgree x) ★ own γ1 (Excl ())) ∨
-     (∃ (x y: val), p ↦ InjRV y ★ own γx ((1/2)%Qp, DecAgree x) ★ ■ Q x y ★ own γ2 (Excl ())))%I.
+     (∃ (x: val),   p ↦ InjLV x ★ own γx ((1/2)%Qp, DecAgree x) ★ own γ2 (Excl ())) ∨
+     (∃ (x y: val), p ↦ InjRV y ★ own γx ((1/2)%Qp, DecAgree x) ★ ■ Q x y ★ own γ3 (Excl ())))%I.
   
-  Lemma srv_inv_timeless γx γ1 γ2 p Q: TimelessP (srv_inv γx γ1 γ2 p Q).
+  Lemma srv_inv_timeless γx γ1 γ2 γ3 p Q: TimelessP (srv_inv γx γ1 γ2 γ3 p Q).
   Proof. apply _. Qed.
 
-  Lemma wait_spec (Φ: val → iProp Σ) (Q: val → val → Prop) x γx γ1 γ2 p:
+  Lemma wait_spec (Φ: val → iProp Σ) (Q: val → val → Prop) x γx γ1 γ2 γ3 p:
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_inv γx γ1 γ2 p Q) ★
-    own γx ((1/2)%Qp, DecAgree x) ★ own γ1 (Excl ()) ★
-    (∀ x y, own γ2 (Excl ()) -★ own γx (1%Qp, DecAgree x) -★ ■ Q x y-★ Φ y)
+    heap_ctx ★ inv N (srv_inv γx γ1 γ2 γ3 p Q) ★
+    own γx ((1/2)%Qp, DecAgree x) ★ own γ1 (Excl ()) ★ own γ3 (Excl ()) ★
+    (∀ y, own γ1 (Excl ()) ★ own γ2 (Excl ()) -★ own γx (1%Qp, DecAgree x) -★ ■ Q x y-★ Φ y)
     ⊢ WP wait #p {{ Φ }}.
   Proof.
-    iIntros (HN) "(#Hh & #Hsrv & Hx & Hempty & HΦ)".
+    iIntros (HN) "(#Hh & #Hsrv & Hx & Hempty & Hfinished & HΦ)".
     iLöb as "IH".
     wp_rec. wp_bind (! #p)%E.
     iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
@@ -87,39 +87,12 @@ Section proof.
       wp_load.
       iVs ("Hclose" with "[Hp Hx' Hissued]").
       { iNext. iRight. iLeft. iExists x'. by iFrame. }
-      iVsIntro. wp_match. by iApply ("IH" with "Hx Hempty").
-    + iDestruct "Hinv" as (x' y') "(Hp & Hx' & % & Hissued)".
-      wp_load.
-      destruct (decide (x = x')) as [->|Hneq].
-      { subst.
-        iVs ("Hclose" with "[Hp Hx' Hissued]").
-        { iNext. iRight. iRight. iExists x', y'. by iFrame. }
-        iVsIntro. wp_match.
-        wp_bind (_ <- _)%E.
-        iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
-        - iExFalso. iDestruct "Hinv" as (?) "[_ Ho1]".
-          iCombine "Hempty" "Ho1" as "Hempty".
-          iDestruct (own_valid with "Hempty") as "%". done.
-        - iExFalso. iDestruct "Hinv" as (?) "[_ [_ Ho1]]". 
-          iCombine "Hempty" "Ho1" as "Hempty".
-          iDestruct (own_valid with "Hempty") as "%". done.
-        - iDestruct "Hinv" as (x'' y'') "(Hp & Hx'' & % & Hissued)".
-          iCombine "Hx" "Hx''" as "Hx".
-          destruct (decide (x' = x'')) as [->|Hneq].
-          + wp_store. iVs ("Hclose" with "[Hp Hempty]").
-            { iNext. iLeft. iExists #0. by iFrame. }
-            iVsIntro. wp_seq.
-            iDestruct (own_update with "Hx") as "Hx"; first by apply pair_l_frac_op.
-            iVs "Hx". iVsIntro.
-            by iApply ("HΦ" $! x'' y' with "Hissued Hx").
-          + iExFalso. iDestruct (own_valid with "Hx") as "%".
-            iPureIntro. apply Hneq. destruct H1 as [_ Hag]. apply dec_agree_op_inv in Hag.
-            by inversion Hag. }
-      { iCombine "Hx" "Hx'" as "Hx". iExFalso. iDestruct (own_valid with "Hx") as "%".
-        iPureIntro. apply Hneq. destruct H0 as [_ Hag]. apply dec_agree_op_inv in Hag.
-        by inversion Hag. }
+      iVsIntro. wp_match. by iApply ("IH" with "Hx Hempty Hfinished").
+    + iDestruct "Hinv" as (x' y') "(Hp & Hx' & % & Ho3)".
+      iCombine "Hfinished" "Ho3" as "Hfinished".
+      by iDestruct (own_valid with "Hfinished") as "%".
   Qed.
-                  
+
   Lemma mk_srv_spec (f: val) Q:
     heapN ⊥ N →
     heap_ctx ★ □ (∀ x:val, WP f x {{ v, ■ Q x v }})
@@ -127,14 +100,15 @@ Section proof.
   Proof.
     iIntros (HN) "[#Hh #Hf]".
     wp_let. wp_alloc p as "Hp".
-    iVs (own_alloc (Excl ())) as (γ1) "Hempty"; first done. (* black token *)
-    iVs (own_alloc (Excl ())) as (γ2) "Hissued"; first done. (* white token *)
+    iVs (own_alloc (Excl ())) as (γ1) "Hempty"; first done.
+    iVs (own_alloc (Excl ())) as (γ2) "Hissued"; first done.
+    iVs (own_alloc (Excl ())) as (γ3) "Hfinished"; first done.
     iVs (own_alloc (1%Qp, DecAgree #0)) as (γx) "Hx"; first done.
-    iVs (inv_alloc N _ (srv_inv γx γ1 γ2 p Q) with "[Hp Hempty]") as "#?".
+    iVs (inv_alloc N _ (srv_inv γx γ1 γ2 γ3 p Q) with "[Hp Hempty]") as "#?".
     { iNext. rewrite /srv_inv. iLeft. iExists #0. by iFrame. }
     wp_let. wp_bind (newlock _).
     iApply newlock_spec=>//. iFrame "Hh".
-    iAssert (∃ x, own γx (1%Qp, DecAgree x) ★ own γ2 (Excl ()))%I with "[Hissued Hx]" as "Hinv".
+    iAssert (∃ x, own γx (1%Qp, DecAgree x) ★ own γ2 (Excl ()) ★ own γ3 (Excl ()))%I with "[Hissued Hfinished Hx]" as "Hinv".
     { iExists #0. by iFrame. }
     iFrame "Hinv". iIntros (lk γlk) "#Hlk".
     wp_let. wp_apply wp_fork.
@@ -144,35 +118,41 @@ Section proof.
       iAlways. iIntros (x).
       wp_let. wp_bind (acquire _). iApply acquire_spec.
       iFrame "Hlk". iIntros "Hlked Ho".
-      iDestruct "Ho" as (x') "[Hx Hissued]".
+      iDestruct "Ho" as (x') "[Hx [Hissued Hfinished]]".
       wp_seq. wp_bind (_ <- _)%E.
       iInv N as ">Hinv" "Hclose".
       rewrite /srv_inv.
       iDestruct "Hinv" as "[Hinv|[Hinv|Hinv]]".
       + iDestruct "Hinv" as (x'') "[Hp Hempty]".
         wp_store.
-        iAssert (own γx (1%Qp, DecAgree x') -★ (own γx ((1/2)%Qp, DecAgree x) ★ own γx ((1/2)%Qp, DecAgree x)))%I as "Hsplit".
-        { admit. }
-        iDestruct ("Hsplit" with "Hx") as "[Hx1 Hx2]".
-        iVs ("Hclose" with "[Hp Hissued Hx1]").
+        iAssert (|=r=> own γx (1%Qp, DecAgree x))%I with "[Hx]" as "Ho".
+        { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
+          apply cmra_update_exclusive. done. }
+        iVs "Ho". iDestruct (own_update with "Ho") as "==>[Ho1 Ho2]"; first by apply pair_l_frac_op'.
+        iVs ("Hclose" with "[Hp Hissued Ho1]").
         { rewrite /locked. iNext. iRight. iLeft.
           iExists x. by iFrame. }
-        (* now prove things about wait *)
         iVsIntro. wp_seq.
         wp_bind (wait _).
-        iApply (wait_spec with "[Hempty Hx2 Hlked]"); first by auto.
-        { iFrame "Hh". iFrame "~". iFrame.
-          iIntros (y) "Hempty Hx HQ".
-          wp_let.
-          wp_bind (release _).
-          iApply release_spec.
-          iFrame "Hlk Hlked".
-          iSplitL "Hempty Hx".
-          - iExists x. by iFrame.
-          - by wp_seq.
+        iApply (wait_spec with "[Hempty Hfinished Ho2 Hlked]"); first by done.
+        { iFrame "Hh". iFrame "#". iFrame.
+          iIntros (y3) "[Hempty Hissued] Hx %".
+          wp_let. wp_bind (release _).
+          iApply pvs_wp.
+          iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
+          - admit.
+          - admit.
+          - iDestruct "Hinv" as (x4 y4) "(Hp & _ & _ & Hfinished)".
+            iVs ("Hclose" with "[Hp Hempty]").
+            { iNext. iLeft. iExists y4. by iFrame. }
+            iApply release_spec.
+            iFrame "Hlk Hlked".
+            iSplitL "Hissued Hfinished Hx".
+            { iExists x. by iFrame. }
+            by wp_seq.
         }
-      + (* Impossible: reenter locked *)
-        iExFalso. admit.
-      + (* Impossible: reenter locked *)
-        iExFalso. admit.      
+      + admit.
+      + admit.
+    - (* server side *)
+      
   Admitted.