Library zoo_saturn.queue_mpmc_2

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.relations.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_bool.
Require Import zoo_std.option.
Require Export zoo_saturn.queue_mpmc_2__code.
Require Import zoo_saturn.queue_mpmc_2__types.
Require Import zoo.options.

Implicit Type strong : bool.
Implicit Type l back back_prev : location.
Implicit Type backs : gmap location nat.
Implicit Type v w t pref suff 𝑚𝑜𝑣𝑒 : val.
Implicit Type o : option val.
Implicit Type vs vs_front vs_back move : list val.

Variant emptiness :=
  | Empty
  | Nonempty.
Implicit Type empty : emptiness.

#[local] Instance emptiness ｰ inhabited : Inhabited emptiness :=
  populate Empty.
#[local] Instance emptiness ｰ eq_dec : EqDecision emptiness :=
  ltac:(solve_decision).

Variant status :=
  | Stable empty
  | Unstable back move.
Implicit Type status : status.

#[local] Instance status ｰ inhabited : Inhabited status :=
  populate (Stable inhabitant).
#[local] Instance status ｰ eq_dec : EqDecision status :=
  ltac:(solve_decision).

Record state :=
  { state ۰ backs : gmap location nat
  ; state ۰ index : nat
  ; state ۰ status : status
  }.
Implicit Type state : state.

#[local] Definition state ۰ with_status state status :=
  {|state ۰ backs := state.(state ۰ backs)
  ; state ۰ index := state.(state ۰ index)
  ; state ۰ status := status
  |}.

Definition state ۰ wf backs i :=
  map_Forall (λ _ i_back, i_back ≤ i) backs.

#[local] Definition state ۰ le state1 state2 :=
  state1.(state ۰ backs) ⊆ state2.(state ۰ backs) ∧
  state1.(state ۰ index) ≤ state2.(state ۰ index).

#[local] Instance state ｰ inhabited : Inhabited state :=
  populate
    {|state ۰ backs := inhabitant
    ; state ۰ index := inhabitant
    ; state ۰ status := inhabitant
    |}.

#[local] Instance state ۰ le ｰ reflexive :
  Reflexive state ۰ le.
#[local] Instance state ۰ le ｰ transitive :
  Transitive state ۰ le.

Variant step : relation state :=
  | step ｰ empty state1 state2 :
      state1.(state ۰ status) = Stable Nonempty →
      state2 = state ۰ with_status state1 (Stable Empty) →
      step state1 state2
  | step ｰ destabilize state1 state2 back move :
      state1.(state ۰ status) = Stable Empty →
      state2 = state ۰ with_status state1 (Unstable back move) →
      step state1 state2
  | step ｰ stabilize state1 state2 back move :
      state1.(state ۰ status) = Unstable back move →
      state1.(state ۰ backs) !! back = None →
      state2 =
        {|state ۰ backs := <[back := state1.(state ۰ index) + length move ]> state1 .(state ۰ backs )
        ; state ۰ index := state1.(state ۰ index) + length move
        ; state ۰ status := Stable Nonempty
        |} →
      step state1 state2.
#[local] Hint Constructors step : core.

#[local] Definition steps :=
  rtc step.

#[local] Lemma step ｰ mono state1 state2 :
  step state1 state2 →
  state ۰ le state1 state2.
#[local] Lemma steps ｰ mono state1 state2 :
  steps state1 state2 →
  state ۰ le state1 state2.

Class QueueMpmc2G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] queue_mpmc_2 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (list val))
  ; #[local] queue_mpmc_2 ۰ G ۰ state ۰ G :: AuthMonoG (A := leibnizO state) Σ step
  ; #[local] queue_mpmc_2 ۰ G ۰ front ۰ G :: AuthNatMaxG Σ
  }.

Definition queue_mpmc_2 ۰ Σ :=
  #[twins ۰ Σ (leibnizO (list val))
  ; auth_mono ۰ Σ (A := leibnizO state) step
  ; auth_nat_max ۰ Σ
  ].
#[global] Instance subG ｰ queue_mpmc_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG queue_mpmc_2 ۰ Σ Σ →
  QueueMpmc2G Σ.

#[local] Fixpoint suffix ۰ to_val (i : nat) vs : val :=
  match vs with
  | [] ⇒
      ‘Front [ #i ]
  | v :: vs ⇒
      ‘Cons [ #i , v, suffix ۰ to_val ˖i vs ]
  end.

#[local] Lemma suffix ۰ to_val ｰ generative i1 vs1 i2 vs2 :
  suffix ۰ to_val i1 vs1 ≈ suffix ۰ to_val i2 vs2 →
  suffix ۰ to_val i1 vs1 = suffix ۰ to_val i2 vs2.

#[local] Instance suffix ۰ to_val ｰ inj2 :
  Inj2 (=) (=) (=) suffix ۰ to_val.
#[local] Instance suffix ۰ to_val ｰ inj2' :
  Inj2 (=) (=) (≈) suffix ۰ to_val.

#[local] Fixpoint prefix ۰ to_val (i : nat) back vs : val :=
  match vs with
  | [] ⇒
      #back
  | v :: vs ⇒
      ‘Snoc [ #⁺(i + ˖(length vs )), v, prefix ۰ to_val i back vs ]
  end.

#[local] Lemma prefix ۰ to_val ｰ generative i1 back1 vs1 i2 back2 vs2 :
  prefix ۰ to_val i1 back1 vs1 ≈ prefix ۰ to_val i2 back2 vs2 →
  prefix ۰ to_val i1 back1 vs1 = prefix ۰ to_val i2 back2 vs2.

#[local] Lemma prefix ۰ to_val ｰ inj i1 back1 vs1 i2 back2 vs2 :
  prefix ۰ to_val i1 back1 vs1 = prefix ۰ to_val i2 back2 vs2 →
    (vs1 ≠ [] → i1 = i2) ∧
    back1 = back2 ∧
    vs1 = vs2.
#[local] Lemma prefix ۰ to_val ｰ inj' i1 back1 vs1 i2 back2 vs2 :
  prefix ۰ to_val i1 back1 vs1 ≈ prefix ۰ to_val i2 back2 vs2 →
    (vs1 ≠ [] → i1 = i2) ∧
    back1 = back2 ∧
    vs1 = vs2.

Section queue_mpmc_2 ۰ G.
  Context `{queue_mpmc_2 ۰ G : QueueMpmc2G Σ}.

  Record metadata :=
    { metadata ۰ inv : namespace
    ; metadata ۰ model : gname
    ; metadata ۰ state : gname
    ; metadata ۰ front : gname
    }.
  Implicit Type γ : metadata.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

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

  #[local] Definition state ۰ auth' γ_state backs i status : iProp Σ :=
    auth_mono ۰ auth _ γ_state (DfracOwn 1)
      {|state ۰ backs := backs
      ; state ۰ index := i
      ; state ۰ status := status
      |} ∗
    ⌜state ۰ wf backs i ⌝.
  #[local] Instance : CustomIpat "state۰auth" :=
    " ( Hauth & %Hwf ) ".
  #[local] Definition state ۰ auth γ backs i status :=
    state ۰ auth' γ.(metadata ۰ state) backs i status.
  #[local] Definition state ۰ lb γ backs i status :=
    auth_mono ۰ lb _ γ.(metadata ۰ state)
      {|state ۰ backs := backs
      ; state ۰ index := i
      ; state ۰ status := status
      |}.
  #[local] Definition state ۰ seen γ back i_prev back_prev move : iProp Σ :=
    ∃ backs ,
    state ۰ lb γ backs i_prev (Unstable back move) ∗
    ⌜backs !! back_prev = Some i_prev ⌝.
  #[local] Instance : CustomIpat "state۰seen" :=
    " ( %backs{} & #Hstate_lb & %Hbacks{}_lookup ) ".
  #[local] Definition state ۰ at γ back i_back : iProp Σ :=
    ∃ backs i status ,
    state ۰ lb γ backs i status ∗
    ⌜backs !! back = Some i_back ⌝ ∗
    ⌜i_back ≤ i ⌝.
  #[local] Instance : CustomIpat "state۰at" :=
    " ( %backs{} & %i{} & %status{} & #Hstate_lb{_{}} & %Hbacks{}_lookup & %Hi{} ) ".

  #[local] Definition front ۰ auth' γ_front i :=
    auth_nat_max ۰ auth γ_front (DfracOwn 1) i.
  #[local] Definition front ۰ auth γ i :=
    front ۰ auth' γ.(metadata ۰ front) i.
  #[local] Definition front ۰ lb γ i :=
    auth_nat_max ۰ lb γ.(metadata ۰ front) i.

  #[local] Definition move ۰ model₁ 𝑚𝑜𝑣𝑒 i_prev back_prev move : iProp Σ :=
      ⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
    ∨ ⌜𝑚𝑜𝑣𝑒 = prefix ۰ to_val i_prev back_prev move ⌝ ∗
      ⌜0 < length move ⌝ ∗
      back_prev ↦ₕ Header §Back 2.
  #[local] Instance : CustomIpat "move۰model₁" :=
    " [ -> | ( -> & % & #Hback{}_prev_header ) ] ".
  #[local] Definition move ۰ model₂ γ back 𝑚𝑜𝑣𝑒 : iProp Σ :=
    ∃ backs_prev i_prev back_prev move ,
    state ۰ lb γ backs_prev i_prev (Unstable back move) ∗
    move ۰ model₁ 𝑚𝑜𝑣𝑒 i_prev back_prev move.
  #[local] Instance : CustomIpat "move۰model₂" :=
    " ( %backs{}_prev & %i{}_prev{_{!}} & %back{}_prev{_{!}} & %move{}{_{!}} & #Hstate_lb_unstable{_{}} & H𝑚𝑜𝑣𝑒{} ) ".

  #[local] Definition back ۰ model₁ back (i : nat) : iProp Σ :=
    back ↦ₕ Header §Back 2 ∗
    back .[index ] ↦□ #i.
  #[local] Instance : CustomIpat "back۰model₁" :=
    " ( { {!} _ ; #Hback{}_header ; #Hback_header } & #Hback{}_index{_{!}} ) ".
  #[local] Definition back ۰ model₂ back (i : nat) 𝑚𝑜𝑣𝑒 : iProp Σ :=
    back ۰ model₁ back i ∗
    back .[move ] ↦ 𝑚𝑜𝑣𝑒.
  #[local] Instance : CustomIpat "back۰model₂" :=
    " ( { {only_move} _ ; (:back۰model₁ // /!/) } & Hback{}_move{_{suff}} ) ".
  #[local] Definition back ۰ model₃ γ back i : iProp Σ :=
    ∃ 𝑚𝑜𝑣𝑒 ,
    back ۰ model₂ back i 𝑚𝑜𝑣𝑒 ∗
    move ۰ model₂ γ back 𝑚𝑜𝑣𝑒.
  #[local] Instance : CustomIpat "back۰model₃" :=
    " ( %𝑚𝑜𝑣𝑒{} & (:back۰model₂) & H𝑚𝑜𝑣𝑒{} ) ".

  #[local] Definition inv ۰ status ۰ stable γ i vs_front i_back back vs_back vs empty : iProp Σ :=
    ⌜i_back = i ⌝ ∗
    ⌜vs = vs_front ++ reverse vs_back ⌝ ∗
    ⌜if empty then vs_front = [] else 0 < length vs_front ⌝ ∗
    state ۰ at γ back i_back.
  #[local] Instance : CustomIpat "inv۰status۰stable" :=
    " ( {>;}-> & {>;}%Hvs{} & {>;}{{empty}->;%Hempty{};%Hempty} & {>;}#Hstate_at{_{}} ) ".
  #[local] Definition inv ۰ status ۰ unstable strong γ backs i vs_front i_back back vs_back vs back_ move : iProp Σ :=
    ∃ back_prev ,
    ⌜back_ = back ⌝ ∗
    ⌜i_back = (i + length move)%nat⌝ ∗
    ⌜vs_front = []⌝ ∗
    ⌜vs_back = []⌝ ∗
    ⌜vs = reverse move ⌝ ∗
    ⌜0 < length move ⌝ ∗
    state ۰ at γ back_prev i ∗
    back ۰ model₂ back i_back (prefix ۰ to_val i back_prev move) ∗
    if strong then
      ⌜backs !! back = None ⌝ ∗
      back_prev ↦ₕ Header §Back 2
    else
      True.
  #[local] Instance : CustomIpat "inv۰status۰unstable" :=
    " ( %back{}_prev & {>;}-> & {>;}-> & {>;}{{lazy}%Hvs_front{};->} & {>;}{{lazy}%Hvs_back{};->} & {>;}-> & {>;}% & {>;}#Hstate_at_back{}_prev & Hback{} & { {strong} %Hbacks{}_lookup & #Hback{}_prev_header ; _ } ) ".
  #[local] Definition inv ۰ status strong γ backs i status vs_front i_back back vs_back vs : iProp Σ :=
    match status with
    | Stable empty ⇒
        inv ۰ status ۰ stable γ i vs_front i_back back vs_back vs empty
    | Unstable back_ move ⇒
        inv ۰ status ۰ unstable strong γ backs i vs_front i_back back vs_back vs back_ move
    end.

  #[local] Definition inv ۰ inner strong l γ : iProp Σ :=
    ∃ backs i status i_front vs_front i_back back vs_back vs ,
    l .[front ] ↦ suffix ۰ to_val i_front vs_front ∗
    front ۰ auth γ i_front ∗
    l .[back ] ↦ prefix ۰ to_val i_back back vs_back ∗
    ([∗ map ] back ↦ i ∈ backs , back ۰ model₃ γ back i ) ∗
    model₂ γ vs ∗
    state ۰ auth γ backs i status ∗
    ⌜(i_front + length vs_front)%nat = ˖i ⌝ ∗
    inv ۰ status strong γ backs i status vs_front i_back back vs_back vs.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %backs{} & %i{} & %status{} & %i_front{} & %vs_front{} & %i_back{} & %back{} & %vs_back{} & %vs{} & Hl_front & {>;}Hfront_auth & Hl_back & Hbacks & Hmodel₂ & {>;}Hstate_auth & {>;}%Hfront{} & Hstatus ) ".
  #[local] Definition inv' l γ : iProp Σ :=
    inv γ.(metadata ۰ inv) (inv ۰ inner false l γ).
  Definition queue_mpmc_2 ۰ inv t ι : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    ⌜ι = γ.(metadata ۰ inv)⌝ ∗
    l ↪ γ ∗
    inv' l γ.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & -> & #Hmeta & #Hinv ) ".

  Definition queue_mpmc_2 ۰ model t vs : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    model₁ γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".

  #[local] Instance state ۰ auth ｰ timeless γ backs i status :
    Timeless (state ۰ auth γ backs i status).
  #[local] Instance state ۰ at ｰ timeless γ back i_back :
    Timeless (state ۰ at γ back i_back).
  #[global] Instance queue_mpmc_2 ۰ model ｰ timeless t vs :
    Timeless (queue_mpmc_2 ۰ model t vs).

  #[local] Instance state ۰ at ｰ persistent γ back i_back :
    Persistent (state ۰ at γ back i_back).
  #[global] Instance queue_mpmc_2 ۰ inv ｰ persistent t ι :
    Persistent (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 state ｰ alloc back :
    ⊢ |==>
      ∃ γ_state ,
      state ۰ auth' γ_state ∅ 0 (Unstable back []).
  #[local] Lemma state ۰ auth ｰ wf γ backs i status :
    state ۰ auth γ backs i status ⊢
    ⌜state ۰ wf backs i ⌝.
  #[local] Lemma state ۰ lb ｰ get γ backs i status :
    state ۰ auth γ backs i status ⊢
    state ۰ lb γ backs i status.
  #[local] Lemma state ۰ at ｰ get {γ backs i status} back i_back :
    backs !! back = Some i_back →
    state ۰ auth γ backs i status ⊢
    state ۰ at γ back i_back.
  #[local] Lemma state ۰ lb ｰ valid γ backs1 i1 status1 backs2 i2 status2 :
    state ۰ auth γ backs1 i1 status1 -∗
    state ۰ lb γ backs2 i2 status2 -∗
      ⌜backs2 ⊆ backs1 ⌝ ∗
      ⌜i2 ≤ i1 ⌝.
  #[local] Lemma state ۰ lb ｰ valid ｰ Unstable γ backs1 i1 status1 backs2 i2 back2 move2 :
    state ۰ auth γ backs1 i1 status1 -∗
    state ۰ lb γ backs2 i2 (Unstable back2 move2) -∗
        ⌜backs1 = backs2 ⌝ ∗
        ⌜i1 = i2 ⌝ ∗
        ⌜status1 = Unstable back2 move2 ⌝
      ∨ ⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
        ⌜i2 + length move2 ≤ i1 ⌝ ∗
        state ۰ at γ back2 (i2 + length move2).
  #[local] Lemma state ۰ lb ｰ lookup {γ backs1 i1 status1 backs2 i2 status2} back i_back :
    backs2 !! back = Some i_back →
    state ۰ auth γ backs1 i1 status1 -∗
    state ۰ lb γ backs2 i2 status2 -∗
    ⌜backs1 !! back = Some i_back ⌝.
  #[local] Lemma state ۰ seen ｰ valid γ backs i status back i_prev back_prev move :
    state ۰ auth γ backs i status -∗
    state ۰ seen γ back i_prev back_prev move -∗
      ⌜backs !! back_prev = Some i_prev ⌝ ∗
      ( ⌜i = i_prev ⌝ ∗
        ⌜status = Unstable back move ⌝
      ∨ ⌜backs !! back = Some (i_prev + length move)%nat⌝ ∗
        ⌜i_prev + length move ≤ i ⌝ ∗
        state ۰ at γ back (i_prev + length move)
      ).
  #[local] Lemma state ۰ at ｰ valid γ backs i status back i_back :
    state ۰ auth γ backs i status -∗
    state ۰ at γ back i_back -∗
      ⌜backs !! back = Some i_back ⌝ ∗
      ⌜i_back ≤ i ⌝.
  #[local] Lemma state ۰ lb ｰ stabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
    ( status1 ≠ Unstable back2 move2
    ∨ i2 + length move2 ≤ i1 ∧
      0 < length move2
    ) →
    state ۰ auth γ backs1 i1 status1 -∗
    state ۰ lb γ backs2 i2 (Unstable back2 move2) -∗
      ⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
      state ۰ at γ back2 (i2 + length move2).
  #[local] Lemma state ۰ lb ｰ unstabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
    i1 < i2 + length move2 →
    state ۰ auth γ backs1 i1 status1 -∗
    state ۰ lb γ backs2 i2 (Unstable back2 move2) -∗
      ⌜backs1 = backs2 ⌝ ∗
      ⌜i1 = i2 ⌝ ∗
      ⌜status1 = Unstable back2 move2 ⌝.
  #[local] Lemma state ｰ stabilize γ backs i back move :
    backs !! back = None →
    state ۰ auth γ backs i (Unstable back move) ⊢ |==>
      state ۰ auth γ (<[back := i + length move ]> backs) (i + length move) (Stable Nonempty) ∗
      state ۰ lb γ (<[back := i + length move ]> backs) (i + length move) (Stable Nonempty) ∗
      state ۰ at γ back (i + length move).
  #[local] Lemma state ｰ empty γ backs i :
    state ۰ auth γ backs i (Stable Nonempty) ⊢ |==>
    state ۰ auth γ backs i (Stable Empty).
  #[local] Lemma state ｰ destabilize {γ backs i} back move :
    state ۰ auth γ backs i (Stable Empty) ⊢ |==>
    state ۰ auth γ backs i (Unstable back move).

  #[local] Lemma front ｰ alloc :
    ⊢ |==>
      ∃ γ_front ,
      front ۰ auth' γ_front 1.
  #[local] Lemma front ۰ lb ｰ get γ i :
    front ۰ auth γ i ⊢
    front ۰ lb γ i.
  #[local] Lemma front ۰ lb ｰ valid γ i1 i2 :
    front ۰ auth γ i1 -∗
    front ۰ lb γ i2 -∗
    ⌜i2 ≤ i1 ⌝.
  #[local] Lemma front ｰ update γ i :
    front ۰ auth γ i ⊢ |==>
    front ۰ auth γ ˖i.

  Opaque state ۰ auth.
  Opaque state ۰ at.

  #[local] Lemma inv ۰ status ｰ weaken γ backs i status vs_front i_back back vs_back vs :
    inv ۰ status true γ backs i status vs_front i_back back vs_back vs ⊢
    inv ۰ status false γ backs i status vs_front i_back back vs_back vs.
  #[local] Lemma inv ۰ status ｰ Stable strong γ backs i status vs_front i_back back vs_back vs :
    ( strong = true ∧ is_Some (backs !! back)
    ∨ 0 < length vs_front
    ∨ 0 < length vs_back
    ) →
    inv ۰ status strong γ backs i status vs_front i_back back vs_back vs ⊢
      ∃ empty ,
      ⌜status = Stable empty ⌝ ∗
      inv ۰ status ۰ stable γ i vs_front i_back back vs_back vs empty.

  #[local] Lemma inv ۰ inner ｰ strengthen l γ :
    inv ۰ inner false l γ ⊢
    inv ۰ inner true l γ.

  #[local] Lemma inv'ｰ state ۰ at {l γ} back i_back :
    inv' l γ -∗
    state ۰ at γ back i_back ={⊤}=∗
    back ۰ model₁ back i_back.

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

  #[local] Lemma queue_mpmc_2 ٠ suffix_index ｰ spec (i : nat) vs :
    {{{
      True
    }}}
      queue_mpmc_2 ٠ suffix_index (suffix ۰ to_val i vs)
    {{{
      RET #i ;
      True
    }}}.

  #[local] Lemma queue_mpmc_2 ٠ prefix_index ｰ spec (i : nat) back vs :
    {{{
      back ↦ₕ Header §Back 2 ∗
      back .[index ] ↦□ #i
    }}}
      queue_mpmc_2 ٠ prefix_index (prefix ۰ to_val i back vs)
    {{{
      RET #⁺(i + length vs );
      True
    }}}.

  #[local] Lemma queue_mpmc_2 ٠ rev₁ ｰ spec i vs1 vs2 back :
    0 < length vs1 →
    {{{
      back ↦ₕ Header §Back 2
    }}}
      queue_mpmc_2 ٠ rev₁ (suffix ۰ to_val (i + ˖(length vs2 )) vs1) (prefix ۰ to_val i back vs2)
    {{{
      RET suffix ۰ to_val ˖i (reverse vs2 ++ vs1);
      True
    }}}.
  #[local] Lemma queue_mpmc_2 ٠ rev ｰ spec i back vs :
    0 < length vs →
    {{{
      back ↦ₕ Header §Back 2
    }}}
      queue_mpmc_2 ٠ rev (prefix ۰ to_val i back vs)
    {{{
      RET suffix ۰ to_val ˖i (reverse vs);
      True
    }}}.

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

  #[local] Lemma front ｰ spec_strong {l γ} i_front i_back :
    {{{
      inv' l γ ∗
      match i_front with
      | None ⇒
          True
      | Some i_front ⇒
          front ۰ lb γ i_front
      end ∗
      match i_back with
      | None ⇒
          True
      | Some i_back ⇒
          ∃ back ,
          state ۰ at γ back i_back
      end
    }}}
      (#l ).{front }
    {{{
      i_front' vs_front'
    , RET suffix ۰ to_val i_front' vs_front';
      front ۰ lb γ i_front' ∗
      match i_front with
      | None ⇒
          True
      | Some i_front ⇒
          ⌜i_front ≤ i_front'⌝
      end ∗
      match i_back with
      | None ⇒
          True
      | Some i_back ⇒
          ∃ i',
          ⌜i_back ≤ i'⌝ ∗
          ⌜(i_front' + length vs_front')%nat = ˖i'⌝
      end
    }}}.
  #[local] Lemma front ｰ spec l γ :
    {{{
      inv' l γ
    }}}
      (#l ).{front }
    {{{
      i_front' vs_front'
    , RET suffix ۰ to_val i_front' vs_front';
      front ۰ lb γ i_front'
    }}}.

  #[local] Lemma move ｰ spec l γ backs back i move :
    {{{
      inv' l γ ∗
      state ۰ lb γ backs i (Unstable back move)
    }}}
      (#back ).{move }
    {{{
      𝑚𝑜𝑣𝑒
    , RET 𝑚𝑜𝑣𝑒 ;
        ⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
      ∨ ∃ backs i back_prev move ,
        ⌜𝑚𝑜𝑣𝑒 = prefix ۰ to_val i back_prev move ⌝ ∗
        ⌜0 < length move ⌝ ∗
        state ۰ lb γ backs i (Unstable back move)
    }}}.

  Lemma queue_mpmc_2 ٠ size ｰ spec t ι :
    <<<
      queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpmc_2 ۰ model t vs
    >>>
      queue_mpmc_2 ٠ size t @ ↑ι
    <<<
      queue_mpmc_2 ۰ model t vs
    | RET #(length vs );
      True
    >>>.

  Lemma queue_mpmc_2 ٠ is_empty ｰ spec t ι :
    <<<
      queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpmc_2 ۰ model t vs
    >>>
      queue_mpmc_2 ٠ is_empty t @ ↑ι
    <<<
      queue_mpmc_2 ۰ model t vs
    | RET #(bool_decide (vs = []%list));
      True
    >>>.

  #[local] Lemma queue_mpmc_2 ٠ finish ｰ spec {l γ} i_back back :
    {{{
      inv' l γ ∗
      state ۰ at γ back i_back
    }}}
      queue_mpmc_2 ٠ finish #back
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma queue_mpmc_2 ٠ help ｰ spec {l γ backs i back_prev back} move :
    0 < length move →
    {{{
      inv' l γ ∗
      state ۰ lb γ backs i (Unstable back move) ∗
      back_prev ↦ₕ Header §Back 2
    }}}
      queue_mpmc_2 ٠ help #l #back #⁺(i + length move ) (prefix ۰ to_val i back_prev move)
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma queue_mpmc_2 ٠ push ｰ spec ｰ aux l γ v :
    ⊢ (
      ∀ back i ws (j : Z ),
      <<<
        ⌜j = ⁺(i + length ws )⌝ ∗
        inv' l γ ∗
        state ۰ at γ back i
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ push_aux #l v #j (prefix ۰ to_val i back ws) @ ↑γ.(metadata ۰ inv)
      <<<
        model₁ γ (vs ++ [v])
      | RET ();
        True
      >>>
    ) ∧ (
      <<<
        inv' l γ
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ push #l v @ ↑γ.(metadata ۰ inv)
      <<<
        model₁ γ (vs ++ [v])
      | RET ();
        True
      >>>
    ).
  Lemma queue_mpmc_2 ٠ push ｰ spec t v ι :
    <<<
      queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpmc_2 ۰ model t vs
    >>>
      queue_mpmc_2 ٠ push t v @ ↑ι
    <<<
      queue_mpmc_2 ۰ model t (vs ++ [v])
    | RET ();
      True
    >>>.

  #[local] Lemma queue_mpmc_2 ٠ pop ｰ spec ｰ aux l γ :
    ⊢ (
      ∀ i_front vs_front ,
      <<<
        inv' l γ ∗
        front ۰ lb γ i_front
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ pop_1 #l (suffix ۰ to_val i_front vs_front) @ ↑γ.(metadata ۰ inv)
      <<<
        ∃∃ o ,
        match o with
        | None ⇒
            model₁ γ vs
        | Some v ⇒
            ∃ vs',
            ⌜vs = v :: vs'⌝ ∗
            model₁ γ vs'
        end
      | RET o ;
        True
      >>>
    ) ∧ (
      ∀ (i_front : nat) backs back i back_prev move ,
      <<<
        ⌜i_front ≤ ˖i ⌝ ∗
        ⌜1 < length move ⌝ ∗
        inv' l γ ∗
        state ۰ lb γ backs i (Unstable back move) ∗
        back_prev ↦ₕ Header §Back 2
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ pop_2 #l ’Front [ #i_front ] #back (prefix ۰ to_val i back_prev move) @ ↑γ.(metadata ۰ inv)
      <<<
        ∃∃ o ,
        match o with
        | None ⇒
            model₁ γ vs
        | Some v ⇒
            ∃ vs',
            ⌜vs = v :: vs'⌝ ∗
            model₁ γ vs'
        end
      | RET o ;
        True
      >>>
    ) ∧ (
      ∀ i_front ,
      <<<
        inv' l γ
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ pop_3 #l ’Front [ #i_front ] @ ↑γ.(metadata ۰ inv)
      <<<
        ∃∃ o ,
        match o with
        | None ⇒
            model₁ γ vs
        | Some v ⇒
            ∃ vs',
            ⌜vs = v :: vs'⌝ ∗
            model₁ γ vs'
        end
      | RET o ;
        True
      >>>
    ) ∧ (
      <<<
        inv' l γ
      | ∀∀ vs ,
        model₁ γ vs
      >>>
        queue_mpmc_2 ٠ pop #l @ ↑γ.(metadata ۰ inv)
      <<<
        ∃∃ o ,
        match o with
        | None ⇒
            model₁ γ vs
        | Some v ⇒
            ∃ vs',
            ⌜vs = v :: vs'⌝ ∗
            model₁ γ vs'
        end
      | RET o ;
        True
      >>>
    ).
  Lemma queue_mpmc_2 ٠ pop ｰ spec t ι :
    <<<
      queue_mpmc_2 ۰ inv t ι
    | ∀∀ vs ,
      queue_mpmc_2 ۰ model t vs
    >>>
      queue_mpmc_2 ٠ pop t @ ↑ι
    <<<
      ∃∃ o ,
      match o with
      | None ⇒
          queue_mpmc_2 ۰ model t vs
      | Some v ⇒
          ∃ vs',
          ⌜vs = v :: vs'⌝ ∗
          queue_mpmc_2 ۰ model t vs'
      end
    | RET o ;
      True
    >>>.
End queue_mpmc_2 ۰ G.

Require zoo_saturn.queue_mpmc_2__opaque.

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