adequacy.v 1.2 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.algebra Require Import auth.
3
4
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Import proofmode notation.
5
Set Default Proof Using "Type".
6

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

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

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