demo.v 5.23 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From tutorial_popl20 Require Import language.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import adequacy.
Amin Timany's avatar
Amin Timany committed
4

Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
24
     ∅ ⊨ e : τ  →  e is safe, i.e. cannot crash
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29

5. We prove that we get more by showing that certain "unsafe" programs are also
   semantically typed
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Amin Timany committed
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's avatar
Robbert Krebbers committed
103 104
    | TRef τ => SemTy (λ w,  l : loc,
        w = #l   inv (nroot .@ "ref" .@ l) ( v, l  v  interp τ v))
Amin Timany's avatar
Amin Timany committed
105 106 107
    end%I.

  Definition interp_env (Γ : gmap string ty) (vs : gmap string val) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
108
    [ map] τ;v  Γ;vs, interp τ v.
Amin Timany's avatar
Amin Timany committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
148 149

  Lemma sem_typed_unsafe_pure :
Robbert Krebbers's avatar
Robbert Krebbers committed
150
      (if: #true then #13 else #13 #37) : TInt.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153
    iIntros "!#" (vs) "Hvs /=". wp_pures. auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
End semtyp.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158

Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
  (at level 74, e, A at next level).

Amin Timany's avatar
Amin Timany committed
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's avatar
Robbert Krebbers committed
167
Proof.
Amin Timany's avatar
Amin Timany committed
168
  intros Hty σ es' e' σ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Amin Timany committed
176
Lemma type_safety e τ :   e : τ  safe e.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180
Proof.
  intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?.
  by apply fundamental.
Qed.