Implement support for nested borrows in loops, and add loop tests

1 files changed, 48 insertions, 3 deletions

diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index d315a4f0..9cf5db1f 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,25 +9,70 @@ open Loops.Types
 unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
   if i <= max then max - i else 0
 
+(** [loops::sum_with_mut_borrows]: decreases clause *)
+unfold
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+  if max >= mi then max - mi else 0
 
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_shared_borrows]: decreases clause *)
 unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
-  if mi <= max then max - mi else 0
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+  if max >= i then max - i else 0
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
 let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
   i
 
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
+  ls
+
 (** [loops::list_nth_mut_loop_pair]: decreases clause *)
 unfold
 let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
   (i : u32) : nat =
   i
 
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l
+
 (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
 unfold
 let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : nat =
   i
+
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+  (l0 : list_t t) (i : u32) : list_t t =
+  l