Library zoo_persistent.puf

From zoo Require Import
  prelude.
From zoo.common Require Import
  fin_maps.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_persistent Require Export
  base
  puf__code.
From zoo_persistent Require Import
  puf__types
  pstore_2.
From zoo Require Import
  options.

Implicit Types rank : Z.
Implicit Types elt repr parent : location.
Implicit Types t s descr : val.
Implicit Types reprs : gmap location location.
Implicit Types descrs : gmap location val.

Class PufG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] puf_G_pstore_G :: Pstore2G Σ
  }.

Definition puf_Σ :=
  #[pstore_2_Σ
  ].
#[global] Instance subG_puf_Σ Σ `{zoo_G : !ZooG Σ} :
  subG puf_Σ Σ →
  PufG Σ.

#[local] Definition unify_at repr1 repr2 repr :=
  if decide (repr = repr1) then
    repr2
  else
    repr.

#[local] Lemma unify_at_1 repr1 repr2 :
  unify_at repr1 repr2 repr1 = repr2.
#[local] Lemma unify_at_2 repr1 repr2 repr :
  repr ≠ repr1 →
  unify_at repr1 repr2 repr = repr.

#[local] Definition unify repr1 repr2 reprs :=
  unify_at repr1 repr2 <$> reprs.

#[local] Lemma unify_lookup_1 reprs repr1 repr2 elt :
  reprs !! elt = Some repr1 →
  unify repr1 repr2 reprs !! elt = Some repr2.
#[local] Lemma unify_lookup_2 {reprs repr1 repr2 elt} repr :
  reprs !! elt = Some repr →
  repr ≠ repr1 →
  unify repr1 repr2 reprs !! elt = Some repr.
#[local] Lemma unify_lookup_2' reprs repr1 repr2 :
  reprs !! repr2 = Some repr2 →
  repr1 ≠ repr2 →
  unify repr1 repr2 reprs !! repr2 = Some repr2.
#[local] Lemma dom_unify repr1 repr2 reprs :
  dom (unify repr1 repr2 reprs) = dom reprs.

Opaque unify_at.
Opaque unify.

#[local] Definition consistent_at reprs elt repr descr :=
  ( ∃ rank,
    repr = elt ∧
    descr = ‘Root( #rank )%V
  ) ∨ (
    ∃ parent,
    elt ≠ repr ∧
    descr = ‘Link( #parent )%V ∧
    reprs !! parent = Some repr ∧
    reprs !! repr = Some repr
  ).
#[local] Definition consistent reprs descrs :=
  map_Forall2 (consistent_at reprs) reprs descrs.

#[local] Lemma consistent_empty :
  consistent ∅ ∅.
#[local] Lemma consistent_lookup_None {reprs descrs} elt :
  consistent reprs descrs →
  descrs !! elt = None →
  reprs !! elt = None.
#[local] Lemma consistent_lookup_Some {reprs descrs} elt repr :
  consistent reprs descrs →
  reprs !! elt = Some repr →
    ∃ descr,
    descrs !! elt = Some descr ∧
    consistent_at reprs elt repr descr.
#[local] Lemma consistent_insert {reprs descrs} elt :
  descrs !! elt = None →
  consistent reprs descrs →
  consistent
    (<[elt := elt]> reprs)
    (<[elt := ‘Root( 0 )%V]> descrs).
#[local] Lemma consistent_link_repr {reprs descrs} elt repr :
  elt ≠ repr →
  reprs !! elt = Some repr →
  reprs !! repr = Some repr →
  consistent reprs descrs →
  consistent
    reprs
    (<[elt := ‘Link( #repr )%V]> descrs).
#[local] Lemma consistent_link_union {reprs descrs} repr1 repr2 :
  repr1 ≠ repr2 →
  reprs !! repr1 = Some repr1 →
  reprs !! repr2 = Some repr2 →
  consistent reprs descrs →
  consistent
    (unify repr1 repr2 reprs)
    (<[repr1 := ‘Link( #repr2 )%V]> descrs).
#[local] Lemma consistent_update_rank {reprs descrs} repr rank :
  reprs !! repr = Some repr →
  consistent reprs descrs →
  consistent
    reprs
    (<[repr := ‘Root( #rank )%V]> descrs).

Opaque consistent_at.
Opaque consistent.

Section puf_G.
  Context `{puf_G : PufG Σ}.

  Definition puf_model t reprs : iProp Σ :=
    ∃ descrs,
    pstore_2_model t descrs ∗
    ⌜consistent reprs descrs⌝.
  #[local] Instance : CustomIpat "model" :=
    " ( %descrs{} & Hmodel{} & %Hconsistent{} ) ".

  Definition puf_snapshot s t reprs : iProp Σ :=
    ∃ descrs,
    pstore_2_snapshot s t descrs ∗
    ⌜consistent reprs descrs⌝.
  #[local] Instance : CustomIpat "snapshot" :=
    " ( %descrs{} & Hsnapshot{} & %Hconsistent{} ) ".

  #[global] Instance puf_model_timeless t reprs :
    Timeless (puf_model t reprs).

  #[global] Instance puf_snapshot_persistent s t reprs :
    Persistent (puf_snapshot s t reprs).

  Lemma puf_model_valid {t reprs} elt repr :
    reprs !! elt = Some repr →
    puf_model t reprs ⊢
    ⌜reprs !! repr = Some repr⌝.
  Lemma puf_model_exclusive t reprs1 reprs2 :
    puf_model t reprs1 -∗
    puf_model t reprs2 -∗
    False.

  Lemma puf٠create𑁒spec :
    {{{
      True
    }}}
      puf٠create ()
    {{{
      t
    , RET t;
      puf_model t ∅
    }}}.

  Lemma puf٠make𑁒spec t reprs :
    {{{
      puf_model t reprs
    }}}
      puf٠make t
    {{{
      elt
    , RET #elt;
      puf_model t (<[elt := elt]> reprs)
    }}}.

  Lemma puf٠repr𑁒spec {t reprs elt} repr :
    reprs !! elt = Some repr →
    {{{
      puf_model t reprs
    }}}
      puf٠repr t #elt
    {{{
      RET #repr;
      puf_model t reprs
    }}}.

  Lemma puf٠equiv𑁒spec {t reprs elt1} repr1 {elt2} repr2 :
    reprs !! elt1 = Some repr1 →
    reprs !! elt2 = Some repr2 →
    {{{
      puf_model t reprs
    }}}
      puf٠equiv t #elt1 #elt2
    {{{
      RET #(bool_decide (repr1 = repr2));
      puf_model t reprs
    }}}.

  #[local] Lemma puf٠rank𑁒spec t reprs elt :
    reprs !! elt = Some elt →
    {{{
      puf_model t reprs
    }}}
      puf٠rank t #elt
    {{{
      rank
    , RET #rank;
      puf_model t reprs
    }}}.
  Definition puf_union_condition reprs repr1 repr2 reprs' :=
    dom reprs = dom reprs' ∧
    ( ∀ elt repr,
      reprs !! elt = Some repr →
      repr ≠ repr1 →
      repr ≠ repr2 →
      reprs' !! elt = Some repr
    ) ∧
    ( ∃ repr12,
      (repr12 = repr1 ∨ repr12 = repr2) ∧
        ∀ elt repr,
        reprs !! elt = Some repr →
        repr = repr1 ∨ repr = repr2 →
        reprs' !! elt = Some repr12
    ).
  #[local] Lemma puf_union_condition_refl reprs repr :
    puf_union_condition reprs repr repr reprs.
  #[local] Lemma puf_union_condition_sym reprs repr1 repr2 reprs' :
    puf_union_condition reprs repr1 repr2 reprs' →
    puf_union_condition reprs repr2 repr1 reprs'.
  #[local] Lemma unify_union_condition_1 reprs repr1 repr2 :
    repr1 ≠ repr2 →
    puf_union_condition reprs repr1 repr2 (unify repr1 repr2 reprs).
  #[local] Lemma unify_union_condition_2 reprs repr1 repr2 :
    repr1 ≠ repr2 →
    puf_union_condition reprs repr2 repr1 (unify repr1 repr2 reprs).
  #[local] Opaque puf_union_condition.
  Lemma puf٠union𑁒spec {t reprs elt1} repr1 {elt2} repr2 :
    reprs !! elt1 = Some repr1 →
    reprs !! elt2 = Some repr2 →
    {{{
      puf_model t reprs
    }}}
      puf٠union t #elt1 #elt2
    {{{
      reprs'
    , RET ();
      puf_model t reprs' ∗
      ⌜puf_union_condition reprs repr1 repr2 reprs'⌝
    }}}.

  Lemma puf٠capture𑁒spec t reprs :
    {{{
      puf_model t reprs
    }}}
      puf٠capture t
    {{{
      s
    , RET s;
      puf_model t reprs ∗
      puf_snapshot s t reprs
    }}}.

  Lemma puf٠restore𑁒spec t reprs s reprs' :
    {{{
      puf_model t reprs ∗
      puf_snapshot s t reprs'
    }}}
      puf٠restore t s
    {{{
      RET ();
      puf_model t reprs'
    }}}.
End puf_G.

From zoo_persistent Require
  puf__opaque.

#[global] Opaque puf_model.
#[global] Opaque puf_snapshot.