Library zoo_partition.partition

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gset.
Require Import zoo.iris.algebra.big_op.
Require Import zoo.iris.base_logic.lib.mono_gset.
Require Import zoo.base.
Require Import zoo_std.xdlchain.
Require Export zoo_partition.partition__code.
Require Import zoo_partition.partition__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type sz : nat.
Implicit Type elt first last split class : location.
Implicit Type v v_elts : val.
Implicit Type cl : gset location.
Implicit Type part : gset (gset location).

Record descriptor :=
  { descriptor۰elts : list location
  ; descriptor۰prev : location
  ; descriptor۰next : location
  }.

#[local] Instance descriptorｰinhabited : Inhabited descriptor :=
  populate
    {|descriptor۰elts := inhabitant
    ; descriptor۰prev := inhabitant
    ; descriptor۰next := inhabitant
    |}.
#[local] Instance descriptorｰeq_dec : EqDecision descriptor :=
  ltac:(solve_decision).
#[local] Instance descriptorｰcountable :
  Countable descriptor.

Implicit Type descr : descriptor.
Implicit Type descrs : gmap location descriptor.

Class PartitionG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] partition۰G۰elts۰G :: MonoGsetG Σ location
  }.

Definition partition۰Σ :=
  #[mono_gset۰Σ location
  ].
#[global] Instance subGｰpartition۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG partition۰Σ Σ →
  PartitionG Σ.

Section partition۰G.
  Context `{partition۰G : PartitionG Σ}.

  #[local] Definition metadata :=
    gname.
  Implicit Type γ : metadata.

  #[local] Definition elements۰auth γ elts :=
    mono_gset۰auth γ (DfracOwn 1) elts.
  #[local] Definition elements۰elem γ elt :=
    mono_gset۰elem γ elt.

  #[local] Definition element۰model class descr elt : iProp Σ :=
    elt.[class_] ↦ #class ∗
    elt.[seen] ↦ false.
  #[local] Instance : CustomIpat "element۰model" :=
    " ( Helt{}_class{_{suff}} & Helt{}_seen{_{suff}} ) ".
  #[local] Definition descriptor۰model class descrs descr : iProp Σ :=
    ∃ first last prev_descr prev next_descr next,
    ⌜head descr.(descriptor۰elts) = Some first⌝ ∗
    ⌜list.last descr.(descriptor۰elts) = Some last⌝ ∗
    ⌜descrs !! descr.(descriptor۰prev) = Some prev_descr⌝ ∗
    ⌜list.last prev_descr.(descriptor۰elts) = Some prev⌝ ∗
    ⌜descrs !! descr.(descriptor۰next) = Some next_descr⌝ ∗
    ⌜head next_descr.(descriptor۰elts) = Some next⌝ ∗
    class.[first] ↦ #first ∗
    class.[last] ↦ #last ∗
    class.[len] ↦ #(length descr.(descriptor۰elts)) ∗
    class.[split] ↦ #first ∗
    class.[split_len] ↦ 0 ∗
    xdlchain #prev descr.(descriptor۰elts) #next ∗
    [∗ list] elt ∈ descr.(descriptor۰elts),
      element۰model class descr elt.
  #[local] Instance : CustomIpat "descriptor۰model" :=
    " ( %first{} & %last{} & %prev{}_descr & %prev{} & %next{}_descr & %next{} & %Hfirst{} & %Hlast{} & %Hdescrs{}_elem_prev & %Hprev{} & %Hdescrs{}_elem_next & %Hnext{} & Hclass{}_first & Hclass{}_last & Hclass{}_len & Hclass{}_split & Hclass{}_split_len & Hchain{} & Helts{} ) ".
  #[local] Definition model' γ descrs : iProp Σ :=
    elements۰auth γ ([∪ map] descr ∈ descrs, list_to_set descr.(descriptor۰elts)) ∗
    [∗ map] class ↦ descr ∈ descrs,
      descriptor۰model class descrs descr.
  #[local] Instance : CustomIpat "model'" :=
    " ( Helts_auth & Hdescrs ) ".
  Definition partition۰model γ part : iProp Σ :=
    ∃ descrs,
    ⌜part = map_to_set (λ _, list_to_set ∘ descriptor۰elts) descrs⌝ ∗
    model' γ descrs.
  #[local] Instance : CustomIpat "model" :=
    " ( %descrs & -> & Hmodel ) ".

  Definition partition۰element γ elt v : iProp Σ :=
    elements۰elem γ elt ∗
    elt.[data] ↦□ v.
  #[local] Instance : CustomIpat "element" :=
    " ( Helts_elem{}{_{suff}} & Helt{}_data{_{suff}} ) ".

  #[global] Instance partition۰modelｰtimeless γ part :
    Timeless (partition۰model γ part).
  #[global] Instance partition۰elementｰtimeless γ elt v :
    Timeless (partition۰element γ elt v).

  #[global] Instance partition۰elementｰpersistent γ elt v :
    Persistent (partition۰element γ elt v).

  #[local] Lemma elementsｰalloc :
    ⊢ |==>
      ∃ γ,
      elements۰auth γ ∅.
  #[local] Lemma elements۰elemｰvalid γ elts elt :
    elements۰auth γ elts -∗
    elements۰elem γ elt -∗
    ⌜elt ∈ elts⌝.
  #[local] Lemma elementsｰinsert {γ elts} elt :
    elements۰auth γ elts ⊢ |==>
      elements۰auth γ ({[elt]} ∪ elts) ∗
      elements۰elem γ elt.

  #[local] Lemma modelｰdisjoint' {γ descrs} class1 descr1 class2 descr2 elt :
    descrs !! class1 = Some descr1 →
    elt ∈ descr1.(descriptor۰elts) →
    descrs !! class2 = Some descr2 →
    elt ∈ descr2.(descriptor۰elts) →
    model' γ descrs ⊢
      ⌜class1 = class2⌝ ∗
      ⌜descr1 = descr2⌝.
  #[local] Lemma modelｰdisjoint'' {γ descrs} class descr elt :
    descrs !! class = Some descr →
    elt ∈ descr.(descriptor۰elts) →
    model' γ descrs ⊢
    ⌜ ∀ class' descr',
      descrs !! class' = Some descr' →
      elt ∈ descr'.(descriptor۰elts) →
        class' = class ∧
        descr' = descr
    ⌝.
  #[local] Lemma partition۰elementｰvalid' γ descrs elt v :
    model' γ descrs -∗
    partition۰element γ elt v -∗
      ∃ class descr,
      ⌜descrs !! class = Some descr⌝ ∗
      ⌜elt ∈ descr.(descriptor۰elts)⌝ ∗
      ⌜ ∀ class' descr',
        descrs !! class' = Some descr' →
        elt ∈ descr'.(descriptor۰elts) →
          class' = class ∧
          descr' = descr
      ⌝.
  #[local] Lemma modelｰNoDup {γ descrs} class descr :
    descrs !! class = Some descr →
    model' γ descrs ⊢
    ⌜NoDup descr.(descriptor۰elts)⌝.

  Lemma partition۰modelｰempty :
    ⊢ |==>
      ∃ γ,
      partition۰model γ ∅.
  Lemma partition۰modelｰnon_empty {γ part} cl :
    cl ∈ part →
    partition۰model γ part ⊢
    ⌜cl ≠ ∅⌝.
  Lemma partition۰modelｰdisjoint {γ part} elt cl1 cl2 :
    cl1 ∈ part →
    elt ∈ cl1 →
    cl2 ∈ part →
    elt ∈ cl2 →
    partition۰model γ part ⊢
    ⌜cl1 = cl2⌝.

  Lemma partition۰elementｰvalid γ part elt v :
    partition۰model γ part -∗
    partition۰element γ elt v -∗
      ∃ cl,
      ⌜cl ∈ part⌝ ∗
      ⌜elt ∈ cl⌝.
  Lemma partition۰elementｰagree γ elt v1 v2 :
    partition۰element γ elt v1 -∗
    partition۰element γ elt v2 -∗
    ⌜v1 = v2⌝.

  #[local] Lemma partition٠dllist٠createｰspec v v_class :
    {{{
      True
    }}}
      partition٠dllist٠create v v_class
    {{{
      elt
    , RET #elt;
      elt.[prev] ↦ #elt ∗
      elt.[next] ↦ #elt ∗
      elt.[data] ↦□ v ∗
      elt.[class_] ↦ v_class ∗
      elt.[seen] ↦ false
    }}}.

  #[local] Lemma partition٠get_classｰspec γ descrs elt v :
    {{{
      model' γ descrs ∗
      partition۰element γ elt v
    }}}
      (#elt).{class_}
    {{{
      class descr
    , RET #class;
      model' γ descrs ∗
      ⌜descrs !! class = Some descr⌝ ∗
      ⌜elt ∈ descr.(descriptor۰elts)⌝ ∗
      ⌜ ∀ class' descr',
        descrs !! class' = Some descr' →
        elt ∈ descr'.(descriptor۰elts) →
          class' = class ∧
          descr' = descr
      ⌝
    }}}.

  Lemma partition٠makeｰspec γ part v :
    {{{
      partition۰model γ part
    }}}
      partition٠make v
    {{{
      elt
    , RET #elt;
      partition۰model γ (part ∪ {[{[elt]}]}) ∗
      partition۰element γ elt v
    }}}.

  Lemma partition٠make_same_classｰspec γ part elt v v' :
    {{{
      partition۰model γ part ∗
      partition۰element γ elt v
    }}}
      partition٠make_same_class #elt v'
    {{{
      elt' part'
    , RET #elt';
      partition۰model γ part' ∗
      partition۰element γ elt' v' ∗
      ⌜ ∃ part'' cl,
        elt ∈ cl ∧
        part = part'' ∪ {[cl]} ∧
        part' = part'' ∪ {[cl ∪ {[elt']}]}
      ⌝
    }}}.

  Lemma partition٠getｰspec γ elt v :
    {{{
      partition۰element γ elt v
    }}}
      partition٠get #elt
    {{{
      RET v;
      True
    }}}.

  Lemma partition٠equalｰspec γ elt1 v1 elt2 v2 :
    {{{
      True
    }}}
      partition٠equal #elt1 #elt2
    {{{
      RET #(bool_decide (elt1 = elt2));
      True
    }}}.

  Lemma partition٠equivｰspec γ part elt1 v1 elt2 v2 :
    {{{
      partition۰model γ part ∗
      partition۰element γ elt1 v1 ∗
      partition۰element γ elt2 v2
    }}}
      partition٠equiv #elt1 #elt2
    {{{
      b
    , RET #b;
      partition۰model γ part ∗
      ⌜ ∀ cl1 cl2,
        cl1 ∈ part →
        elt1 ∈ cl1 →
        cl2 ∈ part →
        elt2 ∈ cl2 →
        if b then cl1 = cl2 else cl1 ≠ cl2
      ⌝
    }}}.

  Lemma partition٠reprｰspec γ part elt v :
    {{{
      partition۰model γ part ∗
      partition۰element γ elt v
    }}}
      partition٠repr #elt
    {{{
      elt'
    , RET #elt';
      partition۰model γ part ∗
      ⌜ ∀ cl,
        cl ∈ part →
        elt ∈ cl ↔ elt' ∈ cl
      ⌝
    }}}.

  Lemma partition٠cardinalｰspec γ part elt v :
    {{{
      partition۰model γ part ∗
      partition۰element γ elt v
    }}}
      partition٠cardinal #elt
    {{{
      sz
    , RET #sz;
      partition۰model γ part ∗
      ⌜ ∀ cl,
        cl ∈ part →
        elt ∈ cl →
        size cl = sz
      ⌝
    }}}.

  Lemma partition٠refineｰspec {γ part v_elts} elts :
    list۰model' v_elts (#*@{location} elts) →
    {{{
      partition۰model γ part
    }}}
      partition٠refine v_elts
    {{{
      part'
    , RET ();
      partition۰model γ part' ∗
      ⌜ ∀ cl',
        cl' ∈ part' ↔
          cl' ≠ ∅ ∧
            ∃ cl,
            cl ∈ part ∧
            ( cl' = cl ∩ list_to_set elts
            ∨ cl' = cl ∖ list_to_set elts
            )
      ⌝
    }}}.
End partition۰G.

Require zoo_partition.partition__opaque.

#[global] Opaque partition۰model.
#[global] Opaque partition۰element.