adequacy.v 1.07 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
4
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import proph_map.
5
From iris.proofmode Require Import tactics.
6
Set Default Proof Using "Type".
7

Ralf Jung's avatar
Ralf Jung committed
8
9
10
Class heapPreG Σ := HeapPreG {
  heap_preG_iris :> invPreG Σ;
  heap_preG_heap :> gen_heapPreG loc val Σ;
11
  heap_preG_proph :> proph_mapPreG proph_id val Σ
12
}.
13

14
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
Ralf Jung's avatar
Ralf Jung committed
15
Instance subG_heapPreG {Σ} : subG heapΣ Σ  heapPreG Σ.
16
Proof. solve_inG. Qed.
17

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