adequacy.v 984 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.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.program_logic Require Import ownership 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 :=
Ralf Jung's avatar
Ralf Jung committed
14
  #[irisΣ heap_lang; 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σ".
Ralf Jung's avatar
Ralf Jung committed
23
  iVs (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.