Library zoo_std.chain

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.chain__code.
Require Import zoo_std.chain__types.
Require Import zoo.options.

Implicit Type l : location.
Implicit Type 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 .[next ] ↦ t' ∗
        l .[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₁ tag v :
    ⊢ chain ۰ model tag v [] v.
  Lemma chain ۰ model ｰ nil₂ tag t dst :
    chain ۰ model tag t [] dst ⊢
    ⌜t = dst ⌝.

  Lemma chain ۰ model ｰ app₁ 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₂ 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₁ 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₂ 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 .{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 .{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 .{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 <-{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 <-{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 <-{next } dst'
    {{{
      RET ();
      chain ۰ model tag t [v] dst'
    }}}.
End zoo ۰ G.

#[global] Opaque chain ۰ model.