Hash Functions

Hash interface

Here we construct an abstract interface for hash functions. This will allow us to work with hashes using a random oracle model, i.e. the first time we hash a key it will return a uniformly sampled value, and subsequent times will return the same value. Note that this is not how real world hashes work, but it is a common model to reason about hash-based data structures and algorithms. One can actually implement a data structure that behaves like this by using a map/dictionary whose values are sampled at random, but for the purpose of this tutorial we will work with the abstract interface. At the code level, the hash will be accessed through a function f, which is a value. Our logical view of the hash function will be given by a partial map m from keys to values.

Operations

Predicates

The hashfun predicate connects the code level function f with its abstract representation m. Here val_size is a bound on the codomain of the hash, i.e., the hash should return values in 0,...,val_size

Properties

All values must be within 0,...,val_size

Specifications

The key spec for working with hash functions is below. Here we are hashing a fresh key k, and we want its value v to fall outside of a set avoid. Instead of directly specifying that v∉avoid, we will distribute our current error budget ↯ε depending on whether v falls inside or outside avoid, giving ↯εI to the former and ↯εO to the latter. Since we assume that values for the hash are distributed uniformly, we will impose the condition (εI * size avoid + εO * (val_size + 1 - size avoid) <= ε * (val_size + 1)) Note that: (1) The probability of falling in avoid is (size avoid / (val_size + 1)) (2) The probability of falling outside of avoid is (val_size + 1 - size avoid) / (val_size + 1) Therefore the inequality above states that the ε is at least equal or larger to the expected amount of error credits we will have after hashing On returning, we will get a value n, an updated view on the hash, where the partial map now contains the key-value pair (k,n) and an amount of error credits depending on whether n ∈ avoid or n ∉ avoid.

If we are hashing a previously hashed elem, then we simply return its assigned value, which is in the map

Derived lemmas about hash functions

We derive some lemmas that will allow us to work with the hash function. First, one can always query a fresh element without spending error credits, and then one gets no information about the value, besides that it is within range

Second, if one has enough error credits, one can avoid hashing a fresh element into a value in the avoid set

The key to this proof is the following step, where we assign ↯ 1 to the case where we sample an index in avoid and ↯ 0 otherwise.

We can actually get rid of the hypothesis (∀ x, x ∈ avoid → x < S val_size) This is used to ensure we have the right multiplier for credits whenever we fall outside of the avoid set, but since we are giving 0 credits to that case it does not matter

We first compute the intersection of avoid with with 0,...,val_size to obtain a new set avoid' satisfying the premise of hash_query_spec_fresh_avoid_aux

The rest of the proof is mostly simple reasoning about sets

An example program

As a first use of our hash specifications, we will consider a simple example, where initialize a hash, hash two different integers, and check that their outputs are different

We first initialize the hash, with size 7 for values

We now hash 1. The map is currently empty, and any result is valid at this point. Therefore, we do not need to spend any amount of error credits

We now hash 2. At this point, we want to avoid a collision with 1, that is, we want the result to not be v1. Since this is a singleton set, and the size of the value space is 8, we can spend ↯(1/8) to avoid it