Library zoo_std.ivar_3

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Import
  lib.mono_gmultiset
  lib.oneshot
  lib.subpreds.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  ivar_3__code.
From zoo_std Require Import
  ivar_3__types
  list
  option.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types v waiter ctx : val.
Implicit Types waiters : list val.
Implicit Types own : ownership.

Class Ivar3G Σ `{zoo_G : !ZooG Σ} waiter_name `{Countable waiter_name} :=
  { #[local] ivar_3_G_lstate_G :: OneshotG Σ unit val
  ; #[local] ivar_3_G_consumer_G :: SubpredsG Σ val
  ; #[local] ivar_3_G_waiters_G :: MonoGmultisetG Σ (val × waiter_name)
  }.

Definition ivar_3_Σ waiter_name `{Countable waiter_name} :=
  #[oneshot_Σ unit val
  ; subpreds_Σ val
  ; mono_gmultiset_Σ (val × waiter_name)
  ].
#[global] Instance subG_ivar_3_Σ Σ `{zoo_G : !ZooG Σ} waiter_name `{Countable waiter_name} :
  subG (ivar_3_Σ waiter_name) Σ →
  Ivar3G Σ waiter_name.

Module base.
  Variant state :=
    | Unset waiters
    | Set_ v.
  Implicit Types state : state.

  #[local] Instance state_inhabited : Inhabited state :=
    populate (Unset []).

  #[local] Definition state_to_bool state :=
    match state with
    | Unset _ ⇒
        false
    | Set_ _ ⇒
        true
    end.
  #[local] Definition state_to_option state :=
    match state with
    | Unset _ ⇒
        None
    | Set_ v ⇒
        Some v
    end.
  #[local] Coercion state_to_val state :=
    match state with
    | Unset waiters ⇒
        ‘Unset[ list_to_val waiters ]
    | Set_ v ⇒
        ‘Set( v )
    end%V.

  Section ivar_3_G.
    Context `{ivar_3_G : Ivar3G Σ waiter_name}.

    Implicit Types t : location.
    Implicit Types ω : waiter_name.
    Implicit Types ωs : list waiter_name.
    Implicit Types Ψ Χ Ξ : val → iProp Σ.
    Implicit Types Ω : val → val → waiter_name → iProp Σ.

    Record ivar_3_name :=
      { ivar_3_name_lstate : gname
      ; ivar_3_name_consumer : gname
      ; ivar_3_name_waiters : gname
      }.
    Implicit Types γ : ivar_3_name.

    #[global] Instance ivar_3_name_eq_dec : EqDecision ivar_3_name :=
      ltac:(solve_decision).
    #[global] Instance ivar_3_name_countable :
      Countable ivar_3_name.

    #[local] Definition lstate_unset₁' γ_lstate :=
      oneshot_pending γ_lstate (DfracOwn (1/3)) ().
    #[local] Definition lstate_unset₁ γ :=
      lstate_unset₁' γ.(ivar_3_name_lstate).
    #[local] Definition lstate_unset₂' γ_lstate :=
      oneshot_pending γ_lstate (DfracOwn (2/3)) ().
    #[local] Definition lstate_unset₂ γ :=
      lstate_unset₂' γ.(ivar_3_name_lstate).
    #[local] Definition lstate_set γ :=
      oneshot_shot γ.(ivar_3_name_lstate).

    #[local] Definition consumer_auth' :=
      subpreds_auth.
    #[local] Definition consumer_auth γ :=
      consumer_auth' γ.(ivar_3_name_consumer).
    #[local] Definition consumer_frag' :=
      subpreds_frag.
    #[local] Definition consumer_frag γ :=
      consumer_frag' γ.(ivar_3_name_consumer).

    #[local] Definition waiters_auth' γ_waiters own waiters ωs : iProp Σ :=
      ∃ 𝑤𝑎𝑖𝑡𝑒𝑟𝑠,
      ⌜𝑤𝑎𝑖𝑡𝑒𝑟𝑠 = list_to_set_disj (zip waiters ωs)⌝ ∗
      mono_gmultiset_auth γ_waiters own 𝑤𝑎𝑖𝑡𝑒𝑟𝑠.
    #[local] Definition waiters_auth γ :=
      waiters_auth' γ.(ivar_3_name_waiters).
    #[local] Instance : CustomIpat "waiters_auth" :=
      " ( %𝑤𝑎𝑖𝑡𝑒𝑟𝑠 & -> & Hauth ) ".
    #[local] Definition waiters_elem γ waiter ω :=
      mono_gmultiset_elem γ.(ivar_3_name_waiters) (waiter, ω).

    #[local] Definition inv_state_unset t γ Ω waiters : iProp Σ :=
      ∃ ωs,
      lstate_unset₁ γ ∗
      waiters_auth γ Own waiters ωs ∗
      [∗ list] waiter; ω ∈ waiters; ωs, Ω #t waiter ω.
    #[local] Instance : CustomIpat "inv_state_unset" :=
      " ( %ωs & {>;}Hlstate_unset₁ & {>;}Hwaiters_auth & Hwaiters ) ".
    #[local] Definition inv_state_set γ Ξ v : iProp Σ :=
      lstate_set γ v ∗
      □ Ξ v.
    #[local] Instance : CustomIpat "inv_state_set" :=
      " ( {>;}#Hlstate_set{_{}} & #HΞ{_{}} ) ".
    #[local] Definition inv_state t γ Ξ Ω state :=
      match state with
      | Unset waiters ⇒
          inv_state_unset t γ Ω waiters
      | Set_ v ⇒
          inv_state_set γ Ξ v
      end.

    #[local] Definition inv_inner t γ Ψ Ξ Ω : iProp Σ :=
      ∃ state,
      t ↦ᵣ state ∗
      consumer_auth γ Ψ (state_to_option state) ∗
      inv_state t γ Ξ Ω state.
    #[local] Instance : CustomIpat "inv_inner" :=
      " ( %state & Ht & Hconsumer_auth & Hstate ) ".
    Definition ivar_3_inv t γ Ψ Ξ Ω : iProp Σ :=
      inv nroot (inv_inner t γ Ψ Ξ Ω).
    #[local] Instance : CustomIpat "inv" :=
      " #Hinv ".

    Definition ivar_3_producer :=
      lstate_unset₂.
    #[local] Instance : CustomIpat "producer" :=
      " Hlstate_unset₂{_{}} ".

    Definition ivar_3_consumer :=
      consumer_frag.
    #[local] Instance : CustomIpat "consumer" :=
      " Hconsumer{}_frag ".

    Definition ivar_3_result :=
      lstate_set.
    #[local] Instance : CustomIpat "result" :=
      " #Hlstate_set{_{}} ".
    Definition ivar_3_resolved γ : iProp Σ :=
      ∃ v,
      ivar_3_result γ v.

    Definition ivar_3_waiters γ :=
      waiters_auth γ Discard.

    Definition ivar_3_waiter :=
      waiters_elem.

    #[global] Instance ivar_3_inv_contractive t γ n :
      Proper (
        (pointwise_relation _ $ dist_later n) ==>
        (pointwise_relation _ $ dist_later n) ==>
        (pointwise_relation _ $ pointwise_relation _ $ pointwise_relation _ $ dist_later n) ==>
        (≡{n}≡)
      ) (ivar_3_inv t γ).
    #[global] Instance ivar_3_inv_proper t γ :
      Proper (
        (pointwise_relation _ (≡)) ==>
        (pointwise_relation _ (≡)) ==>
        (pointwise_relation _ $ pointwise_relation _ $ pointwise_relation _ (≡)) ==>
        (≡)
      ) (ivar_3_inv t γ).
    #[global] Instance ivar_3_consumer_contractive γ n :
      Proper (
        (pointwise_relation _ $ dist_later n) ==>
        (≡{n}≡)
      ) (ivar_3_consumer γ).
    #[global] Instance ivar_3_consumer_proper γ :
      Proper (
        (pointwise_relation _ (≡)) ==>
        (≡)
      ) (ivar_3_consumer γ).

    #[local] Instance waiters_auth_timeless γ own waiters ωs :
      Timeless (waiters_auth γ own waiters ωs).
    #[global] Instance ivar_3_producer_timeless γ :
      Timeless (ivar_3_producer γ).
    #[global] Instance ivar_3_result_timeless γ v :
      Timeless (ivar_3_result γ v).
    #[global] Instance ivar_3_waiters_timeless γ waiters ωs :
      Timeless (ivar_3_waiters γ waiters ωs).
    #[global] Instance ivar_3_waiter_timeless γ waiter ω :
      Timeless (ivar_3_waiter γ waiter ω).

    #[global] Instance ivar_3_inv_persistent t γ Ψ Ξ Ω :
      Persistent (ivar_3_inv t γ Ψ Ξ Ω).
    #[global] Instance ivar_3_result_persistent γ v :
      Persistent (ivar_3_result γ v).
    #[global] Instance ivar_3_waiters_persistent γ waiters ωs :
      Persistent (ivar_3_waiters γ waiters ωs).
    #[global] Instance ivar_3_waiter_persistent γ waiter ω :
      Persistent (ivar_3_waiter γ waiter ω).

    #[local] Lemma lstate_alloc :
      ⊢ |==>
        ∃ γ_lstate,
        lstate_unset₁' γ_lstate ∗
        lstate_unset₂' γ_lstate.
    #[local] Lemma lstate_unset₂_exclusive γ :
      lstate_unset₂ γ -∗
      lstate_unset₂ γ -∗
      False.
    #[local] Lemma lstate_set_agree γ v1 v2 :
      lstate_set γ v1 -∗
      lstate_set γ v2 -∗
      ⌜v1 = v2⌝.
    #[local] Lemma lstate_unset₁_set γ v :
      lstate_unset₁ γ -∗
      lstate_set γ v -∗
      False.
    #[local] Lemma lstate_unset₂_set γ v :
      lstate_unset₂ γ -∗
      lstate_set γ v -∗
      False.
    #[local] Lemma lstate_update {γ} v :
      lstate_unset₁ γ -∗
      lstate_unset₂ γ ==∗
      lstate_set γ v.

    #[local] Lemma consumer_alloc Ψ :
      ⊢ |==>
        ∃ γ_consumer,
        consumer_auth' γ_consumer Ψ None ∗
        consumer_frag' γ_consumer Ψ.
    #[local] Lemma consumer_wand {γ Ψ} {state : option val} {Χ1} Χ2 E :
      ▷ consumer_auth γ Ψ state -∗
      consumer_frag γ Χ1 -∗
      (∀ v, Χ1 v -∗ Χ2 v) ={E}=∗
        ▷ consumer_auth γ Ψ state ∗
        consumer_frag γ Χ2.
    #[local] Lemma consumer_divide {γ Ψ} {state : option val} Χs E :
      ▷ consumer_auth γ Ψ state -∗
      consumer_frag γ (λ v, [∗ list] Χ ∈ Χs, Χ v) ={E}=∗
        ▷ consumer_auth γ Ψ state ∗
        [∗ list] Χ ∈ Χs, consumer_frag γ Χ.
    #[local] Lemma consumer_produce {γ Ψ} v :
      consumer_auth γ Ψ None -∗
      Ψ v -∗
      consumer_auth γ Ψ (Some v).
    #[local] Lemma consumer_consume γ Ψ v Χ E :
      ▷ consumer_auth γ Ψ (Some v) -∗
      consumer_frag γ Χ ={E}=∗
        ▷ consumer_auth γ Ψ (Some v) ∗
        ▷^2 Χ v.

    #[local] Lemma waiters_alloc :
      ⊢ |==>
        ∃ γ_waiters,
        waiters_auth' γ_waiters Own [] [].
    #[local] Lemma waiters_elem_valid γ own waiters ωs waiter ω :
      waiters_auth γ own waiters ωs -∗
      waiters_elem γ waiter ω -∗
        ∃ i,
        ⌜waiters !! i = Some waiter⌝ ∗
        ⌜ωs !! i = Some ω⌝.
    #[local] Lemma waiters_insert {γ waiters ωs} waiter ω :
      waiters_auth γ Own waiters ωs ⊢ |==>
        waiters_auth γ Own (waiter :: waiters) (ω :: ωs) ∗
        waiters_elem γ waiter ω.
    #[local] Lemma waiters_auth_discard γ waiters ωs :
      waiters_auth γ Own waiters ωs ⊢ |==>
      waiters_auth γ Discard waiters ωs.
    Opaque waiters_auth'.

    Lemma ivar_3_producer_exclusive γ :
      ivar_3_producer γ -∗
      ivar_3_producer γ -∗
      False.

    Lemma ivar_3_consumer_wand {t γ Ψ Ξ Ω Χ1} Χ2 :
      ivar_3_inv t γ Ψ Ξ Ω -∗
      ivar_3_consumer γ Χ1 -∗
      (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
      ivar_3_consumer γ Χ2.
    Lemma ivar_3_consumer_divide {t γ Ψ Ξ Ω} Χs :
      ivar_3_inv t γ Ψ Ξ Ω -∗
      ivar_3_consumer γ (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
      [∗ list] Χ ∈ Χs, ivar_3_consumer γ Χ.

    Lemma ivar_3_result_agree γ v1 v2 :
      ivar_3_result γ v1 -∗
      ivar_3_result γ v2 -∗
      ⌜v1 = v2⌝.

    Lemma ivar_3_producer_result γ v :
      ivar_3_producer γ -∗
      ivar_3_result γ v -∗
      False.

    Lemma ivar_3_inv_result t γ Ψ Ξ Ω v :
      ivar_3_inv t γ Ψ Ξ Ω -∗
      ivar_3_result γ v ={⊤}=∗
      ▷ □ Ξ v.
    Lemma ivar_3_inv_result_consumer t γ Ψ Ξ Ω v Χ :
      ivar_3_inv t γ Ψ Ξ Ω -∗
      ivar_3_result γ v -∗
      ivar_3_consumer γ Χ ={⊤}=∗
        ▷^2 Χ v ∗
        ▷ □ Ξ v.

    Lemma ivar_3_waiter_valid γ waiters ωs waiter ω :
      ivar_3_waiters γ waiters ωs -∗
      ivar_3_waiter γ waiter ω -∗
        ∃ i,
        ⌜waiters !! i = Some waiter⌝ ∗
        ⌜ωs !! i = Some ω⌝.

    Lemma ivar_3٠create𑁒spec Ψ Ξ Ω :
      {{{
        True
      }}}
        ivar_3٠create ()
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_producer γ ∗
        ivar_3_consumer γ Ψ
      }}}.

    Lemma ivar_3٠make𑁒spec Ψ Ξ Ω v :
      {{{
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}}
        ivar_3٠make v
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_consumer γ Ψ ∗
        ivar_3_result γ v ∗
        ivar_3_waiters γ [] []
      }}}.

    Lemma ivar_3٠is_unset𑁒spec t γ Ψ Ξ Ω :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω
      }}}
        ivar_3٠is_unset #t
      {{{
        b
      , RET #b;
        if b then
          True
        else
          £ 2 ∗
          ivar_3_resolved γ
      }}}.
    Lemma ivar_3٠is_unset𑁒spec_result t γ Ψ Ξ Ω v :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_result γ v
      }}}
        ivar_3٠is_unset #t
      {{{
        RET false;
        £ 2
      }}}.

    Lemma ivar_3٠is_set𑁒spec t γ Ψ Ξ Ω :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω
      }}}
        ivar_3٠is_set #t
      {{{
        b
      , RET #b;
        if b then
          £ 2 ∗
          ivar_3_resolved γ
        else
          True
      }}}.
    Lemma ivar_3٠is_set𑁒spec_result t γ Ψ Ξ Ω v :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_result γ v
      }}}
        ivar_3٠is_set #t
      {{{
        RET true;
        £ 2
      }}}.

    Lemma ivar_3٠try_get𑁒spec t γ Ψ Ξ Ω :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω
      }}}
        ivar_3٠try_get #t
      {{{
        o
      , RET o;
        if o is Some v then
          £ 2 ∗
          ivar_3_result γ v
        else
          True
      }}}.
    Lemma ivar_3٠try_get𑁒spec_result t γ Ψ Ξ Ω v :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_result γ v
      }}}
        ivar_3٠try_get #t
      {{{
        RET Some v;
        £ 2
      }}}.

    Lemma ivar_3٠get𑁒spec t γ Ψ Ξ Ω v :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_result γ v
      }}}
        ivar_3٠get #t
      {{{
        RET v;
        £ 2
      }}}.

    Lemma ivar_3٠wait𑁒spec ω P t γ Ψ Ξ Ω waiter :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        P ∗
        (P -∗ Ω #t waiter ω)
      }}}
        ivar_3٠wait #t waiter
      {{{
        o
      , RET o;
        if o is Some v then
          £ 2 ∗
          ivar_3_result γ v ∗
          P
        else
          ivar_3_waiter γ waiter ω
      }}}.

    Lemma ivar_3٠set𑁒spec t γ Ψ Ξ Ω v :
      {{{
        ivar_3_inv t γ Ψ Ξ Ω ∗
        ivar_3_producer γ ∗
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}}
        ivar_3٠set #t v
      {{{
        waiters ωs
      , RET list_to_val waiters;
        ivar_3_result γ v ∗
        ivar_3_waiters γ waiters ωs ∗
        [∗ list] waiter; ω ∈ waiters; ωs, Ω #t waiter ω
      }}}.
  End ivar_3_G.

  #[global] Opaque ivar_3_inv.
  #[global] Opaque ivar_3_producer.
  #[global] Opaque ivar_3_consumer.
  #[global] Opaque ivar_3_result.
  #[global] Opaque ivar_3_waiter.
  #[global] Opaque ivar_3_waiters.
End base.

From zoo_std Require
  ivar_3__opaque.

Section ivar_3_G.
  Context `{ivar_3_G : Ivar3G Σ waiter_name}.

  Implicit Types 𝑡 : location.
  Implicit Types t : val.
  Implicit Types Ψ Χ Ξ : val → iProp Σ.
  Implicit Types Ω : val → val → waiter_name → iProp Σ.

  Definition ivar_3_inv t Ψ Ξ Ω : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_inv 𝑡 γ Ψ Ξ Ω.
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".

  Definition ivar_3_producer t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_producer γ.
  #[local] Instance : CustomIpat "producer" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hproducer{_{}} ) ".

  Definition ivar_3_consumer t Χ : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_consumer γ Χ.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hconsumer{_{}} ) ".

  Definition ivar_3_result t v : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_result γ v.
  #[local] Instance : CustomIpat "result" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hresult{_{}} ) ".
  Definition ivar_3_resolved t : iProp Σ :=
    ∃ v,
    ivar_3_result t v.

  Definition ivar_3_waiters t waiters ωs : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_waiters γ waiters ωs.
  #[local] Instance : CustomIpat "waiters" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hwaiters{_{}} ) ".

  Definition ivar_3_waiter t waiter ω : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    base.ivar_3_waiter γ waiter ω.
  #[local] Instance : CustomIpat "waiter" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hwaiter{_{}} ) ".

  #[global] Instance ivar_3_inv_contractive t n :
    Proper (
      (pointwise_relation _ $ dist_later n) ==>
      (pointwise_relation _ $ dist_later n) ==>
      (pointwise_relation _ $ pointwise_relation _ $ pointwise_relation _ $ dist_later n) ==>
      (≡{n}≡)
    ) (ivar_3_inv t).
  #[global] Instance ivar_3_inv_proper t :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (pointwise_relation _ (≡)) ==>
      (pointwise_relation _ $ pointwise_relation _ $ pointwise_relation _ (≡)) ==>
      (≡)
    ) (ivar_3_inv t).
  #[global] Instance ivar_3_consumer_contractive t n :
    Proper (
      (pointwise_relation _ $ dist_later n) ==>
      (≡{n}≡)
    ) (ivar_3_consumer t).
  #[global] Instance ivar_3_consumer_proper t :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (≡)
    ) (ivar_3_consumer t).

  #[global] Instance ivar_3_producer_timeless t :
    Timeless (ivar_3_producer t).
  #[global] Instance ivar_3_result_timeless t v :
    Timeless (ivar_3_result t v).
  #[global] Instance ivar_3_waiters_timeless t waiters ωs :
    Timeless (ivar_3_waiters t waiters ωs).
  #[global] Instance ivar_3_waiter_timeless t waiter ω :
    Timeless (ivar_3_waiter t waiter ω).

  #[global] Instance ivar_3_inv_persistent t Ψ Ξ Ω :
    Persistent (ivar_3_inv t Ψ Ξ Ω).
  #[global] Instance ivar_3_result_persistent t v :
    Persistent (ivar_3_result t v).
  #[global] Instance ivar_3_waiters_persistent t waiters ωs :
    Persistent (ivar_3_waiters t waiters ωs).
  #[global] Instance ivar_3_waiter_persistent t waiter ω :
    Persistent (ivar_3_waiter t waiter ω).

  Lemma ivar_3_producer_exclusive t :
    ivar_3_producer t -∗
    ivar_3_producer t -∗
    False.

  Lemma ivar_3_consumer_wand {t Ψ Ξ Ω Χ1} Χ2 :
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_consumer t Χ1 -∗
    (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
    ivar_3_consumer t Χ2.
  Lemma ivar_3_consumer_divide {t Ψ Ξ Ω} Χs :
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_consumer t (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
    [∗ list] Χ ∈ Χs, ivar_3_consumer t Χ.
  Lemma ivar_3_consumer_split {t Ψ Ξ Ω} Χ1 Χ2 :
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
      ivar_3_consumer t Χ1 ∗
      ivar_3_consumer t Χ2.
  Lemma ivar_3_result_agree t v1 v2 :
    ivar_3_result t v1 -∗
    ivar_3_result t v2 -∗
    ⌜v1 = v2⌝.

  Lemma ivar_3_producer_result t v :
    ivar_3_producer t -∗
    ivar_3_result t v -∗
    False.

  Lemma ivar_3_inv_result t Ψ Ξ Ω v :
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_result t v ={⊤}=∗
    ▷ □ Ξ v.
  Lemma ivar_3_inv_result' t Ψ Ξ Ω v :
    £ 1 -∗
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_result t v ={⊤}=∗
    □ Ξ v.
  Lemma ivar_3_inv_result_consumer t Ψ Ξ Ω v Χ :
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_result t v -∗
    ivar_3_consumer t Χ ={⊤}=∗
      ▷^2 Χ v ∗
      ▷ □ Ξ v.
  Lemma ivar_3_inv_result_consumer' t Ψ Ξ Ω v Χ :
    £ 2 -∗
    ivar_3_inv t Ψ Ξ Ω -∗
    ivar_3_result t v -∗
    ivar_3_consumer t Χ ={⊤}=∗
      Χ v ∗
      □ Ξ v.

  Lemma ivar_3_waiter_valid t waiters ωs waiter ω :
    ivar_3_waiters t waiters ωs -∗
    ivar_3_waiter t waiter ω -∗
      ∃ i,
      ⌜waiters !! i = Some waiter⌝ ∗
      ⌜ωs !! i = Some ω⌝.

  Lemma ivar_3٠create𑁒spec Ψ Ξ Ω :
    {{{
      True
    }}}
      ivar_3٠create ()
    {{{
      t
    , RET t;
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_producer t ∗
      ivar_3_consumer t Ψ
    }}}.

  Lemma ivar_3٠make𑁒spec Ψ Ξ Ω v :
    {{{
      ▷ Ψ v ∗
      ▷ □ Ξ v
    }}}
      ivar_3٠make v
    {{{
      t
    , RET t;
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_consumer t Ψ ∗
      ivar_3_result t v ∗
      ivar_3_waiters t [] []
    }}}.

  Lemma ivar_3٠is_unset𑁒spec t Ψ Ξ Ω :
    {{{
      ivar_3_inv t Ψ Ξ Ω
    }}}
      ivar_3٠is_unset t
    {{{
      b
    , RET #b;
      if b then
        True
      else
        £ 2 ∗
        ivar_3_resolved t
    }}}.
  Lemma ivar_3٠is_unset𑁒spec_result t Ψ Ξ Ω v :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_result t v
    }}}
      ivar_3٠is_unset t
    {{{
      RET false;
      £ 2
    }}}.

  Lemma ivar_3٠is_set𑁒spec t Ψ Ξ Ω :
    {{{
      ivar_3_inv t Ψ Ξ Ω
    }}}
      ivar_3٠is_set t
    {{{
      b
    , RET #b;
      if b then
        £ 2 ∗
        ivar_3_resolved t
      else
        True
    }}}.
  Lemma ivar_3٠is_set𑁒spec_result t Ψ Ξ Ω v :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_result t v
    }}}
      ivar_3٠is_set t
    {{{
      RET true;
      £ 2
    }}}.

  Lemma ivar_3٠try_get𑁒spec t Ψ Ξ Ω :
    {{{
      ivar_3_inv t Ψ Ξ Ω
    }}}
      ivar_3٠try_get t
    {{{
      o
    , RET o;
      if o is Some v then
        £ 2 ∗
        ivar_3_result t v
      else
        True
    }}}.
  Lemma ivar_3٠try_get𑁒spec_result t Ψ Ξ Ω v :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_result t v
    }}}
      ivar_3٠try_get t
    {{{
      RET Some v;
      £ 2
    }}}.

  Lemma ivar_3٠get𑁒spec t Ψ Ξ Ω v :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_result t v
    }}}
      ivar_3٠get t
    {{{
      RET v;
      £ 2
    }}}.

  Lemma ivar_3٠wait𑁒spec ω P t Ψ Ξ Ω waiter :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      P ∗
      (P -∗ Ω t waiter ω)
    }}}
      ivar_3٠wait t waiter
    {{{
      o
    , RET o;
      if o is Some v then
        £ 2 ∗
        ivar_3_result t v ∗
        P
      else
        ivar_3_waiter t waiter ω
    }}}.

  Lemma ivar_3٠set𑁒spec t Ψ Ξ Ω v :
    {{{
      ivar_3_inv t Ψ Ξ Ω ∗
      ivar_3_producer t ∗
      ▷ Ψ v ∗
      ▷ □ Ξ v
    }}}
      ivar_3٠set t v
    {{{
      waiters ωs
    , RET list_to_val waiters;
      ivar_3_result t v ∗
      ivar_3_waiters t waiters ωs ∗
      [∗ list] waiter; ω ∈ waiters; ωs, Ω t waiter ω
    }}}.
End ivar_3_G.

#[global] Opaque ivar_3_inv.
#[global] Opaque ivar_3_producer.
#[global] Opaque ivar_3_consumer.
#[global] Opaque ivar_3_result.
#[global] Opaque ivar_3_waiter.
#[global] Opaque ivar_3_waiters.