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

1 files changed, 49 insertions, 2 deletions

diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 3e44ef4f..cd29ca13 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -9,9 +9,14 @@ open Loops.Types
 (** [loops::sum]: decreases clause *)
 unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
 
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_mut_borrows]: decreases clause *)
 unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+  admit ()
+
+(** [loops::sum_with_shared_borrows]: decreases clause *)
+unfold
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
@@ -19,15 +24,57 @@ unfold
 let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
   admit ()
 
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
+  =
+  admit ()
+
 (** [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 =
   admit ()
 
+(** [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) : nat =
+  admit ()
+
 (** [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 =
   admit ()
 
+(** [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) : nat =
+  admit ()
+
+(** [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) : nat =
+  admit ()
+
+(** [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) : nat =
+  admit ()
+
+(** [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) : nat =
+  admit ()
+
+(** [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) : nat =
+  admit ()
+