Regenerate the tests

tests/coq/arrays/Arrays.v

@@ -428,7 +428,8 @@ Fixpoint sum2_loop
 Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
   let i := slice_len s in
   let i1 := slice_len s2 in
-  if i s= i1 then sum2_loop n s s2 0%u32 0%usize else Fail_ Failure
+  _ <- massert (i s= i1);
+  sum2_loop n s s2 0%u32 0%usize
 .
 
 (** [arrays::f0]:

tests/coq/hashmap/Hashmap_Funs.v

@@ -543,35 +543,25 @@ Definition test1 (n : nat) : result unit :=
   hm3 <- hashMap_insert n hm2 1024%usize 138%u64;
   hm4 <- hashMap_insert n hm3 1056%usize 256%u64;
   i <- hashMap_get n hm4 128%usize;
-  if i s= 18%u64
-  then (
-    p <- hashMap_get_mut n hm4 1024%usize;
-    let (_, get_mut_back) := p in
-    let hm5 := get_mut_back 56%u64 in
-    i1 <- hashMap_get n hm5 1024%usize;
-    if i1 s= 56%u64
-    then (
-      p1 <- hashMap_remove n hm5 1024%usize;
-      let (x, hm6) := p1 in
-      match x with
-      | None => Fail_ Failure
-      | Some x1 =>
-        if x1 s= 56%u64
-        then (
-          i2 <- hashMap_get n hm6 0%usize;
-          if i2 s= 42%u64
-          then (
-            i3 <- hashMap_get n hm6 128%usize;
-            if i3 s= 18%u64
-            then (
-              i4 <- hashMap_get n hm6 1056%usize;
-              if i4 s= 256%u64 then Ok tt else Fail_ Failure)
-            else Fail_ Failure)
-          else Fail_ Failure)
-        else Fail_ Failure
-      end)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 18%u64);
+  p <- hashMap_get_mut n hm4 1024%usize;
+  let (_, get_mut_back) := p in
+  let hm5 := get_mut_back 56%u64 in
+  i1 <- hashMap_get n hm5 1024%usize;
+  _ <- massert (i1 s= 56%u64);
+  p1 <- hashMap_remove n hm5 1024%usize;
+  let (x, hm6) := p1 in
+  match x with
+  | None => Fail_ Failure
+  | Some x1 =>
+    _ <- massert (x1 s= 56%u64);
+    i2 <- hashMap_get n hm6 0%usize;
+    _ <- massert (i2 s= 42%u64);
+    i3 <- hashMap_get n hm6 128%usize;
+    _ <- massert (i3 s= 18%u64);
+    i4 <- hashMap_get n hm6 1056%usize;
+    massert (i4 s= 256%u64)
+  end
 .
 
 End Hashmap_Funs.

tests/coq/misc/AdtBorrows.v

@@ -31,7 +31,7 @@ Definition sharedWrapper_unwrap
 Definition use_shared_wrapper : result unit :=
   w <- sharedWrapper_create 0%i32;
   p <- sharedWrapper_unwrap w;
-  if 0%i32 s= p then Ok tt else Fail_ Failure
+  massert (0%i32 s= p)
 .
 
 (** [adt_borrows::SharedWrapper1]
@@ -64,7 +64,7 @@ Definition sharedWrapper1_unwrap
 Definition use_shared_wrapper1 : result unit :=
   w <- sharedWrapper1_create 0%i32;
   p <- sharedWrapper1_unwrap w;
-  if 0%i32 s= p then Ok tt else Fail_ Failure
+  massert (0%i32 s= p)
 .
 
 (** [adt_borrows::SharedWrapper2]
@@ -99,9 +99,8 @@ Definition use_shared_wrapper2 : result unit :=
   w <- sharedWrapper2_create 0%i32 1%i32;
   p <- sharedWrapper2_unwrap w;
   let (px, py) := p in
-  if 0%i32 s= px
-  then if 1%i32 s= py then Ok tt else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (0%i32 s= px);
+  massert (1%i32 s= py)
 .
 
 (** [adt_borrows::MutWrapper]
@@ -131,7 +130,7 @@ Definition use_mut_wrapper : result unit :=
   let (p2, unwrap_back) := p1 in
   p3 <- i32_add p2 1%i32;
   let x := create_back (unwrap_back p3) in
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** [adt_borrows::MutWrapper1]
@@ -166,7 +165,7 @@ Definition use_mut_wrapper1 : result unit :=
   let (p2, unwrap_back) := p1 in
   p3 <- i32_add p2 1%i32;
   let x := create_back (unwrap_back p3) in
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** [adt_borrows::MutWrapper2]
@@ -223,16 +222,14 @@ Definition use_mut_wrapper2 : result unit :=
         mutWrapper2_x := (unwrap_back px1).(mutWrapper2_x);
         mutWrapper2_y := w.(mutWrapper2_y)
       |} in
-  if x s= 1%i32
-  then
-    let y :=
-      create_back1
-        {|
-          mutWrapper2_x := w.(mutWrapper2_x);
-          mutWrapper2_y := (unwrap_back1 py1).(mutWrapper2_y)
-        |} in
-    if y s= 11%i32 then Ok tt else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (x s= 1%i32);
+  let y :=
+    create_back1
+      {|
+        mutWrapper2_x := w.(mutWrapper2_x);
+        mutWrapper2_y := (unwrap_back1 py1).(mutWrapper2_y)
+      |} in
+  massert (y s= 11%i32)
 .
 
 End AdtBorrows.

tests/coq/misc/NoNestedBorrows.v

@@ -93,7 +93,7 @@ Definition test3 : result unit :=
   x <- get_max 4%u32 3%u32;
   y <- get_max 10%u32 11%u32;
   z <- u32_add x y;
-  if z s= 15%u32 then Ok tt else Fail_ Failure
+  massert (z s= 15%u32)
 .
 
 (** Unit test for [no_nested_borrows::test3] *)
@@ -102,7 +102,7 @@ Check (test3)%return.
 (** [no_nested_borrows::test_neg1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 90:0-94:1 *)
 Definition test_neg1 : result unit :=
-  y <- i32_neg 3%i32; if y s= (-3)%i32 then Ok tt else Fail_ Failure
+  y <- i32_neg 3%i32; massert (y s= (-3)%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
@@ -111,24 +111,18 @@ Check (test_neg1)%return.
 (** [no_nested_borrows::refs_test1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 97:0-106:1 *)
 Definition refs_test1 : result unit :=
-  if 1%i32 s= 1%i32 then Ok tt else Fail_ Failure
-.
+  massert (1%i32 s= 1%i32).
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 Check (refs_test1)%return.
 
 (** [no_nested_borrows::refs_test2]:
     Source: 'tests/src/no_nested_borrows.rs', lines 108:0-120:1 *)
 Definition refs_test2 : result unit :=
-  if 2%i32 s= 2%i32
-  then
-    if 0%i32 s= 0%i32
-    then
-      if 2%i32 s= 2%i32
-      then if 2%i32 s= 2%i32 then Ok tt else Fail_ Failure
-      else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (2%i32 s= 2%i32);
+  _ <- massert (0%i32 s= 0%i32);
+  _ <- massert (2%i32 s= 2%i32);
+  massert (2%i32 s= 2%i32)
 .
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
@@ -149,7 +143,7 @@ Definition test_box1 : result unit :=
   let (_, deref_mut_back) := p in
   let b := deref_mut_back 1%i32 in
   x <- alloc_boxed_Box_deref b;
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -181,7 +175,7 @@ Definition test_panic_msg (b : bool) : result unit :=
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 *)
 Definition test_copy_int : result unit :=
-  y <- copy_int 0%i32; if 0%i32 s= y then Ok tt else Fail_ Failure
+  y <- copy_int 0%i32; massert (0%i32 s= y)
 .
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -196,7 +190,7 @@ Definition is_cons {T : Type} (l : List_t T) : result bool :=
 (** [no_nested_borrows::test_is_cons]:
     Source: 'tests/src/no_nested_borrows.rs', lines 181:0-185:1 *)
 Definition test_is_cons : result unit :=
-  b <- is_cons (List_Cons 0%i32 List_Nil); if b then Ok tt else Fail_ Failure
+  b <- is_cons (List_Cons 0%i32 List_Nil); massert b
 .
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -213,7 +207,7 @@ Definition split_list {T : Type} (l : List_t T) : result (T * (List_t T)) :=
 Definition test_split_list : result unit :=
   p <- split_list (List_Cons 0%i32 List_Nil);
   let (hd, _) := p in
-  if hd s= 0%i32 then Ok tt else Fail_ Failure
+  massert (hd s= 0%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -234,13 +228,10 @@ Definition choose_test : result unit :=
   p <- choose true 0%i32 0%i32;
   let (z, choose_back) := p in
   z1 <- i32_add z 1%i32;
-  if z1 s= 1%i32
-  then
-    let (x, y) := choose_back z1 in
-    if x s= 1%i32
-    then if y s= 0%i32 then Ok tt else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (z1 s= 1%i32);
+  let (x, y) := choose_back z1 in
+  _ <- massert (x s= 1%i32);
+  massert (y s= 0%i32)
 .
 
 (** Unit test for [no_nested_borrows::choose_test] *)
@@ -335,34 +326,22 @@ Definition test_list_functions : result unit :=
   let l := List_Cons 2%i32 List_Nil in
   let l1 := List_Cons 1%i32 l in
   i <- list_length (List_Cons 0%i32 l1);
-  if i s= 3%u32
-  then (
-    i1 <- list_nth_shared (List_Cons 0%i32 l1) 0%u32;
-    if i1 s= 0%i32
-    then (
-      i2 <- list_nth_shared (List_Cons 0%i32 l1) 1%u32;
-      if i2 s= 1%i32
-      then (
-        i3 <- list_nth_shared (List_Cons 0%i32 l1) 2%u32;
-        if i3 s= 2%i32
-        then (
-          p <- list_nth_mut (List_Cons 0%i32 l1) 1%u32;
-          let (_, list_nth_mut_back) := p in
-          let ls := list_nth_mut_back 3%i32 in
-          i4 <- list_nth_shared ls 0%u32;
-          if i4 s= 0%i32
-          then (
-            i5 <- list_nth_shared ls 1%u32;
-            if i5 s= 3%i32
-            then (
-              i6 <- list_nth_shared ls 2%u32;
-              if i6 s= 2%i32 then Ok tt else Fail_ Failure)
-            else Fail_ Failure)
-          else Fail_ Failure)
-        else Fail_ Failure)
-      else Fail_ Failure)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 3%u32);
+  i1 <- list_nth_shared (List_Cons 0%i32 l1) 0%u32;
+  _ <- massert (i1 s= 0%i32);
+  i2 <- list_nth_shared (List_Cons 0%i32 l1) 1%u32;
+  _ <- massert (i2 s= 1%i32);
+  i3 <- list_nth_shared (List_Cons 0%i32 l1) 2%u32;
+  _ <- massert (i3 s= 2%i32);
+  p <- list_nth_mut (List_Cons 0%i32 l1) 1%u32;
+  let (_, list_nth_mut_back) := p in
+  let ls := list_nth_mut_back 3%i32 in
+  i4 <- list_nth_shared ls 0%u32;
+  _ <- massert (i4 s= 0%i32);
+  i5 <- list_nth_shared ls 1%u32;
+  _ <- massert (i5 s= 3%i32);
+  i6 <- list_nth_shared ls 2%u32;
+  massert (i6 s= 2%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -459,23 +438,15 @@ Definition new_pair1 : result (StructWithPair_t u32 u32) :=
 Definition test_constants : result unit :=
   swt <- new_tuple1;
   let (i, _) := swt.(structWithTuple_p) in
-  if i s= 1%u32
-  then (
-    swt1 <- new_tuple2;
-    let (i1, _) := swt1.(structWithTuple_p) in
-    if i1 s= 1%i16
-    then (
-      swt2 <- new_tuple3;
-      let (i2, _) := swt2.(structWithTuple_p) in
-      if i2 s= 1%u64
-      then (
-        swp <- new_pair1;
-        if swp.(structWithPair_p).(pair_x) s= 1%u32
-        then Ok tt
-        else Fail_ Failure)
-      else Fail_ Failure)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 1%u32);
+  swt1 <- new_tuple2;
+  let (i1, _) := swt1.(structWithTuple_p) in
+  _ <- massert (i1 s= 1%i16);
+  swt2 <- new_tuple3;
+  let (i2, _) := swt2.(structWithTuple_p) in
+  _ <- massert (i2 s= 1%u64);
+  swp <- new_pair1;
+  massert (swp.(structWithPair_p).(pair_x) s= 1%u32)
 .
 
 (** Unit test for [no_nested_borrows::test_constants] *)
@@ -493,7 +464,8 @@ Check (test_weird_borrows1)%return.
     Source: 'tests/src/no_nested_borrows.rs', lines 414:0-418:1 *)
 Definition test_mem_replace (px : u32) : result u32 :=
   let (y, _) := core_mem_replace px 1%u32 in
-  if y s= 0%u32 then Ok 2%u32 else Fail_ Failure
+  _ <- massert (y s= 0%u32);
+  Ok 2%u32
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:

tests/coq/misc/Paper.v

@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'tests/src/paper.rs', lines 11:0-15:1 *)
 Definition test_incr : result unit :=
-  x <- ref_incr 0%i32; if x s= 1%i32 then Ok tt else Fail_ Failure
+  x <- ref_incr 0%i32; massert (x s= 1%i32)
 .
 
 (** Unit test for [paper::test_incr] *)
@@ -37,13 +37,10 @@ Definition test_choose : result unit :=
   p <- choose true 0%i32 0%i32;
   let (z, choose_back) := p in
   z1 <- i32_add z 1%i32;
-  if z1 s= 1%i32
-  then
-    let (x, y) := choose_back z1 in
-    if x s= 1%i32
-    then if y s= 0%i32 then Ok tt else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (z1 s= 1%i32);
+  let (x, y) := choose_back z1 in
+  _ <- massert (x s= 1%i32);
+  massert (y s= 0%i32)
 .
 
 (** Unit test for [paper::test_choose] *)
@@ -97,7 +94,7 @@ Definition test_nth : result unit :=
   x1 <- i32_add x 1%i32;
   let l2 := list_nth_mut_back x1 in
   i <- sum l2;
-  if i s= 7%i32 then Ok tt else Fail_ Failure
+  massert (i s= 7%i32)
 .
 
 (** Unit test for [paper::test_nth] *)

tests/fstar/arrays/Arrays.Funs.fst

@@ -343,7 +343,8 @@ let rec sum2_loop
 let sum2 (s : slice u32) (s2 : slice u32) : result u32 =
   let i = slice_len s in
   let i1 = slice_len s2 in
-  if i = i1 then sum2_loop s s2 0 0 else Fail Failure
+  let* _ = massert (i = i1) in
+  sum2_loop s s2 0 0
 
 (** [arrays::f0]:
     Source: 'tests/src/arrays.rs', lines 274:0-277:1 *)