almost finish rwlock, only rwlockreadguard drop code left

_CoqProject

@@ -66,6 +66,7 @@ theories/typing/lib/refcell/ref.v
 theories/typing/lib/rwlock/rwlock.v
 theories/typing/lib/rwlock/rwlockreadguard.v
 theories/typing/lib/rwlock/rwlockwriteguard.v
+theories/typing/lib/rwlock/rwlock_code.v
 theories/typing/lib/rwlock/rwlockwriteguard_code.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v

theories/typing/lib/rwlock/rwlock.v

+From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
@@ -99,8 +100,10 @@ Section rwlock_inv.
   Qed.
 
   Lemma rwown_global_reading_st st q ν γs:
-    rwown γs (st_global st) -∗  rwown γs (reading_st q ν) -∗
-    ⌜∃ q' n, st = Some (inr (ν,q',n))⌝.
+    rwown γs (st_global st) -∗ rwown γs (reading_st q ν) -∗
+    ⌜∃ q' n, st = Some (inr (ν,q',n))
+      ∧ ( q' = q ∧ n = 1%positive
+        ∨ (∃ q0, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝.
   Proof.
     iIntros "m r". iCombine "m" "r" as "mr".
     iDestruct (own_valid with "mr") as %[INCL VAL]%auth_valid_discrete_2.
@@ -112,13 +115,40 @@ Section rwlock_inv.
         /Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[a[b[Eqa[Eqb INCL]]]]]]].
       + inversion Eq as [| ?? Eq1 |]. inversion Eq1 as [Eq2].
         inversion Eq2 as [Eq3 ]. simpl in Eq3. apply to_agree_inj in Eq3.
-        inversion Eq3. by do 2 eexists.
+        inversion Eq3. simpl in *. subst. do 2 eexists.
+        split; [done|by left].
       + inversion Eqa. inversion Eqb. subst a b.
-        apply prod_included in INCL as [[INCL%to_agree_included _]%prod_included _].
-        inversion INCL. by do 2 eexists.
+        apply prod_included in INCL as
+          [[INCL%to_agree_included LE1]%prod_included LE2%pos_included].
+        inversion INCL. do 2 eexists. split; [done|]. right. split.
+        * rewrite /= in LE1. destruct LE1 as [q1 LE1]. exists q1. by rewrite -frac_op'.
+        * rewrite -Pplus_one_succ_l Pos.succ_pred => //?. by subst.
     - by apply option_included in INCL as [?|[?[?[?[??]]]]].
   Qed.
 
+  Lemma rwown_update_read_dealloc_1 γs ν q:
+    rwown γs (st_global (Some (inr (ν,q,1%positive)))) -∗ rwown γs (reading_st q ν)
+    ==∗ rwown γs (st_global None).
+  Proof.
+    iIntros "m r". iCombine "m" "r" as "mr".
+    iMod (own_update with "mr") as "$"; [|done].
+    apply auth_update_dealloc.
+    rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+  Qed.
+
+  Lemma rwown_update_read_dealloc γs ν q q' n:
+    rwown γs (st_global (Some (inr (ν,(q + q')%Qp,(1 + n)%positive))))
+    -∗ rwown γs (reading_st q' ν)
+    ==∗ rwown γs (st_global (Some (inr (ν,q,n)))).
+  Proof.
+    iIntros "m r". iCombine "m" "r" as "mr".
+    iMod (own_update with "mr") as "$"; [|done].
+    apply auth_update_dealloc.
+    rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q)
+            -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
+    by apply (cancel_local_update_unit (Some _)), _.
+  Qed.
+
   Lemma rwown_global_writing_st st γs:
     rwown γs (st_global st) -∗  rwown γs writing_st -∗
     ⌜st = (Some (inl tt))⌝.
@@ -145,10 +175,11 @@ Section rwlock_inv.
                   GPS_SWSharedWriter l () #0 γ ∗
                   (∃ n', GPS_SWSharedReader l () #n' 1%Qp γ)
             | Some (inr (ν, q, n)) => (* Locked for read. *)
+                  GPS_SWSharedWriter l () #(Z.pos n) γ ∗
                   ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
                     ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
-                    (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
-                    GPS_SWSharedWriter l () #(Z.pos n) γ ∗
+                    (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗
+                    q'.[ν] ∗
                     (∃ n', GPS_SWSharedReader l () #n' q' γ)
             | _ => (* Locked for write. *) True
             end
@@ -263,8 +294,8 @@ Section rwlock_inv.
       { iIntros (?) "W". iDestruct (GPS_SWRawWriter_RawReader with "W") as "#$".
         iSplitR ""; iExists (Some $ inr (ν, (1/2)%Qp, n)); [|by iFrame "Share"].
         iModIntro. iSplitL ""; [done|]. iFrame "Hst".
-        iExists _. iFrame "Hshr Htok2 Hhν".
         iDestruct (GPS_SWRawWriter_shared with "W") as "[$ [R ?]]".
+        iExists _. iFrame "Hshr Htok2 Hhν".
         iSplitR "R"; last iSplitL ""; [|by rewrite Qp_div_2|by iExists _].
         iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]". }
       iExists γ, γs, tyO, tyS. iModIntro. iFrame "inv EqO EqS". by iExists _.

theories/typing/lib/rwlock/rwlock_code.v

@@ -251,8 +251,8 @@ Section rwlock_functions.
           iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
           destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
           + exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
-          + iDestruct 1 as (?) "[_ #Share]".
-            iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & W & Rs)".
+          + iDestruct 1 as (?) "[_ #Share]". iDestruct "INT" as "[W INT]".
+            iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & Rs)".
             iDestruct "Hqq'" as %Hqq'.
             iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
             iModIntro. iExists (). iSplitL ""; [done|].
@@ -285,7 +285,7 @@ Section rwlock_functions.
             iSplitL "Htok2 rst R1"; last iSplitR "".
             * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
             * iExists st2. subst st2. rewrite /= -Eqst. iSplitL ""; [done|].
-              iFrame "g". iExists _. iFrame "H† Hh Hshr Htok1 W".
+              iFrame "g W". iExists _. iFrame "H† Hh Hshr Htok1".
               rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
             * iExists st2. subst st2. rewrite /= -Eqst. by iFrame "Share".
           + iDestruct "R" as (vR') "[R1 R2]".
@@ -293,7 +293,7 @@ Section rwlock_functions.
             subst q'. rewrite -Eqst /=. iSplitL "Htok2 rst R1"; last iSplitR "".
             * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
             * iExists st2. subst st2. simpl. iSplitL ""; [done|].
-              iFrame "g". iExists _. iFrame "H† Hshr Htok1 W".
+              iFrame "g W". iExists _. iFrame "H† Hshr Htok1".
               iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
               rewrite Qp_div_2. iSplitL ""; [done|by iExists _].
             * iExists st2. subst st2. rewrite /=. by iFrame "Share". }
@@ -409,10 +409,11 @@ Section rwlock_functions.
 
     iNext. simpl.
     iIntros (b v' [])
-            "(INV & _ &[([%%] &_& mst & sst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
+            "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% Neq] & R' & _ & _)])".
     - subst b v'.
-      iMod ("Hclose''" with "[mst INV]") as "Hβtok".
-      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+      iDestruct "R'" as (?) "R'".
+      iMod (GPS_SWSharedWriter_revert with "W R' INV") as "[W INV]".
+      iMod ("Hclose''" with "INV") as "Hβtok".
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_case.
       iApply (type_type  _ _ _
@@ -422,15 +423,11 @@ Section rwlock_functions.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame "Hx Hr".
         iExists γs, β. iSplitL "Hβ"; [by iApply (bor_iff with "[$EqO] Hβ")|].
-        iFrame "Hαβ wst sst".
-        iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
+        iFrame "Hαβ wst". iExists _,_,_. iFrame "W EqO EqS Hinv". by iExists _. }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
     - subst b.
-      iDestruct (rel_exist with "P") as (st') "mst".
-      iDestruct (rel_embed_elim with "mst") as "mst".
-      iMod ("Hclose''" with "[INV mst]") as "Hβtok".
-      { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+      iMod ("Hclose''" with "INV") as "Hβtok".
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_case.
       iApply (type_type _ _ _

theories/typing/lib/rwlock/rwlockreadguard_code.v

@@ -5,7 +5,7 @@ From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-From gpfsl.gps Require Import middleware.
+From gpfsl.gps Require Import middleware protocols.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
@@ -74,7 +74,7 @@ Section rwlockreadguard_functions.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
     iDestruct "Hx'" as (ν q γs β) "(Hx' & #Hαβ & Hν & H◯ & H† & Hinv)".
-    iDestruct "Hinv" as (γ tyO tyS) "(R & (EqO & EqS) & #Hinv)".
+    iDestruct "Hinv" as (γ tyO tyS) "(R & (EqO & EqS & _) & #Hinv)".
     iDestruct "R" as (vR) "R".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
@@ -94,12 +94,20 @@ Section rwlockreadguard_functions.
     set Q : () → vProp Σ := (λ _, True)%I.
     set R : () → lit → vProp Σ := (λ _ _, True)%I.
     set T : () → () → vProp Σ :=
-      (λ _ _,
+      (λ _ _, (q).[ν] ∗
       □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
-      ∃ ν q' st2, (q').[ν] ∗
-        rwown γs (st_global st2) ∗
-       □ tyS (β ⊓ ν) ∗
-       □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]))%I.
+      rwown γs (reading_st q ν) ∗
+      ∃ q' n,
+       ⌜Z_of_rwlock_st st2 = Z.pos n ∧
+        (q' = q ∧ n = 1%positive ∨
+          (∃ q0 : Qp, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝ ∗
+       rwown γs (st_global (Some (inr (ν,q',n)))) ∗
+       (∃ qr, □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+          ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO) ∗
+          □ tyS (β ⊓ ν)  ∗
+          ⌜(q' + qr)%Qp = 1%Qp⌝ ∗
+          (qr).[ν] ∗
+          (∃ n', GPS_SWSharedReader lx' ((): unitProtocol) #n' qr γ)))%I.
     iApply (GPS_SWSharedWriter_CAS_int_strong (rwlock_interp γs β tyO tyS) _
               rwlock_noCAS _ _ _ _ #(Z_of_rwlock_st st2 - 1) () _ _ _
               P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
@@ -109,60 +117,40 @@ Section rwlockreadguard_functions.
     { iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
     { simpl. iSplitR "H◯ Hν"; last iFrame "∗".
       iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"]. iSplitL "".
-      - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [g INT]]".
+      - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [H● INT]]".
         iDestruct "Eqst" as %Eqst.
-        iDestruct (rwown_global_reading_st with "g H◯") as %[q' [n Eqst2']].
-        subst st2'. iDestruct 1 as (?) "[_ #Share]".
+        iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
+        subst st2'. simpl in Eqst. iDestruct 1 as (?) "[_ #Share]". iModIntro.
         iExists (). rewrite Eqst /=. iSplitL ""; [done|].
-        admit.
-      - iIntros ([] _) "T W R". iSplitL ""; [done|].
+        iDestruct "INT" as "[$ INT]". rewrite /T. iFrame "Hν Share H◯".
+        iExists _,_. iFrame "H●". iSplitL""; [by inversion Eqst|]. iFrame "INT".
+      - iIntros ([] _) "(Hν & #Share & H◯ & T) W R". iSplitL ""; [done|].
+        iDestruct "T" as (q' n [Eqst Eq']) "[H● T]".
+        iDestruct "T" as (qr) "(#H† & Hh & #Hshr & Hqrq' & Hqr & Rm)".
+        iDestruct "Hqrq'" as %Hqrq'.
+        iDestruct "Rm" as (?) "Rm".
+        iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
+        iCombine "Hν" "Hqr" as "Hν".
+        destruct Eq' as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
+        + rewrite Hqrq'.
+          iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●". iModIntro.
+          rewrite Eqst /=. iSplitR ""; iExists None; [|by iFrame "Share"].
+          iSplitL ""; [done|]. iFrame "H● W". iSplitR "R"; [|by iExists _].
+          admit.
+          (* iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
+          iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame. *)
+        + rewrite Eqn Qp_plus_comm Eqst.
+          iMod (rwown_update_read_dealloc with "H● H◯") as "H●". iModIntro.
+          have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
+          { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
+          iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
+          iSplitL ""; [done|]. iFrame "H● W".
+          iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν". iSplitR "R"; [|by iExists _].
+          by rewrite Qp_plus_assoc (Qp_plus_comm q0). }
 
-
-    wp_read.
-    iMod ("Hcloseβ" with "[H↦ INV]") as "Hβ"; first by iExists _; iFrame.
-    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
-    iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
-    iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
-    destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
-    + iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}▷=>
-               (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
-        with "[H● H◯ Hx' Hν Hst H†]" as "INV".
-      { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
-           %option_included Hv]%auth_valid_discrete_2.
-        - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
-          intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
-                 %(inj Cinr)%(inj2 pair).
-          iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
-          rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
-          iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
-          iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
-            last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|];
-            [apply union_least; solve_ndisj|].
-          iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
-          iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
-          iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
-          rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
-        - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
-          apply csum_included in Hle.
-          destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
-            [by subst|].
-          destruct Hle as [[Hag [q0 Hq]]%prod_included Hn%pos_included].
-          iDestruct "Hst" as (ν' q'') "(EQν & H†' & Hh & Hshr & Hq & Hν')".
-          iDestruct "EQν" as %EQν. revert Hag Hq. rewrite /= EQν to_agree_included.
-          intros <-%leibniz_equiv ->%leibniz_equiv.
-          iExists (Some (Cinr (to_agree ν, q0, Pos.pred n))).
-          iSplitL "Hlx"; first by destruct n.
-          replace (q ⋅ q0 + q'')%Qp with (q0 + (q + q''))%Qp by
-              by rewrite (comm _ q q0) assoc. iCombine "Hν" "Hν'" as "Hν".
-          iSplitL "H● H◯"; last by eauto with iFrame.
-          iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
-          assert (n = 1%positive ⋅ Pos.pred n) as EQn.
-          { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
-          rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
-          apply (cancel_local_update_unit (reading_st q ν)) , _. }
-      iApply (wp_step_fupd with "INV"). done. set_solver.
-      iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
-      iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
+    iNext. iIntros (b v' []) "(INV & _ & CASE)".
+    iDestruct "CASE" as "[[[% %] _]|[[% NE] [R' [_ [H◯ Hν]]]]]".
+    - subst b v'. iMod ("Hcloseβ" with "INV") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_if.
       iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
@@ -171,14 +159,16 @@ Section rwlockreadguard_functions.
       iApply type_delete; [solve_typing..|].
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_jump; solve_typing.
-    + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
-      iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
+    - subst b. iMod ("Hcloseβ" with "INV") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. wp_if.
       iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
-                tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
+                tctx_hasty_val' //=; simpl.
+        iFrame "Hx". iExists _,_,_,_. iFrame "Hx' Hαβ Hν H◯ H†".
+        iExists _,_,_. iSplitL "R'"; [by iExists _|]. iFrame "EqO EqS Hinv".
+        iExists _. by iFrame "RR". }
       iApply type_jump; solve_typing.
-  Qed.
+  Admitted.
 End rwlockreadguard_functions.