adequacy.v 976 Bytes
Newer Older
1
2
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap.
3
From iris.algebra Require Import auth.
4
From iris.program_logic Require Import wsat auth.
5
From iris.heap_lang Require Import proofmode notation.
6
From iris.proofmode Require Import tactics.
7

8
9
Class heapPreG Σ := HeapPreG {
  heap_preG_iris :> irisPreG heap_lang Σ;
Ralf Jung's avatar
Ralf Jung committed
10
  heap_preG_heap :> authG Σ heapUR
11
}.
12

13
Definition heapΣ : gFunctors :=
14
  #[irisΣ state; authΣ heapUR].
15
Instance subG_heapPreG {Σ} : subG heapΣ Σ  heapPreG Σ.
Ralf Jung's avatar
Ralf Jung committed
16
Proof. intros [? ?]%subG_inv. split; apply _. Qed.
17
18

Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
19
20
21
22
  ( `{heapG Σ}, heap_ctx  WP e {{ v,  φ v }}) 
  adequate e σ φ.
Proof.
  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
23
  iMod (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
Ralf Jung's avatar
Ralf Jung committed
24
  { exact: to_heap_valid. }
25
26
  set (Hheap := HeapG _ _ _ γ).
  iApply (Hwp _). by rewrite /heap_ctx.
Ralf Jung's avatar
Ralf Jung committed
27
Qed.