diff options
Diffstat (limited to 'tests/hashmap_on_disk')
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 67 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Clauses.fst | 61 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 742 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Opaque.fsti | 16 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Properties.fst | 48 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Types.fsti | 28 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/Makefile | 47 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/Primitives.fst | 287 |
8 files changed, 0 insertions, 1296 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst deleted file mode 100644 index 55685114..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ /dev/null @@ -1,67 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: templates for the decreases clauses *) -module HashmapMain.Clauses.Template -open Primitives -open HashmapMain.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *) -unfold -let hashmap_hash_map_allocate_slots_decreases (t : Type0) - (slots : vec (hashmap_list_t t)) (n : usize) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *) -unfold -let hashmap_hash_map_clear_slots_decreases (t : Type0) - (slots : vec (hashmap_list_t t)) (i : usize) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *) -unfold -let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) - (value : t) (ls : hashmap_list_t t) : nat = - admit () - -(** [core::num::u32::{9}::MAX] *) -let core_num_u32_max_body : result u32 = Return 4294967295 -let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body - -(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) -unfold -let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) - (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: decreases clause *) -unfold -let hashmap_hash_map_move_elements_decreases (t : Type0) - (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize) - : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *) -unfold -let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: decreases clause *) -unfold -let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *) -unfold -let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : nat = - admit () - -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *) -unfold -let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : nat = - admit () - diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.fst deleted file mode 100644 index b864e32a..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.fst +++ /dev/null @@ -1,61 +0,0 @@ -(** [hashmap]: the decreases clauses *) -module HashmapMain.Clauses -open Primitives -open FStar.List.Tot -open HashmapMain.Types - -#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" - -(** [hashmap::HashMap::allocate_slots]: decreases clause *) -unfold -let hashmap_hash_map_allocate_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t)) - (n : usize) : nat = n - -(** [hashmap::HashMap::clear_slots]: decreases clause *) -unfold -let hashmap_hash_map_clear_slots_decreases (t : Type0) (slots : vec (hashmap_list_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_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) - (ls : hashmap_list_t t) : hashmap_list_t t = - ls - -(** [hashmap::HashMap::move_elements_from_list]: decreases clause *) -unfold -let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) - (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : hashmap_list_t t = - ls - -(** [hashmap::HashMap::move_elements]: decreases clause *) -unfold -let hashmap_hash_map_move_elements_decreases (t : Type0) (ntable : hashmap_hash_map_t t) - (slots : vec (hashmap_list_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_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : hashmap_list_t t = - ls - -(** [hashmap::HashMap::get_in_list]: decreases clause *) -unfold -let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : - hashmap_list_t t = - ls - -(** [hashmap::HashMap::get_mut_in_list]: decreases clause *) -unfold -let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : hashmap_list_t t = - ls - -(** [hashmap::HashMap::remove_from_list]: decreases clause *) -unfold -let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) : hashmap_list_t t = - ls - diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst deleted file mode 100644 index 82b44dbd..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ /dev/null @@ -1,742 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: function definitions *) -module HashmapMain.Funs -open Primitives -include HashmapMain.Types -include HashmapMain.Opaque -include HashmapMain.Clauses - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [hashmap_main::hashmap::hash_key] *) -let hashmap_hash_key_fwd (k : usize) : result usize = Return k - -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) -let rec hashmap_hash_map_allocate_slots_fwd - (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : - Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) - = - if n = 0 - then Return slots - else - begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with - | Fail -> Fail - | Return slots0 -> - begin match usize_sub n 1 with - | Fail -> Fail - | Return i -> - begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with - | Fail -> Fail - | Return v -> Return v - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) -let hashmap_hash_map_new_with_capacity_fwd - (t : Type0) (capacity : usize) (max_load_dividend : usize) - (max_load_divisor : usize) : - result (hashmap_hash_map_t t) - = - let v = vec_new (hashmap_list_t t) in - begin match hashmap_hash_map_allocate_slots_fwd t v capacity with - | Fail -> Fail - | Return slots -> - begin match usize_mul capacity max_load_dividend with - | Fail -> Fail - | Return i -> - begin match usize_div i max_load_divisor with - | Fail -> Fail - | Return i0 -> - Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 - slots) - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::new] *) -let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail -> Fail - | Return hm -> Return hm - end - -(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) -let rec hashmap_hash_map_clear_slots_fwd_back - (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : - Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_clear_slots_decreases t slots i)) - = - let i0 = vec_len (hashmap_list_t t) slots in - if i < i0 - then - begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil - with - | Fail -> Fail - | Return slots0 -> - begin match usize_add i 1 with - | Fail -> Fail - | Return i1 -> - begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail -> Fail - | Return slots1 -> Return slots1 - end - end - end - else Return slots - -(** [hashmap_main::hashmap::HashMap::{0}::clear] *) -let hashmap_hash_map_clear_fwd_back - (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match - hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - -(** [hashmap_main::hashmap::HashMap::{0}::len] *) -let hashmap_hash_map_len_fwd - (t : Type0) (self : hashmap_hash_map_t t) : result usize = - Return self.hashmap_hash_map_num_entries - -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -let rec hashmap_hash_map_insert_in_list_fwd - (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : - Tot (result bool) - (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls)) - = - begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return false - else - begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with - | Fail -> Fail - | Return b -> Return b - end - | HashmapListNil -> Return true - end - -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -let rec hashmap_hash_map_insert_in_list_back - (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : - Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls)) - = - begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return (HashmapListCons ckey value ls0) - else - begin match hashmap_hash_map_insert_in_list_back t key value ls0 with - | Fail -> Fail - | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) - end - | HashmapListNil -> - let l = HashmapListNil in Return (HashmapListCons key value l) - end - -(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) -let hashmap_hash_map_insert_no_resize_fwd_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : - result (hashmap_hash_map_t t) - = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_insert_in_list_fwd t key value l with - | Fail -> Fail - | Return inserted -> - if inserted - then - begin match usize_add self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail - | Return i0 -> - begin match hashmap_hash_map_insert_in_list_back t key value l - with - | Fail -> Fail - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - else - begin match hashmap_hash_map_insert_in_list_back t key value l with - | Fail -> Fail - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end - end - -(** [core::num::u32::{9}::MAX] *) -let core_num_u32_max_body : result u32 = Return 4294967295 -let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body - -(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) -let rec hashmap_hash_map_move_elements_from_list_fwd_back - (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : - Tot (result (hashmap_hash_map_t t)) - (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls)) - = - begin match ls with - | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> Fail - | Return ntable0 -> - begin match - hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail -> Fail - | Return ntable1 -> Return ntable1 - end - end - | HashmapListNil -> Return ntable - end - -(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) -let rec hashmap_hash_map_move_elements_fwd_back - (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) - (i : usize) : - Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))) - (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i)) - = - let i0 = vec_len (hashmap_list_t t) slots in - if i < i0 - then - begin match vec_index_mut_fwd (hashmap_list_t t) slots i with - | Fail -> Fail - | Return l -> - let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls - with - | Fail -> Fail - | Return ntable0 -> - let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with - | Fail -> Fail - | Return slots0 -> - begin match usize_add i 1 with - | Fail -> Fail - | Return i1 -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with - | Fail -> Fail - | Return (ntable1, slots1) -> Return (ntable1, slots1) - end - end - end - end - end - else Return (ntable, slots) - -(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) -let hashmap_hash_map_try_resize_fwd_back - (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail -> Fail - | Return max_usize -> - let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_div max_usize 2 with - | Fail -> Fail - | Return n1 -> - let (i, i0) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i with - | Fail -> Fail - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail -> Fail - | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail -> Fail - | Return ntable -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable - self.hashmap_hash_map_slots 0 with - | Fail -> Fail - | Return (ntable0, _) -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - (i, i0) ntable0.hashmap_hash_map_max_load - ntable0.hashmap_hash_map_slots) - end - end - end - else - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, - i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::insert] *) -let hashmap_hash_map_insert_fwd_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : - result (hashmap_hash_map_t t) - = - begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> Fail - | Return self0 -> - begin match hashmap_hash_map_len_fwd t self0 with - | Fail -> Fail - | Return i -> - if i > self0.hashmap_hash_map_max_load - then - begin match hashmap_hash_map_try_resize_fwd_back t self0 with - | Fail -> Fail - | Return self1 -> Return self1 - end - else Return self0 - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) -let rec hashmap_hash_map_contains_key_in_list_fwd - (t : Type0) (key : usize) (ls : hashmap_list_t t) : - Tot (result bool) - (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey x ls0 -> - if ckey = key - then Return true - else - begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with - | Fail -> Fail - | Return b -> Return b - end - | HashmapListNil -> Return false - end - -(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) -let hashmap_hash_map_contains_key_fwd - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_contains_key_in_list_fwd t key l with - | Fail -> Fail - | Return b -> Return b - end - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) -let rec hashmap_hash_map_get_in_list_fwd - (t : Type0) (key : usize) (ls : hashmap_list_t t) : - Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return cvalue - else - begin match hashmap_hash_map_get_in_list_fwd t key ls0 with - | Fail -> Fail - | Return x -> Return x - end - | HashmapListNil -> Fail - end - -(** [hashmap_main::hashmap::HashMap::{0}::get] *) -let hashmap_hash_map_get_fwd - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_get_in_list_fwd t key l with - | Fail -> Fail - | Return x -> Return x - end - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) -let rec hashmap_hash_map_get_mut_in_list_fwd - (t : Type0) (key : usize) (ls : hashmap_list_t t) : - Tot (result t) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return cvalue - else - begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with - | Fail -> Fail - | Return x -> Return x - end - | HashmapListNil -> Fail - end - -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) -let rec hashmap_hash_map_get_mut_in_list_back - (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) : - Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return (HashmapListCons ckey ret ls0) - else - begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with - | Fail -> Fail - | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) - end - | HashmapListNil -> Fail - end - -(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) -let hashmap_hash_map_get_mut_fwd - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_get_mut_in_list_fwd t key l with - | Fail -> Fail - | Return x -> Return x - end - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) -let hashmap_hash_map_get_mut_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) : - result (hashmap_hash_map_t t) - = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_get_mut_in_list_back t key l ret with - | Fail -> Fail - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod l0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) -let rec hashmap_hash_map_remove_from_list_fwd - (t : Type0) (key : usize) (ls : hashmap_list_t t) : - Tot (result (option t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey x tl -> - if ckey = key - then - let mv_ls = - mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) - HashmapListNil in - begin match mv_ls with - | HashmapListCons i cvalue tl0 -> Return (Some cvalue) - | HashmapListNil -> Fail - end - else - begin match hashmap_hash_map_remove_from_list_fwd t key tl with - | Fail -> Fail - | Return opt -> Return opt - end - | HashmapListNil -> Return None - end - -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) -let rec hashmap_hash_map_remove_from_list_back - (t : Type0) (key : usize) (ls : hashmap_list_t t) : - Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) - = - begin match ls with - | HashmapListCons ckey x tl -> - if ckey = key - then - let mv_ls = - mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) - HashmapListNil in - begin match mv_ls with - | HashmapListCons i cvalue tl0 -> Return tl0 - | HashmapListNil -> Fail - end - else - begin match hashmap_hash_map_remove_from_list_back t key tl with - | Fail -> Fail - | Return tl0 -> Return (HashmapListCons ckey x tl0) - end - | HashmapListNil -> Return HashmapListNil - end - -(** [hashmap_main::hashmap::HashMap::{0}::remove] *) -let hashmap_hash_map_remove_fwd - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail -> Fail - | Return x -> - begin match x with - | None -> Return None - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail - | Return _ -> Return (Some x0) - end - end - end - end - end - end - -(** [hashmap_main::hashmap::HashMap::{0}::remove] *) -let hashmap_hash_map_remove_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : - result (hashmap_hash_map_t t) - = - begin match hashmap_hash_key_fwd key with - | Fail -> Fail - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail -> Fail - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail -> Fail - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail -> Fail - | Return x -> - begin match x with - | None -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail -> Fail - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail - | Return i0 -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail -> Fail - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end - end - end - end - -(** [hashmap_main::hashmap::test1] *) -let hashmap_test1_fwd : result unit = - begin match hashmap_hash_map_new_fwd u64 with - | Fail -> Fail - | Return hm -> - begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with - | Fail -> Fail - | Return hm0 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail -> Fail - | Return hm1 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail -> Fail - | Return hm2 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail -> Fail - | Return hm3 -> - begin match hashmap_hash_map_get_fwd u64 hm3 128 with - | Fail -> Fail - | Return i -> - if not (i = 18) - then Fail - else - begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with - | Fail -> Fail - | Return hm4 -> - begin match hashmap_hash_map_get_fwd u64 hm4 1024 with - | Fail -> Fail - | Return i0 -> - if not (i0 = 56) - then Fail - else - begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with - | Fail -> Fail - | Return x -> - begin match x with - | None -> Fail - | Some x0 -> - if not (x0 = 56) - then Fail - else - begin match - hashmap_hash_map_remove_back u64 hm4 1024 with - | Fail -> Fail - | Return hm5 -> - begin match hashmap_hash_map_get_fwd u64 hm5 0 - with - | Fail -> Fail - | Return i1 -> - if not (i1 = 42) - then Fail - else - begin match - hashmap_hash_map_get_fwd u64 hm5 128 with - | Fail -> Fail - | Return i2 -> - if not (i2 = 18) - then Fail - else - begin match - hashmap_hash_map_get_fwd u64 hm5 1056 - with - | Fail -> Fail - | Return i3 -> - if not (i3 = 256) - then Fail - else Return () - end - end - end - end - end - end - end - end - end - end - end - end - end - end - -(** Unit test for [hashmap_main::hashmap::test1] *) -let _ = assert_norm (hashmap_test1_fwd = Return ()) - -(** [hashmap_main::insert_on_disk] *) -let insert_on_disk_fwd - (key : usize) (value : u64) (st : state) : result (state & unit) = - begin match hashmap_utils_deserialize_fwd st with - | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail -> Fail - | Return hm0 -> - begin match hashmap_utils_serialize_fwd hm0 st0 with - | Fail -> Fail - | Return (st1, _) -> Return (st1, ()) - end - end - end - -(** [hashmap_main::main] *) -let main_fwd : result unit = Return () - -(** Unit test for [hashmap_main::main] *) -let _ = assert_norm (main_fwd = Return ()) - diff --git a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/hashmap_on_disk/HashmapMain.Opaque.fsti deleted file mode 100644 index 6e54ea10..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti +++ /dev/null @@ -1,16 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: opaque function definitions *) -module HashmapMain.Opaque -open Primitives -include HashmapMain.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [hashmap_main::hashmap_utils::deserialize] *) -val hashmap_utils_deserialize_fwd - : state -> result (state & (hashmap_hash_map_t u64)) - -(** [hashmap_main::hashmap_utils::serialize] *) -val hashmap_utils_serialize_fwd - : hashmap_hash_map_t u64 -> state -> result (state & unit) - diff --git a/tests/hashmap_on_disk/HashmapMain.Properties.fst b/tests/hashmap_on_disk/HashmapMain.Properties.fst deleted file mode 100644 index 4df039a8..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Properties.fst +++ /dev/null @@ -1,48 +0,0 @@ -(** Properties about the hashmap written on disk *) -module HashmapMain.Properties -open Primitives -open HashmapMain.Funs - -#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" - -/// Below, we focus on the functions to read from disk/write to disk to showcase -/// how such reasoning which mixes opaque functions together with a state-error -/// monad can be performed. - -(*** Hypotheses *) - -/// [state_v] gives us the hash map currently stored on disk -assume -val state_v : state -> hashmap_hash_map_t u64 - -/// [serialize] updates the hash map stored on disk -assume -val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma ( - match hashmap_utils_serialize_fwd hm st with - | Fail -> True - | Return (st', ()) -> state_v st' == hm) - [SMTPat (hashmap_utils_serialize_fwd hm st)] - -/// [deserialize] gives us the hash map stored on disk, without updating it -assume -val deserialize_lem (st : state) : Lemma ( - match hashmap_utils_deserialize_fwd st with - | Fail -> True - | Return (st', hm) -> hm == state_v st /\ st' == st) - [SMTPat (hashmap_utils_deserialize_fwd st)] - -(*** Lemmas *) - -/// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk -/// is exactly the hash map produced from inserting the binding ([key], [value]) -/// in the hash map previously stored on disk. -val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma ( - match insert_on_disk_fwd key value st with - | Fail -> True - | Return (st', ()) -> - let hm = state_v st in - match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail -> False - | Return hm' -> hm' == state_v st') - -let insert_on_disk_fwd_lem key value st = () diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti deleted file mode 100644 index ce4d6485..00000000 --- a/tests/hashmap_on_disk/HashmapMain.Types.fsti +++ /dev/null @@ -1,28 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: type definitions *) -module HashmapMain.Types -open Primitives - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [hashmap_main::hashmap::List] *) -type hashmap_list_t (t : Type0) = -| HashmapListCons : usize -> t -> hashmap_list_t t -> hashmap_list_t t -| HashmapListNil : hashmap_list_t t - -(** [hashmap_main::hashmap::HashMap] *) -type hashmap_hash_map_t (t : Type0) = -{ - hashmap_hash_map_num_entries : usize; - hashmap_hash_map_max_load_factor : (usize & usize); - hashmap_hash_map_max_load : usize; - hashmap_hash_map_slots : vec (hashmap_list_t t); -} - -(** [core::num::u32::{9}::MAX] *) -let core_num_u32_max_body : result u32 = Return 4294967295 -let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body - -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile deleted file mode 100644 index a16b0edb..00000000 --- a/tests/hashmap_on_disk/Makefile +++ /dev/null @@ -1,47 +0,0 @@ -INCLUDE_DIRS = . - -FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) - -FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints - -FSTAR_OPTIONS = $(FSTAR_HINTS) \ - --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ - --warn_error '+241@247+285-274' \ - -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj - -FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) - -# The F* roots are used to compute the dependency graph, and generate the .depend file -FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) - -# Build all the files -all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) - -# This is the right way to ensure the .depend file always gets re-built. -ifeq (,$(filter %-in,$(MAKECMDGOALS))) -ifndef NODEPEND -ifndef MAKE_RESTARTS -.depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ - -.PHONY: .FORCE -.FORCE: -endif -endif - -include .depend -endif - -# For the interactive mode -%.fst-in %.fsti-in: - @echo $(FSTAR_OPTIONS) - -# Generete the .checked files in batch mode -%.checked: - $(FSTAR) $(FSTAR_OPTIONS) $< && \ - touch -c $@ - -.PHONY: clean -clean: - rm -f obj/* diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst deleted file mode 100644 index 96138e46..00000000 --- a/tests/hashmap_on_disk/Primitives.fst +++ /dev/null @@ -1,287 +0,0 @@ -/// This file lists primitive and assumed functions and types -module Primitives -open FStar.Mul -open FStar.List.Tot - -#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" - -(*** Utilities *) -val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : - ls':list a{ - length ls' = length ls /\ - index ls' i == x - } -#push-options "--fuel 1" -let rec list_update #a ls i x = - match ls with - | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x -#pop-options - -(*** Result *) -type result (a : Type0) : Type0 = -| Return : v:a -> result a -| Fail : result a - -// Monadic bind and return. -// Re-definining those allows us to customize the result of the monadic notations -// like: `y <-- f x;` -let return (#a : Type0) (x:a) : result a = Return x -let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = - match m with - | Return x -> f x - | Fail -> Fail - -// Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail - -// Normalize and unwrap a successful result (used for globals). -let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x - -(*** Misc *) -type char = FStar.Char.char -type string = string - -let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x -let mem_replace_back (a : Type0) (x : a) (y : a) : a = y - -(*** Scalars *) -/// Rk.: most of the following code was at least partially generated - -let isize_min : int = -9223372036854775808 // TODO: should be opaque -let isize_max : int = 9223372036854775807 // TODO: should be opaque -let i8_min : int = -128 -let i8_max : int = 127 -let i16_min : int = -32768 -let i16_max : int = 32767 -let i32_min : int = -2147483648 -let i32_max : int = 2147483647 -let i64_min : int = -9223372036854775808 -let i64_max : int = 9223372036854775807 -let i128_min : int = -170141183460469231731687303715884105728 -let i128_max : int = 170141183460469231731687303715884105727 -let usize_min : int = 0 -let usize_max : int = 4294967295 // TODO: should be opaque -let u8_min : int = 0 -let u8_max : int = 255 -let u16_min : int = 0 -let u16_max : int = 65535 -let u32_min : int = 0 -let u32_max : int = 4294967295 -let u64_min : int = 0 -let u64_max : int = 18446744073709551615 -let u128_min : int = 0 -let u128_max : int = 340282366920938463463374607431768211455 - -type scalar_ty = -| Isize -| I8 -| I16 -| I32 -| I64 -| I128 -| Usize -| U8 -| U16 -| U32 -| U64 -| U128 - -let scalar_min (ty : scalar_ty) : int = - match ty with - | Isize -> isize_min - | I8 -> i8_min - | I16 -> i16_min - | I32 -> i32_min - | I64 -> i64_min - | I128 -> i128_min - | Usize -> usize_min - | U8 -> u8_min - | U16 -> u16_min - | U32 -> u32_min - | U64 -> u64_min - | U128 -> u128_min - -let scalar_max (ty : scalar_ty) : int = - match ty with - | Isize -> isize_max - | I8 -> i8_max - | I16 -> i16_max - | I32 -> i32_max - | I64 -> i64_max - | I128 -> i128_max - | Usize -> usize_max - | U8 -> u8_max - | U16 -> u16_max - | U32 -> u32_max - | U64 -> u64_max - | U128 -> u128_max - -type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} - -let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail - -let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) - -let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail - -/// The remainder operation -let int_rem (x : int) (y : int{y <> 0}) : int = - if x >= 0 then (x % y) else -(x % y) - -(* Checking consistency with Rust *) -let _ = assert_norm(int_rem 1 2 = 1) -let _ = assert_norm(int_rem (-1) 2 = -1) -let _ = assert_norm(int_rem 1 (-2) = 1) -let _ = assert_norm(int_rem (-1) (-2) = -1) - -let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail - -let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x + y) - -let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x - y) - -let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x * y) - -(** Cast an integer from a [src_ty] to a [tgt_ty] *) -// TODO: check the semantics of casts in Rust -let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = - mk_scalar tgt_ty x - -/// The scalar types -type isize : eqtype = scalar Isize -type i8 : eqtype = scalar I8 -type i16 : eqtype = scalar I16 -type i32 : eqtype = scalar I32 -type i64 : eqtype = scalar I64 -type i128 : eqtype = scalar I128 -type usize : eqtype = scalar Usize -type u8 : eqtype = scalar U8 -type u16 : eqtype = scalar U16 -type u32 : eqtype = scalar U32 -type u64 : eqtype = scalar U64 -type u128 : eqtype = scalar U128 - -/// Negation -let isize_neg = scalar_neg #Isize -let i8_neg = scalar_neg #I8 -let i16_neg = scalar_neg #I16 -let i32_neg = scalar_neg #I32 -let i64_neg = scalar_neg #I64 -let i128_neg = scalar_neg #I128 - -/// Division -let isize_div = scalar_div #Isize -let i8_div = scalar_div #I8 -let i16_div = scalar_div #I16 -let i32_div = scalar_div #I32 -let i64_div = scalar_div #I64 -let i128_div = scalar_div #I128 -let usize_div = scalar_div #Usize -let u8_div = scalar_div #U8 -let u16_div = scalar_div #U16 -let u32_div = scalar_div #U32 -let u64_div = scalar_div #U64 -let u128_div = scalar_div #U128 - -/// Remainder -let isize_rem = scalar_rem #Isize -let i8_rem = scalar_rem #I8 -let i16_rem = scalar_rem #I16 -let i32_rem = scalar_rem #I32 -let i64_rem = scalar_rem #I64 -let i128_rem = scalar_rem #I128 -let usize_rem = scalar_rem #Usize -let u8_rem = scalar_rem #U8 -let u16_rem = scalar_rem #U16 -let u32_rem = scalar_rem #U32 -let u64_rem = scalar_rem #U64 -let u128_rem = scalar_rem #U128 - -/// Addition -let isize_add = scalar_add #Isize -let i8_add = scalar_add #I8 -let i16_add = scalar_add #I16 -let i32_add = scalar_add #I32 -let i64_add = scalar_add #I64 -let i128_add = scalar_add #I128 -let usize_add = scalar_add #Usize -let u8_add = scalar_add #U8 -let u16_add = scalar_add #U16 -let u32_add = scalar_add #U32 -let u64_add = scalar_add #U64 -let u128_add = scalar_add #U128 - -/// Substraction -let isize_sub = scalar_sub #Isize -let i8_sub = scalar_sub #I8 -let i16_sub = scalar_sub #I16 -let i32_sub = scalar_sub #I32 -let i64_sub = scalar_sub #I64 -let i128_sub = scalar_sub #I128 -let usize_sub = scalar_sub #Usize -let u8_sub = scalar_sub #U8 -let u16_sub = scalar_sub #U16 -let u32_sub = scalar_sub #U32 -let u64_sub = scalar_sub #U64 -let u128_sub = scalar_sub #U128 - -/// Multiplication -let isize_mul = scalar_mul #Isize -let i8_mul = scalar_mul #I8 -let i16_mul = scalar_mul #I16 -let i32_mul = scalar_mul #I32 -let i64_mul = scalar_mul #I64 -let i128_mul = scalar_mul #I128 -let usize_mul = scalar_mul #Usize -let u8_mul = scalar_mul #U8 -let u16_mul = scalar_mul #U16 -let u32_mul = scalar_mul #U32 -let u64_mul = scalar_mul #U64 -let u128_mul = scalar_mul #U128 - -(*** Vector *) -type vec (a : Type0) = v:list a{length v <= usize_max} - -let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); [] -let vec_len (a : Type0) (v : vec a) : usize = length v - -// The **forward** function shouldn't be used -let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () -let vec_push_back (a : Type0) (v : vec a) (x : a) : - Pure (result (vec a)) - (requires True) - (ensures (fun res -> - match res with - | Fail -> True - | Return v' -> length v' = length v + 1)) = - if length v < usize_max then begin - (**) assert_norm(length [x] == 1); - (**) append_length v [x]; - (**) assert(length (append v [x]) = length v + 1); - Return (append v [x]) - end - else Fail - -// The **forward** function shouldn't be used -let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail -let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail - -// The **backward** function shouldn't be used -let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail -let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail - -let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail -let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail - |