Open addressing

23 fully proved

Open Addressing

StructureOpen-addressing hash table#✓fully proved

Let \(K\) be a type of keys, \(V\) a type of values, \(m\) a natural number, and \(p\) a probe sequence assigning to each key \(k\) and each \(i \in \mathbb{N}\) a slot \(p(k, i) \in \{0, \dots, m - 1\}\). An open-addressing hash table with \(m\) slots and probe sequence \(p\) consists of \(m\) slots, each either empty or holding a single pair \((k, v)\) with \(k \in K\) and \(v \in V\).

No expected constant-time bound is claimed because the model supplies neither a probability distribution nor a uniform-hashing assumption about the probe sequence.

public structure OpenAddressing (K : Type u) (V : Type v) (m : Nat)
    (probe : K → Nat → Fin m) where
  /-- The `m` slots, each empty or holding one key-value pair. -/
  slots : Vector (Option (K × V)) m

Used by 20

Used byEmpty open-addressing table · Insertion into an open-addressing table · Bounded insertion scan · Lookup in an open-addressing table · Bounded lookup scan · Lookup in the empty open-addressing table · Lookup of an absent key fails · Lookup in a valid table returns exactly the stored binding · Lookup after a successful open-addressing insertion · Insertion does not affect lookups of other keys · Open-addressing lookup succeeds exactly on stored keys · Valid open-addressing tables find every stored key · Failed open-addressing insertion finds every probed slot taken · Stored binding in an open-addressing table · Open-addressing insertion leaves other keys' bindings unchanged · Open-addressing lookup returns only stored bindings · Bindings in a valid open-addressing table are unique · Valid open-addressing tables · The empty open-addressing table is valid · Insertion preserves validity of an open-addressing table

DefinitionLinear-probing probe sequence#✓fully proved

Given a hash function \(h : K \to \mathbb{N}\) and a number of slots \(m > 0\), the \(i\)-th probe of a key \(k\) is the slot \((h(k) + i) \bmod m\) in \(\{0, \dots, m - 1\}\).

public def linearProbe {K : Type u} (hash : K → Nat) (m : Nat) (hm : 0 < m) :
    K → Nat → Fin m :=
  fun k i => ⟨(hash k + i) % m, Nat.mod_lt _ hm⟩

DefinitionDouble-hashing probe sequence#✓fully proved

Given hash functions \(h_1, h_2 : K \to \mathbb{N}\) and a number of slots \(m > 0\), the \(i\)-th probe of a key \(k\) is the slot \((h_1(k) + i \cdot h_2(k)) \bmod m\) in \(\{0, \dots, m - 1\}\).

public def doubleHashProbe {K : Type u} (hash1 hash2 : K → Nat) (m : Nat)
    (hm : 0 < m) : K → Nat → Fin m :=
  fun k i => ⟨(hash1 k + i * hash2 k) % m, Nat.mod_lt _ hm⟩

DefinitionEmpty open-addressing table#✓fully proved

The open-addressing table with \(m\) slots and a given probe sequence in which every slot is empty.

public def empty : OpenAddressing K V m probe :=
  ⟨Vector.replicate m none⟩

Uses 1 · Used by 2

Statement usesOpen-addressing hash table

Used byLookup in the empty open-addressing table · The empty open-addressing table is valid

DefinitionBounded lookup scan#✓fully proved

Given a table with \(m\) slots and probe sequence \(p\), a key \(k\), a starting index \(s\) and a budget \(f\) of probes, examine the slots \(p(k, s), p(k, s + 1), \dots\) in order, for at most \(f\) probes. The scan returns the value bound to \(k\) in the first examined slot that holds a binding for \(k\), and returns no value if it first reaches an empty slot or exhausts the budget.

This is the helper behind lookup, which starts at index \(0\) with budget \(m\).

def lookupAux (table : OpenAddressing K V m probe) (key : K) (start : Nat) :
    Nat → Option V
  | 0 => none
  | fuel + 1 =>
      match table.slots.get (probe key start) with
      | none => none
      | some (k', value) =>
          if k' = key then some value else lookupAux table key (start + 1) fuel

Uses 1 · Used by 5

Statement usesOpen-addressing hash table

Used byLookup in an open-addressing table · Lookup in the empty open-addressing table · Lookup after a successful open-addressing insertion · Valid open-addressing tables find every stored key · Open-addressing lookup returns only stored bindings

DefinitionLookup in an open-addressing table#✓fully proved

Let \(T\) be an open-addressing hash table with \(m\) slots and probe sequence \(p\), and let \(k\) be a key. The lookup of \(k\) in \(T\) inspects the slots \(p(k, 0), p(k, 1), \dots, p(k, m - 1)\) in this order. It returns the value \(v\) of the first inspected slot that holds a pair \((k, v)\), and returns nothing if an empty slot is inspected first or if none of the \(m\) inspected slots holds the key \(k\).

public def lookup (table : OpenAddressing K V m probe) (key : K) : Option V :=
  lookupAux table key 0 m

Uses 2 · Used by 8

Statement usesOpen-addressing hash table · Bounded lookup scan

Used byLookup in the empty open-addressing table · Lookup of an absent key fails · Lookup in a valid table returns exactly the stored binding · Lookup after a successful open-addressing insertion · Insertion does not affect lookups of other keys · Open-addressing lookup succeeds exactly on stored keys · Valid open-addressing tables find every stored key · Open-addressing lookup returns only stored bindings

DefinitionBounded insertion scan#✓fully proved

Given a table with \(m\) slots and probe sequence \(p\), a key \(k\), a value \(v\), a starting index \(s\) and a budget \(f\) of probes, examine the slots \(p(k, s), p(k, s + 1), \dots\) in order, for at most \(f\) probes. At the first examined slot that is empty or holds a binding for \(k\), the scan returns the table with that slot overwritten by the binding \(k \mapsto v\) and every other slot unchanged; if all \(f\) examined slots hold bindings for other keys (in particular if \(f = 0\)), it fails and returns no table.

This is the helper behind insertion, which starts at index \(0\) with budget \(m\).

def insertAux (table : OpenAddressing K V m probe) (key : K) (value : V)
    (start : Nat) : Nat → Option (OpenAddressing K V m probe)
  | 0 => none
  | fuel + 1 =>
      match table.slots.get (probe key start) with
      | none =>
          some ⟨table.slots.set (probe key start).val (some (key, value))
            (probe key start).isLt⟩
      | some (k', _) =>
          if k' = key then
            some ⟨table.slots.set (probe key start).val (some (key, value))
              (probe key start).isLt⟩
          else
            insertAux table key value (start + 1) fuel

Uses 1 · Used by 5

Statement usesOpen-addressing hash table

Used byInsertion into an open-addressing table · Lookup after a successful open-addressing insertion · Failed open-addressing insertion finds every probed slot taken · Open-addressing insertion leaves other keys' bindings unchanged · Insertion preserves validity of an open-addressing table

DefinitionInsertion into an open-addressing table#✓fully proved

To insert the binding \(k \mapsto v\) into a table with \(m\) slots and probe sequence \(p\), examine the slots \(p(k, 0), p(k, 1), \dots, p(k, m - 1)\) in order. At the first one that is empty or already holds a binding for \(k\), write \(k \mapsto v\) there, leaving every other slot unchanged, and return the updated table. If all \(m\) examined slots hold bindings for other keys, the insertion fails and returns no table.

public def insert (table : OpenAddressing K V m probe) (key : K) (value : V) :
    Option (OpenAddressing K V m probe) :=
  insertAux table key value 0 m

Uses 2 · Used by 5

Statement usesOpen-addressing hash table · Bounded insertion scan

Used byLookup after a successful open-addressing insertion · Insertion does not affect lookups of other keys · Failed open-addressing insertion finds every probed slot taken · Open-addressing insertion leaves other keys' bindings unchanged · Insertion preserves validity of an open-addressing table

DefinitionValid open-addressing tables#✓fully proved

Let \(T\) be an open-addressing table with \(m\) slots and probe sequence \(p\), where \(p(k, i) \in \{0, \dots, m - 1\}\) is the slot visited by the \(i\)-th probe of key \(k\). Then \(T\) is valid when it satisfies two conditions. Probe-closedness: whenever slot \(j\) holds a binding \(k \mapsto v\), there is an \(i < m\) with \(p(k, i) = j\) such that the slots \(p(k, i')\) are occupied for all \(i' < i\); this is what lets a lookup stop at the first empty slot. Key uniqueness: if slots \(j_1\) and \(j_2\) hold bindings with the same key \(k\), then \(j_1 = j_2\); so each key has at most one binding and insertion genuinely replaces it.

public def Valid (table : OpenAddressing K V m probe) : Prop :=
  (∀ (j : Fin m) (key : K) (value : V), table.slots.get j = some (key, value) →
    ∃ i < m, probe key i = j ∧
      ∀ i' < i, (table.slots.get (probe key i')).isSome) ∧
  (∀ (j₁ j₂ : Fin m) (key : K) (value₁ value₂ : V),
    table.slots.get j₁ = some (key, value₁) →
    table.slots.get j₂ = some (key, value₂) → j₁ = j₂)

Uses 1 · Used by 7

Statement usesOpen-addressing hash table

Used byLookup in a valid table returns exactly the stored binding · Insertion does not affect lookups of other keys · Open-addressing lookup succeeds exactly on stored keys · Valid open-addressing tables find every stored key · Bindings in a valid open-addressing table are unique · The empty open-addressing table is valid · Insertion preserves validity of an open-addressing table

DefinitionStored binding in an open-addressing table#✓fully proved

An open-addressing hash table \(T\) stores the binding \(k \mapsto v\) when some slot of \(T\) holds the pair \((k, v)\).

public def Stored (table : OpenAddressing K V m probe) (key : K) (value : V) :
    Prop :=
  ∃ j : Fin m, table.slots.get j = some (key, value)

Uses 1 · Used by 8

Statement usesOpen-addressing hash table

Used byLookup of an absent key fails · Lookup in a valid table returns exactly the stored binding · Insertion does not affect lookups of other keys · Open-addressing lookup succeeds exactly on stored keys · Valid open-addressing tables find every stored key · Open-addressing insertion leaves other keys' bindings unchanged · Open-addressing lookup returns only stored bindings · Bindings in a valid open-addressing table are unique

TheoremThe empty open-addressing table is valid#✓fully proved

For all types \(K\) and \(V\), every number of slots \(m\) and every probe sequence \(p\), which assigns to each key \(k\) and each \(i \in \mathbb{N}\) a slot \(p(k, i) \in \{0, \dots, m - 1\}\), the empty table with \(m\) slots and probe sequence \(p\), in which every slot is vacant, is valid: it is probe-closed and no key is stored in two different slots.

public theorem valid_empty :
    Valid (empty : OpenAddressing K V m probe)

Uses 3

Statement usesValid open-addressing tables · Empty open-addressing table

Proof usesOpen-addressing hash table

TheoremLookup in the empty open-addressing table#✓fully proved

For every key \(k\), looking up \(k\) in the empty open-addressing table returns no value.

@[simp]
public theorem lookup_empty (key : K) :
    lookup (empty : OpenAddressing K V m probe) key = none

Uses 4

Statement usesEmpty open-addressing table · Lookup in an open-addressing table

Proof usesOpen-addressing hash table · Bounded lookup scan

TheoremLookup after a successful open-addressing insertion#✓fully proved

If inserting the binding \(k \mapsto v\) into an open-addressing hash table \(T\) succeeds and yields the table \(T'\), then looking up \(k\) in \(T'\) returns \(v\). No validity assumption on \(T\) is needed.

public theorem lookup_insert (table : OpenAddressing K V m probe) (key : K)
    (value : V) (updated : OpenAddressing K V m probe)
    (inserted : insert table key value = some updated) :
    lookup updated key = some value

Uses 5

Statement usesOpen-addressing hash table · Insertion into an open-addressing table · Lookup in an open-addressing table

Proof usesBounded insertion scan · Bounded lookup scan

TheoremInsertion preserves validity of an open-addressing table#✓fully proved

Let \(T\) be a valid table with \(m\) slots and probe sequence \(p\), whose keys have decidable equality. If inserting the binding \(k \mapsto v\) into \(T\) (adding it, or replacing the binding already stored for \(k\)) succeeds and returns the table \(T'\), then \(T'\) is valid: it is probe-closed and no key is stored in two different slots.

public theorem valid_insert (table : OpenAddressing K V m probe) (key : K)
    (value : V) (updated : OpenAddressing K V m probe) (valid : Valid table)
    (inserted : insert table key value = some updated) :
    Valid updated

Uses 4 · Used by 1

Statement usesOpen-addressing hash table · Valid open-addressing tables · Insertion into an open-addressing table

Proof usesBounded insertion scan

Used byInsertion does not affect lookups of other keys

TheoremOpen-addressing lookup returns only stored bindings#✓fully proved

If looking up a key \(k\) in an open-addressing hash table \(T\) returns the value \(v\), then \(T\) stores the binding \(k \mapsto v\). No validity assumption is needed.

public theorem stored_of_lookup_eq_some (table : OpenAddressing K V m probe)
    (key : K) (value : V) (found : lookup table key = some value) :
    Stored table key value

Uses 4 · Used by 4

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Lookup in an open-addressing table

Proof usesBounded lookup scan

Used byLookup of an absent key fails · Lookup in a valid table returns exactly the stored binding · Insertion does not affect lookups of other keys · Open-addressing lookup succeeds exactly on stored keys

TheoremLookup of an absent key fails#✓fully proved

Let \(T\) be an open-addressing table and \(k\) a key such that no slot of \(T\) stores a binding \(k \mapsto v\) for any value \(v\). Then looking up \(k\) in \(T\) returns no value. No validity assumption on \(T\) is needed.

public theorem lookup_eq_none_of_not_stored (table : OpenAddressing K V m probe)
    (key : K) (absent : ∀ value : V, ¬ Stored table key value) :
    lookup table key = none

Uses 4 · Used by 1

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Lookup in an open-addressing table

Proof usesOpen-addressing lookup returns only stored bindings

Used byInsertion does not affect lookups of other keys

TheoremValid open-addressing tables find every stored key#✓fully proved

If a valid open-addressing hash table \(T\) stores the binding \(k \mapsto v\), then looking up \(k\) in \(T\) returns some value.

public theorem lookup_isSome_of_stored (table : OpenAddressing K V m probe)
    (key : K) (value : V) (valid : Valid table)
    (stored : Stored table key value) :
    (lookup table key).isSome

Uses 5 · Used by 2

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Valid open-addressing tables · Lookup in an open-addressing table

Proof usesBounded lookup scan

Used byLookup in a valid table returns exactly the stored binding · Open-addressing lookup succeeds exactly on stored keys

TheoremOpen-addressing lookup succeeds exactly on stored keys#✓fully proved

Let \(T\) be a valid open-addressing hash table and \(k\) a key. Looking up \(k\) in \(T\) returns a value if and only if \(T\) stores a binding \(k \mapsto v\) for some value \(v\).

This membership characterization is used in place of a finite-map abstraction of the table.

public theorem lookup_isSome_iff (table : OpenAddressing K V m probe) (key : K)
    (valid : Valid table) :
    (lookup table key).isSome ↔ ∃ value : V, Stored table key value

Uses 6

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Valid open-addressing tables · Lookup in an open-addressing table

Proof usesValid open-addressing tables find every stored key · Open-addressing lookup returns only stored bindings

TheoremBindings in a valid open-addressing table are unique#✓fully proved

If a valid open-addressing hash table \(T\) stores both \(k \mapsto v_1\) and \(k \mapsto v_2\), then \(v_1 = v_2\).

public theorem stored_unique (table : OpenAddressing K V m probe)
    (valid : Valid table) {key : K} {value₁ value₂ : V}
    (stored₁ : Stored table key value₁) (stored₂ : Stored table key value₂) :
    value₁ = value₂

Uses 3 · Used by 1

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Valid open-addressing tables

Used byLookup in a valid table returns exactly the stored binding

TheoremLookup in a valid table returns exactly the stored binding#✓fully proved

Let \(T\) be a valid open-addressing table, \(k\) a key and \(v\) a value. Then looking up \(k\) in \(T\) returns \(v\) if and only if the binding \(k \mapsto v\) is stored in some slot of \(T\).

Together with the fact that lookup after a successful insertion of \(k \mapsto v\) returns \(v\), this says that a successful insertion really replaces the old binding: no other value for \(k\) remains stored afterwards.

public theorem lookup_eq_some_iff (table : OpenAddressing K V m probe)
    (key : K) (value : V) (valid : Valid table) :
    lookup table key = some value ↔ Stored table key value

Uses 7 · Used by 1

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Valid open-addressing tables · Lookup in an open-addressing table

Proof usesValid open-addressing tables find every stored key · Open-addressing lookup returns only stored bindings · Bindings in a valid open-addressing table are unique

Used byInsertion does not affect lookups of other keys

TheoremOpen-addressing insertion leaves other keys' bindings unchanged#✓fully proved

Let \(T\) be an open-addressing hash table, and suppose that inserting the binding \(k \mapsto v\) into \(T\) succeeds and yields the table \(T'\). Then for every key \(k' \neq k\) and every value \(v'\), the table \(T'\) stores \(k' \mapsto v'\) if and only if \(T\) stores \(k' \mapsto v'\).

No validity assumption is needed: the insertion writes a single slot, previously empty or previously holding \(k\), and leaves every other slot unchanged.

public theorem stored_insert_of_ne (table : OpenAddressing K V m probe) (key : K)
    (value : V) (updated : OpenAddressing K V m probe)
    (inserted : insert table key value = some updated) {other : K}
    (different : other ≠ key) {otherValue : V} :
    Stored updated other otherValue ↔ Stored table other otherValue

Uses 4 · Used by 1

Statement usesOpen-addressing hash table · Stored binding in an open-addressing table · Insertion into an open-addressing table

Proof usesBounded insertion scan

Used byInsertion does not affect lookups of other keys

TheoremInsertion does not affect lookups of other keys#✓fully proved

Let \(T\) be a valid open-addressing table and suppose inserting the binding \(k \mapsto v\) into \(T\) succeeds with result \(T'\). Then for every key \(k' \ne k\), looking up \(k'\) in \(T'\) gives the same result as looking up \(k'\) in \(T\).

Together with the fact that looking up \(k\) in \(T'\) returns \(v\), this is the map-update specification of insertion, matching the corresponding statement for separate chaining.

public theorem lookup_insert_of_ne (table : OpenAddressing K V m probe) (key : K)
    (value : V) (updated : OpenAddressing K V m probe) (valid : Valid table)
    (inserted : insert table key value = some updated) {other : K}
    (different : other ≠ key) :
    lookup updated other = lookup table other

Uses 10

Statement usesOpen-addressing hash table · Valid open-addressing tables · Insertion into an open-addressing table · Lookup in an open-addressing table

Proof usesStored binding in an open-addressing table · Lookup of an absent key fails · Lookup in a valid table returns exactly the stored binding · Open-addressing insertion leaves other keys' bindings unchanged · Open-addressing lookup returns only stored bindings · Insertion preserves validity of an open-addressing table

TheoremFailed open-addressing insertion finds every probed slot taken#✓fully proved

Let \(T\) be an open-addressing hash table with \(m\) slots and probe sequence \(p\). If inserting a binding \(k \mapsto v\) into \(T\) fails, then for every \(i < m\) the slot \(p(k, i)\) holds a pair \((k', v')\) with \(k' \neq k\).

For probe sequences that are permutations of the slots, this says that every slot of the table holds a key other than \(k\).

public theorem occupied_of_insert_eq_none (table : OpenAddressing K V m probe)
    (key : K) (value : V) (failed : insert table key value = none) :
    ∀ attempts < m, ∃ (otherKey : K) (otherValue : V),
      table.slots.get (probe key attempts) = some (otherKey, otherValue) ∧
        otherKey ≠ key

Uses 3

Statement usesOpen-addressing hash table · Insertion into an open-addressing table

Proof usesBounded insertion scan

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.