Library zoo.program_logic.bwp_adequacy

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.diaframe.
Require Export zoo.program_logic.bwp.
Require Import zoo.options.

Implicit Type e : expr.
Implicit Type es : list expr.

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

  Implicit Type Φ : val → iProp Σ.
  Implicit Type Φs : list (val → iProp Σ).

  Definition bwps nt es Φs : iProp Σ :=
    [∗ list ] i ↦ e ; Φ ∈ es ; Φs ,
      BWP e ∶ nt + i {{ Φ }}.

  #[local] Lemma bwp ｰ step tid e1 σ1 e2 σ2 κ κs es ns nt Φ :
    prim_step tid e1 σ1 κ e2 σ2 es →
    state_interp ns nt σ1 (κ ++ κs) -∗
    £ (later ۰ function ns ) -∗
    BWP e1 ∶ tid {{ Φ }} -∗
      |={⊤}[∅]▷=>
      state_interp ˖ns (nt + length es) σ2 κs ∗
      BWP e2 ∶ tid {{ Φ }} ∗
      bwps nt es (replicate (length es) fork_post).
  #[local] Lemma bwps ｰ step es1 σ1 es2 σ2 κ κs ns Φs :
    step (es1 , σ1 ) κ (es2 , σ2 ) →
    state_interp ns (length es1) σ1 (κ ++ κs) -∗
    £ (later ۰ function ns ) -∗
    bwps 0 es1 Φs -∗
      |={⊤}[∅]▷=>
      state_interp ˖ns (length es2) σ2 κs ∗
      bwps 0 es2 (Φs ++ replicate (length es2 - length es1) fork_post).
  #[local] Lemma bwps ｰ steps n es1 σ1 es2 σ2 κs1 κs2 ns Φs :
    nsteps n (es1 , σ1 ) κs1 (es2 , σ2 ) →
    state_interp ns (length es1) σ1 (κs1 ++ κs2) -∗
    £ (later ۰ sum ns n ) -∗
    bwps 0 es1 Φs -∗
      |={⊤,∅}=> |={∅}▷=>^n |={∅,⊤}=>
      state_interp (ns + n) (length es2) σ2 κs2 ∗
      bwps 0 es2 (Φs ++ replicate (length es2 - length es1) fork_post).

  #[local] Lemma bwp ｰ not ｰ stuck e tid ns nt σ κs Φ :
    state_interp ns nt σ κs -∗
    BWP e ∶ tid {{ Φ }} -∗
      |={⊤, ∅}=>
      ⌜not_stuck tid e σ ⌝.

  #[local] Lemma bwps ｰ progress n es1 σ1 tid e2 es2 σ2 κs1 κs2 ns Φs :
    nsteps n (es1 , σ1 ) κs1 (es2 , σ2 ) →
    es2 !! tid = Some e2 →
    state_interp ns (length es1) σ1 (κs1 ++ κs2) -∗
    £ (later ۰ sum ns n ) -∗
    bwps 0 es1 Φs -∗
      |={⊤, ∅}=> |={∅}▷=>^n |={∅}=>
      ⌜not_stuck tid e2 σ2 ⌝.
End zoo ۰ G.

Lemma bwp ｰ progress `{inv_Gpre : !invGpreS Σ} n es1 σ1 es2 σ2 κs :
  ( ∀ `{inv ۰ G : !invGS Σ},
    ⊢ |={⊤}=>
      ∃ (zoo ۰ G : ZooG Σ) Φs ,
      ⌜zoo ۰ G.(zoo ۰ G ۰ inv ۰ G) = inv ۰ G ⌝ ∗
      state_interp 0 (length es1) σ1 κs ∗
      bwps 0 es1 Φs
  ) →
  nsteps n (es1 , σ1 ) κs (es2 , σ2 ) →
  Foralli (λ tid e2, not_stuck tid e2 σ2) es2.

Lemma bwp ｰ adequacy' `{inv_Gpre : !invGpreS Σ} e σ :
  ( ∀ `{inv ۰ G : !invGS Σ} κs,
    ⊢ |={⊤}=>
      ∃ (zoo ۰ G : ZooG Σ) Φ ,
      ⌜zoo ۰ G.(zoo ۰ G ۰ inv ۰ G) = inv ۰ G ⌝ ∗
      state_interp 0 1 σ κs ∗
      BWP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ ).
Lemma bwp ｰ adequacy `{zoo ۰ Gpre : !ZooGpre Σ} {e σ} v :
  state ۰ wf σ v →
  ( ∀ `{zoo ۰ G : !ZooG Σ},
    ⊢ ∃ Φ ,
      ([∗ map ] l ↦ v ∈ state ۰ heap ۰ initial σ , l ↦ v ) -∗
      0 ↦ₗ v -∗
      BWP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ ).