2 files changed, 27 insertions, 0 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v
index 6d791873..6ff3066a 100644
--- a/tests/coq/array/Array_Funs.v
+++ b/tests/coq/array/Array_Funs.v
@@ -183,6 +183,10 @@ Definition index_index_array_fwd
   array_index_shared u32 32%usize a j
 .
 
+(** [array::const_gen_ret]: forward function *)
+Definition const_gen_ret_fwd (N : usize) : result usize :=
+  Return N.
+
 (** [array::update_update_array]: forward function *)
 Definition update_update_array_fwd
   (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) :
@@ -447,6 +451,15 @@ Definition f3_fwd (n : nat) : result u32 :=
   sum2_fwd n s s0
 .
 
+(** [array::SZ] *)
+Definition sz_body : result usize := Return 32%usize.
+Definition sz_c : usize := sz_body%global.
+
+(** [array::f5]: forward function *)
+Definition f5_fwd (x : array u32 32%usize) : result u32 :=
+  array_index_shared u32 32%usize x 0%usize
+.
+
 (** [array::ite]: forward function *)
 Definition ite_fwd : result unit :=
   s <-
diff --git a/tests/coq/array/Primitives.v b/tests/coq/array/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/array/Primitives.v
+++ b/tests/coq/array/Primitives.v
@@ -394,6 +394,20 @@ 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.
 
+(** 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 *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;