(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [loops]: function definitions *)
module Loops.Funs
open Primitives
include Loops.Types
include Loops.Clauses

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [loops::sum]: loop 0:
    Source: 'tests/src/loops.rs', lines 4:0-14:1 *)
let rec sum_loop
  (max : u32) (i : u32) (s : u32) :
  Tot (result u32) (decreases (sum_loop_decreases max i s))
  =
  if i < max
  then let* s1 = u32_add s i in let* i1 = u32_add i 1 in sum_loop max i1 s1
  else u32_mul s 2

(** [loops::sum]:
    Source: 'tests/src/loops.rs', lines 4:0-4:27 *)
let sum (max : u32) : result u32 =
  sum_loop max 0 0

(** [loops::sum_with_mut_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 19:0-31:1 *)
let rec sum_with_mut_borrows_loop
  (max : u32) (i : u32) (s : u32) :
  Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s))
  =
  if i < max
  then
    let* ms = u32_add s i in
    let* mi = u32_add i 1 in
    sum_with_mut_borrows_loop max mi ms
  else u32_mul s 2

(** [loops::sum_with_mut_borrows]:
    Source: 'tests/src/loops.rs', lines 19:0-19:44 *)
let sum_with_mut_borrows (max : u32) : result u32 =
  sum_with_mut_borrows_loop max 0 0

(** [loops::sum_with_shared_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 34:0-48:1 *)
let rec sum_with_shared_borrows_loop
  (max : u32) (i : u32) (s : u32) :
  Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s))
  =
  if i < max
  then
    let* i1 = u32_add i 1 in
    let* s1 = u32_add s i1 in
    sum_with_shared_borrows_loop max i1 s1
  else u32_mul s 2

(** [loops::sum_with_shared_borrows]:
    Source: 'tests/src/loops.rs', lines 34:0-34:47 *)
let sum_with_shared_borrows (max : u32) : result u32 =
  sum_with_shared_borrows_loop max 0 0

(** [loops::sum_array]: loop 0:
    Source: 'tests/src/loops.rs', lines 50:0-58:1 *)
let rec sum_array_loop
  (n : usize) (a : array u32 n) (i : usize) (s : u32) :
  Tot (result u32) (decreases (sum_array_loop_decreases n a i s))
  =
  if i < n
  then
    let* i1 = array_index_usize u32 n a i in
    let* s1 = u32_add s i1 in
    let* i2 = usize_add i 1 in
    sum_array_loop n a i2 s1
  else Ok s

(** [loops::sum_array]:
    Source: 'tests/src/loops.rs', lines 50:0-50:52 *)
let sum_array (n : usize) (a : array u32 n) : result u32 =
  sum_array_loop n a 0 0

(** [loops::clear]:
    Source: 'tests/src/loops.rs', lines 62:0-62:30 *)
let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) =
  admit

(** [loops::list_mem]:
    Source: 'tests/src/loops.rs', lines 76:0-76:52 *)
let list_mem (x : u32) (ls : list_t u32) : result bool =
  admit

(** [loops::list_nth_mut_loop]:
    Source: 'tests/src/loops.rs', lines 88:0-88:71 *)
let list_nth_mut_loop
  (t : Type0) (ls : list_t t) (i : u32) :
  result (t & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_shared_loop]:
    Source: 'tests/src/loops.rs', lines 101:0-101:66 *)
let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
  admit

(** [loops::get_elem_mut]:
    Source: 'tests/src/loops.rs', lines 113:0-113:73 *)
let get_elem_mut
  (slots : alloc_vec_Vec (list_t usize)) (x : usize) :
  result (usize & (usize -> result (alloc_vec_Vec (list_t usize))))
  =
  admit

(** [loops::get_elem_shared]:
    Source: 'tests/src/loops.rs', lines 129:0-129:68 *)
let get_elem_shared
  (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
  admit

(** [loops::id_mut]:
    Source: 'tests/src/loops.rs', lines 145:0-145:50 *)
let id_mut
  (t : Type0) (ls : list_t t) :
  result ((list_t t) & (list_t t -> result (list_t t)))
  =
  Ok (ls, Ok)

(** [loops::id_shared]:
    Source: 'tests/src/loops.rs', lines 149:0-149:45 *)
let id_shared (t : Type0) (ls : list_t t) : result (list_t t) =
  Ok ls

(** [loops::list_nth_mut_loop_with_id]:
    Source: 'tests/src/loops.rs', lines 154:0-154:75 *)
let list_nth_mut_loop_with_id
  (t : Type0) (ls : list_t t) (i : u32) :
  result (t & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_shared_loop_with_id]:
    Source: 'tests/src/loops.rs', lines 168:0-168:70 *)
let list_nth_shared_loop_with_id
  (t : Type0) (ls : list_t t) (i : u32) : result t =
  admit

(** [loops::list_nth_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 184:0-188:27 *)
let list_nth_mut_loop_pair
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 208:0-212:19 *)
let list_nth_shared_loop_pair
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
  admit

(** [loops::list_nth_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 233:0-237:27 *)
let list_nth_mut_loop_pair_merge
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))
  =
  admit

(** [loops::list_nth_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 251:0-255:19 *)
let list_nth_shared_loop_pair_merge
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
  admit

(** [loops::list_nth_mut_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 269:0-273:23 *)
let list_nth_mut_shared_loop_pair
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_mut_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 288:0-292:23 *)
let list_nth_mut_shared_loop_pair_merge
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_shared_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 307:0-311:23 *)
let list_nth_shared_mut_loop_pair
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & (t -> result (list_t t)))
  =
  admit

(** [loops::list_nth_shared_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 326:0-330:23 *)
let list_nth_shared_mut_loop_pair_merge
  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
  result ((t & t) & (t -> result (list_t t)))
  =
  admit

(** [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 345:0-349:1 *)
let rec ignore_input_mut_borrow_loop
  (i : u32) :
  Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
  =
  if i > 0
  then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1
  else Ok ()

(** [loops::ignore_input_mut_borrow]:
    Source: 'tests/src/loops.rs', lines 345:0-345:56 *)
let ignore_input_mut_borrow (_a : u32) (i : u32) : result u32 =
  let* _ = ignore_input_mut_borrow_loop i in Ok _a

(** [loops::incr_ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 353:0-358:1 *)
let rec incr_ignore_input_mut_borrow_loop
  (i : u32) :
  Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
  =
  if i > 0
  then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1
  else Ok ()

(** [loops::incr_ignore_input_mut_borrow]:
    Source: 'tests/src/loops.rs', lines 353:0-353:60 *)
let incr_ignore_input_mut_borrow (a : u32) (i : u32) : result u32 =
  let* a1 = u32_add a 1 in
  let* _ = incr_ignore_input_mut_borrow_loop i in
  Ok a1

(** [loops::ignore_input_shared_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 362:0-366:1 *)
let rec ignore_input_shared_borrow_loop
  (i : u32) :
  Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
  =
  if i > 0
  then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1
  else Ok ()

(** [loops::ignore_input_shared_borrow]:
    Source: 'tests/src/loops.rs', lines 362:0-362:59 *)
let ignore_input_shared_borrow (_a : u32) (i : u32) : result u32 =
  let* _ = ignore_input_shared_borrow_loop i in Ok _a