Library zoo.program_logic.state_interp

Require Import iris.base_logic.lib.invariants.

Require Import zoo.prelude.
Require Import zoo.iris.diaframe.
Require Import zoo.language.notations.
Require Export zoo.program_logic.ghost_state.
Require Import zoo.options.

Implicit Type cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Type tid : thread_id.
Implicit Type l : location.
Implicit Type v : val.
Implicit Type vs : list val.
Implicit Type hdr : header.
Implicit Type hdrs : gmap location header.
Implicit Type σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Type κ κs : list observation.

Record state ۰ wf σ v :=
  { state ۰ wf ｰ locals :
      σ.(state ۰ locals) = [v]
  ; state ۰ wf ｰ counter :
      σ.(state ۰ heap) !! zoo_counter = Some 0%V
  }.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Definition state_interp ns nt σ κs : iProp Σ :=
    headers ۰ auth σ.(state ۰ headers) ∗
    heap ۰ auth σ.(state ۰ heap) ∗
    prophets ۰ auth κs σ.(state ۰ prophets) ∗
    steps ۰ auth ns ∗
    locals ۰ auth σ.(state ۰ locals) ∗
    ⌜length σ.(state ۰ locals) = nt ⌝ ∗
    zoo_counter ۰ inv.

  Definition fork_post (_ : val) : iProp Σ :=
    True.
End zoo ۰ G.

#[local] Instance : CustomIpat "state_interp" :=
  " ( Hheaders_auth & Hheap_auth & Hprophets_auth & Hsteps_auth & Hlocals_auth & %Hlocals & Hcounter_inv ) ".

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Lemma state_interp ｰ mono ns nt σ κs :
    state_interp ns nt σ κs ⊢ |==>
    state_interp ˖ns nt σ κs.

  Lemma state_interp ｰ zoo_counter ۰ inv ns nt σ κs :
    state_interp ns nt σ κs ⊢
    zoo_counter ۰ inv.
End zoo ۰ G.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  #[local] Lemma big_sepM ｰ chunk {A} (Φ : location → A → iProp Σ) l xs :
    ([∗ map ] l ↦ x ∈ chunk l xs , Φ l x ) ⊢
    [∗ list ] i ↦ x ∈ xs , Φ (l +ₗ i) x.

  Lemma state_interp ｰ alloc {ns nt σ κs} l tag vs :
    σ.(state ۰ headers) !! l = None →
    ( ∀ i,
      i < length vs →
      σ.(state ۰ heap) !! (l +ₗ i ) = None
    ) →
    state_interp ns nt σ κs ⊢ |==>
      let hdr := Header tag (length vs) in
      state_interp ns nt (state ۰ alloc l hdr vs σ) κs ∗
      l ↦ₕ hdr ∗
      meta_token l ⊤ ∗
      l ↦∗ vs.

  Lemma state_interp ｰ headers ۰ at ｰ valid ns nt σ κs l hdr :
    state_interp ns nt σ κs -∗
    l ↦ₕ hdr -∗
    ⌜σ.(state ۰ headers) !! l = Some hdr ⌝.

  Lemma state_interp ｰ pointsto ｰ valid ns nt σ κs l dq v :
    state_interp ns nt σ κs -∗
    l ↦{dq } v -∗
    ⌜σ.(state ۰ heap) !! l = Some v ⌝.
  Lemma state_interp ｰ pointstos ｰ valid ns nt σ κs l dq vs :
    state_interp ns nt σ κs -∗
    l ↦∗{dq } vs -∗
    ⌜ ∀ (i : nat) v,
      vs !! i = Some v →
      σ.(state ۰ heap) !! (l +ₗ i ) = Some v
    ⌝.
  Lemma state_interp ｰ pointsto ｰ update {ns nt σ κs l w} v :
    state_interp ns nt σ κs -∗
    l ↦ w ==∗
      state_interp ns nt (state ۰ set_location l v σ) κs ∗
      l ↦ v.

  Lemma state_interp ｰ steps ۰ lb ｰ get ns nt σ κs :
    state_interp ns nt σ κs ⊢
    ⧖ ns.
  Lemma state_interp ｰ steps ۰ lb ｰ valid ns1 nt σ κs ns2 :
    state_interp ns1 nt σ κs -∗
    ⧖ ns2 -∗
    ⌜ns2 ≤ ns1 ⌝.

  Lemma state_interp ｰ local_pointsto ｰ valid ns nt σ κs tid dq v :
    state_interp ns nt σ κs -∗
    tid ↦ₗ {dq } v -∗
    ⌜σ.(state ۰ locals) !! tid = Some v ⌝.
  Lemma state_interp ｰ fork {ns nt σ κs} v :
    state_interp ns nt σ κs ⊢ |==>
      state_interp ns (nt + 1) (state ۰ add_local v σ) κs ∗
      nt ↦ₗ v.
  Lemma state_interp ｰ local_pointsto ｰ update {ns nt σ κs tid w} v :
    state_interp ns nt σ κs -∗
    tid ↦ₗ w ==∗
      state_interp ns nt (state ۰ set_local tid v σ) κs ∗
      tid ↦ₗ v.

  Lemma state_interp ｰ prophet ｰ new {ns nt σ κs} pid :
    pid ∉ σ.(state ۰ prophets) →
    state_interp ns nt σ κs ⊢ |==>
      ∃ prophs ,
      state_interp ns nt (state ۰ add_prophet pid σ) κs ∗
      prophet ۰ model pid prophs.
  Lemma state_interp ｰ prophet ｰ resolve ns nt σ κs pid proph prophs :
    state_interp ns nt σ ((pid , proph ) :: κs) -∗
    prophet ۰ model pid prophs ==∗
      ∃ prophs',
      ⌜prophs = proph :: prophs'⌝ ∗
      state_interp ns nt σ κs ∗
      prophet ۰ model pid prophs'.
End zoo ۰ G.

Definition state ۰ heap ۰ initial σ :=
  delete zoo_counter σ.(state ۰ heap).

Lemma state_interp ｰ init `{zoo ۰ Gpre : !ZooGpre Σ} `{inv ۰ G : !invGS Σ} σ v κs :
  state ۰ wf σ v →
  ⊢ |={⊤}=>
    ∃ zoo ۰ G : ZooG Σ ,
    ⌜zoo ۰ G.(zoo ۰ G ۰ inv ۰ G) = inv ۰ G ⌝ ∗
    state_interp 0 1 σ κs ∗
    ([∗ map ] l ↦ v ∈ state ۰ heap ۰ initial σ , l ↦ v ) ∗
    0 ↦ₗ v.

#[global] Opaque state_interp.