Regenerate the files and fix the proofs

1 files changed, 85 insertions, 70 deletions

diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 36dea95b..8424a7cc 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -32,38 +32,38 @@ type sum_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::neg_test] *)
 let neg_test_fwd (x : i32) : result i32 =
-  begin match i32_neg x with | Fail -> Fail | Return i -> Return i end
+  begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::add_test] *)
 let add_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_add x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::subs_test] *)
 let subs_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test] *)
 let div_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_div x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test1] *)
 let div_test1_fwd (x : u32) : result u32 =
-  begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::rem_test] *)
 let rem_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::cast_test] *)
 let cast_test_fwd (x : u32) : result i32 =
   begin match scalar_cast U32 I32 x with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i -> Return i
   end
 
 (** [no_nested_borrows::test2] *)
 let test2_fwd : result unit =
-  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
+  begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -75,14 +75,14 @@ let get_max_fwd (x : u32) (y : u32) : result u32 =
 (** [no_nested_borrows::test3] *)
 let test3_fwd : result unit =
   begin match get_max_fwd 4 3 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return x ->
     begin match get_max_fwd 10 11 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return y ->
       begin match u32_add x y with
-      | Fail -> Fail
-      | Return z -> if not (z = 15) then Fail else Return ()
+      | Fail e -> Fail e
+      | Return z -> if not (z = 15) then Fail Failure else Return ()
       end
     end
   end
@@ -93,15 +93,16 @@ let _ = assert_norm (test3_fwd = Return ())
 (** [no_nested_borrows::test_neg1] *)
 let test_neg1_fwd : result unit =
   begin match i32_neg 3 with
-  | Fail -> Fail
-  | Return y -> if not (y = -3) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (y = -3) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
 
 (** [no_nested_borrows::refs_test1] *)
-let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return ()
+let refs_test1_fwd : result unit =
+  if not (1 = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 let _ = assert_norm (refs_test1_fwd = Return ())
@@ -109,11 +110,14 @@ let _ = assert_norm (refs_test1_fwd = Return ())
 (** [no_nested_borrows::refs_test2] *)
 let refs_test2_fwd : result unit =
   if not (2 = 2)
-  then Fail
+  then Fail Failure
   else
     if not (0 = 0)
-    then Fail
-    else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return ()
+    then Fail Failure
+    else
+      if not (2 = 2)
+      then Fail Failure
+      else if not (2 = 2) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
 let _ = assert_norm (refs_test2_fwd = Return ())
@@ -126,7 +130,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
 
 (** [no_nested_borrows::test_box1] *)
 let test_box1_fwd : result unit =
-  let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
+  let b = 1 in let x = b in if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1_fwd = Return ())
@@ -136,16 +140,17 @@ let copy_int_fwd (x : i32) : result i32 = Return x
 
 (** [no_nested_borrows::test_unreachable] *)
 let test_unreachable_fwd (b : bool) : result unit =
-  if b then Fail else Return ()
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_panic] *)
-let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
+let test_panic_fwd (b : bool) : result unit =
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_copy_int] *)
 let test_copy_int_fwd : result unit =
   begin match copy_int_fwd 0 with
-  | Fail -> Fail
-  | Return y -> if not (0 = y) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (0 = y) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -162,8 +167,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
 let test_is_cons_fwd : result unit =
   let l = ListNil in
   begin match is_cons_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return b -> if not b then Fail else Return ()
+  | Fail e -> Fail e
+  | Return b -> if not b then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -171,14 +176,18 @@ let _ = assert_norm (test_is_cons_fwd = Return ())
 
 (** [no_nested_borrows::split_list] *)
 let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
-  begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
+  begin match l with
+  | ListCons hd tl -> Return (hd, tl)
+  | ListNil -> Fail Failure
+  end
 
 (** [no_nested_borrows::test_split_list] *)
 let test_split_list_fwd : result unit =
   let l = ListNil in
   begin match split_list_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return p ->
+    let (hd, _) = p in if not (hd = 0) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -196,18 +205,20 @@ let choose_back
 (** [no_nested_borrows::choose_test] *)
 let choose_test_fwd : result unit =
   begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return z ->
     begin match i32_add z 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return z0 ->
       if not (z0 = 1)
-      then Fail
+      then Fail Failure
       else
         begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+          if not (x = 1)
+          then Fail Failure
+          else if not (y = 0) then Fail Failure else Return ()
         end
     end
   end
@@ -233,9 +244,12 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   begin match l with
   | ListCons x l1 ->
     begin match list_length_fwd t l1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match u32_add 1 i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | ListNil -> Return 0
   end
@@ -248,14 +262,14 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_shared_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -266,14 +280,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -285,14 +299,14 @@ let rec list_nth_mut_back
     then Return (ListCons ret tl)
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_rev_aux] *)
@@ -301,7 +315,7 @@ let rec list_rev_aux_fwd
   begin match li with
   | ListCons hd tl ->
     begin match list_rev_aux_fwd t tl (ListCons hd lo) with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return l -> Return l
     end
   | ListNil -> Return lo
@@ -311,7 +325,7 @@ let rec list_rev_aux_fwd
 let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
   let li = mem_replace_fwd (list_t t) l ListNil in
   begin match list_rev_aux_fwd t li ListNil with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return l0 -> Return l0
   end
 
@@ -321,48 +335,48 @@ let test_list_functions_fwd : result unit =
   let l0 = ListCons 2 l in
   let l1 = ListCons 1 l0 in
   begin match list_length_fwd i32 (ListCons 0 l1) with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i ->
     if not (i = 3)
-    then Fail
+    then Fail Failure
     else
       begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         if not (i0 = 0)
-        then Fail
+        then Fail Failure
         else
           begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i1 ->
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return i2 ->
                 if not (i2 = 2)
-                then Fail
+                then Fail Failure
                 else
                   begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return ls ->
                     begin match list_nth_shared_fwd i32 ls 0 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return i3 ->
                       if not (i3 = 0)
-                      then Fail
+                      then Fail Failure
                       else
                         begin match list_nth_shared_fwd i32 ls 1 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return i4 ->
                           if not (i4 = 3)
-                          then Fail
+                          then Fail Failure
                           else
                             begin match list_nth_shared_fwd i32 ls 2 with
-                            | Fail -> Fail
+                            | Fail e -> Fail e
                             | Return i5 ->
-                              if not (i5 = 2) then Fail else Return ()
+                              if not (i5 = 2) then Fail Failure else Return ()
                             end
                         end
                     end
@@ -449,31 +463,31 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =
   begin match new_tuple1_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return swt ->
     let (i, _) = swt.struct_with_tuple_p in
     if not (i = 1)
-    then Fail
+    then Fail Failure
     else
       begin match new_tuple2_fwd with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return swt0 ->
         let (i0, _) = swt0.struct_with_tuple_p in
         if not (i0 = 1)
-        then Fail
+        then Fail Failure
         else
           begin match new_tuple3_fwd with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return swt1 ->
             let (i1, _) = swt1.struct_with_tuple_p in
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match new_pair1_fwd with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return swp ->
                 if not (swp.struct_with_pair_p.pair_x = 1)
-                then Fail
+                then Fail Failure
                 else Return ()
               end
           end
@@ -491,7 +505,8 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
 
 (** [no_nested_borrows::test_mem_replace] *)
 let test_mem_replace_fwd_back (px : u32) : result u32 =
-  let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
+  let y = mem_replace_fwd u32 px 1 in
+  if not (y = 0) then Fail Failure else Return 2
 
 (** [no_nested_borrows::test_shared_borrow_bool1] *)
 let test_shared_borrow_bool1_fwd (b : bool) : result u32 =