Cryptography · 7 min

Hashes and collisions

A hash maps an input to a fixed-size value. Lean’s built-in hash returns UInt64 and needs no additional library. A Hashable instance determines how each type is hashed.

Implementing the function below shows the basic API. In the related example, hashing 0 and 2^64 as Nat produces the same result even though the numbers differ. Such a pair is a collision.

Core hash supports data structures; it is not a cryptographic hash API. SHA-256 is designed to resist finding collisions or an input for a given digest. Hashing does not hide predictable inputs: an attacker can hash likely messages and compare the results. Collisions still exist because the output has a fixed size.

Comparing hashes does not prove that arbitrary inputs are equal. The checks for this exercise verify the requested implementation on several inputs; they do not prove collision resistance.

Exercise

Return hash text from fingerprint, then run main.

def fingerprint (text : String) : UInt64 := 0

def main : IO Unit := do
  IO.println (fingerprint "Lean")

def fingerprint (text : String) : UInt64 := hash text

def main : IO Unit := do
  IO.println (fingerprint "Lean")

Related example