adequacy.v 1.03 KB
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 proph_map.
4
From iris.proofmode Require Import tactics.
5
Set Default Proof Using "Type".
6

7 8 9 10
Class heap_prophPreG Σ := HeapProphPreG {
  heap_proph_preG_iris :> invPreG Σ;
  heap_proph_preG_heap :> gen_heapPreG loc val Σ;
  heap_proph_preG_proph :> proph_mapPreG proph val Σ
11
}.
12

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

17
Definition heap_adequacy Σ `{heap_prophPreG Σ} s e σ φ :
18
  ( `{heapG Σ}, WP e @ s;  {{ v, ⌜φ v }}%I) 
19
  adequate s e σ (λ v _, φ v).
20
Proof.
21
  intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
22 23 24 25 26
  iMod (gen_heap_init σ.1) as (?) "Hh".
  iMod (proph_map_init κs σ.2) as (?) "Hp".
  iModIntro.
  iExists (fun σ κs => (gen_heap_ctx σ.1  proph_map_ctx κs σ.2)%I). iFrame.
  iApply (Hwp (HeapG _ _ _ _)).
Ralf Jung's avatar
Ralf Jung committed
27
Qed.