package coq-ceramist

Ceramist extends coq-infotheo to support reasoning about probabilistic algorithms, and includes a collection of lemmas on random oracle based hash functions.

Provides an example implementation of a bloom filter and uses the library to prove the probability of a false positive.