diff options
Diffstat (limited to 'tests/coq/hashmap_main/HashmapMain_Funs.v')
-rw-r--r-- | tests/coq/hashmap_main/HashmapMain_Funs.v | 589 |
1 files changed, 589 insertions, 0 deletions
diff --git a/tests/coq/hashmap_main/HashmapMain_Funs.v b/tests/coq/hashmap_main/HashmapMain_Funs.v new file mode 100644 index 00000000..f6467d5a --- /dev/null +++ b/tests/coq/hashmap_main/HashmapMain_Funs.v @@ -0,0 +1,589 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import HashmapMain_Types. +Include HashmapMain_Types. +Require Import HashmapMain_FunsExternal. +Include HashmapMain_FunsExternal. +Module HashmapMain_Funs. + +(** [hashmap_main::hashmap::hash_key]: + Source: 'tests/src/hashmap.rs', lines 35:0-35:32 *) +Definition hashmap_hash_key (k : usize) : result usize := + Ok k. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0: + Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) +Fixpoint hashmap_HashMap_allocate_slots_loop + (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) + : + result (alloc_vec_Vec (hashmap_List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n2 => + if n1 s> 0%usize + then ( + slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; + n3 <- usize_sub n1 1%usize; + hashmap_HashMap_allocate_slots_loop T n2 slots1 n3) + else Ok slots + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: + Source: 'tests/src/hashmap.rs', lines 58:4-58:76 *) +Definition hashmap_HashMap_allocate_slots + (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) + : + result (alloc_vec_Vec (hashmap_List_t T)) + := + hashmap_HashMap_allocate_slots_loop T n slots n1 +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]: + Source: 'tests/src/hashmap.rs', lines 67:4-71:13 *) +Definition hashmap_HashMap_new_with_capacity + (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) + (max_load_divisor : usize) : + result (hashmap_HashMap_t T) + := + slots <- + hashmap_HashMap_allocate_slots T n (alloc_vec_Vec_new (hashmap_List_t T)) + capacity; + i <- usize_mul capacity max_load_dividend; + i1 <- usize_div i max_load_divisor; + Ok + {| + hashmap_HashMap_num_entries := 0%usize; + hashmap_HashMap_max_load_factor := (max_load_dividend, max_load_divisor); + hashmap_HashMap_max_load := i1; + hashmap_HashMap_slots := slots + |} +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]: + Source: 'tests/src/hashmap.rs', lines 83:4-83:24 *) +Definition hashmap_HashMap_new + (T : Type) (n : nat) : result (hashmap_HashMap_t T) := + hashmap_HashMap_new_with_capacity T n 32%usize 4%usize 5%usize +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0: + Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) +Fixpoint hashmap_HashMap_clear_loop + (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : + result (alloc_vec_Vec (hashmap_List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + let i1 := alloc_vec_Vec_len (hashmap_List_t T) slots in + if i s< i1 + then ( + p <- + alloc_vec_Vec_index_mut (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) slots + i; + let (_, index_mut_back) := p in + i2 <- usize_add i 1%usize; + slots1 <- index_mut_back Hashmap_List_Nil; + hashmap_HashMap_clear_loop T n1 slots1 i2) + else Ok slots + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: + Source: 'tests/src/hashmap.rs', lines 88:4-88:27 *) +Definition hashmap_HashMap_clear + (T : Type) (n : nat) (self : hashmap_HashMap_t T) : + result (hashmap_HashMap_t T) + := + hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; + Ok + {| + hashmap_HashMap_num_entries := 0%usize; + hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := hm + |} +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: + Source: 'tests/src/hashmap.rs', lines 98:4-98:30 *) +Definition hashmap_HashMap_len + (T : Type) (self : hashmap_HashMap_t T) : result usize := + Ok self.(hashmap_HashMap_num_entries) +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) +Fixpoint hashmap_HashMap_insert_in_list_loop + (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : + result (bool * (hashmap_List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons ckey cvalue tl => + if ckey s= key + then Ok (false, Hashmap_List_Cons ckey value tl) + else ( + p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl; + let (b, tl1) := p in + Ok (b, Hashmap_List_Cons ckey cvalue tl1)) + | Hashmap_List_Nil => + Ok (true, Hashmap_List_Cons key value Hashmap_List_Nil) + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: + Source: 'tests/src/hashmap.rs', lines 105:4-105:71 *) +Definition hashmap_HashMap_insert_in_list + (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : + result (bool * (hashmap_List_t T)) + := + hashmap_HashMap_insert_in_list_loop T n key value ls +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]: + Source: 'tests/src/hashmap.rs', lines 125:4-125:54 *) +Definition hashmap_HashMap_insert_no_resize + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : + result (hashmap_HashMap_t T) + := + hash <- hashmap_hash_key key; + let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + hash_mod <- usize_rem hash i; + p <- + alloc_vec_Vec_index_mut (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) + self.(hashmap_HashMap_slots) hash_mod; + let (l, index_mut_back) := p in + p1 <- hashmap_HashMap_insert_in_list T n key value l; + let (inserted, l1) := p1 in + if inserted + then ( + i1 <- usize_add self.(hashmap_HashMap_num_entries) 1%usize; + v <- index_mut_back l1; + Ok + {| + hashmap_HashMap_num_entries := i1; + hashmap_HashMap_max_load_factor := + self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := v + |}) + else ( + v <- index_mut_back l1; + Ok + {| + hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); + hashmap_HashMap_max_load_factor := + self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := v + |}) +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) +Fixpoint hashmap_HashMap_move_elements_from_list_loop + (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : + result (hashmap_HashMap_t T) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons k v tl => + ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v; + hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl + | Hashmap_List_Nil => Ok ntable + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: + Source: 'tests/src/hashmap.rs', lines 191:4-191:72 *) +Definition hashmap_HashMap_move_elements_from_list + (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : + result (hashmap_HashMap_t T) + := + hashmap_HashMap_move_elements_from_list_loop T n ntable ls +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0: + Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) +Fixpoint hashmap_HashMap_move_elements_loop + (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) + (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : + result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + let i1 := alloc_vec_Vec_len (hashmap_List_t T) slots in + if i s< i1 + then ( + p <- + alloc_vec_Vec_index_mut (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) slots + i; + let (l, index_mut_back) := p in + let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in + ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; + i2 <- usize_add i 1%usize; + slots1 <- index_mut_back l1; + hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2) + else Ok (ntable, slots) + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: + Source: 'tests/src/hashmap.rs', lines 179:4-179:95 *) +Definition hashmap_HashMap_move_elements + (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) + (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : + result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) + := + hashmap_HashMap_move_elements_loop T n ntable slots i +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: + Source: 'tests/src/hashmap.rs', lines 148:4-148:28 *) +Definition hashmap_HashMap_try_resize + (T : Type) (n : nat) (self : hashmap_HashMap_t T) : + result (hashmap_HashMap_t T) + := + max_usize <- scalar_cast U32 Usize core_u32_max; + let capacity := + alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + n1 <- usize_div max_usize 2%usize; + let (i, i1) := self.(hashmap_HashMap_max_load_factor) in + i2 <- usize_div n1 i; + if capacity s<= i2 + then ( + i3 <- usize_mul capacity 2%usize; + ntable <- hashmap_HashMap_new_with_capacity T n i3 i i1; + p <- + hashmap_HashMap_move_elements T n ntable self.(hashmap_HashMap_slots) + 0%usize; + let (ntable1, _) := p in + Ok + {| + hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); + hashmap_HashMap_max_load_factor := (i, i1); + hashmap_HashMap_max_load := ntable1.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := ntable1.(hashmap_HashMap_slots) + |}) + else + Ok + {| + hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); + hashmap_HashMap_max_load_factor := (i, i1); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := self.(hashmap_HashMap_slots) + |} +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]: + Source: 'tests/src/hashmap.rs', lines 137:4-137:48 *) +Definition hashmap_HashMap_insert + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : + result (hashmap_HashMap_t T) + := + self1 <- hashmap_HashMap_insert_no_resize T n self key value; + i <- hashmap_HashMap_len T self1; + if i s> self1.(hashmap_HashMap_max_load) + then hashmap_HashMap_try_resize T n self1 + else Ok self1 +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) +Fixpoint hashmap_HashMap_contains_key_in_list_loop + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons ckey _ tl => + if ckey s= key + then Ok true + else hashmap_HashMap_contains_key_in_list_loop T n1 key tl + | Hashmap_List_Nil => Ok false + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: + Source: 'tests/src/hashmap.rs', lines 214:4-214:68 *) +Definition hashmap_HashMap_contains_key_in_list + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := + hashmap_HashMap_contains_key_in_list_loop T n key ls +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]: + Source: 'tests/src/hashmap.rs', lines 207:4-207:49 *) +Definition hashmap_HashMap_contains_key + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : + result bool + := + hash <- hashmap_hash_key key; + let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + hash_mod <- usize_rem hash i; + l <- + alloc_vec_Vec_index (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) + self.(hashmap_HashMap_slots) hash_mod; + hashmap_HashMap_contains_key_in_list T n key l +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) +Fixpoint hashmap_HashMap_get_in_list_loop + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons ckey cvalue tl => + if ckey s= key + then Ok cvalue + else hashmap_HashMap_get_in_list_loop T n1 key tl + | Hashmap_List_Nil => Fail_ Failure + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: + Source: 'tests/src/hashmap.rs', lines 232:4-232:70 *) +Definition hashmap_HashMap_get_in_list + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := + hashmap_HashMap_get_in_list_loop T n key ls +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]: + Source: 'tests/src/hashmap.rs', lines 247:4-247:55 *) +Definition hashmap_HashMap_get + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result T := + hash <- hashmap_hash_key key; + let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + hash_mod <- usize_rem hash i; + l <- + alloc_vec_Vec_index (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) + self.(hashmap_HashMap_slots) hash_mod; + hashmap_HashMap_get_in_list T n key l +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) +Fixpoint hashmap_HashMap_get_mut_in_list_loop + (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : + result (T * (T -> result (hashmap_List_t T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons ckey cvalue tl => + if ckey s= key + then + let back := fun (ret : T) => Ok (Hashmap_List_Cons ckey ret tl) in + Ok (cvalue, back) + else ( + p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key; + let (t, back) := p in + let back1 := + fun (ret : T) => + tl1 <- back ret; Ok (Hashmap_List_Cons ckey cvalue tl1) in + Ok (t, back1)) + | Hashmap_List_Nil => Fail_ Failure + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: + Source: 'tests/src/hashmap.rs', lines 253:4-253:86 *) +Definition hashmap_HashMap_get_mut_in_list + (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : + result (T * (T -> result (hashmap_List_t T))) + := + hashmap_HashMap_get_mut_in_list_loop T n ls key +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: + Source: 'tests/src/hashmap.rs', lines 265:4-265:67 *) +Definition hashmap_HashMap_get_mut + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : + result (T * (T -> result (hashmap_HashMap_t T))) + := + hash <- hashmap_hash_key key; + let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + hash_mod <- usize_rem hash i; + p <- + alloc_vec_Vec_index_mut (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) + self.(hashmap_HashMap_slots) hash_mod; + let (l, index_mut_back) := p in + p1 <- hashmap_HashMap_get_mut_in_list T n l key; + let (t, get_mut_in_list_back) := p1 in + let back := + fun (ret : T) => + l1 <- get_mut_in_list_back ret; + v <- index_mut_back l1; + Ok + {| + hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); + hashmap_HashMap_max_load_factor := + self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := v + |} in + Ok (t, back) +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: + Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) +Fixpoint hashmap_HashMap_remove_from_list_loop + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : + result ((option T) * (hashmap_List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match ls with + | Hashmap_List_Cons ckey t tl => + if ckey s= key + then + let (mv_ls, _) := + core_mem_replace (hashmap_List_t T) (Hashmap_List_Cons ckey t tl) + Hashmap_List_Nil in + match mv_ls with + | Hashmap_List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1) + | Hashmap_List_Nil => Fail_ Failure + end + else ( + p <- hashmap_HashMap_remove_from_list_loop T n1 key tl; + let (o, tl1) := p in + Ok (o, Hashmap_List_Cons ckey t tl1)) + | Hashmap_List_Nil => Ok (None, Hashmap_List_Nil) + end + end +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: + Source: 'tests/src/hashmap.rs', lines 273:4-273:69 *) +Definition hashmap_HashMap_remove_from_list + (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : + result ((option T) * (hashmap_List_t T)) + := + hashmap_HashMap_remove_from_list_loop T n key ls +. + +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]: + Source: 'tests/src/hashmap.rs', lines 302:4-302:52 *) +Definition hashmap_HashMap_remove + (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : + result ((option T) * (hashmap_HashMap_t T)) + := + hash <- hashmap_hash_key key; + let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in + hash_mod <- usize_rem hash i; + p <- + alloc_vec_Vec_index_mut (hashmap_List_t T) usize + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) + self.(hashmap_HashMap_slots) hash_mod; + let (l, index_mut_back) := p in + p1 <- hashmap_HashMap_remove_from_list T n key l; + let (x, l1) := p1 in + match x with + | None => + v <- index_mut_back l1; + Ok (None, + {| + hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); + hashmap_HashMap_max_load_factor := + self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := v + |}) + | Some x1 => + i1 <- usize_sub self.(hashmap_HashMap_num_entries) 1%usize; + v <- index_mut_back l1; + Ok (Some x1, + {| + hashmap_HashMap_num_entries := i1; + hashmap_HashMap_max_load_factor := + self.(hashmap_HashMap_max_load_factor); + hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); + hashmap_HashMap_slots := v + |}) + end +. + +(** [hashmap_main::hashmap::test1]: + Source: 'tests/src/hashmap.rs', lines 323:0-323:10 *) +Definition hashmap_test1 (n : nat) : result unit := + hm <- hashmap_HashMap_new u64 n; + hm1 <- hashmap_HashMap_insert u64 n hm 0%usize 42%u64; + hm2 <- hashmap_HashMap_insert u64 n hm1 128%usize 18%u64; + hm3 <- hashmap_HashMap_insert u64 n hm2 1024%usize 138%u64; + hm4 <- hashmap_HashMap_insert u64 n hm3 1056%usize 256%u64; + i <- hashmap_HashMap_get u64 n hm4 128%usize; + if negb (i s= 18%u64) + then Fail_ Failure + else ( + p <- hashmap_HashMap_get_mut u64 n hm4 1024%usize; + let (_, get_mut_back) := p in + hm5 <- get_mut_back 56%u64; + i1 <- hashmap_HashMap_get u64 n hm5 1024%usize; + if negb (i1 s= 56%u64) + then Fail_ Failure + else ( + p1 <- hashmap_HashMap_remove u64 n hm5 1024%usize; + let (x, hm6) := p1 in + match x with + | None => Fail_ Failure + | Some x1 => + if negb (x1 s= 56%u64) + then Fail_ Failure + else ( + i2 <- hashmap_HashMap_get u64 n hm6 0%usize; + if negb (i2 s= 42%u64) + then Fail_ Failure + else ( + i3 <- hashmap_HashMap_get u64 n hm6 128%usize; + if negb (i3 s= 18%u64) + then Fail_ Failure + else ( + i4 <- hashmap_HashMap_get u64 n hm6 1056%usize; + if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt))) + end)) +. + +(** [hashmap_main::insert_on_disk]: + Source: 'tests/src/hashmap_main.rs', lines 13:0-13:43 *) +Definition insert_on_disk + (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := + p <- hashmap_utils_deserialize st; + let (st1, hm) := p in + hm1 <- hashmap_HashMap_insert u64 n hm key value; + hashmap_utils_serialize hm1 st1 +. + +(** [hashmap_main::main]: + Source: 'tests/src/hashmap_main.rs', lines 22:0-22:13 *) +Definition main : result unit := + Ok tt. + +End HashmapMain_Funs. |