HOCAP-like specification for the counter

_CoqProject

@@ -44,6 +44,7 @@ theories/examples/symbol.v
 theories/examples/generative.v
 theories/examples/Y.v
 theories/examples/FAI.v
+theories/examples/hospec/modular_counter.v
 theories/tests/typetest.v
 theories/tests/ghosttp.v
 theories/tests/tactics.v

theories/examples/hospec/modular_counter.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac agree.
+From iris.base_logic.lib Require Import invariants viewshifts.
+From iris_logrel Require Export logrel.
+From iris_logrel.examples Require Import counter.
+
+Definition cntCmra : cmraT := (prodR fracR (agreeR natC)).
+
+Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
+Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
+
+Instance subG_cntΣ {Σ} : subG cntΣ Σ → cntG Σ.
+Proof. solve_inG. Qed.
+
+Definition newcounter : val :=
+  λ: "m", ref "m".
+
+Section cnt_model.
+  Context `{!cntG Σ}.
+
+  Definition makeElem (q : Qp) (m : nat) : cntCmra := (q, to_agree m).
+
+  Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
+    (at level 20, q at level 50, format "γ ⤇[ q ]  m") : uPred_scope.
+  Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
+    (at level 20, format "γ ⤇½  m") : uPred_scope.
+
+  Global Instance makeElem_fractional γ m: Fractional (λ q, γ ⤇[q] m)%I.
+  Proof.
+    intros p q. rewrite /makeElem.
+    rewrite -own_op pair_op agree_idemp; f_equiv.
+  Qed.
+
+  Global Instance makeElem_as_fractional γ m q:
+    AsFractional (own γ (makeElem q m)) (λ q, γ ⤇[q] m)%I q.
+  Proof.
+    split; [ done | apply _ ].
+  Qed.
+
+  Global Instance makeElem_Exclusive m: Exclusive (makeElem 1 m).
+  Proof.
+    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.
+    by rewrite /makeElem pair_op agree_idemp.
+  Qed.
+
+  Lemma makeElem_eq γ p q (n m : nat):
+    γ ⤇[p] n -∗ γ ⤇[q] m -∗ ⌜n = m⌝.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (own_valid_2 with "H1 H2") as %HValid.
+    destruct HValid as [_ H2].
+    iIntros "!%"; by apply agree_op_invL'.
+  Qed.
+
+  Lemma makeElem_entail γ p q (n m : nat):
+    γ ⤇[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.
+  Qed.
+
+  Lemma makeElem_update γ (n m k : nat):
+    γ ⤇½ n -∗ γ ⤇½ m ==∗ γ ⤇[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.
+  Qed.
+End cnt_model.
+
+Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
+  (at level 20, q at level 50, format "γ ⤇[ q ]  m") : uPred_scope.
+Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
+  (at level 20, format "γ ⤇½  m") : uPred_scope.
+
+Section cnt_spec.
+  Context `{!logrelG Σ, !cntG Σ} (N : namespace).
+  Context (HNN : N ## counterN).
+  Context (HNN' : N ## logrelN).
+  Definition cnt_inv ℓ γ := (∃ (m : nat), ℓ ↦ᵢ #m ∗ γ ⤇½ m)%I.
+
+  Definition Cnt (ℓ : loc) (γ : gname) : iProp Σ :=
+    inv (N .@ "internal") (cnt_inv ℓ γ).
+
+  Lemma Cnt_alloc (E : coPset) (m : nat) (ℓ : loc):
+    (ℓ ↦ᵢ #m) ={E}=∗ ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m.
+  Proof.
+    iIntros "Hpt".
+    iMod (own_alloc (makeElem 1 m)) as (γ) "[Hown1 Hown2]"; first done.
+    iMod (inv_alloc (N.@ "internal") _ (cnt_inv ℓ γ)%I with "[Hpt Hown1]") as "#HInc".
+    { iExists _; iFrame. }
+    iModIntro; iExists _; iFrame "# Hown2".
+  Qed.
+
+  (** This type of specification is easy to prove (just like in HOCAP), but it is not very useful, or at least not as useful as the atomic-triples. *)
+  Theorem newcounter_l_useless (m : nat) Δ Γ K t τ :
+    (∀ (ℓ : loc) (γ : gname), Cnt ℓ γ ∗ γ ⤇½ m -∗
+      {Δ;Γ} ⊨ fill K #ℓ ≤log≤ t : τ) -∗
+    ({Δ;Γ} ⊨ fill K (newcounter #m) ≤log≤ t : τ).
+  Proof.
+    iIntros "H". unlock newcounter.
+    rel_rec_l. rel_alloc_l as ℓ "Hl".
+    iMod (Cnt_alloc with "Hl") as (γ) "Hcnt".
+    by iApply "H".
+  Qed.
+
+  (** We are going to make use of alternative invariant opening rules *)
+  Lemma inv_open_cow (E E' : coPset) M P :
+    ↑M ⊆ E → ↑M ⊆ E' → inv M P ={E,E∖↑M}=∗ ▷ P ∗ (▷ P ={E'∖↑M,E'}=∗ True).
+  Proof.
+    iIntros (? ?) "#Hinv".
+    iMod (inv_open_strong E M with "Hinv") as "[HP Hcl]"; first done.
+    iFrame. iIntros "!> HP".
+    iMod ("Hcl" $! E' ∖ ↑M with "HP") as "_".
+    rewrite -union_difference_L; eauto.
+  Qed.
+
+
+(** This specification for the increment function allows us to
+     1) derive the "standard" lifting of unary HOVS specification
+        (by picking E = ∅)
+     2) prove the refinement w.r.t. coarse-grained counter
+        (by picking E = ↑counterN) *)
+  Theorem FG_increment_l (γ : gname) (E : coPset) (ℓ : loc) Δ Γ K t τ:
+    ↑(N .@ "internal") ## E →
+    Cnt ℓ γ -∗
+    (∀ (n : nat),
+       γ ⤇½ n ={⊤∖ ↑(N .@ "internal"), ⊤∖↑(N .@ "internal")∖E}=∗
+       γ ⤇½ (n+1) ∗ {⊤∖E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ) -∗
+    {Δ;Γ} ⊨ fill K (FG_increment #ℓ) ≤log≤ t : τ.
+  Proof.
+    iIntros (?) "#Hcnt Hupd".
+    iLöb as "IH".
+    unlock {2}FG_increment. rel_rec_l.
+    rel_load_l_atomic.
+    iInv (N .@ "internal") as (m) "[>Hl >Hown]" "Hcl".
+    iModIntro. iExists _; iFrame. iNext. iIntros "Hl".
+    iMod ("Hcl" with "[Hl Hown]") as "_".
+    { iNext. iExists _. iFrame. }
+    rel_let_l. rel_op_l.
+    rel_cas_l_atomic.
+    iMod (inv_open_strong with "Hcnt") as "[HH Hcl]"; first done.
+    iDestruct "HH" as (m') "[>Hl >Hown]".
+    iModIntro. iExists _; iFrame.
+    iSplit; iIntros (Hmm'); simplify_eq; iNext; iIntros "Hl"; rel_if_l.
+    - iMod ("Hcl" with "[Hl Hown]") as "_".
+      { iNext. iExists _. iFrame. }
+      rewrite -union_difference_L; last done.
+      unlock FG_increment. iApply ("IH" with "Hupd").
+    - iClear "IH".
+      iMod ("Hupd" with "Hown") as "[Hown Hlog]".
+      assert (⊤ ∖ ↑N.@"internal" ∖ E
+                = ((⊤ ∖ E) ∖ ↑N.@"internal" : coPset)) as -> by set_solver.
+      iMod ("Hcl" with "[Hl Hown]") as "_".
+      { iNext. iExists _. iFrame. assert (S m = m+1) as -> by omega. done. }
+      rewrite -union_difference_L; last set_solver.
+      iApply "Hlog".
+  Qed.
+
+  Definition counter_inv l γ cnt' : iProp Σ :=
+    (∃ n : nat, γ ⤇½ n ∗ l ↦ₛ #false ∗ cnt' ↦ₛ #n)%I.
+
+  Lemma FG_CG_increment_refinement l γ cnt cnt' Δ Γ :
+    Cnt cnt γ -∗
+    inv counterN (counter_inv l γ cnt') -∗
+    {Δ;Γ} ⊨ FG_increment #cnt ≤log≤ CG_increment #cnt' #l : TNat.
+  Proof.
+    iIntros "#Hcnt #Hinv".
+    rel_apply_l
+      (FG_increment_l _ (↑counterN)
+         (* (fun n => γ ⤇½ (n+1) ∗ l ↦ₛ #false ∗ cnt' ↦ₛ #n *)
+         (*        ∗ (▷ counter_inv l γ cnt' ={⊤ ∖ ↑counterN,⊤}=∗ True))%I *)
+         with "Hcnt"); eauto.
+    { solve_ndisj. }
+    (** Proving the view shift *)
+    iIntros (n) "Hγ".
+    iMod (inv_open_cow _ ⊤ counterN with "Hinv") as "[HH Hcl]";
+      [ solve_ndisj | solve_ndisj | idtac ].
+    iDestruct "HH" as (n') "(>Hγ'&>Hl&>Hcnt')".
+    (* iInv counterN as (n') "(>Hγ'&>Hl&>Hcnt')" "Hcl". *)
+    iDestruct (makeElem_eq with "Hγ Hγ'") as %<-.
+    iMod (makeElem_update _ _ _ (n+1) with "Hγ Hγ'") as "[Hγ Hγ']".
+    iModIntro. iFrame.
+    rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl").
+    { solve_ndisj. }
+    iIntros "Hcnt' Hl".
+    iMod ("Hcl" with "[-]") as "_".
+    { iNext. iExists _. iFrame. assert (S n = n+1) as -> by lia; done. }
+    by iApply bin_log_related_nat.
+  Qed.
+
+  (** Proving the refinement with the WP rule doesn't really work out that well: *)
+  Theorem incr_spec (γ : gname) (P : iProp Σ) (Q : nat → iProp Σ) (ℓ : loc):
+    □(∀ (n : nat), γ ⤇½ n ∗ P  ={⊤ ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q n) ⊢
+    {{{ Cnt ℓ γ ∗ P }}} FG_increment #ℓ {{{ (m : nat), RET #m; Cnt ℓ γ ∗ Q m}}}.
+  Proof.
+    iIntros "#HVS".
+    iIntros (Φ) "!# [HInc HP] HCont".
+    iLöb as "IH". unlock FG_increment.
+    wp_rec.
+    wp_bind (! _)%E.
+    iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
+    wp_load.
+    iMod ("HClose" with "[Hpt Hown]") as "_".
+    { iNext; iExists _; iFrame. }
+    iModIntro.
+    wp_let.
+    wp_op.
+    wp_bind (CAS _ _ _)%E.
+    iInv (N .@ "internal") as (m') "[>Hpt >Hown]" "HClose".
+    destruct (decide (m = m')); simplify_eq.
+    - wp_cas_suc.
+      iMod ("HVS" $! m' with "[Hown HP]") as "[Hown HQ]"; first iFrame.
+      iMod ("HClose" with "[Hpt Hown]") as "_".
+      { iNext; iExists _; iFrame. assert (m' + 1 = S m') as -> by lia. done. }
+      iModIntro.
+      wp_if.
+      iApply "HCont"; iFrame.
+    - wp_cas_fail.
+      iMod ("HClose" with "[Hpt Hown]") as "_".
+      { iNext; iExists _; iFrame. }
+      iModIntro.
+      wp_if.
+      iApply ("IH" with "HInc HP HCont").
+  Qed.
+
+  Lemma FG_CG_increment_refinement2 l γ cnt cnt' Δ Γ :
+    Cnt cnt γ -∗
+    inv counterN (counter_inv l γ cnt') -∗
+    {Δ;Γ} ⊨ FG_increment #cnt ≤log≤ CG_increment #cnt' #l : TNat.
+  Proof.
+    iIntros "#Hcnt #Hinv".
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros (vvs ρ)  "#Hspec #HΓ". iIntros (j K) "Hj /=".
+    rewrite /env_subst !Closed_subst_p_id.
+    iModIntro.
+    iApply
+      (incr_spec _
+        (j ⤇ fill K ((CG_increment (#cnt')%E) (#l)%E))%I
+        (fun m => j ⤇ fill K #m)%I with "[] [$Hcnt $Hj]").
+    - iAlways. iIntros (n) "[Hγ Hj]".
+      iInv counterN as (n') "(>Hγ'&>Hl&>Hcnt')" "Hcl".
+      iDestruct (makeElem_eq with "Hγ Hγ'") as %->.
+      unlock CG_increment.
+      tp_rec j.
+      tp_rec j.
+      (* etc, i don't actually have tp_ tactics for locks *)
+      iAssert (|={⊤ ∖ ↑N.@"internal" ∖ ↑counterN}=> j ⤇ fill K #n' ∗ cnt' ↦ₛ #(n' + 1))%I with "[Hj Hcnt']" as "HH".
+      { admit. }
+      iMod "HH" as "[Hj Hcnt']".
+      iMod (makeElem_update _ _ _ (n'+1) with "Hγ Hγ'") as "[Hγ Hγ']".
+      iMod ("Hcl" with "[Hcnt' Hl Hγ']") as "_".
+      { iNext. iExists _; iFrame. }
+      iModIntro. iFrame.
+    - iNext. iIntros (m) "(_ & Hj)".
+      iExists (#m); iFrame "Hj"; eauto.
+  Abort.
+
+End cnt_spec.