ByteArray.copySlice behavior inconsistent with its def

[JiechengZhao]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Hi, found ByteArray.copySlice behavior inconsistent with its def when srcOff + len > src.size

Steps to Reproduce

/--
@[extern "lean_byte_array_copy_slice"]
def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + len) dest.data.size⟩
-/

def copySlice_ (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + len) dest.data.size⟩

#eval copySlice_ ⟨#[1, 2, 3]⟩ 1 ⟨#[4, 5, 6, 7 , 8 , 9, 10, 11, 12, 13]⟩ 0 6 -- [2, 3, 10, 11, 12, 13]
#eval ByteArray.copySlice ⟨#[1, 2, 3]⟩ 1 ⟨#[4, 5, 6, 7 , 8 , 9, 10, 11, 12, 13]⟩ 0 6 -- [2, 3, 6, 7, 8, 9, 10, 11, 12, 13]

Expected behavior:

The copySlice_ and ByteArray.copySlice should be same

Actual behavior:
ByteArray.copySlice works like this.

def some_func (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
  let len_ := min (len) (src.size)
  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len_) ++ dest.data.extract (destOff + len_) dest.data.size⟩

Versions

"4.3.0-rc2"
Ubuntu 22.04.3 LTS

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.