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