summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap_on_disk
diff options
context:
space:
mode:
authorSon Ho2023-09-07 16:06:14 +0200
committerSon Ho2023-09-07 16:06:14 +0200
commitce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch)
tree933d2bd806026930d216e4f16f113ea2749ca250 /tests/coq/hashmap_on_disk
parent1181aecddbcb3232c21b191fbde59c2e9596846a (diff)
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/coq/hashmap_on_disk')
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v6
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v14
2 files changed, 15 insertions, 5 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 657d5590..a85adbf2 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -208,10 +208,6 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
|})
.
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
(** [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 ()) *)
Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
@@ -282,7 +278,7 @@ Definition hashmap_hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
:=
- max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+ max_usize <- scalar_cast U32 Usize core_u32_max;
let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
n1 <- usize_div max_usize 2%usize;
let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/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;