diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 6bfe6423..acf863be 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -1,6 +1,7 @@
 (* Low* to Rust backend *)
 
 module LidMap = Idents.LidMap
+module LidSet = Idents.LidSet
 
 (* Location information *)
 
@@ -347,7 +348,6 @@ type env = {
   prefix: string list;
   heap_structs: Idents.LidSet.t;
   pointer_holding_structs: Idents.LidSet.t;
-  (* A map from lid (type name) to the list of fields for that struct. *)
   struct_fields: MiniRust.struct_field list DataTypeMap.t;
   location: location;
 }
@@ -453,15 +453,18 @@ let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): Min
       begin try
         Name (lookup_type env lid, generic_params)
       with Not_found ->
+        (* KPrint.bprintf "Type name not found: %a\n" PrintAst.plid lid; *)
         Name (translate_unknown_lid lid, generic_params)
       end
   | TArrow _ ->
       let t, ts = Helpers.flatten_arrow t in
       let ts = match ts with [ TUnit ] -> [] | _ -> ts in
       Function (0, List.map (translate_type_with_config env config) ts, translate_type_with_config env config t)
-  | TApp _ -> failwith "TODO: TApp"
+  | TApp ((["Pulse"; "Lib"; "Slice"], "slice"), [ t ]) ->
+      Ref (config.lifetime, Shared, Slice (translate_type_with_config env config t))
+  | TApp _ -> failwith (KPrint.bsprintf "TODO: TApp %a" PrintAst.ptyp t)
   | TBound i -> Bound i
-  | TTuple _ -> failwith "TODO: TTuple"
+  | TTuple ts -> Tuple (List.map (translate_type_with_config env config) ts)
   | TAnonymous _ -> failwith "unexpected: we don't compile data types going to Rust"
   | TCgArray _ -> failwith "Impossible: TCgArray"
   | TCgApp _ -> failwith "Impossible: TCgApp"
@@ -508,7 +511,7 @@ let translate_lid env lid =
 let translate_binder_name (b: Ast.binder) =
   let open Ast in
   if snd !(b.node.mark) = AtMost 0 then "_" ^ b.node.name else b.node.name
-          
+
 
 (* Trying to compile a *reference* to variable, who originates from a split of `v_base`, and whose
    original path in the tree is `path`. *)
@@ -582,7 +585,7 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
 (* However, generally, we will have a type provided by the context that may
    necessitate the insertion of conversions *)
 and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr =
-  KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e;
+  (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *)
 
   let erase_lifetime_info = (object(self)
     inherit [_] MiniRust.DeBruijn.map
@@ -621,7 +624,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         (* DEAD CODE -- no method try_into on Vec *)
         MethodCall (MethodCall (x, ["try_into"], []), ["unwrap"], [])
     | _, Array _, App (Name (["Box"], _), [Slice _]) ->
-        (* COPY *)
+        (* COPY (remember that Box::new does not take any type argument) *)
         Call (Name ["Box"; "new"], [], [x])
 
     (* More conversions due to vec-ing types *)
@@ -696,8 +699,13 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       env, Operator o
   | EQualified lid ->
       begin try
-        let name, t = lookup_decl env lid in
-        env, possibly_convert (Name name) t
+        match lid with
+        | [ "C" ], "_zero_for_deref" ->
+            (* CInt for Rust means no suffix -- rustc will convert to usize or u32 *)
+            env, Constant (CInt, "0")
+        | _ ->
+            let name, t = lookup_decl env lid in
+            env, possibly_convert (Name name) t
       with Not_found ->
         (* External -- TODO: make sure external definitions are properly added
            to the scope *)
@@ -722,6 +730,40 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, es = translate_expr_list env es in
       env, possibly_convert (MethodCall (List.hd es, [ H.wrapping_operator o ], List.tl es)) (Constant w)
 
+  (* BEGIN PULSE BUILTINS *)
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "from_array"); _ }, [], [], [ t ]); _ }, [e1; _e2]) ->
+      let env, e1 = translate_expr env e1 in
+      let t = translate_type env t in
+      env, possibly_convert e1 (Ref (None, Shared, Slice t))
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "op_Array_Access"); _ }, [], [], _); _ }, [e1; e2]) ->
+      let env, e1 = translate_expr env e1 in
+      let env, e2 = translate_expr env e2 in
+      env, Index (e1, e2)
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "op_Array_Assignment"); _ }, [], [], t); _ }, [ e1; e2; e3]) ->
+      let env, e1 = translate_expr env e1 in
+      let env, e2 = translate_expr env e2 in
+      let env, e3 = translate_expr env e3 in
+      env, Assign (Index (e1, e2), e3, translate_type env (KList.one t))
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "split"); _ }, [], [], [_]); _ }, [e1; e2]) ->
+      let env, e1 = translate_expr env e1 in
+      let env, e2 = translate_expr env e2 in
+      env, MethodCall (e1, ["split_at"], [ e2 ])
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "copy"); _ }, [], [], _); _ }, [e1; e2]) ->
+      let env, e1 = translate_expr env e1 in
+      let env, e2 = translate_expr env e2 in
+      env, MethodCall (e1, ["copy_from_slice"], [ e2 ])
+
+  | EApp ({ node = ETApp ({ node = EQualified (["Pulse"; "Lib"; "Slice"], "len"); _ }, [], [], _); _ }, [e1]) ->
+      let env, e1 = translate_expr env e1 in
+      env, MethodCall (e1, ["len"], [])
+
+  (* END PULSE BUILTINS *)
+
   | EApp ({ node = EQualified ([ "LowStar"; "BufferOps" ], s); _ }, e1 :: _) when KString.starts_with s "op_Bang_Star__" ->
       let env, e1 = translate_expr env e1 in
       (* env, Deref e1 *)
@@ -847,7 +889,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let t = translate_type env b.typ in
       let is_owned_struct =
         match b.typ with
-        | TQualified lid when Idents.LidSet.mem lid env.heap_structs || Idents.LidSet.mem lid env.pointer_holding_structs -> true
+        | TQualified lid when Idents.LidSet.mem lid env.heap_structs -> true
         | _ -> false
       in
       (* TODO how does this play out with the new "translate as non-mut by
@@ -955,10 +997,20 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
   | EPopFrame ->
       failwith "unexpected: EPopFrame"
 
-  | ETuple _ ->
-      failwith "TODO: ETuple"
+  | ETuple es ->
+      let env, es = List.fold_left (fun (env, es) e ->
+        let env, e = translate_expr env e in
+        env, e :: es
+      ) (env, []) es in
+      env, Tuple (List.rev es)
 
   | EMatch (_, e, branches) ->
+      let is_struct =
+        List.length branches > 0 &&
+        match e.typ with
+        | TQualified lid when DataTypeMap.mem (`Struct lid) env.struct_fields -> true
+        | _ -> false
+      in
       let t = translate_type env e.typ in
       let env, e = translate_expr env e in
       let branches = List.map (fun (binders, pat, e) ->
@@ -970,11 +1022,25 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         let _, e = translate_expr env e in
         binders, pat, e
       ) branches in
+      let branches =
+        let is_tuple = match t with Tuple _ when List.length branches > 0 -> true | _ -> false in
+        if not (List.exists (fun (_, p, _) -> p = MiniRust.Wildcard) branches) && not (is_tuple) && not (is_struct) then
+          branches @ [ [], Wildcard, Panic "Incomplete pattern matching" ]
+        else
+          branches
+      in
       env, Match (e, t, branches)
 
-  | ECons _ ->
+  | ECons (cons, es) ->
       (* ECons = variant type *)
-      failwith "TODO: ECons"
+      let t_lid = Helpers.assert_tlid e.typ in
+      let variant_fields = DataTypeMap.find (`Variant (t_lid, cons)) env.struct_fields in
+      let env, fields = List.fold_left2 (fun (env, fields) e (f: MiniRust.struct_field) ->
+        let env, e = translate_expr_with_type env e f.typ in
+        env, (f.name, e) :: fields
+      ) (env, []) es variant_fields in
+      env, Struct (`Variant (lookup_type env t_lid, cons), List.rev fields)
+
 
   | ESwitch (scrut, patexprs) ->
       let t = translate_type env e.typ in
@@ -1005,7 +1071,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
 
   | EEnum lid ->
       let name = lookup_type env (Helpers.assert_tlid e.typ) in
-      env, Name (name @ [ snd lid ])
+      env, Struct (`Variant (name, snd lid), [])
 
   | EFlat fields ->
       (* EFlat = struct type *)
@@ -1017,7 +1083,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         let env, e = translate_expr_with_type env e ret_t in
         env, (f, e) :: fields
       ) (env, []) fields in
-      env, Struct (lookup_type env t_lid, List.rev fields)
+      env, Struct (`Struct (lookup_type env t_lid), List.rev fields)
 
   | EField (e, f) ->
       let env, e_ = translate_expr env e in
@@ -1030,8 +1096,12 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       failwith "TODO: EContinue"
   | EReturn _ ->
       failwith "TODO: EReturn"
-  | EWhile _ ->
-      failwith "TODO: EWhile"
+  | EWhile (e1, e2) ->
+      (* See below *)
+      let env0 = env in
+      let env, e1 = translate_expr env e1 in
+      let _, e2 = translate_expr env e2 in
+      env0, While (e1, e2)
 
   (* The introduction of the unroll_loops macro requires a "fake" binder
      for the iterated value, which messes up with variable substitutions
@@ -1105,14 +1175,20 @@ and translate_pat env (p: Ast.pattern): MiniRust.pat =
          type_name::constructor, followed by fields (named) *)
       let lid = Helpers.assert_tlid p.typ in
       let name = lookup_type env lid in
-      let field_names = DataTypeMap.find (`Variant (lid, cons)) env.struct_fields in
+      let field_names =
+        try DataTypeMap.find (`Variant (lid, cons)) env.struct_fields
+        with Not_found ->
+          KPrint.bprintf "ERROR: variant %s of %a not found\n" cons PrintAst.plid lid;
+          raise Not_found
+      in
       StructP (`Variant (name, cons), List.map2 (fun f p ->
         f.MiniRust.name, translate_pat env p
       ) field_names pats)
   | PUnit -> failwith "TODO: PUnit"
   | PBool _ -> failwith "TODO: PBool"
   | PEnum _ -> failwith "TODO: PEnum"
-  | PTuple _ -> failwith "TODO: PTuple"
+  | PTuple ps ->
+      TupleP (List.map (translate_pat env) ps)
   | PDeref _ -> failwith "TODO: PDeref"
 
 let make_poly (t: MiniRust.typ) n: MiniRust.typ =
@@ -1132,6 +1208,10 @@ let is_handled_primitively = function
   | _ ->
       false
 
+let is_contained t =
+  let t = KList.last t in
+  List.exists (fun t' -> KString.starts_with t t') !Options.contained
+
 (* In Rust, like in C, all the declarations from the current module are in
  * scope immediately. This requires us to duplicate a little bit of work. *)
 let bind_decl env (d: Ast.decl): env =
@@ -1146,8 +1226,20 @@ let bind_decl env (d: Ast.decl): env =
         else
           args
       in
+      let needs_lifetime = List.exists (function
+          | Ast.TQualified lid -> LidSet.mem lid env.pointer_holding_structs
+          | _ -> false
+      ) (t :: (List.map (fun (b: Ast.binder) -> b.typ) args))
+      in
+      let lifetime = if needs_lifetime then Some (MiniRust.Label "a") else None in
+      let config = { default_config with lifetime } in
+
       let parameters = List.map (fun (b: Ast.binder) ->
-        translate_type env b.typ
+        match translate_type_with_config env config b.typ with
+        | Ref (_, m, (Slice (Name (t, _ :: _)) as slice_t)) when is_contained t ->
+            MiniRust.Ref (Some (Label "b"), m, slice_t)
+        | t ->
+            t
       ) args in
       let is_likely_heap_allocation =
         KString.exists (snd lid) "new" ||
@@ -1162,7 +1254,7 @@ let bind_decl env (d: Ast.decl): env =
         | _ ->
             false
         in
-        translate_type_with_config env { default_config with box } t
+        translate_type_with_config env { config with box } t
       in
       push_decl env lid (name, Function (type_parameters, parameters, return_type))
 
@@ -1183,15 +1275,22 @@ let bind_decl env (d: Ast.decl): env =
       push_decl env lid (name, make_poly (translate_type env t) type_parameters)
 
   | DType (lid, _flags, _, _, decl) ->
-      let env, name = translate_lid env lid in
-      let env = push_type env lid name in
+      let env, name =
+        if LidMap.mem lid env.types then
+          (* Name already assigned thanks to a forward declaration *)
+          env, lookup_type env lid
+        else
+          let env, name = translate_lid env lid in
+          let env = push_type env lid name in
+          env, name
+      in
       match decl with
       | Flat fields ->
           (* These sets are mutually exclusive, so we don't box *and* introduce a
              lifetime at the same time *)
           let box = Idents.LidSet.mem lid env.heap_structs in
           let lifetime = Idents.LidSet.mem lid env.pointer_holding_structs in
-          KPrint.bprintf "%a (FLAT): lifetime=%b box=%b\n" PrintAst.Ops.plid lid lifetime box;
+          KPrint.bprintf "%a (FLAT): lifetime=%b box=%b --> %s\n" PrintAst.Ops.plid lid lifetime box (String.concat "::" name);
           let lifetime =
             if lifetime then
               Some (MiniRust.Label "a")
@@ -1202,18 +1301,26 @@ let bind_decl env (d: Ast.decl): env =
             let f = Option.get f in
             { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t }
           ) fields in
-          { env with struct_fields = DataTypeMap.add (`Struct lid) fields env.struct_fields }
+          { env with
+            struct_fields = DataTypeMap.add (`Struct lid) fields env.struct_fields }
       | Variant branches ->
           let box = Idents.LidSet.mem lid env.heap_structs in
           let lifetime = Idents.LidSet.mem lid env.pointer_holding_structs in
-          KPrint.bprintf "%a (VARIANT): lifetime=%b box=%b\n" PrintAst.Ops.plid lid lifetime box;
+          KPrint.bprintf "%a (VARIANT): lifetime=%b box=%b --> %s\n" PrintAst.Ops.plid lid lifetime box (String.concat "::" name);
+          let lifetime =
+            if lifetime then
+              Some (MiniRust.Label "a")
+            else
+              None
+          in
           List.fold_left (fun env (cons, fields) ->
             let cons_lid = `Variant (lid, cons) in
             let fields = List.map (fun (f, (t, _)) ->
-              { MiniRust.name = f; visibility = Some Pub; typ = translate_type env t }
+              { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t }
             ) fields
             in
-            { env with struct_fields = DataTypeMap.add cons_lid fields env.struct_fields }
+            { env with
+              struct_fields = DataTypeMap.add cons_lid fields env.struct_fields }
           ) env branches
       | _ ->
           env
@@ -1248,22 +1355,36 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
   match d with
   | DFunction (_, _, _, _, _, lid, _, _) when is_handled_primitively lid ->
       None
-  | DFunction (_cc, flags, n_cgs, type_parameters, _t, lid, args, body) ->
-      assert (type_parameters = 0 && n_cgs = 0);
+  | DFunction (_cc, flags, n_cgs, type_parameters, ret_t, lid, args, body) ->
       if Options.debug "rs" then
         KPrint.bprintf "Ast.DFunction (%a)\n" PrintAst.Ops.plid lid;
+      assert (type_parameters = 0 && n_cgs = 0);
+      let needs_lifetime = List.exists (function
+          | Ast.TQualified lid -> LidSet.mem lid env.pointer_holding_structs
+          | _ -> false
+      ) (ret_t :: (List.map (fun (x: Ast.binder) -> x.typ) args))
+      in
+      let lifetime = if needs_lifetime then Some (MiniRust.Label "a") else None in
+      let generic_params = match lifetime with Some l -> [ MiniRust.Lifetime l ] | None -> [] in
+
       let name, parameters, return_type =
         match lookup_decl env lid with
         | name, Function (_, parameters, return_type) -> name, parameters, return_type
         | _ -> failwith "impossible"
       in
+      let generic_params =
+        if List.exists (function MiniRust.Ref (l, _, _) when l <> lifetime -> true | _ -> false) parameters then
+          MiniRust.Lifetime (Label "b") :: generic_params
+        else
+          generic_params
+      in
       let body, args = if parameters = [] then DeBruijn.subst Helpers.eunit 0 body, [] else body, args in
       let parameters = List.map2 (fun typ a -> { MiniRust.mut = false; name = a.Ast.node.Ast.name; typ; ref = false }) parameters args in
       let env = List.fold_left push env parameters in
       let _, body = translate_expr_with_type env body return_type in
       let meta = translate_meta flags in
       let inline = List.mem Common.Inline flags in
-      Some (MiniRust.Function { type_parameters; parameters; return_type; body; name; meta; inline })
+      Some (MiniRust.Function { type_parameters; parameters; return_type; body; name; meta; inline; generic_params })
 
   | DGlobal (flags, lid, _, _t, e) ->
       let name, typ = lookup_decl env lid in
@@ -1296,18 +1417,25 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
           in
           let generic_params = match lifetime with Some l -> [ MiniRust.Lifetime l ] | None -> [] in
           let fields = DataTypeMap.find (`Struct lid) env.struct_fields in
-          Some (Struct { name; meta; fields; generic_params })
+          let derives = [] in
+          Some (Struct { name; meta; fields; generic_params; derives })
       | Enum idents ->
           (* No need to do name binding here since there are entirely resolved via the type name. *)
           let items = List.map (fun i -> snd i, None) idents in
-          Some (Enumeration { name; meta; items; derives = [ PartialEq; Clone; Copy ] })
+          let derives = [] in
+          Some (Enumeration { name; meta; items; derives; generic_params = [] })
       | Abbrev t ->
           let has_inner_pointer = (object
-            inherit [_] Ast.reduce
+            inherit [_] Ast.reduce as super
             method zero = false
             method plus = (||)
             method! visit_TBuf _ _ _ = true
             method! visit_TQualified _ lid = Idents.LidSet.mem lid env.pointer_holding_structs
+            method! visit_TApp env lid ts =
+              if lid = (["Pulse"; "Lib"; "Slice"], "slice") then
+                true
+              else
+                super#visit_TApp env lid ts
           end)#visit_typ () t in
           let lifetime, generic_params =
             if has_inner_pointer then
@@ -1318,15 +1446,26 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
           let t = translate_type_with_config env { default_config with lifetime } t in
           Some (Alias { name; meta; body = t; generic_params })
       | Variant branches ->
-          let items = List.map (fun (cons, fields) ->
-            cons, Some (List.map (fun (f, (t, _mut)) ->
-              { name = f; typ = translate_type env t; MiniRust.visibility = None }
-            ) fields)
+          let lifetime =
+            (* creative naming for the lifetime *)
+            if Idents.LidSet.mem lid env.pointer_holding_structs then
+              Some (MiniRust.Label "a")
+            else
+              None
+          in
+          let generic_params = match lifetime with Some l -> [ MiniRust.Lifetime l ] | None -> [] in
+          let items = List.map (fun (cons, _) ->
+            let fields = DataTypeMap.find (`Variant (lid, cons)) env.struct_fields in
+            let fields = List.map (fun (x: MiniRust.struct_field) -> { x with visibility = None }) fields in
+            cons, Some fields
           ) branches in
-          Some (Enumeration { name; meta; items = items; derives = [] })
-      | Union _
-      | Forward _ ->
+          let derives = [] in
+          Some (Enumeration { name; meta; items; derives; generic_params })
+      | Union _ ->
           Warn.failwith "TODO: Ast.DType (%a)\n" PrintAst.Ops.plid lid
+      | Forward _ ->
+          (* Nothing to translate here *)
+          None
 
 let identify_path_components_rev filename =
   let components = ref [] in
@@ -1349,6 +1488,8 @@ let compute_struct_info files =
       match decl with
       | Ast.DType (lid, _, _, _, Flat fields) ->
           Idents.LidMap.add lid fields acc
+      | Ast.DType (lid, _, _, _, Variant branches) ->
+          Idents.LidMap.add lid (List.concat_map (fun (_, fields) -> List.map (fun (c, f) -> Some c, f) fields) branches) acc
       | _ ->
           acc
     ) acc decls
@@ -1415,7 +1556,12 @@ let compute_struct_info files =
           end)#visit_fields_t_opt () fields
         in
         let directly_contains_pointers =
-          List.exists (fun (_, (t, _)) -> match t with Ast.TBuf _ -> true | _ -> false) fields
+          List.exists (fun (_, (t, _)) ->
+            match t with
+            | Ast.TBuf _ -> true
+            | TApp ((["Pulse"; "Lib"; "Slice"], "slice"), [ _ ]) -> true
+            | _ -> false
+          ) fields
         in
         directly_contains_pointers || recursively_contains_pointers
     in
@@ -1429,9 +1575,12 @@ let compute_struct_info files =
 
   (* The base case of the fixpoint is structs that are *not returned* and still contain
      pointers. We backpropagate starting from that. *)
-  let with_inner_pointers = struct_fixpoint (fun lid -> not (Idents.LidSet.mem lid returned)) in
+  let with_inner_pointers = struct_fixpoint (fun lid ->
+    if !Options.no_box then true else not (Idents.LidSet.mem lid returned)
+  ) in
   (* This one eliminates structs that are in the returned-set but do not contain pointers. *)
   let returned = struct_fixpoint (fun lid -> Idents.LidSet.mem lid returned) in
+  let returned = if !Options.no_box then LidSet.empty else returned in
 
   assert Idents.LidSet.(is_empty (inter with_inner_pointers returned));
 
@@ -1469,6 +1618,13 @@ let translate_files files =
     let total = List.length decls in
     let env = { env with prefix } in
 
+    (* Step 0: filter stuff with builtin treatment *)
+    let decls = List.filter (fun d ->
+      match Ast.lid_of_decl d with
+      | ["Pulse"; "Lib"; "Slice"], ("from_array" | "op_Array_Access" | "op_Array_Assignment" | "split" | "copy") -> false
+      | _ -> true
+    ) decls in
+
     (* Step 1: bind all declarations and add them to the environment with their types *)
     let env = List.fold_left (fun env d ->
       try
diff --git a/lib/Builtin.ml b/lib/Builtin.ml
index e7446d0a..b2a4b053 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -434,7 +434,12 @@ let is_model name =
       "C_Compat_String";
       "FStar_String";
       "Steel_SpinLock"
-    ]
+    ] || (
+      Options.rust () &&
+      List.mem name [
+        "Pulse_Lib_Slice"
+      ]
+    )
 
 (* We have several different treatments. *)
 let prepare files =
diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml
index 4a922c79..de945a44 100644
--- a/lib/DataTypes.ml
+++ b/lib/DataTypes.ml
@@ -203,7 +203,7 @@ let build_scheme_map files =
           Hashtbl.add map lid ToEnum (* logic replicated in Monomorphization *)
         else if List.length branches = 1 then
           Hashtbl.add map lid (ToFlat (List.map fst (snd (List.hd branches))))
-        else if List.length non_constant = 1 then
+        else if List.length non_constant = 1 && not (Options.rust ()) then
           Hashtbl.add map lid (ToFlatTaggedUnion branches)
         else
           Hashtbl.add map lid (ToTaggedUnion branches);
diff --git a/lib/Inlining.ml b/lib/Inlining.ml
index 7a46467f..a08654a2 100644
--- a/lib/Inlining.ml
+++ b/lib/Inlining.ml
@@ -201,7 +201,7 @@ let mk_crate_of files =
     StringMap.find f map
 
 (** This phase is concerned with three whole-program, cross-compilation-unit
-    analyses, performed ina single pass:
+    analyses, performed in a single pass:
     - assign correct visibility to declarations in the presence of bundling,
       static-header, mutually-recursive definitions, stackinline,
       inline_for_extraction, the friend mechanism, and the krmlinit_globals
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index a98cc1d2..126936e7 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -1,7 +1,7 @@
 (* A minimalistic representation of Rust *)
 
 module Name = struct
-  type t = string list
+  type t = string list [@@ deriving show ]
   let compare = compare
 end
 
@@ -12,7 +12,7 @@ type borrow_kind = borrow_kind_ [@ opaque ]
 and constant = Constant.t [@ opaque ]
 and width = Constant.width [@ opaque ]
 and op = Constant.op [@ opaque ]
-and name = Name.t [@ opaque ]
+and name = Name.t [@ visitors.opaque ]
 
 (* Some design choices.
    - We don't intend to perform any deep semantic transformations on this Rust
@@ -36,7 +36,7 @@ type typ =
   | Unit [@name "tunit"]
   | Function of int * typ list * typ
   | Name of name * generic_param list [@name "tname"]
-  | Tuple of typ list
+  | Tuple of typ list [@name "ttuple"]
   | App of typ * typ list
   | Bound of db_index
 [@@deriving show,
@@ -62,8 +62,7 @@ let usize = Constant SizeT
 
 type binding = { name: string; typ: typ; mut: bool; ref: bool (* only for pattern variables *) }
 [@@deriving show,
-  visitors { variety = "map"; name = "map_binding";
-    ancestors = [ "map_misc"; "map_typ" ] }]
+  visitors { variety = "map"; name = "map_binding"; ancestors = [ "map_misc"; "map_typ" ] }]
 
 (* Top-level declarations *)
 
@@ -96,8 +95,9 @@ and expr =
   | While of expr * expr
   | MethodCall of expr * name * expr list
   | Range of expr option * expr option * bool (* inclusive? *)
-  | Struct of name * (string * expr) list
+  | Struct of struct_name * (string * expr) list
   | Match of expr * typ * match_arm list
+  | Tuple of expr list
 
   (* Place expressions *)
   | Var of db_index
@@ -120,11 +120,16 @@ and match_arm = binding list * pat * expr
 and pat =
   | Literal of constant
   | Wildcard
-  (* A "struct pattern" per the Rust grammar that covers both Enum and Struct *)
-  | StructP of ([ `Struct of name | `Variant of name * string ] [@ opaque]) * (string * pat) list
+  | TupleP of pat list
+  | StructP of struct_name * (string * pat) list
   | VarP of db_index
   | OpenP of open_var
 
+(* In the Rust grammar, both variants and structs are covered by the struct
+  case. We disambiguate between the two *)
+and struct_name =
+  [ `Struct of name | `Variant of name * string ] [@ opaque]
+
 and open_var = {
   name: string;
   atom: atom_t
@@ -163,6 +168,7 @@ type decl =
     body: expr;
     meta: meta;
     inline: bool;
+    generic_params: generic_param list;
   }
   | Constant of {
     name: name;
@@ -175,10 +181,12 @@ type decl =
     items: item list;
     derives: trait list;
     meta: meta;
+    generic_params: generic_param list;
   }
   | Struct of {
     name: name;
     fields: struct_field list;
+    derives: trait list;
     meta: meta;
     generic_params: generic_param list;
   }
diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml
index e5ee7951..f2880b77 100644
--- a/lib/Monomorphization.ml
+++ b/lib/Monomorphization.ml
@@ -147,7 +147,7 @@ module NameGen = struct
         let n = Printf.sprintf "%s_%02x" n (hash land 0xFF) in
         let n = Idents.mk_fresh n (fun n -> Hashtbl.mem seen (m, n)) in
         Hashtbl.add seen (m, n) ();
-        (m, n), [ Common.AutoGenerated; gen_comment lid ts extra ] 
+        (m, n), [ Common.AutoGenerated; gen_comment lid ts extra ]
     else
       let doc =
         separate_map underscore print_typ ts ^^
@@ -432,7 +432,7 @@ let monomorphize_data_types map = object(self)
       if Options.debug "data-types-traversal" then
         KPrint.bprintf "decl %a\n" plid (lid_of_decl d);
       match d with
-      | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not (Hashtbl.mem state (tuple_lid, args, [])) ->
+      | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) ->
           Hashtbl.remove map lid;
           if Options.debug "monomorphization" then
             KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args));
@@ -514,13 +514,19 @@ let monomorphize_data_types map = object(self)
       super#visit_DType env name flags n d
 
   method! visit_ETuple under_ref es =
-    EFlat (List.mapi (fun i e -> Some (self#field_at i), self#visit_expr under_ref e) es)
+    if not !Options.keep_tuples then
+      EFlat (List.mapi (fun i e -> Some (self#field_at i), self#visit_expr under_ref e) es)
+    else
+      super#visit_ETuple under_ref es
 
   method! visit_PTuple under_ref pats =
-    PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats)
+    if not !Options.keep_tuples then
+      PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats)
+    else
+      super#visit_PTuple under_ref pats
 
   method! visit_TTuple under_ref ts =
-    if not (has_variables ts) && not (has_cg_array ts) then
+    if not !Options.keep_tuples && not (has_variables ts) && not (has_cg_array ts) then
       TQualified (self#visit_node under_ref (tuple_lid, ts, []))
     else
       super#visit_TTuple under_ref ts
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 3029568c..6028d525 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -33,27 +33,87 @@
 open MiniRust
 open PrintMiniRust
 
-module NameMap = Map.Make(Name)
-module DataTypeMap = Map.Make(struct
+module DataType = struct
   type t = [ `Struct of Name.t | `Variant of Name.t * string ]
   let compare = compare
-end)
+end
+
+module NameMap = Map.Make(Name)
+module DataTypeMap = Map.Make(DataType)
 module VarSet = Set.Make(Atom)
+module IntSet = Set.Make(Int)
 
+module TraitSet = Set.Make(struct
+  type t = MiniRust.trait
+  let compare = compare
+end)
+
+(* Because of (possibly mutual) recursion, we need to express mutability
+   inference as a fixed point computation. To each top-level function name, we
+   map a property, which is the set of parameters that have to be promoted to
+   mutable borrow (mut parameters themselves don't matter -- they're just passed
+   by copy and only the function-local copy is mutable). Because parameters may
+   or may not have unique names, we identify a function f's parameter with their
+   indices. *)
+module F = Fix.Fix.ForOrderedType(Name)(Fix.Prop.Set(Set.Make(Int)))
+
+(* The fixed point inference will need to compute unrelated information on the
+   go, namely, which struct fields need to become mutable. It is difficult to
+   express this as a system of equations, so we simply record those in some
+   global state. *)
+let structs: (DataType.t, MiniRust.struct_field list) Hashtbl.t =
+  Hashtbl.create 31
+
+(* Our environments only contain signatures, and as such, are immutable -- these
+   signatures will need to be augmented with information from the valuation to
+   get the intended type. *)
 type env = {
-  seen: typ list NameMap.t;
-  (* A map from Rust name to the list of fields for that struct. *)
-  structs: MiniRust.struct_field list DataTypeMap.t;
+  signatures: typ list NameMap.t;
 }
 
-let debug env =
+(* Promote a reference to mutable *)
+let make_mut t =
+  match t with
+  | MiniRust.Ref (l, _, t) ->
+      MiniRust.Ref (l, Mut, t)
+  | _ ->
+      failwith "unexpected: not a ref"
+
+(* Adjust the types of a function's parameters, originally without Mut
+   qualifiers, based on what is currently computed in the valuation. *)
+let adjust ts mut =
+  List.mapi (fun i t ->
+    if IntSet.mem i mut then
+      make_mut t
+    else
+      t
+  ) ts
+
+(* Convert the mutability qualifiers into a set suitable for fitting as a
+   property. *)
+let distill ts =
+  IntSet.of_list (List.filter_map (fun x -> x) (List.mapi (fun i t ->
+    match t with
+    | MiniRust.Ref (_, Mut, _) -> Some i
+    | _ -> None
+  ) ts))
+
+(* Get the type of the arguments of `name`, based on the current state of
+   `valuation` *)
+let lookup env valuation name =
+  (* KPrint.bprintf "lookup: %a\n" PrintMiniRust.pname name; *)
+  let ts = NameMap.find name env.signatures in
+  adjust ts (valuation name)
+
+let debug env valuation =
   KPrint.bprintf "OptimizeMiniRust -- ENV DEBUG\n";
   NameMap.iter (fun n t ->
+    let t = adjust t (valuation n) in
     KPrint.bprintf "%s: %a\n" (String.concat "::" n) ptyps t
-  ) env.seen
+  ) env.signatures
 
+(* Now moving on to the local state, for a single function body. *)
 type known = {
-  structs: MiniRust.struct_field list DataTypeMap.t;
   v: VarSet.t;
   r: VarSet.t;
   p: VarSet.t;
@@ -90,30 +150,37 @@ let is_mut_borrow = function
   | Tuple [Ref (_, Mut, _); Ref (_, Mut, _)] -> true
   | _ -> false
 
-let make_mut_borrow = function
+let rec make_mut_borrow = function
   | Ref (l, _, t) -> Ref (l, Mut, t)
   | Tuple [Ref (l1, _, t1); Ref (l2, _, t2)] -> Tuple [Ref (l1, Mut, t1); Ref (l2, Mut, t2)]
   | Vec t -> Vec t
   | App (Name (["Box"], []), [_]) as t -> t
+  | Array (t, n) -> Array (make_mut_borrow t, n)
   | t ->
       KPrint.bprintf "[make_mut_borrow] %a\n" ptyp t;
       failwith "impossible: make_mut_borrow"
 
 (* Only works for struct types. *)
-let add_mut_field ty f known =
-  let n = assert_name ty in
-  let fields = DataTypeMap.find (`Struct n) known.structs in
+let add_mut_field (n: DataType.t) f =
+  let fields = Hashtbl.find structs n in
   (* Update the mutability of the field element *)
   let fields = List.map (fun (sf: MiniRust.struct_field) ->
     if sf.name = f then {sf with typ = make_mut_borrow sf.typ} else sf) fields in
-  {known with structs = DataTypeMap.add (`Struct n) fields known.structs}
+  Hashtbl.replace structs n fields
 
-let retrieve_pair_type = function
+let retrieve_pair_type (t: typ) =
+  match t with
   | Tuple [e1; e2] -> assert (e1 = e2); e1
   | _ -> failwith "impossible: retrieve_pair_type"
 
-let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr =
-  (* KPrint.bprintf "[infer] %a @ %a\n" pexpr e ptyp expected; *)
+
+(*  known is the local state, which contains the V, R and P states (see above)
+
+    additionally, this function relies on `valuation` (for the least fixed point
+    formulation of this analysis) and mutates `structs` globally *)
+let rec infer_expr (env: env) valuation (expected: typ) (known: known) (e: expr): known * expr =
+  if Options.debug "rs-mut" then
+    KPrint.bprintf "[infer_expr] %a @ %a\n" pexpr e ptyp expected;
   match e with
   | Borrow (k, e) ->
       (* If we expect this borrow to be a mutable borrow, then we make it a mutable borrow
@@ -125,9 +192,19 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         | Open { atom; _ } ->
             add_mut_var atom known, Borrow (Mut, e)
         | Index (e1, (Range _ as r))  ->
-            let known, e1 = infer env expected known e1 in
+            let known, e1 = infer_expr env valuation expected known e1 in
             known, Borrow (Mut, Index (e1, r))
 
+        | Index (Open { atom; _ } as e1, e2)  ->
+            let known = add_mut_var atom known in
+            let known, e2 = infer_expr env valuation Unit known e2 in
+            known, Borrow (Mut, Index (e1, e2))
+
+        | Index (Borrow (_, (Open { atom; _ } as e1)), e2)  ->
+            let known = add_mut_var atom known in
+            let known, e2 = infer_expr env valuation Unit known e2 in
+            known, Borrow (Mut, Index (Borrow (Mut, e1), e2))
+
         | Field (Open _, "0", None)
         | Field (Open _, "1", None) -> failwith "TODO: borrowing slices"
 
@@ -141,10 +218,10 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
             add_mut_borrow atom known, Borrow (Mut, e)
 
         | _ ->
-            KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" pexpr e;
+            KPrint.bprintf "[infer_expr-mut, borrow] borrwing %a is not supported\n" pexpr e;
             failwith "TODO: borrowing something other than a variable"
       else
-        let known, e = infer env (assert_borrow expected) known e in
+        let known, e = infer_expr env valuation (assert_borrow expected) known e in
         known, Borrow (k, e)
 
   | Open { atom; _ } ->
@@ -156,62 +233,59 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         known, e
 
   | Let (b, e1, e2) ->
-      (* KPrint.bprintf "[infer-mut,let] %a\n" pexpr e; *)
+      (* KPrint.bprintf "[infer_expr-mut,let] %a\n" pexpr e; *)
       let a, e2 = open_ b e2 in
-      (* KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a); *)
-      let known, e2 = infer env expected known e2 in
+      (* KPrint.bprintf "[infer_expr-mut,let] opened %s[%s]\n" b.name (show_atom_t a); *)
+      let known, e2 = infer_expr env valuation expected known e2 in
       let mut_var = want_mut_var a known in
       let mut_borrow = want_mut_borrow a known in
-      (* KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name *)
-      (*   (show_atom_t a) *)
-      (*   ptyp b.typ mut_var mut_borrow; *)
+      (* KPrint.bprintf "[infer_expr-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
+        (show_atom_t a)
+        ptyp b.typ mut_var mut_borrow;
+      *)
       let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in
-      let known, e1 = infer env t1 known e1 in
+      let known, e1 = infer_expr env valuation t1 known e1 in
       known, Let ({ b with mut = mut_var; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
 
   | Call (Name n, targs, es) ->
-      if NameMap.mem n env.seen then
-        (* TODO: substitute targs in ts -- for now, we assume we don't have a type-polymorphic
-           function that gets instantiated with a reference type *)
-        let ts = NameMap.find n env.seen in
-        let known, es = List.fold_left2 (fun (known, es) e t ->
-            let known, e = infer env t known e in
-            known, e :: es
-          ) (known, []) es ts
-        in
-        let es = List.rev es in
-        known, Call (Name n, targs, es)
-      else if n = ["lowstar";"ignore";"ignore"] then
+      if n = ["lowstar";"ignore";"ignore"] then
         (* Since we do not have type-level substitutions in MiniRust, we special-case ignore here.
            Ideally, it would be added to builtins with `Bound 0` as a suitable type for the
            argument. *)
-        let known, e = infer env (KList.one targs) known (KList.one es) in
+        let known, e = infer_expr env valuation (KList.one targs) known (KList.one es) in
         known, Call (Name n, targs, [ e ])
       else if n = ["Box"; "new"] then
-        let known, e = infer env (KList.one targs) known (KList.one es) in
-        known, Call (Name n, targs, [ e ])
-      else if n = [ "lib"; "memzero0"; "memzero" ] then (
+        (* FIXME: we no longer have the type handy so we can't recursively
+           descend on KList.one es *)
+        known, Call (Name n, targs, es)
+      else if n = [ "lib"; "memzero0"; "memzero" ] then
         (* Same as ignore above *)
-        assert (List.length es = 2);
         let e1, e2 = KList.two es in
-        let known, e1 = infer env (Ref (None, Mut, Slice (KList.one targs))) known e1 in
-        let known, e2 = infer env u32 known e2 in
+        let known, e1 = infer_expr env valuation (Ref (None, Mut, Slice (KList.one targs))) known e1 in
+        let known, e2 = infer_expr env valuation u32 known e2 in
         known, Call (Name n, targs, [ e1; e2 ])
-      ) else (
-        KPrint.bprintf "[infer-mut,call] recursing on %s\n" (String.concat " :: " n);
-        debug env;
-        failwith "TODO: recursion or missing function"
-      )
+      else
+        (* TODO: substitute targs in ts -- for now, we assume we don't have a type-polymorphic
+           function that gets instantiated with a reference type *)
+        let ts = lookup env valuation n in
+        let known, es = List.fold_left2 (fun (known, es) e t ->
+            let known, e = infer_expr env valuation t known e in
+            known, e :: es
+          ) (known, []) es ts
+        in
+        let es = List.rev es in
+        known, Call (Name n, targs, es)
 
-  | Call (Operator o, [], _) -> begin match o with
+  | Call (Operator o, [], _) ->
       (* Most operators are wrapping and were translated to a methodcall.
          We list the few remaining ones here *)
+      begin match o with
       | Add | Sub
       | BOr | BAnd | BXor | BNot
       | Eq | Neq | Lt | Lte | Gt | Gte
       | And | Or | Xor | Not -> known, e
       | _ ->
-        KPrint.bprintf "[infer-mut,call] %a not supported\n" pexpr e;
+        KPrint.bprintf "[infer_expr-mut,call] %a not supported\n" pexpr e;
         failwith "TODO: operator not supported"
     end
 
@@ -219,10 +293,10 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       failwith "TODO: Call"
 
   (* atom = e3 *)
-  | Assign (Open { atom; _ }, e3, t) ->
-      (* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
-      let known, e3 = infer env t known e3 in
-      add_mut_var atom known, e3
+  | Assign (Open { atom; _ } as e1, e3, t) ->
+      (* KPrint.bprintf "[infer_expr-mut,assign] %a\n" pexpr e; *)
+      let known, e3 = infer_expr env valuation t known e3 in
+      add_mut_var atom known, Assign (e1, e3, t)
 
   (* atom[e2] = e2 *)
   | Assign (Index (Open { atom; _ } as e1, e2), e3, t)
@@ -237,60 +311,66 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
   (* atom.1[e2] = e3 *)
   | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t) ->
-      (* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
+      (* KPrint.bprintf "[infer_expr-mut,assign] %a\n" pexpr e; *)
       let known = add_mut_borrow atom known in
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env t known e3 in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
-  (* x.f[e2] = e3 *)
+  (* (x.f)[e2] = e3 *)
   | Assign (Index (Field (_, f, st (* optional type *)) as e1, e2), e3, t) ->
-      let known = add_mut_field st f known in
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env t known e3 in
+      add_mut_field (`Struct (assert_name st)) f;
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
   (* (&atom)[e2] = e3 *)
   | Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
-      (* KPrint.bprintf "[infer-mut,assign] %a\n" pexpr e; *)
+      (* KPrint.bprintf "[infer_expr-mut,assign] %a\n" pexpr e; *)
       let known = add_mut_var atom known in
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env t known e3 in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation t known e3 in
       known, Assign (Index (Borrow (Mut, e1), e2), e3, t)
 
   | Assign (Field (_, "0", None), _, _)
   | Assign (Field (_, "1", None), _, _) ->
       failwith "TODO: assignment on slice"
 
-  (* (atom.f)[e2] = e3 *)
+  (* (atom[e2]).f = e3 *)
   | Assign (Field (Index ((Open {atom; _} as e1), e2), f, st), e3, t) ->
       let known = add_mut_borrow atom known in
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env t known e3 in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation t known e3 in
       known, Assign (Field (Index (e1, e2), f, st), e3, t)
 
   (* (&n)[e2] = e3 *)
   | Assign (Index (Borrow (_, Name n), e2), e3, t) ->
       (* This case should only occur for globals. For now, we simply mutably borrow it *)
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env t known e3 in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation t known e3 in
       known, Assign (Index (Borrow (Mut, Name n), e2), e3, t)
 
   (* (&(&atom)[e2])[e3] = e4 *)
   | Assign (Index (Borrow (_, Index (Borrow (_, (Open {atom; _} as e1)), e2)), e3), e4, t) ->
       let known = add_mut_var atom known in
-      let known, e2 = infer env usize known e2 in
-      let known, e3 = infer env usize known e3 in
-      let known, e4 = infer env t known e4 in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation usize known e3 in
+      let known, e4 = infer_expr env valuation t known e4 in
       known, Assign (Index (Borrow (Mut, Index (Borrow (Mut, e1), e2)), e3), e4, t)
 
+  (* (&(atom.f))[e1] = e2 *)
+  | Assign (Index (Borrow (_, Field (Open {atom; _} as e1, f, t)), e2), e3, t1) ->
+      let known = add_mut_var atom known in
+      let known, e2 = infer_expr env valuation usize known e2 in
+      let known, e3 = infer_expr env valuation usize known e3 in
+      known, Assign (Index (Borrow (Mut, Field (e1, f, t)), e2), e3, t1)
+
   | Assign _ ->
-      KPrint.bprintf "[infer-mut,assign] %a unsupported\n" pexpr e;
+      KPrint.bprintf "[infer_expr-mut,assign] %a unsupported %s\n" pexpr e (show_expr e);
       failwith "TODO: unknown assignment"
 
-  | AssignOp _ -> failwith "AssignOp nodes should only be introduced after mutability inference"
+  | AssignOp _ -> failwith "AssignOp nodes should only be introduced after mutability infer_exprence"
   | Var _
-  | Array _
   | VecNew _
   | Name _
   | Constant _
@@ -300,13 +380,37 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Operator _ ->
       known, e
 
+  | Array (List es) as e0 ->
+      (* FIXME: we are sometimes recursively called with not enough type
+         information from the copy_from_slice case, below *)
+      if expected <> Unit then
+        let t_elt = match expected with Slice t | Array (t, _) -> t | _ -> failwith (KPrint.bsprintf "impossible: %a" ptyp expected) in
+        let known, es = List.fold_left (fun (known, es) e ->
+          let known, e = infer_expr env valuation t_elt known e in
+          known, e :: es
+        ) (known, []) es in
+        let es = List.rev es in
+        known, Array (List es)
+      else
+        known, e0
+
+  | Array (Repeat (e, n)) as e0 ->
+      (* FIXME: we are sometimes recursively called with not enough type
+         information from the copy_from_slice case, below *)
+      if expected <> Unit then
+        let t_elt = match expected with Slice t | Array (t, _) -> t | _ -> failwith (KPrint.bsprintf "impossible: %a" ptyp expected) in
+        let known, e = infer_expr env valuation t_elt known e in
+        known, Array (Repeat (e, n))
+      else
+        known, e0
+
   | IfThenElse (e1, e2, e3) ->
-      let known, e1 = infer env bool known e1 in
-      let known, e2 = infer env expected known e2 in
+      let known, e1 = infer_expr env valuation bool known e1 in
+      let known, e2 = infer_expr env valuation expected known e2 in
       let known, e3 =
         match e3 with
         | Some e3 ->
-            let known, e3 = infer env expected known e3 in
+            let known, e3 = infer_expr env valuation expected known e3 in
             known, Some e3
         | None ->
             known, None
@@ -315,15 +419,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
 
   | As (e, t) ->
       (* Not really correct, but As is only used for integer casts *)
-      let known, e = infer env t known e in
+      let known, e = infer_expr env valuation t known e in
       known, As (e, t)
 
   | For (b, e1, e2) ->
-      let known, e2 = infer env Unit known e2 in
+      let known, e2 = infer_expr env valuation Unit known e2 in
       known, For (b, e1, e2)
 
   | While (e1, e2) ->
-      let known, e2 = infer env Unit known e2 in
+      let known, e2 = infer_expr env valuation Unit known e2 in
       known, While (e1, e2)
 
   | MethodCall (e1, m, e2) ->
@@ -335,28 +439,33 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       | [ "wrapping_add" | "wrapping_div" | "wrapping_mul"
       |   "wrapping_neg" | "wrapping_rem" | "wrapping_shl"
       |   "wrapping_shr" | "wrapping_sub"
-      |   "to_vec" | "into_boxed_slice" | "into" ] ->
+      |   "to_vec" | "into_boxed_slice" | "into" | "len" ] ->
           known, MethodCall (e1, m, e2)
       | ["split_at"] ->
           assert (List.length e2 = 1);
-          let known, e2 = infer env usize known (List.hd e2) in
+          let known, e2 = infer_expr env valuation usize known (List.hd e2) in
           let t1 = retrieve_pair_type expected in
-          let known, e1 = infer env t1 known e1 in
+          let known, e1 = infer_expr env valuation t1 known e1 in
           if is_mut_borrow expected then
             known, MethodCall (e1, ["split_at_mut"], [e2])
           else
             known, MethodCall (e1, m, [e2])
-      | ["copy_from_slice"] -> begin match e1 with
+      | ["copy_from_slice"] ->
+          assert (List.length e2 = 1);
+          begin match e1 with
           | Index (dst, range) ->
-            assert (List.length e2 = 1);
-            (* We do not have access to the types of e1 and e2. However, the concrete
-               type should not matter during mut inference, we thus use Unit as a default *)
-            let known, dst = infer env (Ref (None, Mut, Unit)) known dst in
-            let known, e2 = infer env (Ref (None, Shared, Unit)) known (List.hd e2) in
-            known, MethodCall (Index (dst, range), m, [e2])
-          (* The AstToMiniRust translation should always introduce an index
-              as the left argument of copy_from_slice *)
-          | _ -> failwith "ill-formed copy_from_slice"
+              (* We do not have access to the types of e1 and e2. However, the concrete
+                 type should not matter during mut infer_exprence, we thus use Unit as a default *)
+              let known, dst = infer_expr env valuation (Ref (None, Mut, Unit)) known dst in
+              let known, e2 = infer_expr env valuation (Ref (None, Shared, Unit)) known (List.hd e2) in
+              known, MethodCall (Index (dst, range), m, [e2])
+          | _ ->
+              (* The other form stems from Pulse.Lib.Slice which, here, puts an
+                  actual slice on the left-hand side. *)
+              let e2 = KList.one e2 in
+              let known, e1 = infer_expr env valuation (Ref (None, Mut, Slice Unit)) known e1 in
+              let known, e2 = infer_expr env valuation (Ref (None, Shared, Slice Unit)) known e2 in
+              known, MethodCall (e1, m, [e2])
           end
       | [ "push" ] -> begin match e1 with
           | Open {atom; _} -> add_mut_var atom known, MethodCall (e1, m, e2)
@@ -370,26 +479,30 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Range (e1, e2, b) ->
       known, Range (e1, e2, b)
 
-  | Struct (name, _es) ->
+  | Struct (name, es) ->
       (* The declaration of the struct should have been traversed beforehand, hence
          it should be in the map *)
-      let _fields_mut = DataTypeMap.find (`Struct name) known.structs in
-      (* TODO: This should be modified depending on the current struct
-         in known. *)
-      known, e
+      let fields_mut = Hashtbl.find structs name in
+      let known, es = List.fold_left2 (fun (known, es) (fn, e) (f: struct_field) ->
+        assert (fn = f.name);
+        let known, e = infer_expr env valuation f.typ known e in
+        known, (fn, e) :: es
+      ) (known, []) es fields_mut in
+      let es = List.rev es in
+      known, Struct (name, es)
 
   | Match (e_scrut, t, arms) as _e_match ->
-      (* We have the expected type of the scrutinee: recurse *)
-      let known, e = infer env t known e_scrut in
+      (* We have the expected type of the scrutinee: valuation *)
+      let known, e = infer_expr env valuation t known e_scrut in
       let known, arms = List.fold_left_map (fun known ((bs, _, _) as branch) ->
         let atoms, pat, e = open_branch branch in
-        let known, e = infer env expected known e in
+        let known, e = infer_expr env valuation expected known e in
         (* Given a pattern p of type t, and a known map:
           i.  if the pattern contains f = x *and* x is in R, then the field f of
               the struct type (provided by the context t) needs to be mutable --
               this is the same as when we see x.f[0] = 1 -- field f needs to be
               mutable (but not x!)
-          ii. if the pattern contains f = x *and* x is a borrow, then this is
+          ii. if the pattern contains f = x *and* x is a /mutable/ borrow, then this is
               going to be a move-out -- this is not the same behavior as a
               let-binding. Since borrows do not implement Copy, we need to do
               some extra work. Consider this example:
@@ -427,55 +540,56 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
               So we need to do two things: ii.a. mark the field as a ref mut
               pattern, and ii.b. mark the variable itself as mutable...
         *)
-        let rec update_fields known pat (t: typ): known * pat =
+        let rec update_fields (known: known) pat: known * pat =
           match pat with
-          | StructP (name, fieldpats) ->
-              (* If it's not in the map, it's an enum. *)
-              if DataTypeMap.mem name known.structs then
-                let fields = DataTypeMap.find name known.structs in
-                let known, fieldpats = List.fold_left2 (fun (known, fieldpats) (f, pat) { name; typ; _ } ->
-                  assert (f = name);
-                  match pat with
-                  | OpenP open_var ->
-                      let { atom; _ } = open_var in
-                      let mut = VarSet.mem atom known.r in
-                      let ref = match typ with
-                        | App (Name (["Box"], []), [_]) | Vec _ | Ref _ ->
-                            true (* prevent a move-out, again *)
-                        | _ ->
-                            mut (* something mutated relying on an implicit conversion to ref *)
-                      in
-                      (* KPrint.bprintf "In match:\n%a\nPattern variable %s: mut=%b, ref=%b\n" *)
-                      (*   pexpr e_match open_var.name mut ref; *)
-                      (* i., above *)
-                      let known = if mut then add_mut_field (Some t) f known else known in
-                      (* ii.b. *)
-                      let known = match e_scrut with
-                        | Open { atom; _ } when mut -> add_mut_var atom known
-                        | Deref (Open { atom; _ }) when mut -> add_mut_borrow atom known
-                        | _ ->
-                            (* KPrint.bprintf "%a is not open or deref\n" pexpr e; *)
-                            known
-                      in
-                      (* ii.a *)
-                      let known = if ref then { known with p = VarSet.add atom known.p } else known in
-                      known, (f, OpenP open_var) :: fieldpats
-                  | _ ->
-                      let known, pat = update_fields known pat typ in
-                      known, (f, pat) :: fieldpats
-                ) (known, []) fieldpats fields in
-                let fieldpats = List.rev fieldpats in
-                known, StructP (name, fieldpats)
-
-              else
-                (* Enum case; nothing to do *)
-                known, pat
+          | StructP (name as struct_name, fieldpats) ->
+              let fields = Hashtbl.find structs name in
+              let known, fieldpats = List.fold_left2 (fun (known, fieldpats) (f, pat) { name; typ; _ } ->
+                assert (f = name);
+                match pat with
+                | OpenP open_var ->
+                    let { atom; _ } = open_var in
+                    let mut = VarSet.mem atom known.r in
+                    let ref = match typ with
+                      | App (Name (["Box"], []), [_]) | Vec _ | Ref (_, Mut, _) ->
+                          true (* prevent a move-out, again *)
+                      | _ ->
+                          mut (* something mutated relying on an implicit conversion to ref *)
+                    in
+                    (* KPrint.bprintf "In match:\n%a\nPattern variable %s: mut=%b, ref=%b\n"
+                      pexpr _e_match open_var.name mut ref; *)
+                    (* i., above *)
+                    if mut then add_mut_field struct_name f;
+                    (* ii.b. *)
+                    let known = match e_scrut with
+                      | Open { atom; _ } when mut -> add_mut_var atom known
+                      | Deref (Open { atom; _ }) when mut -> add_mut_borrow atom known
+                      | _ ->
+                          (* KPrint.bprintf "%a is not open or deref\n" pexpr e; *)
+                          known
+                    in
+                    (* ii.a *)
+                    let known = if ref then { known with p = VarSet.add atom known.p } else known in
+                    known, (f, OpenP open_var) :: fieldpats
+                | _ ->
+                    let known, pat = update_fields known pat in
+                    known, (f, pat) :: fieldpats
+              ) (known, []) fieldpats fields in
+              let fieldpats = List.rev fieldpats in
+              known, StructP (name, fieldpats)
+
+          | TupleP ps ->
+              let known, ps = List.fold_left (fun (known, ps) p ->
+                let known, p = update_fields known p in
+                known, p :: ps
+              ) (known, []) ps in
+              known, TupleP (List.rev ps)
 
           | Wildcard | Literal _ -> known, pat
           | OpenP _ -> known, pat (* no such thing as mutable struct fields or variables in Low* *)
           |  _ -> Warn.failwith "TODO: Match %a" ppat pat
         in
-        let known, pat = update_fields known pat t in
+        let known, pat = update_fields known pat in
         let bs = List.map2 (fun a b ->
           let ref = VarSet.mem a known.p in
           let mut = VarSet.mem a known.r in
@@ -491,26 +605,73 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
          earlier. This should therefore only occur when accessing a variable
          in an array *)
       let expected = Ref (None, Shared, expected) in
-      let known, e1 = infer env expected known e1 in
-      let known, e2 = infer env usize known e2 in
+      let known, e1 = infer_expr env valuation expected known e1 in
+      let known, e2 = infer_expr env valuation usize known e2 in
       known, Index (e1, e2)
 
   (* Special case for array slices. This occurs, e.g., when calling a function with
      a struct field *)
-  | Field (Open { atom; _ }, "0", None) | Field (Open { atom; _}, "1", None) ->
+  | Field (Open { atom; _ }, "0", None) | Field (Open { atom; _ }, "1", None) ->
       if is_mut_borrow expected then
         add_mut_borrow atom known, e
-      else known, e
+      else
+        known, e
 
-  | Field _ ->
-      (* We should be able to ignore this case, on the basis that we are not going to get any
-         mutability constraints from a field expression. However, we need to modify all of the cases
-         above (such as assignment) to handle the case where the assignee is a field. *)
+  | Field (_, f, t) ->
+      if is_mut_borrow expected then
+        add_mut_field (`Struct (assert_name t)) f;
       known, e
 
   | Deref _ ->
       known, e
 
+  | Tuple es ->
+      let t_elt = match expected with Tuple t -> t | _ -> failwith "impossible" in
+      let known, es = List.fold_left2 (fun (known, es) e t ->
+        let known, e = infer_expr env valuation t known e in
+        known, e :: es
+      ) (known, []) es t_elt in
+      known, Tuple (List.rev es)
+
+
+let empty: known = { v = VarSet.empty; r = VarSet.empty; p = VarSet.empty }
+
+let infer_function (env: env) valuation (d: decl): decl =
+  match d with
+  | Function ({ name; body; return_type; parameters; _ } as f) ->
+      if Options.debug "rs-mut" then
+        KPrint.bprintf "[infer-mut] visiting %s\n" (String.concat "::" name);
+      let atoms, body =
+        List.fold_right (fun binder (atoms, e) ->
+          let a, e = open_ binder e in
+          (* KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) pexpr e; *)
+          a :: atoms, e
+        ) parameters ([], body)
+      in
+      (* KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
+        pexpr body; *)
+      (* Start the analysis with the current state of struct mutability *)
+      let known, body = infer_expr env valuation return_type empty body in
+      let parameters, body =
+        List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
+          let e = close atom (Var 0) (lift 1 e) in
+          (* KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) pexpr e; *)
+          let mut = want_mut_var atom known in
+          let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
+          { binder with mut; typ } :: parameters, e
+        ) ([], body) parameters atoms
+      in
+      let parameters = List.rev parameters in
+      (* We update the environment in two ways. First, we add the function declaration,
+         with the mutability of the parameters inferred during the analysis.
+         Second, we propagate the information about the mutability of struct fields
+         inferred while traversing this function to the global environment. Note, since
+         the traversal does not add or remove any bindings, but only increases the
+         mutability, we can do a direct replacement instead of a more complex merge *)
+      Function { f with body; parameters }
+  | _ ->
+      assert false
+
 (* We store here a list of builtins, with the types of their arguments.
    Type substitutions are currently not supported, functions with generic
    args should be added directly to Call in infer *)
@@ -832,93 +993,80 @@ let builtins : (name * typ list) list = [
   [ "vale"; "stdcalls_x64_fswap"; "cswap2_e" ], [
     u64; Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
   ];
-
-  (* TODO: These functions are recursive, and should be handled properly.
-     For now, we hardcode their expected type and mutability in HACL *)
-  [ "bignum"; "bignum"; "bn_karatsuba_mul_uint32"], [
-      u32; Ref (None, Shared, Slice u32); Ref (None, Shared, Slice u32);
-      Ref (None, Mut, Slice u32); Ref (None, Mut, Slice u32)
-  ];
-  [ "bignum"; "bignum"; "bn_karatsuba_mul_uint64"], [
-      u64; Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64);
-      Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
-  ];
-  [ "bignum"; "bignum"; "bn_karatsuba_sqr_uint32"], [
-      u32; Ref (None, Shared, Slice u32);
-      Ref (None, Mut, Slice u32); Ref (None, Mut, Slice u32)
-  ];
-  [ "bignum"; "bignum"; "bn_karatsuba_sqr_uint64"], [
-      u64; Ref (None, Shared, Slice u64);
-      Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
-  ];
-
-
 ]
 
 let infer_mut_borrows files =
-  (* Map.of_list is only available from OCaml 5.1 onwards *)
-  let env = { seen = List.to_seq builtins |> NameMap.of_seq; structs = DataTypeMap.empty } in
-  let known = { structs = DataTypeMap.empty; v = VarSet.empty; r = VarSet.empty; p = VarSet.empty } in
-  let env, files =
-    List.fold_left (fun (env, files) (filename, decls) ->
-      let env, decls = List.fold_left (fun (env, decls) decl ->
-        match decl with
-        | Function ({ name; body; return_type; parameters; _ } as f) ->
-            (* KPrint.bprintf "[infer-mut] visiting %s\n" (String.concat "::" name); *)
-            let atoms, body =
-              List.fold_right (fun binder (atoms, e) ->
-                let a, e = open_ binder e in
-                (* KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) pexpr e; *)
-                a :: atoms, e
-              ) parameters ([], body)
-            in
-            (* KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
-              pexpr body; *)
-            (* Start the analysis with the current state of struct mutability *)
-            let known, body = infer env return_type {known with structs = env.structs} body in
-            let parameters, body =
-              List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
-                let e = close atom (Var 0) (lift 1 e) in
-                (* KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) pexpr e; *)
-                let mut = want_mut_var atom known in
-                let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
-                { binder with mut; typ } :: parameters, e
-              ) ([], body) parameters atoms
-            in
-            let parameters = List.rev parameters in
-            (* We update the environment in two ways. First, we add the function declaration,
-               with the mutability of the parameters inferred during the analysis.
-               Second, we propagate the information about the mutability of struct fields
-               inferred while traversing this function to the global environment. Note, since
-               the traversal does not add or remove any bindings, but only increases the
-               mutability, we can do a direct replacement instead of a more complex merge *)
-            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen; structs = known.structs } in
-            env, Function { f with body; parameters } :: decls
-        | Struct ({name; fields; _}) ->
-            { env with structs = DataTypeMap.add (`Struct name) fields env.structs }, decl :: decls
-        | Enumeration { name; items; _ } ->
-            List.fold_left (fun (env: env) (cons, fields) ->
-              match fields with
-              | None -> env
-              | Some fields -> { env with structs = DataTypeMap.add (`Variant (name, cons)) fields env.structs }
-            ) env items, decl :: decls
-        | _ ->
-            env, decl :: decls
-      ) (env, []) decls in
-      let decls = List.rev decls in
-      env, (filename, decls) :: files
-    ) (env, []) files
+  (* Fill the `structs` global table with initial field information. Some of
+     these fields will be promoted to "mutable" as a side-effect of the
+     mutability inference. *)
+  List.iter (fun (_, decls) ->
+    List.iter (fun decl ->
+      match decl with
+      | Struct ({name; fields; _}) ->
+          Hashtbl.add structs (`Struct name) fields
+      | Enumeration { name; items; _ } ->
+          List.iter (fun (cons, fields) ->
+            Option.value fields ~default:[] |>
+            Hashtbl.add structs (`Variant (name, cons))
+          ) items
+      | _ ->
+          ()
+    ) decls
+  ) files;
+
+  (* When inside a function body, we only care about the type of the parameters. *)
+  let env = {
+    signatures = NameMap.of_seq (List.to_seq (builtins @
+      List.concat_map (fun (_, decls) ->
+        List.filter_map (function
+          | Function { parameters; name; _ } ->
+              Some (name, List.map (fun (p: MiniRust.binding) -> p.typ) parameters)
+          | _ ->
+              None
+        ) decls) files))
+  } in
+
+  (* But for the fixed point computation, we need complete definitions for each
+     name, in order to implement rhs. *)
+  let definitions = List.fold_left (fun map (_, decls) ->
+    List.fold_left (fun map decl -> NameMap.add (name_of_decl decl) decl map) map decls
+  ) NameMap.empty files in
+
+  let builtins = NameMap.of_seq (List.to_seq builtins) in
+
+  (* Given `name`, and given sets of mutable parameters for other definitions in
+    `valuation`, compute which of the parameters in this function need to be
+    mutable borrows. *)
+  let rhs name valuation =
+    if NameMap.mem name builtins then
+      (* No computation needed for builtins, the information is readily available *)
+      distill (NameMap.find name builtins)
+    else
+      match infer_function env valuation (NameMap.find name definitions) with
+      | Function { parameters; _ } -> distill (List.map (fun (b: MiniRust.binding) -> b.typ) parameters)
+      | _ -> failwith "impossible"
   in
 
-  (* We traverse all declarations again, and update the structure decls
-     with the new mutability info *)
+  let valuation = F.lfp rhs in
+
+  (* lfp does not actually perform any computation.
+    We now apply the valuation to all functions to compute mutability inference. *)
+  let files = List.map (fun (filename, decls) -> filename, List.map (function
+    | Function _ as decl ->
+        infer_function env valuation decl
+    | x -> x
+    ) decls
+  ) (List.rev files) in
+
+  (* We can finally update the struct and enumeration fields mutability
+     based on the information computed during inference on functions *)
   List.map (fun (filename, decls) -> filename, List.map (function
-    | Struct ({ name; _ } as s) -> Struct { s with fields = DataTypeMap.find (`Struct name) env.structs }
+    | Struct ({ name; _ } as s) -> Struct { s with fields = Hashtbl.find structs (`Struct name) }
     | Enumeration s  ->
         Enumeration { s with items = List.map (fun (cons, fields) ->
           cons, match fields with
             | None -> None
-            | Some _ -> Some (DataTypeMap.find (`Variant (s.name, cons)) env.structs)
+            | Some _ -> Some (Hashtbl.find structs (`Variant (s.name, cons)))
         ) s.items }
     | x -> x
     ) decls
@@ -1025,6 +1173,21 @@ let remove_deref_addrof = object
     | _ -> Deref e
 end
 
+let cleanup_splits = object(self)
+  inherit [_] map_expr as super
+  method! visit_Match _ e_scrut t branches =
+    match t with
+    | Tuple [ _; _ ] ->
+        let bs, p, e = KList.one branches in
+        let b1, b2 = KList.two bs in
+        assert (match p with TupleP _ -> true | _ -> false);
+        Let (b1, Field (e_scrut, "0", None),
+        Let (b2, Field (lift 1 e_scrut, "1", None),
+        self#visit_expr () e))
+    | _ ->
+        super#visit_Match () e_scrut t branches
+end
+
 let map_funs f_map files =
   let files =
     List.fold_left (fun files (filename, decls) ->
@@ -1041,6 +1204,81 @@ let map_funs f_map files =
   in
   List.rev files
 
+let compute_derives files =
+  (* A map from lid to Ast definition, of type decl *)
+  let definitions = List.fold_left (fun map (_, decls) ->
+    List.fold_left (fun map decl -> NameMap.add (name_of_decl decl) decl map) map decls
+  ) NameMap.empty files in
+
+  (* The bottom element of our lattice *)
+  let everything = TraitSet.of_list [ MiniRust.PartialEq; Clone; Copy ] in
+
+  let module F = Fix.Fix.ForOrderedType(struct
+    type t = name
+    let compare = compare
+  end)(struct
+    type property = TraitSet.t
+    let bottom = everything
+    let equal = (=)
+    let is_maximal _ = false
+  end) in
+
+  let equations lid valuation =
+    match NameMap.find_opt lid definitions with
+    | None -> everything
+    | Some decl ->
+        let traits_visitor = object(self)
+          inherit [_] reduce_typ as super
+          method zero = everything
+          method plus = TraitSet.inter
+          method! visit_tname _ lid _ =
+            valuation lid
+          method! visit_Ref _ _lifetime m t =
+            self#plus (self#visit_typ () t) (if m = Mut then TraitSet.singleton PartialEq else everything)
+          method! visit_Vec _ t =
+            self#plus (self#visit_typ () t) (TraitSet.of_list [ PartialEq; Clone ])
+          method! visit_App _ t ts =
+            match t with
+            | Name (["Box"], []) ->
+                self#plus (self#visit_typ () (KList.one ts)) (TraitSet.of_list [ PartialEq; Clone ])
+            | _ ->
+                super#visit_App () t ts
+        end in
+        let traits t = traits_visitor#visit_typ () t in
+        match decl with
+        | Function _ -> failwith "impossible"
+        | Constant _ -> failwith "impossible"
+        | Alias _  -> TraitSet.empty
+        | Struct { fields; _ } ->
+            let ts = List.map (fun (sf: struct_field) -> traits sf.typ) fields in
+            List.fold_left TraitSet.inter everything ts
+        | Enumeration { items; _ } ->
+            let ts = List.concat_map (fun (_cons, fields) ->
+              match fields with
+              | Some fields ->
+                  List.map (fun sf -> traits sf.typ) fields
+              | None ->
+                  []
+            ) items in
+            List.fold_left TraitSet.inter everything ts
+  in
+
+  F.lfp equations
+
+let add_derives valuation files =
+  let to_list ts = List.of_seq (TraitSet.to_seq ts) in
+  List.map (fun (f, decls) ->
+    f, List.map (function
+      | Struct s -> Struct { s with derives = to_list (valuation s.name) }
+      | Enumeration s -> Enumeration { s with derives = to_list (valuation s.name) }
+      | d -> d
+    ) decls
+  ) files
+
+let cleanup_minirust files =
+  let files = map_funs cleanup_splits#visit_expr files in
+  files
+
 let simplify_minirust files =
   let files = map_funs unroll_loops#visit_expr files in
   let files = map_funs remove_auto_deref#visit_expr files in
@@ -1050,4 +1288,5 @@ let simplify_minirust files =
   (* We do this simplification last, as the previous passes might
      have introduced unit statements *)
   let files = map_funs remove_trailing_unit#visit_expr files in
+  let files = add_derives (compute_derives files) files in
   files
diff --git a/lib/Options.ml b/lib/Options.ml
index 5ee6b67a..b796f1e5 100644
--- a/lib/Options.ml
+++ b/lib/Options.ml
@@ -45,6 +45,9 @@ type backend = C | Rust | Wasm
 let backend = ref C
 let wasm () = !backend = Wasm
 let rust () = !backend = Rust
+let no_box = ref false
+let contained: string list ref = ref []
+let keep_tuples = ref false
 
 let static_header: Bundle.pat list ref = ref []
 let minimal = ref false
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index 7a7e0a49..fb134864 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -452,17 +452,20 @@ and print_expr env (context: int) (e: expr): document =
 
   | Struct (cons, fields) ->
       group @@
-      print_name env cons ^/^ braces_with_nesting (
-        separate_map (comma ^^ break1) (fun (f, e) ->
-          group @@
-          if string f = print_expr env max_int e then
-            (* If the field name is the same as the expression assigned to it
-               (typically, a variable name), we do not need to duplicate it *)
-            string f
-          else
-            string f ^^ colon ^/^ group (print_expr env max_int e)
-        ) fields
-      )
+      print_data_type_name env cons ^^ (
+        match cons with
+        | `Variant _ when fields = [] -> empty
+        | _ -> break 1 ^^ braces_with_nesting (
+            separate_map (comma ^^ break1) (fun (f, e) ->
+              group @@
+              if string f = print_expr env max_int e then
+                (* If the field name is the same as the expression assigned to it
+                   (typically, a variable name), we do not need to duplicate it *)
+                string f
+              else
+                string f ^^ colon ^/^ group (print_expr env max_int e)
+            ) fields
+      ))
 
   | Var v ->
       begin match lookup env v with
@@ -494,9 +497,12 @@ and print_expr env (context: int) (e: expr): document =
 
   | Open { name; _ } -> at ^^ string name
 
+  | Tuple es ->
+      parens_with_nesting (separate_map comma (print_expr env max_int) es)
+
 and print_data_type_name env = function
   | `Struct name -> print_name env name
-  | `Variant (name, cons) -> print_name env (name @ [ cons ])
+  | `Variant (name, cons) -> print_name env name ^^ string "::" ^^ string cons
 
 and print_pat env (p: pat) =
   match p with
@@ -514,7 +520,11 @@ and print_pat env (p: pat) =
       else
         break1 ^^ braces_with_nesting (
         separate_map (comma ^^ break1) (fun (name, pat) ->
-          group (group (string name ^^ colon) ^/^ group (print_pat env pat))
+          match pat with
+          | VarP v when match lookup env v with Bound b -> b.name = name | _ -> false ->
+              print_pat env pat
+          | _ ->
+              group (group (string name ^^ colon) ^/^ group (print_pat env pat))
         ) fields ^^ trailing
       )
   | VarP v ->
@@ -526,6 +536,8 @@ and print_pat env (p: pat) =
       | _ -> failwith "incorrect bound var in pattern"
       end
   | OpenP { name; _ } -> at ^^ string name
+  | TupleP ps ->
+      parens_with_nesting (separate_map comma (print_pat env) ps)
 
 and print_array_expr env (e: array_expr) =
   match e with
@@ -559,12 +571,12 @@ let rec print_decl env (d: decl) =
   let env, target_name = register_global env (name_of_decl d) in
   let target_name = KList.last target_name in
   env, match d with
-  | Function { type_parameters; parameters; return_type; body; meta; inline; _ } ->
+  | Function { type_parameters; parameters; return_type; body; meta; inline; generic_params; _ } ->
       assert (type_parameters = 0);
       let parameters = List.map (fun (b: binding) -> { b with name = allocate_name env b.name }) parameters in
       let env = List.fold_left (fun env (b: binding) -> push env (Bound b)) env parameters in
       group @@
-      group (group (print_inline_and_meta inline meta ^^ string "fn" ^/^ string target_name) ^^
+      group (group (print_inline_and_meta inline meta ^^ string "fn" ^/^ string target_name ^^ print_generic_params generic_params) ^^
         parens_with_nesting (separate_map (comma ^^ break1) (print_binding env) parameters) ^^
         (match return_type with | Unit -> empty | _ -> space ^^ arrow ^^ (nest 4 (break1 ^^ print_typ env return_type)))) ^/^
       print_block_expression env body
@@ -572,19 +584,21 @@ let rec print_decl env (d: decl) =
       group @@
       group (print_meta meta ^^ string "const" ^/^ string target_name ^^ colon ^/^ print_typ env typ ^/^ equals) ^^
       nest 4 (break1 ^^ print_expr env max_int body) ^^ semi
-  | Enumeration { items; meta; derives; _ } ->
+  | Enumeration { items; meta; derives; generic_params; _ } ->
       group @@
       group (print_derives derives) ^/^
-      group (print_meta meta ^^ string "enum" ^/^ string target_name) ^/^
+      group (print_meta meta ^^ string "enum" ^/^ string target_name ^^ print_generic_params generic_params) ^/^
       braces_with_nesting (
         separate_map (comma ^^ hardline) (fun (item_name, item_struct) ->
           group @@
           string item_name ^^ match item_struct with
           | None -> empty
+          | Some [] -> empty
           | Some item_struct -> break1 ^^ braces_with_nesting (print_struct env item_struct)
       ) items)
-  | Struct { fields; meta; generic_params; _ } ->
+  | Struct { fields; meta; generic_params; derives; _ } ->
       group @@
+      group (print_derives derives) ^/^
       group (print_meta meta ^^ string "struct" ^/^ string target_name ^^ print_generic_params generic_params) ^/^
       braces_with_nesting (print_struct env fields)
   | Alias { generic_params; body; meta; _ } ->
@@ -635,6 +649,8 @@ let print_decls ns ds =
     ) env.globals;
   separate (hardline ^^ hardline) ds ^^ hardline
 
+let pname = printf_of_pprint (print_name debug)
+let pdataname = printf_of_pprint (print_data_type_name debug)
 let pexpr = printf_of_pprint (print_expr debug max_int)
 let ptyp = printf_of_pprint (print_typ debug)
 let ptyps = printf_of_pprint (separate_map (comma ^^ break1) (print_typ debug))
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
index 1d897f18..1bc1c372 100644
--- a/lib/Simplify.ml
+++ b/lib/Simplify.ml
@@ -223,6 +223,8 @@ let unused private_count_table lid ts (i: int) =
   unused_i i &&
   implies (i = 0) (List.exists not (List.init (List.length ts) unused_i))
 
+(* TODO: this is not a fixed point computation, meaning some opportunities for
+   unused parameter elimination are missed *)
 let remove_unused_parameters = object (self)
   inherit [_] map
 
@@ -1113,9 +1115,6 @@ and hoist_stmt loc e =
   | EContinue ->
       mk EContinue
 
-  | ETuple _ ->
-      failwith "[hoist_t]: ETuple not properly desugared"
-
   | ESequence _ ->
       failwith "[hoist_t]: sequences should've been translated as let _ ="
 
@@ -1361,11 +1360,16 @@ and hoist_expr loc pos e =
       ) fields) in
       List.flatten lhs, mk (EFlat fields)
 
-  | ECons _ ->
-      failwith "[hoist_t]: ECons, why?"
+  | ECons (cons, fields) ->
+      let lhs, fields = List.split (List.map (fun expr ->
+        let lhs, expr = hoist_expr loc Unspecified expr in
+        lhs, expr
+      ) fields) in
+      List.flatten lhs, mk (ECons (cons, fields))
 
-  | ETuple _ ->
-      failwith "[hoist_t]: ETuple not properly desugared"
+  | ETuple es ->
+      let lhs, es = List.split (List.map (hoist_expr loc Unspecified) es) in
+      List.flatten lhs, mk (ETuple es)
 
   | ESequence _ ->
       fatal_error "[hoist_t]: sequences should've been translated as let _ ="
diff --git a/src/Karamel.ml b/src/Karamel.ml
index 94869c7b..19db0da3 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -287,6 +287,10 @@ Supported options:|}
     "", Arg.Unit (fun _ -> ()), " ";
     "-by-ref", Arg.String (fun s -> prepend Options.by_ref (Parsers.lid s)), " \
       pass the given struct type by reference, always";
+    "-fno-box", Arg.Set Options.no_box, "  don't generate Box (Rust only)";
+    "-fcontained-type", Arg.String (fun s -> Options.contained := s :: !Options.contained), "  \
+      type passed by reference with a different lifetime";
+    "-fkeep-tuples", Arg.Set Options.keep_tuples, "  do not monomorphize tuples";
     "-fbuiltin-uint128", Arg.Set Options.builtin_uint128, "  target compiler \
       supports arithmetic operators for uint128 -- this is NON PORTABLE, \
       works only with GCC/Clang";
@@ -755,6 +759,7 @@ Supported options:|}
     if Options.debug "rs" then
       print PrintAst.print_files files;
     let files = AstToMiniRust.translate_files files in
+    let files = OptimizeMiniRust.cleanup_minirust files in
     let files = OptimizeMiniRust.infer_mut_borrows files in
     let files = OptimizeMiniRust.simplify_minirust files in
     OutputRust.write_all files