safety.v 2.67 KB
Newer Older
1
From iris.heap_lang Require Export adequacy.
Ralf Jung's avatar
Ralf Jung committed
2
From solutions Require Export fundamental.
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

(** * Semantic and syntactic type safety *)
(** We prove *semantic type safety*, which says that any _closed_ expression
that is semantically typed is safe, i.e., it does not crash. Based on this
theorem we then prove *syntactic type safety* as a corollary, i.e., any _closed_ syntactically well-typed program is safe. Semantic type safety is a consequence
of Iris's adequacy theorem, and syntactic type safety is a consequence of the
fundamental theorem together and semantic type safety. *)

(** ** Semantic type safety *)
(** Before proving semantic type safety, we first prove a stronger lemma. We
use this lemma in the file [parametricity.v] to prove parametricity properties.
This stronger lemma states that given a closed program [e], heap [σ], and a
_Coq_ predicate [φ : val → Prop], if there is a semantic type [A] such that [A]
implies [φ], and [e] is semantically typed at type [A], then we have
[adequate NotStuck e σ (λ v σ, φ v)].

The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in the
Iris library) means that [e], starting in heap [σ] does not get stuck, and if
[e] reduces to a value [v], we have [φ v]. *)
Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ :
  ( `{!heapG Σ},  A : sem_ty Σ, ( v, A v - ⌜φ v)  (  e : A)%I) 
  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.

(** The actual theorem for semantic type safety lemma states that semantically
typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
  ( `{!heapG Σ},  A, (  e : A)%I) 
  rtc erased_step ([e], σ) (es, σ')  e'  es 
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros Hty.
  apply sem_gen_type_safety with (φ := λ _, True)=> // ?.
  specialize (Hty _) as [A Hty]; eauto.
Qed.

(** ** Syntactic type safety *)
(** Syntactic type safety is a consequence of the fundamental theorem together
and semantic type safety. *)
Corollary type_safety e σ es σ' e' τ :
  (  e : τ) 
  rtc erased_step ([e], σ) (es, σ')  e'  es 
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros Hty. apply (sem_type_safety (Σ:=heapΣ))=> ?.
  exists ( τ  []). rewrite -(interp_env_empty []).
  by apply fundamental.
Qed.