Library zoo_saturn.inf_queue_mpmc_2

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.function.
Require Import zoo.common.list.
Require Import zoo.common.relations.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_identifier.
Require Import zoo.program_logic.prophet_multi.
Require Import zoo.program_logic.prophet_nat.
Require Export zoo_saturn.inf_queue_mpmc_2__code.
Require Import zoo_saturn.inf_queue_mpmc_2__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type front back : nat.
Implicit Type v : val.
Implicit Type o : option val.
Implicit Type vs : list val.
Implicit Type hist : list (option val).
Implicit Type slot : optional val.
Implicit Type slots : nat → optional val.
Implicit Type η : gname.
Implicit Type ηs : list gname.
Implicit Type past prophs : list prophet_identifier.(prophet_typed ۰ type).
Implicit Type pasts prophss : nat → list prophet_identifier.(prophet_typed ۰ type).

Variant lstate :=
  | Producer
  | ProducerProducer
  | ProducerConsumer
  | Consumer
  | ConsumerProducer η
  | ConsumerConsumer.
#[local] Canonical lstate ۰ O {SI : sidx} :=
  leibnizO lstate.
Implicit Type lstate : lstate.
Implicit Type lstates : list lstate.

#[local] Definition lstate ۰ winner lstate :=
  match lstate with
  | Producer ⇒
      Producer
  | ProducerProducer ⇒
      Producer
  | ProducerConsumer ⇒
      Consumer
  | Consumer ⇒
      Consumer
  | ConsumerProducer η ⇒
      Producer
  | ConsumerConsumer ⇒
      Consumer
  end.

#[local] Definition lstate ۰ measure lstate :=
  match lstate with
  | Producer
  | Consumer ⇒
      0
  | ProducerProducer
  | ProducerConsumer
  | ConsumerProducer _
  | ConsumerConsumer ⇒
      1
  end.

Variant lstep : lstate → lstate → Prop :=
  | lstep ｰ producer ｰ producer :
      lstep Producer ProducerProducer
  | lstep ｰ producer ｰ consumer :
      lstep Consumer ProducerConsumer
  | lstep ｰ consumer ｰ producer η :
      lstep Producer (ConsumerProducer η)
  | lstep ｰ consumer ｰ consumer :
      lstep Consumer ConsumerConsumer.

#[local] Lemma lstep ｰ measure lstate1 lstate2 :
  lstep lstate1 lstate2 →
  lstate ۰ measure lstate1 < lstate ۰ measure lstate2.
#[local] Lemma lstep ｰ tc ｰ measure lstate1 lstate2 :
  tc lstep lstate1 lstate2 →
  lstate ۰ measure lstate1 < lstate ۰ measure lstate2.
#[local] Lemma lstep ｰ rtc ｰ measure lstate1 lstate2 :
  rtc lstep lstate1 lstate2 →
  lstate ۰ measure lstate1 ≤ lstate ۰ measure lstate2.

#[local] Instance lsteps ｰ antisymm :
  AntiSymm (=) (rtc lstep).

#[local] Lemma lstate ۰ winner ｰ lb lstate :
  rtc lstep (lstate ۰ winner lstate) lstate.
#[local] Lemma lstep ｰ winner lstate1 lstate2 :
  lstep lstate1 lstate2 →
  lstate ۰ winner lstate1 = lstate ۰ winner lstate2.
#[local] Lemma lsteps ｰ winner lstate1 lstate2 :
  rtc lstep lstate1 lstate2 →
  lstate ۰ winner lstate1 = lstate ۰ winner lstate2.

Class InfQueueMpmc2G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] inf_queue_mpmc_2 ۰ G ۰ inf_array ۰ G :: InfArrayG Σ
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ prophet ۰ G :: ProphetMultiG Σ prophet_identifier
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (list val))
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ history ۰ G :: MonoListG Σ (option val)
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ lstate ۰ G :: AuthMonoG Σ lstep
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ lstates ۰ G :: MonoListG Σ gname
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ saved_pred ۰ G :: SavedPredG Σ val
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ producer ۰ G :: OneshotG Σ () ()
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ producers ۰ G :: MonoListG Σ gname
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ consumer ۰ G :: OneshotG Σ () ()
  ; #[local] inf_queue_mpmc_2 ۰ G ۰ consumers ۰ G :: MonoListG Σ gname
  }.

Definition inf_queue_mpmc_2 ۰ Σ :=
  #[inf_array ۰ Σ
  ; prophet_multi ۰ Σ prophet_identifier
  ; twins ۰ Σ (leibnizO (list val))
  ; mono_list ۰ Σ (option val)
  ; mono_list ۰ Σ gname
  ; auth_mono ۰ Σ lstep
  ; saved_pred ۰ Σ val
  ; oneshot ۰ Σ () ()
  ; mono_list ۰ Σ gname
  ; oneshot ۰ Σ () ()
  ; mono_list ۰ Σ gname
  ].
#[global] Instance subG ｰ inf_queue_mpmc_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG inf_queue_mpmc_2 ۰ Σ Σ →
  InfQueueMpmc2G Σ.

Module base.
  Section inf_queue_mpmc_2 ۰ G.
    Context `{inf_queue_mpmc_2 ۰ G : InfQueueMpmc2G Σ}.

    Implicit Type t : location.
    Implicit Type Ψ : val → iProp Σ.

    Record inf_queue_mpmc_2 ۰ name :=
      { inf_queue_mpmc_2 ۰ name ۰ data : val
      ; inf_queue_mpmc_2 ۰ name ۰ inv : namespace
      ; inf_queue_mpmc_2 ۰ name ۰ prophet : prophet_id
      ; inf_queue_mpmc_2 ۰ name ۰ prophet_name : prophet_multi ۰ name
      ; inf_queue_mpmc_2 ۰ name ۰ model : gname
      ; inf_queue_mpmc_2 ۰ name ۰ history : gname
      ; inf_queue_mpmc_2 ۰ name ۰ lstates : gname
      ; inf_queue_mpmc_2 ۰ name ۰ producers : gname
      ; inf_queue_mpmc_2 ۰ name ۰ consumers : gname
      }.
    Implicit Type γ : inf_queue_mpmc_2 ۰ name.

    #[global] Instance inf_queue_mpmc_2 ۰ name ｰ eq_dec : EqDecision inf_queue_mpmc_2 ۰ name :=
      ltac:(solve_decision).
    #[global] Instance inf_queue_mpmc_2 ۰ name ｰ countable :
      Countable inf_queue_mpmc_2 ۰ name.

    #[local] Definition model₁' γ_model vs :=
      twins ۰ twin₁ γ_model (DfracOwn 1) vs.
    #[local] Definition model₁ γ vs :=
      model₁' γ.(inf_queue_mpmc_2 ۰ name ۰ model) vs.
    #[local] Definition model₂' γ_model vs :=
      twins ۰ twin₂ γ_model vs.
    #[local] Definition model₂ γ vs :=
      model₂' γ.(inf_queue_mpmc_2 ۰ name ۰ model) vs.

    #[local] Definition history ۰ auth' γ_history hist :=
      mono_list ۰ auth γ_history (DfracOwn 1) hist.
    #[local] Definition history ۰ auth γ :=
      history ۰ auth' γ.(inf_queue_mpmc_2 ۰ name ۰ history).
    #[local] Definition history ۰ at γ i o :=
      mono_list ۰ at γ.(inf_queue_mpmc_2 ۰ name ۰ history) i o.

    #[local] Definition lstates ۰ auth' γ_lstates lstates : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ auth γ_lstates (DfracOwn 1) ηs ∗
      [∗ list ] η ; lstate ∈ ηs ; lstates ,
        auth_mono ۰ auth _ η DfracDiscarded lstate.
    #[local] Definition lstates ۰ auth γ :=
      lstates ۰ auth' γ.(inf_queue_mpmc_2 ۰ name ۰ lstates).
    #[local] Instance : CustomIpat "lstates۰auth" :=
      " ( %ηs & Hauth & Hηs ) ".
    #[local] Definition lstates ۰ at γ i lstate : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_2 ۰ name ۰ lstates) i η ∗
      auth_mono ۰ auth _ η DfracDiscarded lstate.
    #[local] Instance : CustomIpat "lstates۰at" :=
      " ( %η{} & #Hat{_{}} & #Hη_auth{_{}} ) ".
    #[local] Definition lstates ۰ lb γ i lstate : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_2 ۰ name ۰ lstates) i η ∗
      auth_mono ۰ lb _ η lstate.
    #[local] Instance : CustomIpat "lstates۰lb" :=
      " ( %η{} & #Hat{_{}} & #Hη_lb{_{}} ) ".

    #[local] Definition producers ۰ auth' γ_producers i : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ auth γ_producers (DfracOwn 1) ηs ∗
      ⌜length ηs = i ⌝.
    #[local] Definition producers ۰ auth γ :=
      producers ۰ auth' γ.(inf_queue_mpmc_2 ۰ name ۰ producers).
    #[local] Instance : CustomIpat "producers۰auth" :=
      " ( %ηs & Hauth & %Hηs ) ".
    #[local] Definition producers ۰ at γ i own : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_2 ۰ name ۰ producers) i η ∗
      match own with
      | Own ⇒
          oneshot ۰ pending η (DfracOwn 1) ()
      | Discard ⇒
          oneshot ۰ shot η ()
      end.
    #[local] Instance : CustomIpat "producers۰at" :=
      " ( %η{} & Hat{_{}} & Hη{} ) ".

    #[local] Definition consumers ۰ auth' γ_consumers i : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ auth γ_consumers (DfracOwn 1) ηs ∗
      ⌜length ηs = i ⌝.
    #[local] Definition consumers ۰ auth γ :=
      consumers ۰ auth' γ.(inf_queue_mpmc_2 ۰ name ۰ consumers).
    #[local] Instance : CustomIpat "consumers۰auth" :=
      " ( %ηs{} & Hauth{} & %Hηs{} ) ".
    #[local] Definition consumers ۰ at γ i own : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_2 ۰ name ۰ consumers) i η ∗
      match own with
      | Own ⇒
          oneshot ۰ pending η (DfracOwn 1) ()
      | Discard ⇒
          oneshot ۰ shot η ()
      end.
    #[local] Instance : CustomIpat "consumers۰at" :=
      " ( %η{} & Hat{_{}} & Hη{} ) ".
    #[local] Definition consumers ۰ lb γ i : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ lb γ.(inf_queue_mpmc_2 ۰ name ۰ consumers) ηs ∗
      ⌜length ηs = i ⌝.
    #[local] Instance : CustomIpat "consumers۰lb" :=
      " ( %ηs{} & Hlb{} & %Hηs{} ) ".

    #[local] Definition winner γ i : iProp Σ :=
      ∃ id prophs ,
      prophet_multi ۰ full prophet_identifier γ.(inf_queue_mpmc_2 ۰ name ۰ prophet_name) i prophs ∗
      ⌜head prophs = Some id ⌝ ∗
      identifier ۰ model id.
    #[local] Instance : CustomIpat "winner" :=
      " ( %id{} & %prophs{} & Hprophet_full{_{}} & %Hprophs{} & Hid{} ) ".

    #[local] Definition consumer ۰ au γ Ψ : iProp Σ :=
      AU <{
        ∃∃ vs ,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(inf_queue_mpmc_2 ۰ name ۰ inv), ∅ <{
        ∀∀ v vs',
        ⌜vs = v :: vs'⌝ ∗
        model₁ γ vs'
      , COMM
        Ψ v
      }>.

    #[local] Definition inv ۰ lstate ۰ left γ back i lstate : iProp Σ :=
      match lstate with
      | ProducerProducer ⇒
          ∃ v ,
          history ۰ at γ i (Some v) ∗
          winner γ i
      | ProducerConsumer ⇒
          history ۰ at γ i None
      | ConsumerProducer η ⇒
          ∃ Ψ v ,
          consumers ۰ lb γ ˖i ∗
          saved_pred η Ψ ∗
          history ۰ at γ i (Some v) ∗
          ( Ψ v
          ∨ consumers ۰ at γ i Discard
          )
      | ConsumerConsumer ⇒
          consumers ۰ lb γ ˖i
      | _ ⇒
          False
      end.
    #[local] Instance : CustomIpat "inv۰lstate۰left۰producer" :=
      " ( %v & #Hhistory_at & Hwinner ) ".
    #[local] Instance : CustomIpat "inv۰lstate۰left۰consumer" :=
      " ( %Ψ & %v_ & #Hconsumers_lb & #Hη_ & #Hhistory_at_ & HΨ ) ".

    #[local] Definition inv ۰ lstate ۰ right γ i lstate : iProp Σ :=
      match lstate with
      | ConsumerProducer η ⇒
          ∃ Ψ ,
          saved_pred η Ψ ∗
          consumer ۰ au γ Ψ
      | ConsumerConsumer ⇒
          winner γ i
      | _ ⇒
          False
      end.
    #[local] Instance : CustomIpat "inv۰lstate۰right" :=
      " ( %Ψ & #Hη & Hconsumer_au ) ".

    #[local] Definition inv ۰ slot γ i slot past : iProp Σ :=
      match slot with
      | Nothing ⇒
          ⌜past = []⌝
      | Something v ⇒
          history ۰ at γ i (Some v) ∗
          producers ۰ at γ i Discard ∗
          lstates ۰ lb γ i Producer
      | Anything ⇒
          consumers ۰ at γ i Discard ∗
          ( lstates ۰ lb γ i Consumer
          ∨ producers ۰ at γ i Discard
          )
      end.
    #[local] Instance : CustomIpat "inv۰slot۰nothing" :=
      " %Hpast ".
    #[local] Instance : CustomIpat "inv۰slot۰something" :=
      " ( #Hhistory_at{_{suff}} & #Hproducers_at{_{suff}} & #Hlstates_lb_producer ) ".
    #[local] Instance : CustomIpat "inv۰slot۰anything" :=
      " ( #Hconsumers_at{_{suff}} & { _{suff} ; [ #Hlstates_lb_consumer | #Hproducers_at_ ] } ) ".

    #[local] Definition inv ۰ inner t γ : iProp Σ :=
      ∃ front back hist slots vs lstates pasts prophss ,
      t .[front ] ↦ #front ∗
      t .[back ] ↦ #back ∗
      inf_array ۰ model γ.(inf_queue_mpmc_2 ۰ name ۰ data) slots ∗
      model₂ γ vs ∗
      ⌜vs = oflatten (drop front hist)⌝ ∗
      history ۰ auth γ hist ∗
      ⌜length hist = back ⌝ ∗
      lstates ۰ auth γ lstates ∗
      ⌜length lstates = front `max ` back ⌝ ∗
      prophet_multi ۰ model prophet_identifier γ.(inf_queue_mpmc_2 ۰ name ۰ prophet) γ.(inf_queue_mpmc_2 ۰ name ۰ prophet_name) pasts prophss ∗
      producers ۰ auth γ back ∗
      consumers ۰ auth γ front ∗
      ( [∗ list ] i ↦ lstate ∈ take back lstates ,
        inv ۰ lstate ۰ left γ back i lstate
      ) ∗
      ( [∗ list ] k ↦ lstate ∈ drop back lstates ,
        inv ۰ lstate ۰ right γ (back + k) lstate
      ) ∗
      ( ∀ i ,
        inv ۰ slot γ i (slots i) (pasts i)
      ).
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %front{} & %back{} & %hist{} & %slots{} & %vs{} & %lstates{} & %pasts{} & %prophss{} & Ht_front & Ht_back & >Hdata_model & Hmodel₂ & >%Hvs{} & Hhistory_auth & >%Hhist{} & Hlstates_auth & >%Hlstates{} & >Hprophet_model & Hproducers_auth & Hconsumers_auth & Hlstates_left & Hlstates_right & Hslots ) ".
    Definition inf_queue_mpmc_2 ۰ inv t γ ι : iProp Σ :=
      ⌜ι = γ.(inf_queue_mpmc_2 ۰ name ۰ inv)⌝ ∗
      t .[data ] ↦□ γ.(inf_queue_mpmc_2 ۰ name ۰ data) ∗
      t .[proph ] ↦□ #γ.(inf_queue_mpmc_2 ۰ name ۰ prophet) ∗
      inf_array ۰ inv γ.(inf_queue_mpmc_2 ۰ name ۰ data) ∗
      inv γ.(inf_queue_mpmc_2 ۰ name ۰ inv) (inv ۰ inner t γ).
    #[local] Instance : CustomIpat "inv" :=
      " ( -> & #Ht_data & #Ht_proph & #Hdata_inv & #Hinv ) ".

    Definition inf_queue_mpmc_2 ۰ model :=
      model₁.
    #[local] Instance : CustomIpat "model" :=
      " Hmodel₁{_{}} ".

    #[global] Instance inf_queue_mpmc_2 ۰ model ｰ timeless γ vs :
      Timeless (inf_queue_mpmc_2 ۰ model γ vs).

    #[local] Instance lstates ۰ at ｰ persistent γ i lstate :
      Persistent (lstates ۰ at γ i lstate).
    #[local] Instance lstates ۰ lb ｰ persistent γ i lstate :
      Persistent (lstates ۰ lb γ i lstate).
    #[local] Instance producers ۰ at ｰ persistent γ i :
      Persistent (producers ۰ at γ i Discard).
    #[local] Instance consumers ۰ at ｰ persistent γ i :
      Persistent (consumers ۰ at γ i Discard).
    #[local] Instance consumers ۰ lb ｰ persistent γ i :
      Persistent (consumers ۰ lb γ i).
    #[local] Instance inv ۰ slot ｰ persistent γ i slot past :
      Persistent (inv ۰ slot γ i slot past).
    #[global] Instance inf_queue_mpmc_2 ۰ inv ｰ persistent t γ ι :
      Persistent (inf_queue_mpmc_2 ۰ inv t γ ι).

    #[local] Lemma model ｰ alloc :
      ⊢ |==>
        ∃ γ_model ,
        model₁' γ_model [] ∗
        model₂' γ_model [].
    #[local] Lemma model₁ ｰ exclusive γ vs1 vs2 :
      model₁ γ vs1 -∗
      model₁ γ vs2 -∗
      False.
    #[local] Lemma model ｰ agree γ vs1 vs2 :
      model₁ γ vs1 -∗
      model₂ γ vs2 -∗
      ⌜vs1 = vs2 ⌝.
    #[local] Lemma model ｰ update {γ vs1 vs2} vs :
      model₁ γ vs1 -∗
      model₂ γ vs2 ==∗
        model₁ γ vs ∗
        model₂ γ vs.

    #[local] Lemma history ｰ alloc :
      ⊢ |==>
        ∃ γ_history ,
        history ۰ auth' γ_history [].
    #[local] Lemma history ۰ at ｰ lookup γ hist i o :
      history ۰ auth γ hist -∗
      history ۰ at γ i o -∗
      ⌜hist !! i = Some o ⌝.
    #[local] Lemma history ۰ at ｰ agree γ i o1 o2 :
      history ۰ at γ i o1 -∗
      history ۰ at γ i o2 -∗
      ⌜o1 = o2 ⌝.
    #[local] Lemma history ۰ at ｰ get {γ hist} i o :
      hist !! i = Some o →
      history ۰ auth γ hist ⊢
      history ۰ at γ i o.
    #[local] Lemma history ｰ update {γ hist} o :
      history ۰ auth γ hist ⊢ |==>
        history ۰ auth γ (hist ++ [o]) ∗
        history ۰ at γ (length hist) o.

    #[local] Lemma lstates ｰ alloc :
      ⊢ |==>
        ∃ γ_lstates ,
        lstates ۰ auth' γ_lstates [].
    #[local] Lemma lstates ۰ at ｰ lookup γ lstates i lstate :
      lstates ۰ auth γ lstates -∗
      lstates ۰ at γ i lstate -∗
      ⌜lstates !! i = Some lstate ⌝.
    #[local] Lemma lstates ۰ lb ｰ get {γ lstates} i lstate :
      lstates !! i = Some lstate →
      lstates ۰ auth γ lstates -∗
      lstates ۰ lb γ i (lstate ۰ winner lstate).
    #[local] Lemma lstates ۰ lb ｰ agree γ i lstate1 lstate2 :
      lstates ۰ lb γ i lstate1 -∗
      lstates ۰ lb γ i lstate2 -∗
      ⌜lstate ۰ winner lstate1 = lstate ۰ winner lstate2 ⌝.
    #[local] Lemma lstates ｰ update {γ lstates} lstate :
      lstates ۰ auth γ lstates ⊢ |==>
        lstates ۰ auth γ (lstates ++ [lstate]) ∗
        lstates ۰ lb γ (length lstates) (lstate ۰ winner lstate) ∗
        lstates ۰ at γ (length lstates) lstate.
    Opaque lstates ۰ auth'.
    Opaque lstates ۰ at.
    Opaque lstates ۰ lb.

    #[local] Lemma producers ｰ alloc :
      ⊢ |==>
        ∃ γ_producers ,
        producers ۰ auth' γ_producers 0.
    #[local] Lemma producers ۰ at ｰ exclusive γ i own :
      producers ۰ at γ i Own -∗
      producers ۰ at γ i own -∗
      False.
    #[local] Lemma producers ۰ at ｰ discard γ i :
      producers ۰ at γ i Own ⊢ |==>
      producers ۰ at γ i Discard.
    #[local] Lemma producers ｰ update γ i :
      producers ۰ auth γ i ⊢ |==>
        producers ۰ auth γ ˖i ∗
        producers ۰ at γ i Own.
    Opaque producers ۰ auth'.
    Opaque producers ۰ at.

    #[local] Lemma consumers ｰ alloc :
      ⊢ |==>
        ∃ γ_consumers ,
        consumers ۰ auth' γ_consumers 0.
    #[local] Lemma consumers ۰ at ｰ exclusive γ i own :
      consumers ۰ at γ i Own -∗
      consumers ۰ at γ i own -∗
      False.
    #[local] Lemma consumers ۰ at ｰ discard γ i :
      consumers ۰ at γ i Own ⊢ |==>
      consumers ۰ at γ i Discard.
    #[local] Lemma consumers ۰ lb ｰ valid γ i j :
      consumers ۰ auth γ i -∗
      consumers ۰ lb γ j -∗
      ⌜j ≤ i ⌝.
    #[local] Lemma consumers ۰ lb ｰ le {γ i1} i2 :
      i2 ≤ i1 →
      consumers ۰ lb γ i1 ⊢
      consumers ۰ lb γ i2.
    #[local] Lemma consumers ۰ lb ｰ get γ i :
      consumers ۰ auth γ i ⊢
      consumers ۰ lb γ i.
    #[local] Lemma consumers ۰ lb ｰ get' {γ i} i' :
      i' ≤ i →
      consumers ۰ auth γ i ⊢
      consumers ۰ lb γ i'.
    #[local] Lemma consumers ｰ update γ i :
      consumers ۰ auth γ i ⊢ |==>
        consumers ۰ auth γ ˖i ∗
        consumers ۰ at γ i Own.
    Opaque consumers ۰ auth'.
    Opaque consumers ۰ at.
    Opaque consumers ۰ lb.

    #[local] Lemma winner ｰ exclusive γ i :
      winner γ i -∗
      winner γ i -∗
      False.

    #[local] Lemma inv ۰ slot ｰ not ｰ nothing ｰ past {γ i slot past1} past2 :
      slot ≠ Nothing →
      inv ۰ slot γ i slot past1 ⊣⊢
      inv ۰ slot γ i slot past2.

    Lemma inf_queue_mpmc_2 ۰ model ｰ exclusive γ vs1 vs2 :
      inf_queue_mpmc_2 ۰ model γ vs1 -∗
      inf_queue_mpmc_2 ۰ model γ vs2 -∗
      False.

    Lemma inf_queue_mpmc_2 ٠ create ｰ spec ι :
      {{{
        True
      }}}
        inf_queue_mpmc_2 ٠ create ()
      {{{
        t γ
      , RET #t ;
        meta_token t ⊤ ∗
        inf_queue_mpmc_2 ۰ inv t γ ι ∗
        inf_queue_mpmc_2 ۰ model γ []
      }}}.

    Lemma inf_queue_mpmc_2 ٠ size ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_2 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_2 ۰ model γ vs
      >>>
        inf_queue_mpmc_2 ٠ size #t @ ↑ι
      <<<
        inf_queue_mpmc_2 ۰ model γ vs
      | sz ,
        RET #sz ;
        ⌜length vs ≤ sz ⌝
      >>>.

    Lemma inf_queue_mpmc_2 ٠ is_empty ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_2 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_2 ۰ model γ vs
      >>>
        inf_queue_mpmc_2 ٠ is_empty #t @ ↑ι
      <<<
        inf_queue_mpmc_2 ۰ model γ vs
      | b ,
        RET #b ;
        ⌜if b then vs = [] else True ⌝
      >>>.

    Lemma inf_queue_mpmc_2 ٠ push ｰ spec t γ ι v :
      <<<
        inf_queue_mpmc_2 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_2 ۰ model γ vs
      >>>
        inf_queue_mpmc_2 ٠ push #t v @ ↑ι
      <<<
        inf_queue_mpmc_2 ۰ model γ (vs ++ [v])
      | RET ();
        True
      >>>.

    Lemma inf_queue_mpmc_2 ٠ pop ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_2 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_2 ۰ model γ vs
      >>>
        inf_queue_mpmc_2 ٠ pop #t @ ↑ι
      <<<
        ∃∃ v vs',
        ⌜vs = v :: vs'⌝ ∗
        inf_queue_mpmc_2 ۰ model γ vs'
      | RET v ;
        True
      >>>.
  End inf_queue_mpmc_2 ۰ G.

  #[global] Opaque inf_queue_mpmc_2 ۰ inv.
  #[global] Opaque inf_queue_mpmc_2 ۰ model.
End base.

Require zoo_saturn.inf_queue_mpmc_2__opaque.

Section inf_queue_mpmc_2 ۰ G.
  Context `{inf_queue_mpmc_2 ۰ G : InfQueueMpmc2G Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.

  Definition inf_queue_mpmc_2 ۰ inv t ι : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    base.inf_queue_mpmc_2 ۰ inv 𝑡 γ ι.
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".

  Definition inf_queue_mpmc_2 ۰ model t vs : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    base.inf_queue_mpmc_2 ۰ model γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".

  #[global] Instance inf_queue_mpmc_2 ۰ model ｰ timeless t vs :
    Timeless (inf_queue_mpmc_2 ۰ model t vs).

  #[global] Instance inf_queue_mpmc_2 ۰ inv ｰ persistent t ι :
    Persistent (inf_queue_mpmc_2 ۰ inv t ι).

  Lemma inf_queue_mpmc_2 ۰ model ｰ exclusive t vs1 vs2 :
    inf_queue_mpmc_2 ۰ model t vs1 -∗
    inf_queue_mpmc_2 ۰ model t vs2 -∗
    False.

  Lemma inf_queue_mpmc_2 ٠ create ｰ spec ι :
    {{{
      True
    }}}
      inf_queue_mpmc_2 ٠ create ()
    {{{
      t
    , RET t ;
      inf_queue_mpmc_2 ۰ inv t ι ∗
      inf_queue_mpmc_2 ۰ model t []
    }}}.

  Lemma inf_queue_mpmc_2 ٠ size ｰ spec t ι :
    <<<
      inf_queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_2 ۰ model t vs
    >>>
      inf_queue_mpmc_2 ٠ size t @ ↑ι
    <<<
      inf_queue_mpmc_2 ۰ model t vs
    | sz ,
      RET #sz ;
      ⌜length vs ≤ sz ⌝
    >>>.

  Lemma inf_queue_mpmc_2 ٠ is_empty ｰ spec t ι :
    <<<
      inf_queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_2 ۰ model t vs
    >>>
      inf_queue_mpmc_2 ٠ is_empty t @ ↑ι
    <<<
      inf_queue_mpmc_2 ۰ model t vs
    | b ,
      RET #b ;
      ⌜if b then vs = [] else True ⌝
    >>>.

  Lemma inf_queue_mpmc_2 ٠ push ｰ spec t ι v :
    <<<
      inf_queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_2 ۰ model t vs
    >>>
      inf_queue_mpmc_2 ٠ push t v @ ↑ι
    <<<
      inf_queue_mpmc_2 ۰ model t (vs ++ [v])
    | RET ();
      True
    >>>.

  Lemma inf_queue_mpmc_2 ٠ pop ｰ spec t ι :
    <<<
      inf_queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_2 ۰ model t vs
    >>>
      inf_queue_mpmc_2 ٠ pop t @ ↑ι
    <<<
      ∃∃ v vs',
      ⌜vs = v :: vs'⌝ ∗
      inf_queue_mpmc_2 ۰ model t vs'
    | RET v ;
      True
    >>>.
End inf_queue_mpmc_2 ۰ G.

#[global] Opaque inf_queue_mpmc_2 ۰ inv.
#[global] Opaque inf_queue_mpmc_2 ۰ model.