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

2 files changed, 188 insertions, 423 deletions

diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 56cff453..51021daf 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -18,15 +18,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd
   (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n))
   =
   if n > 0
-  then
-    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
-    | Fail e -> Fail e
-    | Return slots0 ->
-      begin match usize_sub n 1 with
-      | Fail e -> Fail e
-      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
-      end
-    end
+  then begin
+    let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in
+    let* n0 = usize_sub n 1 in
+    hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end
   else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
@@ -43,20 +38,11 @@ let hashmap_hash_map_new_with_capacity_fwd
   result (hashmap_hash_map_t t)
   =
   let v = vec_new (hashmap_list_t t) in
-  begin match hashmap_hash_map_allocate_slots_fwd t v capacity with
-  | Fail e -> Fail e
-  | Return slots ->
-    begin match usize_mul capacity max_load_dividend with
-    | Fail e -> Fail e
-    | Return i ->
-      begin match usize_div i max_load_divisor with
-      | Fail e -> Fail e
-      | Return i0 ->
-        Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
-          slots)
-      end
-    end
-  end
+  let* slots = hashmap_hash_map_allocate_slots_fwd t v capacity in
+  let* i = usize_mul capacity max_load_dividend in
+  let* i0 = usize_div i max_load_divisor in
+  Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
+    slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
@@ -70,28 +56,20 @@ let rec hashmap_hash_map_clear_loop_fwd_back
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
-  then
-    begin match usize_add i 1 with
-    | Fail e -> Fail e
-    | Return i1 ->
-      begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
-        with
-      | Fail e -> Fail e
-      | Return slots0 -> hashmap_hash_map_clear_loop_fwd_back t slots0 i1
-      end
-    end
+  then begin
+    let* i1 = usize_add i 1 in
+    let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
+      in
+    hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end
   else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
-  begin match
-    hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 with
-  | Fail e -> Fail e
-  | Return v ->
-    Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
-      self.hashmap_hash_map_max_load v)
-  end
+  let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
+    in
+  Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
+    self.hashmap_hash_map_max_load v)
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
 let hashmap_hash_map_len_fwd
@@ -127,11 +105,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return (HashmapListCons ckey value tl)
-    else
-      begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
-      end
+    else begin
+      let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in
+      Return (HashmapListCons ckey cvalue tl0) end
   | HashmapListNil ->
     let l = HashmapListNil in Return (HashmapListCons key value l)
   end
@@ -148,59 +124,30 @@ let hashmap_hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
   result (hashmap_hash_map_t t)
   =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_insert_in_list_fwd t key value l with
-        | Fail e -> Fail e
-        | Return inserted ->
-          if inserted
-          then
-            begin match usize_add self.hashmap_hash_map_num_entries 1 with
-            | Fail e -> Fail e
-            | Return i0 ->
-              begin match hashmap_hash_map_insert_in_list_back t key value l
-                with
-              | Fail e -> Fail e
-              | Return l0 ->
-                begin match
-                  vec_index_mut_back (hashmap_list_t t)
-                    self.hashmap_hash_map_slots hash_mod l0 with
-                | Fail e -> Fail e
-                | Return v ->
-                  Return (Mkhashmap_hash_map_t i0
-                    self.hashmap_hash_map_max_load_factor
-                    self.hashmap_hash_map_max_load v)
-                end
-              end
-            end
-          else
-            begin match hashmap_hash_map_insert_in_list_back t key value l with
-            | Fail e -> Fail e
-            | Return l0 ->
-              begin match
-                vec_index_mut_back (hashmap_list_t t)
-                  self.hashmap_hash_map_slots hash_mod l0 with
-              | Fail e -> Fail e
-              | Return v ->
-                Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
-                  self.hashmap_hash_map_max_load_factor
-                  self.hashmap_hash_map_max_load v)
-              end
-            end
-        end
-      end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+    in
+  let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in
+  if inserted
+  then begin
+    let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in
+    let* l0 = hashmap_hash_map_insert_in_list_back t key value l in
+    let* v =
+      vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
+      self.hashmap_hash_map_max_load v) end
+  else begin
+    let* l0 = hashmap_hash_map_insert_in_list_back t key value l in
+    let* v =
+      vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+      self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
     end
-  end
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -215,11 +162,8 @@ let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
-    | Fail e -> Fail e
-    | Return ntable0 ->
-      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
-    end
+    let* ntable0 = hashmap_hash_map_insert_no_resize_fwd_back t ntable k v in
+    hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
   | HashmapListNil -> Return ntable
   end
 
@@ -239,27 +183,15 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
-  then
-    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
-    | Fail e -> Fail e
-    | Return l ->
-      let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
-        with
-      | Fail e -> Fail e
-      | Return ntable0 ->
-        begin match usize_add i 1 with
-        | Fail e -> Fail e
-        | Return i1 ->
-          let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
-          begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
-          | Fail e -> Fail e
-          | Return slots0 ->
-            hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
-          end
-        end
-      end
-    end
+  then begin
+    let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in
+    let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+    let* ntable0 =
+      hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls in
+    let* i1 = usize_add i 1 in
+    let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
+    let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in
+    hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end
   else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
@@ -273,59 +205,34 @@ let hashmap_hash_map_move_elements_fwd_back
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
-  begin match scalar_cast U32 Usize core_num_u32_max_c with
-  | Fail e -> Fail e
-  | Return max_usize ->
-    let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_div max_usize 2 with
-    | Fail e -> Fail e
-    | Return n1 ->
-      let (i, i0) = self.hashmap_hash_map_max_load_factor in
-      begin match usize_div n1 i with
-      | Fail e -> Fail e
-      | Return i1 ->
-        if capacity <= i1
-        then
-          begin match usize_mul capacity 2 with
-          | Fail e -> Fail e
-          | Return i2 ->
-            begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
-            | Fail e -> Fail e
-            | Return ntable ->
-              begin match
-                hashmap_hash_map_move_elements_fwd_back t ntable
-                  self.hashmap_hash_map_slots 0 with
-              | Fail e -> Fail e
-              | Return (ntable0, _) ->
-                Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
-                  (i, i0) ntable0.hashmap_hash_map_max_load
-                  ntable0.hashmap_hash_map_slots)
-              end
-            end
-          end
-        else
-          Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i,
-            i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
-      end
-    end
-  end
+  let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
+  let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* n1 = usize_div max_usize 2 in
+  let (i, i0) = self.hashmap_hash_map_max_load_factor in
+  let* i1 = usize_div n1 i in
+  if capacity <= i1
+  then begin
+    let* i2 = usize_mul capacity 2 in
+    let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in
+    let* (ntable0, _) =
+      hashmap_hash_map_move_elements_fwd_back t ntable
+        self.hashmap_hash_map_slots 0 in
+    Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
+      ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end
+  else
+    Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
+      self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
 let hashmap_hash_map_insert_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
   result (hashmap_hash_map_t t)
   =
-  begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with
-  | Fail e -> Fail e
-  | Return self0 ->
-    begin match hashmap_hash_map_len_fwd t self0 with
-    | Fail e -> Fail e
-    | Return i ->
-      if i > self0.hashmap_hash_map_max_load
-      then hashmap_hash_map_try_resize_fwd_back t self0
-      else Return self0
-    end
-  end
+  let* self0 = hashmap_hash_map_insert_no_resize_fwd_back t self key value in
+  let* i = hashmap_hash_map_len_fwd t self0 in
+  if i > self0.hashmap_hash_map_max_load
+  then hashmap_hash_map_try_resize_fwd_back t self0
+  else Return self0
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hashmap_hash_map_contains_key_in_list_loop_fwd
@@ -349,21 +256,12 @@ let hashmap_hash_map_contains_key_in_list_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
 let hashmap_hash_map_contains_key_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
-        with
-      | Fail e -> Fail e
-      | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l
-      end
-    end
-  end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
+  hashmap_hash_map_contains_key_in_list_fwd t key l
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
 let rec hashmap_hash_map_get_in_list_loop_fwd
@@ -387,21 +285,12 @@ let hashmap_hash_map_get_in_list_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::get] *)
 let hashmap_hash_map_get_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
-        with
-      | Fail e -> Fail e
-      | Return l -> hashmap_hash_map_get_in_list_fwd t key l
-      end
-    end
-  end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
+  hashmap_hash_map_get_in_list_fwd t key l
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
@@ -432,11 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return (HashmapListCons ckey ret tl)
-    else
-      begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
-      end
+    else begin
+      let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in
+      Return (HashmapListCons ckey cvalue tl0) end
   | HashmapListNil -> Fail Failure
   end
 
@@ -450,55 +337,31 @@ let hashmap_hash_map_get_mut_in_list_back
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 let hashmap_hash_map_get_mut_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail e -> Fail e
-      | Return l -> hashmap_hash_map_get_mut_in_list_fwd t l key
-      end
-    end
-  end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+    in
+  hashmap_hash_map_get_mut_in_list_fwd t l key
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 let hashmap_hash_map_get_mut_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) :
   result (hashmap_hash_map_t t)
   =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_get_mut_in_list_back t l key ret with
-        | Fail e -> Fail e
-        | Return l0 ->
-          begin match
-            vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
-              hash_mod l0 with
-          | Fail e -> Fail e
-          | Return v ->
-            Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
-              self.hashmap_hash_map_max_load_factor
-              self.hashmap_hash_map_max_load v)
-          end
-        end
-      end
-    end
-  end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+    in
+  let* l0 = hashmap_hash_map_get_mut_in_list_back t l key ret in
+  let* v =
+    vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+      l0 in
+  Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+    self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
@@ -543,11 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back
       | HashmapListCons i cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail Failure
       end
-    else
-      begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (HashmapListCons ckey x tl0)
-      end
+    else begin
+      let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in
+      Return (HashmapListCons ckey x tl0) end
   | HashmapListNil -> Return HashmapListNil
   end
 
@@ -561,32 +422,17 @@ let hashmap_hash_map_remove_from_list_back
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
 let hashmap_hash_map_remove_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_remove_from_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x ->
-          begin match x with
-          | None -> Return None
-          | Some x0 ->
-            begin match usize_sub self.hashmap_hash_map_num_entries 1 with
-            | Fail e -> Fail e
-            | Return _ -> Return (Some x0)
-            end
-          end
-        end
-      end
-    end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+    in
+  let* x = hashmap_hash_map_remove_from_list_fwd t key l in
+  begin match x with
+  | None -> Return None
+  | Some x0 ->
+    let* _ = usize_sub self.hashmap_hash_map_num_entries 1 in Return (Some x0)
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
@@ -594,141 +440,66 @@ let hashmap_hash_map_remove_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) :
   result (hashmap_hash_map_t t)
   =
-  begin match hashmap_hash_key_fwd key with
-  | Fail e -> Fail e
-  | Return hash ->
-    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
-    begin match usize_rem hash i with
-    | Fail e -> Fail e
-    | Return hash_mod ->
-      begin match
-        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
-          hash_mod with
-      | Fail e -> Fail e
-      | Return l ->
-        begin match hashmap_hash_map_remove_from_list_fwd t key l with
-        | Fail e -> Fail e
-        | Return x ->
-          begin match x with
-          | None ->
-            begin match hashmap_hash_map_remove_from_list_back t key l with
-            | Fail e -> Fail e
-            | Return l0 ->
-              begin match
-                vec_index_mut_back (hashmap_list_t t)
-                  self.hashmap_hash_map_slots hash_mod l0 with
-              | Fail e -> Fail e
-              | Return v ->
-                Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
-                  self.hashmap_hash_map_max_load_factor
-                  self.hashmap_hash_map_max_load v)
-              end
-            end
-          | Some x0 ->
-            begin match usize_sub self.hashmap_hash_map_num_entries 1 with
-            | Fail e -> Fail e
-            | Return i0 ->
-              begin match hashmap_hash_map_remove_from_list_back t key l with
-              | Fail e -> Fail e
-              | Return l0 ->
-                begin match
-                  vec_index_mut_back (hashmap_list_t t)
-                    self.hashmap_hash_map_slots hash_mod l0 with
-                | Fail e -> Fail e
-                | Return v ->
-                  Return (Mkhashmap_hash_map_t i0
-                    self.hashmap_hash_map_max_load_factor
-                    self.hashmap_hash_map_max_load v)
-                end
-              end
-            end
-          end
-        end
-      end
-    end
+  let* hash = hashmap_hash_key_fwd key in
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  let* hash_mod = usize_rem hash i in
+  let* l =
+    vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+    in
+  let* x = hashmap_hash_map_remove_from_list_fwd t key l in
+  begin match x with
+  | None ->
+    let* l0 = hashmap_hash_map_remove_from_list_back t key l in
+    let* v =
+      vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+      self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)
+  | Some x0 ->
+    let* i0 = usize_sub self.hashmap_hash_map_num_entries 1 in
+    let* l0 = hashmap_hash_map_remove_from_list_back t key l in
+    let* v =
+      vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+        hash_mod l0 in
+    Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
+      self.hashmap_hash_map_max_load v)
   end
 
 (** [hashmap_main::hashmap::test1] *)
 let hashmap_test1_fwd : result unit =
-  begin match hashmap_hash_map_new_fwd u64 with
-  | Fail e -> Fail e
-  | Return hm ->
-    begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with
-    | Fail e -> Fail e
-    | Return hm0 ->
-      begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with
-      | Fail e -> Fail e
-      | Return hm1 ->
-        begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with
-        | Fail e -> Fail e
-        | Return hm2 ->
-          begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with
-          | Fail e -> Fail e
-          | Return hm3 ->
-            begin match hashmap_hash_map_get_fwd u64 hm3 128 with
-            | Fail e -> Fail e
-            | Return i ->
-              if not (i = 18)
-              then Fail Failure
-              else
-                begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with
-                | Fail e -> Fail e
-                | Return hm4 ->
-                  begin match hashmap_hash_map_get_fwd u64 hm4 1024 with
-                  | Fail e -> Fail e
-                  | Return i0 ->
-                    if not (i0 = 56)
-                    then Fail Failure
-                    else
-                      begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with
-                      | Fail e -> Fail e
-                      | Return x ->
-                        begin match x with
-                        | None -> Fail Failure
-                        | Some x0 ->
-                          if not (x0 = 56)
-                          then Fail Failure
-                          else
-                            begin match
-                              hashmap_hash_map_remove_back u64 hm4 1024 with
-                            | Fail e -> Fail e
-                            | Return hm5 ->
-                              begin match hashmap_hash_map_get_fwd u64 hm5 0
-                                with
-                              | Fail e -> Fail e
-                              | Return i1 ->
-                                if not (i1 = 42)
-                                then Fail Failure
-                                else
-                                  begin match
-                                    hashmap_hash_map_get_fwd u64 hm5 128 with
-                                  | Fail e -> Fail e
-                                  | Return i2 ->
-                                    if not (i2 = 18)
-                                    then Fail Failure
-                                    else
-                                      begin match
-                                        hashmap_hash_map_get_fwd u64 hm5 1056
-                                        with
-                                      | Fail e -> Fail e
-                                      | Return i3 ->
-                                        if not (i3 = 256)
-                                        then Fail Failure
-                                        else Return ()
-                                      end
-                                  end
-                              end
-                            end
-                        end
-                      end
-                  end
-                end
-            end
-          end
-        end
-      end
-    end
-  end
+  let* hm = hashmap_hash_map_new_fwd u64 in
+  let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm 0 42 in
+  let* hm1 = hashmap_hash_map_insert_fwd_back u64 hm0 128 18 in
+  let* hm2 = hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 in
+  let* hm3 = hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 in
+  let* i = hashmap_hash_map_get_fwd u64 hm3 128 in
+  if not (i = 18)
+  then Fail Failure
+  else begin
+    let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in
+    let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in
+    if not (i0 = 56)
+    then Fail Failure
+    else begin
+      let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in
+      begin match x with
+      | None -> Fail Failure
+      | Some x0 ->
+        if not (x0 = 56)
+        then Fail Failure
+        else begin
+          let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in
+          let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in
+          if not (i1 = 42)
+          then Fail Failure
+          else begin
+            let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in
+            if not (i2 = 18)
+            then Fail Failure
+            else begin
+              let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in
+              if not (i3 = 256) then Fail Failure else Return () end end end
+      end end end
 
 (** Unit test for [hashmap_main::hashmap::test1] *)
 let _ = assert_norm (hashmap_test1_fwd = Return ())
@@ -736,18 +507,10 @@ let _ = assert_norm (hashmap_test1_fwd = Return ())
 (** [hashmap_main::insert_on_disk] *)
 let insert_on_disk_fwd
   (key : usize) (value : u64) (st : state) : result (state & unit) =
-  begin match hashmap_utils_deserialize_fwd st with
-  | Fail e -> Fail e
-  | Return (st0, hm) ->
-    begin match hashmap_hash_map_insert_fwd_back u64 hm key value with
-    | Fail e -> Fail e
-    | Return hm0 ->
-      begin match hashmap_utils_serialize_fwd hm0 st0 with
-      | Fail e -> Fail e
-      | Return (st1, _) -> Return (st1, ())
-      end
-    end
-  end
+  let* (st0, hm) = hashmap_utils_deserialize_fwd st in
+  let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm key value in
+  let* (st1, _) = hashmap_utils_serialize_fwd hm0 st0 in
+  Return (st1, ())
 
 (** [hashmap_main::main] *)
 let main_fwd : result unit = Return ()
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index bf0f9078..98a696b6 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/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