Merge branch 'main' into unsigned-max

1 files changed, 48 insertions, 48 deletions

diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 0eafeebb..05e77046 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -8,7 +8,7 @@ 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 *)
+    Source: 'tests/src/loops.rs', lines 8:0-18:1 *)
 let rec sum_loop
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (sum_loop_decreases max i s))
@@ -18,12 +18,12 @@ let rec sum_loop
   else u32_mul s 2
 
 (** [loops::sum]:
-    Source: 'tests/src/loops.rs', lines 4:0-4:27 *)
+    Source: 'tests/src/loops.rs', lines 8:0-8: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 *)
+    Source: 'tests/src/loops.rs', lines 23:0-35: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))
@@ -36,12 +36,12 @@ let rec sum_with_mut_borrows_loop
   else u32_mul s 2
 
 (** [loops::sum_with_mut_borrows]:
-    Source: 'tests/src/loops.rs', lines 19:0-19:44 *)
+    Source: 'tests/src/loops.rs', lines 23:0-23: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 *)
+    Source: 'tests/src/loops.rs', lines 38:0-52: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))
@@ -54,12 +54,12 @@ let rec sum_with_shared_borrows_loop
   else u32_mul s 2
 
 (** [loops::sum_with_shared_borrows]:
-    Source: 'tests/src/loops.rs', lines 34:0-34:47 *)
+    Source: 'tests/src/loops.rs', lines 38:0-38: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 *)
+    Source: 'tests/src/loops.rs', lines 54:0-62: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))
@@ -73,12 +73,12 @@ let rec sum_array_loop
   else Ok s
 
 (** [loops::sum_array]:
-    Source: 'tests/src/loops.rs', lines 50:0-50:52 *)
+    Source: 'tests/src/loops.rs', lines 54:0-54:52 *)
 let sum_array (n : usize) (a : array u32 n) : result u32 =
   sum_array_loop n a 0 0
 
 (** [loops::clear]: loop 0:
-    Source: 'tests/src/loops.rs', lines 62:0-68:1 *)
+    Source: 'tests/src/loops.rs', lines 66:0-72:1 *)
 let rec clear_loop
   (v : alloc_vec_Vec u32) (i : usize) :
   Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i))
@@ -95,12 +95,12 @@ let rec clear_loop
   else Ok v
 
 (** [loops::clear]:
-    Source: 'tests/src/loops.rs', lines 62:0-62:30 *)
+    Source: 'tests/src/loops.rs', lines 66:0-66:30 *)
 let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) =
   clear_loop v 0
 
 (** [loops::list_mem]: loop 0:
-    Source: 'tests/src/loops.rs', lines 76:0-85:1 *)
+    Source: 'tests/src/loops.rs', lines 80:0-89:1 *)
 let rec list_mem_loop
   (x : u32) (ls : list_t u32) :
   Tot (result bool) (decreases (list_mem_loop_decreases x ls))
@@ -111,12 +111,12 @@ let rec list_mem_loop
   end
 
 (** [loops::list_mem]:
-    Source: 'tests/src/loops.rs', lines 76:0-76:52 *)
+    Source: 'tests/src/loops.rs', lines 80:0-80:52 *)
 let list_mem (x : u32) (ls : list_t u32) : result bool =
   list_mem_loop x ls
 
 (** [loops::list_nth_mut_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 88:0-98:1 *)
+    Source: 'tests/src/loops.rs', lines 92:0-102:1 *)
 let rec list_nth_mut_loop_loop
   (t : Type0) (ls : list_t t) (i : u32) :
   Tot (result (t & (t -> result (list_t t))))
@@ -135,7 +135,7 @@ let rec list_nth_mut_loop_loop
   end
 
 (** [loops::list_nth_mut_loop]:
-    Source: 'tests/src/loops.rs', lines 88:0-88:71 *)
+    Source: 'tests/src/loops.rs', lines 92:0-92:71 *)
 let list_nth_mut_loop
   (t : Type0) (ls : list_t t) (i : u32) :
   result (t & (t -> result (list_t t)))
@@ -143,7 +143,7 @@ let list_nth_mut_loop
   list_nth_mut_loop_loop t ls i
 
 (** [loops::list_nth_shared_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 101:0-111:1 *)
+    Source: 'tests/src/loops.rs', lines 105:0-115:1 *)
 let rec list_nth_shared_loop_loop
   (t : Type0) (ls : list_t t) (i : u32) :
   Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i))
@@ -157,12 +157,12 @@ let rec list_nth_shared_loop_loop
   end
 
 (** [loops::list_nth_shared_loop]:
-    Source: 'tests/src/loops.rs', lines 101:0-101:66 *)
+    Source: 'tests/src/loops.rs', lines 105:0-105:66 *)
 let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t =
   list_nth_shared_loop_loop t ls i
 
 (** [loops::get_elem_mut]: loop 0:
-    Source: 'tests/src/loops.rs', lines 113:0-127:1 *)
+    Source: 'tests/src/loops.rs', lines 117:0-131:1 *)
 let rec get_elem_mut_loop
   (x : usize) (ls : list_t usize) :
   Tot (result (usize & (usize -> result (list_t usize))))
@@ -180,7 +180,7 @@ let rec get_elem_mut_loop
   end
 
 (** [loops::get_elem_mut]:
-    Source: 'tests/src/loops.rs', lines 113:0-113:73 *)
+    Source: 'tests/src/loops.rs', lines 117:0-117:73 *)
 let get_elem_mut
   (slots : alloc_vec_Vec (list_t usize)) (x : usize) :
   result (usize & (usize -> result (alloc_vec_Vec (list_t usize))))
@@ -193,7 +193,7 @@ let get_elem_mut
   Ok (i, back1)
 
 (** [loops::get_elem_shared]: loop 0:
-    Source: 'tests/src/loops.rs', lines 129:0-143:1 *)
+    Source: 'tests/src/loops.rs', lines 133:0-147:1 *)
 let rec get_elem_shared_loop
   (x : usize) (ls : list_t usize) :
   Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls))
@@ -204,7 +204,7 @@ let rec get_elem_shared_loop
   end
 
 (** [loops::get_elem_shared]:
-    Source: 'tests/src/loops.rs', lines 129:0-129:68 *)
+    Source: 'tests/src/loops.rs', lines 133:0-133:68 *)
 let get_elem_shared
   (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
   let* ls =
@@ -213,7 +213,7 @@ let get_elem_shared
   get_elem_shared_loop x ls
 
 (** [loops::id_mut]:
-    Source: 'tests/src/loops.rs', lines 145:0-145:50 *)
+    Source: 'tests/src/loops.rs', lines 149:0-149:50 *)
 let id_mut
   (t : Type0) (ls : list_t t) :
   result ((list_t t) & (list_t t -> result (list_t t)))
@@ -221,12 +221,12 @@ let id_mut
   Ok (ls, Ok)
 
 (** [loops::id_shared]:
-    Source: 'tests/src/loops.rs', lines 149:0-149:45 *)
+    Source: 'tests/src/loops.rs', lines 153:0-153:45 *)
 let id_shared (t : Type0) (ls : list_t t) : result (list_t t) =
   Ok ls
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 154:0-165:1 *)
+    Source: 'tests/src/loops.rs', lines 158:0-169:1 *)
 let rec list_nth_mut_loop_with_id_loop
   (t : Type0) (i : u32) (ls : list_t t) :
   Tot (result (t & (t -> result (list_t t))))
@@ -245,7 +245,7 @@ let rec list_nth_mut_loop_with_id_loop
   end
 
 (** [loops::list_nth_mut_loop_with_id]:
-    Source: 'tests/src/loops.rs', lines 154:0-154:75 *)
+    Source: 'tests/src/loops.rs', lines 158:0-158:75 *)
 let list_nth_mut_loop_with_id
   (t : Type0) (ls : list_t t) (i : u32) :
   result (t & (t -> result (list_t t)))
@@ -256,7 +256,7 @@ let list_nth_mut_loop_with_id
   Ok (x, back1)
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 168:0-179:1 *)
+    Source: 'tests/src/loops.rs', lines 172:0-183:1 *)
 let rec list_nth_shared_loop_with_id_loop
   (t : Type0) (i : u32) (ls : list_t t) :
   Tot (result t)
@@ -271,13 +271,13 @@ let rec list_nth_shared_loop_with_id_loop
   end
 
 (** [loops::list_nth_shared_loop_with_id]:
-    Source: 'tests/src/loops.rs', lines 168:0-168:70 *)
+    Source: 'tests/src/loops.rs', lines 172:0-172:70 *)
 let list_nth_shared_loop_with_id
   (t : Type0) (ls : list_t t) (i : u32) : result t =
   let* ls1 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls1
 
 (** [loops::list_nth_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 184:0-205:1 *)
+    Source: 'tests/src/loops.rs', lines 188:0-209:1 *)
 let rec list_nth_mut_loop_pair_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))))
@@ -306,7 +306,7 @@ let rec list_nth_mut_loop_pair_loop
   end
 
 (** [loops::list_nth_mut_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 184:0-188:27 *)
+    Source: 'tests/src/loops.rs', lines 188:0-192: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)))
@@ -314,7 +314,7 @@ let list_nth_mut_loop_pair
   list_nth_mut_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 208:0-229:1 *)
+    Source: 'tests/src/loops.rs', lines 212:0-233:1 *)
 let rec list_nth_shared_loop_pair_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
@@ -333,13 +333,13 @@ let rec list_nth_shared_loop_pair_loop
   end
 
 (** [loops::list_nth_shared_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 208:0-212:19 *)
+    Source: 'tests/src/loops.rs', lines 212:0-216:19 *)
 let list_nth_shared_loop_pair
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
   list_nth_shared_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 233:0-248:1 *)
+    Source: 'tests/src/loops.rs', lines 237:0-252:1 *)
 let rec list_nth_mut_loop_pair_merge_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))))
@@ -369,7 +369,7 @@ let rec list_nth_mut_loop_pair_merge_loop
   end
 
 (** [loops::list_nth_mut_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 233:0-237:27 *)
+    Source: 'tests/src/loops.rs', lines 237:0-241: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))))
@@ -377,7 +377,7 @@ let list_nth_mut_loop_pair_merge
   list_nth_mut_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 251:0-266:1 *)
+    Source: 'tests/src/loops.rs', lines 255:0-270:1 *)
 let rec list_nth_shared_loop_pair_merge_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
@@ -398,13 +398,13 @@ let rec list_nth_shared_loop_pair_merge_loop
   end
 
 (** [loops::list_nth_shared_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 251:0-255:19 *)
+    Source: 'tests/src/loops.rs', lines 255:0-259:19 *)
 let list_nth_shared_loop_pair_merge
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
   list_nth_shared_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 269:0-284:1 *)
+    Source: 'tests/src/loops.rs', lines 273:0-288:1 *)
 let rec list_nth_mut_shared_loop_pair_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -428,7 +428,7 @@ let rec list_nth_mut_shared_loop_pair_loop
   end
 
 (** [loops::list_nth_mut_shared_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 269:0-273:23 *)
+    Source: 'tests/src/loops.rs', lines 273:0-277: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)))
@@ -436,7 +436,7 @@ let list_nth_mut_shared_loop_pair
   list_nth_mut_shared_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 288:0-303:1 *)
+    Source: 'tests/src/loops.rs', lines 292:0-307:1 *)
 let rec list_nth_mut_shared_loop_pair_merge_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -461,7 +461,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
   end
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 288:0-292:23 *)
+    Source: 'tests/src/loops.rs', lines 292:0-296: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)))
@@ -469,7 +469,7 @@ let list_nth_mut_shared_loop_pair_merge
   list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 307:0-322:1 *)
+    Source: 'tests/src/loops.rs', lines 311:0-326:1 *)
 let rec list_nth_shared_mut_loop_pair_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -493,7 +493,7 @@ let rec list_nth_shared_mut_loop_pair_loop
   end
 
 (** [loops::list_nth_shared_mut_loop_pair]:
-    Source: 'tests/src/loops.rs', lines 307:0-311:23 *)
+    Source: 'tests/src/loops.rs', lines 311:0-315: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)))
@@ -501,7 +501,7 @@ let list_nth_shared_mut_loop_pair
   list_nth_shared_mut_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 326:0-341:1 *)
+    Source: 'tests/src/loops.rs', lines 330:0-345:1 *)
 let rec list_nth_shared_mut_loop_pair_merge_loop
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -526,7 +526,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
   end
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]:
-    Source: 'tests/src/loops.rs', lines 326:0-330:23 *)
+    Source: 'tests/src/loops.rs', lines 330:0-334: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)))
@@ -534,7 +534,7 @@ let list_nth_shared_mut_loop_pair_merge
   list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 345:0-349:1 *)
+    Source: 'tests/src/loops.rs', lines 349:0-353:1 *)
 let rec ignore_input_mut_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
@@ -544,12 +544,12 @@ let rec ignore_input_mut_borrow_loop
   else Ok ()
 
 (** [loops::ignore_input_mut_borrow]:
-    Source: 'tests/src/loops.rs', lines 345:0-345:56 *)
+    Source: 'tests/src/loops.rs', lines 349:0-349: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 *)
+    Source: 'tests/src/loops.rs', lines 357:0-362:1 *)
 let rec incr_ignore_input_mut_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
@@ -559,14 +559,14 @@ let rec incr_ignore_input_mut_borrow_loop
   else Ok ()
 
 (** [loops::incr_ignore_input_mut_borrow]:
-    Source: 'tests/src/loops.rs', lines 353:0-353:60 *)
+    Source: 'tests/src/loops.rs', lines 357:0-357: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 *)
+    Source: 'tests/src/loops.rs', lines 366:0-370:1 *)
 let rec ignore_input_shared_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
@@ -576,7 +576,7 @@ let rec ignore_input_shared_borrow_loop
   else Ok ()
 
 (** [loops::ignore_input_shared_borrow]:
-    Source: 'tests/src/loops.rs', lines 362:0-362:59 *)
+    Source: 'tests/src/loops.rs', lines 366:0-366:59 *)
 let ignore_input_shared_borrow (_a : u32) (i : u32) : result u32 =
   let* _ = ignore_input_shared_borrow_loop i in Ok _a