3 files changed, 139 insertions, 20 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index ae961ac2..d462715f 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -213,6 +213,7 @@ 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 .
@@ -394,13 +395,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 +412,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/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 98a696b6..9db82069 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/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/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
index 2d4a567b..6c95fd78 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/Array.lean
@@ -57,7 +57,7 @@ def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Re
  -/
 
 @[pspec]
-theorem Array.index_shared_spec {α : Type u} {n : Usize}[Inhabited α] (v: Array α n) (i: Usize)
+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]
@@ -202,32 +202,32 @@ theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α
 /- 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.
+   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 (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+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_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+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_mut_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
-  to_slice α n v
+def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+  to_slice_shared α n v
 
 @[pspec]
-theorem Array.to_mut_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, Array.to_slice α n v = ret s ∧ v.val = s.val := to_slice_spec v
+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_mut_slice_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
+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_mut_slice_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
-  ∃ na, to_mut_slice_back α n a ns = ret na ∧ na.val = ns.val
-  := by simp [to_mut_slice_back, *]
+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