summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/array/Primitives.v14
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v10
-rw-r--r--tests/coq/betree/Primitives.v14
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v6
-rw-r--r--tests/coq/hashmap/Primitives.v14
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v6
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v14
-rw-r--r--tests/coq/misc/Constants.v6
-rw-r--r--tests/coq/misc/Primitives.v14
-rw-r--r--tests/fstar/array/Primitives.fst47
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst8
-rw-r--r--tests/fstar/betree/Primitives.fst47
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst8
-rw-r--r--tests/fstar/betree_back_stateful/Primitives.fst47
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst6
-rw-r--r--tests/fstar/hashmap/Primitives.fst47
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst6
-rw-r--r--tests/fstar/hashmap_on_disk/Primitives.fst47
-rw-r--r--tests/fstar/misc/Constants.fst6
-rw-r--r--tests/fstar/misc/Primitives.fst47
-rw-r--r--tests/hol4/betree/betreeMain_FunsScript.sml12
-rw-r--r--tests/hol4/betree/betreeMain_FunsTheory.sig14
-rw-r--r--tests/hol4/hashmap/hashmap_FunsScript.sml10
-rw-r--r--tests/hol4/hashmap/hashmap_FunsTheory.sig12
-rw-r--r--tests/hol4/hashmap/hashmap_PropertiesScript.sml2
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml10
-rw-r--r--tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig12
-rw-r--r--tests/hol4/misc-constants/constantsScript.sml10
-rw-r--r--tests/hol4/misc-constants/constantsTheory.sig12
-rw-r--r--tests/lean/BetreeMain/Funs.lean9
-rw-r--r--tests/lean/Constants.lean6
-rw-r--r--tests/lean/Hashmap/Funs.lean6
-rw-r--r--tests/lean/HashmapMain/Funs.lean6
33 files changed, 320 insertions, 215 deletions
diff --git a/tests/coq/array/Primitives.v b/tests/coq/array/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/array/Primitives.v
+++ b/tests/coq/array/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 1e457433..cfa1f8fb 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -75,12 +75,6 @@ Definition betree_node_id_counter_fresh_id_back
Return {| Betree_node_id_counter_next_node_id := i |}
.
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body : result u64 :=
- Return 18446744073709551615%u64
-.
-Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
-
(** [betree_main::betree::upsert_update]: forward function *)
Definition betree_upsert_update_fwd
(prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 :=
@@ -93,8 +87,8 @@ Definition betree_upsert_update_fwd
| Some prev0 =>
match st with
| BetreeUpsertFunStateAdd v =>
- margin <- u64_sub core_num_u64_max_c prev0;
- if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
+ margin <- u64_sub core_u64_max prev0;
+ if margin s>= v then u64_add prev0 v else Return core_u64_max
| BetreeUpsertFunStateSub v =>
if prev0 s>= v then u64_sub prev0 v else Return 0%u64
end
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index e950ba0b..054880d4 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -190,10 +190,6 @@ Definition hash_map_insert_no_resize_fwd_back
|})
.
-(** [core::num::u32::{8}::MAX] *)
-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]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Fixpoint hash_map_move_elements_from_list_loop_fwd_back
@@ -259,7 +255,7 @@ Definition hash_map_move_elements_fwd_back
(there is a single backward function, and the forward function returns ()) *)
Definition hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
- max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+ max_usize <- scalar_cast U32 Usize core_u32_max;
let capacity := vec_len (List_t T) self.(Hash_map_slots) in
n1 <- usize_div max_usize 2%usize;
let (i, i0) := self.(Hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 657d5590..a85adbf2 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -208,10 +208,6 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
|})
.
-(** [core::num::u32::{8}::MAX] *)
-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]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
@@ -282,7 +278,7 @@ Definition hashmap_hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
:=
- max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+ max_usize <- scalar_cast U32 Usize core_u32_max;
let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
n1 <- usize_div max_usize 2%usize;
let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index f1c32730..5dd78a09 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -12,12 +12,8 @@ Module Constants.
Definition x0_body : result u32 := Return 0%u32.
Definition x0_c : u32 := x0_body%global.
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
(** [constants::X1] *)
-Definition x1_body : result u32 := Return core_num_u32_max_c.
+Definition x1_body : result u32 := Return core_u32_max.
Definition x1_c : u32 := x1_body%global.
(** [constants::X2] *)
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope.
Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope.
Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope.
+(** Constants *)
+Definition core_u8_max := u8_max %u32.
+Definition core_u16_max := u16_max %u32.
+Definition core_u32_max := u32_max %u32.
+Definition core_u64_max := u64_max %u64.
+Definition core_u128_max := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max := i8_max %i32.
+Definition core_i16_max := i16_max %i32.
+Definition core_i32_max := i32_max %i32.
+Definition core_i64_max := i64_max %i64.
+Definition core_i128_max := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
(*** Range *)
Record range (T : Type) := mk_range {
start: T;
diff --git a/tests/fstar/array/Primitives.fst b/tests/fstar/array/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/array/Primitives.fst
+++ b/tests/fstar/array/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
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 847dc865..2bb2352b 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -60,10 +60,6 @@ let betree_node_id_counter_fresh_id_back
let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
Return { betree_node_id_counter_next_node_id = i }
-(** [core::num::u64::{9}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
(** [betree_main::betree::upsert_update]: forward function *)
let betree_upsert_update_fwd
(prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -76,8 +72,8 @@ let betree_upsert_update_fwd
| Some prev0 ->
begin match st with
| BetreeUpsertFunStateAdd v ->
- let* margin = u64_sub core_num_u64_max_c prev0 in
- if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
+ let* margin = u64_sub core_u64_max prev0 in
+ if margin >= v then u64_add prev0 v else Return core_u64_max
| BetreeUpsertFunStateSub v ->
if prev0 >= v then u64_sub prev0 v else Return 0
end
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/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
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 3d08cd3c..8083ee8f 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -60,10 +60,6 @@ let betree_node_id_counter_fresh_id_back
let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
Return { betree_node_id_counter_next_node_id = i }
-(** [core::num::u64::{9}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
(** [betree_main::betree::upsert_update]: forward function *)
let betree_upsert_update_fwd
(prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -76,8 +72,8 @@ let betree_upsert_update_fwd
| Some prev0 ->
begin match st with
| BetreeUpsertFunStateAdd v ->
- let* margin = u64_sub core_num_u64_max_c prev0 in
- if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
+ let* margin = u64_sub core_u64_max prev0 in
+ if margin >= v then u64_add prev0 v else Return core_u64_max
| BetreeUpsertFunStateSub v ->
if prev0 >= v then u64_sub prev0 v else Return 0
end
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/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
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
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 1c94209c..5af90bd8 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -157,10 +157,6 @@ let hashmap_hash_map_insert_no_resize_fwd_back
hash_mod l0 in
Return { self with hashmap_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_main::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 hashmap_hash_map_move_elements_from_list_loop_fwd_back
@@ -218,7 +214,7 @@ let hashmap_hash_map_move_elements_fwd_back
(there is a single backward function, and the forward function returns ()) *)
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
- let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
+ let* max_usize = scalar_cast U32 Usize core_u32_max in
let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
let* n1 = usize_div max_usize 2 in
let (i, i0) = self.hashmap_hash_map_max_load_factor in
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/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
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index d2b0415e..7dfb6f36 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -9,12 +9,8 @@ open Primitives
let x0_body : result u32 = Return 0
let x0_c : u32 = eval_global x0_body
-(** [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
-
(** [constants::X1] *)
-let x1_body : result u32 = Return core_num_u32_max_c
+let x1_body : result u32 = Return core_u32_max
let x1_c : u32 = eval_global x1_body
(** [constants::X2] *)
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/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
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 5e604f8c..bd16c16c 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -88,14 +88,6 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘
od
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body_def:
- core_num_u64_max_body : u64 result = Return (int_to_u64 18446744073709551615)
-End
-Definition core_num_u64_max_c_def:
- core_num_u64_max_c : u64 = get_return_value core_num_u64_max_body
-End
-
val betree_upsert_update_fwd_def = Define ‘
(** [betree_main::betree::upsert_update]: forward function *)
betree_upsert_update_fwd
@@ -109,8 +101,8 @@ val betree_upsert_update_fwd_def = Define ‘
(case st of
| BetreeUpsertFunStateAdd v =>
do
- margin <- u64_sub core_num_u64_max_c prev0;
- if u64_ge margin v then u64_add prev0 v else Return core_num_u64_max_c
+ margin <- u64_sub core_u64_max prev0;
+ if u64_ge margin v then u64_add prev0 v else Return core_u64_max
od
| BetreeUpsertFunStateSub v =>
if u64_ge prev0 v then u64_sub prev0 v else Return (int_to_u64 0)))
diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betreeMain_FunsTheory.sig
index 6c249f70..c922ca9f 100644
--- a/tests/hol4/betree/betreeMain_FunsTheory.sig
+++ b/tests/hol4/betree/betreeMain_FunsTheory.sig
@@ -58,8 +58,6 @@ sig
val betree_store_internal_node_fwd_def : thm
val betree_store_leaf_node_fwd_def : thm
val betree_upsert_update_fwd_def : thm
- val core_num_u64_max_body_def : thm
- val core_num_u64_max_c_def : thm
val main_fwd_def : thm
val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1215,22 +1213,14 @@ sig
case st of
BetreeUpsertFunStateAdd v =>
do
- margin <- u64_sub core_num_u64_max_c prev0;
+ margin <- u64_sub core_u64_max prev0;
if u64_ge margin v then u64_add prev0 v
- else Return core_num_u64_max_c
+ else Return core_u64_max
od
| BetreeUpsertFunStateSub v' =>
if u64_ge prev0 v' then u64_sub prev0 v'
else Return (int_to_u64 0)
- [core_num_u64_max_body_def] Definition
-
- ⊢ core_num_u64_max_body = Return (int_to_u64 18446744073709551615)
-
- [core_num_u64_max_c_def] Definition
-
- ⊢ core_num_u64_max_c = get_return_value core_num_u64_max_body
-
[main_fwd_def] Definition
⊢ main_fwd = Return ()
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
index e3c3d2a5..682c5760 100644
--- a/tests/hol4/hashmap/hashmap_FunsScript.sml
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -170,14 +170,6 @@ val hash_map_insert_no_resize_fwd_back_def = Define ‘
od
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
- core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
- core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
(** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
@@ -241,7 +233,7 @@ val hash_map_try_resize_fwd_back_def = Define ‘
(there is a single backward function, and the forward function returns ()) *)
hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
do
- max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ max_usize <- mk_usize (u32_to_int core_u32_max);
let capacity = vec_len self.hash_map_slots in
do
n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig
index 50482547..bb3e192b 100644
--- a/tests/hol4/hashmap/hashmap_FunsTheory.sig
+++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
type thm = Thm.thm
(* Definitions *)
- val core_num_u32_max_body_def : thm
- val core_num_u32_max_c_def : thm
val hash_key_fwd_def : thm
val hash_map_allocate_slots_fwd_def : thm
val hash_map_allocate_slots_loop_fwd_def : thm
@@ -48,14 +46,6 @@ sig
(*
[hashmap_Types] Parent theory of "hashmap_Funs"
- [core_num_u32_max_body_def] Definition
-
- ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-
- [core_num_u32_max_c_def] Definition
-
- ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-
[hash_key_fwd_def] Definition
⊢ ∀k. hash_key_fwd k = Return k
@@ -472,7 +462,7 @@ sig
⊢ ∀self.
hash_map_try_resize_fwd_back self =
do
- max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ max_usize <- mk_usize (u32_to_int core_u32_max);
capacity <<- vec_len self.hash_map_slots;
n1 <- usize_div max_usize (int_to_usize 2);
(i,i0) <<- self.hash_map_max_load_factor;
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 7259f2f5..8bc12fa5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1296,7 +1296,7 @@ Proof
rw [hash_map_try_resize_fwd_back_def] >>
(* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *)
assume_tac usize_u32_bounds >>
- fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >>
+ fs [core_u32_max_def, u32_max_def] >>
massage >> fs [mk_usize_def, u32_max_def] >>
(* / 2 *)
progress >>
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
index b21c4f58..c1e30aa6 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
@@ -193,14 +193,6 @@ val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘
od
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
- core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
- core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
@@ -271,7 +263,7 @@ val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
hashmap_hash_map_try_resize_fwd_back
(self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
do
- max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ max_usize <- mk_usize (u32_to_int core_u32_max);
let capacity = vec_len self.hashmap_hash_map_slots in
do
n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
index 1d24cb26..d4e43d9a 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
type thm = Thm.thm
(* Definitions *)
- val core_num_u32_max_body_def : thm
- val core_num_u32_max_c_def : thm
val hashmap_hash_key_fwd_def : thm
val hashmap_hash_map_allocate_slots_fwd_def : thm
val hashmap_hash_map_allocate_slots_loop_fwd_def : thm
@@ -50,14 +48,6 @@ sig
(*
[hashmapMain_Opaque] Parent theory of "hashmapMain_Funs"
- [core_num_u32_max_body_def] Definition
-
- ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-
- [core_num_u32_max_c_def] Definition
-
- ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-
[hashmap_hash_key_fwd_def] Definition
⊢ ∀k. hashmap_hash_key_fwd k = Return k
@@ -506,7 +496,7 @@ sig
⊢ ∀self.
hashmap_hash_map_try_resize_fwd_back self =
do
- max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ max_usize <- mk_usize (u32_to_int core_u32_max);
capacity <<- vec_len self.hashmap_hash_map_slots;
n1 <- usize_div max_usize (int_to_usize 2);
(i,i0) <<- self.hashmap_hash_map_max_load_factor;
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/misc-constants/constantsScript.sml
index d589d348..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/misc-constants/constantsScript.sml
@@ -13,17 +13,9 @@ Definition x0_c_def:
x0_c : u32 = get_return_value x0_body
End
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
- core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
- core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
(** [constants::X1] *)
Definition x1_body_def:
- x1_body : u32 result = Return core_num_u32_max_c
+ x1_body : u32 result = Return core_u32_max
End
Definition x1_c_def:
x1_c : u32 = get_return_value x1_body
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 149d7e22..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -4,8 +4,6 @@ sig
(* Definitions *)
val add_fwd_def : thm
- val core_num_u32_max_body_def : thm
- val core_num_u32_max_c_def : thm
val get_z1_fwd_def : thm
val get_z1_z1_body_def : thm
val get_z1_z1_c_def : thm
@@ -110,14 +108,6 @@ sig
⊢ ∀a b. add_fwd a b = i32_add a b
- [core_num_u32_max_body_def] Definition
-
- ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-
- [core_num_u32_max_c_def] Definition
-
- ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-
[get_z1_fwd_def] Definition
⊢ get_z1_fwd = Return get_z1_z1_c
@@ -321,7 +311,7 @@ sig
[x1_body_def] Definition
- ⊢ x1_body = Return core_num_u32_max_c
+ ⊢ x1_body = Return core_u32_max
[x1_c_def] Definition
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 07ef08dc..6681731f 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -64,11 +64,6 @@ def betree.NodeIdCounter.fresh_id_back
let i ← self.next_node_id + (U64.ofInt 1)
Result.ret { next_node_id := i }
-/- [core::num::u64::{9}::MAX] -/
-def core_num_u64_max_body : Result U64 :=
- Result.ret (U64.ofInt 18446744073709551615)
-def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
-
/- [betree_main::betree::upsert_update]: forward function -/
def betree.upsert_update
(prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -81,10 +76,10 @@ def betree.upsert_update
match st with
| betree.UpsertFunState.Add v =>
do
- let margin ← core_num_u64_max_c - prev0
+ let margin ← core_u64_max - prev0
if margin >= v
then prev0 + v
- else Result.ret core_num_u64_max_c
+ else Result.ret core_u64_max
| betree.UpsertFunState.Sub v =>
if prev0 >= v
then prev0 - v
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 51b415d6..b0cdaa90 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -9,12 +9,8 @@ namespace constants
def x0_body : Result U32 := Result.ret (U32.ofInt 0)
def x0_c : U32 := eval_global x0_body (by simp)
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
/- [constants::X1] -/
-def x1_body : Result U32 := Result.ret core_num_u32_max_c
+def x1_body : Result U32 := Result.ret core_u32_max
def x1_c : U32 := eval_global x1_body (by simp)
/- [constants::X2] -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 30b30e0b..01c61de4 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -132,10 +132,6 @@ def HashMap.insert_no_resize
let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
Result.ret { self with slots := v }
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
/- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
divergent def HashMap.move_elements_from_list_loop
@@ -184,7 +180,7 @@ def HashMap.move_elements
(there is a single backward function, and the forward function returns ()) -/
def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
- let max_usize ← Scalar.cast .Usize core_num_u32_max_c
+ let max_usize ← Scalar.cast .Usize core_u32_max
let capacity := Vec.len (List T) self.slots
let n1 ← max_usize / (Usize.ofInt 2)
let (i, i0) := self.max_load_factor
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index aec957ec..848b1a35 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -147,10 +147,6 @@ def hashmap.HashMap.insert_no_resize
let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
Result.ret { self with slots := v }
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
divergent def hashmap.HashMap.move_elements_from_list_loop
@@ -206,7 +202,7 @@ def hashmap.HashMap.move_elements
def hashmap.HashMap.try_resize
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
- let max_usize ← Scalar.cast .Usize core_num_u32_max_c
+ let max_usize ← Scalar.cast .Usize core_u32_max
let capacity := Vec.len (hashmap.List T) self.slots
let n1 ← max_usize / (Usize.ofInt 2)
let (i, i0) := self.max_load_factor