Rename some subdirectories for consistency

1 files changed, 598 insertions, 0 deletions

diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
new file mode 100644
index 00000000..d4e43d9a
--- /dev/null
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -0,0 +1,598 @@
+signature hashmapMain_FunsTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val hashmap_hash_key_fwd_def : thm
+    val hashmap_hash_map_allocate_slots_fwd_def : thm
+    val hashmap_hash_map_allocate_slots_loop_fwd_def : thm
+    val hashmap_hash_map_clear_fwd_back_def : thm
+    val hashmap_hash_map_clear_loop_fwd_back_def : thm
+    val hashmap_hash_map_contains_key_fwd_def : thm
+    val hashmap_hash_map_contains_key_in_list_fwd_def : thm
+    val hashmap_hash_map_contains_key_in_list_loop_fwd_def : thm
+    val hashmap_hash_map_get_fwd_def : thm
+    val hashmap_hash_map_get_in_list_fwd_def : thm
+    val hashmap_hash_map_get_in_list_loop_fwd_def : thm
+    val hashmap_hash_map_get_mut_back_def : thm
+    val hashmap_hash_map_get_mut_fwd_def : thm
+    val hashmap_hash_map_get_mut_in_list_back_def : thm
+    val hashmap_hash_map_get_mut_in_list_fwd_def : thm
+    val hashmap_hash_map_get_mut_in_list_loop_back_def : thm
+    val hashmap_hash_map_get_mut_in_list_loop_fwd_def : thm
+    val hashmap_hash_map_insert_fwd_back_def : thm
+    val hashmap_hash_map_insert_in_list_back_def : thm
+    val hashmap_hash_map_insert_in_list_fwd_def : thm
+    val hashmap_hash_map_insert_in_list_loop_back_def : thm
+    val hashmap_hash_map_insert_in_list_loop_fwd_def : thm
+    val hashmap_hash_map_insert_no_resize_fwd_back_def : thm
+    val hashmap_hash_map_len_fwd_def : thm
+    val hashmap_hash_map_move_elements_from_list_fwd_back_def : thm
+    val hashmap_hash_map_move_elements_from_list_loop_fwd_back_def : thm
+    val hashmap_hash_map_move_elements_fwd_back_def : thm
+    val hashmap_hash_map_move_elements_loop_fwd_back_def : thm
+    val hashmap_hash_map_new_fwd_def : thm
+    val hashmap_hash_map_new_with_capacity_fwd_def : thm
+    val hashmap_hash_map_remove_back_def : thm
+    val hashmap_hash_map_remove_from_list_back_def : thm
+    val hashmap_hash_map_remove_from_list_fwd_def : thm
+    val hashmap_hash_map_remove_from_list_loop_back_def : thm
+    val hashmap_hash_map_remove_from_list_loop_fwd_def : thm
+    val hashmap_hash_map_remove_fwd_def : thm
+    val hashmap_hash_map_try_resize_fwd_back_def : thm
+    val hashmap_test1_fwd_def : thm
+    val insert_on_disk_fwd_def : thm
+    val main_fwd_def : thm
+  
+  val hashmapMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs"
+   
+   [hashmap_hash_key_fwd_def]  Definition
+      
+      ⊢ ∀k. hashmap_hash_key_fwd k = Return k
+   
+   [hashmap_hash_map_allocate_slots_fwd_def]  Definition
+      
+      ⊢ ∀slots n.
+          hashmap_hash_map_allocate_slots_fwd slots n =
+          hashmap_hash_map_allocate_slots_loop_fwd slots n
+   
+   [hashmap_hash_map_allocate_slots_loop_fwd_def]  Definition
+      
+      ⊢ ∀slots n.
+          hashmap_hash_map_allocate_slots_loop_fwd slots n =
+          if usize_gt n (int_to_usize 0) then
+            do
+              slots0 <- vec_push_back slots HashmapListNil;
+              n0 <- usize_sub n (int_to_usize 1);
+              hashmap_hash_map_allocate_slots_loop_fwd slots0 n0
+            od
+          else Return slots
+   
+   [hashmap_hash_map_clear_fwd_back_def]  Definition
+      
+      ⊢ ∀self.
+          hashmap_hash_map_clear_fwd_back self =
+          do
+            v <-
+              hashmap_hash_map_clear_loop_fwd_back
+                self.hashmap_hash_map_slots (int_to_usize 0);
+            Return
+              (self with
+               <|hashmap_hash_map_num_entries := int_to_usize 0;
+                 hashmap_hash_map_slots := v|>)
+          od
+   
+   [hashmap_hash_map_clear_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀slots i.
+          hashmap_hash_map_clear_loop_fwd_back slots i =
+          (let
+             i0 = vec_len slots
+           in
+             if usize_lt i i0 then
+               do
+                 i1 <- usize_add i (int_to_usize 1);
+                 slots0 <- vec_index_mut_back slots i HashmapListNil;
+                 hashmap_hash_map_clear_loop_fwd_back slots0 i1
+               od
+             else Return slots)
+   
+   [hashmap_hash_map_contains_key_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hashmap_hash_map_contains_key_fwd self key =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
+            hashmap_hash_map_contains_key_in_list_fwd key l
+          od
+   
+   [hashmap_hash_map_contains_key_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_contains_key_in_list_fwd key ls =
+          hashmap_hash_map_contains_key_in_list_loop_fwd key ls
+   
+   [hashmap_hash_map_contains_key_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_contains_key_in_list_loop_fwd key ls =
+          case ls of
+            HashmapListCons ckey t tl =>
+              if ckey = key then Return T
+              else hashmap_hash_map_contains_key_in_list_loop_fwd key tl
+          | HashmapListNil => Return F
+   
+   [hashmap_hash_map_get_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hashmap_hash_map_get_fwd self key =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod;
+            hashmap_hash_map_get_in_list_fwd key l
+          od
+   
+   [hashmap_hash_map_get_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_get_in_list_fwd key ls =
+          hashmap_hash_map_get_in_list_loop_fwd key ls
+   
+   [hashmap_hash_map_get_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_get_in_list_loop_fwd key ls =
+          case ls of
+            HashmapListCons ckey cvalue tl =>
+              if ckey = key then Return cvalue
+              else hashmap_hash_map_get_in_list_loop_fwd key tl
+          | HashmapListNil => Fail Failure
+   
+   [hashmap_hash_map_get_mut_back_def]  Definition
+      
+      ⊢ ∀self key ret.
+          hashmap_hash_map_get_mut_back self key ret =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
+            l0 <- hashmap_hash_map_get_mut_in_list_back l key ret;
+            v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0;
+            Return (self with hashmap_hash_map_slots := v)
+          od
+   
+   [hashmap_hash_map_get_mut_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hashmap_hash_map_get_mut_fwd self key =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
+            hashmap_hash_map_get_mut_in_list_fwd l key
+          od
+   
+   [hashmap_hash_map_get_mut_in_list_back_def]  Definition
+      
+      ⊢ ∀ls key ret.
+          hashmap_hash_map_get_mut_in_list_back ls key ret =
+          hashmap_hash_map_get_mut_in_list_loop_back ls key ret
+   
+   [hashmap_hash_map_get_mut_in_list_fwd_def]  Definition
+      
+      ⊢ ∀ls key.
+          hashmap_hash_map_get_mut_in_list_fwd ls key =
+          hashmap_hash_map_get_mut_in_list_loop_fwd ls key
+   
+   [hashmap_hash_map_get_mut_in_list_loop_back_def]  Definition
+      
+      ⊢ ∀ls key ret.
+          hashmap_hash_map_get_mut_in_list_loop_back ls key ret =
+          case ls of
+            HashmapListCons ckey cvalue tl =>
+              if ckey = key then Return (HashmapListCons ckey ret tl)
+              else
+                do
+                  tl0 <-
+                    hashmap_hash_map_get_mut_in_list_loop_back tl key ret;
+                  Return (HashmapListCons ckey cvalue tl0)
+                od
+          | HashmapListNil => Fail Failure
+   
+   [hashmap_hash_map_get_mut_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀ls key.
+          hashmap_hash_map_get_mut_in_list_loop_fwd ls key =
+          case ls of
+            HashmapListCons ckey cvalue tl =>
+              if ckey = key then Return cvalue
+              else hashmap_hash_map_get_mut_in_list_loop_fwd tl key
+          | HashmapListNil => Fail Failure
+   
+   [hashmap_hash_map_insert_fwd_back_def]  Definition
+      
+      ⊢ ∀self key value.
+          hashmap_hash_map_insert_fwd_back self key value =
+          do
+            self0 <-
+              hashmap_hash_map_insert_no_resize_fwd_back self key value;
+            i <- hashmap_hash_map_len_fwd self0;
+            if usize_gt i self0.hashmap_hash_map_max_load then
+              hashmap_hash_map_try_resize_fwd_back self0
+            else Return self0
+          od
+   
+   [hashmap_hash_map_insert_in_list_back_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hashmap_hash_map_insert_in_list_back key value ls =
+          hashmap_hash_map_insert_in_list_loop_back key value ls
+   
+   [hashmap_hash_map_insert_in_list_fwd_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hashmap_hash_map_insert_in_list_fwd key value ls =
+          hashmap_hash_map_insert_in_list_loop_fwd key value ls
+   
+   [hashmap_hash_map_insert_in_list_loop_back_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hashmap_hash_map_insert_in_list_loop_back key value ls =
+          case ls of
+            HashmapListCons ckey cvalue tl =>
+              if ckey = key then Return (HashmapListCons ckey value tl)
+              else
+                do
+                  tl0 <-
+                    hashmap_hash_map_insert_in_list_loop_back key value tl;
+                  Return (HashmapListCons ckey cvalue tl0)
+                od
+          | HashmapListNil =>
+            (let
+               l = HashmapListNil
+             in
+               Return (HashmapListCons key value l))
+   
+   [hashmap_hash_map_insert_in_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key value ls.
+          hashmap_hash_map_insert_in_list_loop_fwd key value ls =
+          case ls of
+            HashmapListCons ckey cvalue tl =>
+              if ckey = key then Return F
+              else hashmap_hash_map_insert_in_list_loop_fwd key value tl
+          | HashmapListNil => Return T
+   
+   [hashmap_hash_map_insert_no_resize_fwd_back_def]  Definition
+      
+      ⊢ ∀self key value.
+          hashmap_hash_map_insert_no_resize_fwd_back self key value =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
+            inserted <- hashmap_hash_map_insert_in_list_fwd key value l;
+            if inserted then
+              do
+                i0 <-
+                  usize_add self.hashmap_hash_map_num_entries
+                    (int_to_usize 1);
+                l0 <- hashmap_hash_map_insert_in_list_back key value l;
+                v <-
+                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
+                    l0;
+                Return
+                  (self with
+                   <|hashmap_hash_map_num_entries := i0;
+                     hashmap_hash_map_slots := v|>)
+              od
+            else
+              do
+                l0 <- hashmap_hash_map_insert_in_list_back key value l;
+                v <-
+                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
+                    l0;
+                Return (self with hashmap_hash_map_slots := v)
+              od
+          od
+   
+   [hashmap_hash_map_len_fwd_def]  Definition
+      
+      ⊢ ∀self.
+          hashmap_hash_map_len_fwd self =
+          Return self.hashmap_hash_map_num_entries
+   
+   [hashmap_hash_map_move_elements_from_list_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable ls.
+          hashmap_hash_map_move_elements_from_list_fwd_back ntable ls =
+          hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
+   
+   [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable ls.
+          hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls =
+          case ls of
+            HashmapListCons k v tl =>
+              do
+                ntable0 <-
+                  hashmap_hash_map_insert_no_resize_fwd_back ntable k v;
+                hashmap_hash_map_move_elements_from_list_loop_fwd_back
+                  ntable0 tl
+              od
+          | HashmapListNil => Return ntable
+   
+   [hashmap_hash_map_move_elements_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable slots i.
+          hashmap_hash_map_move_elements_fwd_back ntable slots i =
+          hashmap_hash_map_move_elements_loop_fwd_back ntable slots i
+   
+   [hashmap_hash_map_move_elements_loop_fwd_back_def]  Definition
+      
+      ⊢ ∀ntable slots i.
+          hashmap_hash_map_move_elements_loop_fwd_back ntable slots i =
+          (let
+             i0 = vec_len slots
+           in
+             if usize_lt i i0 then
+               do
+                 l <- vec_index_mut_fwd slots i;
+                 ls <<- mem_replace_fwd l HashmapListNil;
+                 ntable0 <-
+                   hashmap_hash_map_move_elements_from_list_fwd_back ntable
+                     ls;
+                 i1 <- usize_add i (int_to_usize 1);
+                 l0 <<- mem_replace_back l HashmapListNil;
+                 slots0 <- vec_index_mut_back slots i l0;
+                 hashmap_hash_map_move_elements_loop_fwd_back ntable0
+                   slots0 i1
+               od
+             else Return (ntable,slots))
+   
+   [hashmap_hash_map_new_fwd_def]  Definition
+      
+      ⊢ hashmap_hash_map_new_fwd =
+        hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32)
+          (int_to_usize 4) (int_to_usize 5)
+   
+   [hashmap_hash_map_new_with_capacity_fwd_def]  Definition
+      
+      ⊢ ∀capacity max_load_dividend max_load_divisor.
+          hashmap_hash_map_new_with_capacity_fwd capacity max_load_dividend
+            max_load_divisor =
+          (let
+             v = vec_new
+           in
+             do
+               slots <- hashmap_hash_map_allocate_slots_fwd v capacity;
+               i <- usize_mul capacity max_load_dividend;
+               i0 <- usize_div i max_load_divisor;
+               Return
+                 <|hashmap_hash_map_num_entries := int_to_usize 0;
+                   hashmap_hash_map_max_load_factor :=
+                     (max_load_dividend,max_load_divisor);
+                   hashmap_hash_map_max_load := i0;
+                   hashmap_hash_map_slots := slots|>
+             od)
+   
+   [hashmap_hash_map_remove_back_def]  Definition
+      
+      ⊢ ∀self key.
+          hashmap_hash_map_remove_back self key =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
+            x <- hashmap_hash_map_remove_from_list_fwd key l;
+            case x of
+              NONE =>
+                do
+                  l0 <- hashmap_hash_map_remove_from_list_back key l;
+                  v <-
+                    vec_index_mut_back self.hashmap_hash_map_slots hash_mod
+                      l0;
+                  Return (self with hashmap_hash_map_slots := v)
+                od
+            | SOME x0 =>
+              do
+                i0 <-
+                  usize_sub self.hashmap_hash_map_num_entries
+                    (int_to_usize 1);
+                l0 <- hashmap_hash_map_remove_from_list_back key l;
+                v <-
+                  vec_index_mut_back self.hashmap_hash_map_slots hash_mod
+                    l0;
+                Return
+                  (self with
+                   <|hashmap_hash_map_num_entries := i0;
+                     hashmap_hash_map_slots := v|>)
+              od
+          od
+   
+   [hashmap_hash_map_remove_from_list_back_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_remove_from_list_back key ls =
+          hashmap_hash_map_remove_from_list_loop_back key ls
+   
+   [hashmap_hash_map_remove_from_list_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_remove_from_list_fwd key ls =
+          hashmap_hash_map_remove_from_list_loop_fwd key ls
+   
+   [hashmap_hash_map_remove_from_list_loop_back_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_remove_from_list_loop_back key ls =
+          case ls of
+            HashmapListCons ckey t tl =>
+              if ckey = key then
+                (let
+                   mv_ls =
+                     mem_replace_fwd (HashmapListCons ckey t tl)
+                       HashmapListNil
+                 in
+                   case mv_ls of
+                     HashmapListCons i cvalue tl0 => Return tl0
+                   | HashmapListNil => Fail Failure)
+              else
+                do
+                  tl0 <- hashmap_hash_map_remove_from_list_loop_back key tl;
+                  Return (HashmapListCons ckey t tl0)
+                od
+          | HashmapListNil => Return HashmapListNil
+   
+   [hashmap_hash_map_remove_from_list_loop_fwd_def]  Definition
+      
+      ⊢ ∀key ls.
+          hashmap_hash_map_remove_from_list_loop_fwd key ls =
+          case ls of
+            HashmapListCons ckey t tl =>
+              if ckey = key then
+                (let
+                   mv_ls =
+                     mem_replace_fwd (HashmapListCons ckey t tl)
+                       HashmapListNil
+                 in
+                   case mv_ls of
+                     HashmapListCons i cvalue tl0 => Return (SOME cvalue)
+                   | HashmapListNil => Fail Failure)
+              else hashmap_hash_map_remove_from_list_loop_fwd key tl
+          | HashmapListNil => Return NONE
+   
+   [hashmap_hash_map_remove_fwd_def]  Definition
+      
+      ⊢ ∀self key.
+          hashmap_hash_map_remove_fwd self key =
+          do
+            hash <- hashmap_hash_key_fwd key;
+            i <<- vec_len self.hashmap_hash_map_slots;
+            hash_mod <- usize_rem hash i;
+            l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod;
+            x <- hashmap_hash_map_remove_from_list_fwd key l;
+            case x of
+              NONE => Return NONE
+            | SOME x0 =>
+              monad_ignore_bind
+                (usize_sub self.hashmap_hash_map_num_entries
+                   (int_to_usize 1)) (Return (SOME x0))
+          od
+   
+   [hashmap_hash_map_try_resize_fwd_back_def]  Definition
+      
+      ⊢ ∀self.
+          hashmap_hash_map_try_resize_fwd_back self =
+          do
+            max_usize <- mk_usize (u32_to_int core_u32_max);
+            capacity <<- vec_len self.hashmap_hash_map_slots;
+            n1 <- usize_div max_usize (int_to_usize 2);
+            (i,i0) <<- self.hashmap_hash_map_max_load_factor;
+            i1 <- usize_div n1 i;
+            if usize_le capacity i1 then
+              do
+                i2 <- usize_mul capacity (int_to_usize 2);
+                ntable <- hashmap_hash_map_new_with_capacity_fwd i2 i i0;
+                (ntable0,_) <-
+                  hashmap_hash_map_move_elements_fwd_back ntable
+                    self.hashmap_hash_map_slots (int_to_usize 0);
+                Return
+                  (ntable0 with
+                   <|hashmap_hash_map_num_entries :=
+                       self.hashmap_hash_map_num_entries;
+                     hashmap_hash_map_max_load_factor := (i,i0)|>)
+              od
+            else
+              Return (self with hashmap_hash_map_max_load_factor := (i,i0))
+          od
+   
+   [hashmap_test1_fwd_def]  Definition
+      
+      ⊢ hashmap_test1_fwd =
+        do
+          hm <- hashmap_hash_map_new_fwd;
+          hm0 <-
+            hashmap_hash_map_insert_fwd_back hm (int_to_usize 0)
+              (int_to_u64 42);
+          hm1 <-
+            hashmap_hash_map_insert_fwd_back hm0 (int_to_usize 128)
+              (int_to_u64 18);
+          hm2 <-
+            hashmap_hash_map_insert_fwd_back hm1 (int_to_usize 1024)
+              (int_to_u64 138);
+          hm3 <-
+            hashmap_hash_map_insert_fwd_back hm2 (int_to_usize 1056)
+              (int_to_u64 256);
+          i <- hashmap_hash_map_get_fwd hm3 (int_to_usize 128);
+          if i ≠ int_to_u64 18 then Fail Failure
+          else
+            do
+              hm4 <-
+                hashmap_hash_map_get_mut_back hm3 (int_to_usize 1024)
+                  (int_to_u64 56);
+              i0 <- hashmap_hash_map_get_fwd hm4 (int_to_usize 1024);
+              if i0 ≠ int_to_u64 56 then Fail Failure
+              else
+                do
+                  x <- hashmap_hash_map_remove_fwd hm4 (int_to_usize 1024);
+                  case x of
+                    NONE => Fail Failure
+                  | SOME x0 =>
+                    if x0 ≠ int_to_u64 56 then Fail Failure
+                    else
+                      do
+                        hm5 <-
+                          hashmap_hash_map_remove_back hm4
+                            (int_to_usize 1024);
+                        i1 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 0);
+                        if i1 ≠ int_to_u64 42 then Fail Failure
+                        else
+                          do
+                            i2 <-
+                              hashmap_hash_map_get_fwd hm5
+                                (int_to_usize 128);
+                            if i2 ≠ int_to_u64 18 then Fail Failure
+                            else
+                              do
+                                i3 <-
+                                  hashmap_hash_map_get_fwd hm5
+                                    (int_to_usize 1056);
+                                if i3 ≠ int_to_u64 256 then Fail Failure
+                                else Return ()
+                              od
+                          od
+                      od
+                od
+            od
+        od
+   
+   [insert_on_disk_fwd_def]  Definition
+      
+      ⊢ ∀key value st.
+          insert_on_disk_fwd key value st =
+          do
+            (st0,hm) <- hashmap_utils_deserialize_fwd st;
+            hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
+            (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+            Return (st1,())
+          od
+   
+   [main_fwd_def]  Definition
+      
+      ⊢ main_fwd = Return ()
+   
+   
+*)
+end