From 689bd4ffde55d32850c82ecb52bf01d1cd3104de Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 1 Jul 2025 23:23:19 -0300 Subject: [PATCH 1/4] feat: migrate beq for improved perf using memcmp --- src/Init/Data/ByteArray/Basic.lean | 12 ++++++++++-- src/runtime/object.cpp | 11 +++++++++++ src/runtime/object.h | 1 - 3 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 8592e9af3a1b..786727f76c8b 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -23,10 +23,18 @@ attribute [extern "lean_byte_array_data"] ByteArray.data namespace ByteArray -deriving instance BEq for ByteArray - attribute [ext] ByteArray +/-- +Checks whether two `ByteArray` instances have the same length and identical content. Normally used +via the `==` operator. +-/ +@[extern "lean_byte_array_beq"] +protected def beq (a b : @& ByteArray) : Bool := + BEq.beq a.data b.data + +instance : BEq ByteArray := ⟨ByteArray.beq⟩ + instance : DecidableEq ByteArray := fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 8e6ea4908324..647f35c6b790 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2419,6 +2419,17 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_mk(obj_arg a) { return r; } +extern "C" LEAN_EXPORT bool lean_byte_array_beq(obj_arg a, obj_arg b) { + size_t size_a = lean_sarray_size(a); + size_t size_b = lean_sarray_size(b); + + if (size_a != size_b) { + return 0; + } + + return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0; +} + extern "C" LEAN_EXPORT obj_res lean_byte_array_data(obj_arg a) { usize sz = lean_sarray_size(a); obj_res r = lean_alloc_array(sz, sz); diff --git a/src/runtime/object.h b/src/runtime/object.h index 577c92e2f437..b9ca9525a988 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -220,7 +220,6 @@ inline uint8 * sarray_cptr(object * o) { return lean_sarray_cptr(o); } // ByteArray inline obj_res byte_array_mk(obj_arg a) { return lean_byte_array_mk(a); } -inline obj_res byte_array_data(obj_arg a) { return lean_byte_array_data(a); } inline obj_res copy_byte_array(obj_arg a) { return lean_copy_byte_array(a); } inline obj_res mk_empty_byte_array(b_obj_arg capacity) { return lean_mk_empty_byte_array(capacity); } inline obj_res byte_array_size(b_obj_arg a) { return lean_byte_array_size(a); } From 24f2699e78e03e309785b64516230e862d4a05f6 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 7 Jul 2025 18:26:04 -0300 Subject: [PATCH 2/4] revert: change --- src/runtime/object.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/runtime/object.h b/src/runtime/object.h index b9ca9525a988..577c92e2f437 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -220,6 +220,7 @@ inline uint8 * sarray_cptr(object * o) { return lean_sarray_cptr(o); } // ByteArray inline obj_res byte_array_mk(obj_arg a) { return lean_byte_array_mk(a); } +inline obj_res byte_array_data(obj_arg a) { return lean_byte_array_data(a); } inline obj_res copy_byte_array(obj_arg a) { return lean_copy_byte_array(a); } inline obj_res mk_empty_byte_array(b_obj_arg capacity) { return lean_mk_empty_byte_array(capacity); } inline obj_res byte_array_size(b_obj_arg a) { return lean_byte_array_size(a); } From 4ff5e275ef86a675387689a382b03f24f8b48499 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 25 Jul 2025 13:40:48 -0300 Subject: [PATCH 3/4] feat: add same obj comparison --- src/runtime/object.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 647f35c6b790..e11b0d3da11e 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2420,14 +2420,18 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_mk(obj_arg a) { } extern "C" LEAN_EXPORT bool lean_byte_array_beq(obj_arg a, obj_arg b) { - size_t size_a = lean_sarray_size(a); - size_t size_b = lean_sarray_size(b); + if (a == b) { + return 1; + } - if (size_a != size_b) { - return 0; - } + size_t size_a = lean_sarray_size(a); + size_t size_b = lean_sarray_size(b); + + if (size_a != size_b) { + return 0; + } - return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0; + return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0; } extern "C" LEAN_EXPORT obj_res lean_byte_array_data(obj_arg a) { From 3609d2e32130bb7175d4a8aff550762b265dec53 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 25 Jul 2025 14:32:54 -0300 Subject: [PATCH 4/4] fix: change 0 and 1 to false and true --- src/runtime/object.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index e11b0d3da11e..032aae0e01df 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2421,14 +2421,14 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_mk(obj_arg a) { extern "C" LEAN_EXPORT bool lean_byte_array_beq(obj_arg a, obj_arg b) { if (a == b) { - return 1; + return true; } size_t size_a = lean_sarray_size(a); size_t size_b = lean_sarray_size(b); if (size_a != size_b) { - return 0; + return false; } return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0;