Do not introduce match on the fuel for non-recursive functions

1 files changed, 158 insertions, 225 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 94a390df..295ec489 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -37,29 +37,20 @@ Definition hashmap_hash_map_new_with_capacity_fwd
   (max_load_divisor : usize) :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let v := vec_new (Hashmap_list_t T) in
-    slots <- hashmap_hash_map_allocate_slots_fwd T n0 v capacity;
-    i <- usize_mul capacity max_load_dividend;
-    i0 <- usize_div i max_load_divisor;
-    Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend,
-      max_load_divisor) i0 slots)
-  end
+  let v := vec_new (Hashmap_list_t T) in
+  slots <- hashmap_hash_map_allocate_slots_fwd T n v capacity;
+  i <- usize_mul capacity max_load_dividend;
+  i0 <- usize_div i max_load_divisor;
+  Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend, max_load_divisor)
+    i0 slots)
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 Definition hashmap_hash_map_new_fwd
   (T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <-
-      hashmap_hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize)
-        (5%usize);
-    Return hm
-  end
+  hm <-
+    hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize);
+  Return hm
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
@@ -86,16 +77,11 @@ Definition hashmap_hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    v <-
-      hashmap_hash_map_clear_slots_fwd_back T n0 self.(Hashmap_hash_map_slots)
-        (0%usize);
-    Return (mkHashmap_hash_map_t (0%usize)
-      self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load)
-      v)
-  end
+  v <-
+    hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots)
+      (0%usize);
+  Return (mkHashmap_hash_map_t (0%usize)
+    self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
@@ -150,34 +136,29 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
   :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod;
-    inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l;
-    if inserted
-    then (
-      i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize;
-      l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
-      v <-
-        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-          hash_mod l0;
-      Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
-        self.(Hashmap_hash_map_max_load) v))
-    else (
-      l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
-      v <-
-        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-          hash_mod l0;
-      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
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <-
+    vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  inserted <- hashmap_hash_map_insert_in_list_fwd T n key value l;
+  if inserted
+  then (
+    i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize;
+    l0 <- hashmap_hash_map_insert_in_list_back T n key value l;
+    v <-
+      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod l0;
+    Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
+      self.(Hashmap_hash_map_max_load) v))
+  else (
+    l0 <- hashmap_hash_map_insert_in_list_back T n key value l;
+    v <-
+      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod l0;
+    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))
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -235,28 +216,24 @@ Definition hashmap_hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
-    let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    n1 <- usize_div max_usize 2%usize;
-    let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
-    i1 <- usize_div n1 i;
-    if capacity s<= i1
-    then (
-      i2 <- usize_mul capacity 2%usize;
-      ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i2 i i0;
-      p <-
-        hashmap_hash_map_move_elements_fwd_back T n0 ntable
-          self.(Hashmap_hash_map_slots) (0%usize);
-      let (ntable0, _) := p 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)))
-    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
+  max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+  let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  n1 <- usize_div max_usize 2%usize;
+  let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
+  i1 <- usize_div n1 i;
+  if capacity s<= i1
+  then (
+    i2 <- usize_mul capacity 2%usize;
+    ntable <- hashmap_hash_map_new_with_capacity_fwd T n i2 i i0;
+    p <-
+      hashmap_hash_map_move_elements_fwd_back T n ntable
+        self.(Hashmap_hash_map_slots) (0%usize);
+    let (ntable0, _) := p 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)))
+  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] *)
@@ -265,16 +242,11 @@ Definition hashmap_hash_map_insert_fwd_back
   :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 self key value;
-    i <- hashmap_hash_map_len_fwd T self0;
-    if i s> self0.(Hashmap_hash_map_max_load)
-    then (
-      self1 <- hashmap_hash_map_try_resize_fwd_back T n0 self0; Return self1)
-    else Return self0
-  end
+  self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n self key value;
+  i <- hashmap_hash_map_len_fwd T self0;
+  if i s> self0.(Hashmap_hash_map_max_load)
+  then (self1 <- hashmap_hash_map_try_resize_fwd_back T n self0; Return self1)
+  else Return self0
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
@@ -299,17 +271,12 @@ Definition hashmap_hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result bool
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-    b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l;
-    Return b
-  end
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  b <- hashmap_hash_map_contains_key_in_list_fwd T n key l;
+  Return b
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
@@ -333,17 +300,12 @@ Definition hashmap_hash_map_get_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result T
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-    t <- hashmap_hash_map_get_in_list_fwd T n0 key l;
-    Return t
-  end
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  t <- hashmap_hash_map_get_in_list_fwd T n key l;
+  Return t
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -387,18 +349,13 @@ Definition hashmap_hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result T
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod;
-    t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l;
-    Return t
-  end
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <-
+    vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  t <- hashmap_hash_map_get_mut_in_list_fwd T n key l;
+  Return t
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
@@ -406,23 +363,17 @@ Definition hashmap_hash_map_get_mut_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod;
-    l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret;
-    v <-
-      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod l0;
-    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
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <-
+    vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  l0 <- hashmap_hash_map_get_mut_in_list_back T n key l ret;
+  v <-
+    vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+      hash_mod l0;
+  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] *)
@@ -483,23 +434,18 @@ Definition hashmap_hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result (option T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod;
-    x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
-    match x with
-    | None => Return None
-    | Some x0 =>
-      i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
-      let _ := i0 in
-      Return (Some x0)
-    end
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <-
+    vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  x <- hashmap_hash_map_remove_from_list_fwd T n key l;
+  match x with
+  | None => Return None
+  | Some x0 =>
+    i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
+    let _ := i0 in
+    Return (Some x0)
   end
 .
 
@@ -508,91 +454,78 @@ Definition hashmap_hash_map_remove_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
   result (Hashmap_hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <-
-      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-        hash_mod;
-    x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
-    match x with
-    | None =>
-      l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
-      v <-
-        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-          hash_mod l0;
-      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 =>
-      i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
-      l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
-      v <-
-        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
-          hash_mod l0;
-      Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
-        self.(Hashmap_hash_map_max_load) v)
-    end
+  hash <- hashmap_hash_key_fwd key;
+  let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <-
+    vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+  x <- hashmap_hash_map_remove_from_list_fwd T n key l;
+  match x with
+  | None =>
+    l0 <- hashmap_hash_map_remove_from_list_back T n key l;
+    v <-
+      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod l0;
+    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 =>
+    i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
+    l0 <- hashmap_hash_map_remove_from_list_back T n key l;
+    v <-
+      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod l0;
+    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] *)
 Definition hashmap_test1_fwd (n : nat) : result unit :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hashmap_hash_map_new_fwd u64 n0;
-    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
-    hm1 <- hashmap_hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
-    hm2 <- hashmap_hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
-    hm3 <- hashmap_hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
-    i <- hashmap_hash_map_get_fwd u64 n0 hm3 (128%usize);
-    if negb (i s= 18%u64)
+  hm <- hashmap_hash_map_new_fwd u64 n;
+  hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64);
+  hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64);
+  hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64);
+  hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64);
+  i <- hashmap_hash_map_get_fwd u64 n hm3 (128%usize);
+  if negb (i s= 18%u64)
+  then Fail_ Failure
+  else (
+    hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64);
+    i0 <- hashmap_hash_map_get_fwd u64 n hm4 (1024%usize);
+    if negb (i0 s= 56%u64)
     then Fail_ Failure
     else (
-      hm4 <- hashmap_hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
-      i0 <- hashmap_hash_map_get_fwd u64 n0 hm4 (1024%usize);
-      if negb (i0 s= 56%u64)
-      then Fail_ Failure
-      else (
-        x <- hashmap_hash_map_remove_fwd u64 n0 hm4 (1024%usize);
-        match x with
-        | None => Fail_ Failure
-        | Some x0 =>
-          if negb (x0 s= 56%u64)
+      x <- hashmap_hash_map_remove_fwd u64 n hm4 (1024%usize);
+      match x with
+      | None => Fail_ Failure
+      | Some x0 =>
+        if negb (x0 s= 56%u64)
+        then Fail_ Failure
+        else (
+          hm5 <- hashmap_hash_map_remove_back u64 n hm4 (1024%usize);
+          i1 <- hashmap_hash_map_get_fwd u64 n hm5 (0%usize);
+          if negb (i1 s= 42%u64)
           then Fail_ Failure
           else (
-            hm5 <- hashmap_hash_map_remove_back u64 n0 hm4 (1024%usize);
-            i1 <- hashmap_hash_map_get_fwd u64 n0 hm5 (0%usize);
-            if negb (i1 s= 42%u64)
+            i2 <- hashmap_hash_map_get_fwd u64 n hm5 (128%usize);
+            if negb (i2 s= 18%u64)
             then Fail_ Failure
             else (
-              i2 <- hashmap_hash_map_get_fwd u64 n0 hm5 (128%usize);
-              if negb (i2 s= 18%u64)
-              then Fail_ Failure
-              else (
-                i3 <- hashmap_hash_map_get_fwd u64 n0 hm5 (1056%usize);
-                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
-        end))
-  end
+              i3 <- hashmap_hash_map_get_fwd u64 n hm5 (1056%usize);
+              if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
+      end))
 .
 
 (** [hashmap_main::insert_on_disk] *)
 Definition insert_on_disk_fwd
   (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- hashmap_utils_deserialize_fwd st;
-    let (st0, hm) := p in
-    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm key value;
-    p0 <- hashmap_utils_serialize_fwd hm0 st0;
-    let (st1, _) := p0 in
-    Return (st1, tt)
-  end
+  p <- hashmap_utils_deserialize_fwd st;
+  let (st0, hm) := p in
+  hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm key value;
+  p0 <- hashmap_utils_serialize_fwd hm0 st0;
+  let (st1, _) := p0 in
+  Return (st1, tt)
 .
 
 (** [hashmap_main::main] *)