adequacy.v 983 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.program_logic Require Export weakestpre adequacy.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.heap_lang Require Export lifting.
3
From iris.algebra Require Import auth.
4
From iris.heap_lang Require Import proofmode notation.
5
From iris.proofmode Require Import tactics.
6
Set Default Proof Using "Type".
7

8
Class heapPreG Σ := HeapPreG {
9
  heap_preG_iris :> invPreG Σ;
10
  heap_preG_heap :> gen_heapPreG loc val Σ
11
}.
12

13
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
14
Instance subG_heapPreG {Σ} : subG heapΣ Σ  heapPreG Σ.
15
Proof. solve_inG. Qed.
16

17 18 19
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
  ( `{heapG Σ}, WP e {{ v, ⌜φ v }}%I) 
  adequate e σ φ.
20
Proof.
21
  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
22 23 24
  iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
  iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
Ralf Jung's avatar
Ralf Jung committed
25
  set (Hheap := GenHeapG loc val Σ _ _ _ γ).
26
  iApply (Hwp (HeapG _ _ _)).
Ralf Jung's avatar
Ralf Jung committed
27
Qed.