added new lang

parent 23e24474
Pipeline #5992 failed with stages
in 0 seconds
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
Qed.
This diff is collapsed.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ mcounterG Σ.
Proof. solve_inG. Qed.
Section mono_proof.
Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ ( (n : mnat)) l #n)%I.
Definition mcounter (l : loc) (n : nat) : iProp Σ :=
( γ, inv N (mcounter_inv γ l) own γ ( (n : mnat)))%I.
(** The main proofs. *)
Global Instance mcounter_persistent l n : Persistent (mcounter l n).
Proof. apply _. Qed.
Lemma newcounter_mono_spec :
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
Qed.
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]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10.
Qed.
Lemma read_mono_spec l j :
{{{ mcounter l j }}} read #l {{{ i, RET #i; j i%nat mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
Qed.
End mono_proof.
(** Counter with contributions *)
Class ccounterG Σ :=
CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
Definition ccounterΣ : gFunctors :=
#[GFunctor (frac_authR natR)].
Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ ccounterG Σ.
Proof. solve_inG. Qed.
Section contrib_spec.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ (! n) l #n)%I.
Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
inv N (ccounter_inv γ l).
Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
own γ (!{q} n).
(** 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 frag_auth_op -own_op. Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) :
{{{ True }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
Qed.
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]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
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)); omega. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ccounter γ q n }}} read #l
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
Qed.
Lemma read_contrib_spec_1 γ l n :
{{{ ccounter_ctx γ l ccounter γ 1 n }}} read #l
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
Qed.
End contrib_spec.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *)
newlock : val;
acquire : val;
release : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
name : Type;
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
locked_timeless γ : Timeless (locked γ);
locked_exclusive γ : locked γ - locked γ - False;
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
acquire_spec N γ lk R :
{{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ R }}};
release_spec N γ lk R :
{{{ is_lock N γ lk R locked γ R }}} release lk {{{ RET #(); True }}}
}.
Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _ _.
Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
Proper (() ==> ()) (is_lock L N γ lk) := ne_proper _.
From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !spawnG Σ}.
(* 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 Σ) e (f1 f2 : val) (Φ : val iProp Σ)
`{Hef : !IntoVal e (f1,f2)} :
WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}.
Proof.
apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ".
rewrite /par /=. wp_let. wp_proj.
wp_apply (spawn_spec parN with "Hf1").
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". by wp_let.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp Σ)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp Σ) :
WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP e1 ||| e2 {{ Φ }}.
Proof.
iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
by wp_let. by wp_let. auto.
Qed.
End proof.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Set Default Proof Using "Type".
Definition spawn : val :=
λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c".
Definition join : val :=
rec: "join" "c" :=
match: !"c" with
SOME "x" => "x"
| NONE => "join" "c"
end.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( lv, l lv (lv = NONEV
w, lv = SOMEV w (Ψ w own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γ, own γ (Excl ()) inv N (spawn_inv γ l Ψ))%I.
Global Instance spawn_inv_ne n γ l :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.
Global Instance join_handle_ne n l :
Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) `{Hef : !IntoVal e f} :
{{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
apply of_to_val in Hef as <-. iIntros (Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
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]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ".
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
Qed.
End proof.
Typeclasses Opaque join_handle.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
( l: loc, lk = #l inv N (lock_inv γ l R))%I.
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ):
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iModIntro. iApply "HΦ". iExists l. eauto.
Qed.
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. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
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Φ"; iFrame.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
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_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque is_lock locked.
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth gset.
From iris.heap_lang.lib Require Export lock.
Set Default Proof Using "Type".
Import uPred.
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".
Definition newlock : val :=
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
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".
Definition release : val :=
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
(** The CMRAs we need. *)
Class tlockG Σ :=
tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
Definition tlockΣ : gFunctors :=
#[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ tlockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
( o n : nat,
lo #o ln #n
own γ ( (Excl' o, GSet (seq_set 0 n)))
((own γ ( (Excl' o, GSet )) R) own γ ( (ε, GSet {[ o ]}))))%I.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
( lo ln : loc,
lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R))%I.
Definition issued (γ : gname) (x : nat) : iProp Σ :=
own γ ( (ε, GSet {[ x ]}))%I.
Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, GSet )))%I.
Global Instance lock_inv_ne γ lo ln :
NonExpansive (lock_inv γ lo ln).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
Proof. solve_proper. Qed.
Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof.
iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
iDestruct (own_valid_2 with "H1 H2") as %[[] _].
Qed.
Lemma newlock_spec (R : iProp Σ) :