Certifying Certainty and Uncertainty in Approximate Membership Query Structures -- Extended Version

TL;DR

This paper introduces a formal framework and Coq library for rigorously verifying the probabilistic properties of approximate membership query structures, ensuring correctness and automating proofs of false positive and negative guarantees.

Contribution

It provides a systematic decomposition framework and a Coq-based library for mechanising proofs of AMQ properties, including complex structures like Bloom filters and quotient filters.

Findings

Verified probabilistic guarantees for various AMQs

Automated proof tactics for probabilistic properties

Framework ensures absence of false negatives by construction

Abstract

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.