phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma try_acquire_reader_spec γ lk Φ :
    {{{ is_rw_lock γ lk Φ }}}
      try_acquire_reader lk
    {{{ (b : bool), RET #b; if b then ∃ q, reader_locked γ q ∗ Φ q else True }}}.
Proof.
    iIntros (φ) "[#HΦdup (%l & -> & #Hlockinv)] Hφ".
    wp_lam.
    wp_bind (!_)%E.
    iInv "Hlockinv" as (z) "[> Hl Hz]".
    wp_load.
    iSplitL "Hl Hz"; first by eauto with iFrame.
    iModIntro.
    wp_pures.
    destruct (Z.le_dec 0%Z z) as [Hle|?]; last first.
    { rewrite bool_decide_false //.
      wp_pures.
      iApply "Hφ".
      done. }
    rewrite bool_decide_true //.
    wp_pures.
    wp_bind (CmpXchg _ _ _).
    iInv "Hlockinv" as (z') "[> Hl Hz]".
    wp_cmpxchg as [= ->]|?; last first.
    { iSplitR "Hφ".
      { eauto with iFrame. }
      iModIntro.
      wp_pures.
      by iApply "Hφ". }
    iDestruct "Hz" as "[[-> _]|(Hz_ge_0 & %q & %g & Hg)]"; first done.
    iDestruct "Hg" as "(Hauth & %Hsize & %Hfold & HΦ)".
    rewrite -[q in Φ q]Qp.div_2.
    iDestruct ("HΦdup" $! (q / 2)%Qp (q / 2)%Qp with "HΦ") as "[HΦ HΦgive]".
    iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅
      ◯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
    { apply auth_update_alloc.
      rewrite -{2}[({[+ (q / 2)%Qp+]})]gmultiset_disj_union_left_id.
      apply gmultiset_local_update_alloc. }
    iSplitR "HΦgive Hview Hφ".
    { iExists (z + 1)%Z.
      iModIntro.
      iModIntro.
      iFrame.
      iRight.
      iSplitL "Hz_ge_0"; first by eauto with lia.
      iExists _, _.
      iFrame.
      iSplit.
      { iPureIntro.
        rewrite gmultiset_size_disj_union gmultiset_size_singleton.
        lia. }
      iPureIntro.
      rewrite
        gmultiset_set_fold_disj_union
        gmultiset_set_fold_singleton
        -gmultiset_set_fold_comm_acc.
        { rewrite Qp.div_2 //. }
        intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //. }
    iModIntro.
    wp_pures.
    iApply "Hφ".
    eauto with iFrame.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma acquire_reader_spec γ lk Φ :
    {{{ is_rw_lock γ lk Φ }}}
      acquire_reader lk
    {{{ q, RET #(); reader_locked γ q ∗ Φ q }}}.
Proof.
    iIntros (φ) "#Hislock Hφ".
    iLöb as "IH".
    wp_rec.
    wp_apply (try_acquire_reader_spec with "Hislock"); iIntros ([|]).
    - iIntros "[% ?]".
      wp_if_true.
      iApply "Hφ".
      eauto with iFrame.
    - iIntros.
      wp_if_false.
      iApply "IH".
      eauto.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma release_reader_spec γ lk Φ q :
    {{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
      release_reader lk
    {{{ RET #(); True }}}.
Proof.
    iIntros (φ) "((#HΦdup & %l & -> & Hlockinv) & Hlocked & HΦ) Hφ".
    wp_lam.
    wp_bind (FAA _ _).
    iInv "Hlockinv" as (z) "[> Hl Hz]".
    wp_faa.
    unfold reader_locked.
    iDestruct "Hz" as "[[_ Hempty]|(%Hz_ge_0 & %q' & %g & Hg & %Hsize & %Hsum & HΦq')]".
    { iExFalso.
      iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
      multiset_solver. }
    iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as %?.
    { iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
      iPureIntro.
      split; last assumption.
      apply Z2Nat.neq_0_pos.
      rewrite -Hsize gmultiset_size_empty_iff.
      multiset_solver. }
    iCombine "Hg Hlocked" as "Hown".
    iMod (own_update _ _ (●(g ∖ {[+ q +]})) with "Hown") as "Hown".
    { apply auth_update_dealloc.
      replace ε with ({[+ q +]} ∖ {[+ q +]} : gmultiset Qp); last first.
      { rewrite gmultiset_difference_diag //. }
      apply gmultiset_local_update_dealloc.
      multiset_solver. }
    iModIntro.
    iSplitR "Hφ".
    { iExists (z + -1)%Z.
      iFrame.
      iRight.
      iSplit.
      { eauto with lia. }
      iExists _, _.
      iDestruct ("HΦdup" $! q q' with "[$HΦ $HΦq']") as "HΦ".
      iModIntro.
      iFrame.
      iSplit.
      { iPureIntro.
        rewrite gmultiset_size_difference; last multiset_solver.
        rewrite gmultiset_size_singleton.
        lia. }
      iPureIntro.
      rewrite -Hsum gmultiset_set_fold_comm_acc; last first.
      { intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
      rewrite
        -gmultiset_set_fold_singleton
        -gmultiset_set_fold_disj_union
        gmultiset_disj_union_comm
        -gmultiset_disj_union_difference //.
      multiset_solver. }
    wp_pures.
    by iApply "Hφ".
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma try_acquire_writer_spec γ lk Φ :
    {{{ is_rw_lock γ lk Φ }}}
      try_acquire_writer lk
    {{{ (b : bool), RET #b; if b then writer_locked γ ∗ Φ 1%Qp else True }}}.
Proof.
    iIntros (φ) "(#HΦdup & %l & -> & #Hlockinv) Hφ".
    wp_lam.
    wp_bind (CmpXchg _ _ _).
    iInv ("Hlockinv") as (z) "[> Hl Hz]".
    wp_cmpxchg as [= ->]|?; last first.
    { iModIntro.
      iSplitL "Hl Hz".
      { eauto with iFrame. }
      wp_pures.
      by iApply "Hφ". }
    iDestruct "Hz" as "[[%H0_eq_1 ?]|(_ & %q & %g & Hg & %Hsize & %Hfold & HΦ)]".
    { done. }
    apply gmultiset_size_empty_inv in Hsize as ->.
    rewrite gmultiset_set_fold_empty in Hfold. subst q.
    rewrite -[in (●{# 1} _)]Qp.quarter_three_quarter.
    iDestruct "Hg" as "[Hg Hg_give]".
    iModIntro.
    iSplitL "Hl Hg".
    { eauto 10 with iFrame. }
    wp_pures.
    iApply "Hφ".
    by iFrame.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma acquire_writer_spec γ lk Φ :
    {{{ is_rw_lock γ lk Φ }}}
      acquire_writer lk
    {{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}}.
Proof.
    iIntros (φ) "#Hislock Hφ".
    iLöb as "IH".
    wp_rec.
    wp_apply (try_acquire_writer_spec with "Hislock"); iIntros ([|]).
    - iIntros.
      wp_if_true.
      iApply "Hφ".
      eauto with iFrame.
    - iIntros.
      wp_if_false.
      iApply "IH".
      eauto.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma release_writer_spec γ lk Φ :
    {{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
      release_writer lk
    {{{ RET #(); True }}}.
Proof.
    iIntros (φ) "((#HΦdup & %l & -> & #Hlockinv) & Hlocked & HΦ) Hφ".
    wp_lam.
    iInv ("Hlockinv") as (z) "[> Hl Hz]".
    wp_store.
    iDestruct "Hz" as "[[? Hg]|(_ & % & % & Hg_owned & _)]"; last first.
    { iExFalso.
      iCombine "Hg_owned Hlocked" gives %Hvalid.
      rewrite
        auth_auth_dfrac_op_valid
        dfrac_op_own
        dfrac_valid_own in Hvalid.
      by destruct Hvalid as [? _]. }
    iCombine "Hg Hlocked" as "Hown".
    rewrite Qp.quarter_three_quarter.
    iSplitR "Hφ"; first by eauto 15 with iFrame.
    by iApply "Hφ".
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition rw_spin_lock : rwlock
:=
  {| rw_lock.rwlockG := rw_spin_lockG;
     rw_lock.writer_locked_exclusive _ _ _ _ := writer_locked_exclusive;
     rw_lock.writer_locked_not_reader_locked _ _ _ _ := writer_locked_not_reader_locked;
     rw_lock.is_rw_lock_iff _ _ _ _ := is_rw_lock_iff;
     rw_lock.newlock_spec _ _ _ _ := newlock_spec;
     rw_lock.acquire_reader_spec _ _ _ _ := acquire_reader_spec;
     rw_lock.release_reader_spec _ _ _ _ := release_reader_spec;
     rw_lock.acquire_writer_spec _ _ _ _ := acquire_writer_spec;
     rw_lock.release_writer_spec _ _ _ _ := release_writer_spec |}.
(* iris_heap_lang/lib/spawn.v *)
Definition spawn : val
:=
  λ: "f",
    let: "c" := ref NONE in
    Fork ("c" <- SOME ("f" #())) ;; "c".
(* iris_heap_lang/lib/spawn.v *)
Definition join : val
:=
  rec: "join" "c" :=
    match: !"c" with
      SOME "x" => "x"
    | NONE => "join" "c"
    end.
(* iris_heap_lang/lib/spawn.v *)
(* Not bundling heapGS, as it may be shared with other users. *)
Class spawnG Σ
:= SpawnG { #[local] spawn_tokG :: inG Σ (exclR unitO) }.
(* iris_heap_lang/lib/spawn.v *)
Definition spawnΣ : gFunctors
:= #[GFunctor (exclR unitO)].
(* iris_heap_lang/lib/spawn.v *)
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/spawn.v *)
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ
:=
  ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
                  ∃ w, ⌜lv = SOMEV w⌝ ∗ (Ψ w ∨ own γ (Excl ()))).
(* iris_heap_lang/lib/spawn.v *)
Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ
:=
  ∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ).
(* iris_heap_lang/lib/spawn.v *)
Instance spawn_inv_ne n γ l :
  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.
(* iris_heap_lang/lib/spawn.v *)
Instance join_handle_ne n l :
  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.
(* iris_heap_lang/lib/spawn.v *)
(* The main proofs. *)
Lemma spawn_spec (Ψ : val → iProp Σ) (f : val) :
  {{{ WP f #() {{ Ψ }} }}} spawn f {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
  iIntros (Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
  wp_alloc l as "Hl".
  iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
  iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
  { iNext. iExists NONEV. iFrame; eauto. }
  wp_smart_apply (wp_fork with "[Hf]").
  - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
    wp_inj. iInv N as (v') "[Hl _]".
    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
  - wp_pures. iApply "HΦ". rewrite /join_handle. eauto.
Qed.
(* iris_heap_lang/lib/spawn.v *)
Lemma join_spec (Ψ : val → iProp Σ) l :
  {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof.
  iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
    wp_smart_apply ("IH" with "Hγ [HΦ]"). auto.
  - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
      wp_pures. by iApply "HΦ".
    + iCombine "Hγ Hγ'" gives %[].
Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Definition newlock : val
:= λ: <>, ref #false.
(* iris_heap_lang/lib/spin_lock.v *)
Definition try_acquire : val
:= λ: "l", CAS "l" #false #true.
(* iris_heap_lang/lib/spin_lock.v *)
Definition acquire : val
:=
  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
(* iris_heap_lang/lib/spin_lock.v *)
Definition release : val
:= λ: "l", "l" <- #false.
(* iris_heap_lang/lib/spin_lock.v *)
(* The CMRA we need. *)
Class spin_lockG Σ
:= LockG { #[local] lock_tokG :: tokenG Σ }.
(* iris_heap_lang/lib/spin_lock.v *)
Definition spin_lockΣ : gFunctors
:= #[tokenΣ].
(* iris_heap_lang/lib/spin_lock.v *)
Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Let N
:= nroot .@ "spin_lock".
(* iris_heap_lang/lib/spin_lock.v *)
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ
:=
    ∃ b : bool, l ↦ #b ∗ if b then True else token γ ∗ R.
(* iris_heap_lang/lib/spin_lock.v *)
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ
:=
    ∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R).
(* iris_heap_lang/lib/spin_lock.v *)
Definition locked (γ : gname) : iProp Σ
:= token γ.
(* iris_heap_lang/lib/spin_lock.v *)
Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
(* iris_heap_lang/lib/spin_lock.v *)
(* The main proofs. *)
Lemma is_lock_iff γ lk R1 R2 :
    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2.
Proof.
    iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
    iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
    iIntros "!> !>"; iSplit; iDestruct 1 as (b) "[Hl H]";
      iExists b; iFrame "Hl"; destruct b;
      first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
  Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Lemma newlock_spec_delay_init :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; ∀ R E, R ={E}=∗ is_lock γ lk R }}}.
Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam. wp_alloc l as "Hl".
    iMod token_alloc as (γ) "Hγ".
    iApply "HΦ".
    iIntros "!> %R %E HR".
    iMod (inv_alloc N _ (lock_inv γ l R) with "[-]") as "#?".
    { iIntros "!>". iExists false. by iFrame. }
    iExists l. eauto.
  Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Lemma try_acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} try_acquire lk
    {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
Proof.
    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
    wp_rec. wp_bind (CmpXchg _ _ _). iInv N as ([]) "[Hl HR]".
    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl". { iNext. iExists true; eauto. }
      wp_pures. iApply ("HΦ" $! false). done.
    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
      iModIntro. iSplitL "Hl". { iNext; iExists true; eauto. }
      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
  Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Lemma acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; auto with iFrame.
    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
  Qed.
(* iris_heap_lang/lib/spin_lock.v *)
Lemma release_spec γ lk R :
    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
    iDestruct "Hlock" as (l ->) "#Hinv".
    rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
    iModIntro. iNext. iExists false. by iFrame.
  Qed.
(* iris_heap_lang/lib/spin_lock.v *)
(* NOT an instance because users should choose explicitly to use it
     (using [Existing Instance]). *)
Definition spin_lock : lock
:=
  {| lock.lockG := spin_lockG;
     lock.locked_exclusive _ _ _ _ := locked_exclusive;
     lock.is_lock_iff _ _ _ _ := is_lock_iff;
     lock.newlock_spec_delay_init _ _ _ _ := newlock_spec_delay_init;
     lock.acquire_spec _ _ _ _ := acquire_spec;
     lock.release_spec _ _ _ _ := release_spec |}.
(* iris_heap_lang/lib/ticket_lock.v *)
Definition wait_loop: val
:=
  rec: "wait_loop" "x" "lk" :=
    let: "o" := !(Fst "lk") in
    if: "x" = "o"
      then #() (* my turn *)
      else "wait_loop" "x" "lk".
(* iris_heap_lang/lib/ticket_lock.v *)
Definition newlock : val
:=
  λ: <>, ((* owner *) ref #0, (* next *) ref #0).
(* iris_heap_lang/lib/ticket_lock.v *)
Definition acquire : val
:=
  rec: "acquire" "lk" :=
    let: "n" := !(Snd "lk") in
    if: CAS (Snd "lk") "n" ("n" + #1)
      then wait_loop "n" "lk"
      else "acquire" "lk".
(* iris_heap_lang/lib/ticket_lock.v *)
Definition release : val
:=
  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
(* iris_heap_lang/lib/ticket_lock.v *)
(* The CMRAs we need. *)
Class tlockG Σ
:=
  #[local] tlock_G ::
    inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
(* iris_heap_lang/lib/ticket_lock.v *)
Definition tlockΣ : gFunctors
:=
  #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
(* iris_heap_lang/lib/ticket_lock.v *)
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Let N
:= nroot .@ "ticket_lock".
(* iris_heap_lang/lib/ticket_lock.v *)
Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ
:=
    ∃ o n : nat,
      lo ↦ #o ∗ ln ↦ #n ∗
      own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))).
(* iris_heap_lang/lib/ticket_lock.v *)
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ
:=
    ∃ lo ln : loc,
      ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R).
(* iris_heap_lang/lib/ticket_lock.v *)
Definition issued (γ : gname) (x : nat) : iProp Σ
:=
    own γ (◯ (ε, GSet {[ x ]})).
(* iris_heap_lang/lib/ticket_lock.v *)
Definition locked (γ : gname) : iProp Σ
:= ∃ o, own γ (◯ (Excl' o, GSet ∅)).
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
Proof.
    iIntros "[%σ1 H1] [%σ2 H2]".
    iCombine "H1 H2" gives %[[] _]%auth_frag_op_valid_1.
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma is_lock_iff γ lk R1 R2 :
    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2.
Proof.
    iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
    iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
    iIntros "!> !>"; iSplit; iIntros "(%o & %n & Ho & Hn & H● & H)";
      iExists o, n; iFrame "Ho Hn H●";
      (iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]).
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma newlock_spec_delay_init :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; ∀ R E, R ={E}=∗ is_lock γ lk R }}}.
Proof.
    iIntros (Φ) "_ HΦ". wp_lam.
    wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
    iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
    { by apply auth_both_valid_discrete. }
    wp_pures. iApply "HΦ".
    iIntros "!> %R %E HR".
    iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-]").
    { iNext. rewrite /lock_inv.
      iExists 0, 0. auto with iFrame. }
    iExists lo, ln. eauto.
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma wait_loop_spec γ lk x R :
    {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iLöb as "IH". wp_rec. subst. wp_pures. wp_bind (! _)%E.
    iInv N as (o n) "(Hlo & Hln & Ha)".
    wp_load. destruct (decide (x = o)) as [->|Hneq].
    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
      + iModIntro. iFrame "Hlo Hln Hainv Ht".
        wp_pures. case_bool_decide; [|done]. wp_if.
        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame.
      + iCombine "Ht Haown"
          gives %[_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
        set_solver.
    - iModIntro. iFrame "Hlo Hln Ha".
      wp_pures. case_bool_decide; [simplify_eq |].
      wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
    iInv N as (o n) "[Hlo [Hln Ha]]".
    wp_load. iModIntro. iFrame "Hlo Hln Ha".
    wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
    - iMod (own_update with "Hauth") as "[Hauth Hofull]".
      { eapply auth_update_alloc, prod_local_update_2.
        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
        apply (set_seq_S_end_disjoint 0). }
      rewrite -(set_seq_S_end_union_L 0).
      wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
      { iNext. iExists o', (S n).
        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
      wp_pures.
      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
      + rewrite /is_lock; eauto 10.
      + by iNext.
    - wp_cmpxchg_fail. iModIntro. iFrame "Hlo' Hln' Hauth Haown".
      wp_pures. by iApply "IH"; auto.
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Lemma release_spec γ lk R :
    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iDestruct "Hγ" as (o) "Hγo".
    wp_lam. wp_proj. wp_bind (! _)%E.
    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
    wp_load.
    iCombine "Hauth Hγo" gives
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
    iModIntro. iFrame. wp_pures.
    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
    iApply wp_fupd. wp_store.
    iCombine "Hauth Hγo" gives
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
    iDestruct "Haown" as "[[Hγo' _]|Haown]".
    { iCombine "Hγo Hγo'" gives %[[] ?]%auth_frag_op_valid_1. }
    iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
    { apply auth_update, prod_local_update_1.
      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
    iIntros "!> !>". iExists (S o), n'.
    rewrite Nat2Z.inj_succ -Z.add_1_r. auto with iFrame.
  Qed.
(* iris_heap_lang/lib/ticket_lock.v *)
Definition ticket_lock : lock
:=
  {| lock.lockG := tlockG;
     lock.locked_exclusive _ _ _ _ := locked_exclusive;
     lock.is_lock_iff _ _ _ _ := is_lock_iff;
     lock.newlock_spec_delay_init _ _ _ _ := newlock_spec_delay_init;
     lock.acquire_spec _ _ _ _ := acquire_spec;
     lock.release_spec _ _ _ _ := release_spec |}.
(* iris_heap_lang/lib/unwrap.v *)
(* The function [unwrap o] (unsafely) asserts that [o] is [SOMEV v],
and returns the contained value [v]. *)
Definition unwrap : val
:= λ: "o",
  match: "o" with
    NONE => assert: #false
  | SOME "v" => "v"
  end.
(* iris_heap_lang/lib/unwrap.v *)
Lemma unwrap_spec Φ v : ▷ Φ v ⊢ WP unwrap (SOMEV v) {{ Φ }}.
Proof. iIntros "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
(* iris_unstable/algebra/list.v *)
Instance list_op_instance : Op (list A)
:=
    fix go l1 l2 := let _ : Op _ := @go in
    match l1, l2 with
    | [], _ => l2
    | _, [] => l1
    | x :: l1, y :: l2 => x ⋅ y :: l1 ⋅ l2
    end.
(* iris_unstable/algebra/list.v *)
Instance list_pcore_instance : PCore (list A)
:= λ l, Some (core <$> l).
(* iris_unstable/algebra/list.v *)
Instance list_valid_instance : Valid (list A)
:= Forall (λ x, ✓ x).
(* iris_unstable/algebra/list.v *)
Instance list_validN_instance : ValidN (list A)
:= λ n, Forall (λ x, ✓{n} x).
(* iris_unstable/algebra/list.v *)
Lemma cons_valid l x : ✓ (x :: l) ↔ ✓ x ∧ ✓ l.
Proof. apply Forall_cons. Qed.
(* iris_unstable/algebra/list.v *)
Lemma cons_validN n l x : ✓{n} (x :: l) ↔ ✓{n} x ∧ ✓{n} l.
Proof. apply Forall_cons. Qed.
(* iris_unstable/algebra/list.v *)
Lemma app_valid l1 l2 : ✓ (l1 ++ l2) ↔ ✓ l1 ∧ ✓ l2.
Proof. apply Forall_app. Qed.
(* iris_unstable/algebra/list.v *)
Lemma app_validN n l1 l2 : ✓{n} (l1 ++ l2) ↔ ✓{n} l1 ∧ ✓{n} l2.
Proof. apply Forall_app. Qed.
(* iris_unstable/algebra/list.v *)
Lemma list_lookup_valid l : ✓ l ↔ ∀ i, ✓ (l !! i).
Proof.
    rewrite {1}/valid /list_valid_instance Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Qed.
(* iris_unstable/algebra/list.v *)
Lemma list_lookup_validN n l : ✓{n} l ↔ ∀ i, ✓{n} (l !! i).
Proof.
    rewrite {1}/validN /list_validN_instance Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Qed.
(* iris_unstable/algebra/list.v *)
Lemma list_lookup_op l1 l2 i : (l1 ⋅ l2) !! i = l1 !! i ⋅ l2 !! i.
Proof.
    revert i l2. induction l1 as [|x l1]; intros [|i] [|y l2];
      by rewrite /= ?left_id_L ?right_id_L.
  Qed.
(* iris_unstable/algebra/list.v *)
Lemma list_lookup_core l i : core l !! i = core (l !! i).
Proof.
    rewrite /core /= list_lookup_fmap.
    destruct (l !! i); by rewrite /= ?Some_core.
  Qed.
(* iris_unstable/algebra/list.v *)
Lemma list_lookup_included l1 l2 : l1 ≼ l2 ↔ ∀ i, l1 !! i ≼ l2 !! i.
Proof.
    split.
    { intros [l Hl] i. exists (l !! i). by rewrite Hl list_lookup_op. }
    revert l1. induction l2 as [|y l2 IH]=>-[|x l1] Hl.
    - by exists [].
    - destruct (Hl 0) as [[z|] Hz]; inversion Hz.
    - by exists (y :: l2).
    - destruct (IH l1) as [l3 ?]; first (intros i; apply (Hl (S i))).
      destruct (Hl 0) as [[z|] Hz]; inversion_clear Hz; simplify_eq/=.
      + exists (z :: l3); by constructor.
      + exists (core x :: l3); constructor; by rewrite ?cmra_core_r.
  Qed.