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

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

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

16 17
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
  ( `{heapG Σ}, WP e @ s;  {{ v, ⌜φ v }}%I) 
18
  adequate s e σ (λ v _, φ v).
19
Proof.
20
  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
21 22
  iMod (gen_heap_init σ) as (?) "Hh".
  iModIntro. iExists gen_heap_ctx. iFrame "Hh".
23
  iApply (Hwp (HeapG _ _ _)).
Ralf Jung's avatar
Ralf Jung committed
24
Qed.