phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_init_loop stk E l i n k f  :
      n = Z.of_nat (i + k) →
      [[{
        (l +ₗ i) ↦∗ replicate k #() ∗
        [∗ list] j ∈ seq i k, WP f #(j : nat) @ stk; E [{ Q j }]
      }]]
        array_init_loop #l #i #n f @ stk; E
      [[{ vs, RET #();
        ⌜ length vs = k ⌝ ∗ (l +ₗ i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
      }]].
Proof.
      iIntros (Hn Φ) "[Hl Hf] HΦ".
      iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
      { rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
        wp_pures. iApply ("HΦ" $! []). auto. }
      rewrite bool_decide_eq_false_2; last naive_solver lia.
      iDestruct (array_cons with "Hl") as "[Hl HSl]".
      iDestruct "Hf" as "[Hf HSf]".
      wp_smart_apply (twp_wand with "Hf") as (v) "Hv". wp_store. wp_pures.
      rewrite Z.add_1_r -Nat2Z.inj_succ.
      iApply ("IH" with "[%] [HSl] HSf"); first lia.
      { by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ. }
      iIntros (vs). iDestruct 1 as (<-) "[HSl Hvs]".
      iApply ("HΦ" $! (v :: vs)). iSplit; [naive_solver|]. iSplitL "Hl HSl".
      - iFrame "Hl". by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ.
      - iEval (rewrite /= Nat.add_0_r; setoid_rewrite Nat.add_succ_r). iFrame.
    Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_init stk E n f :
      (0 < n)%Z →
      {{{
        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E {{ Q i }}
      }}}
        array_init #n f @ stk; E
      {{{ l vs, RET #l;
        ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v
      }}}.
Proof.
      iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
      wp_smart_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n)
        with "[Hl $Hf] [HΦ]") as "!> %vs".
      { by rewrite /= Z2Nat.id; last lia. }
      { by rewrite Loc.add_0. }
      iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
      iApply ("HΦ" $! _ vs). iModIntro. iSplit.
      { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
      rewrite Loc.add_0. iFrame.
    Qed.
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_init stk E n f :
      (0 < n)%Z →
      [[{
        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E [{ Q i }]
      }]]
        array_init #n f @ stk; E
      [[{ l vs, RET #l;
        ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v
      }]].
Proof.
      iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
      wp_smart_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n)
        with "[Hl $Hf] [HΦ]") as "%vs".
      { by rewrite /= Z2Nat.id; last lia. }
      { by rewrite Loc.add_0. }
      iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
      iApply ("HΦ" $! _ vs). iModIntro. iSplit.
      { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
      rewrite Loc.add_0. iFrame.
    Qed.
(* iris_heap_lang/lib/array.v *)
Lemma big_sepL_exists_eq vs :
      ([∗ list] k↦v ∈ vs, ∃ x, ⌜v = g x⌝ ∗ Q k x) -∗
      ∃ xs, ⌜ vs = g <$> xs ⌝ ∗ [∗ list] k↦x ∈ xs, Q k x.
Proof.
      iIntros "Hvs". iInduction vs as [|v vs IH] forall (Q); simpl.
      { iExists []. by auto. }
      iDestruct "Hvs" as "[(%x & -> & Hv) Hvs]".
      iDestruct ("IH" with "Hvs") as (xs ->) "Hxs".
      iExists (x :: xs). by iFrame.
    Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_init_fmap stk E n f :
      (0 < n)%Z →
      {{{
        [∗ list] i ∈ seq 0 (Z.to_nat n),
          WP f #(i : nat) @ stk; E {{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }}
      }}}
        array_init #n f @ stk; E
      {{{ l xs, RET #l;
        ⌜Z.of_nat (length xs) = n⌝ ∗ l ↦∗ (g <$> xs) ∗ [∗ list] k↦x ∈ xs, Q k x
      }}}.
Proof.
      iIntros (Hn Φ) "Hf HΦ". iApply (wp_array_init with "Hf"); first done.
      iIntros "!>" (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
      iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
      iApply "HΦ". iFrame "Hl Hxs". by rewrite length_fmap.
    Qed.
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_init_fmap stk E n f :
      (0 < n)%Z →
      [[{
        [∗ list] i ∈ seq 0 (Z.to_nat n),
          WP f #(i : nat) @ stk; E [{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }]
      }]]
        array_init #n f @ stk; E
      [[{ l xs, RET #l;
        ⌜Z.of_nat (length xs) = n⌝ ∗ l ↦∗ (g <$> xs) ∗ [∗ list] k↦x ∈ xs, Q k x
      }]].
Proof.
      iIntros (Hn Φ) "Hf HΦ". iApply (twp_array_init with "Hf"); first done.
      iIntros (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
      iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
      iApply "HΦ". iFrame "Hl Hxs". by rewrite length_fmap.
    Qed.
(* iris_heap_lang/lib/assert.v *)
Definition assert : val
:=
  λ: "v", if: "v" #() then #() else #0 #0.
(* iris_heap_lang/lib/assert.v *)
(* just below ;; *)
Notation "'assert:' e"
:= (assert (λ: <>, e)%E) (at level 99) : expr_scope.
(* iris_heap_lang/lib/assert.v *)
Notation "'assert:' e"
:= (assert (λ: <>, e)%V) (at level 99) : val_scope.
(* iris_heap_lang/lib/assert.v *)
Lemma twp_assert `{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
  WP (assert: e)%V @ E [{ Φ }].
Proof.
  iIntros "HΦ". wp_lam.
  wp_smart_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
(* iris_heap_lang/lib/assert.v *)
Lemma wp_assert `{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
  WP (assert: e)%V @ E {{ Φ }}.
Proof.
  iIntros "HΦ". wp_lam.
  wp_smart_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
(* This is the namespace that atomic heap implementations may use for their
invariants (the [heap_inv] field of [atomic_heap] below).

We hardcode it since one should have only one instance of [atomic_heap], so
having it as a parameter of this module is unnecessary. An alternative would be
adding it as a field of the class. This however would make it impossible for
the client to open its own invariants around heap operations, as they won't be
able to prove disjointness between their namespaces and the heap's. *)
Definition atomic_heapN
:= nroot .@ "atomic_heap".
(* iris_heap_lang/lib/atomic_heap.v *)
Notation CAS e1 e2 e3
:= (Snd (cmpxchg e1 e2 e3)).
(* iris_heap_lang/lib/atomic_heap.v *)
Definition faa_atomic `{!atomic_heap} : val
:=
  rec: "faa" "l" "n" :=
    let: "m" := load "l" in
    if: CAS "l" "m" ("m" + "n") then "m" else "faa" "l" "n".
(* iris_heap_lang/lib/atomic_heap.v *)
Notation "l ↦ dq v"
:= (pointsto l dq v)
    (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
(* iris_heap_lang/lib/atomic_heap.v *)
Notation "'ref' e"
:= (alloc e) : expr_scope.
(* iris_heap_lang/lib/atomic_heap.v *)
Notation "! e"
:= (load e) : expr_scope.
(* iris_heap_lang/lib/atomic_heap.v *)
Notation "e1 <- e2"
:= (store e1 e2) : expr_scope.
(* iris_heap_lang/lib/atomic_heap.v *)
Notation FAA e1 e2
:= (faa_atomic e1 e2).
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma pointsto_agree l dq1 dq2 v1 v2 :
    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
Proof.
    iIntros "Hl1 Hl2". by iCombine "Hl1" "Hl2" gives %[_ ->].
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma pointsto_combine l dq1 dq2 v1 v2 :
    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
Proof.
    iIntros "Hl1 Hl2".
    iDestruct (pointsto_agree with "[$][$]") as "->".
    by iCombine "Hl1 Hl2" as "$".
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma cas_spec (l : loc) (w1 w2 : val) :
    val_is_unboxed w1 →
    heap_inv -∗
    <<{ ∀∀ v, pointsto l (DfracOwn 1) v }>>
      CAS #l w1 w2 @ ↑atomic_heapN
    <<{ if decide (v = w1)
        then pointsto l (DfracOwn 1) w2 else pointsto l (DfracOwn 1) v
      | RET #(if decide (v = w1) then true else false) }>>.
Proof.
    iIntros (?) "#Hheap %Φ AU".
    awp_apply cmpxchg_spec; [done..|].
    iApply (aacc_aupd_commit with "AU"); first done.
    iIntros (v) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
    iIntros "$ !> HΦ !>". wp_pures. done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma faa_spec (l : loc) (i2 : Z) :
    heap_inv -∗
    <<{ ∀∀ i1 : Z, pointsto l (DfracOwn 1) #i1 }>>
      FAA #l #i2 @ ↑atomic_heapN
    <<{ pointsto l (DfracOwn 1) #(i1 + i2) | RET #i1 }>>.
Proof.
    iIntros "#Hheap %Φ AU". rewrite /faa_atomic. iLöb as "IH".
    wp_pures. awp_apply load_spec; first done.
    iApply (aacc_aupd_abort with "AU"); first done.
    iIntros (i1) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
    iIntros "$ !> AU !>". wp_pures.
    awp_apply cas_spec; [done..|].
    iApply (aacc_aupd with "AU"); first done.
    iIntros (m) "Hl".
    iAaccIntro with "Hl"; first by eauto with iFrame.
    iIntros "Hl"; destruct (decide (#m = #i1)); simplify_eq.
    - iModIntro. iRight. iFrame. iIntros "Hpost". iModIntro. by wp_pures.
    - iModIntro. iLeft. iFrame. iIntros "AU". iModIntro. wp_pure.
      by iApply "IH".
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
(* Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val
:=
  λ: "v", ref "v".
(* iris_heap_lang/lib/atomic_heap.v *)
Definition primitive_free : val
:=
  λ: "v", Free "v".
(* iris_heap_lang/lib/atomic_heap.v *)
Definition primitive_load : val
:=
  λ: "l", !"l".
(* iris_heap_lang/lib/atomic_heap.v *)
Definition primitive_store : val
:=
  λ: "l" "x", "l" <- "x".
(* iris_heap_lang/lib/atomic_heap.v *)
Definition primitive_cmpxchg : val
:=
  λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma primitive_alloc_spec (v : val) :
    True -∗ {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
Proof.
    iIntros "_ %Φ !> _ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma primitive_free_spec (l : loc) (v : val) :
    True -∗ {{{ l ↦ v }}} primitive_free #l {{{ l, RET #l; True }}}.
Proof.
    iIntros "_ %Φ !> Hl HΦ". wp_lam. wp_free. iApply "HΦ". done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma primitive_load_spec (l : loc) :
    True -∗
    <<{ ∀∀ (v : val) q, l ↦{q} v }>> primitive_load #l @ ↑atomic_heapN
    <<{ l ↦{q} v | RET v }>>.
Proof.
    iIntros "_ %Φ AU". wp_lam.
    iMod "AU" as (v q) "[H↦ [_ Hclose]]".
    wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma primitive_store_spec (l : loc) (w : val) :
    True -∗
    <<{ ∀∀ v, l ↦ v }>> primitive_store #l w @ ↑atomic_heapN
    <<{ l ↦ w | RET #() }>>.
Proof.
    iIntros "_ %Φ AU". wp_lam. wp_let.
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
    wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
    val_is_unboxed w1 →
    True -∗
    <<{ ∀∀ (v : val), l ↦ v }>>
      primitive_cmpxchg #l w1 w2 @ ↑atomic_heapN
    <<{ if decide (v = w1) then l ↦ w2 else l ↦ v
      | RET (v, #(if decide (v = w1) then true else false)) }>>.
Proof.
    iIntros (?) "_ %Φ AU". wp_lam. wp_pures.
    iMod "AU" as (v) "[H↦ [_ Hclose]]".
    destruct (decide (v = w1)) as [Heq|Hne];
      [wp_cmpxchg_suc|wp_cmpxchg_fail];
    iMod ("Hclose" with "H↦") as "HΦ"; done.
  Qed.
(* iris_heap_lang/lib/atomic_heap.v *)
(* NOT an instance because users should choose explicitly to use it
     (using [Existing Instance]). *)
Definition primitive_atomic_heap : atomic_heap
:=
  {| atomic_heapGS _ := TCTrue
   ; alloc_spec _ _ _ _ := primitive_alloc_spec
   ; free_spec _ _ _ _ := primitive_free_spec
   ; load_spec _ _ _ _ := primitive_load_spec
   ; store_spec _ _ _ _ := primitive_store_spec
   ; cmpxchg_spec _ _ _ _ := primitive_cmpxchg_spec
   ; pointsto_persist _ _ _ _ := primitive_laws.pointsto_persist |}.
(* iris_heap_lang/lib/clairvoyant_coin.v *)
(* The clairvoyant coin predicts all the values that it will
*non-deterministically* choose throughout the execution of the
program. This can be seen in the spec. The predicate [coin c bs]
expresses that [bs] is the list of all the values of the coin in the
future. The [read_coin] operation always returns the head of [bs] and the
[toss_coin] operation takes the [tail] of [bs]. *)
Definition new_coin: val
:=
  λ: <>, (ref (nondet_bool #()), NewProph).
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Definition read_coin : val
:= λ: "cp", !(Fst "cp").
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Definition toss_coin : val
:=
  λ: "cp",
  let: "c" := Fst "cp" in
  let: "p" := Snd "cp" in
  let: "r" := nondet_bool #() in
  "c" <- "r";; resolve_proph: "p" to: "r";; #().
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Definition prophecy_to_list_bool (vs : list (val * val)) : list bool
:=
    (λ v, bool_decide (v = #true)) ∘ snd <$> vs.
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Definition coin (cp : val) (bs : list bool) : iProp Σ
:=
    ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
       ⌜cp = (#c, #p)%V⌝ ∗
       ⌜bs ≠ []⌝ ∗ ⌜tail bs = prophecy_to_list_bool vs⌝ ∗
       proph p vs ∗
       from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs).
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c bs, RET c; coin c bs }}}.
Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam.
    wp_apply wp_new_proph as (vs p) "Hp"; first done.
    wp_apply nondet_bool_spec as (b) "_"; first done.
    wp_alloc c as "Hc".
    wp_pair.
    iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)).
    rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Lemma read_coin_spec cp bs :
    {{{ coin cp bs }}}
      read_coin cp
    {{{b bs', RET #b; ⌜bs = b :: bs'⌝ ∗ coin cp bs }}}.
Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
    destruct bs as [|b bs]; simplify_eq/=.
    wp_lam. wp_load.
    iApply "HΦ"; iSplitR; first done.
    rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/clairvoyant_coin.v *)
Lemma toss_coin_spec cp bs :
    {{{ coin cp bs }}}
      toss_coin cp
    {{{b bs', RET #(); ⌜bs = b :: bs'⌝ ∗ coin cp bs' }}}.
Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
    destruct bs as [|b bs]; simplify_eq/=.
    wp_lam. do 2 (wp_proj; wp_let).
    wp_apply nondet_bool_spec as (r) "_"; first done.
    wp_store.
    wp_apply (wp_resolve_proph with "[Hp]") as (ws) "[-> Hp]"; first done.
    wp_seq.
    iApply "HΦ"; iSplitR; first done.
    destruct r; rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/counter.v *)
Definition newcounter : val
:= λ: <>, ref #0.
(* iris_heap_lang/lib/counter.v *)
Definition incr : val
:= rec: "incr" "l" :=
    let: "n" := !"l" in
    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
(* iris_heap_lang/lib/counter.v *)
Definition read : val
:= λ: "l", !"l".
(* iris_heap_lang/lib/counter.v *)
(* Monotone counter *)
Class mcounterG Σ
:=
  MCounterG { #[local] mcounter_inG :: inG Σ (authR max_natUR) }.
(* iris_heap_lang/lib/counter.v *)
Definition mcounterΣ : gFunctors
:= #[GFunctor (authR max_natUR)].
(* iris_heap_lang/lib/counter.v *)
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/counter.v *)
Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ
:=
    ∃ n, own γ (● (MaxNat n)) ∗ l ↦ #n.
(* iris_heap_lang/lib/counter.v *)
Definition mcounter (l : loc) (n : nat) : iProp Σ
:=
    ∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (MaxNat n)).
(* iris_heap_lang/lib/counter.v *)
(* The main proofs. *)
Instance mcounter_persistent l n : Persistent (mcounter l n).
Proof. apply _. Qed.
(* iris_heap_lang/lib/counter.v *)
Lemma newcounter_mono_spec :
    {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
    iMod (own_alloc (● (MaxNat O) ⋅ ◯ (MaxNat O))) as (γ) "[Hγ Hγ']";
      first by apply auth_both_valid_discrete.
    iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
    { iNext. iExists 0. by iFrame. }
    iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
  Qed.
(* iris_heap_lang/lib/counter.v *)
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 (γ) "[#? Hγf]".
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as (c') ">[Hγ Hl]".
    destruct (decide (c' = c)) as [->|].
    - iCombine "Hγ Hγf"
        gives %[?%max_nat_included _]%auth_both_valid_discrete.
      iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
      { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
      wp_pures. iApply "HΦ". iModIntro. iExists γ; repeat iSplit; eauto.
      iApply (own_mono with "Hγf").
      (* FIXME: FIXME(Coq #6294): needs new unification *)
      apply: auth_frag_mono. by apply max_nat_included, le_n_S.
    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
      wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
      rewrite {3}/mcounter; eauto 10.
  Qed.
(* iris_heap_lang/lib/counter.v *)
Lemma read_mono_spec l j :
    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝ ∧ mcounter l i }}}.
Proof.
    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
    wp_load.
    iCombine "Hγ Hγf"
      gives %[?%max_nat_included _]%auth_both_valid_discrete.
    iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
    { apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. }
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
  Qed.
(* iris_heap_lang/lib/counter.v *)
(* Counter with contributions *)
Class ccounterG Σ
:=
  CCounterG { #[local] ccounter_inG :: inG Σ (frac_authR natR) }.
(* iris_heap_lang/lib/counter.v *)
Definition ccounterΣ : gFunctors
:=
  #[GFunctor (frac_authR natR)].
(* iris_heap_lang/lib/counter.v *)
Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/counter.v *)
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ
:=
    ∃ n, own γ (●F n) ∗ l ↦ #n.
(* iris_heap_lang/lib/counter.v *)
Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ
:=
    inv N (ccounter_inv γ l).
(* iris_heap_lang/lib/counter.v *)
Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ
:=
    own γ (◯F{q} n).
(* iris_heap_lang/lib/counter.v *)
(* The main proofs. *)
Lemma ccounter_op γ q1 q2 n1 n2 :
    ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2.
Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed.
(* iris_heap_lang/lib/counter.v *)
Lemma newcounter_contrib_spec (R : iProp Σ) :
    {{{ True }}} newcounter #()
    {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
Proof.
    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
    iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']";
      first by apply auth_both_valid_discrete.
    iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
    { iNext. iExists 0. by iFrame. }
    iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
  Qed.
(* iris_heap_lang/lib/counter.v *)
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.
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as (c') ">[Hγ Hl]".
    destruct (decide (c' = c)) as [->|].
    - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
      wp_pures. by iApply "HΦ".
    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
      wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
  Qed.
(* iris_heap_lang/lib/counter.v *)
Lemma read_contrib_spec γ l q n :
    {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
    {{{ c, RET #c; ⌜n ≤ c⌝ ∧ ccounter γ q n }}}.
Proof.
    iIntros (Φ) "[#? Hγf] HΦ".
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
    iCombine "Hγ Hγf" gives % ?%frac_auth_included_total%nat_included.
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
  Qed.
(* iris_heap_lang/lib/counter.v *)
Lemma read_contrib_spec_1 γ l n :
    {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
    {{{ RET #n; ccounter γ 1 n }}}.
Proof.
    iIntros (Φ) "[#? Hγf] HΦ".
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
    iCombine "Hγ Hγf" gives % <-%frac_auth_agree_L.
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/diverge.v *)
(* This library provides a [diverge] function that goes into an infinite loop
when provided with an (arbitrary) argument value. This function can be used to
let the program diverge in corner cases that one wants to omit in proofs. This
mechanism should be used with care and communicated clearly, obviously.

Note that this mechanism only works when establishing partial correctness with
the ordinary version of weakest preconditions, and not when establishing total
correctness using the total version of weakest preconditions.

A typical application for [diverge] is insertion functions for data structures
having a fixed capacity. In such cases, we can choose divergence instead of an
explicit error handling when the full capacity has already been reached. *)
Definition diverge : val
:=
  rec: "diverge" "v" := "diverge" "v".
(* iris_heap_lang/lib/diverge.v *)
Lemma wp_diverge `{!heapGS Σ} s E (Φ : val → iProp Σ) (v : val) :
  ⊢ WP diverge v @ s;E {{ Φ }}.
Proof.
  iLöb as "IH". wp_lam. iApply "IH".
Qed.
(* iris_heap_lang/lib/increment.v *)
Definition incr_phy : val
:=
    rec: "incr" "l" :=
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
         then "oldv" (* return old value if success *)
         else "incr" "l".
(* iris_heap_lang/lib/increment.v *)
Lemma incr_phy_spec (l: loc) :
    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr_phy #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
Proof.
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    (* [iMod] knows how to eliminate [AU] assertions. They are mask-changing
    though so we first need to bind to make sure we have an atomic expression.
    Out of the [AU], we then get the atomic precondition as well as the
    closing updates. There's two closing updates, one to "abort" the update
    and one to "commit"; in this case, we only need the "abort". *)
    wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
    wp_load. iMod ("Hclose" with "Hl") as "AU".
    iModIntro. wp_pures.
    (* As above, but this time we need both the "abort" and "commit" updates. *)
    wp_bind (CmpXchg _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
    destruct (decide (#v = #w)) as [[= ->]|Hx].
    - wp_cmpxchg_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
      iModIntro. wp_pures. done.
    - wp_cmpxchg_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
      iModIntro. wp_pures. iApply "IH". done.
  Qed.
(* iris_heap_lang/lib/increment.v *)
Definition incr : val
:=
    rec: "incr" "l" :=
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
         then "oldv" (* return old value if success *)
         else "incr" "l".