ByteArray.copySlice behavior inconsistent with its def

Stream: lean4

[ZHAO Jiecheng]

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

/--
@[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 some_func (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 some_func ⟨#[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]

[ZHAO Jiecheng]

Opened an Issue https://github.com/leanprover/lean4/issues/2966

[Scott Morrison]

Fixed at lean#2967

[ZHAO Jiecheng]

@Scott Morrison sorry, but I guess this is not the ticket you what to commented on.

[ZHAO Jiecheng]

Scott Morrison said:

Fixed at #2967

Sorry again. I found the pr. Thank you for your help. I think the link is not so correct. It pointed to a mathlib fix.

[ZHAO Jiecheng]

Fixed at https://github.com/leanprover/lean4/pull/2967/checks