Library zoo_std.chain

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  chain__types.
From zoo Require Import
  options.

Implicit Types l : location.
Implicit Types v w t dst : val.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Fixpoint chain_model tag t vs dst : iProp Σ :=
    match vs with
    | [] ⇒
        ⌜t = dst⌝
    | v :: vs ⇒
        ∃ l t',
        ⌜t = #l⌝ ∗
        from_option (λ tag, l ↦ₕ Header tag 2) True tag ∗
        l.[chain_next] ↦ t' ∗
        l.[chain_data] ↦ v ∗
        chain_model tag t' vs dst
    end.
  #[global] Arguments chain_model _ _ !_ _ / : assert.
  #[local] Instance : CustomIpat "model" :=
    " ( %l{} & %t{}' & {%Heq{eq};->} & Hl{}_header & Hl{}_next & Hl{}_data & Hmodel{}' ) ".

  #[global] Instance chain_model_timeless tag t vs dst :
    Timeless (chain_model tag t vs dst).

  Lemma chain_physically_distinct tag1 t1 vs1 dst1 tag2 t2 vs2 dst2 :
    0 < length vs1 →
    0 < length vs2 →
    t1 ≉ t2 →
    chain_model tag1 t1 vs1 dst1 -∗
    chain_model tag2 t2 vs2 dst2 -∗
    ⌜t1 ≠ t2⌝.
  Lemma chain_physically_distinct' tag t vs dst :
    0 < length vs →
    t ≉ t →
    chain_model tag t vs dst ⊢
    False.
  Lemma wp_equal_chain tag1 t1 vs1 dst1 tag2 t2 vs2 dst2 Φ :
    0 < length vs1 →
    0 < length vs2 →
    chain_model tag1 t1 vs1 dst1 -∗
    chain_model tag2 t2 vs2 dst2 -∗
    ( chain_model tag1 t1 vs1 dst1 -∗
      chain_model tag2 t2 vs2 dst2 -∗
        (⌜t1 ≠ t2⌝ -∗ Φ false%V) ∧
        (⌜t1 = t2⌝ -∗ Φ true%V)
    ) -∗
    WP t1 == t2 {{ Φ }}.

  Lemma chain_model_tag tag t vs dst :
    length vs ≠ 0 →
    chain_model (Some tag) t vs dst ⊢
      ∃ l,
      ⌜t = #l⌝ ∗
      l ↦ₕ Header tag 2.

  Lemma chain_model_nil tag t dst :
    ⌜t = dst⌝ ⊣⊢
    chain_model tag t [] dst.
  Lemma chain_model_nil_1 tag v :
    ⊢ chain_model tag v [] v.
  Lemma chain_model_nil_2 tag t dst :
    chain_model tag t [] dst ⊢
    ⌜t = dst⌝.

  Lemma chain_model_app_1 vs1 vs2 tag t vs dst :
    vs = vs1 ++ vs2 →
    chain_model tag t vs dst ⊢
      ∃ t',
      chain_model tag t vs1 t' ∗
      chain_model tag t' vs2 dst.
  Lemma chain_model_app_2 tag t1 vs1 t2 vs2 dst :
    chain_model tag t1 vs1 t2 -∗
    chain_model tag t2 vs2 dst -∗
    chain_model tag t1 (vs1 ++ vs2) dst.
  Lemma chain_model_app tag t vs vs1 vs2 dst :
    vs = vs1 ++ vs2 →
    chain_model tag t vs dst ⊣⊢
      ∃ t',
      chain_model tag t vs1 t' ∗
      chain_model tag t' vs2 dst.

  Lemma chain_model_snoc tag t vs vs' v dst :
    vs = vs' ++ [v] →
    chain_model tag t vs dst ⊣⊢
      ∃ t',
      chain_model tag t vs' t' ∗
      chain_model tag t' [v] dst.
  Lemma chain_model_snoc_1 tag t vs vs' v dst :
    vs = vs' ++ [v] →
    chain_model tag t (vs ++ [v]) dst ⊢
      ∃ t',
      chain_model tag t vs t' ∗
      chain_model tag t' [v] dst.
  Lemma chain_model_snoc_2 tag t1 vs t2 v dst :
    chain_model tag t1 vs t2 -∗
    chain_model tag t2 [v] dst -∗
    chain_model tag t1 (vs ++ [v]) dst.

  Lemma chain_model_exclusive t tag1 vs1 dst1 tag2 vs2 dst2 :
    0 < length vs1 →
    0 < length vs2 →
    chain_model tag1 t vs1 dst1 -∗
    chain_model tag2 t vs2 dst2 -∗
    False.

  Lemma chain٠block𑁒spec tag t vs dst v :
    {{{
      chain_model tag t vs dst
    }}}
      Block Mutable (default 0%nat tag) [Val t; Val v]
    {{{
      t'
    , RET t';
      chain_model tag t' (v :: vs) dst
    }}}.

  Lemma chain٠data𑁒spec tag t v vs dst :
    {{{
      chain_model tag t (v :: vs) dst
    }}}
      t.{chain_data}
    {{{
      RET v;
      chain_model tag t (v :: vs) dst
    }}}.

  Lemma chain٠next𑁒spec tag t v vs dst :
    {{{
      chain_model tag t (v :: vs) dst
    }}}
      t.{chain_next}
    {{{
      t'
    , RET t';
      chain_model tag t [v] t' ∗
      chain_model tag t' vs dst
    }}}.
  Lemma chain٠next𑁒spec_singleton tag t v dst :
    {{{
      chain_model tag t [v] dst
    }}}
      t.{chain_next}
    {{{
      RET dst;
      chain_model tag t [v] dst
    }}}.

  Lemma chain٠set_data𑁒spec tag t v vs dst w :
    {{{
      chain_model tag t (v :: vs) dst
    }}}
      t <-{chain_data} w
    {{{
      RET ();
      chain_model tag t (w :: vs) dst
    }}}.

  Lemma chain٠set_next𑁒spec tag t v vs dst v' :
    {{{
      chain_model tag t (v :: vs) dst
    }}}
      t <-{chain_next} v'
    {{{
      t'
    , RET ();
      chain_model tag t [v] v' ∗
      chain_model tag t' vs dst
    }}}.
  Lemma chain٠set_next𑁒spec_singleton tag t v dst dst' :
    {{{
      chain_model tag t [v] dst
    }}}
      t <-{chain_next} dst'
    {{{
      RET ();
      chain_model tag t [v] dst'
    }}}.
End zoo_G.

#[global] Opaque chain_model.