From c52add165764d3a0b68ee5181901109078e9b19b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Jan 2023 16:44:25 +0100 Subject: Update the hashmap and regenerate --- tests/coq/hashmap/Hashmap_Funs.v | 14 ++++---------- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 18 ++++++------------ tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 4 ++-- tests/fstar/hashmap/Hashmap.Clauses.fst | 4 ++-- tests/fstar/hashmap/Hashmap.Funs.fst | 15 +++++---------- tests/fstar/hashmap/Hashmap.Properties.fst | 19 +++++++++---------- .../hashmap_on_disk/HashmapMain.Clauses.Template.fst | 4 ++-- tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst | 4 ++-- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 17 +++++------------ 9 files changed, 37 insertions(+), 62 deletions(-) diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0d55b171..f1af0c21 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -55,8 +55,8 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) . -(** [hashmap::HashMap::{0}::clear_slots] *) -Fixpoint hash_map_clear_slots_loop_fwd_back +(** [hashmap::HashMap::{0}::clear] *) +Fixpoint hash_map_clear_loop_fwd_back (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) : result (vec (List_t T)) := @@ -68,21 +68,15 @@ Fixpoint hash_map_clear_slots_loop_fwd_back then ( i1 <- usize_add i 1%usize; slots0 <- vec_index_mut_back (List_t T) slots i ListNil; - hash_map_clear_slots_loop_fwd_back T n0 slots0 i1) + hash_map_clear_loop_fwd_back T n0 slots0 i1) else Return slots 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); + v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize); Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 670e527a..7c86dbe1 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -58,8 +58,8 @@ Definition hashmap_hash_map_new_fwd hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) . -(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) -Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back +(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +Fixpoint hashmap_hash_map_clear_loop_fwd_back (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) : result (vec (Hashmap_list_t T)) := @@ -71,25 +71,19 @@ Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back then ( i1 <- usize_add i 1%usize; slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil; - hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1) + hashmap_hash_map_clear_loop_fwd_back T n0 slots0 i1) else Return slots 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); + v <- + hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots) + (0%usize); Return (mkHashmap_hash_map_t (0%usize) self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v) . diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index 4e490b6c..aef5e25e 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -12,9 +12,9 @@ let hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (list_t t)) (n : usize) : nat = admit () -(** [hashmap::HashMap::{0}::clear_slots]: decreases clause *) +(** [hashmap::HashMap::{0}::clear]: decreases clause *) unfold -let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t)) +let hash_map_clear_loop_decreases (t : Type0) (slots : vec (list_t t)) (i : usize) : nat = admit () diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst index b525880a..d8bb8d20 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.fst @@ -11,9 +11,9 @@ unfold let hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (list_t t)) (n : usize) : nat = n -(** [hashmap::HashMap::clear_slots]: decreases clause *) +(** [hashmap::HashMap::clear]: decreases clause *) unfold -let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t)) +let hash_map_clear_loop_decreases (t : Type0) (slots : vec (list_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 7137e92a..68bda221 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -58,11 +58,11 @@ let hash_map_new_with_capacity_fwd 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_loop_fwd_back +(** [hashmap::HashMap::{0}::clear] *) +let rec hash_map_clear_loop_fwd_back (t : Type0) (slots : vec (list_t t)) (i : usize) : Tot (result (vec (list_t t))) - (decreases (hash_map_clear_slots_loop_decreases t slots i)) + (decreases (hash_map_clear_loop_decreases t slots i)) = let i0 = vec_len (list_t t) slots in if i < i0 @@ -72,20 +72,15 @@ let rec hash_map_clear_slots_loop_fwd_back | Return i1 -> begin match vec_index_mut_back (list_t t) slots i ListNil with | Fail e -> Fail e - | Return slots0 -> hash_map_clear_slots_loop_fwd_back t slots0 i1 + | Return slots0 -> hash_map_clear_loop_fwd_back t slots0 i1 end end else Return slots -(** [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 with + begin match hash_map_clear_loop_fwd_back t self.hash_map_slots 0 with | Fail e -> Fail e | Return v -> Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst index b1352443..49d96cd5 100644 --- a/tests/fstar/hashmap/Hashmap.Properties.fst +++ b/tests/fstar/hashmap/Hashmap.Properties.fst @@ -617,14 +617,14 @@ let hash_map_new_fwd_lem_aux t = /// The lemma we reveal in the .fsti 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 +(*** clear *) +/// [clear]: the loop doesn't fail and simply clears the slots starting at index i #push-options "--fuel 1" -let rec hash_map_clear_slots_loop_fwd_back_lem +let rec hash_map_clear_loop_fwd_back_lem (t : Type0) (slots : vec (list_t t)) (i : usize) : Lemma (ensures ( - match hash_map_clear_slots_loop_fwd_back t slots i with + match hash_map_clear_loop_fwd_back t slots i with | Fail _ -> False | Return slots' -> // The length is preserved @@ -633,7 +633,7 @@ let rec hash_map_clear_slots_loop_fwd_back_lem (forall (j:nat{j < i /\ j < length slots}). index slots' j == index slots j) /\ // The slots after i are set to ListNil (forall (j:nat{i <= j /\ j < length slots}). index slots' j == ListNil))) - (decreases (hash_map_clear_slots_loop_decreases t slots i)) + (decreases (hash_map_clear_loop_decreases t slots i)) = let i0 = vec_len (list_t t) slots in let b = i < i0 in @@ -645,8 +645,8 @@ let rec hash_map_clear_slots_loop_fwd_back_lem begin match usize_add i 1 with | Fail _ -> () | Return i1 -> - hash_map_clear_slots_loop_fwd_back_lem t v i1; - begin match hash_map_clear_slots_loop_fwd_back t v i1 with + hash_map_clear_loop_fwd_back_lem t v i1; + begin match hash_map_clear_loop_fwd_back t v i1 with | Fail _ -> () | Return slots1 -> assert(length slots1 == length slots); @@ -658,7 +658,6 @@ let rec hash_map_clear_slots_loop_fwd_back_lem else () #pop-options -(*** clear *) /// [clear] doesn't fail and turns the hash map into an empty map val hash_map_clear_fwd_back_lem_aux (#t : Type0) (self : hash_map_t t) : @@ -683,8 +682,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_loop_fwd_back_lem t v 0; - begin match hash_map_clear_slots_loop_fwd_back t v 0 with + hash_map_clear_loop_fwd_back_lem t v 0; + begin match hash_map_clear_loop_fwd_back t v 0 with | Fail _ -> () | Return slots1 -> slots_t_al_v_all_nil_is_empty_lem slots1; diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst index f3afa008..1e15d1f9 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -12,9 +12,9 @@ let hashmap_hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : nat = admit () -(** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *) +(** [hashmap_main::hashmap::HashMap::{0}::clear]: decreases clause *) unfold -let hashmap_hash_map_clear_slots_loop_decreases (t : Type0) +let hashmap_hash_map_clear_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : nat = admit () diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst index 2f6a0acc..699ff3b2 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst @@ -11,9 +11,9 @@ unfold let hashmap_hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : nat = n -(** [hashmap::HashMap::clear_slots]: decreases clause *) +(** [hashmap::HashMap::clear]: decreases clause *) unfold -let hashmap_hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) +let hashmap_hash_map_clear_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index f3b480c3..56cff453 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -62,11 +62,11 @@ let hashmap_hash_map_new_with_capacity_fwd 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_loop_fwd_back +(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +let rec hashmap_hash_map_clear_loop_fwd_back (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_clear_slots_loop_decreases t slots i)) + (decreases (hashmap_hash_map_clear_loop_decreases t slots i)) = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 @@ -77,23 +77,16 @@ let rec hashmap_hash_map_clear_slots_loop_fwd_back begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil with | Fail e -> Fail e - | Return slots0 -> hashmap_hash_map_clear_slots_loop_fwd_back t slots0 i1 + | Return slots0 -> hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end end else Return slots -(** [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 with + hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 with | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor -- cgit v1.2.3