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

3 files changed, 477 insertions, 667 deletions

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] *)