Certifying Certainty and Uncertainty in Approximate Membership Query Structures -- Extended Version
Kiran Gopinathan, Ilya Sergey

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCaching and Content Delivery · Advanced Database Systems and Queries · Network Packet Processing and Optimization
