diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 830d6662..e349f7b5 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -467,7 +467,9 @@ let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): Min
       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 (None, 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"
   | TAnonymous _ -> failwith "unexpected: we don't compile data types going to Rust"
@@ -735,6 +737,51 @@ 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"); _ }, [], [], [t]); _ }, [e1; e2]) ->
+      let env, e1 = translate_expr env e1 in
+      let env, e2 = translate_expr env e2 in
+      let t = translate_type env t in
+      let b: MiniRust.binding = {
+        name = "actual_pair";
+        typ = Tuple [ Ref (None, Shared, Slice t); Ref (None, Shared, Slice t) ];
+        mut = false;
+        ref = false
+      } in
+      let ret_lid = Helpers.assert_tlid e.typ in
+      (* FIXME super unpleasant mismatch because there's a custom pair type in Pulse *)
+      env, Let (b,
+        MethodCall (e1, ["split_at"], [ e2 ]),
+        Struct (`Struct (lookup_type env ret_lid), [ "fst", Field (Var 0, "0", None); "snd", Field (Var 0, "1", None) ]))
+
+  | 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 *)
@@ -1576,6 +1623,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..8008d844 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -407,6 +407,10 @@ let make_abstract (name, decls) =
   name, List.filter_map (function
     | DType (_, _, _, _, Abbrev _) as t ->
         Some t
+    | DType ((_, "slice_pair"), _, _, _, _) as t when Options.rust () ->
+        (* FIXME remove this hack once Tahina exhibits a repro as to why he
+           can't use actual pairs *)
+        Some t
     | DType _ ->
         None
     | DGlobal (_, name, _, _, _) when KString.starts_with (snd name) "op_" ->
@@ -434,7 +438,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/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 50a00992..c1bec6e3 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -96,6 +96,7 @@ let distill 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)
 
@@ -397,7 +398,7 @@ let rec infer_expr (env: env) valuation (expected: typ) (known: known) (e: 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);
@@ -408,17 +409,22 @@ let rec infer_expr (env: env) valuation (expected: typ) (known: known) (e: expr)
             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 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 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, Mut, 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)