λleanlab

Cryptography

Hashing and collisions

Use Lean’s built-in hash and see why a hash match is not proof of equality.

Open Hashing.lean in editor
-- hash is in Lean's core library. No import is needed.
-- It returns a UInt64 using a Hashable instance for the input type.
def fingerprint (text : String) : UInt64 := hash text

def main : IO Unit := do
  let original := fingerprint "Lean"
  let unchanged := fingerprint "Lean"
  let changed := fingerprint "lean"
  IO.println s!"Same input: {original == unchanged}"
  IO.println s!"Changed input: {original == changed}"

  -- For Nat, hash simply wraps the number to 64 bits.
  -- These distinct numbers therefore have the same hash.
  let a : Nat := 0
  let b : Nat := 2^64
  IO.println s!"Equal values: {a == b}"
  IO.println s!"Equal hashes: {hash a == hash b}"

-- A collision means distinct inputs have the same hash.
-- Lean's hash is for data structures, not cryptographic commitments.
-- Open the SHA-256 example for a cryptographic hash algorithm.

Explanation

hash · Hashable

hash asks the input type’s Hashable instance for a 64-bit hash. The implementation depends on the type and is not a cryptographic guarantee.

UInt64

An unsigned 64-bit integer. There are only 2^64 possible outputs, so hashing unbounded inputs must allow collisions.

hash a == hash b

Equal hashes do not establish a = b. This program shows a concrete collision.

Expected output

Reference only. Run the file to check its actual result.

Same input: true
Changed input: false
Equal values: false
Equal hashes: true

Exercise

Print fingerprint "Lean". Then hash 1 and 2^64 + 1 as natural numbers to find another collision.

Related examples

Further reading