diff options
author | Son HO | 2024-05-27 09:39:39 +0200 |
---|---|---|
committer | GitHub | 2024-05-27 09:39:39 +0200 |
commit | aeff52b13b9b3068efcc4a805a9786bf2053d141 (patch) | |
tree | 229e6fc225bf8456a01985cd3b583e510acc3886 /tests/fstar/hashmap_main | |
parent | 3ff6d93822fe5b2e233d4b12b88b38839c8533c5 (diff) | |
parent | 4971b7edf4538144df735f9fa5327fe4d0e2e003 (diff) |
Merge branch 'main' into unsigned-max
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.Clauses.Template.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst) | 18 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.Clauses.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst) | 0 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.Funs.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst) | 64 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.FunsExternal.fsti (renamed from tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti) | 4 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.Properties.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst) | 0 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.Types.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Types.fst) | 4 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/HashmapMain.TypesExternal.fsti (renamed from tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti) | 0 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/Makefile (renamed from tests/fstar/hashmap_on_disk/Makefile) | 0 | ||||
-rw-r--r-- | tests/fstar/hashmap_main/Primitives.fst (renamed from tests/fstar/hashmap_on_disk/Primitives.fst) | 0 |
9 files changed, 45 insertions, 45 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_main/HashmapMain.Clauses.Template.fst index 0715bdcb..cdd73210 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/fstar/hashmap_main/HashmapMain.Clauses.Template.fst @@ -7,35 +7,35 @@ open HashmapMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: decreases clause - Source: 'tests/src/hashmap.rs', lines 50:4-56:5 *) + Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) unfold let hashmap_HashMap_allocate_slots_loop_decreases (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: decreases clause - Source: 'tests/src/hashmap.rs', lines 80:4-88:5 *) + Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) unfold let hashmap_HashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 97:4-114:5 *) + Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) unfold let hashmap_HashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 183:4-196:5 *) + Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) unfold let hashmap_HashMap_move_elements_from_list_loop_decreases (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: decreases clause - Source: 'tests/src/hashmap.rs', lines 171:4-180:5 *) + Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) unfold let hashmap_HashMap_move_elements_loop_decreases (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) @@ -43,28 +43,28 @@ let hashmap_HashMap_move_elements_loop_decreases (t : Type0) admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 206:4-219:5 *) + Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) unfold let hashmap_HashMap_contains_key_in_list_loop_decreases (t : Type0) (key : usize) (ls : hashmap_List_t t) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 224:4-237:5 *) + Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) unfold let hashmap_HashMap_get_in_list_loop_decreases (t : Type0) (key : usize) (ls : hashmap_List_t t) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 245:4-254:5 *) + Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) unfold let hashmap_HashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : hashmap_List_t t) (key : usize) : nat = admit () (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 265:4-291:5 *) + Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) unfold let hashmap_HashMap_remove_from_list_loop_decreases (t : Type0) (key : usize) (ls : hashmap_List_t t) : nat = diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_main/HashmapMain.Clauses.fst index be5a4ab1..be5a4ab1 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst +++ b/tests/fstar/hashmap_main/HashmapMain.Clauses.fst diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_main/HashmapMain.Funs.fst index 4a032207..c88a746e 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_main/HashmapMain.Funs.fst @@ -9,12 +9,12 @@ include HashmapMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 27:0-27:32 *) + Source: 'tests/src/hashmap.rs', lines 35:0-35:32 *) let 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 50:4-56:5 *) + Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) let rec hashmap_HashMap_allocate_slots_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : Tot (result (alloc_vec_Vec (hashmap_List_t t))) @@ -29,7 +29,7 @@ let rec hashmap_HashMap_allocate_slots_loop else Ok slots (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 50:4-50:76 *) + Source: 'tests/src/hashmap.rs', lines 58:4-58:76 *) let hashmap_HashMap_allocate_slots (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : result (alloc_vec_Vec (hashmap_List_t t)) @@ -37,7 +37,7 @@ let hashmap_HashMap_allocate_slots hashmap_HashMap_allocate_slots_loop t slots n (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 59:4-63:13 *) + Source: 'tests/src/hashmap.rs', lines 67:4-71:13 *) let hashmap_HashMap_new_with_capacity (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -57,12 +57,12 @@ let hashmap_HashMap_new_with_capacity } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]: - Source: 'tests/src/hashmap.rs', lines 75:4-75:24 *) + Source: 'tests/src/hashmap.rs', lines 83:4-83:24 *) let hashmap_HashMap_new (t : Type0) : result (hashmap_HashMap_t t) = hashmap_HashMap_new_with_capacity t 32 4 5 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 80:4-88:5 *) + Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) let rec hashmap_HashMap_clear_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : Tot (result (alloc_vec_Vec (hashmap_List_t t))) @@ -81,20 +81,20 @@ let rec hashmap_HashMap_clear_loop else Ok slots (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: - Source: 'tests/src/hashmap.rs', lines 80:4-80:27 *) + Source: 'tests/src/hashmap.rs', lines 88:4-88:27 *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = let* hm = hashmap_HashMap_clear_loop t self.slots 0 in Ok { self with num_entries = 0; slots = hm } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: - Source: 'tests/src/hashmap.rs', lines 90:4-90:30 *) + Source: 'tests/src/hashmap.rs', lines 98:4-98:30 *) let hashmap_HashMap_len (t : Type0) (self : hashmap_HashMap_t t) : result usize = Ok self.num_entries (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 97:4-114:5 *) + Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) let rec hashmap_HashMap_insert_in_list_loop (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : Tot (result (bool & (hashmap_List_t t))) @@ -111,7 +111,7 @@ let rec hashmap_HashMap_insert_in_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 97:4-97:71 *) + Source: 'tests/src/hashmap.rs', lines 105:4-105:71 *) let hashmap_HashMap_insert_in_list (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : result (bool & (hashmap_List_t t)) @@ -119,7 +119,7 @@ let hashmap_HashMap_insert_in_list hashmap_HashMap_insert_in_list_loop t key value ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 117:4-117:54 *) + Source: 'tests/src/hashmap.rs', lines 125:4-125:54 *) let hashmap_HashMap_insert_no_resize (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : result (hashmap_HashMap_t t) @@ -140,7 +140,7 @@ let hashmap_HashMap_insert_no_resize else let* v = index_mut_back l1 in Ok { self with slots = v } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 183:4-196:5 *) + Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) let rec hashmap_HashMap_move_elements_from_list_loop (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : Tot (result (hashmap_HashMap_t t)) @@ -155,7 +155,7 @@ let rec hashmap_HashMap_move_elements_from_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 183:4-183:72 *) + Source: 'tests/src/hashmap.rs', lines 191:4-191:72 *) let hashmap_HashMap_move_elements_from_list (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : result (hashmap_HashMap_t t) @@ -163,7 +163,7 @@ let hashmap_HashMap_move_elements_from_list hashmap_HashMap_move_elements_from_list_loop t ntable ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 171:4-180:5 *) + Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) let rec hashmap_HashMap_move_elements_loop (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : @@ -185,7 +185,7 @@ let rec hashmap_HashMap_move_elements_loop else Ok (ntable, slots) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 171:4-171:95 *) + Source: 'tests/src/hashmap.rs', lines 179:4-179:95 *) let hashmap_HashMap_move_elements (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : @@ -194,7 +194,7 @@ let hashmap_HashMap_move_elements hashmap_HashMap_move_elements_loop t ntable slots i (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 140:4-140:28 *) + Source: 'tests/src/hashmap.rs', lines 148:4-148:28 *) let hashmap_HashMap_try_resize (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = let* max_usize = scalar_cast U32 Usize core_u32_max in @@ -214,7 +214,7 @@ let hashmap_HashMap_try_resize else Ok { self with max_load_factor = (i, i1) } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]: - Source: 'tests/src/hashmap.rs', lines 129:4-129:48 *) + Source: 'tests/src/hashmap.rs', lines 137:4-137:48 *) let hashmap_HashMap_insert (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : result (hashmap_HashMap_t t) @@ -224,7 +224,7 @@ let hashmap_HashMap_insert if i > self1.max_load then hashmap_HashMap_try_resize t self1 else Ok self1 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 206:4-219:5 *) + Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) let rec hashmap_HashMap_contains_key_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result bool) @@ -239,13 +239,13 @@ let rec hashmap_HashMap_contains_key_in_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 206:4-206:68 *) + Source: 'tests/src/hashmap.rs', lines 214:4-214:68 *) let hashmap_HashMap_contains_key_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result bool = hashmap_HashMap_contains_key_in_list_loop t key ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 199:4-199:49 *) + Source: 'tests/src/hashmap.rs', lines 207:4-207:49 *) let hashmap_HashMap_contains_key (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result bool = let* hash = hashmap_hash_key key in @@ -258,7 +258,7 @@ let hashmap_HashMap_contains_key hashmap_HashMap_contains_key_in_list t key l (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 224:4-237:5 *) + Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) let rec hashmap_HashMap_get_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result t) @@ -271,13 +271,13 @@ let rec hashmap_HashMap_get_in_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 224:4-224:70 *) + Source: 'tests/src/hashmap.rs', lines 232:4-232:70 *) let hashmap_HashMap_get_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result t = hashmap_HashMap_get_in_list_loop t key ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]: - Source: 'tests/src/hashmap.rs', lines 239:4-239:55 *) + Source: 'tests/src/hashmap.rs', lines 247:4-247:55 *) let hashmap_HashMap_get (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result t = let* hash = hashmap_hash_key key in @@ -290,7 +290,7 @@ let hashmap_HashMap_get hashmap_HashMap_get_in_list t key l (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 245:4-254:5 *) + Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) let rec hashmap_HashMap_get_mut_in_list_loop (t : Type0) (ls : hashmap_List_t t) (key : usize) : Tot (result (t & (t -> result (hashmap_List_t t)))) @@ -312,7 +312,7 @@ let rec hashmap_HashMap_get_mut_in_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 245:4-245:86 *) + Source: 'tests/src/hashmap.rs', lines 253:4-253:86 *) let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result (t & (t -> result (hashmap_List_t t))) @@ -320,7 +320,7 @@ let hashmap_HashMap_get_mut_in_list hashmap_HashMap_get_mut_in_list_loop t ls key (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 257:4-257:67 *) + Source: 'tests/src/hashmap.rs', lines 265:4-265:67 *) let hashmap_HashMap_get_mut (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result (t & (t -> result (hashmap_HashMap_t t))) @@ -341,7 +341,7 @@ let hashmap_HashMap_get_mut Ok (x, back) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 265:4-291:5 *) + Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) let rec hashmap_HashMap_remove_from_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result ((option t) & (hashmap_List_t t))) @@ -365,7 +365,7 @@ let rec hashmap_HashMap_remove_from_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 265:4-265:69 *) + Source: 'tests/src/hashmap.rs', lines 273:4-273:69 *) let hashmap_HashMap_remove_from_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result ((option t) & (hashmap_List_t t)) @@ -373,7 +373,7 @@ let hashmap_HashMap_remove_from_list hashmap_HashMap_remove_from_list_loop t key ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]: - Source: 'tests/src/hashmap.rs', lines 294:4-294:52 *) + Source: 'tests/src/hashmap.rs', lines 302:4-302:52 *) let hashmap_HashMap_remove (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result ((option t) & (hashmap_HashMap_t t)) @@ -395,7 +395,7 @@ let hashmap_HashMap_remove end (** [hashmap_main::hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 315:0-315:10 *) + Source: 'tests/src/hashmap.rs', lines 323:0-323:10 *) let hashmap_test1 : result unit = let* hm = hashmap_HashMap_new u64 in let* hm1 = hashmap_HashMap_insert u64 hm 0 42 in @@ -432,7 +432,7 @@ let hashmap_test1 : result unit = end (** [hashmap_main::insert_on_disk]: - Source: 'tests/src/hashmap_main.rs', lines 7:0-7:43 *) + Source: 'tests/src/hashmap_main.rs', lines 13:0-13:43 *) let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st1, hm) = hashmap_utils_deserialize st in @@ -440,7 +440,7 @@ let insert_on_disk hashmap_utils_serialize hm1 st1 (** [hashmap_main::main]: - Source: 'tests/src/hashmap_main.rs', lines 16:0-16:13 *) + Source: 'tests/src/hashmap_main.rs', lines 22:0-22:13 *) let main : result unit = Ok () diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti b/tests/fstar/hashmap_main/HashmapMain.FunsExternal.fsti index 3afc4689..cc20d988 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti +++ b/tests/fstar/hashmap_main/HashmapMain.FunsExternal.fsti @@ -7,12 +7,12 @@ include HashmapMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap_utils::deserialize]: - Source: 'tests/src/hashmap_utils.rs', lines 10:0-10:43 *) + Source: 'tests/src/hashmap_utils.rs', lines 11:0-11:43 *) val hashmap_utils_deserialize : state -> result (state & (hashmap_HashMap_t u64)) (** [hashmap_main::hashmap_utils::serialize]: - Source: 'tests/src/hashmap_utils.rs', lines 5:0-5:42 *) + Source: 'tests/src/hashmap_utils.rs', lines 6:0-6:42 *) val hashmap_utils_serialize : hashmap_HashMap_t u64 -> state -> result (state & unit) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_main/HashmapMain.Properties.fst index beb3dc2c..beb3dc2c 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst +++ b/tests/fstar/hashmap_main/HashmapMain.Properties.fst diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst b/tests/fstar/hashmap_main/HashmapMain.Types.fst index 21d32541..85bcaeea 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst +++ b/tests/fstar/hashmap_main/HashmapMain.Types.fst @@ -7,13 +7,13 @@ include HashmapMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap::List] - Source: 'tests/src/hashmap.rs', lines 19:0-19:16 *) + Source: 'tests/src/hashmap.rs', lines 27:0-27:16 *) type hashmap_List_t (t : Type0) = | Hashmap_List_Cons : usize -> t -> hashmap_List_t t -> hashmap_List_t t | Hashmap_List_Nil : hashmap_List_t t (** [hashmap_main::hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 35:0-35:21 *) + Source: 'tests/src/hashmap.rs', lines 43:0-43:21 *) type hashmap_HashMap_t (t : Type0) = { num_entries : usize; diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_main/HashmapMain.TypesExternal.fsti index 75747408..75747408 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti +++ b/tests/fstar/hashmap_main/HashmapMain.TypesExternal.fsti diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_main/Makefile index fa7d1f36..fa7d1f36 100644 --- a/tests/fstar/hashmap_on_disk/Makefile +++ b/tests/fstar/hashmap_main/Makefile diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_main/Primitives.fst index 9951ccc3..9951ccc3 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_main/Primitives.fst |