summaryrefslogtreecommitdiff
path: root/tests/coq/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/betree')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v10
-rw-r--r--tests/coq/betree/Primitives.v14
2 files changed, 16 insertions, 8 deletions
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;