Library zoo.program_logic.bwp_adequacy

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

Implicit Types e : expr.
Implicit Types es : list expr.

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

  Implicit Types Φ : val → iProp Σ.
  Implicit Types Φ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 (S 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 (S 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 σ} param :
  state_wf σ param →
  ( ∀ `{zoo_G : !ZooG Σ},
    ⊢ ∃ Φ,
      ([∗ map] l ↦ v ∈ state_heap_initial σ, l ↦ v) -∗
      0 ↦ₗ param.(zoo_parameter_local) -∗
      BWP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ).