feat: add BEq instance for ByteArray that uses memcmp

[algebraic-dev]

This PR adds a BEq instance for ByteArray that uses memcmp.

[Rob23oba]

FWIW I have a draft at #8165 with some ideas for expanding the byte array API that includes:

/--
Return true iff the slices `[asOff, asOff + len)` in `as` and `[bsOff, bsOff + len)` in
`bs` contain the same data.
-/
@[extern "lean_byte_array_slice_eq"]
def sliceEq' (as : @& ByteArray) (asOff : @& Nat) (bs : @& ByteArray) (bsOff : @& Nat) (len : @& Nat)
    (h : asOff + len ≤ as.size := by get_elem_tactic)
    (h' : bsOff + len ≤ bs.size := by get_elem_tactic) : Bool :=
  as.data.extract asOff (asOff + len) == bs.data.extract bsOff (bsOff + len)

/--
Returns whether two byte arrays are equal.
The notation `==` is preferred over using this function directly.
-/
protected def beq (as bs : ByteArray) : Bool :=
  if h : as.size = bs.size then
    sliceEq' as 0 bs 0 as.size
  else
    false

[algebraic-dev]

@Rob23oba Why is it still a draft? Is there anything I can add to your PR to help get it merged as soon as possible?

[Rob23oba]

Well there's a lot of other stuff I haven't quite figured out yet; In particular the code generated for the set functions is more than suboptimal because of all the rc checks, maybe I should just implement them in C though; and I'm not quite sure about the API of these functions; a lot of these are really low level and require a lot of proofs and sometimes Quot to work with. I guess you can take a look at the changes and review them though if you want.