Library zoo.program_logic.wp_adequacy

From zoo Require Import
  prelude.
From zoo.iris Require Import
  diaframe.
From zoo.program_logic Require Export
  bwp_adequacy
  wp.
From zoo Require Import
  options.

Implicit Types e : expr.
Implicit Types v : val.
Implicit Types σ : state.

Lemma wp_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 ∗
      WP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ).
Lemma wp_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) -∗
      WP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ).