Regenerate the F* files for hashmap_main.rs

1 files changed, 241 insertions, 180 deletions

diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index a4167186..1b281acb 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -92,7 +92,7 @@ let rec hashmap_hash_map_clear_slots_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let rec hashmap_hash_map_clear_slots_back
   (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) :
-  Tot (result (state & (vec (hashmap_list_t t))))
+  Tot (result (vec (hashmap_list_t t)))
   (decreases (hashmap_hash_map_clear_slots_decreases t slots i st))
   =
   let i0 = vec_len (hashmap_list_t t) slots in
@@ -107,11 +107,11 @@ let rec hashmap_hash_map_clear_slots_back
       | Return i1 ->
         begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with
         | Fail -> Fail
-        | Return (st0, slots1) -> Return (st0, slots1)
+        | Return slots1 -> Return slots1
         end
       end
     end
-  else Return (st, slots)
+  else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 let hashmap_hash_map_clear_fwd
@@ -127,13 +127,13 @@ let hashmap_hash_map_clear_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 let hashmap_hash_map_clear_back
   (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  result (hashmap_hash_map_t t)
   =
   begin match
     hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with
   | Fail -> Fail
-  | Return (st0, v) ->
-    Return (st0, Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
+  | Return v ->
+    Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
       self.hashmap_hash_map_max_load v)
   end
 
@@ -165,20 +165,20 @@ let rec hashmap_hash_map_insert_in_list_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
 let rec hashmap_hash_map_insert_in_list_back
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
-  Tot (result (state & (hashmap_list_t t)))
+  Tot (result (hashmap_list_t t))
   (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
   =
   begin match ls with
   | HashmapListCons ckey cvalue ls0 ->
     if ckey = key
-    then Return (st, HashmapListCons ckey value ls0)
+    then Return (HashmapListCons ckey value ls0)
     else
       begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
       | Fail -> Fail
-      | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
+      | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
       end
   | HashmapListNil ->
-    let l = HashmapListNil in Return (st, HashmapListCons key value l)
+    let l = HashmapListNil in Return (HashmapListCons key value l)
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
@@ -218,7 +218,7 @@ let hashmap_hash_map_insert_no_resize_fwd
 let hashmap_hash_map_insert_no_resize_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
   (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key st with
   | Fail -> Fail
@@ -234,39 +234,38 @@ let hashmap_hash_map_insert_no_resize_back
       | Return l ->
         begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
         | Fail -> Fail
-        | Return (st1, inserted) ->
+        | Return (_, inserted) ->
           if inserted
           then
             begin match usize_add self.hashmap_hash_map_num_entries 1 with
             | Fail -> Fail
             | Return i0 ->
               begin match
-                hashmap_hash_map_insert_in_list_back t key value l st1 with
+                hashmap_hash_map_insert_in_list_back t key value l st0 with
               | Fail -> Fail
-              | Return (st2, l0) ->
+              | Return l0 ->
                 begin match
                   vec_index_mut_back (hashmap_list_t t)
                     self.hashmap_hash_map_slots hash_mod l0 with
                 | Fail -> Fail
                 | Return v ->
-                  Return (st2, Mkhashmap_hash_map_t i0
+                  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 st1
+            begin match hashmap_hash_map_insert_in_list_back t key value l st0
               with
             | Fail -> Fail
-            | Return (st2, l0) ->
+            | Return l0 ->
               begin match
                 vec_index_mut_back (hashmap_list_t t)
                   self.hashmap_hash_map_slots hash_mod l0 with
               | Fail -> Fail
               | Return v ->
-                Return (st2, Mkhashmap_hash_map_t
-                  self.hashmap_hash_map_num_entries
+                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
@@ -286,13 +285,17 @@ let rec hashmap_hash_map_move_elements_from_list_fwd
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
+    begin match hashmap_hash_map_insert_no_resize_fwd t ntable k v st with
     | Fail -> Fail
-    | Return (st0, ntable0) ->
-      begin match hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0
-        with
+    | Return (st0, _) ->
+      begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
       | Fail -> Fail
-      | Return (st1, _) -> Return (st1, ())
+      | Return ntable0 ->
+        begin match
+          hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0 with
+        | Fail -> Fail
+        | Return (st1, _) -> Return (st1, ())
+        end
       end
     end
   | HashmapListNil -> Return (st, ())
@@ -302,22 +305,26 @@ let rec hashmap_hash_map_move_elements_from_list_fwd
 let rec hashmap_hash_map_move_elements_from_list_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
   (st : state) :
-  Tot (result (state & (hashmap_hash_map_t t)))
+  Tot (result (hashmap_hash_map_t t))
   (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls
   st))
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
+    begin match hashmap_hash_map_insert_no_resize_fwd t ntable k v st with
     | Fail -> Fail
-    | Return (st0, ntable0) ->
-      begin match
-        hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
+    | Return (st0, _) ->
+      begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
       | Fail -> Fail
-      | Return (st1, ntable1) -> Return (st1, ntable1)
+      | Return ntable0 ->
+        begin match
+          hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
+        | Fail -> Fail
+        | Return ntable1 -> Return ntable1
+        end
       end
     end
-  | HashmapListNil -> Return (st, ntable)
+  | HashmapListNil -> Return ntable
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
@@ -334,21 +341,26 @@ let rec hashmap_hash_map_move_elements_fwd
     | Fail -> Fail
     | Return l ->
       let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
+      begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st
         with
       | Fail -> Fail
-      | Return (st0, ntable0) ->
-        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
+      | Return (st0, _) ->
+        begin match
+          hashmap_hash_map_move_elements_from_list_back t ntable ls st with
         | Fail -> Fail
-        | Return slots0 ->
-          begin match usize_add i 1 with
+        | Return ntable0 ->
+          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 -> Fail
-          | Return i1 ->
-            begin match
-              hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
+          | Return slots0 ->
+            begin match usize_add i 1 with
             | Fail -> Fail
-            | Return (st1, _) -> Return (st1, ())
+            | Return i1 ->
+              begin match
+                hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
+              | Fail -> Fail
+              | Return (st1, _) -> Return (st1, ())
+              end
             end
           end
         end
@@ -360,7 +372,7 @@ let rec hashmap_hash_map_move_elements_fwd
 let rec hashmap_hash_map_move_elements_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
   (i : usize) (st : state) :
-  Tot (result (state & ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))))
+  Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t))))
   (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
   =
   let i0 = vec_len (hashmap_list_t t) slots in
@@ -370,28 +382,33 @@ let rec hashmap_hash_map_move_elements_back
     | Fail -> Fail
     | Return l ->
       let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
+      begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st
         with
       | Fail -> Fail
-      | Return (st0, ntable0) ->
-        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
+      | Return (st0, _) ->
+        begin match
+          hashmap_hash_map_move_elements_from_list_back t ntable ls st with
         | Fail -> Fail
-        | Return slots0 ->
-          begin match usize_add i 1 with
+        | Return ntable0 ->
+          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 -> Fail
-          | Return i1 ->
-            begin match
-              hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 with
+          | Return slots0 ->
+            begin match usize_add i 1 with
             | Fail -> Fail
-            | Return (st1, (ntable1, slots1)) ->
-              Return (st1, (ntable1, slots1))
+            | Return i1 ->
+              begin match
+                hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0
+                with
+              | Fail -> Fail
+              | Return (ntable1, slots1) -> Return (ntable1, slots1)
+              end
             end
           end
         end
       end
     end
-  else Return (st, (ntable, slots))
+  else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_fwd
@@ -415,10 +432,16 @@ let hashmap_hash_map_try_resize_fwd
           | Fail -> Fail
           | Return (st0, ntable) ->
             begin match
-              hashmap_hash_map_move_elements_back t ntable
+              hashmap_hash_map_move_elements_fwd t ntable
                 self.hashmap_hash_map_slots 0 st0 with
             | Fail -> Fail
-            | Return (st1, (_, _)) -> Return (st1, ())
+            | Return (st1, _) ->
+              begin match
+                hashmap_hash_map_move_elements_back t ntable
+                  self.hashmap_hash_map_slots 0 st0 with
+              | Fail -> Fail
+              | Return (_, _) -> Return (st1, ())
+              end
             end
           end
         end
@@ -429,7 +452,7 @@ let hashmap_hash_map_try_resize_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_back
   (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  result (hashmap_hash_map_t t)
   =
   let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
   begin match usize_div 4294967295 2 with
@@ -451,17 +474,16 @@ let hashmap_hash_map_try_resize_back
               hashmap_hash_map_move_elements_back t ntable
                 self.hashmap_hash_map_slots 0 st0 with
             | Fail -> Fail
-            | Return (st1, (ntable0, _)) ->
-              Return (st1, Mkhashmap_hash_map_t
-                self.hashmap_hash_map_num_entries (i, i0)
-                ntable0.hashmap_hash_map_max_load
+            | 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 (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (
-          i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+        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
 
@@ -471,24 +493,28 @@ let hashmap_hash_map_insert_fwd
   (st : state) :
   result (state & unit)
   =
-  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+  begin match hashmap_hash_map_insert_no_resize_fwd t self key value st with
   | Fail -> Fail
-  | Return (st0, self0) ->
-    begin match hashmap_hash_map_len_fwd t self0 st0 with
+  | Return (st0, _) ->
+    begin match hashmap_hash_map_insert_no_resize_back t self key value st with
     | Fail -> Fail
-    | Return (st1, i) ->
-      if i > self0.hashmap_hash_map_max_load
-      then
-        begin match
-          hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
-            self0.hashmap_hash_map_num_entries
-            self0.hashmap_hash_map_max_load_factor
-            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
-            st1 with
-        | Fail -> Fail
-        | Return (st2, _) -> Return (st2, ())
-        end
-      else Return (st1, ())
+    | Return self0 ->
+      begin match hashmap_hash_map_len_fwd t self0 st0 with
+      | Fail -> Fail
+      | Return (st1, i) ->
+        if i > self0.hashmap_hash_map_max_load
+        then
+          begin match
+            hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
+              self0.hashmap_hash_map_num_entries
+              self0.hashmap_hash_map_max_load_factor
+              self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1
+            with
+          | Fail -> Fail
+          | Return (st2, _) -> Return (st2, ())
+          end
+        else Return (st1, ())
+      end
     end
   end
 
@@ -496,29 +522,33 @@ let hashmap_hash_map_insert_fwd
 let hashmap_hash_map_insert_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
   (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  result (hashmap_hash_map_t t)
   =
-  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+  begin match hashmap_hash_map_insert_no_resize_fwd t self key value st with
   | Fail -> Fail
-  | Return (st0, self0) ->
-    begin match hashmap_hash_map_len_fwd t self0 st0 with
+  | Return (st0, _) ->
+    begin match hashmap_hash_map_insert_no_resize_back t self key value st with
     | Fail -> Fail
-    | Return (st1, i) ->
-      if i > self0.hashmap_hash_map_max_load
-      then
-        begin match
-          hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
-            self0.hashmap_hash_map_num_entries
+    | Return self0 ->
+      begin match hashmap_hash_map_len_fwd t self0 st0 with
+      | Fail -> Fail
+      | Return (st1, i) ->
+        if i > self0.hashmap_hash_map_max_load
+        then
+          begin match
+            hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
+              self0.hashmap_hash_map_num_entries
+              self0.hashmap_hash_map_max_load_factor
+              self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1
+            with
+          | Fail -> Fail
+          | Return self1 -> Return self1
+          end
+        else
+          Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
             self0.hashmap_hash_map_max_load_factor
-            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
-            st1 with
-        | Fail -> Fail
-        | Return (st2, self1) -> Return (st2, self1)
-        end
-      else
-        Return (st1, Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
-          self0.hashmap_hash_map_max_load_factor
-          self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+      end
     end
   end
 
@@ -628,18 +658,18 @@ let rec hashmap_hash_map_get_mut_in_list_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_back
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) (st : state) :
-  Tot (result (state & (hashmap_list_t t)))
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) (ret : t) :
+  Tot (result (hashmap_list_t t))
   (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
   =
   begin match ls with
   | HashmapListCons ckey cvalue ls0 ->
     if ckey = key
-    then Return (st, HashmapListCons ckey ret ls0)
+    then Return (HashmapListCons ckey ret ls0)
     else
-      begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with
+      begin match hashmap_hash_map_get_mut_in_list_back t key ls0 st ret with
       | Fail -> Fail
-      | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
+      | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
       end
   | HashmapListNil -> Fail
   end
@@ -671,9 +701,9 @@ let hashmap_hash_map_get_mut_fwd
 
 (** [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)
-  (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state)
+  (ret : t) :
+  result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key st with
   | Fail -> Fail
@@ -687,15 +717,15 @@ let hashmap_hash_map_get_mut_back
           hash_mod with
       | Fail -> Fail
       | Return l ->
-        begin match hashmap_hash_map_get_mut_in_list_back t key l ret st0 with
+        begin match hashmap_hash_map_get_mut_in_list_back t key l st0 ret with
         | Fail -> Fail
-        | Return (st1, l0) ->
+        | Return l0 ->
           begin match
             vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
               hash_mod l0 with
           | Fail -> Fail
           | Return v ->
-            Return (st1, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+            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
@@ -732,7 +762,7 @@ let rec hashmap_hash_map_remove_from_list_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_back
   (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
-  Tot (result (state & (hashmap_list_t t)))
+  Tot (result (hashmap_list_t t))
   (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
   =
   begin match ls with
@@ -743,15 +773,15 @@ let rec hashmap_hash_map_remove_from_list_back
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i cvalue tl0 -> Return (st, tl0)
+      | HashmapListCons i cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail
       end
     else
       begin match hashmap_hash_map_remove_from_list_back t key tl st with
       | Fail -> Fail
-      | Return (st0, tl0) -> Return (st0, HashmapListCons ckey x tl0)
+      | Return tl0 -> Return (HashmapListCons ckey x tl0)
       end
-  | HashmapListNil -> Return (st, HashmapListNil)
+  | HashmapListNil -> Return HashmapListNil
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
@@ -790,7 +820,7 @@ let hashmap_hash_map_remove_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
 let hashmap_hash_map_remove_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
-  result (state & (hashmap_hash_map_t t))
+  result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key st with
   | Fail -> Fail
@@ -806,19 +836,18 @@ let hashmap_hash_map_remove_back
       | Return l ->
         begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with
         | Fail -> Fail
-        | Return (st1, x) ->
+        | Return (_, x) ->
           begin match x with
           | None ->
-            begin match hashmap_hash_map_remove_from_list_back t key l st1 with
+            begin match hashmap_hash_map_remove_from_list_back t key l st0 with
             | Fail -> Fail
-            | Return (st2, l0) ->
+            | Return l0 ->
               begin match
                 vec_index_mut_back (hashmap_list_t t)
                   self.hashmap_hash_map_slots hash_mod l0 with
               | Fail -> Fail
               | Return v ->
-                Return (st2, Mkhashmap_hash_map_t
-                  self.hashmap_hash_map_num_entries
+                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
@@ -827,16 +856,16 @@ let hashmap_hash_map_remove_back
             begin match usize_sub self.hashmap_hash_map_num_entries 1 with
             | Fail -> Fail
             | Return i0 ->
-              begin match hashmap_hash_map_remove_from_list_back t key l st1
+              begin match hashmap_hash_map_remove_from_list_back t key l st0
                 with
               | Fail -> Fail
-              | Return (st2, l0) ->
+              | Return l0 ->
                 begin match
                   vec_index_mut_back (hashmap_list_t t)
                     self.hashmap_hash_map_slots hash_mod l0 with
                 | Fail -> Fail
                 | Return v ->
-                  Return (st2, Mkhashmap_hash_map_t i0
+                  Return (Mkhashmap_hash_map_t i0
                     self.hashmap_hash_map_max_load_factor
                     self.hashmap_hash_map_max_load v)
                 end
@@ -853,80 +882,108 @@ let hashmap_test1_fwd (st : state) : result (state & unit) =
   begin match hashmap_hash_map_new_fwd u64 st with
   | Fail -> Fail
   | Return (st0, hm) ->
-    begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with
+    begin match hashmap_hash_map_insert_fwd u64 hm 0 42 st0 with
     | Fail -> Fail
-    | Return (st1, hm0) ->
-      begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with
+    | Return (st1, _) ->
+      begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with
       | Fail -> Fail
-      | Return (st2, hm1) ->
-        begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2 with
+      | Return hm0 ->
+        begin match hashmap_hash_map_insert_fwd u64 hm0 128 18 st1 with
         | Fail -> Fail
-        | Return (st3, hm2) ->
-          begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3 with
+        | Return (st2, _) ->
+          begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with
           | Fail -> Fail
-          | Return (st4, hm3) ->
-            begin match hashmap_hash_map_get_fwd u64 hm3 128 st4 with
+          | Return hm1 ->
+            begin match hashmap_hash_map_insert_fwd u64 hm1 1024 138 st2 with
             | Fail -> Fail
-            | Return (st5, i) ->
-              if not (i = 18)
-              then Fail
-              else
-                begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 st5
+            | Return (st3, _) ->
+              begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2
+                with
+              | Fail -> Fail
+              | Return hm2 ->
+                begin match hashmap_hash_map_insert_fwd u64 hm2 1056 256 st3
                   with
                 | Fail -> Fail
-                | Return (st6, hm4) ->
-                  begin match hashmap_hash_map_get_fwd u64 hm4 1024 st6 with
+                | Return (st4, _) ->
+                  begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3
+                    with
                   | Fail -> Fail
-                  | Return (st7, i0) ->
-                    if not (i0 = 56)
-                    then Fail
-                    else
-                      begin match hashmap_hash_map_remove_fwd u64 hm4 1024 st7
-                        with
-                      | Fail -> Fail
-                      | Return (st8, x) ->
-                        begin match x with
-                        | None -> Fail
-                        | Some x0 ->
-                          if not (x0 = 56)
-                          then Fail
-                          else
+                  | Return hm3 ->
+                    begin match hashmap_hash_map_get_fwd u64 hm3 128 st4 with
+                    | Fail -> Fail
+                    | Return (st5, i) ->
+                      if not (i = 18)
+                      then Fail
+                      else
+                        begin match
+                          hashmap_hash_map_get_mut_fwd u64 hm3 1024 st5 with
+                        | Fail -> Fail
+                        | Return (st6, _) ->
+                          begin match
+                            hashmap_hash_map_get_mut_back u64 hm3 1024 st5 56
+                            with
+                          | Fail -> Fail
+                          | Return hm4 ->
                             begin match
-                              hashmap_hash_map_remove_back u64 hm4 1024 st8
-                              with
+                              hashmap_hash_map_get_fwd u64 hm4 1024 st6 with
                             | Fail -> Fail
-                            | Return (st9, hm5) ->
-                              begin match
-                                hashmap_hash_map_get_fwd u64 hm5 0 st9 with
-                              | Fail -> Fail
-                              | Return (st10, i1) ->
-                                if not (i1 = 42)
-                                then Fail
-                                else
-                                  begin match
-                                    hashmap_hash_map_get_fwd u64 hm5 128 st10
-                                    with
-                                  | Fail -> Fail
-                                  | Return (st11, i2) ->
-                                    if not (i2 = 18)
+                            | Return (st7, i0) ->
+                              if not (i0 = 56)
+                              then Fail
+                              else
+                                begin match
+                                  hashmap_hash_map_remove_fwd u64 hm4 1024 st7
+                                  with
+                                | Fail -> Fail
+                                | Return (st8, x) ->
+                                  begin match x with
+                                  | None -> Fail
+                                  | Some x0 ->
+                                    if not (x0 = 56)
                                     then Fail
                                     else
                                       begin match
-                                        hashmap_hash_map_get_fwd u64 
-                                          hm5 1056 st11 with
+                                        hashmap_hash_map_remove_back u64 hm4
+                                          1024 st7 with
                                       | Fail -> Fail
-                                      | Return (st12, i3) ->
-                                        if not (i3 = 256)
-                                        then Fail
-                                        else Return (st12, ())
+                                      | Return hm5 ->
+                                        begin match
+                                          hashmap_hash_map_get_fwd u64 hm5 0
+                                            st8 with
+                                        | Fail -> Fail
+                                        | Return (st9, i1) ->
+                                          if not (i1 = 42)
+                                          then Fail
+                                          else
+                                            begin match
+                                              hashmap_hash_map_get_fwd u64 hm5
+                                                128 st9 with
+                                            | Fail -> Fail
+                                            | Return (st10, i2) ->
+                                              if not (i2 = 18)
+                                              then Fail
+                                              else
+                                                begin match
+                                                  hashmap_hash_map_get_fwd u64
+                                                    hm5 1056 st10 with
+                                                | Fail -> Fail
+                                                | Return (st11, i3) ->
+                                                  if not (i3 = 256)
+                                                  then Fail
+                                                  else Return (st11, ())
+                                                end
+                                            end
+                                        end
                                       end
                                   end
-                              end
+                                end
                             end
+                          end
                         end
-                      end
+                    end
                   end
                 end
+              end
             end
           end
         end
@@ -940,12 +997,16 @@ let insert_on_disk_fwd
   begin match hashmap_utils_deserialize_fwd st with
   | Fail -> Fail
   | Return (st0, hm) ->
-    begin match hashmap_hash_map_insert_back u64 hm key value st0 with
+    begin match hashmap_hash_map_insert_fwd u64 hm key value st0 with
     | Fail -> Fail
-    | Return (st1, hm0) ->
-      begin match hashmap_utils_serialize_fwd hm0 st1 with
+    | Return (st1, _) ->
+      begin match hashmap_hash_map_insert_back u64 hm key value st0 with
       | Fail -> Fail
-      | Return (st2, _) -> Return (st2, ())
+      | Return hm0 ->
+        begin match hashmap_utils_serialize_fwd hm0 st1 with
+        | Fail -> Fail
+        | Return (st2, _) -> Return (st2, ())
+        end
       end
     end
   end