Library zoo.program_logic.wp_adequacy

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

Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : 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 σ} v :
  state ۰ wf σ v →
  ( ∀ `{zoo ۰ G : !ZooG Σ},
    ⊢ ∃ Φ ,
      ([∗ map ] l ↦ v ∈ state ۰ heap ۰ initial σ , l ↦ v ) -∗
      0 ↦ₗ v -∗
      WP e ∶ 0 {{ Φ }}
  ) →
  safe ([e], σ ).