diff --git a/ml-proto/given/lib.ml b/ml-proto/given/lib.ml
index 36b24c3ddf..9ab792ef25 100644
--- a/ml-proto/given/lib.ml
+++ b/ml-proto/given/lib.ml
@@ -44,3 +44,10 @@ struct
     if x < 0 then failwith "is_power_of_two";
     x <> 0 && (x land (x - 1)) = 0
 end
+
+module Int64 =
+struct
+  let is_power_of_two x =
+    if x < 0L then failwith "is_power_of_two";
+    x <> 0L && (Int64.logand x (Int64.sub x 1L)) = 0L
+end
diff --git a/ml-proto/given/lib.mli b/ml-proto/given/lib.mli
index 17ea37e1df..155cae477c 100644
--- a/ml-proto/given/lib.mli
+++ b/ml-proto/given/lib.mli
@@ -23,3 +23,8 @@ module Int :
 sig
   val is_power_of_two : int -> bool
 end
+
+module Int64 :
+sig
+  val is_power_of_two : int64 -> bool
+end
diff --git a/ml-proto/host/params.ml b/ml-proto/host/params.ml
index e733d788fd..2badb1b6af 100644
--- a/ml-proto/host/params.ml
+++ b/ml-proto/host/params.ml
@@ -1 +1 @@
-let page_size = 4096
+let page_size = 4096L
diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly
index fe19130460..954cb46dd7 100644
--- a/ml-proto/host/parser.mly
+++ b/ml-proto/host/parser.mly
@@ -269,7 +269,7 @@ func :
 
 segment :
   | LPAR SEGMENT INT TEXT RPAR
-    { {Memory.addr = int_of_string $3; Memory.data = $4} @@ at() }
+    { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at() }
 ;
 segment_list :
   | /* empty */ { [] }
@@ -278,10 +278,10 @@ segment_list :
 
 memory :
   | LPAR MEMORY INT INT segment_list RPAR
-    { {initial = int_of_string $3; max = int_of_string $4; segments = $5 }
+    { {initial = Int64.of_string $3; max = Int64.of_string $4; segments = $5}
         @@ at() }
   | LPAR MEMORY INT segment_list RPAR
-    { {initial = int_of_string $3; max = int_of_string $3; segments = $4 }
+    { {initial = Int64.of_string $3; max = Int64.of_string $3; segments = $4}
         @@ at() }
 ;
 
diff --git a/ml-proto/host/script.ml b/ml-proto/host/script.ml
index 1fe8bb512b..53804fcfe9 100644
--- a/ml-proto/host/script.ml
+++ b/ml-proto/host/script.ml
@@ -25,7 +25,7 @@ let trace name = if !Flags.trace then print_endline ("-- " ^ name)
 let current_module : Eval.instance option ref = ref None
 
 let eval_args es at =
-  let evs = List.map Eval.eval es in
+  let evs = List.map Eval.host_eval es in
   let reject_none = function
     | Some v -> v
     | None -> Error.error at "unexpected () value" in
@@ -88,7 +88,7 @@ let run_command cmd =
     let m = get_module cmd.at in
     let arg_vs = eval_args arg_es cmd.at in
     let got_v = Eval.invoke m name arg_vs in
-    let expect_v = Eval.eval expect_e in
+    let expect_v = Eval.host_eval expect_e in
     (match got_v, expect_v with
      | Some Int32 got_i32, Some Int32 expect_i32 ->
        if got_i32 <> expect_i32 then begin
diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml
index d42de9d2fc..28afc891f0 100644
--- a/ml-proto/spec/check.ml
+++ b/ml-proto/spec/check.ml
@@ -22,13 +22,10 @@ type context =
   tables : func_type list;
   locals : value_type list;
   return : expr_type;
-  labels : expr_type list
+  labels : expr_type list;
+  has_memory : bool
 }
 
-let c0 =
-  {funcs = []; imports = []; tables = [];
-   locals = []; return = None; labels = []}
-
 let lookup category list x =
   try List.nth list x.it with Failure _ ->
     error x.at ("unknown " ^ category ^ " " ^ string_of_int x.it)
@@ -215,12 +212,15 @@ let rec check_expr c et e =
     check_type (Some t) et e.at
 
   | PageSize ->
+    check_has_memory c e.at;
     check_type (Some Int32Type) et e.at
 
   | MemorySize ->
+    check_has_memory c e.at;
     check_type (Some Int32Type) et e.at
 
   | ResizeMemory e ->
+    check_has_memory c e.at;
     check_expr c (Some Int32Type) e;
     check_type None et e.at
 
@@ -243,16 +243,21 @@ and check_arm c t et arm =
   check_expr c (if fallthru then None else et) e
 
 and check_load c et memop e1 at =
+  check_has_memory c at;
   check_align memop.align at;
   check_expr c (Some Int32Type) e1;
   check_type (Some memop.ty) et at
 
 and check_store c et memop e1 e2 at =
+  check_has_memory c at;
   check_align memop.align at;
   check_expr c (Some Int32Type) e1;
   check_expr c (Some memop.ty) e2;
   check_type (Some memop.ty) et at
 
+and check_has_memory c at =
+  require c.has_memory at "memory ops require a memory section";
+
 and check_align align at =
   Lib.Option.app (fun a ->
     require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment") align
@@ -281,14 +286,15 @@ let check_func c f =
                    return = Lib.Option.map it result} in
   check_expr c' (Lib.Option.map it result) e
 
-let check_table c tab =
+let check_table funcs tables tab =
   match tab.it with
   | [] ->
     error tab.at "empty table"
   | x::xs ->
-    let s = func c x in
-    List.iter (fun xI -> check_func_type (func c xI) s xI.at) xs;
-    {c with tables = c.tables @ [s]}
+    let func x = lookup "function" funcs x in
+    let s = func x in
+    List.iter (fun xI -> check_func_type (func xI) s xI.at) xs;
+    tables @ [s]
 
 module NameSet = Set.Make(String)
 
@@ -300,7 +306,8 @@ let check_export c set ex =
   NameSet.add name set
 
 let check_segment size prev_end seg =
-  let seg_end = seg.it.Memory.addr + String.length seg.it.Memory.data in
+  let seg_len = Int64.of_int (String.length seg.it.Memory.data) in
+  let seg_end = Int64.add seg.it.Memory.addr seg_len in
   require (seg.it.Memory.addr >= prev_end) seg.at
     "data segment not disjoint and ordered";
   require (size >= seg_end) seg.at
@@ -308,15 +315,23 @@ let check_segment size prev_end seg =
   seg_end
 
 let check_memory memory =
-  require (memory.it.initial <= memory.it.max) memory.at
+  let mem = memory.it in
+  require (mem.initial <= mem.max) memory.at
     "initial memory size must be less than maximum";
-  ignore (List.fold_left (check_segment memory.it.initial) 0 memory.it.segments)
+  require (mem.max <= 4294967296L) memory.at
+    "linear memory size must be less or equal to 4GiB";
+  ignore (List.fold_left (check_segment mem.initial) Int64.zero mem.segments)
 
 let check_module m =
   let {imports; exports; tables; funcs; memory} = m.it in
   Lib.Option.app check_memory memory;
-  let c = {c0 with funcs = List.map type_func funcs;
-                 imports = List.map type_import imports} in
-  let c' = List.fold_left check_table c tables in
-  List.iter (check_func c') funcs;
-  ignore (List.fold_left (check_export c') NameSet.empty exports)
+  let func_types = List.map type_func funcs in
+  let c = {funcs = func_types;
+           imports = List.map type_import imports;
+           tables = List.fold_left (check_table func_types) [] tables;
+           locals = [];
+           return = None;
+           labels = [];
+           has_memory = memory <> None} in
+  List.iter (check_func c) funcs;
+  ignore (List.fold_left (check_export c) NameSet.empty exports)
diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml
index 0a074e6c1b..ccb6bf9c55 100644
--- a/ml-proto/spec/eval.ml
+++ b/ml-proto/spec/eval.ml
@@ -25,7 +25,7 @@ type instance =
   imports : import list;
   exports : export_map;
   tables : func list list;
-  memory : Memory.t;
+  memory : Memory.t option;
   host : host_params
 }
 
@@ -42,9 +42,6 @@ type config =
   return : label
 }
 
-let page_size c =
-  I32.of_int32 (Int32.of_int c.module_.host.page_size)
-
 let lookup category list x =
   try List.nth list x.it with Failure _ ->
     error x.at ("runtime: undefined " ^ category ^ " " ^ string_of_int x.it)
@@ -88,6 +85,11 @@ let numerics_error at = function
       error at "runtime: invalid conversion to integer"
   | exn -> raise exn
 
+let some_memory c at =
+  match c.module_.memory with
+  | Some m -> m
+  | _ -> error at "memory operation but no memory section"
+
 let some v at =
   match v with
   | Some v -> v
@@ -98,6 +100,11 @@ let int32 v at =
   | Int32 i -> i
   | v -> type_error at v Types.Int32Type
 
+let mem_size v at =
+  let i32 = int32 v at in
+  let i64 = Int64.of_int32 i32 in
+  Int64.shift_right_logical (Int64.shift_left i64 32) 32
+
 
 (* Evaluation *)
 
@@ -169,31 +176,27 @@ let rec eval_expr (c : config) (e : expr) =
     Some v1
 
   | Load ({ty; align = _}, e1) ->
-    let v1 = some (eval_expr c e1) e1.at in
-    let a = Memory.address_of_value v1 in
-    (try Some (Memory.load c.module_.memory a ty)
-    with exn -> memory_error e.at exn)
+    let mem = some_memory c e.at in
+    let v1 = mem_size (eval_expr c e1) e1.at in
+    (try Some (Memory.load mem v1 ty) with exn -> memory_error e.at exn)
 
   | Store ({ty = _; align = _}, e1, e2) ->
-    let v1 = some (eval_expr c e1) e1.at in
+    let mem = some_memory c e.at in
+    let v1 = mem_size (eval_expr c e1) e1.at in
     let v2 = some (eval_expr c e2) e2.at in
-    let a = Memory.address_of_value v1 in
-    (try Memory.store c.module_.memory a v2
-    with exn -> memory_error e.at exn);
+    (try Memory.store mem v1 v2 with exn -> memory_error e.at exn);
     Some v2
 
   | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) ->
-    let v1 = some (eval_expr c e1) e1.at in
-    let a = Memory.address_of_value v1 in
-    (try Some (Memory.load_extend c.module_.memory a sz ext ty)
-    with exn -> memory_error e.at exn)
+    let mem = some_memory c e.at in
+    let v1 = mem_size (eval_expr c e1) e1.at in
+    (try Some (Memory.load_extend mem v1 sz ext ty) with exn -> memory_error e.at exn)
 
   | StoreWrap ({memop = {ty; align = _}; sz}, e1, e2) ->
-    let v1 = some (eval_expr c e1) e1.at in
+    let mem = some_memory c e.at in
+    let v1 = mem_size (eval_expr c e1) e1.at in
     let v2 = some (eval_expr c e2) e2.at in
-    let a = Memory.address_of_value v1 in
-    (try Memory.store_wrap c.module_.memory a sz v2
-    with exn -> memory_error e.at exn);
+    (try Memory.store_wrap mem v1 sz v2 with exn -> memory_error e.at exn);
     Some v2
 
   | Const v ->
@@ -232,17 +235,20 @@ let rec eval_expr (c : config) (e : expr) =
       | exn -> numerics_error e.at exn)
 
   | PageSize ->
-    Some (Int32 (page_size c))
+    Some (Int32 (Int64.to_int32 c.module_.host.page_size))
 
   | MemorySize ->
-    Some (Int32 (I32.of_int32 (Int32.of_int (Memory.size c.module_.memory))))
+    let mem = some_memory c e.at in
+    let i64 = Memory.size mem in
+    assert (i64 < Int64.of_int32 (Int32.max_int));
+    Some (Int32 (Int64.to_int32 i64))
 
   | ResizeMemory e ->
-    let i = int32 (eval_expr c e) e.at in
-    if (I32.rem_u i (page_size c)) <> I32.zero then
+    let mem = some_memory c e.at in
+    let sz = mem_size (eval_expr c e) e.at in
+    if (Int64.rem sz c.module_.host.page_size) <> 0L then
       error e.at "runtime: resize_memory operand not multiple of page_size";
-    (* TODO: The conversion to int could overflow. *)
-    Memory.resize c.module_.memory (Int32.to_int i);
+    Memory.resize mem sz;
     None
 
 and eval_expr_option c eo =
@@ -272,36 +278,32 @@ and eval_func (m : instance) (f : func) (evs : value list) =
 
 (* Modules *)
 
-let init_memory ast =
-  match ast with
-  | None ->
-    Memory.create 0
-  | Some {it = {initial; segments; _}} ->
-    let mem = Memory.create initial in
-    Memory.init mem (List.map it segments);
-    mem
+let init_memory {it = {initial; segments; _}} =
+  let mem = Memory.create initial in
+  Memory.init mem (List.map it segments);
+  mem
 
 let init m imports host =
   assert (List.length imports = List.length m.it.Ast.imports);
-  assert (host.page_size > 0);
-  assert (Lib.Int.is_power_of_two host.page_size);
+  assert (host.page_size > 0L);
+  assert (Lib.Int64.is_power_of_two host.page_size);
   let {Ast.exports; tables; funcs; memory; _} = m.it in
-  let mem = init_memory memory in
+  let memory' = Lib.Option.map init_memory memory in
   let func x = List.nth funcs x.it in
   let export ex = ExportMap.add ex.it.name (func ex.it.func) in
   let exports = List.fold_right export exports ExportMap.empty in
   let tables = List.map (fun tab -> List.map func tab.it) tables in
-  {funcs; imports; exports; tables; memory = mem; host}
+  {funcs; imports; exports; tables; memory = memory'; host}
 
 let invoke m name vs =
   let f = export m (name @@ no_region) in
   assert (List.length vs = List.length f.it.params);
   eval_func m f vs
 
-let eval e =
+(* This function is not part of the spec. *)
+let host_eval e =
   let f = {params = []; result = None; locals = []; body = e} @@ no_region in
-  let memory = Memory.create 0 in
   let exports = ExportMap.singleton "eval" f in
-  let host = {page_size = 1} in
-  let m = {imports = []; exports; tables = []; funcs = [f]; memory; host} in
+  let host = {page_size = 1L} in
+  let m = {imports = []; exports; tables = []; funcs = [f]; memory = None; host} in
   eval_func m f []
diff --git a/ml-proto/spec/eval.mli b/ml-proto/spec/eval.mli
index 4c737a0103..2442bfe13f 100644
--- a/ml-proto/spec/eval.mli
+++ b/ml-proto/spec/eval.mli
@@ -10,4 +10,6 @@ type host_params = {page_size : Memory.size}
 val init : Ast.module_ -> import list -> host_params -> instance
 val invoke : instance -> string -> value list -> value option
   (* raise Error.Error *)
-val eval : Ast.expr -> value option (* raise Error.Error *)
+
+(* This function is not part of the spec. *)
+val host_eval : Ast.expr -> value option (* raise Error.Error *)
diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml
index 4263b9fa69..336a36ffd5 100644
--- a/ml-proto/spec/memory.ml
+++ b/ml-proto/spec/memory.ml
@@ -6,10 +6,7 @@ open Bigarray
 open Types
 open Values
 
-
-(* Types and view types *)
-
-type address = int
+type address = int64
 type size = address
 type mem_size = Mem8 | Mem16 | Mem32
 type extension = SX | ZX
@@ -21,15 +18,37 @@ type memory' = (int, int8_unsigned_elt, c_layout) Array1.t
 type memory = memory' ref
 type t = memory
 
-
-(* Creation and initialization *)
-
 exception Type
 exception Bounds
 exception Address
 
+(*
+ * These limitations should be considered part of the host environment and not
+ * part of the spec defined by this file.
+ * ==========================================================================
+ *)
+
+let host_size_of_int64 n =
+  if n < Int64.zero || n > (Int64.of_int max_int) then raise Out_of_memory;
+  Int64.to_int n
+
+let int64_of_host_size n =
+  Int64.of_int n
+
+let host_index_of_int64 a n =
+  assert (n >= 0);
+  let n' = Int64.of_int n in
+  if (a < Int64.zero) ||
+     (Int64.sub Int64.max_int a < n') ||
+     (Int64.add a n' > Int64.of_int max_int) then raise Bounds;
+  Int64.to_int a
+
+(* ========================================================================== *)
+
+
 let create' n =
-  let mem = Array1.create Int8_unsigned C_layout n in
+  let sz = host_size_of_int64 n in
+  let mem = Array1.create Int8_unsigned C_layout sz in
   Array1.fill mem 0;
   mem
 
@@ -38,48 +57,45 @@ let create n =
 
 let init_seg mem seg =
   (* There currently is no way to blit from a string. *)
-  for i = 0 to String.length seg.data - 1 do
-    !mem.{seg.addr + i} <- Char.code seg.data.[i]
+  let n = String.length seg.data in
+  let base = host_index_of_int64 seg.addr n in
+  for i = 0 to n - 1 do
+    !mem.{base + i} <- Char.code seg.data.[i]
   done
 
 let init mem segs =
   try List.iter (init_seg mem) segs with Invalid_argument _ -> raise Bounds
 
-
 let size mem =
-  Array1.dim !mem
+  int64_of_host_size (Array1.dim !mem)
 
 let resize mem n =
-  let before = !mem in
   let after = create' n in
-  let min = min (Array1.dim before) n in
-  Array1.blit (Array1.sub before 0 min) (Array1.sub after 0 min);
+  let min = host_index_of_int64 (min (size mem) n) 0 in
+  Array1.blit (Array1.sub !mem 0 min) (Array1.sub after 0 min);
   mem := after
 
-open Values
-
-(* TODO: The conversion to int could overflow *)
-let address_of_value = function
-  | Int32 i -> Int32.to_int (I32.to_int32 i)
-  | _ -> raise Address
-
-
-(* Load and store *)
-
 let rec loadn mem n a =
   assert (n > 0 && n <= 8);
-  let byte = try Int64.of_int !mem.{a} with Invalid_argument _ -> raise Bounds in
+  let i = host_index_of_int64 a n in
+  try loadn' mem n i with Invalid_argument _ -> raise Bounds
+
+and loadn' mem n i =
+  let byte = Int64.of_int !mem.{i} in
   if n = 1 then
     byte
   else
-    Int64.logor byte (Int64.shift_left (loadn mem (n-1) (a+1)) 8)
+    Int64.logor byte (Int64.shift_left (loadn' mem (n-1) (i+1)) 8)
 
 let rec storen mem n a v =
   assert (n > 0 && n <= 8);
-  let byte = (Int64.to_int v) land 255 in
-  (try !mem.{a} <- byte with Invalid_argument _ -> raise Bounds);
+  let i = host_index_of_int64 a n in
+  try storen' mem n i v with Invalid_argument _ -> raise Bounds
+
+and storen' mem n i v =
+  !mem.{i} <- (Int64.to_int v) land 255;
   if (n > 1) then
-    storen mem (n-1) (a+1) (Int64.shift_right v 8)
+    storen' mem (n-1) (i+1) (Int64.shift_right v 8)
 
 let load mem a t =
   match t with
diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli
index 6f7112a29f..2b3320a00d 100644
--- a/ml-proto/spec/memory.mli
+++ b/ml-proto/spec/memory.mli
@@ -4,7 +4,7 @@
 
 type memory
 type t = memory
-type address = int
+type address = int64
 type size = address
 type mem_size = Mem8 | Mem16 | Mem32
 type extension = SX | ZX
@@ -24,5 +24,3 @@ val load : memory -> address -> value_type -> value
 val store : memory -> address -> value -> unit
 val load_extend : memory -> address -> mem_size -> extension -> value_type -> value
 val store_wrap : memory -> address -> mem_size -> value -> unit
-
-val address_of_value : Values.value -> address
diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast
index 2ec068f3c0..f27a8b82cb 100644
--- a/ml-proto/test/memory.wast
+++ b/ml-proto/test/memory.wast
@@ -35,29 +35,29 @@
 )
 
 ;; Test alignment annotation rules
-(module (func (i32.load8_u/2 (i32.const 0))))
-(module (func (i32.load16_u/4 (i32.const 0))))
-(module (func (i32.load/8 (i32.const 0))))
-(module (func (f32.load/8 (i32.const 0))))
+(module (memory 0) (func (i32.load8_u/2 (i32.const 0))))
+(module (memory 0) (func (i32.load16_u/4 (i32.const 0))))
+(module (memory 0) (func (i32.load/8 (i32.const 0))))
+(module (memory 0) (func (f32.load/8 (i32.const 0))))
 
 (assert_invalid
-  (module (func (i64.load/0 (i32.const 0))))
+  (module (memory 0) (func (i64.load/0 (i32.const 0))))
   "non-power-of-two alignment"
 )
 (assert_invalid
-  (module (func (i64.load/3 (i32.const 0))))
+  (module (memory 0) (func (i64.load/3 (i32.const 0))))
   "non-power-of-two alignment"
 )
 (assert_invalid
-  (module (func (i64.load/5 (i32.const 0))))
+  (module (memory 0) (func (i64.load/5 (i32.const 0))))
   "non-power-of-two alignment"
 )
 (assert_invalid
-  (module (func (i64.load/6 (i32.const 0))))
+  (module (memory 0) (func (i64.load/6 (i32.const 0))))
   "non-power-of-two alignment"
 )
 (assert_invalid
-  (module (func (i64.load/7 (i32.const 0))))
+  (module (memory 0) (func (i64.load/7 (i32.const 0))))
   "non-power-of-two alignment"
 )