  Approximate Membership Query structures (AMQs) rely on randomisation for
time- and space-efficiency, while introducing a possibility of false positive
and false negative answers. Correctness proofs of such structures involve
subtle reasoning about bounds on probabilities of getting certain outcomes.
Because of these subtleties, a number of unsound arguments in such proofs have
been made over the years. In this work, we address the challenge of building
rigorous and reusable computer-assisted proofs about probabilistic
specifications of AMQs. We describe the framework for systematic decomposition
of AMQs and their properties into a series of interfaces and reusable
components. We implement our framework as a library in the Coq proof assistant
and showcase it by encoding in it a number of non-trivial AMQs, such as Bloom
filters, counting filters, quotient filters and blocked constructions, and
mechanising the proofs of their probabilistic specifications. We demonstrate
how AMQs encoded in our framework guarantee the absence of false negatives by
construction. We also show how the proofs about probabilities of false
positives for complex AMQs can be obtained by means of verified reduction to
the implementations of their simpler counterparts. Finally, we provide a
library of domain-specific theorems and tactics that allow a high degree of
automation in probabilistic proofs.
