Library zoo_saturn.bag_2

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

Implicit Types l node π‘π‘œπ‘›π‘ π‘’π‘šπ‘’π‘Ÿ : location.
Implicit Types nodes : list location.
Implicit Types v t producer consumer : val.
Implicit Types o : option val.
Implicit Types vs ws : list val.
Implicit Types vss wss : gmap val (list val).

Class Bag2G Ξ£ `{zoo_G : !ZooG Ξ£} :=
  { #[local] bag_2_G_spmc_queue_G :: SpmcQueueG Ξ£
  ; #[local] bag_2_G_queues_G :: MonoGmapG Ξ£ location val
  ; #[local] bag_2_G_model_G :: TwinsG Ξ£ (leibnizO (gmap val (list val)))
  }.

Definition bag_2_Ξ£ :=
  #[spmc_queue_Ξ£
  ; 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 Types π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ : 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 Types descr : descriptor.
Implicit Types 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 Types Ξ³ : 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 βˆ—
        spmc_queue_inv queue (Ξ³.(metadata_inv).@"producer")
    end.
  #[local] Instance : CustomIpat "queues_elem" :=
    " ( %node & #Hqueues_at & #Hqueue_inv ) ".

  #[local] Definition model₁' Ξ³_model vss :=
    twins_twin1 Ξ³_model (DfracOwn 1) vss.
  #[local] Definition model₁ Ξ³ :=
    model₁' Ξ³.(metadata_model).
  #[local] Definition modelβ‚‚' Ξ³_model vss :=
    twins_twin2 Ξ³_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⌝ βˆ—
    spmc_queue_inv descr.(descriptor_queue) (Ξ³.(metadata_inv).@"producer") βˆ—
    spmc_queue_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)⌝ βˆ—
    meta l nroot Ξ³ βˆ—
    inv' l Ξ³.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %Ξ³ & -> & -> & #Hmeta & #Hinv ) ".

  Definition bag_2_model t vss : iProp Ξ£ :=
    βˆƒ l Ξ³,
    βŒœt = #l⌝ βˆ—
    meta l nroot Ξ³ βˆ—
    model₁ Ξ³ vss.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{;_} & %Ξ³{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".

  Definition bag_2_producer t producer ws : iProp Ξ£ :=
    βˆƒ l Ξ³ π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ,
    βŒœt = #l⌝ βˆ—
    βŒœproducer = π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘ŸβŒ βˆ—
    meta l nroot Ξ³ βˆ—
    π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ.(producer_node) ↦ₕ Header Β§Node 2 βˆ—
    queues_at Ξ³ π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ.(producer_node) π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ.(producer_queue) βˆ—
    spmc_queue_inv π‘π‘Ÿπ‘œπ‘‘π‘’π‘π‘’π‘Ÿ.(producer_queue) (Ξ³.(metadata_inv).@"producer") βˆ—
    spmc_queue_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⌝ βˆ—
    meta l nroot Ξ³ βˆ—
    βŒœ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) :
    <<<
      meta l nroot Ξ³ βˆ—
      inv' l Ξ³ βˆ—
      spmc_queue_inv queue (Ξ³.(metadata_inv).@"producer") βˆ—
      spmc_queue_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) :
    <<<
      meta l nroot Ξ³ βˆ—
      inv' l Ξ³ βˆ—
      spmc_queue_inv queue (Ξ³.(metadata_inv).@"producer") βˆ—
      spmc_queue_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 :
    <<<
      meta l nroot Ξ³ βˆ—
      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.

From zoo_saturn Require
  bag_2__opaque.

#[global] Opaque bag_2_inv.
#[global] Opaque bag_2_model.
#[global] Opaque bag_2_producer.
#[global] Opaque bag_2_consumer.