phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/lib/increment.v *)
(* A proof of the incr specification that unfolds the definition of atomic
      accessors.  This is the style that most logically atomic proofs take. *)
Lemma incr_spec_direct (l: loc) :
    heap_inv -∗
    <<{ ∀∀ (v : Z), l ↦ #v }>>
      incr #l @ ↑atomic_heapN
    <<{ l ↦ #(v + 1) | RET #v }>>.
Proof.
    iIntros "#Hheap %Φ AU". iLöb as "IH". wp_lam.
    awp_apply (load_spec with "Hheap").
    (* Prove the atomic update for load *)
    (* To [iMod] a *mask-changing* update (like "AU"), we have to unfold
       [atomic_acc] in the goal.
       Note that non-mask-changing [iMod] and [iInv] would work here without
       unfolding, i.e., an [AACC] in the goal supports eliminating
       non-mask-changing updates and accessors but it does not support
       eliminating mask-changing updates. *)
    rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
    (* Usually, we would use [iAaccIntro], but here we cannot because we
       unfolded [atomic_acc], so we do it by hand. *)
    iModIntro. iExists _, _. iFrame "Hl". iSplit.
    { (* abort case *) done. }
    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
    (* Now go on *)
    wp_pures. awp_apply (cas_spec with "Hheap"); first done.
    (* Prove the atomic update for CAS. We want to prove the precondition of
       that update (the ↦) as quickly as possible because every step we take
       along the way has to be "reversible" to prove the "abort" update. *)
    rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
    iModIntro. iExists _. iFrame "Hl". iSplit.
    { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
    (* Good, we proved the precondition, now we can proceed "as normal". *)
    iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
    - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
      iIntros "!>". wp_if. by iApply "HΦ".
    - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
      iIntros "!>". wp_if. iApply "IH". done.
  Qed.
(* iris_heap_lang/lib/increment.v *)
(* A proof of the incr specification that uses lemmas ([aacc_aupd_*]) to
      avoid reasoning with the definition of atomic accessors. These lemmas are
      only usable here because the atomic update we have and the one we try to
      prove are in 1:1 correspondence; most logically atomic proofs will not be
      able to use them. *)
Lemma incr_spec (l: loc) :
    heap_inv -∗
    <<{ ∀∀ (v : Z), l ↦ #v }>>
      incr #l @ ↑atomic_heapN
    <<{ l ↦ #(v + 1) | RET #v }>>.
Proof.
    iIntros "#Hheap %Φ AU". iLöb as "IH". wp_lam.
    awp_apply (load_spec with "Hheap").
    (* Prove the atomic update for load *)
    iApply (aacc_aupd_abort with "AU"); first done.
    iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
    iIntros "$ !> AU !>".
    (* Now go on *)
    wp_pures. awp_apply (cas_spec with "Hheap"); first done.
    (* Prove the atomic update for CAS *)
    iApply (aacc_aupd with "AU"); first done.
    iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
    iIntros "H↦ !>".
    simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
    - iRight. iFrame. iIntros "HΦ !>".
      wp_if. by iApply "HΦ".
    - iLeft. iFrame. iIntros "AU !>".
      wp_if. iApply "IH". done.
  Qed.
(* iris_heap_lang/lib/increment.v *)
(* A "weak increment": assumes that there is no race *)
Definition weak_incr: val
:=
    rec: "weak_incr" "l" :=
       let: "oldv" := !"l" in
       "l" <- ("oldv" + #1);;
       "oldv" (* return old value *).
(* iris_heap_lang/lib/increment.v *)
(* TODO: Generalize to q and 1-q, based on some theory for a "maybe-pointsto"
     connective that works on [option Qp] (the type of 1-q). *)
Lemma weak_incr_spec (l: loc) (v : Z) :
    heap_inv -∗
    l ↦{#1/2} #v -∗
    <<{ ∀∀ (v' : Z), l ↦{#1/2} #v' }>>
      weak_incr #l @ ↑atomic_heapN
    <<{ ⌜v = v'⌝ ∗ l ↦ #(v + 1)
      | RET #v }>>.
Proof.
    iIntros "#Hheap Hl" (Φ) "AU". wp_lam.
    iPoseProof (load_spec with "Hheap") as "load_spec".
    wp_apply (atomic_wp_seq with "load_spec Hl") as "Hl".
    wp_pures. awp_apply store_spec; first done.
    (* Prove the atomic update for store *)
    iApply (aacc_aupd_commit with "AU"); first done.
    iIntros (x) "H↦".
    iDestruct (pointsto_agree with "Hl H↦") as %[= <-].
    iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
    { iIntros "[$ $]"; eauto. }
    iIntros "$ !>". iSplit; first done.
    iIntros "HΦ !>". wp_seq. done.
  Qed.
(* iris_heap_lang/lib/increment.v *)
Definition incr_client : val
:=
    λ: "x",
       let: "l" := ref "x" in
       incr "l" ||| incr "l".
(* iris_heap_lang/lib/increment.v *)
Lemma incr_client_safe (x: Z):
    heap_inv -∗
    WP incr_client #x {{ _, True }}.
Proof using Type*.
    iIntros "#Hheap". wp_lam.
    wp_apply (alloc_spec with "Hheap [//]"). iIntros (l) "Hl". wp_pures.
    iMod (inv_alloc (nroot .@ "incr_client") _ (∃x':Z, l ↦ #x')%I
           with "[Hl]") as "#Hinv"; first eauto.
    (* FIXME: I am only using persistent stuff, so I should be allowed
       to move this to the persisten context even without the additional □. *)
    iAssert (□ WP incr #l {{ _, True }})%I as "#Aupd".
    { iIntros "!>". awp_apply incr_spec; first done. clear x.
      iInv "Hinv" as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
      iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
      (* The continuation: From after the atomic triple to the postcondition of the WP *)
      done.
    }
    wp_smart_apply wp_par.
    - iAssumption.
    - iAssumption.
    - iIntros (??) "_ !>". done.
  Qed.
(* iris_heap_lang/lib/lazy_coin.v *)
Definition new_coin: val
:= λ: <>, (ref NONE, NewProph).
(* iris_heap_lang/lib/lazy_coin.v *)
Definition read_coin : val
:=
  λ: "cp",
  let: "c" := Fst "cp" in
  let: "p" := Snd "cp" in
  match: !"c" with
    NONE => let: "r" := nondet_bool #() in
           "c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
  | SOME "b" => "b"
  end.
(* iris_heap_lang/lib/lazy_coin.v *)
Definition val_to_bool (v : val) : bool
:= bool_decide (v = #true).
(* iris_heap_lang/lib/lazy_coin.v *)
Definition prophecy_to_bool (vs : list (val * val)) : bool
:=
    default false (val_to_bool ∘ snd <$> head vs).
(* iris_heap_lang/lib/lazy_coin.v *)
Lemma prophecy_to_bool_of_bool (b : bool) v vs :
    prophecy_to_bool ((v, #b) :: vs) = b.
Proof. by destruct b. Qed.
(* iris_heap_lang/lib/lazy_coin.v *)
Definition coin (cp : val) (b : bool) : iProp Σ
:=
    ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
       ⌜cp = (#c, #p)%V⌝ ∗ proph p vs ∗
       (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vs⌝)).
(* iris_heap_lang/lib/lazy_coin.v *)
Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}.
Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam.
    wp_apply wp_new_proph; first done.
    iIntros (vs p) "Hp".
    wp_alloc c as "Hc".
    wp_pair.
    iApply ("HΦ" $! (#c, #p)%V ).
    rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/lazy_coin.v *)
Lemma read_coin_spec cp b :
    {{{ coin cp b }}} read_coin cp {{{ RET #b; coin cp b }}}.
Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]".
    - wp_lam. wp_load. wp_match.
      iApply "HΦ".
      rewrite /coin; eauto 10 with iFrame.
    - wp_lam. wp_load. wp_match.
      wp_apply nondet_bool_spec; first done.
      iIntros (r) "_".
      wp_let.
      wp_store.
      wp_apply (wp_resolve_proph with "[Hp]"); first done.
      iIntros (ws) "[-> Hws]".
      rewrite !prophecy_to_bool_of_bool.
      wp_seq.
      iApply "HΦ".
      rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/lock.v *)
(* A general interface for a lock.

All parameters are implicit, since it is expected that there is only one
[heapGS_gen] in scope that could possibly apply.

Only one instance of this class should ever be in scope. To write a library that
is generic over the lock, just add a [`{!lock}] implicit parameter around the
code and [`{!lockG Σ}] around the proofs. To use a particular lock instance, use
[Local Existing Instance <lock instance>].

When writing an instance of this class, please take care not to shadow the class
projections (e.g., either use [Local Definition newlock] or avoid the name
[newlock] altogether), and do not register an instance -- just make it a
[Definition] that others can register later. *)
Class lock
:= Lock {
  (** * Operations *)
  newlock : val;
  acquire : val;
  release : val;
  (** * Ghost state *)
  (** The assumptions about [Σ] *)
  lockG : gFunctors → Type;
  (** [name] is used to associate [locked] with [is_lock] *)
  lock_name : Type;
  #[global] lock_name_inhabited :: Inhabited lock_name;
  (** * Predicates *)
  (** No namespace [N] parameter because we only expose program specs, which
  anyway have the full mask. *)
  is_lock `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
  locked `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) : iProp Σ;
  (** * General properties of the predicates *)
  #[global] is_lock_persistent `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R ::
    Persistent (is_lock (L:=L) γ lk R);
  is_lock_iff `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R1 R2 :
    is_lock (L:=L) γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock (L:=L) γ lk R2;
  #[global] locked_timeless `{!heapGS_gen hlc Σ} {L : lockG Σ} γ ::
    Timeless (locked (L:=L) γ);
  locked_exclusive `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :
    locked (L:=L) γ -∗ locked (L:=L) γ -∗ False;
  (** * Program specs *)
  newlock_spec_delay_init `{!heapGS_gen hlc Σ} {L : lockG Σ} :
    {{{ True }}}
      newlock #()
    {{{ lk γ, RET lk; ∀ R E, R ={E}=∗ is_lock (L:=L) γ lk R  }}};
  acquire_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :
    {{{ is_lock (L:=L) γ lk R }}} acquire lk {{{ RET #(); locked (L:=L) γ ∗ R }}};
  release_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :
    {{{ is_lock (L:=L) γ lk R ∗ locked (L:=L) γ ∗ R }}} release lk {{{ RET #(); True }}}
}.
(* iris_heap_lang/lib/lock.v *)
Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
  Contractive (is_lock γ lk).
Proof.
  apply (contractive_internal_eq (PROP:=iPropI Σ)).
  iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>".
  iSplit; iIntros "H"; iApply (is_lock_iff with "H");
    iNext; iRewrite "HPQ"; auto.
Qed.
(* iris_heap_lang/lib/lock.v *)
Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
  Proper ((≡) ==> (≡)) (is_lock γ lk)
:= ne_proper _.
(* iris_heap_lang/lib/lock.v *)
Lemma newlock_spec (R : iProp Σ) :
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
    iIntros (Φ) "HR HΦ".
    iApply wp_fupd.
    wp_apply newlock_spec_delay_init; first done.
    iIntros (lk γ) "Hlk". iApply "HΦ".
    by iMod ("Hlk" $! R ⊤ with "HR").
  Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Inductive state
:= Free | Locked.
(* iris_heap_lang/lib/logatom_lock.v *)
Class alockG Σ
:= LockG { #[local] lock_tokG :: ghost_varG Σ state }.
(* iris_heap_lang/lib/logatom_lock.v *)
Definition alockΣ : gFunctors
:= #[ghost_varΣ state].
(* iris_heap_lang/lib/logatom_lock.v *)
Instance subG_alockΣ {Σ} : subG alockΣ Σ → alockG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Record tada_lock_name
:= TadaLockName {
    tada_lock_name_state : gname;
    tada_lock_name_lock : lock_name;
  }.
(* iris_heap_lang/lib/logatom_lock.v *)
Definition tada_lock_state (γ : tada_lock_name) (s : state) : iProp Σ
:=
    γ.(tada_lock_name_state) ↪VAR{#3/4} s ∗
    if s is Locked then
      locked γ.(tada_lock_name_lock) ∗ γ.(tada_lock_name_state) ↪VAR{#1/4} Locked
    else True.
(* iris_heap_lang/lib/logatom_lock.v *)
Definition tada_is_lock (γ : tada_lock_name) (lk : val) : iProp Σ
:=
    is_lock γ.(tada_lock_name_lock) lk
      (γ.(tada_lock_name_state) ↪VAR{#1/4} Free).
(* iris_heap_lang/lib/logatom_lock.v *)
Instance tada_is_lock_persistent γ lk : Persistent (tada_is_lock γ lk).
Proof. apply _. Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Instance tada_lock_state_timeless γ s : Timeless (tada_lock_state γ s).
Proof. destruct s; apply _. Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Lemma tada_lock_state_exclusive γ s1 s2 :
    tada_lock_state γ s1 -∗ tada_lock_state γ s2 -∗ False.
Proof.
    iIntros "[Hvar1 _] [Hvar2 _]".
    iCombine "Hvar1 Hvar2" gives %[Hval _].
    exfalso. done.
  Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Lemma newlock_tada_spec :
    {{{ True }}}
      newlock #()
    {{{ lk γ, RET lk; tada_is_lock γ lk ∗ tada_lock_state γ Free }}}.
Proof.
    iIntros (Φ) "_ HΦ".
    iMod (ghost_var_alloc Free) as (γvar) "Hvar".
    replace 1%Qp with (3/4 + 1/4)%Qp; last first.
    { rewrite Qp.three_quarter_quarter //. }
    iDestruct "Hvar" as "[Hvar1 Hvar2]".
    wp_apply (newlock_spec with "Hvar2") as (lk γlock) "Hlock".
    iApply ("HΦ" $! lk (TadaLockName _ _)).
    iFrame.
  Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Lemma acquire_tada_spec γ lk :
    tada_is_lock γ lk -∗
    <<{ ∀∀ s, tada_lock_state γ s }>>
      acquire lk @ ∅
    <<{ ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked | RET #() }>>.
Proof.
    iIntros "#Hislock %Φ AU". iApply wp_fupd.
    wp_apply (acquire_spec with "Hislock") as "[Hlocked Hvar1]".
    iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
    iCombine "Hvar1 Hvar2" gives %[_ <-].
    iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
    { rewrite Qp.quarter_three_quarter //. }
    iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"); done.
  Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
Lemma release_tada_spec γ lk :
    tada_is_lock γ lk -∗
    <<{ tada_lock_state γ Locked }>>
      release lk @ ∅
    <<{ tada_lock_state γ Free | RET #() }>>.
Proof.
    iIntros "#Hislock %Φ AU". iApply fupd_wp.
    iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
    iMod (ghost_var_update_2 Free with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
    { rewrite Qp.three_quarter_quarter //. }
    iMod ("Hclose" with "[$Hvar1]"). iModIntro.
    wp_apply (release_spec with "[$Hislock $Hlocked $Hvar2]").
    auto.
  Qed.
(* iris_heap_lang/lib/nondet_bool.v *)
Definition nondet_bool : val
:=
  λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
(* iris_heap_lang/lib/nondet_bool.v *)
Lemma nondet_bool_spec : {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}.
Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam. wp_alloc l as "Hl". wp_let.
    pose proof (nroot .@ "rnd") as rndN.
    iMod (inv_alloc rndN _ (∃ (b : bool), l ↦ #b)%I with "[Hl]") as "#Hinv";
      first by eauto.
    wp_apply wp_fork.
    - iInv rndN as (?) "?". wp_store; eauto.
    - wp_seq. iInv rndN as (?) "?". wp_load.
      iSplitR "HΦ"; first by eauto.
      by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/par.v *)
Definition parN : namespace
:= nroot .@ "par".
(* iris_heap_lang/lib/par.v *)
Definition par : val
:=
  λ: "e1" "e2",
    let: "handle" := spawn "e1" in
    let: "v2" := "e2" #() in
    let: "v1" := join "handle" in
    ("v1", "v2").
(* iris_heap_lang/lib/par.v *)
Notation "e1 ||| e2"
:= (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
(* iris_heap_lang/lib/par.v *)
Notation "e1 ||| e2"
:= (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
(* iris_heap_lang/lib/par.v *)
(* Notice that this allows us to strip a later *after* the two Ψ have been
   brought together.  That is strictly stronger than first stripping a later
   and then merging them, as demonstrated by [tests/joining_existentials.v].
   This is why these are not Texan triples. *)
Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ) :
  WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
  (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
  WP par f1 f2 {{ Φ }}.
Proof.
  iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
  wp_apply (spawn_spec parN with "Hf1") as (l) "Hl".
  wp_let. wp_bind (f2 _).
  wp_apply (wp_wand with "Hf2") as (v) "H2". wp_let.
  wp_apply (join_spec with "[$Hl]") as (w) "H1".
  iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
Qed.
(* iris_heap_lang/lib/par.v *)
Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
  WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
  (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
  WP (e1 ||| e2)%V {{ Φ }}.
Proof.
  iIntros "H1 H2 H".
  wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
Qed.
(* iris_heap_lang/lib/rw_lock.v *)
Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk n :
  Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
Proof.
  assert (Contractive (is_rw_lock γ lk : (Qp -d> iPropO Σ) → _)) as Hcontr.
  { apply (contractive_internal_eq (PROP:=iPropI Σ)); iIntros (Φ1 Φ2) "#HΦ".
    rewrite discrete_fun_equivI.
    iApply prop_ext_2; iIntros "!>"; iSplit; iIntros "H";
      iApply (is_rw_lock_iff with "H");
      iIntros "!> !>" (q); iRewrite ("HΦ" $! q); auto. }
  intros Φ1 Φ2 HΦ. apply Hcontr. dist_later_intro. apply HΦ.
Qed.
(* iris_heap_lang/lib/rw_lock.v *)
Instance is_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk :
  Proper (pointwise_relation _ (≡) ==> (≡)) (is_rw_lock γ lk).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply is_rw_lock_contractive=> q.
  dist_later_intro. apply equiv_dist, HΦ.
Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition newlock : val
:= λ: <>, ref #0.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition try_acquire_reader : val
:=
  λ: "l",
    let: "n" := !"l" in
    if: #0 ≤ "n"
      then CAS "l" "n" ("n" + #1)
      else #false.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition acquire_reader : val
:=
  rec: "acquire" "l" :=
    if: try_acquire_reader "l"
      then #()
      else "acquire" "l".
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition release_reader : val
:=
  λ: "l", FAA "l" #(-1) ;; #().
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition try_acquire_writer : val
:=
  λ: "l", CAS "l" #0 #(-1).
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition acquire_writer : val
:=
  rec: "acquire" "l" :=
    if: try_acquire_writer "l"
      then #()
      else "acquire" "l".
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition release_writer : val
:=
  λ: "l", "l" <- #0.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Class rw_spin_lockG Σ
:=
  RwLockG { #[local] rwlock_tokG :: inG Σ (authR (gmultisetUR Qp)) }.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition rw_spin_lockΣ : gFunctors
:= #[GFunctor (authR (gmultisetUR Qp)) ].
(* iris_heap_lang/lib/rw_spin_lock.v *)
Instance subG_rw_spin_lockΣ {Σ} : subG rw_spin_lockΣ Σ → rw_spin_lockG Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Let N
:= nroot .@ "rw_lock".
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition rw_state_inv (γ : gname) (l : loc) (Φ : Qp → iProp Σ) : iProp Σ
:=
    ∃ z : Z, l ↦ #z ∗
      (* We need *some* ghost state that allows us to establish a contradiction
      in the left disjunct (where the lock is write-locked) when proving
      [release_reader_spec], so we use a fraction of the empty authoritative
      reader set (the rest goes to [writer_locked].) Any fraction would do, but
      the benefit of giving over half to [writer_locked] (and keeping less than
      half here) is that we can prove [writer_locked_exclusive]. *)
      (⌜(z = -1)%Z⌝ ∗ own γ (●{# 1/4} ∅)
      ∨ ⌜(0 ≤ z)%Z⌝ ∗ ∃ (q : Qp) (g : gmultiset Qp),
          own γ (● g) ∗
          ⌜size g = Z.to_nat z⌝ ∗
          ⌜set_fold Qp.add q g = 1%Qp⌝ ∗
          Φ q
      ).
(* iris_heap_lang/lib/rw_spin_lock.v *)
(* This definition is [tc_opaque] because the ▷ around [internal_fractional]
  should be preserved even when taking steps (otherwise it's more annoying to
  re-establish.) *)
Definition is_rw_lock (γ : gname) (lk : val) (Φ : Qp → iProp Σ) : iProp Σ
:=
    tc_opaque (▷ internal_fractional Φ ∗
      ∃ l : loc, ⌜lk = #l⌝ ∗ inv N (rw_state_inv γ l Φ))%I.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Instance is_rw_lock_persistent γ lk Φ : Persistent (is_rw_lock γ lk Φ).
Proof. unfold is_rw_lock, tc_opaque. apply _. Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition reader_locked (γ : gname) (q : Qp) : iProp Σ
:= own γ (◯ {[+ q +]}).
(* iris_heap_lang/lib/rw_spin_lock.v *)
Definition writer_locked (γ : gname) : iProp Σ
:= own γ (● {# 3/4} ∅).
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma writer_locked_exclusive γ :
    writer_locked γ -∗ writer_locked γ -∗ False.
Proof.
    iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
    rewrite
      auth_auth_dfrac_op_valid
      dfrac_op_own
      dfrac_valid_own in Hvalid.
    by destruct Hvalid as [? _].
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma writer_locked_not_reader_locked γ q :
    writer_locked γ -∗ reader_locked γ q -∗ False.
Proof.
    iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
    apply auth_both_dfrac_valid in Hvalid as (_ & Hvalid & _).
    generalize (Hvalid 0)=> /cmra_discrete_included_r /gmultiset_included /(_ q).
    rewrite multiplicity_empty multiplicity_singleton_eq. by lia.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma is_rw_lock_iff γ lk Φ Ψ :
    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ.
Proof.
    iIntros "[#HΦdup [%l [-> #Hlockinv]]] #Hiff".
    iSplitR.
    { iApply (internal_fractional_iff with "Hiff HΦdup"). }
    iExists l; iSplitR; first done.
    iApply (inv_iff with "[Hlockinv Hiff //]"); iIntros "!> !>".
    iDestruct "Hiff" as "#Hiff".
    iClear "HΦdup Hlockinv".
    iSplit.
    - iIntros "(%z & ? & Hstate)". iExists z. iFrame.
      iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
      + iFrame.
      + iRight.
        iFrame.
        by iApply "Hiff".
    - iIntros "(%z & ? & Hstate)". iExists z. iFrame.
      iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
      + iFrame.
      + iRight.
        iFrame.
        by iApply "Hiff".
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
(* Some helper lemmas for "auth of a multiset" *)
Lemma auth_valid_gmultiset_singleton `{Countable A} dq (v : A) (g : gmultiset A) :
    ✓ (● { dq } g ⋅ ◯ ({[+ v +]})) → v ∈ g.
Proof.
    rewrite
      auth_both_dfrac_valid_discrete
      gmultiset_included
      gmultiset_singleton_subseteq_l.
    intros (_ & ? & _); assumption.
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma own_auth_gmultiset_singleton_2 γ dq v g :
    own γ (● { dq } g) ∗ own γ (◯ ({[+ v +]})) ⊢ ⌜v ∈ g⌝.
Proof.
    iIntros "[Hauth Hfrag]".
    iCombine "Hauth Hfrag" gives %Hvalid.
    iPureIntro.
    apply (auth_valid_gmultiset_singleton _ _ _ Hvalid).
  Qed.
(* iris_heap_lang/lib/rw_spin_lock.v *)
Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
    {{{ P }}}
      newlock #()
    {{{ lk γ, RET lk; is_rw_lock γ lk Φ }}}.
Proof.
    iIntros (φ) "HΦ Hφ".
    wp_lam.
    iMod (own_alloc (● ∅)) as (γ) "Hγ".
    { apply auth_auth_valid; done. }
    wp_alloc l as "Hl".
    iMod (inv_alloc N _ (rw_state_inv γ l Φ) with "[-Hφ]") as "#?".
    { rewrite [P]as_fractional.
      eauto 10 with iFrame. }
    iApply "Hφ".
    iSplitR.
    { iApply fractional_internal_fractional.
      apply (as_fractional_fractional (P:=P)). }
    eauto 10.
  Qed.