adequacy.v 782 Bytes
Newer Older
1 2 3 4 5 6
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap.
From iris.program_logic Require Import auth ownership.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics weakestpre.

7
Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
8 9 10 11 12 13 14 15 16 17 18

Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ :
  ( `{heapG Σ}, heap_ctx  WP e {{ v,  φ v }}) 
  adequate e σ φ.
Proof.
  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
  iVs (auth_alloc (ownP  of_heap) heapN _ (to_heap σ) with "[Hσ]") as (γ) "[??]".
  - auto using to_heap_valid.
  - rewrite /= (from_to_heap σ); auto.
  - iApply (Hwp (HeapG _ _ _ γ)). by rewrite /heap_ctx.
Qed.