From 9bd2c159258dc542f8dc8bb1985dec6663c220a5 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 25 May 2021 13:16:39 +0200
Subject: [PATCH 1/6] Track uninitialised locals

---
 interpreter/exec/eval.ml     |  35 ++++----
 interpreter/host/spectest.ml |   4 +-
 interpreter/runtime/value.ml |  16 ++--
 interpreter/syntax/types.ml  |   2 +
 interpreter/util/lib.ml      |   6 ++
 interpreter/util/lib.mli     |   1 +
 interpreter/valid/match.ml   |   1 +
 interpreter/valid/valid.ml   | 153 +++++++++++++++++++----------------
 test/core/func.wast          |   7 +-
 test/core/local_get.wast     |  41 +++++++++-
 10 files changed, 169 insertions(+), 97 deletions(-)

diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 9737e71e..a8a84a10 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -49,7 +49,7 @@ type 'a stack = 'a list
 type frame =
 {
   inst : module_inst;
-  locals : value ref list;
+  locals : value option ref list;
 }
 
 type code = value stack * admin_instr list
@@ -74,8 +74,8 @@ type config =
   budget : int;  (* to model stack overflow *)
 }
 
-let frame inst = {inst; locals = []}
-let config inst vs es = {frame = frame inst; code = vs, es; budget = 300}
+let frame inst locals = {inst; locals}
+let config inst vs es = {frame = frame inst []; code = vs, es; budget = 300}
 
 let plain e = Plain e.it @@ e.at
 
@@ -279,14 +279,19 @@ let rec step (c : config) : config =
           v1 :: vs', []
 
       | LocalGet x, vs ->
-        !(local c.frame x) :: vs, []
+        (match !(local c.frame x) with
+        | Some v ->
+          v :: vs, []
+        | None ->
+          Crash.error e.at "read of uninitialized local"
+        )
 
       | LocalSet x, v :: vs' ->
-        local c.frame x := v;
+        local c.frame x := Some v;
         vs', []
 
       | LocalTee x, v :: vs' ->
-        local c.frame x := v;
+        local c.frame x := Some v;
         v :: vs', []
 
       | GlobalGet x, vs ->
@@ -578,9 +583,11 @@ let rec step (c : config) : config =
       vs' @ vs, [e']
 
     | Local (n, vs0, code'), vs ->
-      let frame' = {c.frame with locals = List.map ref vs0 @ c.frame.locals} in
+      let locals = List.map (fun v -> ref (Some v)) vs0 in
+      let frame' = {c.frame with locals = locals @ c.frame.locals} in
       let c' = step {c with frame = frame'; code = code'} in
-      let vs0' = List.map (!) (take (List.length vs0) c'.frame.locals e.at) in
+      let vs0' = List.map (fun loc -> Option.get (!loc))
+        (take (List.length vs0) c'.frame.locals e.at) in
       vs, [Local (n, vs0', c'.code) @@ e.at]
 
     | Frame (n, frame', (vs', [])), vs ->
@@ -605,17 +612,17 @@ let rec step (c : config) : config =
 
     | Invoke f, vs ->
       let FuncType (ts1, ts2) = Func.type_of f in
-      let args, vs' = split (List.length ts1) vs e.at in
+      let n1, n2 = List.length ts1, List.length ts2 in
+      let args, vs' = split n1 vs e.at in
       (match f with
       | Func.AstFunc (_, inst', func) ->
         let {locals; body; _} = func.it in
         let m = Lib.Promise.value inst' in
         let ts = List.map (fun t -> Types.sem_value_type m.types t.it) locals in
-        let vs0 = List.rev args @ List.map default_value ts in
-        let locals' = List.map (fun t -> t @@ func.at) ts1 @ locals in
-        let bt = VarBlockType (SemVar (alloc (FuncDefType (FuncType ([], ts2))))) in
-        let es0 = [Plain (Let (bt, locals', body)) @@ func.at] in
-        vs', [Frame (List.length ts2, frame m, (List.rev vs0, es0)) @@ e.at]
+        let locals' = List.rev (List.map Option.some args) @ List.map default_value ts in
+        let frame' = {inst = m; locals = List.map ref locals'} in
+        let instr' = [Label (n2, [], ([], List.map plain body)) @@ func.at] in
+        vs', [Frame (n2, frame', ([], instr')) @@ e.at]
 
       | Func.HostFunc (_, f) ->
         (try List.rev (f (List.rev args)) @ vs', []
diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml
index 168fb9ff..511c15a3 100644
--- a/interpreter/host/spectest.ml
+++ b/interpreter/host/spectest.ml
@@ -28,10 +28,10 @@ let print_value v =
   Printf.printf "%s : %s\n"
     (string_of_value v) (string_of_value_type (type_of_value v))
 
-let print (FuncType (_, out)) vs =
+let print _ vs =
   List.iter print_value vs;
   flush_all ();
-  List.map default_value out
+  []
 
 
 let lookup name t =
diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml
index c5a5059e..cae5caaf 100644
--- a/interpreter/runtime/value.ml
+++ b/interpreter/runtime/value.ml
@@ -47,18 +47,18 @@ let type_of_value = function
 (* Defaults *)
 
 let default_num = function
-  | I32Type -> I32 I32.zero
-  | I64Type -> I64 I64.zero
-  | F32Type -> F32 F32.zero
-  | F64Type -> F64 F64.zero
+  | I32Type -> Some (Num (I32 I32.zero))
+  | I64Type -> Some (Num (I64 I64.zero))
+  | F32Type -> Some (Num (F32 F32.zero))
+  | F64Type -> Some (Num (F64 F64.zero))
 
 let default_ref = function
-  | (Nullable, t) -> NullRef t
-  | (NonNullable, _) -> assert false
+  | (Nullable, t) -> Some (Ref (NullRef t))
+  | (NonNullable, _) -> None
 
 let default_value = function
-  | NumType t' -> Num (default_num t')
-  | RefType t' -> Ref (default_ref t')
+  | NumType t' -> default_num t'
+  | RefType t' -> default_ref t'
   | BotType -> assert false
 
 
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index afb2bc1c..a201c1bf 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -6,6 +6,7 @@ and syn_var = int32
 and sem_var = def_type Lib.Promise.t
 and var = SynVar of syn_var | SemVar of sem_var
 
+and init = Initialized | Uninitialized
 and nullability = NonNullable | Nullable
 and num_type = I32Type | I64Type | F32Type | F64Type
 and ref_type = nullability * heap_type
@@ -22,6 +23,7 @@ type mutability = Immutable | Mutable
 type table_type = TableType of Int32.t limits * ref_type
 type memory_type = MemoryType of Int32.t limits
 type global_type = GlobalType of value_type * mutability
+type local_type = LocalType of value_type * init
 type extern_type =
   | ExternFuncType of func_type
   | ExternTableType of table_type
diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml
index 23bace33..0285d3c2 100644
--- a/interpreter/util/lib.ml
+++ b/interpreter/util/lib.ml
@@ -137,6 +137,12 @@ struct
     | n, _::xs' when n > 0l -> nth xs' (Int32.sub n 1l)
     | _ -> failwith "nth"
 
+  let rec replace xs n y =
+    match n, xs with
+    | 0l, _::xs' -> y::xs'
+    | n, x::xs' when n > 0l -> x :: replace xs' (Int32.sub n 1l) y
+    | _ -> failwith "replace"
+
   let rec take n xs =
     match n, xs with
     | 0l, _ -> []
diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli
index bde64f1d..e9476b98 100644
--- a/interpreter/util/lib.mli
+++ b/interpreter/util/lib.mli
@@ -34,6 +34,7 @@ sig
   val make : int32 -> 'a -> 'a list
   val length : 'a list -> int32
   val nth : 'a list -> int32 -> 'a (* raises Failure *)
+  val replace : 'a list -> int32 -> 'a -> 'a list (* raises Failure *)
   val take : int32 -> 'a list -> 'a list (* raises Failure *)
   val drop : int32 -> 'a list -> 'a list (* raises Failure *)
   val mapi : (int32 -> 'a -> 'b) -> 'a list -> 'b list
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
index 143b2dc0..a6dc5f24 100644
--- a/interpreter/valid/match.ml
+++ b/interpreter/valid/match.ml
@@ -46,6 +46,7 @@ and eq_value_type c a t1 t2 =
   match t1, t2 with
   | NumType t1', NumType t2' -> eq_num_type c a t1' t2'
   | RefType t1', RefType t2' -> eq_ref_type c a t1' t2'
+  | BotType, BotType -> true
   | _, _ -> false
 
 and eq_result_type c a ts1 ts2 =
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index f40b46ea..5d652ce1 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -24,7 +24,7 @@ type context =
   globals : global_type list;
   elems : ref_type list;
   datas : unit list;
-  locals : value_type list;
+  locals : local_type list;
   results : value_type list;
   labels : result_type list;
   refs : Free.t;
@@ -41,6 +41,10 @@ let lookup category list x =
   try Lib.List32.nth list x.it with Failure _ ->
     error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
 
+let replace category list x y =
+  try Lib.List32.replace list x.it y with Failure _ ->
+    error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
+
 let type_ (c : context) x = lookup "type" c.types x
 let func_var (c : context) x = lookup "function" c.funcs x
 let table (c : context) x = lookup "table" c.tables x
@@ -51,6 +55,9 @@ let data (c : context) x = lookup "data segment" c.datas x
 let local (c : context) x = lookup "local" c.locals x
 let label (c : context) x = lookup "label" c.labels x
 
+let replace_local (c : context) x y =
+  {c with locals = replace "local" c.locals x y}
+
 let func_type (c : context) x =
   match type_ c x with
   | FuncDefType ft -> ft
@@ -283,75 +290,77 @@ let check_block_type (c : context) (bt : block_type) at : func_type =
   | VarBlockType (SynVar x) -> func_type c (x @@ at)
   | VarBlockType (SemVar _) -> assert false
 
-let check_local (c : context) (defaults : bool) (t : local) =
+let check_local (c : context) (defaulted : bool) (t : local) : local_type =
   check_value_type c t.it t.at;
-  require (not defaults || defaultable_value_type t.it) t.at
-    "non-defaultable local type"
+  let init =
+    if not defaulted || defaultable_value_type t.it
+    then Initialized else Uninitialized
+  in LocalType (t.it, init)
 
-let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type =
+let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type * context =
   match e.it with
   | Unreachable ->
-    [] -->... []
+    [] -->... [], c
 
   | Nop ->
-    [] --> []
+    [] --> [], c
 
   | Drop ->
-    [peek 0 s] --> []
+    [peek 0 s] --> [], c
 
   | Select None ->
     let t = peek_num 1 s e.at in
-    [t; t; NumType I32Type] --> [t]
+    [t; t; NumType I32Type] --> [t], c
 
   | Select (Some ts) ->
     require (List.length ts = 1) e.at "invalid result arity other than 1 is not (yet) allowed";
     check_result_type c ts e.at;
-    (ts @ ts @ [NumType I32Type]) --> ts
+    (ts @ ts @ [NumType I32Type]) --> ts, c
 
   | Block (bt, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts2 :: c.labels} es ft e.at;
-    ts1 --> ts2
+    ts1 --> ts2, c
 
   | Loop (bt, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts1 :: c.labels} es ft e.at;
-    ts1 --> ts2
+    ts1 --> ts2, c
 
   | If (bt, es1, es2) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts2 :: c.labels} es1 ft e.at;
     check_block {c with labels = ts2 :: c.labels} es2 ft e.at;
-    (ts1 @ [NumType I32Type]) --> ts2
+    (ts1 @ [NumType I32Type]) --> ts2, c
 
   | Let (bt, locals, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    List.iter (check_local c false) locals;
+    let ts = List.map (check_local c false) locals in
     let c' =
       { c with
         labels = ts2 :: c.labels;
-        locals = List.map Source.it locals @ c.locals;
+        locals = ts @ c.locals;
       }
     in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2
+    (ts1 @ List.map Source.it locals) --> ts2, c
 
   | Br x ->
-    label c x -->... []
+    label c x -->... [], c
 
   | BrIf x ->
-    (label c x @ [NumType I32Type]) --> label c x
+    (label c x @ [NumType I32Type]) --> label c x, c
 
   | BrTable (xs, x) ->
     let n = List.length (label c x) in
     let ts = Lib.List.table n (fun i -> peek (n - i) s) in
     check_stack c ts (label c x) x.at;
     List.iter (fun x' -> check_stack c ts (label c x') x'.at) xs;
-    (ts @ [NumType I32Type]) -->... []
+    (ts @ [NumType I32Type]) -->... [], c
 
   | BrOnNull x ->
     let (_, t) = peek_ref 0 s e.at in
     (label c x @ [RefType (Nullable, t)]) -->
-      (label c x @ [RefType (NonNullable, t)])
+      (label c x @ [RefType (NonNullable, t)]), c
 
   | BrOnNonNull x ->
     let (_, ht) as rt = peek_ref 0 s e.at in
@@ -363,22 +372,22 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_value_type c.types [] t' t) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
        " but label has " ^ string_of_result_type (label c x));
-    (ts0 @ [RefType rt]) --> ts0
+    (ts0 @ [RefType rt]) --> ts0, c
 
   | Return ->
-    c.results -->... []
+    c.results -->... [], c
 
   | Call x ->
     let FuncType (ts1, ts2) = func c x in
-    ts1 --> ts2
+    ts1 --> ts2, c
 
   | CallRef ->
     (match peek_ref 0 s e.at with
     | (nul, DefHeapType (SynVar x)) ->
       let FuncType (ts1, ts2) = func_type c (x @@ e.at) in
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2, c
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... []
+      [RefType rt] -->... [], c
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -391,7 +400,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t (Nullable, FuncHeapType)) x.at
       ("type mismatch: instruction requires table of function type" ^
        " but table has element type " ^ string_of_ref_type t);
-    (ts1 @ [NumType I32Type]) --> ts2
+    (ts1 @ [NumType I32Type]) --> ts2, c
 
   | ReturnCallRef ->
     (match peek_ref 0 s e.at with
@@ -401,9 +410,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
         ("type mismatch: current function requires result type " ^
          string_of_result_type c.results ^
          " but callee returns " ^ string_of_result_type ts2);
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... []
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], c
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... []
+      [RefType rt] -->... [], c
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -421,9 +430,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
       require (match_func_type c.types [] (FuncType (ts12, ts2)) ft') e.at
         "type mismatch in function type";
       (ts11 @ [RefType (nul, DefHeapType (SynVar y))]) -->
-        [RefType (NonNullable, DefHeapType (SynVar x.it))]
+        [RefType (NonNullable, DefHeapType (SynVar x.it))], c
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))]
+      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))], c
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -431,42 +440,46 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     )
 
   | LocalGet x ->
-    [] --> [local c x]
+    let LocalType (t, init) = local c x in
+    require (init = Initialized) x.at "local is uninitialized";
+    [] --> [t], c
 
   | LocalSet x ->
-    [local c x] --> []
+    let LocalType (t, _) = local c x in
+    [t] --> [], replace_local c x (LocalType (t, Initialized))
 
   | LocalTee x ->
-    [local c x] --> [local c x]
+    let LocalType (t, _) = local c x in
+    [t] --> [t], replace_local c x (LocalType (t, Initialized))
 
   | GlobalGet x ->
     let GlobalType (t, _mut) = global c x in
-    [] --> [t]
+    [] --> [t], c
 
   | GlobalSet x ->
     let GlobalType (t, mut) = global c x in
     require (mut = Mutable) x.at "global is immutable";
-    [t] --> []
+    [t] --> [], c
 
   | TableGet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type] --> [RefType t]
+    [NumType I32Type] --> [RefType t], c
 
   | TableSet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t] --> []
+    [NumType I32Type; RefType t] --> [], c
 
   | TableSize x ->
     let _tt = table c x in
-    [] --> [NumType I32Type]
+    [] --> [NumType I32Type], c
 
   | TableGrow x ->
     let TableType (_lim, t) = table c x in
-    [RefType t; NumType I32Type] --> [NumType I32Type]
+    [RefType t; NumType I32Type] --> [NumType I32Type], c
 
   | TableFill x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t; NumType I32Type] --> []
+    [NumType I32Type; RefType t; NumType I32Type] --> [], c
 
   | TableCopy (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -474,7 +487,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: source element type " ^ string_of_ref_type t1 ^
        " does not match destination element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
 
   | TableInit (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -482,103 +495,103 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: element segment's type " ^ string_of_ref_type t1 ^
        " does not match table's element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
 
   | ElemDrop x ->
     ignore (elem c x);
-    [] --> []
+    [] --> [], c
 
   | Load memop ->
     check_memop c memop (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [NumType memop.ty]
+    [NumType I32Type] --> [NumType memop.ty], c
 
   | Store memop ->
     check_memop c memop (fun sz -> sz) e.at;
-    [NumType I32Type; NumType memop.ty] --> []
+    [NumType I32Type; NumType memop.ty] --> [], c
 
   | MemorySize ->
     let _mt = memory c (0l @@ e.at) in
-    [] --> [NumType I32Type]
+    [] --> [NumType I32Type], c
 
   | MemoryGrow ->
     let _mt = memory c (0l @@ e.at) in
-    [NumType I32Type] --> [NumType I32Type]
+    [NumType I32Type] --> [NumType I32Type], c
 
   | MemoryFill ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
 
   | MemoryCopy ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
 
   | MemoryInit x ->
     ignore (memory c (0l @@ e.at));
     ignore (data c x);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
 
   | DataDrop x ->
     ignore (data c x);
-    [] --> []
+    [] --> [], c
 
   | RefNull t ->
     check_heap_type c t e.at;
-    [] --> [RefType (Nullable, t)]
+    [] --> [RefType (Nullable, t)], c
 
   | RefIsNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [NumType I32Type]
+    [RefType (Nullable, t)] --> [NumType I32Type], c
 
   | RefAsNonNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [RefType (NonNullable, t)]
+    [RefType (Nullable, t)] --> [RefType (NonNullable, t)], c
 
   | RefFunc x ->
     let y = func_var c x in
     refer_func c x;
-    [] --> [RefType (NonNullable, DefHeapType (SynVar y))]
+    [] --> [RefType (NonNullable, DefHeapType (SynVar y))], c
 
   | Const v ->
     let t = NumType (type_num v.it) in
-    [] --> [t]
+    [] --> [t], c
 
   | Test testop ->
     let t = NumType (type_testop testop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], c
 
   | Compare relop ->
     let t = NumType (type_relop relop) in
-    [t; t] --> [NumType I32Type]
+    [t; t] --> [NumType I32Type], c
 
   | Unary unop ->
     check_unop unop e.at;
     let t = NumType (type_unop unop) in
-    [t] --> [t]
+    [t] --> [t], c
 
   | Binary binop ->
     let t = NumType (type_binop binop) in
-    [t; t] --> [t]
+    [t; t] --> [t], c
 
   | Convert cvtop ->
     let t1, t2 = type_cvtop e.at cvtop in
-    [NumType t1] --> [NumType t2]
+    [NumType t1] --> [NumType t2], c
 
 and check_seq (c : context) (s : infer_result_type) (es : instr list)
-  : infer_result_type =
+  : infer_result_type * context =
   match es with
   | [] ->
-    s
+    s, c
 
   | _ ->
     let es', e = Lib.List.split_last es in
-    let s' = check_seq c s es' in
-    let {ins; outs} = check_instr c e s' in
-    push c outs (pop c ins s' e.at)
+    let s', c' = check_seq c s es' in
+    let {ins; outs}, c'' = check_instr c' e s' in
+    push c' outs (pop c' ins s' e.at), c''
 
 and check_block (c : context) (es : instr list) (ft : func_type) at =
   let FuncType (ts1, ts2) = ft in
-  let s = check_seq c (stack ts1) es in
-  let s' = pop c (stack ts2) s at in
+  let s, c' = check_seq c (stack ts1) es in
+  let s' = pop c' (stack ts2) s at in
   require (snd s' = []) at
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^
      " but stack has " ^ string_of_result_type (snd s))
@@ -601,10 +614,10 @@ and check_block (c : context) (es : instr list) (ft : func_type) at =
 let check_func (c : context) (f : func) =
   let {ftype; locals; body} = f.it in
   let FuncType (ts1, ts2) = func_type c ftype in
-  List.iter (check_local c true) locals;
+  let ts = List.map (check_local c true) locals in
   let c' =
     { c with
-      locals = ts1 @ List.map Source.it locals;
+      locals = List.map (fun t -> LocalType (t, Initialized)) ts1 @ ts;
       results = ts2;
       labels = [ts2]
     }
diff --git a/test/core/func.wast b/test/core/func.wast
index a5e0ec75..1fc6e779 100644
--- a/test/core/func.wast
+++ b/test/core/func.wast
@@ -666,8 +666,11 @@
 )
 
 (assert_invalid
-  (module (type $t (func)) (func $type-local-no-default (local (ref $t))))
-  "non-defaultable local type"
+  (module
+    (type $t (func))
+    (func $type-local-uninitialized (local $x (ref $t)) (drop (local.get $x)))
+  )
+  "local is uninitialized"
 )
 
 
diff --git a/test/core/local_get.wast b/test/core/local_get.wast
index 6acab398..27c4e83f 100644
--- a/test/core/local_get.wast
+++ b/test/core/local_get.wast
@@ -175,7 +175,7 @@
 )
 
 
-;; local.set should have retval
+;; Invalid result type
 
 (assert_invalid
   (module (func $type-empty-vs-i32 (local i32) (local.get 0)))
@@ -224,3 +224,42 @@
   "unknown local"
 )
 
+
+;; Uninitialized undefaulted locals
+
+(module
+  (func (export "get-after-set") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (local.set $x (local.get $p))
+    (local.get $x)
+  )
+  (func (export "get-after-tee") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (drop (local.tee $x (local.get $p)))
+    (local.get $x)
+  )
+  (func (export "get-in-block-after-set") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (local.set $x (local.get $p))
+    (block (result (ref extern)) (local.get $x))
+  )
+)
+
+(assert_return (invoke "get-after-set" (ref.extern 1)) (ref.extern 1))
+(assert_return (invoke "get-after-tee" (ref.extern 2)) (ref.extern 2))
+(assert_return (invoke "get-in-block-after-set" (ref.extern 3)) (ref.extern 3))
+
+(assert_invalid
+  (module (func $uninit (local $x (ref extern)) (drop (local.get $x))))
+  "local is uninitialized"
+)
+(assert_invalid
+  (module
+    (func $uninit-after-end (param $p (ref extern))
+      (local $x (ref extern))
+      (block (local.set $x (local.get $p)) (drop (local.tee $x (local.get $p))))
+      (drop (local.get $x))
+    )
+  )
+  "local is uninitialized"
+)

From ea5bd117bd3ca7c5268831a1f6fd11d8ff4f2d02 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Thu, 16 Jun 2022 11:44:38 +0200
Subject: [PATCH 2/6] Merge fallout

---
 interpreter/runtime/value.ml |  8 ++++----
 interpreter/valid/valid.ml   | 38 ++++++++++++++++++------------------
 2 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml
index 1683dbd0..e323a1ce 100644
--- a/interpreter/runtime/value.ml
+++ b/interpreter/runtime/value.ml
@@ -139,16 +139,16 @@ let default_num = function
   | F64Type -> Some (Num (F64 F64.zero))
 
 let default_vec = function
-  | V128Type -> V128 V128.zero
+  | V128Type -> Some (Vec (V128 V128.zero))
 
 let default_ref = function
   | (Nullable, t) -> Some (Ref (NullRef t))
   | (NonNullable, _) -> None
 
 let default_value = function
-  | NumType t' -> Num (default_num t')
-  | VecType t' -> Vec (default_vec t')
-  | RefType t' -> Ref (default_ref t')
+  | NumType t' -> default_num t'
+  | VecType t' -> default_vec t'
+  | RefType t' -> default_ref t'
   | BotType -> assert false
 
 
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index eb077b9b..ad654e0e 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -532,23 +532,23 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
 
   | VecLoad memop ->
     check_memop c memop vec_size (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [VecType memop.ty]
+    [NumType I32Type] --> [VecType memop.ty], c
 
   | VecStore memop ->
     check_memop c memop vec_size (fun _ -> None) e.at;
-    [NumType I32Type; VecType memop.ty] --> []
+    [NumType I32Type; VecType memop.ty] --> [], c
 
   | VecLoadLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty]
+    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty], c
 
   | VecStoreLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  []
+    [NumType I32Type; VecType memop.ty] -->  [], c
 
   | MemorySize ->
     let _mt = memory c (0l @@ e.at) in
@@ -620,71 +620,71 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
 
   | VecConst v ->
     let t = VecType (type_vec v.it) in
-    [] --> [t]
+    [] --> [t], c
 
   | VecTest testop ->
     let t = VecType (type_vec testop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], c
 
   | VecUnary unop ->
     let t = VecType (type_vec unop) in
-    [t] --> [t]
+    [t] --> [t], c
 
   | VecBinary binop ->
     check_vec_binop binop e.at;
     let t = VecType (type_vec binop) in
-    [t; t] --> [t]
+    [t; t] --> [t], c
 
   | VecCompare relop ->
     let t = VecType (type_vec relop) in
-    [t; t] --> [t]
+    [t; t] --> [t], c
 
   | VecConvert cvtop ->
     let t = VecType (type_vec cvtop) in
-    [t] --> [t]
+    [t] --> [t], c
 
   | VecShift shiftop ->
     let t = VecType (type_vec shiftop) in
-    [t; NumType I32Type] --> [VecType V128Type]
+    [t; NumType I32Type] --> [VecType V128Type], c
 
   | VecBitmask bitmaskop ->
     let t = VecType (type_vec bitmaskop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], c
 
   | VecTestBits vtestop ->
     let t = VecType (type_vec vtestop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], c
 
   | VecUnaryBits vunop ->
     let t = VecType (type_vec vunop) in
-    [t] --> [t]
+    [t] --> [t], c
 
   | VecBinaryBits vbinop ->
     let t = VecType (type_vec vbinop) in
-    [t; t] --> [t]
+    [t; t] --> [t], c
 
   | VecTernaryBits vternop ->
     let t = VecType (type_vec vternop) in
-    [t; t; t] --> [t]
+    [t; t; t] --> [t], c
 
   | VecSplat splatop ->
     let t1 = type_vec_lane splatop in
     let t2 = VecType (type_vec splatop) in
-    [NumType t1] --> [t2]
+    [NumType t1] --> [t2], c
 
   | VecExtract extractop ->
     let t = VecType (type_vec extractop) in
     let t2 = type_vec_lane extractop in
     require (lane_extractop extractop < num_lanes extractop) e.at
       "invalid lane index";
-    [t] --> [NumType t2]
+    [t] --> [NumType t2], c
 
   | VecReplace replaceop ->
     let t = VecType (type_vec replaceop) in
     let t2 = type_vec_lane replaceop in
     require (lane_replaceop replaceop < num_lanes replaceop) e.at
       "invalid lane index";
-    [t; NumType t2] --> [t]
+    [t; NumType t2] --> [t], c
 
 and check_seq (c : context) (s : infer_result_type) (es : instr list)
   : infer_result_type * context =

From 35500076a1b5293548afd295884334d5875b80bd Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Thu, 16 Jun 2022 12:42:33 +0200
Subject: [PATCH 3/6] Introduce instr_type

---
 interpreter/syntax/types.ml               |   5 +-
 interpreter/valid/valid.ml                | 181 +++++++++++-----------
 proposals/function-references/Overview.md |  65 ++++++++
 3 files changed, 162 insertions(+), 89 deletions(-)

diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 0922833b..0f065b7d 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -1,8 +1,10 @@
 (* Types *)
 
+type type_idx = int32
+type local_idx = int32
 type name = int list
 
-and syn_var = int32
+and syn_var = type_idx
 and sem_var = def_type Lib.Promise.t
 and var = SynVar of syn_var | SemVar of sem_var
 
@@ -17,6 +19,7 @@ and value_type =
   NumType of num_type | VecType of vec_type | RefType of ref_type | BotType
 
 and result_type = value_type list
+and instr_type = result_type * local_idx list
 and func_type = FuncType of result_type * result_type
 and def_type = FuncDefType of func_type
 
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index ad654e0e..1080c56d 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -41,10 +41,6 @@ let lookup category list x =
   try Lib.List32.nth list x.it with Failure _ ->
     error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
 
-let replace category list x y =
-  try Lib.List32.replace list x.it y with Failure _ ->
-    error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
-
 let type_ (c : context) x = lookup "type" c.types x
 let func (c : context) x = lookup "function" c.funcs x
 let table (c : context) x = lookup "table" c.tables x
@@ -55,8 +51,16 @@ let data (c : context) x = lookup "data segment" c.datas x
 let local (c : context) x = lookup "local" c.locals x
 let label (c : context) x = lookup "label" c.labels x
 
-let replace_local (c : context) x y =
-  {c with locals = replace "local" c.locals x y}
+let replace category list x y =
+  try Lib.List32.replace list x.it y with Failure _ ->
+    error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
+
+let init_local (c : context) x =
+  let LocalType (t, _) = local c x in
+  {c with locals = replace "local" c.locals x (LocalType (t, Initialized))}
+
+let init_locals (c : context) xs =
+  List.fold_left init_local c xs
 
 let func_type (c : context) x =
   match type_ c x with
@@ -146,7 +150,8 @@ let check_def_type (c : context) (dt : def_type) at =
 
 type ellipses = NoEllipses | Ellipses
 type infer_result_type = ellipses * value_type list
-type op_type = {ins : infer_result_type; outs : infer_result_type}
+type infer_func_type = {ins : infer_result_type; outs : infer_result_type}
+type infer_instr_type = infer_func_type * idx list
 
 let stack ts = (NoEllipses, ts)
 let (-->) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
@@ -314,45 +319,45 @@ let check_local (c : context) (defaulted : bool) (t : local) : local_type =
     then Initialized else Uninitialized
   in LocalType (t.it, init)
 
-let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type * context =
+let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_instr_type =
   match e.it with
   | Unreachable ->
-    [] -->... [], c
+    [] -->... [], []
 
   | Nop ->
-    [] --> [], c
+    [] --> [], []
 
   | Drop ->
-    [peek 0 s] --> [], c
+    [peek 0 s] --> [], []
 
   | Select None ->
     let t = peek 1 s in
     require (is_num_type t || is_vec_type t) e.at
       ("type mismatch: instruction requires numeric or vector type" ^
        " but stack has " ^ string_of_value_type t);
-    [t; t; NumType I32Type] --> [t], c
+    [t; t; NumType I32Type] --> [t], []
 
   | Select (Some ts) ->
     require (List.length ts = 1) e.at
       "invalid result arity other than 1 is not (yet) allowed";
     check_result_type c ts e.at;
-    (ts @ ts @ [NumType I32Type]) --> ts, c
+    (ts @ ts @ [NumType I32Type]) --> ts, []
 
   | Block (bt, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts2 :: c.labels} es ft e.at;
-    ts1 --> ts2, c
+    ts1 --> ts2, []
 
   | Loop (bt, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts1 :: c.labels} es ft e.at;
-    ts1 --> ts2, c
+    ts1 --> ts2, []
 
   | If (bt, es1, es2) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
     check_block {c with labels = ts2 :: c.labels} es1 ft e.at;
     check_block {c with labels = ts2 :: c.labels} es2 ft e.at;
-    (ts1 @ [NumType I32Type]) --> ts2, c
+    (ts1 @ [NumType I32Type]) --> ts2, []
 
   | Let (bt, locals, es) ->
     let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
@@ -363,25 +368,25 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
         locals = ts @ c.locals;
       }
     in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2, c
+    (ts1 @ List.map Source.it locals) --> ts2, []
 
   | Br x ->
-    label c x -->... [], c
+    label c x -->... [], []
 
   | BrIf x ->
-    (label c x @ [NumType I32Type]) --> label c x, c
+    (label c x @ [NumType I32Type]) --> label c x, []
 
   | BrTable (xs, x) ->
     let n = List.length (label c x) in
     let ts = Lib.List.table n (fun i -> peek (n - i) s) in
     check_stack c ts (label c x) x.at;
     List.iter (fun x' -> check_stack c ts (label c x') x'.at) xs;
-    (ts @ [NumType I32Type]) -->... [], c
+    (ts @ [NumType I32Type]) -->... [], []
 
   | BrOnNull x ->
     let (_, t) = peek_ref 0 s e.at in
     (label c x @ [RefType (Nullable, t)]) -->
-      (label c x @ [RefType (NonNullable, t)]), c
+      (label c x @ [RefType (NonNullable, t)]), []
 
   | BrOnNonNull x ->
     let (_, ht) as rt = peek_ref 0 s e.at in
@@ -393,22 +398,22 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_value_type c.types [] t' t) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
        " but label has " ^ string_of_result_type (label c x));
-    (ts0 @ [RefType rt]) --> ts0, c
+    (ts0 @ [RefType rt]) --> ts0, []
 
   | Return ->
-    c.results -->... [], c
+    c.results -->... [], []
 
   | Call x ->
     let FuncType (ts1, ts2) = func c x in
-    ts1 --> ts2, c
+    ts1 --> ts2, []
 
   | CallRef ->
     (match peek_ref 0 s e.at with
     | (nul, DefHeapType (SynVar x)) ->
       let FuncType (ts1, ts2) = func_type c (x @@ e.at) in
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2, c
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2, []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... [], c
+      [RefType rt] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -421,7 +426,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t (Nullable, FuncHeapType)) x.at
       ("type mismatch: instruction requires table of function type" ^
        " but table has element type " ^ string_of_ref_type t);
-    (ts1 @ [NumType I32Type]) --> ts2, c
+    (ts1 @ [NumType I32Type]) --> ts2, []
 
   | ReturnCallRef ->
     (match peek_ref 0 s e.at with
@@ -431,9 +436,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
         ("type mismatch: current function requires result type " ^
          string_of_result_type c.results ^
          " but callee returns " ^ string_of_result_type ts2);
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], c
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... [], c
+      [RefType rt] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -451,9 +456,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
       require (match_func_type c.types [] (FuncType (ts12, ts2)) ft') e.at
         "type mismatch in function type";
       (ts11 @ [RefType (nul, DefHeapType (SynVar y))]) -->
-        [RefType (NonNullable, DefHeapType (SynVar x.it))], c
+        [RefType (NonNullable, DefHeapType (SynVar x.it))], []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))], c
+      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -463,44 +468,44 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
   | LocalGet x ->
     let LocalType (t, init) = local c x in
     require (init = Initialized) x.at "local is uninitialized";
-    [] --> [t], c
+    [] --> [t], []
 
   | LocalSet x ->
     let LocalType (t, _) = local c x in
-    [t] --> [], replace_local c x (LocalType (t, Initialized))
+    [t] --> [], [x]
 
   | LocalTee x ->
     let LocalType (t, _) = local c x in
-    [t] --> [t], replace_local c x (LocalType (t, Initialized))
+    [t] --> [t], [x]
 
   | GlobalGet x ->
     let GlobalType (t, _mut) = global c x in
-    [] --> [t], c
+    [] --> [t], []
 
   | GlobalSet x ->
     let GlobalType (t, mut) = global c x in
     require (mut = Mutable) x.at "global is immutable";
-    [t] --> [], c
+    [t] --> [], []
 
   | TableGet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type] --> [RefType t], c
+    [NumType I32Type] --> [RefType t], []
 
   | TableSet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t] --> [], c
+    [NumType I32Type; RefType t] --> [], []
 
   | TableSize x ->
     let _tt = table c x in
-    [] --> [NumType I32Type], c
+    [] --> [NumType I32Type], []
 
   | TableGrow x ->
     let TableType (_lim, t) = table c x in
-    [RefType t; NumType I32Type] --> [NumType I32Type], c
+    [RefType t; NumType I32Type] --> [NumType I32Type], []
 
   | TableFill x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t; NumType I32Type] --> [], c
+    [NumType I32Type; RefType t; NumType I32Type] --> [], []
 
   | TableCopy (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -508,7 +513,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: source element type " ^ string_of_ref_type t1 ^
        " does not match destination element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | TableInit (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -516,192 +521,192 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: element segment's type " ^ string_of_ref_type t1 ^
        " does not match table's element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | ElemDrop x ->
     ignore (elem c x);
-    [] --> [], c
+    [] --> [], []
 
   | Load memop ->
     check_memop c memop num_size (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [NumType memop.ty], c
+    [NumType I32Type] --> [NumType memop.ty], []
 
   | Store memop ->
     check_memop c memop num_size (fun sz -> sz) e.at;
-    [NumType I32Type; NumType memop.ty] --> [], c
+    [NumType I32Type; NumType memop.ty] --> [], []
 
   | VecLoad memop ->
     check_memop c memop vec_size (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [VecType memop.ty], c
+    [NumType I32Type] --> [VecType memop.ty], []
 
   | VecStore memop ->
     check_memop c memop vec_size (fun _ -> None) e.at;
-    [NumType I32Type; VecType memop.ty] --> [], c
+    [NumType I32Type; VecType memop.ty] --> [], []
 
   | VecLoadLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty], c
+    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty], []
 
   | VecStoreLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  [], c
+    [NumType I32Type; VecType memop.ty] -->  [], []
 
   | MemorySize ->
     let _mt = memory c (0l @@ e.at) in
-    [] --> [NumType I32Type], c
+    [] --> [NumType I32Type], []
 
   | MemoryGrow ->
     let _mt = memory c (0l @@ e.at) in
-    [NumType I32Type] --> [NumType I32Type], c
+    [NumType I32Type] --> [NumType I32Type], []
 
   | MemoryFill ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | MemoryCopy ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | MemoryInit x ->
     ignore (memory c (0l @@ e.at));
     ignore (data c x);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], c
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | DataDrop x ->
     ignore (data c x);
-    [] --> [], c
+    [] --> [], []
 
   | RefNull t ->
     check_heap_type c t e.at;
-    [] --> [RefType (Nullable, t)], c
+    [] --> [RefType (Nullable, t)], []
 
   | RefIsNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [NumType I32Type], c
+    [RefType (Nullable, t)] --> [NumType I32Type], []
 
   | RefAsNonNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [RefType (NonNullable, t)], c
+    [RefType (Nullable, t)] --> [RefType (NonNullable, t)], []
 
   | RefFunc x ->
     let ft = func c x in
     let y = Lib.Option.force (Lib.List32.index_of (FuncDefType ft) c.types) in
     refer_func c x;
-    [] --> [RefType (NonNullable, DefHeapType (SynVar y))], c
+    [] --> [RefType (NonNullable, DefHeapType (SynVar y))], []
 
   | Const v ->
     let t = NumType (type_num v.it) in
-    [] --> [t], c
+    [] --> [t], []
 
   | Test testop ->
     let t = NumType (type_num testop) in
-    [t] --> [NumType I32Type], c
+    [t] --> [NumType I32Type], []
 
   | Compare relop ->
     let t = NumType (type_num relop) in
-    [t; t] --> [NumType I32Type], c
+    [t; t] --> [NumType I32Type], []
 
   | Unary unop ->
     check_unop unop e.at;
     let t = NumType (type_num unop) in
-    [t] --> [t], c
+    [t] --> [t], []
 
   | Binary binop ->
     let t = NumType (type_num binop) in
-    [t; t] --> [t], c
+    [t; t] --> [t], []
 
   | Convert cvtop ->
     let t1, t2 = type_cvtop e.at cvtop in
-    [NumType t1] --> [NumType t2], c
+    [NumType t1] --> [NumType t2], []
 
   | VecConst v ->
     let t = VecType (type_vec v.it) in
-    [] --> [t], c
+    [] --> [t], []
 
   | VecTest testop ->
     let t = VecType (type_vec testop) in
-    [t] --> [NumType I32Type], c
+    [t] --> [NumType I32Type], []
 
   | VecUnary unop ->
     let t = VecType (type_vec unop) in
-    [t] --> [t], c
+    [t] --> [t], []
 
   | VecBinary binop ->
     check_vec_binop binop e.at;
     let t = VecType (type_vec binop) in
-    [t; t] --> [t], c
+    [t; t] --> [t], []
 
   | VecCompare relop ->
     let t = VecType (type_vec relop) in
-    [t; t] --> [t], c
+    [t; t] --> [t], []
 
   | VecConvert cvtop ->
     let t = VecType (type_vec cvtop) in
-    [t] --> [t], c
+    [t] --> [t], []
 
   | VecShift shiftop ->
     let t = VecType (type_vec shiftop) in
-    [t; NumType I32Type] --> [VecType V128Type], c
+    [t; NumType I32Type] --> [VecType V128Type], []
 
   | VecBitmask bitmaskop ->
     let t = VecType (type_vec bitmaskop) in
-    [t] --> [NumType I32Type], c
+    [t] --> [NumType I32Type], []
 
   | VecTestBits vtestop ->
     let t = VecType (type_vec vtestop) in
-    [t] --> [NumType I32Type], c
+    [t] --> [NumType I32Type], []
 
   | VecUnaryBits vunop ->
     let t = VecType (type_vec vunop) in
-    [t] --> [t], c
+    [t] --> [t], []
 
   | VecBinaryBits vbinop ->
     let t = VecType (type_vec vbinop) in
-    [t; t] --> [t], c
+    [t; t] --> [t], []
 
   | VecTernaryBits vternop ->
     let t = VecType (type_vec vternop) in
-    [t; t; t] --> [t], c
+    [t; t; t] --> [t], []
 
   | VecSplat splatop ->
     let t1 = type_vec_lane splatop in
     let t2 = VecType (type_vec splatop) in
-    [NumType t1] --> [t2], c
+    [NumType t1] --> [t2], []
 
   | VecExtract extractop ->
     let t = VecType (type_vec extractop) in
     let t2 = type_vec_lane extractop in
     require (lane_extractop extractop < num_lanes extractop) e.at
       "invalid lane index";
-    [t] --> [NumType t2], c
+    [t] --> [NumType t2], []
 
   | VecReplace replaceop ->
     let t = VecType (type_vec replaceop) in
     let t2 = type_vec_lane replaceop in
     require (lane_replaceop replaceop < num_lanes replaceop) e.at
       "invalid lane index";
-    [t; NumType t2] --> [t], c
+    [t; NumType t2] --> [t], []
 
 and check_seq (c : context) (s : infer_result_type) (es : instr list)
-  : infer_result_type * context =
+  : infer_result_type * idx list =
   match es with
   | [] ->
-    s, c
+    s, []
 
   | _ ->
     let es', e = Lib.List.split_last es in
-    let s', c' = check_seq c s es' in
-    let {ins; outs}, c'' = check_instr c' e s' in
-    push c' outs (pop c' ins s' e.at), c''
+    let s', xs = check_seq c s es' in
+    let {ins; outs}, xs' = check_instr (init_locals c xs) e s' in
+    push c outs (pop c ins s' e.at), xs @ xs'
 
 and check_block (c : context) (es : instr list) (ft : func_type) at =
   let FuncType (ts1, ts2) = ft in
-  let s, c' = check_seq c (stack ts1) es in
-  let s' = pop c' (stack ts2) s at in
+  let s, xs = check_seq c (stack ts1) es in
+  let s' = pop c (stack ts2) s at in
   require (snd s' = []) at
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^
      " but stack has " ^ string_of_result_type (snd s))
diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index da019d1f..ef66593a 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -199,6 +199,33 @@ The following rules, now defined in terms of heap types, replace and extend the
 * TODO: Table definitions with a type that is not defaultable must have an initialiser value. (Imports are not affected.)
 
 
+#### Local Types
+
+* Locals are now types in the context with types of the following form:
+  - `localtype ::= set? <valtype>`
+  - the flag `set` records that the local has been initialized
+  - all locals with non-defaultable type start out unset
+
+
+#### Instruction Types
+
+* Instructions and instruction sequences are now typed with types of the following form:
+  - `instrtype ::= <functype> <localidx>*`
+  - the local indices record which locals have been set by the instructions
+  - most typing rules except those for locals and for instruction sequences remain unchanged, since the index list is empty
+
+* There is a natural notion of subtyping on instruction types:
+  - `[t1*] -> [t2*] x1*  <:  [t3*] -> [t4*] x2*`
+    - iff `t1* = t0* t1'*`
+    - and `t2* = t0* t2'*`
+    - and `[t1'*] -> [t2'*] <: [t3*] -> [t4*]*`
+    - and `{x2*} subset {x1*}`
+
+* Block types are instruction types with empty index set.
+
+Note: Extending block types to with index sets is a possible extension.
+
+
 ### Instructions
 
 #### Functions
@@ -276,6 +303,44 @@ The rule also implies that let-bound locals are mutable.
 Like all other block instructions, `let` binds a label
 
 
+#### Locals
+
+Typing of local instructions is updated to account for uninitialized locals.
+
+* `local.get $x`
+  - `local.get $x : [] -> [t]`
+    - iff `$x : set t`
+
+* `local.set $x`
+  - `local.set $x : [t] -> [] $x`
+    - iff `$x : set? t`
+
+* `local.tee $x`
+  - `local.tee $x : [t] -> [t] $x`
+    - iff `$x : set? t`
+
+Note: These typing rules do not try to suppress indices for locals that have already been set, but an implementation could.
+
+
+#### Instruction sequences
+
+Typing of instruction sequences is updated to account for initialization of locals.
+
+* `instr1 instr*`
+  - `instr1 instr* : [t1*] -> [t3*] x1* x2*`
+    - iff `instr1 : [t1*] -> [t2*] x1*`
+    - and `instr* : [t2*] -> [t3*] x2*` under a context where `x1*` are changed to `set`
+
+Note: This typing rules does not try to eliminate duplicate indices, but an implementation could.
+
+A weakening rule for instructions allows to go to a supertype:
+
+* `instr`
+  - `instr : [t1*] -> [t2*] x*`
+    - iff `instr : [t1'*] -> [t2'*] x'*`
+    - and `[t1'*] -> [t2'*] x'*  <:  [t1*] -> [t2*] x*`
+
+
 ### Tables
 
 * TODO: Table definitions have an initialiser value: `(table <tabletype> <constexpr>)`

From 444d458a27f9f85965e836a98177b264ea351bb4 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 22 Jul 2022 09:45:03 +0200
Subject: [PATCH 4/6] Tweaks

---
 interpreter/syntax/types.ml               |  8 ++--
 interpreter/valid/valid.ml                |  4 +-
 proposals/function-references/Overview.md | 19 +++++-----
 test/core/func.wast                       | 46 +++++++++++++----------
 test/core/local_get.wast                  |  4 +-
 5 files changed, 45 insertions(+), 36 deletions(-)

diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 0f065b7d..b9766b98 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -2,7 +2,7 @@
 
 type type_idx = int32
 type local_idx = int32
-type name = int list
+type name = Utf8.unicode
 
 and syn_var = type_idx
 and sem_var = def_type Lib.Promise.t
@@ -19,7 +19,7 @@ and value_type =
   NumType of num_type | VecType of vec_type | RefType of ref_type | BotType
 
 and result_type = value_type list
-and instr_type = result_type * local_idx list
+and instr_type = result_type * result_type * local_idx list
 and func_type = FuncType of result_type * result_type
 and def_type = FuncDefType of func_type
 
@@ -212,10 +212,12 @@ let string_of_name n =
   List.iter escape n;
   Buffer.contents b
 
+let string_of_idx x = I32.to_string_u x
+
 let rec string_of_var =
   let inner = ref false in
   function
-  | SynVar x -> I32.to_string_u x
+  | SynVar x -> string_of_idx x
   | SemVar x ->
     if !inner then "..." else
     ( inner := true;
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 1080c56d..80bf0238 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -291,7 +291,7 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  *   e  : instr
  *   es : instr list
  *   v  : value
- *   t  : value_type var
+ *   t  : value_type
  *   ts : result_type
  *   x  : variable
  *
@@ -467,7 +467,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
 
   | LocalGet x ->
     let LocalType (t, init) = local c x in
-    require (init = Initialized) x.at "local is uninitialized";
+    require (init = Initialized) x.at "uninitialized local";
     [] --> [t], []
 
   | LocalSet x ->
diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index ef66593a..5b619f36 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -201,7 +201,7 @@ The following rules, now defined in terms of heap types, replace and extend the
 
 #### Local Types
 
-* Locals are now types in the context with types of the following form:
+* Locals are now recorded in the context with types of the following form:
   - `localtype ::= set? <valtype>`
   - the flag `set` records that the local has been initialized
   - all locals with non-defaultable type start out unset
@@ -223,7 +223,7 @@ The following rules, now defined in terms of heap types, replace and extend the
 
 * Block types are instruction types with empty index set.
 
-Note: Extending block types to with index sets is a possible extension.
+Note: Extending block types with index sets to allow initialization status to last beyond a block's end is a possible extension.
 
 
 ### Instructions
@@ -305,7 +305,7 @@ Like all other block instructions, `let` binds a label
 
 #### Locals
 
-Typing of local instructions is updated to account for uninitialized locals.
+Typing of local instructions is updated to account for the initialization status of locals.
 
 * `local.get $x`
   - `local.get $x : [] -> [t]`
@@ -319,21 +319,22 @@ Typing of local instructions is updated to account for uninitialized locals.
   - `local.tee $x : [t] -> [t] $x`
     - iff `$x : set? t`
 
-Note: These typing rules do not try to suppress indices for locals that have already been set, but an implementation could.
+Note: These typing rules do not try to exclude indices for locals that have already been set, but an implementation could.
 
 
-#### Instruction sequences
+#### Instruction Sequences
 
 Typing of instruction sequences is updated to account for initialization of locals.
 
-* `instr1 instr*`
+* `instr*`
   - `instr1 instr* : [t1*] -> [t3*] x1* x2*`
     - iff `instr1 : [t1*] -> [t2*] x1*`
     - and `instr* : [t2*] -> [t3*] x2*` under a context where `x1*` are changed to `set`
+  - `epsilon : [] -> [] epsilon`
 
-Note: This typing rules does not try to eliminate duplicate indices, but an implementation could.
-
-A weakening rule for instructions allows to go to a supertype:
+Note: These typing rules do not try to eliminate duplicate indices, but an implementation could.
+ 
+A subsumption rule allows to go to a supertype for any instruction:
 
 * `instr`
   - `instr : [t1*] -> [t2*] x*`
diff --git a/test/core/func.wast b/test/core/func.wast
index eebe5522..f2d18cc9 100644
--- a/test/core/func.wast
+++ b/test/core/func.wast
@@ -661,7 +661,7 @@
     (type $t (func))
     (func $type-local-uninitialized (local $x (ref $t)) (drop (local.get $x)))
   )
-  "local is uninitialized"
+  "uninitialized local"
 )
 
 
@@ -961,22 +961,28 @@
 
 ;; Duplicate name errors
 
-(assert_malformed (module quote
-  "(func $foo)"
-  "(func $foo)")
-  "duplicate func")
-(assert_malformed (module quote
-  "(import \"\" \"\" (func $foo))"
-  "(func $foo)")
-  "duplicate func")
-(assert_malformed (module quote
-  "(import \"\" \"\" (func $foo))"
-  "(import \"\" \"\" (func $foo))")
-  "duplicate func")
-
-(assert_malformed (module quote "(func (param $foo i32) (param $foo i32))")
-  "duplicate local")
-(assert_malformed (module quote "(func (param $foo i32) (local $foo i32))")
-  "duplicate local")
-(assert_malformed (module quote "(func (local $foo i32) (local $foo i32))")
-  "duplicate local")
+(assert_malformed
+  (module quote "(func $foo)" "(func $foo)")
+  "duplicate func"
+)
+(assert_malformed
+  (module quote "(import \"\" \"\" (func $foo))" "(func $foo)")
+  "duplicate func"
+)
+(assert_malformed
+  (module quote "(import \"\" \"\" (func $foo))" "(import \"\" \"\" (func $foo))")
+  "duplicate func"
+)
+
+(assert_malformed
+  (module quote "(func (param $foo i32) (param $foo i32))")
+  "duplicate local"
+)
+(assert_malformed
+  (module quote "(func (param $foo i32) (local $foo i32))")
+  "duplicate local"
+)
+(assert_malformed
+  (module quote "(func (local $foo i32) (local $foo i32))")
+  "duplicate local"
+)
diff --git a/test/core/local_get.wast b/test/core/local_get.wast
index 27c4e83f..b56aeec3 100644
--- a/test/core/local_get.wast
+++ b/test/core/local_get.wast
@@ -251,7 +251,7 @@
 
 (assert_invalid
   (module (func $uninit (local $x (ref extern)) (drop (local.get $x))))
-  "local is uninitialized"
+  "uninitialized local"
 )
 (assert_invalid
   (module
@@ -261,5 +261,5 @@
       (drop (local.get $x))
     )
   )
-  "local is uninitialized"
+  "uninitialized local"
 )

From 8519712628c616644242435dacd7f145609716bd Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 22 Jul 2022 10:14:16 +0200
Subject: [PATCH 5/6] Remove let

---
 interpreter/binary/decode.ml    |  9 +---
 interpreter/binary/encode.ml    |  2 -
 interpreter/exec/eval.ml        | 27 +----------
 interpreter/syntax/ast.ml       |  1 -
 interpreter/syntax/free.ml      |  3 --
 interpreter/syntax/operators.ml |  1 -
 interpreter/text/arrange.ml     |  3 --
 interpreter/text/parser.mly     | 83 ++++-----------------------------
 interpreter/valid/valid.ml      | 11 -----
 9 files changed, 10 insertions(+), 130 deletions(-)

diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 2e66bfc8..4134e893 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -322,14 +322,7 @@ let rec instr s =
   | 0x15 -> return_call_ref
   | 0x16 -> func_bind (at var s)
 
-  | 0x17 ->
-    let bt = block_type s in
-    let locs = locals s in
-    let es = instr_block s in
-    end_ s;
-    let_ bt locs es
-
-  | 0x18 | 0x19 as b -> illegal s pos b
+  | 0x17 | 0x18 | 0x19 as b -> illegal s pos b
 
   | 0x1a -> drop
   | 0x1b -> select None
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 1553dc71..fb76434f 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -189,8 +189,6 @@ struct
       op 0x04; block_type bt; list instr es1;
       if es2 <> [] then op 0x05;
       list instr es2; end_ ()
-    | Let (bt, locs, es) ->
-      op 0x17; block_type bt; locals locs; list instr es; end_ ()
 
     | Br x -> op 0x0c; var x
     | BrIf x -> op 0x0d; var x
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 9b12a590..b74c3ea0 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -64,7 +64,6 @@ and admin_instr' =
   | ReturningInvoke of value stack * func_inst
   | Breaking of int32 * value stack
   | Label of int * instr list * code
-  | Local of int * value list * code
   | Frame of int * frame * code
 
 type config =
@@ -184,16 +183,6 @@ let rec step (c : config) : config =
         else
           vs', [Plain (Block (bt, es1)) @@ e.at]
 
-      | Let (bt, locals, es'), vs ->
-        let vs0, vs' = split (List.length locals) vs e.at in
-        let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
-        let vs1, vs2 = split (List.length ts1) vs' e.at in
-        vs2, [
-          Local (List.length ts2, List.rev vs0,
-            (vs1, [Plain (Block (bt, es')) @@ e.at])
-          ) @@ e.at
-        ]
-
       | Br x, vs ->
         [], [Breaking (x.it, vs) @@ e.at]
 
@@ -694,20 +683,6 @@ let rec step (c : config) : config =
       let c' = step {c with code = code'} in
       vs, [Label (n, es0, c'.code) @@ e.at]
 
-    | Local (n, vs0, (vs', [])), vs ->
-      vs' @ vs, []
-
-    | Local (n, vs0, (vs', e' :: es')), vs when is_jumping e' ->
-      vs' @ vs, [e']
-
-    | Local (n, vs0, code'), vs ->
-      let locals = List.map (fun v -> ref (Some v)) vs0 in
-      let frame' = {c.frame with locals = locals @ c.frame.locals} in
-      let c' = step {c with frame = frame'; code = code'} in
-      let vs0' = List.map (fun loc -> Option.get (!loc))
-        (take (List.length vs0) c'.frame.locals e.at) in
-      vs, [Local (n, vs0', c'.code) @@ e.at]
-
     | Frame (n, frame', (vs', [])), vs ->
       vs' @ vs, []
 
@@ -737,7 +712,7 @@ let rec step (c : config) : config =
         let {locals; body; _} = func.it in
         let m = Lib.Promise.value inst' in
         let ts = List.map (fun t -> Types.sem_value_type m.types t.it) locals in
-        let locals' = List.rev (List.map Option.some args) @ List.map default_value ts in
+        let locals' = List.(rev (map Option.some args) @ map default_value ts) in
         let frame' = {inst = m; locals = List.map ref locals'} in
         let instr' = [Label (n2, [], ([], List.map plain body)) @@ func.at] in
         vs', [Frame (n2, frame', ([], instr')) @@ e.at]
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index bba6d72c..8d0e00c9 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -148,7 +148,6 @@ and instr' =
   | Block of block_type * instr list  (* execute in sequence *)
   | Loop of block_type * instr list   (* loop header *)
   | If of block_type * instr list * instr list   (* conditional *)
-  | Let of block_type * local list * instr list  (* local bindings *)
   | Br of idx                         (* break to n-th surrounding label *)
   | BrIf of idx                       (* conditional break *)
   | BrTable of idx list * idx         (* indexed break *)
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index f597b28f..556542b6 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -108,9 +108,6 @@ let rec instr (e : instr) =
   | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
   | Block (bt, es) | Loop (bt, es) -> block_type bt ++ block es
   | If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
-  | Let (bt, ts, es) ->
-    let free = block_type bt ++ block es in
-    {free with locals = Lib.Fun.repeat (List.length ts) shift free.locals}
   | Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
   | BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
   | Return | CallRef | ReturnCallRef -> empty
diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml
index bae67b07..33b739c4 100644
--- a/interpreter/syntax/operators.ml
+++ b/interpreter/syntax/operators.ml
@@ -21,7 +21,6 @@ let select t = Select t
 let block bt es = Block (bt, es)
 let loop bt es = Loop (bt, es)
 let if_ bt es1 es2 = If (bt, es1, es2)
-let let_ bt ts es = Let (bt, ts, es)
 
 let br x = Br x
 let br_if x = BrIf x
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 18a0a871..d4e86874 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -448,9 +448,6 @@ let rec instr e =
     | If (bt, es1, es2) ->
       "if", block_type bt @
         [Node ("then", list instr es1); Node ("else", list instr es2)]
-    | Let (bt, locals, es) ->
-      "let", block_type bt @ decls "local" (List.map Source.it locals) @
-        list instr es
     | Br x -> "br " ^ var x, []
     | BrIf x -> "br_if " ^ var x, []
     | BrTable (xs, x) ->
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index c1feb01a..b6f0e48b 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -142,19 +142,6 @@ let force_locals (c : context) =
   List.fold_right Stdlib.(@@) !(c.deferred_locals) ();
   c.deferred_locals := []
 
-let merge_locals (c : context) (c' : context) at =
-  force_locals c';  (* check that there aren't too many locals locally *)
-  if VarMap.is_empty c'.locals.map then
-    defer_locals c (fun () -> bind "local" c.locals c'.locals.count at)
-  else
-  (
-    force_locals c;
-    let n = c.locals.count in
-    ignore (bind "local" c.locals c'.locals.count at);
-    c.locals.map <- VarMap.union (fun x i1 i2 -> Some i1)
-      c.locals.map (scoped "local" n c'.locals at).map
-  )
-
 
 let lookup category space x =
   try VarMap.find x.it space.map
@@ -241,7 +228,7 @@ let inline_func_type_explicit (c : context) x ft at =
 %token NAT INT FLOAT STRING VAR
 %token NUM_TYPE VEC_TYPE VEC_SHAPE FUNCREF EXTERNREF REF EXTERN NULL MUT
 %token UNREACHABLE NOP DROP SELECT
-%token BLOCK END IF THEN ELSE LOOP LET
+%token BLOCK END IF THEN ELSE LOOP
 %token BR BR_IF BR_TABLE BR_ON_NULL BR_ON_NON_NULL
 %token CALL CALL_REF CALL_INDIRECT RETURN RETURN_CALL_REF FUNC_BIND
 %token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET
@@ -623,10 +610,6 @@ block_instr :
   | IF labeling_opt block ELSE labeling_end_opt instr_list END labeling_end_opt
     { fun c -> let c' = $2 c ($5 @ $8) in
       let ts, es1 = $3 c' in if_ ts es1 ($6 c') }
-  | LET labeling_opt let_block END labeling_end_opt
-    { let at = at () in
-      fun c -> let c' = enter_let ($2 c $5) at in
-      let ts, ls, es = $3 c c' in let_ ts ls es }
 
 block :
   | type_use block_param_body
@@ -658,59 +641,6 @@ block_result_body :
       FuncType (ins, snd $3 c @ out), es }
 
 
-let_block :
-  | type_use let_block_param_body
-    { let at = at () in
-      fun c c' -> let ft, ls, es = $2 c c' in
-      let x = inline_func_type_explicit c ($1 c type_) ft at in
-      VarBlockType (SynVar x.it), ls, es }
-  | let_block_param_body  /* Sugar */
-    { let at = at () in
-      fun c c' -> let ft, ls, es = $1 c c' in
-      let bt =
-        match ft with
-        | FuncType ([], []) -> ValBlockType None
-        | FuncType ([], [t]) -> ValBlockType (Some t)
-        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it)
-      in bt, ls, es }
-
-let_block_param_body :
-  | let_block_result_body { $1 }
-  | LPAR PARAM value_type_list RPAR let_block_param_body
-    { fun c c' ->
-      let FuncType (ins, out), ls, es = $5 c c' in
-      FuncType (snd $3 c @ ins, out), ls, es }
-
-let_block_result_body :
-  | let_block_local_body
-    { let at = at () in
-      fun c c' -> let ls, es = $1 c c' at in FuncType ([], []), ls, es }
-  | LPAR RESULT value_type_list RPAR let_block_result_body
-    { fun c c' ->
-      let FuncType (ins, out), ls, es = $5 c c' in
-      FuncType (ins, snd $3 c @ out), ls, es }
-
-let_block_local_body :
-  | instr_list
-    { fun c c' at -> merge_locals c' c at; [], $1 c' }
-  | LPAR LOCAL local_type_list RPAR let_block_local_body
-    { let at3 = ati 3 in let at4 = ati 4 in
-      fun c c' at -> ignore (anon_locals c' (fst $3) at3);
-      let at' = {left = at.left; right = at4.right} in
-      let ls, es = $5 c c' at' in snd $3 c @ ls, es }
-  | LPAR LOCAL bind_var local_type RPAR let_block_local_body  /* Sugar */
-    { let at5 = ati 5 in
-      fun c c' at -> ignore (bind_local c' $3);
-      let at' = {left = at.left; right = at5.right} in
-      let ls, es = $6 c c' at' in $4 c :: ls, es }
-
-local_type :
-  | value_type { let at = at () in fun c -> $1 c @@ at }
-
-local_type_list :
-  | /* empty */ { 0l, fun c -> [] }
-  | local_type local_type_list { I32.add (fst $2) 1l, fun c -> $1 c :: snd $2 c }
-
 expr :  /* Sugar */
   | LPAR expr1 RPAR
     { let at = at () in fun c -> let es, e' = $2 c in es @ [e' @@ at] }
@@ -733,10 +663,6 @@ expr1 :  /* Sugar */
   | IF labeling_opt if_block
     { fun c -> let c' = $2 c [] in
       let bt, (es, es1, es2) = $3 c c' in es, if_ bt es1 es2 }
-  | LET labeling_opt let_block
-    { let at = at () in
-      fun c -> let c' = enter_let ($2 c []) at in
-      let bt, ls, es = $3 c c' in [], let_ bt ls es }
 
 select_expr_results :
   | LPAR RESULT value_type_list RPAR select_expr_results
@@ -900,6 +826,13 @@ func_body :
     { fun c -> ignore (bind_local c $3); let f = $6 c in
       {f with locals = $4 c :: f.locals} }
 
+local_type :
+  | value_type { let at = at () in fun c -> $1 c @@ at }
+
+local_type_list :
+  | /* empty */ { 0l, fun c -> [] }
+  | local_type local_type_list { I32.add (fst $2) 1l, fun c -> $1 c :: snd $2 c }
+
 
 /* Tables, Memories & Globals */
 
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 80bf0238..2872cbcf 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -359,17 +359,6 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     check_block {c with labels = ts2 :: c.labels} es2 ft e.at;
     (ts1 @ [NumType I32Type]) --> ts2, []
 
-  | Let (bt, locals, es) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    let ts = List.map (check_local c false) locals in
-    let c' =
-      { c with
-        labels = ts2 :: c.labels;
-        locals = ts @ c.locals;
-      }
-    in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2, []
-
   | Br x ->
     label c x -->... [], []
 

From 0204c1422ed03ab65365e3b8ff8bb1849ec7da54 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 22 Jul 2022 12:37:14 +0200
Subject: [PATCH 6/6] Remove let from overview as well

---
 proposals/function-references/Overview.md | 27 ++---------------------
 1 file changed, 2 insertions(+), 25 deletions(-)

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index bef287e6..4a5fcafb 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -8,7 +8,7 @@ The proposal distinguished regular and nullable function reference. The former c
 
 The proposal has instructions for producing and consuming (calling) function references. It also includes instruction for testing and converting between regular and nullable references.
 
-Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialisation, the proposal also introduces a new instruction `let` for block-scoped locals whose initialisation values are taken from the operand stack.
+Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialisation, the proposal also tracks the initialisation status of locals during validation.
 
 
 ### Motivation
@@ -36,7 +36,7 @@ Typed references have no canonical default value, because they cannot be null. T
 
 * Refine the instruction `ref.func $f` to return a typed function reference
 
-* Add a block instruction `let (local t*) ... end` for introducing locals with block scope, in order to handle reference types without default initialisation values
+* Track initialisation status of locals during validation and only allow `local.get` after a `local.set/tee` in the same or a surrounding block.
 
 * Add an optional initialiser expression to table definitions, for element types that do not have an implicit default value.
 
@@ -242,28 +242,6 @@ Note: Extending block types with index sets to allow initialization status to la
 * Note: `ref.is_null` already exists via the [reference types proposal](https://github.com/WebAssembly/reference-types)
 
 
-#### Local Bindings
-
-* `let <blocktype> (local <valtype>)* <instr>* end` locally binds operands to variables
-  - `let bt (local t)* instr* end : [t1* t*] -> [t2*]`
-    - iff `bt = [t1*] -> [t2*]`
-    - and `instr* : bt` under a context with `locals` extended with `t*` and `labels` extended with `[t2*]`
-
-Note: The latter condition implies that inside the body of the `let`, its locals are prepended to the list of locals. Nesting multiple `let` blocks hence addresses them relatively, similar to labels. Function-level local declarations can be viewed as syntactic sugar for a bunch of zero constant instructions and a `let` wrapping the function body. That is,
-```
-(func ... (local t)* ...)
-```
-is equivalent to
-```
-(func ... (t.default)* (let (local t)* ...))
-```
-where `(t.default)` is `(t.const 0)` for numeric types `t`, and `(ref.null)` for reference types.
-
-The rule also implies that let-bound locals are mutable.
-
-Like all other block instructions, `let` binds a label
-
-
 #### Locals
 
 Typing of local instructions is updated to account for the initialization status of locals.
@@ -339,7 +317,6 @@ The opcode for heap types is encoded as an `s33`.
 | ------ | ------------------------ | ---------- |
 | 0x14   | `call_ref`               |            |
 | 0x15   | `return_call_ref`        |            |
-| 0x17   | `let <bt> <locals>`      | `bt : blocktype, locals : (as in functions)` |
 | 0xd3   | `ref.as_non_null`        |            |
 | 0xd4   | `br_on_null $l`          | `$l : u32` |
 | 0xd6   | `br_on_non_null $l`      | `$l : u32` |