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

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

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

Ralf Jung's avatar
Ralf Jung committed
17
Definition heap_adequacy Σ `{heapPreG Σ} 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.