Library zoo_boxroot.gc

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo.options.

Implicit Type ofs : nat.
Implicit Type l root : location.
Implicit Type roots : list location.
Implicit Type fn iter : val.

Parameter gc ۰ state : Type.
Implicit Type gc : gc ۰ state.

Parameter gc ۰ location : Type.
Implicit Type ω : gc ۰ location.
Implicit Type ωs : list gc ۰ location.

Parameter gc ۰ location ｰ inhabited : Inhabited gc ۰ location.
#[global] Existing Instance gc ۰ location ｰ inhabited.

Parameter gc ۰ val : Type.
Parameter GcInt : Z → gc ۰ val.
Parameter GcLoc : gc ۰ location → gc ۰ val.
Parameter gc ۰ val ۰ to_val : gc ۰ val → val.
Parameter gc ۰ val ۰ of_val : val → option gc ۰ val.
Implicit Type ν : gc ۰ val.
Implicit Type νs : list gc ۰ val.

Parameter gc ۰ model : ∀ `{zoo ۰ G : !ZooG Σ}, gc ۰ state → iProp Σ.
Parameter gc ۰ pointsto : ∀ `{zoo ۰ G : !ZooG Σ}, gc ۰ location → list gc ۰ val → iProp Σ.
Parameter gc ۰ realized : gc ۰ state → gc ۰ location → location → Prop.
Definition gc ۰ root `{zoo ۰ G : !ZooG Σ} gc root ω : iProp Σ :=
  ∃ l ,
  root ↦ #l ∗
  ⌜gc ۰ realized gc ω l ⌝.

Notation "ω '↦gc' νs" := (
  gc ۰ pointsto ω νs
)(at level 20,
  format "ω ↦gc νs"
) : bi_scope.
Notation "ω '↦gc[' gc ] l" := (
  gc ۰ realized gc ω l
)(at level 20,
  format "ω ↦gc[ gc ] l"
) : stdpp_scope.
Notation "root '↦root[' gc ] ω" := (
  gc ۰ root gc root ω
)(at level 20,
  format "root ↦root[ gc ] ω"
) : bi_scope.

Axiom gc ۰ realized ｰ agree : ∀ gc ω l1 l2,
  ω ↦gc [gc ] l1 →
  ω ↦gc [gc ] l2 →
  l1 = l2.

Parameter gc ｰ wp ｰ load : ∀ `{zoo ۰ G : !ZooG Σ} ν gc ω νs l i,
  (0 ≤ i)%Z →
  νs !! ₊i = Some ν →
  ω ↦gc [gc ] l →
  {{{
    gc ۰ model gc ∗
    ω ↦gc νs
  }}}
    Load #l #i
  {{{
    RET gc ۰ val ۰ to_val ν ;
    gc ۰ model gc ∗
    ω ↦gc νs
  }}}.

Parameter gc ｰ wp ｰ store : ∀ `{zoo ۰ G : !ZooG Σ} ν gc ω νs l i v,
  (0 ≤ i < length νs)%Z →
  gc ۰ val ۰ of_val v = Some ν →
  ω ↦gc [gc ] l →
  {{{
    gc ۰ model gc ∗
    ω ↦gc νs
  }}}
    Store #l #i v
  {{{
    RET gc ۰ val ۰ to_val ν ;
    gc ۰ model gc ∗
    ω ↦gc <[₊i := ν ]> νs
  }}}.

Lemma gc ｰ wp ｰ load ｰ root `{zoo ۰ G : !ZooG Σ} gc root ω root_base root_ofs :
  root = root_base +ₗ root_ofs →
  {{{
    root ↦root [gc ] ω
  }}}
    Load #root_base #root_ofs
  {{{
    l
  , RET #l ;
    ⌜ω ↦gc [gc ] l ⌝ ∗
    root ↦root [gc ] ω
  }}}.
Lemma gc ｰ wp ｰ load ｰ root' `{zoo ۰ G : !ZooG Σ} {gc root ω} l root_base root_ofs :
  root = root_base +ₗ root_ofs →
  ω ↦gc [gc ] l →
  {{{
    root ↦root [gc ] ω
  }}}
    Load #root_base #root_ofs
  {{{
    RET #l ;
    root ↦root [gc ] ω
  }}}.

Lemma gc ｰ wp ｰ store ｰ root `{zoo ۰ G : !ZooG Σ} {gc root ω'} ω l root_base root_ofs :
  root = root_base +ₗ root_ofs →
  ω ↦gc [gc ] l →
  {{{
    root ↦root [gc ] ω'
  }}}
    Store #root_base #root_ofs #l
  {{{
    RET ();
    root ↦root [gc ] ω
  }}}.

Parameter gc ۰ roots : ∀ `{zoo ۰ G : !ZooG Σ}, (gc ۰ state → iProp Σ) → iProp Σ.
Parameter gc ٠ set_roots : val.
Axiom gc ٠ set_roots ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} {gc Χ' iter} Χ Ξ ofs,
  {{{
    gc ۰ model gc ∗
    gc ۰ roots Χ' ∗
    □ (
      ∀ gc ,
      Χ gc ∗-∗
        ∃ roots ω s ,
        Ξ roots ω s ∗
        ( [∗ list ] root ; ω ∈ roots ; ω s ,
          (root +ₗ ofs ) ↦root [gc ] ω
        )
    ) ∗
    □ (
      ∀ Ψ roots ω s fn ,
      {{{
        ▷ Ψ [] ∗
        Ξ roots ω s ∗
        □ (
          ∀ roots_done root roots_todo ,
          ⌜roots = roots_done ++ root :: roots_todo ⌝ -∗
          Ψ roots_done -∗
          WP fn #root {{ res ,
            ⌜res = ()%V⌝ ∗
            ▷ Ψ (roots_done ++ [root])
          }}
        )
      }}}
        iter fn
      {{{
        RET ();
        Ξ roots ω s ∗
        Ψ roots
      }}}
    )
  }}}
    gc ٠ set_roots iter #ofs
  {{{
    RET ();
    gc ۰ model gc ∗
    gc ۰ roots Χ
  }}}.

Parameter gc ٠ alloc : val.
Axiom gc ٠ alloc ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} gc Χ n,
  (0 < n)%Z →
  {{{
    gc ۰ model gc ∗
    gc ۰ roots Χ ∗
    Χ gc
  }}}
    gc ٠ alloc #n
  {{{
    l gc ω
  , RET #l ;
    ⌜ω ↦gc [gc ] l ⌝ ∗
    gc ۰ model gc ∗
    gc ۰ roots Χ ∗
    Χ gc ∗
    ω ↦gc replicate ₊n (GcInt 0)
  }}}.