Generate hashmap_on_disk

1 files changed, 949 insertions, 0 deletions

diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
new file mode 100644
index 00000000..0eda588f
--- /dev/null
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -0,0 +1,949 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: function definitions *)
+module HashmapMain.Funs
+open Primitives
+include HashmapMain.Types
+include HashmapMain.Opaque
+include HashmapMain.Clauses
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap_main::hashmap::hash_key] *)
+let hashmap_hash_key_fwd (k : usize) (st : state) : result (state & usize) =
+  Return (st, k)
+
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+let rec hashmap_hash_map_allocate_slots_fwd
+  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) :
+  Tot (result (state & (vec (hashmap_list_t t))))
+  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st))
+  =
+  begin match n with
+  | 0 -> Return (st, slots)
+  | _ ->
+    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
+    | Fail -> Fail
+    | Return v ->
+      begin match usize_sub n 1 with
+      | Fail -> Fail
+      | Return i ->
+        begin match hashmap_hash_map_allocate_slots_fwd t v i st with
+        | Fail -> Fail
+        | Return (st0, v0) -> Return (st0, v0)
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+let hashmap_hash_map_new_with_capacity_fwd
+  (t : Type0) (capacity : usize) (max_load_dividend : usize)
+  (max_load_divisor : usize) (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  let v = vec_new (hashmap_list_t t) in
+  begin match hashmap_hash_map_allocate_slots_fwd t v capacity st with
+  | Fail -> Fail
+  | Return (st0, v0) ->
+    begin match usize_mul capacity max_load_dividend with
+    | Fail -> Fail
+    | Return i ->
+      begin match usize_div i max_load_divisor with
+      | Fail -> Fail
+      | Return i0 ->
+        Return (st0, Mkhashmap_hash_map_t 0 (max_load_dividend,
+          max_load_divisor) i0 v0)
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+let hashmap_hash_map_new_fwd
+  (t : Type0) (st : state) : result (state & (hashmap_hash_map_t t)) =
+  begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 st with
+  | Fail -> Fail
+  | Return (st0, hm) -> Return (st0, hm)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+let rec hashmap_hash_map_clear_slots_fwd
+  (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) :
+  Tot (result (state & unit))
+  (decreases (hashmap_hash_map_clear_slots_decreases t slots i st))
+  =
+  let i0 = vec_len (hashmap_list_t t) slots in
+  if i < i0
+  then
+    begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
+      with
+    | Fail -> Fail
+    | Return v ->
+      begin match usize_add i 1 with
+      | Fail -> Fail
+      | Return i1 ->
+        begin match hashmap_hash_map_clear_slots_fwd t v i1 st with
+        | Fail -> Fail
+        | Return (st0, _) -> Return (st0, ())
+        end
+      end
+    end
+  else Return (st, ())
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+let rec hashmap_hash_map_clear_slots_back
+  (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) :
+  Tot (result (state & (vec (hashmap_list_t t))))
+  (decreases (hashmap_hash_map_clear_slots_decreases t slots i st))
+  =
+  let i0 = vec_len (hashmap_list_t t) slots in
+  if i < i0
+  then
+    begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
+      with
+    | Fail -> Fail
+    | Return v ->
+      begin match usize_add i 1 with
+      | Fail -> Fail
+      | Return i1 ->
+        begin match hashmap_hash_map_clear_slots_back t v i1 st with
+        | Fail -> Fail
+        | Return (st0, v0) -> Return (st0, v0)
+        end
+      end
+    end
+  else Return (st, slots)
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+let hashmap_hash_map_clear_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
+  result (state & unit)
+  =
+  begin match
+    hashmap_hash_map_clear_slots_fwd t self.hashmap_hash_map_slots 0 st with
+  | Fail -> Fail
+  | Return (st0, _) -> Return (st0, ())
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+let hashmap_hash_map_clear_back
+  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  begin match
+    hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with
+  | Fail -> Fail
+  | Return (st0, v) ->
+    Return (st0, Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
+      self.hashmap_hash_map_max_load v)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+let hashmap_hash_map_len_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
+  result (state & usize)
+  =
+  Return (st, self.hashmap_hash_map_num_entries)
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+let rec hashmap_hash_map_insert_in_list_fwd
+  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & bool))
+  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey cvalue ls0 ->
+    if ckey = key
+    then Return (st, false)
+    else
+      begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 st with
+      | Fail -> Fail
+      | Return (st0, b) -> Return (st0, b)
+      end
+  | HashmapListNil -> Return (st, true)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+let rec hashmap_hash_map_insert_in_list_back
+  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & (hashmap_list_t t)))
+  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey cvalue ls0 ->
+    if ckey = key
+    then Return (st, HashmapListCons ckey value ls0)
+    else
+      begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
+      | Fail -> Fail
+      | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+      end
+  | HashmapListNil ->
+    let l = HashmapListNil in Return (st, HashmapListCons key value l)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+let hashmap_hash_map_insert_no_resize_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
+  (st : state) :
+  result (state & unit)
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
+        | Fail -> Fail
+        | Return (st1, b) ->
+          if b
+          then
+            begin match usize_add self.hashmap_hash_map_num_entries 1 with
+            | Fail -> Fail
+            | Return _ -> Return (st1, ())
+            end
+          else Return (st1, ())
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+let hashmap_hash_map_insert_no_resize_back
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
+  (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
+        | Fail -> Fail
+        | Return (st1, b) ->
+          if b
+          then
+            begin match usize_add self.hashmap_hash_map_num_entries 1 with
+            | Fail -> Fail
+            | Return i1 ->
+              begin match
+                hashmap_hash_map_insert_in_list_back t key value l st1 with
+              | Fail -> Fail
+              | Return (st2, l0) ->
+                begin match
+                  vec_index_mut_back (hashmap_list_t t)
+                    self.hashmap_hash_map_slots hash_mod l0 with
+                | Fail -> Fail
+                | Return v ->
+                  Return (st2, Mkhashmap_hash_map_t i1
+                    self.hashmap_hash_map_max_load_factor
+                    self.hashmap_hash_map_max_load v)
+                end
+              end
+            end
+          else
+            begin match hashmap_hash_map_insert_in_list_back t key value l st1
+              with
+            | Fail -> Fail
+            | Return (st2, l0) ->
+              begin match
+                vec_index_mut_back (hashmap_list_t t)
+                  self.hashmap_hash_map_slots hash_mod l0 with
+              | Fail -> Fail
+              | Return v ->
+                Return (st2, Mkhashmap_hash_map_t
+                  self.hashmap_hash_map_num_entries
+                  self.hashmap_hash_map_max_load_factor
+                  self.hashmap_hash_map_max_load v)
+              end
+            end
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+let rec hashmap_hash_map_move_elements_from_list_fwd
+  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
+  (st : state) :
+  Tot (result (state & unit))
+  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls
+  st))
+  =
+  begin match ls with
+  | HashmapListCons k v tl ->
+    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
+    | Fail -> Fail
+    | Return (st0, hm) ->
+      begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with
+      | Fail -> Fail
+      | Return (st1, _) -> Return (st1, ())
+      end
+    end
+  | HashmapListNil -> Return (st, ())
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+let rec hashmap_hash_map_move_elements_from_list_back
+  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
+  (st : state) :
+  Tot (result (state & (hashmap_hash_map_t t)))
+  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls
+  st))
+  =
+  begin match ls with
+  | HashmapListCons k v tl ->
+    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
+    | Fail -> Fail
+    | Return (st0, hm) ->
+      begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0
+        with
+      | Fail -> Fail
+      | Return (st1, hm0) -> Return (st1, hm0)
+      end
+    end
+  | HashmapListNil -> Return (st, ntable)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+let rec hashmap_hash_map_move_elements_fwd
+  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
+  (i : usize) (st : state) :
+  Tot (result (state & unit))
+  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
+  =
+  let i0 = vec_len (hashmap_list_t t) slots in
+  if i < i0
+  then
+    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
+    | Fail -> Fail
+    | Return l ->
+      let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+      begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+        with
+      | Fail -> Fail
+      | Return (st0, hm) ->
+        let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
+        begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
+        | Fail -> Fail
+        | Return v ->
+          begin match usize_add i 1 with
+          | Fail -> Fail
+          | Return i1 ->
+            begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with
+            | Fail -> Fail
+            | Return (st1, _) -> Return (st1, ())
+            end
+          end
+        end
+      end
+    end
+  else Return (st, ())
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+let rec hashmap_hash_map_move_elements_back
+  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
+  (i : usize) (st : state) :
+  Tot (result (state & ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))))
+  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
+  =
+  let i0 = vec_len (hashmap_list_t t) slots in
+  if i < i0
+  then
+    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
+    | Fail -> Fail
+    | Return l ->
+      let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
+      begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
+        with
+      | Fail -> Fail
+      | Return (st0, hm) ->
+        let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
+        begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
+        | Fail -> Fail
+        | Return v ->
+          begin match usize_add i 1 with
+          | Fail -> Fail
+          | Return i1 ->
+            begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with
+            | Fail -> Fail
+            | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0))
+            end
+          end
+        end
+      end
+    end
+  else Return (st, (ntable, slots))
+
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+let hashmap_hash_map_try_resize_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
+  result (state & unit)
+  =
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  begin match usize_div 4294967295 2 with
+  | Fail -> Fail
+  | Return n1 ->
+    let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+    begin match usize_div n1 i0 with
+    | Fail -> Fail
+    | Return i2 ->
+      if i <= i2
+      then
+        begin match usize_mul i 2 with
+        | Fail -> Fail
+        | Return i3 ->
+          begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+          | Fail -> Fail
+          | Return (st0, hm) ->
+            begin match
+              hashmap_hash_map_move_elements_back t hm
+                self.hashmap_hash_map_slots 0 st0 with
+            | Fail -> Fail
+            | Return (st1, (_, _)) -> Return (st1, ())
+            end
+          end
+        end
+      else Return (st, ())
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+let hashmap_hash_map_try_resize_back
+  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+  begin match usize_div 4294967295 2 with
+  | Fail -> Fail
+  | Return n1 ->
+    let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+    begin match usize_div n1 i0 with
+    | Fail -> Fail
+    | Return i2 ->
+      if i <= i2
+      then
+        begin match usize_mul i 2 with
+        | Fail -> Fail
+        | Return i3 ->
+          begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
+          | Fail -> Fail
+          | Return (st0, hm) ->
+            begin match
+              hashmap_hash_map_move_elements_back t hm
+                self.hashmap_hash_map_slots 0 st0 with
+            | Fail -> Fail
+            | Return (st1, (hm0, v)) ->
+              let v0 =
+                mem_replace_back (vec (hashmap_list_t t)) v
+                  hm0.hashmap_hash_map_slots in
+              Return (st1, Mkhashmap_hash_map_t
+                self.hashmap_hash_map_num_entries (i0, i1)
+                hm0.hashmap_hash_map_max_load v0)
+            end
+          end
+        end
+      else
+        Return (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (
+          i0, i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+let hashmap_hash_map_insert_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
+  (st : state) :
+  result (state & unit)
+  =
+  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+  | Fail -> Fail
+  | Return (st0, hm) ->
+    begin match hashmap_hash_map_len_fwd t hm st0 with
+    | Fail -> Fail
+    | Return (st1, i) ->
+      if i > hm.hashmap_hash_map_max_load
+      then
+        begin match
+          hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
+            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
+            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+        | Fail -> Fail
+        | Return (st2, _) -> Return (st2, ())
+        end
+      else Return (st1, ())
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+let hashmap_hash_map_insert_back
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
+  (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
+  | Fail -> Fail
+  | Return (st0, hm) ->
+    begin match hashmap_hash_map_len_fwd t hm st0 with
+    | Fail -> Fail
+    | Return (st1, i) ->
+      if i > hm.hashmap_hash_map_max_load
+      then
+        begin match
+          hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
+            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
+            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+        | Fail -> Fail
+        | Return (st2, hm0) -> Return (st2, hm0)
+        end
+      else
+        Return (st1, Mkhashmap_hash_map_t hm.hashmap_hash_map_num_entries
+          hm.hashmap_hash_map_max_load_factor hm.hashmap_hash_map_max_load
+          hm.hashmap_hash_map_slots)
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+let rec hashmap_hash_map_contains_key_in_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & bool))
+  (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey x ls0 ->
+    if ckey = key
+    then Return (st, true)
+    else
+      begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 st with
+      | Fail -> Fail
+      | Return (st0, b) -> Return (st0, b)
+      end
+  | HashmapListNil -> Return (st, false)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+let hashmap_hash_map_contains_key_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+  result (state & bool)
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+        with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_contains_key_in_list_fwd t key l st0 with
+        | Fail -> Fail
+        | Return (st1, b) -> Return (st1, b)
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+let rec hashmap_hash_map_get_in_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & t))
+  (decreases (hashmap_hash_map_get_in_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey cvalue ls0 ->
+    if ckey = key
+    then Return (st, cvalue)
+    else
+      begin match hashmap_hash_map_get_in_list_fwd t key ls0 st with
+      | Fail -> Fail
+      | Return (st0, x) -> Return (st0, x)
+      end
+  | HashmapListNil -> Fail
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get] *)
+let hashmap_hash_map_get_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+  result (state & t)
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
+        with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_get_in_list_fwd t key l st0 with
+        | Fail -> Fail
+        | Return (st1, x) -> Return (st1, x)
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+let rec hashmap_hash_map_get_mut_in_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & t))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey cvalue ls0 ->
+    if ckey = key
+    then Return (st, cvalue)
+    else
+      begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 st with
+      | Fail -> Fail
+      | Return (st0, x) -> Return (st0, x)
+      end
+  | HashmapListNil -> Fail
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+let rec hashmap_hash_map_get_mut_in_list_back
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) (st : state) :
+  Tot (result (state & (hashmap_list_t t)))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey cvalue ls0 ->
+    if ckey = key
+    then Return (st, HashmapListCons ckey ret ls0)
+    else
+      begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with
+      | Fail -> Fail
+      | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+      end
+  | HashmapListNil -> Fail
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+let hashmap_hash_map_get_mut_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+  result (state & t)
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_get_mut_in_list_fwd t key l st0 with
+        | Fail -> Fail
+        | Return (st1, x) -> Return (st1, x)
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+let hashmap_hash_map_get_mut_back
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t)
+  (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_get_mut_in_list_back t key l ret st0 with
+        | Fail -> Fail
+        | Return (st1, l0) ->
+          begin match
+            vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
+              hash_mod l0 with
+          | Fail -> Fail
+          | Return v ->
+            Return (st1, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+              self.hashmap_hash_map_max_load_factor
+              self.hashmap_hash_map_max_load v)
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+let rec hashmap_hash_map_remove_from_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & (option t)))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey x tl ->
+    if ckey = key
+    then
+      let mv_ls =
+        mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
+          HashmapListNil in
+      begin match mv_ls with
+      | HashmapListCons i cvalue tl0 -> Return (st, Some cvalue)
+      | HashmapListNil -> Fail
+      end
+    else
+      begin match hashmap_hash_map_remove_from_list_fwd t key tl st with
+      | Fail -> Fail
+      | Return (st0, opt) -> Return (st0, opt)
+      end
+  | HashmapListNil -> Return (st, None)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+let rec hashmap_hash_map_remove_from_list_back
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) :
+  Tot (result (state & (hashmap_list_t t)))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st))
+  =
+  begin match ls with
+  | HashmapListCons ckey x tl ->
+    if ckey = key
+    then
+      let mv_ls =
+        mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
+          HashmapListNil in
+      begin match mv_ls with
+      | HashmapListCons i cvalue tl0 -> Return (st, tl0)
+      | HashmapListNil -> Fail
+      end
+    else
+      begin match hashmap_hash_map_remove_from_list_back t key tl st with
+      | Fail -> Fail
+      | Return (st0, l) -> Return (st0, HashmapListCons ckey x l)
+      end
+  | HashmapListNil -> Return (st, HashmapListNil)
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+let hashmap_hash_map_remove_fwd
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+  result (state & (option t))
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with
+        | Fail -> Fail
+        | Return (st1, x) ->
+          begin match x with
+          | None -> Return (st1, None)
+          | Some x0 ->
+            begin match usize_sub self.hashmap_hash_map_num_entries 1 with
+            | Fail -> Fail
+            | Return _ -> Return (st1, Some x0)
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+let hashmap_hash_map_remove_back
+  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) :
+  result (state & (hashmap_hash_map_t t))
+  =
+  begin match hashmap_hash_key_fwd key st with
+  | Fail -> Fail
+  | Return (st0, i) ->
+    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match
+        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
+          hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with
+        | Fail -> Fail
+        | Return (st1, x) ->
+          begin match x with
+          | None ->
+            begin match hashmap_hash_map_remove_from_list_back t key l st1 with
+            | Fail -> Fail
+            | Return (st2, l0) ->
+              begin match
+                vec_index_mut_back (hashmap_list_t t)
+                  self.hashmap_hash_map_slots hash_mod l0 with
+              | Fail -> Fail
+              | Return v ->
+                Return (st2, Mkhashmap_hash_map_t
+                  self.hashmap_hash_map_num_entries
+                  self.hashmap_hash_map_max_load_factor
+                  self.hashmap_hash_map_max_load v)
+              end
+            end
+          | Some x0 ->
+            begin match usize_sub self.hashmap_hash_map_num_entries 1 with
+            | Fail -> Fail
+            | Return i1 ->
+              begin match hashmap_hash_map_remove_from_list_back t key l st1
+                with
+              | Fail -> Fail
+              | Return (st2, l0) ->
+                begin match
+                  vec_index_mut_back (hashmap_list_t t)
+                    self.hashmap_hash_map_slots hash_mod l0 with
+                | Fail -> Fail
+                | Return v ->
+                  Return (st2, Mkhashmap_hash_map_t i1
+                    self.hashmap_hash_map_max_load_factor
+                    self.hashmap_hash_map_max_load v)
+                end
+              end
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::hashmap::test1] *)
+let hashmap_test1_fwd (st : state) : result (state & unit) =
+  begin match hashmap_hash_map_new_fwd u64 st with
+  | Fail -> Fail
+  | Return (st0, hm) ->
+    begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with
+    | Fail -> Fail
+    | Return (st1, hm0) ->
+      begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with
+      | Fail -> Fail
+      | Return (st2, hm1) ->
+        begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2 with
+        | Fail -> Fail
+        | Return (st3, hm2) ->
+          begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3 with
+          | Fail -> Fail
+          | Return (st4, hm3) ->
+            begin match hashmap_hash_map_get_fwd u64 hm3 128 st4 with
+            | Fail -> Fail
+            | Return (st5, i) ->
+              if not (i = 18)
+              then Fail
+              else
+                begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 st5
+                  with
+                | Fail -> Fail
+                | Return (st6, hm4) ->
+                  begin match hashmap_hash_map_get_fwd u64 hm4 1024 st6 with
+                  | Fail -> Fail
+                  | Return (st7, i0) ->
+                    if not (i0 = 56)
+                    then Fail
+                    else
+                      begin match hashmap_hash_map_remove_fwd u64 hm4 1024 st7
+                        with
+                      | Fail -> Fail
+                      | Return (st8, x) ->
+                        begin match x with
+                        | None -> Fail
+                        | Some x0 ->
+                          if not (x0 = 56)
+                          then Fail
+                          else
+                            begin match
+                              hashmap_hash_map_remove_back u64 hm4 1024 st8
+                              with
+                            | Fail -> Fail
+                            | Return (st9, hm5) ->
+                              begin match
+                                hashmap_hash_map_get_fwd u64 hm5 0 st9 with
+                              | Fail -> Fail
+                              | Return (st10, i1) ->
+                                if not (i1 = 42)
+                                then Fail
+                                else
+                                  begin match
+                                    hashmap_hash_map_get_fwd u64 hm5 128 st10
+                                    with
+                                  | Fail -> Fail
+                                  | Return (st11, i2) ->
+                                    if not (i2 = 18)
+                                    then Fail
+                                    else
+                                      begin match
+                                        hashmap_hash_map_get_fwd u64 
+                                          hm5 1056 st11 with
+                                      | Fail -> Fail
+                                      | Return (st12, i3) ->
+                                        if not (i3 = 256)
+                                        then Fail
+                                        else Return (st12, ())
+                                      end
+                                  end
+                              end
+                            end
+                        end
+                      end
+                  end
+                end
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap_main::insert_on_disk] *)
+let insert_on_disk_fwd
+  (key : usize) (value : u64) (st : state) : result (state & unit) =
+  begin match hashmap_utils_deserialize_fwd st with
+  | Fail -> Fail
+  | Return (st0, hm) ->
+    begin match hashmap_hash_map_insert_back u64 hm key value st0 with
+    | Fail -> Fail
+    | Return (st1, hm0) ->
+      begin match hashmap_utils_serialize_fwd hm0 st1 with
+      | Fail -> Fail
+      | Return (st2, _) -> Return (st2, ())
+      end
+    end
+  end
+
+(** [hashmap_main::main] *)
+let main_fwd (st : state) : result (state & unit) = Return (st, ())
+