{{ message }}
/ ceramist Public

Verified hash-based AMQ structures in Coq

# verse-lab/ceramist

Switch branches/tags
Nothing to show

## Files

Failed to load latest commit information.
Type
Name
Commit time

# Ceramist - Verified Hash-based Approximate Membership Structures

## Installation (using Opam)

Create a new switch

opam switch create ceramist 4.09.0
eval $(opam env)  Add coq-released repository to opam: opam repo add coq-released https://coq.inria.fr/opam/released  Install ceramist: opam install coq-ceramist.1.0.1  ## Installation (from Sources) Use opam to install dependencies opam install ./opam  Then build the project: make clean && make  Takes around an hour to build. ## Project Structure The structure of the overall development is as follows: . ├── Computation │ ├── Comp.v │ └── Notationv1.v ├── Structures │ ├── BlockedAMQ │ │ └── BlockedAMQ.v │ ├── BloomFilter │ │ ├── BloomFilter_Definitions.v │ │ └── BloomFilter_Probability.v │ ├── Core │ │ ├── AMQHash.v │ │ ├── AMQReduction.v │ │ ├── AMQ.v │ │ ├── FixedList.v │ │ ├── FixedMap.v │ │ ├── Hash.v │ │ └── HashVec.v │ ├── CountingBloomFilter │ │ ├── CountingBloomFilter_Definitions.v │ │ └── CountingBloomFilter_Probability.v │ └── QuotientFilter │ ├── QuotientFilter_Definitions.v │ └── QuotientFilter_Probability.v └── Utils ├── InvMisc.v ├── rsum_ext.v ├── seq_ext.v ├── seq_subset.v ├── stirling.v └── tactics.v 8 directories, 22 files  The library is split into separate logical components by directory: • Computation - defines a probability monad and associated notation for it on top of the 'coq-infotheo' probability library. • Utils - collection of utility lemmas and tactics used throughout the development • Structures/Core - contains definitions and properties about the core probabilistic primitives exported by the library, and defines the abstract AMQ interface satisfied by all instantiations. • Structures/BloomFilter - example use of the exported library to prove various probabilistic properties on bloom filters. • Structures/CountingBloomFilter - another exemplar use of the library to prove probabilistic properties on counting bloom filters. • Structures/QuotientBloomFilter - exemplar use of library to prove probabilistic properties of quotient filters • Structures/BlockedAMQ - exemplar use of library to prove probabilistic properties of a higher order AMQ - the blockedAMQ Check out Structures/Demo.v for an example instantiation of the BlockedAMQ to derive Blocked Bloom filters, Counting Blocked bloom filters and Blocked Quotient filters. ## Tactics To simplify reasoning about probabilistic computations, we provide a few helper tactics under ProbHash.Utils: • comp_normalize - is a tactic which normalizes probabilistic computations in the goal to a standard form consisting of a nested summation with a summand which is the product of each individual statement: For example, if our goal contains a term of the form: d[ res <-$ hash n v hsh;
x <- fst res;
ret x ] value


applying comp_normalize normalizes it to:

\sum_(i in HashState n)
\sum_(i0 in 'I_Hash_size.+1)
((d[ hash n v hsh]) (i, i0) *R*
((value == i0) %R))


This tactic works by simply recursively descending the computation and expanding the definition of the distribution.

• comp_simplify - is a tactic which effectively applies beta reduction to the normalized form, substituting any ret x (which have been normalized to a factor of the form (x == ...) by the previous tactic) statements into the rest of the computation - applying it to the previous example would result in:

\sum_(i in HashState n)
(d[ hash n v hsh]) (i, value)

• comp_simplify_n n - is a variant of the previous one which applies the reduction a fixed number n of times as sometimes the previous tactic may loop.

• comp_possible_decompose - is a tactic which converts a fact (must be first element of goal) about a possible computation ( d[ c1; c2; ....; cn] v != 0) into a fact about the possibility of the individual statements of the computation forall v1,v2, ..., vn, d[ c1 ] v1 != 0 -> d[ c2] v2 -> .... d[ cn] vn != 0

• comp_possible_exists is a tactic which converts a goal about a computation being possible ( d[ c1; c2; ....; cn] v != 0) into a corresponding proof of existance, where one must provide possible outcomes for each statement outcome exists v1,v2, ..., vn, d[ c1 ] v1 != 0 /\ d[ c2] v2 /\ .... /\ d[ cn] vn != 0

• comp_impossible_decompose - is a tactic which automatically decomposes an impossibility statement \sum_{v1} ... \sum_{vn} P[c1 = v1] * ... * P[ cn = vn ] = 0 into properties about its component parts forall v1,..,vn, P[c1 = v1] * ... * P[cn = vn] = 0

• exchange_big_inwards f - is a tactic which moves the outermost summation in a series of nested summations to the innermost position, then applies the supplied tactic f in this context.

• exchange_big_outwards n - is a tactic which moves the nth summation in a series of nested summations to the outermost position.

Given its dependencies:

Verified hash-based AMQ structures in Coq

## Packages 0

No packages published

•
•