soundness_unary.v 1.4 KB
Newer Older
1
From iris_logrel.F_mu_ref_conc Require Export fundamental_unary.
2 3 4 5
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth.

Dan Frumin's avatar
Dan Frumin committed
6 7 8 9
Class heapPreIG Σ := HeapPreIG {
  heap_preG_iris :> invPreG Σ;
  heap_preG_heap :> gen_heapPreG loc val Σ
}.
10

Dan Frumin's avatar
Dan Frumin committed
11
Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
  ( `{heapIG Σ}, log_typed [] e τ) 
  rtc step ([e], σ) (thp, σ')  e'  thp 
14 15
  is_Some (to_val e')  reducible e' σ'.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
Dan Frumin's avatar
Dan Frumin committed
17 18 19 20 21 22 23 24 25 26 27
  eapply (wp_adequacy Σ _). 
  iIntros (Hinv). 
  iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
  - apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)).
  - iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
    set (HΣ := IrisG _ _ Hinv (λ σ, own γ ( to_gen_heap σ))%I).
    iApply wp_wand_r.
    iSplitR. rewrite -(empty_env_subst e).
    set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
    iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
    eauto.
28
Qed.
29

30
Corollary type_soundness e τ e' thp σ σ' :
31
  [] ⊢ₜ e : τ 
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  rtc step ([e], σ) (thp, σ')  e'  thp 
33 34
  is_Some (to_val e')  reducible e' σ'.
Proof.
Dan Frumin's avatar
Dan Frumin committed
35 36
  intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
  set (HG := HeapPreIG Σ _ _). 
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  eapply (soundness Σ); eauto using fundamental.
38
Qed.