3 files changed, 208 insertions, 0 deletions

diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 79a9dc4e..3e44ef4f 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -9,8 +9,25 @@ 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 *)
+unfold
+let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+  admit ()
+
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
 let list_nth_mut_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_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 ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 2087f2e7..d315a4f0 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,8 +9,25 @@ 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_borrows]: decreases clause *)
+unfold
+let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+  if mi <= max then max - mi 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_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_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
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index cf05b7f2..05d1f70f 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -27,6 +27,27 @@ let rec sum_loop_fwd
 (** [loops::sum] *)
 let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
 
+(** [loops::sum_with_borrows] *)
+let rec sum_with_borrows_loop_fwd
+  (max : u32) (mi : u32) (ms : u32) :
+  Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms))
+  =
+  if mi < max
+  then
+    begin match u32_add ms mi with
+    | Fail e -> Fail e
+    | Return ms0 ->
+      begin match u32_add mi 1 with
+      | Fail e -> Fail e
+      | Return mi0 -> sum_with_borrows_loop_fwd max mi0 ms0
+      end
+    end
+  else u32_mul ms 2
+
+(** [loops::sum_with_borrows] *)
+let sum_with_borrows_fwd (max : u32) : result u32 =
+  sum_with_borrows_loop_fwd max 0 0
+
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop_fwd
   (t : Type0) (ls : list_t t) (i : u32) :
@@ -74,3 +95,156 @@ let list_nth_mut_loop_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
   list_nth_mut_loop_loop_back t ls i ret
 
+(** [loops::list_nth_mut_loop_pair] *)
+let rec list_nth_mut_loop_pair_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  =
+  begin match l with
+  | ListCons x0 tl0 ->
+    begin match l0 with
+    | ListCons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 -> list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair] *)
+let list_nth_mut_loop_pair_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_loop_pair] *)
+let rec list_nth_mut_loop_pair_loop_back'a
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  =
+  begin match l with
+  | ListCons x0 tl0 ->
+    begin match l0 with
+    | ListCons x1 tl1 ->
+      if i = 0
+      then Return (ListCons ret tl0)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 ->
+          begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
+          | Fail e -> Fail e
+          | Return l1 -> Return (ListCons x0 l1)
+          end
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair] *)
+let list_nth_mut_loop_pair_back'a
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_loop_pair] *)
+let rec list_nth_mut_loop_pair_loop_back'b
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  =
+  begin match l with
+  | ListCons x0 tl0 ->
+    begin match l0 with
+    | ListCons x1 tl1 ->
+      if i = 0
+      then Return (ListCons ret tl1)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 ->
+          begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
+          | Fail e -> Fail e
+          | Return l1 -> Return (ListCons x1 l1)
+          end
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair] *)
+let list_nth_mut_loop_pair_back'b
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let rec list_nth_mut_loop_pair_merge_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  =
+  begin match l with
+  | ListCons x0 tl0 ->
+    begin match l0 with
+    | ListCons x1 tl1 ->
+      if i = 0
+      then Return (x0, x1)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 -> list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let list_nth_mut_loop_pair_merge_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let rec list_nth_mut_loop_pair_merge_loop_back
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : (t & t)) :
+  Tot (result ((list_t t) & (list_t t)))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  =
+  begin match l with
+  | ListCons x0 tl0 ->
+    begin match l0 with
+    | ListCons x1 tl1 ->
+      if i = 0
+      then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 ->
+          begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
+            with
+          | Fail e -> Fail e
+          | Return (l1, l2) -> Return (ListCons x0 l1, ListCons x1 l2)
+          end
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_pair_merge] *)
+let list_nth_mut_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
+  result ((list_t t) & (list_t t))
+  =
+  list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+