soundness_unary.v 1.39 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 ?).
Amin Timany's avatar
Amin Timany committed
18 19
  iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
Ralf Jung's avatar
Ralf Jung committed
20
  iModIntro. iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
Amin Timany's avatar
Amin Timany committed
21 22
  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
  iApply (wp_wand with "[]").
Amin Timany's avatar
Amin Timany committed
23
  - replace e with e.[env_subst[]] by by asimpl.
Amin Timany's avatar
Amin Timany committed
24 25 26 27 28 29
    iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
  - eauto.
Qed.

Corollary type_soundness e τ e' thp σ σ' :
  []  e : τ 
Ralf Jung's avatar
Ralf Jung committed
30
  rtc erased_step ([e], σ) (thp, σ')  e'  thp 
Amin Timany's avatar
Amin Timany committed
31 32 33 34 35 36
  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.