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/lean | |
parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) |
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/lean')
-rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 9 | ||||
-rw-r--r-- | tests/lean/Constants.lean | 6 | ||||
-rw-r--r-- | tests/lean/Hashmap/Funs.lean | 6 | ||||
-rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 6 |
4 files changed, 5 insertions, 22 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 07ef08dc..6681731f 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -64,11 +64,6 @@ def betree.NodeIdCounter.fresh_id_back let i ← self.next_node_id + (U64.ofInt 1) Result.ret { next_node_id := i } -/- [core::num::u64::{9}::MAX] -/ -def core_num_u64_max_body : Result U64 := - Result.ret (U64.ofInt 18446744073709551615) -def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp) - /- [betree_main::betree::upsert_update]: forward function -/ def betree.upsert_update (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := @@ -81,10 +76,10 @@ def betree.upsert_update match st with | betree.UpsertFunState.Add v => do - let margin ← core_num_u64_max_c - prev0 + let margin ← core_u64_max - prev0 if margin >= v then prev0 + v - else Result.ret core_num_u64_max_c + else Result.ret core_u64_max | betree.UpsertFunState.Sub v => if prev0 >= v then prev0 - v diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index 51b415d6..b0cdaa90 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -9,12 +9,8 @@ namespace constants def x0_body : Result U32 := Result.ret (U32.ofInt 0) def x0_c : U32 := eval_global x0_body (by simp) -/- [core::num::u32::{8}::MAX] -/ -def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295) -def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) - /- [constants::X1] -/ -def x1_body : Result U32 := Result.ret core_num_u32_max_c +def x1_body : Result U32 := Result.ret core_u32_max def x1_c : U32 := eval_global x1_body (by simp) /- [constants::X2] -/ diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 30b30e0b..01c61de4 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -132,10 +132,6 @@ def HashMap.insert_no_resize let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 Result.ret { self with slots := v } -/- [core::num::u32::{8}::MAX] -/ -def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295) -def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) - /- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ divergent def HashMap.move_elements_from_list_loop @@ -184,7 +180,7 @@ def HashMap.move_elements (there is a single backward function, and the forward function returns ()) -/ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do - let max_usize ← Scalar.cast .Usize core_num_u32_max_c + let max_usize ← Scalar.cast .Usize core_u32_max let capacity := Vec.len (List T) self.slots let n1 ← max_usize / (Usize.ofInt 2) let (i, i0) := self.max_load_factor diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index aec957ec..848b1a35 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -147,10 +147,6 @@ def hashmap.HashMap.insert_no_resize let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 Result.ret { self with slots := v } -/- [core::num::u32::{8}::MAX] -/ -def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295) -def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) - /- [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 ()) -/ divergent def hashmap.HashMap.move_elements_from_list_loop @@ -206,7 +202,7 @@ def hashmap.HashMap.move_elements def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let max_usize ← Scalar.cast .Usize core_num_u32_max_c + let max_usize ← Scalar.cast .Usize core_u32_max let capacity := Vec.len (hashmap.List T) self.slots let n1 ← max_usize / (Usize.ofInt 2) let (i, i0) := self.max_load_factor |