temp

theories/chainable/implementation_gset.v

+From iris.heap_lang Require Export notation lang.
+From iris.proofmode Require Export proofmode.
+From iris.heap_lang Require Import proofmode.
+From iris.base_logic Require Import invariants lib.saved_prop.
+From iris.algebra Require Import auth excl gset.
+From iris.prelude Require Import options.
+
+From barriers.chainable Require Import specification.
+
+(* Iris implementation of barrier with receive splitting and chains. 
+   This implementation is based on [1].
+   
+   [1]: Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen,
+        and Lars Birkedal. 2016. Verifying Custom Synchronization Constructs
+        Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38,
+        2, Article 4 (January 2016), 72 pages. https://doi.org/10.1145/2818638 *)
+
+Definition new_barrier : val :=
+  λ: <>, SOME (ref (#false, NONEV)).
+
+Definition unwrap : val :=
+  λ: "x", 
+    match: "x" with
+      NONE => #() #()
+    | SOME "x" => "x"
+    end.
+
+Definition signal : val :=
+  λ: "b",
+    let: "b" := unwrap "b" in
+    let: "x" := ! "b" in
+    "b" <- (#true, Snd "x").
+
+Definition wait : val :=
+  rec: "wait" "b" :=
+    match: "b" with
+      NONE => #()
+    | SOME "hd" =>
+      let: "x" := ! "hd" in
+      if: Fst "x" then "wait" (Snd "x")
+      else "wait" "b"
+    end.
+
+Definition extend : val :=
+  λ: "b",
+    let: "b" := unwrap "b" in
+    let: "x" := ! "b" in
+    let: "flag" := Fst "x" in
+    let: "prev" := Snd "x" in
+    let: "b'" := ref (#false, "prev") in
+    "b" <- ("flag", SOME "b'");;
+    (SOME "b'", SOME "b").
+
+Record barrier : Set := {
+  location : loc;
+  γsp : gname;
+  γr : gname;
+  (* Can't be barrier as we can't have recursive records :/ *)
+  prev : option loc;
+}.
+
+Context `{!EqDecision barrier, !Countable barrier}.
+
+Class barrierG Σ := BarrierG {
+  barrier_inG :> inG Σ (authR (gset_disjUR barrier));
+  barrier_inG' :> inG Σ (exclR unitO);
+  barrier_savedPropG :> savedPropG Σ;
+}.
+
+Definition barrierΣ : gFunctors :=
+  #[ GFunctor (authR (gset_disjUR barrier)); GFunctor (exclR unitO); savedPropΣ ].
+
+Global Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+
+  Context `{!heapGS Σ, !barrierG Σ}.
+
+  Definition option_to_val (o : option val) : val :=
+    match o with
+    | Some v => SOMEV v
+    | None   => NONEV
+    end.
+
+  Definition option_loc_to_val (o : option loc) : val :=
+    option_to_val ((LitV ∘ LitLoc) <$> o).
+
+  Definition is_barrier (γ' : gname) (b : barrier) (bs : gset barrier) : iProp Σ :=
+    ∃ (flag : bool) (b' : option barrier) (P : iProp Σ),
+    (* ⌜b.(prev) = location <$> b'⌝ *)
+      b.(location) ↦{#1 / 2} (#flag, option_loc_to_val (location <$> b'))
+      ∗ saved_prop_own b.(γsp) DfracDiscarded P
+      ∗ (if flag then own (b.(γr)) (Excl ()) ∨ P else True)
+      ∗ match b' with
+        | None => True
+        | Some b' => ⌜b' ∈ bs ∖ {[b]}⌝
+        end.
+
+  Definition barrierN := nroot .@ "chainable_barrier".
+  Definition barrier_inv (γ γ' : gname) : iProp Σ :=
+    ∃ (bs : gset barrier), own γ (● GSet bs) ∗ own γ' (● GSet bs)
+      ∗ [∗ set] b ∈ bs, is_barrier γ' b bs.
+
+  Definition send (v : val) (P : iProp Σ) : iProp Σ :=
+    ∃ (γ γ' : gname) (b : barrier),
+      ⌜v = SOMEV #b.(location)⌝
+        ∗ b.(location) ↦{#1 / 2} (#false, option_loc_to_val b.(prev))
+        ∗ own γ (◯ GSet {[b]})
+        ∗ saved_prop_own b.(γsp) DfracDiscarded P
+        ∗ inv barrierN (barrier_inv γ γ').
+  
+  Definition recv (v : val) (P : iProp Σ) : iProp Σ :=
+    ∃ (γ γ' : gname) (b : barrier),
+      ⌜v = SOMEV #b.(location)⌝
+        ∗ own γ' (◯ GSet {[b]})
+        ∗ own b.(γr) (Excl ())
+        ∗ saved_prop_own b.(γsp) DfracDiscarded P
+        ∗ inv barrierN (barrier_inv γ γ').
+
+  Lemma option_loc_to_val_inj (l l' : option loc) :
+    option_loc_to_val l = option_loc_to_val l' -> l = l'.
+  Proof.
+    unfold option_loc_to_val. intros H.
+    destruct l; destruct l';
+    try discriminate H; try injection H as ->; auto.
+  Qed.
+
+  Lemma frag_in_gset (γ : gname) (b : barrier) (bs : gset barrier) :
+    own γ (● GSet bs) -∗
+    own γ (◯ GSet {[b]}) -∗
+      ⌜b ∈ bs⌝.
+  Proof.
+    iIntros "H● H◯".
+    iDestruct (own_valid_2 with "H● H◯")
+      as %[Hin%gset_disj_included%singleton_subseteq_l _]%auth_both_valid_discrete.
+    done.
+  Qed.
+
+  Lemma new_barrier_spec (P : iProp Σ) :
+    {{{ True }}} new_barrier #() {{{ b, RET b; send b P ∗ recv b P }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    wp_lam. wp_alloc l as "[Hl Hl']".
+    wp_inj. iApply "HΦ".
+    iMod (saved_prop_alloc P DfracDiscarded) as (γsp) "#Hsp"; first done.
+    iMod (own_alloc (Excl ())) as (γr) "Hγr"; first done.
+    set (b := {|location := l; γsp := γsp; γr := γr; prev := None|}).
+    iMod (own_alloc (● GSet {[b]} ⋅ ◯ GSet {[b]})) as (γ) "[H●s H◯s]".
+    { rewrite auth_both_valid_discrete. done. }
+    iMod (own_alloc (● GSet {[b]} ⋅ ◯ GSet {[b]})) as (γ') "[H●r H◯r]".
+    { rewrite auth_both_valid_discrete. done. }
+    iMod (inv_alloc barrierN _ (barrier_inv γ γ') with "[Hl' H●s H●r]") as "#Hinv".
+    { iExists {[b]}. iFrame.
+      iApply big_sepS_singleton.
+      iExists false, None, P.
+      auto with iFrame. }
+    iSplitR "H◯r Hγr".
+    - iExists γ, γ', b. auto with iFrame.
+    - iExists γ, γ', b. auto with iFrame.
+  Qed.
+
+  Lemma unwrap_spec (v : val) Φ :
+    Φ v -∗ WP unwrap (SOMEV v) {{ v', Φ v' }}.
+  Proof.
+    iIntros "HΦ". wp_lam. wp_match. iApply "HΦ".
+  Qed.
+
+  Lemma signal_spec (b : val) (P : iProp Σ) :
+    {{{ send b P ∗ P }}} signal b {{{ RET #(); True }}}.
+  Proof.
+    rename b into v.
+    iIntros (Φ) "[Hs HP] HΦ".
+    iDestruct "Hs" as (γ γ' b ->) "(Hl & H◯ & #Hsp & #Hinv)".
+    wp_lam. wp_apply unwrap_spec. wp_let. wp_load.
+    wp_let. wp_proj. wp_pair.
+    iInv barrierN as (bs) "(>H●s & >H●r & Hbs)" "Hclose".
+    iDestruct (frag_in_gset with "H●s H◯") as %Hin.
+    iDestruct (big_sepS_delete with "Hbs") as "(Hb & Hbs)"; first apply Hin.
+    iDestruct "Hb" as (flag b' P') "(>Hl' & #Hsp' & HP' & Hprev)".
+    iDestruct (mapsto_agree with "Hl' Hl") as %[=-> ?%option_loc_to_val_inj].
+    (* We can't just subst this away since we need it to close the invariant *)
+    rewrite <- H0.
+    iCombine "Hl Hl'" as "Hl". wp_store. iDestruct "Hl" as "[Hl _]".
+    iMod ("Hclose" with "[- HΦ]"); last by iApply "HΦ".
+    iExists bs. iFrame "H●s H●r".
+    iApply big_sepS_delete; first apply Hin.
+    iFrame "Hbs". iExists true, b', P.
+    auto with iFrame.
+  Qed.
+
+  Lemma wait_spec (b : val) (P : iProp Σ) :
+    {{{ recv b P }}} wait b {{{ RET #(); P }}}.
+  Proof.
+    rename b into v.
+    iIntros (Φ) "Hr HΦ".
+    iDestruct "Hr" as (γ γ' b ->) "(H◯ & Hγr & #Hsp & #Hinv)".
+    iLöb as "IH" forall (b P) "Hsp".
+    wp_rec. wp_match. wp_bind (! _)%E.
+    iInv barrierN as (bs) "(>H●s & >H●r & Hbs)" "Hclose".
+    iDestruct (frag_in_gset with "H●r H◯") as %Hin.
+    iDestruct (big_sepS_delete with "Hbs") as "[Hb Hbs]"; first apply Hin.
+    iDestruct "Hb" as (flag b' P') "(>Hl & #Hsp' & HP' & Hprev)".
+    wp_load. iDestruct (saved_prop_agree with "Hsp Hsp'") as "Heq".
+    destruct flag.
+    - (* l ↦ (#true, prev) so we check if we need to wait on a previous barrier *)
+      iDestruct "HP'" as "[Hγr' | HP']".
+      { iDestruct (own_valid_2 with "Hγr Hγr'") as %[]. }
+      destruct b' as [b'|].
+      + (* There is a previous barrier *)
+        iDestruct "Hprev" as %Hin'.
+        iDestruct (big_sepS_delete with "Hbs") as "[Hb' Hbs]"; first apply Hin'.
+        iDestruct "Hb'" as (flag b'' P'') "(Hl' & #Hsp'' & HP'' & Hprev)".
+        iMod ("Hclose" with "[H●s H●r Hbs Hl Hγr Hl' HP'' Hprev]") as "_".
+        { iExists bs. iFrame "H●s H●r".
+          iApply big_sepS_delete; first apply Hin.
+          iSplitL "Hl Hγr".
+          { iExists true, (Some b'), P. auto with iFrame. }
+          iApply (big_sepS_delete _ _ b'); first set_solver.
+          iFrame "Hbs". iExists flag, b'', P''. by iFrame. }
+        iModIntro. wp_let. wp_proj. wp_if_true. wp_proj.
+        unfold option_loc_to_val; simpl.
+        (* iApply ("IH" with "H◯' [] [-] Hsp''"). *)
+        admit.
+      + (* There is no previous barrier *)
+        iMod ("Hclose" with "[H●s H●r Hl Hγr Hbs]") as "_".
+        { iExists bs. iFrame "H●s H●r".
+          iApply big_sepS_delete; first apply Hin.
+          iFrame "Hbs". iExists true, None, P.
+          auto with iFrame. }
+        iModIntro. wp_let. wp_proj. wp_if_true. wp_proj.
+        wp_rec. wp_match. iApply "HΦ". by iRewrite "Heq".
+    - (* l ↦ (#false, prev) so we continue waiting for ourselves *)
+      iMod ("Hclose" with "[H●s H●r Hbs Hl Hprev]") as "_".
+      { iExists bs. iFrame "H●s H●r".
+        iApply big_sepS_delete; first apply Hin.
+        iFrame "Hbs". iExists false, b', P'.
+        auto with iFrame. }
+      iModIntro. wp_let. wp_proj. wp_if_false.
+      iApply ("IH" with "H◯ Hγr HΦ Hsp").
+  Admitted.
+
+  (* TODO: Make chain by default at least length 1? *)
+  Fixpoint is_chain (hd : val) (xs : list bool) : iProp Σ :=
+    match xs with
+    | [] => ⌜hd = NONEV⌝
+    | x :: xs => ∃ (l : loc) hd', ⌜hd = SOMEV #l⌝ ∗ l ↦ (#x, hd') ∗ is_chain hd' xs
+    end%I.
+
+  (* Weak specs to verify that all functions are somewhat implemented correctly *)
+  Lemma new_barrier_weak_spec :
+    {{{ True }}} new_barrier #() {{{ b, RET b; is_chain b [false] }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". wp_lam.
+    wp_alloc l as "Hl". wp_inj.
+    iApply "HΦ". simpl.
+    iExists l, NONEV. by iFrame.
+  Qed.
+
+  Lemma signal_weak_spec b v1 vs :
+    {{{ is_chain b (v1 :: vs) }}}
+      signal b
+    {{{ RET #(); is_chain b (true :: vs) }}}.
+  Proof.
+    iIntros (Φ) "Hb HΦ". iSimpl in "Hb".
+    iDestruct "Hb" as (l b' ->) "[Hl Hb']".
+    wp_lam. wp_apply unwrap_spec. wp_let.
+    wp_load. wp_let. wp_proj. wp_store.
+    iApply "HΦ". simpl.
+    iExists l, b'. by iFrame.
+  Qed.
+
+  Lemma wait_weak_spec xs b n :
+    n = length xs ->
+    {{{ is_chain b xs }}} wait b {{{ RET #(); is_chain b (replicate n true) }}}.
+  Proof.
+    iIntros (Hn Φ) "Hb HΦ". iRevert (Hn).
+    iLöb as "IH" forall (xs n b); iIntros (Hn).
+    destruct xs as [|x xs].
+    - iDestruct "Hb" as %->. wp_rec.
+      wp_match. iApply "HΦ".
+      subst n. done.
+    - simpl. iDestruct "Hb" as (l b' ->) "[Hl Hb']".
+      wp_rec. wp_match. wp_load. wp_let. wp_proj. destruct x.
+      + (* wait on the previous *)
+        wp_if_true. wp_proj. iApply ("IH" with "Hb' [Hl HΦ] [//]").
+        iIntros "!> Hb'". iApply "HΦ". subst n.
+        simpl. iExists l, b'. by iFrame.
+      + (* keep waiting on ourselves *)
+        wp_if_false. iApply ("IH" $! (false :: xs) with "[Hl Hb'] HΦ [//]").
+        simpl. iExists l, b'. by iFrame.
+  Qed.
+
+  Lemma extend_weak_spec (v1 : bool) (vs : list bool) (b : val) :
+    {{{ is_chain b (v1 :: vs) }}}
+      extend b
+    {{{ (b' : val), RET (b', b); is_chain b (v1 :: false :: vs) }}}.
+  Proof.
+    iIntros (Φ) "Hb HΦ". iSimpl in "Hb".
+    iDestruct "Hb" as (l' b' ->) "[Hl' Hb']".
+    wp_lam. wp_apply unwrap_spec.
+    wp_let. wp_load. wp_let. wp_proj. wp_let.
+    wp_proj. wp_let. wp_alloc l as "Hl". wp_let.
+    wp_store. wp_inj. wp_inj. wp_pair. iApply "HΦ".
+    simpl. iExists l', (InjRV #l). iFrame. iSplitR; first auto.
+    iExists l, b'. by iFrame.
+  Qed.
+
+  Global Opaque new_barrier signal wait extend.
+End proof.

theories/chainable/implementation_list.v

+From iris.heap_lang Require Export notation lang.
+From iris.proofmode Require Export proofmode.
+From iris.heap_lang Require Import proofmode.
+From iris.base_logic Require Import invariants lib.saved_prop.
+From iris.algebra Require Import agree frac list.
+From iris.prelude Require Import options.
+
+From barriers.chainable Require Import specification.
+
+(* Iris implementation of barrier with receive splitting and chains. 
+   This implementation is based on [1].
+   
+   [1]: Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen,
+        and Lars Birkedal. 2016. Verifying Custom Synchronization Constructs
+        Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38,
+        2, Article 4 (January 2016), 72 pages. https://doi.org/10.1145/2818638 *)
+
+Definition new_barrier : val :=
+  λ: <>, SOME (ref (#false, NONEV)).
+
+Definition unwrap : val :=
+  λ: "x", 
+    match: "x" with
+      NONE => #() #()
+    | SOME "x" => "x"
+    end.
+
+Definition signal : val :=
+  λ: "b",
+    let: "b" := unwrap "b" in
+    let: "x" := ! "b" in
+    "b" <- (#true, Snd "x").
+
+Definition wait : val :=
+  rec: "wait" "b" :=
+    match: "b" with
+      NONE => #()
+    | SOME "hd" =>
+      let: "x" := ! "hd" in
+      if: Fst "x" then "wait" (Snd "x")
+      else "wait" "b"
+    end.
+
+Definition extend : val :=
+  λ: "b",
+    let: "b" := unwrap "b" in
+    let: "x" := ! "b" in
+    let: "flag" := Fst "x" in
+    let: "prev" := Snd "x" in
+    let: "b'" := ref (#false, "prev") in
+    "b" <- ("flag", SOME "b'");;
+    (SOME "b'", SOME "b").
+
+Record barrier : Set := {
+  location : loc;
+  γsp : gname;
+  prev : option loc;
+}.
+
+Global Instance barrier_inhabited : Inhabited barrier :=
+  populate {| location := inhabitant; γsp := inhabitant; prev := inhabitant |}.
+
+(* Global Instance barrier_eq_decision : EqDecision barrier.
+Proof.
+  intros [???] [???].
+  destruct (decide (loc0 = loc1));
+  destruct (decide (flag0 = flag1));
+  destruct (decide (γsp0 = γsp1)).
+  1: left; subst; reflexivity.
+  all: right; intros [=]; auto.
+Qed.
+Global Program Instance barrier_countable : Countable barrier := 
+  {| encode b :=
+        prod_encode (encode b.(loc))
+                    (prod_encode (encode b.(flag)) (b.(γsp)));
+     decode p :=
+        l ← prod_decode_fst p ≫= decode;
+        fγ ← prod_decode_snd p ≫= decode;
+        {| loc := |}
+        (* x ← prod_decode_fst p ≫= decode;
+        y ← prod_decode_snd p ≫= decode; Some (x, y) *)
+
+  |}. *)
+
+(* Context `{!EqDecision barrier, !Countable barrier}. *)
+
+Canonical Structure barrierO := leibnizO barrier.
+Class barrierG Σ := BarrierG {
+  (* barrier_inG :> inG Σ (authR (gset_disjUR barrier)); *)
+  barrier_inG :> inG Σ (prodR fracR (agreeR (listO barrierO)));
+  barrier_savedPropG :> savedPropG Σ;
+}.
+
+Definition barrierΣ : gFunctors :=
+  #[ GFunctor (prodR fracR (agreeR (listO barrierO))); savedPropΣ ].
+
+Global Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+
+  Context `{!heapGS Σ, !barrierG Σ}.
+
+  Definition option_to_val (o : option val) : val :=
+    match o with
+    | Some v => SOMEV v
+    | None   => NONEV
+    end.
+
+  Definition option_loc_to_val (o : option loc) : val :=
+    option_to_val ((LitV ∘ LitLoc) <$> o).
+
+  Definition barrierN := nroot .@ "chainable_barrier".
+  Definition barrier_inv (γ : gname) (P : iProp Σ) : iProp Σ :=
+    ∃ (bs : list barrier), own γ ((1/2)%Qp, to_agree bs)
+      ∗ [∗ list] b ∈ bs,
+          ∃ (flag : bool) (R : iProp Σ),
+            b.(location) ↦{#1 / 2} (#flag, option_loc_to_val b.(prev))
+              ∗ saved_prop_own b.(γsp) DfracDiscarded R
+              ∗ ((if flag then True else P) -∗ ▷ R).
+  
+  Definition contains (γ : gname) (bs : list barrier) (b : barrier) : iProp Σ :=
+    ∃ (i : nat),
+      ⌜bs !! i = Some b⌝
+        ∗ ⌜(i = length bs - 1 ∧ b.(prev) = None)
+            ∨ (i < length bs - 1 ∧ b.(prev) = location <$> (bs !! (i + 1)%nat))⌝
+        ∗ own γ ((1/2/2)%Qp, to_agree bs).
+
+  Definition send (b : val) (P : iProp Σ) : iProp Σ :=
+    ∃ (l : loc) (γ γsp : gname) (prev : option loc) (bs : list barrier),
+      ⌜b = SOMEV #l⌝
+        ∗ contains γ bs {| location := l; γsp := γsp; prev := prev |}
+        ∗ l ↦{#1 / 2} (#false, option_loc_to_val prev)
+        ∗ inv barrierN (barrier_inv γ P).
+  
+  Definition recv (b : val) (R : iProp Σ) : iProp Σ :=
+    ∃ (l : loc) (γ γsp : gname) (prev : option loc) (bs : list barrier) (P : iProp Σ),
+      ⌜b = SOMEV #l⌝
+        ∗ contains γ bs {| location := l; γsp := γsp; prev := prev |}
+        ∗ saved_prop_own γsp DfracDiscarded R
+        ∗ inv barrierN (barrier_inv γ P).
+
+  Lemma option_loc_to_val_inj (l l' : option loc) :
+    option_loc_to_val l = option_loc_to_val l' -> l = l'.
+  Proof.
+    unfold option_loc_to_val. intros H.
+    destruct l; destruct l';
+    try discriminate H; try injection H as ->; auto.
+  Qed.
+
+  Lemma contains_agree' (γ : gname) (b : barrier) (q : Qp) (bs bs' : list barrier) :
+    contains γ bs b -∗ own γ (q, to_agree bs') -∗ ⌜bs = bs'⌝.
+  Proof.
+    iDestruct 1 as (???) "Hγ".
+    iIntros "Hγ'".
+    iDestruct (own_valid_2 with "Hγ Hγ'")
+      as %[_ Heq%to_agree_op_valid]%pair_valid.
+    iPureIntro.
+    Admitted. (* TODO: How to fix this? *)
+
+  Lemma contains_agree (γ : gname) (b b' : barrier) (bs bs' : list barrier) :
+    contains γ bs b -∗ contains γ bs' b -∗ ⌜bs = bs'⌝.
+  Proof.
+    iIntros "Hγ".
+    iDestruct 1 as (???) "Hγ'".
+    iApply (contains_agree' with "Hγ Hγ'").
+  Qed.
+
+  Lemma contains_lookup (γ : gname) (bs : list barrier) (b : barrier) :
+    contains γ bs b -∗ ∃ (i : nat), ⌜bs !! i = Some b⌝.
+  Proof.
+    iDestruct 1 as (i Hlookup Hprev) "_". by iExists i.
+  Qed.
+
+  (* Lemma contains_big_sepL_delete. *)
+
+  Lemma new_barrier_spec (P : iProp Σ) :
+    {{{ True }}} new_barrier #() {{{ b, RET b; send b P ∗ recv b P }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    wp_lam. wp_alloc l as "[Hl Hl']".
+    wp_inj. iApply "HΦ".
+    iMod (saved_prop_alloc P DfracDiscarded) as (γsp) "#Hsp"; first done.
+    set (b := {|location := l; γsp := γsp; prev := None|}).
+    iMod (own_alloc (1%Qp, to_agree [b])) as (γ) "[Hlist Hlist']"; first done.
+    iMod (inv_alloc barrierN _ (barrier_inv γ P) with "[Hl' Hlist']") as "#Hinv".
+    { iExists [b]. iFrame "Hlist'".
+      iApply big_sepL_singleton.
+      iExists false, P.
+      auto with iFrame. }
+    iDestruct "Hlist" as "[Hlist Hlist']". iSplitR "Hlist'".
+    - iExists l, γ, γsp, None, [b]. iSplitR; first auto.
+      iFrame "Hl Hinv". iExists 0. iFrame "Hlist". auto.
+    - iExists l, γ, γsp, None, [b], P. iSplitR; first auto.
+      iFrame "Hsp Hinv". iExists 0. iFrame "Hlist'". auto.
+  Qed.
+
+  Lemma unwrap_spec (v : val) Φ :
+    Φ v -∗ WP unwrap (SOMEV v) {{ v', Φ v' }}.
+  Proof.
+    iIntros "HΦ". wp_lam. wp_match. iApply "HΦ".
+  Qed.
+
+  Lemma signal_spec (b : val) (P : iProp Σ) :
+    {{{ send b P ∗ P }}} signal b {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "[Hs HP] HΦ".
+    iDestruct "Hs" as (l γ γsp prev bs ->) "(Hcontains & Hl & #Hinv)".
+    wp_lam. wp_apply unwrap_spec. wp_let. wp_load.
+    iDestruct (contains_lookup with "Hcontains") as %(i & Hlookup).
+    wp_let. wp_proj. wp_pair.
+    iInv barrierN as (bs') "[>Hlist Hbs]" "Hclose".
+    iDestruct (contains_agree' with "Hcontains Hlist") as %<-.
+
+    iDestruct (big_sepL_delete _ bs i _ Hlookup with "Hbs") as "[Hl' Hbs]".
+    simpl. iDestruct "Hl'" as (flag R) "(>Hl' & #Hsp & HR)".
+    iDestruct (mapsto_agree with "Hl' Hl") as %[= ->].
+    iCombine "Hl Hl'" as "Hl". wp_store. iDestruct "Hl" as "[Hl _]".
+    iMod ("Hclose" with "[- HΦ]") as "_"; last by iApply "HΦ".
+    iExists bs. iFrame "Hlist".
+    iApply (big_sepL_delete _ bs i _ Hlookup).
+    iFrame "Hbs". simpl. iExists true, R.
+    iIntros "!> {$Hl $Hsp} _". by iApply "HR".
+  Qed.
+
+  Lemma wait_spec (b : val) (P : iProp Σ) :
+    {{{ recv b P }}} wait b {{{ RET #(); P }}}.
+  Proof.
+    rename P into R. iIntros (Φ) "Hr HΦ".
+    iDestruct "Hr" as (l γ γsp prev bs P ->) "(Hcontains & #Hsp & #Hinv)".
+    iRevert "Hsp". iLöb as "IH" forall (l γsp prev R); iIntros "#Hsp".
+    wp_rec. wp_match. wp_bind (! _)%E.
+    iInv barrierN as (bs') "[>Hlist Hbs]" "Hclose".
+    iDestruct (contains_agree' with "Hcontains Hlist") as %<-.
+    iDestruct "Hcontains" as (i Hlookup Hprev) "Hlist'"; simpl in Hprev.
+    iDestruct (big_sepL_delete _ bs i _ Hlookup with "Hbs") as "[Hl Hbs]".
+    simpl. iDestruct "Hl" as (flag R') "(>Hl & #Hsp' & HR')".
+    wp_load.
+    
+    iMod ("Hclose" with "[Hlist Hbs Hl HR']") as "_".
+    { iExists bs. iFrame "Hlist".
+      iApply (big_sepL_delete _ bs i _ Hlookup).
+      iFrame "Hbs". iExists flag, R'. by iFrame. }
+    iModIntro.
+    
+    destruct flag.
+    - (* l ↦ (#true, prev) so we continue waiting for the previous barrier *)
+      iDestruct (saved_prop_agree with "Hsp Hsp'") as "Heq".
+      destruct Hprev as [[-> ->] | [Hi ->]].
+      + (* There is no previous barrier, so we're done waiting *)
+        wp_let. wp_proj. wp_if_true. wp_proj. wp_lam.
+        unfold option_loc_to_val. wp_match. admit.
+        (* TODO: This invariant isn't quite right... *)
+      + wp_let. wp_proj. wp_if_true. wp_proj.
+        assert (Hprev : bs !! (i + 1) = Some (bs !!! (i + 1))).
+        { apply list_lookup_lookup_total_lt. lia. }
+        rewrite Hprev. unfold option_loc_to_val. simpl.
+