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

8 9 10 11
Class heapPreG Σ := HeapPreG {
  heap_preG_iris :> irisPreG heap_lang Σ;
  heap_preG_heap :> inG Σ (authR heapUR)
}.
12

13 14 15 16 17 18
Definition heapΣ : gFunctors :=
  #[irisΣ heap_lang; GFunctor (constRF (authR heapUR))].
Instance subG_heapPreG {Σ} : subG heapΣ Σ  heapPreG Σ.
Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.

Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
19 20 21 22
  ( `{heapG Σ}, heap_ctx  WP e {{ v,  φ v }}) 
  adequate e σ φ.
Proof.
  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
23 24 25 26 27
  iVs (own_alloc ( to_heap σ)) as (γ) "Hh".
  { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
  set (Hheap := HeapG _ _ _ γ).
  iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|].
  iApply (Hwp _). by rewrite /heap_ctx.
28
Qed.