diff options
author | Son Ho | 2023-09-07 16:06:14 +0200 |
---|---|---|
committer | Son Ho | 2023-09-07 16:06:14 +0200 |
commit | ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch) | |
tree | 933d2bd806026930d216e4f16f113ea2749ca250 /tests/coq/betree/BetreeMain_Funs.v | |
parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) |
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/coq/betree/BetreeMain_Funs.v')
-rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 10 |
1 files changed, 2 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 |