Library zoo_partition.partition

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable
  gset.
From zoo.iris.algebra Require Import
  big_op.
From zoo.iris.base_logic Require Import
  mono_gset.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  list
  xdlchain.
From zoo_partition Require Import
  partition__types.
From zoo_partition Require Export
  partition__code.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types sz : nat.
Implicit Types elt first last split class : location.
Implicit Types v v_elts : val.
Implicit Types cl : gset location.
Implicit Types 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 Types descr : descriptor.
Implicit Types 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 Types γ : 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.

From zoo_partition Require
  partition__opaque.

#[global] Opaque partition_model.
#[global] Opaque partition_element.