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/hol4/betree | |
| parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) | |
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/hol4/betree')
| -rw-r--r-- | tests/hol4/betree/betreeMain_FunsScript.sml | 12 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_FunsTheory.sig | 14 |
2 files changed, 4 insertions, 22 deletions
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 () |