11 files changed, 546 insertions, 61 deletions

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 22378af7..613b6076 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,6 +1,6 @@
 import Base.Primitives.Base
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Primitives.Vec
 import Base.Primitives.Alloc
-import Base.Primitives.CoreOpsDeref
+import Base.Primitives.CoreOps
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 0580421f..34590499 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -1,6 +1,6 @@
 import Lean
 import Base.Primitives.Base
-import Base.Primitives.CoreOpsDeref
+import Base.Primitives.CoreOps
 
 open Primitives
 open Result
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 49c84bee..47807a0d 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -1,4 +1,4 @@
-/- Arrays/slices -/
+/- Arrays/Slices -/
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
@@ -7,6 +7,7 @@ import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Primitives.Range
+import Base.Primitives.CoreOps
 import Base.Arith
 import Base.Progress.Base
 
@@ -400,4 +401,160 @@ theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α)
     have := h2 i (by int_tac) (by int_tac)
     simp [*]
 
+/- Trait declaration: [core::slice::index::private_slice_index::Sealed] -/
+structure core.slice.index.private_slice_index.Sealed (Self : Type) where
+
+/- Trait declaration: [core::slice::index::SliceIndex] -/
+structure core.slice.index.SliceIndex (Self T0 : Type) where
+  sealedInst :core.slice.index.private_slice_index.Sealed Self
+  Output : Type
+  get : Self → T0 → Result (Option Output)
+  get_mut : Self → T0 → Result (Option Output)
+  get_mut_back : Self → T0 → Option Output → Result T0
+  get_unchecked : Self → ConstRawPtr T0 → Result (ConstRawPtr Output)
+  get_unchecked_mut : Self → MutRawPtr T0 → Result (MutRawPtr Output)
+  index : Self → T0 → Result Output
+  index_mut : Self → T0 → Result Output
+  index_mut_back : Self → T0 → Output → Result T0
+
+/- [core::slice::index::[T]::index]: forward function -/
+def core.slice.index.Slice.index
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0))
+  (slice : Slice T0) (i : I) : Result inst.Output := do
+  let x ← inst.get i slice
+  match x with
+  | none => fail panic
+  | some x => ret x
+
+/- [core::slice::index::Range:::get]: forward function -/
+def core.slice.index.Range.get (T0 : Type) (i : Range Usize) (slice : Slice T0) :
+  Result (Option (Slice T0)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: forward function -/
+def core.slice.index.Range.get_mut
+  (T0 : Type) : Range Usize → Slice T0 → Result (Option (Slice T0)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: backward function 0 -/
+def core.slice.index.Range.get_mut_back
+  (T0 : Type) :
+  Range Usize → Slice T0 → Option (Slice T0) → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_unchecked]: forward function -/
+def core.slice.index.Range.get_unchecked
+  (T0 : Type) :
+  Range Usize → ConstRawPtr (Slice T0) → Result (ConstRawPtr (Slice T0)) :=
+  -- Don't know what the model should be - for now we always fail to make
+  -- sure code which uses it fails
+  fun _ _ => fail panic
+
+/- [core::slice::index::Range::get_unchecked_mut]: forward function -/
+def core.slice.index.Range.get_unchecked_mut
+  (T0 : Type) :
+  Range Usize → MutRawPtr (Slice T0) → Result (MutRawPtr (Slice T0)) :=
+  -- Don't know what the model should be - for now we always fail to make
+  -- sure code which uses it fails
+  fun _ _ => fail panic
+
+/- [core::slice::index::Range::index]: forward function -/
+def core.slice.index.Range.index
+  (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: forward function -/
+def core.slice.index.Range.index_mut
+  (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: backward function 0 -/
+def core.slice.index.Range.index_mut_back
+  (T0 : Type) : Range Usize → Slice T0 → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: forward function -/
+def core.slice.index.Slice.index_mut
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  Slice T0 → I → Result inst.Output :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: backward function 0 -/
+def core.slice.index.Slice.index_mut_back
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  Slice T0 → I → inst.Output → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index]: forward function -/
+def core.array.Array.index
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T0) I) :
+  Array T0 N → I → Result inst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: forward function -/
+def core.array.Array.index_mut
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) :
+  Array T0 N → I → Result inst.indexInst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: backward function 0 -/
+def core.array.Array.index_mut_back
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) :
+  Array T0 N → I → inst.indexInst.Output → Result (Array T0 N) :=
+  sorry -- TODO
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexInst (T0 I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  core.ops.index.Index (Slice T0) I := {
+  Output := inst.Output
+  index := core.slice.index.Slice.index T0 I inst
+}
+
+/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
+def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
+
+/- Trait implementation: [core::slice::index::Range] -/
+def core.slice.index.Range.coresliceindexSliceIndexInst (T0 : Type) :
+  core.slice.index.SliceIndex (Range Usize) (Slice T0) := {
+  sealedInst :=
+    core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  Output := Slice T0
+  get := core.slice.index.Range.get T0
+  get_mut := core.slice.index.Range.get_mut T0
+  get_mut_back := core.slice.index.Range.get_mut_back T0
+  get_unchecked := core.slice.index.Range.get_unchecked T0
+  get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T0
+  index := core.slice.index.Range.index T0
+  index_mut := core.slice.index.Range.index_mut T0
+  index_mut_back := core.slice.index.Range.index_mut_back T0
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexMutInst (T0 I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  core.ops.index.IndexMut (Slice T0) I := {
+  indexInst := core.slice.index.Slice.coreopsindexIndexInst T0 I inst
+  index_mut := core.slice.index.Slice.index_mut T0 I inst
+  index_mut_back := core.slice.index.Slice.index_mut_back T0 I inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexInst (T0 I : Type) (N : Usize)
+  (inst : core.ops.index.Index (Slice T0) I) :
+  core.ops.index.Index (Array T0 N) I := {
+  Output := inst.Output
+  index := core.array.Array.index T0 I N inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize)
+  (inst : core.ops.index.IndexMut (Slice T0) I) :
+  core.ops.index.IndexMut (Array T0 N) I := {
+  indexInst := core.array.Array.coreopsindexIndexInst T0 I N inst.indexInst
+  index_mut := core.array.Array.index_mut T0 I N inst
+  index_mut_back := core.array.Array.index_mut_back T0 I N inst
+}
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 10af8f67..7fc33251 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -127,4 +127,11 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
  Use with `simp [ aeneas ]` -/
 register_simp_attr aeneas
 
+-- We don't really use raw pointers for now
+structure MutRawPtr (T : Type) where
+  v : T
+
+structure ConstRawPtr (T : Type) where
+  v : T
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean
new file mode 100644
index 00000000..da458f66
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreOps.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+
+open Primitives
+open Result
+
+namespace core.ops
+
+namespace index -- core.ops.index
+
+/- Trait declaration: [core::ops::index::Index] -/
+structure Index (Self Idx : Type) where
+  Output : Type
+  index : Self → Idx → Result Output
+
+/- Trait declaration: [core::ops::index::IndexMut] -/
+structure IndexMut (Self Idx : Type) where
+  indexInst : Index Self Idx
+  index_mut : Self → Idx → Result indexInst.Output
+  index_mut_back : Self → Idx → indexInst.Output → Result Self
+
+end index -- core.ops.index
+
+namespace deref -- core.ops.deref
+
+structure Deref (Self : Type) where
+  Target : Type
+  deref : Self → Result Target
+
+structure DerefMut (Self : Type) where
+  derefInst : Deref Self
+  deref_mut : Self → Result derefInst.Target
+  deref_mut_back : Self → derefInst.Target → Result Self
+
+end deref -- core.ops.deref
+
+end core.ops
diff --git a/backends/lean/Base/Primitives/CoreOpsDeref.lean b/backends/lean/Base/Primitives/CoreOpsDeref.lean
deleted file mode 100644
index 2b540012..00000000
--- a/backends/lean/Base/Primitives/CoreOpsDeref.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Lean
-import Base.Primitives.Base
-
-open Primitives
-open Result
-
-namespace core.ops.deref
-
-structure Deref (Self : Type) where
-  Target : Type
-  deref : Self → Result Target
-
-structure DerefMut (Self : Type) where
-  derefInst : Deref Self
-  deref_mut : Self → Result derefInst.Target
-  deref_mut_back : Self → derefInst.Target → Result Self
-
-end core.ops.deref
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index c4c4d9f2..99fcedc6 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Arith
 import Base.Progress.Base
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index afd722e5..6b6a2686 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -234,26 +234,20 @@ let assumed_adts () : (assumed_ty * string) list =
         (Array, "Array");
         (Slice, "Slice");
         (Str, "Str");
+        (RawPtr Mut, "MutRawPtr");
+        (RawPtr Const, "ConstRawPtr");
       ]
-  | Coq | FStar ->
+  | Coq | FStar | HOL4 ->
       [
         (State, "state");
         (Result, "result");
         (Error, "error");
-        (Fuel, "nat");
-        (Array, "array");
-        (Slice, "slice");
-        (Str, "str");
-      ]
-  | HOL4 ->
-      [
-        (State, "state");
-        (Result, "result");
-        (Error, "error");
-        (Fuel, "num");
+        (Fuel, if !backend = HOL4 then "num" else "nat");
         (Array, "array");
         (Slice, "slice");
         (Str, "str");
+        (RawPtr Mut, "mut_raw_ptr");
+        (RawPtr Const, "const_raw_ptr");
       ]
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
@@ -1378,7 +1372,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
   let def_name =
     match info with
     | None -> ctx.fmt.type_name def.name
-    | Some info -> String.concat "." info.rust_name
+    | Some info -> info.extract_name
   in
   let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
   (* Compute and register:
@@ -4281,16 +4275,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
             string * (RegionGroupId.id option * string) list =
           let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string
               =
-            (* We do something special: we use the base name but remove everything
-               but the crate (because [get_name] removes it) and the last ident.
-               This allows us to reuse the [ctx_compute_fun_decl] function.
-            *)
-            let basename : name =
-              match (f.basename : name) with
-              | Ident crate :: name ->
-                  Ident crate :: [ Collections.List.last name ]
-              | _ -> raise (Failure "Unexpected")
-            in
+            (* We do something special to reuse the [ctx_compute_fun_decl]
+               function. TODO: make it cleaner. *)
+            let basename : name = [ Ident item_name ] in
             let f = { f with basename } in
             let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in
             let name = ctx_compute_fun_name trans f ctx in
@@ -4503,6 +4490,17 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params
     cg_params trait_clauses;
 
+  (* Add the parent clauses as local clauses, so that we can refer to them *)
+  let ctx =
+    List.fold_left
+      (fun ctx clause ->
+        let item_name =
+          ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
+        in
+        ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx)
+      ctx decl.generics.trait_clauses
+  in
+
   F.pp_print_space fmt ();
   (match !backend with
   | Lean -> F.pp_print_string fmt "where"
@@ -4522,6 +4520,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
         ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
       in
       let ty () =
+        F.pp_print_space fmt ();
         extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
       in
       extract_trait_decl_item ctx fmt item_name ty)
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 4c6fe014..c781463e 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -121,7 +121,7 @@ let builtin_types () : builtin_type_info list =
       rust_name = [ "alloc"; "alloc"; "Global" ];
       extract_name =
         (match !backend with
-        | Lean -> "AllocGlobal"
+        | Lean -> "alloc.alloc.Global"
         | Coq | FStar | HOL4 -> "alloc_global");
       keep_params = None;
       body_info = None;
@@ -335,7 +335,7 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref"
             | Lean -> "alloc.boxed.Box.deref");
         };
         (* The backward function shouldn't be used *)
@@ -343,7 +343,7 @@ let builtin_funs () :
           rg = rg0;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_back"
             | Lean -> "alloc.boxed.Box.deref_back");
         };
       ] );
@@ -354,7 +354,7 @@ let builtin_funs () :
           rg = None;
           extract_name =
             (match !backend with
-            | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut"
+            | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_mut"
             | Lean -> "alloc.boxed.Box.deref_mut");
         };
         {
@@ -365,6 +365,179 @@ let builtin_funs () :
             | Lean -> "alloc.boxed.Box.deref_mut_back");
         };
       ] );
+    (* TODO: fix the same like "[T]" below *)
+    ( [ "core"; "slice"; "index"; "[T]"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index"
+            | Lean -> "core.slice.index.Slice.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_back"
+            | Lean -> "core.slice.index.Slice.index_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "[T]"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut"
+            | Lean -> "core.slice.index.Slice.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut_back"
+            | Lean -> "core.slice.index.Slice.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "array"; "[T; N]"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index"
+            | Lean -> "core.array.Array.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_back"
+            | Lean -> "core.array.Array.index_back");
+        };
+      ] );
+    ( [ "core"; "array"; "[T; N]"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_mut"
+            | Lean -> "core.array.Array.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_array_Array_index_mut_back"
+            | Lean -> "core.array.Array.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get"
+            | Lean -> "core.slice.index.Range.get");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_back"
+            | Lean -> "core.slice.index.Range.get_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut"
+            | Lean -> "core.slice.index.Range.get_mut");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut_back"
+            | Lean -> "core.slice.index.Range.get_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "index" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index"
+            | Lean -> "core.slice.index.Range.index");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_back"
+            | Lean -> "core.slice.index.Range.index_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "index_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut"
+            | Lean -> "core.slice.index.Range.index_mut");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut_back"
+            | Lean -> "core.slice.index.Range.index_mut_back");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked"
+            | Lean -> "core.slice.index.Range.get_unchecked");
+        };
+      ] );
+    ( [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ],
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked_mut"
+            | Lean -> "core.slice.index.Range.get_unchecked_mut");
+        };
+      ] );
   ]
 
 let mk_builtin_funs_map () =
@@ -528,7 +701,7 @@ let builtin_trait_decls_info () =
         [
           (match !backend with
           | Coq | FStar | HOL4 -> "index_inst"
-          | Lean -> "IndexInst");
+          | Lean -> "indexInst");
         ];
       consts = [];
       types = [];
@@ -547,6 +720,104 @@ let builtin_trait_decls_info () =
             ] );
         ];
     };
+    {
+      (* Sealed *)
+      rust_name = "core::slice::index::private_slice_index::Sealed";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_slice_index_sealed"
+        | Lean -> "core.slice.index.private_slice_index.Sealed");
+      parent_clauses = [];
+      consts = [];
+      types = [];
+      funs = [];
+    };
+    {
+      (* SliceIndex *)
+      rust_name = "core::slice::index::SliceIndex";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_SliceIndex"
+        | Lean -> "core.slice.index.SliceIndex");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "sealed_inst"
+          | Lean -> "sealedInst");
+        ];
+      consts = [];
+      types =
+        [
+          ( "Output",
+            ( (match !backend with
+              | Coq | FStar | HOL4 -> "core_SliceIndex_Output"
+              | Lean -> "Output"),
+              [] ) );
+        ];
+      funs =
+        [
+          ( "get",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get"
+                | Lean -> "get" );
+              (* The backward function shouldn't be used *)
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_back"
+                | Lean -> "get_back" );
+            ] );
+          ( "get_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut"
+                | Lean -> "get_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut_back"
+                | Lean -> "get_mut_back" );
+            ] );
+          ( "get_unchecked",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked"
+                | Lean -> "get_unchecked" );
+            ] );
+          ( "get_unchecked_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked_mut"
+                | Lean -> "get_unchecked_mut" );
+            ] );
+          ( "index",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index"
+                | Lean -> "index" );
+              (* The backward function shouldn't be used *)
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_back"
+                | Lean -> "index_back" );
+            ] );
+          ( "index_mut",
+            [
+              ( None,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut"
+                | Lean -> "index_mut" );
+              ( rg0,
+                match !backend with
+                | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut_back"
+                | Lean -> "index_mut_back" );
+            ] );
+        ];
+    };
   ]
 
 let mk_builtin_trait_decls_map () =
@@ -577,6 +848,7 @@ end
 module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
 
 let builtin_trait_impls_info () : ((string list * string list) * string) list =
+  (* TODO: fix the names like "[T]" below *)
   [
     (* core::ops::Deref<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
@@ -584,6 +856,28 @@ let builtin_trait_impls_info () : ((string list * string list) * string) list =
     (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
     ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
       "alloc.boxed.Box.coreOpsDerefMutInst" );
+    (* core::ops::index::Index<[T], I> *)
+    ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]),
+      "core.slice.index.Slice.coreopsindexIndexInst" );
+    (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
+    ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ],
+        [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ),
+      "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst"
+    );
+    (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
+    ( ( [ "core"; "slice"; "index"; "Range" ],
+        [ "core"; "slice"; "index"; "SliceIndex" ] ),
+      "core.slice.index.Range.coresliceindexSliceIndexInst" );
+    (* core::ops::index::IndexMut<[T], I> *)
+    ( ( [ "core"; "slice"; "index"; "[T]" ],
+        [ "core"; "ops"; "index"; "IndexMut" ] ),
+      "core.slice.index.Slice.coreopsindexIndexMutInst" );
+    (* core::ops::index::Index<[T; N], I> *)
+    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]),
+      "core.array.Array.coreopsindexIndexInst" );
+    (* core::ops::index::IndexMut<[T; N], I> *)
+    ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]),
+      "core.array.Array.coreopsindexIndexMutInst" );
   ]
 
 let mk_builtin_trait_impls_map () =
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 2553127a..0ab4ed94 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -13,14 +13,14 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
   | Regular id -> (FunDeclId.Map.find id fun_decls).name
   | Assumed aid -> Assumed.get_assumed_fun_name aid
 
-(** Return the opaque declarations found in the crate.
+(** Return the opaque declarations found in the crate, which are also *not builtin*.
 
     [filter_assumed]: if [true], do not consider as opaque the external definitions
     that we will map to definitions from the standard library.
 
     Remark: the list of functions also contains the list of opaque global bodies.
  *)
-let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
+let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     T.type_decl list * fun_decl list =
   let open ExtractBuiltin in
   let is_opaque_fun (d : fun_decl) : bool =
@@ -30,14 +30,21 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
     && ((not filter_assumed)
-       || not (SimpleNameMap.mem sname builtin_globals_map))
+       || (not (SimpleNameMap.mem sname builtin_globals_map))
+          && not (SimpleNameMap.mem sname (builtin_funs_map ())))
+  in
+  let is_opaque_type (d : T.type_decl) : bool =
+    let sname = name_to_simple_name d.name in
+    d.kind = T.Opaque
+    && ((not filter_assumed)
+       || not (SimpleNameMap.mem sname (builtin_types_map ())))
   in
-  let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
   (* Note that by checking the function bodies we also the globals *)
   ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types),
     List.filter is_opaque_fun (FunDeclId.Map.values k.functions) )
 
 (** Return true if the crate contains opaque declarations, ignoring the assumed
     definitions. *)
-let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool =
-  crate_get_opaque_decls k filter_assumed <> ([], [])
+let crate_has_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
+    bool =
+  crate_get_opaque_non_builtin_decls k filter_assumed <> ([], [])
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 35dff9e6..019a5c35 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -390,10 +390,10 @@ type gen_config = {
     [filter_assumed]: if [true], do not consider as opaque the external definitions
     that we will map to definitions from the standard library.
  *)
-let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool
-    =
+let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) :
+    bool * bool =
   let types, funs =
-    LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed
+    LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed
   in
   log#ldebug
     (lazy
@@ -1257,7 +1257,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Check if there are opaque types and functions - in which case we need
       * to split *)
-     let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in
+     let has_opaque_types, has_opaque_funs =
+       crate_has_opaque_non_builtin_decls ctx true
+     in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
      (* Extract the types *)