path: root/tests/hashmap_on_disk/HashmapMain.Funs.fst

(** 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 slots0 ->
      begin match usize_sub n 1 with
      | Fail -> Fail
      | Return i ->
        begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with
        | Fail -> Fail
        | Return (st0, v) -> Return (st0, v)
        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, slots) ->
    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 slots)
      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 slots0 ->
      begin match usize_add i 1 with
      | Fail -> Fail
      | Return i1 ->
        begin match hashmap_hash_map_clear_slots_fwd t slots0 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 slots0 ->
      begin match usize_add i 1 with
      | Fail -> Fail
      | Return i1 ->
        begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with
        | Fail -> Fail
        | Return (st0, slots1) -> Return (st0, slots1)
        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, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
      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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, inserted) ->
          if inserted
          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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, inserted) ->
          if inserted
          then
            begin match usize_add self.hashmap_hash_map_num_entries 1 with
            | Fail -> Fail
            | Return i0 ->
              begin match
                hashmap_hash_map_insert_in_list_back t key value l st1 with
              | 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 i0
                    self.hashmap_hash_map_max_load_factor
                    self.hashmap_hash_map_max_load v)
                end
              end
            end
          else
            begin match hashmap_hash_map_insert_in_list_back t key value l st1
              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, ntable0) ->
      begin match hashmap_hash_map_move_elements_from_list_fwd t ntable0 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, ntable0) ->
      begin match
        hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
      | Fail -> Fail
      | Return (st1, ntable1) -> Return (st1, ntable1)
      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 ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
      begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
        with
      | Fail -> Fail
      | Return (st0, ntable0) ->
        let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
        begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
        | Fail -> Fail
        | Return slots0 ->
          begin match usize_add i 1 with
          | Fail -> Fail
          | Return i1 ->
            begin match
              hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
            | Fail -> Fail
            | Return (st1, _) -> Return (st1, ())
            end
          end
        end
      end
    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 ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
      begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
        with
      | Fail -> Fail
      | Return (st0, ntable0) ->
        let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
        begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
        | Fail -> Fail
        | Return slots0 ->
          begin match usize_add i 1 with
          | Fail -> Fail
          | Return i1 ->
            begin match
              hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 with
            | Fail -> Fail
            | Return (st1, (ntable1, slots1)) ->
              Return (st1, (ntable1, slots1))
            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 capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
  begin match usize_div 4294967295 2 with
  | Fail -> Fail
  | Return n1 ->
    let (i, i0) = self.hashmap_hash_map_max_load_factor in
    begin match usize_div n1 i with
    | Fail -> Fail
    | Return i1 ->
      if capacity <= i1
      then
        begin match usize_mul capacity 2 with
        | Fail -> Fail
        | Return i2 ->
          begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
          | Fail -> Fail
          | Return (st0, ntable) ->
            begin match
              hashmap_hash_map_move_elements_back t ntable
                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 capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
  begin match usize_div 4294967295 2 with
  | Fail -> Fail
  | Return n1 ->
    let (i, i0) = self.hashmap_hash_map_max_load_factor in
    begin match usize_div n1 i with
    | Fail -> Fail
    | Return i1 ->
      if capacity <= i1
      then
        begin match usize_mul capacity 2 with
        | Fail -> Fail
        | Return i2 ->
          begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with
          | Fail -> Fail
          | Return (st0, ntable) ->
            begin match
              hashmap_hash_map_move_elements_back t ntable
                self.hashmap_hash_map_slots 0 st0 with
            | Fail -> Fail
            | Return (st1, (ntable0, _)) ->
              Return (st1, Mkhashmap_hash_map_t
                self.hashmap_hash_map_num_entries (i, i0)
                ntable0.hashmap_hash_map_max_load
                ntable0.hashmap_hash_map_slots)
            end
          end
        end
      else
        Return (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (
          i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
    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, self0) ->
    begin match hashmap_hash_map_len_fwd t self0 st0 with
    | Fail -> Fail
    | Return (st1, i) ->
      if i > self0.hashmap_hash_map_max_load
      then
        begin match
          hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
            self0.hashmap_hash_map_num_entries
            self0.hashmap_hash_map_max_load_factor
            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
            st1 with
        | Fail -> Fail
        | Return (st2, _) -> Return (st2, ())
        end
      else Return (st1, ())
    end
  end

(** [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, self0) ->
    begin match hashmap_hash_map_len_fwd t self0 st0 with
    | Fail -> Fail
    | Return (st1, i) ->
      if i > self0.hashmap_hash_map_max_load
      then
        begin match
          hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
            self0.hashmap_hash_map_num_entries
            self0.hashmap_hash_map_max_load_factor
            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
            st1 with
        | Fail -> Fail
        | Return (st2, self1) -> Return (st2, self1)
        end
      else
        Return (st1, Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
          self0.hashmap_hash_map_max_load_factor
          self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
    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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
      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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, tl0) -> Return (st0, HashmapListCons ckey x tl0)
      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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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, hash) ->
    let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem hash i 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 i0 ->
              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 i0
                    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, ())