theories/lecture_notes/ccounter.v

@@ -35,7 +35,7 @@ Section ccounter.
   Qed.
 
   Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ :=
-    (∃ n, own γ₁ (●F n) ∗ γ₂ ⤇½ (Z.of_nat n))%I.
+    (∃ n, own γ₁ (●F n) ∗ γ₂ ⤇[1] (Z.of_nat n))%I.
 
   Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (◯F{q} n) ∗ inv (N .@ "counter") (ccounter_inv γ₁ γ₂)  ∗ Cnt N l γ₂)%I.
 
@@ -73,7 +73,7 @@ Section ccounter.
     iApply (incr_spec N γ₂ _ (own γ₁ (◯F{q} n))%I (λ _, (own γ₁ (◯F{q} (S n))))%I with "[] [Hown]"); first set_solver.
     - iIntros (m) "!# [HOwnElem HP]".
       iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
-      iDestruct (makeElem_eq with "HOwnElem H2") as %->.
+      iDestruct (makeElemAuth_eq with "HOwnElem H2") as %<-.
       iMod (makeElem_update _ _ _ (k+1) with "HOwnElem H2") as "[HOwnElem H2]".
       iMod (own_update_2 with "H1 HP") as "[H1 HP]".
       { apply ccounterRA_update. }
@@ -81,13 +81,44 @@ Section ccounter.
       { iNext; iExists (S k); iFrame.
         rewrite Nat2Z.inj_succ Z.add_1_r //.
       }
-      by iFrame.
+      iModIntro. by iFrame.
     - by iFrame.
     - iNext.
       iIntros (m) "[HCnt' Hown]".
       iApply "HΦ". by iFrame.
   Qed.
 
+  Lemma wk_incr_contrib_spec γ₁ γ₂ ℓ n :
+    {{{ is_ccounter γ₁ γ₂ ℓ 1 n  }}}
+        wk_incr #ℓ
+    {{{ RET #(); is_ccounter γ₁ γ₂ ℓ 1 (S n) }}}.
+  Proof.
+    iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
+    iApply (wk_incr_spec N γ₂ _ (own γ₁ (◯F n))%I (own γ₁ (◯F (S n)))%I with "[] [Hown]"); first set_solver.
+    - iIntros (m) "!# [HOwnElem HP]".
+      iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
+      iDestruct (own_valid_2 with "H1 HP") as %->%ccounterRA_valid_full.
+      iDestruct (makeElemAuth_eq with "HOwnElem H2") as %<-.
+      iMod ("HClose" with "[H1 H2]") as "_".
+      { iNext; iExists k; iFrame. }
+      iModIntro. iFrame "HOwnElem". iIntros (m) "HOwnElem".
+      iInv (N .@ "counter") as (k') "[>H1 >H2]" "HClose".
+      iDestruct (makeElemAuth_eq with "HOwnElem H2") as %<-.
+      iMod (makeElem_update _ _ _ (k+1) with "HOwnElem H2") as "[HOwnElem H2]".
+      iDestruct (own_valid_2 with "H1 HP") as %->%ccounterRA_valid_full.
+      iMod (own_update_2 with "H1 HP") as "[H1 HP]".
+      { apply ccounterRA_update. }
+      iMod ("HClose" with "[H1 H2]") as "_".
+      { iNext; iExists (S k'); iFrame.
+        rewrite Nat2Z.inj_succ Z.add_1_r //.
+      }
+      iModIntro. by iFrame.
+    - by iFrame.
+    - iNext.
+      iIntros "[HCnt' Hown]".
+      iApply "HΦ". by iFrame.
+  Qed.
+
   Lemma read_contrib_spec γ₁ γ₂ ℓ q n :
     {{{ is_ccounter γ₁ γ₂ ℓ q n }}}
         read #ℓ
@@ -97,7 +128,7 @@ Section ccounter.
     wp_apply (read_spec N γ₂ _ (own γ₁ (◯F{q} n))%I (λ m, ⌜n ≤ m⌝ ∗ (own γ₁ (◯F{q} n)))%I with "[] [Hown]"); first set_solver.
     - iIntros (m) "!# [HownE HOwnfrag]".
       iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
-      iDestruct (makeElem_eq with "HownE H2") as %->.
+      iDestruct (makeElemAuth_eq with "HownE H2") as %<-.
       iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
       iMod ("HClose" with "[H1 H2]") as "_".
       { iExists _; by iFrame. }
@@ -118,7 +149,7 @@ Section ccounter.
     wp_apply (read_spec N γ₂ _ (own γ₁ (◯F n))%I (λ m, ⌜Z.of_nat n = m⌝ ∗ (own γ₁ (◯F n)))%I with "[] [Hown]"); first set_solver.
     - iIntros (m) "!# [HownE HOwnfrag]".
       iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
-      iDestruct (makeElem_eq with "HownE H2") as %->.
+      iDestruct (makeElemAuth_eq with "HownE H2") as %<-.
       iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
       iMod ("HClose" with "[H1 H2]") as "_".
       { iExists _; by iFrame. }

theories/lecture_notes/modular_incr.v

@@ -3,13 +3,13 @@
 From iris.program_logic Require Export hoare weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import agree frac frac_auth.
+From iris.algebra Require Import agree frac lib.frac_auth.
 
 From iris.bi.lib Require Import fractional.
 
 From iris.heap_lang.lib Require Import par.
 
-Definition cntCmra : cmraT := prodR fracR (agreeR ZO).
+Definition cntCmra : cmraT := frac_authR (agreeR ZO).
 
 Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
 Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
@@ -36,86 +36,97 @@ Definition wk_incr : val :=
 Section cnt_model.
   Context `{!cntG Σ}.
 
-  Definition makeElem (q : Qp) (m : Z) : cntCmra := (q, to_agree m).
-  Typeclasses Opaque makeElem.
+  Definition makeElemFrag (q : Qp) (m : Z) : cntCmra := ◯F{q} (to_agree m).
+  Definition makeElemAuth (m : Z) : cntCmra := ●F (to_agree m).
+  Typeclasses Opaque makeElemFrag makeElemAuth.
 
-  Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
+  Notation "γ ⤇[ q ] m" := (own γ (makeElemFrag q m))
     (at level 20, q at level 50, format "γ ⤇[ q ]  m") : bi_scope.
-  Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
+  Notation "γ ⤇½ m" := (own γ (makeElemFrag (1/2) m))
     (at level 20, format "γ ⤇½  m") : bi_scope.
+  Notation "γ ⤇ₐ m" := (own γ (makeElemAuth m))
+    (at level 20, format "γ ⤇ₐ  m") : bi_scope.
 
   Global Instance makeElem_fractional γ m: Fractional (λ q, γ ⤇[q] m)%I.
   Proof.
-    intros p q. rewrite /makeElem.
+    intros p q. rewrite /makeElemFrag.
     rewrite -own_op; f_equiv.
-    split; first done.
-    by rewrite /= agree_idemp.
+    rewrite -{1}(agree_idemp (to_agree m)).
+    apply frac_auth_frag_op.
   Qed.
 
   Global Instance makeElem_as_fractional γ m q:
-    AsFractional (own γ (makeElem q m)) (λ q, γ ⤇[q] m)%I q.
+    AsFractional (γ ⤇[q] m)%I (λ q, γ ⤇[q] m)%I q.
   Proof.
     split. done. apply _.
   Qed.
 
-  Global Instance makeElem_Exclusive m: Exclusive (makeElem 1 m).
+  Lemma makeElem_valid2 γ (q1 q2 : Qp) m n : γ ⤇[q1] m -∗ γ ⤇[q2] n -∗ ✓ (q1 + q2)%Qp.
   Proof.
-    rewrite /makeElem. intros [y ?] [H _]. apply (exclusive_l _ _ H).
-  Qed.
-
-  Lemma makeElem_op p q n:
-    makeElem p n ⋅ makeElem q n ≡ makeElem (p + q) n.
-  Proof.
-    rewrite /makeElem; split; first done.
-    by rewrite /= agree_idemp.
+    iIntros "H1 H2". iCombine "H1 H2" as "H".
+    rewrite /makeElemFrag -frac_auth_frag_op.
+    iDestruct (own_valid with "H") as %[HValid _]%frac_auth_frag_valid.
+    by iPureIntro.
   Qed.
 
   Lemma makeElem_eq γ p q (n m : Z):
     γ ⤇[p] n -∗ γ ⤇[q] m -∗ ⌜n = m⌝.
   Proof.
-    iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %HValid.
-    destruct HValid as [_ H2].
+    iIntros "H1 H2".  iCombine "H1 H2" as "H".
+    rewrite /makeElemFrag -frac_auth_frag_op.
+    iDestruct (own_valid with "H") as %[_ HValid]%frac_auth_frag_valid.
     iIntros "!%"; by apply agree_op_invL'.
   Qed.
 
+  Lemma makeElemAuth_eq γ p (n m : Z):
+    γ ⤇ₐ m -∗ γ ⤇[p] n -∗ ⌜n = m⌝.
+  Proof.
+    iIntros "H1 H2".  iCombine "H1 H2" as "H".
+    rewrite /makeElemFrag /makeElemAuth.
+    iDestruct (own_valid with "H") as %HValid%frac_auth_included_total.
+    apply to_agree_included in HValid. by unfold_leibniz.
+  Qed.
+
   Lemma makeElem_entail γ p q (n m : Z):
     γ ⤇[p] n -∗ γ ⤇[q] m -∗ γ ⤇[p + q] n.
   Proof.
     iIntros "H1 H2".
     iDestruct (makeElem_eq with "H1 H2") as %->.
-    iCombine "H1" "H2" as "H".
-    by rewrite makeElem_op.
+    iCombine "H1 H2" as "H".
+    by rewrite /makeElemFrag -frac_auth_frag_op agree_idemp.
   Qed.
 
   Lemma makeElem_update γ (n m k : Z):
-    γ ⤇½ n -∗ γ ⤇½ m ==∗ γ ⤇[1] k.
+    γ ⤇ₐ m -∗ γ ⤇[1] n  ==∗ γ ⤇ₐ k ∗ γ ⤇[1] k.
   Proof.
     iIntros "H1 H2".
-    iDestruct (makeElem_entail with "H1 H2") as "H".
-    rewrite Qp_div_2.
-    iApply (own_update with "H"); by apply cmra_update_exclusive.
+    rewrite -own_op.
+    iApply (own_update_2 with "H1 H2").
+    by apply frac_auth_update_1.
   Qed.
 End cnt_model.
 
-Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
+Notation "γ ⤇[ q ] m" := (own γ (makeElemFrag q m))
   (at level 20, q at level 50, format "γ ⤇[ q ]  m") : bi_scope.
-Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
+Notation "γ ⤇½ m" := (own γ (makeElemFrag (1/2) m))
   (at level 20, format "γ ⤇½  m") : bi_scope.
+Notation "γ ⤇ₐ m" := (own γ (makeElemAuth m))
+  (at level 20, format "γ ⤇ₐ  m") : bi_scope.
 
 Section cnt_spec.
   Context `{!heapG Σ, !cntG Σ} (N : namespace).
 
-  Definition cnt_inv ℓ γ := (∃ (m : Z), ℓ ↦ #m ∗ γ ⤇½ m)%I.
+  Definition cnt_inv ℓ γ := (∃ (m : Z), ℓ ↦ #m ∗ γ ⤇ₐ m)%I.
 
   Definition Cnt (ℓ : loc) (γ : gname) : iProp Σ :=
     inv (N .@ "internal") (cnt_inv ℓ γ).
 
   Lemma Cnt_alloc (E : coPset) (m : Z) (ℓ : loc):
-    (ℓ ↦ #m) ={E}=∗ ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m.
+    (ℓ ↦ #m) ={E}=∗ ∃ γ, Cnt ℓ γ ∗ γ ⤇[1] m.
   Proof.
     iIntros "Hpt".
-    iMod (own_alloc (makeElem 1 m)) as (γ) "[Hown1 Hown2]"; first done.
+    iMod (own_alloc (makeElemAuth m ⋅ makeElemFrag 1 m)) as (γ) "[Hown1 Hown2]".
+    { rewrite /makeElemAuth /makeElemFrag. by apply frac_auth_valid. }
     iMod (inv_alloc (N.@ "internal") _ (cnt_inv ℓ γ)%I with "[Hpt Hown1]") as "#HInc".
     { iExists _; iFrame. }
     iModIntro; iExists _; iFrame "# Hown2".
@@ -123,7 +134,7 @@ Section cnt_spec.
 
   Theorem newcounter_spec (E : coPset) (m : Z):
     ↑(N .@ "internal") ⊆ E →
-    {{{ True }}} newcounter #m @ E {{{ (ℓ : loc), RET #ℓ; ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m}}}.
+    {{{ True }}} newcounter #m @ E {{{ (ℓ : loc), RET #ℓ; ∃ γ, Cnt ℓ γ ∗ γ ⤇[1] m}}}.
   Proof.
     iIntros (Hsubset Φ) "#Ht HΦ".
     rewrite -wp_fupd.
@@ -135,7 +146,7 @@ Section cnt_spec.
 
   Theorem read_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ m, (γ ⤇½ m ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ m ∗ Q m)) ⊢
+    (∀ m, (γ ⤇ₐ m ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ m ∗ Q m)) ⊢
     {{{ Cnt ℓ γ ∗ P}}} read #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m }}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -155,7 +166,7 @@ Section cnt_spec.
 
   Theorem incr_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ (n : Z), γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n) ⊢
+    (∀ (n : Z), γ ⤇ₐ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ (n+1) ∗ Q n) ⊢
     {{{ Cnt ℓ γ ∗ P }}} incr #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m}}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -188,26 +199,24 @@ Section cnt_spec.
       iApply ("IH" with "HP HCont").
   Qed.
 
-  Theorem wk_incr_spec (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
+  Theorem wk_incr_spec (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) :
     ↑(N .@ "internal") ⊆ E →
-    (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q) -∗
-    {{{ Cnt ℓ γ ∗ γ ⤇[q] n ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗ Q}}}.
+    (∀ n, γ ⤇ₐ n ∗ P ={E ∖ ↑(N .@ "internal")}=>
+          γ ⤇ₐ n ∗ (∀ m, γ ⤇ₐ m ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇ₐ (n+1) ∗ Q)) -∗
+    {{{ Cnt ℓ γ ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗ Q }}}.
   Proof.
     iIntros (Hsubset) "#HVS".
-    iIntros (Φ) "!# [#HInc [Hγ HP]] HCont".
-    wp_lam.
-    wp_bind (! _)%E.
+    iIntros (Φ) "!# [#HInc HP] HCont".
+    wp_lam. wp_bind (! _)%E.
     iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
+    iMod ("HVS" with "[$Hown $HP]") as "[Hown HVS']".
     wp_load.
-    iDestruct (makeElem_eq with "Hγ Hown") as %->.
     iMod ("HClose" with "[Hpt Hown]") as "_".
     { iNext; iExists _; iFrame. }
     iModIntro.
-    wp_let.
-    wp_op.
+    wp_pures.
     iInv (N .@ "internal") as (k) "[>Hpt >Hown]" "HClose".
-    iDestruct (makeElem_eq with "Hγ Hown") as %->.
-    iMod ("HVS" with "[$Hown $HP $Hγ]") as "[Hown HQ]".
+    iMod ("HVS'" with "Hown") as "[Hown HQ]".
     wp_store.
     iMod ("HClose" with "[Hpt Hown]") as "_".
     { iNext; iExists _; iFrame. }
@@ -215,13 +224,29 @@ Section cnt_spec.
     iApply "HCont"; by iFrame.
   Qed.
 
-  Theorem wk_incr_spec' (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
+  Theorem wk_incr_spec_seq (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
+    ↑(N .@ "internal") ⊆ E →
+    (γ ⤇ₐ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ (n+1) ∗ Q) -∗
+    {{{ Cnt ℓ γ ∗ γ ⤇[q] n ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗ Q }}}.
+  Proof.
+    iIntros (Hsubset) "#HVS".
+    iIntros (Φ) "!# [#HInc [Hγ HP]] HCont".
+    iApply (wk_incr_spec _ _ (γ ⤇[q] n ∗ P) Q with "[HVS] [$HInc $HP $Hγ] HCont"); first done.
+    iIntros (m). iIntros "!> (Ha & Hγ & HP)".
+    iDestruct (makeElemAuth_eq with "Ha Hγ") as %<-.
+    iModIntro. iFrame. iIntros (m) "Ha".
+    iDestruct (makeElemAuth_eq with "Ha Hγ") as %<-.
+    iMod ("HVS" with "[$Ha $Hγ $HP]") as "[Ha HQ]".
+    iModIntro. by iFrame.
+  Qed.
+
+  Theorem wk_incr_spec_seq' (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
     ↑(N .@ "internal") ⊆ E →
-    (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗  γ ⤇[q] (n + 1) ∗ Q) -∗
+    (γ ⤇ₐ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ (n+1) ∗  γ ⤇[q] (n + 1) ∗ Q) -∗
     {{{ Cnt ℓ γ ∗ γ ⤇[q] n ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗  γ ⤇[q] (n + 1) ∗ Q}}}.
   Proof.
     iIntros (Hsubset) "#HVS".
-    iApply wk_incr_spec; done.
+    iApply wk_incr_spec_seq; done.
 Qed.
 
 End cnt_spec.
@@ -233,9 +258,9 @@ Section incr_twice.
 
   Theorem incr_twice_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q Q' : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ (n : Z), (γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n))
+    (∀ (n : Z), (γ ⤇ₐ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ (n+1) ∗ Q n))
       -∗
-      (∀ (n : Z), γ ⤇½ n ∗ (∃ m, Q m)  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q' n)
+      (∀ (n : Z), γ ⤇ₐ n ∗ (∃ m, Q m)  ={E ∖ ↑(N .@ "internal")}=> γ ⤇ₐ (n+1) ∗ Q' n)
       -∗
       {{{ Cnt N ℓ γ ∗ P }}} incr_twice #ℓ @ E {{{ (m : Z), RET #m; Cnt N ℓ γ ∗ Q' m}}}.
   Proof.
@@ -268,13 +293,13 @@ Section example_1.
     wp_bind (newcounter _)%E.
     wp_apply newcounter_spec; auto; iIntros (ℓ) "H".
     iDestruct "H" as (γ) "[#HInc Hown2]".
-    iMod (inv_alloc (N.@ "external") _ (∃m, own γ (makeElem (1/2) m))%I with "[Hown2]") as "#Hinv".
+    iMod (inv_alloc (N.@ "external") _ (∃m, γ⤇[1] m)%I with "[Hown2]") as "#Hinv".
     { iNext; iExists _; iFrame. }
     iDestruct (incr_spec N γ ⊤ True%I (λ _, True)%I with "[]") as "#HIncr"; eauto.
     { iIntros (n) "!# [Hown _]".
       iInv (N .@ "external") as (m) ">Hownm" "H2".
       iMod (makeElem_update _ _ _ (n + 1) with "Hown Hownm") as "[Hown Hown']".
-      iMod ("H2" with "[Hown]") as "_".
+      iMod ("H2" with "[Hown']") as "_".
       { iExists _; iFrame. }
       iModIntro; iFrame.
     }