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/hol4/betree/betreeMain_FunsScript.sml | 12 ++---------- tests/hol4/betree/betreeMain_FunsTheory.sig | 14 ++------------ tests/hol4/hashmap/hashmap_FunsScript.sml | 10 +--------- tests/hol4/hashmap/hashmap_FunsTheory.sig | 12 +----------- tests/hol4/hashmap/hashmap_PropertiesScript.sml | 2 +- tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml | 10 +--------- tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig | 12 +----------- tests/hol4/misc-constants/constantsScript.sml | 10 +--------- tests/hol4/misc-constants/constantsTheory.sig | 12 +----------- 9 files changed, 11 insertions(+), 83 deletions(-) (limited to 'tests/hol4') 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 -- cgit v1.2.3