A Separation Logic for Negative Dependence

Jialu Bao

Cornell University

Marco Gaboardi

Boston University

Justin Hsu

Cornell University

Joseph Tassarotti

Boston College

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 , 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 can verify probabilistic properties of hash-based data structures and
balls-into-bins processes.

<concept_desc>Theory of computation Separation logic</concept_desc>

[500]Theory of computation Separation logic

§ INTRODUCTION

Hashing plays a fundamental role in many probabilistic data structures, from
basic hash tables to more sophisticated schemes such as Bloom filters. In
these applications, a hash function $h$ maps a universe of
possible values, typically large, to a set of buckets, typically small.
Hash-based data structures satisfy a variety
of probabilistic guarantees. For instance, we may
be interested in the false positive rate: the
probability that a data structure mistakenly identifies an element as
being stored in a collection, when it was not inserted. We
may also be interested in load measures, such as the probability
that a bucket in the data structure overflows. A typical way to
analyze these quantities is to treat random hash functions as
balls-into-bins processes. For example, hashing $N$ unique elements into
$B$ bins can be modeled as throwing $N$ balls into $B$ bins, where each bin is
drawn uniformly at random.

While this modeling is convenient, one complication is that the counts
of the elements in the different buckets are not probabilistically
independent: one bin containing many elements makes it more
likely that other bins contain few elements. The lack of
independence makes it difficult to reason about
multiple bins, for instance bounding the number of empty bins. Moreover, many
common tools for analyzing probabilistic processes, like concentration
bounds, usually require independence. This subtlety has also been a
source of problems in pen-and-paper analyses of probabilistic
data structures. For instance, the standard analysis of the Bloom filter
bounds the number of occupied bins in order to bound the false
positive rate. The original version of this
analysis presented by <cit.>, and also repeated in many papers,
assumes that the bin counts are independent. However,
<cit.> pointed out that this assumption is
incorrect, and in fact the claimed upper-bound on the false-positive rate is
actually a lower bound. Proving a correct bound on the false-positive
rate required a substantially more complicated argument; recently,
<cit.> mechanized a correct, but complex proof in

We aim to develop a simpler method to formally reason about hash-based
data structures and balls-into-bins processes, drawing on a key concept in
probability theory: negative dependence.

*Towards a simpler analysis: negative dependence.
To study balls-into-bins processes and other phenomena, researchers in
probability theory have developed a theory of negative
dependence <cit.>. Intuitively, variables are negatively
dependent if when one is larger, then the others tend to be smaller. The counts
of the bins in the balls-into-bins process is a motivating example of negative

While there are multiple incomparable definitions of negative dependence,
<cit.> proposed a notion called negative association
(NA) that has many good probabilistic properties. For instance, the bins' counts
in the balls-into-bins process satisfies NA, and NA's closure properties enable
simple, calculation-free proofs of NA. More intriguingly, as
<cit.> identified, sums of NA variables satisfy some
concentration bounds that usually assume probabilistic independence, including
the widely-used Chernoff bounds.

*Our goal: formal reasoning about negative dependence.
From a verification perspective, the closure properties suggest a compositional
method for proving NA in probabilistic programs. In this work, we develop a
separation logic for negative dependence, building on a separation logic for
probabilistic programs called PSL <cit.>. Like all separation logics, PSL
is a program logic where assertions are drawn from the logic of bunched
implications (BI) <cit.>, a substructural logic. In PSL, the separating
conjunction $\sepand$ states that two sets of variables are probabilistically
independent, a common and useful property when analyzing probabilistic programs.

We aim to extend the assertions of PSL so that they can describe both
independence and negative dependence. There are three main difficulties:

* To support reasoning about negative dependence, the assertion logic
needs to be extended with a second separating conjunction that is weaker
than the separating conjunction of PSL. It is easy to extend the syntax of
formulas, but the extended logic should also enjoy good metatheoretical
properties like BI does, including a sound and complete proof system.

* The standard resource semantics of BI <cit.>, based on partial
commutative monoids (PCMs), is not expressive enough to model negative
association because two variables with given marginal distributions can be
negatively associated in more than one way.

* Defining the semantics of separating conjunction to capture NA is
surprisingly challenging. Straightforward definitions fail to satisfy
expected properties, like associativity of separating conjunction.

Beyond the assertions, it is also unclear how to integrate negative association
with the proof rules of PSL. In particular, to view negative association as a
kind of separation, our program logic should have an analogue of the Frame rule
for NA.

*Contributions and outline.
In this paper, we offer the following contributions.

* A novel logic that extends BI with multiple separating
conjunctions, related by a pre-order. Following <cit.>,
models of allow two states to be combined into a single state in more
than one way (<Ref>). We develop a proof system for , and use
Docherty's duality-theoretic approach to prove soundness and completeness.

* A probabilistic model of that can capture both the independence and
negative association (<Ref>). There are two interesting aspects
of our model:

* We crucially use the “non-deterministic” combination of resources
allowed by Docherty's semantics of BI. While this semantics was
originally used to simplify the metatheory of BI, our model shows that
the added flexibility can enable new applications of the logic.

* Our model relies on a novel notion called that is more
expressive than <cit.>'s NA. The generalization is
needed to satisfy the conditions for an model. Moreover, the
closure properties and useful consequences of NA continue to hold for
our generalization.

* A program logic, (Logic of Independence
and Negative Association), extending PSL with
-assertions and a new negative-association Frame rule
(<Ref>). Being a conservative extension of PSL, the proof rules of
PSL remain valid in . We demonstrate our program logic by
proving negative association and related properties on several case studies
(<Ref>). For example, using NA, it is possible to give a
significantly simpler verification of the false positive rate of the Bloom
filter. Another example—an analysis of a repeated balls-into-bins process
motivated by distributed computing—involves a loop with a probabilistic
guard, and requires reasoning about conditional distributions.

We discuss related work in <Ref>, and conclude in <Ref>.

§ OVERVIEW AND KEY IDEA

In this section, we introduce negative association as a tool for analyzing
hashing-based algorithms. We use Bloom filters, a hash-based data structure, as
a motivating example. After sketching a standard proof applying negative
association to Bloom filters, we will show how the same analysis can be
formalized in .

§.§ Background on negative association

Negative association is a property of a set of random variables, which
intuitively says that when some variables are larger, we expect the others to be
smaller. It is formalized as follows:

Let $X_1, \dots X_n$ be random variables. The set $\{X_i\}_i$ is
negatively associated (NA) if for every pair of subsets $I, J \subseteq
\{1, \dots, n\}$ such that $I \cap J = \emptyset$, and every pair of both
monotone or both antitone functions[
In the following, we will consistently use monotone to mean monotonically
non-decreasing and antitone to mean monotonically non-increasing.]
$f : \mathbb{R}^{|I|} \rightarrow \mathbb{R}$ and $g :\mathbb{R}^{|J|} \rightarrow \mathbb{R}$,
where $f, g$ is either lower bounded or upper bounded, we have:

\[ \Ex{f(X_i, i\in I) \cdot g(X_j, j\in J)} \leq \Ex{f(X_i, i \in I)} \cdot \Ex{g(X_j, j\in J)} \]

We can view NA as generalizing independence: a set of independent random
variables is NA because equality holds. NA also strengthens negative
covariance, a simpler notion of negative dependence that requires $\Ex{
\prod_{i \in [n]} X_i} \leq  \prod_{i \in [n]} \Ex{X_i} $.

The survey paper by <cit.> explains several properties of NA
random variables useful for algorithm analysis. First, some standard theorems
about sums of independent random variables apply more generally to sums of NA
random variables. In particular, the widely-used Chernoff bound, which
intuitively says that the sum of independent random variables is close to the
expected value of the sum with high probability, holds also for NA variables. In
addition, NA is preserved by some common operations on random variables. Thus,
we can easily prove that a set of random variables satisfies NA if they are
generated by applying NA-preserving operations to a few basic, building-block
random variables:

The random variables $\{X_i\}_i$ in the following cases are negatively

* Let $\{X_1, \dots, X_n\}$ be Bernoulli random variables such that
$\sum X_i = 1$.

* Let $X_i$ be the $i$-th entry in the vector $X$, where $X$ is a
uniformly random permutation of a finite, nonempty set $A$.

* Let $\{X_1, \dots, X_n\}$ be independent random variables.

In particular, the first case of this theorem implies that if we draw a
length-$n$ one-hot vector, i.e., a vector that has one entry being one
and all remaining entries being zero, uniformly at random, then the entries of
the vector satisfy negative association.

The following theorem states two key closure properties of NA random variables.

The set $S$ of random variables in the following cases are negatively

* Let $T$ be negatively associated, and let $S$ be a non-empty subset of $T$.

* Let $T$ and $U$ be two sets of negatively associated random variables such that every $X \in T$ and $Y \in U$ is independent of each other. Let $S = T \cup U$.

* Let $\{X_1, \dots X_n\}$ be negatively-associated, and
$I_1, \dots, I_m$ be a partition of the set $\{1, \dots, n\}$.
For each $1 \leq j \leq m$, let $f_j : \mathbb{R}^{|I_j|} \rightarrow \mathbb{R}$ be monotone.
Let $S = \{ f_1(X_k, k \in I_1), \dots, f_m(X_k, k \in I_m) \}$.

The first case shows that negative association is preserved if we discard random
variables, while the second case allows us to join two independent sets of
negatively associated random variables to form a larger negatively associated
set. Finally, the third case guarantees that negative association is preserved
under applying monotone maps on disjoint subsets of variables.

§.§ Example: Bloom filters

We demonstrate how NA and its closure properties can be used to analyze Bloom
filters. A Bloom filter is a space-efficient probabilistic data structure for
storing a set of items from a universe $U$. An $N$-bit Bloom filter consists of
a length-$N$ array $bloom$ holding zero-one entries. We assume there is a
family $\mathcal{A}$ of hash functions mapping $U$ to $\{0, \dots, N-1\}$ such
that for any $x \in U$ and any bucket $k$, $\mathbb{P}_{f \in \mathcal{A}}(f(x)
= k) = 1/N $. Let $l_1, \dots, l_H$ be a collection of hash functions drawn from
$\mathcal{A}$. We assume the hash functions are independent, meaning the
collection of variables $\{l_i(x) \mid x \in U, i \in \{1, \dots, H\}\}$ are
mutually independent. To add an item $x \in U$ to the filter, we compute
$l_1(x), \dots, l_H(x)$ to get $H$ positions in the bit array and then set the
bits at each of these positions to $1$. To check if an item $y$ is in the
filter, we check whether the bits at positions $l_1(y), \dots, l_H(y)$ in
$bloom$ are all $1$. If they are, the item is said to be in the filter, but if
any is $0$, then the item is not in the filter. This membership test may suffer
from false positives, i.e., it may show that an item $y$ is in the filter
even when $y$ was never added to the filter. This can happen because with hash
collisions, other items added to the Bloom filter could set all the bits at
locations $l_1(y), \dots, l_H(y)$ to 1. A basic quantity of interest is the
false positive rate: the probability that a Bloom filter reports a false

Our goal is to bound an $N$-bit Bloom filter's false positive rate after $M$
distinct items are added, assuming that it uses $H$ independent hash functions.
Here, we briefly sketch a standard proof where negative association plays a key
role. Let $x$ be some data item not in the set, and let $\fpevent$ be the event
the Bloom filter returns a false positive on $x$. We split the analysis of the
probability of $\fpevent$ into two steps.

For the first step, we condition on $\rho$, the fraction of bits in
$bloom$ that are set to 1 after all items have been added. With $\rho$ fixed to
some value, for each hash function $l_{\alpha}$ the probability that
$bloom[l_{\alpha}(x)] = 1$ is $\rho$.  For $x$ to be a false positive, we must have
$bloom[l_{\alpha}(x)] = 1$ for all $\alpha$.  Since $l_1, \dots, l_H$ are
independent hash functions, this occurs with probability $\rho^H$.

The next step is to show that with high probability, $\rho$ lies within a narrow
range around its expected value. Before showing how to prove this, let us first
see why such a bound is useful. Let $\mu$ be the expected value of $\rho$.
Suppose we have that for some small $\epsilon$ and $\delta$ that $\Pr[\rho \leq \mu
+ \epsilon] \geq 1 - \delta$.  Then, by the law of total probability we have:

\begin{align*}
\Pr[\fpevent]
&\leq \Pr[\fpevent \mid \rho \leq \mu + \epsilon] + \Pr[\rho > \mu + \epsilon] \\
&\leq (\mu + \epsilon)^H + \delta
\end{align*}

where the second line follows from the calculation of the probability
of $\fpevent$ when conditioned on $\rho$.

Now, we turn to the question of how to obtain a bound of the form

$\Pr[\rho \leq \mu + \epsilon] < 1 - \delta$.

As mentioned in <Ref>, a common (incorrect) analysis of $\rho$ assumes that
the entries of $bloom$ are independent, and then applies a Chernoff bound. However,
the entries in $bloom$, $\{bloom[\beta]\}_\beta$, are not independent—what we
can actually prove is that are negatively associated, which fortunately
still allows us to apply the Chernoff bound, as stated later in <Ref>.

\[
\begin{array}{l}
\Assn{bloom}{zero(N)}; \\
\Assn{m}{0}; \\
\DWhile{m < M}{} \\
\quad \Assn{h}{0} \\
\quad \DWhile{h < H}{} \\
\quad\quad \Rand{bin}{oh([N])}; \\
\quad\quad \Assn{upd}{bloom \mathop{||}  bin}; \\
\quad\quad \Assn{bloom}{upd}; \\
\quad\quad \Assn{h}{h+1}; \\
\quad \Assn{m}{m + 1}
\end{array}
\]

Example: Bloom filter

To see that the $\{bloom[\beta]\}_\beta$ are NA, consider the program in
<Ref>, which models the process of adding $M$ distinct
items to the Bloom filter. Because the $M$ items are distinct, we model the
hash functions as independently, randomly sampling hash values for each item as
they are added, a standard model used in the analysis of hashing data
structures <cit.>. That is, we encode the hashing step as
sampling a one-hot vector with the command $oh$ and storing it in the variable
$bin$, where the hot bit of the vector $bin$ represents the selected position.
To set the corresponding position in the filter to 1, we update $bloom$ to be $bloom
\mathop{||} bin$, the bitwise-or of the current array and the sampled one-hot
array. To show that $\{ bloom[\beta] \}_\beta$ are NA, we can reason using the
closure properties. Initially, $bloom$ is set to $zero(N)$. Any set of constant
random variables is independent, and hence negatively associated by
<Ref>. Next, when an item is added, the $bin$ array is NA by
<Ref>. Because $bin$ is sampled independently of $bloom$, the set
$\{bloom[\beta]\}_\beta \cup \{bin[\beta]\}_\beta$ is NA. The bitwise-or operation
$\mathop{||}$ is monotone, so again by <Ref>, the array $upd$ is
negatively associated, thereby showing that $bloom$ is NA at the end of each
loop iteration.

§.§ Representing negative association with separating conjunction

Now that we have seen some properties of negative association and how they can
be used to analyze the Bloom filter, we give a high-level explanation of how
these ideas are formalized in , a novel program logic that is a
core contribution of our work. As mentioned in <Ref>, an earlier
separation logic PSL has a separating conjunction $\sepand$ which is interpreted
as probabilistic independence.  That is, a program state satisfies $P \sepand Q$
if its randomized program variables can be split so that one subset satisfies
$P$, another satisfies $Q$, and the distributions of these two sets are
independent. augments PSL with a weaker separating
conjunction $\negand$ modeling negative association. The precise
definition of negative association needs to be modified to form a
proper model of bunched implications, but for now, one can informally think of $P
\negand Q$ as meaning the random variables can be split into two sets negatively
associated with each other that satisfy $P$ and $Q$ respectively.

The proof rules of can be used to prove NA by applying closure
properties to building-block NA-distributions, much like in our proof sketch
above for the Bloom filter. For example, we can derive a rule that captures NA
of entries in a one-hot distribution:

⊢⊤xoh(n)_β= 0^nx[β] ,

where the assertion $\apDist{y}$ means that the program variable $y$ is
distributed according to some unspecified probability distribution, and
$\bigneg$ is an iterated version of the $\negand$ separating conjunction. Thus,
the post-condition here says that all of the entries of the $x$ vector are
negatively associated.

Meanwhile, since NA is closed under monotone maps, we obtain a form of
separation logic's frame rule for $\negand$:

$f$ monotone

(side conditions omitted)

⊢ ϕηcy  η ,

where $X$ is a set of variables contained in any program states satisfying
$\phi$, $f$ is a monotone function mapping $X$ to a variable $y$, and $\eta$ is
an assertion on some other random variables that are negatively associated with
those satisfying $\phi$.
(We describe a complete version of this rule with all side conditions later, in
<Ref>.) Using this rule, we can show monotone vector operations
like $\mathop{||}$ in the Bloom filter example preserve negative associativity.
For example, we can derive:

⊢ _β= 0^n x[β] _γ= 0^n y[γ]zx || y_β= 0^n z[β] ,

which says that if the union of entries in $x$ and entries in $y$ satisfy NA,
then entries in $z = x \mathop{||} y$ also satisfy NA.

We now sketch how to formalize the proof that $\{bloom[\beta]\}_\beta$ in the
Bloom filter are NA; we defer the rest of the proof of this example to
<Ref>.  The basic idea is to establish $\bigneg_{\beta = 0}^N
{\apDist{bloom[\beta]}}$ as a loop invariant. When an item is added in the loop,
we combine the frame rule with the one-hot sampling vector rule to get that the
$bin$ vector is negatively associated, thus showing: $\bigneg_{\beta = 0}^N
{\apDist{bloom[\beta]}} \negand \bigneg_{\gamma=0}^N {\apDist{bin[\gamma]}}$.
Applying the rule for $\mathop{||}$ above, we obtain that $upd$ is negatively
associated, $\bigneg_{\beta = 0}^N \apDist{upd[\beta]}$. At that point $upd$ is
assigned to $bloom$, restoring the loop invariant.

§ THE LOGIC

Having seen the role of negative association in analyzing randomized algorithms
and how its properties correspond to rules in , we now show how
negative association can be interpreted by separating conjunction. As a first
step, we extend the logic of bunched implications (BI), the assertion logic
underlying separation logic, to support multiple forms of separating conjunction
simultaneously, related by a pre-order. Our motivation to design this logic is
to reason about independence and negative association in one logic and capture
that independence implies negative association, but the logic is more general
and accommodates other potentially interesting models.

§.§ The syntax and proof rules

Let $\mathcal{AP}$ be a set of atomic propositions, and $(\idxset, \leq)$ be a finite pre-order.
The formula in the logic of $\idxset$-bunched implications ($\idxset$-BI) has the following grammar:

\begin{align*}
P, Q &::= p \in \mathcal{AP}
\mid \top
\mid \sepid_{\idx \in \idxset}
\mid \bot
\mid P \land Q
\mid P \lor Q
\mid P \rightarrow Q
\mid P \sepand_{\idx \in \idxset} Q
\mid P \sepimp_{\idx \in \idxset} Q.
\end{align*}

associates each element of $\idxset$ with a separating conjunction
$\sepand_\idx$, a corresponding multiplicative identity $\sepid_{\idx}$ and a
separating implication $\sepimp_{\idx}$.  The proof system for
-BI is based on the proof system for BI, with indexed copy of rules for
each separation, and in addition has $\sepand$-Weakening rules. We
present the full Hilbert-style proof system in
the extended version;
most of the rules are the
same as in the proof system for BI. Here, we only comment on the new rules.

The $\sepand$-Weakening rule says that if $m_1 \leq m_2$, then the
assertion $P \sepand_{\idx_{1}} Q$ implies $P \sepand_{\idx_{2}} Q$.

* [right= $\sepand$-Weakening]
_1 ≤_2
P __1 Q ⊢P __2 Q

We can derive analogous weakening rules for separating implications and
multiplicative identities, in the reverse direction.

The following rules are derivable in $\idxset$-BI:

* [right= $\sepimp$-Weakening]
_1 ≤_2
P __2 Q ⊢P __1 Q

* [right= UnitWeakening]
_1 ≤_2
__2 ⊢__1

§.§ Semantics

As is standard with bunched logics <cit.>, we give a Kripke style
semantics to . We will define a structure called  frame, and
then define  models and the satisfaction rules on models.

An frame is a collection of BI frames satisfying some frame
conditions. While BI frames are often presented as partial, pre-ordered
commutative monoids over states, we need the more general presentation due
to <cit.>, where the binary operation returns a set of
states, instead of at most one state. Such binary operations can be
deterministic (returning a set of at most one element) or non-deterministic. The
admission of non-deterministic models was originally motivated by the
metatheory; somewhat surprisingly, it is also a crucial ingredient in defining
the negative association model we will see in <Ref>.

A (Down-Closed) BI frame is a structure $\mathcal{X} = (X, \sqsubseteq,
\oplus, E)$ such that $\sqsubseteq$ is a pre-order on the set of states $X$,
$\oplus\colon X^2 \rightarrow \mathcal{P}(X)$ is a binary
operation,  and $E \subseteq X$, satisfying following frame conditions (with outermost universal
quantification omitted for readability):

\[\begin{array}{ll}
\text{(Down-Closed)} &  z \in x \oplus y \land x' \sqsubseteq x \land y' \sqsubseteq y \rightarrow
\exists z' (z' \sqsubseteq z \land z' \in x' \oplus y'); \\
\text{(Commutativity)} & z \in x \oplus y \rightarrow z \in y \oplus x; \\
\text{(Associativity)} & w \in t \oplus z \land t \in x \oplus y \rightarrow
\exists s(s \in y \oplus z \land w \in x \oplus s); \\
\text{(Unit Existence)} & \exists e \in E(x \in e \oplus x); \\
\text{(Unit Coherence)} & e \in E \land x \in y \oplus e \rightarrow y \sqsubseteq x; \\
\text{(Unit Closure)} & e \in E \land e \sqsubseteq e' \rightarrow e' \in E.
\end{array} \]

Since all frames we consider in this paper will be Down-Closed, we often
abbreviate Down-Closed BI frame as just BI frame.

The (Commutativity), (Associativity) and (Unit Existence) conditions capture the
properties of commutative monoids, and the (Down-Closed) condition ensures that
the binary operation is coherent with the pre-order. Properties (Associativity)
and (Commutativity) are generalizations of the usual algebraic properties to
accommodate the non-determinism. The three Unit frame conditions
ensure that the set $E$ behaves like a set of units, and satisfies various
closure properties under the binary operation and the pre-order.

We can now define frame to be a collection of BI frames sharing the same
set of states and pre-order, with ordered binary operations:

An $\idxset$-BI frame is a structure $\mathcal{X} = (X, \sqsubseteq, \oplus_{\idx \in \idxset}, E_{\idx})$ such that
for each $\idx$, $(X, \sqsubseteq, \oplus_\idx, E_\idx)$ is a BI frame, and
there is a preorder $\leq$ on $M$ satisfying:

\[\begin{array}{ll}
\text{(Operation Inclusion)} & \idx_1 \leq \idx_2 \rightarrow x \oplus_{\idx_1} y \subseteq x \oplus_{\idx_2} y . \\
\end{array} \]

The (Operation Inclusion) condition together with the frame conditions of BI also imply an
inclusion on unit sets:

Let $\mathcal{X}$ be an $\idxset$-BI frame. If $\idx_1 \leq \idx_2$ then $E_{\idx_2} \subseteq E_{\idx_1}$.

Let $e_2 \in E_{\idx_2}$. By (Unit Existence), there exists $e_1 \in
E_{\idx_1}$ such that $e_2 \in e_1 \oplus_{\idx_1} e_2$. By (Operation
Inclusion), $e_2 \in e_1 \oplus_{\idx_2} e_2$, so (Unit Coherence) implies
that $e_1 \sqsubseteq e_2$, and then (Unit Closure) implies $e_2 \in
E_{\idx_1}$.  So $E_{\idx_2} \subseteq E_{\idx_1}$.

To obtain a BI model over a given BI frame, we must provide a valuation,
which defines which atomic propositions hold at each states in the frame. For
the soundness of the proof system, it is important that the valuation is
persistent: any formula true at a state remains true at any larger state.
Formally, we define models as follows.

A persistent
valuation is a map $\valuation : \mathcal{AP} \rightarrow \mathcal{P}(X)$ such
that, for all $P \in \mathcal{AP}$, if $x \in \valuation(P)$ and $x \sqsubseteq y$ then $y \in
\valuation(P)$.
An model  $(\mathcal{X}, \valuation)$ is an frame
$\mathcal{X} = (X, \sqsubseteq, \oplus_{\idx},
E_{\idx})$ associated with a persistent valuation $\valuation$ on it.

Next, we define which formula are true at a state in a model.

On model $(\mathcal{X}, \valuation)$,
we define the satisfaction relation $\models_\valuation$ between states in $\mathcal{X}$ and formula: for $x \in \mathcal{X}$

$x \models_\valuation p$      iff       $x \in \valuation(p)$

$x \models_\valuation \top$      iff       $\TRUE$

$x \models_\valuation \sepid_{\idx}$      iff       $x \in E_{\idx} $

$x \models_\valuation \bot$      iff       $ $

$x \models_\valuation P \land Q$      iff       $x \models_\valuation P $ and $ x \models_\valuation Q$

$x \models_\valuation P \lor Q$      iff       $x \models_\valuation P$ or $ x \models_\valuation Q$

$x \models_\valuation P \rightarrow Q$      iff       for all $y$ such that $x \sqsubseteq y $, if $y \models_\valuation P$ then $y \models_\valuation Q $

$x \models_\valuation P \sepand_{\idx} Q$      iff       there exist $x'$, $y$, and $z$ with $x' \sqsubseteq x$ and $x' \in y \oplus_{\idx} z$ such that $y \models_\valuation P$ and $z \models_\valuation Q$

$x \models_\valuation P \sepimp_{\idx} Q$      iff       for all $y$ and $z$ such that $z \in x \oplus_{\idx} y$, if $y \models _\valuation P$ then $z \models_\valuation Q$

We say that a formula $P$ is valid in the model $(\mathcal{X}, \valuation)$, written as $\mathcal{X} \models_{\valuation} P$, iff $x \models_{\valuation} P$
for all $x \in \mathcal{X}$.
We also say that $P$ is valid if and only if $P$ is valid in all models and write that as $\models P$. Finally, we write $P \models Q$ if and only if for any model $(\mathcal{X}, \valuation)$,
$\mathcal{X} \models_{\valuation} P$ implies $\mathcal{X} \models_{\valuation} Q$.

We prove the following theorem in
the extended version.

Let $P$ and $Q$ be any two formulas. Then $P \models Q$ iff $P \vdash Q$.

The reverse direction of (soundness) is straightforward by induction on the
proof derivation, but the forward direction (completeness) is less obvious; we
use the duality-theoretic framework proposed by <cit.> to
establish this theorem.

§.§ Potential models

Our design of is mainly motivated by our intended model of negative
association and probabilistic independence, which we will see in the next
section, but the logic is quite flexible and we can see other natural
models. Here we outline three models, inspired by the heap model of separation
logic <cit.>.

*Hierarchical heaps.
In the heap model of separation logic, heaps are partial maps $h : \NN
\rightharpoonup \Val$ from integer addresses to values, and heap combination
$\circ_{heap}$ is a partial binary operation that takes the union if the two
heaps have disjoint domains, and is not defined otherwise. In many systems,
memory addresses are partitioned into larger units, for instance pages.
We can define another partial binary operation $\circ_{page}$ that takes the
union if the two heaps have disjoint domains and are defined on disjoint
pages. Then, $h_1 \circ_{page} h_2 \subseteq h_1 \circ_{heap} h_2$, so we can
build a model of on the two-point pre-order. The two separating
conjunctions $\sepand_{heap}$ and $\sepand_{page}$ then describe heap and page
separation respectively, which could be useful for reasoning about which memory
accesses may require a page-table lookup.

*Strong separation logic.
Heaps in separation logic can store values, but also addresses of other
locations. In the standard heap model, two separate heaps must have disjoint
domains but may store common addresses, i.e., they may hold dangling pointers to
the same locations. Searching for a separation logic with better decidability
properties, <cit.> proposed a notion of strong
separation logic, where two strongly-separated heaps can only hold common
addresses that are already stored in stack variables. The resulting form of
separation can be modeled by a separating conjunction $\sepand_{st}$, and the
standard (weak) form of separation can be modeled by a separating conjunction
$\sepand_{wk}$. Since strong separation implies weak separation, we can again
build a model of supporting both conjunctions on the two-point pre-order.

every picture/.style=line width=0.75pt

(234.31,60.41) – (255.99,75.9) – (257.66,73.56) – (265.45,85.72) – (251.43,82.29) – (253.1,79.95) – (231.42,64.46) – cycle ;

(153.31,94.41) – (174.99,109.9) – (176.66,107.56) – (184.45,119.72) – (170.43,116.29) – (172.1,113.95) – (150.42,98.46) – cycle ;

(182,61.41) – (160.32,76.9) – (158.65,74.56) – (150.86,86.72) – (164.89,83.29) – (163.22,80.95) – (184.9,65.46) – cycle ;

(263.01,96.41) – (241.32,111.9) – (239.65,109.56) – (231.86,121.72) – (245.89,118.29) – (244.22,115.95) – (265.9,100.46) – cycle ;

(195,47) node [anchor=north west][inner sep=0.75pt]   [align=left] $\displaystyle \sepand _{(h, p)}$;

(272,85) node [anchor=north west][inner sep=0.75pt]   [align=left] $\displaystyle \sepand _{h}$;

(130,81.72) node [anchor=north west][inner sep=0.75pt]   [align=left] $\displaystyle \sepand _{p}$;

(200,120) node [anchor=north west][inner sep=0.75pt]   [align=left] $\displaystyle \sepand _{-}$;

The pre-order for $\sepand_{\idx}$

*Tagged memory.
In some security-focused architectures, pointers contain an address as well as a
tag, indicating capabilities that may be performed with that piece of memory.
To reason about these machines, we can consider a resource frame where states
are pairs of $(h, p)$, where $h$ is a heap and $p$ is a permission (say shared
access, or exclusive access). We can then consider four kinds of separation
taking all combinations of heaps aliasing/non-aliasing, and permissions
compatible/incompatible. The result is a frame, with the lattice of
separating conjunctions depicted in <Ref>. Assertions in models
on this frame can reason about all four kinds of separation, where
$\sepand_{-}$ degenerates to the standard conjunction $\land$.

§ A MODEL OF NEGATIVE ASSOCIATION AND INDEPENDENCE

In this section, we will present a model for reasoning about both
probabilistic independence and negative association. <cit.> proposed a BI
model that captures probabilistic independence, developed a program logic (PSL)
to reason about independence in probabilistic programs.  We will construct a BI
model for negative association and combine it with the PSL model to obtain a
$\mathbf{2}$-BI model for both probabilistic independence and negative
association, where $\mathbf{2} = \{ 1, 2\}$ is the two-point set with pre-order
$1 \leq 2$.

One may wonder if it is a simple exercise to replace the independence semantics
of the separating conjunction in PSL by a semantics that capture negative
association, but there are technical challenges. As we will show
in <Ref>, two intuitive BI model definitions fail to
satisfy all frame conditions. To overcome the difficulties,
in <Ref> we define a new notion of negative association that can
express negative dependence of various strengths, and then define a model based
on our new notion.
All omitted proofs can be found in the extended version.

§.§ Preliminaries and the PSL model

We need to introduce some notation to define the models.

First, we represent program states as memories.
Let the set of all program variables be $\Var$, and the set of all possible
values be $\Val$.  For any finite set of variables $S \subseteq \Var$, a memory
on $S$ is a map $S \to \Val$, and $\Mem[S]$ denotes the set of memories on $S$.
For disjoint sets of variables $S,T \subseteq \Var$, and $m_1 \in \Mem[S]$,
$m_2 \in \Mem[T]$, we define $m_1 \bowtie m_2$ to be the union of $m_1, m_2$.

Now we will introduce probabilistic memories.  For a real-valued function $f$,
we say that $x$ is in the support of $f$ if $f(x) \neq 0$.  A countable
distribution on a set $X$ is a countable support function $\mu: X \to [0,1]$
such that $\sum_{x \in X} \mu(x) = 1$.  Let $\Dist(X)$ denote the set of
countable distributions on $X$.  A probabilistic memory on variables $S$
is a distribution over $\Mem[S]$, so the set of probabilistic memories on $S$ is

Next, we will need some constructions on distributions.
A family of special distributions in $\DMem{S}$ is Dirac distributions: for any $x \in \Mem[S]$, the Dirac distribution $\delta(x)$ puts all the weight on $x$, that is, for any $y \in \Mem[S]$,
$\delta(x)(y) = 1$ if $x = y$, and $\delta(x)(y) = 0$ otherwise.

For any sets of variables $S \subseteq S'$, we define the projection map $\pi_{S', S}$ to
map a distribution $\mu$ on $\Mem[S']$ to a distribution on $\Mem[S]$: for any $x \in
\Mem[S]$,

\begin{align*}
\pi_{S', S} \mu(x) \defeq \sum_{x' \in \Mem[S'] \text{ and } \p_{S}(x') = x } \mu(x'),
\end{align*}

where $\p_{S}(x')$ is $x'$ restricted on $S$.
Often $S'$ is clear, so we just write $\pi_{S}$ for $\pi_{S', S}$.
Then, we can formally define independence of variables in a distribution:

For any $\mu \in \DMem{S}$, and disjoint $T_1, T_2 \subseteq S$, we say
$T_1, T_2$ are independent in $\mu$ if for any $x \in \Mem[T_1 \cup T_2]$,

\begin{align*}
\pi_{T_1 \cup T_2} \mu (x) = \pi_{T_1} \mu (\p_{T_1}(x)) \cdot  \pi_{T_2} \mu (\p_{T_2}(x)).
\end{align*}

We then define the independent product
$\otimes$ as: for any $\mu_1 \in \DMem{S}$, $\mu_2 \in \DMem{T}$,

\begin{align*}
\mu_1 \otimes \mu_2
\begin{cases}
\emptyset & \text{if $S, T$ not disjoint} \\
\{\mu  \mid \text{for any $x \in \Mem[S \cup T]$, } \mu(x) = \mu_1(\p_S(x)) \cdot \mu_2(\p_T(x))\}  & \text{if $S, T$ disjoint}
\end{cases}
\end{align*}

For any distribution $\mu \in \DMem{S}$, we call $S$ the domain of $\mu$,
denoted $\dom(\mu)$.  By construction, if $\mu \in \mu_1 \otimes \mu_2$, then
$\dom(\mu_1)$ and $\dom(\mu_2)$ are independent in $\mu$, and $\mu$ is the
unique element in $\mu_1 \otimes \mu_2$. Simple calculations also show that if
$\mu \in \mu_1 \otimes \mu_2$, then $\pi_S \mu = \mu_1$, $\pi_T \mu = \mu_2$.

We can then present the Independence frame from <cit.> as the following BI
frame. For simplicity, we restrict its states to probabilistic memories for
Technically we take a slightly different notion of BI frames that is more
suitable for our purposes. <cit.> presents BI frames with partial,
pre-ordered commutative monoids, which require a unique unit for all states.
But we can encode their frame as our BI frame by taking its partial operation
as an operation that returns sets of size at most one and defining the unit set
$E$ to include their unique unit and be closed under $\sqsubseteq$.]

Let $\PSLset = \cup_{S \subseteq \Var} \DMem{S}$.
Say $\mu \sqsubseteq \mu'$ iff $\dom(\mu) \subseteq \dom(\mu')$ and $\pi_{\dom(\mu)} \mu' = \mu$.
Let $\PSLunit = \PSLset$.
We call $\PSLmodel = (\PSLset, \sqsubseteq, \otimes, \PSLunit)$ the Independence structure.

This Independence structure $\PSLmodel$ is a BI frame.

§.§ Initial attempts at a NA model

Our goal is to design a BI model $\PNAmodel$ that can capture negative
association and can be combined with $\PSLmodel$. To be compatible with
$\PSLmodel$, we let $\PNAmodel$ have the same set of states and the same
pre-order as $\PSLmodel$.  The important remaining piece of the puzzle is the
binary operation $\oplus$, which must satisfy the frame conditions.

One first attempt is to let  $\mu_1 \oplus \mu_2$ return the set of
distributions that agree with $\mu_1, \mu_2$, and satisfy strong NA—we
say $\mu$ satisfies strong NA if $\dom(\mu)$ satisfies NA.

(Attempt 1: Strong NA model)

Let $\PSLset = \cup_{S \subseteq \Var} \DMem{S}$.
For $\mu, \mu' \in \PSLset$, say $\mu \sqsubseteq \mu'$ iff $\dom(\mu) \subseteq \dom(\mu')$ and $\pi_{\dom(\mu)} \mu' = \mu$.
Let $E_s = \PSLset$.
Define $\oplus_s : \PSLset \times \PSLset \to \mathcal{P}(\PSLset)$:

\[
\mu_1 \oplus_s \mu_2 =
\{ \mu \in \DMem{S \cup T} \mid \mu \text{ satisfies strong NA}, \pi_S \mu = \mu_1, \pi_T \mu = \mu_2, S \cap T = \emptyset \} .
\]

We call $\mathcal{\PSLset}_s = (\PSLset, \sqsubseteq, \oplus_s, E_s)$ the strong NA structure.

Unfortunately, the strong NA structure fails to have the (Unit Existence)
property: if $\mu$ does not satisfy strong NA, then there exists no $\mu'$ that
marginalizes to $\mu$ and satisfies strong NA, and thus no $e$ such that $\mu
\in e \oplus_s \mu$. The failure of this property implies that whether or not
two states can be combined depends on properties of the single states in
isolation (e.g., whether a distribution satisfies strong NA), and not just on
how the two states relate to each other; this is hard to justify if we are to
read $\oplus$ as describing which pairs of states can be safely combined.

Looking for a different way of capturing NA, we can take inspiration from the
$\PSLmodel$. There, $\mu_1 \otimes \mu_2$ returns a distribution that agrees with
$\mu_1, \mu_2$ and on which $\dom(\mu_1)$ are independent from $\dom(\mu_2)$.
Thus, we can try letting $\mu_1 \oplus \mu_2$ return distributions that agree
with $\mu_1, \mu_2$ where any variable $x$ in $\dom(\mu_1)$ must be negatively
associated with any variable $y$ in $\dom(\mu_2)$, but variables within
$\dom(\mu_1)$ and variables within $\dom(\mu_2)$ need not be negatively
associated. We call this notion weak NA.

Let $S \subseteq \Var$ be a set of variables,
and let $A, B$ be two disjoint subsets of $S$.  A
distribution $\mu \in \DMem{S}$ satisfies $(A,B)$-NA if
for every pair of both monotone or both antitone functions $f : \Mem[A] \to
\mathbb{R}$, $g : \Mem[B] \to \mathbb{R}$, where we take the point-wise orders on $\Mem[A]$ and $\Mem[B]$,
such that $f, g$ is either lower bounded or upper bounded, we have

\[
\mathbb{E}_{m \sim \mu} [ f(\p_A m) \cdot g(\p_B m) ]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m) ] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m) ] .
\]

By definition, being $(A, B)$-NA for all disjoint $A, B
\subseteq S$ is equivalent to strong NA on $S$. Now, we can try defining another
model based on weak NA.

(Attempt 2: Weak NA model)

Let $\PSLset = \cup_{S \subseteq \Var} \DMem{S}$.
For $\mu, \mu' \in \PSLset$, $\mu \sqsubseteq \mu'$ iff $\dom(\mu) \subseteq \dom(\mu')$ and $\pi_{\dom(\mu)} \mu' = \mu$. Let $E_w = \PSLset$.
Define $\oplus_w : \PSLset \times \PSLset \to \mathcal{P}(\PSLset)$:

\[
\mu_1 \oplus_w \mu_2 =
\{ \mu \in \DMem{S \cup T} \mid \mu \text{ satisfies } (S, T)\text{-NA}, \pi_S \mu = \mu_1, \pi_T \mu = \mu_2, S \cap T = \emptyset \} .
\]

We call $\mathcal{\PSLset}_w = (\PSLset, \sqsubseteq, \oplus_w, E_w)$ the weak NA structure.

This weak NA structure satisfies most BI frame conditions, except that
(Associativity) is unclear.  In short, the definition of $\oplus_w$ and
(Associativity) requires that: if $w$ satisfies $(R \cup S, T)$-NA and $(R,
S)$-NA, then $w$ also satisfies $(S, T)$-NA and $(R, S \cup T)$-NA. Now
$w$ satisfies $(S, T)$-NA by projection closure, but it is unclear whether
$w$ must satisfy $(R, S \cup T)$-NA; we leave this question as an interesting
open problem.

Failing to satisfy (Associativity) would lead to a logic where separating
conjunction is not associative, and significantly more difficult to use. Since
it is unknown whether $\mathcal{\PSLset}_w$ is a BI frame, we will define
another structure to capture negative association.

§.§ Our NA model

Facing the problems with the strong NA structure and the weak NA structures, we
will define a BI model for negative association based on a new notion of
negative association called partition negative association (). This
notion interpolates weak NA and strong NA, in the following sense: $\{A,
B\}$-is equivalent to $(A,B)$-NA for disjoint $A, B \subseteq S$, and $\{
\{s\} \mid s \in S\}$-is equivalent to strong NA for distributions in

We say a partition $\mathcal{S}'$ coarsens a partition $\mathcal{S}$ if
$\cup \mathcal{S} = \cup \mathcal{S}'$ and for any $s' \in \mathcal{S}'$, $s' = \cup \mathcal{R}$ for some $\mathcal{R} \subseteq \mathcal{S}$.

A distribution $\mu$ is $\mathcal{S}$-if and only if
for any $\mathcal{T}$ that coarsens $\mathcal{S}$,
for any family of non-negative monotone functions
(or family of non-negative antitone functions),
$\{f_{A} : \Mem[A] \to \mathbb{R}^+\}_{A \in \mathcal{T}}$,[
We restrict the family of functions to be non-negative: prior work
like <cit.> has assumed non-negativity when working with
notions of NA on partitions; furthermore, without that requirement, for
partitions with odd number of components, would be equivalent to
independence, a strange property.]
where we take the point-wise order on $\Mem[A]$ for each $A \in \mathcal{T}$,
we have

\[
\mathbb{E}_{m \sim \mu} \left[ \prod_{A \in \mathcal{T}} f_{A}(\p_A m) \right]
\leq \prod_{A \in \mathcal{T}} \mathbb{E}_{m \sim \mu} [ f_{A}(\p_A m) ].
\]

We can use to prove NA:

Given a set of variables $S$, $S$ satisfies NA in $\mu$
iff $\mu$ satisfies $\mathcal{S}$-for any
$\mathcal{S}$ partitioning $S$ iff $\mu$  satisfies $\{ \{s\} \mid s \in S\}$-.[
Technically, we slightly modify <cit.>'s NA when defining it in <Ref> by
in addition assuming that $f, g$ are bounded from one side.
We add that condition
to have a cleaner version of this theorem and <Ref>.
All our other results and properties we state about NA in <Ref> hold with or without this condition. ]

We require to be closed under coarsening, which helps us to prove the
next structure we define is a BI frame.

Let $\PNAmodel = (\PSLset, \sqsubseteq, \oplus, \PNAunit)$,
where $\PSLset = \PNAunit = \cup_{S \subseteq \Var} \DMem{S}$.
For $\mu, \mu' \in \PSLset$, say $\mu \sqsubseteq \mu'$ iff $\dom(\mu) \subseteq \dom(\mu')$ and $\pi_{\dom(\mu)} \mu' = \mu$.
Define the operation $\oplus : \PSLset \times \PSLset \to \mathcal{P}(\PSLset)$:

\[
\begin{aligned}
\mu_1 \oplus \mu_2 = \{\mu \in \DMem{S \cup T} \mid{} &\pi_{S} \mu = \mu_1,  \pi_{T} \mu = \mu_2, \\
&\text{$\mu$ is $(\mathcal{S} \cup \mathcal{T})$-\CPNA for any partition $\mathcal{S}, \mathcal{T}$ such that } \\
&\text{$\mu_1$ is $\mathcal{S}$-\CPNA, and $\mu_2$ is $\mathcal{T}$-\CPNA, and $(\cup \mathcal{S}) \cap (\cup \mathcal{T}) = \emptyset$} .\}
\end{aligned}
\]

This definition of $\oplus$ interpolates $\oplus_w$ and $\oplus_s$, in the
following sense.

For any two states $\mu_1, \mu_2 \in \PSLset$,
$ \mu_1 \oplus_s \mu_2 \subseteq \mu_1 \oplus \mu_2 \subseteq \mu_1 \oplus_w \mu_2$.

The first inclusion is because $\mu$
satisfying strong NA implies $\mu$ is $\mathcal{R}$-for any partition
$\mathcal{R}$ on $\dom(\mu)$. The second inclusion is because $\mu_1 \in
\DMem{S}$ satisfies $\{S\}$-and $\mu_2 \in \DMem{T}$ satisfies
$\{T\}$-trivially, which implies any $\mu \in \mu_1 \oplus \mu_2$ would
satisfy $(S, T)$-NA.

Note that $\oplus$ is non-deterministic, and not just partial.

There are distributions $\mu_1, \mu_2$ such that $|\mu_1 \oplus \mu_2| \geq

Let $\mu_1 \in \DMem{\{ x \}}$ and $\mu_2 \in \DMem{\{ y \}}$ be uniform
distribution over memories over 0/1 variables $x$, $y$. Then the
independent product $\mu_{\otimes} \in \mu_1 \otimes \mu_2$ is in $\mu_1 \oplus
\mu_2$, because the projections to $x$ and to $y$ are $\mu_1$ and $\mu_2$
respectively, and $\mu_{\otimes}$ satisfies since independence
implies (we will see this shortly in <Ref>). But the
one-hot uniform distribution $\mu_{oh}$ over variables $x$ and $y$, i.e.,
$\mu_{oh}([x \mapsto 1, y \mapsto 0]) = \mu_{oh}([x \mapsto 0, y \mapsto 1]) =
1/2$, is also in $\mu_1 \oplus \mu_2$,
since again the projections match $\mu_1$ and $\mu_2$ and the one-hot
distribution satisfies NA, and hence . Since $\mu_{oh} \neq
\mu_{\oplus}$, we are done.

Thus, we can build a BI frame on probabilistic memories, crucially using a
non-deterministic combination operation on states <cit.>.

The structure $\PNAmodel = (\PSLset, \sqsubseteq, \oplus, \PNAunit)$ is a Down-Closed BI frame.

See the full proof in <Ref>.
For the frame conditions
where the previous attempts failed, (Unit Existence) holds by letting the unit
$e$ to always be the trivial distribution on the empty set, and
(Associativity) can be proved using the facts that is closed under coarsening
and coarsening commute with projections.  We call
$\PNAmodel$ the model.

Now that we know the frame is a BI frame and captures NA, we want to
combine it with the PSL frame to construct a frame.  To combine them,
we need to show that for any $\mu_1, \mu_2 \in \PSLset$,

\begin{align*}
\mu_1 \otimes \mu_2 \subseteq \mu_1 \oplus \mu_2.
\end{align*}

The inclusion is implied by the following theorem:

[Independence implies ]theoremIndepClosure

Let $S, T \subseteq \Var$ be two disjoint sets of variables.
Suppose $\mu_1 \in \DMem{S}$, $\mu_2 \in \DMem{T}$.
If $\mu_1$ satisfies $\mathcal{S}$-and
$\mu_2$ satisfies $\mathcal{T}$-, then any $\mu \in \mu_S \otimes \mu_T$
satisfies $\mathcal{S} \cup \mathcal{T}$-.

This theorem generalizes the independence closure for NA from <Ref>.
Its proof, however, is more involved because is more expressive and is closed under coarsening.
(See the proof in <Ref>.)

Thus, we can combine $\PSLmodel$ and $\PNAmodel$ into a $\mathbf{2}$-BI model.

Let $\mathbf{2} = \{1, 2\}$ with pre-order $1 \leq 2$.
Let $\oplus_1 = \otimes$, $E_1 = \PSLunit$, $\oplus_2 = \oplus$, $E_2 = \PNAunit$.
The structure $\ProbModel = (\PSLset, \sqsubseteq, \oplus_1, E_1, \oplus_2, E_2)$ is a $\mathbf{2}$-BI model.

Thus $\ProbModel$ is a $\mathbf{2}$-BI frame on probabilistic memories.

§.§ Combining with deterministic memory

While we can model the program states of probabilistic programs as
probabilistic memories, some variables might only get deterministic
assignments. It is useful to know whether a variable is deterministic; for
instance, a deterministic variable is automatically independent of other
variables. To keep track of deterministic variables, we want a $\mathbf{2}$-BI
frame whose states distinguish deterministic memories and probabilistic
memories. We will construct it using a general approach for composing models. In particular, we will compose $\ProbModel$ with a $\mathbf{2}$-BI
frame on deterministic memories.

We can define the product of two frames if they share the same pre-order for indexing, $\idxset$.

Let $\idxset$ be a pre-order.
Given two frames,
$\mathcal{X}_1 = (X_1, \sqsubseteq_1, \oplus_{(1, \idx \in \idxset)}, E_{(1, m  \in \idxset)})$ and
$\mathcal{X}_2 = (X_2, \sqsubseteq_2, \oplus_{(2, \idx \in \idxset)}, E_{(2, \idx \in \idxset)})$.
The product frame, $\mathcal{X} = \mathcal{X}_1 \times \mathcal{X}_2 = (X, \sqsubseteq, \oplus_{\idx \in \idxset}, E_{\idx \in \idxset})$ is defined as

* $X = X_1 \times X_2$;

* $(x_1, x_2) \sqsubseteq (x_1', x_2')$ if and only if $x_1 \sqsubseteq_1 x_1'$ and $x_2 \sqsubseteq_2 x_2'$;

* For $\idx \in \idxset$, $(x_1, x_2) \oplus_{\idx} (x_1', x_2') = \{
(y_1, y_2) \mid y_1 \in x_1 \oplus_{1, \idx} x_1' \land y_2 \in x_2 \oplus_{2, \idx} x_2' \}$;

* $E_{\idx} = E_{1, \idx} \times E_{2, \idx}$.

If $\mathcal{X}_1$ and $\mathcal{X}_2$ are two $\LOGIC$ frames,
then $\mathcal{X} = \mathcal{X}_1 \times \mathcal{X}_2$
is also an frame.

The proof is straightforward.

We now define a $\mathbf{2}$-BI frame modeling the independence and NA separation
on the deterministic memories. Because deterministic variables are
automatically independent of other variables, it is meaningless to check whether a set of
deterministic variables can be separated into two disjoint subsets
independent of each other. Thus, we do not require the separation of
domain when modeling the independence and NA of deterministic variables:

Let $\DetSet = \cup_{S \in \Var} \Mem[S]$, and $\sqsubseteq$ be $=$, and the unit set $\DetUnit = \DetSet$. Define $\oplus_d$ by:

\[ m_1 \oplus_d m_2 =
\begin{cases}
\{ m_1 \} &\quad \text{if $m_1 = m_2$} \\
\emptyset &\quad \text{if $m_1 \neq m_2$}
\end{cases}
\]

The structure $\DetModel = (\DetSet, \sqsubseteq_d, \oplus_1, E_1, \oplus_2, E_2)$, where $\oplus_1 = \oplus_2 = \oplus_d$ and $E_1 = E_2 = \DetUnit$,
is a $\mathbf{2}$-BI frame.

Both $\DetModel$ and $\ProbModel$ are $\mathbf{2}$-BI frames, so we can take
their product.

$\CombModel = \DetModel \times \ProbModel$ is a $\mathbf{2}$-BI frame.

As desired, the states of $\CombModel$ describe both deterministic memories and
probabilistic memories.  Furthermore, restricting to the BI model in
$\CombModel$ with operators indexed by 1 recovers the probabilistic BI model
in <cit.>.

§ PROGRAM LOGIC

Given the model for NA developed in the previous section, we now have a suitable
logic of assertions. In this section, we complete the picture by designing a
program logic, named , for reasoning about negative association and
independence on probabilistic programs.
We defer proofs and details to
the extended version.

§.§ Probabilistic programs

We consider probabilistic programs in a basic probabilistic imperative language
. Let $\DetVar, \RanVar$ be disjoint countable subsets of $\Var$ that
respectively contain all deterministic variables and all probabilistic
variables. We consider program states to be a pair of a deterministic memory
$\sigma$, and a distribution $\mu$ over the probabilistic memory, i.e.,
$(\sigma, \mu) \in \Mem[\DetVar] \times \DMem{\RanVar}$.

Because we will want to decompose a program state as a product of two disjoint
memories, each satisfying a sub-formula, we also want to interpret program
expressions on memories whose probabilistic part is only on part of $\RanVar$. These
memories have type $\Mem[\DetVar] \times \DMem{T}$ for some $T \subseteq
\RanVar$, and we call them configurations, denoted $\Config$.

We assume all expressions in are well-typed:

\begin{align*}
%\DetExp &\ni e_d \defdefeq \DetVar \mid [\DetExp, \dots, \DetExp] \mid  \DetExp + \DetExp \mid \DetExp \land \DetExp \mid \dots \\
\Expr &\ni e \defdefeq \DetVar \mid \RanVar \mid [\Expr, \dots, \Expr] \mid \Expr + \Expr \mid \Expr \land \Expr \mid \dots
\end{align*}

Given an expression $e$, we can interpret it as $\Mem[\DetVar] \times \Mem[T]
\to \Val$ for any $T \subseteq \RanVar$ that includes all the free variables in
$e$.  We can also lift it to an interpretation from configurations to
distributions of values, i.e.,
$\Sem{e}: \Mem[\DetVar] \times \DMem{T} \to \Dist(\Val)$
(see <Ref>).
$\Sem{e}: \Mem[\DetVar] \times \DMem{T} \to \Dist(\Val)$.

We then define commands in and again assume that they are well-typed:

\begin{align*}
\Command \ni c &\defdefeq \Skip \mid \Assn{\DetVar}{\Exp} \mid \Assn{\RanVar}{\Exp} \mid  \Rand{\RanVar}{\Unif{T}} \mid \Seq{\Command}{\Command} \\
%&\mid \DCond{\DetExp}{\Command}{\Command} \mid \DWhile{\DetExp}{\Command}
&	\mid \RCond{\Expr}{\Command}{\Command}
\mid \RWhile{\Expr}{\Command}.
\end{align*}

The randomization is introduced by the sampling command:
$\Rand{\RanVar}{\Unif{T}}$, where $\Unif{T}$ stands for the uniform
distribution on a multi-set  $T$.
We assume that the $\mathbf{while}$ loops terminate in finite steps
on all inputs.
We also assume that an expression assigned to a
deterministic variable only mentions deterministic variables, and a command
branching on a randomized expression does not assign to deterministic variables
in its body/branches. This assumption ensures that deterministic
variables will not receive randomized values during the execution. It is not
to enforce this condition by a syntactic restriction, which we omit for a cleaner

Following the standard semantics for probabilistic programs due
to <cit.>, we interpret programs as transformers from
program states to program states, i.e.,

\[\Sem{c}:  \Mem[\DetVar] \times \DMem{\RanVar} \to \Mem[\DetVar] \times \DMem{\RanVar}. \]

The semantics of is standard
(see <Ref>).
The semantics of is standard.

In our examples, permutation distributions, uniform distributions over

Given a finite multi-set of $A$, a permutation of $A$ is a bijective function
$\alpha : A \to A$.
We let $\textsf{permutation}(A)$ be the multi-set of $A$'s permutations.
When $A$ has duplicates, we distinguish them using additional labels;
so there are always $|A|!$ elements in $\textsf{permutation}(A)$.

Let ([n]) denote the set of length-$n$ one hot vectors. We then
define the shorthands:

\begin{align*}
\Rand{\RanVar}{\perm(A)} &\triangleq \Rand{\RanVar}{\Unif{\textsf{permutation}(A)}} \\
\Rand{\RanVar}{\onehot(n)} &\triangleq \Rand{\RanVar}{\Unif{\textsf{one-hot}([n])}}\\
\Condt{b}{c} &\triangleq \Cond{b}{c}{\Skip}.
\end{align*}

§.§ Assertion Logic: atomic propositions and axioms

Like other program logics, has two layers: the program logic
layer describing the relation between pre-conditions, programs and
post-conditions, and the assertion logic layer describing program states.
In <Ref>, we have constructed a probabilistic model of
$\mathbf{2}$-BI, $\CombModel$, whose states encompass all of , so our
starting point for the assertion logic is this model. In this section, we
introduce atomic propositions $\AP$ for describing states in $\CombModel$ and
some axioms that will hold on $\CombModel$.

We extend the core atomic formula from <cit.>.
To talk about probabilities on program states distributions,
we first define an event to be a function that maps a deterministic
program configuration to 0 or 1,
and let $\Event$ be a set of expressions that can be interpreted as event on deterministic configurations
i.e., for any $ev \in \Event$, $\Sem{ev}:  \Mem[\DetVar] \times \Mem[T]
\to \{0, 1\}$ for some $T \subseteq \RanVar$. Since boolean expressions in the
programming language can also be interpreted as this type, we will let $\Event$
include all boolean expression. Let

\begin{align} \label{def:ap}
\AP \ni p &\defdefeq \apUnif{\Expr}{T} \mid \apBern{\Expr}{p}	\mid \apDetm{\Expr}% \mid \apOnehot{\RanExp}{N}	 \mid \apPerm{\RanExp}{A} \\
\mid \apEq{\Expr}{\Expr} \mid \Expr \leq \Expr \mid
\apEventgeneral{\Event}{b} \mid \Pr[\Event] \bowtie \delta
\end{align}

where ${\bowtie} \mathrel{\in} \{ =, \leq, \geq \}$, $b \in \{0, 1\}$, and $\delta \in \mathbb{R}$ is a constant.
In particular, for boolean expression $e$ and for $b \in \{0,1\}$,
since we can also view $e$ as an event,
$\apEq{e}{b}$ and $\apEventgeneral{e}{b}$ are both valid atomic propositions.
We distinguish their notations ($\apEq{}{}$ v.s. $\apEventgeneral{}{}$) because, in
general, the left hand side of $\apEventgeneral{\Event}{b}$ may not be an
expression and the left hand side of $\apEq{\Expr}{\Expr}$ may not be an

We define the satisfaction of atomic proposition on program configurations as follows.
Let $\FV(e)$ be the set of free variables in expression $e$.

For $(\sigma, \mu) \in \CombModel$, define

* $(\sigma, \mu) \models \apUnif{e}{T}$ iff $\FV(e) \subseteq
\dom(\sigma) \cup \dom(\mu)$ and $\Sem{e}(\sigma, \mu)$ is a distribution
that assigns probability $\frac{1}{|T|}$ to each element of $T$;

* $(\sigma, \mu) \models \apBern{e}{p}$ iff $\FV(e) \subseteq \dom(\sigma)
\cup \dom(\mu)$ and $\Sem{e}(\sigma, \mu)$ is a distribution that assign
probability $p$ to 1 and probability $1-p$ to 0, i.e., the Bernoulli

* $(\sigma, \mu) \models \apDetm{e}$ iff $\FV(e) \subseteq
\dom(\sigma) \cup \dom(\mu)$ and $\Sem{e}(\sigma, \mu)$ is a Dirac

* $(\sigma, \mu) \models \apEq{e}{e'}$ iff $\FV(e) \cup \FV(e')
\subseteq \dom(\sigma) \cup \dom(\mu)$ and $\Sem{e}(\sigma, m)
=\Sem{e'}(\sigma, m)$ for any $m$ in the support of $\mu$;

* $(\sigma, \mu) \models e \leq e'$ iff  $\FV(e) \cup
\FV(e') \subseteq \dom(\sigma) \cup \dom(\mu)$ and $\Sem{e} (\sigma, m) \leq
\Sem{e'} (\sigma, m)$ for any $m$ in the support of $\mu$;

* $(\sigma, \mu) \models \apEventgeneral{ev}{b}$ if for any $m$ in the support
of $\mu$, $\Sem{ev}(\sigma, m) = b$.

* $(\sigma, \mu) \models \Pr[ev] \bowtie \delta$ iff the probability of
event $\Sem{ev}$ in $(\sigma, \mu)$, defined to be $\Pr_{(\sigma, \mu)}[ev] =
\sum_{m \in \Mem[\dom(\mu)]} \mu(m) \cdot \Sem{ev}(\sigma, m)$, satisfies
$\Pr_{(\sigma, \mu)}[e] \bowtie \delta$.

We use the abbreviations:

* $\apIn{e} \triangleq \apEq{e}{e}$. That is, $(\sigma, \mu) \models
\apIn{e}$ holds if all of the variables in $e$ are defined in $\sigma$ and

* $\apOnehot{e}{N} \triangleq \apUnif{e}{\textrm{one-hot([N])}}$.

* For multi-set $A$, $\apPerm{e}{A} \triangleq \apUnif{e}{\textrm{permutation(A)}}$.

For any operation $\odot \in \{ \land, \lor, \negand, \indand\}$, we pick the
corresponding big-operation $\bigodot \in \left\{ \bigwedge, \bigvee, \bigneg,
\bigind\right\}$ to be
their iterated version (see <Ref>).
their iterated version.

With the atomic propositions and abbreviations, we can formally state that $\CombModel$ captures NA.

Let $S$ be any subset of $\RanVar$.
A set of randomized program variables $Y = \{y_i \mid 0 \leq i < K\}$ satisfies NA in distribution $\mu \in \DMem{S}$ if and only if
for any deterministic memory $\sigma \in \Mem[\DetVar]$, we have
$(\sigma, \mu) \models \bigneg_{i = 0}^{K} \apIn{y_i} $.

In the $\CombModel$ model, all axioms from <cit.> still hold,
and we have new axioms for the negative association conjunction and the
permutation distribution.

Let $x_{\gamma}$ be variables. The following axioms are valid in $\CombModel$.

\begin{align}
&\models \apOnehot{[x_0, \dots, x_{N - 1}]}{N} \to \bigneg_{\gamma = 0}^{N} \apIn{x_{\gamma}} \tag{OH-PNA}
\label{ax:oh-pna}
\\
&\models \apPerm{[x_0, \dots, x_{N -1}]}{A} \to \bigneg_{\gamma = 0}^{N} \apIn{x_{\gamma}} \tag{Perm-PNA}
\label{ax:perm-pna}
\end{align}

The two axioms follow from <Ref>, which shows that random
variables in one-hot distributions and permutation distributions are NA,
and <Ref>, which shows that $\negand$ captures the NA of
random variables. We can also encode the monotone map closure
in <Ref> as an axiom in the logic.

[Monotone map]lemmaMonotoneMapAxiom
Let $x$, $x_{\gamma, \alpha}$ and $y_{\gamma}$ be variables.
The following is valid in $\CombModel$.

\begin{align}
\models \bigneg_{\gamma = 0}^{N} \left(\bigwedge_{\alpha = 0}^{K_{\gamma} + 1} \apIn{x_{\gamma, \alpha}} \right) &\land \bigwedge_{\gamma = 0}^{N} y_{\gamma} = f_{\gamma} \left(x_{\gamma, 0}, \dots, x_{\gamma, K_{\gamma} } \right) \to \bigneg_{\gamma=0}^{N} \apIn{y_{\gamma}}
\notag \\
&\textrm{ when } f_1, \dots, f_N \textrm{ all monotone or all antitone}
\tag{Mono-Map} \label{ax:mono-map}
\end{align}

When we establish NA from permutation distributions, it is preserved under not
only monotone/antitone maps but also any element-wise homogeneous maps. The
reason is that fixing a multi-set and a permutation, permuting first and then
applying the same map on each element is the equivalent to applying the map on
each element and then permuting. So applying homogeneous maps on a permutation
distribution gives another permutation distribution. We can capture this
property in an axiom.

Let $x_{\gamma}$ be variables, and $f(A)$ be $\{f(a) \mid a \in A \}$. The
following axiom is valid in $\CombModel$.

\begin{equation}
\label{ax:perm-map}
\models \apPerm{[x_1, \dots, x_N]}{A} \land \apEq{y}{[f(x_1), \dots, f(x_N)]} \to \apPerm{y}{f(A)} \tag{Perm-Map}
\end{equation}

§.§ Restricting the assertion language

When designing a separation logic for reasoning about negative association and
independence, we sometimes want to separate out a smaller configuration
$(\sigma', \mu')$ inside a given program state $(\sigma, \mu) \models \phi$,
such that $(\sigma', \mu')$  satisfies some sub-formula of $\phi$.  In the
program logic we will present in <Ref>, the soundness of
RCase, Const, Frame and NegFrame rules all
rely on the ability to do that.  To ensure there exists such a smaller
configuration, we require the assertion logic to satisfy a key condition called
restriction, which says that to check whether a configuration satisfies
$\phi$, it suffices to check whether the configuration's projection on
$\FV(\phi)$ satisfies $\phi$.  We identify a subset of formulas that
satisfy the restriction property when interpreted on states in $\CombModel$:

We define as

\begin{align*}
\AssertLOGIC \ni P, Q &::= p \in \mathcal{AP}
\mid \top
\mid \bot
\mid P \land Q
\mid P \lor Q
\mid P \rightarrow Q
\mid P \indand Q
\mid P \indimp Q
\mid P \negand Q
\end{align*}

where $\mathcal{AP}$ is defined as in <Ref>.

omits multiplicative identities $I_{\idx}$ because on $\CombModel$
they are all equivalent to $\top$.
The only limitation is that excludes the use of $\negimp$.

Let $(\sigma, \mu)$ be any configuration,
and let $\phi$ be an formula interpreted on $\CombModel$,
Then, for any $m \in \Mem[\DetVar \setminus \FV(\phi)]$,

\[(\sigma, \mu) \models \phi \iff (\p_{\FV(\phi)}\sigma \bowtie m, \pi_{\FV(\phi)}\mu) \models \phi. \]

Indeed, we can exhibit a counterexample showing that $\negimp$ does not
satisfy restriction.

There exists $(\sigma, \mu) \in \Config$ and formula $\phi$ such that
$(\sigma, \mu) \models \phi$ but $(\sigma, \pi_{\FV(\phi)}) \not\models \phi$.

In the following, we will consider $\AssertLOGIC$ formula on the $\CombModel$
model as the assertion logic.

§.§ The program logic

We now introduce the program logic layer of .
Judgements in have the form $\hoare{\prop}{c}{\propB}$, where $c \in \Command$ is a probabilistic program,
and $\prop, \propB \in \AssertLOGIC$ are restricted assertions.

A judgment is valid, written $\models
\hoare{\prop}{c}{\propB}$, if for all $( \sigma, \mu ) \in \Mem[\DetVar]
\times \DMem{\RanVar}$ such that $( \sigma, \mu )  \models \prop$, we have
$\Sem{c}(\sigma, \mu ) \models \propB$.

*[Left= Cond]

⊢ϕb c'ψ

*[Left= Loop]

x_r ∉(e_r)

x_r ∉(ϕ)

ϕ' →ϕψ→ψ'

⊢ϕ_1 ϕ_2cψ_1 ψ_2

⊢ϕ_1 ϕ_2cψ_1 ψ_2

(η) ∩(c) = ∅

(η) ∩(c) = ∅

(ψ) ⊆T ∪(c) ∪(c)

ϕ→T ∪(c)

rules: from PSL.

_η→⋁_α∈S η_α

∀α∈S. ⊢ϕη_αcψ

(η) ∩(c) = ∅

X ⊆(c) ∖(c)

y ∉(η)

⊢ϕcy ∼f(X)

$f$ is a monotone function

⊢ ϕηcy  η

⊢ev_1c[ev_2] ≤δ
⊢[ev_1] ≥1 - ϵc[ev_2] ≤δ+ ϵ

rules: new and extended.

Next, we present the proof system of . Since our assertions are a
conservative extension of assertions from PSL, most of the rules carry over
unchanged; we list existing rules in <Ref>. Here, we
comment on the new and generalized rules, which we list in

*NA frame rule.
Our most important addition is the frame rule for the negative association
conjunction $\negand$. Informally, the NegFrame rule says that if a
set of variables $X$ is negatively associated with another set of variables
$Y$ that satisfy $\eta$ in a program state, and the program $c$ performs a
monotone operation $f$ on $X$ and stores the result in a variable $y$, then in
the resulting program state, $y$ and the untouched variables $Y$ will also be
negatively associated, and $Y$ will still satisfy $\eta$.  Like the
Frame rule for independence $\indand$, the NegFrame rule
uses syntactic restrictions to control which variables the program may read
and write. The three sets of variables $\RV(c), \WV(c), \MV(c)$ represent the
variables that $c$ may read from, must write to, and may modify, respectively;
these sets can be defined by induction on the syntax of the program. Roughly,
the side conditions guarantee the program $c$ does not read from or modify $Y$,
the set of variables satisfying $\eta$; they in addition guarantee that $X$,
the domain of the monotone map will not be modified by $c$, and $y$, the
codomain of the monotone map does not belong to $Y$.

*Generalized random case analysis.
As a more minor extension, we also generalize the randomized case analysis
rule from PSL in RCase. At a high level, this rule allows reasoning
by case analysis on a property $\eta$ of the program memory (e.g., whether a
variable is true or false). Since the input is a distribution, which may have
some probability of $\eta$ holding, and some probability of $\eta$ not
holding, soundness of the rule is a delicate matter requiring several
technical side conditions. The original rule in PSL only allowed case analysis
on a Boolean expression; we generalize this rule to allow a case analysis on
any finite number of cases (e.g., performing case analysis on the value of a
bounded variable).

To explain this rule, we first introduce the side conditions in order. We say
that a formula $\eta$ is closed under conditioning (CC) if for any
$(\sigma, \mu) \models \eta$, for any $m$ in the support of $\mu$,
$(\sigma, \delta(m)) \models \eta$. In the second condition, $\models_\Mem
\phi$ denotes that for any $\sigma \in \Mem[\DetVar]$, $m \in \Mem[T]$ where
$T \subseteq \RanVar$, $(\sigma, \delta(m)) \models \phi$, which says
$\phi$ is valid on all effectively deterministic configurations. Finally, we say
that a formula $\phi$ is closed under mixtures (CM) if $(\sigma, \mu_1)
\models \phi$,	$(\sigma, \mu_2) \models \phi$ and $\mu$ is a convex
combination of $\mu_1, \mu_2$ together imply $(\sigma, \mu') \models \phi$.

Then, the rule RCase says if an assertion $\eta$ is independent from
the rest of the assertions in the pre-condition, $\eta$ is closed under
conditioning, and the post-condition $\psi$ is closed under mixtures, then we
can perform case analysis on $\eta$ to derive $\hoare{\phi \sepand
\eta}{c}{\psi}$. Intuitively, every memory $m$ in the support of the input
memory distribution satisfies $\eta_a$ for some case $a \in S$. The main premise shows that
the output distribution of program $c$ from any such input $m$ satisfies $\psi$. Then,
since any distribution $\mu$ on inputs is a convex combination of
such memories $m$, and $\psi$ holds on each conditional output distribution,
we have $\psi$ holds on the entire output distribution by convex closure.

*Bounding bad events.
In addition, we present the rule ProbBound to facilitate bounding
tail probabilities. It says that if the pre-condition $\apEvent{ev_1}$
guarantees that event $ev_2$ happens for at most $\delta$ probability
after command $c$, then in general, event $ev_2$ happens for at most
probability $\delta + \epsilon$ after $c$, where $\epsilon$ upper bounds the
probability that $ev_1$ is not true in the pre-condition.  The validity of
this rule uses the law of total probability, which says for any two events
$ev_1$ and $ev_2$,

\begin{align*}
\Pr(ev_1) &= \Pr(ev_1 \mid ev_2) \cdot \Pr(ev_2) + \Pr(ev_1 \mid \neg ev_2) \cdot \Pr(\neg ev_2) \\
&\leq \Pr(ev_1 \mid ev_2) +  \Pr(\neg ev_2).
\end{align*}

As expected, the proof system is sound.
(Soundness of )
If $\vdash \hoare{\phi}{c}{\psi}$ is derivable,
then it is valid: $\models \hoare{\phi}{c}{\psi}$.

§ EXAMPLES

Now that we have introduced , we present a series of formalized
case studies. Our examples are extracted from various algorithms using hashing
and balls-into-bins processes.

§.§ Preliminaries: probabilities, expectations, concentration bounds

Our examples will use a handful of standard facts about probability
distributions, encoded as axioms in the assertion logic. We will
generally mention these axioms before they are used, but here we
introduce one fact that we will use through all of our examples: the
Chernoff bound.

In each of our examples we will establish negative
dependence of a sequence of random variables $\{ X_i \}_i$ and apply a
concentration bound: a theorem showing that the sum $X_1 + \cdots + X_n$
is usually close to its expected value. This kind of analysis is useful for
establishing high-probability guarantees of randomized algorithms, e.g.,
showing that the error of a random estimate is at most $0.01$ with probability
at least $99\%$.

Let $X_1, \dots, X_n$ be a sequence of NA random variables, each bounded in
$[0, 1]$, and let $Y = \sum_{i = 1}^n X_i$. Then for any failure probability
$\beta \in (0, 1]$, we have:

\[
\Pr[ |Y - \EE[Y]| \geq T(\beta, n) ] \leq \beta
\ \
\text{ where }
T(\beta, n) = \sqrt{ (n/2) \ln(2/\beta) }.
\]

To hide complex numerical bounds, we use the notation $T(\beta, n)$
for the above function throughout. In our assertion logic, the
Chernoff bound can be encoded as the following axiom schema:

Let $\{ x_\alpha \}$ be a family of variables indexed by $\alpha$, where
each variable is bounded in $[0, 1]$ and is a monotone function of its program
variables. Then for any $\beta \in (0, 1]$, the following axiom schema is
sound in our model:

\begin{equation} \label{ax:na-chernoff}
\models \bigneg_{\alpha = 0}^N \apDist{x_\alpha}
\to \Pr \left[ \ \bigmid \sum_{\alpha = 0}^N x_\alpha - \EE\left[\sum_{\alpha = 0}^N x_\alpha\right] \bigmid\ \geq T(\beta, n) \right] \leq \beta
\tag{NA-Chernoff}
\end{equation}

We will also use a new expression in our assertions: $\EE[f]$, where $f$ is a
non-negative and bounded numeric expression, denotes the expected value of $f$
in the current program configuration. We also observe the following conventions
throughout the examples: logical variables are denoted by Greek ($\alpha, \beta,
\gamma, \dots$) and capital Roman letters ($M, N, K, \dots$). Program variables
start with lower-case Roman letters ($x, y, z, \dots$).

§.§ Bloom filter, high-level

\[
\begin{array}{l}
\textsc{Bloom}: \\
\quad\Assn{bloom}{zero(N)}; \\
\quad\Assn{m}{0}; \\
\quad\DWhile{m < M}{} \\
\quad\quad \Assn{h}{0} \\
\quad\quad \DWhile{h < H}{} \\
\quad\quad\quad \Rand{bin}{oh([N])}; \\
\quad\quad\quad \Assn{upd}{bloom \mathop{||}  bin}; \\
\quad\quad\quad \Assn{bloom}{upd}; \\
\\
\\
\\
\quad\quad\quad \Assn{h}{h+1}; \\
\quad\quad \Assn{m}{m + 1};
\end{array}
\]

Higher-level version

\[
\begin{array}{l}
\textsc{BloomArray}: \\
\quad\Assn{bloom}{zero(N)}; \\
\quad\Assn{m}{0}; \\
\quad\DWhile{m < M}{} \\
\quad\quad \Assn{h}{0} \\
\quad\quad \DWhile{h < H}{} \\
\quad\quad\quad \Rand{bin}{oh([N])}; \\
\quad\quad\quad \Assn{n}{0}; \\
\quad\quad\quad \DWhile{n < N}{} \\
\quad\quad\quad\quad \Assn{upd}{bloom[n] \mathop{||} bin[n]}; \\
\quad\quad\quad\quad \Assn{bloom[n]}{upd}; \\
\quad\quad\quad\quad \Assn{n}{n + 1} \\
\quad\quad\quad \Assn{h}{h+1}; \\
\quad\quad \Assn{m}{m + 1}
\end{array}
\]

Array version

Bloom filter examples

Next, we revisit the Bloom filter example introduced in <Ref>.  We
show how to translate the informal argument in <Ref> into formal
proofs in our program logic. First, we will analyze the process of adding items
into a Bloom filter $bloom$ and prove that the entries in $bloom$ are negatively
associated at the end of the process. Second, we will analyze a program that
checks the membership of a new item in a given Bloom filter and show how
to bound its false positive rate. Last, we combine them together into one proof
that bounds the false positive rate of a Bloom filter with $M$ elements.

Proving NA of $bloom$
We reproduce the code for Bloom in <Ref>.
This program is a higher-level version of the program in <Ref>,
which performs array operations bit-by-bit.
We align the two versions so that the equivalent operations are side-by-side.
We will demonstrate our program logic on the higher-level version first and
analyze the array version later in <Ref>.

Recall that the code models inserting $M$ distinct elements into a Bloom filter
backed by an array $bloom$ of length $N$, where each element is hashed by $H$
functions, each producing an element of $[N]$ uniformly at random.
We refer to the outer loop as $\mathit{outer}$, and the inner
loop as $\mathit{inner}$. For both the outer and the inner loop, we apply the
rule Loop with the loop invariant:

$ \bigneg_{\beta = 0}^N \apDist{bloom[\beta]} $.

We consider the inner loop first. We show that the invariant is preserved by the
body of $\mathit{inner}$. After the $oh$ sampling command, RSamp* gives:

\[ \left(\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}\right) \indand \apOnehot{bin}{[N]} \]

By negative association of the one-hot distribution (<ref>), we get

\[ \left(\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}\right) \indand \left(\bigneg_{\gamma = 0}^N bin[\gamma]\right)\]

which implies

\[ \left(\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}\right) \negand \left(\bigneg_{\gamma = 0}^N bin[\gamma]\right)\]

using Weak. Rearranging terms, this is equivalent to

\[ \bigneg_{\beta = 0}^N \apDist{bloom[\beta]} \negand \apDist{bin[\beta]} . \]

After the assignment to $upd$, we have:

\[
\left(\bigneg_{\beta = 0}^N \apDist{bloom[\beta]} \negand \apDist{bin[\beta]} \right)
\land \apEq{upd}{bloom \mathop{||} bin} .
\]

Because $\mathop{||}$ is monotone, applying the monotone mapping axiom
(<ref>) gives us:

\[
\bigneg_{\beta = 0}^N \apDist{upd[\beta]} .
\]

Using the assignment rule (RAssn) on the assignment to $\mathit{bloom}$
shows that the loop invariant is preserved by the inner loop. Thus,
Loop gives:

\[
\hoare{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}}
{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}}
\]

Next, we turn to the outer loop. The argument showing that the invariant is
preserved by the outer loop follows by a straightforward argument, since the
outer loop only modifies $bloom$ through the inner loop, so Loop gives:

\[
\hoare{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}}
{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}}
\]

Then, we have:

\[
\hoare{\top}{\textsc{Bloom}}{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}}
\]

because initializing $bloom$ to the all-zeros vector, a deterministic value,
establishes the loop invariant. This judgment shows that the $bloom$ vector
satisfies NA at the end of the program.

\[
\begin{array}{l}
\CheckMem(H, bloom): \\
\quad \Assn{h}{0}; \\
\quad\Assn{allhit}{1} \\
\quad \DWhile{h < H}{} \\
\quad\quad \Rand{bin}{\Unif{[N]}}; \\
\quad\quad \Assn{hit}{bloom[bin]}; \\
\quad\quad\Assn{allhit}{hit \mathop{\&\&} allhit}; \\
\quad\quad\Assn{h}{h+1};
\end{array}
\]

Check the membership of a new item

Bounding the false positive rate
Now, we turn to verifying a bound on the false positive rate of the Bloom
filter. Recall that a false positive occurs if when querying with an element
that was not inserted, the filter returns true. We can encode the membership
check of a new element as a program $(H,bloom)$, listed
in <Ref>, which hashes the new element into $H$ uniformly
random positions and checks if these positions are all set to one in the filter.
If so, the Bloom filter will report that the new element is in set, when it was
never inserted—a false positive.

To verify the false positive rate, we place the program $\CheckMem(H, bloom)$
immediately after Bloom, and then verify a bound on the probability
that $allhit$ is 1 at the end of the combined program. We first apply the
Chernoff bound to the NA variables (<ref>) to prove that, with
high probability, the number of occupied bins in Bloom is near its mean
with high probability:

\[
\Bigg\{\top\Bigg\}{\textsc{Bloom}}
\Bigg\{\Pr \left[ \ \bigmid \sum_{\beta = 0}^N bloom[\beta] - \EE\left[\sum_{\beta = 0}^N
bloom[\beta] \right] \bigmid\ \geq T(\delta, N) \right] \leq \delta \Bigg\}.
\]

This concentration bound implies that a tail bound, which says with high
probability $\sum_{\beta = 0}^N bloom[\beta]$ is upper bounded by its expected
value plus $T(\delta, N)$,

\begin{align}
\label{eq:ex:bloom}
\Bigg\{\top\Bigg\} {\textsc{Bloom}}
\Bigg\{\Pr \left[ \sum_{\beta = 0}^N bloom[\beta] < \EE\left[\sum_{\beta = 0}^N
bloom[\beta] \right] + T(\delta, N) \right]  \geq 1 - \delta \Bigg\}.
\end{align}

Then we analyze and show in
the extended version

\begin{align*}
\Big\{\sum_{\beta = 0}^N bloom[\beta] < K \Big\}{\CheckMem}
\Big\{\Pr[allhit] \leq (K/N)^H \Big\}.
\end{align*}

Then, by the ProbBound rule and basic axioms about probabilities,
we have

\begin{align}
\label{eq:ex:checkmem}
\hoare{\Pr[\sum_{\beta = 0}^N bloom[\beta] < K] \geq 1 - \delta}{\CheckMem}{\Pr[allhit] \leq (K/N)^H + \delta}.
\end{align}

We then use Seqn to combine the proved judgements for Bloom
(<ref>) and  (<ref>) to derive that, for any

\begin{align*}
\hoare{\top}{\textsc{Bloom}; \CheckMem }
{\Pr[allhit] \leq \left( \frac{\EE\big[\sum_{\beta = 0}^N bloom[\beta]\big] +
T(\delta, N)}{N} \right)^H + \delta}.
\end{align*}

Since $allhit$ is 1 exactly when there is a false positive, this judgment
proves an upper bound on the false positive rate of the Bloom filter.[
The precise expected value is $N \cdot (1 - (1 - 1/N)^{M \cdot H})$, a fact
which can also be shown in our logic. Roughly speaking, this fact follows
because each element of $bloom$ is the logical-or of $M \cdot H$
probabilistically independent bits, each $1$ with probability $1/N$ and $0$
otherwise. This argument does not rely on negative association.]

§.§ Bloom filter, low-level

The previous Bloom filter uses a vector operation $bloom \mathop{||} bin$ to
transform an array of negatively associated values. We next consider a
lower-level version of the previous example, BloomArray, in
<Ref>, where the vector operation is replaced by a loop that
applies the Boolean-or.

Let $\mathit{outer}$ and $\mathit{mid}$ be the outer-most and second outer-most
loops, and let $\mathit{inner}$ be the inner-most loop.  Again, our goal is to
show that the vector $bloom$ is negatively associated at the end of the program.
We first prove the following judgment for $\mathit{inner}$:

\[
\hoare{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\indand \bigneg_{\gamma = 0}^N \apDist{bin[\gamma]} }
{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\negand
\bigneg_{\gamma = n}^N \apDist{bin[\gamma]}}
\]

We will apply the rule Loop on $\mathit{inner}$ with the following loop

\[
\phi = \bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\negand
\bigneg_{\gamma = k}^N \apDist{bin[\gamma]}
\]

To show that the loop invariant is preserved by the body, we can first show:

\[
\hoare{\apDist{bloom[n], bin[n]}}
{\Assn{upd}{bloom[n] \mathop{||} bin[n]}}
{\apEq{upd}{bloom[n] \mathop{||} bin[n]}}
\]

using RAssn. Noting that the boolean-or operator is a monotone operation, we
may apply the frame rule NegFrame to obtain:

\[
\hoare{\apDist{bloom[n], bin[n]} \negand \eta}
{\Assn{upd}{bloom[n] \mathop{||} bin[n]}}
{\apDist{upd} \negand \eta}
\]

with the framing condition

\[
\eta = \left( \bigneg_{\beta = 0}^n \apDist{bloom[\beta]} \right)
\negand \left( \bigneg_{\beta = n + 1}^N \apDist{bloom[\beta]} \right)
\negand \left( \bigneg_{\gamma = n + 1}^N \apDist{bin[\gamma]} \right) .
\]

Thus, by re-associating the separating conjunction and applying RAssn
for the remaining two assignments in the inner-most loop, we have:

\[
\hoare{\phi}{\Assn{upd}{bloom[n] \mathop{||} bin[n]}; \Assn{bloom[n]}{upd};
\Assn{n}{n + 1}}{\phi}
\]

and thus by Loop, we have:

\[
\hoare{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\negand
\bigneg_{\gamma = n}^N \apDist{bin[\gamma]}}
{\bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\negand
\bigneg_{\gamma = n}^N \apDist{bin[\gamma]}} .
\]

Now for loop $\mathit{mid}$, we establish the same loop invariant as we took

\[
\psi = \bigneg_{\beta = 0}^N \apDist{bloom[\beta]}
\]

If $\psi$ holds at the beginning of $\mathit{mid}$, then invariant for the
inner-most loop $\phi$ holds after assigning $0$ to $n$ and sampling $bin$,
since $bin$ is independent of $\psi$ (RSamp*) and $bin$ is distributed
as $\onehot(n)$, which implies entries in $bin$ are negatively associated
(<ref>). Furthermore, $\phi$ implies $\psi$ at the exit of
$\mathit{inner}$, by dropping the conjunct describing $bin$. Thus, $\psi$ is a
valid invariant for $\mathit{mid}$, and the rest of the proof proceeds

§.§ Permutation hashing

\[
\begin{array}{l}
\textsc{PermHash}: \\
\quad\Rand{g}{\perm([B \cdot K])}; \\
\quad\Assn{n}{0}; \\
\quad\Assn{ct}{0}; \\
\quad\DWhile{n < N}{} \\
\quad\quad \Assn{bin[n]}{mod(g[n], B)}; \\
\quad\quad \Assn{hitZ[n]}{[bin[n] = Z]}; \\
\quad\quad \Assn{ct}{ct + hitZ[n]}; \\
\quad\quad \Assn{n}{n+1}
\end{array}
\]

Permutation hashing

Our second example considers a scheme for hashing using a random permutation.
Consider the program in <Ref>, from an algorithm for fast set
intersection <cit.>. Letting $B$ be the number of
bins, and the data universe be $[B \cdot K] = \{ 1, \dots, B \cdot K \}$ where
$B \cdot K \geq N$, we
first draw a uniformly random permutation $g$ of the data universe. Then, we
hash the numbers $n \in [N]$ into $bin[n]$ by applying the hash function $g$ and
then taking the result modulo $B$. Then, we record whether the item landed in a
specific bucket $Z$ by computing the indicator $hitZ[n] = [bin[n] = Z]$, which
is $1$ if $bin[n] = Z$ and $0$ otherwise, and accumulate the result into the
count $ct$.

Our goal is to show that $ct$ is usually not far from its expected value, which
is $N/B$. If the quantities $\{[bin[n] = Z]\}_{n}$ were independent, we would be
able to apply a standard concentration bound to the sum $ct$. However,
$\{ bin[n] = Z \}_n$ are not independent: for instance, since exactly
$K$ elements from $[B \cdot K]$ map to $Z$, if $bin[n] = Z$ for $n \in \{ 0,
1, \dots, K - 1 \}$, then $bin[K] = Z$ must be false.

Nevertheless, we can show that $\{ [bin[n] = Z] \}_n$ are negatively associated
random variables. Intuitively, $\{ g[n] \}_n$ are NA random variables because
the result of a uniformly random permutation is NA. Then, $\{ bin[n] \}_n$ is
computed by mapping the function $mod(-, B)$ over the array $g$; since this
produces another uniform permutation distribution, the vector $\{ bin[n] \}_n$
is also NA. By similar reasoning $\{ [bin[n] = Z] \}_n$ is also NA, as it is
obtained by mapping the function $[- \mathrel{=} Z]$ over $\{ bin[n] \}_n$.
Since this example is similar to the first Bloom filter example, except applying
the negative association of the permutation distribution (<ref>) and
the permutation map axiom (<ref>), we defer the details to the

§.§ Fully-dynamic dictionary

\[
\begin{array}{l}
\textsc{FDDict}: \\
\quad\Assn{binCt}{zero(C,P)}; \\
\quad\Assn{n}{0}; \\
\quad\DWhile{n < N}{} \\
\quad\quad \Rand{crate[n]}{oh([C])}; \\
\quad\quad \Rand{pocket[n]}{oh([P])}; \\
\quad\quad \Assn{bin[n]}{crate[n]^\top \cdot pocket[n]}; \\
\quad\quad \Assn{p}{0}; \\
\quad\quad \DWhile{p < P}{} \\
\quad\quad\quad \Assn{c}{0}; \\
\quad\quad\quad \DWhile{c < C}{} \\
\quad\quad\quad\quad \Assn{upd}{binCt[c][p] + bin[n][c][p]}; \\
\quad\quad\quad\quad \Assn{binCt[c][p]}{upd}; \\
\quad\quad\quad\quad \Assn{c}{c + 1}; \\
\quad\quad\quad \Assn{p}{p + 1}; \\
\quad\quad \Assn{n}{n + 1}; \\
\quad\Assn{p}{0}; \\
\quad\DWhile{p < P}{} \\
\quad\quad \Assn{c}{0}; \\
\quad\quad \DWhile{c < C}{} \\
\quad\quad\quad \Assn{over[c][p]}{[binCt[c][p] > T_{bin}]}; \\
\quad\quad\quad \Assn{upd}{overCt[c] + over[c][p]}; \\
\quad\quad\quad \Assn{overCt[c]}{upd}; \\
\quad\quad\quad \Assn{c}{c + 1}; \\
\quad\quad \Assn{p}{p + 1}
\end{array}
\]

Fully-dynamic dictionary <cit.>

\[
\begin{array}{l}
\textsc{RepeatBIB}: \\
\quad\Assn{r}{0}; \\
\quad\DWhile{r < R}{} \\
\quad\quad \Assn{n}{0} \\
\quad\quad \Assn{rem}{0}; \\
\quad\quad \DWhile{n < N}{} \\
\quad\quad\quad \Assn{ct[n]}{ct[n] - [ct[n] > 0]}; \\
\quad\quad\quad \Assn{rem}{rem + [ct[n] > 0]}; \\
\quad\quad\quad \Assn{n}{n + 1}; \\
\quad\quad \Assn{j}{0}; \\
\quad\quad \RWhile{j < rem}{} \\
\quad\quad\quad \Rand{bin[j]}{oh([N])}; \\
\quad\quad\quad \Assn{k}{0}; \\
\quad\quad\quad \RWhile{k < N}{} \\
\quad\quad\quad\quad \Assn{upd}{ct[k] + bin[j][k]}; \\
\quad\quad\quad\quad \Assn{ct[k]}{upd}; \\
\quad\quad\quad\quad \Assn{k}{k + 1}; \\
\quad\quad\quad \Assn{j}{j + 1}; \\
\quad\quad \Assn{n}{0}; \\
\quad\quad \Assn{emptyCt[r]}{0}; \\
\quad\quad \Assn{empty}{isZero(ct)}; \\
\quad\quad \DWhile{n < N}{} \\
\quad\quad\quad \Assn{upd}{emptyCt[r] + empty[n]}; \\
\quad\quad\quad \Assn{emptyCt[r]}{upd}; \\
\quad\quad\quad \Assn{n}{n + 1}; \\
\quad\quad \Assn{r}{r + 1};
\end{array}
\]

Repeated balls-into-bins <cit.>

Larger examples

For our next example, we consider a hashing scheme for a
fully-dynamic dictionary, a space-efficient data structure that supports
insertions, deletions, and membership queries. The top level of the
data structure by <cit.> uses a two-level
hashing scheme: elements are first hashed into a crate, and then hashed
into a pocket dictionary within each crate. As part of the space
analysis of their scheme, <cit.> proves a
high-probability bound on the number of pocket dictionaries that overflow after
a given number of elements are inserted.

We extract the program FDDict in <Ref> from the
scheme in <cit.>. The program models the
insertion of $N$ elements. Each element is first hashed into one of $C$ possible
crates uniformly at random, and then hashed into one of $P$ possible pocket
dictionaries uniformly at random.  The variable $bin[n]$ is a $C$ by $P$ matrix,
with all entries zero except for the entry at $(crate[n], pocket[n])$, which is
set to $1$. Next, the program totals up the number of elements hashing to each
(crate, pocket) pair, storing the result in the $C$ by $P$ matrix $binCt$.
Finally, the program checks which (crate, pocket) pairs have count larger than
some concrete threshold $T_{bin}$ ($over$), and totals up the number of full
pocket dictionaries in each crate ($overCt$).

Our logic can prove a judgment of the following form:

\[
\bigg\{\top\bigg\}
\bigg\{\bigwedge_{\gamma = 0}^C \Pr [ overCt[\gamma] > P \cdot \rho_{bin} + T(\rho_{over}, P) ] \leq \rho_{over}\bigg\} ,
\]

where the logical variables $\rho_{bin}$ and $\rho_{over}$ represents the
parametric overflow properties.  This formalizes a result similar to
<cit.>, which states that except
with probability $\beta$, all crates have at most $T_{over}$ overfull pocket
dictionaries. The core of the proof shows that for every crate index $\gamma$,
the counts $binCt[\gamma][\beta]$ are negatively associated, using the
NegFrame rule as in the array version of the Bloom filter example.
Then, we show that vector $over[\gamma][\beta]$, which indicates whether each
pocket dictionary $\beta$ in crate $\gamma$ is overfull or not, is also
negatively associated. This holds because $over[\gamma][\beta]$ is obtained from
$binCt[\gamma][\beta]$ by applying a monotone function. Furthermore, the count
of overflows $overCt[\gamma]$ is obtained by another monotone function on
$over[\gamma][\beta]$ and thus its entries are also negatively associated.

§.§ Repeated balls-into-bins process

Our final example considers a probabilistic protocol proposed by
<cit.>, implemented as RepeatBIB in
<Ref>. Intuitively, the program implements a repeated
balls-into-bins process. Initially, $N$ balls are distributed among $N$ bins
($ct[n]$). For $R$ rounds, in each round a ball is first removed from every
non-empty bin. Then, the $rem$ removed balls are randomly reassigned to bins.
This process is useful for distributed protocols and scheduling algorithms,
where the balls represent tasks and the bins represent computation nodes.
<cit.> proposed and analyzed this algorithm
(e.g., bounding the maximum load, proving how long it takes for all balls to
visit all bins). We can verify the following lower-bound on the number of empty
bins, analogous to <cit.>:

\[
\Bigg\{N \geq 2 \land \apEq{\sum_{\alpha = 0}^N ct[\alpha]}{N} \Bigg\}
\Bigg\{
\Pr\left[ \bigvee_{\beta = 0}^R (emptyCt[\beta] < N/15 - T(\rho_{empty}, N)) \right] \leq R \cdot \rho_{empty}
\Bigg\}
\]

Two aspects of this program make it more difficult to verify.  First, there is
a loop with a randomized guard: the number of removed balls $rem$ is randomized
quantity. Reasoning about such loops is challenging, because our Loop
rule is not directly applicable and only far weaker rules are available for
loops with general randomized guards.  <cit.>
sidestep this problem by conditioning on the number of balls in each
bin, which also fixes $rem$ to be some value, proving the target property for
every fixed setting, and then combining the proofs together. can
formalize this style of reasoning using the randomized case analysis rule
(RCase) to condition on $rem$'s value, and then apply the
Loop rule; however, the post-condition of RCase must be
closed under mixtures (CM), while independence and negative association are
known not to satisfy this side-condition.  Thus, it is not possible to
prove negative association by first conditioning and then combining. To work
around this second problem, we use a technique from
<cit.> and prove, on each conditional
distribution, a high-probability bound using the Chernoff bound. The
benefit of this approach is that high-probability bounds are CM, so we
can apply RCase to combine the results. In our view, the fact that
can handle this kind of subtle argument involving conditioning is
a strength of our approach.

§ RELATED WORK

*Bunched implications.
The logic of bunched implications (BI) <cit.> is a well-studied
substructural logic. BI has a resource semantics <cit.>, where
states are resources and the separating conjunction combines compatible
resources together. We follow Docherty's uniform presentation and
investigation of BI <cit.>; in particular, our negative
association model relies on Docherty's non-deterministic frame conditions, and
we use his duality-theoretic framework to establish 's metatheory.

*Separation logics.
The first separation logic was developed to verify pointer-manipulating
programs <cit.>. There is long line of work on
separation logic for concurrency, starting
from <cit.> and
continuing to the present day (e.g., <cit.>).

More recently, separation logics have been
developed for probabilistic programs. is an extension of
PSL <cit.>, a separation logic for probabilistic independence.
<cit.> propose DIBI, an extension of BI with a non-commutative
conjunction, and developed a program logic with DIBI assertions that is capable
of proving conditional independence.  <cit.>
propose QSL, a separation logic where assertions have a quantitative
interpretation, and used their logic to verify probabilistic and
heap-manipulating programs. <cit.> develop a separation logic for
relational reasoning about probabilistic programs, using the coupling approach
of pRHL <cit.>.

*Verifying approximate data structures and applying concentration bounds.
Bloom filters are a data structure supporting approximate membership
queries (AMQs). Ceramist <cit.> is a recent
framework for verifying hash-based AMQ structures in the Coq theorem prover.
Besides handling Bloom filters, Ceramist supports subtle proofs of correctness
for many other AMQs. Compared with our approach, Ceramist proofs are more
precise but also more intricate, applying theorems about Stirling numbers to
achieve a precise bound on the false positive probability.  In contrast, our
approach reasons about negative dependence to achieve a substantially simpler
proof, albeit with less precise bounds.

Prior works in verification have also applied the Chernoff bound to bound sums
of independent random quantities (e.g., <cit.>). While independence is easier to establish, the negative
association property that we need is more subtle.

*Negative dependence.
There are multiple definitions of negative dependence in the literature, each
with their own strengths and weaknesses. We work with negative association
(NA) <cit.>, because it holds in many
situations where negative dependence should hold and it is closed under various
notions of composition. Recently, the notion of Strong Rayleigh (SR) <cit.>
distribution has been proposed as an ideal definition of negative dependence.
The SR condition satisfies more closure properties than NA does; in particular,
it is preserved under various forms of conditioning. However, SR distributions
have mostly been studied for Boolean variables only, and we do not know if an
analogue of the monotone maps property of NA holds for SR.

Beyond theoretical investigations, negative dependence plays a useful role in
many practical applications. In machine learning, negative dependence can help
ensure diversity in predictions by a
model <cit.>, and fast algorithms are known to
learn and sample from negatively-dependent
distributions <cit.>. In algorithm design, negative
dependence is a useful tool to randomly round solutions of linear programs to
integral solutions <cit.>. Negative dependence can
ensure that certain constraints are satisfied exactly after rounding, while
still allowing concentration bounds to be applied to analyze the quality of the
rounded solution.

§ CONCLUSION AND FUTURE DIRECTION

We introduced , a probabilistic program logic that can reason about
independence and negative association. Assertions in are based on
a novel probabilistic model of , an extension of the logic of Bunched
Implications with multiple separating conjunctions. We demonstrated how to use
to reason about probabilistic hashing schemes, and a repeated
balls-into-bins process. There are several natural directions for future work.

*Other models of , and non-deterministic frames.
The assertion logic was primarily motivated by our NA model, but it is
general enough that we believe there are likely other natural models. Exploring
these directions could allow modeling finer notions of separation, and could
further justify as an interesting logic in its own right. It would also
be interesting to see if there are other models that use a non-deterministic
operator to combine resources, as proposed by <cit.>.

*Verifying negative association for sampling algorithms.
We used NA to analyze probabilistic hashing schemes. Another classical
application of NA is in sampling schemes, which generate a sample from a
target distribution while satisfying certain
constraints <cit.>. NA
samplers are useful in algorithm design <cit.> and
statistics, and it would be interesting to understand how to verify these
programs. Many samplers employ rejection sampling, which is not easily analyzed
in but which could be expressed with an explicit conditioning
operator, as in probabilistic programming
languages <cit.>.

We thank the anonymous reviewers for their helpful feedback and suggestions.
This work benefited from discussions with Simon Docherty. This work was
supported in part by the
GS100000001NSFhttp://dx.doi.org/10.13039/100000001 under
Grant No. GS1000000012035314, GS1000000011943130, GS1000000012040249, GS1000000012040222
and GS1000000012152831.

§ PRELIMINARIES

Say $\mathcal{S} = \{ S_i \mid 1 \leq i \leq N\}$ where $S_i$ are disjoint,
$S = \cup \mathcal{S}$ and $\mu \in \Mem[S]$,

Then, $S_i$ are independent in $\mu$
if and only if for any family of all monotone or all antitone functions
$f_i: \Mem[S_i] \to \mathbb{R}^+$,

\begin{align}
\EE_{x \sim \mu}\left[\prod_{S_i \in \mathcal{S}} f_i (\p_{S_i} x) \right] =  \prod_{S_i \in \mathcal{S}} \EE_{x \in \mu}[f_i (\p_{S_i} x) ].
\label{eq:gpnaindep}
\end{align}

The forward direction is straightforward.
The backward direction needs more careful analysis.
In general, zero correlation does not imply independence,
but here, we have the equality for all family of monotone or antitone functions,
so that suffices for independence.

We prove by induction on $\mathcal{T} = \{ S_i \mid 1 \leq i \leq K\}$ that for any family of $v_i \in \Mem[S_i]$,

\begin{align} \label{eq:gpnainduction}
\mathbb{E}_{x \in \mu} \left[ \left( \bigwedge_{S_i \in \mathcal{T}} \p_{S_i} x = v_i \right) \land \left(\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T}} \p_{S_i} x < v_i \right) \right]
= \prod_{S_i \in \mathcal{T}} \mathbb{E}_{x \in \mu} \left[\p_{S_i} x = v_i\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T}} \mathbb{E}_{x \in \mu}\left[\p_{S_i} x < v_i \right].
\end{align}

Case $|\mathcal{T}| = 1$: Say $\mathcal{T} = \{ S_j \}$.
Since indicator functions $S_i < v_i$ and $S_i \leq v_i$
are both monotonically decreasing,

\begin{align*}
&\mathbb{E}_{x \in \mu} \left[\p_{S_j} x = v_j \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T} } \p_{S_i} x < v_i) \right]\\
&=	\mathbb{E}_{x \in \mu} \left[ \p_{S_j} x \leq v_j \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T} } \p_{S_i} x < v_i) \right]
- \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x < v_j \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T} } \p_{S_i} x < v_i) \right]\\
&=	\mathbb{E}_{x \in \mu} \left[\p_{S_j} x \leq v_j\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T} } \mathbb{E}_{x \in \mu} \left[ \p_{S_i} x < v_i\right]
- \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x < v_j \right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T} } \mathbb{E}_{x \in \mu} \left[ \p_{S_i} x < v_i \right] \tag{By~\Cref{eq:gpnaindep}}\\
&= 	(\mathbb{E}_{x \in \mu} \left[ \p_{S_j} x  \leq v_j \right] 	- \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x < v_j \right]) \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T} } \mathbb{E}_{x \in \mu} \left[\p_{S_i} x < v_i \right]\\
&= 	\mathbb{E}_{x \in \mu} \left[ \p_{S_j} x = v_j\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T} } \mathbb{E}_{x \in \mu} \left[\p_{S_i} x < v_i\right]
\end{align*}

Case $|\mathcal{T}| > 1$ Let $S_j$ be an element in $\mathcal{T}$.

\begin{align*}
&\mathbb{E}_{x \in \mu} \left[ (\bigwedge_{S_i \in \mathcal{T}} \p_{S_i} x = v_i ) \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T}} \p_{S_i} x < v_i) \right] \\
&= \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x \leq v_j \land (\bigwedge_{S_i \in \mathcal{T} \setminus \{S_j\} } \p_{S_i} x = v_i) \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T}} \p_{S_i} x < v_i) \right] \\
&- \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x < v_j \land (\bigwedge_{S_i \in \mathcal{T} \setminus \{S_j\} } \p_{S_i} x = v_i ) \land (\bigwedge_{S_i \in \mathcal{S} \setminus \mathcal{T}} \p_{S_i} x < v_i) \right]\\
&= \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x \leq v_j\right] \cdot \prod_{S_i \in \mathcal{T} \setminus \{S_j\} } \mathbb{E}_{x \in \mu} \left[\p_{S_i} x = v_i\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T}} \mathbb{E}_{x \in \mu} \left[\p_{S_i} x < v_i \right] \\
&- \mathbb{E}_{x \in \mu} \left[\p_{S_j} x < v_j\right] \cdot \prod_{S_i \in \mathcal{T} \setminus \{S_j\} } \mathbb{E}_{x \in \mu} \left[\p_{S_i} x = v_i\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T}} \mathbb{E}_{x \in \mu} \left[\p_{S_i} x < v_i \right] \\
&=  \mathbb{E}_{x \in \mu} \left[ \p_{S_j} x = v_j\right] \cdot \prod_{S_i \in \mathcal{T} \setminus \{S_j\} } \mathbb{E}_{x \in \mu} \left[\p_{S_i} x = v_i\right] \cdot \prod_{S_i \in \mathcal{S} \setminus \mathcal{T}} \mathbb{E}_{x \in \mu} \left[\p_{S_i} x < v_i \right]
\end{align*}

When $\mathcal{T} = \mathcal{S}$, <Ref> implies

\begin{align*}
\mathbb{E}_{x \in \mu} \left[ \bigwedge_{S_i \in \mathcal{S}} \p_{S_i} x = v_i\right]
\prod_{S_i \in \mathcal{S}} 	\mathbb{E}_{x \in \mu} \left[ \p_{S_i} x = v_i \right]
\end{align*}

for any $v_i$'s. Thus, components in $\mathcal{S}$ are independent.

§.§ Coarsening

We prove some properties of coarsening.
In the following we will use an alternative definition of coarsening,
which will be shown to be equivalent to what we define in the main text.

We first index any partition $\mathcal{S}$ as $\mathcal{S}_1, \dots, \mathcal{S}_{|\mathcal{S}|}$.
Say $|\mathcal{S}'| = m$, $|\mathcal{S}| = n$.
We say	 $\mathcal{S}'$ coarsens a partition $\mathcal{S}$
there exists a function a $f: [m] \to \mathcal{P}([n])$ such that
1) $\cup_{i \in [m]} f(i) = [n] $;
2) for any $i, j \in [m]$, either $i = j$ or $f(i), f(j)$ are disjoint;
3) $\mathcal{S}' = \{ \cup \{ \mathcal{S}_j \mid j \in f(i)  \} \mid i \in [m] \}$.

Let $\mathcal{S}$, $\mathcal{S}'$ be two partitions. Then $\mathcal{S}'$
coarsens $\mathcal{S}$ according to <Ref> if and
only if $\mathcal{S}'$ coarsens $\mathcal{S}$ according to <Ref> .

We index  $\mathcal{S}$ as $\mathcal{S}_1, \dots, \mathcal{S}_{n}$ and
$\mathcal{S}'$ as $\mathcal{S}'_1, \dots, \mathcal{S}'_{|m|}$ .

Backward direction:
By that definition, we know
a) for any $\mathcal{S}'_i \in \mathcal{S}'$, $\mathcal{S}'_i = \cup \mathcal{R}$ for some $\mathcal{R} \subseteq \mathcal{S}$;
b) $\cup \mathcal{S} = \cup \mathcal{S}'$.

We define the function $g: [m] \to \mathcal{P}([n])$ as
$g(i) = \{j \mid \mathcal{S}_j \subseteq \mathcal{S}'_i\}$.
This $g$ would satisfies all the conditions required:

* By substitution, $\cup_{i \in [m]} g(i) =  \cup_{i \in [m]} \{j \mid \mathcal{S}_j \subseteq \mathcal{S}'_i\} = \cup_{s' \in \mathcal{S}'}\{j \mid \mathcal{S}_j \subseteq s'\} $.
By b), for any $j \in [n]$, $\mathcal{S}_j \subseteq \cup \mathcal{S}'$.
Then by a) and that $\mathcal{S}$ is a partition,	if $s'$ covers any of $\mathcal{S}_j$, it must
covers all of $\mathcal{S}_j$,
then $\mathcal{S}_j \subseteq \cup \mathcal{S}'$ implies there exists $s' \in \mathcal{S}'$ such that $\mathcal{S}_j \subseteq s'$.
Thus, $j \in  \{j \mid \mathcal{S}_j \subseteq s'\} \subseteq \cup_{s' \in \mathcal{S}'}\{j \mid \mathcal{S}_j \subseteq s'\} $.
For any $j \not\in [n]$, $\mathcal{S}_j$ is undefined,
so it is impossible that $\mathcal{S}_j \subseteq s'$ for some $s' \subseteq \mathcal{S}'$.
Therefore, $\cup_{s' \in \mathcal{S}'}\{j \mid \mathcal{S}_j \subseteq s'\} = [n]$.

For any $k \in g(i)$, $\mathcal{S}_k \subseteq \mathcal{S}'_i$.
If $i \neq j$, then $\mathcal{S}'_i $ and $\mathcal{S}'_j$ are disjoint since $\mathcal{S}'$ is a partition.
Thus, $\mathcal{S}_k \not\subseteq \mathcal{S}'_j$, and $k \not\in g(j)$.
So for any $i \neq j$, $g(i), g(j)$ are disjoint.

* By substitution,

\begin{align*}
\{ \cup \{ \mathcal{S}_j \mid j \in g(i)  \} \mid i \in [m] \}
&=  \{ \cup \{ \mathcal{S}_j \mid \mathcal{S}_j \subseteq \mathcal{S}'_i  \} \mid i \in [m] \}
&=  \{ \cup \{ \mathcal{S}_j \mid \mathcal{S}_j \subseteq s' \} \mid s' \in \mathcal{S}' \}
\end{align*}

Again, by a) and that $\mathcal{S}$ is a partition, if $s' \in \mathcal{S}$ covers any part of of $\mathcal{S}_j$, it must
covers all of $\mathcal{S}_j$, so  $\cup \{ \mathcal{S}_j \mid \mathcal{S}_j \subseteq s' \}  = s'$.
Thus, $\{ \cup \{ \mathcal{S}_j \mid \mathcal{S}_j \subseteq s' \} \mid s' \in \mathcal{S}' \} =\mathcal{S}'$.

Forward direction:
By 3), we know that  $\mathcal{S}' = \{ \cup \{ \mathcal{S}_j \mid j \in f(i)  \} \mid i \in [m] \}$.
So for any $\mathcal{S}'_i \in \mathcal{S}'$, we have $s' = \cup \{ \mathcal{S}_j \mid j \in f(i)  \} $, which is a subset of $\mathcal{S}'$ by construction. So we proved a).
Also, $\cup \mathcal{S}' = \cup \{ \cup \{ \mathcal{S}_j \mid j \in f(i)  \} \mid i \in [m] \}
= \cup \{ \mathcal{S}_j \mid j \in f(i)  \mid i \in [m] \} $,
and by 1), that is equivalent to
$\cup \{ \mathcal{S}_j \mid j \in [n] \}  $, which is equivalent to $\cup \mathcal{S}$.

We can prove that coarsening commute with projections.

Given a partition $\mathcal{S} = \{ \mathcal{S}_i \}_i$ and a set $X$,
let $\mathcal{S}_X = \{\mathcal{S}_i \cap X \mid \mathcal{S}_i \in \mathcal{S}\}$.
For any $\mathcal{T}$ coarsening $\mathcal{S}_X$,
there exists a coarsening $\mathcal{S}'$ of $\mathcal{S}$ such that
$\mathcal{T} = \{\mathcal{S}_i \cap X \mid \mathcal{S}_i \in \mathcal{S}'\}$;
conversely, for any $\mathcal{S}'$ coarsening $\mathcal{S}$,
and $\mathcal{S}'_X = \{\mathcal{S}_i \cap X \mid \mathcal{S}_i \in \mathcal{S}'\}$,
we have $\mathcal{S}'_X$ coarsens $\mathcal{S}_X$.

Forward direction:
By <Ref>, there exists a coarsening function $f$ such that

\begin{align*}
\mathcal{T} &= \{ \cup \{ {(\mathcal{S}_X)}_j \mid j \in f(i)  \} \mid i \in [|\mathcal{T}|] \}\\
&= \{ \cup \{ \mathcal{S}_j \cap X \mid j \in f(i)\} \mid i \in [|\mathcal{T}|] \}\\
&= \{ (\cup \{ \mathcal{S}_j \mid j \in f(i)\}) \cap X \mid i \in [|\mathcal{T}|] \}\\
&= \{ S' \cap X \mid S' \in \mathcal{S}' \} \tag{where $\mathcal{S}' = \{\cup \{ \mathcal{S}_j \mid j \in f(i)\} \mid i \in [|\mathcal{T}|]\}$}
\end{align*}

$\mathcal{S}'$ has the same size as $\mathcal{T}$, so
$\mathcal{S}' = \{\cup \{ \mathcal{S}_j \mid j \in f(i)\} \mid i \in [|\mathcal{S}'|]\}$,
and thus $\mathcal{S}'$ coarsens $\mathcal{S}$.

Backward direction:
$\mathcal{S}'$ coarsens $\mathcal{S}$, so there exists a coarsening function $f$ such that

\begin{align*}
\mathcal{S}' &= \{ \cup \{ S_j \mid j \in f(i)\} \mid i \in [|\mathcal{S}'|] \} .
\end{align*}

\begin{align*}
\mathcal{S}'_X &= \{(\cup \{ S_j \mid j \in f(i)\}) \cap X \mid i \in [|\mathcal{S}'|] \} \\
&= \{\cup \{ S_j \cap X \mid j \in f(i)\} \mid i \in [|\mathcal{S}'|] \} \\
&= \{\cup \{ {S_X}_j \mid j \in f(i)\} \mid i \in [|\mathcal{S}'|] \} .
\end{align*}

Therefore, $\mathcal{S}'_X$ coarsens $\mathcal{S}_X$.

§ THE LOGIC

<Ref> gives a Hilbert-style proof system for $\idxset$-BI. If
one erases the subscripts on $\sepand$ and $\sepimp$, then the rules without the
last three form a Hilbert proof system for BI.

P ⊢P

* [right = $\top$]

P ⊢⊤

* [right = $\bot$]

* [right=$\lor$-E]
P ⊢R
Q ⊢R
P Q ⊢R

* [right=$\lor$-I]
P ⊢Q_i
P ⊢Q_1 Q_2

* [right=$\land$-I1]
P ⊢Q
P ⊢R
P ⊢Q R

* [right=$\land$-I2]
Q ⊢R
P Q ⊢R

* [right=$\land$-E]
P ⊢Q_1 Q_2
P ⊢Q_i

* [right=$\rightarrow$-I]
P Q ⊢R
P ⊢Q →R

* [right=$\rightarrow$-E]
P ⊢Q →R
P ⊢Q
P ⊢R

* [right=$\sepimp$]
P _Q ⊢R
P ⊢Q _R

* [right=$\sepimp$-E]
P ⊢Q _R S ⊢Q
P _S ⊢R

* [right=$\sepand$-Unit]

P ⊣⊢P __

* [right=$\sepand$-Conj]
P ⊢R
Q ⊢S
P _Q ⊢R _S

* [right=$\sepand$-Comm]

P _Q ⊢Q _P

* [right= $\sepand$-Assoc]

(P _Q) _R ⊣⊢P _(Q _R)

* [right= $\sepand$-Inclusion]
_1 ≤_2
P __1 Q ⊢P __2 Q

Hilbert system for $\idxset$-BI

Using the -BI rules, we can derive the rule $\textsc{Cut}$:
$P \vdash Q$
$Q \vdash R$
$\land 2$
$P \land Q \vdash R$
$P \vdash Q \rightarrow R$
$P \vdash R$

Let $\idx_1 \leq \idx_2$. For the first rule, it suffices to show that $(P
\sepimp_{\idx_2} Q) \sepand_{\idx_1} P \vdash Q$. By
$\sepand$-Weakening, we have that $(P \sepimp_{\idx_2} Q)
\sepand_{\idx_1} P \vdash (P \sepimp_{\idx_2} Q) \sepand_{\idx_2} P$ so the
result follows from Cut and $\sepimp-\textsc{E}$.

For the second rule, $\sepand_{1}$-Unit implies $ \sepid_{\idx_2} \vdash \sepid_{\idx_2} \sepand_{\idx_1}
\sepid_{\idx_1}$;
$\sepand$-Weakening implies $\sepid_{\idx_2} \sepand_{\idx_1}
\sepid_{\idx_1} \vdash \sepid_{\idx_2} \sepand_{\idx_2} \sepid_{\idx_1}$;
and $\sepand_{2}$-Unit implies $\sepid_{\idx_2} \sepand_{\idx_2} \sepid_{\idx_1} \vdash \sepid_{\idx_1}.$
Then by Cut, we have $ \sepid_{\idx_2} \vdash \sepid_{\idx_1} $

§ THE MODEL OF NEGATIVE DEPENDENCE AND INDEPENDENCE

§.§ A BI model for negative association

Let $S$ denote $\dom(\mu_1)$ and $T$ denote $\dom(\mu_2)$.

For any $\mu \in \mu_1 \oplus_s \mu_2$, we have
$\pi_S \mu = \mu_1$,
$\pi_T \mu = \mu_2$, and $\mu$ satisfies NA.
$\mu$ being NA
implies $\mu$ is $\mathcal{R}$-for any partition $\mathcal{R}$ on
So for any partition $\mathcal{S}$ on $S$, partition $\mathcal{T}$ on $T$,
$\mu$ is $\mathcal{S} \cup \mathcal{T}$-.
Therefore, $\mu \in \mu_1 \oplus \mu_2$.

For any $\mu \in \mu_1 \oplus \mu_2$,
$\pi_S \mu = \mu_1$,
$\pi_T \mu = \mu_2$,
and $\mu$ is $\{S, T\}$-since $\mu_1$ is $\{S\}$-,
$\mu_2$ is $\{T\}$-.
Thus, $\mu \in \mu_1 \oplus_w \mu_2$.

We sketch the conditions, using the notation from the definition:

Let $dom(x) = S, dom(x') = S', dom(y) = T, dom(y') = T'$. We claim that we
can take $z' = \pi_{S' \cup T'} z$. We evidently have $z \sqsupseteq z'$,
and $\pi_{S'} z' = \pi_{S'} \pi_{S} z = x'$ and $\pi_{T'} z' = \pi_{T'}
\pi_T z = y'$.

What remains to show is that $z'$ is $\mathcal{S} \cup \mathcal{T}$-for any $\mathcal{S}$, $\mathcal{T}$
such that $x'$ is $\mathcal{S}$-, $y'$ is $\mathcal{T}$-,
and $(\cup \mathcal{S}) \cap (\cup \mathcal{T}) = \emptyset$.

If $x'$ is $\mathcal{S}$-, then $x$ is $\mathcal{S}$-;
if $y'$ is $\mathcal{T}$-, then $y$ is $\mathcal{T}$-;
then $z \in x \oplus y$ must be $\mathcal{S} \cup \mathcal{T}$-.
Since $z' := \pi_{S' \cup T'} z$, and $(\cup \mathcal{S}) \cup (\cup \mathcal{T}) \subseteq S' \cup T'$, we have $z'$ is $\mathcal{S} \cup \mathcal{T}$-too.
And evidently, $dom(z') = S' \cup T' = dom(x') \cup dom(y')$.
So $z' \in x' \oplus y'$.

Let $dom(x) = R, dom(y) = S, dom(z) = T$. We can assume that these sets
are all disjoint, otherwise there is nothing to prove. We claim that we
can take $s = \pi_{S \cup T} w$.
For any $w$ in $t \oplus z$, $t \in x \oplus y$,
we want to show that $w \in x \oplus s$ and $s \in y \oplus z$.

* For any partition $\mathcal{R}, \mathcal{S}$ such that
$(\cup \mathcal{R})  \cap (\cup \mathcal{S}) = \emptyset$
and $x$ is $\mathcal{R}$-, $s$ is $\mathcal{S}$-.
For set $X \in \Var$,
write $\{ Y \cap X \mid Y \in \mathcal{S}\}$ as $\mathcal{S}_X$.
Then, by <Ref>,
$s$ is $\mathcal{S}$-implies $y$ must be $\mathcal{S}_S$-.
$s$ is $\mathcal{S}$-implies $z$ must be $\mathcal{S}_T$-.

Then, $t \in x \oplus y$ must be $\mathcal{R} \cup (\mathcal{S}_S) $-,
and $w \in t \oplus z$ must be
$\mathcal{R} \cup \mathcal{S}_S \cup \mathcal{S}_T$-.
Note that $\mathcal{S}$ coarsens $\mathcal{S}_S \cup \mathcal{S}_T$
so $w$ is $\mathcal{R} \cup \mathcal{S}_S \cup \mathcal{S}_T$-implies that $w$ is $\mathcal{R} \cup \mathcal{S} $-.

Also, $\pi_{R} w = \pi_R \pi_{R \cup S} w = \pi_R t = x$,
and $dom(w) = R \cup S \cup T = dom(x) \cup dom(s)$.

Hence, $w \in x \oplus s$.

* Note that $x$ is trivially $\{R\}$-.
Then, for any partition $\mathcal{S}, \mathcal{T}$ such that
$R \cap (\cup \mathcal{S})  \cap (\cup \mathcal{T}) = \emptyset$
and $y$ is $\mathcal{S}$-and $z$ is $\mathcal{T}$-,
first $t$ must be $(\{R\} \cup \mathcal{S})$-,
and then $w$ must be $(\{R\} \cup \mathcal{S} \cup \mathcal{T})$-.
By projection, $s = \pi_{S \cup T}$ must be $\mathcal{S} \cup \mathcal{T} z$-.

Also, $\pi_{S} s = \pi_{S} \pi_{S \cup T} w = \pi_S w = \pi_S \pi_{R \cup S} w = \pi_S t = y$,
and similarly, $\pi_T s = z$.
Also, $dom(s) = S \cup T = dom(y) \cup dom(z)$.

Hence, $s \in y \oplus z$.

Unit Existence.
Take $e$ to be $\mu$ where $\mu$ is the (unique) distribution in $\DMem{\emptyset}$.

Unit Closure.
Immediate as we take $E = M$.

Unit Coherence.
Immediate: $x \in y \oplus e$ entails $y = \pi_{dom(y)} x$, which implies $y \sqsubseteq x$.

Given a set of variables $S$, $S$ satisfies NA in $\mu$
iff $\mu$ satisfies $\mathcal{S}$-for any
$\mathcal{S}$ partitioning $S$ iff $\mu$  satisfies $\{ \{s\} \mid s \in S\}$-.

The second equivalence is straightforward:

* $\{\{s\} \mid s \in \mathcal{S} \}$ is a partition of $S$, so we have the backward direction.

* Any $\mathcal{S}$
partitioning $S$ coarsens $\{\{s\} \mid s \in \S \}$, so we have the first direction.

For the forward direction of the first equivalence,
it suffices to prove that for any partition $\mathcal{S}$ of $S$,
any family of all monotone or all antitone functions
$f_i: \Mem[S_i] \to \mathbb{R}^+$

\begin{align}
\mathbb{E}_{x \sim \mu} \left[ \prod_{S_i \in \mathcal{S}} f_i(\p_{S_i} m) \right]
&\leq  \prod_{S_i \in \mathcal{S}} \mathbb{E}_{x \sim \mu} \left[ f_i(\p_{S_i} m) \right].
\end{align}

We prove that by induction on the size of $\mathcal{S}$.

Base case $|\mathcal{S}| = 1$: $\mathcal{S}$-is trivial.

Base case $|\mathcal{S}| = 2$:  $\mathcal{S}$-is straightforward from NA.

Inductive case:
Assuming $\mu$ satisfies $\mathcal{S}$-for any partition
with size less than $K$,
we want to show that $\mu$ satisfies $\mathcal{S}$-for any partition
with size equals to $K$.

Say $\mathcal{S} = \{S_1, \dots, S_K\}$.
For any family of all monotone or all antitone functions
$f_i: \Mem[S_i] \to \mathcal{R}^+$,
either both $ m \mapsto \prod_{i = 1}^{K-1} f_i(\p_{S_i} m)$ and $f_K$ are monotone,
or both $ m \mapsto \prod_{i = 1}^{K-1} f_i(\p_{S_i} m)$ and $f_K$ are antitone.
Thus, by the inductive hypothesis

\begin{align*}
\mathbb{E}_{x \sim \mu} \left[ \prod_{i = 1}^K f_i(\p_{S_i} m) \right]
&\leq	\mathbb{E}_{x \sim \mu} \left[ \prod_{i = 1}^{K - 1} f_i(\p_{S_i} m) \right]
\cdot \mathbb{E}_{x \sim \mu} \left[ f_K(\p_{S_K} m)\right] \\
&\leq  \prod_{i = 1}^{K - 1} \mathbb{E}_{x \sim \mu} \left[ f_i(\p_{S_i} m) \right]
\cdot \mathbb{E}_{x \sim \mu} \left[ f_K(\p_{S_K} m)\right] \\
&=  \prod_{i = 1}^{K} \mathbb{E}_{x \sim \mu} \left[ f_i(\p_{S_i} m) \right] .
\end{align*}

The backward direction of the first equivalence is more involved.
For any two disjoint $A, B \subseteq S$, we know $\mu$ satisfies $\{A, B\}$-,
so for every pair of both monotone or both antitone functions
$f: \Mem[A] \to \mathbb{R}^+$,
$g: \Mem[B] \to \mathbb{R}^+$,

\[
\mathbb{E}_{m \sim \mu} [ f(\p_A m) \cdot g(\p_B m) ]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m) ] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m) ] .
\]

But the problem is to show this inequality when $f, g$ are not both
non-negative. We prove that in three steps:

* If $f, g$ are lower-bounded by $-L$, i.e., $f(x) \geq  -L$
and $g(x) \geq  -L$ for any $x$. Then $x \to f(x) + L$ and
$x \to g(x) + L$ are both non-negative functions.

\begin{align}
\label{eq:PNAeqNA_plusM}
\mathbb{E}_{m \sim \mu} [ (f(\p_A m) + L) \cdot (g(\p_B m) + L) ]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m) + L] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m) + L] .
\end{align}

\begin{align*}
\mathbb{E} [ (f(\p_A m) + L) \cdot (g(\p_B m) + L) ]
&= \mathbb{E} [ f(\p_A m) \cdot g(\p_B m) ]
+ L \cdot \mathbb{E} [ f(\p_A m)]
+  L \cdot \mathbb{E} [ g(\p_B m)] + L^2 \\
\mathbb{E} [ f(\p_A m) + L] \cdot \mathbb{E}[ g(\p_B m) + L]
&=(\mathbb{E} [f(\p_A m)] + L) \cdot (\mathbb{E}[g(\p_B m)] + L) \\
&= \mathbb{E} [ f(\p_A m) ] \cdot \mathbb{E} [g(\p_B m) ]
+ L \cdot \mathbb{E} [ f(\p_A m)]
+  L \cdot \mathbb{E} [ g(\p_B m)]  + L^2 .
\end{align*}

So <Ref> implies that

\begin{align*}
\mathbb{E}_{m \sim \mu} [ f(\p_A m) \cdot g(\p_B m)]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m)] .
\end{align*}

* If the codomain of $f$ or $g$ does not range across both negative and positive numbers,
then we can also prove the desired inequality by applying the monotone convergence theorem
on the result for lower-bounded functions.

* Say $f$ is non-negative and $g$ is non-positive.
For any natural number $n$,  $m \in \Mem[A \cup B]$,
we define $g_n(\p_B m) = \max(g(\p_B m), -n)$,
$h_n(m) = f(\p_A m) \cdot g_n(\p_B m) $.
Then for any $n$, $g_n$ and $h_n$ are lower-bounded non-positive functions;
and for any $m$, $\{g_n(m)\}_{n \in \mathbb{N}}$ is a monotonically decreasing sequence
converging to $g(m)$,
$\{h_n(m)\}_{n \in \mathbb{N}}$ is a monotonically decreasing sequence
converging to $f(\p_A m) \cdot g(\p_B m) $.
By the monotone convergence theorem,

\begin{align*}
\mathbb{E}_{m \sim \mu} f(\p_A m) \cdot g(\p_B m) &= \lim_{n \to \infty} \mathbb{E}_{m \sim \mu} h_n (m) \\
\mathbb{E}_{m \sim \mu} g(\p_B m) &= \lim_{n \to \infty} \mathbb{E}_{m \sim \mu} g_n (\pi_B m).
\end{align*}

By what we proved above, for any $n$, we have

\begin{align*}
\mathbb{E}_{m \sim \mu} [ h_n(m) ]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g_n(\p_B m)]
\end{align*}

Taking that to the limit $n \to \infty$,

\begin{align*}
\lim_{n \to \infty} \mathbb{E}_{m \sim \mu} [ h_n(m) ]
&\leq \lim_{n \to \infty} \left( \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m)] \right) \\
&= \lim_{n \to \infty}  \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \lim_{n \to \infty}  \mathbb{E}_{m \sim \mu} [ g(\p_B m)]
\end{align*}

Therefore, for any distribution $\mu \in \DMem{A \cup B}$,

\begin{align*}
\mathbb{E}_{m \sim \mu} [ f(\p_A m) \cdot g(\p_B m)]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m)] .
\end{align*}

* The case where $f$ is non-positive and $g$ is non-negative is symmetric.

* The case where $f$ and $g$ are both non-positive is also similar.
We will define $f_n(\p_A m) = \max(f(\p_A m), -n)$,  $g_n(\p_B m) = \max(g(\p_B m), -n)$,
$h_n(m) = f_n(\p_A m) \cdot g_n(\p_B m) $. Then we have

\begin{align*}
\mathbb{E}_{m \sim \mu} f(\p_A m) \cdot g(\p_B m) &= \lim_{n \to \infty} \mathbb{E}_{m \sim \mu} h_n (m) \\
\mathbb{E}_{m \sim \mu} g(\p_B m) &= \lim_{n \to \infty} \mathbb{E}_{m \sim \mu} g_n (\pi_B m)\\
\mathbb{E}_{m \sim \mu} f(\p_B m) &= \lim_{n \to \infty} \mathbb{E}_{m \sim \mu} f_n (\pi_A m).
\end{align*}

And the rest follows.

* Now we consider the general case where we only know both $f$ and $g$
are either lower-bounded or upper bounded.

* If both $f$ and $g$ are lower-bounded, reduce to the first case.

* If $f$ is lower-bounded by $L$, $g$ is upper-bounded by $U$,
then we can consider function $f' = f + L$ and $g' = g - U$.
Then $f'$ is non-negative and $g'$ is non-positive, so by step 2, we have

\begin{align*}
\mathbb{E}_{m \sim \mu} [ f'(\p_A m) \cdot g'(\p_B m)]
\leq \mathbb{E}_{m \sim \mu} [ f'(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g'(\p_B m)] .
\end{align*}

By calculations analogous to what we did in step 1, that implies

\begin{align*}
\mathbb{E}_{m \sim \mu} [ f(\p_A m) \cdot g(\p_B m)]
\leq \mathbb{E}_{m \sim \mu} [ f(\p_A m)] \cdot \mathbb{E}_{m \sim \mu} [ g(\p_B m)] .
\end{align*}

* If $f$ is upper-bounded and $g$ is lower-bounded: analogous to above.

* If both $f$ and $g$ are upper-bounded: also, analogous to above.

Thus, $\mu$ satisfies $\{A, B\}$-implies $\mu$ satisfies $(A, B)$-NA.
And therefore, $\mu$ satisfies $\{A, B\}$-for any $A, B \subseteq S$
implies $S$  satisfies strong NA in $\mu$.

§.§ A $\mathbf{2}$-BI model for independence and negative association

The proof that independence implies will use the following lemma.

In a distribution $\mu$, if $\mu$ satisfies $\{S_1, S_2\}$-,
$\mu$ satisfies	$\{T_1, T_2\}$-,
and $S_1 \cup S_2$ is independent from $T_1 \cup T_2$ in $\mu$
then $\mu$ is $\{S_1 \cup T_1, S_2 \cup T_2\}$-.

By the definition of and independence, $S_1, S_2$ are disjoint,
$T_1, T_2$ are disjoint, and $S_1 \cup T_1, S_2 \cup T_2$ are disjoint.
For any monotonically decreasing/increasing functions
$f: \Mem[S_1 \cup T_1] \to \mathbb{R}^+, g: \Mem[S_2 \cup T_2] \to \mathbb{R}^+$,

\begin{align*}
&\mathbb{E}_{m \sim \mu}[f(\p_{S_1 \cup T_1} m) \cdot g(\p_{S_2 \cup T_2} m)] \\
&=\mathbb{E}_{s \sim \pi_{S_1 \cup S_2} \mu} \mathbb{E}_{t \sim \pi_{T_1 \cup T_2}\mu}[f(\p_{S_1} s, \p_{T_1} t) \cdot g(\p_{S_2} s, \p_{T_2} t)] \tag{By independence of $S_1 \cup S_2$ and $T_1 \cup T_2$}\\
&\leq \mathbb{E}_{s \sim \pi_{S_1 \cup S_2} \mu} \left( \mathbb{E}_{t_1 \sim \pi_{T_1} \mu}[f(\p_{S_1} s, t_1)] \cdot  \mathbb{E}_{t_2 \sim \pi_{T_2} \mu} [g(\p_{S_2} s, t_2)]\right) \tag{$\diamondsuit$} \\
&\leq \mathbb{E}_{s_1 \sim \pi_{S_1} \mu} \mathbb{E}_{t_1 \sim \pi_{T_1} \mu}[f(s_1, t_1)] \cdot  \mathbb{E}_{s_2 \sim \pi_{S_2} \mu} \mathbb{E}_{t_2 \sim \pi_{T_2} \mu} [g(s_2, t_2)] \tag{$\heartsuit$} \\
&\leq \mathbb{E}_{m \sim \mu}[f(\p_{S_1 \cup T_1} m)] \cdot \mathbb{E}_{m \sim \mu}[g(\p_{S_2 \cup T_2} m)] \tag{$\clubsuit$}
\end{align*}

where $\diamondsuit$ is because  $\pi_{T_1 \cup T_2} \mu$ is $T_1, T_2$-and $f(\p_{S_1} s, t_1), g(\p_{S_2} s, t_2)$ are both monotonically
decreasing/increasing in $T_1, T_2$; $\heartsuit$ is because $\pi_{S_1 \cup
S_2} \mu$ is $S_1, S_2$-and that $ \mathbb{E}_{t_1 \sim \pi_{T_1}
\mu}[f(\p_{S_1} s, t_1)]$, and $\mathbb{E}_{t_2 \sim \pi_{T_2} \mu}
[g(\p_{S_2} s, t_2)]$  are both monotonically decreasing/increasing in $S_1,
S_2$; $\clubsuit$ is by independence of $S_1$ and $T_1$ and the independence of
$S_2$ and $T_2$ in $\mu$.

Fix $\mathcal{S}$ and $\mathcal{T}$.
Say $\mathcal{S} = \{S_1, \dots, S_p\}$ and $\mathcal{T} = \{T_1, \dots, T_q\} $.  For any
$\mathcal{R}$ coarsening $\mathcal{S} \cup \mathcal{T}$, indexing $\mathcal{S}
\cup \mathcal{T}$ as $\{U_1, \dots, U_{p + q}\}$, indexing $\mathcal{R}$ as
$\{R_1, \dots, R_n\}$, we have:

\begin{align*}
\mathcal{R} = \{ \cup \{ U_j \mid j \in f(i)  \} \mid i \in [n] \} .
\end{align*}

Then, given a family of monotonically increasing/decreasing functions
$g_i: R_i \to \mathbb{R}^{+}$

\begin{align*}
\mathbb{E}_{m \sim \mu} \left[\prod_{R_i \in \mathcal{R}} g_i(\p_{R_i} m)\right]
\mathbb{E}_{m \sim \mu} \left[\prod_{i \in [n]} g_i(\p_{\cup \{U_j \mid j \in f(i)\}} m ) \right].
\end{align*}

For each $i$, $\cup \{U_j \mid j \in f(i)\}$ can be divided into the part in $S$ and the part in $T$. We refer to them as
$S'_i$ and $T'_i$. (Some of $S'_i$ and $T'_i$ may be empty).
Thus, for each $i$,

\begin{align*}
g_i(\p_{\cup \{U_j \mid j \in f(i)\}} m )
&= g_i(\p_{S'_i \cup T'_i} m ) .
\end{align*}

By <Ref>, $\mathcal{S}' = \{S'_1, \dots, S'_n\}$
coarsens $\mathcal{S}$, and $\mathcal{T}' = \{T'_1, \dots, T'_n\}$
coarsens $\mathcal{T}$. So $\mu$ is $\mathcal{S}'$-and

We prove by induction on $k \in [n]$ that

\begin{align*}
\mathbb{E}_{m \sim \mu} \left[\prod_{i \in [k]} g_i(\p_{S'_i \cup T'_i} m ) \right] &\leq \prod_{i \in [k]} \mathbb{E}_{m \sim \mu} \left[g_i(\p_{S'_i \cup T'_i} m )\right] .
\end{align*}

Base case When $k = 1$, trivial.

Inductive case
For $k < n$, assume

\begin{align*}
\mathbb{E}_{m \sim \mu} [\prod_{i \in [k]} g_i(\p_{S'_i \cup T'_i} m )] &\leq \prod_{i \in [k]} \mathbb{E}_{m \sim \mu} [g_i(\p_{S'_i \cup T'_i} m )].
\end{align*}

Note that $\mu$ is $\mathcal{S}'$-implies that
$\mu$ is $\{\cup_{i \in [k]} (S'_i), S'_{k+1}\}$-, and
$\mu$ is $\mathcal{T}'$-implies that $\{\cup_{i \in [k]} (T'_i), T'_{k+1}\}$-NA.
Thus, by <Ref>, $\mu$ is also
$\{\{\cup_{i \in [k]} (S'_i) \cup \{\cup_{i \in [k]} (T'_i) , S'_{k+1} \cup T'_{k+1}\} $-NA.
Also, since all $g_i$ is monotonically increasing (decreasing) and non-negative,
$m \mapsto \prod_{i \in [k]} g_i(m)$ is also a monotonically increasing (decreasing) function from $ \cup_{i \in [k]} S'_i \cup \cup_{i \in [k]} T'_i$ to $\mathbb{R}^+$.

\begin{align*}
\mathbb{E}_{m \sim \mu} [\prod_{i \in [k + 1]} g_i(\p_{S'_i \cup T'_i} m )]
&\leq \mathbb{E}_{m \sim \mu} [\prod_{i \in [k]}g_i(\p_{S'_i \cup T'_i} m )] \cdot \mathbb{E}_{m \sim \mu} [g_{k + 1}(\p_{S'_{k + 1} \cup T'_{k + 1}} m )] \\
&\leq \prod_{i \in [k+1]} \mathbb{E}_{m \sim \mu} [g_i(\p_{S'_i \cup T'_i} m )],
\end{align*}

where the second inequality follows from the inductive hypothesis.

Thus, the desired inequality holds for any $\mathcal{R}$ coarsening $\mathcal{S} \cup \mathcal{T}$ and any family of monotonically increasing (decreasing) functions on $\mathcal{R}$.
Thus, $\mu$ is $\mathcal{S} \cup \mathcal{T}$-.

Let $\mathcal{X}_{i, \idx} = (X_i, \sqsubseteq_i, \oplus_{i, \idx}, E_{i, \idx})$.
For any $i \in \{1, 2\}$, $\idx \in \idxset$, $\mathcal{X}_{i, \idx}$ is a BI frame.

First, for any $\idx \in \idxset$,
we prove that $(X, \sqsubseteq, \oplus_{\idx}, E_{\idx})$ is a BI frame.

Down-Closed. Let $(z_1, z_2) \in (x_1, x_2) \oplus_{\idx} (y_1, y_2)$ with
$(x_1, x_2) \sqsupseteq (x_1', x_2')$ and $(y_1, y_2) \sqsupseteq (y_1', y_2')$.
Then, from the Down-Closed property of $\mathcal{X}_{1, \idx}$ and $\mathcal{X}_{2, \idx}$ respectively,
we have that there exists $z_1'$ and $z_2'$ such that
$z_i \sqsupseteq_i z_i'$ and $z_i' \in x_i' \oplus y_i'$ for $i \in \{1, 2\}$.
Hence $(z_1, z_2) \sqsupseteq (z_1', z_2')$ and $(z_1', z_2') \in (x_1', x_2') \oplus_{\idx} (y_1', y_2')$.

Commutativity. Immediate.

Associativity. Let $(w_1, w_2) \in (t_1, t_2) \oplus_{\idx} (z_1, z_2)$ and $(t_1, t_2) \in (x_1, x_2) \oplus_{\idx} (y_1, y_2)$.
Then for $i \in \{1, 2\}$ there exists $s_i \in y_i \oplus_{i, \idx} z_i$ such that $w_i \in x_i \oplus_{i, \idx} s_i$.
Thus, $(s_1, s_2) \in (y_1, y_2) \oplus_{\idx} (z_1, z_2)$ and $(w_1, w_2) \in (x_1, x_2) \oplus_{\idx} (s_1, s_2)$.

Unit Existence. Immediate.

Unit Closure.
If $(e_1, e_2) \in E_{\idx}$ and $(e_1', e_2') \sqsupseteq (e_1, e_2)$, then $e_i' \in E_{i, \idx}$, so
$(e_1', e_2') \in E_{\idx}$.

Unit Coherence.
Let $(e_1, e_2) \in E_{\idx}$ and $(x_1, x_2) \in (y_1, y_2) \oplus_{\idx} (e_1, e_2)$. Then
$x_i \sqsupseteq_{i} y_i$, which implies that $(x_1, x_2) \sqsupseteq (y_1, y_2)$.

Second, we show
if $\idx \leq \idx' \in \idxset$, then $(\mu_1, \mu_1') \oplus_{\idx} (\mu_2, \mu_2') \subseteq (\mu_1, \mu_1') \oplus_{\idx'} (\mu_2, \mu_2') $:

$\mathcal{X}_1$ and $\mathcal{X}_2$ are frames, so $\idx \leq \idx'$ implies that  $\mu_1 \oplus_{1, \idx} \mu_2 \subseteq_1 \mu_1 \oplus_{1, \idx'} \mu_2 $ and  $\mu_1' \oplus_{2, \idx'} \mu_2' \subseteq_2 \mu_1' \oplus_{2, \idx'} \mu_2'$.
Therefore, $(\mu_1, \mu_1') \oplus_{\idx} (\mu_2, \mu_2') \subseteq (\mu_1, \mu_1') \oplus_{\idx'} (\mu_2, \mu_2') $.

§ PROGRAM LOGIC

§.§ The semantics of

We assume all expressions are well-typed.
We interpret them as $\Mem[\DetVar] \times \Mem[T] \to \Val$, which can be naturally lifted to $\Mem[\DetVar] \times \DMem{T} \to \Dist(\Val)$. For $\sigma \in \Mem[\DetVar]$, $m \in \Mem[T]$,

\begin{align*}
\Sem{x_d} (\sigma, m) &= \sigma(x_d) \\
\Sem{x_r} (\sigma, m) &= m(x_r)  \\
\Sem{[e_1, \dots, e_n]} (\sigma, m) &= [\Sem{e_1}(\sigma, m) , \dots, \Sem{e_n}(\sigma, m) ] \\
\Sem{e + f} (\sigma, m)  &=
\Sem{e}(\sigma, m)  + \Sem{f}(\sigma, m)  &\text{when $\Sem{e}(\sigma, m) $ and $\Sem{f_r}(\sigma, m) $ are numbers} \\
\Sem{e \land f} (\sigma, m) &=
\Sem{e}(\sigma, m)  \land \Sem{f}(\sigma, m)  &\text{when $\Sem{e}(\sigma, m) $ and $\Sem{f_r}(\sigma, m) $ are booleans}
\end{align*}

Let the binary operator $\comb_{\rho}$ takes a convex combination of two distributions, i.e.,
for any $\mu_1, \mu_2 \in \DMem{S}$, for any $x \in \Mem[S]$,

\begin{align*}
\mu_1 \comb_{\rho} \mu_2 (x) \triangleq \rho \cdot \mu_1(x) + (1- \rho) \cdot \mu_2(x).
\end{align*}

Let $\text{Unif}_S$ denotes the uniform distribution on finite set $S$, i.e., $\mu: s \mapsto \frac{1}{|S|}$ for any $s \in S$.