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.