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

4 files changed, 820 insertions, 18 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 67ee0880..4fc68e1c 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -22,8 +22,8 @@ Definition sum_fwd (n : nat) (max : u32) : result u32 :=
   sum_loop_fwd n max (0%u32) (0%u32)
 .
 
-(** [loops::sum_with_borrows] *)
-Fixpoint sum_with_borrows_loop_fwd
+(** [loops::sum_with_mut_borrows] *)
+Fixpoint sum_with_mut_borrows_loop_fwd
   (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -32,14 +32,34 @@ Fixpoint sum_with_borrows_loop_fwd
     then (
       ms0 <- u32_add ms mi;
       mi0 <- u32_add mi 1%u32;
-      sum_with_borrows_loop_fwd n0 max mi0 ms0)
+      sum_with_mut_borrows_loop_fwd n0 max mi0 ms0)
     else u32_mul ms 2%u32
   end
 .
 
-(** [loops::sum_with_borrows] *)
-Definition sum_with_borrows_fwd (n : nat) (max : u32) : result u32 :=
-  sum_with_borrows_loop_fwd n max (0%u32) (0%u32)
+(** [loops::sum_with_mut_borrows] *)
+Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 :=
+  sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32)
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Fixpoint sum_with_shared_borrows_loop_fwd
+  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    if i s< max
+    then (
+      i0 <- u32_add i 1%u32;
+      s0 <- u32_add s i0;
+      sum_with_shared_borrows_loop_fwd n0 max i0 s0)
+    else u32_mul s 2%u32
+  end
+.
+
+(** [loops::sum_with_shared_borrows] *)
+Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
+  sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32)
 .
 
 (** [loops::List] *)
@@ -102,6 +122,28 @@ Definition list_nth_mut_loop_back
   list_nth_mut_loop_loop_back T n ls i ret
 .
 
+(** [loops::list_nth_shared_loop] *)
+Fixpoint list_nth_shared_loop_loop_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (i0 <- u32_sub i 1%u32; list_nth_shared_loop_loop_fwd T n0 tl i0)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_loop] *)
+Definition list_nth_shared_loop_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  list_nth_shared_loop_loop_fwd T n ls i
+.
+
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_fwd
   (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
@@ -200,6 +242,38 @@ Definition list_nth_mut_loop_pair_back'b
   list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret
 .
 
+(** [loops::list_nth_shared_loop_pair] *)
+Fixpoint list_nth_shared_loop_pair_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_loop_pair] *)
+Definition list_nth_shared_loop_pair_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
 (** [loops::list_nth_mut_loop_pair_merge] *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
   (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
@@ -268,4 +342,298 @@ Definition list_nth_mut_loop_pair_merge_back
   list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+Definition list_nth_shared_loop_pair_merge_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_mut_shared_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Fixpoint list_nth_mut_shared_loop_pair_loop_back
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (ListCons ret tl0)
+        else (
+          i0 <- u32_sub i 1%u32;
+          l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l1))
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+Definition list_nth_mut_shared_loop_pair_back
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_mut_shared_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (ListCons ret tl0)
+        else (
+          i0 <- u32_sub i 1%u32;
+          l1 <-
+            list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l1))
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+Definition list_nth_mut_shared_loop_pair_merge_back
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_shared_mut_loop_pair_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Fixpoint list_nth_shared_mut_loop_pair_loop_back
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (ListCons ret tl1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l1))
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+Definition list_nth_shared_mut_loop_pair_back
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (x0, x1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          list_nth_shared_mut_loop_pair_merge_loop_fwd T n0 tl0 tl1 i0)
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_fwd
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
+  result (T * T)
+  :=
+  list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
+  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match l with
+    | ListCons x0 tl0 =>
+      match l0 with
+      | ListCons x1 tl1 =>
+        if i s= 0%u32
+        then Return (ListCons ret tl1)
+        else (
+          i0 <- u32_sub i 1%u32;
+          l1 <-
+            list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l1))
+      | ListNil => Fail_ Failure
+      end
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+Definition list_nth_shared_mut_loop_pair_merge_back
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
+.
+
 End Loops .
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 ()
+
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
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 05d1f70f..ee8e95d2 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -27,10 +27,10 @@ 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
+(** [loops::sum_with_mut_borrows] *)
+let rec sum_with_mut_borrows_loop_fwd
   (max : u32) (mi : u32) (ms : u32) :
-  Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms))
+  Tot (result u32) (decreases (sum_with_mut_borrows_decreases max mi ms))
   =
   if mi < max
   then
@@ -39,14 +39,35 @@ let rec sum_with_borrows_loop_fwd
     | Return ms0 ->
       begin match u32_add mi 1 with
       | Fail e -> Fail e
-      | Return mi0 -> sum_with_borrows_loop_fwd max mi0 ms0
+      | Return mi0 -> sum_with_mut_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::sum_with_mut_borrows] *)
+let sum_with_mut_borrows_fwd (max : u32) : result u32 =
+  sum_with_mut_borrows_loop_fwd max 0 0
+
+(** [loops::sum_with_shared_borrows] *)
+let rec sum_with_shared_borrows_loop_fwd
+  (max : u32) (i : u32) (s : u32) :
+  Tot (result u32) (decreases (sum_with_shared_borrows_decreases max i s))
+  =
+  if i < max
+  then
+    begin match u32_add i 1 with
+    | Fail e -> Fail e
+    | Return i0 ->
+      begin match u32_add s i0 with
+      | Fail e -> Fail e
+      | Return s0 -> sum_with_shared_borrows_loop_fwd max i0 s0
+      end
+    end
+  else u32_mul s 2
+
+(** [loops::sum_with_shared_borrows] *)
+let sum_with_shared_borrows_fwd (max : u32) : result u32 =
+  sum_with_shared_borrows_loop_fwd max 0 0
 
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop_fwd
@@ -95,6 +116,27 @@ 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_shared_loop] *)
+let rec list_nth_shared_loop_loop_fwd
+  (t : Type0) (ls : list_t t) (i : u32) :
+  Tot (result t) (decreases (list_nth_shared_loop_decreases t ls i))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return x
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 -> list_nth_shared_loop_loop_fwd t tl i0
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop] *)
+let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
+  list_nth_shared_loop_loop_fwd t ls i
+
 (** [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) :
@@ -187,6 +229,33 @@ let list_nth_mut_loop_pair_back'b
   =
   list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
 
+(** [loops::list_nth_shared_loop_pair] *)
+let rec list_nth_shared_loop_pair_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_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_shared_loop_pair_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_pair] *)
+let list_nth_shared_loop_pair_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_loop_pair_loop_fwd t ls0 ls1 i
+
 (** [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) :
@@ -248,3 +317,276 @@ let list_nth_mut_loop_pair_merge_back
   =
   list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
 
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let rec list_nth_shared_loop_pair_merge_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_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_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let list_nth_shared_loop_pair_merge_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_shared_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_shared_loop_pair_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_shared_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_back
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_shared_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_shared_loop_pair_loop_back 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_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_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_shared_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_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_mut_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_back
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_shared_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 (ListCons ret tl0)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 ->
+          begin match
+            list_nth_mut_shared_loop_pair_merge_loop_back 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_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_fwd
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_shared_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_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_mut_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_back
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_shared_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_shared_mut_loop_pair_loop_back 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_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_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_shared_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_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
+        end
+    | ListNil -> Fail Failure
+    end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_fwd
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+  list_nth_shared_mut_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_back
+  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_shared_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 (ListCons ret tl1)
+      else
+        begin match u32_sub i 1 with
+        | Fail e -> Fail e
+        | Return i0 ->
+          begin match
+            list_nth_shared_mut_loop_pair_merge_loop_back 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_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_back
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+  result (list_t t)
+  =
+  list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+