From 4a34537a7fe33fa33d618b153832f9e750276480 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 14 Jun 2024 10:41:06 +0200 Subject: Update the code of the hashmap --- tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 38 ++-- tests/fstar/hashmap/Hashmap.Clauses.fst | 22 +- tests/fstar/hashmap/Hashmap.Funs.fst | 248 +++++++++++------------ tests/fstar/hashmap/Hashmap.FunsExternal.fsti | 4 +- tests/fstar/hashmap/Hashmap.Types.fst | 14 +- 5 files changed, 163 insertions(+), 163 deletions(-) (limited to 'tests/fstar') diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index 57003613..888cd4ec 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -7,65 +7,65 @@ open Hashmap.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::{hashmap::HashMap}::allocate_slots]: decreases clause - Source: 'tests/src/hashmap.rs', lines 60:4-66:5 *) + Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *) unfold let hashMap_allocate_slots_loop_decreases (t : Type0) - (slots : alloc_vec_Vec (list_t t)) (n : usize) : nat = + (slots : alloc_vec_Vec (aList_t t)) (n : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::clear]: decreases clause - Source: 'tests/src/hashmap.rs', lines 90:4-98:5 *) + Source: 'tests/src/hashmap.rs', lines 91:4-99:5 *) unfold -let hashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (list_t t)) - (i : usize) : nat = +let hashMap_clear_loop_decreases (t : Type0) + (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::insert_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 107:4-124:5 *) + Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *) unfold let hashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t) - (ls : list_t t) : nat = + (ls : aList_t t) : nat = admit () (** [hashmap::{hashmap::HashMap}::move_elements_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 193:4-206:5 *) + Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *) unfold let hashMap_move_elements_from_list_loop_decreases (t : Type0) - (ntable : hashMap_t t) (ls : list_t t) : nat = + (ntable : hashMap_t t) (ls : aList_t t) : nat = admit () (** [hashmap::{hashmap::HashMap}::move_elements]: decreases clause - Source: 'tests/src/hashmap.rs', lines 181:4-190:5 *) + Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *) unfold let hashMap_move_elements_loop_decreases (t : Type0) (ntable : hashMap_t t) - (slots : alloc_vec_Vec (list_t t)) (i : usize) : nat = + (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 216:4-229:5 *) + Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *) unfold let hashMap_contains_key_in_list_loop_decreases (t : Type0) (key : usize) - (ls : list_t t) : nat = + (ls : aList_t t) : nat = admit () (** [hashmap::{hashmap::HashMap}::get_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 234:4-247:5 *) + Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *) unfold let hashMap_get_in_list_loop_decreases (t : Type0) (key : usize) - (ls : list_t t) : nat = + (ls : aList_t t) : nat = admit () (** [hashmap::{hashmap::HashMap}::get_mut_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 255:4-264:5 *) + Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *) unfold -let hashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : list_t t) +let hashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : aList_t t) (key : usize) : nat = admit () (** [hashmap::{hashmap::HashMap}::remove_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 275:4-301:5 *) + Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *) unfold let hashMap_remove_from_list_loop_decreases (t : Type0) (key : usize) - (ls : list_t t) : nat = + (ls : aList_t t) : nat = admit () diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst index 6c699d05..3a389b94 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.fst @@ -9,53 +9,53 @@ open Hashmap.Types (** [hashmap::HashMap::allocate_slots]: decreases clause *) unfold let hashMap_allocate_slots_loop_decreases (t : Type0) - (slots : alloc_vec_Vec (list_t t)) (n : usize) : nat = n + (slots : alloc_vec_Vec (aList_t t)) (n : usize) : nat = n (** [hashmap::HashMap::clear]: decreases clause *) unfold -let hashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (list_t t)) +let hashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 (** [hashmap::HashMap::insert_in_list]: decreases clause *) unfold let hashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t) - (ls : list_t t) : list_t t = + (ls : aList_t t) : aList_t t = ls (** [hashmap::HashMap::move_elements_from_list]: decreases clause *) unfold let hashMap_move_elements_from_list_loop_decreases (t : Type0) - (ntable : hashMap_t t) (ls : list_t t) : list_t t = + (ntable : hashMap_t t) (ls : aList_t t) : aList_t t = ls (** [hashmap::HashMap::move_elements]: decreases clause *) unfold let hashMap_move_elements_loop_decreases (t : Type0) (ntable : hashMap_t t) - (slots : alloc_vec_Vec (list_t t)) (i : usize) : nat = + (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 (** [hashmap::HashMap::contains_key_in_list]: decreases clause *) unfold let hashMap_contains_key_in_list_loop_decreases (t : Type0) (key : usize) - (ls : list_t t) : list_t t = + (ls : aList_t t) : aList_t t = ls (** [hashmap::HashMap::get_in_list]: decreases clause *) unfold -let hashMap_get_in_list_loop_decreases (t : Type0) (key : usize) (ls : list_t t) : - list_t t = +let hashMap_get_in_list_loop_decreases (t : Type0) (key : usize) (ls : aList_t t) : + aList_t t = ls (** [hashmap::HashMap::get_mut_in_list]: decreases clause *) unfold -let hashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : list_t t) - (key : usize) : list_t t = +let hashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : aList_t t) + (key : usize) : aList_t t = ls (** [hashmap::HashMap::remove_from_list]: decreases clause *) unfold let hashMap_remove_from_list_loop_decreases (t : Type0) (key : usize) - (ls : list_t t) : list_t t = + (ls : aList_t t) : aList_t t = ls diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index fb77c7ef..0569c32a 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -9,41 +9,41 @@ include Hashmap.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 37:0-37:32 *) + Source: 'tests/src/hashmap.rs', lines 38:0-38:32 *) let hash_key (k : usize) : result usize = Ok k (** [hashmap::{hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 60:4-66:5 *) + Source: 'tests/src/hashmap.rs', lines 61:4-67:5 *) let rec hashMap_allocate_slots_loop - (t : Type0) (slots : alloc_vec_Vec (list_t t)) (n : usize) : - Tot (result (alloc_vec_Vec (list_t t))) + (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) : + Tot (result (alloc_vec_Vec (aList_t t))) (decreases (hashMap_allocate_slots_loop_decreases t slots n)) = if n > 0 then - let* slots1 = alloc_vec_Vec_push (list_t t) slots List_Nil in + let* slots1 = alloc_vec_Vec_push (aList_t t) slots AList_Nil in let* n1 = usize_sub n 1 in hashMap_allocate_slots_loop t slots1 n1 else Ok slots (** [hashmap::{hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 60:4-60:76 *) + Source: 'tests/src/hashmap.rs', lines 61:4-61:78 *) let hashMap_allocate_slots - (t : Type0) (slots : alloc_vec_Vec (list_t t)) (n : usize) : - result (alloc_vec_Vec (list_t t)) + (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) : + result (alloc_vec_Vec (aList_t t)) = hashMap_allocate_slots_loop t slots n (** [hashmap::{hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 69:4-73:13 *) + Source: 'tests/src/hashmap.rs', lines 70:4-74:13 *) let hashMap_new_with_capacity (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : result (hashMap_t t) = - let* slots = hashMap_allocate_slots t (alloc_vec_Vec_new (list_t t)) capacity - in + let* slots = + hashMap_allocate_slots t (alloc_vec_Vec_new (aList_t t)) capacity in let* i = usize_mul capacity max_load_dividend in let* i1 = usize_div i max_load_divisor in Ok @@ -55,141 +55,141 @@ let hashMap_new_with_capacity } (** [hashmap::{hashmap::HashMap}::new]: - Source: 'tests/src/hashmap.rs', lines 85:4-85:24 *) + Source: 'tests/src/hashmap.rs', lines 86:4-86:24 *) let hashMap_new (t : Type0) : result (hashMap_t t) = hashMap_new_with_capacity t 32 4 5 (** [hashmap::{hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 90:4-98:5 *) + Source: 'tests/src/hashmap.rs', lines 91:4-99:5 *) let rec hashMap_clear_loop - (t : Type0) (slots : alloc_vec_Vec (list_t t)) (i : usize) : - Tot (result (alloc_vec_Vec (list_t t))) + (t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : + Tot (result (alloc_vec_Vec (aList_t t))) (decreases (hashMap_clear_loop_decreases t slots i)) = - let i1 = alloc_vec_Vec_len (list_t t) slots in + let i1 = alloc_vec_Vec_len (aList_t t) slots in if i < i1 then let* (_, index_mut_back) = - alloc_vec_Vec_index_mut (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in + alloc_vec_Vec_index_mut (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) slots i in let* i2 = usize_add i 1 in - let* slots1 = index_mut_back List_Nil in + let* slots1 = index_mut_back AList_Nil in hashMap_clear_loop t slots1 i2 else Ok slots (** [hashmap::{hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 90:4-90:27 *) + Source: 'tests/src/hashmap.rs', lines 91:4-91:27 *) let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = let* hm = hashMap_clear_loop t self.slots 0 in Ok { self with num_entries = 0; slots = hm } (** [hashmap::{hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 100:4-100:30 *) + Source: 'tests/src/hashmap.rs', lines 101:4-101:30 *) let hashMap_len (t : Type0) (self : hashMap_t t) : result usize = Ok self.num_entries (** [hashmap::{hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 107:4-124:5 *) + Source: 'tests/src/hashmap.rs', lines 108:4-125:5 *) let rec hashMap_insert_in_list_loop - (t : Type0) (key : usize) (value : t) (ls : list_t t) : - Tot (result (bool & (list_t t))) + (t : Type0) (key : usize) (value : t) (ls : aList_t t) : + Tot (result (bool & (aList_t t))) (decreases (hashMap_insert_in_list_loop_decreases t key value ls)) = begin match ls with - | List_Cons ckey cvalue tl -> + | AList_Cons ckey cvalue tl -> if ckey = key - then Ok (false, List_Cons ckey value tl) + then Ok (false, AList_Cons ckey value tl) else let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in - Ok (b, List_Cons ckey cvalue tl1) - | List_Nil -> Ok (true, List_Cons key value List_Nil) + Ok (b, AList_Cons ckey cvalue tl1) + | AList_Nil -> Ok (true, AList_Cons key value AList_Nil) end (** [hashmap::{hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 107:4-107:71 *) + Source: 'tests/src/hashmap.rs', lines 108:4-108:72 *) let hashMap_insert_in_list - (t : Type0) (key : usize) (value : t) (ls : list_t t) : - result (bool & (list_t t)) + (t : Type0) (key : usize) (value : t) (ls : aList_t t) : + result (bool & (aList_t t)) = hashMap_insert_in_list_loop t key value ls (** [hashmap::{hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 127:4-127:54 *) + Source: 'tests/src/hashmap.rs', lines 128:4-128:54 *) let hashMap_insert_no_resize (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) = let* hash = hash_key key in - let i = alloc_vec_Vec_len (list_t t) self.slots in + let i = alloc_vec_Vec_len (aList_t t) self.slots in let* hash_mod = usize_rem hash i in - let* (l, index_mut_back) = - alloc_vec_Vec_index_mut (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots + let* (a, index_mut_back) = + alloc_vec_Vec_index_mut (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) self.slots hash_mod in - let* (inserted, l1) = hashMap_insert_in_list t key value l in + let* (inserted, a1) = hashMap_insert_in_list t key value a in if inserted then let* i1 = usize_add self.num_entries 1 in - let* v = index_mut_back l1 in + let* v = index_mut_back a1 in Ok { self with num_entries = i1; slots = v } - else let* v = index_mut_back l1 in Ok { self with slots = v } + else let* v = index_mut_back a1 in Ok { self with slots = v } (** [hashmap::{hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 193:4-206:5 *) + Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *) let rec hashMap_move_elements_from_list_loop - (t : Type0) (ntable : hashMap_t t) (ls : list_t t) : + (t : Type0) (ntable : hashMap_t t) (ls : aList_t t) : Tot (result (hashMap_t t)) (decreases (hashMap_move_elements_from_list_loop_decreases t ntable ls)) = begin match ls with - | List_Cons k v tl -> + | AList_Cons k v tl -> let* ntable1 = hashMap_insert_no_resize t ntable k v in hashMap_move_elements_from_list_loop t ntable1 tl - | List_Nil -> Ok ntable + | AList_Nil -> Ok ntable end (** [hashmap::{hashmap::HashMap}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 193:4-193:72 *) + Source: 'tests/src/hashmap.rs', lines 194:4-194:73 *) let hashMap_move_elements_from_list - (t : Type0) (ntable : hashMap_t t) (ls : list_t t) : result (hashMap_t t) = + (t : Type0) (ntable : hashMap_t t) (ls : aList_t t) : result (hashMap_t t) = hashMap_move_elements_from_list_loop t ntable ls (** [hashmap::{hashmap::HashMap}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 181:4-190:5 *) + Source: 'tests/src/hashmap.rs', lines 182:4-191:5 *) let rec hashMap_move_elements_loop - (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t)) + (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : - Tot (result ((hashMap_t t) & (alloc_vec_Vec (list_t t)))) + Tot (result ((hashMap_t t) & (alloc_vec_Vec (aList_t t)))) (decreases (hashMap_move_elements_loop_decreases t ntable slots i)) = - let i1 = alloc_vec_Vec_len (list_t t) slots in + let i1 = alloc_vec_Vec_len (aList_t t) slots in if i < i1 then - let* (l, index_mut_back) = - alloc_vec_Vec_index_mut (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in - let (ls, l1) = core_mem_replace (list_t t) l List_Nil in + let* (a, index_mut_back) = + alloc_vec_Vec_index_mut (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) slots i in + let (ls, a1) = core_mem_replace (aList_t t) a AList_Nil in let* ntable1 = hashMap_move_elements_from_list t ntable ls in let* i2 = usize_add i 1 in - let* slots1 = index_mut_back l1 in + let* slots1 = index_mut_back a1 in hashMap_move_elements_loop t ntable1 slots1 i2 else Ok (ntable, slots) (** [hashmap::{hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 181:4-181:95 *) + Source: 'tests/src/hashmap.rs', lines 182:4-182:96 *) let hashMap_move_elements - (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t)) + (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t)) (i : usize) : - result ((hashMap_t t) & (alloc_vec_Vec (list_t t))) + result ((hashMap_t t) & (alloc_vec_Vec (aList_t t))) = hashMap_move_elements_loop t ntable slots i (** [hashmap::{hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 150:4-150:28 *) + Source: 'tests/src/hashmap.rs', lines 151:4-151:28 *) let hashMap_try_resize (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = let* max_usize = scalar_cast U32 Usize core_u32_max in - let capacity = alloc_vec_Vec_len (list_t t) self.slots in + let capacity = alloc_vec_Vec_len (aList_t t) self.slots in let* n1 = usize_div max_usize 2 in let (i, i1) = self.max_load_factor in let* i2 = usize_div n1 i in @@ -205,7 +205,7 @@ let hashMap_try_resize else Ok { self with max_load_factor = (i, i1) } (** [hashmap::{hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 139:4-139:48 *) + Source: 'tests/src/hashmap.rs', lines 140:4-140:48 *) let hashMap_insert (t : Type0) (self : hashMap_t t) (key : usize) (value : t) : result (hashMap_t t) @@ -215,169 +215,169 @@ let hashMap_insert if i > self1.max_load then hashMap_try_resize t self1 else Ok self1 (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 216:4-229:5 *) + Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *) let rec hashMap_contains_key_in_list_loop - (t : Type0) (key : usize) (ls : list_t t) : + (t : Type0) (key : usize) (ls : aList_t t) : Tot (result bool) (decreases (hashMap_contains_key_in_list_loop_decreases t key ls)) = begin match ls with - | List_Cons ckey _ tl -> + | AList_Cons ckey _ tl -> if ckey = key then Ok true else hashMap_contains_key_in_list_loop t key tl - | List_Nil -> Ok false + | AList_Nil -> Ok false end (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 216:4-216:68 *) + Source: 'tests/src/hashmap.rs', lines 217:4-217:69 *) let hashMap_contains_key_in_list - (t : Type0) (key : usize) (ls : list_t t) : result bool = + (t : Type0) (key : usize) (ls : aList_t t) : result bool = hashMap_contains_key_in_list_loop t key ls (** [hashmap::{hashmap::HashMap}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 209:4-209:49 *) + Source: 'tests/src/hashmap.rs', lines 210:4-210:49 *) let hashMap_contains_key (t : Type0) (self : hashMap_t t) (key : usize) : result bool = let* hash = hash_key key in - let i = alloc_vec_Vec_len (list_t t) self.slots in + let i = alloc_vec_Vec_len (aList_t t) self.slots in let* hash_mod = usize_rem hash i in - let* l = - alloc_vec_Vec_index (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots + let* a = + alloc_vec_Vec_index (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) self.slots hash_mod in - hashMap_contains_key_in_list t key l + hashMap_contains_key_in_list t key a (** [hashmap::{hashmap::HashMap}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 234:4-247:5 *) + Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *) let rec hashMap_get_in_list_loop - (t : Type0) (key : usize) (ls : list_t t) : + (t : Type0) (key : usize) (ls : aList_t t) : Tot (result t) (decreases (hashMap_get_in_list_loop_decreases t key ls)) = begin match ls with - | List_Cons ckey cvalue tl -> + | AList_Cons ckey cvalue tl -> if ckey = key then Ok cvalue else hashMap_get_in_list_loop t key tl - | List_Nil -> Fail Failure + | AList_Nil -> Fail Failure end (** [hashmap::{hashmap::HashMap}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 234:4-234:70 *) -let hashMap_get_in_list (t : Type0) (key : usize) (ls : list_t t) : result t = + Source: 'tests/src/hashmap.rs', lines 235:4-235:71 *) +let hashMap_get_in_list (t : Type0) (key : usize) (ls : aList_t t) : result t = hashMap_get_in_list_loop t key ls (** [hashmap::{hashmap::HashMap}::get]: - Source: 'tests/src/hashmap.rs', lines 249:4-249:55 *) + Source: 'tests/src/hashmap.rs', lines 250:4-250:55 *) let hashMap_get (t : Type0) (self : hashMap_t t) (key : usize) : result t = let* hash = hash_key key in - let i = alloc_vec_Vec_len (list_t t) self.slots in + let i = alloc_vec_Vec_len (aList_t t) self.slots in let* hash_mod = usize_rem hash i in - let* l = - alloc_vec_Vec_index (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots + let* a = + alloc_vec_Vec_index (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) self.slots hash_mod in - hashMap_get_in_list t key l + hashMap_get_in_list t key a (** [hashmap::{hashmap::HashMap}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 255:4-264:5 *) + Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *) let rec hashMap_get_mut_in_list_loop - (t : Type0) (ls : list_t t) (key : usize) : - Tot (result (t & (t -> result (list_t t)))) + (t : Type0) (ls : aList_t t) (key : usize) : + Tot (result (t & (t -> result (aList_t t)))) (decreases (hashMap_get_mut_in_list_loop_decreases t ls key)) = begin match ls with - | List_Cons ckey cvalue tl -> + | AList_Cons ckey cvalue tl -> if ckey = key - then let back = fun ret -> Ok (List_Cons ckey ret tl) in Ok (cvalue, back) + then let back = fun ret -> Ok (AList_Cons ckey ret tl) in Ok (cvalue, back) else let* (x, back) = hashMap_get_mut_in_list_loop t tl key in let back1 = - fun ret -> let* tl1 = back ret in Ok (List_Cons ckey cvalue tl1) in + fun ret -> let* tl1 = back ret in Ok (AList_Cons ckey cvalue tl1) in Ok (x, back1) - | List_Nil -> Fail Failure + | AList_Nil -> Fail Failure end (** [hashmap::{hashmap::HashMap}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 255:4-255:86 *) + Source: 'tests/src/hashmap.rs', lines 256:4-256:87 *) let hashMap_get_mut_in_list - (t : Type0) (ls : list_t t) (key : usize) : - result (t & (t -> result (list_t t))) + (t : Type0) (ls : aList_t t) (key : usize) : + result (t & (t -> result (aList_t t))) = hashMap_get_mut_in_list_loop t ls key (** [hashmap::{hashmap::HashMap}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 267:4-267:67 *) + Source: 'tests/src/hashmap.rs', lines 268:4-268:67 *) let hashMap_get_mut (t : Type0) (self : hashMap_t t) (key : usize) : result (t & (t -> result (hashMap_t t))) = let* hash = hash_key key in - let i = alloc_vec_Vec_len (list_t t) self.slots in + let i = alloc_vec_Vec_len (aList_t t) self.slots in let* hash_mod = usize_rem hash i in - let* (l, index_mut_back) = - alloc_vec_Vec_index_mut (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots + let* (a, index_mut_back) = + alloc_vec_Vec_index_mut (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) self.slots hash_mod in - let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t l key in + let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t a key in let back = fun ret -> - let* l1 = get_mut_in_list_back ret in - let* v = index_mut_back l1 in + let* a1 = get_mut_in_list_back ret in + let* v = index_mut_back a1 in Ok { self with slots = v } in Ok (x, back) (** [hashmap::{hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 275:4-301:5 *) + Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *) let rec hashMap_remove_from_list_loop - (t : Type0) (key : usize) (ls : list_t t) : - Tot (result ((option t) & (list_t t))) + (t : Type0) (key : usize) (ls : aList_t t) : + Tot (result ((option t) & (aList_t t))) (decreases (hashMap_remove_from_list_loop_decreases t key ls)) = begin match ls with - | List_Cons ckey x tl -> + | AList_Cons ckey x tl -> if ckey = key then let (mv_ls, _) = - core_mem_replace (list_t t) (List_Cons ckey x tl) List_Nil in + core_mem_replace (aList_t t) (AList_Cons ckey x tl) AList_Nil in begin match mv_ls with - | List_Cons _ cvalue tl1 -> Ok (Some cvalue, tl1) - | List_Nil -> Fail Failure + | AList_Cons _ cvalue tl1 -> Ok (Some cvalue, tl1) + | AList_Nil -> Fail Failure end else let* (o, tl1) = hashMap_remove_from_list_loop t key tl in - Ok (o, List_Cons ckey x tl1) - | List_Nil -> Ok (None, List_Nil) + Ok (o, AList_Cons ckey x tl1) + | AList_Nil -> Ok (None, AList_Nil) end (** [hashmap::{hashmap::HashMap}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 275:4-275:69 *) + Source: 'tests/src/hashmap.rs', lines 276:4-276:70 *) let hashMap_remove_from_list - (t : Type0) (key : usize) (ls : list_t t) : - result ((option t) & (list_t t)) + (t : Type0) (key : usize) (ls : aList_t t) : + result ((option t) & (aList_t t)) = hashMap_remove_from_list_loop t key ls (** [hashmap::{hashmap::HashMap}::remove]: - Source: 'tests/src/hashmap.rs', lines 304:4-304:52 *) + Source: 'tests/src/hashmap.rs', lines 305:4-305:52 *) let hashMap_remove (t : Type0) (self : hashMap_t t) (key : usize) : result ((option t) & (hashMap_t t)) = let* hash = hash_key key in - let i = alloc_vec_Vec_len (list_t t) self.slots in + let i = alloc_vec_Vec_len (aList_t t) self.slots in let* hash_mod = usize_rem hash i in - let* (l, index_mut_back) = - alloc_vec_Vec_index_mut (list_t t) usize - (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots + let* (a, index_mut_back) = + alloc_vec_Vec_index_mut (aList_t t) usize + (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) self.slots hash_mod in - let* (x, l1) = hashMap_remove_from_list t key l in + let* (x, a1) = hashMap_remove_from_list t key a in begin match x with - | None -> let* v = index_mut_back l1 in Ok (None, { self with slots = v }) + | None -> let* v = index_mut_back a1 in Ok (None, { self with slots = v }) | Some x1 -> let* i1 = usize_sub self.num_entries 1 in - let* v = index_mut_back l1 in + let* v = index_mut_back a1 in Ok (Some x1, { self with num_entries = i1; slots = v }) end (** [hashmap::insert_on_disk]: - Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *) + Source: 'tests/src/hashmap.rs', lines 336:0-336:43 *) let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st1, hm) = utils_deserialize st in @@ -385,7 +385,7 @@ let insert_on_disk utils_serialize hm1 st1 (** [hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *) + Source: 'tests/src/hashmap.rs', lines 351:0-351:10 *) let test1 : result unit = let* hm = hashMap_new u64 in let* hm1 = hashMap_insert u64 hm 0 42 in diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti index f2f305e6..9362150d 100644 --- a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti +++ b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti @@ -7,10 +7,10 @@ include Hashmap.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::utils::deserialize]: - Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) + Source: 'tests/src/hashmap.rs', lines 331:4-331:47 *) val utils_deserialize : state -> result (state & (hashMap_t u64)) (** [hashmap::utils::serialize]: - Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) + Source: 'tests/src/hashmap.rs', lines 326:4-326:46 *) val utils_serialize : hashMap_t u64 -> state -> result (state & unit) diff --git a/tests/fstar/hashmap/Hashmap.Types.fst b/tests/fstar/hashmap/Hashmap.Types.fst index 818cb9d1..a10bd16c 100644 --- a/tests/fstar/hashmap/Hashmap.Types.fst +++ b/tests/fstar/hashmap/Hashmap.Types.fst @@ -6,19 +6,19 @@ include Hashmap.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [hashmap::List] - Source: 'tests/src/hashmap.rs', lines 29:0-29:16 *) -type list_t (t : Type0) = -| List_Cons : usize -> t -> list_t t -> list_t t -| List_Nil : list_t t +(** [hashmap::AList] + Source: 'tests/src/hashmap.rs', lines 30:0-30:17 *) +type aList_t (t : Type0) = +| AList_Cons : usize -> t -> aList_t t -> aList_t t +| AList_Nil : aList_t t (** [hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 45:0-45:21 *) + Source: 'tests/src/hashmap.rs', lines 46:0-46:21 *) type hashMap_t (t : Type0) = { num_entries : usize; max_load_factor : (usize & usize); max_load : usize; - slots : alloc_vec_Vec (list_t t); + slots : alloc_vec_Vec (aList_t t); } -- cgit v1.2.3