ccounter.v 5.23 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
(* Counter with contributions. A specification derived from the modular
   specification proved in modular_incr module. *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth.

From iris_examples.lecture_notes Require Import modular_incr.

Class ccounterG Σ := CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
Definition ccounterΣ : gFunctors := #[GFunctor (frac_authR natR)].

Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ  ccounterG Σ.
Proof. solve_inG. Qed.

Section ccounter.
  Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace).

  Lemma ccounterRA_valid (m n : natR) (q : frac):  (! m  !{q} n)  (n  m)%nat.
  Proof.
    intros ?.
    (* This property follows directly from the generic properties of the relevant RAs. *)
    by apply nat_included, (frac_auth_included_total q).
  Qed.

  Lemma ccounterRA_valid_full (m n : natR):  (! m  ! n)  (n = m)%nat.
  Proof.
    by intros ?%frac_auth_agree.
  Qed.    

  Lemma ccounterRA_update (m n : natR) (q : frac): (! m  !{q} n) ~~> (! (S m)  !{q} (S n)).
  Proof.
    apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
    lia.
  Qed.

  Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ :=
    ( n, own γ₁ (! n)  γ₂ ⤇½ (Z.of_nat n))%I.

  Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (!{q} n)  inv (N .@ "counter") (ccounter_inv γ₁ γ₂)   Cnt N l γ₂)%I.

  (** The main proofs. *)
  Lemma is_ccounter_op γ₁ γ₂  q1 q2 (n1 n2 : nat) :
    is_ccounter γ₁ γ₂  (q1 + q2) (n1 + n2)%nat  is_ccounter γ₁ γ₂  q1 n1  is_ccounter γ₁ γ₂  q2 n2.
  Proof.
    apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
    - iIntros "[? #?]".
      iFrame "#"; iFrame.
    - iIntros "[[? #?] [? _]]".
      iFrame "#"; iFrame.
  Qed.

  Lemma newcounter_contrib_spec (R : iProp Σ) m:
    {{{ True }}} 
        newcounter #m
    {{{ γ₁ γ₂ , RET #; is_ccounter γ₁ γ₂  1 m%nat }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
    wp_apply newcounter_spec; auto.
    iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
    iMod (own_alloc (! m%nat  ! m%nat)) as (γ₁) "[Hγ Hγ']"; first done.
    iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
    { iNext. iExists _. by iFrame. }
    iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
  Qed.

  Lemma incr_contrib_spec γ₁ γ₂  q n :
    {{{ is_ccounter γ₁ γ₂  q n  }}}
        incr # 
    {{{ (y : Z), RET #y; is_ccounter γ₁ γ₂  q (S n) }}}.
  Proof.
    iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ". 
    iApply (incr_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ _, (own γ₁ (!{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 %->. 
      iMod (makeElem_update _ _ _ (k+1) with "HOwnElem H2") as "[HOwnElem H2]".
      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 //.
      } 
      by iFrame.
    - by iFrame.
    - iNext.
      iIntros (m) "[HCnt' Hown]".
      iApply "HΦ". by iFrame.
  Qed.

  Lemma read_contrib_spec γ₁ γ₂  q n :
    {{{ is_ccounter γ₁ γ₂  q n }}} 
        read #
    {{{ (c : Z), RET #c; Z.of_nat n  c  is_ccounter γ₁ γ₂  q n }}}.
  Proof.
    iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
    wp_apply (read_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ m, n  m  (own γ₁ (!{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 (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
      iMod ("HClose" with "[H1 H2]") as "_".
      { iExists _; by iFrame. }
      iFrame; iIntros "!>!%".
      auto using inj_le.
    - by iFrame.
    - iIntros (i) "[_ [% HQ]]".
      iApply "HΦ".
      iSplit; first by iIntros "!%".
      iFrame; iFrame "#".
  Qed.

  Lemma read_contrib_spec_1 γ₁ γ₂  n :
    {{{ is_ccounter γ₁ γ₂  1%Qp n }}} read #
    {{{ RET #n; is_ccounter γ₁ γ₂  1 n }}}.
  Proof.
    iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
    wp_apply (read_spec N γ₂ _ (own γ₁ (! n))%I (λ m, Z.of_nat n = m  (own γ₁ (! 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 (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
      iMod ("HClose" with "[H1 H2]") as "_".
      { iExists _; by iFrame. }
      iFrame; by iIntros "!>!%".
    - by iFrame.
    - iIntros (i) "[_ [% HQ]]".
      simplify_eq. iApply "HΦ".
      iFrame; iFrame "#".
  Qed.
End ccounter.