feat: Hashable (BitVec n) (#5881)

src/Init/Data/BitVec/Basic.lean

@@ -634,6 +634,16 @@ def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
 
 end bitwise
 
+/-- Compute a hash of a bitvector, combining 64-bit words using `mixHash`. -/
+def hash (bv : BitVec n) : UInt64 :=
+  if n ≤ 64 then
+    bv.toFin.val.toUInt64
+  else
+    mixHash (bv.toFin.val.toUInt64) (hash ((bv >>> 64).setWidth (n - 64)))
+
+instance : Hashable (BitVec n) where
+  hash := hash
+
 section normalization_eqs
 /-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
 @[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl

src/Init/Data/Hashable.lean

@@ -48,6 +48,9 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
+instance : Hashable ByteArray where
+  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
+
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64