From tutorial_popl20 Require Import language. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import adequacy. (** 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: ∅ ⊨ e : τ → e is safe, i.e. cannot crash 5. We prove that we get more by showing that certain "unsafe" programs are also semantically typed *) 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 τ). 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}}) | TRef τ => SemTy (λ w, ∃ l : loc, ⌜ w = #l ⌝ ∗ inv (nroot .@ "ref" .@ l) (∃ v, l ↦ v ∗ interp τ v)) end%I. Definition interp_env (Γ : gmap string ty) (vs : gmap string val) : iProp Σ := [∗ map] τ;v ∈ Γ;vs, interp τ v. 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. Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. intros Htyped. iInduction Htyped as [] "IH". 5:{ iApply Pair_sem_typed; auto. } Admitted. Lemma sem_typed_unsafe_pure : ∅ ⊨ (if: #true then #13 else #13 #37) : TInt. Proof. iIntros "!#" (vs) "Hvs /=". wp_pures. auto. Qed. End semtyp. Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). 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. Proof. intros Hty σ es' e' σ'. 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. Lemma type_safety e τ : ∅ ⊢ₜ e : τ → safe e. Proof. intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?. by apply fundamental. Qed.