From 3ee72d39cc372f699c8029c27d722b3f238ab4e0 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Thu, 17 Oct 2019 08:57:51 -0400
Subject: [PATCH] Removed experimental folder

---
 experimental/encodable.v         |  91 ------------
 experimental/flist.v             | 229 -------------------------------
 experimental/producer_consumer.v | 131 ------------------
 experimental/spin_lock.v         | 144 -------------------
 4 files changed, 595 deletions(-)
 delete mode 100644 experimental/encodable.v
 delete mode 100644 experimental/flist.v
 delete mode 100644 experimental/producer_consumer.v
 delete mode 100644 experimental/spin_lock.v

diff --git a/experimental/encodable.v b/experimental/encodable.v
deleted file mode 100644
index d6b660e..0000000
--- a/experimental/encodable.v
+++ /dev/null
@@ -1,91 +0,0 @@
-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
deleted file mode 100644
index 48c301e..0000000
--- a/experimental/flist.v
+++ /dev/null
@@ -1,229 +0,0 @@
-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
deleted file mode 100644
index c011e32..0000000
--- a/experimental/producer_consumer.v
+++ /dev/null
@@ -1,131 +0,0 @@
-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
deleted file mode 100644
index 6925075..0000000
--- a/experimental/spin_lock.v
+++ /dev/null
@@ -1,144 +0,0 @@
-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