Skip to content

Cuckoo hashing

24 fully proved

Cuckoo Hashing

StructureCuckoo hash table#✓fully proved

Given a type \(K\) of keys, a type \(V\) of values, a number \(m\) of slots, and two hash functions \(h_1, h_2 : K \to \{0, \dots, m - 1\}\), a cuckoo hash table consists of two tables, each a vector of \(m\) slots; every slot is either empty or holds a key–value pair \((k, v)\) with \(k \in K\) and \(v \in V\). The structure itself does not require a pair \((k, v)\) to sit at slot \(h_1(k)\) of the first table or at slot \(h_2(k)\) of the second.

No expected constant-time bound is claimed because the model supplies neither a probability distribution nor an independence assumption about the hashes.

public structure CuckooHashing (K : Type u) (V : Type v) (m : Nat)
    (h1 h2 : K → Fin m) where
  /-- The first table; key `k` may occupy slot `h1 k`. -/
  table1 : Vector (Option (K × V)) m
  /-- The second table; key `k` may occupy slot `h2 k`. -/
  table2 : Vector (Option (K × V)) m
Used by 22
Used byEmpty cuckoo hash table · Cuckoo hash insertion · Cuckoo eviction loop · Key determinism of a cuckoo hash table · The empty cuckoo hash table is key-deterministic · Cuckoo insertion preserves key determinism · Cuckoo hash table lookup · Lookup in the empty cuckoo hash table · Cuckoo lookup finds exactly the stored bindings · Cuckoo lookup finds every stored binding · Cuckoo lookup finds a key in its first-table slot · Cuckoo lookup finds a key in its second-table slot · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged · Cuckoo lookup finds every stored key · Soundness of cuckoo lookup · Binding stored in a cuckoo hash table · Cuckoo insertion stores the inserted binding · Cuckoo insertion preserves the bindings of other keys · Placement invariant of a cuckoo hash table · The empty cuckoo hash table satisfies the placement invariant · Cuckoo insertion preserves the placement invariant

DefinitionEmpty cuckoo hash table#✓fully proved

The empty cuckoo hash table has every slot of both tables vacant.

public def empty : CuckooHashing K V m h1 h2 :=
  ⟨Vector.replicate m none, Vector.replicate m none⟩
Uses 1 · Used by 3
Statement usesCuckoo hash table
Used byThe empty cuckoo hash table is key-deterministic · Lookup in the empty cuckoo hash table · The empty cuckoo hash table satisfies the placement invariant

DefinitionPlacement invariant of a cuckoo hash table#✓fully proved

A cuckoo hash table with hash functions \(h_1, h_2\) satisfies the placement invariant when every pair \((k, v)\) in slot \(i\) of the first table has \(i = h_1(k)\), and every pair \((k, v)\) in slot \(i\) of the second table has \(i = h_2(k)\).

This is what lets lookup check only two slots.

public def Valid (table : CuckooHashing K V m h1 h2) : Prop :=
  (∀ (i : Fin m) (key : K) (value : V),
    table.table1.get i = some (key, value) → i = h1 key) ∧
    ∀ (i : Fin m) (key : K) (value : V),
      table.table2.get i = some (key, value) → i = h2 key
Uses 1 · Used by 9
Statement usesCuckoo hash table
Used byCuckoo insertion preserves key determinism · Cuckoo lookup finds exactly the stored bindings · Cuckoo lookup finds every stored binding · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged · Cuckoo lookup finds every stored key · Cuckoo insertion preserves the bindings of other keys · The empty cuckoo hash table satisfies the placement invariant · Cuckoo insertion preserves the placement invariant

DefinitionBinding stored in a cuckoo hash table#✓fully proved

A key \(k\) is stored with value \(v\) in a cuckoo hash table when the pair \((k, v)\) occupies some slot of the first table or some slot of the second table.

public def Stored (table : CuckooHashing K V m h1 h2) (key : K) (value : V) : Prop :=
  (∃ i : Fin m, table.table1.get i = some (key, value)) ∨
    ∃ i : Fin m, table.table2.get i = some (key, value)
Uses 1 · Used by 11
Statement usesCuckoo hash table
Used byKey determinism of a cuckoo hash table · The empty cuckoo hash table is key-deterministic · Cuckoo insertion preserves key determinism · Cuckoo lookup finds exactly the stored bindings · Cuckoo lookup finds every stored binding · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged · Cuckoo lookup finds every stored key · Soundness of cuckoo lookup · Cuckoo insertion stores the inserted binding · Cuckoo insertion preserves the bindings of other keys

DefinitionKey determinism of a cuckoo hash table#✓fully proved

A cuckoo hash table is key-deterministic when each key is stored with at most one value: for every key \(k\) and values \(v_1, v_2\), if the bindings \(k \mapsto v_1\) and \(k \mapsto v_2\) are both stored in the table, then \(v_1 = v_2\). Duplicate copies of the same pair are allowed.

public def KeyDet (table : CuckooHashing K V m h1 h2) : Prop :=
  ∀ (key : K) (v₁ v₂ : V), Stored table key v₁ → Stored table key v₂ → v₁ = v₂
Uses 2 · Used by 6
Statement usesCuckoo hash table · Binding stored in a cuckoo hash table
Used byThe empty cuckoo hash table is key-deterministic · Cuckoo insertion preserves key determinism · Cuckoo lookup finds exactly the stored bindings · Cuckoo lookup finds every stored binding · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged

TheoremThe empty cuckoo hash table satisfies the placement invariant#✓fully proved

For any hash functions \(h_1, h_2\) into \(m\) slots, the empty cuckoo hash table, with every slot of both tables vacant, satisfies the placement invariant.

public theorem valid_empty : Valid (empty : CuckooHashing K V m h1 h2)
Uses 3
Statement usesPlacement invariant of a cuckoo hash table · Empty cuckoo hash table
Proof usesCuckoo hash table

TheoremThe empty cuckoo hash table is key-deterministic#✓fully proved

No key is stored with two different values in the empty cuckoo hash table, vacuously.

public theorem keyDet_empty : KeyDet (empty : CuckooHashing K V m h1 h2)
Uses 4
Statement usesKey determinism of a cuckoo hash table · Empty cuckoo hash table
Proof usesCuckoo hash table · Binding stored in a cuckoo hash table

DefinitionCuckoo eviction loop#✓fully proved

The eviction loop takes a cuckoo hash table with hash functions \(h_1\) and \(h_2\), a key–value pair \((k, v)\), a choice of the first or second table, and a natural number as fuel, and either returns a table or fails. With fuel \(0\) it fails. With fuel \(n + 1\) and the first table chosen, it writes \((k, v)\) into slot \(h_1(k)\) of the first table; if that slot was empty it returns the resulting table, and otherwise it repeats on the resulting table with the evicted pair, the second table and fuel \(n\). With the second table chosen it does the same at slot \(h_2(k)\) of the second table and continues with the first table.

Cslib.Algorithms.Lean.CuckooHashing.insertAux · 20 lines 
def insertAux (table : CuckooHashing K V m h1 h2) (cur : K × V) (first : Bool) :
    Nat → Option (CuckooHashing K V m h1 h2)
  | 0 => none
  | fuel + 1 =>
      if first then
        match table.table1.get (h1 cur.1) with
        | none =>
            some ⟨table.table1.set (h1 cur.1).val (some cur) (h1 cur.1).isLt, table.table2⟩
        | some occ =>
            insertAux
              ⟨table.table1.set (h1 cur.1).val (some cur) (h1 cur.1).isLt, table.table2⟩
              occ false fuel
      else
        match table.table2.get (h2 cur.1) with
        | none =>
            some ⟨table.table1, table.table2.set (h2 cur.1).val (some cur) (h2 cur.1).isLt⟩
        | some occ =>
            insertAux
              ⟨table.table1, table.table2.set (h2 cur.1).val (some cur) (h2 cur.1).isLt⟩
              occ true fuel
Uses 1 · Used by 6
Statement usesCuckoo hash table
Used byCuckoo hash insertion · Cuckoo insertion preserves key determinism · Cuckoo lookup returns an inserted value · Cuckoo insertion stores the inserted binding · Cuckoo insertion preserves the bindings of other keys · Cuckoo insertion preserves the placement invariant

DefinitionCuckoo hash table lookup#✓fully proved

For a cuckoo hash table \(T\) with hash functions \(h_1\) and \(h_2\) and a key \(k\), the lookup of \(k\) in \(T\) returns \(v\) if slot \(h_1(k)\) of the first table holds a pair \((k, v)\); otherwise it returns \(v\) if slot \(h_2(k)\) of the second table holds a pair \((k, v)\); otherwise it returns nothing. No other slot is examined.

public def lookup (table : CuckooHashing K V m h1 h2) (key : K) : Option V :=
  match table.table1.get (h1 key) with
  | some (k₁, v₁) =>
      if k₁ = key then some v₁
      else
        match table.table2.get (h2 key) with
        | some (k₂, v₂) => if k₂ = key then some v₂ else none
        | none => none
  | none =>
      match table.table2.get (h2 key) with
      | some (k₂, v₂) => if k₂ = key then some v₂ else none
      | none => none
Uses 1 · Used by 9
Statement usesCuckoo hash table
Used byLookup in the empty cuckoo hash table · Cuckoo lookup finds exactly the stored bindings · Cuckoo lookup finds every stored binding · Cuckoo lookup finds a key in its first-table slot · Cuckoo lookup finds a key in its second-table slot · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged · Cuckoo lookup finds every stored key · Soundness of cuckoo lookup

TheoremLookup in the empty cuckoo hash table#✓fully proved

Looking up any key in the empty cuckoo hash table finds no value.

@[simp]
public theorem lookup_empty (key : K) :
    lookup (empty : CuckooHashing K V m h1 h2) key = none
Uses 3
Statement usesEmpty cuckoo hash table · Cuckoo hash table lookup
Proof usesCuckoo hash table

TheoremCuckoo lookup finds a key in its first-table slot#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\), let \(k\) be a key and \(v\) a value. If slot \(h_1(k)\) of the first table of \(T\) holds the pair \((k, v)\), then looking up \(k\) in \(T\) returns \(v\).

public theorem lookup_eq_some_of_table1 (table : CuckooHashing K V m h1 h2) (key : K)
    (value : V) (atSlot : table.table1.get (h1 key) = some (key, value)) :
    lookup table key = some value
Uses 2 · Used by 3
Statement usesCuckoo hash table · Cuckoo hash table lookup
Used byCuckoo lookup finds every stored binding · Cuckoo lookup returns an inserted value · Cuckoo lookup finds every stored key

TheoremCuckoo lookup finds a key in its second-table slot#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\), let \(k\) be a key and \(v\) a value. If slot \(h_2(k)\) of the second table of \(T\) holds the pair \((k, v)\) and slot \(h_1(k)\) of the first table of \(T\) holds no pair whose key is \(k\), then looking up \(k\) in \(T\) returns \(v\).

public theorem lookup_eq_some_of_table2 (table : CuckooHashing K V m h1 h2) (key : K)
    (value : V) (atSlot : table.table2.get (h2 key) = some (key, value))
    (notFirst : ∀ v₁, table.table1.get (h1 key) ≠ some (key, v₁)) :
    lookup table key = some value
Uses 2 · Used by 3
Statement usesCuckoo hash table · Cuckoo hash table lookup
Used byCuckoo lookup finds every stored binding · Cuckoo lookup returns an inserted value · Cuckoo lookup finds every stored key

TheoremSoundness of cuckoo lookup#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\), let \(k\) be a key and \(v\) a value. If looking up \(k\) in \(T\) returns \(v\), then the binding \(k \mapsto v\) is stored in some slot of the first or the second table of \(T\).

public theorem lookup_sound (table : CuckooHashing K V m h1 h2) (key : K) (value : V)
    (found : lookup table key = some value) : Stored table key value
Uses 3 · Used by 2
Statement usesCuckoo hash table · Binding stored in a cuckoo hash table · Cuckoo hash table lookup
Used byCuckoo lookup finds exactly the stored bindings · Cuckoo insertion leaves lookups of other keys unchanged

TheoremCuckoo lookup finds every stored key#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\) that satisfies the placement invariant, and let \(k\) be a key and \(v\) a value. If the binding \(k \mapsto v\) is stored in some slot of either table of \(T\), then looking up \(k\) in \(T\) returns some value.

The returned value may differ from \(v\) when \(k\) is stored with two different values; when \(T\) stores each key with at most one value, it is \(v\).

public theorem lookup_isSome_of_stored (table : CuckooHashing K V m h1 h2)
    (valid : Valid table) (key : K) (value : V) (stored : Stored table key value) :
    (lookup table key).isSome
Uses 6
Statement usesCuckoo hash table · Binding stored in a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash table lookup
Proof usesCuckoo lookup finds a key in its first-table slot · Cuckoo lookup finds a key in its second-table slot

TheoremCuckoo lookup finds every stored binding#✓fully proved

Let \(T\) be a cuckoo hash table that satisfies the placement invariant and is key-deterministic. For every key \(k\) and value \(v\), if the binding \(k \mapsto v\) is stored in \(T\), then looking up \(k\) in \(T\) returns \(v\).

public theorem lookup_eq_some_of_stored (table : CuckooHashing K V m h1 h2)
    (valid : Valid table) (det : KeyDet table) (key : K) (value : V)
    (stored : Stored table key value) :
    lookup table key = some value
Uses 7 · Used by 3
Statement usesCuckoo hash table · Key determinism of a cuckoo hash table · Binding stored in a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash table lookup
Proof usesCuckoo lookup finds a key in its first-table slot · Cuckoo lookup finds a key in its second-table slot
Used byCuckoo lookup finds exactly the stored bindings · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged

TheoremCuckoo lookup finds exactly the stored bindings#✓fully proved

Let \(T\) be a cuckoo hash table that satisfies the placement invariant and is key-deterministic. For every key \(k\) and value \(v\), looking up \(k\) in \(T\) returns \(v\) if and only if the binding \(k \mapsto v\) is stored in \(T\).

public theorem lookup_eq_some_iff_stored (table : CuckooHashing K V m h1 h2)
    (valid : Valid table) (det : KeyDet table) (key : K) (value : V) :
    lookup table key = some value ↔ Stored table key value
Uses 7
Statement usesCuckoo hash table · Key determinism of a cuckoo hash table · Binding stored in a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash table lookup
Proof usesCuckoo lookup finds every stored binding · Soundness of cuckoo lookup

DefinitionSlot holds a key#✓fully proved

A slot of a cuckoo hash table is either empty or holds a pair \((k, v)\) of a key and a value. For a slot \(s\) and a key \(k'\), this test is true when \(s\) holds a pair whose key is \(k'\), and false when \(s\) is empty or holds a pair with a different key.

def slotHasKey (slot : Option (K × V)) (key : K) : Bool :=
  match slot with
  | some pair => decide (pair.1 = key)
  | none => false
Used by 6
Used byCuckoo hash insertion · Cuckoo insertion preserves key determinism · Cuckoo lookup returns an inserted value · Cuckoo insertion stores the inserted binding · Cuckoo insertion preserves the bindings of other keys · Cuckoo insertion preserves the placement invariant

DefinitionCuckoo hash insertion#✓fully proved

Inserting a key \(k\) with value \(v\) into a cuckoo hash table with hash functions \(h_1\) and \(h_2\), with fuel \(n\), either returns a table or fails. If slot \(h_1(k)\) of the first table holds a binding for \(k\), that slot is overwritten with \((k, v)\), and slot \(h_2(k)\) of the second table is cleared if it also holds a binding for \(k\), so no stale competing value remains. Otherwise, if slot \(h_2(k)\) of the second table holds a binding for \(k\), that slot is overwritten with \((k, v)\). Otherwise the eviction loop runs on \((k, v)\), starting with the first table, with fuel \(n\), and its result is returned. Failure, when the loop exhausts its fuel, models the rehash trigger of the classical algorithm.

public def insert (table : CuckooHashing K V m h1 h2) (key : K) (value : V) (fuel : Nat) :
    Option (CuckooHashing K V m h1 h2) :=
  if slotHasKey (table.table1.get (h1 key)) key then
    some ⟨table.table1.set (h1 key).val (some (key, value)) (h1 key).isLt,
      if slotHasKey (table.table2.get (h2 key)) key then
        table.table2.set (h2 key).val none (h2 key).isLt
      else table.table2⟩
  else if slotHasKey (table.table2.get (h2 key)) key then
    some ⟨table.table1, table.table2.set (h2 key).val (some (key, value)) (h2 key).isLt⟩
  else
    insertAux table (key, value) true fuel
Uses 3 · Used by 6
Statement usesCuckoo hash table · Cuckoo eviction loop · Slot holds a key
Used byCuckoo insertion preserves key determinism · Cuckoo lookup returns an inserted value · Cuckoo insertion leaves lookups of other keys unchanged · Cuckoo insertion stores the inserted binding · Cuckoo insertion preserves the bindings of other keys · Cuckoo insertion preserves the placement invariant

TheoremCuckoo insertion stores the inserted binding#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\). If inserting (or replacing) the binding \(k \mapsto v\) in \(T\) with fuel \(f\) succeeds and returns the table \(T'\), then the binding \(k \mapsto v\) is stored in some slot of either table of \(T'\).

public theorem stored_insert (table : CuckooHashing K V m h1 h2) (key : K) (value : V)
    (fuel : Nat) (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated) :
    Stored updated key value
Uses 5
Statement usesCuckoo hash table · Binding stored in a cuckoo hash table · Cuckoo hash insertion
Proof usesCuckoo eviction loop · Slot holds a key

TheoremCuckoo insertion preserves the placement invariant#✓fully proved

Let \(T\) be a cuckoo hash table that satisfies the placement invariant. If inserting the binding \(k \mapsto v\) into \(T\) (which replaces an existing binding for \(k\) in place) with some fuel bound succeeds and returns the table \(T'\), then \(T'\) satisfies the placement invariant.

public theorem valid_insert (table : CuckooHashing K V m h1 h2) (key : K) (value : V)
    (fuel : Nat) (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated) (valid : Valid table) :
    Valid updated
Uses 5 · Used by 1
Statement usesCuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash insertion
Proof usesCuckoo eviction loop · Slot holds a key
Used byCuckoo insertion leaves lookups of other keys unchanged

TheoremCuckoo insertion preserves key determinism#✓fully proved

Let \(T\) be a cuckoo hash table that satisfies the placement invariant and is key-deterministic. If inserting a key \(k\) with value \(v\) into \(T\) with some fuel succeeds with result \(T'\), then \(T'\) is key-deterministic. In particular, replacement leaves no stale copy of \(k\) with a different value in the other slot.

public theorem keyDet_insert (table : CuckooHashing K V m h1 h2) (key : K) (value : V)
    (fuel : Nat) (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated)
    (valid : Valid table) (det : KeyDet table) :
    KeyDet updated
Uses 7 · Used by 1
Statement usesCuckoo hash table · Key determinism of a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash insertion
Proof usesBinding stored in a cuckoo hash table · Cuckoo eviction loop · Slot holds a key
Used byCuckoo insertion leaves lookups of other keys unchanged

TheoremCuckoo lookup returns an inserted value#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\) that satisfies the placement invariant and stores each key with at most one value. If inserting (or replacing) the binding \(k \mapsto v\) in \(T\) with fuel \(f\) succeeds and returns the table \(T'\), then looking up \(k\) in \(T'\) returns \(v\).

public theorem lookup_insert (table : CuckooHashing K V m h1 h2) (valid : Valid table)
    (det : KeyDet table) (key : K) (value : V) (fuel : Nat)
    (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated) :
    lookup updated key = some value
Uses 11
Statement usesCuckoo hash table · Key determinism of a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash insertion · Cuckoo hash table lookup
Proof usesBinding stored in a cuckoo hash table · Cuckoo eviction loop · Cuckoo lookup finds every stored binding · Cuckoo lookup finds a key in its first-table slot · Cuckoo lookup finds a key in its second-table slot · Slot holds a key

TheoremCuckoo insertion preserves the bindings of other keys#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\) that satisfies the placement invariant. Suppose inserting (or replacing) the binding \(k \mapsto v\) in \(T\) with fuel \(f\) succeeds and returns the table \(T'\). Then for every key \(k' \ne k\) and every value \(v'\), the binding \(k' \mapsto v'\) is stored in \(T'\) if and only if it is stored in \(T\).

public theorem stored_insert_iff_of_ne (table : CuckooHashing K V m h1 h2)
    (valid : Valid table) (key : K) (value : V) (fuel : Nat)
    (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated)
    {other : K} {otherValue : V} (different : other ≠ key) :
    Stored updated other otherValue ↔ Stored table other otherValue
Uses 6 · Used by 1
Statement usesCuckoo hash table · Binding stored in a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash insertion
Proof usesCuckoo eviction loop · Slot holds a key
Used byCuckoo insertion leaves lookups of other keys unchanged

TheoremCuckoo insertion leaves lookups of other keys unchanged#✓fully proved

Let \(T\) be a cuckoo hash table with hash functions \(h_1\) and \(h_2\) that satisfies the placement invariant and stores each key with at most one value. If inserting (or replacing) the binding \(k \mapsto v\) in \(T\) with fuel \(f\) succeeds and returns the table \(T'\), then for every key \(k' \ne k\), looking up \(k'\) in \(T'\) gives the same result as looking up \(k'\) in \(T\): either both return nothing or both return the same value.

public theorem lookup_insert_of_ne (table : CuckooHashing K V m h1 h2)
    (valid : Valid table) (det : KeyDet table) (key : K) (value : V)
    (fuel : Nat) (updated : CuckooHashing K V m h1 h2)
    (inserted : insert table key value fuel = some updated)
    {other : K} (different : other ≠ key) :
    lookup updated other = lookup table other
Uses 11
Statement usesCuckoo hash table · Key determinism of a cuckoo hash table · Placement invariant of a cuckoo hash table · Cuckoo hash insertion · Cuckoo hash table lookup
Proof usesBinding stored in a cuckoo hash table · Cuckoo insertion preserves key determinism · Cuckoo lookup finds every stored binding · Soundness of cuckoo lookup · Cuckoo insertion preserves the bindings of other keys · Cuckoo insertion preserves the placement invariant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.