Merge branch 'main' into afromher_shifts

19 files changed, 1893 insertions, 585 deletions

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 71a2d9c3..83f860b6 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -63,13 +63,15 @@ Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
-
 Definition string := Coq.Strings.String.string.
 Definition char := Coq.Strings.Ascii.ascii.
 Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte.
 
-Definition mem_replace_fwd (a : Type) (x : a) (y : a) : a := x .
-Definition mem_replace_back (a : Type) (x : a) (y : a) : a := y .
+Definition core_mem_replace (a : Type) (x : a) (y : a) : a := x .
+Definition core_mem_replace_back (a : Type) (x : a) (y : a) : a := y .
+
+Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
+Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
 
 (*** Scalars *)
 
@@ -394,12 +396,89 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
-(*** Range *)
-Record range (T : Type) := mk_range {
-  start: T;
-  end_: T;
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
+(*** core::ops *)
+
+(* Trait declaration: [core::ops::index::Index] *)
+Record core_ops_index_Index (Self Idx : Type) := mk_core_ops_index_Index {
+  core_ops_index_Index_Output : Type;
+  core_ops_index_Index_index : Self -> Idx -> result core_ops_index_Index_Output;
+}.
+Arguments mk_core_ops_index_Index {_ _}.
+Arguments core_ops_index_Index_Output {_ _}.
+Arguments core_ops_index_Index_index {_ _}.
+
+(* Trait declaration: [core::ops::index::IndexMut] *)
+Record core_ops_index_IndexMut (Self Idx : Type) := mk_core_ops_index_IndexMut {
+  core_ops_index_IndexMut_indexInst : core_ops_index_Index Self Idx;
+  core_ops_index_IndexMut_index_mut : Self -> Idx -> result core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output);
+  core_ops_index_IndexMut_index_mut_back : Self -> Idx -> core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self;
+}.
+Arguments mk_core_ops_index_IndexMut {_ _}.
+Arguments core_ops_index_IndexMut_indexInst {_ _}.
+Arguments core_ops_index_IndexMut_index_mut {_ _}.
+Arguments core_ops_index_IndexMut_index_mut_back {_ _}.
+
+(* Trait declaration [core::ops::deref::Deref] *)
+Record core_ops_deref_Deref (Self : Type) := mk_core_ops_deref_Deref {
+  core_ops_deref_Deref_target : Type;
+  core_ops_deref_Deref_deref : Self -> result core_ops_deref_Deref_target;
+}.
+Arguments mk_core_ops_deref_Deref {_}.
+Arguments core_ops_deref_Deref_target {_}.
+Arguments core_ops_deref_Deref_deref {_}.
+
+(* Trait declaration [core::ops::deref::DerefMut] *)
+Record core_ops_deref_DerefMut (Self : Type) := mk_core_ops_deref_DerefMut {
+  core_ops_deref_DerefMut_derefInst : core_ops_deref_Deref Self;
+  core_ops_deref_DerefMut_deref_mut : Self -> result core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target);
+  core_ops_deref_DerefMut_deref_mut_back : Self -> core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self;
 }.
-Arguments mk_range {_}.
+Arguments mk_core_ops_deref_DerefMut {_}.
+Arguments core_ops_deref_DerefMut_derefInst {_}.
+Arguments core_ops_deref_DerefMut_deref_mut {_}.
+Arguments core_ops_deref_DerefMut_deref_mut_back {_}.
+
+Record core_ops_range_Range (T : Type) := mk_core_ops_range_Range {
+  core_ops_range_Range_start : T;
+  core_ops_range_Range_end_ : T;
+}.
+Arguments mk_core_ops_range_Range {_}.
+Arguments core_ops_range_Range_start {_}.
+Arguments core_ops_range_Range_end_ {_}.
+
+(*** [alloc] *)
+
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x.
+
+(* Trait instance *)
+Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
+  core_ops_deref_Deref_target := Self;
+  core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self;
+|}.
+
+(* Trait instance *)
+Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
+  core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self;
+  core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self;
+  core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self;
+|}.
+
 
 (*** Arrays *)
 Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}.
@@ -419,51 +498,50 @@ Qed.
 (* TODO: finish the definitions *)
 Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n.
 
-Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
-Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
-Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n).
+(* For initialization *)
+Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n.
+
+Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
+Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n).
 
 (*** Slice *)
 Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}.
 
 Axiom slice_len : forall (T : Type) (s : slice T), usize.
-Axiom slice_index_shared : forall (T : Type) (x : slice T) (i : usize), result T.
-Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T.
-Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T).
+Axiom slice_index_usize : forall (T : Type) (x : slice T) (i : usize), result T.
+Axiom slice_update_usize : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T).
 
 (*** Subslices *)
 
-Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T).
-Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T).
-Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n).
+Axiom array_to_slice : forall (T : Type) (n : usize) (x : array T n), result (slice T).
+Axiom array_from_slice : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n).
+
+Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
+Axiom array_update_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize) (ns : slice T), result (array T n).
 
-Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
-Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
-Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n).
-Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
-Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
-Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T).
+Axiom slice_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize), result (slice T).
+Axiom slice_update_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize) (ns : slice T), result (slice T).
 
 (*** Vectors *)
 
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+Definition alloc_vec_Vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
 
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
+Definition alloc_vec_Vec_to_list {T: Type} (v: alloc_vec_Vec T) : list T := proj1_sig v.
 
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+Definition alloc_vec_Vec_length {T: Type} (v: alloc_vec_Vec T) : Z := Z.of_nat (length (alloc_vec_Vec_to_list v)).
 
-Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
+Definition alloc_vec_Vec_new (T: Type) : alloc_vec_Vec T := (exist _ [] le_0_usize_max).
 
-Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
+Lemma alloc_vec_Vec_len_in_usize {T} (v: alloc_vec_Vec T) : usize_min <= alloc_vec_Vec_length v <= usize_max.
 Proof.
-  unfold vec_length, usize_min.
+  unfold alloc_vec_Vec_length, usize_min.
   split.
   - lia.
   - apply (proj2_sig v).
 Qed.
 
-Definition vec_len (T: Type) (v: vec T) : usize :=
-  exist _ (vec_length v) (vec_len_in_usize v).
+Definition alloc_vec_Vec_len (T: Type) (v: alloc_vec_Vec T) : usize :=
+  exist _ (alloc_vec_Vec_length v) (alloc_vec_Vec_len_in_usize v).
 
 Fixpoint list_update {A} (l: list A) (n: nat) (a: A)
   : list A :=
@@ -474,50 +552,279 @@ Fixpoint list_update {A} (l: list A) (n: nat) (a: A)
     | S m => x :: (list_update t m a)
 end end.
 
-Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (vec B) :=
-  l <- f (vec_to_list v) ;
+Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
+  l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
   | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 (* The **forward** function shouldn't be used *)
-Definition vec_push_fwd (T: Type) (v: vec T) (x: T) : unit := tt.
+Definition alloc_vec_Vec_push_fwd (T: Type) (v: alloc_vec_Vec T) (x: T) : unit := tt.
 
-Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) :=
-  vec_bind v (fun l => Return (l ++ [x])).
+Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
+  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
 
 (* The **forward** function shouldn't be used *)
-Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
+Definition alloc_vec_Vec_insert_fwd (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result unit :=
+  if to_Z i <? alloc_vec_Vec_length v then Return tt else Fail_ Failure.
 
-Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
-  vec_bind v (fun l =>
+Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
+  alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
     then Return (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
-(* The **backward** function shouldn't be used *)
-Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T :=
-  match nth_error (vec_to_list v) (usize_to_nat i) with
-  | Some n => Return n
-  | None   => Fail_ Failure
-  end.
-
-Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
-
-(* The **backward** function shouldn't be used *)
-Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T :=
-  match nth_error (vec_to_list v) (usize_to_nat i) with
-  | Some n => Return n
-  | None   => Fail_ Failure
+(* Helper *)
+Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize), result T.
+
+(* Helper *)
+Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T).
+
+(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
+Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
+
+(* Trait declaration: [core::slice::index::SliceIndex] *)
+Record core_slice_index_SliceIndex (Self T : Type) := mk_core_slice_index_SliceIndex {
+  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
+  core_slice_index_SliceIndex_Output : Type;
+  core_slice_index_SliceIndex_get : Self -> T -> result (option core_slice_index_SliceIndex_Output);
+  core_slice_index_SliceIndex_get_mut : Self -> T -> result (option core_slice_index_SliceIndex_Output);
+  core_slice_index_SliceIndex_get_mut_back : Self -> T -> option core_slice_index_SliceIndex_Output -> result T;
+  core_slice_index_SliceIndex_get_unchecked : Self -> const_raw_ptr T -> result (const_raw_ptr core_slice_index_SliceIndex_Output);
+  core_slice_index_SliceIndex_get_unchecked_mut : Self -> mut_raw_ptr T -> result (mut_raw_ptr core_slice_index_SliceIndex_Output);
+  core_slice_index_SliceIndex_index : Self -> T -> result core_slice_index_SliceIndex_Output;
+  core_slice_index_SliceIndex_index_mut : Self -> T -> result core_slice_index_SliceIndex_Output;
+  core_slice_index_SliceIndex_index_mut_back : Self -> T -> core_slice_index_SliceIndex_Output -> result T;
+}.
+Arguments mk_core_slice_index_SliceIndex {_ _}.
+Arguments core_slice_index_SliceIndex_sealedInst {_ _}.
+Arguments core_slice_index_SliceIndex_Output {_ _}.
+Arguments core_slice_index_SliceIndex_get {_ _}.
+Arguments core_slice_index_SliceIndex_get_mut {_ _}.
+Arguments core_slice_index_SliceIndex_get_mut_back {_ _}.
+Arguments core_slice_index_SliceIndex_get_unchecked {_ _}.
+Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}.
+Arguments core_slice_index_SliceIndex_index {_ _}.
+Arguments core_slice_index_SliceIndex_index_mut {_ _}.
+Arguments core_slice_index_SliceIndex_index_mut_back {_ _}.
+
+(* [core::slice::index::[T]::index]: forward function *)
+Definition core_slice_index_Slice_index
+  (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
+  (s : slice T) (i : Idx) : result inst.(core_slice_index_SliceIndex_Output) :=
+  x <- inst.(core_slice_index_SliceIndex_get) i s;
+  match x with
+  | None => Fail_ Failure
+  | Some x => Return x
   end.
 
-Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
-  vec_bind v (fun l =>
-    if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
-    else Fail_ Failure).
+(* [core::slice::index::Range:::get]: forward function *)
+Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)).
+
+(* [core::slice::index::Range::get_mut]: forward function *)
+Axiom core_slice_index_RangeUsize_get_mut :
+  forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)).
+
+(* [core::slice::index::Range::get_mut]: backward function 0 *)
+Axiom core_slice_index_RangeUsize_get_mut_back :
+  forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T).
+
+(* [core::slice::index::Range::get_unchecked]: forward function *)
+Definition core_slice_index_RangeUsize_get_unchecked
+  (T : Type) :
+  core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) :=
+  (* Don't know what the model should be - for now we always fail to make
+     sure code which uses it fails *)
+  fun _ _ => Fail_ Failure.
+
+(* [core::slice::index::Range::get_unchecked_mut]: forward function *)
+Definition core_slice_index_RangeUsize_get_unchecked_mut
+  (T : Type) :
+  core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) :=
+  (* Don't know what the model should be - for now we always fail to make
+    sure code which uses it fails *)
+  fun _ _ => Fail_ Failure.
+
+(* [core::slice::index::Range::index]: forward function *)
+Axiom core_slice_index_RangeUsize_index :
+  forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).
+
+(* [core::slice::index::Range::index_mut]: forward function *)
+Axiom core_slice_index_RangeUsize_index_mut :
+  forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).
+
+(* [core::slice::index::Range::index_mut]: backward function 0 *)
+Axiom core_slice_index_RangeUsize_index_mut_back :
+  forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T).
+
+(* [core::slice::index::[T]::index_mut]: forward function *)
+Axiom core_slice_index_Slice_index_mut :
+  forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)),
+  slice T -> Idx -> result inst.(core_slice_index_SliceIndex_Output).
+
+(* [core::slice::index::[T]::index_mut]: backward function 0 *)
+Axiom core_slice_index_Slice_index_mut_back :
+  forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)),
+  slice T -> Idx -> inst.(core_slice_index_SliceIndex_Output) -> result (slice T).
+
+(* [core::array::[T; N]::index]: forward function *)
+Axiom core_array_Array_index :
+  forall (T Idx : Type) (N : usize) (inst : core_ops_index_Index (slice T) Idx)
+  (a : array T N) (i : Idx), result inst.(core_ops_index_Index_Output).
+
+(* [core::array::[T; N]::index_mut]: forward function *)
+Axiom core_array_Array_index_mut :
+  forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
+  (a : array T N) (i : Idx), result inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output).
+
+(* [core::array::[T; N]::index_mut]: backward function 0 *)
+Axiom core_array_Array_index_mut_back :
+  forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
+  (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N).
+
+(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
+Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
+  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
+
+(* Trait implementation: [core::slice::index::Range] *)
+Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) :
+  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {|
+  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
+  core_slice_index_SliceIndex_Output := slice T;
+  core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T;
+  core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T;
+  core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T;
+  core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T;
+  core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T;
+  core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T;
+  core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T;
+  core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T;
+|}.
+
+(* Trait implementation: [core::slice::index::[T]] *)
+Definition core_ops_index_IndexSliceTIInst (T Idx : Type)
+  (inst : core_slice_index_SliceIndex Idx (slice T)) :
+  core_ops_index_Index (slice T) Idx := {|
+  core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
+  core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst;
+|}.
+
+(* Trait implementation: [core::slice::index::[T]] *)
+Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type)
+  (inst : core_slice_index_SliceIndex Idx (slice T)) :
+  core_ops_index_IndexMut (slice T) Idx := {|
+  core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst;
+  core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst;
+  core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst;
+|}.
+
+(* Trait implementation: [core::array::[T; N]] *)
+Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize)
+  (inst : core_ops_index_Index (slice T) Idx) :
+  core_ops_index_Index (array T N) Idx := {|
+  core_ops_index_Index_Output := inst.(core_ops_index_Index_Output);
+  core_ops_index_Index_index := core_array_Array_index T Idx N inst;
+|}.
+
+(* Trait implementation: [core::array::[T; N]] *)
+Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize)
+  (inst : core_ops_index_IndexMut (slice T) Idx) :
+  core_ops_index_IndexMut (array T N) Idx := {|
+  core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
+  core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst;
+  core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst;
+|}.
+
+(* [core::slice::index::usize::get]: forward function *)
+Axiom core_slice_index_usize_get : forall (T : Type), usize -> slice T -> result (option T).
+
+(* [core::slice::index::usize::get_mut]: forward function *)
+Axiom core_slice_index_usize_get_mut : forall (T : Type), usize -> slice T -> result (option T).
+
+(* [core::slice::index::usize::get_mut]: backward function 0 *)
+Axiom core_slice_index_usize_get_mut_back :
+  forall (T : Type), usize -> slice T -> option T -> result (slice T).
+
+(* [core::slice::index::usize::get_unchecked]: forward function *)
+Axiom core_slice_index_usize_get_unchecked :
+  forall (T : Type), usize -> const_raw_ptr (slice T) -> result (const_raw_ptr T).
+
+(* [core::slice::index::usize::get_unchecked_mut]: forward function *)
+Axiom core_slice_index_usize_get_unchecked_mut :
+  forall (T : Type), usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr T).
+
+(* [core::slice::index::usize::index]: forward function *)
+Axiom core_slice_index_usize_index : forall (T : Type), usize -> slice T -> result T.
+
+(* [core::slice::index::usize::index_mut]: forward function *)
+Axiom core_slice_index_usize_index_mut : forall (T : Type), usize -> slice T -> result T.
+
+(* [core::slice::index::usize::index_mut]: backward function 0 *)
+Axiom core_slice_index_usize_index_mut_back :
+  forall (T : Type), usize -> slice T -> T -> result (slice T).
+
+(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
+Definition core_slice_index_private_slice_index_SealedUsizeInst
+  : core_slice_index_private_slice_index_Sealed usize := tt.
+
+(* Trait implementation: [core::slice::index::usize] *)
+Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
+  core_slice_index_SliceIndex usize (slice T) := {|
+  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
+  core_slice_index_SliceIndex_Output := T;
+  core_slice_index_SliceIndex_get := core_slice_index_usize_get T;
+  core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T;
+  core_slice_index_SliceIndex_get_mut_back := core_slice_index_usize_get_mut_back T;
+  core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked T;
+  core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_usize_get_unchecked_mut T;
+  core_slice_index_SliceIndex_index := core_slice_index_usize_index T;
+  core_slice_index_SliceIndex_index_mut := core_slice_index_usize_index_mut T;
+  core_slice_index_SliceIndex_index_mut_back := core_slice_index_usize_index_mut_back T;
+|}.
+
+(* [alloc::vec::Vec::index]: forward function *)
+Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
+  (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output).
+
+(* [alloc::vec::Vec::index_mut]: forward function *)
+Axiom alloc_vec_Vec_index_mut : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
+  (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output).
+
+(* [alloc::vec::Vec::index_mut]: backward function 0 *)
+Axiom alloc_vec_Vec_index_mut_back :
+  forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
+  (Self : alloc_vec_Vec T) (i : Idx) (x : inst.(core_slice_index_SliceIndex_Output)), result (alloc_vec_Vec T).
+
+(* Trait implementation: [alloc::vec::Vec] *)
+Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
+  (inst : core_slice_index_SliceIndex Idx (slice T)) :
+  core_ops_index_Index (alloc_vec_Vec T) Idx := {|
+  core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
+  core_ops_index_Index_index := alloc_vec_Vec_index T Idx inst;
+|}.
+
+(* Trait implementation: [alloc::vec::Vec] *)
+Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
+  (inst : core_slice_index_SliceIndex Idx (slice T)) :
+  core_ops_index_IndexMut (alloc_vec_Vec T) Idx := {|
+  core_ops_index_IndexMut_indexInst := alloc_vec_Vec_coreopsindexIndexInst T Idx inst;
+  core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut T Idx inst;
+  core_ops_index_IndexMut_index_mut_back := alloc_vec_Vec_index_mut_back T Idx inst;
+|}.
+
+(*** Theorems *)
+
+Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
+  alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
+    alloc_vec_Vec_index_usize v i.
+
+Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
+  alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
+    alloc_vec_Vec_index_usize v i.
+
+Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
+  alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x =
+    alloc_vec_Vec_update_usize v i x.
 
 End Primitives.
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 9db82069..94322ead 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -55,8 +55,12 @@ type string = string
 let is_zero (n: nat) : bool = n = 0
 let decrease (n: nat{n > 0}) : nat = n - 1
 
-let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
-let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
+let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+
+// We don't really use raw pointers for now
+type mut_raw_ptr (t : Type0) = { v : t }
+type const_raw_ptr (t : Type0) = { v : t }
 
 (*** Scalars *)
 /// Rem.: most of the following code was partially generated
@@ -100,6 +104,11 @@ type scalar_ty =
 | U64
 | U128
 
+let is_unsigned = function
+  | Isize | I8 | I16 | I32 | I64 | I128 -> false
+  | Usize | U8 | U16 | U32 | U64 | U128 -> true
+
+
 let scalar_min (ty : scalar_ty) : int =
   match ty with
   | Isize -> isize_min
@@ -162,6 +171,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
 let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x * y)
 
+let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize })
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logxor #8 x y
+  | U16 -> FStar.UInt.logxor #16 x y
+  | U32 -> FStar.UInt.logxor #32 x y
+  | U64 -> FStar.UInt.logxor #64 x y
+  | U128 -> FStar.UInt.logxor #128 x y
+
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 // TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
@@ -169,17 +187,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
@@ -231,7 +276,7 @@ let u32_add = scalar_add #U32
 let u64_add = scalar_add #U64
 let u128_add = scalar_add #U128
 
-/// Substraction
+/// Subtraction
 let isize_sub = scalar_sub #Isize
 let i8_sub = scalar_sub #I8
 let i16_sub = scalar_sub #I16
@@ -259,12 +304,65 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
-(*** Range *)
-type range (a : Type0) = {
+/// Logical operators, defined for unsigned types only, so far
+let u8_xor = scalar_lxor #U8
+let u16_xor = scalar_lxor #U16
+let u32_xor = scalar_lxor #U32
+let u64_xor = scalar_lxor #U64
+let u128_xor = scalar_lxor #U128
+
+(*** core::ops *)
+
+// Trait declaration: [core::ops::index::Index]
+noeq type core_ops_index_Index (self idx : Type0) = {
+  output : Type0;
+  index : self → idx → result output
+}
+
+// Trait declaration: [core::ops::index::IndexMut]
+noeq type core_ops_index_IndexMut (self idx : Type0) = {
+  indexInst : core_ops_index_Index self idx;
+  index_mut : self → idx → result indexInst.output;
+  index_mut_back : self → idx → indexInst.output → result self;
+}
+
+// Trait declaration [core::ops::deref::Deref]
+noeq type core_ops_deref_Deref (self : Type0) = {
+  target : Type0;
+  deref : self → result target;
+}
+
+// Trait declaration [core::ops::deref::DerefMut]
+noeq type core_ops_deref_DerefMut (self : Type0) = {
+  derefInst : core_ops_deref_Deref self;
+  deref_mut : self → result derefInst.target;
+  deref_mut_back : self → derefInst.target → result self;
+}
+
+type core_ops_range_Range (a : Type0) = {
   start : a;
   end_ : a;
 }
 
+(*** [alloc] *)
+
+let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
+  target = self;
+  deref = alloc_boxed_Box_deref self;
+}
+
+// Trait instance
+let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
+  derefInst = alloc_boxed_Box_coreopsDerefInst self;
+  deref_mut = alloc_boxed_Box_deref_mut self;
+  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
+}
+
 (*** Array *)
 type array (a : Type0) (n : usize) = s:list a{length s = n}
 
@@ -278,15 +376,11 @@ let mk_array (a : Type0) (n : usize)
   normalize_term_spec (FStar.List.Tot.length l);
   l
 
-let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
-  if i < length x then Return (index x i)
-  else Fail Failure
-
-let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
+let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
   if i < length x then Return (index x i)
   else Fail Failure
 
-let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
@@ -295,55 +389,54 @@ type slice (a : Type0) = s:list a{length s <= usize_max}
 
 let slice_len (a : Type0) (s : slice a) : usize = length s
 
-let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a =
+let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a =
   if i < length x then Return (index x i)
   else Fail Failure
 
-let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a =
-  if i < length x then Return (index x i)
-  else Fail Failure
-
-let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
+let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
 (*** Subslices *)
 
-let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
-let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
-let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
+let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
+let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
   if length s = n then Return s
   else Fail Failure
 
 // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
-let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) =
-  admit()
-
-let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) =
+let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
   admit()
 
-let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) =
+let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) =
   admit()
 
-let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) =
+let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
   admit()
 
-let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) =
+let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
   admit()
 
-let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) =
+let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
   admit()
 
 (*** Vector *)
-type vec (a : Type0) = v:list a{length v <= usize_max}
+type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max}
 
-let vec_new (a  : Type0) : vec a = assert_norm(length #a [] == 0); []
-let vec_len (a : Type0) (v : vec a) : usize = length v
+let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
+let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v
+
+// Helper
+let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
+  if i < length v then Return (index v i) else Fail Failure
+// Helper
+let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **forward** function shouldn't be used
-let vec_push_fwd (a  : Type0) (v : vec a) (x : a) : unit = ()
-let vec_push_back (a  : Type0) (v : vec a) (x : a) :
-  Pure (result (vec a))
+let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
+let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
+  Pure (result (alloc_vec_Vec a))
   (requires True)
   (ensures (fun res ->
     match res with
@@ -358,18 +451,279 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   else Fail Failure
 
 // The **forward** function shouldn't be used
-let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
   if i < length v then Return () else Fail Failure
-let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
+let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Return (list_update v i x) else Fail Failure
 
-// The **backward** function shouldn't be used
-let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail Failure
-let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail Failure
+// Trait declaration: [core::slice::index::private_slice_index::Sealed]
+type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
+
+// Trait declaration: [core::slice::index::SliceIndex]
+noeq type core_slice_index_SliceIndex (self t : Type0) = {
+  sealedInst : core_slice_index_private_slice_index_Sealed self;
+  output : Type0;
+  get : self → t → result (option output);
+  get_mut : self → t → result (option output);
+  get_mut_back : self → t → option output → result t;
+  get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
+  get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
+  index : self → t → result output;
+  index_mut : self → t → result output;
+  index_mut_back : self → t → output → result t;
+}
 
-let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail Failure
-let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail Failure
+// [core::slice::index::[T]::index]: forward function
+let core_slice_index_Slice_index
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (s : slice t) (i : idx) : result inst.output =
+  let* x = inst.get i s in
+  match x with
+  | None -> Fail Failure
+  | Some x -> Return x
+
+// [core::slice::index::Range:::get]: forward function
+let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
+  result (option (slice t)) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_mut]: forward function
+let core_slice_index_RangeUsize_get_mut
+  (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_mut]: backward function 0
+let core_slice_index_RangeUsize_get_mut_back
+  (t : Type0) :
+  core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::get_unchecked]: forward function
+let core_slice_index_RangeUsize_get_unchecked
+  (t : Type0) :
+  core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::get_unchecked_mut]: forward function
+let core_slice_index_RangeUsize_get_unchecked_mut
+  (t : Type0) :
+  core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) =
+  // Don't know what the model should be - for now we always fail to make
+  // sure code which uses it fails
+  fun _ _ -> Fail Failure
+
+// [core::slice::index::Range::index]: forward function
+let core_slice_index_RangeUsize_index
+  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::index_mut]: forward function
+let core_slice_index_RangeUsize_index_mut
+  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::Range::index_mut]: backward function 0
+let core_slice_index_RangeUsize_index_mut_back
+  (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::[T]::index_mut]: forward function
+let core_slice_index_Slice_index_mut
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
+  slice t → idx → result inst.output =
+  admit () // 
+
+// [core::slice::index::[T]::index_mut]: backward function 0
+let core_slice_index_Slice_index_mut_back
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
+  slice t → idx → inst.output → result (slice t) =
+  admit () // TODO
+
+// [core::array::[T; N]::index]: forward function
+let core_array_Array_index
+  (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
+  (a : array t n) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [core::array::[T; N]::index_mut]: forward function
+let core_array_Array_index_mut
+  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
+  (a : array t n) (i : idx) : result inst.indexInst.output =
+  admit () // TODO
+
+// [core::array::[T; N]::index_mut]: backward function 0
+let core_array_Array_index_mut_back
+  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
+  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::Range]
+let core_slice_index_private_slice_index_SealedRangeUsizeInst
+  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
+
+// Trait implementation: [core::slice::index::Range]
+let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
+  output = slice t;
+  get = core_slice_index_RangeUsize_get t;
+  get_mut = core_slice_index_RangeUsize_get_mut t;
+  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
+  get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
+  index = core_slice_index_RangeUsize_index t;
+  index_mut = core_slice_index_RangeUsize_index_mut t;
+  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (slice t) idx = {
+  output = inst.output;
+  index = core_slice_index_Slice_index t idx inst;
+}
+
+// Trait implementation: [core::slice::index::[T]]
+let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (slice t) idx = {
+  indexInst = core_ops_index_IndexSliceTIInst t idx inst;
+  index_mut = core_slice_index_Slice_index_mut t idx inst;
+  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_Index (slice t) idx) :
+  core_ops_index_Index (array t n) idx = {
+  output = inst.output;
+  index = core_array_Array_index t idx n inst;
+}
+
+// Trait implementation: [core::array::[T; N]]
+let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
+  (inst : core_ops_index_IndexMut (slice t) idx) :
+  core_ops_index_IndexMut (array t n) idx = {
+  indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
+  index_mut = core_array_Array_index_mut t idx n inst;
+  index_mut_back = core_array_Array_index_mut_back t idx n inst;
+}
+
+// [core::slice::index::usize::get]: forward function
+let core_slice_index_usize_get
+  (t : Type0) : usize → slice t → result (option t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_mut]: forward function
+let core_slice_index_usize_get_mut
+  (t : Type0) : usize → slice t → result (option t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_mut]: backward function 0
+let core_slice_index_usize_get_mut_back
+  (t : Type0) : usize → slice t → option t → result (slice t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked]: forward function
+let core_slice_index_usize_get_unchecked
+  (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::get_unchecked_mut]: forward function
+let core_slice_index_usize_get_unchecked_mut
+  (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) =
+  admit () // TODO
+
+// [core::slice::index::usize::index]: forward function
+let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
+  admit () // TODO
+
+// [core::slice::index::usize::index_mut]: forward function
+let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
+  admit () // TODO
+
+// [core::slice::index::usize::index_mut]: backward function 0
+let core_slice_index_usize_index_mut_back
+  (t : Type0) : usize → slice t → t → result (slice t) =
+  admit () // TODO
+
+// Trait implementation: [core::slice::index::private_slice_index::usize]
+let core_slice_index_private_slice_index_SealedUsizeInst
+  : core_slice_index_private_slice_index_Sealed usize = ()
+
+// Trait implementation: [core::slice::index::usize]
+let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
+  core_slice_index_SliceIndex usize (slice t) = {
+  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
+  output = t;
+  get = core_slice_index_usize_get t;
+  get_mut = core_slice_index_usize_get_mut t;
+  get_mut_back = core_slice_index_usize_get_mut_back t;
+  get_unchecked = core_slice_index_usize_get_unchecked t;
+  get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
+  index = core_slice_index_usize_index t;
+  index_mut = core_slice_index_usize_index_mut t;
+  index_mut_back = core_slice_index_usize_index_mut_back t;
+}
+
+// [alloc::vec::Vec::index]: forward function
+let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [alloc::vec::Vec::index_mut]: forward function
+let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
+  admit () // TODO
+
+// [alloc::vec::Vec::index_mut]: backward function 0
+let alloc_vec_Vec_index_mut_back
+  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
+  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
+  admit () // TODO
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_Index (alloc_vec_Vec t) idx = {
+  output = inst.output;
+  index = alloc_vec_Vec_index t idx inst;
+}
+
+// Trait implementation: [alloc::vec::Vec]
+let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
+  (inst : core_slice_index_SliceIndex idx (slice t)) :
+  core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
+  indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
+  index_mut = alloc_vec_Vec_index_mut t idx inst;
+  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
+}
+
+(*** Theorems *)
+
+let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
+  Lemma (
+    alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
+  =
+  admit()
+
+let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
+  Lemma (
+    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
+      alloc_vec_Vec_update_usize v i x)
+  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
+  =
+  admit()
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 82da4de9..916988be 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -555,6 +555,32 @@ Proof
 QED
 val _ = evalLib.add_unfold_thm "mk_isize_unfold"
 
+(** Constants *)
+val core_i8_min_def    = Define ‘core_i8_min     = int_to_i8 i8_min’
+val core_i8_max_def    = Define ‘core_i8_max     = int_to_i8 i8_max’
+val core_i16_min_def   = Define ‘core_i16_min    = int_to_i16 i16_min’
+val core_i16_max_def   = Define ‘core_i16_max    = int_to_i16 i16_max’
+val core_i32_min_def   = Define ‘core_i32_min    = int_to_i32 i32_min’
+val core_i32_max_def   = Define ‘core_i32_max    = int_to_i32 i32_max’
+val core_i64_min_def   = Define ‘core_i64_min    = int_to_i64 i64_min’
+val core_i64_max_def   = Define ‘core_i64_max    = int_to_i64 i64_max’
+val core_i128_min_def  = Define ‘core_i128_min   = int_to_i128 i128_min’
+val core_i128_max_def  = Define ‘core_i128_max   = int_to_i128 i128_max’
+val core_isize_min_def = Define ‘core_isize_min  = int_to_isize isize_min’
+val core_isize_max_def = Define ‘core_isize_max  = int_to_isize isize_max’
+val core_u8_min_def    = Define ‘core_u8_min     = int_to_u8 0’
+val core_u8_max_def    = Define ‘core_u8_max     = int_to_u8 u8_max’
+val core_u16_min_def   = Define ‘core_u16_min    = int_to_u16 0’
+val core_u16_max_def   = Define ‘core_u16_max    = int_to_u16 u16_max’
+val core_u32_min_def   = Define ‘core_u32_min    = int_to_u32 0’
+val core_u32_max_def   = Define ‘core_u32_max    = int_to_u32 u32_max’
+val core_u64_min_def   = Define ‘core_u64_min    = int_to_u64 0’
+val core_u64_max_def   = Define ‘core_u64_max    = int_to_u64 u64_max’
+val core_u128_min_def  = Define ‘core_u128_min   = int_to_u128 0’
+val core_u128_max_def  = Define ‘core_u128_max   = int_to_u128 u128_max’
+val core_usize_min_def = Define ‘core_usize_min  = int_to_usize 0’
+val core_usize_max_def = Define ‘core_usize_max  = int_to_usize usize_max’
+
 val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’
 val i8_neg_def    = Define ‘i8_neg x    = mk_i8 (- (i8_to_int x))’
 val i16_neg_def   = Define ‘i16_neg x   = mk_i16 (- (i16_to_int x))’
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 6660b02d..4ae6bb3e 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -46,6 +46,30 @@ sig
   
   (*  Definitions  *)
     val bind_def : thm
+    val core_i128_max_def : thm
+    val core_i128_min_def : thm
+    val core_i16_max_def : thm
+    val core_i16_min_def : thm
+    val core_i32_max_def : thm
+    val core_i32_min_def : thm
+    val core_i64_max_def : thm
+    val core_i64_min_def : thm
+    val core_i8_max_def : thm
+    val core_i8_min_def : thm
+    val core_isize_max_def : thm
+    val core_isize_min_def : thm
+    val core_u128_max_def : thm
+    val core_u128_min_def : thm
+    val core_u16_max_def : thm
+    val core_u16_min_def : thm
+    val core_u32_max_def : thm
+    val core_u32_min_def : thm
+    val core_u64_max_def : thm
+    val core_u64_min_def : thm
+    val core_u8_max_def : thm
+    val core_u8_min_def : thm
+    val core_usize_max_def : thm
+    val core_usize_min_def : thm
     val error_BIJ : thm
     val error_CASE : thm
     val error_TY_DEF : thm
@@ -566,6 +590,102 @@ sig
           monad_bind x f =
           case x of Return y => f y | Fail e => Fail e | Diverge => Diverge
    
+   [core_i128_max_def]  Definition
+      
+      ⊢ core_i128_max = int_to_i128 i128_max
+   
+   [core_i128_min_def]  Definition
+      
+      ⊢ core_i128_min = int_to_i128 i128_min
+   
+   [core_i16_max_def]  Definition
+      
+      ⊢ core_i16_max = int_to_i16 i16_max
+   
+   [core_i16_min_def]  Definition
+      
+      ⊢ core_i16_min = int_to_i16 i16_min
+   
+   [core_i32_max_def]  Definition
+      
+      ⊢ core_i32_max = int_to_i32 i32_max
+   
+   [core_i32_min_def]  Definition
+      
+      ⊢ core_i32_min = int_to_i32 i32_min
+   
+   [core_i64_max_def]  Definition
+      
+      ⊢ core_i64_max = int_to_i64 i64_max
+   
+   [core_i64_min_def]  Definition
+      
+      ⊢ core_i64_min = int_to_i64 i64_min
+   
+   [core_i8_max_def]  Definition
+      
+      ⊢ core_i8_max = int_to_i8 i8_max
+   
+   [core_i8_min_def]  Definition
+      
+      ⊢ core_i8_min = int_to_i8 i8_min
+   
+   [core_isize_max_def]  Definition
+      
+      ⊢ core_isize_max = int_to_isize isize_max
+   
+   [core_isize_min_def]  Definition
+      
+      ⊢ core_isize_min = int_to_isize isize_min
+   
+   [core_u128_max_def]  Definition
+      
+      ⊢ core_u128_max = int_to_u128 u128_max
+   
+   [core_u128_min_def]  Definition
+      
+      ⊢ core_u128_min = int_to_u128 0
+   
+   [core_u16_max_def]  Definition
+      
+      ⊢ core_u16_max = int_to_u16 u16_max
+   
+   [core_u16_min_def]  Definition
+      
+      ⊢ core_u16_min = int_to_u16 0
+   
+   [core_u32_max_def]  Definition
+      
+      ⊢ core_u32_max = int_to_u32 u32_max
+   
+   [core_u32_min_def]  Definition
+      
+      ⊢ core_u32_min = int_to_u32 0
+   
+   [core_u64_max_def]  Definition
+      
+      ⊢ core_u64_max = int_to_u64 u64_max
+   
+   [core_u64_min_def]  Definition
+      
+      ⊢ core_u64_min = int_to_u64 0
+   
+   [core_u8_max_def]  Definition
+      
+      ⊢ core_u8_max = int_to_u8 u8_max
+   
+   [core_u8_min_def]  Definition
+      
+      ⊢ core_u8_min = int_to_u8 0
+   
+   [core_usize_max_def]  Definition
+      
+      ⊢ core_usize_max = int_to_usize usize_max
+   
+   [core_usize_min_def]  Definition
+      
+      ⊢ core_usize_min = int_to_usize 0
+   
    [error_BIJ]  Definition
       
       ⊢ (∀a. num2error (error2num a) = a) ∧
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index 9c11ed45..8ada4171 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -57,4 +57,16 @@ theorem int_pos_ind (p : Int → Prop) :
 -- TODO: there is probably something more general to do
 theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp
 
+-- This is mostly used in termination proofs
+theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
+  ↑(x.toNat) < y := by
+  simp [*]
+
+-- This is mostly used in termination proofs
+theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
+  (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) :
+  ↑(x.toNat - x') < y := by
+  have : 0 ≤ x := by linarith
+  simp [Int.toNat_sub_of_le, *]
+
 end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 3359ecdb..a57f8bb1 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -162,7 +162,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false)
+    Utils.simpAt true [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
     -- Return the new value
     pure nval
 
@@ -240,7 +240,7 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Ta
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
   -- More preprocessing
-  Tactic.allGoals (Utils.tryTac (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard))
+  Tactic.allGoals (Utils.tryTac (Utils.simpAt true [] [``nat_zero_eq_int_zero] [] .wildcard))
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
@@ -270,6 +270,17 @@ elab "int_tac" args:(" split_goal"?): tactic =>
   let split := args.raw.getArgs.size > 0
   intTac split (do pure ())
 
+-- For termination proofs
+syntax "int_decr_tac" : tactic
+macro_rules
+  | `(tactic| int_decr_tac) =>
+    `(tactic|
+      simp_wf;
+      -- TODO: don't use a macro (namespace problems)
+      (first | apply Arith.to_int_to_nat_lt
+             | apply Arith.to_int_sub_to_nat_lt) <;>
+      simp_all <;> int_tac)
+
 example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
   int_tac_preprocess
   linarith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 47751c8a..2342cce6 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -17,7 +17,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
    -- Reveal the concrete bounds, simplify calls to [ofInt]
-   Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
+   Utils.simpAt true [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
                  ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
                  ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
                  ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
@@ -36,6 +36,17 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
 elab "scalar_tac" : tactic =>
   scalarTac false
 
+-- For termination proofs
+syntax "scalar_decr_tac" : tactic
+macro_rules
+  | `(tactic| scalar_decr_tac) =>
+    `(tactic|
+      simp_wf;
+      -- TODO: don't use a macro (namespace problems)
+      (first | apply Arith.to_int_to_nat_lt
+             | apply Arith.to_int_sub_to_nat_lt) <;>
+      simp_all <;> scalar_tac)
+
 instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
   -- prop_ty is inferred
   prop := λ x => And.intro x.hmin x.hmax
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a940da25..f71f2de2 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -112,7 +112,13 @@ def pairwise_rel
 
 section Lemmas
 
-variable {α : Type u} 
+variable {α : Type u}
+
+def ireplicate {α : Type u} (i : ℤ) (x : α) : List α :=
+  if i ≤ 0 then []
+  else x :: ireplicate (i - 1) x
+termination_by ireplicate i x => i.toNat
+decreasing_by int_decr_tac
 
 @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
 @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update]
@@ -129,6 +135,10 @@ variable {α : Type u}
 @[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice]
 @[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice]
 
+@[simp] theorem ireplicate_zero : ireplicate 0 x = [] := by rw [ireplicate]; simp
+@[simp] theorem ireplicate_nzero_cons (hne : 0 < i) : ireplicate i x = x :: ireplicate (i - 1) x := by
+  rw [ireplicate]; simp [*]; intro; linarith
+
 @[simp]
 theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl :=
   match tl with
@@ -144,6 +154,33 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s
         conv at this => lhs; simp [slice, *]
         simp [*, slice]
 
+@[simp]
+theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+  ireplicate l x = replicate l.toNat x :=
+  if hz: l = 0 then by
+    simp [*]
+  else by
+    have : 0 < l := by int_tac
+    have hr := ireplicate_replicate (l - 1) x (by int_tac)
+    simp [*]
+    have hl : l.toNat = .succ (l.toNat - 1) := by
+      cases hl: l.toNat <;> simp_all
+    conv => rhs; rw[hl]
+termination_by ireplicate_replicate l x h => l.toNat
+decreasing_by int_decr_tac
+
+@[simp]
+theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+  (ireplicate l x).len = l :=
+  if hz: l = 0 then by
+    simp [*]
+  else by
+    have : 0 < l := by int_tac
+    have hr := ireplicate_len (l - 1) x (by int_tac)
+    simp [*]
+termination_by ireplicate_len l x h => l.toNat
+decreasing_by int_decr_tac
+
 theorem len_eq_length (ls : List α) : ls.len = ls.length := by
   induction ls
   . rfl
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 6b7b0792..613b6076 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,4 +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.CoreOps
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
new file mode 100644
index 00000000..6c89c6bb
--- /dev/null
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+import Base.Primitives.CoreOps
+
+open Primitives
+open Result
+
+namespace alloc
+
+namespace boxed -- alloc.boxed
+
+namespace Box -- alloc.boxed.Box
+
+def deref (T : Type) (x : T) : Result T := ret x
+def deref_mut (T : Type) (x : T) : Result T := ret x
+def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
+
+/-- Trait instance -/
+def coreopsDerefInst (Self : Type) :
+  core.ops.deref.Deref Self := {
+  Target := Self
+  deref := deref Self
+}
+
+/-- Trait instance -/
+def coreopsDerefMutInst (Self : Type) :
+  core.ops.deref.DerefMut Self := {
+  derefInst := coreopsDerefInst Self
+  deref_mut := deref_mut Self
+  deref_mut_back := deref_mut_back Self
+}
+
+end Box -- alloc.boxed.Box
+
+end boxed -- alloc.boxed
+
+end alloc
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
deleted file mode 100644
index 6c95fd78..00000000
--- a/backends/lean/Base/Primitives/Array.lean
+++ /dev/null
@@ -1,394 +0,0 @@
-/- Arrays/slices -/
-import Lean
-import Lean.Meta.Tactic.Simp
-import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
-import Mathlib.Tactic.Linarith
-import Base.IList
-import Base.Primitives.Scalar
-import Base.Primitives.Range
-import Base.Arith
-import Base.Progress.Base
-
-namespace Primitives
-
-open Result Error
-
-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
-  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
-
-instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
-  prop_ty := λ x => p x
-  prop := λ x => x.property
-
-@[simp]
-abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
-
-@[simp]
-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.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.make Int (Usize.ofInt 2) [0, 1]
-
-@[simp]
-abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
-  v.val.index i
-
-@[simp]
-abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
-  v.val.slice i j
-
-def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some x => ret x
-
-/- In the theorems below: we don't always need the `∃ ..`, but we use one
-   so that `progress` introduces an opaque variable and an equality. This
-   helps control the context.
- -/
-
-@[pspec]
-theorem Array.index_shared_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
-  (hbound : i.val < v.length) :
-  ∃ x, v.index_shared α n i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_shared]
-  -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp [*]
-
--- This shouldn't be used
-def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (_: α) : Result Unit :=
-  if i.val < List.length v.val then
-    .ret ()
-  else
-    .fail arrayOutOfBounds
-
-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
-
-@[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 α 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) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
-
-@[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 α n i x = ret nv ∧
-  nv.val = v.val.update i.val x
-  := by
-  simp only [index_mut_back]
-  have h := List.indexOpt_bounds v.val i.val
-  split
-  . simp_all [length]; cases h <;> scalar_tac
-  . simp_all
-
-def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
-
-instance (a : Type u) : Arith.HasIntProp (Slice a) where
-  prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
-  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
-
-instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
-  prop_ty := λ x => p x
-  prop := λ x => x.property
-
-@[simp]
-abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
-
-@[simp]
-abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
-
-example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
-  scalar_tac
-
-def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
-
--- TODO: very annoying that the α is an explicit parameter
-def Slice.len (α : Type u) (v : Slice α) : Usize :=
-  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
-
-@[simp]
-theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
-  by rfl
-
-@[simp]
-abbrev Slice.index {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
-  v.val.index i
-
-@[simp]
-abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
-  s.val.slice i j
-
-def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some x => ret x
-
-/- In the theorems below: we don't always need the `∃ ..`, but we use one
-   so that `progress` introduces an opaque variable and an equality. This
-   helps control the context.
- -/
-
-@[pspec]
-theorem Slice.index_shared_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
-  (hbound : i.val < v.length) :
-  ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_shared]
-  -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp [*]
-
--- This shouldn't be used
-def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
-  if i.val < List.length v.val then
-    .ret ()
-  else
-    .fail arrayOutOfBounds
-
-def Slice.index_mut (α : Type u) (v: Slice α) (i: Usize) : Result α :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some x => ret x
-
-@[pspec]
-theorem Slice.index_mut_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
-  (hbound : i.val < v.length) :
-  ∃ x, v.index_mut α 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 Slice.index_mut_back (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
-
-@[pspec]
-theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
-  (hbound : i.val < v.length) :
-  ∃ nv, v.index_mut_back α i x = ret nv ∧
-  nv.val = v.val.update i.val x
-  := by
-  simp only [index_mut_back]
-  have h := List.indexOpt_bounds v.val i.val
-  split
-  . simp_all [length]; cases h <;> scalar_tac
-  . 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_shared_spec` spec theorem below (through the
-   `progress` tactic), meaning `Array.to_slice_shared` should be considered as opaque.
-   All what the spec theorem reveals is that the "representative" lists are the same. -/
-def Array.to_slice_shared (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
-  ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
-
-@[pspec]
-theorem Array.to_slice_shared_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, to_slice_shared α n v = ret s ∧ v.val = s.val := by simp [to_slice_shared]
-
-def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
-  to_slice_shared α n v
-
-@[pspec]
-theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, Array.to_slice_shared α n v = ret s ∧ v.val = s.val := to_slice_shared_spec v
-
-def Array.to_slice_mut_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
-  if h: s.val.len = n.val then
-    ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
-  else fail panic
-
-@[pspec]
-theorem Array.to_slice_mut_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
-  ∃ na, to_slice_mut_back α n a ns = ret na ∧ na.val = ns.val
-  := by simp [to_slice_mut_back, *]
-
-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,
-          by
-            simp [← List.len_eq_length]
-            have := a.val.slice_len_le r.start.val r.end_.val
-            scalar_tac ⟩
-  else
-    fail panic
-
-@[pspec]
-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, 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 [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.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
-  Array.subslice_shared α n a r
-
-@[pspec]
-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, 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))
-  := subslice_shared_spec a r h0 h1
-
-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
-    let s_end := a.val.idrop r.end_.val
-    have : s_beg.len = r.start.val := by
-      apply List.itake_len
-      . simp_all; scalar_tac
-      . scalar_tac
-    have : s_end.len = a.val.len - r.end_.val := by
-      apply List.idrop_len
-      . scalar_tac
-      . scalar_tac
-    let na := s_beg.append (s.val.append s_end)
-    have : na.len = a.val.len := by simp [*]
-    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
-  else
-    fail panic
-
--- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
--- but: some symbols like `+` are already overloaded to be notations for monadic
--- operations/
--- We should introduce special symbols for the monadic arithmetic operations
--- (the use will never write those symbols directly).
-@[pspec]
-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, 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 [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
-  have ⟨ h0, h1, h2 ⟩ := h
-  clear h
-  split_conjs
-  . intro i _ _
-    have := h0 i (by int_tac) (by int_tac)
-    simp [*]
-  . intro i _ _
-    have := h1 i (by int_tac) (by int_tac)
-    simp [*]
-  . intro i _ _
-    have := h2 i (by int_tac) (by int_tac)
-    simp [*]
-
-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,
-          by
-            simp [← List.len_eq_length]
-            have := s.val.slice_len_le r.start.val r.end_.val
-            scalar_tac ⟩
-  else
-    fail panic
-
-@[pspec]
-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, 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 [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.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
-  Slice.subslice_shared α s r
-
-@[pspec]
-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, 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))
-  := 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.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
-    let s_end := s.val.idrop r.end_.val
-    have : s_beg.len = r.start.val := by
-      apply List.itake_len
-      . simp_all; scalar_tac
-      . scalar_tac
-    have : s_end.len = s.val.len - r.end_.val := by
-      apply List.idrop_len
-      . scalar_tac
-      . scalar_tac
-    let ns := s_beg.append (ss.val.append s_end)
-    have : ns.len = s.val.len := by simp [*]
-    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
-  else
-    fail panic
-
-@[pspec]
-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, 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 [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
-  have ⟨ h0, h1, h2 ⟩ := h
-  clear h
-  split_conjs
-  . intro i _ _
-    have := h0 i (by int_tac) (by int_tac)
-    simp [*]
-  . intro i _ _
-    have := h1 i (by int_tac) (by int_tac)
-    simp [*]
-  . intro i _ _
-    have := h2 i (by int_tac) (by int_tac)
-    simp [*]
-
-end Primitives
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
new file mode 100644
index 00000000..f68c0846
--- /dev/null
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -0,0 +1,552 @@
+/- Arrays/Slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+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
+
+namespace Primitives
+
+open Result Error core.ops.range
+
+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
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
+
+@[simp]
+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.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.make Int (Usize.ofInt 2) [0, 1]
+
+@[simp]
+abbrev Array.index_s {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
+  v.val.index i
+
+@[simp]
+abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
+  v.val.slice i j
+
+def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+-- For initialization
+def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
+  ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩
+
+@[pspec]
+theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
+  ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by
+  simp [Array.repeat]
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_usize]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some _ =>
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.update_usize α n i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [update_usize]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
+
+def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
+
+instance (a : Type u) : Arith.HasIntProp (Slice a) where
+  prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
+
+@[simp]
+abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
+
+example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+
+-- TODO: very annoying that the α is an explicit parameter
+def Slice.len (α : Type u) (v : Slice α) : Usize :=
+  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
+  by rfl
+
+@[simp]
+abbrev Slice.index_s {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
+  v.val.index i
+
+@[simp]
+abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
+  s.val.slice i j
+
+def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_usize]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+-- This shouldn't be used
+def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
+  if i.val < List.length v.val then
+    .ret ()
+  else
+    .fail arrayOutOfBounds
+
+def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some _ =>
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.update_usize α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [update_usize]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . 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 ⟩
+
+@[pspec]
+theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
+  ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+
+def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
+  if h: s.val.len = n.val then
+    ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+  else fail panic
+
+@[pspec]
+theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
+  ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+  := by simp [from_slice, *]
+
+def Array.subslice (α : 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,
+          by
+            simp [← List.len_eq_length]
+            have := a.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Array.subslice_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, subslice α 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 [subslice, *]
+  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.update_subslice (α : 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
+    let s_end := a.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = a.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let na := s_beg.append (s.val.append s_end)
+    have : na.len = a.val.len := by simp [*]
+    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+-- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
+-- but: some symbols like `+` are already overloaded to be notations for monadic
+-- operations/
+-- We should introduce special symbols for the monadic arithmetic operations
+-- (the use will never write those symbols directly).
+@[pspec]
+theorem Array.update_subslice_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, update_subslice α n a r s = ret na ∧
+  (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+  (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
+  (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
+  simp [update_subslice, *]
+  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
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h2 i (by int_tac) (by int_tac)
+    simp [*]
+
+def Slice.subslice (α : 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,
+          by
+            simp [← List.len_eq_length]
+            have := s.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+  (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
+  ∃ ns, subslice α 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_s i = s.index_s (r.start.val + i))
+  := by
+  simp [subslice, *]
+  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 [*]
+
+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.update_subslice (α : 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
+    let s_end := s.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = s.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let ns := s_beg.append (ss.val.append s_end)
+    have : ns.len = s.val.len := by simp [*]
+    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.update_subslice_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, update_subslice α a r ss = ret na ∧
+  (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+  (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
+  (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
+  simp [update_subslice, *]
+  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
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    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 T : Type) where
+  sealedInst : core.slice.index.private_slice_index.Sealed Self
+  Output : Type
+  get : Self → T → Result (Option Output)
+  get_mut : Self → T → Result (Option Output)
+  get_mut_back : Self → T → Option Output → Result T
+  get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output)
+  get_unchecked_mut : Self → MutRawPtr T → Result (MutRawPtr Output)
+  index : Self → T → Result Output
+  index_mut : Self → T → Result Output
+  index_mut_back : Self → T → Output → Result T
+
+/- [core::slice::index::[T]::index]: forward function -/
+def core.slice.index.Slice.index
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (slice : Slice T) (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.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
+  Result (Option (Slice T)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: forward function -/
+def core.slice.index.RangeUsize.get_mut
+  (T : Type) : Range Usize → Slice T → Result (Option (Slice T)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: backward function 0 -/
+def core.slice.index.RangeUsize.get_mut_back
+  (T : Type) :
+  Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_unchecked]: forward function -/
+def core.slice.index.RangeUsize.get_unchecked
+  (T : Type) :
+  Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) :=
+  -- 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.RangeUsize.get_unchecked_mut
+  (T : Type) :
+  Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) :=
+  -- 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.RangeUsize.index
+  (T : Type) : Range Usize → Slice T → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: forward function -/
+def core.slice.index.RangeUsize.index_mut
+  (T : Type) : Range Usize → Slice T → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: backward function 0 -/
+def core.slice.index.RangeUsize.index_mut_back
+  (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: forward function -/
+def core.slice.index.Slice.index_mut
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
+  Slice T → I → Result inst.Output :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: backward function 0 -/
+def core.slice.index.Slice.index_mut_back
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
+  Slice T → I → inst.Output → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index]: forward function -/
+def core.array.Array.index
+  (T I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T) I)
+  (a : Array T N) (i : I) : Result inst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: forward function -/
+def core.array.Array.index_mut
+  (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
+  (a : Array T N) (i : I) : Result inst.indexInst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: backward function 0 -/
+def core.array.Array.index_mut_back
+  (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
+  (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
+  sorry -- TODO
+
+/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
+def core.slice.index.private_slice_index.SealedRangeUsizeInst
+  : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
+
+/- Trait implementation: [core::slice::index::Range] -/
+def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
+  core.slice.index.SliceIndex (Range Usize) (Slice T) := {
+  sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst
+  Output := Slice T
+  get := core.slice.index.RangeUsize.get T
+  get_mut := core.slice.index.RangeUsize.get_mut T
+  get_mut_back := core.slice.index.RangeUsize.get_mut_back T
+  get_unchecked := core.slice.index.RangeUsize.get_unchecked T
+  get_unchecked_mut := core.slice.index.RangeUsize.get_unchecked_mut T
+  index := core.slice.index.RangeUsize.index T
+  index_mut := core.slice.index.RangeUsize.index_mut T
+  index_mut_back := core.slice.index.RangeUsize.index_mut_back T
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.ops.index.IndexSliceTIInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (Slice T) I := {
+  Output := inst.Output
+  index := core.slice.index.Slice.index T I inst
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.ops.index.IndexMutSliceTIInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.IndexMut (Slice T) I := {
+  indexInst := core.ops.index.IndexSliceTIInst T I inst
+  index_mut := core.slice.index.Slice.index_mut T I inst
+  index_mut_back := core.slice.index.Slice.index_mut_back T I inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.ops.index.IndexArrayIInst (T I : Type) (N : Usize)
+  (inst : core.ops.index.Index (Slice T) I) :
+  core.ops.index.Index (Array T N) I := {
+  Output := inst.Output
+  index := core.array.Array.index T I N inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize)
+  (inst : core.ops.index.IndexMut (Slice T) I) :
+  core.ops.index.IndexMut (Array T N) I := {
+  indexInst := core.ops.index.IndexArrayIInst T I N inst.indexInst
+  index_mut := core.array.Array.index_mut T I N inst
+  index_mut_back := core.array.Array.index_mut_back T I N inst
+}
+
+/- [core::slice::index::usize::get]: forward function -/
+def core.slice.index.Usize.get
+  (T : Type) : Usize → Slice T → Result (Option T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: forward function -/
+def core.slice.index.Usize.get_mut
+  (T : Type) : Usize → Slice T → Result (Option T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: backward function 0 -/
+def core.slice.index.Usize.get_mut_back
+  (T : Type) : Usize → Slice T → Option T → Result (Slice T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked]: forward function -/
+def core.slice.index.Usize.get_unchecked
+  (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked_mut]: forward function -/
+def core.slice.index.Usize.get_unchecked_mut
+  (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index]: forward function -/
+def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: forward function -/
+def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T :=
+  sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: backward function 0 -/
+def core.slice.index.Usize.index_mut_back
+  (T : Type) : Usize → Slice T → T → Result (Slice T) :=
+  sorry -- TODO
+
+/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
+def core.slice.index.private_slice_index.SealedUsizeInst
+  : core.slice.index.private_slice_index.Sealed Usize := {}
+
+/- Trait implementation: [core::slice::index::usize] -/
+def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
+  core.slice.index.SliceIndex Usize (Slice T) := {
+  sealedInst := core.slice.index.private_slice_index.SealedUsizeInst
+  Output := T
+  get := core.slice.index.Usize.get T
+  get_mut := core.slice.index.Usize.get_mut T
+  get_mut_back := core.slice.index.Usize.get_mut_back T
+  get_unchecked := core.slice.index.Usize.get_unchecked T
+  get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T
+  index := core.slice.index.Usize.index T
+  index_mut := core.slice.index.Usize.index_mut T
+  index_mut_back := core.slice.index.Usize.index_mut_back T
+}
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 7c0fa3bb..7fc33251 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,11 +120,18 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
 -- MISC --
 ----------
 
-@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
-@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a := x
+@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : a := y
 
 /-- Aeneas-translated function -- useful to reduce non-recursive definitions.
  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/Range.lean b/backends/lean/Base/Primitives/Range.lean
index 26cbee42..a268bcba 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -11,7 +11,7 @@ import Base.Progress.Base
 
 namespace Primitives
 
-structure Range (α : Type u) where
+structure core.ops.range.Range (α : Type u) where
   mk ::
   start: α
   end_: α
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 55227a9f..ec9665a5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int :=
   | .Usize => Scalar.max .U32
   | _ => Scalar.max ty
 
+theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by
+  cases ty <;> simp [Scalar.min, Scalar.max]
+  . simp [Isize.min, Isize.max]
+    have h1 := Isize.refined_min.property
+    have h2 := Isize.refined_max.property
+    cases h1 <;> cases h2 <;> simp [*]
+  . simp [Usize.max]
+    have h := Usize.refined_max.property
+    cases h <;> simp [*]
+
+theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by
+  have := Scalar.min_lt_max ty
+  int_tac
+
 theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by
   cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
   have h := Isize.refined_min.property
@@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
 @[reducible] def U64   := Scalar .U64
 @[reducible] def U128  := Scalar .U128
 
+-- TODO: reducible?
+@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min
+@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max
+@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min
+@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max
+@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min
+@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max
+@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min
+@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max
+@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min
+@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max
+
+-- TODO: reducible?
+@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min
+@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
+@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min
+@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max
+@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min
+@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max
+@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min
+@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max
+@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min
+@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max
+@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min
+@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max
+
 -- TODO: below: not sure this is the best way.
 -- Should we rather overload operations like +, -, etc.?
 -- Also, it is possible to automate the generation of those definitions
@@ -861,33 +903,33 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
 
 -- ofIntCore
 -- TODO: typeclass?
-@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize
-@[reducible] def I8.ofIntCore    := @Scalar.ofIntCore .I8
-@[reducible] def I16.ofIntCore   := @Scalar.ofIntCore .I16
-@[reducible] def I32.ofIntCore   := @Scalar.ofIntCore .I32
-@[reducible] def I64.ofIntCore   := @Scalar.ofIntCore .I64
-@[reducible] def I128.ofIntCore  := @Scalar.ofIntCore .I128
-@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize
-@[reducible] def U8.ofIntCore    := @Scalar.ofIntCore .U8
-@[reducible] def U16.ofIntCore   := @Scalar.ofIntCore .U16
-@[reducible] def U32.ofIntCore   := @Scalar.ofIntCore .U32
-@[reducible] def U64.ofIntCore   := @Scalar.ofIntCore .U64
-@[reducible] def U128.ofIntCore  := @Scalar.ofIntCore .U128
+def Isize.ofIntCore := @Scalar.ofIntCore .Isize
+def I8.ofIntCore    := @Scalar.ofIntCore .I8
+def I16.ofIntCore   := @Scalar.ofIntCore .I16
+def I32.ofIntCore   := @Scalar.ofIntCore .I32
+def I64.ofIntCore   := @Scalar.ofIntCore .I64
+def I128.ofIntCore  := @Scalar.ofIntCore .I128
+def Usize.ofIntCore := @Scalar.ofIntCore .Usize
+def U8.ofIntCore    := @Scalar.ofIntCore .U8
+def U16.ofIntCore   := @Scalar.ofIntCore .U16
+def U32.ofIntCore   := @Scalar.ofIntCore .U32
+def U64.ofIntCore   := @Scalar.ofIntCore .U64
+def U128.ofIntCore  := @Scalar.ofIntCore .U128
 
 --  ofInt
 -- TODO: typeclass?
-@[reducible] def Isize.ofInt := @Scalar.ofInt .Isize
-@[reducible] def I8.ofInt    := @Scalar.ofInt .I8
-@[reducible] def I16.ofInt   := @Scalar.ofInt .I16
-@[reducible] def I32.ofInt   := @Scalar.ofInt .I32
-@[reducible] def I64.ofInt   := @Scalar.ofInt .I64
-@[reducible] def I128.ofInt  := @Scalar.ofInt .I128
-@[reducible] def Usize.ofInt := @Scalar.ofInt .Usize
-@[reducible] def U8.ofInt    := @Scalar.ofInt .U8
-@[reducible] def U16.ofInt   := @Scalar.ofInt .U16
-@[reducible] def U32.ofInt   := @Scalar.ofInt .U32
-@[reducible] def U64.ofInt   := @Scalar.ofInt .U64
-@[reducible] def U128.ofInt  := @Scalar.ofInt .U128
+abbrev Isize.ofInt := @Scalar.ofInt .Isize
+abbrev I8.ofInt    := @Scalar.ofInt .I8
+abbrev I16.ofInt   := @Scalar.ofInt .I16
+abbrev I32.ofInt   := @Scalar.ofInt .I32
+abbrev I64.ofInt   := @Scalar.ofInt .I64
+abbrev I128.ofInt  := @Scalar.ofInt .I128
+abbrev Usize.ofInt := @Scalar.ofInt .Usize
+abbrev U8.ofInt    := @Scalar.ofInt .U8
+abbrev U16.ofInt   := @Scalar.ofInt .U16
+abbrev U32.ofInt   := @Scalar.ofInt .U32
+abbrev U64.ofInt   := @Scalar.ofInt .U64
+abbrev U128.ofInt  := @Scalar.ofInt .U128
 
 postfix:max "#isize" => Isize.ofInt
 postfix:max "#i8"    => I8.ofInt
@@ -905,9 +947,46 @@ postfix:max "#u128"  => U128.ofInt
 -- Testing the notations
 example : Result Usize := 0#usize + 1#usize
 
+-- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
   simp [Scalar.ofInt, Scalar.ofIntCore]
 
+@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
 -- Comparisons
 instance {ty} : LT (Scalar ty) where
   lt a b := LT.lt a.val b.val
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index c4c4d9f2..e600a151 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
 
@@ -14,6 +14,8 @@ namespace Primitives
 
 open Result Error
 
+namespace alloc.vec
+
 def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 
 instance (a : Type u) : Arith.HasIntProp (Vec a) where
@@ -79,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
-def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
@@ -90,51 +92,83 @@ def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
  -/
 
 @[pspec]
-theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
-  (hbound : i.val < v.length) :
-  ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_shared]
-  -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp [*]
-
--- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
-  if i.val < List.length v.val then
-    .ret ()
-  else
-    .fail arrayOutOfBounds
-
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
-  match v.val.indexOpt i.val with
-  | none => fail .arrayOutOfBounds
-  | some x => ret x
-
-@[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
-  simp only [index_mut]
+  ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
-theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  ∃ nv, v.update_usize i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
-  simp only [index_mut_back]
+  simp only [update_usize]
   have h := List.indexOpt_bounds v.val i.val
   split
   . simp_all [length]; cases h <;> scalar_tac
   . simp_all
 
+/- [alloc::vec::Vec::index]: forward function -/
+def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) : Result inst.Output :=
+  sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: forward function -/
+def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) : Result inst.Output :=
+  sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: backward function 0 -/
+def Vec.index_mut_back
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (self : Vec T) (i : I) (x : inst.Output) : Result (alloc.vec.Vec T) :=
+  sorry -- TODO
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (alloc.vec.Vec T) I := {
+  Output := inst.Output
+  index := Vec.index T I inst
+}
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexMutInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.IndexMut (alloc.vec.Vec T) I := {
+  indexInst := Vec.coreopsindexIndexInst T I inst
+  index_mut := Vec.index_mut T I inst
+  index_mut_back := Vec.index_mut_back T I inst
+}
+
+@[simp]
+theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
+  Vec.index_mut_back α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i x =
+  Vec.update_usize v i x :=
+  sorry
+
+end alloc.vec
+
 end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 8b0759c5..ba63f09d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -8,6 +8,27 @@ namespace Progress
 open Lean Elab Term Meta Tactic
 open Utils
 
+-- TODO: the scalar types annoyingly often get reduced when we use the progress
+-- tactic. We should find a way of controling reduction. For now we use rewriting
+-- lemmas to make sure the goal remains clean, but this complexifies proof terms.
+-- It seems there used to be a `fold` tactic.
+theorem scalar_isize_eq : Primitives.Scalar .Isize = Primitives.Isize := by rfl
+theorem scalar_i8_eq    : Primitives.Scalar .I8 = Primitives.I8 := by rfl
+theorem scalar_i16_eq   : Primitives.Scalar .I16 = Primitives.I16 := by rfl
+theorem scalar_i32_eq   : Primitives.Scalar .I32 = Primitives.I32 := by rfl
+theorem scalar_i64_eq   : Primitives.Scalar .I64 = Primitives.I64 := by rfl
+theorem scalar_i128_eq  : Primitives.Scalar .I128 = Primitives.I128 := by rfl
+theorem scalar_usize_eq : Primitives.Scalar .Usize = Primitives.Usize := by rfl
+theorem scalar_u8_eq    : Primitives.Scalar .U8 = Primitives.U8 := by rfl
+theorem scalar_u16_eq   : Primitives.Scalar .U16 = Primitives.U16 := by rfl
+theorem scalar_u32_eq   : Primitives.Scalar .U32 = Primitives.U32 := by rfl
+theorem scalar_u64_eq   : Primitives.Scalar .U64 = Primitives.U64 := by rfl
+theorem scalar_u128_eq  : Primitives.Scalar .U128 = Primitives.U128 := by rfl
+def scalar_eqs := [
+  ``scalar_isize_eq, ``scalar_i8_eq, ``scalar_i16_eq, ``scalar_i32_eq, ``scalar_i64_eq, ``scalar_i128_eq,
+  ``scalar_usize_eq, ``scalar_u8_eq, ``scalar_u16_eq, ``scalar_u32_eq, ``scalar_u64_eq, ``scalar_u128_eq
+]
+
 inductive TheoremOrLocal where
 | Theorem (thName : Name)
 | Local (asm : LocalDecl)
@@ -111,8 +132,11 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     splitEqAndPost fun hEq hPost ids => do
     trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
     tryTac (
-      simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+      simpAt true []
+             [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
              [hEq.fvarId!] (.targets #[] true))
+    -- TODO: remove this (some types get unfolded too much: we "fold" them back)
+    tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
     -- Clear the equality, unless the user requests not to do so
     let mgoal ← do
       if keep.isSome then getMainGoal
@@ -359,6 +383,7 @@ namespace Test
   -- #eval showStoredPSpec
   -- #eval showStoredPSpecClass
   -- #eval showStoredPSpecExprClass
+  open alloc.vec
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
@@ -384,7 +409,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.index_mut_back α i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 5224e1c3..b917a789 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -604,16 +604,12 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
   rename_i x y z
   exists x + y + z
 
-/- Call the simp tactic.
-   The initialization of the context is adapted from Tactic.elabSimpArgs.
-   Something very annoying is that there is no function which allows to
-   initialize a simp context without doing an elaboration - as a consequence
-   we write our own here. -/
-def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
-  (loc : Tactic.Location) :
-  Tactic.TacticM Unit := do
-  -- Initialize with the builtin simp theorems
-  let simpThms ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+  Tactic.TacticM Simp.Context := do
+  -- Initialize either with the builtin simp theorems or with all the simp theorems
+  let simpThms ←
+    if simpOnly then Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+    else getSimpTheorems
   -- Add the equational theorem for the declarations to unfold
   let simpThms ←
     declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms
@@ -637,8 +633,63 @@ def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVar
         throwError "Not a proposition: {thmName}"
       ) simpThms
   let congrTheorems ← getSimpCongrTheorems
-  let ctx : Simp.Context := { simpTheorems := #[simpThms], congrTheorems }
+  pure { simpTheorems := #[simpThms], congrTheorems }
+
+
+inductive Location where
+  /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/
+  | wildcard
+  /-- Apply the tactic everywhere, including in the variable types (i.e., in
+      assumptions which are not propositions).  --/
+  | wildcard_dep
+  /-- Same as Tactic.Location -/
+  | targets (hypotheses : Array Syntax) (type : Bool)
+
+-- Comes from Tactic.simpLocation
+def customSimpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+  (loc : Location) : TacticM Simp.UsedSimps := do
+  match loc with
+  | Location.targets hyps simplifyTarget =>
+    withMainContext do
+      let fvarIds ← Lean.Elab.Tactic.getFVarIds hyps
+      go fvarIds simplifyTarget
+  | Location.wildcard =>
+    withMainContext do
+      go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
+  | Location.wildcard_dep =>
+    withMainContext do
+      let ctx ← Lean.MonadLCtx.getLCtx
+      let decls ← ctx.getDecls
+      let tgts := (decls.map (fun d => d.fvarId)).toArray
+      go tgts (simplifyTarget := true)
+where
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
+    let mvarId ← getMainGoal
+    let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    match result? with
+    | none => replaceMainGoal []
+    | some (_, mvarId) => replaceMainGoal [mvarId]
+    return usedSimps
+
+/- Call the simp tactic.
+   The initialization of the context is adapted from Tactic.elabSimpArgs.
+   Something very annoying is that there is no function which allows to
+   initialize a simp context without doing an elaboration - as a consequence
+   we write our own here. -/
+def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+  (loc : Location) :
+  Tactic.TacticM Unit := do
+  -- Initialize the simp context
+  let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse
+  -- Apply the simplifier
+  let _ ← customSimpLocation ctx (discharge? := .none) loc
+
+-- Call the simpAll tactic
+def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+  Tactic.TacticM Unit := do
+  -- Initialize the simp context
+  let ctx ← mkSimpCtx false declsToUnfold thms hypsToUse
   -- Apply the simplifier
-  let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
+  let _ ← Lean.Meta.simpAll (← getMainGoal) ctx
 
 end Utils