Add SliceLen as a primitive function and make minor adjustments

6 files changed, 100 insertions, 77 deletions

diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
index d19e9144..2d4a567b 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/Array.lean
@@ -14,7 +14,7 @@ namespace Primitives
 
 open Result Error
 
-abbrev Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
+def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
 
 instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
   prop_ty := λ v => v.val.len = n.val
@@ -33,19 +33,10 @@ abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
 example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Array.mk (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
+def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
   Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩
 
-example : Array Int (Usize.ofInt 2) := Array.mk Int (Usize.ofInt 2) [0, 1]
-
--- Remark: not used yet, but could be used if explicit calls to Len are used in Rust
--- TODO: very annoying that the α and the n are explicit parameters
-def Array.len (α : Type u) (n : Usize) (v : Array α n) : Usize :=
-  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
-
-@[simp]
-theorem Array.len_val {α : Type u} {n : Usize} (v : Array α n) : (Array.len α n v).val = v.length :=
-  by rfl
+example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1]
 
 @[simp]
 abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
@@ -81,7 +72,7 @@ def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize)
   else
     .fail arrayOutOfBounds
 
-def Array.index_mut (α : Type u) (v: Array α n) (i: Usize) : Result α :=
+def Array.index_mut (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
@@ -89,13 +80,13 @@ def Array.index_mut (α : Type u) (v: Array α n) (i: Usize) : Result α :=
 @[pspec]
 theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_mut α n i = ret x ∧ x = v.val.index i.val := by
   simp only [index_mut]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
-def Array.index_mut_back (α : Type u) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
+def Array.index_mut_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
@@ -104,7 +95,7 @@ def Array.index_mut_back (α : Type u) (v: Array α n) (i: Usize) (x: α) : Resu
 @[pspec]
 theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  ∃ nv, v.index_mut_back α n i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [index_mut_back]
@@ -209,6 +200,11 @@ theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α
   . simp_all
 
 /- Array to slice/subslices -/
+
+/- We could make this function not use the `Result` type. By making it monadic, we
+   push the user to use the `Array.to_slice_spec` spec theorem below (through the
+   `progress` tactic), meaning `Array.to_slice` should be considered as opaque.
+   All what the spec theorem reveals is that the "representative" lists are the same. -/
 def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
   ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
 
@@ -233,7 +229,7 @@ theorem Array.to_mut_slice_back_spec {α : Type u} {n : Usize} (a : Array α n)
   ∃ na, to_mut_slice_back α n a ns = ret na ∧ na.val = ns.val
   := by simp [to_mut_slice_back, *]
 
-def Array.shared_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
     ret ⟨ a.val.slice r.start.val r.end_.val,
@@ -245,29 +241,29 @@ def Array.shared_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
     fail panic
 
 @[pspec]
-theorem Array.shared_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+theorem Array.subslice_shared_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
-  ∃ s, shared_subslice α n a r = ret s ∧
+  ∃ s, subslice_shared α n a r = ret s ∧
   s.val = a.val.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
   := by
-  simp [shared_subslice, *]
+  simp [subslice_shared, *]
   intro i _ _
   have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
   simp [*]
 
-def Array.mut_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
-  Array.shared_subslice α n a r
+def Array.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+  Array.subslice_shared α n a r
 
 @[pspec]
-theorem Array.mut_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+theorem Array.subslice_mut_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
-  ∃ s, mut_subslice α n a r = ret s ∧
+  ∃ s, subslice_mut α n a r = ret s ∧
   s.val = a.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
-  := shared_subslice_spec a r h0 h1
+  := subslice_shared_spec a r h0 h1
 
-def Array.mut_subslice_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
+def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
   -- TODO: not completely sure here
   if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then
     let s_beg := a.val.itake r.start.val
@@ -292,13 +288,13 @@ def Array.mut_subslice_back (α : Type u) (n : Usize) (a : Array α n) (r : Rang
 -- We should introduce special symbols for the monadic arithmetic operations
 -- (the use will never write those symbols directly).
 @[pspec]
-theorem Array.mut_subslice_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
+theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
-  ∃ na, mut_subslice_back α n a r s = ret na ∧
+  ∃ na, subslice_mut_back α n a r s = ret na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by
-  simp [mut_subslice_back, *]
+  simp [subslice_mut_back, *]
   have h := List.replace_slice_index r.start.val r.end_.val a.val s.val
     (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
   simp [List.replace_slice] at h
@@ -315,7 +311,7 @@ theorem Array.mut_subslice_back_spec {α : Type u} {n : Usize} [Inhabited α] (a
     have := h2 i (by int_tac) (by int_tac)
     simp [*]
 
-def Slice.shared_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
     ret ⟨ s.val.slice r.start.val r.end_.val,
@@ -327,32 +323,32 @@ def Slice.shared_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Resul
     fail panic
 
 @[pspec]
-theorem Slice.shared_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+theorem Slice.subslice_shared_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
-  ∃ ns, shared_subslice α s r = ret ns ∧
+  ∃ ns, subslice_shared α s r = ret ns ∧
   ns.val = s.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
   := by
-  simp [shared_subslice, *]
+  simp [subslice_shared, *]
   intro i _ _
   have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
   simp [*]
 
-def Slice.mut_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
-  Slice.shared_subslice α s r
+def Slice.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+  Slice.subslice_shared α s r
 
 @[pspec]
-theorem Slice.mut_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+theorem Slice.subslice_mut_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
-  ∃ ns, mut_subslice α s r = ret ns ∧
+  ∃ ns, subslice_mut α s r = ret ns ∧
   ns.val = s.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
-  := shared_subslice_spec s r h0 h1
+  := subslice_shared_spec s r h0 h1
 
 attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
 set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
 
-def Slice.mut_subslice_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
+def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
   -- TODO: not completely sure here
   if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then
     let s_beg := s.val.itake r.start.val
@@ -372,13 +368,13 @@ def Slice.mut_subslice_back (α : Type u) (s : Slice α) (r : Range Usize) (ss :
     fail panic
 
 @[pspec]
-theorem Slice.mut_subslice_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
+theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
-  ∃ na, mut_subslice_back α a r ss = ret na ∧
+  ∃ na, subslice_mut_back α a r ss = ret na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by
-  simp [mut_subslice_back, *]
+  simp [subslice_mut_back, *]
   have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val
     (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
   simp [List.replace_slice, *] at h
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index e0a2efea..572b0a24 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -347,20 +347,42 @@ module Sig = struct
 
   let slice_subslice_sig (is_mut : bool) =
     mk_array_slice_subslice_sig false is_mut
+
+  (** Helper:
+      [fn<T>(&'a [T]) -> usize]
+   *)
+  let slice_len_sig : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ]
+    in
+    let output = mk_usize_ty (* usize *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      const_generic_params = empty_const_generic_params;
+      inputs;
+      output;
+    }
 end
 
 type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
 
 (** The list of assumed functions and all their information:
     - their signature
-    - a boolean indicating whether the function can fail or not
+    - a boolean indicating whether the function can fail or not (if true: can fail)
     - their name
 
     Rk.: following what is written above, we don't include [Box::free].
-    
+
     Remark about the vector functions: for [Vec::len] to be correct and return
     a [usize], we have to make sure that vectors are bounded by the max usize.
-    Followingly, [Vec::push] is monadic.
+    As a consequence, [Vec::push] is monadic.
  *)
 let assumed_infos : assumed_info list =
   let deref_pre = [ "core"; "ops"; "deref" ] in
@@ -402,11 +424,11 @@ let assumed_infos : assumed_info list =
     (* Array to slice*)
     ( ArrayToSharedSlice,
       Sig.array_to_slice_sig false,
-      false,
+      true,
       to_name [ "@ArrayToSharedSlice" ] );
     ( ArrayToMutSlice,
       Sig.array_to_slice_sig true,
-      false,
+      true,
       to_name [ "@ArrayToMutSlice" ] );
     (* Array Subslice *)
     ( ArraySharedSubslice,
@@ -432,6 +454,7 @@ let assumed_infos : assumed_info list =
       Sig.slice_subslice_sig true,
       true,
       to_name [ "@SliceMutSubslice" ] );
+    (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
   ]
 
 let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1de7d68b..84d11895 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -261,7 +261,7 @@ let assumed_adts () : (assumed_ty * string) list =
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
-  | Lean -> [ (Range, "Range.mk"); (Array, "Array.mk") ]
+  | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ]
   | Coq -> [ (Range, "range.mk"); (Array, "array.mk") ]
   | FStar -> [ (Range, "mkrange"); (Array, "mkarray") ]
   | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
@@ -329,21 +329,22 @@ let assumed_llbc_functions () :
         (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
         (VecIndexMut, None, "vec_index_mut_fwd");
         (VecIndexMut, rg0, "vec_index_mut_back");
-        (ArraySharedIndex, None, "array_index");
-        (ArrayMutIndex, None, "array_mut_index_fwd");
-        (ArrayMutIndex, rg0, "array_mut_index_back");
+        (ArraySharedIndex, None, "array_index_shared");
+        (ArrayMutIndex, None, "array_index_mut_fwd");
+        (ArrayMutIndex, rg0, "array_index_mut_back");
         (ArrayToSharedSlice, None, "array_to_slice");
         (ArrayToMutSlice, None, "array_to_mut_slice_fwd");
         (ArrayToMutSlice, rg0, "array_to_mut_slice_back");
-        (ArraySharedSubslice, None, "array_subslice");
-        (ArrayMutSubslice, None, "array_mut_subslice_fwd");
-        (ArrayMutSubslice, rg0, "array_mut_subslice_back");
-        (SliceSharedIndex, None, "slice_index");
-        (SliceMutIndex, None, "slice_mut_index_fwd");
-        (SliceMutIndex, rg0, "slice_mut_index_back");
-        (SliceSharedSubslice, None, "slice_subslice");
-        (SliceMutSubslice, None, "slice_mut_subslice_fwd");
-        (SliceMutSubslice, rg0, "slice_mut_subslice_back");
+        (ArraySharedSubslice, None, "array_subslice_shared");
+        (ArrayMutSubslice, None, "array_subslice_mut_fwd");
+        (ArrayMutSubslice, rg0, "array_subslice_mut_back");
+        (SliceSharedIndex, None, "slice_index_shared");
+        (SliceMutIndex, None, "slice_index_mut_fwd");
+        (SliceMutIndex, rg0, "slice_index_mut_back");
+        (SliceSharedSubslice, None, "slice_subslice_mut");
+        (SliceMutSubslice, None, "slice_subslice_mut_fwd");
+        (SliceMutSubslice, rg0, "slice_subslice_mut_back");
+        (SliceLen, None, "slice_len_fwd");
       ]
   | Lean ->
       [
@@ -355,27 +356,28 @@ let assumed_llbc_functions () :
         (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
         (VecInsert, rg0, "Vec.insert");
         (VecLen, None, "Vec.len");
-        (VecIndex, None, "Vec.index");
-        (VecIndex, rg0, "Vec.index_back") (* shouldn't be used *);
+        (VecIndex, None, "Vec.index_shared");
+        (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *);
         (VecIndexMut, None, "Vec.index_mut");
         (VecIndexMut, rg0, "Vec.index_mut_back");
-        (* TODO: it would be good to only use Array.index (no Array.mut_index)
+        (* TODO: it would be good to only use Array.index (no Array.index_mut)
            (same for subslice, etc.) *)
-        (ArraySharedIndex, None, "Array.index");
-        (ArrayMutIndex, None, "Array.mut_index");
-        (ArrayMutIndex, rg0, "Array.mut_index_back");
+        (ArraySharedIndex, None, "Array.index_shared");
+        (ArrayMutIndex, None, "Array.index_mut");
+        (ArrayMutIndex, rg0, "Array.index_mut_back");
         (ArrayToSharedSlice, None, "Array.to_slice");
         (ArrayToMutSlice, None, "Array.to_mut_slice");
         (ArrayToMutSlice, rg0, "Array.to_mut_slice_back");
-        (ArraySharedSubslice, None, "Array.subslice");
-        (ArrayMutSubslice, None, "Array.mut_subslice");
-        (ArrayMutSubslice, rg0, "Array.mut_subslice_back");
-        (SliceSharedIndex, None, "Slice.index");
-        (SliceMutIndex, None, "Slice.mut_index");
-        (SliceMutIndex, rg0, "Slice.mut_index_back");
-        (SliceSharedSubslice, None, "Slice.subslice");
-        (SliceMutSubslice, None, "Slice.mut_subslice");
-        (SliceMutSubslice, rg0, "Slice.mut_subslice_back");
+        (ArraySharedSubslice, None, "Array.subslice_shared");
+        (ArrayMutSubslice, None, "Array.subslice_mut");
+        (ArrayMutSubslice, rg0, "Array.subslice_mut_back");
+        (SliceSharedIndex, None, "Slice.index_shared");
+        (SliceMutIndex, None, "Slice.index_mut");
+        (SliceMutIndex, rg0, "Slice.index_mut_back");
+        (SliceSharedSubslice, None, "Slice.subslice_shared");
+        (SliceMutSubslice, None, "Slice.subslice_mut");
+        (SliceMutSubslice, rg0, "Slice.subslice_mut_back");
+        (SliceLen, None, "Slice.len");
       ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 207acef6..157cca38 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -647,7 +647,7 @@ let eval_non_local_function_call_concrete (config : C.config)
           | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice
           | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice
           | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice
-          | SliceMutSubslice ->
+          | SliceMutSubslice | SliceLen ->
               raise (Failure "Unimplemented")
         in
 
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 43b11aa5..ad7ab05f 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -512,6 +512,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
   | ArrayToMutSlice -> "@ArrayToMutSlice"
   | ArraySharedSubslice -> "@ArraySharedSubslice"
   | ArrayMutSubslice -> "@ArrayMutSubslice"
+  | SliceLen -> "@SliceLen"
   | SliceSharedIndex -> "@SliceSharedIndex"
   | SliceMutIndex -> "@SliceMutIndex"
   | SliceSharedSubslice -> "@SliceSharedSubslice"
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 58a5f9e2..52eeee26 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1567,7 +1567,8 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | VecIndex | VecIndexMut | ArraySharedSubslice
                     | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex
                     | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex
-                    | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice ),
+                    | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice
+                    | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)
             | _ -> super#visit_texpression env e)