adjust invariant

srv.v

@@ -42,11 +42,11 @@ Definition flat : val :=
 Global Opaque doOp install loop flat.
 
 Definition hdset := gset loc.
-Definition gnmap := gmap loc (dec_agree (gname * gname * gname * gname * gname)).
+Definition gnmap := gmap loc (dec_agree (gname * gname * gname * gname)).
 
 Definition srvR := prodR fracR (dec_agreeR val).
 Definition hdsetR := gset_disjUR loc.
-Definition gnmapR := gmapUR loc (dec_agreeR (gname * gname * gname * gname * gname)).
+Definition gnmapR := gmapUR loc (dec_agreeR (gname * gname * gname * gname)).
 
 Class srvG Σ :=
   SrvG {
@@ -75,162 +75,171 @@ Section proof.
      (∃ (x: val), p ↦ InjLV x ★ own γx ((1/4)%Qp, DecAgree x) ★ own γ2 (Excl ()) ★ own γ4 (Excl ())) ∨
      (∃ (x y: val), p ↦ InjRV y ★ own γx ((1/2)%Qp, DecAgree x) ★ ■ Q x y ★ own γ1 (Excl ()) ★ own γ4 (Excl ())))%I.
 
-  Definition p_inv' (γs: dec_agree (gname * gname * gname * gname * gname)) p Q :=
+  Definition p_inv' γ2 (γs: dec_agree (gname * gname * gname * gname)) p Q :=
     match γs with
       | DecAgreeBot => False%I
-      | DecAgree (γx, γ1, γ2, γ3, γ4) => p_inv γx γ1 γ2 γ3 γ4 p Q
+      | DecAgree (γx, γ1, γ3, γ4) => p_inv γx γ1 γ2 γ3 γ4 p Q
     end.
 
-  Definition srv_inv (γhd γgn: gname) (s: loc) (Q: val → val → Prop) : iProp Σ :=
+  Definition srv_inv (γhd γgn γ2: gname) (s: loc) (Q: val → val → Prop) : iProp Σ :=
     (∃ (hds: hdset) (gnm: gnmap),
        own γhd (● GSet hds) ★ own γgn (● gnm) ★
        (∃ xs: list loc, is_stack s (map (fun x => # (LitLoc x)) xs) ★
                         [★ list] k ↦ x ∈ xs, ■ (x ∈ dom (gset loc) gnm)) ★
        ([★ set] hd ∈ hds, ∃ xs, is_list hd (map (fun x => # (LitLoc x)) xs) ★
                                 [★ list] k ↦ x ∈ xs, ■ (x ∈ dom (gset loc) gnm)) ★
-       ([★ map] p ↦ γs ∈ gnm, p_inv' γs p Q)
+       ([★ map] p ↦ γs ∈ gnm, p_inv' γ2 γs p Q)
     )%I.
 
-  Instance p_inv_timeless γx γ1 γ2 γ3 γ4 p Q: TimelessP (p_inv γx γ1 γ2 γ3 γ4 p Q).  
+  Instance p_inv_timeless γx γ1 γ2 γ3 γ4 p Q: TimelessP (p_inv γx γ1 γ2 γ3 γ4 p Q).
   Proof. apply _. Qed.
 
-  Instance p_inv'_timeless γs p Q: TimelessP (p_inv' γs p Q).
+  Instance p_inv'_timeless γ2 γs p Q: TimelessP (p_inv' γ2 γs p Q).
   Proof.
     rewrite /p_inv'. destruct γs as [γs|].
     - repeat (destruct γs as [γs ?]). apply _.
     - apply _.
   Qed.
 
-  Instance srv_inv_timeless γhd γgn s Q: TimelessP (srv_inv γhd γgn s Q).
+  Instance srv_inv_timeless γhd γgn γ2 s Q: TimelessP (srv_inv γhd γgn γ2 s Q).
   Proof. apply _. Qed.
 
-  Lemma push_spec
-        (Φ: val → iProp Σ) (Q: val → val → Prop)
-        (p: loc) (γx γ1 γ2 γ3 γ4: gname)
-        (γhd γgn: gname) (s: loc) (x: val) :
+  (* Lemma push_spec *)
+  (*       (Φ: val → iProp Σ) (Q: val → val → Prop) *)
+  (*       (p: loc) (γx γ1 γ2 γ3 γ4: gname) *)
+  (*       (γhd γgn: gname) (s: loc) (x: val) : *)
+  (*   heapN ⊥ N → *)
+  (*   heap_ctx ★ inv N (srv_inv γhd γgn s Q) ★ own γx ((1/2)%Qp, DecAgree x) ★ *)
+  (*   p ↦ InjLV x ★ own γ1 (Excl ()) ★ own γ4 (Excl ()) ★ (True -★ Φ #()) *)
+  (*   ⊢ WP push #s #p {{ Φ }}. *)
+  (* Proof. *)
+  (*   iIntros (HN) "(#Hh & #Hsrv & Hp & Hx & Ho1 & Ho4 & HΦ)".     *)
+  (*   iDestruct (push_atomic_spec N s #p with "Hh") as "Hpush"=>//. *)
+  (*   rewrite /push_triple /atomic_triple. *)
+  (*   iSpecialize ("Hpush" $! (p ↦ InjLV x ★ own γ1 (Excl ()) ★ own γ4 (Excl ()) ★ *)
+  (*                            own γx ((1/2)%Qp, DecAgree x))%I *)
+  (*                           (fun _ ret => ret = #())%I with "[]"). *)
+  (*   - iIntros "!#". iIntros "(Hp & Hx & Ho1 & Ho4)". *)
+  (*     (* open the invariant *) *)
+  (*     iInv N as (hds gnm) ">(Hohd & Hogn & Hxs & Hhd & Hps)" "Hclose". *)
+  (*     iDestruct "Hxs" as (xs) "(Hs & Hgn)". *)
+  (*     (* mask magic *) *)
+  (*     iApply pvs_intro'. *)
+  (*     { apply ndisj_subseteq_difference; auto. } *)
+  (*     iIntros "Hvs". *)
+  (*     iExists (map (λ x : loc, #x) xs). *)
+  (*     iFrame "Hs". iSplit. *)
+  (*     + (* provide a way to rollback *) *)
+  (*       iIntros "Hl'". *)
+  (*       iVs "Hvs". iVs ("Hclose" with "[-Hp Hx Ho1 Ho4]"); last by iFrame. *)
+  (*       iNext. rewrite /srv_inv. iExists hds, gnm. *)
+  (*       iFrame. iExists xs. by iFrame. *)
+  (*     + (* provide a way to commit *) *)
+  (*       iIntros (?) "[% Hs]". subst. *)
+  (*       iVs "Hvs". iVs ("Hclose" with "[-]"); last done. *)
+  (*       iNext. rewrite /srv_inv. iExists hds, (gnm ∪ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}). *)
+  (*       iFrame. *)
+  (*       iClear "Hogn". *)
+  (*       iAssert (own γgn (● (gnm ∪ {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) ★ *)
+  (*                own γgn (◯ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}))%I as "[Hogn' Hfrag]". *)
+  (*       { admit. } *)
+  (*       iFrame. iSplitL "Hs Hgn". *)
+  (*       { iExists (p::xs). *)
+  (*         iFrame. admit. } *)
+  (*       iSplitL "Hhd". *)
+  (*       { admit. } *)
+  (*       iAssert (p_inv' (DecAgree (γx, γ1, γ2, γ3, γ4)) p Q)  with "[Hp Hx Ho1 Ho4]" as "Hinvp". *)
+  (*       { rewrite /p_inv' /p_inv. iRight. iLeft. iExists x. by iFrame. } *)
+  (*       admit. *)
+  (*   - iApply wp_wand_r. iSplitR "HΦ". *)
+  (*     + iApply "Hpush". by iFrame. *)
+  (*     + iIntros (?) "H". iDestruct "H" as (?) "%". subst. by iApply "HΦ". *)
+  (* Admitted. *)
+
+  (* Lemma install_spec *)
+  (*       (Φ: val → iProp Σ) (Q: val → val → Prop) *)
+  (*       (x: val) (γhd γgn: gname) (s: loc): *)
+  (*   heapN ⊥ N → *)
+  (*   heap_ctx ★ inv N (srv_inv γhd γgn s Q) ★ *)
+  (*   (∀ (p: loc) (γx γ1 γ2 γ3 γ4: gname), *)
+  (*      own γ2 (Excl ()) -★ own γ3 (Excl ()) -★ own γgn (◯ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}) -★ *)
+  (*      own γx ((1/2)%Qp, DecAgree x) -★ Φ #p) *)
+  (*   ⊢ WP install x #s {{ Φ }}. *)
+  (* Proof. *)
+  (*   iIntros (HN) "(#Hh & #Hsrv & HΦ)". *)
+  (*   wp_seq. wp_let. wp_alloc p as "Hl". *)
+  (*   iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done. *)
+  (*   iVs (own_alloc (Excl ())) as (γ2) "Ho2"; first done. *)
+  (*   iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done. *)
+  (*   iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done. *)
+  (*   iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done. *)
+  (*   iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]". *)
+  (*   { by apply pair_l_frac_op_1'. } *)
+  (*   wp_let. wp_bind ((push _) _). *)
+  (*   iApply push_spec=>//. *)
+  (*   iFrame "Hh Hsrv Hx1 Hl Ho1 Ho4". *)
+  (*   iIntros "_". wp_seq. iVsIntro. *)
+  (*   iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4). *)
+  (*   iAssert (own γgn (◯ {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) as "Hfrag". *)
+  (*   { admit. } *)
+  (*   iApply ("HΦ" with "Ho2 Ho3 Hfrag Hx2"). *)
+  (* Admitted. *)
+
+  (* Definition pinv_sub RI γx γ1 γ2 γ3 γ4 p Q := (RI ⊣⊢ ∃ Rf, Rf ★ p_inv γx γ1 γ2 γ3 γ4 p Q)%I. *)
+
+  (* Lemma doOp_spec Φ (f: val) (RI: iProp Σ) γx γ1 γ2 γ3 γ4 p Q `{TimelessP _ RI}: *)
+  (*   heapN ⊥ N → pinv_sub RI γx γ1 γ2 γ3 γ4 p Q → *)
+  (*   heap_ctx ★ inv N RI ★ own γ2 (Excl ()) ★ *)
+  (*   □ (∀ x:val, WP f x {{ v, ■ Q x v }})%I ★ (own γ2 (Excl ()) -★ Φ #()) *)
+  (*   ⊢ WP doOp f #p {{ Φ }}. *)
+  (* Proof. *)
+  (*   iIntros (HN Hsub) "(#Hh & #HRI & Ho2 & #Hf & HΦ)". *)
+  (*   wp_seq. wp_let. wp_bind (! _)%E. *)
+  (*   iInv N as ">H" "Hclose". *)
+  (*   iDestruct (Hsub with "H") as (Rf) "[HRf [Hp | [Hp | [Hp | Hp]]]]". *)
+  (*   - iDestruct "Hp" as (y) "(Hp & Ho1 & Ho3)". *)
+  (*     wp_load. iVs ("Hclose" with "[HRf Hp Ho1 Ho3]"). *)
+  (*     { iNext. iApply Hsub. iExists Rf. iFrame "HRf". *)
+  (*       iLeft. iExists y. by iFrame. } *)
+  (*     iVsIntro. wp_match. by iApply "HΦ". *)
+  (*   - iDestruct "Hp" as (x) "(Hp & Hx & Ho1 & Ho4)". *)
+  (*     wp_load. *)
+  (*     iAssert (|=r=> own γx (((1 / 4)%Qp, DecAgree x) ⋅ ((1 / 4)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]". *)
+  (*     { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption. *)
+  (*       replace ((1 / 2)%Qp) with (1/4 + 1/4)%Qp; last by apply Qp_div_S. *)
+  (*       by apply pair_l_frac_op'. } *)
+  (*     iVs ("Hclose" with "[HRf Hp Hx1 Ho2 Ho4]"). *)
+  (*     { iNext. iApply Hsub. iExists Rf. iFrame "HRf". *)
+  (*       iRight. iRight. iLeft. iExists x. by iFrame. } *)
+  (*     iVsIntro. wp_match. *)
+  (*     wp_bind (f _). iApply wp_wand_r. *)
+  (*     iSplitR; first by iApply "Hf". *)
+  (*     iIntros (y) "%". *)
+  (*     iInv N as ">H" "Hclose". *)
+  (*     iDestruct (Hsub with "H") as (Rf') "[HRf [Hp | [Hp | [Hp | Hp]]]]". *)
+  (*     + admit. *)
+  (*     + admit. *)
+  (*     + iDestruct "Hp" as (x') "(Hp & Hx & Ho2 & Ho4)". *)
+  (*       destruct (decide (x = x')) as [->|Hneq]; last by admit. *)
+  (*       iCombine "Hx2" "Hx" as "Hx". *)
+  (*       iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op. *)
+  (*       rewrite Qp_div_S. *)
+  (*       wp_store. iVs ("Hclose" with "[HRf Hp Hx Ho1 Ho4]"). *)
+  (*       { iNext. iApply Hsub. iExists Rf'. iFrame "HRf". *)
+  (*         iRight. iRight. iRight. iExists x', y. *)
+  (*         by iFrame. } *)
+  (*       iVsIntro. by iApply "HΦ". *)
+  (*     + admit. *)
+  (*   - admit. *)
+  (*   - admit. *)
+  (* Admitted. *)
+
+  Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) Q (γhd γgn γ2: gname) xs:
     heapN ⊥ N →
-    heap_ctx ★ inv N (srv_inv γhd γgn s Q) ★ own γx ((1/2)%Qp, DecAgree x) ★
-    p ↦ InjLV x ★ own γ1 (Excl ()) ★ own γ4 (Excl ()) ★ (True -★ Φ #())
-    ⊢ WP push #s #p {{ Φ }}.
+    heap_ctx ★ inv N (srv_inv γhd γgn γ2 s Q) ★ □ (∀ x:val, WP f x {{ v, ■ Q x v }})%I ★ own γ2 (Excl ()) ★
+    is_list hd xs ★ own γhd (◯ GSet {[ hd ]}) ★ Φ #()
+    ⊢ WP iter' #hd (doOp f) {{ Φ }}.
   Proof.
-    iIntros (HN) "(#Hh & #Hsrv & Hp & Hx & Ho1 & Ho4 & HΦ)".    
-    iDestruct (push_atomic_spec N s #p with "Hh") as "Hpush"=>//.
-    rewrite /push_triple /atomic_triple.
-    iSpecialize ("Hpush" $! (p ↦ InjLV x ★ own γ1 (Excl ()) ★ own γ4 (Excl ()) ★
+    iIntros (HN) "(#Hh & #? & #Hf & Hxs & Hhd & Ho2 & HΦ)".
+    
+    
\ No newline at end of file
-                             own γx ((1/2)%Qp, DecAgree x))%I
-                            (fun _ ret => ret = #())%I with "[]").
-    - iIntros "!#". iIntros "(Hp & Hx & Ho1 & Ho4)".
-      (* open the invariant *)
-      iInv N as (hds gnm) ">(Hohd & Hogn & Hxs & Hhd & Hps)" "Hclose".
-      iDestruct "Hxs" as (xs) "(Hs & Hgn)".
-      (* mask magic *)
-      iApply pvs_intro'.
-      { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists (map (λ x : loc, #x) xs).
-      iFrame "Hs". iSplit.
-      + (* provide a way to rollback *)
-        iIntros "Hl'".
-        iVs "Hvs". iVs ("Hclose" with "[-Hp Hx Ho1 Ho4]"); last by iFrame.
-        iNext. rewrite /srv_inv. iExists hds, gnm.
-        iFrame. iExists xs. by iFrame.
-      + (* provide a way to commit *)
-        iIntros (?) "[% Hs]". subst.
-        iVs "Hvs". iVs ("Hclose" with "[-]"); last done.
-        iNext. rewrite /srv_inv. iExists hds, (gnm ∪ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}).
-        iFrame.
-        iClear "Hogn".
-        iAssert (own γgn (● (gnm ∪ {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) ★
-                 own γgn (◯ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}))%I as "[Hogn' Hfrag]".
-        { admit. }
-        iFrame. iSplitL "Hs Hgn".
-        { iExists (p::xs).
-          iFrame. admit. }
-        iSplitL "Hhd".
-        { admit. }
-        iAssert (p_inv' (DecAgree (γx, γ1, γ2, γ3, γ4)) p Q)  with "[Hp Hx Ho1 Ho4]" as "Hinvp".
-        { rewrite /p_inv' /p_inv. iRight. iLeft. iExists x. by iFrame. }
-        admit.
-    - iApply wp_wand_r. iSplitR "HΦ".
-      + iApply "Hpush". by iFrame.
-      + iIntros (?) "H". iDestruct "H" as (?) "%". subst. by iApply "HΦ".
-  Admitted.
-
-  Lemma install_spec
-        (Φ: val → iProp Σ) (Q: val → val → Prop)
-        (x: val) (γhd γgn: gname) (s: loc):
-    heapN ⊥ N →
-    heap_ctx ★ inv N (srv_inv γhd γgn s Q) ★
-    (∀ (p: loc) (γx γ1 γ2 γ3 γ4: gname),
-       own γ2 (Excl ()) -★ own γ3 (Excl ()) -★ own γgn (◯ {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}) -★
-       own γx ((1/2)%Qp, DecAgree x) -★ Φ #p)
-    ⊢ WP install x #s {{ Φ }}.
-  Proof.
-    iIntros (HN) "(#Hh & #Hsrv & HΦ)".
-    wp_seq. wp_let. wp_alloc p as "Hl".
-    iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
-    iVs (own_alloc (Excl ())) as (γ2) "Ho2"; first done.
-    iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
-    iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
-    iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
-    iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]".
-    { by apply pair_l_frac_op_1'. }
-    wp_let. wp_bind ((push _) _).
-    iApply push_spec=>//.
-    iFrame "Hh Hsrv Hx1 Hl Ho1 Ho4".
-    iIntros "_". wp_seq. iVsIntro.
-    iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4).
-    iAssert (own γgn (◯ {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) as "Hfrag".
-    { admit. }
-    iApply ("HΦ" with "Ho2 Ho3 Hfrag Hx2").
-  Admitted.
-
-  Definition pinv_sub RI γx γ1 γ2 γ3 γ4 p Q := (RI ⊣⊢ ∃ Rf, Rf ★ p_inv γx γ1 γ2 γ3 γ4 p Q)%I.
-
-  Lemma doOp_spec Φ (f: val) (RI: iProp Σ) γx γ1 γ2 γ3 γ4 p Q `{TimelessP _ RI}:
-    heapN ⊥ N → pinv_sub RI γx γ1 γ2 γ3 γ4 p Q →
-    heap_ctx ★ inv N RI ★ own γ2 (Excl ()) ★
-    □ (∀ x:val, WP f x {{ v, ■ Q x v }})%I ★ (own γ2 (Excl ()) -★ Φ #())
-    ⊢ WP doOp f #p {{ Φ }}.
-  Proof.
-    iIntros (HN Hsub) "(#Hh & #HRI & Ho2 & #Hf & HΦ)".
-    wp_seq. wp_let. wp_bind (! _)%E.
-    iInv N as ">H" "Hclose".
-    iDestruct (Hsub with "H") as (Rf) "[HRf [Hp | [Hp | [Hp | Hp]]]]".
-    - iDestruct "Hp" as (y) "(Hp & Ho1 & Ho3)".
-      wp_load. iVs ("Hclose" with "[HRf Hp Ho1 Ho3]").
-      { iNext. iApply Hsub. iExists Rf. iFrame "HRf".
-        iLeft. iExists y. by iFrame. }
-      iVsIntro. wp_match. by iApply "HΦ".
-    - iDestruct "Hp" as (x) "(Hp & Hx & Ho1 & Ho4)".
-      wp_load.
-      iAssert (|=r=> own γx (((1 / 4)%Qp, DecAgree x) ⋅ ((1 / 4)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]".
-      { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
-        replace ((1 / 2)%Qp) with (1/4 + 1/4)%Qp; last by apply Qp_div_S.
-        by apply pair_l_frac_op'. }
-      iVs ("Hclose" with "[HRf Hp Hx1 Ho2 Ho4]").
-      { iNext. iApply Hsub. iExists Rf. iFrame "HRf".
-        iRight. iRight. iLeft. iExists x. by iFrame. }
-      iVsIntro. wp_match.
-      wp_bind (f _). iApply wp_wand_r.
-      iSplitR; first by iApply "Hf".
-      iIntros (y) "%".
-      iInv N as ">H" "Hclose".
-      iDestruct (Hsub with "H") as (Rf') "[HRf [Hp | [Hp | [Hp | Hp]]]]".
-      + admit.
-      + admit.
-      + iDestruct "Hp" as (x') "(Hp & Hx & Ho2 & Ho4)".
-        destruct (decide (x = x')) as [->|Hneq]; last by admit.
-        iCombine "Hx2" "Hx" as "Hx".
-        iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op.
-        rewrite Qp_div_S.
-        wp_store. iVs ("Hclose" with "[HRf Hp Hx Ho1 Ho4]").
-        { iNext. iApply Hsub. iExists Rf'. iFrame "HRf".
-          iRight. iRight. iRight. iExists x', y.
-          by iFrame. }
-        iVsIntro. by iApply "HΦ".
-      + admit.
-    - admit.
-    - admit.
-  Admitted.
-  
\ No newline at end of file