total_adequacy.v 790 Bytes
Newer Older
1
From iris.proofmode Require Import tactics.
2
3
4
5
6
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

7
Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
Ralf Jung's avatar
Ralf Jung committed
8
  ( `{!heapG Σ},  inv_heap_inv - WP e @ s;  [{ v, ⌜φ v }]) 
9
  sn erased_step ([e], σ).
10
Proof.
Ralf Jung's avatar
Ralf Jung committed
11
  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
Ralf Jung's avatar
Ralf Jung committed
12
  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
Ralf Jung's avatar
Ralf Jung committed
13
  iMod (inv_heap_init loc val) as (?) ">Hi".
14
  iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
Ralf Jung's avatar
Ralf Jung committed
15
  iModIntro.
16
17
  iExists
    (λ σ κs _, (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I),
18
    (λ _, True%I); iFrame.
Ralf Jung's avatar
Ralf Jung committed
19
  iApply (Hwp (HeapG _ _ _ _ _)). done.
20
Qed.