clarified hash and equality: depend on sha1 digest to be collision-free;

--- a/src/Pure/General/bytes.scala	Wed Jun 12 21:59:44 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jun 12 22:09:16 2024 +0200
@@ -172,35 +172,30 @@
     else throw new IndexOutOfBoundsException
 
 
-  /* equality */
+  /* hash and equality */
+
+  lazy val sha1_digest: SHA1.Digest =
+    if (is_empty) SHA1.digest_empty else SHA1.digest(bytes, offset, length)
+
+  override def hashCode(): Int = sha1_digest.hashCode()
 
   override def equals(that: Any): Boolean = {
     that match {
       case other: Bytes =>
-        this.eq(other) ||
-        Arrays.equals(bytes, offset, offset + length,
-          other.bytes, other.offset, other.offset + other.length)
+        if (this.eq(other)) true
+        else if (size != other.size) false
+        else if (size <= 10 * SHA1.digest_length) {
+          Arrays.equals(bytes, offset, offset + length,
+            other.bytes, other.offset, other.offset + other.length)
+        }
+        else sha1_digest == other.sha1_digest
       case _ => false
     }
   }
 
-  private lazy val hash: Int = {
-    var h = 0
-    for (i <- offset until offset + length) {
-      val b = bytes(i).asInstanceOf[Int] & 0xFF
-      h = 31 * h + b
-    }
-    h
-  }
-
-  override def hashCode(): Int = hash
-
 
   /* content */
 
-  lazy val sha1_digest: SHA1.Digest =
-    if (is_empty) SHA1.digest_empty else SHA1.digest(bytes, offset, length)
-
   def array: Array[Byte] = {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)