From 7f2f81e18d1ccd082dfe0400503729529ef07276 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Jul 2019 21:31:58 +0200
Subject: [PATCH] Revert "Removed Experimental" now that we prepared the
 artifact.

This reverts commit f9234e4fb10b6cefc9e59a635f2d504f3f7b7095.
---
 experimental/encodable.v         |  91 ++++++++++++
 experimental/flist.v             | 229 +++++++++++++++++++++++++++++++
 experimental/producer_consumer.v | 131 ++++++++++++++++++
 experimental/spin_lock.v         | 144 +++++++++++++++++++
 4 files changed, 595 insertions(+)
 create mode 100644 experimental/encodable.v
 create mode 100644 experimental/flist.v
 create mode 100644 experimental/producer_consumer.v
 create mode 100644 experimental/spin_lock.v

diff --git a/experimental/encodable.v b/experimental/encodable.v
new file mode 100644
index 0000000..d6b660e
--- /dev/null
+++ b/experimental/encodable.v
@@ -0,0 +1,91 @@
+From iris.heap_lang Require Export notation.
+
+Class ValEnc A := val_encode : A → val.
+Class ValDec A := val_decode : val → option A.
+Class ValEncDec A `{!ValEnc A, !ValDec A} := {
+  val_encode_decode v : val_decode (val_encode v) = Some v;
+  val_decode_encode v x : val_decode v = Some x → val_encode x = v;
+}.
+
+Local Arguments val_encode _ _ !_ /.
+Local Arguments val_decode _ _ !_ /.
+
+Lemma val_encode_decode_iff `{ValEncDec A} v x :
+  val_encode x = v ↔ val_decode v = Some x.
+Proof.
+  split; last apply val_decode_encode. intros <-. by rewrite -val_encode_decode.
+Qed.
+Instance val_encode_inj `{ValEncDec A} : Inj (=) (=) val_encode.
+Proof.
+  intros x y Heq. apply (inj Some).
+  by rewrite -(val_encode_decode x) Heq val_encode_decode.
+Qed.
+
+(* Instances *)
+Instance val_val_enc : ValEnc val := id.
+Instance val_val_dec : ValDec val := id $ Some.
+Instance val_val_enc_dec : ValEncDec val.
+Proof. split. done. by intros ?? [= ->]. Qed.
+
+Instance int_val_enc : ValEnc Z := λ n, #n.
+Instance int_val_dec : ValDec Z := λ v,
+  match v with LitV (LitInt z) => Some z | _ => None end.
+Instance int_val_enc_dec : ValEncDec Z.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
+
+Instance bool_val_enc : ValEnc bool := λ b, #b.
+Instance bool_val_dec : ValDec bool := λ v,
+  match v with LitV (LitBool b) => Some b | _ => None end.
+Instance bool_val_enc_dec : ValEncDec bool.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
+
+Instance loc_val_enc : ValEnc loc := λ l, #l.
+Instance loc_val_dec : ValDec loc := λ v,
+  match v with LitV (LitLoc l) => Some l | _ => None end.
+Instance loc_val_enc_dec : ValEncDec loc.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
+
+Instance unit_val_enc : ValEnc unit := λ _, #().
+Instance unit_val_dec : ValDec unit := λ v,
+  match v with LitV LitUnit => Some () | _ => None end.
+Instance unit_val_enc_dec : ValEncDec unit.
+Proof. split. by intros []. by intros [[]| | | |] ? [= <-]. Qed.
+
+Instance pair_val_enc `{ValEnc A, ValEnc B} : ValEnc (A * B) := λ p,
+  (val_encode p.1, val_encode p.2)%V.
+Arguments pair_val_enc {_ _ _ _} !_ /.
+Instance pair_val_dec `{ValDec A, ValDec B} : ValDec (A * B) := λ v,
+  match v with
+  | PairV v1 v2 => x1 ← val_decode v1; x2 ← val_decode v2; Some (x1, x2)
+  | _ => None
+  end.
+Arguments pair_val_dec {_ _ _ _} !_ /.
+Instance pair_val_enc_dec `{ValEncDec A, ValEncDec B} : ValEncDec (A * B).
+Proof.
+  split.
+  - intros []. by rewrite /= val_encode_decode /= val_encode_decode.
+  - intros [] ??; simplify_option_eq;
+      by repeat match goal with
+      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
+      end.
+Qed.
+
+Instance option_val_enc `{ValEnc A} : ValEnc (option A) := λ mx,
+  match mx with Some x => SOMEV (val_encode x) | None => NONEV end%V.
+Arguments option_val_enc {_ _} !_ /.
+Instance option_val_dec `{ValDec A} : ValDec (option A) := λ v,
+  match v with
+  | SOMEV v => x ← val_decode v; Some (Some x)
+  | NONEV => Some None
+  | _ => None
+  end.
+Arguments option_val_dec {_ _} !_ /.
+Instance option_val_enc_dec `{ValEncDec A} : ValEncDec (option A).
+Proof.
+  split.
+  - intros []=> //. by rewrite /= val_encode_decode.
+  - intros [] ??; repeat (simplify_option_eq || case_match);
+      by repeat match goal with
+      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
+      end.
+Qed.
diff --git a/experimental/flist.v b/experimental/flist.v
new file mode 100644
index 0000000..48c301e
--- /dev/null
+++ b/experimental/flist.v
@@ -0,0 +1,229 @@
+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import assert.
+
+(** Immutable ML-style functional lists *)
+Fixpoint flist (vs : list val) : val :=
+  match vs with
+  | [] => NONEV
+  | v :: vs => SOMEV (v,flist vs)
+  end%V.
+Arguments flist : simpl never.
+
+Definition fnil : val := λ: <>, NONEV.
+Definition fcons : val := λ: "x" "l", SOME ("x", "l").
+
+Definition fisnil : val := λ: "l",
+  match: "l" with
+    SOME "p" => #false
+  | NONE => #true
+  end.
+
+Definition fhead : val := λ: "l",
+  match: "l" with
+    SOME "p" => Fst "p"
+  | NONE => assert: #false
+  end.
+
+Definition ftail : val := λ: "l",
+  match: "l" with
+    SOME "p" => Snd "p"
+  | NONE => assert: #false
+  end.
+
+Definition flookup : val :=
+  rec: "go" "n" "l" :=
+    if: "n" = #0 then fhead "l" else
+    let: "l" := ftail "l" in "go" ("n" - #1) "l".
+
+Definition finsert : val :=
+  rec: "go" "n" "x" "l" :=
+    if: "n" = #0 then let: "l" := ftail "l" in fcons "x" "l" else
+    let: "k" := ftail "l" in
+    let: "k" := "go" ("n" - #1) "x" "k" in
+    fcons (fhead "l") "k".
+
+Definition freplicate : val :=
+  rec: "go" "n" "x" :=
+    if: "n" = #0 then fnil #() else
+    let: "l" := "go" ("n" - #1) "x" in fcons "x" "l".
+
+Definition flength : val :=
+  rec: "go" "l" :=
+    match: "l" with
+      NONE => #0
+    | SOME "p" => #1 + "go" (Snd "p")
+    end.
+
+Definition fapp : val :=
+  rec: "go" "l" "k" :=
+    match: "l" with
+      NONE => "k"
+    | SOME "p" => fcons (Fst "p") ("go" (Snd "p") "k")
+    end.
+
+Definition fsnoc : val := λ: "l" "x", fapp "l" (fcons "x" (fnil #())).
+
+Definition ftake : val :=
+  rec: "go" "l" "n" :=
+    if: "n" ≤ #0 then NONEV else
+    match: "l" with
+      NONE => NONEV
+    | SOME "l" => fcons (Fst "l") ("go" (Snd "l") ("n"-#1))
+    end.
+
+Definition fdrop : val :=
+  rec: "go" "l" "n" :=
+    if: "n" ≤ #0 then "l" else
+    match: "l" with
+      NONE => NONEV
+    | SOME "l" => "go" (Snd "l") ("n"-#1)
+    end.
+
+Definition fsplit_at : val := λ: "l" "n", (ftake "l" "n", fdrop "l" "n").
+
+Definition fsplit : val := λ: "l", fsplit_at "l" (flength "l" `quot` #2).
+
+Section lists.
+Context `{heapG Σ}.
+Implicit Types i : nat.
+Implicit Types v : val.
+Implicit Types vs : list val.
+
+Lemma fnil_spec :
+  {{{ True }}} fnil #() {{{ RET flist []; True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
+
+Lemma fcons_spec v vs :
+  {{{ True }}} fcons v (flist vs) {{{ RET flist (v :: vs); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma fisnil_spec vs:
+  {{{ True }}}
+    fisnil (flist vs)
+  {{{ RET #(if vs is [] then true else false); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. destruct vs; wp_pures; by iApply "HΦ". Qed.
+
+Lemma fhead_spec v vs :
+  {{{ True }}} fhead (flist (v :: vs)) {{{ RET v; True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma ftail_spec v vs :
+  {{{ True }}} ftail (flist (v :: vs)) {{{ RET flist vs; True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma flookup_spec i vs v :
+  vs !! i = Some v →
+  {{{ True }}} flookup #i (flist vs) {{{ RET v; True }}}.
+Proof.
+  iIntros (Hi Φ _) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (i Hi);
+    destruct i as [|i]=> //; simplify_eq/=.
+  { wp_lam. wp_pures. by iApply (fhead_spec with "[//]"). }
+  wp_lam. wp_pures.
+  wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
+  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
+Qed.
+
+Lemma finsert_spec i vs v :
+  is_Some (vs !! i) →
+  {{{ True }}} finsert #i v (flist vs) {{{ RET flist (<[i:=v]>vs); True }}}.
+Proof.
+  iIntros ([w Hi] Φ _) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (i Hi Φ);
+    destruct i as [|i]=> //; simplify_eq/=.
+  { wp_lam. wp_pures. wp_apply (ftail_spec with "[//]"); iIntros (_).
+    wp_let. by iApply (fcons_spec with "[//]"). }
+  wp_lam; wp_pures.
+  wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
+  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
+  wp_apply ("IH" with "[//]"); iIntros (_).
+  wp_apply (fhead_spec with "[//]"); iIntros "_".
+  by wp_apply (fcons_spec with "[//]").
+Qed.
+
+Lemma freplicate_spec i v :
+  {{{ True }}} freplicate #i v {{{ RET flist (replicate i v); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
+  { wp_lam; wp_pures. iApply (fnil_spec with "[//]"); auto. }
+  wp_lam; wp_pures.
+  rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
+  wp_apply "IH"; iIntros (_). wp_let. by iApply (fcons_spec with "[//]").
+Qed.
+
+Lemma flength_spec vs :
+  {{{ True }}} flength (flist vs) {{{ RET #(length vs); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (Φ); simplify_eq/=.
+  { wp_lam. wp_match. by iApply "HΦ". }
+  wp_lam. wp_match. wp_proj.
+  wp_apply "IH"; iIntros "_ /=". wp_op.
+  rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
+Qed.
+
+Lemma fapp_spec vs1 vs2 :
+  {{{ True }}} fapp (flist vs1) (flist vs2) {{{ RET (flist (vs1 ++ vs2)); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ".
+  iInduction vs1 as [|v1 vs1] "IH" forall (Φ); simpl.
+  { wp_rec. wp_pures. by iApply "HΦ". }
+  wp_rec. wp_pures. wp_apply "IH". iIntros (_). by wp_apply fcons_spec.
+Qed.
+
+Lemma fsnoc_spec vs v :
+  {{{ True }}} fsnoc (flist vs) v {{{ RET (flist (vs ++ [v])); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ". wp_lam. wp_apply (fnil_spec with "[//]"); iIntros (_).
+  wp_apply (fcons_spec with "[//]"); iIntros (_).
+  wp_apply (fapp_spec with "[//]"); iIntros (_). by iApply "HΦ".
+Qed.
+
+Lemma ftake_spec vs (n : nat) :
+  {{{ True }}} ftake (flist vs) #n {{{ RET flist (take n vs); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ".
+  iInduction vs as [|x' vs] "IH" forall (n Φ).
+  - wp_rec. wp_pures.
+    destruct (bool_decide (n ≤ 0)); wp_pures; rewrite take_nil; by iApply "HΦ".
+  - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
+    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
+    wp_apply "IH"; iIntros (_).
+    wp_apply (fcons_spec with "[//]"); iIntros (_). by iApply "HΦ".
+Qed.
+
+Lemma fdrop_spec vs (n : nat) :
+  {{{ True }}} fdrop (flist vs) #n {{{ RET flist (drop n vs); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ".
+  iInduction vs as [|x' vs] "IH" forall (n Φ).
+  - wp_rec. wp_pures.
+    destruct (bool_decide (n ≤ 0)); wp_pures; rewrite drop_nil; by iApply "HΦ".
+  - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
+    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
+    wp_apply "IH"; iIntros (_). by iApply "HΦ".
+Qed.
+
+Lemma fsplit_at_spec vs (n : nat) :
+  {{{ True }}}
+    fsplit_at (flist vs) #n
+  {{{ RET (flist (take n vs), flist (drop n vs)); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ". wp_lam.
+  wp_apply (fdrop_spec with "[//]"); iIntros (_).
+  wp_apply (ftake_spec with "[//]"); iIntros (_).
+  wp_pures. by iApply "HΦ".
+Qed.
+
+Lemma fsplit_spec vs :
+  {{{ True }}}
+    fsplit (flist vs)
+  {{{ ws1 ws2, RET (flist ws1, flist ws2); ⌜ vs = ws1 ++ ws2 ⌝ }}}.
+Proof.
+  iIntros (Φ _) "HΦ". wp_lam.
+  wp_apply (flength_spec with "[//]"); iIntros (_). wp_pures.
+  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
+  wp_apply (fsplit_at_spec with "[//]"); iIntros (_).
+  iApply "HΦ". by rewrite take_drop.
+Qed.
+End lists.
diff --git a/experimental/producer_consumer.v b/experimental/producer_consumer.v
new file mode 100644
index 0000000..c011e32
--- /dev/null
+++ b/experimental/producer_consumer.v
@@ -0,0 +1,131 @@
+From stdpp Require Import sorting.
+From actris.channel Require Import proto_channel proofmode.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import assert.
+From actris.utils Require Import list compare spin_lock.
+
+Definition qenqueue : val := λ: "q" "v", #().
+Definition qdequeue : val := λ: "q", #().
+
+Definition enq := true.
+Definition deq := false.
+
+Definition cont := true.
+Definition stop := false.
+
+Definition some := true.
+Definition none := false.
+
+Definition pd_loop : val :=
+  rec: "go" "q" "pc" "cc" "c" :=
+    if: "cc" ≤ #0 then #() else 
+    if: recv "c" then (* enq/deq *)
+      if: recv "c" then (* cont/stop *)
+        let: "x" := recv "x" in
+        "go" (qenqueue "q" "x") "pc" "cc" "c"
+      else "go" "q" ("pc"-#1) "cc" "c"
+    else
+      if: lisnil "q" then
+        if: "pc" ≤ #0 then
+          send "c" #stop;;
+          "go" "q" "pc" ("cc"-#1) "c"
+        else
+          send "c" #cont;; send "c" #none;;
+          "go" "q" "pc" "cc" "c"
+      else
+        send "c" #cont;; send "c" #some;;
+        let: "qv" := qdequeue "q" in
+        send "c" (Snd "qv");;
+        "go" (Fst "qv") "pc" "cc" "c".
+
+Definition new_pd : val := λ: "pc" "cc",
+  let: "q" := lnil #() in
+  let: "c" := start_chan (λ: "c", pd_loop "q" "pc" "cc" "c") in
+  let: "l" := new_lock #() in
+  ("c", "l").
+
+Definition pd_send : val := λ: "cl" "x",
+  acquire (Snd "cl");;
+  send (Fst "cl") #enq;; send (Fst "cl") #cont;; send (Fst "cl") "x";;
+  release (Snd "cl").
+
+Definition pd_stop : val := λ: "cl",
+  acquire (Fst "cl");;
+  send (Snd "cl") #enq;; send (Snd "cl") #stop;;
+  release (Fst "cl").
+
+Definition pd_recv : val :=
+  rec: "go" "cl" :=
+    acquire (Fst "cl");;
+    send (Snd "cl") #deq;;
+    if: recv (Snd "cl") then    (* cont/stop *)
+       if: recv (Snd "cl") then (* some/none *)
+         let: "v" := recv (Snd "cl") in
+         release (Fst "cl");; SOME "v"
+       else release (Fst "cl");; "go" "c" "l"
+    else release (Fst "cl");; NONE.
+
+Section sort_elem.
+  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+
+  Definition queue_prot : iProto Σ := (END)%proto.
+
+  Lemma dist_queue_spec c :
+    {{{ c ↣ queue_prot @ N }}}
+      dist_queue (qnew #()) #0 #0 c
+    {{{ RET #(); c ↣ END @ N }}}.
+  Proof. Admitted.
+
+  (* Need predicate for end of production? *)
+  Definition produce_spec σ P (produce : val) :=
+    ∀ vs,
+    {{{ σ vs }}}
+      produce #()
+    {{{ v, RET v; (∃ w, ⌜v = SOMEV w⌝ ∧ P w ∗ σ (w::vs)) ∨ (⌜v = NONEV⌝) }}}.
+
+  Definition consume_spec σ P Q (consume : val) :=
+    ∀ vs, ∀ v : val,
+    {{{ σ vs ∗ P v }}}
+      consume v
+    {{{ RET #(); σ (v::vs) ∗ Q v }}}.
+
+  Lemma produce_consume_spec produce consume pσ cσ P Q pc cc :
+    pc > 0 → cc > 0 → 
+    produce_spec pσ P produce →
+    consume_spec cσ P Q consume →
+    {{{ pσ [] ∗ cσ [] }}}
+      produce_consume produce consume #pc #cc
+    {{{ vs, RET #(); pσ vs ∗ cσ vs ∗ [∗ list] v ∈ vs, Q v }}}.
+  Proof. Admitted.
+
+  (* Example producer *)
+  Definition ints_to_n (l : val) (n:nat) : val:=
+    λ: <>, let: "v" := !l in
+           if: "v" < #n
+           then l <- "v" + #1;; SOME "v"
+           else NONE.
+
+  Lemma ints_to_n_spec l n :
+    produce_spec (λ vs, (∃ loc, ⌜loc = LitV $ LitLoc l⌝ ∗ l ↦ #(length vs))%I)
+                 (λ v, ⌜∃ i, v = LitV $ LitInt i⌝%I) (ints_to_n #l n).
+  Proof.
+    iIntros (vs Φ) "Hσ HΦ".
+    iDestruct "Hσ" as (loc ->) "Hσ".
+    wp_lam. wp_load. wp_pures.
+    case_bool_decide.
+    - wp_store. wp_pures. iApply "HΦ".
+      (* Does this not exist? *)
+      assert (∀ n : nat, (n + 1) = (S n)). intros m. lia. rewrite H0.
+      by eauto 10 with iFrame.
+    - wp_pures. iApply "HΦ". by iRight.
+  Qed.
+
+  Definition consume_to_list l : val:=
+    λ: "v", 
+      let: "xs" := !l in
+      l <- lcons "v" "xs".
+
+  Lemma consume_to_list_spec l :
+    consume_spec (λ vs, (∃ loc, ⌜loc = LitV $ LitLoc l⌝ ∗ l ↦ val_encode vs)%I)
+                 (λ v, ⌜True⌝%I) (λ v, ⌜True⌝%I) (consume_to_list #l).
+  Proof. Admitted.
diff --git a/experimental/spin_lock.v b/experimental/spin_lock.v
new file mode 100644
index 0000000..6925075
--- /dev/null
+++ b/experimental/spin_lock.v
@@ -0,0 +1,144 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import excl auth frac csum.
+From iris.base_logic.lib Require Import cancelable_invariants.
+From iris.bi.lib Require Import fractional.
+Set Default Proof Using "Type".
+
+Definition new_lock : 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.
+
+Class lockG Σ := LockG {
+  lock_tokG :> inG Σ (authR (optionUR (exclR fracR)));
+  lock_cinvG :> cinvG Σ;
+}.
+Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracR))); cinvΣ].
+
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+  Definition lock_inv (γ γi : gname) (lk : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, lk ↦ #b ∗
+                 if b then (∃ p, own γ (● (Excl' p)) ∗ cinv_own γi (p/2))
+                 else own γ (● None) ∗ R)%I.
+
+  Definition is_lock (lk : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv N γi (lock_inv γ γi lk R))%I.
+
+  Definition unlocked (lk : loc) (q : Qp) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi q)%I.
+
+  Definition locked (lk : loc) (q : Qp) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi (q/2) ∗ own γ (◯ (Excl' q)))%I.
+
+  Global Instance unlocked_fractional lk : Fractional (unlocked lk).
+  Proof.
+    intros q1 q2. iSplit.
+    - iDestruct 1 as (γ γi) "[#Hm [Hq Hq']]". iSplitL "Hq"; iExists γ, γi; by iSplit.
+    - iIntros "[Hq1 Hq2]". iDestruct "Hq1" as (γ γi) "[#Hm Hq1]".
+      iDestruct "Hq2" as (γ' γi') "[#Hm' Hq2]".
+      iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
+      iExists γ, γi; iSplit; first done. by iSplitL "Hq1".
+  Qed.
+  Global Instance unlocked_as_fractional γ :
+    AsFractional (unlocked γ p) (unlocked γ) p.
+  Proof. split. done. apply _. Qed.
+
+  Global Instance lock_inv_ne γ γi lk : NonExpansive (lock_inv γ γi lk).
+  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 lk q : Timeless (locked lk q).
+  Proof. apply _. Qed.
+  Global Instance unlocked_timeless lk q : Timeless (unlocked lk q).
+  Proof. apply _. Qed.
+
+  Lemma lock_cancel E lk R : ↑ N ⊆ E → is_lock lk R -∗ unlocked lk 1 ={E}=∗ ▷ R.
+  Proof.
+    intros. iDestruct 1 as (γ γi) "#[Hm Hinv]". iDestruct 1 as (γ' γi') "[Hm' Hq]".
+    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
+    iMod (cinv_open_strong with "[$] [$]") as "(HR & Hq & Hclose)"; first done.
+    iDestruct "HR" as ([]) "[Hl HR]".
+    - iDestruct "HR" as (p) "[_ Hq']". iDestruct (cinv_own_1_l with "Hq Hq'") as ">[]".
+    - iDestruct "HR" as "[_ $]". iApply "Hclose"; auto.
+  Qed.
+
+  Lemma new_lock_spec :
+    {{{ True }}}
+      new_lock #()
+    {{{ lk, RET #lk; unlocked lk 1 ∗ (∀ R, R ={⊤}=∗ is_lock lk R) }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
+    wp_apply (wp_alloc with "[//]"); iIntros (l) "[Hl Hm]".
+    iDestruct (meta_token_difference _ (↑N) with "Hm") as "[Hm1 Hm2]"; first done.
+    iMod (own_alloc (● None)) as (γ) "Hγ"; first by apply auth_auth_valid.
+    iMod (cinv_alloc_strong (λ _, True))
+      as (γi _) "[Hγi H]"; first by apply pred_infinite_True.
+    iMod (meta_set _ _ (γ,γi) with "Hm1") as "#Hm1"; first done.
+    iApply "HΦ"; iSplitL "Hγi"; first by (iExists γ, γi; auto).
+    iIntros "!>" (R) "HR".
+    iMod ("H" $! (lock_inv γ γi l R) with "[HR Hl Hγ]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    iModIntro. iExists γ, γi; auto.
+  Qed.
+
+  Lemma try_acquire_spec lk R q :
+    {{{ is_lock lk R ∗ unlocked lk q }}}
+      try_acquire #lk
+    {{{ b, RET #b; if b is true then locked lk q ∗ R else unlocked lk q }}}.
+  Proof.
+    iIntros (Φ) "[#Hl Hq] HΦ". iDestruct "Hl" as (γ γi) "#[Hm Hinv]".
+    iDestruct "Hq" as (γ' γi') "[Hm' Hq]".
+    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
+    wp_rec. wp_bind (CmpXchg _ _ _).
+    iInv N as "[HR Hq]"; iDestruct "HR" as ([]) "[Hl HR]".
+    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl HR"; first (iExists true; iFrame).
+      wp_pures. iApply ("HΦ" $! false). iExists γ, γi; auto.
+    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]". iDestruct "Hq" as "[Hq Hq']".
+      iMod (own_update with "Hγ") as "[Hγ Hγ']".
+      { by apply auth_update_alloc, (alloc_option_local_update (Excl q)). }
+      iModIntro. iSplitL "Hl Hγ Hq"; first (iNext; iExists true; eauto with iFrame).
+      wp_pures. iApply ("HΦ" $! true with "[$HR Hγ' Hq']"). iExists γ, γi; by iFrame.
+  Qed.
+
+  Lemma acquire_spec lk R q :
+    {{{ is_lock lk R ∗ unlocked lk q }}} acquire #lk {{{ RET #(); locked lk q ∗ R }}}.
+  Proof.
+    iIntros (Φ) "[#Hlk Hq] HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "[$Hlk $Hq]"); iIntros ([]).
+    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "Hq". wp_if. iApply ("IH" with "[$]"); auto.
+  Qed.
+
+  Lemma release_spec lk R q :
+    {{{ is_lock lk R ∗ locked lk q ∗ R }}} release #lk {{{ RET #(); unlocked lk q }}}.
+  Proof.
+    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
+    iDestruct "Hlock" as (γ γi) "#[Hm Hinv]".
+    iDestruct "Hlocked" as (γ' γi') "(#Hm' & Hq & Hγ')".
+    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
+    wp_lam. iInv N as "[HR' Hq]"; iDestruct "HR'" as ([]) "[Hl HR']".
+    - iDestruct "HR'" as (p) ">[Hγ Hq']".
+      iDestruct (own_valid_2 with "Hγ Hγ'")
+        as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
+      iMod (own_update_2 with "Hγ Hγ'") as "Hγ".
+      { eapply auth_update_dealloc, delete_option_local_update; apply _. }
+      wp_store. iIntros "!>". iSplitL "Hl Hγ HR"; first (iExists false); iFrame.
+      iApply "HΦ". iExists γ, γi. iSplit; first done. by iSplitL "Hq".
+    - iDestruct "HR'" as "[>Hγ _]".
+      by iDestruct (own_valid_2 with "Hγ Hγ'")
+        as %[[[] ?%leibniz_equiv] _]%auth_both_valid.
+  Qed.
+End proof.
+
+Typeclasses Opaque is_lock locked.
-- 
GitLab