  Formal reasoning about hashing-based probabilistic data structures often
requires reasoning about random variables where when one variable gets larger
(such as the number of elements hashed into one bucket), the others tend to be
smaller (like the number of elements hashed into the other buckets). This is an
example of negative dependence, a generalization of probabilistic independence
that has recently found interesting applications in algorithm design and
machine learning. Despite the usefulness of negative dependence for the
analyses of probabilistic data structures, existing verification methods cannot
establish this property for randomized programs.
  To fill this gap, we design LINA, a probabilistic separation logic for
reasoning about negative dependence. Following recent works on probabilistic
separation logic using separating conjunction to reason about the probabilistic
independence of random variables, we use separating conjunction to reason about
negative dependence. Our assertion logic features two separating conjunctions,
one for independence and one for negative dependence. We generalize the logic
of bunched implications (BI) to support multiple separating conjunctions, and
provide a sound and complete proof system. Notably, the semantics for
separating conjunction relies on a non-deterministic, rather than partial,
operation for combining resources. By drawing on closure properties for
negative dependence, our program logic supports a Frame-like rule for negative
dependence and monotone operations. We demonstrate how LINA can verify
probabilistic properties of hash-based data structures and balls-into-bins
processes.
