adequacy.v 859 Bytes
Newer Older
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
1
From iris.program_logic Require Export weakestpre adequacy.
2
From iris.dist_lang Require Export lifting.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

Class heapPreG Σ := HeapPreG {
  heap_preG_iris :> invPreG Σ;
  heap_preG_heap :> gen_heapPreG loc val Σ
}.

Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ  heapPreG Σ.
Proof. solve_inG. Qed.

Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
  ( `{heapG Σ}, WP e @ s;  {{ v, ⌜φ v }}%I) 
  adequate s e σ φ.
Proof.
  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
  iMod (gen_heap_init σ) as (?) "Hh".
  iModIntro. iExists gen_heap_ctx. iFrame "Hh".
  iApply (Hwp (HeapG _ _ _)).
Qed.