diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 5065d5b9da83ae667e2bb34c9d41200c9777887c..561b68b60f06b2189e769e0bc5aaaffe557876a5 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -5,12 +5,12 @@ From iris.algebra Require Import frac auth. From iris.heap_lang Require Import proofmode notation. Definition newcounter : val := λ: <>, ref #0. -Definition inc : val := - rec: "inc" "l" := +Definition incr : val := + rec: "incr" "l" := let: "n" := !"l" in - if: CAS "l" "n" (#1 + "n") then #() else "inc" "l". + if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". Definition read : val := λ: "l", !"l". -Global Opaque newcounter inc get. +Global Opaque newcounter incr get. (** Monotone counter *) Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }. @@ -44,8 +44,8 @@ Section mono_proof. iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10. Qed. - Lemma inc_mono_spec l n : - {{{ mcounter l n }}} inc #l {{{ RET #(); mcounter l (S n) }}}. + Lemma incr_mono_spec l n : + {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}. Proof. iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec. iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)". @@ -122,8 +122,8 @@ Section contrib_spec. iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10. Qed. - Lemma inc_contrib_spec γ l q n : - {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} inc #l + Lemma incr_contrib_spec γ l q n : + {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} incr #l {{{ RET #(); ccounter γ q (S n) }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec. diff --git a/tests/counter.v b/tests/counter.v index 7b2c15763c3377e5215aed952f5031173109436e..62251deb90ef392b7e5dbf72a833453a12c1e3b9 100644 --- a/tests/counter.v +++ b/tests/counter.v @@ -11,12 +11,12 @@ From iris.heap_lang Require Import proofmode notation. Import uPred. Definition newcounter : val := λ: <>, ref #0. -Definition inc : val := - rec: "inc" "l" := +Definition incr : val := + rec: "incr" "l" := let: "n" := !"l" in - if: CAS "l" "n" (#1 + "n") then #() else "inc" "l". + if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". Definition read : val := λ: "l", !"l". -Global Opaque newcounter inc read. +Global Opaque newcounter incr read. (** The CMRA we need. *) Inductive M := Auth : nat → M | Frag : nat → M | Bot. @@ -103,8 +103,8 @@ Proof. iModIntro. rewrite /C; eauto 10. Qed. -Lemma inc_spec l n : - {{ C l n }} inc #l {{ v, v = #() ∧ C l (S n) }}. +Lemma incr_spec l n : + {{ C l n }} incr #l {{ v, v = #() ∧ C l (S n) }}. Proof. iIntros "!# Hl /=". iLöb as "IH". wp_rec. iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".