counter.v 3.46 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.heap_lang Require Export lang.
3
From iris.proofmode Require Import tactics.
4
5
6
7
8
9
From iris.program_logic Require Import auth.
From iris.heap_lang Require Import proofmode notation.

Definition newcounter : val := λ: <>, ref #0.
Definition inc : val :=
  rec: "inc" "l" :=
10
11
12
    let: "n" := !"l" in
    if: CAS "l" "n" (#1 + "n") then #() else "inc" "l".
Definition read : val := λ: "l", !"l".
13
14
15
Global Opaque newcounter inc get.

(** The CMRA we need. *)
16
Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
17
Definition counterΣ : gFunctors := #[authΣ mnatUR].
18

19
20
Instance subG_counterΣ {Σ} : subG counterΣ Σ  counterG Σ.
Proof. intros [? _]%subG_inv. split; apply _. Qed.
21
22

Section proof.
23
Context `{!heapG Σ, !counterG Σ} (N : namespace).
24

25
Definition counter_inv (l : loc) (n : mnat) : iProp Σ := (l  #n)%I.
26

27
Definition counter (l : loc) (n : nat) : iProp Σ :=
28
29
  ( γ, heapN  N  heap_ctx 
        auth_ctx γ N (counter_inv l)  auth_own γ (n:mnat))%I.
30
31
32
33
34

(** The main proofs. *)
Global Instance counter_persistent l n : PersistentP (counter l n).
Proof. apply _. Qed.

35
Lemma newcounter_spec (R : iProp Σ) Φ :
36
  heapN  N 
37
  heap_ctx  ( l, counter l 0 - Φ #l)  WP newcounter #() {{ Φ }}.
38
Proof.
39
  iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
40
  iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
41
    as (γ) "[#? Hγ]"; try by auto.
42
  iVsIntro. iApply "HΦ". rewrite /counter; eauto 10.
43
44
Qed.

45
Lemma inc_spec l j (Φ : val  iProp Σ) :
46
47
48
  counter l j  (counter l (S j) - Φ #())  WP inc #l {{ Φ }}.
Proof.
  iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
49
  iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)".
50
  wp_bind (! _)%E.
51
52
53
  iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
  rewrite {2}/counter_inv.
  wp_load. iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
54
  iVsIntro. wp_let; wp_op. wp_bind (CAS _ _ _).
55
56
  iVs (auth_open (counter_inv l) with "[Hγf]") as (j'') "(% & Hl & Hclose)"; auto.
  rewrite {2}/counter_inv.
57
  destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
58
59
60
61
62
63
64
65
  - wp_cas_suc; first (by do 3 f_equal).
    iVs ("Hclose" $! (1 + j `max` j')%nat with "[Hl]") as "Hγf".
    { iSplit; [iPureIntro|iNext].
      { apply mnat_local_update. abstract lia. }
      rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
      by rewrite Nat2Z.inj_succ -Z.add_1_l. }
    iVsIntro. wp_if.
    iVsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto.
66
67
    iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
  - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
68
69
    iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
    iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
70
71
Qed.

72
Lemma read_spec l j (Φ : val  iProp Σ) :
73
74
75
  counter l j  ( i,  (j  i)%nat  counter l i - Φ #i)
   WP read #l {{ Φ }}.
Proof.
76
  iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)".
77
  rewrite /read /=. wp_let.
78
79
80
81
82
83
84
85
  iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
  wp_load.
  iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf".
  { iSplit; [iPureIntro|iNext].
    { apply mnat_local_update; abstract lia. }
    by rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent. }
  iVsIntro. rewrite !mnat_op_max.
  iApply ("HΦ" with "[%]"); first abstract lia. rewrite /counter; eauto 10.
86
87
Qed.
End proof.