HepLean Documentation

Std.Data.DHashMap.Internal.Index

This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

File contents: mapping a hash to a hash map bucket

source
@[inline]
def Std.DHashMap.Internal.scrambleHash (hash : UInt64) :
UInt64

Scramble the hash code in order to protect against bad hash functions.

Example: if Hashable Float was implemented using the "identity" reinterpreting the bit pattern as a UInt64, then the hash codes of all small positive or negative integers would end in around 50 zeroes, meaning that they all land in bucket 0 in reasonably-sized hash maps.

To counteract this, we xor the hash code with some shifted-down versions of itself, to make sure that all of the entropy of the hash code appears in the lower 16 bits at least.

The scrambling operation is very fast. It does not have a measurable impact on performance in the insert benchmark.

Equations
Instances For
    source
    @[irreducible, inline]
    def Std.DHashMap.Internal.mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
    { u : USize // u.toNat < sz }

    sz is an explicit parameter because having it inferred from h can lead to suboptimal IR, cf. https://github.com/leanprover/lean4/issues/4157

    Equations
    Instances For