Unfix f in flat combiner; Unifies atomic_triple

atomic.v

@@ -5,38 +5,21 @@ From iris.proofmode Require Import tactics.
 Import uPred.
 
 Section atomic.
-  Context `{irisG Λ Σ} {A: Type}.
+  Context `{irisG Λ Σ} (A: Type).
 
-  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
-  Definition atomic_triple
-             (α: A → iProp Σ)
-             (β: A → val _ → iProp Σ)
-             (Ei Eo: coPset)
-             (e: expr _) : iProp Σ :=
-    (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
-                                α x ★
-                                ((α x ={Ei, Eo}=★ P) ∧
-                                 (∀ v, β x v ={Ei, Eo}=★ Q x v))
-            ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
-
-  (* Weakest-pre version of the above one. Also weaker in some sense *)
-  Definition atomic_triple_wp
+  Definition atomic_triple_base
              (α: A → iProp Σ)
              (β: A → val _ → iProp Σ)
              (Ei Eo: coPset)
-             (e: expr _) : iProp Σ :=
-    (∀ P Q, (P ={Eo, Ei}=> ∃ x,
-                              α x ★
-                              ((α x ={Ei, Eo}=★ P) ∧
-                               (∀ v, β x v ={Ei, Eo}=★ Q x v))
-            ) -★ P -★ WP e @ ⊤ {{ v, (∃ x, Q x v) }})%I.
+             (e: expr _) P Q : iProp Σ :=
+    ((P ={Eo, Ei}=> ∃ x:A,
+                       α x ★
+                       ((α x ={Ei, Eo}=★ P) ∧
+                        (∀ v, β x v ={Ei, Eo}=★ Q x v))
+     ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
 
-  Lemma atomic_triple_weaken α β Ei Eo e:
-    atomic_triple α β Ei Eo e ⊢ atomic_triple_wp α β Ei Eo e.
-  Proof.
-    iIntros "H". iIntros (P Q) "Hvs Hp".
-    by iApply ("H" $! P Q with "Hvs").
-  Qed.
+  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
+  Definition atomic_triple α β Ei Eo e := (∀ P Q, atomic_triple_base α β Ei Eo e P Q)%I.
 
   Arguments atomic_triple {_} _ _ _ _.
 End atomic.
@@ -57,11 +40,11 @@ Section incr.
 
   (* TODO: Can we have a more WP-style definition and avoid the equality? *)
   Definition incr_triple (l: loc) :=
-    atomic_triple (fun (v: Z) => l ↦ #v)%I
-                  (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
-                  (nclose heapN)
-                  ⊤
-                  (incr #l).
+    atomic_triple _ (fun (v: Z) => l ↦ #v)%I
+                    (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
+                    (nclose heapN)
+                    ⊤
+                    (incr #l).
 
   Lemma incr_atomic_spec: ∀ (l: loc), heapN ⊥ N → heap_ctx ⊢ incr_triple l.
   Proof.

atomic_sync.v

@@ -13,9 +13,7 @@ Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
 Proof. by intros ?%subG_inG. Qed.
 
 Section atomic_sync.
-  Context `{!heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR val))} (N : namespace).
-
-  Definition A := val. (* FIXME: can't use a general A instead of val *)
+  Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))} (N : namespace).
 
   Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g).
 
@@ -24,15 +22,16 @@ Section atomic_sync.
              (β: val → A → A → val → iProp Σ)
              (Ei Eo: coPset)
              (f x: val) γ : iProp Σ :=
-    (∀ P Q, (∀ g, (P x ={Eo, Ei}=> gHalf γ g ★ □ α x) ★
-                  (gHalf γ g ★ □ α x ={Ei, Eo}=> P x) ★
-                  (∀ g' r, gHalf γ g' ★ β x g g' r ={Ei, Eo}=> Q x r))
-            -★ {{ P x }} f x {{ v, Q x v }})%I.
-
-  Definition sync (syncer: val) : val :=
+    (∀ P Q, atomic_triple_base A (fun g => gHalf γ g ★ □ α x)
+                                 (fun g v => ∃ g':A, gHalf γ g' ★ β x g g' v)
+                                 Ei Eo
+                                (f x) (P x) (fun _ => Q x))%I.
+       
+  Definition sync (mk_syncer: val) : val :=
     λ: "f_cons" "f_seq",
-        let: "l"  := "f_cons" #() in
-        syncer ("f_seq" "l").
+       let: "l" := "f_cons" #() in
+       let: "s" := mk_syncer #() in
+       "s" ("f_seq" "l").
 
   Definition seq_spec (f: val) (ϕ: val → A → iProp Σ) α β (E: coPset) :=
       ∀ (Φ: val → iProp Σ) (l: val),
@@ -48,55 +47,66 @@ Section atomic_sync.
         ⊢ WP f #() {{ Φ }}.
 
   Definition synced R (f' f: val) :=
-    (∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
+    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
+
+  Definition is_syncer (R: iProp Σ) (s: val) :=
+    (∀ (f : val), WP s f {{ f', synced R f' f }})%I.
 
-  Definition mk_sync_spec (syncer: val) :=
-    ∀ f R (Φ: val → iProp Σ),
-      heapN ⊥ N → 
-      heap_ctx ★ R ★ (∀ f', □ synced R f' f -★ Φ f') ⊢ WP syncer f {{ Φ }}.
+  Definition mk_syncer_spec (mk_syncer: val) :=
+    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
   
-  Lemma atomic_spec (syncer f_cons f_seq: val) (ϕ: val → A → iProp Σ) α β Ei:
+  Lemma atomic_spec (mk_syncer f_cons f_seq: val) (ϕ: val → A → iProp Σ) α β Ei:
       ∀ (g0: A),
         heapN ⊥ N → seq_spec f_seq ϕ α β ⊤ → cons_spec f_cons g0 ϕ →
-        mk_sync_spec syncer →
+        mk_syncer_spec mk_syncer →
         heap_ctx
-        ⊢ WP (sync syncer) f_cons f_seq {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
+        ⊢ WP (sync mk_syncer) f_cons f_seq {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
   Proof.
     iIntros (g0 HN Hseq Hcons Hsync) "#Hh". repeat wp_let.
     wp_bind (f_cons _). iApply Hcons=>//. iFrame "Hh".
     iIntros (l γ) "Hϕ HFull HFrag".
-    wp_let. wp_bind (f_seq _)%E.
-    iApply wp_wand_r. iSplitR; first by iApply (Hseq with "[]")=>//.
-    iIntros (f Hf). iApply (Hsync f (∃ g: A, ϕ l g ★ gHalf γ g)%I)=>//.
-    iFrame "#". iSplitL "HFull Hϕ".
+    wp_let. wp_bind (mk_syncer _).
+    iApply (Hsync (∃ g: A, ϕ l g ★ gHalf γ g)%I)=>//. iFrame "Hh".
+    iSplitL "HFull Hϕ".
     { iExists g0. by iFrame. }
-    iIntros (f') "#Hflatten".
+    iIntros (s) "#Hsyncer".
+    wp_let. wp_bind (f_seq _). iApply wp_wand_r.
+    iSplitR; first by iApply (Hseq with "[]")=>//.
+    iIntros (f) "%".
+    iApply wp_wand_r.
+    iSplitR; first iApply "Hsyncer".
+    iIntros (f') "#Hsynced".
     iExists γ. iFrame.
     iIntros (x). iAlways.
     rewrite /atomic_triple'.
     iIntros (P Q) "#Hvss".
     rewrite /synced.
-    iSpecialize ("Hflatten" $! P Q).
-    iApply ("Hflatten" with "[]").
-    iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ HgFull]".
-    (* we should view shift at this point *)
-    iDestruct ("Hvss" $! g) as "[Hvs1 [Hvs2 Hvs3]]".
-    iApply pvs_wp.
-    iVs ("Hvs1" with "HP") as "[HgFrag #Hα]".
-    iVs ("Hvs2" with "[HgFrag]") as "HP"; first by iFrame.
-    iVsIntro. iApply Hf=>//.
-    iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
-    iVs ("Hvs1" with "HP") as "[HgFrag _]".
-    iCombine "HgFull" "HgFrag" as "Hg".
-    rewrite /gHalf.
-    iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I with "[Hg]" as "Hupd".
-    { iApply (own_update); last by iAssumption. apply pair_l_frac_update. }
-    iVs "Hupd" as "[HgFull HgFrag]".
-    iVs ("Hvs3" $! g' ret with "[HgFrag Hβ]"); first by iFrame.
-    iVsIntro.
-    iSplitL "HgFull Hϕ'".
-    - iExists g'. by iFrame.
-    - done.
+    iSpecialize ("Hsynced" $! P Q x). 
+    iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
+    - iApply ("Hsynced" with "[]")=>//.
+      iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
+      (* we should view shift at this point *) 
+      iDestruct ("Hvss" with "HP") as "Hvss'". iApply pvs_wp.
+      iVs "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
+      iVs ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
+      iVsIntro. iApply H=>//.
+      iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
+      iVs ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
+      iSpecialize ("Hvs2" $! ret).
+      iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
+      rewrite Qp_div_2.
+      iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I
+              with "[Hg]" as "==>[Hg1 Hg2]".
+      { iApply own_update; last by iAssumption.
+        apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }        
+      iVs ("Hvs2" with "[Hg1 Hβ]").
+      { iExists g'. iFrame. }
+      iVsIntro. iSplitL "Hg2 Hϕ'".
+      * iExists g'. by iFrame.
+      * done.
+    - iIntros (?) "?". by iExists g0.
   Qed.
-  
+
 End atomic_sync.

misc.v

@@ -84,20 +84,26 @@ End big_op_later.
 
 Section pair.
   Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}.
-  
+
   Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
+    own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2) ⊢ (a1 = a2).
+  Proof.
+    iIntros "[Ho Ho']".
+    destruct (decide (a1 = a2)) as [->|Hneq]=>//.
+    iCombine "Ho" "Ho'" as "Ho".
+    iDestruct (own_valid with "Ho") as %Hvalid.
+    exfalso. destruct Hvalid as [_ Hvalid].
+    simpl in Hvalid. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
+  Qed.
+  
+  Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
     own γm (q1, DecAgree a1) ★ own γm (q2, DecAgree a2)
-    ⊢ |=r=> own γm ((q1 + q2)%Qp, DecAgree a1) ★ (a1 = a2).
+    ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ★ (a1 = a2).
   Proof.
     iIntros "[Ho Ho']".
-    destruct (decide (a1 = a2)) as [->|Hneq].
-    - iSplitL=>//.
-      iCombine "Ho" "Ho'" as "Ho".
-      iDestruct (own_update with "Ho") as "?"; last by iAssumption.
-      by rewrite pair_op frac_op' dec_agree_idemp.
-    - iCombine "Ho" "Ho'" as "Ho".
-      iDestruct (own_valid with "Ho") as %Hvalid.
-      exfalso. destruct Hvalid as [_ Hvalid].
-      simpl in Hvalid. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
+    iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
+    subst. iCombine "Ho" "Ho'" as "Ho".
+    rewrite pair_op frac_op' dec_agree_idemp. by iFrame.
   Qed.
 End pair.
+

simple_sync.v

@@ -7,9 +7,9 @@ From iris_atomic Require Import atomic atomic_sync.
 Import uPred.
 
 Definition mk_sync: val :=
-  λ: "f",
+  λ: <>,
        let: "l" := newlock #() in
-       λ: "x",
+       λ: "f" "x",
           acquire "l";;
           let: "ret" := "f" "x" in
           release "l";;
@@ -20,18 +20,16 @@ Global Opaque mk_sync.
 Section syncer.
   Context `{!heapG Σ, !lockG Σ} (N: namespace).
   
-  Lemma mk_sync_spec (R: iProp Σ) (f: val):
-    ∀ (Φ: val -> iProp Σ),
-      heapN ⊥ N →
-      heap_ctx ★ R ★ (∀ f', □ (synced R f' f) -★ Φ f') ⊢ WP mk_sync f {{ Φ }}.
+  Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
   Proof.
-    iIntros (Φ HN) "(#Hh & HR & HΦ)".
+    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
     wp_seq. wp_bind (newlock _).
     iApply newlock_spec; first done.
     iSplitR "HR HΦ"; first done.
     iFrame "HR".
     iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    rewrite /synced. iIntros (P Q x) "#Hf !# HP".
+    iIntros (f). wp_let. iVsIntro. iAlways.
+    iIntros (P Q x) "#Hf !# HP".
     wp_let. wp_bind (acquire _).
     iApply acquire_spec. iSplit; first done.
     iIntros "Hlocked R". wp_seq. wp_bind (f _).
@@ -42,20 +40,3 @@ Section syncer.
     iFrame. by wp_seq.
   Qed.
 End syncer.
-
-Section atomic_sync.
-  Context `{!heapG Σ, !lockG Σ, !syncG Σ} (N : namespace).
-
-  Lemma mk_sync_atomic_spec (f_cons f_seq: val) (ϕ: val → A → iProp Σ) α β Ei:
-      ∀ (g0: A),
-        heapN ⊥ N → seq_spec N f_seq ϕ α β ⊤ → cons_spec N f_cons g0 ϕ →
-        heap_ctx
-        ⊢ WP (sync mk_sync) f_cons f_seq {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
-  Proof.
-    iIntros (????) "#Hh".
-    iApply (atomic_spec N mk_sync with "[-]")=>//.
-    iIntros (????) "(?&?&?)". iApply (mk_sync_spec N R)=>//.
-    iFrame.
-  Qed.
-  
-End atomic_sync.

treiber.v

@@ -106,8 +106,8 @@ Section proof.
   Qed.
 
   Definition push_triple (s: loc) (x: val) :=
-    atomic_triple (fun xs_hd: list val * loc =>
-                     let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+  atomic_triple _ (fun xs_hd: list val * loc =>
+                       let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
                   (fun xs_hd ret =>
                      let '(xs, hd) := xs_hd in 
                      ∃ hd': loc,
@@ -140,7 +140,7 @@ Section proof.
   Qed.
 
   Definition pop_triple (s: loc) :=
-    atomic_triple (fun xs_hd: list val * loc =>
+  atomic_triple _ (fun xs_hd: list val * loc =>
                      let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
                   (fun xs_hd ret =>
                      let '(xs, hd) := xs_hd in