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 01/11] 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 02/11] 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 03/11] 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 ca3bd3d6a0df08d5c28b7a49614726fee9015eff Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 20 Jun 2022 11:56:14 +0200
Subject: [PATCH 04/11] More tests

---
 interpreter/binary/decode.ml              |  12 +-
 interpreter/binary/encode.ml              |  11 +-
 interpreter/exec/eval.ml                  |   8 +-
 interpreter/script/js.ml                  |   2 +-
 interpreter/syntax/ast.ml                 |   4 +-
 interpreter/syntax/free.ml                |   4 +-
 interpreter/syntax/types.ml               |   5 +-
 interpreter/text/arrange.ml               |  10 +-
 interpreter/text/lexer.mll                |   1 +
 interpreter/text/parser.mly               |  71 ++-
 interpreter/util/lib.ml                   |   4 +
 interpreter/util/lib.mli                  |   1 +
 interpreter/valid/valid.ml                | 117 ++--
 proposals/function-references/Overview.md | 103 +++-
 test/core/func.wast                       |  47 +-
 test/core/local-block-set.wast            | 697 ++++++++++++++++++++++
 test/core/local_get.wast                  |   4 +-
 17 files changed, 975 insertions(+), 126 deletions(-)
 create mode 100644 test/core/local-block-set.wast

diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 2e66bfc8..9ab6ced8 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -249,10 +249,16 @@ let memop s =
   Int32.to_int align, offset
 
 let block_type s =
+  let xs =
+    either [
+      (fun s -> expect 0x41 s ""; vec (at var));
+      (fun s -> fun _ -> []);
+    ] s s
+  in
   either [
-    (fun s -> VarBlockType (var_type s));
-    (fun s -> expect 0x40 s ""; ValBlockType None);
-    (fun s -> ValBlockType (Some (value_type s)));
+    (fun s -> VarBlockType (var_type s, xs));
+    (fun s -> expect 0x40 s ""; ValBlockType (None, xs));
+    (fun s -> ValBlockType (Some (value_type s), xs));
   ] s
 
 let local s =
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 1553dc71..656e6e00 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -165,10 +165,13 @@ struct
   let var x = u32 x.it
 
   let block_type = function
-    | ValBlockType None -> s33 (-0x40l)
-    | ValBlockType (Some t) -> value_type t
-    | VarBlockType (SynVar x) -> s33 x
-    | VarBlockType (SemVar _) -> assert false
+    | ValBlockType (None, []) -> s33 (-0x40l)
+    | ValBlockType (Some t, []) -> value_type t
+    | VarBlockType (SynVar x, []) -> s33 x
+    | ValBlockType (None, xs) -> s33 (-0x3fl); vec var xs; s33 (-0x40l)
+    | ValBlockType (Some t, xs) -> s33 (-0x3fl); vec var xs; value_type t
+    | VarBlockType (SynVar x, xs) -> s33 (-0x3fl); vec var xs; s33 x
+    | VarBlockType (SemVar _, _) -> assert false
 
   let local (t, n) = len n; value_type t.it
 
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 9b12a590..068cf1f3 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -111,10 +111,10 @@ let func_ref inst x i at =
 
 let block_type inst bt at =
   match bt with
-  | ValBlockType None -> FuncType ([], [])
-  | ValBlockType (Some t) -> FuncType ([], [t])
-  | VarBlockType (SynVar x) -> func_type inst (x @@ at)
-  | VarBlockType (SemVar x) -> as_func_def_type (def_of x)
+  | ValBlockType (None, _) -> FuncType ([], [])
+  | ValBlockType (Some t, _) -> FuncType ([], [t])
+  | VarBlockType (SynVar x, _) -> func_type inst (x @@ at)
+  | VarBlockType (SemVar x, _) -> as_func_def_type (def_of x)
 
 let take n (vs : 'a stack) at =
   try Lib.List.take n vs with Failure _ -> Crash.error at "stack underflow"
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index 23f3bb65..854a9d22 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -427,7 +427,7 @@ let wrap item_name wrap_action wrap_assertion at =
   let edesc = FuncExport item @@ at in
   let exports = [{name = Utf8.decode "run"; edesc} @@ at] in
   let body =
-    [ Block (ValBlockType None, action @ assertion @ [Return @@ at]) @@ at;
+    [ Block (ValBlockType (None, []), action @ assertion @ [Return @@ at]) @@ at;
       Unreachable @@ at ]
   in
   let funcs = [{ftype = 0l @@ at; locals; body} @@ at] in
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index bba6d72c..f3aa0cdb 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -137,7 +137,9 @@ type name = Utf8.unicode
 type local = local' Source.phrase
 and local' = value_type
 
-type block_type = VarBlockType of var | ValBlockType of value_type option
+type block_type =
+  | VarBlockType of var * idx list
+  | ValBlockType of value_type option * idx list
 
 type instr = instr' Source.phrase
 and instr' =
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index f597b28f..ac31305f 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -95,8 +95,8 @@ let def_type = function
   | FuncDefType ft -> func_type ft
 
 let block_type = function
-  | VarBlockType x -> var_type x
-  | ValBlockType t -> opt value_type t
+  | VarBlockType (x, xs) -> var_type x ++ list (fun x -> locals (idx x)) xs
+  | ValBlockType (t, xs) -> opt value_type t ++ list (fun x -> locals (idx x)) xs
 
 let rec instr (e : instr) =
   match e.it with
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 0f065b7d..fff3fce4 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,8 @@ 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 label_type = result_type * local_idx Source.phrase list
+and instr_type = func_type * local_idx Source.phrase list
 and func_type = FuncType of result_type * result_type
 and def_type = FuncDefType of func_type
 
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 18a0a871..7ee1e858 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -429,10 +429,14 @@ let vec v = string_of_vec v.it
 let constop v = num_type (type_of_num v) ^ ".const"
 let vec_constop v = vec_type (type_of_vec v) ^ ".const i32x4"
 
+let inits = function
+  | [] -> []
+  | xs -> [Node ("set " ^ String.concat " " (list var xs), [])]
+
 let block_type = function
-  | VarBlockType (SynVar x) -> [Node ("type " ^ nat32 x, [])]
-  | VarBlockType (SemVar _) -> assert false
-  | ValBlockType ts -> decls "result" (list_of_opt ts)
+  | VarBlockType (SynVar x, xs) -> Node ("type " ^ nat32 x, []) :: inits xs
+  | VarBlockType (SemVar _, _) -> assert false
+  | ValBlockType (ts, xs) -> decls "result" (list_of_opt ts) @ inits xs
 
 let rec instr e =
   let head, inner =
diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll
index 4678dd37..864a1015 100644
--- a/interpreter/text/lexer.mll
+++ b/interpreter/text/lexer.mll
@@ -152,6 +152,7 @@ rule token = parse
       | "ref" -> REF
       | "null" -> NULL
       | "mut" -> MUT
+      | "set" -> SET
 
       | "nop" -> NOP
       | "unreachable" -> UNREACHABLE
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index c1feb01a..6aae073e 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -241,7 +241,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 LET SET
 %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
@@ -631,31 +631,38 @@ block_instr :
 block :
   | type_use block_param_body
     { let at1 = ati 1 in
-      fun c -> let ft, es = $2 c in
+      fun c -> let ft, xs, es = $2 c in
       let x = inline_func_type_explicit c ($1 c type_) ft at1 in
-      VarBlockType (SynVar x.it), es }
+      VarBlockType (SynVar x.it, xs), es }
   | block_param_body  /* Sugar */
     { let at = at () in
-      fun c -> let ft, es = $1 c in
+      fun c -> let ft, xs, es = $1 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)
+        | FuncType ([], []) -> ValBlockType (None, xs)
+        | FuncType ([], [t]) -> ValBlockType (Some t, xs)
+        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it, xs)
       in bt, es }
 
 block_param_body :
   | block_result_body { $1 }
   | LPAR PARAM value_type_list RPAR block_param_body
-    { fun c -> let FuncType (ins, out), es = $5 c in
-      FuncType (snd $3 c @ ins, out), es }
+    { fun c -> let FuncType (ins, out), xs, es = $5 c in
+      FuncType (snd $3 c @ ins, out), xs, es }
 
 block_result_body :
-  | instr_list { fun c -> FuncType ([], []), $1 c }
+  | block_set_body
+    { fun c -> let xs, es = $1 c in
+      FuncType ([], []), xs, es }
   | LPAR RESULT value_type_list RPAR block_result_body
-    { fun c ->
-      let FuncType (ins, out), es = $5 c in
-      FuncType (ins, snd $3 c @ out), es }
+    { fun c -> let FuncType (ins, out), xs, es = $5 c in
+      FuncType (ins, snd $3 c @ out), xs, es }
+
+block_set_body :
+  | instr_list { fun c -> [], $1 c }
+  | LPAR SET var_list RPAR block_set_body
+    { fun c -> let xs, es = $5 c in
+      $3 c local @ xs, es }
 
 
 let_block :
@@ -663,15 +670,15 @@ let_block :
     { 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 }
+      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)
+        | 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 :
@@ -772,32 +779,40 @@ call_expr_results :
 if_block :
   | type_use if_block_param_body
     { let at = at () in
-      fun c c' -> let ft, es = $2 c c' in
+      fun c c' -> let ft, xs, es = $2 c c' in
       let x = inline_func_type_explicit c ($1 c type_) ft at in
-      VarBlockType (SynVar x.it), es }
+      VarBlockType (SynVar x.it, xs), es }
   | if_block_param_body  /* Sugar */
     { let at = at () in
-      fun c c' -> let ft, es = $1 c c' in
+      fun c c' -> let ft, xs, 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)
+        | FuncType ([], []) -> ValBlockType (None, xs)
+        | FuncType ([], [t]) -> ValBlockType (Some t, xs)
+        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it, xs)
       in bt, es }
 
 if_block_param_body :
   | if_block_result_body { $1 }
   | LPAR PARAM value_type_list RPAR if_block_param_body
     { fun c c' ->
-      let FuncType (ins, out), es = $5 c c' in
-      FuncType (snd $3 c @ ins, out), es }
+      let FuncType (ins, out), xs, es = $5 c c' in
+      FuncType (snd $3 c @ ins, out), xs, es }
 
 if_block_result_body :
-  | if_ { fun c c' -> FuncType ([], []), $1 c c' }
+  | if_block_set_body
+    { fun c c' -> let xs, es = $1 c c' in
+      FuncType ([], []), xs, es }
   | LPAR RESULT value_type_list RPAR if_block_result_body
     { fun c c' ->
-      let FuncType (ins, out), es = $5 c c' in
-      FuncType (ins, snd $3 c @ out), es }
+      let FuncType (ins, out), xs, es = $5 c c' in
+      FuncType (ins, snd $3 c @ out), xs, es }
+
+if_block_set_body :
+  | if_ { fun c c' -> [], $1 c c' }
+  | LPAR SET var_list RPAR if_block_set_body
+    { fun c c' -> let xs, es = $5 c c' in
+      $3 c local @ xs, es }
 
 if_ :
   | expr if_
diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml
index 1a4ce425..2cd5b402 100644
--- a/interpreter/util/lib.ml
+++ b/interpreter/util/lib.ml
@@ -129,6 +129,10 @@ struct
   and make' n x xs =
     if n = 0l then xs else make' (Int32.sub n 1l) x (x::xs)
 
+  let rec table n f = table' n f []
+  and table' n f xs =
+    if n = 0l then xs else table' (Int32.sub n 1l) f (f (Int32.sub n 1l) :: xs)
+
   let rec length xs = length' xs 0l
   and length' xs n =
     match xs with
diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli
index 164d4d9a..772332e2 100644
--- a/interpreter/util/lib.mli
+++ b/interpreter/util/lib.mli
@@ -33,6 +33,7 @@ end
 module List32 :
 sig
   val make : int32 -> 'a -> 'a list
+  val table : int32 -> (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 *)
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 1080c56d..a73a5953 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -26,7 +26,7 @@ type context =
   datas : unit list;
   locals : local_type list;
   results : value_type list;
-  labels : result_type list;
+  labels : label_type list;
   refs : Free.t;
 }
 
@@ -55,12 +55,16 @@ 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 all_locals (c : context) =
+  Lib.List32.table (Lib.List32.length c.locals) (fun x -> x @@ no_region)
+
 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 init_locals (c : context) xs poly =
+  List.fold_left init_local c (if poly then all_locals c else xs)
+
 
 let func_type (c : context) x =
   match type_ c x with
@@ -157,6 +161,7 @@ let stack ts = (NoEllipses, ts)
 let (-->) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
 let (-->..) ts1 ts2 = {ins = Ellipses, ts1; outs = NoEllipses, ts2}
 let (-->...) ts1 ts2 = {ins = Ellipses, ts1; outs = Ellipses, ts2}
+let poly (ell, _) = (ell = Ellipses)
 
 let check_stack (c : context) ts1 ts2 at =
   require
@@ -305,12 +310,15 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  * declarative typing rules.
  *)
 
-let check_block_type (c : context) (bt : block_type) at : func_type =
-  match bt with
-  | ValBlockType None -> FuncType ([], [])
-  | ValBlockType (Some t) -> check_value_type c t at; FuncType ([], [t])
-  | VarBlockType (SynVar x) -> func_type c (x @@ at)
-  | VarBlockType (SemVar _) -> assert false
+let check_block_type (c : context) (bt : block_type) at : instr_type =
+  let ft, xs =
+    match bt with
+    | ValBlockType (None, xs) -> FuncType ([], []), xs
+    | ValBlockType (Some t, xs) -> check_value_type c t at; FuncType ([], [t]), xs
+    | VarBlockType (SynVar x, xs) -> func_type c (x @@ at), xs
+    | VarBlockType (SemVar _, _) -> assert false
+  in
+  ft, List.map (fun x -> ignore (local c x); x) xs
 
 let check_local (c : context) (defaulted : bool) (t : local) : local_type =
   check_value_type c t.it t.at;
@@ -319,6 +327,13 @@ let check_local (c : context) (defaulted : bool) (t : local) : local_type =
     then Initialized else Uninitialized
   in LocalType (t.it, init)
 
+and check_init (c : context) (xs : idx list) at =
+  List.iter (fun x ->
+    let LocalType (_, init) = local c x in
+    require (init = Initialized) at
+      ("uninitialized local " ^ I32.to_string_u x.it ^ " at branch or block end")
+  ) xs
+
 let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_instr_type =
   match e.it with
   | Unreachable ->
@@ -344,60 +359,73 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (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, []
+    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
+    check_block {c with labels = (ts2, xs) :: c.labels} es it e.at;
+    ts1 --> ts2, xs
 
   | 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, []
+    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
+    check_block {c with labels = (ts1, []) :: c.labels} es it e.at;
+    ts1 --> ts2, xs
 
   | 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, []
+    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
+    check_block {c with labels = (ts2, xs) :: c.labels} es1 it e.at;
+    check_block {c with labels = (ts2, xs) :: c.labels} es2 it e.at;
+    (ts1 @ [NumType I32Type]) --> ts2, xs
 
   | Let (bt, locals, es) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
+    let FuncType (ts1, ts2), xs as it = 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;
+        labels = (ts2, xs) :: c.labels;
         locals = ts @ c.locals;
       }
-    in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2, []
+    in check_block c' es it e.at;
+    (ts1 @ List.map Source.it locals) --> ts2, xs
 
   | Br x ->
-    label c x -->... [], []
+    let ts, xs = label c x in
+    check_init c xs x.at;
+    ts -->... [], []
 
   | BrIf x ->
-    (label c x @ [NumType I32Type]) --> label c x, []
+    let ts, xs = label c x in
+    check_init c xs x.at;
+    (ts @ [NumType I32Type]) --> ts, []
 
   | 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]) -->... [], []
+    let ts, ys = label c x in
+    let n = List.length ts in
+    let ts' = Lib.List.table n (fun i -> peek (n - i) s) in
+    check_init c ys x.at;
+    check_stack c ts' ts x.at;
+    List.iter (fun x' ->
+      let ts'', ys' = label c x' in
+      check_init c ys' x'.at;
+      check_stack c ts' ts'' x'.at
+    ) xs;
+    (ts' @ [NumType I32Type]) -->... [], []
 
   | BrOnNull x ->
+    let ts, xs = label c x in
     let (_, t) = peek_ref 0 s e.at in
-    (label c x @ [RefType (Nullable, t)]) -->
-      (label c x @ [RefType (NonNullable, t)]), []
+    check_init c xs x.at;
+    (ts @ [RefType (Nullable, t)]) --> (ts @ [RefType (NonNullable, t)]), []
 
   | BrOnNonNull x ->
+    let ts, xs = label c x in
     let (_, ht) as rt = peek_ref 0 s e.at in
     let t' = RefType (NonNullable, ht) in
-    require (label c x <> []) e.at
+    check_init c xs x.at;
+    require (ts <> []) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
-    let ts0, t = Lib.List.split_last (label c x) in
+       " but label has " ^ string_of_result_type ts);
+    let ts0, t = Lib.List.split_last ts in
     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));
+       " but label has " ^ string_of_result_type ts);
     (ts0 @ [RefType rt]) --> ts0, []
 
   | Return ->
@@ -467,7 +495,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 ->
@@ -700,13 +728,14 @@ and check_seq (c : context) (s : infer_result_type) (es : instr list)
   | _ ->
     let es', e = Lib.List.split_last es in
     let s', xs = check_seq c s es' in
-    let {ins; outs}, xs' = check_instr (init_locals c xs) e s' in
+    let {ins; outs}, xs' = check_instr (init_locals c xs (poly s')) 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, xs = check_seq c (stack ts1) es in
+and check_block (c : context) (es : instr list) (it : instr_type) at =
+  let FuncType (ts1, ts2), xs = it in
+  let s, xs' = check_seq c (stack ts1) es in
   let s' = pop c (stack ts2) s at in
+  check_init (init_locals c xs' (poly s')) xs at;
   require (snd s' = []) at
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^
      " but stack has " ^ string_of_result_type (snd s))
@@ -734,9 +763,9 @@ let check_func (c : context) (f : func) =
     { c with
       locals = List.map (fun t -> LocalType (t, Initialized)) ts1 @ ts;
       results = ts2;
-      labels = [ts2]
+      labels = [(ts2, [])]
     }
-  in check_block c' body (FuncType ([], ts2)) f.at
+  in check_block c' body (FuncType ([], ts2), []) f.at
 
 
 let is_const (c : context) (e : instr) =
@@ -751,7 +780,7 @@ let is_const (c : context) (e : instr) =
 let check_const (c : context) (const : const) (t : value_type) =
   require (List.for_all (is_const c) const.it) const.at
     "constant expression required";
-  check_block c const.it (FuncType ([], [t])) const.at
+  check_block c const.it (FuncType ([], [t]), []) const.at
 
 
 (* Tables, Memories, & Globals *)
diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index ef66593a..628b04b3 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -207,10 +207,22 @@ The following rules, now defined in terms of heap types, replace and extend the
   - all locals with non-defaultable type start out unset
 
 
+#### Result Types
+
+* Result types are refined to the following form:
+  - `resulttype ::= [<valtype>*] <localidx>*`
+  - the local indices record which locals have been set as a side effect
+
+* There is a natural notion of subtyping on result types:
+  - `[t1*] x1*  <:  [t2*] x2*`
+    - iff `(t1 <: t2)*`
+    - and `{x2*} subset {x1*}`
+
+
 #### Instruction Types
 
 * Instructions and instruction sequences are now typed with types of the following form:
-  - `instrtype ::= <functype> <localidx>*`
+  - `instrtype ::= [<valtype>*] -> <resulttype>`
   - 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
 
@@ -218,12 +230,22 @@ The following rules, now defined in terms of heap types, replace and extend the
   - `[t1*] -> [t2*] x1*  <:  [t3*] -> [t4*] x2*`
     - iff `t1* = t0* t1'*`
     - and `t2* = t0* t2'*`
-    - and `[t1'*] -> [t2'*] <: [t3*] -> [t4*]*`
-    - and `{x2*} subset {x1*}`
+    - and `(t3 <: t1')*`
+    - and `[t2'*] x1* <: [t4*] x2*`
+
 
-* Block types are instruction types with empty index set.
+#### Block Types
 
-Note: Extending block types to with index sets is a possible extension.
+* Block types denote [instruction types](#instruction-types). For that purpose, they are likewise extended with a (possibly empty) sequence of local indices
+  - `blocktype ::= (<valtype> | <typeidx>) <localidx>*`
+    - `t x* == [] -> [t] x*` iff `t ok` and `(x ok)*`
+    - `$t x* == [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
+
+
+#### Label Types
+
+* Labels are now typed as result types:
+  - `labeltype ::= <resulttype>`
 
 
 ### Instructions
@@ -319,21 +341,23 @@ 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*`
-  - `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`
+* `instr*`
+  - `instr* instrN : [t1*] -> [t3*] x1* x2*`
+    - iff `instr* : [t1*] -> [t2*] x1*`
+    - and `instrN : [t2*] -> [t3*] x2*` under a context where `x1*` are changed to `set`
+  - `epsilon : [] -> [] x*`
+    - iff `(x : set t)*`
 
 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:
+A subsumption rule allows to go to a supertype for any instruction:
 
 * `instr`
   - `instr : [t1*] -> [t2*] x*`
@@ -341,6 +365,49 @@ A weakening rule for instructions allows to go to a supertype:
     - and `[t1'*] -> [t2'*] x'*  <:  [t1*] -> [t2*] x*`
 
 
+#### Blocks
+
+The block types ascribed to blocks declare the instruction type of the respective body's instruction sequence.
+
+* `block bt <instr>* end`
+  - `block $l bt <instr>* end : bt`
+    - iff `<instr>* : bt` assuming `$l : [t2*] x*`
+    - where `bt == [t1*] -> [t2*] x*`
+
+* `loop bt <instr>* end`
+  - `loop $l bt <instr>* end : bt`
+    - iff `<instr>* : bt` assuming `$l : [t1*]`
+    - where `bt == [t1*] -> [t2*] x*`
+
+* `if bt <instr1>* else <instr2>* end`
+  - `if $l bt <instr1>* else <instr2>* end : bt`
+    - iff `<instr1>* : bt` assuming `$l : [t2*] x*`
+    - and `<instr2>* : bt` assuming `$l : [t2*] x*`
+    - where `bt == [t1*] -> [t2*] x*`
+
+
+#### Branches
+
+Branches need to match the respective label type. Moreover, stack polymorphism now entails an arbitrary index set.
+
+* `br $l`
+  - `br $l : [t1* t*] -> [t2*] x2*`
+    - iff `$l : [t*] x*`
+    - and `(x : set tX)*`
+
+* `br_if $l`
+  - `br_if $l : [t* i32] -> [t*]`
+    - iff `$l : [t*] x*`
+    - and `(x : set tX)*`
+
+* `br_table $l* $l'`
+  - `br_table $l* $l' : [t'* i32] -> [t'*]`
+    - iff `$l' : [t'*] x'*`
+    - and `(x' : set tX')*`
+    - and `($l : [t*] x*)*`
+    - and `(x : set tX)*`
+
+
 ### Tables
 
 * TODO: Table definitions have an initialiser value: `(table <tabletype> <constexpr>)`
@@ -371,6 +438,18 @@ The opcode for heap types is encoded as an `s33`.
 | -0x10  | `func`          |            |
 | -0x11  | `extern`        |            |
 
+#### Block Types
+
+The opcode for block types is encoded as an `s33`.
+
+| Opcode | Type            | Parameters | Note |
+| ------ | --------------- | ---------- | ---- |
+| -0x40  | `[] -> []`      |            |      |
+| -0x3f  | `<ft> <idx>*`   | `idx* : vec(u32)`, `ft : blocktype` | `ft` must not be `-0x3f` |
+| i < 0  | `valtype`       |            |      |
+| i >= 0 | `$t`            |            |      |
+
+
 ### Instructions
 
 | Opcode | Instruction              | Immediates |
diff --git a/test/core/func.wast b/test/core/func.wast
index eebe5522..b844d4a6 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"
 )
 
 
@@ -959,24 +959,31 @@
   "unexpected token"
 )
 
+
 ;; 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-block-set.wast b/test/core/local-block-set.wast
new file mode 100644
index 00000000..52cb6c0a
--- /dev/null
+++ b/test/core/local-block-set.wast
@@ -0,0 +1,697 @@
+;; Syntax
+
+(module
+  (func (export "syntax")
+    (local $y1 i64)
+    (local $y2 i32)
+
+    (block (set))
+    (block $l (set))
+    (block (param) (set))
+    (block $l (param) (set))
+    (block (result) (set))
+    (block $l (result) (set))
+    (block (param) (result) (set))
+    (block $l (param) (result) (set))
+
+    (block $l (set $y1))
+    (block $l (set $y1 $y2))
+    (block $l (set $y1 $y1 0 1))
+    (block $l (set 0 $y1) (set $y1 $y2))
+
+    (i32.const 1)
+    (block $l (param i32) (result i64) (set $y1 $y2) (br $l (i64.const 3)))
+    (drop)
+
+    block (set) end
+    block $l (set) end
+    block (param) (set) end
+    block $l (param) (set) end
+    block (result) (set) end
+    block $l (result) (set) end
+    block (param) (result) (set) end
+    block $l (param) (result) (set) end
+
+    block $l (set $y1) end
+    block $l (set $y1 $y2) end
+    block $l (set $y1 $y1 0 1) end
+    block $l (set 0 $y1) (set $y1 $y2) end
+
+    (i32.const 1)
+    block $l (param i32) (result i64) (set $y1 $y2) (br $l (i64.const 3)) end
+    (drop)
+
+    (loop (set))
+    (loop $l (set))
+    (loop (param) (set))
+    (loop $l (param) (set))
+    (loop (result) (set))
+    (loop $l (result) (set))
+    (loop (param) (result) (set))
+    (loop $l (param) (result) (set))
+
+    (loop $l (set $y1))
+    (loop $l (set $y1 $y2))
+    (loop $l (set $y1 $y1 0 1))
+    (loop $l (set 0 $y1) (set $y1 $y2))
+
+    (i32.const 1)
+    (loop $l (param i32) (result i64) (set $y1 $y2) (i64.extend_i32_u))
+    (drop)
+
+    loop (set) end
+    loop $l (set) end
+    loop (param) (set) end
+    loop $l (param) (set) end
+    loop (result) (set) end
+    loop $l (result) (set) end
+    loop (param) (result) (set) end
+    loop $l (param) (result) (set) end
+
+    loop $l (set $y1) end
+    loop $l (set $y1 $y2) end
+    loop $l (set $y1 $y1 0 1) end
+    loop $l (set 0 $y1) (set $y1 $y2) end
+
+    (i32.const 1)
+    loop $l (param i32) (result i64) (set $y1 $y2) (i64.extend_i32_u) end
+    (drop)
+
+    (i32.const 1)
+    (if (set) (then))
+    (i32.const 1)
+    (if $l (set) (then))
+    (i32.const 1)
+    (if (param) (set) (then))
+    (i32.const 1)
+    (if $l (param) (set) (then))
+    (i32.const 1)
+    (if (result) (set) (then))
+    (i32.const 1)
+    (if $l (result) (set) (then))
+    (i32.const 1)
+    (if (param) (result) (set) (then))
+    (i32.const 1)
+    (if $l (param) (result) (set) (then))
+
+    (i32.const 1)
+    (if $l (set $y1) (then))
+    (i32.const 1)
+    (if $l (set $y1 $y2) (then))
+    (i32.const 1)
+    (if $l (set $y1 $y1 0 1) (then))
+    (i32.const 1)
+    (if $l (set 0 $y1) (set $y1 $y2) (then))
+
+    (i32.const 1)
+    (i32.const 1)
+    (if $l (param i32) (result i64) (set $y1 $y2)
+      (then (i64.extend_i32_s))
+      (else (br $l (i64.const 4)))
+    )
+    (drop)
+
+    (i32.const 1)
+    if (set) else end
+    (i32.const 1)
+    if $l (set) end
+    (i32.const 1)
+    if (param) (set) else end
+    (i32.const 1)
+    if $l (param) (set) end
+    (i32.const 1)
+    if (result) (set) else end
+    (i32.const 1)
+    if $l (result) (set) end
+    (i32.const 1)
+    if (param) (result) (set) else end
+    (i32.const 1)
+    if $l (param) (result) (set) end
+
+    (i32.const 1)
+    if $l (set $y1) else end
+    (i32.const 1)
+    if $l (set $y1 $y2) end
+    (i32.const 1)
+    if $l (set $y1 $y1 0 1) else end
+    (i32.const 1)
+    if $l (set 0 $y1) (set $y1 $y2) else end
+
+    (i32.const 1)
+    (i32.const 1)
+    if $l (param i32) (result i64) (set $y1 $y2)
+      (br $l (i64.const 3))
+    else
+      (i64.extend_i32_u)
+    end
+    (drop)
+  )
+)
+
+(assert_return (invoke "syntax"))
+
+
+(assert_malformed
+  (module quote "(func (block (set) (param)))")
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func"
+    "  (local i32)"
+    "  (i32.const 0) (i32.const 0)"
+    "  (block (set 0) (param i32) (drop))"
+    ")"
+  )
+  "unexpected token"
+)
+
+(assert_malformed
+  (module quote "(func (block (set) (result)))")
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func (result i32)"
+    "  (local i32)"
+    "  (i32.const 0)"
+    "  (block (set 0) (result i32) (local.get 0))"
+    ")"
+  )
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func (result i32)"
+    "  (local $x i32)"
+    "  (block (set $x) (result i32) (local.get 0))"
+    ")"
+  )
+  "unexpected token"
+)
+
+(assert_malformed
+  (module quote "(func (block (set) $l))")
+  "unexpected token"
+)
+
+
+;; Typing
+
+(module
+  (type $t (func))
+  (func $f)
+  (elem declare func $f)
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (block (set $x)
+        (local.set $x (ref.func $f))
+      )
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (block (set $x)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (br $l)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (i32.const 0)
+        (br_table $l $l)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (unreachable)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (local.set $x (ref.func $f))
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (loop (set $x)
+        (local.set $x (ref.func $f))
+      )
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (loop (set $x)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (br $l)
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (i32.const 0)
+      (br_table $l $l)
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (unreachable)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (i32.const 1)
+    (if (set $x)
+      (then
+        (local.set $x (ref.func $f))
+        (drop (local.get $x))
+      )
+      (else
+        (local.set $x (ref.func $f))
+        (drop (local.get $x))
+      )
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (i32.const 1)
+    (if (set $x)
+      (then
+        (block (set $x)
+          (local.set $x (ref.func $f))
+        )
+        (drop (local.get $x))
+      )
+      (else
+        (block (set $x)
+          (local.set $x (ref.func $f))
+        )
+        (drop (local.get $x))
+      )
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x)
+      (then (drop (local.get $x)))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (br $l)
+          (drop (local.get $x))
+        )
+        (else
+          (br $l)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (i32.const 0)
+          (br_table $l $l)
+          (drop (local.get $x))
+        )
+        (else
+          (i32.const 0)
+          (br_table $l $l)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (unreachable)
+          (drop (local.get $x))
+        )
+        (else
+          (unreachable)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+
+  (elem declare func $pow)
+  (type $pow (func (param $x i64) (param $n i32) (result i64)))
+  (func $pow (export "pow") (param $x i64) (param $n i32) (result i64)
+    (local $y i64)
+    (local $recurse (ref $pow))
+    (local.set $y
+      (if (result i64) (i32.and (local.get $n) (i32.const 1))
+        (then (local.get $x)) (else (i64.const 1))
+      )
+    )
+    (i64.mul
+      (block (result i64) (set $recurse)
+        (local.set $recurse (ref.func $pow))
+        (local.get $y)
+      )
+      (if (result i64) (i32.le_u (local.get $n) (i32.const 1))
+        (then (i64.const 1))
+        (else
+          (call_ref
+            (i64.mul (local.get $x) (local.get $x))
+            (i32.shr_u (local.get $n) (i32.const 1))
+            (local.get $recurse)
+          )
+        )
+      )
+    )
+  )
+)
+
+(assert_return (invoke "pow" (i64.const 17) (i32.const 0)) (i64.const 1))
+(assert_return (invoke "pow" (i64.const 19) (i32.const 1)) (i64.const 19))
+(assert_return (invoke "pow" (i64.const 11) (i32.const 2)) (i64.const 121))
+(assert_return (invoke "pow" (i64.const 13) (i32.const 3)) (i64.const 2197))
+(assert_return (invoke "pow" (i64.const 2) (i32.const 4)) (i64.const 16))
+(assert_return (invoke "pow" (i64.const 3) (i32.const 5)) (i64.const 243))
+(assert_return (invoke "pow" (i64.const 5) (i32.const 6)) (i64.const 15625))
+(assert_return (invoke "pow" (i64.const 7) (i32.const 7)) (i64.const 823543))
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (func
+      (local $x (ref $t))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (func
+      (local $x (ref $t))
+      (block
+        (local.get $x)
+        (drop)
+      )
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (local.set $x (ref.func $f)))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (set $x)
+        (block (local.set $x (ref.func $f)))
+      )
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (set $x))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (loop (set $x))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (if (set $x) (then (local.set $x (ref.func $f))))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (if (set $x) (then) (else (local.set $x (ref.func $f))))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_if $l)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_table 1 1 $l 1)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_table 1 1 $l)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized 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 8f353b60c7a38fdd123b45ef94b34735902839bc Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 20 Jun 2022 12:42:38 +0200
Subject: [PATCH 05/11] Minor refactor

---
 interpreter/exec/eval.ml    |  2 +-
 interpreter/script/run.ml   |  4 +-
 interpreter/syntax/types.ml | 28 +++++++++----
 interpreter/valid/match.ml  |  6 +--
 interpreter/valid/match.mli |  6 +--
 interpreter/valid/valid.ml  | 81 +++++++++++++++++++------------------
 6 files changed, 69 insertions(+), 58 deletions(-)

diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 068cf1f3..2e6acfce 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -660,7 +660,7 @@ let rec step (c : config) : config =
 
       | _ ->
         let s1 = string_of_values (List.rev vs) in
-        let s2 = string_of_result_type (List.map type_of_value (List.rev vs)) in
+        let s2 = string_of_value_types (List.map type_of_value (List.rev vs)) in
         Crash.error e.at
           ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")")
       )
diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml
index 98faf4c4..adbcc045 100644
--- a/interpreter/script/run.ml
+++ b/interpreter/script/run.ml
@@ -220,7 +220,7 @@ let print_module x_opt m =
 let print_values vs =
   let ts = List.map Value.type_of_value vs in
   Printf.printf "%s : %s\n%!"
-    (Value.string_of_values vs) (Types.string_of_result_type ts)
+    (Value.string_of_values vs) (Types.string_of_value_types ts)
 
 let string_of_nan = function
   | CanonicalNan -> "nan:canonical"
@@ -267,7 +267,7 @@ let string_of_results = function
 let print_results rs =
   let ts = List.map type_of_result rs in
   Printf.printf "%s : %s\n%!"
-    (string_of_results rs) (Types.string_of_result_type ts)
+    (string_of_results rs) (Types.string_of_value_types ts)
 
 
 (* Configuration *)
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index fff3fce4..c42bb274 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -18,10 +18,9 @@ and heap_type =
 and value_type =
   NumType of num_type | VecType of vec_type | RefType of ref_type | BotType
 
-and result_type = value_type list
-and label_type = result_type * local_idx Source.phrase list
-and instr_type = func_type * local_idx Source.phrase list
-and func_type = FuncType of result_type * result_type
+and result_type = ResultType of value_type list * local_idx Source.phrase list
+and instr_type = InstrType of value_type list * value_type list * local_idx Source.phrase list
+and func_type = FuncType of value_type list * value_type list
 and def_type = FuncDefType of func_type
 
 type 'a limits = {min : 'a; max : 'a option}
@@ -213,10 +212,13 @@ let string_of_name n =
   List.iter escape n;
   Buffer.contents b
 
+let string_of_idx x = I32.to_string_u x
+let string_of_local_idx x = string_of_idx x.Source.it
+
 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;
@@ -255,12 +257,22 @@ and string_of_value_type = function
   | RefType t -> string_of_ref_type t
   | BotType -> "(something)"
 
-and string_of_result_type ts =
+and string_of_value_types ts =
   "[" ^ String.concat " " (List.map string_of_value_type ts) ^ "]"
 
+and string_of_result_type = function
+  | ResultType (ts, xs) ->
+    String.concat " "
+      (string_of_value_types ts :: List.map string_of_local_idx xs)
+
+and stirng_of_instr_type = function
+  | InstrType (ts1, ts2, xs) ->
+    string_of_value_types ts1 ^ " -> " ^
+      string_of_result_type (ResultType (ts2, xs))
+
 and string_of_func_type = function
-  | FuncType (ins, out) ->
-    string_of_result_type ins ^ " -> " ^ string_of_result_type out
+  | FuncType (ts1, ts2) ->
+    string_of_value_types ts1 ^ " -> " ^ string_of_value_types ts2
 
 and string_of_def_type = function
   | FuncDefType ft -> "func " ^ string_of_func_type ft
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
index 3b1dac44..35fb6f5e 100644
--- a/interpreter/valid/match.ml
+++ b/interpreter/valid/match.ml
@@ -53,12 +53,12 @@ and eq_value_type c a t1 t2 =
   | BotType, BotType -> true
   | _, _ -> false
 
-and eq_result_type c a ts1 ts2 =
+and eq_value_types c a ts1 ts2 =
   List.length ts1 = List.length ts2 &&
   List.for_all2 (eq_value_type c a) ts1 ts2
 
 and eq_func_type c a (FuncType (ts11, ts12)) (FuncType (ts21, ts22)) =
-  eq_result_type c a ts11 ts21 && eq_result_type c a ts12 ts22
+  eq_value_types c a ts11 ts21 && eq_value_types c a ts12 ts22
 
 and eq_def_type c a dt1 dt2 =
   match dt1, dt2 with
@@ -130,7 +130,7 @@ and match_value_type c a t1 t2 =
   | BotType, _ -> true
   | _, _ -> false
 
-and match_result_type c a ts1 ts2 =
+and match_value_types c a ts1 ts2 =
   List.length ts1 = List.length ts2 &&
   List.for_all2 (match_value_type c a) ts1 ts2
 
diff --git a/interpreter/valid/match.mli b/interpreter/valid/match.mli
index d258af5d..1e73519d 100644
--- a/interpreter/valid/match.mli
+++ b/interpreter/valid/match.mli
@@ -9,8 +9,7 @@ type assump = (var * var) list
 val eq_num_type : context -> assump -> num_type -> num_type -> bool
 val eq_ref_type : context -> assump -> ref_type -> ref_type -> bool
 val eq_value_type : context -> assump -> value_type -> value_type -> bool
-
-val eq_result_type : context -> assump -> result_type -> result_type -> bool
+val eq_value_types : context -> assump -> value_type list -> value_type list -> bool
 
 val eq_func_type : context -> assump -> func_type -> func_type -> bool
 val eq_table_type : context -> assump -> table_type -> table_type -> bool
@@ -27,8 +26,7 @@ val eq_def_type : context -> assump -> def_type -> def_type -> bool
 val match_num_type : context -> assump -> num_type -> num_type -> bool
 val match_ref_type : context -> assump -> ref_type -> ref_type -> bool
 val match_value_type : context -> assump -> value_type -> value_type -> bool
-
-val match_result_type : context -> assump -> result_type -> result_type -> bool
+val match_value_types : context -> assump -> value_type list -> value_type list -> bool
 
 val match_func_type : context -> assump -> func_type -> func_type -> bool
 val match_table_type : context -> assump -> table_type -> table_type -> bool
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index a73a5953..fffe8cc1 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -26,7 +26,7 @@ type context =
   datas : unit list;
   locals : local_type list;
   results : value_type list;
-  labels : label_type list;
+  labels : result_type list;
   refs : Free.t;
 }
 
@@ -112,13 +112,13 @@ let check_value_type (c : context) (t : value_type) at =
   | RefType t' -> check_ref_type c t' at
   | BotType -> ()
 
-let check_result_type (c : context) (ts : result_type) at =
+let check_value_types (c : context) (ts : value_type list) at =
   List.iter (fun t -> check_value_type c t at) ts
 
 let check_func_type (c : context) (ft : func_type) at =
   let FuncType (ts1, ts2) = ft in
-  check_result_type c ts1 at;
-  check_result_type c ts2 at
+  check_value_types c ts1 at;
+  check_value_types c ts2 at
 
 let check_table_type (c : context) (tt : table_type) at =
   let TableType (lim, t) = tt in
@@ -167,8 +167,8 @@ let check_stack (c : context) ts1 ts2 at =
   require
     (List.length ts1 = List.length ts2 &&
       List.for_all2 (match_value_type c.types []) ts1 ts2) at
-    ("type mismatch: instruction requires " ^ string_of_result_type ts2 ^
-     " but stack has " ^ string_of_result_type ts1)
+    ("type mismatch: instruction requires " ^ string_of_value_types ts2 ^
+     " but stack has " ^ string_of_value_types ts1)
 
 let pop c (ell1, ts1) (ell2, ts2) at =
   let n1 = List.length ts1 in
@@ -296,8 +296,8 @@ 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
- *   ts : result_type
+ *   t  : value_type
+ *   ts : value_type list
  *   x  : variable
  *
  * Note: To deal with the non-determinism in some of the declarative rules,
@@ -311,14 +311,15 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  *)
 
 let check_block_type (c : context) (bt : block_type) at : instr_type =
-  let ft, xs =
+  let ts1, ts2, xs =
     match bt with
-    | ValBlockType (None, xs) -> FuncType ([], []), xs
-    | ValBlockType (Some t, xs) -> check_value_type c t at; FuncType ([], [t]), xs
-    | VarBlockType (SynVar x, xs) -> func_type c (x @@ at), xs
+    | ValBlockType (None, xs) -> [], [], xs
+    | ValBlockType (Some t, xs) -> check_value_type c t at; [], [t], xs
+    | VarBlockType (SynVar x, xs) ->
+      let FuncType (ts1, ts2) = func_type c (x @@ at) in ts1, ts2, xs
     | VarBlockType (SemVar _, _) -> assert false
   in
-  ft, List.map (fun x -> ignore (local c x); x) xs
+  InstrType (ts1, ts2, List.map (fun x -> ignore (local c x); x) xs)
 
 let check_local (c : context) (defaulted : bool) (t : local) : local_type =
   check_value_type c t.it t.at;
@@ -355,77 +356,77 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
   | 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;
+    check_value_types c ts e.at;
     (ts @ ts @ [NumType I32Type]) --> ts, []
 
   | Block (bt, es) ->
-    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
-    check_block {c with labels = (ts2, xs) :: c.labels} es it e.at;
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es it e.at;
     ts1 --> ts2, xs
 
   | Loop (bt, es) ->
-    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
-    check_block {c with labels = (ts1, []) :: c.labels} es it e.at;
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts1, []) :: c.labels} es it e.at;
     ts1 --> ts2, xs
 
   | If (bt, es1, es2) ->
-    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
-    check_block {c with labels = (ts2, xs) :: c.labels} es1 it e.at;
-    check_block {c with labels = (ts2, xs) :: c.labels} es2 it e.at;
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es1 it e.at;
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es2 it e.at;
     (ts1 @ [NumType I32Type]) --> ts2, xs
 
   | Let (bt, locals, es) ->
-    let FuncType (ts1, ts2), xs as it = check_block_type c bt e.at in
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
     let ts = List.map (check_local c false) locals in
     let c' =
       { c with
-        labels = (ts2, xs) :: c.labels;
+        labels = ResultType (ts2, xs) :: c.labels;
         locals = ts @ c.locals;
       }
     in check_block c' es it e.at;
     (ts1 @ List.map Source.it locals) --> ts2, xs
 
   | Br x ->
-    let ts, xs = label c x in
+    let ResultType (ts, xs) = label c x in
     check_init c xs x.at;
     ts -->... [], []
 
   | BrIf x ->
-    let ts, xs = label c x in
+    let ResultType (ts, xs) = label c x in
     check_init c xs x.at;
     (ts @ [NumType I32Type]) --> ts, []
 
   | BrTable (xs, x) ->
-    let ts, ys = label c x in
+    let ResultType (ts, ys) = label c x in
     let n = List.length ts in
     let ts' = Lib.List.table n (fun i -> peek (n - i) s) in
     check_init c ys x.at;
     check_stack c ts' ts x.at;
     List.iter (fun x' ->
-      let ts'', ys' = label c x' in
+      let ResultType (ts'', ys') = label c x' in
       check_init c ys' x'.at;
       check_stack c ts' ts'' x'.at
     ) xs;
     (ts' @ [NumType I32Type]) -->... [], []
 
   | BrOnNull x ->
-    let ts, xs = label c x in
+    let ResultType (ts, xs) = label c x in
     let (_, t) = peek_ref 0 s e.at in
     check_init c xs x.at;
     (ts @ [RefType (Nullable, t)]) --> (ts @ [RefType (NonNullable, t)]), []
 
   | BrOnNonNull x ->
-    let ts, xs = label c x in
+    let ResultType (ts, xs) = label c x in
     let (_, ht) as rt = peek_ref 0 s e.at in
     let t' = RefType (NonNullable, ht) in
     check_init c xs x.at;
     require (ts <> []) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
-       " but label has " ^ string_of_result_type ts);
+       " but label has " ^ string_of_value_types ts);
     let ts0, t = Lib.List.split_last ts in
     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 ts);
+       " but label has " ^ string_of_value_types ts);
     (ts0 @ [RefType rt]) --> ts0, []
 
   | Return ->
@@ -460,10 +461,10 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (match peek_ref 0 s e.at with
     | (nul, DefHeapType (SynVar x)) ->
       let FuncType (ts1, ts2) = func_type c (x @@ e.at) in
-      require (match_result_type c.types [] ts2 c.results) e.at
+      require (match_value_types c.types [] ts2 c.results) e.at
         ("type mismatch: current function requires result type " ^
-         string_of_result_type c.results ^
-         " but callee returns " ^ string_of_result_type ts2);
+         string_of_value_types c.results ^
+         " but callee returns " ^ string_of_value_types ts2);
       (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], []
     | (_, BotHeapType) as rt ->
       [RefType rt] -->... [], []
@@ -732,13 +733,13 @@ and check_seq (c : context) (s : infer_result_type) (es : instr list)
     push c outs (pop c ins s' e.at), xs @ xs'
 
 and check_block (c : context) (es : instr list) (it : instr_type) at =
-  let FuncType (ts1, ts2), xs = it in
+  let InstrType (ts1, ts2, xs) = it in
   let s, xs' = check_seq c (stack ts1) es in
   let s' = pop c (stack ts2) s at in
   check_init (init_locals c xs' (poly s')) xs at;
   require (snd s' = []) at
-    ("type mismatch: block requires " ^ string_of_result_type ts2 ^
-     " but stack has " ^ string_of_result_type (snd s))
+    ("type mismatch: block requires " ^ string_of_value_types ts2 ^
+     " but stack has " ^ string_of_value_types (snd s))
 
 
 (* Functions & Constants *)
@@ -763,9 +764,9 @@ let check_func (c : context) (f : func) =
     { c with
       locals = List.map (fun t -> LocalType (t, Initialized)) ts1 @ ts;
       results = ts2;
-      labels = [(ts2, [])]
+      labels = [ResultType (ts2, [])]
     }
-  in check_block c' body (FuncType ([], ts2), []) f.at
+  in check_block c' body (InstrType ([], ts2, [])) f.at
 
 
 let is_const (c : context) (e : instr) =
@@ -780,7 +781,7 @@ let is_const (c : context) (e : instr) =
 let check_const (c : context) (const : const) (t : value_type) =
   require (List.for_all (is_const c) const.it) const.at
     "constant expression required";
-  check_block c const.it (FuncType ([], [t]), []) const.at
+  check_block c const.it (InstrType ([], [t], [])) const.at
 
 
 (* Tables, Memories, & Globals *)

From 3f2e10ab3a9689a3463f953a23462e4aaba3eb3b Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 20 Jun 2022 12:58:13 +0200
Subject: [PATCH 06/11] Typos

---
 proposals/function-references/Overview.md | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index 628b04b3..ab6c1c58 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
@@ -212,6 +212,7 @@ The following rules, now defined in terms of heap types, replace and extend the
 * Result types are refined to the following form:
   - `resulttype ::= [<valtype>*] <localidx>*`
   - the local indices record which locals have been set as a side effect
+  - result types are assigned to labels and the result of instruction sequences
 
 * There is a natural notion of subtyping on result types:
   - `[t1*] x1*  <:  [t2*] x2*`
@@ -242,12 +243,6 @@ The following rules, now defined in terms of heap types, replace and extend the
     - `$t x* == [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
 
 
-#### Label Types
-
-* Labels are now typed as result types:
-  - `labeltype ::= <resulttype>`
-
-
 ### Instructions
 
 #### Functions
@@ -327,7 +322,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]`
@@ -355,7 +350,7 @@ Typing of instruction sequences is updated to account for initialization of loca
   - `epsilon : [] -> [] x*`
     - iff `(x : set t)*`
 
-Note: This typing rules does not try to eliminate duplicate indices, but an implementation could.
+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:
 
@@ -388,7 +383,7 @@ The block types ascribed to blocks declare the instruction type of the respectiv
 
 #### Branches
 
-Branches need to match the respective label type. Moreover, stack polymorphism now entails an arbitrary index set.
+Branches need to match the respective label type. Moreover, stack polymorphism now entails an arbitrary initialization set.
 
 * `br $l`
   - `br $l : [t1* t*] -> [t2*] x2*`

From 02aa00c7e6262bdc3edea319fa424994f06b2849 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 20 Jun 2022 13:02:57 +0200
Subject: [PATCH 07/11] Make bt : it explicit

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

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index ab6c1c58..aae4c4ad 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -239,8 +239,8 @@ The following rules, now defined in terms of heap types, replace and extend the
 
 * Block types denote [instruction types](#instruction-types). For that purpose, they are likewise extended with a (possibly empty) sequence of local indices
   - `blocktype ::= (<valtype> | <typeidx>) <localidx>*`
-    - `t x* == [] -> [t] x*` iff `t ok` and `(x ok)*`
-    - `$t x* == [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
+    - `t x* : [] -> [t] x*` iff `t ok` and `(x ok)*`
+    - `$t x* : [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
 
 
 ### Instructions
@@ -365,20 +365,23 @@ A subsumption rule allows to go to a supertype for any instruction:
 The block types ascribed to blocks declare the instruction type of the respective body's instruction sequence.
 
 * `block bt <instr>* end`
-  - `block $l bt <instr>* end : bt`
-    - iff `<instr>* : bt` assuming `$l : [t2*] x*`
-    - where `bt == [t1*] -> [t2*] x*`
+  - `block $l bt <instr>* end : it`
+    - iff `bt : it`
+    - and `<instr>* : it` assuming `$l : [t2*] x*`
+    - where `it = [t1*] -> [t2*] x*`
 
 * `loop bt <instr>* end`
-  - `loop $l bt <instr>* end : bt`
-    - iff `<instr>* : bt` assuming `$l : [t1*]`
-    - where `bt == [t1*] -> [t2*] x*`
+  - `loop $l bt <instr>* end : it`
+    - iff `bt : it`
+    - and `<instr>* : it` assuming `$l : [t1*]`
+    - where `it = [t1*] -> [t2*] x*`
 
 * `if bt <instr1>* else <instr2>* end`
-  - `if $l bt <instr1>* else <instr2>* end : bt`
-    - iff `<instr1>* : bt` assuming `$l : [t2*] x*`
-    - and `<instr2>* : bt` assuming `$l : [t2*] x*`
-    - where `bt == [t1*] -> [t2*] x*`
+  - `if $l bt <instr1>* else <instr2>* end : it`
+    - iff `bt : it`
+    - and `<instr1>* : it` assuming `$l : [t2*] x*`
+    - and `<instr2>* : it` assuming `$l : [t2*] x*`
+    - where `it = [t1*] -> [t2*] x*`
 
 
 #### Branches

From 0363ed79a0dde57d6ac578a0271d8c5b5a20786e Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 20 Jun 2022 13:31:37 +0200
Subject: [PATCH 08/11] Fix br_table

---
 proposals/function-references/Overview.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index aae4c4ad..ba509b98 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -392,6 +392,7 @@ Branches need to match the respective label type. Moreover, stack polymorphism n
   - `br $l : [t1* t*] -> [t2*] x2*`
     - iff `$l : [t*] x*`
     - and `(x : set tX)*`
+    - and `(x2 : set? tX2)*`
 
 * `br_if $l`
   - `br_if $l : [t* i32] -> [t*]`
@@ -399,11 +400,12 @@ Branches need to match the respective label type. Moreover, stack polymorphism n
     - and `(x : set tX)*`
 
 * `br_table $l* $l'`
-  - `br_table $l* $l' : [t'* i32] -> [t'*]`
+  - `br_table $l* $l' : [t1* t'* i32] -> [t2* t'*] x2*`
     - iff `$l' : [t'*] x'*`
     - and `(x' : set tX')*`
     - and `($l : [t*] x*)*`
     - and `(x : set tX)*`
+    - and `(x2 : set? tX2)*`
 
 
 ### Tables

From d9fa273983414705a9ed335ed623eca0cbd69668 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 11 Jul 2022 14:25:17 +0200
Subject: [PATCH 09/11] Add note about try-catch

---
 proposals/function-references/Overview.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index ba509b98..aa475a2d 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -383,6 +383,16 @@ The block types ascribed to blocks declare the instruction type of the respectiv
     - and `<instr2>* : it` assuming `$l : [t2*] x*`
     - where `it = [t1*] -> [t2*] x*`
 
+Note: For a future `try-catch`, the block type associated with `try` would likewise apply to all catch clauses – in order to avoid the need for exception and effect analysis, no assumption is being made about what parts of the `try` block have already been executed when entering a catch clause, and conservatively assumes none. Sketch (omitting `catch_all`):
+
+  - `try $l bt <instr0>* (catch $x <instr>*)* end`
+    - iff `bt : it`
+    - and `<instr0>* : it0` assuming `$l : [t2*] x*`
+    - and `(<instr>* : it)*` assuming `$l : [t2*] x*`
+    - and `($x : [tx*] -> [])*`
+    - where `it0 = [t1*] -> [t2*] x*`
+    - and `(it = [tx*] -> [t2*] x*)*`
+
 
 #### Branches
 

From a82c32adbf280a5a23eee89b43ef123ab9080c5d Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 11 Jul 2022 14:38:55 +0200
Subject: [PATCH 10/11] Add note about blocktype validation

---
 proposals/function-references/Overview.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index aa475a2d..b25e9e11 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -240,9 +240,9 @@ The following rules, now defined in terms of heap types, replace and extend the
 * Block types denote [instruction types](#instruction-types). For that purpose, they are likewise extended with a (possibly empty) sequence of local indices
   - `blocktype ::= (<valtype> | <typeidx>) <localidx>*`
     - `t x* : [] -> [t] x*` iff `t ok` and `(x ok)*`
+      - note: this rule does not enforce that the `x*` are all different
     - `$t x* : [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
 
-
 ### Instructions
 
 #### Functions

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 11/11] 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"
 )