Library zoo_saturn.bag_2

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.fin_maps.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.mono_gmap.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Import zoo_std.xtchain.
Require Export zoo_saturn.bag_2__code.
Require Import zoo_saturn.bag_2__types.
Require Import zoo.options.

Implicit Type l node 𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟 : location.
Implicit Type nodes : list location.
Implicit Type v t producer consumer : val.
Implicit Type o : option val.
Implicit Type vs ws : list val.
Implicit Type vss wss : gmap val (list val).

Class Bag2G Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] bag_2۰G۰queue_spmc۰G :: QueueSpmcG Σ
  ; #[local] bag_2۰G۰queues۰G :: MonoGmapG Σ location val
  ; #[local] bag_2۰G۰model۰G :: TwinsG Σ (leibnizO (gmap val (list val)))
  }.

Definition bag_2۰Σ :=
  #[queue_spmc۰Σ
  ; mono_gmap۰Σ location val
  ; twins۰Σ (leibnizO (gmap val (list val)))
  ].
#[global] Instance subGｰbag_2۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG bag_2۰Σ Σ →
  Bag2G Σ.

Record producer :=
  { producer۰queue : val
  ; producer۰node : location
  }.
Implicit Type 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : producer.

#[local] Coercion producer۰to_val 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : val :=
  ( 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue),
    #𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node)
  ).

#[local] Lemma producerｰeqｰalt 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟1 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟2 :
  𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟1.(producer۰queue) = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟2.(producer۰queue) →
  𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟1.(producer۰node) = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟2.(producer۰node) →
  𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟1 = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟2.
#[local] Instance producer۰to_valｰinj :
  Inj (=) (=) producer۰to_val.

Record descriptor :=
  { descriptor۰queue : val
  ; descriptor۰vals : list val
  }.
Implicit Type descr : descriptor.
Implicit Type descrs : gmap location descriptor.

#[local] Definition descriptor۰update_vals descr f :=
  {|descriptor۰queue := descr.(descriptor۰queue)
  ; descriptor۰vals := f descr.(descriptor۰vals)
  |}.

#[local] Definition descriptor۰to_producer descr node :=
  {|producer۰queue := descr.(descriptor۰queue)
  ; producer۰node := node
  |}.

#[local] Lemma descriptor۰to_producerｰinj descr1 node1 descr2 node2 :
  descriptor۰to_producer descr1 node1 = descriptor۰to_producer descr2 node2 →
  node1 = node2.

Section bag_2۰G.
  Context `{bag_2۰G : Bag2G Σ}.

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

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

  #[local] Definition queues۰auth' γ_queues nodes descrs wss : iProp Σ :=
    mono_gmap۰auth γ_queues (DfracOwn 1) (descriptor۰queue <$> descrs) ∗
    ⌜dom descrs = list_to_set nodes⌝ ∗
    ⌜ map_Forall (λ node descr,
        wss !! (descriptor۰to_producer descr node : val) = Some descr.(descriptor۰vals)
      ) descrs
    ⌝.
  #[local] Instance : CustomIpat "queues۰auth" :=
    " ( Hauth & %Hnodes & %Hdescrs ) ".
  #[local] Definition queues۰auth γ :=
    queues۰auth' γ.(metadata۰queues).
  #[local] Definition queues۰at' :=
    mono_gmap۰at.
  #[local] Definition queues۰at γ :=
    queues۰at' γ.(metadata۰queues).
  #[local] Definition queues۰elem γ queue : iProp Σ :=
    match queue with
    | None ⇒
        True
    | Some queue ⇒
        ∃ node,
        queues۰at γ node queue ∗
        queue_spmc۰inv queue (γ.(metadata۰inv).@"producer")
    end.
  #[local] Instance : CustomIpat "queues۰elem" :=
    " ( %node & #Hqueues_at & #Hqueue_inv ) ".

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

  #[local] Definition descriptor۰model γ node descr : iProp Σ :=
    ∃ o,
    node.[queue] ↦ o ∗
    ⌜from_option (.= descr.(descriptor۰queue)) True o⌝ ∗
    queue_spmc۰inv descr.(descriptor۰queue) (γ.(metadata۰inv).@"producer") ∗
    queue_spmc۰model descr.(descriptor۰queue) descr.(descriptor۰vals).
  #[local] Instance : CustomIpat "descriptor۰model" :=
    " ( %o{} & Hnode{}_queue & {>;}%Ho{} & {{inv}#Hqueue{}_inv;{inv}#Hqueue_inv;_} & {>;}Hqueue{}_model ) ".

  #[local] Definition inv۰inner l γ : iProp Σ :=
    ∃ nodes descrs wss,
    l.[producers] ↦ from_option #@{location} §Null (head nodes) ∗
    xtchain (Header §Node 2) DfracDiscarded nodes §Null ∗
    queues۰auth γ nodes descrs wss ∗
    model₂ γ wss ∗
    [∗ map] node ↦ descr ∈ descrs,
      descriptor۰model γ node descr.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %nodes{} & %descrs{} & %wss & Hl_producers & Hnodes{} & >Hqueues_auth & >Hmodel₂ & Hdescrs ) ".
  #[local] Definition inv' l γ :=
    inv (γ.(metadata۰inv).@"inv") (inv۰inner l γ).
  Definition bag_2۰inv t ι : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    ⌜ι = γ.(metadata۰inv)⌝ ∗
    l ↪ γ ∗
    inv' l γ.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & -> & #Hmeta & #Hinv ) ".

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

  Definition bag_2۰producer t producer ws : iProp Σ :=
    ∃ l γ 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟,
    ⌜t = #l⌝ ∗
    ⌜producer = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟⌝ ∗
    l ↪ γ ∗
    𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) ↦ₕ Header §Node 2 ∗
    queues۰at γ 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue) ∗
    queue_spmc۰inv 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue) (γ.(metadata۰inv).@"producer") ∗
    queue_spmc۰producer 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue) ws.
  #[local] Instance : CustomIpat "producer" :=
    " ( %l{;_} & %γ{;_} & %𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟{} & %Ht_eq{} & {%Hproducer_eq{};->} & #Hmeta{_{};_} & #Hnode_header{_{}} & #Hqueues_at{_{}} & #Hqueue_inv{_{}} & Hqueue_producer{_{}} ) ".

  Definition bag_2۰consumer t consumer : iProp Σ :=
    ∃ l γ 𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟 (queue : option val),
    ⌜t = #l⌝ ∗
    l ↪ γ ∗
    ⌜consumer = #𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟⌝ ∗
    𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟.[consumer_queue] ↦ queue ∗
    queues۰elem γ queue.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l{;_} & %γ{;_} & %𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟{} & %queue{} & %Heq{} & Hmeta_{} & {%Hconsumer_eq{};->} & Hconsumer_queue{_{}} & #Hqueues_elem{_{}} ) ".

  #[local] Instance queues۰authｰtimeless γ nodes descrs wss :
    Timeless (queues۰auth γ nodes descrs wss).
  #[global] Instance bag_2۰modelｰtimeless t vss :
    Timeless (bag_2۰model t vss).

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

  #[local] Lemma queuesｰalloc :
    ⊢ |==>
      ∃ γ_queues,
      queues۰auth' γ_queues [] ∅ ∅.
  #[local] Lemma queues۰atｰget {γ nodes descrs wss} i node :
    nodes !! i = Some node →
    queues۰auth γ nodes descrs wss ⊢
      ∃ descr,
      ⌜descrs !! node = Some descr⌝ ∗
      queues۰at γ node descr.(descriptor۰queue).
  #[local] Lemma queues۰atｰvalid γ nodes descrs wss node queue :
    queues۰auth γ nodes descrs wss -∗
    queues۰at γ node queue -∗
      ∃ descr,
      ⌜descrs !! node = Some descr⌝ ∗
      ⌜descr.(descriptor۰queue) = queue⌝ ∗
      ⌜wss !! (descriptor۰to_producer descr node : val) = Some descr.(descriptor۰vals)⌝.
  #[local] Lemma queues۰atｰvalidｰproducer γ nodes descrs wss 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 :
    queues۰auth γ nodes descrs wss -∗
    queues۰at γ 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue) -∗
      ∃ descr,
      ⌜descrs !! 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) = Some descr⌝ ∗
      ⌜descr.(descriptor۰queue) = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue)⌝ ∗
      ⌜wss !! (𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : val) = Some descr.(descriptor۰vals)⌝.
  #[local] Lemma queuesｰinsert {γ nodes descrs wss} node descr :
    descrs !! node = None →
    queues۰auth γ nodes descrs wss ⊢ |==>
      queues۰auth γ
        (node :: nodes)
        (<[node := descr]> descrs)
        (<[descriptor۰to_producer descr node : val := descr.(descriptor۰vals)]> wss) ∗
      queues۰at γ node descr.(descriptor۰queue).
  #[local] Lemma queuesｰupdate {γ nodes descrs wss} node descr f :
    descrs !! node = Some descr →
    queues۰auth γ nodes descrs wss ⊢
    queues۰auth γ
      nodes
      (<[node := descriptor۰update_vals descr f]> descrs)
      (<[descriptor۰to_producer descr node : val := f descr.(descriptor۰vals)]> wss).
  #[local] Lemma queuesｰupdateｰproducer {γ nodes descrs wss} 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 descr f :
    descrs !! 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) = Some descr →
    descr.(descriptor۰queue) = 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰queue) →
    queues۰auth γ nodes descrs wss ⊢
    queues۰auth γ
      nodes
      (<[𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟.(producer۰node) := descriptor۰update_vals descr f]> descrs)
      (<[𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : val := f descr.(descriptor۰vals)]> wss).

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

  Opaque queues۰auth'.

  Lemma bag_2۰modelｰexclusive t vss1 vss2 :
    bag_2۰model t vss1 -∗
    bag_2۰model t vss2 -∗
    False.

  Lemma bag_2۰producerｰvalid t ι vss producer ws E :
    ↑ι ⊆ E →
    bag_2۰inv t ι -∗
    bag_2۰model t vss -∗
    bag_2۰producer t producer ws ={E}=∗
      ∃ vs,
      ⌜vss !! producer = Some vs⌝ ∗
      ⌜vs `suffix_of` ws⌝.
  Lemma bag_2۰producerｰexclusive t1 t2 producer ws1 ws2 :
    bag_2۰producer t1 producer ws1 -∗
    bag_2۰producer t2 producer ws2 -∗
    False.

  Lemma bag_2۰consumerｰexclusive t1 t2 consumer :
    bag_2۰consumer t1 consumer -∗
    bag_2۰consumer t2 consumer -∗
    False.

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

  #[local] Lemma bag_2٠add_producer₁ｰspec l γ (queue : val) :
    <<<
      l ↪ γ ∗
      inv' l γ ∗
      queue_spmc۰inv queue (γ.(metadata۰inv).@"producer") ∗
      queue_spmc۰model queue []
    | ∀∀ vss,
      model₁ γ vss
    >>>
      bag_2٠add_producer₁ #l (Some queue) @ ↑γ.(metadata۰inv)
    <<<
      ∃∃ node,
      let 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 :=
        {|producer۰queue := queue
        ; producer۰node := node
        |}
      in
      model₁ γ (<[𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : val := []]> vss)
    | RET #node;
      node ↦ₕ Header §Node 2 ∗
      queues۰at γ node queue
    >>>.
  #[local] Lemma bag_2٠add_producerｰspec l γ (queue : val) :
    <<<
      l ↪ γ ∗
      inv' l γ ∗
      queue_spmc۰inv queue (γ.(metadata۰inv).@"producer") ∗
      queue_spmc۰model queue []
    | ∀∀ vss,
      model₁ γ vss
    >>>
      bag_2٠add_producer #l queue @ ↑γ.(metadata۰inv)
    <<<
      ∃∃ node,
      let 𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 :=
        {|producer۰queue := queue
        ; producer۰node := node
        |}
      in
      model₁ γ (<[𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑟 : val := []]> vss)
    | RET #node;
      node ↦ₕ Header §Node 2 ∗
      queues۰at γ node queue
    >>>.
  Lemma bag_2٠create_producerｰspec t ι :
    <<<
      bag_2۰inv t ι
    | ∀∀ vss,
      bag_2۰model t vss
    >>>
      bag_2٠create_producer t @ ↑ι
    <<<
      ∃∃ producer,
      bag_2۰model t (<[producer := []]> vss)
    | RET producer;
      bag_2۰producer t producer []
    >>>.

  Lemma bag_2٠close_producerｰspec t ι producer ws :
    {{{
      bag_2۰inv t ι ∗
      bag_2۰producer t producer ws
    }}}
      bag_2٠close_producer producer
    {{{
      RET ();
      bag_2۰producer t producer ws
    }}}.

  Lemma bag_2٠create_consumerｰspec t ι :
    {{{
      bag_2۰inv t ι
    }}}
      bag_2٠create_consumer t
    {{{
      consumer
    , RET consumer;
      bag_2۰consumer t consumer
    }}}.

  Lemma bag_2٠pushｰspec t ι producer ws v :
    <<<
      bag_2۰inv t ι ∗
      bag_2۰producer t producer ws
    | ∀∀ vss,
      bag_2۰model t vss
    >>>
      bag_2٠push producer v @ ↑ι
    <<<
      ∃∃ vs,
      ⌜vss !! producer = Some vs⌝ ∗
      bag_2۰model t (<[producer := vs ++ [v]]> vss)
    | RET ();
      bag_2۰producer t producer (vs ++ [v])
    >>>.

  #[local] Lemma bag_2٠pop₂ｰspec l γ 𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟 (queue : option val) nodes :
    <<<
      l ↪ γ ∗
      inv' l γ ∗
      𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟.[consumer_queue] ↦ queue ∗
      queues۰elem γ queue ∗
      xtchain (Header §Node 2) DfracDiscarded nodes §Null ∗
      [∗ list] node ∈ nodes,
        ∃ queue,
        queues۰at γ node queue
    | ∀∀ vss,
      model₁ γ vss
    >>>
      bag_2٠pop₂ #𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟 (from_option #@{location} §Null%V $ head nodes) @ ↑γ.(metadata۰inv)
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          model₁ γ vss
      | Some v ⇒
          ∃ producer vs,
          ⌜vss !! producer = Some (v :: vs)⌝ ∗
          model₁ γ (<[producer := vs]> vss)
      end
    | queue : option val,
      RET o;
      𝑐𝑜𝑛𝑠𝑢𝑚𝑒𝑟.[consumer_queue] ↦ queue ∗
      queues۰elem γ queue
    >>>.
  #[local] Lemma bag_2٠pop₁ｰspec t ι consumer :
    <<<
      bag_2۰inv t ι ∗
      bag_2۰consumer t consumer
    | ∀∀ vss,
      bag_2۰model t vss
    >>>
      bag_2٠pop₁ t consumer @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          bag_2۰model t vss
      | Some v ⇒
          ∃ producer vs,
          ⌜vss !! producer = Some (v :: vs)⌝ ∗
          bag_2۰model t (<[producer := vs]> vss)
      end
    | RET o;
      bag_2۰consumer t consumer
    >>>.
  Lemma bag_2٠popｰspec t ι consumer :
    <<<
      bag_2۰inv t ι ∗
      bag_2۰consumer t consumer
    | ∀∀ vss,
      bag_2۰model t vss
    >>>
      bag_2٠pop t consumer @ ↑ι
    <<<
      ∃∃ o,
      match o with
      | None ⇒
          bag_2۰model t vss
      | Some v ⇒
          ∃ producer vs,
          ⌜vss !! producer = Some (v :: vs)⌝ ∗
          bag_2۰model t (<[producer := vs]> vss)
      end
    | RET o;
      bag_2۰consumer t consumer
    >>>.
End bag_2۰G.

Require zoo_saturn.bag_2__opaque.

#[global] Opaque bag_2۰inv.
#[global] Opaque bag_2۰model.
#[global] Opaque bag_2۰producer.
#[global] Opaque bag_2۰consumer.