safety.v 2.67 KB
 Ralf Jung committed Jan 20, 2020 1 ``````From iris.heap_lang Require Export adequacy. `````` Ralf Jung committed Jan 20, 2020 2 ``````From solutions Require Export fundamental. `````` Ralf Jung committed Jan 20, 2020 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.``````