diff --git a/src/basic/boot/FStar.Compiler.Util.fsti b/src/basic/boot/FStar.Compiler.Util.fsti
index 972d9f0b99d..25ab263d385 100644
--- a/src/basic/boot/FStar.Compiler.Util.fsti
+++ b/src/basic/boot/FStar.Compiler.Util.fsti
@@ -436,3 +436,7 @@ val write : ref 'a -> 'a -> unit
 (* Marshaling to and from strings *)
 val marshal: 'a -> string
 val unmarshal: string -> 'a
+
+val print_array (f: 'a -> string) (s:FStar.ConstantTimeSequence.seq 'a) : string 
+val array_length (s:FStar.ConstantTimeSequence.seq 'a) : FStar.BigInt.t
+val array_index (s:FStar.ConstantTimeSequence.seq 'a) (i:FStar.BigInt.t) : 'a
diff --git a/src/basic/ml/FStar_Compiler_Util.ml b/src/basic/ml/FStar_Compiler_Util.ml
index 37c144dcdfa..e1cea882525 100644
--- a/src/basic/ml/FStar_Compiler_Util.ml
+++ b/src/basic/ml/FStar_Compiler_Util.ml
@@ -1253,3 +1253,15 @@ let within_bounds repr signedness width =
   let lower, upper = bounds signedness width in
   let value = Z.of_string (ensure_decimal repr) in
   Z.leq lower value && Z.leq value upper
+
+let print_array (f: 'a -> string) 
+                (s: 'a array)
+  : string 
+  = let ls = Array.fold_left (fun out a -> f a  :: out) [] s in
+    format1 "[| %s |]" (String.concat "; " (List.rev ls))
+
+let array_of_list (l:'a list) = FStar_ConstantTimeSequence.of_list l
+
+let array_length (l:'a FStar_ConstantTimeSequence.seq) = FStar_ConstantTimeSequence.length l
+
+let array_index (l:'a FStar_ConstantTimeSequence.seq) (i:Z.t) = FStar_ConstantTimeSequence.index l i
diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml
index 6c0872bf2eb..8be4f8804cc 100644
--- a/src/ocaml-output/FStar_Parser_Const.ml
+++ b/src/ocaml-output/FStar_Parser_Const.ml
@@ -20,6 +20,14 @@ let (bytes_lid : FStar_Ident.lident) = pconst "bytes"
 let (int_lid : FStar_Ident.lident) = pconst "int"
 let (exn_lid : FStar_Ident.lident) = pconst "exn"
 let (list_lid : FStar_Ident.lident) = pconst "list"
+let (cst_seq_lid : FStar_Ident.lident) =
+  p2l ["FStar"; "ConstantTimeSequence"; "seq"]
+let (cst_of_list_lid : FStar_Ident.lident) =
+  p2l ["FStar"; "ConstantTimeSequence"; "of_list"]
+let (cst_length_lid : FStar_Ident.lident) =
+  p2l ["FStar"; "ConstantTimeSequence"; "length"]
+let (cst_index_lid : FStar_Ident.lident) =
+  p2l ["FStar"; "ConstantTimeSequence"; "index"]
 let (eqtype_lid : FStar_Ident.lident) = pconst "eqtype"
 let (option_lid : FStar_Ident.lident) = psnconst "option"
 let (either_lid : FStar_Ident.lident) = psconst "either"
diff --git a/src/ocaml-output/FStar_Syntax_Embeddings.ml b/src/ocaml-output/FStar_Syntax_Embeddings.ml
index 89987a1c627..85aaa9bc006 100644
--- a/src/ocaml-output/FStar_Syntax_Embeddings.ml
+++ b/src/ocaml-output/FStar_Syntax_Embeddings.ml
@@ -1355,6 +1355,55 @@ let e_list : 'a . 'a embedding -> 'a Prims.list embedding =
     let uu___ =
       let uu___1 = type_of ea in FStar_Syntax_Syntax.t_list_of uu___1 in
     mk_emb_full em un uu___ printer1 emb_t_list_a
+let e_array :
+  'a . 'a embedding -> 'a FStar_ConstantTimeSequence.seq embedding =
+  fun ea ->
+    let t_seq_a =
+      let t_seq =
+        let uu___ =
+          FStar_Syntax_Util.fvar_const FStar_Parser_Const.cst_seq_lid in
+        FStar_Syntax_Syntax.mk_Tm_uinst uu___ [FStar_Syntax_Syntax.U_zero] in
+      let uu___ = let uu___1 = FStar_Syntax_Syntax.as_arg ea.typ in [uu___1] in
+      FStar_Syntax_Syntax.mk_Tm_app t_seq uu___
+        FStar_Compiler_Range.dummyRange in
+    let emb_t_seq_a =
+      let uu___ =
+        let uu___1 =
+          FStar_Compiler_Effect.op_Bar_Greater FStar_Parser_Const.cst_seq_lid
+            FStar_Ident.string_of_lid in
+        (uu___1, [ea.emb_typ]) in
+      FStar_Syntax_Syntax.ET_app uu___ in
+    let printer1 = FStar_Compiler_Util.print_array ea.print in
+    let em arr rng shadow_l norm =
+      FStar_Syntax_Util.mk_lazy arr t_seq_a
+        FStar_Syntax_Syntax.Lazy_native_array FStar_Pervasives_Native.None in
+    let un t0 w norm =
+      let t = unmeta_div_results t0 in
+      let uu___ =
+        let uu___1 = FStar_Syntax_Subst.compress t in
+        uu___1.FStar_Syntax_Syntax.n in
+      match uu___ with
+      | FStar_Syntax_Syntax.Tm_lazy
+          { FStar_Syntax_Syntax.blob = arr;
+            FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_native_array;
+            FStar_Syntax_Syntax.ltyp = uu___1;
+            FStar_Syntax_Syntax.rng = uu___2;_}
+          ->
+          let uu___3 = FStar_Compiler_Dyn.undyn arr in
+          FStar_Pervasives_Native.Some uu___3
+      | uu___1 ->
+          (if w
+           then
+             (let uu___3 =
+                let uu___4 =
+                  let uu___5 = FStar_Syntax_Print.term_to_string t0 in
+                  FStar_Compiler_Util.format1
+                    "Not an embedded native array: %s" uu___5 in
+                (FStar_Errors.Warning_NotEmbedded, uu___4) in
+              FStar_Errors.log_issue t0.FStar_Syntax_Syntax.pos uu___3)
+           else ();
+           FStar_Pervasives_Native.None) in
+    mk_emb_full em un t_seq_a printer1 emb_t_seq_a
 let (e_string_list : Prims.string Prims.list embedding) = e_list e_string
 let (steps_Simpl : FStar_Syntax_Syntax.term) =
   FStar_Syntax_Syntax.tconst FStar_Parser_Const.steps_simpl
diff --git a/src/ocaml-output/FStar_Syntax_Syntax.ml b/src/ocaml-output/FStar_Syntax_Syntax.ml
index ee11e3e942d..e08cecf0a2f 100644
--- a/src/ocaml-output/FStar_Syntax_Syntax.ml
+++ b/src/ocaml-output/FStar_Syntax_Syntax.ml
@@ -355,6 +355,7 @@ and lazy_kind =
   | Lazy_sigelt 
   | Lazy_uvar 
   | Lazy_letbinding 
+  | Lazy_native_array 
   | Lazy_embedding of (emb_typ * term' syntax FStar_Thunk.t) 
   | Lazy_universe 
   | Lazy_universe_uvar 
@@ -923,6 +924,9 @@ let (uu___is_Lazy_uvar : lazy_kind -> Prims.bool) =
 let (uu___is_Lazy_letbinding : lazy_kind -> Prims.bool) =
   fun projectee ->
     match projectee with | Lazy_letbinding -> true | uu___ -> false
+let (uu___is_Lazy_native_array : lazy_kind -> Prims.bool) =
+  fun projectee ->
+    match projectee with | Lazy_native_array -> true | uu___ -> false
 let (uu___is_Lazy_embedding : lazy_kind -> Prims.bool) =
   fun projectee ->
     match projectee with | Lazy_embedding _0 -> true | uu___ -> false
diff --git a/src/ocaml-output/FStar_ToSyntax_Interleave.ml b/src/ocaml-output/FStar_ToSyntax_Interleave.ml
index 91bed48894e..060ebfc66b4 100644
--- a/src/ocaml-output/FStar_ToSyntax_Interleave.ml
+++ b/src/ocaml-output/FStar_ToSyntax_Interleave.ml
@@ -245,11 +245,101 @@ let (ml_mode_prefix_with_iface_decls :
   fun iface ->
     fun impl ->
       match impl.FStar_Parser_AST.d with
-      | FStar_Parser_AST.TopLevelModule uu___ -> (iface, [impl])
-      | FStar_Parser_AST.Open uu___ -> (iface, [impl])
-      | FStar_Parser_AST.Friend uu___ -> (iface, [impl])
-      | FStar_Parser_AST.Include uu___ -> (iface, [impl])
-      | FStar_Parser_AST.ModuleAbbrev uu___ -> (iface, [impl])
+      | FStar_Parser_AST.TopLevelModule uu___ ->
+          let uu___1 =
+            FStar_Compiler_List.span
+              (fun d ->
+                 match d.FStar_Parser_AST.d with
+                 | FStar_Parser_AST.Open uu___2 -> true
+                 | FStar_Parser_AST.ModuleAbbrev uu___2 -> true
+                 | uu___2 -> false) iface in
+          (match uu___1 with
+           | (iface_prefix_opens, iface1) ->
+               let iface2 =
+                 FStar_Compiler_List.filter
+                   (fun d ->
+                      match d.FStar_Parser_AST.d with
+                      | FStar_Parser_AST.Val uu___2 -> true
+                      | FStar_Parser_AST.Tycon uu___2 -> true
+                      | uu___2 -> false) iface1 in
+               (iface2,
+                 (FStar_Compiler_List.op_At [impl] iface_prefix_opens)))
+      | FStar_Parser_AST.Open uu___ ->
+          let uu___1 =
+            FStar_Compiler_List.span
+              (fun d ->
+                 match d.FStar_Parser_AST.d with
+                 | FStar_Parser_AST.Open uu___2 -> true
+                 | FStar_Parser_AST.ModuleAbbrev uu___2 -> true
+                 | uu___2 -> false) iface in
+          (match uu___1 with
+           | (iface_prefix_opens, iface1) ->
+               let iface2 =
+                 FStar_Compiler_List.filter
+                   (fun d ->
+                      match d.FStar_Parser_AST.d with
+                      | FStar_Parser_AST.Val uu___2 -> true
+                      | FStar_Parser_AST.Tycon uu___2 -> true
+                      | uu___2 -> false) iface1 in
+               (iface2,
+                 (FStar_Compiler_List.op_At [impl] iface_prefix_opens)))
+      | FStar_Parser_AST.Friend uu___ ->
+          let uu___1 =
+            FStar_Compiler_List.span
+              (fun d ->
+                 match d.FStar_Parser_AST.d with
+                 | FStar_Parser_AST.Open uu___2 -> true
+                 | FStar_Parser_AST.ModuleAbbrev uu___2 -> true
+                 | uu___2 -> false) iface in
+          (match uu___1 with
+           | (iface_prefix_opens, iface1) ->
+               let iface2 =
+                 FStar_Compiler_List.filter
+                   (fun d ->
+                      match d.FStar_Parser_AST.d with
+                      | FStar_Parser_AST.Val uu___2 -> true
+                      | FStar_Parser_AST.Tycon uu___2 -> true
+                      | uu___2 -> false) iface1 in
+               (iface2,
+                 (FStar_Compiler_List.op_At [impl] iface_prefix_opens)))
+      | FStar_Parser_AST.Include uu___ ->
+          let uu___1 =
+            FStar_Compiler_List.span
+              (fun d ->
+                 match d.FStar_Parser_AST.d with
+                 | FStar_Parser_AST.Open uu___2 -> true
+                 | FStar_Parser_AST.ModuleAbbrev uu___2 -> true
+                 | uu___2 -> false) iface in
+          (match uu___1 with
+           | (iface_prefix_opens, iface1) ->
+               let iface2 =
+                 FStar_Compiler_List.filter
+                   (fun d ->
+                      match d.FStar_Parser_AST.d with
+                      | FStar_Parser_AST.Val uu___2 -> true
+                      | FStar_Parser_AST.Tycon uu___2 -> true
+                      | uu___2 -> false) iface1 in
+               (iface2,
+                 (FStar_Compiler_List.op_At [impl] iface_prefix_opens)))
+      | FStar_Parser_AST.ModuleAbbrev uu___ ->
+          let uu___1 =
+            FStar_Compiler_List.span
+              (fun d ->
+                 match d.FStar_Parser_AST.d with
+                 | FStar_Parser_AST.Open uu___2 -> true
+                 | FStar_Parser_AST.ModuleAbbrev uu___2 -> true
+                 | uu___2 -> false) iface in
+          (match uu___1 with
+           | (iface_prefix_opens, iface1) ->
+               let iface2 =
+                 FStar_Compiler_List.filter
+                   (fun d ->
+                      match d.FStar_Parser_AST.d with
+                      | FStar_Parser_AST.Val uu___2 -> true
+                      | FStar_Parser_AST.Tycon uu___2 -> true
+                      | uu___2 -> false) iface1 in
+               (iface2,
+                 (FStar_Compiler_List.op_At [impl] iface_prefix_opens)))
       | uu___ ->
           let uu___1 =
             FStar_Compiler_List.span
@@ -312,6 +402,8 @@ let ml_mode_check_initial_interface :
                     d.FStar_Parser_AST.drange
               | FStar_Parser_AST.Tycon uu___ -> true
               | FStar_Parser_AST.Val uu___ -> true
+              | FStar_Parser_AST.Open uu___ -> true
+              | FStar_Parser_AST.ModuleAbbrev uu___ -> true
               | uu___ -> false))
 let (ulib_modules : Prims.string Prims.list) =
   ["FStar.Calc";
@@ -391,18 +483,35 @@ let (prefix_with_interface_decls :
     fun impl ->
       fun env ->
         let uu___ =
-          let uu___1 = FStar_Syntax_DsEnv.current_module env in
-          FStar_Syntax_DsEnv.iface_decls env uu___1 in
+          let uu___1 =
+            let uu___2 = FStar_Syntax_DsEnv.current_module env in
+            FStar_Syntax_DsEnv.iface_decls env uu___2 in
+          match uu___1 with
+          | FStar_Pervasives_Native.None -> ([impl], env)
+          | FStar_Pervasives_Native.Some iface ->
+              let uu___2 = prefix_one_decl mname iface impl in
+              (match uu___2 with
+               | (iface1, impl1) ->
+                   let env1 =
+                     let uu___3 = FStar_Syntax_DsEnv.current_module env in
+                     FStar_Syntax_DsEnv.set_iface_decls env uu___3 iface1 in
+                   (impl1, env1)) in
         match uu___ with
-        | FStar_Pervasives_Native.None -> ([impl], env)
-        | FStar_Pervasives_Native.Some iface ->
-            let uu___1 = prefix_one_decl mname iface impl in
-            (match uu___1 with
-             | (iface1, impl1) ->
-                 let env1 =
-                   let uu___2 = FStar_Syntax_DsEnv.current_module env in
-                   FStar_Syntax_DsEnv.set_iface_decls env uu___2 iface1 in
-                 (impl1, env1))
+        | (decls, env1) ->
+            ((let uu___2 =
+                let uu___3 = FStar_Ident.string_of_lid mname in
+                FStar_Options.dump_module uu___3 in
+              if uu___2
+              then
+                let uu___3 =
+                  let uu___4 =
+                    FStar_Compiler_List.map FStar_Parser_AST.decl_to_string
+                      decls in
+                  FStar_Compiler_Effect.op_Bar_Greater uu___4
+                    (FStar_String.concat "\n") in
+                FStar_Compiler_Util.print1 "Interleaved decls:\n%s\n" uu___3
+              else ());
+             (decls, env1))
 let (interleave_module :
   FStar_Parser_AST.modul ->
     Prims.bool -> FStar_Parser_AST.modul FStar_Syntax_DsEnv.withenv)
@@ -478,4 +587,15 @@ let (interleave_module :
                                     uu___6) in
                                 let uu___6 = FStar_Ident.range_of_lid l in
                                 FStar_Errors.raise_error uu___5 uu___6
-                            | uu___3 -> (a1, env1)))))
\ No newline at end of file
+                            | uu___3 ->
+                                ((let uu___5 =
+                                    let uu___6 = FStar_Ident.string_of_lid l in
+                                    FStar_Options.dump_module uu___6 in
+                                  if uu___5
+                                  then
+                                    let uu___6 =
+                                      FStar_Parser_AST.modul_to_string a1 in
+                                    FStar_Compiler_Util.print1
+                                      "Interleaved module is:\n%s\n" uu___6
+                                  else ());
+                                 (a1, env1))))))
\ No newline at end of file
diff --git a/src/ocaml-output/FStar_TypeChecker_Cfg.ml b/src/ocaml-output/FStar_TypeChecker_Cfg.ml
index 898832c91a0..b0eea73eadf 100644
--- a/src/ocaml-output/FStar_TypeChecker_Cfg.ml
+++ b/src/ocaml-output/FStar_TypeChecker_Cfg.ml
@@ -2059,6 +2059,24 @@ let (built_in_primitive_steps : primitive_step FStar_Compiler_Util.psmap) =
               | uu___2 -> FStar_Pervasives_Native.None)
          | uu___1 -> FStar_Pervasives_Native.None)
     | uu___ -> FStar_Pervasives_Native.None in
+  let mixed_ternary_op as_a as_b as_c embed_d f res _norm_cb args =
+    match args with
+    | a1::b1::c1::[] ->
+        let uu___ =
+          let uu___1 = as_a a1 in
+          let uu___2 = as_b b1 in
+          let uu___3 = as_c c1 in (uu___1, uu___2, uu___3) in
+        (match uu___ with
+         | (FStar_Pervasives_Native.Some a2, FStar_Pervasives_Native.Some b2,
+            FStar_Pervasives_Native.Some c2) ->
+             let uu___1 = f res.psc_range a2 b2 c2 in
+             (match uu___1 with
+              | FStar_Pervasives_Native.Some d1 ->
+                  let uu___2 = embed_d res.psc_range d1 in
+                  FStar_Pervasives_Native.Some uu___2
+              | uu___2 -> FStar_Pervasives_Native.None)
+         | uu___1 -> FStar_Pervasives_Native.None)
+    | uu___ -> FStar_Pervasives_Native.None in
   let list_of_string' rng s =
     let name l =
       let uu___ =
@@ -3498,10 +3516,230 @@ let (built_in_primitive_steps : primitive_step FStar_Compiler_Util.psmap) =
                  | uu___3 -> FStar_Pervasives_Native.None))
          (fun body -> body)
          (fun _t -> fun body -> FStar_Pervasives_Native.Some body))) in
+  let array_ops =
+    let of_list_op =
+      let emb_typ t =
+        let uu___ =
+          let uu___1 =
+            FStar_Compiler_Effect.op_Bar_Greater
+              FStar_Parser_Const.cst_seq_lid FStar_Ident.string_of_lid in
+          (uu___1, [t]) in
+        FStar_Syntax_Syntax.ET_app uu___ in
+      let un_lazy t l r =
+        let uu___ =
+          let uu___1 =
+            FStar_Syntax_Util.fvar_const FStar_Parser_Const.cst_of_list_lid in
+          FStar_Syntax_Syntax.mk_Tm_uinst uu___1 [FStar_Syntax_Syntax.U_zero] in
+        let uu___1 =
+          let uu___2 = FStar_Syntax_Syntax.iarg t in
+          let uu___3 = let uu___4 = FStar_Syntax_Syntax.as_arg l in [uu___4] in
+          uu___2 :: uu___3 in
+        FStar_Syntax_Syntax.mk_Tm_app uu___ uu___1 r in
+      (FStar_Parser_Const.cst_of_list_lid, (Prims.of_int (2)), Prims.int_one,
+        (mixed_binary_op
+           (fun uu___ ->
+              match uu___ with
+              | (elt_t, uu___1) -> FStar_Pervasives_Native.Some elt_t)
+           (fun uu___ ->
+              match uu___ with
+              | (l, q) ->
+                  let uu___1 =
+                    arg_as_list FStar_Syntax_Embeddings.e_any (l, q) in
+                  (match uu___1 with
+                   | FStar_Pervasives_Native.Some lst ->
+                       FStar_Pervasives_Native.Some (l, lst)
+                   | uu___2 -> FStar_Pervasives_Native.None))
+           (fun r ->
+              fun uu___ ->
+                match uu___ with
+                | (elt_t, (l, blob)) ->
+                    let uu___1 =
+                      let uu___2 =
+                        let uu___3 =
+                          let uu___4 =
+                            let uu___5 =
+                              let uu___6 =
+                                FStar_Syntax_Embeddings.emb_typ_of
+                                  FStar_Syntax_Embeddings.e_any in
+                              emb_typ uu___6 in
+                            let uu___6 =
+                              FStar_Thunk.mk
+                                (fun uu___7 -> un_lazy elt_t l r) in
+                            (uu___5, uu___6) in
+                          FStar_Syntax_Syntax.Lazy_embedding uu___4 in
+                        let uu___4 =
+                          let uu___5 =
+                            let uu___6 =
+                              FStar_Syntax_Util.fvar_const
+                                FStar_Parser_Const.cst_seq_lid in
+                            FStar_Syntax_Syntax.mk_Tm_uinst uu___6
+                              [FStar_Syntax_Syntax.U_zero] in
+                          let uu___6 =
+                            let uu___7 = FStar_Syntax_Syntax.as_arg elt_t in
+                            [uu___7] in
+                          FStar_Syntax_Syntax.mk_Tm_app uu___5 uu___6 r in
+                        {
+                          FStar_Syntax_Syntax.blob = blob;
+                          FStar_Syntax_Syntax.lkind = uu___3;
+                          FStar_Syntax_Syntax.ltyp = uu___4;
+                          FStar_Syntax_Syntax.rng = r
+                        } in
+                      FStar_Syntax_Syntax.Tm_lazy uu___2 in
+                    FStar_Syntax_Syntax.mk uu___1 r)
+           (fun r ->
+              fun elt_t ->
+                fun uu___ ->
+                  match uu___ with
+                  | (l, lst) ->
+                      let blob = FStar_ConstantTimeSequence.of_list lst in
+                      let uu___1 =
+                        let uu___2 =
+                          let uu___3 = FStar_Compiler_Dyn.mkdyn blob in
+                          (l, uu___3) in
+                        (elt_t, uu___2) in
+                      FStar_Pervasives_Native.Some uu___1)),
+        (FStar_TypeChecker_NBETerm.mixed_binary_op
+           (fun uu___ ->
+              match uu___ with
+              | (elt_t, uu___1) -> FStar_Pervasives_Native.Some elt_t)
+           (fun uu___ ->
+              match uu___ with
+              | (l, q) ->
+                  let uu___1 =
+                    FStar_TypeChecker_NBETerm.arg_as_list
+                      FStar_TypeChecker_NBETerm.e_any (l, q) in
+                  (match uu___1 with
+                   | FStar_Pervasives_Native.None ->
+                       FStar_Pervasives_Native.None
+                   | FStar_Pervasives_Native.Some lst ->
+                       FStar_Pervasives_Native.Some (l, lst)))
+           (fun uu___ ->
+              match uu___ with
+              | (elt_t, (l, blob)) ->
+                  let uu___1 =
+                    let uu___2 =
+                      let uu___3 =
+                        let uu___4 =
+                          let uu___5 =
+                            let uu___6 =
+                              FStar_Syntax_Embeddings.emb_typ_of
+                                FStar_Syntax_Embeddings.e_any in
+                            emb_typ uu___6 in
+                          (blob, uu___5) in
+                        FStar_Pervasives.Inr uu___4 in
+                      let uu___4 =
+                        FStar_Thunk.mk
+                          (fun uu___5 ->
+                             let uu___6 =
+                               let uu___7 =
+                                 let uu___8 =
+                                   FStar_Syntax_Syntax.lid_as_fv
+                                     FStar_Parser_Const.cst_of_list_lid
+                                     FStar_Syntax_Syntax.delta_constant
+                                     FStar_Pervasives_Native.None in
+                                 let uu___9 =
+                                   let uu___10 =
+                                     FStar_TypeChecker_NBETerm.as_arg l in
+                                   [uu___10] in
+                                 (uu___8, [FStar_Syntax_Syntax.U_zero],
+                                   uu___9) in
+                               FStar_TypeChecker_NBETerm.FV uu___7 in
+                             FStar_Compiler_Effect.op_Less_Bar
+                               FStar_TypeChecker_NBETerm.mk_t uu___6) in
+                      (uu___3, uu___4) in
+                    FStar_TypeChecker_NBETerm.Lazy uu___2 in
+                  FStar_Compiler_Effect.op_Less_Bar
+                    FStar_TypeChecker_NBETerm.mk_t uu___1)
+           (fun elt_t ->
+              fun uu___ ->
+                match uu___ with
+                | (l, lst) ->
+                    let blob = FStar_ConstantTimeSequence.of_list lst in
+                    let uu___1 =
+                      let uu___2 =
+                        let uu___3 = FStar_Compiler_Dyn.mkdyn blob in
+                        (l, uu___3) in
+                      (elt_t, uu___2) in
+                    FStar_Pervasives_Native.Some uu___1))) in
+    let arg1_as_elt_t x =
+      FStar_Pervasives_Native.Some (FStar_Pervasives_Native.fst x) in
+    let arg2_as_blob x =
+      let uu___ =
+        let uu___1 =
+          FStar_Syntax_Subst.compress (FStar_Pervasives_Native.fst x) in
+        uu___1.FStar_Syntax_Syntax.n in
+      match uu___ with
+      | FStar_Syntax_Syntax.Tm_lazy
+          { FStar_Syntax_Syntax.blob = blob;
+            FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_embedding
+              (FStar_Syntax_Syntax.ET_app (head, uu___1), uu___2);
+            FStar_Syntax_Syntax.ltyp = uu___3;
+            FStar_Syntax_Syntax.rng = uu___4;_}
+          when
+          let uu___5 =
+            FStar_Ident.string_of_lid FStar_Parser_Const.cst_seq_lid in
+          head = uu___5 -> FStar_Pervasives_Native.Some blob
+      | uu___1 -> FStar_Pervasives_Native.None in
+    let arg2_as_blob_nbe x =
+      match (FStar_Pervasives_Native.fst x).FStar_TypeChecker_NBETerm.nbe_t
+      with
+      | FStar_TypeChecker_NBETerm.Lazy
+          (FStar_Pervasives.Inr
+           (blob, FStar_Syntax_Syntax.ET_app (head, uu___)), uu___1)
+          when
+          let uu___2 =
+            FStar_Ident.string_of_lid FStar_Parser_Const.cst_seq_lid in
+          head = uu___2 -> FStar_Pervasives_Native.Some blob
+      | uu___ -> FStar_Pervasives_Native.None in
+    let length_op =
+      let embed_int r i = embed_simple FStar_Syntax_Embeddings.e_int r i in
+      let run_op blob =
+        let uu___ =
+          let uu___1 = FStar_Compiler_Dyn.undyn blob in
+          FStar_Compiler_Util.array_length uu___1 in
+        FStar_Pervasives_Native.Some uu___ in
+      (FStar_Parser_Const.cst_length_lid, (Prims.of_int (2)), Prims.int_one,
+        (mixed_binary_op arg1_as_elt_t arg2_as_blob embed_int
+           (fun uu___ -> fun uu___1 -> fun blob -> run_op blob)),
+        (FStar_TypeChecker_NBETerm.mixed_binary_op
+           (fun uu___ ->
+              match uu___ with
+              | (elt_t, uu___1) -> FStar_Pervasives_Native.Some elt_t)
+           arg2_as_blob_nbe
+           (fun i ->
+              FStar_TypeChecker_NBETerm.embed FStar_TypeChecker_NBETerm.e_int
+                bogus_cbs i) (fun uu___ -> fun blob -> run_op blob))) in
+    let index_op =
+      (FStar_Parser_Const.cst_index_lid, (Prims.of_int (3)), Prims.int_one,
+        (mixed_ternary_op arg1_as_elt_t arg2_as_blob arg_as_int
+           (fun r -> fun tm -> tm)
+           (fun r ->
+              fun _t ->
+                fun blob ->
+                  fun i ->
+                    let uu___ =
+                      let uu___1 = FStar_Compiler_Dyn.undyn blob in
+                      FStar_Compiler_Util.array_index uu___1 i in
+                    FStar_Pervasives_Native.Some uu___)),
+        (FStar_TypeChecker_NBETerm.mixed_ternary_op
+           (fun uu___ ->
+              match uu___ with
+              | (elt_t, uu___1) -> FStar_Pervasives_Native.Some elt_t)
+           arg2_as_blob_nbe FStar_TypeChecker_NBETerm.arg_as_int
+           (fun tm -> tm)
+           (fun _t ->
+              fun blob ->
+                fun i ->
+                  let uu___ =
+                    let uu___1 = FStar_Compiler_Dyn.undyn blob in
+                    FStar_Compiler_Util.array_index uu___1 i in
+                  FStar_Pervasives_Native.Some uu___))) in
+    [of_list_op; length_op; index_op] in
   let strong_steps =
     FStar_Compiler_List.map (as_primitive_step true)
       (FStar_Compiler_List.op_At basic_ops
-         (FStar_Compiler_List.op_At bounded_arith_ops [reveal_hide])) in
+         (FStar_Compiler_List.op_At bounded_arith_ops
+            (FStar_Compiler_List.op_At [reveal_hide] array_ops))) in
   let weak_steps = FStar_Compiler_List.map (as_primitive_step false) weak_ops in
   FStar_Compiler_Effect.op_Less_Bar prim_from_list
     (FStar_Compiler_List.op_At strong_steps weak_steps)
diff --git a/src/ocaml-output/FStar_TypeChecker_NBETerm.ml b/src/ocaml-output/FStar_TypeChecker_NBETerm.ml
index fed8f2fca48..ec581baf811 100644
--- a/src/ocaml-output/FStar_TypeChecker_NBETerm.ml
+++ b/src/ocaml-output/FStar_TypeChecker_NBETerm.ml
@@ -1291,6 +1291,55 @@ let e_list : 'a . 'a embedding -> 'a Prims.list embedding =
       lid_as_typ FStar_Parser_Const.list_lid [FStar_Syntax_Syntax.U_zero]
         uu___1 in
     mk_emb em un uu___ etyp
+let e_array :
+  'a . 'a embedding -> 'a FStar_ConstantTimeSequence.seq embedding =
+  fun ea ->
+    let etyp =
+      let uu___ =
+        let uu___1 =
+          FStar_Compiler_Effect.op_Bar_Greater FStar_Parser_Const.cst_seq_lid
+            FStar_Ident.string_of_lid in
+        (uu___1, [ea.emb_typ]) in
+      FStar_Syntax_Syntax.ET_app uu___ in
+    let t_seq_a =
+      let t_seq =
+        let uu___ =
+          FStar_Syntax_Util.fvar_const FStar_Parser_Const.cst_seq_lid in
+        FStar_Syntax_Syntax.mk_Tm_uinst uu___ [FStar_Syntax_Syntax.U_zero] in
+      let uu___ =
+        let uu___1 = FStar_Syntax_Syntax.as_arg FStar_Syntax_Syntax.tun in
+        [uu___1] in
+      FStar_Syntax_Syntax.mk_Tm_app t_seq uu___
+        FStar_Compiler_Range.dummyRange in
+    let em cb l =
+      let li =
+        let uu___ = FStar_Compiler_Dyn.mkdyn l in
+        {
+          FStar_Syntax_Syntax.blob = uu___;
+          FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_native_array;
+          FStar_Syntax_Syntax.ltyp = t_seq_a;
+          FStar_Syntax_Syntax.rng = FStar_Compiler_Range.dummyRange
+        } in
+      let rec thunk uu___ =
+        let uu___1 =
+          let uu___2 =
+            let uu___3 = FStar_Thunk.mk thunk in
+            ((FStar_Pervasives.Inl li), uu___3) in
+          Lazy uu___2 in
+        mk_t uu___1 in
+      thunk () in
+    let un cb trm =
+      match trm.nbe_t with
+      | Lazy (FStar_Pervasives.Inl li, uu___) ->
+          let uu___1 = FStar_Compiler_Dyn.undyn li.FStar_Syntax_Syntax.blob in
+          FStar_Pervasives_Native.Some uu___1
+      | uu___ -> FStar_Pervasives_Native.None in
+    let uu___ =
+      let uu___1 =
+        let uu___2 = let uu___3 = type_of ea in as_arg uu___3 in [uu___2] in
+      lid_as_typ FStar_Parser_Const.cst_seq_lid [FStar_Syntax_Syntax.U_zero]
+        uu___1 in
+    mk_emb em un uu___ etyp
 let (e_string_list : Prims.string Prims.list embedding) = e_list e_string
 let e_arrow : 'a 'b . 'a embedding -> 'b embedding -> ('a -> 'b) embedding =
   fun ea ->
@@ -1699,6 +1748,39 @@ let mixed_binary_op :
                       | uu___2 -> FStar_Pervasives_Native.None)
                  | uu___1 -> FStar_Pervasives_Native.None)
             | uu___ -> FStar_Pervasives_Native.None
+let mixed_ternary_op :
+  'a 'b 'c 'd .
+    (arg -> 'a FStar_Pervasives_Native.option) ->
+      (arg -> 'b FStar_Pervasives_Native.option) ->
+        (arg -> 'c FStar_Pervasives_Native.option) ->
+          ('d -> t) ->
+            ('a -> 'b -> 'c -> 'd FStar_Pervasives_Native.option) ->
+              args -> t FStar_Pervasives_Native.option
+  =
+  fun as_a ->
+    fun as_b ->
+      fun as_c ->
+        fun embed_d ->
+          fun f ->
+            fun args1 ->
+              match args1 with
+              | a1::b1::c1::[] ->
+                  let uu___ =
+                    let uu___1 = as_a a1 in
+                    let uu___2 = as_b b1 in
+                    let uu___3 = as_c c1 in (uu___1, uu___2, uu___3) in
+                  (match uu___ with
+                   | (FStar_Pervasives_Native.Some a2,
+                      FStar_Pervasives_Native.Some b2,
+                      FStar_Pervasives_Native.Some c2) ->
+                       let uu___1 = f a2 b2 c2 in
+                       (match uu___1 with
+                        | FStar_Pervasives_Native.Some d1 ->
+                            let uu___2 = embed_d d1 in
+                            FStar_Pervasives_Native.Some uu___2
+                        | uu___2 -> FStar_Pervasives_Native.None)
+                   | uu___1 -> FStar_Pervasives_Native.None)
+              | uu___ -> FStar_Pervasives_Native.None
 let (list_of_string' : Prims.string -> t) =
   fun s ->
     let uu___ = e_list e_char in
diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst
index 7363a8115d4..fd0aa1928e0 100644
--- a/src/parser/FStar.Parser.Const.fst
+++ b/src/parser/FStar.Parser.Const.fst
@@ -45,6 +45,10 @@ let bytes_lid        = pconst "bytes"
 let int_lid          = pconst "int"
 let exn_lid          = pconst "exn"
 let list_lid         = pconst "list"
+let cst_seq_lid      = p2l ["FStar"; "ConstantTimeSequence"; "seq"]
+let cst_of_list_lid  = p2l ["FStar"; "ConstantTimeSequence"; "of_list"]
+let cst_length_lid   = p2l ["FStar"; "ConstantTimeSequence"; "length"]
+let cst_index_lid    = p2l ["FStar"; "ConstantTimeSequence"; "index"]
 let eqtype_lid       = pconst "eqtype"
 let option_lid       = psnconst "option"
 let either_lid       = psconst "either"
diff --git a/src/syntax/FStar.Syntax.Embeddings.fst b/src/syntax/FStar.Syntax.Embeddings.fst
index 4a49c14f136..00377d4691d 100644
--- a/src/syntax/FStar.Syntax.Embeddings.fst
+++ b/src/syntax/FStar.Syntax.Embeddings.fst
@@ -36,6 +36,7 @@ module Ident = FStar.Ident
 module Err = FStar.Errors
 module Z = FStar.BigInt
 open FStar.Char
+module CST = FStar.ConstantTimeSequence
 
 let id_norm_cb : norm_cb = function
     | Inr x -> x
@@ -677,6 +678,38 @@ let e_list (ea:embedding 'a) =
         printer
         emb_t_list_a
 
+let e_array (ea:embedding 'a) 
+  : embedding (CST.seq 'a)
+  = let t_seq_a =
+        let t_seq = S.mk_Tm_uinst (U.fvar_const PC.cst_seq_lid) [U_zero] in
+        S.mk_Tm_app t_seq [S.as_arg ea.typ] Range.dummyRange
+    in
+    let emb_t_seq_a =
+        ET_app(PC.cst_seq_lid |> Ident.string_of_lid, [ea.emb_typ])
+    in
+    let printer = BU.print_array ea.print in
+    let em (arr:CST.seq 'a) (rng:range) (shadow_l:option (Thunk.t term)) (norm:norm_cb) : term =
+        U.mk_lazy arr t_seq_a Lazy_native_array None
+    in
+    let un (t0:term) (w:bool) (norm:norm_cb) : option (CST.seq 'a) = 
+        let t = unmeta_div_results t0 in
+        match (SS.compress t).n with
+        | Tm_lazy {blob=arr; lkind=Lazy_native_array } ->
+          Some (FStar.Compiler.Dyn.undyn arr)
+
+        | _ ->
+          if w
+          then Err.log_issue t0.pos (Err.Warning_NotEmbedded, BU.format1 "Not an embedded native array: %s" (Print.term_to_string t0));
+          None
+    in
+    mk_emb_full
+        em
+        un
+        t_seq_a
+        printer
+        emb_t_seq_a
+
+  
 let e_string_list = e_list e_string
 
 (* the steps as terms *)
diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti
index 3689f50092a..aa1684ffcc3 100644
--- a/src/syntax/FStar.Syntax.Syntax.fsti
+++ b/src/syntax/FStar.Syntax.Syntax.fsti
@@ -322,6 +322,7 @@ and lazy_kind =
   | Lazy_sigelt
   | Lazy_uvar
   | Lazy_letbinding
+  | Lazy_native_array
   | Lazy_embedding of emb_typ * Thunk.t term
   | Lazy_universe
   | Lazy_universe_uvar
diff --git a/src/tosyntax/FStar.ToSyntax.Interleave.fst b/src/tosyntax/FStar.ToSyntax.Interleave.fst
index 540723cd1d9..6f843c3a80c 100644
--- a/src/tosyntax/FStar.ToSyntax.Interleave.fst
+++ b/src/tosyntax/FStar.ToSyntax.Interleave.fst
@@ -231,8 +231,22 @@ let ml_mode_prefix_with_iface_decls
    | Friend _
    | Include _
    | ModuleAbbrev _ ->
-     iface, [impl]
+     let iface_prefix_opens, iface =
+       List.span (fun d -> match d.d with | Open _ | ModuleAbbrev _ -> true | _ -> false) iface     
+     in
+     let iface =
+       List.filter 
+         (fun d ->
+           match d.d with
+           | Val _
+           | Tycon _ -> true //only retain the vals in --MLish mode
+           | _ -> false)
+         iface
+     in
+     iface, [impl]@iface_prefix_opens
+     
    | _ ->
+
      let iface_prefix_tycons, iface =
        List.span (fun d -> match d.d with | Tycon _ -> true | _ -> false) iface
      in
@@ -260,12 +274,10 @@ let ml_mode_check_initial_interface mname (iface:list decl) =
                    "Interface contains an abstract 'type' declaration; \
                     use 'val' instead") d.drange
     | Tycon _
-    | Val _ -> true
+    | Val _
+    | Open _
+    | ModuleAbbrev _ -> true
     | _ -> false)
-  // iface |> List.filter (fun d ->
-  // match d.d with
-  // | Val _ -> true //only retain the vals in --MLish mode
-  // | _ -> false)
 
 let ulib_modules = [
   "FStar.Calc";
@@ -335,13 +347,19 @@ let initialize_interface (mname:Ident.lid) (l:list decl) : E.withenv unit =
 
 let prefix_with_interface_decls mname (impl:decl) : E.withenv (list decl) =
   fun (env:E.env) ->
-    match E.iface_decls env (E.current_module env) with
-    | None ->
-      [impl], env
-    | Some iface ->
-      let iface, impl = prefix_one_decl mname iface impl in
-      let env = E.set_iface_decls env (E.current_module env) iface in
-      impl, env
+    let decls, env = 
+      match E.iface_decls env (E.current_module env) with
+      | None ->
+        [impl], env
+      | Some iface ->
+        let iface, impl = prefix_one_decl mname iface impl in
+        let env = E.set_iface_decls env (E.current_module env) iface in
+        impl, env
+    in
+    if Options.dump_module (Ident.string_of_lid mname)
+    then Util.print1 "Interleaved decls:\n%s\n" (List.map FStar.Parser.AST.decl_to_string decls |> String.concat "\n");
+    decls,env
+    
 
 let interleave_module (a:modul) (expect_complete_modul:bool) : E.withenv modul =
   fun (env:E.env)  ->
@@ -380,5 +398,7 @@ let interleave_module (a:modul) (expect_complete_modul:bool) : E.withenv modul =
                                     (Ident.string_of_lid l)
                                     err)) (Ident.range_of_lid l)
         | _ ->
+          if Options.dump_module (string_of_lid l)
+          then Util.print1 "Interleaved module is:\n%s\n" (FStar.Parser.AST.modul_to_string a);
           a, env
       end
diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst
index 7286b20a993..5751964290b 100644
--- a/src/typechecker/FStar.TypeChecker.Cfg.fst
+++ b/src/typechecker/FStar.TypeChecker.Cfg.fst
@@ -347,6 +347,29 @@ let built_in_primitive_steps : prim_step_set =
                     end
                  | _ -> None
     in
+    let mixed_ternary_op
+           : (arg -> option 'a)
+           -> (arg -> option 'b)
+           -> (arg -> option 'c)           
+           -> (Range.range -> 'd -> term)
+           -> (Range.range -> 'a -> 'b -> 'c -> option 'd)
+           -> psc
+           -> EMB.norm_cb
+           -> args
+           -> option term
+           = fun as_a as_b as_c embed_d f res _norm_cb args ->
+                 match args with
+                 | [a;b;c] ->
+                    begin
+                    match as_a a, as_b b, as_c c with
+                    | Some a, Some b, Some c ->
+                      (match f res.psc_range a b c with
+                       | Some d -> Some (embed_d res.psc_range d)
+                       | _ -> None)
+                    | _ -> None
+                    end
+                 | _ -> None
+    in
     let list_of_string' rng (s:string) : term =
         let name l = mk (Tm_fvar (lid_as_fv l delta_constant None)) rng in
         let char_t = name PC.char_lid in
@@ -1065,9 +1088,94 @@ let built_in_primitive_steps : prim_step_set =
             (fun body -> body)
             (fun _t body -> Some body)
     in
+    let array_ops =
+      let of_list_op =
+        let emb_typ t = ET_app(PC.cst_seq_lid |> Ident.string_of_lid, [t]) in
+        let un_lazy t l r = 
+          S.mk_Tm_app
+            (S.mk_Tm_uinst (U.fvar_const PC.cst_of_list_lid) [U_zero])
+            [S.iarg t; S.as_arg l]
+            r
+        in
+        (  PC.cst_of_list_lid, 2, 1, 
+           mixed_binary_op 
+              (fun (elt_t, _) -> Some elt_t) 
+              (fun (l, q) -> 
+                match arg_as_list FStar.Syntax.Embeddings.e_any (l, q) with
+                | Some lst -> Some (l, lst)
+                | _ -> None)
+              (fun r (elt_t, (l, blob)) -> 
+                S.mk (Tm_lazy { blob;
+                                lkind=Lazy_embedding (emb_typ EMB.(emb_typ_of e_any), Thunk.mk (fun _ -> un_lazy elt_t l r));
+                                ltyp=S.mk_Tm_app (S.mk_Tm_uinst (U.fvar_const PC.cst_seq_lid) [U_zero]) [S.as_arg elt_t] r;
+                                rng=r }) r)
+              (fun r elt_t (l, lst) ->
+                 let blob = FStar.ConstantTimeSequence.of_list #term lst in
+                 Some (elt_t, (l, FStar.Compiler.Dyn.mkdyn blob))),
+           NBETerm.mixed_binary_op 
+             (fun (elt_t, _) -> Some elt_t)
+             (fun (l, q) ->
+               match NBETerm.arg_as_list NBETerm.e_any (l, q) with
+               | None -> None
+               | Some lst -> Some (l, lst))
+             (fun (elt_t, (l, blob)) ->
+               NBETerm.mk_t <|
+               NBETerm.Lazy (Inr (blob, emb_typ EMB.(emb_typ_of e_any)),
+                             Thunk.mk (fun _ -> 
+                               NBETerm.mk_t <| NBETerm.FV (S.lid_as_fv PC.cst_of_list_lid S.delta_constant None, [U_zero], [NBETerm.as_arg l]))))
+             (fun elt_t (l, lst) ->
+                let blob = FStar.ConstantTimeSequence.of_list #NBETerm.t lst in
+                Some (elt_t, (l, FStar.Compiler.Dyn.mkdyn blob))))
+      in
+      let arg1_as_elt_t (x:arg) : option term = Some (fst x) in
+      let arg2_as_blob (x:arg) : option FStar.Compiler.Dyn.dyn =
+          match (SS.compress (fst x)).n with
+          | Tm_lazy {blob=blob; lkind=Lazy_embedding (ET_app(head, _), _)}
+            when head=Ident.string_of_lid PC.cst_seq_lid -> Some blob
+          | _ -> None
+      in
+      let arg2_as_blob_nbe (x:NBETerm.arg) : option FStar.Compiler.Dyn.dyn =
+          let open FStar.TypeChecker.NBETerm in
+          match (fst x).nbe_t with
+          | Lazy (Inr (blob, ET_app(head, _)), _)
+            when head=Ident.string_of_lid PC.cst_seq_lid -> Some blob
+          | _ -> None
+      in
+      let length_op =
+        let embed_int (r:Range.range) (i:Z.t) : term = embed_simple EMB.e_int r i in
+        let run_op (blob:FStar.Compiler.Dyn.dyn) : option Z.t = 
+            Some (BU.array_length #term (FStar.Compiler.Dyn.undyn blob))
+        in
+        ( PC.cst_length_lid, 2, 1,
+          mixed_binary_op arg1_as_elt_t
+                          arg2_as_blob
+                          embed_int
+                          (fun _ _ blob -> run_op blob),
+          NBETerm.mixed_binary_op
+             (fun (elt_t, _) -> Some elt_t)
+             arg2_as_blob_nbe
+             (fun (i:Z.t) -> NBETerm.embed NBETerm.e_int bogus_cbs i)
+             (fun _ blob -> run_op blob) )
+      in
+      let index_op = 
+          (PC.cst_index_lid, 3, 1,
+           mixed_ternary_op arg1_as_elt_t
+                            arg2_as_blob 
+                            arg_as_int
+                            (fun r tm -> tm)
+                            (fun r _t blob i -> Some (BU.array_index #term (FStar.Compiler.Dyn.undyn blob) i)),
+          NBETerm.mixed_ternary_op
+             (fun (elt_t, _) -> Some elt_t)
+             arg2_as_blob_nbe
+             NBETerm.arg_as_int
+             (fun tm -> tm)
+             (fun _t blob i -> Some (BU.array_index #NBETerm.t (FStar.Compiler.Dyn.undyn blob) i)))
+      in             
+      [of_list_op; length_op; index_op]
+    in
     let strong_steps =
       List.map (as_primitive_step true)
-               (basic_ops@bounded_arith_ops@[reveal_hide])
+               (basic_ops@bounded_arith_ops@[reveal_hide]@array_ops)
     in
     let weak_steps   = List.map (as_primitive_step false) weak_ops in
     prim_from_list <| (strong_steps @ weak_steps)
diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst
index a66d28ca9ea..ff51081614f 100644
--- a/src/typechecker/FStar.TypeChecker.Env.fst
+++ b/src/typechecker/FStar.TypeChecker.Env.fst
@@ -309,7 +309,7 @@ let variable_not_found v =
   (Errors.Fatal_VariableNotFound, (format1 "Variable \"%s\" not found" (Print.bv_to_string v)))
 
 //Construct a new universe unification variable
-let new_u_univ () = U_unif (Unionfind.univ_fresh Range.dummyRange)
+let new_u_univ () = U_unif (UF.univ_fresh Range.dummyRange)
 
 let mk_univ_subst (formals : list univ_name) (us : universes) : list subst_elt =
     assert (List.length us = List.length formals);
@@ -1665,7 +1665,7 @@ let is_trivial g = match g with
     | {guard_f=Trivial; deferred=[]; univ_ineqs=([], []); implicits=i} ->
       i |> BU.for_all (fun imp ->
            (U.ctx_uvar_should_check imp.imp_uvar=Allow_unresolved)
-           || (match Unionfind.find imp.imp_uvar.ctx_uvar_head with
+           || (match UF.find imp.imp_uvar.ctx_uvar_head with
                | Some _ -> true
                | None -> false))
     | _ -> false
diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fst b/src/typechecker/FStar.TypeChecker.NBETerm.fst
index 92753068edb..21d7eba9ee8 100644
--- a/src/typechecker/FStar.TypeChecker.NBETerm.fst
+++ b/src/typechecker/FStar.TypeChecker.NBETerm.fst
@@ -499,6 +499,25 @@ let e_list (ea:embedding 'a) =
     in
     mk_emb em un (lid_as_typ PC.list_lid [U_zero] [as_arg (type_of ea)]) etyp
 
+let e_array (ea:embedding 'a)
+  : embedding (FStar.ConstantTimeSequence.seq 'a)
+  = let etyp = ET_app(PC.cst_seq_lid |> Ident.string_of_lid, [ea.emb_typ]) in
+    let t_seq_a =
+        let t_seq = S.mk_Tm_uinst (U.fvar_const PC.cst_seq_lid) [U_zero] in
+        S.mk_Tm_app t_seq [S.as_arg S.tun] Range.dummyRange
+    in
+    let em cb (l:FStar.ConstantTimeSequence.seq 'a) : t =
+      let li = { blob = FStar.Compiler.Dyn.mkdyn l; lkind = Lazy_native_array; ltyp = t_seq_a; rng = Range.dummyRange } in
+      let rec thunk () = mk_t (Lazy (Inl li, Thunk.mk thunk)) in
+      thunk ()
+    in
+    let un cb (trm:t) : option (FStar.ConstantTimeSequence.seq 'a) =
+      match trm.nbe_t with
+      | Lazy (Inl li, _) -> Some (FStar.Compiler.Dyn.undyn li.blob)
+      | _ -> None
+    in
+    mk_emb em un (lid_as_typ PC.cst_seq_lid [U_zero] [as_arg (type_of ea)]) etyp
+  
 let e_string_list = e_list e_string
 
 let e_arrow (ea:embedding 'a) (eb:embedding 'b) : embedding ('a -> 'b) =
@@ -674,6 +693,24 @@ let mixed_binary_op (as_a : arg -> option 'a) (as_b : arg -> option 'b)
                 end
              | _ -> None
 
+let mixed_ternary_op (as_a : arg -> option 'a)
+                     (as_b : arg -> option 'b)
+                     (as_c : arg -> option 'c)                     
+                     (embed_d : 'd -> t) 
+                     (f : 'a -> 'b -> 'c -> option 'd)
+                     (args : args) : option t =
+             match args with
+             | [a;b;c] ->
+                begin
+                match as_a a, as_b b, as_c c with
+                | Some a, Some b, Some c ->
+                  (match f a b c with
+                   | Some d -> Some (embed_d d)
+                   | _ -> None)
+                | _ -> None
+                end
+             | _ -> None
+
 let list_of_string' (s:string) : t =
   embed (e_list e_char) bogus_cbs (list_of_string s)
   // let name l = mk (Tm_fvar (lid_as_fv l delta_constant None)) rng in
diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fsti b/src/typechecker/FStar.TypeChecker.NBETerm.fsti
index 72534d88f3e..d36f1188f42 100644
--- a/src/typechecker/FStar.TypeChecker.NBETerm.fsti
+++ b/src/typechecker/FStar.TypeChecker.NBETerm.fsti
@@ -341,6 +341,14 @@ val interp_prop_eq2 : args -> option t
 
 val mixed_binary_op : (arg -> option 'a) -> (arg -> option 'b) -> ('c -> t) ->
                       ('a -> 'b -> option 'c) -> args -> option t
+
+val mixed_ternary_op (as_a : arg -> option 'a)
+                     (as_b : arg -> option 'b)
+                     (as_c : arg -> option 'c)                     
+                     (embed_d : 'd -> t) 
+                     (f : 'a -> 'b -> 'c -> option 'd)
+                     (args : args) : option t
+
 val unary_op : (arg -> option 'a) -> ('a -> t) -> (args -> option t)
 val binary_op : (arg -> option 'a) -> ('a -> 'a -> t) -> (args -> option t)
 
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst
index 0dfc7e289b4..6a280e4b34e 100644
--- a/src/typechecker/FStar.TypeChecker.Rel.fst
+++ b/src/typechecker/FStar.TypeChecker.Rel.fst
@@ -42,7 +42,7 @@ module S = FStar.Syntax.Syntax
 module SS = FStar.Syntax.Subst
 module N = FStar.TypeChecker.Normalize
 module UF = FStar.Syntax.Unionfind
-module Const = FStar.Parser.Const
+module PC = FStar.Parser.Const
 module FC = FStar.Const
 module TcComm = FStar.TypeChecker.Common
 
@@ -935,7 +935,7 @@ let u_abs (k : typ) (ys : binders) (t : term) : term =
     (* TODO : not putting any cflags here on the annotation... *)
     then //The annotation is imprecise, due to a discrepancy in currying/eta-expansions etc.;
          //causing a loss in precision for the SMT encoding
-         U.abs ys t (Some (U.mk_residual_comp Const.effect_Tot_lid None []))
+         U.abs ys t (Some (U.mk_residual_comp PC.effect_Tot_lid None []))
     else let c = Subst.subst_comp (U.rename_binders xs ys) c in
          U.abs ys t (Some (U.residual_comp_of_comp c))
 
@@ -1815,7 +1815,7 @@ let simplify_guard env g = match g.guard_f with
               [Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm] env f in
       if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplified guard to %s\n" (Print.term_to_string f);
       let f = match (U.unmeta f).n with
-        | Tm_fvar fv when S.fv_eq_lid fv Const.true_lid -> Trivial
+        | Tm_fvar fv when S.fv_eq_lid fv PC.true_lid -> Trivial
         | _ -> NonTrivial f in
       {g with guard_f=f}
 
@@ -3179,7 +3179,7 @@ and solve_t' (env:Env.env) (problem:tprob) (wl:worklist) : solution =
               let treat_as_injective =
                 match (U.un_uinst head1).n with
                 | Tm_fvar fv ->
-                  Env.fv_has_attr env fv Const.unifier_hint_injective_lid
+                  Env.fv_has_attr env fv PC.unifier_hint_injective_lid
                 | _ -> false
               in
               begin
@@ -3421,11 +3421,11 @@ and solve_t' (env:Env.env) (problem:tprob) (wl:worklist) : solution =
                 in
                 let is_reveal_or_hide t =
                   let h, args = U.head_and_args t in
-                  if U.is_fvar Const.reveal h
+                  if U.is_fvar PC.reveal h
                   then match payload_of_hide_reveal h args with
                        | None -> None
                        | Some t -> Some (Inl t)
-                  else if U.is_fvar Const.hide h
+                  else if U.is_fvar PC.hide h
                   then match payload_of_hide_reveal h args with
                        | None -> None
                        | Some t -> Some (Inr t)
@@ -3452,25 +3452,25 @@ and solve_t' (env:Env.env) (problem:tprob) (wl:worklist) : solution =
                 | Some (Inl (u, ty, lhs)), None ->
                   // reveal / _
                   //add hide to both sides to simplify
-                  let rhs = mk_fv_app Const.hide u [(ty, S.as_aqual_implicit true); (t2, None)] t2.pos in
+                  let rhs = mk_fv_app PC.hide u [(ty, S.as_aqual_implicit true); (t2, None)] t2.pos in
                   Some (lhs, rhs)
 
                 | None, Some (Inl (u, ty, rhs)) ->
                   // _ / reveal
                   //add hide to both sides to simplify
-                  let lhs = mk_fv_app Const.hide u [(ty, S.as_aqual_implicit true); (t1, None)] t1.pos in
+                  let lhs = mk_fv_app PC.hide u [(ty, S.as_aqual_implicit true); (t1, None)] t1.pos in
                   Some (lhs, rhs)
 
                 | Some (Inr (u, ty, lhs)), None ->
                   // hide / _
                   //add reveal to both sides to simplify
-                  let rhs = mk_fv_app Const.reveal u [(ty,S.as_aqual_implicit true); (t2, None)] t2.pos in
+                  let rhs = mk_fv_app PC.reveal u [(ty,S.as_aqual_implicit true); (t2, None)] t2.pos in
                   Some (lhs, rhs)
 
                 | None, Some (Inr (u, ty, rhs)) ->
                   // hide / _
                   //add reveal to both sides to simplify
-                  let lhs = mk_fv_app Const.reveal u [(ty,S.as_aqual_implicit true); (t1, None)] t1.pos in
+                  let lhs = mk_fv_app PC.reveal u [(ty,S.as_aqual_implicit true); (t1, None)] t1.pos in
                   Some (lhs, rhs)
             in
             begin
@@ -4901,7 +4901,7 @@ let try_solve_single_valued_implicits env is_tac (imps:Env.implicits) : Env.impl
      let t_norm = N.normalize N.whnf_steps env (U.ctx_uvar_typ ctx_u) in
 
       match (SS.compress t_norm).n with
-      | Tm_fvar fv when S.fv_eq_lid fv Const.unit_lid ->
+      | Tm_fvar fv when S.fv_eq_lid fv PC.unit_lid ->
         r |> S.unit_const_with_range |> Some
      | Tm_refine (b, _) when U.is_unit b.sort ->
         r |> S.unit_const_with_range |> Some
diff --git a/ulib/FStar.ConstantTimeSequence.fsti b/ulib/FStar.ConstantTimeSequence.fsti
new file mode 100644
index 00000000000..6443dd77ac5
--- /dev/null
+++ b/ulib/FStar.ConstantTimeSequence.fsti
@@ -0,0 +1,9 @@
+module FStar.ConstantTimeSequence.Base
+
+val seq (a:Type u#a) : Type u#a
+
+val of_list (#a:Type u#a) (l:list a) : Tot (seq a)
+
+val length (#a:Type) (s:seq a) : Tot nat
+
+val index (#a:Type) (s:seq a) (i:nat { i < length s }) : Tot a