diff options
author | Son Ho | 2023-01-06 19:18:18 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | 8ac12ccdd3e55b8da910c6c8b7bb8dff94a6a640 (patch) | |
tree | 4221fc72f32aa8320593a877148ab81c788679da | |
parent | 586e756761de2730a5147bf19a9f62f455690a08 (diff) |
Regenerate the hashmap code and update the proofs
Diffstat (limited to '')
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 234 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 243 | ||||
-rw-r--r-- | tests/coq/misc/External_Funs.v | 5 | ||||
-rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 4 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 26 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 236 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fst | 40 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 17 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 254 |
10 files changed, 681 insertions, 380 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 1ff3e576..5ec021d1 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -12,22 +12,30 @@ Module Hashmap_Funs. Definition hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) -Fixpoint hash_map_allocate_slots_fwd - (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) : +Fixpoint hash_map_allocate_slots_loop_fwd + (T : Type) (n : nat) (v : vec (List_t T)) (n0 : usize) : result (vec (List_t T)) := match n with | O => Fail_ OutOfFuel | S n1 => - if n0 s= 0%usize - then Return slots - else ( - slots0 <- vec_push_back (List_t T) slots ListNil; - i <- usize_sub n0 1%usize; - hash_map_allocate_slots_fwd T n1 slots0 i) + if n0 s> 0%usize + then ( + slots <- vec_push_back (List_t T) v ListNil; + n2 <- usize_sub n0 1%usize; + hash_map_allocate_slots_loop_fwd T n1 slots n2) + else Return v end . +(** [hashmap::HashMap::{0}::allocate_slots] *) +Definition hash_map_allocate_slots_fwd + (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) : + result (vec (List_t T)) + := + hash_map_allocate_slots_loop_fwd T n slots n0 +. + (** [hashmap::HashMap::{0}::new_with_capacity] *) Definition hash_map_new_with_capacity_fwd (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) @@ -48,27 +56,33 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := . (** [hashmap::HashMap::{0}::clear_slots] *) -Fixpoint hash_map_clear_slots_fwd_back - (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) : +Fixpoint hash_map_clear_slots_loop_fwd_back + (T : Type) (n : nat) (v : vec (List_t T)) (i : usize) : result (vec (List_t T)) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (List_t T) slots in + let i0 := vec_len (List_t T) v in if i s< i0 then ( - slots0 <- vec_index_mut_back (List_t T) slots i ListNil; i1 <- usize_add i 1%usize; - hash_map_clear_slots_fwd_back T n0 slots0 i1) - else Return slots + slots <- vec_index_mut_back (List_t T) v i ListNil; + hash_map_clear_slots_loop_fwd_back T n0 slots i1) + else Return v end . +(** [hashmap::HashMap::{0}::clear_slots] *) +Definition hash_map_clear_slots_fwd_back + (T : Type) (n : nat) (slots : vec (List_t T)) : result (vec (List_t T)) := + hash_map_clear_slots_loop_fwd_back T n slots (0%usize) +. + (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := - v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots) (0%usize); + v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots); Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) . @@ -79,7 +93,7 @@ Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize := . (** [hashmap::HashMap::{0}::insert_in_list] *) -Fixpoint hash_map_insert_in_list_fwd +Fixpoint hash_map_insert_in_list_loop_fwd (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : result bool := @@ -87,17 +101,25 @@ Fixpoint hash_map_insert_in_list_fwd | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey cvalue ls0 => + | ListCons ckey cvalue tl => if ckey s= key then Return false - else hash_map_insert_in_list_fwd T n0 key value ls0 + else hash_map_insert_in_list_loop_fwd T n0 key value tl | ListNil => Return true end end . (** [hashmap::HashMap::{0}::insert_in_list] *) -Fixpoint hash_map_insert_in_list_back +Definition hash_map_insert_in_list_fwd + (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : + result bool + := + hash_map_insert_in_list_loop_fwd T n key value ls +. + +(** [hashmap::HashMap::{0}::insert_in_list] *) +Fixpoint hash_map_insert_in_list_loop_back (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : result (List_t T) := @@ -105,17 +127,25 @@ Fixpoint hash_map_insert_in_list_back | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey cvalue ls0 => + | ListCons ckey cvalue tl => if ckey s= key - then Return (ListCons ckey value ls0) + then Return (ListCons ckey value tl) else ( - ls1 <- hash_map_insert_in_list_back T n0 key value ls0; - Return (ListCons ckey cvalue ls1)) + l <- hash_map_insert_in_list_loop_back T n0 key value tl; + Return (ListCons ckey cvalue l)) | ListNil => let l := ListNil in Return (ListCons key value l) end end . +(** [hashmap::HashMap::{0}::insert_in_list] *) +Definition hash_map_insert_in_list_back + (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : + result (List_t T) + := + hash_map_insert_in_list_loop_back T n key value ls +. + (** [hashmap::HashMap::{0}::insert_no_resize] *) Definition hash_map_insert_no_resize_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) : @@ -145,8 +175,8 @@ Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap::HashMap::{0}::move_elements_from_list] *) -Fixpoint hash_map_move_elements_from_list_fwd_back - (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) : +Fixpoint hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (n : nat) (hm : Hash_map_t T) (ls : List_t T) : result (Hash_map_t T) := match n with @@ -154,36 +184,52 @@ Fixpoint hash_map_move_elements_from_list_fwd_back | S n0 => match ls with | ListCons k v tl => - ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v; - hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl - | ListNil => Return ntable + ntable <- hash_map_insert_no_resize_fwd_back T n0 hm k v; + hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl + | ListNil => Return hm end end . +(** [hashmap::HashMap::{0}::move_elements_from_list] *) +Definition hash_map_move_elements_from_list_fwd_back + (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) : + result (Hash_map_t T) + := + hash_map_move_elements_from_list_loop_fwd_back T n ntable ls +. + (** [hashmap::HashMap::{0}::move_elements] *) -Fixpoint hash_map_move_elements_fwd_back - (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T)) - (i : usize) : +Fixpoint hash_map_move_elements_loop_fwd_back + (T : Type) (n : nat) (hm : Hash_map_t T) (v : vec (List_t T)) (i : usize) : result ((Hash_map_t T) * (vec (List_t T))) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (List_t T) slots in + let i0 := vec_len (List_t T) v in if i s< i0 then ( - l <- vec_index_mut_fwd (List_t T) slots i; + l <- vec_index_mut_fwd (List_t T) v i; let ls := mem_replace_fwd (List_t T) l ListNil in - ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls; - let l0 := mem_replace_back (List_t T) l ListNil in - slots0 <- vec_index_mut_back (List_t T) slots i l0; + ntable <- hash_map_move_elements_from_list_fwd_back T n0 hm ls; i1 <- usize_add i 1%usize; - hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1) - else Return (ntable, slots) + let l0 := mem_replace_back (List_t T) l ListNil in + slots <- vec_index_mut_back (List_t T) v i l0; + hash_map_move_elements_loop_fwd_back T n0 ntable slots i1) + else Return (hm, v) end . +(** [hashmap::HashMap::{0}::move_elements] *) +Definition hash_map_move_elements_fwd_back + (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T)) + (i : usize) : + result ((Hash_map_t T) * (vec (List_t T))) + := + hash_map_move_elements_loop_fwd_back T n ntable slots i +. + (** [hashmap::HashMap::{0}::try_resize] *) Definition hash_map_try_resize_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := @@ -220,21 +266,27 @@ Definition hash_map_insert_fwd_back . (** [hashmap::HashMap::{0}::contains_key_in_list] *) -Fixpoint hash_map_contains_key_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool := +Fixpoint hash_map_contains_key_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : List_t T) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey t ls0 => - if ckey s= key + | ListCons ckey t tl => + if ckey s= i then Return true - else hash_map_contains_key_in_list_fwd T n0 key ls0 + else hash_map_contains_key_in_list_loop_fwd T n0 i tl | ListNil => Return false end end . +(** [hashmap::HashMap::{0}::contains_key_in_list] *) +Definition hash_map_contains_key_in_list_fwd + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool := + hash_map_contains_key_in_list_loop_fwd T n key ls +. + (** [hashmap::HashMap::{0}::contains_key] *) Definition hash_map_contains_key_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool := @@ -246,21 +298,27 @@ Definition hash_map_contains_key_fwd . (** [hashmap::HashMap::{0}::get_in_list] *) -Fixpoint hash_map_get_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := +Fixpoint hash_map_get_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey cvalue ls0 => - if ckey s= key + | ListCons ckey cvalue tl => + if ckey s= i then Return cvalue - else hash_map_get_in_list_fwd T n0 key ls0 + else hash_map_get_in_list_loop_fwd T n0 i tl | ListNil => Fail_ Failure end end . +(** [hashmap::HashMap::{0}::get_in_list] *) +Definition hash_map_get_in_list_fwd + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := + hash_map_get_in_list_loop_fwd T n key ls +. + (** [hashmap::HashMap::{0}::get] *) Definition hash_map_get_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T := @@ -272,41 +330,55 @@ Definition hash_map_get_fwd . (** [hashmap::HashMap::{0}::get_mut_in_list] *) -Fixpoint hash_map_get_mut_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := +Fixpoint hash_map_get_mut_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey cvalue ls0 => - if ckey s= key + | ListCons ckey cvalue tl => + if ckey s= i then Return cvalue - else hash_map_get_mut_in_list_fwd T n0 key ls0 + else hash_map_get_mut_in_list_loop_fwd T n0 i tl | ListNil => Fail_ Failure end end . (** [hashmap::HashMap::{0}::get_mut_in_list] *) -Fixpoint hash_map_get_mut_in_list_back - (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) : +Definition hash_map_get_mut_in_list_fwd + (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T := + hash_map_get_mut_in_list_loop_fwd T n key ls +. + +(** [hashmap::HashMap::{0}::get_mut_in_list] *) +Fixpoint hash_map_get_mut_in_list_loop_back + (T : Type) (n : nat) (i : usize) (ls : List_t T) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | ListCons ckey cvalue ls0 => - if ckey s= key - then Return (ListCons ckey ret ls0) + | ListCons ckey cvalue tl => + if ckey s= i + then Return (ListCons ckey ret tl) else ( - ls1 <- hash_map_get_mut_in_list_back T n0 key ls0 ret; - Return (ListCons ckey cvalue ls1)) + l <- hash_map_get_mut_in_list_loop_back T n0 i tl ret; + Return (ListCons ckey cvalue l)) | ListNil => Fail_ Failure end end . +(** [hashmap::HashMap::{0}::get_mut_in_list] *) +Definition hash_map_get_mut_in_list_back + (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) : + result (List_t T) + := + hash_map_get_mut_in_list_loop_back T n key ls ret +. + (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T := @@ -314,7 +386,7 @@ Definition hash_map_get_mut_fwd let i := vec_len (List_t T) self.(Hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - hash_map_get_mut_in_list_fwd T n key l + hash_map_get_mut_in_list_fwd T n l key . (** [hashmap::HashMap::{0}::get_mut] *) @@ -326,56 +398,68 @@ Definition hash_map_get_mut_back let i := vec_len (List_t T) self.(Hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - l0 <- hash_map_get_mut_in_list_back T n key l ret; + l0 <- hash_map_get_mut_in_list_back T n l key ret; v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; Return (mkHash_map_t self.(Hash_map_num_entries) self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) . (** [hashmap::HashMap::{0}::remove_from_list] *) -Fixpoint hash_map_remove_from_list_fwd - (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) := +Fixpoint hash_map_remove_from_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (option T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey t tl => - if ckey s= key + if ckey s= i then let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in match mv_ls with - | ListCons i cvalue tl0 => Return (Some cvalue) + | ListCons i0 cvalue tl0 => Return (Some cvalue) | ListNil => Fail_ Failure end - else hash_map_remove_from_list_fwd T n0 key tl + else hash_map_remove_from_list_loop_fwd T n0 i tl | ListNil => Return None end end . (** [hashmap::HashMap::{0}::remove_from_list] *) -Fixpoint hash_map_remove_from_list_back - (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) := +Definition hash_map_remove_from_list_fwd + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) := + hash_map_remove_from_list_loop_fwd T n key ls +. + +(** [hashmap::HashMap::{0}::remove_from_list] *) +Fixpoint hash_map_remove_from_list_loop_back + (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey t tl => - if ckey s= key + if ckey s= i then let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in match mv_ls with - | ListCons i cvalue tl0 => Return tl0 + | ListCons i0 cvalue tl0 => Return tl0 | ListNil => Fail_ Failure end else ( - tl0 <- hash_map_remove_from_list_back T n0 key tl; - Return (ListCons ckey t tl0)) + l <- hash_map_remove_from_list_loop_back T n0 i tl; + Return (ListCons ckey t l)) | ListNil => Return ListNil end end . +(** [hashmap::HashMap::{0}::remove_from_list] *) +Definition hash_map_remove_from_list_back + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) := + hash_map_remove_from_list_loop_back T n key ls +. + (** [hashmap::HashMap::{0}::remove] *) Definition hash_map_remove_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : @@ -389,9 +473,7 @@ Definition hash_map_remove_fwd match x with | None => Return None | Some x0 => - i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; - let _ := i0 in - Return (Some x0) + _ <- usize_sub self.(Hash_map_num_entries) 1%usize; Return (Some x0) end . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 3eaaec8a..9ae7942c 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -14,22 +14,30 @@ Module HashmapMain_Funs. Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) -Fixpoint hashmap_hash_map_allocate_slots_fwd - (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) : +Fixpoint hashmap_hash_map_allocate_slots_loop_fwd + (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) : result (vec (Hashmap_list_t T)) := match n with | O => Fail_ OutOfFuel | S n1 => - if n0 s= 0%usize - then Return slots - else ( - slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil; - i <- usize_sub n0 1%usize; - hashmap_hash_map_allocate_slots_fwd T n1 slots0 i) + if n0 s> 0%usize + then ( + slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil; + n2 <- usize_sub n0 1%usize; + hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2) + else Return v end . +(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) +Definition hashmap_hash_map_allocate_slots_fwd + (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) : + result (vec (Hashmap_list_t T)) + := + hashmap_hash_map_allocate_slots_loop_fwd T n slots n0 +. + (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) Definition hashmap_hash_map_new_with_capacity_fwd (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) @@ -51,31 +59,37 @@ Definition hashmap_hash_map_new_fwd . (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) -Fixpoint hashmap_hash_map_clear_slots_fwd_back - (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) : +Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back + (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) : result (vec (Hashmap_list_t T)) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (Hashmap_list_t T) slots in + let i0 := vec_len (Hashmap_list_t T) v in if i s< i0 then ( - slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil; i1 <- usize_add i 1%usize; - hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1) - else Return slots + slots <- vec_index_mut_back (Hashmap_list_t T) v i HashmapListNil; + hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots i1) + else Return v end . +(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) +Definition hashmap_hash_map_clear_slots_fwd_back + (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) : + result (vec (Hashmap_list_t T)) + := + hashmap_hash_map_clear_slots_loop_fwd_back T n slots (0%usize) +. + (** [hashmap_main::hashmap::HashMap::{0}::clear] *) Definition hashmap_hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : result (Hashmap_hash_map_t T) := - v <- - hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots) - (0%usize); + v <- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots); Return (mkHashmap_hash_map_t (0%usize) self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v) . @@ -87,7 +101,7 @@ Definition hashmap_hash_map_len_fwd . (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -Fixpoint hashmap_hash_map_insert_in_list_fwd +Fixpoint hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result bool := @@ -95,17 +109,25 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey cvalue ls0 => + | HashmapListCons ckey cvalue tl => if ckey s= key then Return false - else hashmap_hash_map_insert_in_list_fwd T n0 key value ls0 + else hashmap_hash_map_insert_in_list_loop_fwd T n0 key value tl | HashmapListNil => Return true end end . (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -Fixpoint hashmap_hash_map_insert_in_list_back +Definition hashmap_hash_map_insert_in_list_fwd + (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : + result bool + := + hashmap_hash_map_insert_in_list_loop_fwd T n key value ls +. + +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +Fixpoint hashmap_hash_map_insert_in_list_loop_back (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) := @@ -113,18 +135,26 @@ Fixpoint hashmap_hash_map_insert_in_list_back | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey cvalue ls0 => + | HashmapListCons ckey cvalue tl => if ckey s= key - then Return (HashmapListCons ckey value ls0) + then Return (HashmapListCons ckey value tl) else ( - ls1 <- hashmap_hash_map_insert_in_list_back T n0 key value ls0; - Return (HashmapListCons ckey cvalue ls1)) + l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl; + Return (HashmapListCons ckey cvalue l)) | HashmapListNil => let l := HashmapListNil in Return (HashmapListCons key value l) end end . +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +Definition hashmap_hash_map_insert_in_list_back + (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : + result (Hashmap_list_t T) + := + hashmap_hash_map_insert_in_list_loop_back T n key value ls +. + (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) Definition hashmap_hash_map_insert_no_resize_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) @@ -161,9 +191,8 @@ Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) -Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back - (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) - : +Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) : result (Hashmap_hash_map_t T) := match n with @@ -171,37 +200,54 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back | S n0 => match ls with | HashmapListCons k v tl => - ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v; - hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl - | HashmapListNil => Return ntable + ntable <- hashmap_hash_map_insert_no_resize_fwd_back T n0 hm k v; + hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl + | HashmapListNil => Return hm end end . +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +Definition hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (n : nat) (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 n ntable ls +. + (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) -Fixpoint hashmap_hash_map_move_elements_fwd_back - (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) - (slots : vec (Hashmap_list_t T)) (i : usize) : +Fixpoint hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (v : vec (Hashmap_list_t T)) + (i : usize) : result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T))) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (Hashmap_list_t T) slots in + let i0 := vec_len (Hashmap_list_t T) v in if i s< i0 then ( - l <- vec_index_mut_fwd (Hashmap_list_t T) slots i; + l <- vec_index_mut_fwd (Hashmap_list_t T) v i; let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in - ntable0 <- - hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls; - let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in - slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0; + ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls; i1 <- usize_add i 1%usize; - hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1) - else Return (ntable, slots) + let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in + slots <- vec_index_mut_back (Hashmap_list_t T) v i l0; + hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable slots i1) + else Return (hm, v) end . +(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +Definition hashmap_hash_map_move_elements_fwd_back + (T : Type) (n : nat) (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 n ntable slots i +. + (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) Definition hashmap_hash_map_try_resize_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : @@ -241,21 +287,27 @@ Definition hashmap_hash_map_insert_fwd_back . (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) -Fixpoint hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool := +Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey t ls0 => - if ckey s= key + | HashmapListCons ckey t tl => + if ckey s= i then Return true - else hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0 + else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl | HashmapListNil => Return false end end . +(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) +Definition hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T n key ls +. + (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) Definition hashmap_hash_map_contains_key_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : @@ -269,21 +321,27 @@ Definition hashmap_hash_map_contains_key_fwd . (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) -Fixpoint hashmap_hash_map_get_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := +Fixpoint hashmap_hash_map_get_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey cvalue ls0 => - if ckey s= key + | HashmapListCons ckey cvalue tl => + if ckey s= i then Return cvalue - else hashmap_hash_map_get_in_list_fwd T n0 key ls0 + else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl | HashmapListNil => Fail_ Failure end end . +(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) +Definition hashmap_hash_map_get_in_list_fwd + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := + hashmap_hash_map_get_in_list_loop_fwd T n key ls +. + (** [hashmap_main::hashmap::HashMap::{0}::get] *) Definition hashmap_hash_map_get_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : @@ -297,41 +355,55 @@ Definition hashmap_hash_map_get_fwd . (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) -Fixpoint hashmap_hash_map_get_mut_in_list_fwd - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := +Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey cvalue ls0 => - if ckey s= key + | HashmapListCons ckey cvalue tl => + if ckey s= i then Return cvalue - else hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0 + else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl | HashmapListNil => Fail_ Failure end end . (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) -Fixpoint hashmap_hash_map_get_mut_in_list_back - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) : +Definition hashmap_hash_map_get_mut_in_list_fwd + (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls +. + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +Fixpoint hashmap_hash_map_get_mut_in_list_loop_back + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) (ret : T) : result (Hashmap_list_t T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with - | HashmapListCons ckey cvalue ls0 => - if ckey s= key - then Return (HashmapListCons ckey ret ls0) + | HashmapListCons ckey cvalue tl => + if ckey s= i + then Return (HashmapListCons ckey ret tl) else ( - ls1 <- hashmap_hash_map_get_mut_in_list_back T n0 key ls0 ret; - Return (HashmapListCons ckey cvalue ls1)) + l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret; + Return (HashmapListCons ckey cvalue l)) | HashmapListNil => Fail_ Failure end end . +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +Definition hashmap_hash_map_get_mut_in_list_back + (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) : + result (Hashmap_list_t T) + := + hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret +. + (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) Definition hashmap_hash_map_get_mut_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : @@ -342,7 +414,7 @@ Definition hashmap_hash_map_get_mut_fwd hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - hashmap_hash_map_get_mut_in_list_fwd T n key l + hashmap_hash_map_get_mut_in_list_fwd T n l key . (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) @@ -355,7 +427,7 @@ Definition hashmap_hash_map_get_mut_back hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - l0 <- hashmap_hash_map_get_mut_in_list_back T n key l ret; + l0 <- hashmap_hash_map_get_mut_in_list_back T n l key ret; v <- vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod l0; @@ -364,8 +436,8 @@ Definition hashmap_hash_map_get_mut_back . (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) -Fixpoint hashmap_hash_map_remove_from_list_fwd - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : +Fixpoint hashmap_hash_map_remove_from_list_loop_fwd + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result (option T) := match n with @@ -373,24 +445,32 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd | S n0 => match ls with | HashmapListCons ckey t tl => - if ckey s= key + if ckey s= i 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 => Return (Some cvalue) + | HashmapListCons i0 cvalue tl0 => Return (Some cvalue) | HashmapListNil => Fail_ Failure end - else hashmap_hash_map_remove_from_list_fwd T n0 key tl + else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl | HashmapListNil => Return None end end . (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) -Fixpoint hashmap_hash_map_remove_from_list_back +Definition hashmap_hash_map_remove_from_list_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : + result (option T) + := + hashmap_hash_map_remove_from_list_loop_fwd T n key ls +. + +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +Fixpoint hashmap_hash_map_remove_from_list_loop_back + (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) := match n with @@ -398,23 +478,31 @@ Fixpoint hashmap_hash_map_remove_from_list_back | S n0 => match ls with | HashmapListCons ckey t tl => - if ckey s= key + if ckey s= i 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 => Return tl0 + | HashmapListCons i0 cvalue tl0 => Return tl0 | HashmapListNil => Fail_ Failure end else ( - tl0 <- hashmap_hash_map_remove_from_list_back T n0 key tl; - Return (HashmapListCons ckey t tl0)) + l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl; + Return (HashmapListCons ckey t l)) | HashmapListNil => Return HashmapListNil end end . +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +Definition hashmap_hash_map_remove_from_list_back + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : + result (Hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T n key ls +. + (** [hashmap_main::hashmap::HashMap::{0}::remove] *) Definition hashmap_hash_map_remove_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : @@ -429,8 +517,7 @@ Definition hashmap_hash_map_remove_fwd match x with | None => Return None | Some x0 => - i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; - let _ := i0 in + _ <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; Return (Some x0) end . diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 90390c1b..b5476f25 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -46,10 +46,7 @@ Definition test_new_non_zero_u32_fwd (** [external::test_vec] *) Definition test_vec_fwd : result unit := - let v := vec_new u32 in - v0 <- vec_push_back u32 v (0%u32); - let _ := v0 in - Return tt + let v := vec_new u32 in _ <- vec_push_back u32 v (0%u32); Return tt . (** Unit test for [external::test_vec] *) diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index e91cf81a..10654887 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -67,9 +67,7 @@ Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y. Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x. (** [no_nested_borrows::test2] *) -Definition test2_fwd : result unit := - i <- u32_add 23%u32 44%u32; let _ := i in Return tt -. +Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt. (** Unit test for [no_nested_borrows::test2] *) Check (test2_fwd )%return. diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index c06a6b9e..01fc457e 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -272,7 +272,7 @@ let betree_leaf_split_back0 | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index 3e51c6f1..b8890f86 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -8,14 +8,14 @@ open Hashmap.Types (** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *) unfold -let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t)) +let hash_map_allocate_slots_decreases (t : Type0) (v : vec (list_t t)) (n : usize) : nat = admit () (** [hashmap::HashMap::{0}::clear_slots]: decreases clause *) unfold -let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t)) - (i : usize) : nat = +let hash_map_clear_slots_decreases (t : Type0) (v : vec (list_t t)) (i : usize) + : nat = admit () (** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *) @@ -30,37 +30,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold -let hash_map_move_elements_from_list_decreases (t : Type0) - (ntable : hash_map_t t) (ls : list_t t) : nat = +let hash_map_move_elements_from_list_decreases (t : Type0) (hm : hash_map_t t) + (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::move_elements]: decreases clause *) unfold -let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t) - (slots : vec (list_t t)) (i : usize) : nat = +let hash_map_move_elements_decreases (t : Type0) (hm : hash_map_t t) + (v : vec (list_t t)) (i : usize) : nat = admit () (** [hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *) unfold -let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) +let hash_map_contains_key_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::get_in_list]: decreases clause *) unfold -let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) : +let hash_map_get_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *) unfold -let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) - (ls : list_t t) : nat = +let hash_map_get_mut_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) + : nat = admit () (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *) unfold -let hash_map_remove_from_list_decreases (t : Type0) (key : usize) - (ls : list_t t) : nat = +let hash_map_remove_from_list_decreases (t : Type0) (i : usize) (ls : list_t t) + : nat = admit () diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 59c4e125..d81da40b 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -11,22 +11,27 @@ include Hashmap.Clauses let hash_key_fwd (k : usize) : result usize = Return k (** [hashmap::HashMap::{0}::allocate_slots] *) -let rec hash_map_allocate_slots_fwd - (t : Type0) (slots : vec (list_t t)) (n : usize) : +let rec hash_map_allocate_slots_loop_fwd + (t : Type0) (v : vec (list_t t)) (n : usize) : Tot (result (vec (list_t t))) - (decreases (hash_map_allocate_slots_decreases t slots n)) + (decreases (hash_map_allocate_slots_decreases t v n)) = - if n = 0 - then Return slots - else - begin match vec_push_back (list_t t) slots ListNil with + if n > 0 + then + begin match vec_push_back (list_t t) v ListNil with | Fail e -> Fail e - | Return slots0 -> + | Return slots -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return i -> hash_map_allocate_slots_fwd t slots0 i + | Return n0 -> hash_map_allocate_slots_loop_fwd t slots n0 end end + else Return v + +(** [hashmap::HashMap::{0}::allocate_slots] *) +let hash_map_allocate_slots_fwd + (t : Type0) (slots : vec (list_t t)) (n : usize) : result (vec (list_t t)) = + hash_map_allocate_slots_loop_fwd t slots n (** [hashmap::HashMap::{0}::new_with_capacity] *) let hash_map_new_with_capacity_fwd @@ -54,28 +59,33 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = hash_map_new_with_capacity_fwd t 32 4 5 (** [hashmap::HashMap::{0}::clear_slots] *) -let rec hash_map_clear_slots_fwd_back - (t : Type0) (slots : vec (list_t t)) (i : usize) : +let rec hash_map_clear_slots_loop_fwd_back + (t : Type0) (v : vec (list_t t)) (i : usize) : Tot (result (vec (list_t t))) - (decreases (hash_map_clear_slots_decreases t slots i)) + (decreases (hash_map_clear_slots_decreases t v i)) = - let i0 = vec_len (list_t t) slots in + let i0 = vec_len (list_t t) v in if i < i0 then - begin match vec_index_mut_back (list_t t) slots i ListNil with + begin match usize_add i 1 with | Fail e -> Fail e - | Return slots0 -> - begin match usize_add i 1 with + | Return i1 -> + begin match vec_index_mut_back (list_t t) v i ListNil with | Fail e -> Fail e - | Return i1 -> hash_map_clear_slots_fwd_back t slots0 i1 + | Return slots -> hash_map_clear_slots_loop_fwd_back t slots i1 end end - else Return slots + else Return v + +(** [hashmap::HashMap::{0}::clear_slots] *) +let hash_map_clear_slots_fwd_back + (t : Type0) (slots : vec (list_t t)) : result (vec (list_t t)) = + hash_map_clear_slots_loop_fwd_back t slots 0 (** [hashmap::HashMap::{0}::clear] *) let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = - begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with + begin match hash_map_clear_slots_fwd_back t self.hash_map_slots with | Fail e -> Fail e | Return v -> Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load @@ -87,37 +97,47 @@ let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize = Return self.hash_map_num_entries (** [hashmap::HashMap::{0}::insert_in_list] *) -let rec hash_map_insert_in_list_fwd +let rec hash_map_insert_in_list_loop_fwd (t : Type0) (key : usize) (value : t) (ls : list_t t) : Tot (result bool) (decreases (hash_map_insert_in_list_decreases t key value ls)) = begin match ls with - | ListCons ckey cvalue ls0 -> + | ListCons ckey cvalue tl -> if ckey = key then Return false - else hash_map_insert_in_list_fwd t key value ls0 + else hash_map_insert_in_list_loop_fwd t key value tl | ListNil -> Return true end (** [hashmap::HashMap::{0}::insert_in_list] *) -let rec hash_map_insert_in_list_back +let hash_map_insert_in_list_fwd + (t : Type0) (key : usize) (value : t) (ls : list_t t) : result bool = + hash_map_insert_in_list_loop_fwd t key value ls + +(** [hashmap::HashMap::{0}::insert_in_list] *) +let rec hash_map_insert_in_list_loop_back (t : Type0) (key : usize) (value : t) (ls : list_t t) : Tot (result (list_t t)) (decreases (hash_map_insert_in_list_decreases t key value ls)) = begin match ls with - | ListCons ckey cvalue ls0 -> + | ListCons ckey cvalue tl -> if ckey = key - then Return (ListCons ckey value ls0) + then Return (ListCons ckey value tl) else - begin match hash_map_insert_in_list_back t key value ls0 with + begin match hash_map_insert_in_list_loop_back t key value tl with | Fail e -> Fail e - | Return ls1 -> Return (ListCons ckey cvalue ls1) + | Return l -> Return (ListCons ckey cvalue l) end | ListNil -> let l = ListNil in Return (ListCons key value l) end +(** [hashmap::HashMap::{0}::insert_in_list] *) +let hash_map_insert_in_list_back + (t : Type0) (key : usize) (value : t) (ls : list_t t) : result (list_t t) = + hash_map_insert_in_list_loop_back t key value ls + (** [hashmap::HashMap::{0}::insert_no_resize] *) let hash_map_insert_no_resize_fwd_back (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : @@ -178,48 +198,62 @@ 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::HashMap::{0}::move_elements_from_list] *) -let rec hash_map_move_elements_from_list_fwd_back - (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : +let rec hash_map_move_elements_from_list_loop_fwd_back + (t : Type0) (hm : hash_map_t t) (ls : list_t t) : Tot (result (hash_map_t t)) - (decreases (hash_map_move_elements_from_list_decreases t ntable ls)) + (decreases (hash_map_move_elements_from_list_decreases t hm ls)) = begin match ls with | ListCons k v tl -> - begin match hash_map_insert_no_resize_fwd_back t ntable k v with + begin match hash_map_insert_no_resize_fwd_back t hm k v with | Fail e -> Fail e - | Return ntable0 -> hash_map_move_elements_from_list_fwd_back t ntable0 tl + | Return ntable -> + hash_map_move_elements_from_list_loop_fwd_back t ntable tl end - | ListNil -> Return ntable + | ListNil -> Return hm end +(** [hashmap::HashMap::{0}::move_elements_from_list] *) +let hash_map_move_elements_from_list_fwd_back + (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : result (hash_map_t t) = + hash_map_move_elements_from_list_loop_fwd_back t ntable ls + (** [hashmap::HashMap::{0}::move_elements] *) -let rec hash_map_move_elements_fwd_back - (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : +let rec hash_map_move_elements_loop_fwd_back + (t : Type0) (hm : hash_map_t t) (v : vec (list_t t)) (i : usize) : Tot (result ((hash_map_t t) & (vec (list_t t)))) - (decreases (hash_map_move_elements_decreases t ntable slots i)) + (decreases (hash_map_move_elements_decreases t hm v i)) = - let i0 = vec_len (list_t t) slots in + let i0 = vec_len (list_t t) v in if i < i0 then - begin match vec_index_mut_fwd (list_t t) slots i with + begin match vec_index_mut_fwd (list_t t) v i with | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (list_t t) l ListNil in - begin match hash_map_move_elements_from_list_fwd_back t ntable ls with + begin match hash_map_move_elements_from_list_fwd_back t hm ls with | Fail e -> Fail e - | Return ntable0 -> - let l0 = mem_replace_back (list_t t) l ListNil in - begin match vec_index_mut_back (list_t t) slots i l0 with + | Return ntable -> + begin match usize_add i 1 with | Fail e -> Fail e - | Return slots0 -> - begin match usize_add i 1 with + | Return i1 -> + let l0 = mem_replace_back (list_t t) l ListNil in + begin match vec_index_mut_back (list_t t) v i l0 with | Fail e -> Fail e - | Return i1 -> hash_map_move_elements_fwd_back t ntable0 slots0 i1 + | Return slots -> + hash_map_move_elements_loop_fwd_back t ntable slots i1 end end end end - else Return (ntable, slots) + else Return (hm, v) + +(** [hashmap::HashMap::{0}::move_elements] *) +let hash_map_move_elements_fwd_back + (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : + result ((hash_map_t t) & (vec (list_t t))) + = + hash_map_move_elements_loop_fwd_back t ntable slots i (** [hashmap::HashMap::{0}::try_resize] *) let hash_map_try_resize_fwd_back @@ -278,19 +312,24 @@ let hash_map_insert_fwd_back end (** [hashmap::HashMap::{0}::contains_key_in_list] *) -let rec hash_map_contains_key_in_list_fwd - (t : Type0) (key : usize) (ls : list_t t) : +let rec hash_map_contains_key_in_list_loop_fwd + (t : Type0) (i : usize) (ls : list_t t) : Tot (result bool) - (decreases (hash_map_contains_key_in_list_decreases t key ls)) + (decreases (hash_map_contains_key_in_list_decreases t i ls)) = begin match ls with - | ListCons ckey x ls0 -> - if ckey = key + | ListCons ckey x tl -> + if ckey = i then Return true - else hash_map_contains_key_in_list_fwd t key ls0 + else hash_map_contains_key_in_list_loop_fwd t i tl | ListNil -> Return false end +(** [hashmap::HashMap::{0}::contains_key_in_list] *) +let hash_map_contains_key_in_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : result bool = + hash_map_contains_key_in_list_loop_fwd t key ls + (** [hashmap::HashMap::{0}::contains_key] *) let hash_map_contains_key_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result bool = @@ -309,16 +348,21 @@ let hash_map_contains_key_fwd end (** [hashmap::HashMap::{0}::get_in_list] *) -let rec hash_map_get_in_list_fwd - (t : Type0) (key : usize) (ls : list_t t) : - Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls)) +let rec hash_map_get_in_list_loop_fwd + (t : Type0) (i : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_in_list_decreases t i ls)) = begin match ls with - | ListCons ckey cvalue ls0 -> - if ckey = key then Return cvalue else hash_map_get_in_list_fwd t key ls0 + | ListCons ckey cvalue tl -> + if ckey = i then Return cvalue else hash_map_get_in_list_loop_fwd t i tl | ListNil -> Fail Failure end +(** [hashmap::HashMap::{0}::get_in_list] *) +let hash_map_get_in_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : result t = + hash_map_get_in_list_loop_fwd t key ls + (** [hashmap::HashMap::{0}::get] *) let hash_map_get_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = @@ -337,36 +381,46 @@ let hash_map_get_fwd end (** [hashmap::HashMap::{0}::get_mut_in_list] *) -let rec hash_map_get_mut_in_list_fwd - (t : Type0) (key : usize) (ls : list_t t) : - Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls)) +let rec hash_map_get_mut_in_list_loop_fwd + (t : Type0) (i : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t i ls)) = begin match ls with - | ListCons ckey cvalue ls0 -> - if ckey = key + | ListCons ckey cvalue tl -> + if ckey = i then Return cvalue - else hash_map_get_mut_in_list_fwd t key ls0 + else hash_map_get_mut_in_list_loop_fwd t i tl | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get_mut_in_list] *) -let rec hash_map_get_mut_in_list_back - (t : Type0) (key : usize) (ls : list_t t) (ret : t) : +let hash_map_get_mut_in_list_fwd + (t : Type0) (ls : list_t t) (key : usize) : result t = + hash_map_get_mut_in_list_loop_fwd t key ls + +(** [hashmap::HashMap::{0}::get_mut_in_list] *) +let rec hash_map_get_mut_in_list_loop_back + (t : Type0) (i : usize) (ls : list_t t) (ret : t) : Tot (result (list_t t)) - (decreases (hash_map_get_mut_in_list_decreases t key ls)) + (decreases (hash_map_get_mut_in_list_decreases t i ls)) = begin match ls with - | ListCons ckey cvalue ls0 -> - if ckey = key - then Return (ListCons ckey ret ls0) + | ListCons ckey cvalue tl -> + if ckey = i + then Return (ListCons ckey ret tl) else - begin match hash_map_get_mut_in_list_back t key ls0 ret with + begin match hash_map_get_mut_in_list_loop_back t i tl ret with | Fail e -> Fail e - | Return ls1 -> Return (ListCons ckey cvalue ls1) + | Return l -> Return (ListCons ckey cvalue l) end | ListNil -> Fail Failure end +(** [hashmap::HashMap::{0}::get_mut_in_list] *) +let hash_map_get_mut_in_list_back + (t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) = + hash_map_get_mut_in_list_loop_back t key ls ret + (** [hashmap::HashMap::{0}::get_mut] *) let hash_map_get_mut_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = @@ -380,7 +434,7 @@ let hash_map_get_mut_fwd begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> hash_map_get_mut_in_list_fwd t key l + | Return l -> hash_map_get_mut_in_list_fwd t l key end end end @@ -401,7 +455,7 @@ let hash_map_get_mut_back with | Fail e -> Fail e | Return l -> - begin match hash_map_get_mut_in_list_back t key l ret with + begin match hash_map_get_mut_in_list_back t l key ret with | Fail e -> Fail e | Return l0 -> begin match @@ -417,47 +471,57 @@ let hash_map_get_mut_back end (** [hashmap::HashMap::{0}::remove_from_list] *) -let rec hash_map_remove_from_list_fwd - (t : Type0) (key : usize) (ls : list_t t) : +let rec hash_map_remove_from_list_loop_fwd + (t : Type0) (i : usize) (ls : list_t t) : Tot (result (option t)) - (decreases (hash_map_remove_from_list_decreases t key ls)) + (decreases (hash_map_remove_from_list_decreases t i ls)) = begin match ls with | ListCons ckey x tl -> - if ckey = key + if ckey = i then let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with - | ListCons i cvalue tl0 -> Return (Some cvalue) + | ListCons i0 cvalue tl0 -> Return (Some cvalue) | ListNil -> Fail Failure end - else hash_map_remove_from_list_fwd t key tl + else hash_map_remove_from_list_loop_fwd t i tl | ListNil -> Return None end (** [hashmap::HashMap::{0}::remove_from_list] *) -let rec hash_map_remove_from_list_back - (t : Type0) (key : usize) (ls : list_t t) : +let hash_map_remove_from_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : result (option t) = + hash_map_remove_from_list_loop_fwd t key ls + +(** [hashmap::HashMap::{0}::remove_from_list] *) +let rec hash_map_remove_from_list_loop_back + (t : Type0) (i : usize) (ls : list_t t) : Tot (result (list_t t)) - (decreases (hash_map_remove_from_list_decreases t key ls)) + (decreases (hash_map_remove_from_list_decreases t i ls)) = begin match ls with | ListCons ckey x tl -> - if ckey = key + if ckey = i then let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with - | ListCons i cvalue tl0 -> Return tl0 + | ListCons i0 cvalue tl0 -> Return tl0 | ListNil -> Fail Failure end else - begin match hash_map_remove_from_list_back t key tl with + begin match hash_map_remove_from_list_loop_back t i tl with | Fail e -> Fail e - | Return tl0 -> Return (ListCons ckey x tl0) + | Return l -> Return (ListCons ckey x l) end | ListNil -> Return ListNil end +(** [hashmap::HashMap::{0}::remove_from_list] *) +let hash_map_remove_from_list_back + (t : Type0) (key : usize) (ls : list_t t) : result (list_t t) = + hash_map_remove_from_list_loop_back t key ls + (** [hashmap::HashMap::{0}::remove] *) let hash_map_remove_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) = diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst index 9d1a6469..724ca741 100644 --- a/tests/fstar/hashmap/Hashmap.Properties.fst +++ b/tests/fstar/hashmap/Hashmap.Properties.fst @@ -620,11 +620,11 @@ let hash_map_new_fwd_lem t = hash_map_new_fwd_lem_aux t (*** clear_slots *) /// [clear_slots] doesn't fail and simply clears the slots starting at index i #push-options "--fuel 1" -let rec hash_map_clear_slots_fwd_back_lem +let rec hash_map_clear_slots_loop_fwd_back_lem (t : Type0) (slots : vec (list_t t)) (i : usize) : Lemma (ensures ( - match hash_map_clear_slots_fwd_back t slots i with + match hash_map_clear_slots_loop_fwd_back t slots i with | Fail _ -> False | Return slots' -> // The length is preserved @@ -645,8 +645,8 @@ let rec hash_map_clear_slots_fwd_back_lem begin match usize_add i 1 with | Fail _ -> () | Return i1 -> - hash_map_clear_slots_fwd_back_lem t v i1; - begin match hash_map_clear_slots_fwd_back t v i1 with + hash_map_clear_slots_loop_fwd_back_lem t v i1; + begin match hash_map_clear_slots_loop_fwd_back t v i1 with | Fail _ -> () | Return slots1 -> assert(length slots1 == length slots); @@ -683,8 +683,8 @@ let hash_map_clear_fwd_back_lem_aux #t self = let p = self.hash_map_max_load_factor in let i = self.hash_map_max_load in let v = self.hash_map_slots in - hash_map_clear_slots_fwd_back_lem t v 0; - begin match hash_map_clear_slots_fwd_back t v 0 with + hash_map_clear_slots_loop_fwd_back_lem t v 0; + begin match hash_map_clear_slots_loop_fwd_back t v 0 with | Fail _ -> () | Return slots1 -> slots_t_al_v_all_nil_is_empty_lem slots1; @@ -2703,17 +2703,17 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key (**** get_mut_in_list'fwd *) -val hash_map_get_mut_in_list_fwd_lem +val hash_map_get_mut_in_list_loop_fwd_lem (#t : Type0) (key : usize) (ls : list_t t) : Lemma (ensures ( - match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with + match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) #push-options "--fuel 1" -let rec hash_map_get_mut_in_list_fwd_lem #t key ls = +let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls = begin match ls with | ListCons ckey cvalue ls0 -> let b = ckey = key in @@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls = then () else begin - hash_map_get_mut_in_list_fwd_lem key ls0; - match hash_map_get_mut_in_list_fwd t key ls0 with + hash_map_get_mut_in_list_loop_fwd_lem key ls0; + match hash_map_get_mut_in_list_loop_fwd t key ls0 with | Fail _ -> () | Return x -> () end @@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key = | Fail _ -> () | Return l -> begin - hash_map_get_mut_in_list_fwd_lem key l; - match hash_map_get_mut_in_list_fwd t key l with + hash_map_get_mut_in_list_loop_fwd_lem key l; + match hash_map_get_mut_in_list_loop_fwd t key l with | Fail _ -> () | Return x -> () end @@ -2770,18 +2770,18 @@ let hash_map_get_mut_fwd_lem #t self key = (**** get_mut_in_list'back *) -val hash_map_get_mut_in_list_back_lem +val hash_map_get_mut_in_list_loop_back_lem (#t : Type0) (key : usize) (ls : list_t t) (ret : t) : Lemma (requires (Some? (slot_t_find_s key ls))) (ensures ( - match hash_map_get_mut_in_list_back t key ls ret with + match hash_map_get_mut_in_list_loop_back t key ls ret with | Fail _ -> False | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret) | _ -> False)) #push-options "--fuel 1" -let rec hash_map_get_mut_in_list_back_lem #t key ls ret = +let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret = begin match ls with | ListCons ckey cvalue ls0 -> let b = ckey = key in @@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret = then let ls1 = ListCons ckey ret ls0 in () else begin - hash_map_get_mut_in_list_back_lem key ls0 ret; - match hash_map_get_mut_in_list_back t key ls0 ret with + hash_map_get_mut_in_list_loop_back_lem key ls0 ret; + match hash_map_get_mut_in_list_loop_back t key ls0 ret with | Fail _ -> () | Return l -> let ls1 = ListCons ckey cvalue l in () end @@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret = | Fail _ -> () | Return l -> begin - hash_map_get_mut_in_list_back_lem key l ret; - match hash_map_get_mut_in_list_back t key l ret with + hash_map_get_mut_in_list_loop_back_lem key l ret; + match hash_map_get_mut_in_list_loop_back t key l ret with | Fail _ -> () | Return l0 -> begin match vec_index_mut_back (list_t t) v hash_mod l0 with diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst index 55685114..b3081cd6 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -9,13 +9,13 @@ open HashmapMain.Types (** [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 = + (v : 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 = + (v : vec (hashmap_list_t t)) (i : usize) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *) @@ -31,37 +31,36 @@ 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 = + (hm : 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 = + (hm : hashmap_hash_map_t t) (v : 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) +let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (i : 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) +let hashmap_hash_map_get_in_list_decreases (t : Type0) (i : 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) +let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (i : 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) +let hashmap_hash_map_remove_from_list_decreases (t : Type0) (i : usize) (ls : hashmap_list_t t) : nat = admit () diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index c4f2b039..3da56f41 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -12,22 +12,29 @@ include HashmapMain.Clauses 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) : +let rec hashmap_hash_map_allocate_slots_loop_fwd + (t : Type0) (v : vec (hashmap_list_t t)) (n : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) + (decreases (hashmap_hash_map_allocate_slots_decreases t v n)) = - if n = 0 - then Return slots - else - begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with + if n > 0 + then + begin match vec_push_back (hashmap_list_t t) v HashmapListNil with | Fail e -> Fail e - | Return slots0 -> + | Return slots -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return i -> hashmap_hash_map_allocate_slots_fwd t slots0 i + | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots n0 end end + else Return v + +(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) +let hashmap_hash_map_allocate_slots_fwd + (t : Type0) (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] *) let hashmap_hash_map_new_with_capacity_fwd @@ -56,30 +63,36 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = hashmap_hash_map_new_with_capacity_fwd t 32 4 5 (** [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) : +let rec hashmap_hash_map_clear_slots_loop_fwd_back + (t : Type0) (v : vec (hashmap_list_t t)) (i : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_clear_slots_decreases t slots i)) + (decreases (hashmap_hash_map_clear_slots_decreases t v i)) = - let i0 = vec_len (hashmap_list_t t) slots in + let i0 = vec_len (hashmap_list_t t) v in if i < i0 then - begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil - with + begin match usize_add i 1 with | Fail e -> Fail e - | Return slots0 -> - begin match usize_add i 1 with + | Return i1 -> + begin match vec_index_mut_back (hashmap_list_t t) v i HashmapListNil with | Fail e -> Fail e - | Return i1 -> hashmap_hash_map_clear_slots_fwd_back t slots0 i1 + | Return slots -> hashmap_hash_map_clear_slots_loop_fwd_back t slots i1 end end - else Return slots + else Return v + +(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) +let hashmap_hash_map_clear_slots_fwd_back + (t : Type0) (slots : vec (hashmap_list_t t)) : + result (vec (hashmap_list_t t)) + = + hashmap_hash_map_clear_slots_loop_fwd_back t slots 0 (** [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 + hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots with | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor @@ -92,38 +105,50 @@ let hashmap_hash_map_len_fwd Return self.hashmap_hash_map_num_entries (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -let rec hashmap_hash_map_insert_in_list_fwd +let rec hashmap_hash_map_insert_in_list_loop_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 -> + | HashmapListCons ckey cvalue tl -> if ckey = key then Return false - else hashmap_hash_map_insert_in_list_fwd t key value ls0 + else hashmap_hash_map_insert_in_list_loop_fwd t key value tl | HashmapListNil -> Return true end (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) -let rec hashmap_hash_map_insert_in_list_back +let hashmap_hash_map_insert_in_list_fwd + (t : Type0) (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] *) +let rec hashmap_hash_map_insert_in_list_loop_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 -> + | HashmapListCons ckey cvalue tl -> if ckey = key - then Return (HashmapListCons ckey value ls0) + then Return (HashmapListCons ckey value tl) else - begin match hashmap_hash_map_insert_in_list_back t key value ls0 with + begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with | Fail e -> Fail e - | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) + | Return l -> Return (HashmapListCons ckey cvalue l) end | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) end +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +let hashmap_hash_map_insert_in_list_back + (t : Type0) (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] *) let hashmap_hash_map_insert_no_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : @@ -188,52 +213,67 @@ 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) : +let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back + (t : Type0) (hm : 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)) + (decreases (hashmap_hash_map_move_elements_from_list_decreases t hm ls)) = begin match ls with | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with + begin match hashmap_hash_map_insert_no_resize_fwd_back t hm k v with | Fail e -> Fail e - | Return ntable0 -> - hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl + | Return ntable -> + hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable tl end - | HashmapListNil -> Return ntable + | HashmapListNil -> Return hm end +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +let hashmap_hash_map_move_elements_from_list_fwd_back + (t : Type0) (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] *) -let rec hashmap_hash_map_move_elements_fwd_back - (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) +let rec hashmap_hash_map_move_elements_loop_fwd_back + (t : Type0) (hm : hashmap_hash_map_t t) (v : 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)) + (decreases (hashmap_hash_map_move_elements_decreases t hm v i)) = - let i0 = vec_len (hashmap_list_t t) slots in + let i0 = vec_len (hashmap_list_t t) v in if i < i0 then - begin match vec_index_mut_fwd (hashmap_list_t t) slots i with + begin match vec_index_mut_fwd (hashmap_list_t t) v i with | Fail e -> Fail e | 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 + begin match hashmap_hash_map_move_elements_from_list_fwd_back t hm ls with | Fail e -> Fail e - | 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 + | Return ntable -> + begin match usize_add i 1 with | Fail e -> Fail e - | Return slots0 -> - begin match usize_add i 1 with + | Return i1 -> + let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + begin match vec_index_mut_back (hashmap_list_t t) v i l0 with | Fail e -> Fail e - | Return i1 -> - hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 + | Return slots -> + hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i1 end end end end - else Return (ntable, slots) + else Return (hm, v) + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +let hashmap_hash_map_move_elements_fwd_back + (t : Type0) (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] *) let hashmap_hash_map_try_resize_fwd_back @@ -293,19 +333,24 @@ let hashmap_hash_map_insert_fwd_back 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) : +let rec hashmap_hash_map_contains_key_in_list_loop_fwd + (t : Type0) (i : usize) (ls : hashmap_list_t t) : Tot (result bool) - (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls)) + (decreases (hashmap_hash_map_contains_key_in_list_decreases t i ls)) = begin match ls with - | HashmapListCons ckey x ls0 -> - if ckey = key + | HashmapListCons ckey x tl -> + if ckey = i then Return true - else hashmap_hash_map_contains_key_in_list_fwd t key ls0 + else hashmap_hash_map_contains_key_in_list_loop_fwd t i tl | HashmapListNil -> Return false end +(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) +let hashmap_hash_map_contains_key_in_list_fwd + (t : Type0) (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] *) let hashmap_hash_map_contains_key_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = @@ -326,18 +371,23 @@ let hashmap_hash_map_contains_key_fwd 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)) +let rec hashmap_hash_map_get_in_list_loop_fwd + (t : Type0) (i : usize) (ls : hashmap_list_t t) : + Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t i ls)) = begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key + | HashmapListCons ckey cvalue tl -> + if ckey = i then Return cvalue - else hashmap_hash_map_get_in_list_fwd t key ls0 + else hashmap_hash_map_get_in_list_loop_fwd t i tl | HashmapListNil -> Fail Failure end +(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) +let hashmap_hash_map_get_in_list_fwd + (t : Type0) (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] *) let hashmap_hash_map_get_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = @@ -358,37 +408,49 @@ let hashmap_hash_map_get_fwd 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) : +let rec hashmap_hash_map_get_mut_in_list_loop_fwd + (t : Type0) (i : usize) (ls : hashmap_list_t t) : Tot (result t) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls)) = begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key + | HashmapListCons ckey cvalue tl -> + if ckey = i then Return cvalue - else hashmap_hash_map_get_mut_in_list_fwd t key ls0 + else hashmap_hash_map_get_mut_in_list_loop_fwd t i tl | HashmapListNil -> Fail Failure 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) : +let hashmap_hash_map_get_mut_in_list_fwd + (t : Type0) (ls : hashmap_list_t t) (key : usize) : result t = + hashmap_hash_map_get_mut_in_list_loop_fwd t key ls + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +let rec hashmap_hash_map_get_mut_in_list_loop_back + (t : Type0) (i : 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)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls)) = begin match ls with - | HashmapListCons ckey cvalue ls0 -> - if ckey = key - then Return (HashmapListCons ckey ret ls0) + | HashmapListCons ckey cvalue tl -> + if ckey = i + then Return (HashmapListCons ckey ret tl) else - begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with + begin match hashmap_hash_map_get_mut_in_list_loop_back t i tl ret with | Fail e -> Fail e - | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) + | Return l -> Return (HashmapListCons ckey cvalue l) end | HashmapListNil -> Fail Failure end +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +let hashmap_hash_map_get_mut_in_list_back + (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) : + result (hashmap_list_t t) + = + hashmap_hash_map_get_mut_in_list_loop_back t key ls ret + (** [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 = @@ -403,7 +465,7 @@ let hashmap_hash_map_get_mut_fwd vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> hashmap_hash_map_get_mut_in_list_fwd t key l + | Return l -> hashmap_hash_map_get_mut_in_list_fwd t l key end end end @@ -425,7 +487,7 @@ let hashmap_hash_map_get_mut_back hash_mod with | Fail e -> Fail e | Return l -> - begin match hashmap_hash_map_get_mut_in_list_back t key l ret with + begin match hashmap_hash_map_get_mut_in_list_back t l key ret with | Fail e -> Fail e | Return l0 -> begin match @@ -443,51 +505,63 @@ let hashmap_hash_map_get_mut_back 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) : +let rec hashmap_hash_map_remove_from_list_loop_fwd + (t : Type0) (i : usize) (ls : hashmap_list_t t) : Tot (result (option t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) + (decreases (hashmap_hash_map_remove_from_list_decreases t i ls)) = begin match ls with | HashmapListCons ckey x tl -> - if ckey = key + if ckey = i 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) + | HashmapListCons i0 cvalue tl0 -> Return (Some cvalue) | HashmapListNil -> Fail Failure end - else hashmap_hash_map_remove_from_list_fwd t key tl + else hashmap_hash_map_remove_from_list_loop_fwd t i tl | 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) : +let hashmap_hash_map_remove_from_list_fwd + (t : Type0) (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] *) +let rec hashmap_hash_map_remove_from_list_loop_back + (t : Type0) (i : usize) (ls : hashmap_list_t t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) + (decreases (hashmap_hash_map_remove_from_list_decreases t i ls)) = begin match ls with | HashmapListCons ckey x tl -> - if ckey = key + if ckey = i 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 + | HashmapListCons i0 cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end else - begin match hashmap_hash_map_remove_from_list_back t key tl with + begin match hashmap_hash_map_remove_from_list_loop_back t i tl with | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey x tl0) + | Return l -> Return (HashmapListCons ckey x l) end | HashmapListNil -> Return HashmapListNil end +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +let hashmap_hash_map_remove_from_list_back + (t : Type0) (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] *) let hashmap_hash_map_remove_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = |