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

6 files changed, 527 insertions, 678 deletions

diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 75a6c0ce..b72fa078 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -18,7 +18,14 @@ type fun_info = {
   can_fail : bool;
       (* Not used yet: all the extracted functions use an error monad *)
   stateful : bool;
-  divergent : bool; (* Not used yet *)
+  can_diverge : bool;
+  (* The function can diverge if:
+     - it is recursive
+     - it contains a loop
+     - it calls a functions which can diverge
+  *)
+  is_rec : bool;
+      (* [true] if the function is recursive (or in a mutually recursive group) *)
 }
 [@@deriving show]
 
@@ -48,7 +55,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       fun_info =
     let can_fail = ref false in
     let stateful = ref false in
-    let divergent = ref false in
+    let can_diverge = ref false in
+    let is_rec = ref false in
 
     let visit_fun (f : fun_decl) : unit =
       let obj =
@@ -70,14 +78,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
           method! visit_Call env call =
             (match call.func with
             | Regular id ->
-                if FunDeclId.Set.mem id fun_ids then divergent := true
+                if FunDeclId.Set.mem id fun_ids then (
+                  can_diverge := true;
+                  is_rec := true)
                 else
                   let info = FunDeclId.Map.find id !infos in
                   self#may_fail info.can_fail;
                   stateful := !stateful || info.stateful;
-                  divergent := !divergent || info.divergent
+                  can_diverge := !can_diverge || info.can_diverge
             | Assumed id ->
-                (* None of the assumed functions is stateful for now *)
+                (* None of the assumed functions can diverge nor are considered stateful *)
                 can_fail := !can_fail || Assumed.assumed_can_fail id);
             super#visit_Call env call
 
@@ -86,7 +96,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
             super#visit_Panic env
 
           method! visit_Loop env loop =
-            divergent := true;
+            can_diverge := true;
             super#visit_Loop env loop
         end
       in
@@ -110,7 +120,12 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
      * However, we do keep the result of the analysis for global bodies.
      * *)
     can_fail := (not is_global_decl_body) || !can_fail;
-    { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
+    {
+      can_fail = !can_fail;
+      stateful = !stateful;
+      can_diverge = !can_diverge;
+      is_rec = !is_rec;
+    }
   in
 
   let analyze_fun_decl_group (d : fun_declaration_group) : unit =
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 11f627d7..d9d3a404 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -525,6 +525,8 @@ type fun_effect_info = {
   can_fail : bool;  (** [true] if the return type is a [result] *)
   can_diverge : bool;
       (** [true] if the function can diverge (i.e., not terminate) *)
+  is_rec : bool;
+      (** [true] if the function is recursive (or in a mutually recursive group) *)
 }
 
 (** Meta information about a function signature *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9d8724ab..3bd6c5b3 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -495,7 +495,17 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
   let abs_ids = list_ancestor_abstractions_ids ctx abs in
   List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
 
-(** Small utility *)
+(** Small utility.
+
+    Does the function *decrease* the fuel? [true] if recursive.
+ *)
+let function_decreases_fuel (info : fun_effect_info) : bool =
+  !Config.use_fuel && info.is_rec
+
+(** Small utility.
+
+    Does the function *use* the fuel? [true] if can diverge.
+ *)
 let function_uses_fuel (info : fun_effect_info) : bool =
   !Config.use_fuel && info.can_diverge
 
@@ -522,7 +532,8 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         can_fail = info.can_fail;
         stateful_group;
         stateful;
-        can_diverge = info.divergent;
+        can_diverge = info.can_diverge;
+        is_rec = info.is_rec;
       }
   | A.Assumed aid ->
       {
@@ -530,6 +541,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         stateful_group = false;
         stateful = false;
         can_diverge = false;
+        is_rec = false;
       }
 
 (** Translate a function signature.
@@ -1268,6 +1280,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             stateful_group = false;
             stateful = false;
             can_diverge = false;
+            is_rec = false;
           }
         in
         (ctx, Unop Not, effect_info, args, None)
@@ -1283,6 +1296,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 stateful_group = false;
                 stateful = false;
                 can_diverge = false;
+                is_rec = false;
               }
             in
             (ctx, Unop (Neg int_ty), effect_info, args, None)
@@ -1295,6 +1309,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             stateful_group = false;
             stateful = false;
             can_diverge = false;
+            is_rec = false;
           }
         in
         (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
@@ -1310,6 +1325,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                 stateful_group = false;
                 stateful = false;
                 can_diverge = false;
+                is_rec = false;
               }
             in
             (ctx, Binop (binop, int_ty0), effect_info, args, None)
@@ -1913,14 +1929,20 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
         let body =
-          if function_uses_fuel effect_info then wrap_in_match_fuel body ctx
+          if function_decreases_fuel effect_info then
+            wrap_in_match_fuel body ctx
           else body
         in
         (* Sanity check *)
         type_check_texpression ctx body;
         (* Introduce the fuel parameter, if necessary *)
         let fuel =
-          if function_uses_fuel effect_info then [ mk_fuel_var ctx.fuel0 ]
+          if function_uses_fuel effect_info then
+            let fuel_var =
+              if function_decreases_fuel effect_info then ctx.fuel0
+              else ctx.fuel
+            in
+            [ mk_fuel_var fuel_var ]
           else []
         in
         (* Introduce the forward input state (the state at call site of the
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index d60ef718..ddcff646 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -218,28 +218,24 @@ Definition betree_leaf_split_fwd
   (st : state) :
   result (state * Betree_internal_t)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_list_split_at_fwd (u64 * u64) n0 content
-        params.(Betree_params_split_size);
-    let (content0, content1) := p in
-    p0 <- betree_list_hd_fwd (u64 * u64) content1;
-    let (pivot, _) := p0 in
-    id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
-    node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
-    id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
-    p1 <- betree_store_leaf_node_fwd id0 content0 st;
-    let (st0, _) := p1 in
-    p2 <- betree_store_leaf_node_fwd id1 content1 st0;
-    let (st1, _) := p2 in
-    let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0
-      params.(Betree_params_split_size)) in
-    let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1
-      params.(Betree_params_split_size)) in
-    Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n1 n2)
-  end
+  p <-
+    betree_list_split_at_fwd (u64 * u64) n content
+      params.(Betree_params_split_size);
+  let (content0, content1) := p in
+  p0 <- betree_list_hd_fwd (u64 * u64) content1;
+  let (pivot, _) := p0 in
+  id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
+  node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
+  id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
+  p1 <- betree_store_leaf_node_fwd id0 content0 st;
+  let (st0, _) := p1 in
+  p2 <- betree_store_leaf_node_fwd id1 content1 st0;
+  let (st1, _) := p2 in
+  let n0 := BetreeNodeLeaf (mkBetree_leaf_t id0
+    params.(Betree_params_split_size)) in
+  let n1 := BetreeNodeLeaf (mkBetree_leaf_t id1
+    params.(Betree_params_split_size)) in
+  Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
 .
 
 (** [betree_main::betree::Leaf::{3}::split] *)
@@ -249,25 +245,21 @@ Definition betree_leaf_split_back
   (st : state) :
   result Betree_node_id_counter_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_list_split_at_fwd (u64 * u64) n0 content
-        params.(Betree_params_split_size);
-    let (content0, content1) := p in
-    p0 <- betree_list_hd_fwd (u64 * u64) content1;
-    let _ := p0 in
-    id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
-    node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
-    id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
-    p1 <- betree_store_leaf_node_fwd id0 content0 st;
-    let (st0, _) := p1 in
-    p2 <- betree_store_leaf_node_fwd id1 content1 st0;
-    let (_, _) := p2 in
-    node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
-    Return node_id_cnt1
-  end
+  p <-
+    betree_list_split_at_fwd (u64 * u64) n content
+      params.(Betree_params_split_size);
+  let (content0, content1) := p in
+  p0 <- betree_list_hd_fwd (u64 * u64) content1;
+  let _ := p0 in
+  id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
+  node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
+  id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
+  p1 <- betree_store_leaf_node_fwd id0 content0 st;
+  let (st0, _) := p1 in
+  p2 <- betree_store_leaf_node_fwd id1 content1 st0;
+  let (_, _) := p2 in
+  node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
+  Return node_id_cnt1
 .
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
@@ -641,58 +633,54 @@ Definition betree_node_apply_to_leaf_fwd_back
   (new_msg : Betree_message_t) :
   result (Betree_list_t (u64 * u64))
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings;
-    b <- betree_list_head_has_key_fwd u64 bindings0 key;
-    if b
-    then (
-      hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
-      match new_msg with
-      | BetreeMessageInsert v =>
-        bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-        bindings2 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-        bindings3 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2;
-        Return bindings3
-      | BetreeMessageDelete =>
-        bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      | BetreeMessageUpsert s =>
-        let (_, i) := hd in
-        v <- betree_upsert_update_fwd (Some i) s;
-        bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-        bindings2 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-        bindings3 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2;
-        Return bindings3
-      end)
-    else
-      match new_msg with
-      | BetreeMessageInsert v =>
-        bindings1 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      | BetreeMessageDelete =>
-        bindings1 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0;
-        Return bindings1
-      | BetreeMessageUpsert s =>
-        v <- betree_upsert_update_fwd None s;
-        bindings1 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      end
-  end
+  bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
+  b <- betree_list_head_has_key_fwd u64 bindings0 key;
+  if b
+  then (
+    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      bindings3 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
+      Return bindings3
+    | BetreeMessageDelete =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
+      Return bindings2
+    | BetreeMessageUpsert s =>
+      let (_, i) := hd in
+      v <- betree_upsert_update_fwd (Some i) s;
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      bindings3 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings2;
+      Return bindings3
+    end)
+  else
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      bindings2 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
+      Return bindings2
+    | BetreeMessageDelete =>
+      bindings1 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings0;
+      Return bindings1
+    | BetreeMessageUpsert s =>
+      v <- betree_upsert_update_fwd None s;
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      bindings2 <-
+        betree_node_lookup_mut_in_bindings_back n key bindings bindings1;
+      Return bindings2
+    end
 .
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
@@ -790,71 +778,65 @@ Definition betree_node_apply_to_internal_fwd_back
   (new_msg : Betree_message_t) :
   result (Betree_list_t (u64 * Betree_message_t))
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs;
-    b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key;
-    if b
-    then
-      match new_msg with
-      | BetreeMessageInsert i =>
-        msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
+  msgs0 <- betree_node_lookup_first_message_for_key_fwd n key msgs;
+  b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key;
+  if b
+  then
+    match new_msg with
+    | BetreeMessageInsert i =>
+      msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
+      msgs2 <-
+        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
+          BetreeMessageInsert i);
+      msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
+      Return msgs3
+    | BetreeMessageDelete =>
+      msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
+      msgs2 <-
+        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
+          BetreeMessageDelete);
+      msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2;
+      Return msgs3
+    | BetreeMessageUpsert s =>
+      p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0;
+      let (_, m) := p in
+      match m with
+      | BetreeMessageInsert prev =>
+        v <- betree_upsert_update_fwd (Some prev) s;
+        msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
         msgs2 <-
           betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
-            BetreeMessageInsert i);
+            BetreeMessageInsert v);
         msgs3 <-
-          betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
+          betree_node_lookup_first_message_for_key_back n key msgs msgs2;
         Return msgs3
       | BetreeMessageDelete =>
-        msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
+        v <- betree_upsert_update_fwd None s;
+        msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
         msgs2 <-
           betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
-            BetreeMessageDelete);
+            BetreeMessageInsert v);
         msgs3 <-
-          betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
+          betree_node_lookup_first_message_for_key_back n key msgs msgs2;
         Return msgs3
-      | BetreeMessageUpsert s =>
-        p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0;
-        let (_, m) := p in
-        match m with
-        | BetreeMessageInsert prev =>
-          v <- betree_upsert_update_fwd (Some prev) s;
-          msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
-          msgs2 <-
-            betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1
-              (key, BetreeMessageInsert v);
-          msgs3 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-          Return msgs3
-        | BetreeMessageDelete =>
-          v <- betree_upsert_update_fwd None s;
-          msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
-          msgs2 <-
-            betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1
-              (key, BetreeMessageInsert v);
-          msgs3 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-          Return msgs3
-        | BetreeMessageUpsert ufs =>
-          msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0;
-          msgs2 <-
-            betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1
-              (key, BetreeMessageUpsert s);
-          msgs3 <-
-            betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2;
-          msgs4 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs3;
-          Return msgs4
-        end
+      | BetreeMessageUpsert ufs =>
+        msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0;
+        msgs2 <-
+          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
+            BetreeMessageUpsert s);
+        msgs3 <-
+          betree_node_lookup_first_message_after_key_back n key msgs0 msgs2;
+        msgs4 <-
+          betree_node_lookup_first_message_for_key_back n key msgs msgs3;
+        Return msgs4
       end
-    else (
-      msgs1 <-
-        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
-          new_msg);
-      msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1;
-      Return msgs2)
-  end
+    end
+  else (
+    msgs1 <-
+      betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
+        new_msg);
+    msgs2 <- betree_node_lookup_first_message_for_key_back n key msgs msgs1;
+    Return msgs2)
 .
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
@@ -1099,20 +1081,16 @@ Definition betree_node_apply_fwd
   (new_msg : Betree_message_t) (st : state) :
   result (state * unit)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let l := BetreeListNil in
-    p <-
-      betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st;
-    let (st0, _) := p in
-    p0 <-
-      betree_node_apply_messages_back n0 self params node_id_cnt
-        (BetreeListCons (key, new_msg) l) st;
-    let (_, _) := p0 in
-    Return (st0, tt)
-  end
+  let l := BetreeListNil in
+  p <-
+    betree_node_apply_messages_fwd n self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st;
+  let (st0, _) := p in
+  p0 <-
+    betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st;
+  let (_, _) := p0 in
+  Return (st0, tt)
 .
 
 (** [betree_main::betree::Node::{5}::apply] *)
@@ -1122,16 +1100,12 @@ Definition betree_node_apply_back
   (new_msg : Betree_message_t) (st : state) :
   result (Betree_node_t * Betree_node_id_counter_t)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let l := BetreeListNil in
-    p <-
-      betree_node_apply_messages_back n0 self params node_id_cnt
-        (BetreeListCons (key, new_msg) l) st;
-    let (self0, node_id_cnt0) := p in
-    Return (self0, node_id_cnt0)
-  end
+  let l := BetreeListNil in
+  p <-
+    betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st;
+  let (self0, node_id_cnt0) := p in
+  Return (self0, node_id_cnt0)
 .
 
 (** [betree_main::betree::BeTree::{6}::new] *)
@@ -1154,21 +1128,15 @@ Definition betree_be_tree_apply_fwd
   (st : state) :
   result (state * unit)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_node_apply_fwd n0 self.(Betree_be_tree_root)
-        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
-        st;
-    let (st0, _) := p in
-    p0 <-
-      betree_node_apply_back n0 self.(Betree_be_tree_root)
-        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
-        st;
-    let (_, _) := p0 in
-    Return (st0, tt)
-  end
+  p <-
+    betree_node_apply_fwd n self.(Betree_be_tree_root)
+      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
+  let (st0, _) := p in
+  p0 <-
+    betree_node_apply_back n self.(Betree_be_tree_root)
+      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
+  let (_, _) := p0 in
+  Return (st0, tt)
 .
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
@@ -1177,16 +1145,11 @@ Definition betree_be_tree_apply_back
   (st : state) :
   result Betree_be_tree_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_node_apply_back n0 self.(Betree_be_tree_root)
-        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
-        st;
-    let (n1, nic) := p in
-    Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n1)
-  end
+  p <-
+    betree_node_apply_back n self.(Betree_be_tree_root)
+      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
+  let (n0, nic) := p in
+  Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n0)
 .
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
@@ -1194,15 +1157,11 @@ Definition betree_be_tree_insert_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result (state * unit)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st;
-    let _ := bt in
-    Return (st0, tt)
-  end
+  p <- betree_be_tree_apply_fwd n self key (BetreeMessageInsert value) st;
+  let (st0, _) := p in
+  bt <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
+  let _ := bt in
+  Return (st0, tt)
 .
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
@@ -1210,13 +1169,8 @@ Definition betree_be_tree_insert_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result Betree_be_tree_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <-
-      betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st;
-    Return self0
-  end
+  self0 <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
+  Return self0
 .
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
@@ -1224,15 +1178,11 @@ Definition betree_be_tree_delete_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result (state * unit)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st;
-    let _ := bt in
-    Return (st0, tt)
-  end
+  p <- betree_be_tree_apply_fwd n self key BetreeMessageDelete st;
+  let (st0, _) := p in
+  bt <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
+  let _ := bt in
+  Return (st0, tt)
 .
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
@@ -1240,12 +1190,8 @@ Definition betree_be_tree_delete_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result Betree_be_tree_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st;
-    Return self0
-  end
+  self0 <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
+  Return self0
 .
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
@@ -1254,15 +1200,11 @@ Definition betree_be_tree_upsert_fwd
   (upd : Betree_upsert_fun_state_t) (st : state) :
   result (state * unit)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st;
-    let _ := bt in
-    Return (st0, tt)
-  end
+  p <- betree_be_tree_apply_fwd n self key (BetreeMessageUpsert upd) st;
+  let (st0, _) := p in
+  bt <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
+  let _ := bt in
+  Return (st0, tt)
 .
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
@@ -1271,13 +1213,8 @@ Definition betree_be_tree_upsert_back
   (upd : Betree_upsert_fun_state_t) (st : state) :
   result Betree_be_tree_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <-
-      betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st;
-    Return self0
-  end
+  self0 <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
+  Return self0
 .
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
@@ -1285,13 +1222,9 @@ Definition betree_be_tree_lookup_fwd
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result (state * (option u64))
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_node_lookup_fwd n0 self.(Betree_be_tree_root) key st;
-    let (st0, opt) := p in
-    Return (st0, opt)
-  end
+  p <- betree_node_lookup_fwd n self.(Betree_be_tree_root) key st;
+  let (st0, opt) := p in
+  Return (st0, opt)
 .
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
@@ -1299,13 +1232,9 @@ Definition betree_be_tree_lookup_back
   (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
   result Betree_be_tree_t
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    n1 <- betree_node_lookup_back n0 self.(Betree_be_tree_root) key st;
-    Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
-      self.(Betree_be_tree_node_id_cnt) n1)
-  end
+  n0 <- betree_node_lookup_back n self.(Betree_be_tree_root) key st;
+  Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
+    self.(Betree_be_tree_node_id_cnt) n0)
 .
 
 (** [betree_main::main] *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d12ee1b9..17456d81 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -35,26 +35,18 @@ Definition hash_map_new_with_capacity_fwd
   (max_load_divisor : usize) :
   result (Hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let v := vec_new (List_t T) in
-    slots <- hash_map_allocate_slots_fwd T n0 v capacity;
-    i <- usize_mul capacity max_load_dividend;
-    i0 <- usize_div i max_load_divisor;
-    Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0
-      slots)
-  end
+  let v := vec_new (List_t T) in
+  slots <- hash_map_allocate_slots_fwd T n v capacity;
+  i <- usize_mul capacity max_load_dividend;
+  i0 <- usize_div i max_load_divisor;
+  Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0
+    slots)
 .
 
 (** [hashmap::HashMap::{0}::new] *)
 Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) (5%usize);
-    Return hm
-  end
+  hm <- hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize);
+  Return hm
 .
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
@@ -79,13 +71,9 @@ Fixpoint hash_map_clear_slots_fwd_back
 (** [hashmap::HashMap::{0}::clear] *)
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    v <- hash_map_clear_slots_fwd_back T n0 self.(Hash_map_slots) (0%usize);
-    Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
-      self.(Hash_map_max_load) v)
-  end
+  v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots) (0%usize);
+  Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
+    self.(Hash_map_max_load) v)
 .
 
 (** [hashmap::HashMap::{0}::len] *)
@@ -136,27 +124,23 @@ Definition hash_map_insert_no_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
   result (Hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    inserted <- hash_map_insert_in_list_fwd T n0 key value l;
-    if inserted
-    then (
-      i0 <- usize_add self.(Hash_map_num_entries) 1%usize;
-      l0 <- hash_map_insert_in_list_back T n0 key value l;
-      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-      Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
-        self.(Hash_map_max_load) v))
-    else (
-      l0 <- hash_map_insert_in_list_back T n0 key value l;
-      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-      Return (mkHash_map_t self.(Hash_map_num_entries)
-        self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v))
-  end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  inserted <- hash_map_insert_in_list_fwd T n key value l;
+  if inserted
+  then (
+    i0 <- usize_add self.(Hash_map_num_entries) 1%usize;
+    l0 <- hash_map_insert_in_list_back T n key value l;
+    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+    Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
+      self.(Hash_map_max_load) v))
+  else (
+    l0 <- hash_map_insert_in_list_back T n key value l;
+    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+    Return (mkHash_map_t self.(Hash_map_num_entries)
+      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v))
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -209,28 +193,24 @@ Fixpoint hash_map_move_elements_fwd_back
 (** [hashmap::HashMap::{0}::try_resize] *)
 Definition hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (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 (List_t T) self.(Hash_map_slots) in
-    n1 <- usize_div max_usize 2%usize;
-    let (i, i0) := self.(Hash_map_max_load_factor) in
-    i1 <- usize_div n1 i;
-    if capacity s<= i1
-    then (
-      i2 <- usize_mul capacity 2%usize;
-      ntable <- hash_map_new_with_capacity_fwd T n0 i2 i i0;
-      p <-
-        hash_map_move_elements_fwd_back T n0 ntable self.(Hash_map_slots)
-          (0%usize);
-      let (ntable0, _) := p in
-      Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
-        ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots)))
-    else
-      Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
-        self.(Hash_map_max_load) self.(Hash_map_slots))
-  end
+  max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+  let capacity := vec_len (List_t T) self.(Hash_map_slots) in
+  n1 <- usize_div max_usize 2%usize;
+  let (i, i0) := self.(Hash_map_max_load_factor) in
+  i1 <- usize_div n1 i;
+  if capacity s<= i1
+  then (
+    i2 <- usize_mul capacity 2%usize;
+    ntable <- hash_map_new_with_capacity_fwd T n i2 i i0;
+    p <-
+      hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots)
+        (0%usize);
+    let (ntable0, _) := p in
+    Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
+      ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots)))
+  else
+    Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
+      self.(Hash_map_max_load) self.(Hash_map_slots))
 .
 
 (** [hashmap::HashMap::{0}::insert] *)
@@ -238,15 +218,11 @@ Definition hash_map_insert_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
   result (Hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- hash_map_insert_no_resize_fwd_back T n0 self key value;
-    i <- hash_map_len_fwd T self0;
-    if i s> self0.(Hash_map_max_load)
-    then (self1 <- hash_map_try_resize_fwd_back T n0 self0; Return self1)
-    else Return self0
-  end
+  self0 <- hash_map_insert_no_resize_fwd_back T n self key value;
+  i <- hash_map_len_fwd T self0;
+  if i s> self0.(Hash_map_max_load)
+  then (self1 <- hash_map_try_resize_fwd_back T n self0; Return self1)
+  else Return self0
 .
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
@@ -268,16 +244,12 @@ Fixpoint hash_map_contains_key_in_list_fwd
 (** [hashmap::HashMap::{0}::contains_key] *)
 Definition hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    b <- hash_map_contains_key_in_list_fwd T n0 key l;
-    Return b
-  end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  b <- hash_map_contains_key_in_list_fwd T n key l;
+  Return b
 .
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
@@ -299,16 +271,12 @@ Fixpoint hash_map_get_in_list_fwd
 (** [hashmap::HashMap::{0}::get] *)
 Definition hash_map_get_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    t <- hash_map_get_in_list_fwd T n0 key l;
-    Return t
-  end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  t <- hash_map_get_in_list_fwd T n key l;
+  Return t
 .
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -350,16 +318,12 @@ Fixpoint hash_map_get_mut_in_list_back
 (** [hashmap::HashMap::{0}::get_mut] *)
 Definition hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    t <- hash_map_get_mut_in_list_fwd T n0 key l;
-    Return t
-  end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  t <- hash_map_get_mut_in_list_fwd T n key l;
+  Return t
 .
 
 (** [hashmap::HashMap::{0}::get_mut] *)
@@ -367,18 +331,14 @@ Definition hash_map_get_mut_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) :
   result (Hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    l0 <- hash_map_get_mut_in_list_back T n0 key l ret;
-    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-    Return (mkHash_map_t self.(Hash_map_num_entries)
-      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
-  end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  l0 <- hash_map_get_mut_in_list_back T n key l ret;
+  v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+  Return (mkHash_map_t self.(Hash_map_num_entries)
+    self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
 .
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
@@ -430,21 +390,17 @@ Definition hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
   result (option T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    x <- hash_map_remove_from_list_fwd T n0 key l;
-    match x with
-    | None => Return None
-    | Some x0 =>
-      i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
-      let _ := i0 in
-      Return (Some x0)
-    end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  x <- hash_map_remove_from_list_fwd T n key l;
+  match x with
+  | None => Return None
+  | Some x0 =>
+    i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
+    let _ := i0 in
+    Return (Some x0)
   end
 .
 
@@ -453,69 +409,61 @@ Definition hash_map_remove_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
   result (Hash_map_t T)
   :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    let i := vec_len (List_t T) self.(Hash_map_slots) in
-    hash_mod <- usize_rem hash i;
-    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
-    x <- hash_map_remove_from_list_fwd T n0 key l;
-    match x with
-    | None =>
-      l0 <- hash_map_remove_from_list_back T n0 key l;
-      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-      Return (mkHash_map_t self.(Hash_map_num_entries)
-        self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
-    | Some x0 =>
-      i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
-      l0 <- hash_map_remove_from_list_back T n0 key l;
-      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
-      Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
-        self.(Hash_map_max_load) v)
-    end
+  hash <- hash_key_fwd key;
+  let i := vec_len (List_t T) self.(Hash_map_slots) in
+  hash_mod <- usize_rem hash i;
+  l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+  x <- hash_map_remove_from_list_fwd T n key l;
+  match x with
+  | None =>
+    l0 <- hash_map_remove_from_list_back T n key l;
+    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+    Return (mkHash_map_t self.(Hash_map_num_entries)
+      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
+  | Some x0 =>
+    i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
+    l0 <- hash_map_remove_from_list_back T n key l;
+    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+    Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
+      self.(Hash_map_max_load) v)
   end
 .
 
 (** [hashmap::test1] *)
 Definition test1_fwd (n : nat) : result unit :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hash_map_new_fwd u64 n0;
-    hm0 <- hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
-    hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
-    hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
-    hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
-    i <- hash_map_get_fwd u64 n0 hm3 (128%usize);
-    if negb (i s= 18%u64)
+  hm <- hash_map_new_fwd u64 n;
+  hm0 <- hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64);
+  hm1 <- hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64);
+  hm2 <- hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64);
+  hm3 <- hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64);
+  i <- hash_map_get_fwd u64 n hm3 (128%usize);
+  if negb (i s= 18%u64)
+  then Fail_ Failure
+  else (
+    hm4 <- hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64);
+    i0 <- hash_map_get_fwd u64 n hm4 (1024%usize);
+    if negb (i0 s= 56%u64)
     then Fail_ Failure
     else (
-      hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
-      i0 <- hash_map_get_fwd u64 n0 hm4 (1024%usize);
-      if negb (i0 s= 56%u64)
-      then Fail_ Failure
-      else (
-        x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize);
-        match x with
-        | None => Fail_ Failure
-        | Some x0 =>
-          if negb (x0 s= 56%u64)
+      x <- 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 <- hash_map_remove_back u64 n hm4 (1024%usize);
+          i1 <- hash_map_get_fwd u64 n hm5 (0%usize);
+          if negb (i1 s= 42%u64)
           then Fail_ Failure
           else (
-            hm5 <- hash_map_remove_back u64 n0 hm4 (1024%usize);
-            i1 <- hash_map_get_fwd u64 n0 hm5 (0%usize);
-            if negb (i1 s= 42%u64)
+            i2 <- hash_map_get_fwd u64 n hm5 (128%usize);
+            if negb (i2 s= 18%u64)
             then Fail_ Failure
             else (
-              i2 <- hash_map_get_fwd u64 n0 hm5 (128%usize);
-              if negb (i2 s= 18%u64)
-              then Fail_ Failure
-              else (
-                i3 <- hash_map_get_fwd u64 n0 hm5 (1056%usize);
-                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
-        end))
-  end
+              i3 <- hash_map_get_fwd u64 n hm5 (1056%usize);
+              if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
+      end))
 .
 
 End Hashmap_Funs .
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] *)