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/coq/betree/BetreeMain_Funs.v | 10 ++--------
 tests/coq/betree/Primitives.v      | 14 ++++++++++++++
 2 files changed, 16 insertions(+), 8 deletions(-)

(limited to 'tests/coq/betree')

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;
-- 
cgit v1.2.3