diff --git a/ml-proto/host/arrange.ml b/ml-proto/host/arrange.ml
index b358c8870d..1bd9c00ce0 100644
--- a/ml-proto/host/arrange.ml
+++ b/ml-proto/host/arrange.ml
@@ -272,7 +272,7 @@ let table tab =
 
 let memory mem =
   let {mlimits = lim} = mem.it in
-  Node ("memory " ^ limits int64 lim, [])
+  Node ("memory " ^ limits int32 lim, [])
 
 let segment head dat seg =
   let {offset; init} = seg.it in
diff --git a/ml-proto/host/encode.ml b/ml-proto/host/encode.ml
index a4412abc80..a2c4213310 100644
--- a/ml-proto/host/encode.ml
+++ b/ml-proto/host/encode.ml
@@ -345,7 +345,7 @@ let encode m =
     (* Memory section *)
     let memory mem =
       let {mlimits} = mem.it in
-      limits vu64 mlimits
+      limits vu32 mlimits
 
     let memory_section memo =
       section "memory" (opt memory) memo (memo <> None)
diff --git a/ml-proto/host/encode.ml.rej b/ml-proto/host/encode.ml.rej
new file mode 100644
index 0000000000..3b3e977cb1
--- /dev/null
+++ b/ml-proto/host/encode.ml.rej
@@ -0,0 +1,51 @@
+--- host/encode.ml
++++ host/encode.ml
+@@ -105,31 +105,30 @@
+     let rec expr e =
+       match e.it with
+       | Nop -> op 0x00
+-      | Block es -> op 0x01; list expr es; op 0x17
+-      | Loop es -> op 0x02; list expr es; op 0x17
++      | Block es -> op 0x01; list expr es; op 0x0f
++      | Loop es -> op 0x02; list expr es; op 0x0f
+       | If (e, es1, es2) ->
+         expr e; op 0x03; list expr es1;
+-        if es2 <> [] then op 0x04; list expr es2; op 0x17
++        if es2 <> [] then op 0x04; list expr es2; op 0x0f
+       | Select (e1, e2, e3) -> expr e1; expr e2; expr e3; op 0x05
+       | Br (x, eo) -> opt expr eo; op 0x06; arity1 eo; var x
+       | Br_if (x, eo, e) -> opt expr eo; expr e; op 0x07; arity1 eo; var x
+       | Br_table (xs, x, eo, e) ->
+         opt expr eo; expr e; op 0x08; arity1 eo; vec var32 xs; var32 x
+-
+-      | Ast.I32_const c -> op 0x0a; vs32 c.it
+-      | Ast.I64_const c -> op 0x0b; vs64 c.it
+-      | Ast.F32_const c -> op 0x0c; f32 c.it
+-      | Ast.F64_const c -> op 0x0d; f64 c.it
+-
+-      | Ast.Get_local x -> op 0x0e; var x
+-      | Ast.Set_local (x, e) -> unary e 0x0f; var x
+-      | Ast.Tee_local (x, e) -> unary e 0x10; var x
+-
+-      | Ast.Call (x, es) -> nary es 0x12; var x
+-      | Ast.Call_import (x, es) -> nary es 0x1f; var x
+-      | Ast.Call_indirect (x, e, es) -> expr e; nary es 0x13; var x
+-      | Ast.Return eo -> nary1 eo 0x14
+-      | Ast.Unreachable -> op 0x15
++      | Ast.Return eo -> nary1 eo 0x09
++      | Ast.Unreachable -> op 0x0a
++
++      | Ast.I32_const c -> op 0x10; vs32 c.it
++      | Ast.I64_const c -> op 0x11; vs64 c.it
++      | Ast.F32_const c -> op 0x12; f32 c.it
++      | Ast.F64_const c -> op 0x13; f64 c.it
++
++      | Ast.Get_local x -> op 0x14; var x
++      | Ast.Set_local (x, e) -> unary e 0x15; var x
++
++      | Ast.Call (x, es) -> nary es 0x16; var x
++      | Ast.Call_indirect (x, e, es) -> expr e; nary es 0x17; var x
++      | Ast.Call_import (x, es) -> nary es 0x18; var x
+ 
+       | I32_load8_s (o, a, e) -> unary e 0x20; memop o a
+       | I32_load8_u (o, a, e) -> unary e 0x21; memop o a
diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly
index 1730a67716..e6e0ebf1e1 100644
--- a/ml-proto/host/parser.mly
+++ b/ml-proto/host/parser.mly
@@ -39,6 +39,18 @@ let literal f s =
   | Failure msg -> error s.at ("constant out of range: " ^ msg)
   | _ -> error s.at "constant out of range"
 
+let int s at =
+  try int_of_string s with Failure _ ->
+    error at "int constant out of range"
+
+let int32 s at =
+  try I32.of_string s with Failure _ ->
+    error at "i32 constant out of range"
+
+let int64 s at =
+  try I64.of_string s with Failure _ ->
+    error at "i64 constant out of range"
+
 
 (* Symbolic variables *)
 
@@ -206,7 +218,7 @@ literal :
 ;
 
 var :
-  | NAT { let at = at () in fun c lookup -> int_of_string $1 @@ at }
+  | NAT { let at = at () in fun c lookup -> int $1 at @@ at }
   | VAR { let at = at () in fun c lookup -> lookup c ($1 @@ at) @@ at }
 ;
 var_list :
@@ -365,9 +377,9 @@ elem :
 ;
 
 table_limits :
-  | NAT { {min = Int32.of_string $1; max = None} @@ at () }
+  | NAT { {min = int32 $1 (ati 1); max = None} @@ at () }
   | NAT NAT
-    { {min = Int32.of_string $1; max = Some (Int32.of_string $2)} @@ at () }
+    { {min = int32 $1 (ati 1); max = Some (int32 $2 (ati 2))} @@ at () }
 ;
 table :
   | LPAR TABLE table_limits elem_type RPAR
@@ -386,9 +398,9 @@ data :
 ;
 
 memory_limits :
-  | NAT { {min = Int64.of_string $1; max = None} @@ at () }
+  | NAT { {min = int32 $1 (ati 1); max = None} @@ at () }
   | NAT NAT
-    { {min = Int64.of_string $1; max = Some (Int64.of_string $2)} @@ at () }
+    { {min = int32 $1 (ati 1); max = Some (int32 $2 (ati 2))} @@ at () }
 ;
 memory :
   | LPAR MEMORY memory_limits RPAR
@@ -396,7 +408,7 @@ memory :
   | LPAR MEMORY LPAR DATA text_list RPAR RPAR  /* Sugar */
     { let at = at () in
       fun c ->
-      let size = Int64.(div (add (of_int (String.length $5)) 65535L) 65536L) in
+      let size = Int32.(div (add (of_int (String.length $5)) 65535l) 65536l) in
       {mlimits = {min = size; max = Some size} @@ at} @@ at,
       [{offset = I32_const (0l @@ at) @@ at; init = $5} @@ at] }
 ;
diff --git a/ml-proto/host/parser.mly.orig b/ml-proto/host/parser.mly.orig
new file mode 100644
index 0000000000..bde2f98495
--- /dev/null
+++ b/ml-proto/host/parser.mly.orig
@@ -0,0 +1,510 @@
+%{
+open Source
+open Types
+open Ast
+open Operators
+open Script
+
+
+(* Error handling *)
+
+let error at msg = raise (Script.Syntax (at, msg))
+
+let parse_error msg = error Source.no_region msg
+
+
+(* Position handling *)
+
+let position_to_pos position =
+  { file = position.Lexing.pos_fname;
+    line = position.Lexing.pos_lnum;
+    column = position.Lexing.pos_cnum - position.Lexing.pos_bol
+  }
+
+let positions_to_region position1 position2 =
+  { left = position_to_pos position1;
+    right = position_to_pos position2
+  }
+
+let at () =
+  positions_to_region (Parsing.symbol_start_pos ()) (Parsing.symbol_end_pos ())
+let ati i =
+  positions_to_region (Parsing.rhs_start_pos i) (Parsing.rhs_end_pos i)
+
+
+(* Literals *)
+
+let literal f s =
+  try f s with
+  | Failure msg -> error s.at ("constant out of range: " ^ msg)
+  | _ -> error s.at "constant out of range"
+
+
+(* Symbolic variables *)
+
+module VarMap = Map.Make(String)
+
+type space = {mutable map : int VarMap.t; mutable count : int}
+let empty () = {map = VarMap.empty; count = 0}
+
+type types = {mutable tmap : int VarMap.t; mutable tlist : Types.func_type list}
+let empty_types () = {tmap = VarMap.empty; tlist = []}
+
+type context =
+  {types : types; funcs : space; imports : space;
+   locals : space; labels : int VarMap.t}
+
+let empty_context () =
+  {types = empty_types (); funcs = empty (); imports = empty ();
+   locals = empty (); labels = VarMap.empty}
+
+let enter_func c =
+  assert (VarMap.is_empty c.labels);
+  {c with labels = VarMap.empty; locals = empty ()}
+
+let type_ c x =
+  try VarMap.find x.it c.types.tmap
+  with Not_found -> error x.at ("unknown type " ^ x.it)
+
+let lookup category space x =
+  try VarMap.find x.it space.map
+  with Not_found -> error x.at ("unknown " ^ category ^ " " ^ x.it)
+
+let func c x = lookup "function" c.funcs x
+let import c x = lookup "import" c.imports x
+let local c x = lookup "local" c.locals x
+let label c x =
+  try VarMap.find x.it c.labels
+  with Not_found -> error x.at ("unknown label " ^ x.it)
+
+let bind_type c x ty =
+  if VarMap.mem x.it c.types.tmap then
+    error x.at ("duplicate type " ^ x.it);
+  c.types.tmap <- VarMap.add x.it (List.length c.types.tlist) c.types.tmap;
+  c.types.tlist <- c.types.tlist @ [ty]
+
+let bind category space x =
+  if VarMap.mem x.it space.map then
+    error x.at ("duplicate " ^ category ^ " " ^ x.it);
+  space.map <- VarMap.add x.it space.count space.map;
+  space.count <- space.count + 1
+
+let bind_func c x = bind "function" c.funcs x
+let bind_import c x = bind "import" c.imports x
+let bind_local c x = bind "local" c.locals x
+let bind_label c x =
+  {c with labels = VarMap.add x.it 0 (VarMap.map ((+) 1) c.labels)}
+
+let anon_type c ty =
+  c.types.tlist <- c.types.tlist @ [ty]
+
+let anon space n = space.count <- space.count + n
+
+let anon_func c = anon c.funcs 1
+let anon_import c = anon c.imports 1
+let anon_locals c ts = anon c.locals (List.length ts)
+let anon_label c = {c with labels = VarMap.map ((+) 1) c.labels}
+
+let empty_type = FuncType ([], [])
+
+let explicit_decl c name t at =
+  let x = name c type_ in
+  if
+    x.it < List.length c.types.tlist &&
+    t <> empty_type &&
+    t <> List.nth c.types.tlist x.it
+  then
+    error at "signature mismatch";
+  x
+
+let implicit_decl c t at =
+  match Lib.List.index_of t c.types.tlist with
+  | None -> let i = List.length c.types.tlist in anon_type c t; i @@ at
+  | Some i -> i @@ at
+
+%}
+
+%token NAT INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR
+%token NOP DROP BLOCK END IF THEN ELSE SELECT LOOP BR BR_IF BR_TABLE
+%token CALL CALL_IMPORT CALL_INDIRECT RETURN
+%token GET_LOCAL SET_LOCAL TEE_LOCAL LOAD STORE OFFSET ALIGN
+%token CONST UNARY BINARY COMPARE CONVERT
+%token UNREACHABLE CURRENT_MEMORY GROW_MEMORY
+%token FUNC START TYPE PARAM RESULT LOCAL
+%token MODULE MEMORY SEGMENT IMPORT EXPORT TABLE
+%token ASSERT_INVALID ASSERT_RETURN ASSERT_RETURN_NAN ASSERT_TRAP INVOKE
+%token INPUT OUTPUT
+%token EOF
+
+%token<string> NAT
+%token<string> INT
+%token<string> FLOAT
+%token<string> TEXT
+%token<string> VAR
+%token<Types.value_type> VALUE_TYPE
+%token<string Source.phrase -> Ast.expr' * Values.value> CONST
+%token<Ast.expr'> UNARY
+%token<Ast.expr'> BINARY
+%token<Ast.expr'> TEST
+%token<Ast.expr'> COMPARE
+%token<Ast.expr'> CONVERT
+%token<int option -> Memory.offset -> Ast.expr'> LOAD
+%token<int option -> Memory.offset -> Ast.expr'> STORE
+%token<Memory.offset> OFFSET
+%token<int> ALIGN
+
+%nonassoc LOW
+%nonassoc VAR
+
+%start script script1 module1
+%type<Script.script> script
+%type<Script.script> script1
+%type<Script.definition> module1
+
+%%
+
+/* Auxiliaries */
+
+text_list :
+  | TEXT { $1 }
+  | text_list TEXT { $1 ^ $2 }
+;
+
+/* Types */
+
+value_type_list :
+  | /* empty */ { [] }
+  | VALUE_TYPE value_type_list { $1 :: $2 }
+;
+func_type :
+  | /* empty */
+    { FuncType ([], []) }
+  | LPAR PARAM value_type_list RPAR
+    { FuncType ($3, []) }
+  | LPAR PARAM value_type_list RPAR LPAR RESULT value_type_list RPAR
+    { FuncType ($3, $7) }
+  | LPAR RESULT value_type_list RPAR
+    { FuncType ([], $3) }
+;
+
+
+/* Expressions */
+
+nat :
+  | NAT { int_of_string $1 }
+;
+
+literal :
+  | NAT { $1 @@ at () }
+  | INT { $1 @@ at () }
+  | FLOAT { $1 @@ at () }
+;
+
+var :
+  | NAT { let at = at () in fun c lookup -> int_of_string $1 @@ at }
+  | VAR { let at = at () in fun c lookup -> lookup c ($1 @@ at) @@ at }
+;
+var_list :
+  | /* empty */ { fun c lookup -> [] }
+  | var var_list { fun c lookup -> $1 c lookup :: $2 c lookup }
+;
+bind_var :
+  | VAR { $1 @@ at () }
+;
+
+labeling :
+  | /* empty */ %prec LOW { fun c -> anon_label c }
+  | labeling1 { $1 }
+;
+labeling1 :
+  | bind_var { fun c -> bind_label c $1 }
+;
+
+offset :
+  | /* empty */ { 0L }
+  | OFFSET { $1 }
+;
+align :
+  | /* empty */ { None }
+  | ALIGN { Some $1 }
+;
+
+expr :
+  | op
+    { let at = at () in fun c -> [$1 c @@ at] }
+  | LPAR expr1 RPAR  /* Sugar */
+    { let at = at () in fun c -> let es, e' = $2 c in es @ [e' @@ at] }
+;
+op :
+  | plain_op { $1 }
+  | arity_op { $1 }
+  | block_op END { $1 }
+  | if_op END { $1 }
+;
+plain_op :
+  | UNREACHABLE { fun c -> unreachable }
+  | NOP { fun c -> nop }
+  | DROP { fun c -> drop }
+  | SELECT { fun c -> select }
+  | RETURN { fun c -> return }
+  | CALL var { fun c -> call ($2 c func) }
+  | CALL_IMPORT var { fun c -> call_import ($2 c import) }
+  | CALL_INDIRECT var { fun c -> call_indirect ($2 c type_) }
+  | GET_LOCAL var { fun c -> get_local ($2 c local) }
+  | SET_LOCAL var { fun c -> set_local ($2 c local) }
+  | TEE_LOCAL var { fun c -> tee_local ($2 c local) }
+  | LOAD offset align { fun c -> $1 $3 $2 }
+  | STORE offset align { fun c -> $1 $3 $2 }
+  | CONST literal { fun c -> fst (literal $1 $2) }
+  | UNARY { fun c -> $1 }
+  | BINARY { fun c -> $1 }
+  | TEST { fun c -> $1 }
+  | COMPARE { fun c -> $1 }
+  | CONVERT { fun c -> $1 }
+  | CURRENT_MEMORY { fun c -> current_memory }
+  | GROW_MEMORY { fun c -> grow_memory }
+;
+arity_op :
+  | BR nat var { fun c -> br $2 ($3 c label) }
+  | BR_IF nat var { fun c -> br_if $2 ($3 c label) }
+  | BR_TABLE nat var var_list
+    { fun c -> let xs, x = Lib.List.split_last ($3 c label :: $4 c label) in
+      br_table $2 xs x }
+;
+block_op :
+  | BLOCK labeling expr_list
+    { fun c -> let c' = $2 c in block ($3 c') }
+  | LOOP labeling expr_list
+    { fun c -> let c' = $2 c in loop ($3 c') }
+  | LOOP labeling1 labeling1 expr_list
+    { let at = at () in
+      fun c -> let c' = $2 c in let c'' = $3 c' in
+      block [loop ($4 c'') @@ at] }
+;
+if_op :
+  | IF labeling expr_list
+    { fun c -> let c' = $2 c in if_ ($3 c') [] }
+  | IF labeling expr_list ELSE labeling expr_list
+    { fun c -> let c1 = $2 c in let c2 = $5 c in if_ ($3 c1) ($6 c2) }
+;
+expr1 :  /* Sugar */
+  | plain_op expr_list { fun c -> $2 c, $1 c }
+  | block_op { fun c -> [], $1 c }
+  | BR var expr_list { fun c -> $3 c, br 1 ($2 c label) }
+  | BR_IF var expr_list { fun c -> $3 c, br_if 0 ($2 c label) }
+  | BR_TABLE var var_list expr_list
+    { fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in
+      $4 c, br_table 0 xs x }
+  | IF expr expr { fun c -> let c' = anon_label c in $2 c, if_ ($3 c') [] }
+  | IF expr expr expr
+    { fun c -> let c' = anon_label c in $2 c, if_ ($3 c') ($4 c') }
+  | IF expr LPAR THEN labeling expr_list RPAR
+    { fun c -> let c' = $5 c in $2 c, if_ ($6 c') [] }
+  | IF expr LPAR THEN labeling expr_list RPAR LPAR ELSE labeling expr_list RPAR
+    { fun c -> let c1 = $5 c in let c2 = $10 c in $2 c, if_ ($6 c1) ($11 c2) }
+  | IF labeling expr_list ELSE labeling expr_list  /* TODO(stack): remove? */
+    { fun c -> let c1 = $2 c in let c2 = $5 c in [], if_ ($3 c1) ($6 c2) }
+;
+expr_list :
+  | /* empty */ { fun c -> [] }
+  | expr expr_list { fun c -> $1 c @ $2 c }
+;
+
+
+/* Functions */
+
+func_fields :
+  | func_body { $1 }
+  | LPAR RESULT value_type_list RPAR func_body
+    { let FuncType (ins, out) = fst $5 in
+      FuncType (ins, $3 @ out), fun c -> snd $5 c }
+  | LPAR PARAM value_type_list RPAR func_fields
+    { let FuncType (ins, out) = fst $5 in
+      FuncType ($3 @ ins, out), fun c -> anon_locals c $3; (snd $5) c }
+  | LPAR PARAM bind_var VALUE_TYPE RPAR func_fields  /* Sugar */
+    { let FuncType (ins, out) = fst $6 in
+      FuncType ($4 :: ins, out), fun c -> bind_local c $3; (snd $6) c }
+;
+func_body :
+  | expr_list
+    { empty_type,
+      fun c -> let c' = anon_label c in
+      {ftype = -1 @@ at(); locals = []; body = $1 c'} }
+  | LPAR LOCAL value_type_list RPAR func_body
+    { fst $5,
+      fun c -> anon_locals c $3; let f = (snd $5) c in
+        {f with locals = $3 @ f.locals} }
+  | LPAR LOCAL bind_var VALUE_TYPE RPAR func_body  /* Sugar */
+    { fst $6,
+      fun c -> bind_local c $3; let f = (snd $6) c in
+        {f with locals = $4 :: f.locals} }
+;
+type_use :
+  | LPAR TYPE var RPAR { $3 }
+;
+func :
+  | LPAR FUNC export_opt type_use func_fields RPAR
+    { let at = at () in
+      fun c -> anon_func c; let t = explicit_decl c $4 (fst $5) at in
+        let exs = $3 c in
+        fun () -> {(snd $5 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt bind_var type_use func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_func c $4; let t = explicit_decl c $5 (fst $6) at in
+        let exs = $3 c in
+        fun () -> {(snd $6 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> anon_func c; let t = implicit_decl c (fst $4) at in
+        let exs = $3 c in
+        fun () -> {(snd $4 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt bind_var func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_func c $4; let t = implicit_decl c (fst $5) at in
+        let exs = $3 c in
+        fun () -> {(snd $5 (enter_func c)) with ftype = t} @@ at, exs }
+;
+export_opt :
+  | /* empty */ { fun c -> [] }
+  | TEXT
+    { let at = at () in
+      fun c -> [{name = $1; kind = `Func (c.funcs.count - 1 @@ at)} @@ at] }
+;
+
+
+/* Modules */
+
+start :
+  | LPAR START var RPAR
+    { fun c -> $3 c func }
+
+segment :
+  | LPAR SEGMENT NAT text_list RPAR
+    { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at () }
+;
+segment_list :
+  | /* empty */ { [] }
+  | segment segment_list { $1 :: $2 }
+;
+
+memory :
+  | LPAR MEMORY NAT NAT segment_list RPAR
+    { {min = Int64.of_string $3; max = Int64.of_string $4; segments = $5}
+        @@ at () }
+  | LPAR MEMORY NAT segment_list RPAR
+    { {min = Int64.of_string $3; max = Int64.of_string $3; segments = $4}
+        @@ at () }
+;
+
+type_def :
+  | LPAR TYPE LPAR FUNC func_type RPAR RPAR
+    { fun c -> anon_type c $5 }
+  | LPAR TYPE bind_var LPAR FUNC func_type RPAR RPAR
+    { fun c -> bind_type c $3 $6 }
+;
+
+table :
+  | LPAR TABLE var_list RPAR
+    { fun c -> $3 c func }
+;
+
+import :
+  | LPAR IMPORT TEXT TEXT type_use RPAR
+    { let at = at () in
+      fun c -> anon_import c; let itype = explicit_decl c $5 empty_type at in
+        {itype; module_name = $3; func_name = $4} @@ at }
+  | LPAR IMPORT bind_var TEXT TEXT type_use RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_import c $3; let itype = explicit_decl c $6 empty_type at in
+        {itype; module_name = $4; func_name = $5} @@ at }
+  | LPAR IMPORT TEXT TEXT func_type RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> anon_import c; let itype = implicit_decl c $5 at in
+        {itype; module_name = $3; func_name = $4} @@ at }
+  | LPAR IMPORT bind_var TEXT TEXT func_type RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_import c $3; let itype = implicit_decl c $6 at in
+        {itype; module_name = $4; func_name = $5} @@ at }
+;
+
+export :
+  | LPAR EXPORT TEXT var RPAR
+    { let at = at () in fun c -> {name = $3; kind = `Func ($4 c func)} @@ at }
+  | LPAR EXPORT TEXT MEMORY RPAR
+    { let at = at () in fun c -> {name = $3; kind = `Memory} @@ at }
+;
+
+module_fields :
+  | /* empty */
+    { fun c ->
+      {memory = None; types = c.types.tlist; funcs = []; start = None; imports = [];
+       exports = []; table = []} }
+  | func module_fields
+    { fun c -> let f = $1 c in let m = $2 c in let func, exs = f () in
+      {m with funcs = func :: m.funcs; exports = exs @ m.exports} }
+  | import module_fields
+    { fun c -> let i = $1 c in let m = $2 c in
+      {m with imports = i :: m.imports} }
+  | export module_fields
+    { fun c -> let m = $2 c in
+      {m with exports = $1 c :: m.exports} }
+  | table module_fields
+    { fun c -> let m = $2 c in
+      {m with table = ($1 c) @ m.table} }
+  | type_def module_fields
+    { fun c -> $1 c; $2 c }
+  | memory module_fields
+    { fun c -> let m = $2 c in
+      match m.memory with
+      | Some _ -> error $1.at "multiple memory sections"
+      | None -> {m with memory = Some $1} }
+  | start module_fields
+    { fun c -> let m = $2 c in
+      {m with start = Some ($1 c)} }
+;
+module_ :
+  | LPAR MODULE module_fields RPAR
+    { Textual ($3 (empty_context ()) @@ at ()) @@ at() }
+  | LPAR MODULE text_list RPAR { Binary $3 @@ at() }
+;
+
+
+/* Scripts */
+
+cmd :
+  | module_ { Define $1 @@ at () }
+  | LPAR INVOKE TEXT const_list RPAR { Invoke ($3, $4) @@ at () }
+  | LPAR ASSERT_INVALID module_ TEXT RPAR { AssertInvalid ($3, $4) @@ at () }
+  | LPAR ASSERT_RETURN LPAR INVOKE TEXT const_list RPAR const_list RPAR
+    { AssertReturn ($5, $6, $8) @@ at () }
+  | LPAR ASSERT_RETURN_NAN LPAR INVOKE TEXT const_list RPAR RPAR
+    { AssertReturnNaN ($5, $6) @@ at () }
+  | LPAR ASSERT_TRAP LPAR INVOKE TEXT const_list RPAR TEXT RPAR
+    { AssertTrap ($5, $6, $8) @@ at () }
+  | LPAR INPUT TEXT RPAR { Input $3 @@ at () }
+  | LPAR OUTPUT TEXT RPAR { Output (Some $3) @@ at () }
+  | LPAR OUTPUT RPAR { Output None @@ at () }
+;
+cmd_list :
+  | /* empty */ { [] }
+  | cmd cmd_list { $1 :: $2 }
+;
+
+const :
+  | LPAR CONST literal RPAR { snd (literal $2 $3) @@ ati 3 }
+;
+const_list :
+  | /* empty */ { [] }
+  | const const_list { $1 :: $2 }
+;
+
+script :
+  | cmd_list EOF { $1 }
+;
+script1 :
+  | cmd { [$1] }
+;
+module1 :
+  | module_ EOF { $1 }
+;
+%%
diff --git a/ml-proto/host/parser.mly.save b/ml-proto/host/parser.mly.save
new file mode 100644
index 0000000000..bde2f98495
--- /dev/null
+++ b/ml-proto/host/parser.mly.save
@@ -0,0 +1,510 @@
+%{
+open Source
+open Types
+open Ast
+open Operators
+open Script
+
+
+(* Error handling *)
+
+let error at msg = raise (Script.Syntax (at, msg))
+
+let parse_error msg = error Source.no_region msg
+
+
+(* Position handling *)
+
+let position_to_pos position =
+  { file = position.Lexing.pos_fname;
+    line = position.Lexing.pos_lnum;
+    column = position.Lexing.pos_cnum - position.Lexing.pos_bol
+  }
+
+let positions_to_region position1 position2 =
+  { left = position_to_pos position1;
+    right = position_to_pos position2
+  }
+
+let at () =
+  positions_to_region (Parsing.symbol_start_pos ()) (Parsing.symbol_end_pos ())
+let ati i =
+  positions_to_region (Parsing.rhs_start_pos i) (Parsing.rhs_end_pos i)
+
+
+(* Literals *)
+
+let literal f s =
+  try f s with
+  | Failure msg -> error s.at ("constant out of range: " ^ msg)
+  | _ -> error s.at "constant out of range"
+
+
+(* Symbolic variables *)
+
+module VarMap = Map.Make(String)
+
+type space = {mutable map : int VarMap.t; mutable count : int}
+let empty () = {map = VarMap.empty; count = 0}
+
+type types = {mutable tmap : int VarMap.t; mutable tlist : Types.func_type list}
+let empty_types () = {tmap = VarMap.empty; tlist = []}
+
+type context =
+  {types : types; funcs : space; imports : space;
+   locals : space; labels : int VarMap.t}
+
+let empty_context () =
+  {types = empty_types (); funcs = empty (); imports = empty ();
+   locals = empty (); labels = VarMap.empty}
+
+let enter_func c =
+  assert (VarMap.is_empty c.labels);
+  {c with labels = VarMap.empty; locals = empty ()}
+
+let type_ c x =
+  try VarMap.find x.it c.types.tmap
+  with Not_found -> error x.at ("unknown type " ^ x.it)
+
+let lookup category space x =
+  try VarMap.find x.it space.map
+  with Not_found -> error x.at ("unknown " ^ category ^ " " ^ x.it)
+
+let func c x = lookup "function" c.funcs x
+let import c x = lookup "import" c.imports x
+let local c x = lookup "local" c.locals x
+let label c x =
+  try VarMap.find x.it c.labels
+  with Not_found -> error x.at ("unknown label " ^ x.it)
+
+let bind_type c x ty =
+  if VarMap.mem x.it c.types.tmap then
+    error x.at ("duplicate type " ^ x.it);
+  c.types.tmap <- VarMap.add x.it (List.length c.types.tlist) c.types.tmap;
+  c.types.tlist <- c.types.tlist @ [ty]
+
+let bind category space x =
+  if VarMap.mem x.it space.map then
+    error x.at ("duplicate " ^ category ^ " " ^ x.it);
+  space.map <- VarMap.add x.it space.count space.map;
+  space.count <- space.count + 1
+
+let bind_func c x = bind "function" c.funcs x
+let bind_import c x = bind "import" c.imports x
+let bind_local c x = bind "local" c.locals x
+let bind_label c x =
+  {c with labels = VarMap.add x.it 0 (VarMap.map ((+) 1) c.labels)}
+
+let anon_type c ty =
+  c.types.tlist <- c.types.tlist @ [ty]
+
+let anon space n = space.count <- space.count + n
+
+let anon_func c = anon c.funcs 1
+let anon_import c = anon c.imports 1
+let anon_locals c ts = anon c.locals (List.length ts)
+let anon_label c = {c with labels = VarMap.map ((+) 1) c.labels}
+
+let empty_type = FuncType ([], [])
+
+let explicit_decl c name t at =
+  let x = name c type_ in
+  if
+    x.it < List.length c.types.tlist &&
+    t <> empty_type &&
+    t <> List.nth c.types.tlist x.it
+  then
+    error at "signature mismatch";
+  x
+
+let implicit_decl c t at =
+  match Lib.List.index_of t c.types.tlist with
+  | None -> let i = List.length c.types.tlist in anon_type c t; i @@ at
+  | Some i -> i @@ at
+
+%}
+
+%token NAT INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR
+%token NOP DROP BLOCK END IF THEN ELSE SELECT LOOP BR BR_IF BR_TABLE
+%token CALL CALL_IMPORT CALL_INDIRECT RETURN
+%token GET_LOCAL SET_LOCAL TEE_LOCAL LOAD STORE OFFSET ALIGN
+%token CONST UNARY BINARY COMPARE CONVERT
+%token UNREACHABLE CURRENT_MEMORY GROW_MEMORY
+%token FUNC START TYPE PARAM RESULT LOCAL
+%token MODULE MEMORY SEGMENT IMPORT EXPORT TABLE
+%token ASSERT_INVALID ASSERT_RETURN ASSERT_RETURN_NAN ASSERT_TRAP INVOKE
+%token INPUT OUTPUT
+%token EOF
+
+%token<string> NAT
+%token<string> INT
+%token<string> FLOAT
+%token<string> TEXT
+%token<string> VAR
+%token<Types.value_type> VALUE_TYPE
+%token<string Source.phrase -> Ast.expr' * Values.value> CONST
+%token<Ast.expr'> UNARY
+%token<Ast.expr'> BINARY
+%token<Ast.expr'> TEST
+%token<Ast.expr'> COMPARE
+%token<Ast.expr'> CONVERT
+%token<int option -> Memory.offset -> Ast.expr'> LOAD
+%token<int option -> Memory.offset -> Ast.expr'> STORE
+%token<Memory.offset> OFFSET
+%token<int> ALIGN
+
+%nonassoc LOW
+%nonassoc VAR
+
+%start script script1 module1
+%type<Script.script> script
+%type<Script.script> script1
+%type<Script.definition> module1
+
+%%
+
+/* Auxiliaries */
+
+text_list :
+  | TEXT { $1 }
+  | text_list TEXT { $1 ^ $2 }
+;
+
+/* Types */
+
+value_type_list :
+  | /* empty */ { [] }
+  | VALUE_TYPE value_type_list { $1 :: $2 }
+;
+func_type :
+  | /* empty */
+    { FuncType ([], []) }
+  | LPAR PARAM value_type_list RPAR
+    { FuncType ($3, []) }
+  | LPAR PARAM value_type_list RPAR LPAR RESULT value_type_list RPAR
+    { FuncType ($3, $7) }
+  | LPAR RESULT value_type_list RPAR
+    { FuncType ([], $3) }
+;
+
+
+/* Expressions */
+
+nat :
+  | NAT { int_of_string $1 }
+;
+
+literal :
+  | NAT { $1 @@ at () }
+  | INT { $1 @@ at () }
+  | FLOAT { $1 @@ at () }
+;
+
+var :
+  | NAT { let at = at () in fun c lookup -> int_of_string $1 @@ at }
+  | VAR { let at = at () in fun c lookup -> lookup c ($1 @@ at) @@ at }
+;
+var_list :
+  | /* empty */ { fun c lookup -> [] }
+  | var var_list { fun c lookup -> $1 c lookup :: $2 c lookup }
+;
+bind_var :
+  | VAR { $1 @@ at () }
+;
+
+labeling :
+  | /* empty */ %prec LOW { fun c -> anon_label c }
+  | labeling1 { $1 }
+;
+labeling1 :
+  | bind_var { fun c -> bind_label c $1 }
+;
+
+offset :
+  | /* empty */ { 0L }
+  | OFFSET { $1 }
+;
+align :
+  | /* empty */ { None }
+  | ALIGN { Some $1 }
+;
+
+expr :
+  | op
+    { let at = at () in fun c -> [$1 c @@ at] }
+  | LPAR expr1 RPAR  /* Sugar */
+    { let at = at () in fun c -> let es, e' = $2 c in es @ [e' @@ at] }
+;
+op :
+  | plain_op { $1 }
+  | arity_op { $1 }
+  | block_op END { $1 }
+  | if_op END { $1 }
+;
+plain_op :
+  | UNREACHABLE { fun c -> unreachable }
+  | NOP { fun c -> nop }
+  | DROP { fun c -> drop }
+  | SELECT { fun c -> select }
+  | RETURN { fun c -> return }
+  | CALL var { fun c -> call ($2 c func) }
+  | CALL_IMPORT var { fun c -> call_import ($2 c import) }
+  | CALL_INDIRECT var { fun c -> call_indirect ($2 c type_) }
+  | GET_LOCAL var { fun c -> get_local ($2 c local) }
+  | SET_LOCAL var { fun c -> set_local ($2 c local) }
+  | TEE_LOCAL var { fun c -> tee_local ($2 c local) }
+  | LOAD offset align { fun c -> $1 $3 $2 }
+  | STORE offset align { fun c -> $1 $3 $2 }
+  | CONST literal { fun c -> fst (literal $1 $2) }
+  | UNARY { fun c -> $1 }
+  | BINARY { fun c -> $1 }
+  | TEST { fun c -> $1 }
+  | COMPARE { fun c -> $1 }
+  | CONVERT { fun c -> $1 }
+  | CURRENT_MEMORY { fun c -> current_memory }
+  | GROW_MEMORY { fun c -> grow_memory }
+;
+arity_op :
+  | BR nat var { fun c -> br $2 ($3 c label) }
+  | BR_IF nat var { fun c -> br_if $2 ($3 c label) }
+  | BR_TABLE nat var var_list
+    { fun c -> let xs, x = Lib.List.split_last ($3 c label :: $4 c label) in
+      br_table $2 xs x }
+;
+block_op :
+  | BLOCK labeling expr_list
+    { fun c -> let c' = $2 c in block ($3 c') }
+  | LOOP labeling expr_list
+    { fun c -> let c' = $2 c in loop ($3 c') }
+  | LOOP labeling1 labeling1 expr_list
+    { let at = at () in
+      fun c -> let c' = $2 c in let c'' = $3 c' in
+      block [loop ($4 c'') @@ at] }
+;
+if_op :
+  | IF labeling expr_list
+    { fun c -> let c' = $2 c in if_ ($3 c') [] }
+  | IF labeling expr_list ELSE labeling expr_list
+    { fun c -> let c1 = $2 c in let c2 = $5 c in if_ ($3 c1) ($6 c2) }
+;
+expr1 :  /* Sugar */
+  | plain_op expr_list { fun c -> $2 c, $1 c }
+  | block_op { fun c -> [], $1 c }
+  | BR var expr_list { fun c -> $3 c, br 1 ($2 c label) }
+  | BR_IF var expr_list { fun c -> $3 c, br_if 0 ($2 c label) }
+  | BR_TABLE var var_list expr_list
+    { fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in
+      $4 c, br_table 0 xs x }
+  | IF expr expr { fun c -> let c' = anon_label c in $2 c, if_ ($3 c') [] }
+  | IF expr expr expr
+    { fun c -> let c' = anon_label c in $2 c, if_ ($3 c') ($4 c') }
+  | IF expr LPAR THEN labeling expr_list RPAR
+    { fun c -> let c' = $5 c in $2 c, if_ ($6 c') [] }
+  | IF expr LPAR THEN labeling expr_list RPAR LPAR ELSE labeling expr_list RPAR
+    { fun c -> let c1 = $5 c in let c2 = $10 c in $2 c, if_ ($6 c1) ($11 c2) }
+  | IF labeling expr_list ELSE labeling expr_list  /* TODO(stack): remove? */
+    { fun c -> let c1 = $2 c in let c2 = $5 c in [], if_ ($3 c1) ($6 c2) }
+;
+expr_list :
+  | /* empty */ { fun c -> [] }
+  | expr expr_list { fun c -> $1 c @ $2 c }
+;
+
+
+/* Functions */
+
+func_fields :
+  | func_body { $1 }
+  | LPAR RESULT value_type_list RPAR func_body
+    { let FuncType (ins, out) = fst $5 in
+      FuncType (ins, $3 @ out), fun c -> snd $5 c }
+  | LPAR PARAM value_type_list RPAR func_fields
+    { let FuncType (ins, out) = fst $5 in
+      FuncType ($3 @ ins, out), fun c -> anon_locals c $3; (snd $5) c }
+  | LPAR PARAM bind_var VALUE_TYPE RPAR func_fields  /* Sugar */
+    { let FuncType (ins, out) = fst $6 in
+      FuncType ($4 :: ins, out), fun c -> bind_local c $3; (snd $6) c }
+;
+func_body :
+  | expr_list
+    { empty_type,
+      fun c -> let c' = anon_label c in
+      {ftype = -1 @@ at(); locals = []; body = $1 c'} }
+  | LPAR LOCAL value_type_list RPAR func_body
+    { fst $5,
+      fun c -> anon_locals c $3; let f = (snd $5) c in
+        {f with locals = $3 @ f.locals} }
+  | LPAR LOCAL bind_var VALUE_TYPE RPAR func_body  /* Sugar */
+    { fst $6,
+      fun c -> bind_local c $3; let f = (snd $6) c in
+        {f with locals = $4 :: f.locals} }
+;
+type_use :
+  | LPAR TYPE var RPAR { $3 }
+;
+func :
+  | LPAR FUNC export_opt type_use func_fields RPAR
+    { let at = at () in
+      fun c -> anon_func c; let t = explicit_decl c $4 (fst $5) at in
+        let exs = $3 c in
+        fun () -> {(snd $5 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt bind_var type_use func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_func c $4; let t = explicit_decl c $5 (fst $6) at in
+        let exs = $3 c in
+        fun () -> {(snd $6 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> anon_func c; let t = implicit_decl c (fst $4) at in
+        let exs = $3 c in
+        fun () -> {(snd $4 (enter_func c)) with ftype = t} @@ at, exs }
+  | LPAR FUNC export_opt bind_var func_fields RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_func c $4; let t = implicit_decl c (fst $5) at in
+        let exs = $3 c in
+        fun () -> {(snd $5 (enter_func c)) with ftype = t} @@ at, exs }
+;
+export_opt :
+  | /* empty */ { fun c -> [] }
+  | TEXT
+    { let at = at () in
+      fun c -> [{name = $1; kind = `Func (c.funcs.count - 1 @@ at)} @@ at] }
+;
+
+
+/* Modules */
+
+start :
+  | LPAR START var RPAR
+    { fun c -> $3 c func }
+
+segment :
+  | LPAR SEGMENT NAT text_list RPAR
+    { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at () }
+;
+segment_list :
+  | /* empty */ { [] }
+  | segment segment_list { $1 :: $2 }
+;
+
+memory :
+  | LPAR MEMORY NAT NAT segment_list RPAR
+    { {min = Int64.of_string $3; max = Int64.of_string $4; segments = $5}
+        @@ at () }
+  | LPAR MEMORY NAT segment_list RPAR
+    { {min = Int64.of_string $3; max = Int64.of_string $3; segments = $4}
+        @@ at () }
+;
+
+type_def :
+  | LPAR TYPE LPAR FUNC func_type RPAR RPAR
+    { fun c -> anon_type c $5 }
+  | LPAR TYPE bind_var LPAR FUNC func_type RPAR RPAR
+    { fun c -> bind_type c $3 $6 }
+;
+
+table :
+  | LPAR TABLE var_list RPAR
+    { fun c -> $3 c func }
+;
+
+import :
+  | LPAR IMPORT TEXT TEXT type_use RPAR
+    { let at = at () in
+      fun c -> anon_import c; let itype = explicit_decl c $5 empty_type at in
+        {itype; module_name = $3; func_name = $4} @@ at }
+  | LPAR IMPORT bind_var TEXT TEXT type_use RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_import c $3; let itype = explicit_decl c $6 empty_type at in
+        {itype; module_name = $4; func_name = $5} @@ at }
+  | LPAR IMPORT TEXT TEXT func_type RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> anon_import c; let itype = implicit_decl c $5 at in
+        {itype; module_name = $3; func_name = $4} @@ at }
+  | LPAR IMPORT bind_var TEXT TEXT func_type RPAR  /* Sugar */
+    { let at = at () in
+      fun c -> bind_import c $3; let itype = implicit_decl c $6 at in
+        {itype; module_name = $4; func_name = $5} @@ at }
+;
+
+export :
+  | LPAR EXPORT TEXT var RPAR
+    { let at = at () in fun c -> {name = $3; kind = `Func ($4 c func)} @@ at }
+  | LPAR EXPORT TEXT MEMORY RPAR
+    { let at = at () in fun c -> {name = $3; kind = `Memory} @@ at }
+;
+
+module_fields :
+  | /* empty */
+    { fun c ->
+      {memory = None; types = c.types.tlist; funcs = []; start = None; imports = [];
+       exports = []; table = []} }
+  | func module_fields
+    { fun c -> let f = $1 c in let m = $2 c in let func, exs = f () in
+      {m with funcs = func :: m.funcs; exports = exs @ m.exports} }
+  | import module_fields
+    { fun c -> let i = $1 c in let m = $2 c in
+      {m with imports = i :: m.imports} }
+  | export module_fields
+    { fun c -> let m = $2 c in
+      {m with exports = $1 c :: m.exports} }
+  | table module_fields
+    { fun c -> let m = $2 c in
+      {m with table = ($1 c) @ m.table} }
+  | type_def module_fields
+    { fun c -> $1 c; $2 c }
+  | memory module_fields
+    { fun c -> let m = $2 c in
+      match m.memory with
+      | Some _ -> error $1.at "multiple memory sections"
+      | None -> {m with memory = Some $1} }
+  | start module_fields
+    { fun c -> let m = $2 c in
+      {m with start = Some ($1 c)} }
+;
+module_ :
+  | LPAR MODULE module_fields RPAR
+    { Textual ($3 (empty_context ()) @@ at ()) @@ at() }
+  | LPAR MODULE text_list RPAR { Binary $3 @@ at() }
+;
+
+
+/* Scripts */
+
+cmd :
+  | module_ { Define $1 @@ at () }
+  | LPAR INVOKE TEXT const_list RPAR { Invoke ($3, $4) @@ at () }
+  | LPAR ASSERT_INVALID module_ TEXT RPAR { AssertInvalid ($3, $4) @@ at () }
+  | LPAR ASSERT_RETURN LPAR INVOKE TEXT const_list RPAR const_list RPAR
+    { AssertReturn ($5, $6, $8) @@ at () }
+  | LPAR ASSERT_RETURN_NAN LPAR INVOKE TEXT const_list RPAR RPAR
+    { AssertReturnNaN ($5, $6) @@ at () }
+  | LPAR ASSERT_TRAP LPAR INVOKE TEXT const_list RPAR TEXT RPAR
+    { AssertTrap ($5, $6, $8) @@ at () }
+  | LPAR INPUT TEXT RPAR { Input $3 @@ at () }
+  | LPAR OUTPUT TEXT RPAR { Output (Some $3) @@ at () }
+  | LPAR OUTPUT RPAR { Output None @@ at () }
+;
+cmd_list :
+  | /* empty */ { [] }
+  | cmd cmd_list { $1 :: $2 }
+;
+
+const :
+  | LPAR CONST literal RPAR { snd (literal $2 $3) @@ ati 3 }
+;
+const_list :
+  | /* empty */ { [] }
+  | const const_list { $1 :: $2 }
+;
+
+script :
+  | cmd_list EOF { $1 }
+;
+script1 :
+  | cmd { [$1] }
+;
+module1 :
+  | module_ EOF { $1 }
+;
+%%
diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml
index c50fe9493a..03a4ba155e 100644
--- a/ml-proto/spec/check.ml
+++ b/ml-proto/spec/check.ml
@@ -346,14 +346,14 @@ let check_table (c : context) (tab : table) =
 
 let check_memory_limits (lim : Memory.size limits) =
   let {min; max} = lim.it in
-  require (I64.lt_u min 65536L) lim.at
+  require (I32.lt_u min 65536l) lim.at
     "memory size must be less than 65536 pages (4GiB)";
   match max with
   | None -> ()
   | Some max ->
-    require (I64.lt_u max 65536L) lim.at
+    require (I32.lt_u max 65536l) lim.at
       "memory size must be less than 65536 pages (4GiB)";
-    require (I64.le_u min max) lim.at
+    require (I32.le_u min max) lim.at
       "memory size minimum must not be greater than maximum"
 
 let check_memory (c : context) (mem : memory) =
@@ -366,8 +366,10 @@ let check_table_segment c prev_end seg =
   let start = Values.int32_of_value (Eval.const c.module_ offset) in
   let len = Int32.of_int (List.length init) in
   let end_ = Int32.add start len in
-  require (prev_end <= start) seg.at "table segment not disjoint and ordered";
-  require (end_ <= table c seg.at) seg.at "table segment does not fit memory";
+  require (I32.le_u prev_end start) seg.at
+    "table segment not disjoint and ordered";
+  require (I32.le_u end_ (table c seg.at)) seg.at
+    "table segment does not fit memory";
   ignore (List.map (func c) init);
   end_
 
@@ -378,8 +380,10 @@ let check_memory_segment c prev_end seg =
     Int64.of_int32 (Values.int32_of_value (Eval.const c.module_ offset)) in
   let len = Int64.of_int (String.length init) in
   let end_ = Int64.add start len in
-  require (prev_end <= start) seg.at "data segment not disjoint and ordered";
-  require (end_ <= Int64.mul (memory c seg.at) Memory.page_size) seg.at
+  let limit = Int64.mul (Int64.of_int32 (memory c seg.at)) Memory.page_size in
+  require (I64.le_u prev_end start) seg.at
+    "data segment not disjoint and ordered";
+  require (I64.le_u end_ limit) seg.at
     "data segment does not fit memory";
   end_
 
diff --git a/ml-proto/spec/decode.ml b/ml-proto/spec/decode.ml
index 59645468d6..c7938f0131 100644
--- a/ml-proto/spec/decode.ml
+++ b/ml-proto/spec/decode.ml
@@ -526,7 +526,7 @@ let table_section s =
 (* Memory section *)
 
 let memory s =
-  let lim = at (limits vu64) s in
+  let lim = at (limits vu32) s in
   {mlimits = lim}
 
 let memory_section s =
diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml
index 244aab8ba1..280e15ecd8 100644
--- a/ml-proto/spec/eval.ml
+++ b/ml-proto/spec/eval.ml
@@ -307,23 +307,15 @@ and eval_hostop c hostop vs at =
   | CurrentMemory, [] ->
     let mem = memory c at in
     let size = Memory.size mem in
-    assert (I64.lt_u size (Int64.of_int32 Int32.max_int));
-    Some (Int32 (Int64.to_int32 size))
+    Some (Int32 size)
 
   | GrowMemory, [v] ->
     let mem = memory c at in
-    let delta = address32 v at in
+    let delta = int32 v at in
     let old_size = Memory.size mem in
-    let new_size = Int64.add old_size delta in
-    if I64.lt_u new_size old_size then
-      Trap.error at "memory size overflow";
-    (* Test whether the new size overflows the memory type.
-     * Since we currently only support i32, just test that. *)
-    if I64.gt_u new_size (Int64.of_int32 Int32.max_int) then
-      Trap.error at "memory size exceeds implementation limit";
     let result =
-      try Memory.grow mem delta; Int64.to_int32 old_size
-      with Memory.SizeOverflow | Memory.SizeLimit -> -1l
+      try Memory.grow mem delta; old_size
+      with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l
     in Some (Int32 result)
 
   | _, _ ->
diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml
index a3266e6ba6..0cf43e3107 100644
--- a/ml-proto/spec/memory.ml
+++ b/ml-proto/spec/memory.ml
@@ -2,7 +2,7 @@ open Bigarray
 open Types
 open Values
 
-type size = int64
+type size = int32  (* number of pages *)
 type address = int64
 type offset = int64
 
@@ -20,6 +20,7 @@ exception Type
 exception Bounds
 exception SizeOverflow
 exception SizeLimit
+exception OutOfMemory
 
 let page_size = 0x10000L (* 64 KiB *)
 
@@ -48,26 +49,30 @@ let host_index_of_int64 a n =
 
 let within_limits n = function
   | None -> true
-  | Some max -> I64.le_u n max
+  | Some max -> I32.le_u n max
 
 let create' n =
-  let sz = host_size_of_int64 (Int64.mul n page_size) in
-  let mem = Array1.create Int8_unsigned C_layout sz in
-  Array1.fill mem 0;
-  mem
+  if I32.gt_u n 0x10000l then raise SizeOverflow else
+  try
+    let sz = host_size_of_int64 (Int64.mul (Int64.of_int32 n) page_size) in
+    let mem = Array1.create Int8_unsigned C_layout sz in
+    Array1.fill mem 0;
+    mem
+  with Out_of_memory -> raise OutOfMemory
 
 let create n max =
   assert (within_limits n max);
   {content = create' n; max}
 
 let size mem =
-  Int64.div (int64_of_host_size (Array1.dim mem.content)) page_size
+  Int64.to_int32
+    (Int64.div (int64_of_host_size (Array1.dim mem.content)) page_size)
 
 let grow mem delta =
   let host_old_size = Array1.dim mem.content in
   let old_size = size mem in
-  let new_size = Int64.add old_size delta in
-  if I64.gt_u old_size new_size then raise SizeOverflow else
+  let new_size = Int32.add old_size delta in
+  if I32.gt_u old_size new_size then raise SizeOverflow else
   if not (within_limits new_size mem.max) then raise SizeLimit else
   let after = create' new_size in
   Array1.blit
diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli
index e37a47f0a6..988637e9f6 100644
--- a/ml-proto/spec/memory.mli
+++ b/ml-proto/spec/memory.mli
@@ -1,7 +1,7 @@
 type memory
 type t = memory
 
-type size = int64
+type size = int32  (* number of pages *)
 type address = int64
 type offset = int64
 
@@ -15,12 +15,13 @@ exception Type
 exception Bounds
 exception SizeOverflow
 exception SizeLimit
+exception OutOfMemory
 
-val page_size : size
+val page_size : offset
 
-val create : size -> size option -> memory
+val create : size -> size option -> memory (* raise SizeOverflow, OutOfMemory *)
 val size : memory -> size
-val grow : memory -> size -> unit
+val grow : memory -> size -> unit (* raise SizeOverflow, OutOfMemory *)
 
 val load : memory -> address -> offset -> value_type -> value
 val store : memory -> address -> offset -> value -> unit
diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast
index 7f5e22038a..1170ade959 100644
--- a/ml-proto/test/memory.wast
+++ b/ml-proto/test/memory.wast
@@ -80,7 +80,7 @@
   "memory size must be less than 65536 pages (4GiB)"
 )
 (assert_invalid
-  (module (memory 0 4294967296))
+  (module (memory 0 4294967295))
   "memory size must be less than 65536 pages (4GiB)"
 )
 
diff --git a/ml-proto/test/memory_trap.wast b/ml-proto/test/memory_trap.wast
index a3f45abd6b..3749143890 100644
--- a/ml-proto/test/memory_trap.wast
+++ b/ml-proto/test/memory_trap.wast
@@ -33,4 +33,4 @@
 (assert_trap (invoke "load" (i32.const 0)) "out of bounds memory access")
 (assert_trap (invoke "store" (i32.const 0x80000000) (i32.const 13)) "out of bounds memory access")
 (assert_trap (invoke "load" (i32.const 0x80000000)) "out of bounds memory access")
-(assert_trap (invoke "grow_memory" (i32.const 0x80000000)) "memory size exceeds implementation limit")
+(assert_return (invoke "grow_memory" (i32.const 0x10001)) (i32.const -1))