 Solution

Membership is exactly whether the bucket search finds an entry:

def isInBook(name: String): Boolean = {
  find(name, table(hash(name))) != null
}

By the bucket-placement representation invariant, an entry with this name can occur only in this bucket. The find contract therefore proves true exactly for keys in the map's domain, with no state change. One hash calculation and one bucket traversal suffice; no insertion is performed during the query.