Update the Makefile and regenerate the test files

28 files changed, 637 insertions, 63 deletions

diff --git a/Makefile b/Makefile
index 8865746d..c94544be 100644
--- a/Makefile
+++ b/Makefile
@@ -125,15 +125,13 @@ thol4-paper: SUBDIR := misc-paper
 
 trans-array: OPTIONS += -no-state
 trans-array: SUBDIR := array
-tfstar-array: OPTIONS +=
-tcoq-array: OPTIONS +=
+tfstar-array: OPTIONS += -decreases-clauses -template-clauses
+tcoq-array: OPTIONS += -use-fuel
 tlean-array: SUBDIR :=
 tlean-array: OPTIONS +=
 thol4-array: OPTIONS +=
 
 # TODO: activate the arrays for all the backends
-tcoq-array:
-	echo "Ignoring the array test for Coq"
 thol4-array:
 	echo "Ignoring the array test for HOL4"
 
@@ -144,7 +142,7 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
-trans-hashmap: OPTIONS += -no-state
+trans-hashmap: OPTIONS += -no-state -test-trans-units
 trans-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
@@ -152,7 +150,7 @@ tlean-hashmap: SUBDIR :=
 tlean-hashmap: OPTIONS +=
 thol4-hashmap: OPTIONS +=
 
-trans-hashmap_main: OPTIONS +=
+trans-hashmap_main: OPTIONS += -test-trans-units
 trans-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
@@ -177,7 +175,7 @@ tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
 
-trans-external: OPTIONS +=
+trans-external: OPTIONS += -test-trans-units
 trans-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
@@ -187,7 +185,7 @@ thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-transp-betree_main: OPTIONS += -backward-no-state-update
+transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
 transp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
@@ -239,20 +237,20 @@ transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%
-tfstar-%: OPTIONS += -backend fstar -test-trans-units
+tfstar-%: OPTIONS += -backend fstar
 tfstar-%: BACKEND_SUBDIR := fstar
 tfstar-%:
 	$(AENEAS_CMD)
 
 # "p" stands for "Polonius"
 .PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar -test-trans-units
+tfstarp-%: OPTIONS += -backend fstar
 tfstarp-%: BACKEND_SUBDIR := fstar
 tfstarp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tcoq-%
-tcoq-%: OPTIONS += -backend coq -test-trans-units
+tcoq-%: OPTIONS += -backend coq
 tcoq-%: BACKEND_SUBDIR := coq
 tcoq-%:
 	$(AENEAS_CMD)
@@ -265,7 +263,7 @@ tcoqp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tlean-%
-tlean-%: OPTIONS += -backend lean -test-trans-units
+tlean-%: OPTIONS += -backend lean
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
@@ -273,19 +271,19 @@ tlean-%:
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
 
-tleanp-%: OPTIONS += -backend lean -test-trans-units
+tleanp-%: OPTIONS += -backend lean
 tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
 .PHONY: thol4-%
-thol4-%: OPTIONS += -backend hol4 -test-trans-units
+thol4-%: OPTIONS += -backend hol4
 thol4-%: BACKEND_SUBDIR := hol4
 thol4-%:
 	$(AENEAS_CMD)
 
 .PHONY: thol4p-%
-thol4p-%: OPTIONS += -backend hol4 -test-trans-units
+thol4p-%: OPTIONS += -backend hol4
 thol4p-%: BACKEND_SUBDIR := hol4
 thol4p-%:
 	$(AENEAS_CMD)
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index d462715f..71a2d9c3 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -213,7 +213,6 @@ Proof.
   pose (scalar_max_cons_valid ty).
   lia.
 Qed.
-Print scalar_le_max_valid.
 
 Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool :=
   scalar_ge_min ty x && scalar_le_max ty x .
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 86a9d5f2..85aecfc8 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export BetreeMain_Types.
 Import BetreeMain_Types.
@@ -1190,4 +1192,7 @@ Definition betree_be_tree_lookup_back
 Definition main_fwd : result unit :=
   Return tt.
 
+(** Unit test for [betree_main::main] *)
+Check (main_fwd )%return.
+
 End BetreeMain_Funs .
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index bd49500b..ecd81b9d 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export BetreeMain_Types.
 Import BetreeMain_Types.
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index 25f280dd..c8af54cd 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module BetreeMain_Types.
 
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -394,13 +394,15 @@ 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.
 
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+  start: T;
+  end_: T;
+}.
+Arguments mk_range {_}.
 
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** Arrays *)
+Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}.
 
 Lemma le_0_usize_max : 0 <= usize_max.
 Proof.
@@ -409,6 +411,47 @@ Proof.
   lia.
 Qed.
 
+Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y.
+Proof.
+  lia.
+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).
+
+(*** 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).
+
+(*** 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_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).
+
+(*** Vectors *)
+
+Definition 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 vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
 Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
 
 Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c8630eb6..c412abcd 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export Hashmap_Types.
 Import Hashmap_Types.
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index ce6e7dab..dbde6be9 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Hashmap_Types.
 
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -394,13 +394,15 @@ 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.
 
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+  start: T;
+  end_: T;
+}.
+Arguments mk_range {_}.
 
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** Arrays *)
+Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}.
 
 Lemma le_0_usize_max : 0 <= usize_max.
 Proof.
@@ -409,6 +411,47 @@ Proof.
   lia.
 Qed.
 
+Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y.
+Proof.
+  lia.
+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).
+
+(*** 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).
+
+(*** 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_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).
+
+(*** Vectors *)
+
+Definition 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 vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
 Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
 
 Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 1b7304cc..e6095fe1 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export HashmapMain_Types.
 Import HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
index 1ad9c697..2d17cc29 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export HashmapMain_Types.
 Import HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index b92cbf3a..36aaaf25 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module HashmapMain_Types.
 
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -394,13 +394,15 @@ 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.
 
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+  start: T;
+  end_: T;
+}.
+Arguments mk_range {_}.
 
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** Arrays *)
+Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}.
 
 Lemma le_0_usize_max : 0 <= usize_max.
 Proof.
@@ -409,6 +411,47 @@ Proof.
   lia.
 Qed.
 
+Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y.
+Proof.
+  lia.
+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).
+
+(*** 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).
+
+(*** 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_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).
+
+(*** Vectors *)
+
+Definition 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 vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
 Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
 
 Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 14c05c61..710ae1d9 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Constants.
 
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index f18bbd1f..28370b2b 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
 Import External_Types.
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
index 1224f426..d2ee42d4 100644
--- a/tests/coq/misc/External_Opaque.v
+++ b/tests/coq/misc/External_Opaque.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
 Import External_Types.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index cec5b88e..1883fa6c 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module External_Types.
 
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index f17eb986..82e57576 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Loops.
 
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 470a2cde..f93254e1 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module NoNestedBorrows.
 
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 0f854f31..175a523d 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Paper.
 
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index e94b6dcb..54021bdf 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module PoloniusList.
 
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -394,13 +394,15 @@ 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.
 
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+  start: T;
+  end_: T;
+}.
+Arguments mk_range {_}.
 
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** Arrays *)
+Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}.
 
 Lemma le_0_usize_max : 0 <= usize_max.
 Proof.
@@ -409,6 +411,47 @@ Proof.
   lia.
 Qed.
 
+Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y.
+Proof.
+  lia.
+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).
+
+(*** 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).
+
+(*** 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_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).
+
+(*** Vectors *)
+
+Definition 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 vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
 Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
 
 Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 98a696b6..9db82069 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+(*** Range *)
+type range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  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 =
+  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) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+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 =
+  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) =
+  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) =
+  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) =
+  admit()
+
+let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) =
+  admit()
+
+let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) =
+  admit()
+
 (*** Vector *)
 type vec (a : Type0) = v:list a{length v <= usize_max}
 
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 98a696b6..9db82069 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+(*** Range *)
+type range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  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 =
+  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) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+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 =
+  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) =
+  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) =
+  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) =
+  admit()
+
+let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) =
+  admit()
+
+let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) =
+  admit()
+
 (*** Vector *)
 type vec (a : Type0) = v:list a{length v <= usize_max}
 
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 98a696b6..9db82069 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+(*** Range *)
+type range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  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 =
+  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) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+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 =
+  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) =
+  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) =
+  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) =
+  admit()
+
+let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) =
+  admit()
+
+let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) =
+  admit()
+
 (*** Vector *)
 type vec (a : Type0) = v:list a{length v <= usize_max}
 
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 98a696b6..9db82069 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+(*** Range *)
+type range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  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 =
+  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) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+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 =
+  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) =
+  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) =
+  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) =
+  admit()
+
+let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) =
+  admit()
+
+let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) =
+  admit()
+
 (*** Vector *)
 type vec (a : Type0) = v:list a{length v <= usize_max}
 
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 98a696b6..9db82069 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
+(*** Range *)
+type range (a : Type0) = {
+  start : a;
+  end_ : a;
+}
+
+(*** Array *)
+type array (a : Type0) (n : usize) = s:list a{length s = n}
+
+// We tried putting the normalize_term condition as a refinement on the list
+// but it didn't work. It works with the requires clause.
+let mk_array (a : Type0) (n : usize)
+  (l : list a) :
+  Pure (array a n)
+  (requires (normalize_term(FStar.List.Tot.length l) = n))
+  (ensures (fun _ -> True)) =
+  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 =
+  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) =
+  if i < length x then Return (list_update x i nx)
+  else Fail Failure
+
+(*** Slice *)
+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 =
+  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) =
+  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) =
+  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) =
+  admit()
+
+let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : 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) =
+  admit()
+
+let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : 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) =
+  admit()
+
 (*** Vector *)
 type vec (a : Type0) = v:list a{length v <= usize_max}
 
diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean
index b1365143..8a2c1045 100644
--- a/tests/lean/Array/Funs.lean
+++ b/tests/lean/Array/Funs.lean
@@ -9,24 +9,24 @@ namespace array
 /- [array::array_to_shared_slice_]: forward function -/
 def array_to_shared_slice_
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) :=
-  Array.to_slice T (Usize.ofInt 32) s
+  Array.to_slice_shared T (Usize.ofInt 32) s
 
 /- [array::array_to_mut_slice_]: forward function -/
 def array_to_mut_slice_
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) :=
-  Array.to_mut_slice T (Usize.ofInt 32) s
+  Array.to_slice_mut T (Usize.ofInt 32) s
 
 /- [array::array_to_mut_slice_]: backward function 0 -/
 def array_to_mut_slice__back
   (T : Type) (s : Array T (Usize.ofInt 32)) (ret0 : Slice T) :
   Result (Array T (Usize.ofInt 32))
   :=
-  Array.to_mut_slice_back T (Usize.ofInt 32) s ret0
+  Array.to_slice_mut_back T (Usize.ofInt 32) s ret0
 
 /- [array::array_len]: forward function -/
 def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
   do
-    let s0 ← Array.to_slice T (Usize.ofInt 32) s
+    let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s
     let i := Slice.len T s0
     Result.ret i
 
@@ -34,7 +34,7 @@ def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
 def shared_array_len
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
   do
-    let s0 ← Array.to_slice T (Usize.ofInt 32) s
+    let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s
     let i := Slice.len T s0
     Result.ret i
 
@@ -109,21 +109,22 @@ def slice_subslice_mut__back
   :=
   Slice.subslice_mut_back U32 x (Range.mk y z) ret0
 
-/- [array::array_to_slice_shared]: forward function -/
-def array_to_slice_shared
+/- [array::array_to_slice_shared_]: forward function -/
+def array_to_slice_shared_
   (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
-  Array.to_slice U32 (Usize.ofInt 32) x
+  Array.to_slice_shared U32 (Usize.ofInt 32) x
 
-/- [array::array_to_slice_mut]: forward function -/
-def array_to_slice_mut (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
-  Array.to_mut_slice U32 (Usize.ofInt 32) x
+/- [array::array_to_slice_mut_]: forward function -/
+def array_to_slice_mut_
+  (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
+  Array.to_slice_mut U32 (Usize.ofInt 32) x
 
-/- [array::array_to_slice_mut]: backward function 0 -/
-def array_to_slice_mut_back
+/- [array::array_to_slice_mut_]: backward function 0 -/
+def array_to_slice_mut__back
   (x : Array U32 (Usize.ofInt 32)) (ret0 : Slice U32) :
   Result (Array U32 (Usize.ofInt 32))
   :=
-  Array.to_mut_slice_back U32 (Usize.ofInt 32) x ret0
+  Array.to_slice_mut_back U32 (Usize.ofInt 32) x ret0
 
 /- [array::array_subslice_shared_]: forward function -/
 def array_subslice_shared_
@@ -186,17 +187,14 @@ def array_local_deep_copy (x : Array U32 (Usize.ofInt 32)) : Result Unit :=
 def f0 : Result Unit :=
   do
     let s ←
-      Array.to_mut_slice U32 (Usize.ofInt 2)
+      Array.to_slice_mut U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ])
     let s0 ← Slice.index_mut_back U32 s (Usize.ofInt 0) (U32.ofInt 1)
     let _ ←
-      Array.to_mut_slice_back U32 (Usize.ofInt 2)
+      Array.to_slice_mut_back U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) s0
     Result.ret ()
 
-/- Unit test for [array::f0] -/
-#assert (f0 == .ret ())
-
 /- [array::f1]: forward function -/
 def f1 : Result Unit :=
   do
@@ -206,9 +204,6 @@ def f1 : Result Unit :=
         (Usize.ofInt 0) (U32.ofInt 1)
     Result.ret ()
 
-/- Unit test for [array::f1] -/
-#assert (f1 == .ret ())
-
 /- [array::sum]: loop 0: forward function -/
 divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 :=
   let i0 := Slice.len U32 s
@@ -268,7 +263,7 @@ def f3 : Result U32 :=
         (Usize.ofInt 0)
     let _ ← f2 i
     let s ←
-      Array.to_slice U32 (Usize.ofInt 2)
+      Array.to_slice_shared U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ])
     let s0 ←
       f4