1 files changed, 65 insertions, 3 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index b7bef7c7..35dea58c 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -375,15 +375,58 @@ Definition non_copyable_array : result unit :=
   take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ])
 .
 
+(** [arrays::sum]: loop 0:
+    Source: 'tests/src/arrays.rs', lines 242:0-250:1 *)
+Fixpoint sum_loop
+  (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    let i1 := slice_len u32 s in
+    if i s< i1
+    then (
+      i2 <- slice_index_usize u32 s i;
+      sum3 <- u32_add sum1 i2;
+      i3 <- usize_add i 1%usize;
+      sum_loop n1 s sum3 i3)
+    else Ok sum1
+  end
+.
+
 (** [arrays::sum]:
     Source: 'tests/src/arrays.rs', lines 242:0-242:28 *)
 Definition sum (n : nat) (s : slice u32) : result u32 :=
-  admit.
+  sum_loop n s 0%u32 0%usize
+.
+
+(** [arrays::sum2]: loop 0:
+    Source: 'tests/src/arrays.rs', lines 252:0-261:1 *)
+Fixpoint sum2_loop
+  (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
+  result u32
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    let i1 := slice_len u32 s in
+    if i s< i1
+    then (
+      i2 <- slice_index_usize u32 s i;
+      i3 <- slice_index_usize u32 s2 i;
+      i4 <- u32_add i2 i3;
+      sum3 <- u32_add sum1 i4;
+      i5 <- usize_add i 1%usize;
+      sum2_loop n1 s s2 sum3 i5)
+    else Ok sum1
+  end
+.
 
 (** [arrays::sum2]:
     Source: 'tests/src/arrays.rs', lines 252:0-252:41 *)
 Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
-  admit
+  let i := slice_len u32 s in
+  let i1 := slice_len u32 s2 in
+  if negb (i s= i1) then Fail_ Failure else sum2_loop n s s2 0%u32 0%usize
 .
 
 (** [arrays::f0]:
@@ -464,10 +507,29 @@ Definition ite : result unit :=
   Ok tt
 .
 
+(** [arrays::zero_slice]: loop 0:
+    Source: 'tests/src/arrays.rs', lines 303:0-310:1 *)
+Fixpoint zero_slice_loop
+  (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if i s< len
+    then (
+      p <- slice_index_mut_usize u8 a i;
+      let (_, index_mut_back) := p in
+      i1 <- usize_add i 1%usize;
+      a1 <- index_mut_back 0%u8;
+      zero_slice_loop n1 a1 i1 len)
+    else Ok a
+  end
+.
+
 (** [arrays::zero_slice]:
     Source: 'tests/src/arrays.rs', lines 303:0-303:31 *)
 Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  admit.
+  let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+.
 
 (** [arrays::iter_mut_slice]: loop 0:
     Source: 'tests/src/arrays.rs', lines 312:0-318:1 *)