Update the failing proofs

2 files changed, 17 insertions, 25 deletions

diff --git a/tests/fstar/array/Array.Opaque.fsti b/tests/fstar/array/Array.Opaque.fsti
deleted file mode 100644
index 484cb9ee..00000000
--- a/tests/fstar/array/Array.Opaque.fsti
+++ /dev/null
@@ -1,24 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [array]: external function declarations *)
-module Array.Opaque
-open Primitives
-include Array.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::array::[T; N]::{15}::index]: forward function *)
-val core_array_[T; N]_index_fwd
-  (t i : Type0) (n : usize) (inst : core_ops_index_Index (slice t) i) :
-  array t n -> i -> result inst.core_ops_index_Index_Output
-
-(** [core::array::[T; N]::{16}::index_mut]: forward function *)
-val core_array_[T; N]_index_mut_fwd
-  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
-  array t n -> i -> result inst.index_inst.core_ops_index_Index_Output
-
-(** [core::array::[T; N]::{16}::index_mut]: backward function 0 *)
-val core_array_[T; N]_index_mut_back
-  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
-  array t n -> i -> inst.index_inst.core_ops_index_Index_Output -> result
-    (array t n)
-
diff --git a/tests/fstar/array/Primitives.fst b/tests/fstar/array/Primitives.fst
index 71d75c11..3297803c 100644
--- a/tests/fstar/array/Primitives.fst
+++ b/tests/fstar/array/Primitives.fst
@@ -427,7 +427,7 @@ let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a []
 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) (x : a) : result a =
+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) =
@@ -704,6 +704,22 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
 
 (*** 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_usize_coresliceindexSliceIndexInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst 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_usize_coresliceindexSliceIndexInst a) v i ==
+      alloc_vec_Vec_index_usize v i)
+  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst 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_usize_coresliceindexSliceIndexInst a) v i x ==