4.3. Hashing and result observation are not free🔗

The harness's "did we observe the result" mechanism is Hashable.hash result (or Hashable.hash (sizeOf result) as a fallback). For small or fixed-width return types this is a few ns and you can ignore it. Lean core's Hashable instances vary in cost:

• Hashable Nat is UInt64.ofNat, so a single bignum hashes in constant time regardless of bit width. Containers are still linear in length: a List Nat of length k costs Θ(k) to hash, not Θ(k * limbs).

• Hashable String walks the whole string. Long strings are a real cost.

• Hashable ByteArray likewise walks every byte.

• derived Hashable on a recursive type walks the whole tree. A balanced tree of depth d with n = 2^d leaves takes Θ(n) hash time.

When the result-observation cost is comparable to or larger than the algorithm cost, the verdict reflects the hash, not the algorithm. Two practical responses:

• Measure intermediate work explicitly. Have the benchmark return a small summary (the array's sum, the polynomial's degree, a UInt64 rolling hash) instead of the full structure. The summary needs to actually depend on every part of the work, otherwise the compiler may DCE the parts you don't observe.

• Use with prep := … for setup that should not be re-timed. See Quickstart. The prep result is hashed once, before timing begins, so its construction cost is paid up front and not folded into every inner iteration.

lean-bench's compare reports agreement over the common-param intersection: hashes either match (allAgreed) or diverge at named triples. A function whose return type is not Hashable falls back to "hashUnavailable" — the comparison still runs, but you lose the cross-implementation correctness check. Prefer Hashable-bearing return types when you have a choice.