soundness_unary.v 1.31 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref_conc Require Export fundamental_unary.
Amin Timany's avatar
Amin Timany committed
2 3 4 5 6 7 8 9 10 11 12
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth.

Class heapPreIG Σ := HeapPreIG {
  heap_preG_iris :> invPreG Σ;
  heap_preG_heap :> gen_heapPreG loc F_mu_ref_conc.val Σ
}.

Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
  ( `{heapIG Σ}, []  e : τ) 
Ralf Jung's avatar
Ralf Jung committed
13
  rtc erased_step ([e], σ) (thp, σ')  e'  thp 
Amin Timany's avatar
Amin Timany committed
14 15
  is_Some (to_val e')  reducible e' σ'.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
Ralf Jung's avatar
Ralf Jung committed
17
  eapply (wp_adequacy Σ _). iIntros (Hinv ?).
18
  iMod (gen_heap_init σ) as (Hheap) "Hh".
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
20
  set (HeapΣ := (HeapIG Σ Hinv Hheap)).
Amin Timany's avatar
Amin Timany committed
21
  iApply (wp_wand with "[]").
Amin Timany's avatar
Amin Timany committed
22
  - replace e with e.[env_subst[]] by by asimpl.
Amin Timany's avatar
Amin Timany committed
23 24 25 26 27 28
    iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
  - eauto.
Qed.

Corollary type_soundness e τ e' thp σ σ' :
  []  e : τ 
Ralf Jung's avatar
Ralf Jung committed
29
  rtc erased_step ([e], σ) (thp, σ')  e'  thp 
Amin Timany's avatar
Amin Timany committed
30 31 32 33 34 35
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros ??. set (Σ := #[invΣ ; gen_heapΣ loc F_mu_ref_conc.val]).
  set (HG := HeapPreIG Σ _ _).
  eapply (soundness Σ); eauto using fundamental.
Qed.