Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

4 files changed, 16 insertions, 1 deletions

diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
index c1549e6b..2a3d9cb9 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -24,6 +24,10 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
   (ls : list_t t) : nat =
   admit ()
 
+(** [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]: decreases clause *)
 unfold
 let hash_map_move_elements_from_list_decreases (t : Type0)
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 83c245fb..397ee720 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -188,6 +188,10 @@ let hash_map_insert_no_resize_fwd_back
     end
   end
 
+(** [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] *)
 let rec hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
@@ -244,7 +248,7 @@ let rec hash_map_move_elements_fwd_back
 (** [hashmap::HashMap::{0}::try_resize] *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  begin match scalar_cast U32 Usize 4294967295 with
+  begin match scalar_cast U32 Usize core_num_u32_max_c with
   | Fail -> Fail
   | Return max_usize ->
     let capacity = vec_len (list_t t) self.hash_map_slots in
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
index 91ee26c6..f81f4185 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -19,3 +19,7 @@ type hash_map_t (t : Type0) =
   hash_map_slots : vec (list_t t);
 }
 
+(** [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
+
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string