total_adequacy.v 544 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

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