Do not unfold the monadic lets for the generated F* code

7 files changed, 221 insertions, 521 deletions

diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 9b90e9c7..1a2f4133 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -96,14 +96,7 @@ let q3_c : i32 = eval_global q3_body
 
 (** [constants::get_z2] *)
 let get_z2_fwd : result i32 =
-  begin match get_z1_fwd with
-  | Fail e -> Fail e
-  | Return i ->
-    begin match add_fwd i q3_c with
-    | Fail e -> Fail e
-    | Return i0 -> add_fwd q1_c i0
-    end
-  end
+  let* i = get_z1_fwd in let* i0 = add_fwd i q3_c in add_fwd q1_c i0
 
 (** [constants::S1] *)
 let s1_body : result u32 = Return 6
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 2529ec33..f70a9fc6 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -9,53 +9,30 @@ include External.Opaque
 
 (** [external::swap] *)
 let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match core_mem_swap_back0 t x y st st0 with
-    | Fail e -> Fail e
-    | Return (st1, _) ->
-      begin match core_mem_swap_back1 t x y st st1 with
-      | Fail e -> Fail e
-      | Return (st2, _) -> Return (st2, ())
-      end
-    end
-  end
+  let* (st0, _) = core_mem_swap_fwd t x y st in
+  let* (st1, _) = core_mem_swap_back0 t x y st st0 in
+  let* (st2, _) = core_mem_swap_back1 t x y st st1 in
+  Return (st2, ())
 
 (** [external::swap] *)
 let swap_back
   (t : Type0) (x : t) (y : t) (st : state) (st0 : state) :
   result (state & (t & t))
   =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match core_mem_swap_back0 t x y st st1 with
-    | Fail e -> Fail e
-    | Return (st2, x0) ->
-      begin match core_mem_swap_back1 t x y st st2 with
-      | Fail e -> Fail e
-      | Return (_, y0) -> Return (st0, (x0, y0))
-      end
-    end
-  end
+  let* (st1, _) = core_mem_swap_fwd t x y st in
+  let* (st2, x0) = core_mem_swap_back0 t x y st st1 in
+  let* (_, y0) = core_mem_swap_back1 t x y st st2 in
+  Return (st0, (x0, y0))
 
 (** [external::test_new_non_zero_u32] *)
 let test_new_non_zero_u32_fwd
   (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
-  begin match core_num_nonzero_non_zero_u32_new_fwd x st with
-  | Fail e -> Fail e
-  | Return (st0, opt) ->
-    core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
-  end
+  let* (st0, opt) = core_num_nonzero_non_zero_u32_new_fwd x st in
+  core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
 
 (** [external::test_vec] *)
 let test_vec_fwd : result unit =
-  let v = vec_new u32 in
-  begin match vec_push_back u32 v 0 with
-  | Fail e -> Fail e
-  | Return _ -> Return ()
-  end
+  let v = vec_new u32 in let* _ = vec_push_back u32 v 0 in Return ()
 
 (** Unit test for [external::test_vec] *)
 let _ = assert_norm (test_vec_fwd = Return ())
@@ -63,44 +40,25 @@ let _ = assert_norm (test_vec_fwd = Return ())
 (** [external::custom_swap] *)
 let custom_swap_fwd
   (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match core_mem_swap_back0 t x y st st0 with
-    | Fail e -> Fail e
-    | Return (st1, x0) ->
-      begin match core_mem_swap_back1 t x y st st1 with
-      | Fail e -> Fail e
-      | Return (st2, _) -> Return (st2, x0)
-      end
-    end
-  end
+  let* (st0, _) = core_mem_swap_fwd t x y st in
+  let* (st1, x0) = core_mem_swap_back0 t x y st st0 in
+  let* (st2, _) = core_mem_swap_back1 t x y st st1 in
+  Return (st2, x0)
 
 (** [external::custom_swap] *)
 let custom_swap_back
   (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) :
   result (state & (t & t))
   =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match core_mem_swap_back0 t x y st st1 with
-    | Fail e -> Fail e
-    | Return (st2, _) ->
-      begin match core_mem_swap_back1 t x y st st2 with
-      | Fail e -> Fail e
-      | Return (_, y0) -> Return (st0, (ret, y0))
-      end
-    end
-  end
+  let* (st1, _) = core_mem_swap_fwd t x y st in
+  let* (st2, _) = core_mem_swap_back0 t x y st st1 in
+  let* (_, y0) = core_mem_swap_back1 t x y st st2 in
+  Return (st0, (ret, y0))
 
 (** [external::test_custom_swap] *)
 let test_custom_swap_fwd
   (x : u32) (y : u32) (st : state) : result (state & unit) =
-  begin match custom_swap_fwd u32 x y st with
-  | Fail e -> Fail e
-  | Return (st0, _) -> Return (st0, ())
-  end
+  let* (st0, _) = custom_swap_fwd u32 x y st in Return (st0, ())
 
 (** [external::test_custom_swap] *)
 let test_custom_swap_back
@@ -111,13 +69,7 @@ let test_custom_swap_back
 
 (** [external::test_swap_non_zero] *)
 let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
-  begin match swap_fwd u32 x 0 st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match swap_back u32 x 0 st st0 with
-    | Fail e -> Fail e
-    | Return (st1, (x0, _)) ->
-      if x0 = 0 then Fail Failure else Return (st1, x0)
-    end
-  end
+  let* (st0, _) = swap_fwd u32 x 0 st in
+  let* (st1, (x0, _)) = swap_back u32 x 0 st st0 in
+  if x0 = 0 then Fail Failure else Return (st1, x0)
 
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 3e8425dd..0d3c39f7 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -13,14 +13,8 @@ let rec sum_loop_fwd
   Tot (result u32) (decreases (sum_loop_decreases max i s))
   =
   if i < max
-  then
-    begin match u32_add s i with
-    | Fail e -> Fail e
-    | Return s0 ->
-      begin match u32_add i 1 with
-      | Fail e -> Fail e
-      | Return i0 -> sum_loop_fwd max i0 s0
-      end
+  then begin
+    let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0
     end
   else u32_mul s 2
 
@@ -33,15 +27,10 @@ let rec sum_with_mut_borrows_loop_fwd
   Tot (result u32) (decreases (sum_with_mut_borrows_loop_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_mut_borrows_loop_fwd max mi0 ms0
-      end
-    end
+  then begin
+    let* ms0 = u32_add ms mi in
+    let* mi0 = u32_add mi 1 in
+    sum_with_mut_borrows_loop_fwd max mi0 ms0 end
   else u32_mul ms 2
 
 (** [loops::sum_with_mut_borrows] *)
@@ -54,15 +43,10 @@ let rec sum_with_shared_borrows_loop_fwd
   Tot (result u32) (decreases (sum_with_shared_borrows_loop_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
+  then begin
+    let* i0 = u32_add i 1 in
+    let* s0 = u32_add s i0 in
+    sum_with_shared_borrows_loop_fwd max i0 s0 end
   else u32_mul s 2
 
 (** [loops::sum_with_shared_borrows] *)
@@ -76,15 +60,10 @@ let rec clear_loop_fwd_back
   =
   let i0 = vec_len u32 v in
   if i < i0
-  then
-    begin match usize_add i 1 with
-    | Fail e -> Fail e
-    | Return i1 ->
-      begin match vec_index_mut_back u32 v i 0 with
-      | Fail e -> Fail e
-      | Return v0 -> clear_loop_fwd_back v0 i1
-      end
-    end
+  then begin
+    let* i1 = usize_add i 1 in
+    let* v0 = vec_index_mut_back u32 v i 0 in
+    clear_loop_fwd_back v0 i1 end
   else Return v
 
 (** [loops::clear] *)
@@ -113,11 +92,7 @@ let rec list_nth_mut_loop_loop_fwd
   | 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_mut_loop_loop_fwd t tl i0
-      end
+    else begin let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 end
   | ListNil -> Fail Failure
   end
 
@@ -134,15 +109,10 @@ let rec list_nth_mut_loop_loop_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_loop_loop_back t tl i0 ret with
-        | Fail e -> Fail e
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
+    else begin
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in
+      Return (ListCons x tl0) end
   | ListNil -> Fail Failure
   end
 
@@ -160,10 +130,7 @@ let rec list_nth_shared_loop_loop_fwd
   | 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
+    else begin let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
@@ -184,10 +151,8 @@ let rec get_elem_mut_loop_fwd
 
 (** [loops::get_elem_mut] *)
 let get_elem_mut_fwd (slots : vec (list_t usize)) (x : usize) : result usize =
-  begin match vec_index_mut_fwd (list_t usize) slots 0 with
-  | Fail e -> Fail e
-  | Return l -> get_elem_mut_loop_fwd x l
-  end
+  let* l = vec_index_mut_fwd (list_t usize) slots 0 in
+  get_elem_mut_loop_fwd x l
 
 (** [loops::get_elem_mut] *)
 let rec get_elem_mut_loop_back
@@ -198,11 +163,8 @@ let rec get_elem_mut_loop_back
   | ListCons y tl ->
     if y = x
     then Return (ListCons ret tl)
-    else
-      begin match get_elem_mut_loop_back x tl ret with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (ListCons y tl0)
-      end
+    else begin
+      let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) end
   | ListNil -> Fail Failure
   end
 
@@ -211,14 +173,9 @@ let get_elem_mut_back
   (slots : vec (list_t usize)) (x : usize) (ret : usize) :
   result (vec (list_t usize))
   =
-  begin match vec_index_mut_fwd (list_t usize) slots 0 with
-  | Fail e -> Fail e
-  | Return l ->
-    begin match get_elem_mut_loop_back x l ret with
-    | Fail e -> Fail e
-    | Return l0 -> vec_index_mut_back (list_t usize) slots 0 l0
-    end
-  end
+  let* l = vec_index_mut_fwd (list_t usize) slots 0 in
+  let* l0 = get_elem_mut_loop_back x l ret in
+  vec_index_mut_back (list_t usize) slots 0 l0
 
 (** [loops::get_elem_shared] *)
 let rec get_elem_shared_loop_fwd
@@ -233,10 +190,7 @@ let rec get_elem_shared_loop_fwd
 (** [loops::get_elem_shared] *)
 let get_elem_shared_fwd
   (slots : vec (list_t usize)) (x : usize) : result usize =
-  begin match vec_index_fwd (list_t usize) slots 0 with
-  | Fail e -> Fail e
-  | Return l -> get_elem_shared_loop_fwd x l
-  end
+  let* l = vec_index_fwd (list_t usize) slots 0 in get_elem_shared_loop_fwd x l
 
 (** [loops::id_mut] *)
 let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
@@ -258,21 +212,15 @@ let rec list_nth_mut_loop_with_id_loop_fwd
   | 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_mut_loop_with_id_loop_fwd t i0 tl
-      end
+    else begin
+      let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl end
   | ListNil -> Fail Failure
   end
 
 (** [loops::list_nth_mut_loop_with_id] *)
 let list_nth_mut_loop_with_id_fwd
   (t : Type0) (ls : list_t t) (i : u32) : result t =
-  begin match id_mut_fwd t ls with
-  | Fail e -> Fail e
-  | Return ls0 -> list_nth_mut_loop_with_id_loop_fwd t i ls0
-  end
+  let* ls0 = id_mut_fwd t ls in list_nth_mut_loop_with_id_loop_fwd t i ls0
 
 (** [loops::list_nth_mut_loop_with_id] *)
 let rec list_nth_mut_loop_with_id_loop_back
@@ -284,29 +232,19 @@ let rec list_nth_mut_loop_with_id_loop_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with
-        | Fail e -> Fail e
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
+    else begin
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in
+      Return (ListCons x tl0) end
   | ListNil -> Fail Failure
   end
 
 (** [loops::list_nth_mut_loop_with_id] *)
 let list_nth_mut_loop_with_id_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
-  begin match id_mut_fwd t ls with
-  | Fail e -> Fail e
-  | Return ls0 ->
-    begin match list_nth_mut_loop_with_id_loop_back t i ls0 ret with
-    | Fail e -> Fail e
-    | Return l -> id_mut_back t ls l
-    end
-  end
+  let* ls0 = id_mut_fwd t ls in
+  let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in
+  id_mut_back t ls l
 
 (** [loops::list_nth_shared_loop_with_id] *)
 let rec list_nth_shared_loop_with_id_loop_fwd
@@ -318,10 +256,8 @@ let rec list_nth_shared_loop_with_id_loop_fwd
   | 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_with_id_loop_fwd t i0 tl
+    else begin
+      let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl
       end
   | ListNil -> Fail Failure
   end
@@ -329,10 +265,8 @@ let rec list_nth_shared_loop_with_id_loop_fwd
 (** [loops::list_nth_shared_loop_with_id] *)
 let list_nth_shared_loop_with_id_fwd
   (t : Type0) (ls : list_t t) (i : u32) : result t =
-  begin match id_shared_fwd t ls with
-  | Fail e -> Fail e
-  | Return ls0 -> list_nth_shared_loop_with_id_loop_fwd t i ls0
-  end
+  let* ls0 = id_shared_fwd t ls in
+  list_nth_shared_loop_with_id_loop_fwd t i ls0
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_fwd
@@ -346,10 +280,8 @@ let rec list_nth_mut_loop_pair_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0
         end
     | ListNil -> Fail Failure
     end
@@ -373,15 +305,10 @@ let rec list_nth_mut_loop_pair_loop_back'a
     | 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 tl00 -> Return (ListCons x0 tl00)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in
+        Return (ListCons x0 tl00) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -406,15 +333,10 @@ let rec list_nth_mut_loop_pair_loop_back'b
     | 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 tl10 -> Return (ListCons x1 tl10)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in
+        Return (ListCons x1 tl10) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -439,11 +361,9 @@ let rec list_nth_shared_loop_pair_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -466,11 +386,9 @@ let rec list_nth_mut_loop_pair_merge_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -493,16 +411,11 @@ let rec list_nth_mut_loop_pair_merge_loop_back
     | 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 (tl00, tl10) -> Return (ListCons x0 tl00, ListCons x1 tl10)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* (tl00, tl10) =
+          list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (ListCons x0 tl00, ListCons x1 tl10) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -527,11 +440,9 @@ let rec list_nth_shared_loop_pair_merge_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -554,11 +465,9 @@ let rec list_nth_mut_shared_loop_pair_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -581,16 +490,10 @@ let rec list_nth_mut_shared_loop_pair_loop_back
     | 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 tl00 -> Return (ListCons x0 tl00)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in
+        Return (ListCons x0 tl00) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -615,12 +518,9 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -643,16 +543,11 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
     | 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 tl00 -> Return (ListCons x0 tl00)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl00 =
+          list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (ListCons x0 tl00) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -677,11 +572,9 @@ let rec list_nth_shared_mut_loop_pair_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -704,16 +597,10 @@ let rec list_nth_shared_mut_loop_pair_loop_back
     | 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 tl10 -> Return (ListCons x1 tl10)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in
+        Return (ListCons x1 tl10) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -738,12 +625,9 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
     | 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
+      else begin
+        let* i0 = u32_sub i 1 in
+        list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
@@ -766,16 +650,11 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
     | 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 tl10 -> Return (ListCons x1 tl10)
-          end
-        end
+      else begin
+        let* i0 = u32_sub i 1 in
+        let* tl10 =
+          list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in
+        Return (ListCons x1 tl10) end
     | ListNil -> Fail Failure
     end
   | ListNil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index f8c63798..ce1f544c 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -52,8 +52,7 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y
 let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x
 
 (** [no_nested_borrows::test2] *)
-let test2_fwd : result unit =
-  begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end
+let test2_fwd : result unit = let* _ = u32_add 23 44 in Return ()
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -64,28 +63,17 @@ 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 e -> Fail e
-  | Return x ->
-    begin match get_max_fwd 10 11 with
-    | Fail e -> Fail e
-    | Return y ->
-      begin match u32_add x y with
-      | Fail e -> Fail e
-      | Return z -> if not (z = 15) then Fail Failure else Return ()
-      end
-    end
-  end
+  let* x = get_max_fwd 4 3 in
+  let* y = get_max_fwd 10 11 in
+  let* z = u32_add x y in
+  if not (z = 15) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test3] *)
 let _ = assert_norm (test3_fwd = Return ())
 
 (** [no_nested_borrows::test_neg1] *)
 let test_neg1_fwd : result unit =
-  begin match i32_neg 3 with
-  | Fail e -> Fail e
-  | Return y -> if not (y = -3) then Fail Failure else Return ()
-  end
+  let* y = i32_neg 3 in if not (y = -3) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
@@ -138,10 +126,7 @@ let test_panic_fwd (b : bool) : result unit =
 
 (** [no_nested_borrows::test_copy_int] *)
 let test_copy_int_fwd : result unit =
-  begin match copy_int_fwd 0 with
-  | Fail e -> Fail e
-  | Return y -> if not (0 = y) then Fail Failure else Return ()
-  end
+  let* y = copy_int_fwd 0 in if not (0 = y) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
 let _ = assert_norm (test_copy_int_fwd = Return ())
@@ -156,10 +141,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
 (** [no_nested_borrows::test_is_cons] *)
 let test_is_cons_fwd : result unit =
   let l = ListNil in
-  begin match is_cons_fwd i32 (ListCons 0 l) with
-  | Fail e -> Fail e
-  | Return b -> if not b then Fail Failure else Return ()
-  end
+  let* b = is_cons_fwd i32 (ListCons 0 l) in
+  if not b then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
 let _ = assert_norm (test_is_cons_fwd = Return ())
@@ -174,11 +157,9 @@ let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
 (** [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 e -> Fail e
-  | Return p ->
-    let (hd, _) = p in if not (hd = 0) then Fail Failure else Return ()
-  end
+  let* p = split_list_fwd i32 (ListCons 0 l) in
+  let (hd, _) = p in
+  if not (hd = 0) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
 let _ = assert_norm (test_split_list_fwd = Return ())
@@ -194,24 +175,15 @@ let choose_back
 
 (** [no_nested_borrows::choose_test] *)
 let choose_test_fwd : result unit =
-  begin match choose_fwd i32 true 0 0 with
-  | Fail e -> Fail e
-  | Return z ->
-    begin match i32_add z 1 with
-    | Fail e -> Fail e
-    | Return z0 ->
-      if not (z0 = 1)
-      then Fail Failure
-      else
-        begin match choose_back i32 true 0 0 z0 with
-        | Fail e -> Fail e
-        | Return (x, y) ->
-          if not (x = 1)
-          then Fail Failure
-          else if not (y = 0) then Fail Failure else Return ()
-        end
-    end
-  end
+  let* z = choose_fwd i32 true 0 0 in
+  let* z0 = i32_add z 1 in
+  if not (z0 = 1)
+  then Fail Failure
+  else begin
+    let* (x, y) = choose_back i32 true 0 0 z0 in
+    if not (x = 1)
+    then Fail Failure
+    else if not (y = 0) then Fail Failure else Return () end
 
 (** Unit test for [no_nested_borrows::choose_test] *)
 let _ = assert_norm (choose_test_fwd = Return ())
@@ -232,11 +204,7 @@ and tree_t (t : Type0) =
 (** [no_nested_borrows::list_length] *)
 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 e -> Fail e
-    | Return i -> u32_add 1 i
-    end
+  | ListCons x l1 -> let* i = list_length_fwd t l1 in u32_add 1 i
   | ListNil -> Return 0
   end
 
@@ -246,11 +214,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | 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_fwd t tl i0
-      end
+    else begin let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0 end
   | ListNil -> Fail Failure
   end
 
@@ -260,11 +224,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | 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_mut_fwd t tl i0
-      end
+    else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end
   | ListNil -> Fail Failure
   end
 
@@ -275,15 +235,10 @@ let rec list_nth_mut_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_back t tl i0 ret with
-        | Fail e -> Fail e
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
+    else begin
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_back t tl i0 ret in
+      Return (ListCons x tl0) end
   | ListNil -> Fail Failure
   end
 
@@ -305,57 +260,34 @@ let test_list_functions_fwd : result unit =
   let l = ListNil in
   let l0 = ListCons 2 l in
   let l1 = ListCons 1 l0 in
-  begin match list_length_fwd i32 (ListCons 0 l1) with
-  | Fail e -> Fail e
-  | Return i ->
-    if not (i = 3)
+  let* i = list_length_fwd i32 (ListCons 0 l1) in
+  if not (i = 3)
+  then Fail Failure
+  else begin
+    let* i0 = list_nth_shared_fwd i32 (ListCons 0 l1) 0 in
+    if not (i0 = 0)
     then Fail Failure
-    else
-      begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
-      | Fail e -> Fail e
-      | Return i0 ->
-        if not (i0 = 0)
+    else begin
+      let* i1 = list_nth_shared_fwd i32 (ListCons 0 l1) 1 in
+      if not (i1 = 1)
+      then Fail Failure
+      else begin
+        let* i2 = list_nth_shared_fwd i32 (ListCons 0 l1) 2 in
+        if not (i2 = 2)
         then Fail Failure
-        else
-          begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
-          | Fail e -> Fail e
-          | Return i1 ->
-            if not (i1 = 1)
+        else begin
+          let* ls = list_nth_mut_back i32 (ListCons 0 l1) 1 3 in
+          let* i3 = list_nth_shared_fwd i32 ls 0 in
+          if not (i3 = 0)
+          then Fail Failure
+          else begin
+            let* i4 = list_nth_shared_fwd i32 ls 1 in
+            if not (i4 = 3)
             then Fail Failure
-            else
-              begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
-              | Fail e -> Fail e
-              | Return i2 ->
-                if not (i2 = 2)
-                then Fail Failure
-                else
-                  begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
-                  | Fail e -> Fail e
-                  | Return ls ->
-                    begin match list_nth_shared_fwd i32 ls 0 with
-                    | Fail e -> Fail e
-                    | Return i3 ->
-                      if not (i3 = 0)
-                      then Fail Failure
-                      else
-                        begin match list_nth_shared_fwd i32 ls 1 with
-                        | Fail e -> Fail e
-                        | Return i4 ->
-                          if not (i4 = 3)
-                          then Fail Failure
-                          else
-                            begin match list_nth_shared_fwd i32 ls 2 with
-                            | Fail e -> Fail e
-                            | Return i5 ->
-                              if not (i5 = 2) then Fail Failure else Return ()
-                            end
-                        end
-                    end
-                  end
-              end
-          end
-      end
-  end
+            else begin
+              let* i5 = list_nth_shared_fwd i32 ls 2 in
+              if not (i5 = 2) then Fail Failure else Return () end end end end
+      end end
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
 let _ = assert_norm (test_list_functions_fwd = Return ())
@@ -433,37 +365,25 @@ 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 e -> Fail e
-  | Return swt ->
-    let (i, _) = swt.struct_with_tuple_p in
-    if not (i = 1)
+  let* swt = new_tuple1_fwd in
+  let (i, _) = swt.struct_with_tuple_p in
+  if not (i = 1)
+  then Fail Failure
+  else begin
+    let* swt0 = new_tuple2_fwd in
+    let (i0, _) = swt0.struct_with_tuple_p in
+    if not (i0 = 1)
     then Fail Failure
-    else
-      begin match new_tuple2_fwd with
-      | Fail e -> Fail e
-      | Return swt0 ->
-        let (i0, _) = swt0.struct_with_tuple_p in
-        if not (i0 = 1)
+    else begin
+      let* swt1 = new_tuple3_fwd in
+      let (i1, _) = swt1.struct_with_tuple_p in
+      if not (i1 = 1)
+      then Fail Failure
+      else begin
+        let* swp = new_pair1_fwd in
+        if not (swp.struct_with_pair_p.pair_x = 1)
         then Fail Failure
-        else
-          begin match new_tuple3_fwd with
-          | Fail e -> Fail e
-          | Return swt1 ->
-            let (i1, _) = swt1.struct_with_tuple_p in
-            if not (i1 = 1)
-            then Fail Failure
-            else
-              begin match new_pair1_fwd with
-              | Fail e -> Fail e
-              | Return swp ->
-                if not (swp.struct_with_pair_p.pair_x = 1)
-                then Fail Failure
-                else Return ()
-              end
-          end
-      end
-  end
+        else Return () end end end
 
 (** Unit test for [no_nested_borrows::test_constants] *)
 let _ = assert_norm (test_constants_fwd = Return ())
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 199ceb63..95f13f62 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -10,10 +10,8 @@ let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1
 
 (** [paper::test_incr] *)
 let test_incr_fwd : result unit =
-  begin match ref_incr_fwd_back 0 with
-  | Fail e -> Fail e
-  | Return x -> if not (x = 1) then Fail Failure else Return ()
-  end
+  let* x = ref_incr_fwd_back 0 in
+  if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_incr] *)
 let _ = assert_norm (test_incr_fwd = Return ())
@@ -29,24 +27,15 @@ let choose_back
 
 (** [paper::test_choose] *)
 let test_choose_fwd : result unit =
-  begin match choose_fwd i32 true 0 0 with
-  | Fail e -> Fail e
-  | Return z ->
-    begin match i32_add z 1 with
-    | Fail e -> Fail e
-    | Return z0 ->
-      if not (z0 = 1)
-      then Fail Failure
-      else
-        begin match choose_back i32 true 0 0 z0 with
-        | Fail e -> Fail e
-        | Return (x, y) ->
-          if not (x = 1)
-          then Fail Failure
-          else if not (y = 0) then Fail Failure else Return ()
-        end
-    end
-  end
+  let* z = choose_fwd i32 true 0 0 in
+  let* z0 = i32_add z 1 in
+  if not (z0 = 1)
+  then Fail Failure
+  else begin
+    let* (x, y) = choose_back i32 true 0 0 z0 in
+    if not (x = 1)
+    then Fail Failure
+    else if not (y = 0) then Fail Failure else Return () end
 
 (** Unit test for [paper::test_choose] *)
 let _ = assert_norm (test_choose_fwd = Return ())
@@ -62,11 +51,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   | 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_mut_fwd t tl i0
-      end
+    else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end
   | ListNil -> Fail Failure
   end
 
@@ -77,26 +62,17 @@ let rec list_nth_mut_back
   | ListCons x tl ->
     if i = 0
     then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail e -> Fail e
-      | Return i0 ->
-        begin match list_nth_mut_back t tl i0 ret with
-        | Fail e -> Fail e
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
+    else begin
+      let* i0 = u32_sub i 1 in
+      let* tl0 = list_nth_mut_back t tl i0 ret in
+      Return (ListCons x tl0) end
   | ListNil -> Fail Failure
   end
 
 (** [paper::sum] *)
 let rec sum_fwd (l : list_t i32) : result i32 =
   begin match l with
-  | ListCons x tl ->
-    begin match sum_fwd tl with
-    | Fail e -> Fail e
-    | Return i -> i32_add x i
-    end
+  | ListCons x tl -> let* i = sum_fwd tl in i32_add x i
   | ListNil -> Return 0
   end
 
@@ -105,22 +81,11 @@ let test_nth_fwd : result unit =
   let l = ListNil in
   let l0 = ListCons 3 l in
   let l1 = ListCons 2 l0 in
-  begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
-  | Fail e -> Fail e
-  | Return x ->
-    begin match i32_add x 1 with
-    | Fail e -> Fail e
-    | Return x0 ->
-      begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
-      | Fail e -> Fail e
-      | Return l2 ->
-        begin match sum_fwd l2 with
-        | Fail e -> Fail e
-        | Return i -> if not (i = 7) then Fail Failure else Return ()
-        end
-      end
-    end
-  end
+  let* x = list_nth_mut_fwd i32 (ListCons 1 l1) 2 in
+  let* x0 = i32_add x 1 in
+  let* l2 = list_nth_mut_back i32 (ListCons 1 l1) 2 x0 in
+  let* i = sum_fwd l2 in
+  if not (i = 7) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_nth] *)
 let _ = assert_norm (test_nth_fwd = Return ())
@@ -128,16 +93,8 @@ let _ = assert_norm (test_nth_fwd = Return ())
 (** [paper::call_choose] *)
 let call_choose_fwd (p : (u32 & u32)) : result u32 =
   let (px, py) = p in
-  begin match choose_fwd u32 true px py with
-  | Fail e -> Fail e
-  | Return pz ->
-    begin match u32_add pz 1 with
-    | Fail e -> Fail e
-    | Return pz0 ->
-      begin match choose_back u32 true px py pz0 with
-      | Fail e -> Fail e
-      | Return (px0, _) -> Return px0
-      end
-    end
-  end
+  let* pz = choose_fwd u32 true px py in
+  let* pz0 = u32_add pz 1 in
+  let* (px0, _) = choose_back u32 true px py pz0 in
+  Return px0
 
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 12618dbb..db0dc0d5 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -25,11 +25,8 @@ let rec get_list_at_x_back
   | ListCons hd tl ->
     if hd = x
     then Return ret
-    else
-      begin match get_list_at_x_back tl x ret with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (ListCons hd tl0)
-      end
+    else begin
+      let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) end
   | ListNil -> Return ret
   end
 
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index bf0f9078..98a696b6 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x
 // let* x = y in
 // ...
 // ```
-unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+unfold let (let*) (#a #b : Type0) (m: result a)
+  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
+  result b =
   match m with
   | Return x -> f x
   | Fail e   -> Fail e