diff options
Diffstat (limited to 'tests/lean/hashmap_on_disk/Hashmap')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Funs.lean | 535 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Opaque.lean | 11 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Primitives.lean | 155 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Types.lean | 23 |
4 files changed, 724 insertions, 0 deletions
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean new file mode 100644 index 00000000..a4f2e3e0 --- /dev/null +++ b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean @@ -0,0 +1,535 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: function definitions +import Hashmap.Primitives +import Hashmap.Opaque +import Hashmap.Types + +open result +open hashmap_list_t + +/- [hashmap_main::hashmap::hash_key] -/ +def hashmap_hash_key_fwd (k : USize) : result USize := ret k + +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ +def hashmap_hash_map_allocate_slots_loop_fwd + (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : + result (vec (hashmap_list_t T)) + := + if n > (USize.ofNatCore 0 (by simp)) + then do + let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by simp)) + hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 + else ret slots +termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n +decreasing_by sorry + +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ +def hashmap_hash_map_allocate_slots_fwd + (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : + result (vec (hashmap_list_t T)) + := + hashmap_hash_map_allocate_slots_loop_fwd T slots n + +/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ +def hashmap_hash_map_new_with_capacity_fwd + (T : Type) (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 + let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in + let i <- USize.checked_mul capacity max_load_dividend in + let i0 <- USize.checked_div i max_load_divisor in + ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) (max_load_dividend, + max_load_divisor) i0 slots) + +/- [hashmap_main::hashmap::HashMap::{0}::new] -/ +def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := + hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by simp)) + (USize.ofNatCore 4 (by simp)) (USize.ofNatCore 5 (by simp)) + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_loop_fwd_back + (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : + result (vec (hashmap_list_t T)) + := + let i0 <- vec_len (hashmap_list_t T) slots in + if i < i0 + then ( + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil + in + hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) + else ret slots + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_fwd_back + (T : Type) (slots : vec (hashmap_list_t T)) : + result (vec (hashmap_list_t T)) + := + hashmap_hash_map_clear_slots_loop_fwd_back T slots + (USize.ofNatCore 0 (by simp)) + +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +def hashmap_hash_map_clear_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := + let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + in + ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + +/- [hashmap_main::hashmap::HashMap::{0}::len] -/ +def hashmap_hash_map_len_fwd + (T : Type) (self : hashmap_hash_map_t T) : result USize := + ret self.hashmap_hash_map_num_entries + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_loop_fwd + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then ret false + else hashmap_hash_map_insert_in_list_loop_fwd T key value tl + | HashmapListNil => ret true + end + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_fwd + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := + hashmap_hash_map_insert_in_list_loop_fwd T key value ls + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_loop_back + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then ret (HashmapListCons ckey value tl) + else ( + let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in + ret (HashmapListCons ckey cvalue l)) + | HashmapListNil => + let l <- HashmapListNil in ret (HashmapListCons key value l) + end + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_back + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + hashmap_hash_map_insert_in_list_loop_back T key value ls + +/- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ +def hashmap_hash_map_insert_no_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : + result (hashmap_hash_map_t T) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l in + if inserted + then ( + let i0 <- USize.checked_add self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by simp)) in + let l0 <- hashmap_hash_map_insert_in_list_back T key value l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v)) + else ( + let l0 <- hashmap_hash_map_insert_in_list_back T key value l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) + +/- [core::num::u32::{9}::MAX] -/ +def core_num_u32_max_body : result UInt32 := + ret (UInt32.ofNatCore 4294967295 (by simp)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + match ls with + | HashmapListCons k v tl => + let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | HashmapListNil => ret ntable + end + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + let i0 <- vec_len (hashmap_list_t T) slots in + if i < i0 + then ( + let l <- vec_index_mut_fwd (hashmap_list_t T) slots i in + let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in + let ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in + let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in + hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) + else ret (ntable, slots) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i + +/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ +def hashmap_hash_map_try_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := + let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in + let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by simp)) in + let (i, i0) <- self.hashmap_hash_map_max_load_factor in + let i1 <- USize.checked_div n1 i in + if capacity <= i1 + then ( + let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by simp)) in + let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in + let (ntable0, _) <- + hashmap_hash_map_move_elements_fwd_back T ntable + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by simp)) in + ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) + else + ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + +/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ +def hashmap_hash_map_insert_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : + result (hashmap_hash_map_t T) + := + let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value in + let i <- hashmap_hash_map_len_fwd T self0 in + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back T self0 + else ret self0 + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then ret true + else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl + | HashmapListNil => ret false + end + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ +def hashmap_hash_map_contains_key_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_contains_key_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then ret cvalue + else hashmap_hash_map_get_in_list_loop_fwd T key tl + | HashmapListNil => fail_ panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + hashmap_hash_map_get_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::get] -/ +def hashmap_hash_map_get_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_get_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then ret cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + | HashmapListNil => fail_ panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : + result (hashmap_list_t T) + := + match ls with + | HashmapListCons ckey cvalue tl => + if ckey = key + then ret (HashmapListCons ckey ret0 tl) + else ( + let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 in + ret (HashmapListCons ckey cvalue l)) + | HashmapListNil => fail_ panic + end + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : + result (hashmap_list_t T) + := + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + hashmap_hash_map_get_mut_in_list_fwd T l key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) : + result (hashmap_hash_map_t T) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + l0 in + ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) + HashmapListNil in + match mv_ls with + | HashmapListCons i cvalue tl0 => ret (@some cvalue) + | HashmapListNil => fail_ panic + end + else hashmap_hash_map_remove_from_list_loop_fwd T key tl + | HashmapListNil => ret @none + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (option T) := + hashmap_hash_map_remove_from_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + match ls with + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls <- + mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) + HashmapListNil in + match mv_ls with + | HashmapListCons i cvalue tl0 => ret tl0 + | HashmapListNil => fail_ panic + end + else ( + let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in + ret (HashmapListCons ckey t l)) + | HashmapListNil => ret HashmapListNil + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (option T) := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let x <- hashmap_hash_map_remove_from_list_fwd T key l in + match x with + | @none => ret @none + | @some x0 => + let _ <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by simp)) in + ret (@some x0) + end + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : + result (hashmap_hash_map_t T) + := + let hash <- hashmap_hash_key_fwd key in + let i <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in + let hash_mod <- USize.checked_rem hash i in + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + in + let x <- hashmap_hash_map_remove_from_list_fwd T key l in + match x with + | @none => + let l0 <- hashmap_hash_map_remove_from_list_back T key l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + | @some x0 => + let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by simp)) in + let l0 <- hashmap_hash_map_remove_from_list_back T key l in + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 in + ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + +/- [hashmap_main::hashmap::test1] -/ +def hashmap_test1_fwd : result unit := + let hm <- hashmap_hash_map_new_fwd UInt64 in + let hm0 <- + hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by simp)) + (UInt64.ofNatCore 42 (by simp)) in + let hm1 <- + hashmap_hash_map_insert_fwd_back UInt64 hm0 (USize.ofNatCore 128 (by simp)) + (UInt64.ofNatCore 18 (by simp)) in + let hm2 <- + hashmap_hash_map_insert_fwd_back UInt64 hm1 + (USize.ofNatCore 1024 (by simp)) (UInt64.ofNatCore 138 (by simp)) in + let hm3 <- + hashmap_hash_map_insert_fwd_back UInt64 hm2 + (USize.ofNatCore 1056 (by simp)) (UInt64.ofNatCore 256 (by simp)) in + let i <- hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by simp)) + in + if not (i = (UInt64.ofNatCore 18 (by simp))) + then fail_ panic + else ( + let hm4 <- + hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by simp)) + (UInt64.ofNatCore 56 (by simp)) in + let i0 <- + hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) in + if not (i0 = (UInt64.ofNatCore 56 (by simp))) + then fail_ panic + else ( + let x <- + hashmap_hash_map_remove_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) + in + match x with + | @none => fail_ panic + | @some x0 => + if not (x0 = (UInt64.ofNatCore 56 (by simp))) + then fail_ panic + else ( + let hm5 <- + hashmap_hash_map_remove_back UInt64 hm4 + (USize.ofNatCore 1024 (by simp)) in + let i1 <- + hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by simp)) + in + if not (i1 = (UInt64.ofNatCore 42 (by simp))) + then fail_ panic + else ( + let i2 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 128 (by simp)) in + if not (i2 = (UInt64.ofNatCore 18 (by simp))) + then fail_ panic + else ( + let i3 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 1056 (by simp)) in + if not (i3 = (UInt64.ofNatCore 256 (by simp))) + then fail_ panic + else ret ()))) + end)) + +/- Unit test for [hashmap_main::hashmap::test1] -/ +#assert (hashmap_test1_fwd = ret ()) + +/- [hashmap_main::insert_on_disk] -/ +def insert_on_disk_fwd + (key : USize) (value : UInt64) (st : state) : result (state × unit) := + let (st0, hm) <- hashmap_utils_deserialize_fwd st in + let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in + let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in + ret (st1, ()) + +/- [hashmap_main::main] -/ +def main_fwd : result unit := ret () + +/- Unit test for [hashmap_main::main] -/ +#assert (main_fwd = ret ()) + diff --git a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean new file mode 100644 index 00000000..164995f0 --- /dev/null +++ b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean @@ -0,0 +1,11 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: opaque function definitions +import Hashmap.Primitives +import Hashmap.Types + +/- [hashmap_main::hashmap_utils::deserialize] -/ +axiom hashmap_utils_deserialize_fwd: state → result (state × (hashmap_hash_map_t UInt64)) + +/- [hashmap_main::hashmap_utils::serialize] -/ +axiom hashmap_utils_serialize_fwd: hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean new file mode 100644 index 00000000..83de98db --- /dev/null +++ b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean @@ -0,0 +1,155 @@ +------------- +-- PRELUDE -- +------------- + +-- Results & monadic combinators + +inductive error where + | assertionFailure: error + | integerOverflow: error + | arrayOutOfBounds: error + | maximumSizeExceeded: error + | panic: error +deriving Repr + +open error + +inductive result (α : Type u) where + | ret (v: α): result α + | fail (e: error): result α +deriving Repr + +open result + +-- TODO: is there automated syntax for these discriminators? +def is_ret (α: Type) (r: result α): Bool := + match r with + | result.ret _ => true + | result.fail _ => false + +def eval_global (α: Type) (x: result α) (h: is_ret α x): α := + match x with + | result.fail _ => by contradiction + | result.ret x => x + +def bind (x: result α) (f: α -> result β) : result β := + match x with + | ret v => f v + | fail v => fail v + +-- Allows using result in do-blocks +instance : Bind result where + bind := bind + +-- Allows using return x in do-blocks +instance : Pure result where + pure := fun x => ret x + +def massert (b:Bool) : result Unit := + if b then return () else fail assertionFailure + +-- Machine integers + +-- NOTE: we reuse the USize type from prelude.lean, because at least we know +-- it's defined in an idiomatic style that is going to make proofs easy (and +-- indeed, several proofs here are much shortened compared to Aymeric's earlier +-- attempt.) This is not stricto sensu the *correct* thing to do, because one +-- can query at run-time the value of USize, which we do *not* want to do (we +-- don't know what target we'll run on!), but when the day comes, we'll just +-- define our own USize. +-- ANOTHER NOTE: there is USize.sub but it has wraparound semantics, which is +-- not something we want to define (I think), so we use our own monadic sub (but +-- is it in line with the Rust behavior?) + +-- TODO: I am somewhat under the impression that subtraction is defined as a +-- total function over nats...? the hypothesis in the if condition is not used +-- in the then-branch which confuses me quite a bit + +-- TODO: add a refinement for the result (just like vec_push_back below) that +-- explains that the toNat of the result (in the case of success) is the sub of +-- the toNat of the arguments (i.e. intrinsic specification) +-- ... do we want intrinsic specifications for the builtins? that might require +-- some careful type annotations in the monadic notation for clients, but may +-- give us more "for free" + +-- Note from Chris Bailey: "If there's more than one salient property of your +-- definition then the subtyping strategy might get messy, and the property part +-- of a subtype is less discoverable by the simplifier or tactics like +-- library_search." Try to settle this with a Lean expert on what is the most +-- productive way to go about this? + +-- Further thoughts: look at what has been done here: +-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean +-- and +-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean +-- which both contain a fair amount of reasoning already! +def USize.checked_sub (n: USize) (m: Nat): result USize := + -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? + if USize.toNat n >= m then + let n' := USize.toNat n + let r := USize.ofNatCore (n' - m) (by + have h: n' - m <= n' := by + apply Nat.sub_le_of_le_add + case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left + apply Nat.lt_of_le_of_lt h + apply n.val.isLt + ) + return r + else + fail integerOverflow + +-- TODO: settle the style for usize_sub before we write these +def USize.checked_mul (n: USize) (m: USize): result USize := sorry +def USize.checked_div (n: USize) (m: USize): result USize := sorry + +#eval USize.checked_sub 10 20 +#eval USize.checked_sub 20 10 +-- NOTE: compare with concrete behavior here, which I do not think we want +#eval USize.sub 0 1 +#eval UInt8.add 255 255 + +-- Vectors + +def vec (α : Type u) := { l : List α // List.length l < USize.size } + +def vec_new : result (vec α) := return ⟨ [], by { + match USize.size, usize_size_eq with + | _, Or.inl rfl => simp + | _, Or.inr rfl => simp + } ⟩ + +def vec_len (v : vec α) : USize := + let ⟨ v, l ⟩ := v + USize.ofNatCore (List.length v) l + +#eval do + return (vec_len (<- @vec_new Nat)) + +def vec_push_fwd (_ : vec α) (_ : α) : Unit := () + +-- TODO: more precise error condition here for the fail case +-- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one +-- make the proof work in that case? Probably need to import tactics from +-- mathlib to deal with inequalities... would love to see an example. +def vec_push_back (v : vec α) (x : α) : { res: result (vec α) // + match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1} + := + if h : List.length v.val + 1 < USize.size then + ⟨ return ⟨List.concat v.val x, + by + rw [List.length_concat] + assumption + ⟩, by simp ⟩ + else + ⟨ fail maximumSizeExceeded, by simp ⟩ + +#eval do + -- NOTE: the // notation is syntactic sugar for Subtype, a refinement with + -- fields val and property. However, Lean's elaborator can automatically + -- select the `val` field if the context provides a type annotation. We + -- annotate `x`, which relieves us of having to write `.val` on the right-hand + -- side of the monadic let. + let x: vec Nat ← vec_push_back (<- vec_new) 1 + -- TODO: strengthen post-condition above and do a demo to show that we can + -- safely eliminate the `fail` case + return (vec_len x) diff --git a/tests/lean/hashmap_on_disk/Hashmap/Types.lean b/tests/lean/hashmap_on_disk/Hashmap/Types.lean new file mode 100644 index 00000000..90022fe5 --- /dev/null +++ b/tests/lean/hashmap_on_disk/Hashmap/Types.lean @@ -0,0 +1,23 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: type definitions +import Hashmap.Primitives + +/- [hashmap_main::hashmap::List] -/ +inductive hashmap_list_t (T : Type) := +| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T +| HashmapListNil : hashmap_list_t T + +/- [hashmap_main::hashmap::HashMap] -/ +structure hashmap_hash_map_t (T : Type) where + 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] -/ +def core_num_u32_max_body : result UInt32 := + return (UInt32.ofNatCore 4294967295 (by simp)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) + +/- The state type used in the state-error monad -/ +axiom state : Type
\ No newline at end of file |