demo.v 5.23 KB
 Amin Timany committed Jan 19, 2020 1 ``````From tutorial_popl20 Require Import language. `````` Robbert Krebbers committed Jan 19, 2020 2 3 ``````From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import adequacy. `````` Amin Timany committed Jan 19, 2020 4 `````` `````` Robbert Krebbers committed Jan 19, 2020 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``````(** Plan: 1. HeapLang is a untyped language. We first define a syntactic types and a syntactic typing judgment. Γ ⊢ₜ e : τ 2. Following Derek's talk, we define semantic typing in Iris: Γ ⊨ e : τ 3. We then prove the fundamental theorem: Γ ⊢ₜ e : τ → Γ ⊨ e : τ Every term that is syntactically typed, is also semantically typed 4. We prove safety of semantic typing: `````` Robbert Krebbers committed Jan 19, 2020 24 `````` ∅ ⊨ e : τ → e is safe, i.e. cannot crash `````` Robbert Krebbers committed Jan 19, 2020 25 26 27 28 29 `````` 5. We prove that we get more by showing that certain "unsafe" programs are also semantically typed *) `````` Robbert Krebbers committed Jan 19, 2020 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 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 ``````Inductive ty := | TUnit : ty | TBool : ty | TInt : ty | TProd : ty → ty → ty | TArr : ty → ty → ty | TRef : ty → ty. Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level). Inductive typed : gmap string ty → expr → ty → Prop := (** Variables *) | Var_typed Γ x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ (** Base values *) | UnitV_typed Γ : Γ ⊢ₜ #() : TUnit | BoolV_typed Γ (b : bool) : Γ ⊢ₜ #b : TBool | IntV_val_typed Γ (i : Z) : Γ ⊢ₜ #i : TInt (** Products and sums *) | Pair_typed Γ e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2 | Fst_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1 | Snd_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2 (** Functions *) | Rec_typed Γ f x e τ1 τ2 : binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ) ⊢ₜ e : τ2 → Γ ⊢ₜ Rec f x e : TArr τ1 τ2 | App_typed Γ e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : TArr τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2 (** Heap operations *) | Alloc_typed Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : TRef τ | Load_typed Γ e τ : Γ ⊢ₜ e : TRef τ → Γ ⊢ₜ Load e : τ | Store_typed Γ e1 e2 τ : Γ ⊢ₜ e1 : TRef τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ Store e1 e2 : TUnit (** If *) | If_typed Γ e0 e1 e2 τ : Γ ⊢ₜ e0 : TBool → Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ If e0 e1 e2 : τ where "Γ ⊢ₜ e : τ" := (typed Γ e τ). `````` Amin Timany committed Jan 19, 2020 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 ``````Section semtyp. Context `{!heapG Σ}. Record sem_ty := SemTy { sem_ty_car :> val → iProp Σ; sem_ty_persistent v : Persistent (sem_ty_car v) }. Arguments SemTy _%I {_}. Existing Instance sem_ty_persistent. Fixpoint interp (τ : ty) : sem_ty := match τ with | TUnit => SemTy (λ w, ⌜w = #()⌝) | TBool => SemTy (λ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝) | TInt => SemTy (λ w, ∃ n : Z, ⌜w = #n⌝ ) | TProd τ1 τ2 => SemTy (λ w, ∃ v1 v2, ⌜w = (v1, v2)%V⌝ ∗ interp τ1 v1 ∗ interp τ2 v2) | TArr τ1 τ2 => SemTy (λ w, □ ∀ v, interp τ1 v -∗ WP w v {{ u, interp τ2 u}}) `````` Robbert Krebbers committed Jan 19, 2020 103 104 `````` | TRef τ => SemTy (λ w, ∃ l : loc, ⌜ w = #l ⌝ ∗ inv (nroot .@ "ref" .@ l) (∃ v, l ↦ v ∗ interp τ v)) `````` Amin Timany committed Jan 19, 2020 105 106 107 `````` end%I. Definition interp_env (Γ : gmap string ty) (vs : gmap string val) : iProp Σ := `````` Robbert Krebbers committed Jan 19, 2020 108 `````` [∗ map] τ;v ∈ Γ;vs, interp τ v. `````` Amin Timany committed Jan 19, 2020 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 `````` Definition sem_typed (Γ : gmap string ty) (e : expr) (τ : ty) : iProp Σ := □ ∀ vs, interp_env Γ vs -∗ WP subst_map vs e {{ w, interp τ w }}. Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). Lemma Pair_sem_typed Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Pair e1 e2 : TProd τ1 τ2. Proof. iIntros "#He1 #He2". rewrite /sem_typed. iIntros "!#". iIntros (vs) "#Hvs". simpl. wp_bind (subst_map vs e2). iApply wp_wand. { by iApply "He2". } iIntros (w2) "Hw2". wp_bind (subst_map vs e1). iApply wp_wand. { by iApply "He1". } iIntros (w1) "Hw1". wp_pures. iExists w1, w2. iFrame. auto. Restart. iIntros "#He1 #He2 !#" (vs) "#Hvs /=". wp_apply (wp_wand with "(He2 [\$])"). iIntros (w2) "Hw2". wp_apply (wp_wand with "(He1 [\$])"). iIntros (w1) "Hw1". wp_pures; eauto. Qed. `````` Robbert Krebbers committed Jan 19, 2020 143 144 145 146 147 `````` Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. intros Htyped. iInduction Htyped as [] "IH". 5:{ iApply Pair_sem_typed; auto. } Admitted. `````` Robbert Krebbers committed Jan 19, 2020 148 149 `````` Lemma sem_typed_unsafe_pure : `````` Robbert Krebbers committed Jan 19, 2020 150 `````` ∅ ⊨ (if: #true then #13 else #13 #37) : TInt. `````` Robbert Krebbers committed Jan 19, 2020 151 `````` Proof. `````` Robbert Krebbers committed Jan 19, 2020 152 153 `````` iIntros "!#" (vs) "Hvs /=". wp_pures. auto. Qed. `````` Robbert Krebbers committed Jan 19, 2020 154 ``````End semtyp. `````` Robbert Krebbers committed Jan 19, 2020 155 156 157 158 `````` Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). `````` Amin Timany committed Jan 19, 2020 159 160 161 162 163 164 165 166 ``````Definition safe (e : expr) := ∀ σ es' e' σ', rtc erased_step ([e], σ) (es', σ') → e' ∈ es' → is_Some (to_val e') ∨ reducible e' σ'. Lemma sem_type_safety `{!heapPreG Σ} e τ : (∀ `{!heapG Σ}, ∅ ⊨ e : τ) → safe e. `````` Robbert Krebbers committed Jan 19, 2020 167 ``````Proof. `````` Amin Timany committed Jan 19, 2020 168 `````` intros Hty σ es' e' σ'. `````` Robbert Krebbers committed Jan 19, 2020 169 170 171 172 173 174 175 `````` apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?. iDestruct (Hty \$! ∅) as "#He". rewrite subst_map_empty. iApply (wp_wand with "(He [])"). { rewrite /interp_env. auto. } auto. Qed. `````` Amin Timany committed Jan 19, 2020 176 ``````Lemma type_safety e τ : ∅ ⊢ₜ e : τ → safe e. `````` Robbert Krebbers committed Jan 19, 2020 177 178 179 180 ``````Proof. intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?. by apply fundamental. Qed.``````