Commit e46aa078 authored by Robbert Krebbers's avatar Robbert Krebbers

Add missing heap_lang/adequacy.

parent 5e5e90ea
Pipeline #2562 failed with stage
in 3 minutes and 9 seconds
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap.
From iris.program_logic Require Import auth ownership.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics weakestpre.
Definition heapGF : gFunctorList := [authGF heapUR; irisGF heap_lang].
Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ :
( `{heapG Σ}, heap_ctx WP e {{ v, φ v }})
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iVs (auth_alloc (ownP of_heap) heapN _ (to_heap σ) with "[Hσ]") as (γ) "[??]".
- auto using to_heap_valid.
- rewrite /= (from_to_heap σ); auto.
- iApply (Hwp (HeapG _ _ _ γ)). by rewrite /heap_ctx.
Qed.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment