From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/fstar/hashmap/Hashmap.Funs.fst |  6 +----
 tests/fstar/hashmap/Primitives.fst   | 47 ++++++++++++++++++++++++++++--------
 2 files changed, 38 insertions(+), 15 deletions(-)

(limited to 'tests/fstar/hashmap')

diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index f4c13a7b..40cd0477 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -139,10 +139,6 @@ let hash_map_insert_no_resize_fwd_back
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
     Return { self with hash_map_slots = v }
 
-(** [core::num::u32::{8}::MAX] *)
-let core_num_u32_max_body : result u32 = Return 4294967295
-let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-
 (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec hash_map_move_elements_from_list_loop_fwd_back
@@ -194,7 +190,7 @@ let hash_map_move_elements_fwd_back
     (there is a single backward function, and the forward function returns ()) *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
+  let* max_usize = scalar_cast U32 Usize core_u32_max in
   let capacity = vec_len (list_t t) self.hash_map_slots in
   let* n1 = usize_div max_usize 2 in
   let (i, i0) = self.hash_map_max_load_factor in
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
-- 
cgit v1.2.3