safety.v 1.21 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris.heap_lang Require Export adequacy.
2
From tutorial_popl20 Require Export fundamental.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
Lemma sem_gen_type_safety `{heapPreG Σ} e σ φ :
  ( `{heapG Σ},  A : sem_ty Σ, ( v, A v - ⌜φ v)  (  e : A)) 
Amin Timany's avatar
Amin Timany committed
6
7
8
9
10
11
12
13
14
15
  adequate NotStuck e σ (λ v σ, φ v).
Proof.
  intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?.
  specialize (Hty _) as (A & HA & Hty).
  iStartProof. iDestruct (Hty $! ) as "#He".
  iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed.
  rewrite subst_map_empty. iApply (wp_wand with "He"); auto.
  by iIntros; iApply HA.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Lemma sem_type_safety `{heapPreG Σ} e σ es σ' e' :
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
  ( `{heapG Σ},  A,   e : A) 
  rtc erased_step ([e], σ) (es, σ')  e'  es 
  is_Some (to_val e')  reducible e' σ'.
Proof.
Amin Timany's avatar
Amin Timany committed
21
  intros Hty.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
  apply sem_gen_type_safety with (φ := λ _, True)=> // ?.
  specialize (Hty _) as [A Hty]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
29
30
Qed.

Lemma type_safety e σ es σ' e' τ :
  (  e : τ) 
  rtc erased_step ([e], σ) (es, σ')  e'  es 
  is_Some (to_val e')  reducible e' σ'.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  intros Hty. apply (sem_type_safety (Σ:=heapΣ))=> ?.
32
  exists ( τ  []). rewrite -(interp_env_empty []).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
  by apply fundamental.
Qed.