§ INTRODUCTION

Software systems involving probability are pervasive. Such systems naturally
appear in diverse domains such as network reliability
analysis <cit.>, reliability for
cyberphysical systems <cit.>, distributed software
systems <cit.>, and many others.  As these systems are
increasingly deployed in high-consequence domains, there is a growing need for
formal frameworks capable of reasoning about and verifying probabilistic
correctness properties.  We are especially interested in formal frameworks that
support compositional reasoning: putting probabilistic systems together
correctly is a tricky business, as a probabilistic component often makes subtle
assumptions about the distribution of its inputs.  A formal framework for
reasoning about probabilistic systems should facilitate the sound composition of
formal verifications of individual components.

In the traditional non-probabilistic setting, program logics have become
standard kit for compositionally reasoning about heap-manipulating programs at
scale <cit.>.  In particular, separation logic
enables modular reasoning about heap-manipulating
programs <cit.>.
The key to this
modularity is the frame rule,

\begin{align}
\frac{\triple Pex{Q(x)}}{\triple{F*P}ex{F*Q(x)}},
\end{align}

which states that a program $e$ satisfying precondition $P$ and
postcondition $Q$ doesn't interfere with any parts of the heap $F$ (“frames”)
disjoint from parts of the heap described by $P$ <cit.>.  This
facilitates local reasoning, and is the distinctive advantage of using the
substructural separation logic over ordinary predicate logic in reasoning about
pointers. An equivalent specification without separation logic leads to an
unwieldy proliferation of assertions about inequality of locations and
pointer-graph reachability <cit.>.

What is an effective separation logic for probabilistic programs?
In the probabilistic setting, the fundamental source of modularity is
probabilistic independence. Intuitively, two sources of randomness
are independent if knowledge of one does not give any knowledge of the other.
In direct analogy to disjointness of heaps,
independence structure permeates probabilistic programs:
sampling produces a random variable independent of all previously-sampled ones,
and commonly-used subroutines (e.g. randomly initializing an array) generate
multiple mutually-independent outputs.  Just as in the traditional setting,
attempting to write specifications for these procedures in ordinary predicate
logic leads to a proliferation of independence assertions.  A logic for
compositional probabilistic reasoning should compositionally support
independence, in the same way that ordinary separation logic compositionally
supports reasoning about disjoint heaps.

In this paper we present Lilac, a separation logic whose separating conjunction
means probabilistic independence.
Lilac enjoys a frame rule that is identical
to the frame rule of ordinary separation logic; as a consequence, the same
modular reasoning principles used on heap-manipulating programs apply directly
to the probabilistic setting.
Moreover, we prove that Lilac's separating conjunction completely captures
probabilistic independence: all probabilistic independence relationships are
validated by its semantic model (Lemma <ref>).
Both of these points are improvements over prior
work <cit.>,
and are consequences
of our first core contribution: a new combining operation on probability
spaces, analogous to disjoint union of heap fragments in ordinary separation
logic, that serves as the interpretation of separating conjunction.

Our second core contribution is
a modal treatment of conditional probability.
It is common in many probabilistic systems for a property
to only hold conditional on some random variable: for instance, two random
variables might only be independent conditional on a third, a property called
conditional independence.
Conditional reasoning is a second powerful and
prevalent source of modularity:
correctness arguments for probabilistic programs often hinge upon a clever
choice of what to condition on, exploiting key conditional independence
relationships to complete the proof.
Historically, conditional independence has been very difficult to capture in a substructural
program logic: it has either gone unsupported <cit.>
or required a host of new logical connectives and significant changes to the underlying semantic
model <cit.>.
Lilac captures conditioning via the addition of a single modal operator.
Adding support for this conditioning modality doesn't require any changes to
our underlying semantic model beyond restricting ourselves to a class of
suitably-well-behaved probability spaces.
By importing standard theorems of probability theory, we validate a set of derived rules
about the conditioning modality that we argue captures
the informal flavor of conditional reasoning.

In sum, our contributions are as follows:

* We present Core Lilac, a separation logic
whose separating conjunction captures
independence (Lemma <ref>), alongside
proof rules for reasoning
about a simple probabilistic programming language capable
of expressing all of the examples we will consider
(Section <ref>).
Core Lilac's semantic model is based on a novel combining operation
on probability spaces that resembles disjoint union of heap fragments
(Lemma <ref>).

* We extend Core Lilac with a modal operator $\D$
to express conditional reasoning (Section <ref>).
This makes Lilac the first logic that supports
conditioning and continuous random variables in combination with a substructural
treatment of independence.

* We validate the effectiveness of Lilac as a useful tool for program
verification by proving correctness properties of existing examples from the
literature as well as a new challenging example.  Establishing independence
structure is key for proving certain cryptographic protocols correct.
We give Lilac proofs for the one-time pad, private information retrieval, and oblivious
transfer protocols studied by <cit.>
(see Appendix <ref>).
Lilac can also establish conditional independence properties:
we show this by validating the conditional independence properties of
all programs considered by <cit.> (Sections <ref> and <ref>).
Finally, we consider a challenging new example that goes beyond the scope of existing
separation logics.
We validate an intricate reservoir
sampling algorithm that uses continuous random variables and whose correctness
argument depends crucially on conditional independence structure
(Section <ref>).

§.§ A Tour of Lilac

To concretize the discussion, we now present a few simple examples in order to
illustrate how Lilac's separating conjunction encodes independence and how the
conditioning modality can be used to establish simple conditional independence
relationships. In Section <ref> we will give a more involved
example that simultaneously exercises all of the features described here.

First, consider a program <ref> that samples two reals $X,Y$
uniformly from the interval $[0,1]$:

\begin{equation}
\tag{\textsc{unif2}}
\begin{aligned}
\appllet X\appleq\applunif \applin~~
\appllet Y\appleq\applunif \applin~~
\applret (X,Y)
\end{aligned}
\label{prog:unif2}
\end{equation}

We will write all probabilistic programs in monadic style, in a manner similar to Haskell's
do-notation; the keyword $\applret$lifts the value $(X,Y)$ into a
pure monadic computation.
This program satisfies two main properties of interest. First, the outputs $X$ and $Y$ are independent
and distributed as $\unif[0,1]$. Second, as freshly generated
random variables, both $X$ and $Y$ are independent of all other variables.
Both properties are asserted by the following Hoare triple:

\[
\triple{ \top } {\ref{prog:unif2}} {(X,Y)}{X\sim\unif[0,1] ~~*~~ Y\sim\unif[0,1]}
\]

We write $\triple PMX{Q(X)}$ for a program $M$ that satisfies precondition $P$
and produces a random variable $X$ satisfying postcondition $Q(X)$.
In this case, the precondition is the trivial $\top$.
The proposition $X\sim\unif[0,1]$ is a Lilac assertion: it asserts that random variable $X$ is distributed as
This is in direct analogy to the proposition $\ell\mapsto v$ from ordinary separation logic.
Ordinarily, the separating conjunction $(\ell_1\mapsto
v_1)*(\ell_2\mapsto v_2)$ asserts that $\ell_1$ and $\ell_2$ refer to disjoint
heap chunks containing values $v_1$ and $v_2$ respectively.
Analogously, the postcondition $(X\sim\unif[0,1])*(Y\sim\unif[0,1])$ asserts
that $X$ is independent of $Y$ (henceforth written $X \indep Y$) and that both
are distributed as $\unif[0,1]$.
Finally, the frame rule implies $X$ and $Y$ are independent of all other random variables,
expressing the fact that $X$ and $Y$ are freshly generated.

\begin{align*}
&\assert{\{\top\}} \\
&\hspace{1em}\appllet X\appleq\applunif \applin\\
&\assert{\{X\sim \unif[0,1]\}} \\
&\hspace{1em}\appllet Y\appleq\applunif \applin\\
&\assert{\{X\sim \unif[0,1]~~*~~Y\sim\unif[0,1]\}} \\
&\hspace{1em}\applret (X,Y) \\
&\assert{\{(X,Y).~X\sim \unif[0,1]~~*~~Y\sim\unif[0,1]\}}
\end{align*}

Lilac-annotated <ref>.

To establish this postcondition, Lilac provides proof rules that enable
the usual forward-symbolic-execution-style reasoning <cit.>;
we will present these in Section <ref>.
The rule for generating a random variable using $\applunif$ is:

\begin{align*}
\triple\top{\applunif}X{X\sim\unif~[0,1]},\hspace{6cm}
\end{align*}

in direct analogy to the rule for allocating a new reference in ordinary
separation logic. The rules for monadic operators are standard; see rules H-Let
and H-Ret in Figure <ref>. This allows derivations in the Lilac program
logic to be abbreviated
as assertion-annotated programs in the usual way. For
example, the postcondition for <ref> can be established by the
annotation in Figure <ref>.
So far we have not made use of any probability-specific reasoning principles;
a proof analogous to the above could be carried out for a heap-manipulating program that
allocates twice.
Our next example illustrates how Lilac's notion of separation can be used
together with probability-specific proof rules to compute an expectation.
Consider a program <ref> that takes a random variable $X$ as input,
generates a uniform random variable $Y$, and computes their product:

\begin{equation}
\tag{\textsc{halve}}
\begin{aligned}
\ref{prog:halve}(X)
\hspace{1em}:=\hspace{1em}
\big(\appllet Y\appleq \applunif \applin~ \applret XY\big)
\end{aligned}
\label{prog:halve}
\end{equation}

Because $Y$ is freshly generated, $X$ and $Y$ must be independent;
combined with the fact that $Y$ is uniform, we have $\Ex[XY] = \Ex[X]\Ex[Y] =
\Ex[X]/2$.[
$\Ex[X]$ denotes the expectation of the random variable $X$.]
(Hence the name: $\ref{prog:halve}(X)$'s output is half of $X$ in expectation.)
This argument makes use of two key facts:
expectation distributes over the product of independent random variables,
and for $U \sim \unif[0,1]$ we have $\Ex[U] = 1/2$.

We now show how to express this in Lilac.
The claim that <ref> produces a random variable with expectation
$\Ex[X]/2$ can be expressed by:

\begin{align}
\{\own X\}~ \ref{prog:halve}(X) ~\{Z.~\Ex[Z]= \Ex[X]/2 \}
\label{eq:spec-halve}
\end{align}

The postcondition states that the random variable $Z$ produced by <ref>
has expectation $\Ex[X]/2$.
The precondition $\own X$ is a new kind of Lilac assertion: it asserts “probabilistic ownership” of a random variable $X$
but nothing about its distribution.
Probabilistic ownership is in direct analogy to the assertion
$\ell \mapsto -$ of ordinary separation logic, which asserts ownership of
a location $\ell$ in the heap but nothing about the value stored at $\ell$.
Probabilistic ownership allows us to describe independence relationships involving $X$
without knowledge of its distribution.
In particular, the proposition $\own X ~*~ \own Y$ asserts that $X\indep Y$,
just as the proposition $(\ell_1\mapsto -) ~~*~~ (\ell_2\mapsto -)$ asserts
that $\ell_1$ and $\ell_2$ are disjoint locations in ordinary separation logic.
In Section <ref> we will describe precisely what ownership means in this probabilistic context.

\begin{align*}
&1~\,\assert{\{\own X\}} \\
&2~\,\hspace{1em}\appllet Y\appleq\applunif \applin\\
&3~\,\assert{\{\own X~~*~~Y\sim\unif[0,1]\}} \\
&4~\,\hspace{1em}\applret XY \\
&5~\,\assert{\{Z.~\own X~~*~~Y\sim\unif[0,1]~~*~~Z\asequal XY \}} \\
&6~\,\assert{\Big\{Z.~\Big(\Ex[Y] = 1/2 ~~\land~~ \Ex[XY] = \Ex[X]\Ex[Y] \Big)~~*~~Z\asequal XY \Big\}} \\
&7~\,\assert{\{Z.~\Ex[Y] = 1/2 ~~\land~~ \Ex[Z] = \Ex[X]\Ex[Y]\}} \\
&8~\,\assert{\{Z.~\Ex[Z]= \Ex[X]/2 \}}
\end{align*}

Lilac-annotated <ref>.

The annotation in Figure <ref> proves that <ref> meets
the specification in Equation <ref>. The proof proceeds in two
phases. In the first phase, we apply standard proof rules for $\applunif$ and
$\applret$to obtain the assertion on Line .[
Section <ref> describes these rules in detail.] As is standard for
proofs in separation logic, we implicitly apply the frame rule when needed. In
this case, the frame rule guarantees that $\own X$ is preserved across the
invocation of $\applunif$, giving the separating conjunction on
Line .  This formalizes the intuition that $Y$ is freshly
generated, and therefore independent of $X$.  Line  introduces the
proposition $Z\asequal XY$, which asserts that the output $Z$ is almost-surely
equal to the product $XY$. Two random variables $X$ and $Y$ are
almost-surely equal if they are equal with probability $1$ (i.e., $\Pr(X=Y) =
1$); this is the natural notion of equality for random variables.
See Figure <ref> for the semantics of $(\asequal)$.
Note that using separating conjunction to combine this proposition with the
others does not introduce any spurious independence relationships; unlike $\own
X$ or $Y\sim\unif[0,1]$ the proposition $Z\asequal XY$ does not assert ownership
of any random variable.[Section <ref> will
make this precise.] This is in contrast to prior work such as
<cit.>, where almost-sure equality requires ownership
of the variables being compared and, as a result, proofs involving equalities
often require a cumbersome mixing of $(\land)$ and $(*)$.

Lines - finish the proof using proof
rules expressing nontrivial probability-specific reasoning.
Line  applies the proof rules:

\begin{align}
\own X ~~*~~ \own Y &\hspace{1em}\vdash\hspace{1em} \Ex[XY]=\Ex[X]\Ex[Y] \tag{\textsc{Indep-Prod}}\label{eqn:indep-prod}\\
Y \sim \unif[0,1] &\hspace{1em}\vdash\hspace{1em} \Ex[Y] = 1/2  \tag{\textsc{Ex-Unif}}\label{eqn:ex-unif}
\end{align}

to obtain a conjunction of equalities about the expectations of $Y$ and $XY$.
Unlike the proof rules we have considered so far, which are structural in nature and express
standard logical reasoning principles, these rules express probability-specific facts:
<ref> expresses the fact that
expectation distributes over products of independent
random variables, and <ref> expresses the expectation of
the standard uniform distribution.
As probability-specific proof rules, these do not follow from the ordinary laws of separation logic;
instead, they are validated by the probability-specific model that we will
describe in Section <ref>.
Line  uses the almost-sure equality $Z\asequal XY$ to replace all occurrences of
$XY$ with $Z$.
The rest of the proof follows by calculation.

Lilac's conditioning modality
Conditioning is at the heart of probabilistic reasoning, and is central to most
probabilistic arguments. A core goal of Lilac is to facilitate conditional
probability arguments that would be familiar to probability theorists.
Informally, conditioning “[turns a] random event or variable into a
deterministic one, while preserving the random nature of other events and
variables” <cit.>. We capture this intuition
with the conditioning modality “$\D_{x\gets X}P(x)$”, which asserts that
$P(x)$ holds conditional on all possible values $x$
the random variable $X$ can take on. A key feature of this modality is that
standard separation logic assertions have intuitive conditional readings under it;
thus $\D$ lifts statements about unconditional probability to their natural conditional counterparts.
For instance, we have seen that $\own X* \own Y$
asserts that $X \indep Y$, and $\Ex[X] = v$ asserts that $X$ has
expectation $v$.  Accordingly, $\D_{z\gets Z}~~(\own X* \own Y)$ expresses
conditional independence of $X$ and $Y$ given the random variable $Z$,
denoted $X \indep Y \mid Z$, and $\D_{y\gets Y} ~~(\Ex[X]
= v)$ asserts that $X$ has conditional expectation $v$ given $Y$, i.e. $\Ex[X \mid Y] = v$.

Conditional arguments are driven by a careful distinction between random and
deterministic quantities.  We make these distinctions notationally and
semantically explicit in Lilac. We write random expressions as capital letters
$X$; these variables stand for random variables manipulated by a probabilistic
program, and are compared for equality using $(\asequal)$.  Deterministic
(i.e., non-probabilistic) variables are written in lower-case letters $x$, and
are compared for equality using ordinary $(=)$.

Lilac supports familiar ways of transitioning between deterministic and
probabilistic quantities, and typing rules (given in
Section <ref>) govern precisely where random and
deterministic expressions can appear. For instance, $\Ex[X] = v$ asserts
that a random
expression $X$ relates to a deterministic quantity $v$. The conditioning
modality permits arguments
that mediate between the random and the deterministic.
When a probability-theorist says “and now we proceed by conditioning $X$” in a
pen-and-paper proof, we translate this to entering the conditioning modality.
The proposition
$\D_{x\gets X}P(x)$ binds a new deterministic variable $x$ for use in $P(x)$.
Intuitively, the deterministic $x$ represents an arbitrary but non-probabilistic
value that $X$ has been fixed to inside $P$ via conditioning.  This allows
replacing $X$ with $x$ inside $P$. For example, the proposition
\D_{x\gets X} (\Ex[X] = x)
is valid: under $\D_{x\gets X}$, we can replace $X$ with $x$ to get $\Ex[X] = \Ex[x]$,
and $\Ex[x] = x$ because $x$ is deterministic.

This ability to turn random quantities $X$ into deterministic variables $x$
is especially useful because deterministic variables are, generally speaking,  better behaved than
their random counterparts.
In particular, deterministic variables support
case analysis: if $b$ is a deterministic variable
of type $\applkw{bool}$ then
$P[\vtrue/b] \land P[\vfalse/b] \vdash P$.
This allows Lilac to express
a kind of conditional argument by case analysis that is pervasive in probabilistic reasoning.
For example, consider the following program:

\begin{equation}
\tag{\textsc{CommonCause}}
\begin{aligned}
&\appllet Z \appleq \flip~1/2 \applin \quad
\appllet X \appleq \flip~1/2 \applin  \quad
\appllet Y \appleq \flip~1/2 \applin \\
&\appllet A \appleq \applret(X~\applkw{||}~Z) \applin \quad
\appllet B \appleq \applret(Y~\applkw{||}~Z) \applin \\
&\applret (Z, X, Y, A, B)
\end{aligned}
\label{prog:commoncause}
\end{equation}

This program is taken from
Figure 6(a) of <cit.> (and translated into a monadic style),
where it is used as an example of conditional independence structure.
The program computes $A$ and $B$ from mutually-independent boolean random variables $Z,X,Y$
generated by $\flip~1/2$; at exit, we have that $A \indep B \mid Z$.
In <cit.>, this is established via a logic of
“doubly-bunched” implications – an extension of separation logic with an additional
family of substructural connectives for expressing conditional independence.
We will show how Lilac can state and prove this conditional independence without having
to introduce new connectives beyond $\D$.

The conditional independence property $A \indep B \mid Z$ is captured by the following triple:

\[
\{\top\}~~\ref{prog:commoncause}~~\Big\{ (Z,X,Y,A,B).~\D_{z\gets Z} (\own A * \own B) \Big\}
\]

This postcondition can be established as follows.[
Here we prefer to describe the proof as a mixture of prose and Lilac assertions.
Appendix <ref> gives a fully annotated program.]
First, applying rules for $\flip$ and $\applkw{||}$ gives:

\[
Z \sim \ber 1/2 \hspace{0.5em}*\hspace{0.5em}  X\sim\ber 1/2 \hspace{0.5em}*\hspace{0.5em} Y\sim\ber 1/2
\hspace{0.5em}*\hspace{0.5em} A\asequal (X\lor Z) \hspace{0.5em}*\hspace{0.5em} B\asequal (Y\lor Z)
\]

At this point, an informal proof would continue by case analysis on $Z$ as follows.
Because $Z$ is a Boolean value, it can only take on one of two values: $\vtrue$ or $\vfalse$.
First establish $A \indep B \mid Z=\vtrue$.
If $Z=\vtrue$ then $A=B=\vtrue$, and therefore $A \indep B$ because
by definition $\vtrue \indep \vtrue$.
Now establish $A \indep B \mid Z=\vfalse$.
If $Z=\vfalse$ then $A = X$ and $B = Y$. By construction we have $X \indep Y \indep Z$,
since they are all independent $\flip$s.
This mutual independence implies that $X$ and $Y$ remain independent after
conditioning on $Z=\vfalse$. Hence $A \indep B \mid Z=\vfalse$.
This completes the case analysis, so $A\indep B\mid Z$ as desired.

In Lilac, this conditional argument is expressed by introducing the operator $\D_{z\gets Z}$
and performing case analysis on the deterministic $z$.
First, $\D_{z\gets Z}$ is introduced as follows:

\[
\D_{z\gets Z} \hspace{0.7em} \Big(X\sim\ber 1/2 \hspace{0.5em}*\hspace{0.5em} Y\sim\ber 1/2
\hspace{0.5em}*\hspace{0.5em} A\asequal (X\lor Z) \hspace{0.5em}*\hspace{0.5em} B\asequal (Y\lor Z)\Big)
\]

This step formalizes the idea that anything independent of $Z$ continues to be
independent after conditioning. It is justified by an application of the
rule, which we will describe in Section <ref>.

Conditioning on $Z$ allows us to replace
occurrences of the random variable $Z$ with the newly-introduced deterministic $z$:

\begin{align}
\D_{z\gets Z} \hspace{0.7em} \Big(X\sim\ber 1/2 \hspace{0.5em}*\hspace{0.5em} Y\sim\ber 1/2
\hspace{0.5em}*\hspace{0.5em} A\asequal (X\lor z) \hspace{0.5em}*\hspace{0.5em} B\asequal (Y\lor z)\Big)
\label{eq:intermed-entail}
\end{align}

We are done if we can show that (<ref>) entails $\D_{z\gets
Z}(\own A * \own B)$.  At this point we use a key property of $\D$: as a modal
operator, it respects entailment, so we must establish the
$\D$-free entailment:[ That is, if $P\vdash Q$ then
$\D_{x\gets X}P\vdash \D_{x\gets X}Q$.]

\[ {\small{X\sim\ber 1/2 \hspace{0.3em}*\hspace{0.3em} Y\sim\ber 1/2
\hspace{0.3em}*\hspace{0.3em} A\asequal (X\lor z) \hspace{0.3em}*\hspace{0.3em} B\asequal (Y\lor z)
\hspace{0.5em}\vdash\hspace{0.5em} \own A * \own B}.}
\]

Now the rest of the proof follows directly by cases on $z$:
if $z=\vtrue$ then after simplifying we have:

\[ {\small{A\asequal \vtrue \hspace{0.3em}*\hspace{0.3em} B\asequal \vtrue
\hspace{0.5em}\vdash\hspace{0.5em} \own A * \own B},}
\]

which follows from the rule $X\asequal \vtrue \vdash \own X$ specialized to $X=A$ and $X=B$.
On the other hand, if $z=\vfalse$ then we are left (again, after simplifications) with

\[ {\small{A \sim \ber 1/2 \hspace{0.3em}*\hspace{0.3em} B\sim\ber 1/2
\hspace{0.5em}\vdash\hspace{0.5em} \own A * \own B}},
\]

which follows from the rule $X\sim\ber 1/2 \vdash \own X$.

§.§ A Tour of Lilac's Semantic Model

So far we have sketched a system of proof rules for reasoning about probability that would
appear quite intuitive to a probability theorist. However, reasonable-looking
proof rules are only half of the story. To ensure that the rules are sound and
that Lilac propositions have sensible interpretations in terms of existing
probability-theoretic objects, we construct a model that validates the reasoning
principles described in the previous section and grounds them in probability-theory.

Lilac's semantic model is
designed by analogy with mutable state.
The key idea is that probability spaces —
mathematical objects that model random phenomena — behave like heaps.
To make this concrete, consider the following program:

\begin{equation}
\tag{\textsc{flip2}}
\begin{aligned}
\appllet X\appleq \flip~1/2 \applin ~~
\appllet Y\appleq \flip~1/2 \applin ~~
\applret (X,Y)
\end{aligned}
\label{prog:flip2}
\end{equation}

According to the informal semantics for probabilistic programs used in Section <ref>,
this program “generates” two uniformly distributed boolean random variables
$X$ and $Y$.
To make this precise, we need some standard definitions.
A probability space is a tuple $(\Omega,\calF,\mu)$.
The set $\Omega$ is called the sample space.
The set $\calF$, called the $\sigma$-algebra, is a collection of subsets of $\Omega$
that (1) contains the empty set and $\Omega$, and (2)
satisfies closure under countable union and complements.
Elements $E\in\mathcal F$ are events;
events models an observable property of the phenomenon.
The map $\mu : \calF \rightarrow [0,1]$ is a probability measure assigning each
event its probability.
Given a finite set $A$,
an $A$-valued random variable is a map $X:\Omega\to A$ that is $\mathcal F$-measurable,
which means that the set $\{\omega \mid X(\omega) = a\}$ is an event of $\mathcal F$
for all $a\in A$.
Intuitively, a random variable $X$ represents an object of type $A$ that depends
on the random phenomenon modelled by $\Omega$; the measurability condition ensures that
$X$ only depends on observable properties.

To visualize these objects, we will temporarily fix $\Omega$ to be the unit square $[0,1]\times[0,1]$
and $\mu$ to be the function that assigns to each subset of $\Omega$ its area, if possible.
This allows us to draw a probability space $(\Omega,\mathcal F,\mu)$ as a partitioning of the unit square
given by the $\sigma$-algebra $\mathcal F$. For example,
the square $\fullsqlrbig$
depicts a probability space with
$\sigma$-algebra $\mathcal F_{\fullsqlr} :=\{\emptyset,\leftrect,\rightrect,\Omega\}$
and probability measure:

\[
\mu(\emptyset) = 0 \qquad \mu(\leftrect) = 1/2 \qquad \mu(\rightrect) = 1/2 \qquad \mu(\Omega) = 1.
\]

This probability space models a random phenomenon with two events (the blue rectangle
and the orange rectangle), each with equal probability.

For example, one can define a random variable on the space $\fullsqlr$
as follows.
Let $A$ be the set of boolean values $\{\vtrue,\vfalse\}$
and $X : [0,1]\times[0,1]\to\{\vtrue,\vfalse\}$
be a function that sends blue points to $\vtrue$
and orange points to $\vfalse$.
Concretely, $X(\omega_1, \omega_2) = \vtrue$ if $\omega_1 < 1/2$ and $\vfalse$ otherwise.
This is a random variable: the measurability condition is satisfied because
$X^{-1}(\vtrue)=\leftrect\in \mathcal F_{\fullsqlr}$ and $X^{-1}(\vfalse)=\rightrect\in\mathcal F_{\fullsqlr}$.

We now have the machinery necessary to interpret the <ref> example.
The idea is to think of <ref> as carrying along a probability space
as it executes, analogous to how programs with mutable state carry along a heap.
We can visualize execution of <ref> as follows:

\begin{align}
\begin{tabular}{lll}
1&$\appllet X \appleq \flip~1/2 \applin$
& \scalebox{0.5}{${\tikz[baseline=4.5ex]{
\draw (0.8, 2) ellipse (0.9cm and 0.4cm) node[xshift=9] (xT) {$\mathextralarger\vfalse$} node[xshift=-9] (xF) {$\mathextralarger\vtrue$} node[xshift=35] {$\mathextralarger X$};
\draw[fill=blue,opacity=0.25] (0,0) rectangle (0.75,1.5) node[pos=0.5,yshift=18] (l) {};
\draw[fill=orange,opacity=0.25] (0.75,0) rectangle (1.5,1.5) node[pos=0.5,yshift=18] (r) {};
\draw[->, thick] (l) --  (xF);
\draw[->, thick] (r) --  (xT);
}}$ }
\\
\\
2&$\appllet Y \appleq \flip~1/2 \applin$
\scalebox{0.5}{${\tikz[baseline=4.5ex]{
\draw (0.8, 2) ellipse (0.9cm and 0.4cm) node[xshift=9] (xT) {$\mathextralarger\vfalse$} node[xshift=-9] (xF) {$\mathextralarger\vtrue$} node[xshift=35] {${\mathextralarger X}$};
\draw (2.0, 0.8) ellipse (0.4cm and 0.9cm) node[yshift=9] (yT) {$\mathextralarger\vtrue$} node[yshift=-9] (yF) {$\mathextralarger\vfalse$} node[xshift=18] {$\mathextralarger Y$};
\draw[fill=blue,opacity=0.25] (0,0) rectangle (0.75,1.5) node[pos=0.5,yshift=18] (l) {};
\draw[fill=orange,opacity=0.25] (0.75,0) rectangle (1.5,1.5) node[pos=0.5,yshift=18] (r) {};
\node[] (0,0) {} rectangle (1.5,0.75) node[xshift=-4, yshift=-8] (u) {} {};
\node[] (0,1.5) {} rectangle (1.5,0.75) node[xshift=-4, yshift=8] (d) {} {};
\draw[->, thick] (l) --  (xF);
\draw[->, thick] (r) --  (xT);
\draw[->, thick, lightgray] (u) --  (yF);
\draw[->, thick, lightgray] (d) --  (yT);
\scalebox{0.5}{${\tikz[baseline=4.5ex]{
\draw (0.8, 2) ellipse (0.9cm and 0.4cm) node[xshift=9] (xT) {$\mathextralarger \vfalse$} node[xshift=-9] (xF) {$\mathextralarger \vtrue$} node[xshift=35] {${\mathextralarger X}$};
\draw (2.0, 0.8) ellipse (0.4cm and 0.9cm) node[yshift=9] (yT) {$\mathextralarger \vtrue$} node[yshift=-9] (yF) {$\mathextralarger \vfalse$} node[xshift=18] {${\mathextralarger Y}$};
\node[] (0,0) {} rectangle (0.75,1.5) node[pos=0.5,yshift=18] (l) {};
\node[] (0.75,0) {} rectangle (1.5,1.5) node[pos=0.5,yshift=18, xshift=10] (r) {};
\draw[pattern=north west lines] (0,0) rectangle (1.5,0.75) node[pos=0.5,xshift=18] (u) {};
\draw[pattern=dots] (0,1.5) rectangle (1.5,0.75) node[pos=0.5,xshift=18] (d) {};
\draw[->, thick, lightgray] (l) --  (xF);
\draw[->, thick, lightgray] (r) --  (xT);
\draw[->, thick] (u) --  (yF);
\draw[->, thick] (d) --  (yT);
\scalebox{0.5}{${
\tikz[baseline=4.5ex]{
\draw (0.8, 2) ellipse (0.9cm and 0.4cm) node[xshift=9] (xT) {$\mathextralarger\vfalse$} node[xshift=-9] (xF) {$\mathextralarger\vtrue$} node[xshift=35] {${\mathextralarger X}$};
\draw (2.0, 0.8) ellipse (0.4cm and 0.9cm) node[yshift=9] (yT) {$\mathextralarger\vtrue$} node[yshift=-9] (yF) {$\mathextralarger\vfalse$} node[xshift=18] {${\mathextralarger Y}$};
\draw[fill=blue,opacity=0.25] (0,0) rectangle (0.75,1.5) node[pos=0.5,yshift=18] (l) {};
\draw[fill=orange,opacity=0.25] (0.75,0) rectangle (1.5,1.5) node[pos=0.5,yshift=18] (r) {};
\draw[pattern=north west lines] (0,0) rectangle (1.5,0.75) node[pos=0.5,xshift=18] (u) {};
\draw[pattern=dots] (0,1.5) rectangle (1.5,0.75) node[pos=0.5,xshift=18] (d) {};
\draw[->, thick] (l) --  (xF);
\draw[->, thick] (r) --  (xT);
\draw[->, thick] (u) --  (yF);
\draw[->, thick] (d) --  (yT);
\\
3&$\applret (X,Y)$ & ~
\end{tabular}}
\tag{\textsc{Flip2Annot}}
\label{eq:lilac-semantics}
\end{align}

Before Line 1, the probability space has exactly two events,
$\emptyset$ and $\Omega$, with respective probabilities $0$ and $1$.
This is the trivial probability space, analogous to an empty heap.
After the first line is executed two things change:

* Two new events are allocated, forming the blue-orange probability space $\fullsqlr$
we considered earlier.
This is analogous to how $\new$ allocates a fresh memory cell on the heap: probability spaces correspond to heap fragments.

* The $\flip$ operation yields the random variable $X$ we considered earlier that maps blue points to $\vtrue$;
it is depicted by the arrows.
This is analogous to how $\new$ returns the
location of the newly allocated heap cell:
random variables correspond to locations.

Line 2 allocates a second probability space $\fullsqtb$, whose events are the dotted
region $\toprect$ and dashed region $\botrect$, and a new random variable $Y$ that associates dotted
points to $\vtrue$ and dashed points to $\vfalse$; concretely, $Y(\omega_1, \omega_2) = \vtrue$ if
$\omega_2 > 1/2$ and $\vfalse$ otherwise.
There are many other possible alternatives to $\fullsqtb$
and $Y$; we have simply chosen the ones that are easiest to visualize.
This is analogous to how, in heap-manipulating languages, there are many
possible locations in the heap that $\new$ can choose to allocate in.
Ordinarily, the location chosen by $\new$ is also fresh, so that the entire heap
after executing $\new$ is a disjoint union of the old heap and the newly
allocated cell. Analogously, $\flip$ allocates a probability space
probabilistically independent from the old one, so that the entire space
after executing the second $\flip$ is an independent combination of the
old space $\fullsqlr$ and the newly allocated one $\fullsqtb$.
The operator $(\pdot)$ is
our new combining operation on probability
spaces: it has the same algebraic properties as disjoint union of heap fragments
does in ordinary separation logic (Theorem <ref>), and is the heart of
Lilac's notion of separation.
The events of the combined space $\fullsqlrtb$ are generated by the events
of $\fullsqlr$ and $\fullsqtb$;
we give a formal definition in Section <ref>.
The insight that disjoint union of heaps corresponds to independent combinations of
probability spaces underlies Lilac's interpretation of standard separation logic connectives:
in particular, a probability space $\calP$ satisfies assertion $P_1*P_2$
if there exists a “splitting” of $\calP$ into
an independent combination $\calP_1\pdot\calP_2$ such that $\calP_1$ satisfies $P_1$
and $\calP_2$ satisfies $P_2$.

<ref> also illustrates the second key insight that forms the
basis for our model of separation logic: ownership is measurability.  In
Section <ref> we described the proposition $\own X$ as
asserting “probabilistic ownership” of $X$ but no knowledge of its
distribution.  Now we make this
precise: the proposition  $\own X$ holds in probability space $(\Omega, \calF,
\mu)$ when $X$ is $\mathcal F$-measurable.  In
<ref>, $\own X$ holds in the space $\fullsqlr$ because $X$ is
$\calF_{\fullsqlr}$-measurable.  On the other hand, $\own Y$ does not
hold in $\fullsqlr$, because the event $Y^{-1}(\vfalse) = \botrect$ is not
contained in $\calF_{\fullsqlr}$.  Similarly, $\own X$ does not hold in
$\fullsqtb$ because $X^{-1}(\vtrue) = \leftrect\notin\calF_{\fullsqtb}$.  The
grayed-out arrows depict non-measurability in

§ CORE LILAC

Now that we have given informal descriptions of Lilac's proof rules and semantic model,
we now begin the formal development of Core Lilac, a subset of Lilac without
the conditioning modality.
First we will introduce the syntax and
semantics of Core Lilac propositions. Then we present our
combining operation $(\pdot)$ on probability spaces
described in Section <ref>, and show that it behaves like
disjoint union of heaps. Next, we give the semantics of Lilac propositions,
and fix a small PPL capable of expressing the examples presented in the
previous section, called “APPL”.
Finally, we connect  Lilac to APPL by giving proof
rules for reasoning about APPL programs.

§.§ Syntax and Typing of Core Lilac Propositions

\begin{align*}
P,Q ::=~ &\top \mid \bot \mid P \land Q \mid P \lor Q \mid P\to Q \mid
P * Q \mid P\wand Q \mid \nec P \mid \\
&\forall x\ofty S.P \mid \exists x\ofty S. P \mid
\forallrv X\ofty A.P \mid \existsrv X\ofty A.P \mid
E \sim \mu \mid \own E \mid \Ex[E] = e \mid \weakpre(M, X\ofty A. Q)
\end{align*}

Core Lilac syntax. Metavariables $S,T$ range over sets and $A,B$ over
measurable spaces. Metavariables $E, e, M$, and $\mu$ range over
arbitrary measurable maps of a certain type described in Figure <ref>.

\begin{align*}
S&\in\mathbf{Set} & \Gamma &::= \cdot \mid \Gamma,x:S & \sembr{x_1:S_1,\dots,x_n:S_n} &= S_1\times\cdots\times S_n\\
A&\in\mathbf{Meas} & \Delta &::= \cdot \mid \Delta,X:A &\sembr{X_1:A_1,\dots,X_n:A_n} &= A_1\times\cdots\times A_n
\end{align*}

*[right=T-RandE]E ∈Γ→ΔA
*[right=T-DetE]e ∈Γ→A

*[right=T-Det$\forall$]Γ,xS;Δ⊢PΓ;Δ⊢∀xS. P
*[right=T-Rand$\forall$]Γ;Δ,XA⊢PΓ;Δ⊢XA. P

Γμ: A
*[right=T-$\Ex$]Γ;ΔE:  Γe:
Γ;Δ⊢[E] = e
*[right=T-$\asequal$]Γ;ΔE_1:A   Γ;ΔE_2:A
Γ;Δ⊢E_1 E_2

Core Lilac typing rules. Contexts $\Gamma$ contain the types of deterministic
variables and contexts $\Delta$ contain the types of random variables.
Metavariables $E$ range over random expressions and $e$ over deterministic expressions.
We write $\mathcal GA$ for the set of distributions on $A$.

The syntax of Core Lilac propositions is given in Figure <ref>.
It includes the standard intuitionistic and substructural connectives,
plus the probability-specific ones $\own E$, $E\sim\mu$, $\Ex[E]=e$, and $E_1\asequal E_2$
introduced in Section <ref>.
Figure <ref> gives selected typing rules for Core
Lilac.[The full typing rules are in Appendix <ref>.]
The typing judgment has shape $\Gamma; \Delta \vdash P$, where $\Gamma$ is
a context containing the types of deterministic variables and $\Delta$ is a context
containing the types of random variables.
It is defined in terms of auxiliary judgments
$\Gamma;\Delta\vdashrv E : A$ for typing random expressions $E$, which may mention both
deterministic and random variables,
and $\Gamma\vdashdet e : A$ for typing deterministic expressions $e$,
which can only mention deterministic variables,
and $\Gamma;\Delta\vdashprog M : A$ for typing programs.
Since there are two kinds of variables,
there are also two kinds of quantifiers, with typing rules
T-Det$\forall$ and T-Rand$\forall$.

For clarity of presentation the Core Lilac syntax in
Figure <ref> permits reference to arbitrary measurable
spaces in its types and arbitrary measurable functions in its terms,
in a manner similar to <cit.> and
The rule T-RandE characterizes
the kinds of functions allowed as random expressions:
a random expression $E$ has type $A$ in context $(\Gamma; \Delta)$
if it is a $\sembr{\Gamma}$-indexed family of measurable maps
$\sembr{\Delta}\mto A$.
For instance, the following random expressions are all well-typed
via T-RandE because $(+)$ and $\pow--$ are both
measurable functions $\R\times\R\to\R$:

*[]Γ;ΔE_1 :

Γ;ΔE_2 : Γ; ΔE_1 + E_2 :
*[]Γ;ΔE_1 :

Γ;ΔE_2 : Γ; ΔE_1E_2 :

Similarly, T-DetE says a deterministic expression $e$ is well-typed
at $A$ in $\Gamma$ if it is a function $\sembr{\Gamma}\to A$, and
T-Distr says $\mu$ is well-typed at $A$ in context $\Gamma$ if it
is a $\sembr{\Gamma}$-indexed family of distributions;
we write $\calG A$ for the set of distributions on $A$.
Finally, T-Prog says a program $M$ is well-typed in
$\Gamma;\Delta$ if it is a $\sembr{\Gamma}$-indexed family of Markov
kernels — maps $A \mto \giry B$ often used to give semantics to
probabilistic programs <cit.>.

To reason about the behavior of programs we add a weakest precondition modality
in the style of dynamic logic <cit.>.  Intuitively,
$\weakpre(M, X \ofty A.Q)$ asserts that $M$ produces a random variable $X$
satisfying postcondition $Q$. For example, the fact that
<ref> from Section <ref> produces two independent $\ber~1/2$ is stated
$\weakpre(\sembr{\ref{prog:flip2}}, (X,Y).~ X \sim
\ber 1/2 ~~*~~ Y \sim \ber 1/2)$.

§.§ Combining Independent Probability Spaces

Before we present the semantic interpretation of Core Lilac, we first formally
describe our novel combining operation on probability spaces.
As described in
Section <ref>,
this combining operation behaves like disjoint union of heap fragments,
and underlies Lilac's model of separation. Formally, this is captured by the
notion of a Kripke resource monoid <cit.>:

A Kripke resource monoid
is a tuple $(\calM,\plte,\pdot,\bfone)$ where

* $(\calM,\plte)$ is a poset,

* $(\pdot)$ is a partial function $\calM \times \calM \pto \calM$,

* $(\calM,\pdot,\bfone)$ is a partial commutative monoid,

* $(\pdot)$ respects $(\plte)$: if $x\plte x'$ and $y\plte y'$
and $x'\pdot y'$ defined, then $x\pdot y$ defined and $x\pdot y\plte x' \pdot y'$.[This is a specialization of Definition 5.5 from

Intuitively, a KRM models the notion of a resource. The set $\mathcal M$
models the space of possible resources; the ordering $(\sqsubseteq)$ models how a given resource
can evolve over time. The operation $(\pdot)$ models how resources can be combined;
it is partial because not all resources are compatible with each other (e.g.,
overlapping heap fragments).
The choice of $(\pdot)$, which captures the desired notion of separation, determines the
interpretations of the standard separation logic connectives.
Our choice, as foreshadowed in Section <ref>, combines
two independent probability spaces:

Let $(\Omega, \calE,\mu)$ and $(\Omega, \calF,\nu)$ be probability spaces over the
same ambient sample space $\Omega$. A probability space $(\Omega,\calG,\rho)$ is an
independent combination of $(\Omega,\calE,\mu)$ and $(\Omega, \calF,\nu)$
if (1) $\calG$ is the smallest $\sigma$-algebra containing $\calE$ and $\calF$, and (2)
$\rho$ witnesses the independence of $\mu$ and $\nu$ in the sense that
for all $E\in\calE$ and $F\in\calF$ it holds that
$\rho(E\cap F)=\mu(E)\nu(F)$ .

Recall the program <ref> from Section <ref>.
In this example the probability space $\fullsqlrtb$ is obtained as an independent
combination of $\fullsqlr$
and $\fullsqtb$.
To show this, the areas of the regions in $\fullsqlrtb$
must be products of intersections of regions in $\fullsqlr$ and $\fullsqtb$.
Consider the events $X^{-1}(\vtrue) = \leftrect$ and $Y^{-1}(\vtrue) = \toprect$.
Both of these events have area $1/2$, and
their intersection $\topleftsq$ – the upper-left quandrant of the
unit square – has area $1/4=(1/2)(1/2)$
as desired; clearly this holds for all quadrants.

To form a resource monoid, the combining operation $(\pdot)$ must be a partial function.
Definition <ref>
relates probability spaces to their independent combinations.
However, it requires a witness $\rho$ of independence; if there
are multiple possible choices for $\rho$, then this relation does not define a partial function.
Thankfully – and somewhat surprisingly – it
is possible to establish the uniqueness of $\rho$ and therefore of independent combinations:

Suppose $(\Omega, \calG,\rho)$ and $(\Omega, \calG',\rho')$ are independent combinations of
$(\Omega, \calE,\mu)$ and $(\Omega, \calF,\nu)$.  Then $\calG = \calG'$ and $\rho=\rho'$.

The proof is concise and relies on an application of the well-known Dynkin
$\pi$-$\lambda$ theorem <cit.>; see
Appendix <ref> for details.
Given Lemma <ref>, we can safely write
$(\calE,\mu)\pdot(\calF,\nu)=(\calG,\rho)$ whenever $(\calG,\rho)$
is an independent combination of $(\calE,\mu)$ and $({\calF},\nu)$,
making $(\pdot)$ a partial function on probability spaces.
In addition to being a partial function, Definition <ref> also
requires that $(\pdot)$ forms a partial commutative monoid and respects a certain ordering
relation. This indeed holds of our model: we take the ordering relation to be
inclusion of probability spaces, analogous to inclusion of heaps used in ordinary (affine) separation logic:

Let $\calM$ be the set of probability spaces over a fixed sample space $\Omega$.
Let $(\pdot)$ be the partial function mapping two probability spaces to their independent
combination if it exists.
Let $(\plte)$ be the ordering such that $(\calF,\mu)\plte(\calG,\nu)$ iff
$\calF\subseteq\calG$ and $\mu=\nu|_\calF$.The tuple $(\calM,\plte,\pdot,\mathbf{1})$ is a Kripke resource monoid,
where $\mathbf{1}$ is the trivial probability space $(\calF_\pmbone,\mu_\pmbone)$
with $\calF_\pmbone=\{\emptyset,\Omega\}$ and $\mu_\pmbone(\Omega) = 1$.

For a distribution $\mu : \calG \rightarrow [0,1]$ and sub-$\sigma$-algebra
$\calF \subseteq \calG$, we write $\mu|_\calF$ for the restriction of
$\mu$ to $\calF$.

The main proof obligation is to establish associativity of $(\pdot)$.
This follows from an application of the $\pi$-$\lambda$ theorem.
The proof is intricate;
for details, see Appendix <ref>.

There is a curious contrast between $(\bullet)$ and the standard definition of independence of $\sigma$-algebras in
probability theory. The
standard notion of independence of two sub-$\sigma$-algebras $\calE, \calF
\subseteq \calG$ with respect to an ambient probability space $(\Omega, \calG,
\rho)$ states that $\rho$ factorizes along $\calE$ and $\calF$: i.e., it says that for all $E \in
\calE, F \in \calF$, it holds that $\rho(E \cap F) = \rho(E)\rho(F)$.  This
definition presupposes the existence of an ambient measure $\rho$ by which the
independence of $\calE$ and $\calF$ can be judged. In contrast, our independent
combination does not require $\rho$.
Instead, Lemma <ref> guarantees
that if any such $\rho$ exists, it is unique.
This observation turns the standard definition into
a partial function on probability spaces with the structure of a partial commutative monoid;
once one has combined $\mu$ and $\nu$ to obtain $\rho$ in this way, our definition
coincides with the standard one.

§.§ Semantics of Lilac Propositions

Having established that independent combination of probability spaces
forms a Kripke resource monoid, we are now ready to present Lilac's semantic model
with it as the foundation.
Figure <ref> gives
Lilac's interpretations of standard separation logic connectives,
along with interpretations of the two kinds of quantifiers.
We describe these familiar rules first.
Figure <ref> gives the probability-specific
rules, which we will discuss after.
Both definitions are parameterized by
an ambient sample space $\Omega$ equipped with a $\sigma$-algebra $\Sigma_\Omega$:
all probability spaces $\calP$ are assumed to contain sub-$\sigma$-algebras of $\Sigma_\Omega$,
and $\rv A$ denotes the set of random variables over $\Omega$.
Because $\Omega$ is fixed throughout, we write probability spaces simply as $(\calF,\mu)$.

Figure <ref> defines
the meaning of propositions.
Each proposition
$\Gamma;\Delta\vdash P$
is interpreted as a set of configurations of the form $(\gamma,D,\calP)$ by the relation $\gamma, D, \calP \models P$.
In ordinary separation logic, configurations are of the form $(s,h)$
where $h$ is a heap and $s$ a substitution associating values to variables.
Here, the probability space $\calP$ plays the role of the heap.
The pair $(\gamma,D)$ plays the role of the substitution;
because Lilac has two kinds of variables — random and deterministic — it
also has two kinds of substitutions: $\gamma\in\sembr\Gamma$ maps each deterministic variable to a value,
and $D\in \rv\sembr\Delta$ maps each random variable to a mathematical random
The last four lines of Figure <ref>
give familiar-looking interpretations of quantifiers.
All other lines are standard for separation logics,
and follow from the fact that $(\pdot)$ forms a Kripke resource monoid.

$\gamma,D,\calP\vDash \top$             always

$\gamma,D,\calP\vDash \bot$             never

$\gamma,D,\calP\vDash P\land Q$         iff        $\gamma,D,\calP\vDash P$ and $\gamma,D,\calP\vDash Q$

$\gamma,D,\calP\vDash P\lor Q$          iff        $\gamma,D,\calP\vDash P$ or $\gamma,D,\calP\vDash Q$

$\gamma,D,\calP\vDash P\to Q$           iff        $\gamma,D,\calP'\vDash P$ implies $\gamma,D,\calP'\vDash Q$ for all $\calP'\sqsupseteq \calP$

$\gamma,D,\calP\vDash P*Q$              iff        $\gamma,D,\calP_P\vDash P$ and $\gamma,D,\calP_Q\vDash Q$ for some
$\calP_P\pdot\calP_Q\plte \calP$

$\gamma,D,\calP\vDash P\wand Q$         iff        $\gamma,D,\calP_P\vDash P$ implies
$\gamma,D,\calP_P\pdot\calP\vDash Q$ for all $\calP_P$ with $\calP_P\pdot\calP$ defined

$\gamma,D,\calP\vDash \nec P$           iff        $\gamma,D, \bfone\vDash P$

$\gamma,D,\calP\vDash \forall x\ofty S.P$        iff        $(\gamma,x),D,\calP\vDash P$ for all $x\in S$

$\gamma,D,\calP\vDash \exists x\ofty S.P$        iff        $(\gamma,x),D,\calP\vDash P$ for some $x\in S$

$\gamma,D,\calP\vDash \forallrv X\ofty A.P$        iff        $\gamma,(D,X),\calP\vDash P$ for all
$X:\rv A$

$\gamma,D,\calP\vDash \existsrv X\ofty A.P$        iff        $\gamma,(D,X),\calP\vDash P$ for some
$X:\rv A$

Semantics of basic Lilac connectives.

$\gamma,D,(\calF,\mu)\vDash \own E$                 iff      $E(\gamma)\circ D$ is $\calF$-measurable

$\gamma,D,(\calF,\mu)\vDash E\sim \mu'$            iff      $E(\gamma)\circ D$ is $\calF$-measurable and
&\omega\gets \mu;\\
&\ret (E(\gamma)(D(\omega)))

$\gamma,D,(\calF,\mu)\vDash \Ex[E] = e$        iff      $E(\gamma)\circ D$ is $\calF$-measurable and
$\Ex_{\omega\sim\mu}[E(\gamma)(D(\omega))] = e(\gamma)$

$\gamma,D,(\calF,\mu)\vDash E_1\asequal E_2$        iff      $(E_1(\gamma)\circ D)|_F=(E_2(\gamma)\circ D)|_F$
for some $F\in\calF$ with $\mu(F)=1$

$\gamma,D,\calP\vDash \weakpre(M,X\ofty A.Q)$
iff      for all $\calP_\mathrm{frame}$ and $\mu$
with $\calP_\mathrm{frame}\pdot\calP
\plte(\Sigma_\Omega,\mu)$

and all $D_\textrm{ext}:\rv{\sembr{\Delta_\textrm{ext}}}$

there exists $X:\rv A$ and $\calP'$ and $\mu'$ with
$\calP_\mathrm{frame}\pdot \calP'
\plte(\Sigma_\Omega,\mu')$

such that
&\omega\gets \mu;\\
&v\gets M(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))

and $\gamma,(D,X),\calP'\vDash Q$

Semantics of probability-specific Lilac connectives.

Figure <ref> describes the probability-specific
Lilac connectives.
We start with the first line in the figure, which defines the meaning of ownership.
Following the intuition from Section <ref>, ownership
corresponds to measurability of a random variable with respect to a
particular $\sigma$-algebra. This intuition is made formal here:
the proposition
$\own E$ holds with respect to a configuration $(\gamma,D,(\calF,\mu))$ if
the random variable denoted by the random expression $E$ is $\calF$-measurable.[Formally,
for a probability space $(\Omega, \calF, \mu)$,
a random variable $X : (\Omega, \calF) \rightarrow (A, \mathcal{A})$ is
$\calF$-measurable if for every $E \in \mathcal{A}$
it holds that $X^{-1}(E) \in \calF$.
The expression $E$ can have free variables that are either
random or deterministic. The random variable $E(\gamma) \circ D$ is constructed
by performing
the relevant substitutions:
first all deterministic values are substituted into $E$,
and then the resulting measurable map $E(\gamma)$ is composed
with $D$ to produce a random variable. With this connective in hand, we can
formally relate separating conjunction in Lilac to the familiar
probabilistic notion of independence of random variables:

Fix a configuration $(\gamma,D,\calP)$.
Abbreviate $X_i(\gamma)\circ D$ as $X_i'$. Then,
$\indep_i X'_i$ holds with respect to $\calP$
if and only if $(\gamma,D,\calP) \vDash \hugestar_i \own X_i$.

For a proof, see Appendix <ref>.
Next, proposition $E\sim \mu'$ holds with respect to $(\gamma,D,(\calF,\mu))$ if
$E$ owns $\calF$ and additionally follows distribution $\mu'(\gamma)$, which is the distribution
obtained by substituting the values in $\gamma$ for deterministic variables in the distribution
expression $\mu'$. Throughout this figure, we use Haskell-style notation to
construct distributions using the Giry monad <cit.>; here we use this notation
on the right hand side of the equation for $\mu'(\gamma)$ to construct the
distribution produced by first sampling a value $\omega$ from the ambient probability
measure $\mu$ and then running $E$ on it. Intuitively, this captures the notion
that $\mu'$ is the push-forward of $\mu$ through $E$. The interpretation
of $\Ex[E]=e$ has a similar structure.

The proposition $E_1\asequal E_2$ holds with respect to $(\gamma,D,(\mathcal F,\mu))$
if $E_1$ and $E_2$ are almost-surely equal: formally, we require that there exists some $F\in \calF$
with probability $1$ (i.e., $\mu(F) = 1$) such that the random variables $E_1(\gamma)\circ D$
and $E_2(\gamma)\circ D$ agree on $F$. Note that we do not require $E_1$ or $E_2$ to be
$\calF$-measurable: for $E_1\asequal E_2$ to hold in $\mathcal F$, it need only contain
a single $F$ witnessing the almost-sure equality. This makes $E_1\asequal E_2$
a duplicable proposition,[
As in <cit.>, we say a proposition $P$ is duplicable if $P\vdash P * P$.]
and allows it to be combined with other propositions using separating conjunction without asserting
spurious independence relationships.

The most intricate part of Figure <ref> is the interpretation
of our weakest-precondition modality $\weakpre$.
configurations of the form $(\gamma,D,\calP)$ represent fragments of
a machine state, much like how a configuration $(s,h)$ in ordinary separation logic
represents a fragment of the full heap.
The idea is that $\weakpre(M, X\ofty A.Q)$ should hold in configuration $(\gamma, D, \calP)$
(1) running $M$ with any state
containing fragment $\calP$ produces a new state containing a new
fragment $\calP'$ and a new random variable $X$; (2) the new fragment $\calP'$ satisfies
postcondition $Q$; (3) any fragments $\calP_\textrm{frame}$ independent of $\calP$ are
preserved by $M$, which is necessary to establish a frame rule.
To enforce (1), we quantify over all probability spaces $(\Sigma_\Omega, \mu)$
containing $\calP$ and require that running $M$ in $\mu$
produce a new probability space $(\Sigma_\Omega,\mu')$ containing a new
fragment $\calP'$ and new random variable $X$ whose distribution is equal
to the distribution produced by $M$. To enforce (2),
we require that the new configuration $(\gamma,(D,X),\calP')$ satisfy $Q$.
To enforce (3), we quantify over all possible
“frames” $\calP_\textrm{frame}$, and require that the new space $\mu'$ contain
the exact same frame unchanged.
Finally, in order to prove a fundamental substitution lemma,
we quantify over arbitrary extensions $D_\textrm{ext}$ to the random
substitution $D$; for details on this technical point see Appendix <ref>.

§.§ Syntax and Semantics of APPL

$A,B$     $::=$     $A\times B\mid \boolty \mid \realty \mid A^n \mid \indexty \mid \applgiry A$

$M,N,O$     $::=$     $X\mid \applret M\mid \letin XMN \mid \appltuple{M,N} \mid \applfst~M \mid \applsnd~M \mid$

$\vtrue \mid \vfalse \mid \applite MNO \mid \flip~p \mid r \mid M \oplus N \mid M \prec N \mid \applunif \mid$

$\applarray{M,\dots,M} \mid \applindex MN \mid \applfor n{M_\textrm{init}}iX{M_\textrm{step}}$

APPL syntax. Metavariables $p$ range over probabilities, $r$ over real numbers, and $n$
over natural numbers; $\oplus$ and $\prec$ range over standard arithmetic and comparison

Now we establish a program logic that leverages Core Lilac. We fix a small probabilistic programing language
called APPL capable of expressing the examples in Section <ref>.
The syntax of APPL is given in Figure <ref>.
It is a simply-typed first-order calculus with a sampling operation, immutable arrays, and bounded loops.
It has a simple monadic type-system as in <cit.>.
The important monadic typing rules are:

*[right=T-Unif] Δ:
*[right=T-Ret]ΔM : AΔM:A

Monadic computations have type $\applgiry A$;
the $\applgiry$ stands for the standard Giry monad <cit.>.
The T-Unif rule states that $\applunif$ is a probabilistic computation
producing a real number.

The semantics for APPL are standard and follow <cit.>.
Types $A$ are interpreted as measurable spaces $\sembr{A}$
and typing contexts $\Delta = \{x_1 : A_1, \dots, n_n : A_N\}$
as products $\sembr{\Delta} = \sembr{A_1} \times \cdots \times \sembr{A_n}$.
Programs $\Delta \vdashappl M : \applgiry{} A$ are interpreted as measurable maps
$\sembr{M} : \sembr{\Delta} \mto \calG \sembr{A}$.
The full semantics can be found in Appendix <ref>.

§.§ Reasoning About APPL Programs

*[right=H-Frame $(X\notin F)$]PMXQF*PMXF*Q
*[right=H-Ret] Q[M/X]MXQ
X. QNYR
*[right=H-Uniform] ⊤XX∼ [0,1])
*[right=H-Flip] ⊤ pXX∼p
∀i. XA. I(i,X)MX'I(i+1,X')
P M X Q(X)

X. Q(X) N Y R(EXY)

Selected proof rules for reasoning about APPL programs.

We now show how the semantic model described in the previous section validates
standard proof rules for reasoning about APPL programs.
Using the connectives described in Section <ref>,
we define the meaning of Hoare triples $\triple PMXQ$ in terms of $\weakpre$, following <cit.>.[
Concretely, $\triple PMXQ  ~:=~ \nec (P\wand \weakpre\left(\sembr M,X.\,Q\right))$;
see <cit.> for a detailed explanation.
Then, we use the model described in Section <ref>
to validate the proof rules in Figure <ref>;
these rules justify the annotated programs given in Section <ref>.

The structural rules H-Consequence and H-Frame are completely
standard, as are H-Ret and H-Let.
The rules H-Uniform and H-Flip
specify APPL's sampling operations; they formalize the
intuition that sampling is like allocation. The rule H-For
is a standard proof principle for reasoning about APPL's for-loops:
it states that one can conclude postcondition $I(n+1,X)$
after running a for-loop if an invariant
$I(i,X)$ – a proposition indexed by the loop iteration $i$
and value of the accumulator variable $X$ – holds on entry of the initial accumulator $e$
and is maintained by every loop iteration.
The rule H-If is used to reason about if-then-else.
Unlike in the traditional setting, a probabilistic program can be thought of as taking
both branches of an if-then-else, since it is possible that a Boolean random variable
is both true and false with nonzero probability.
The H-If rule reflects this: it states that, to establish $R(Z)$,
one can first run the $\applthen$-branch to obtain $X$,
and then run the $\applelse$-branch to obtain $Y$,
and then show that $R$ holds of the random variable $(\ite EXY)$
that combines the outcomes of the two branches.

Now we turn our attention to validating these rules with respect to a
suitable model.
Thus far we have been rather abstract about the ambient sample space $\Omega$
underlying Lilac's semantic model.  At this point we make a concrete choice
in order to validate the proof rules in Figure <ref>.  The
soundness of H-Uniform and H-Flip require constructing a new
probability space independent of an existing one.
To ensure that it is always possible to construct such a fresh probability space,
we fix a particular choice of $\Omega$ and restrict our Kripke resource monoid to a class of
probability spaces on $\Omega$ with so-called “finite footprint”; this
guarantees that there is always enough “room” in $\Omega$ for new probability spaces to be allocated.

Specifically, we fix $\Omega$ to be the Hilbert cube $[0,1]^\N$, the collection of infinite streams
of real numbers in the interval $[0,1]$; these infinite streams can be thought of as
infinitely-replenishable randomness sources for use throughout a probabilistic program's execution
A probability space has finite footprint if it only uses finitely-many
dimensions of the Hilbert cube:

A $\sigma$-algebra $\calF$ on $[0,1]^\N$
has finite footprint if there is some finite $n$ such that every $F\in \calF$ is of the form
$F'\times\hilbertcube$ for some $F'\subseteq[0,1]^n$.

Then we restrict our Kripke resource monoid on probability spaces to
only those probability spaces with finite footprint.
With this choice of $\Omega$ and a restriction to suitably-well-behaved probability
spaces in hand, we can validate the above proof rules:

The proof rules in Figure <ref> are sound.

The structural rules, H-Ret, and H-Let follow straightforwardly from unwinding the
definitions of Hoare triples and the interpretations of the logical connectives.
The rule H-For follows by induction on the number of loop iterations.
As foreshadowed, the rules H-Uniform and H-Flip require constructing a
new probability space independent of an existing one; because the existing space
only exhausts some finite $n$ dimensions of the Hilbert cube, we are free to allocate
the new probability space in dimensions $n+1$ and above.
For details see Appendix <ref>.

§ THE CONDITIONING MODALITY

*[lab=C-Entail]P ⊢  Q_xE P ⊢  _xE Q
*[lab=](E) * P  ⊢  _xE P

⊢_xX (E E[x/X] )

_xX ([E] = e)  [e[X/x]] = v
⊢ [E] = v

Selected properties of Lilac's conditioning modality $\D$.

So far we have presented Core Lilac, which defines probabilistic interpretations
of the standard separation logic connectives, along with atomic
propositions for making probability-specific assertions.
Now we describe our
second main contribution: Lilac's modal operator for reasoning
about conditioning. We extend Core Lilac with the proposition
$\D_{x\ofty A\gets E} P$
which states that $P$ holds conditional on the event $E=x$ for all deterministic $x$.
Its typing rule is:

\[
\inferrule*[right=T-$\D$]{\Gamma;\Delta\vdashrv E:A \\ \Gamma,x\ofty A;\Delta\vdash P}
{\Gamma;\Delta\vdash \D_{x\ofty A\gets E} P}
\]

Figure <ref> lists useful laws about $\D$ (proofs are given in
Appendix <ref>).  The rule C-Entail says $\D$ respects
entailment; this allows ordinary logical reasoning to be carried out under $\D$,
automatically lifting statements and proofs about unconditional probability to
the conditional setting. The rule C-Subst captures the intuition that
$X$ can be safely replaced by $x$ under $\D_{x\gets X}$.  The remaining rules
express standard facts about conditioning.  The rule   states that if $P$
holds independent of some random expression $E$, then $P$ also holds conditional
on $E=x$ for any $x$; this acts as a form of introduction rule for $\D$.  The
rule C-Total-Expectation states the Law of Total Expectation, a theorem
of probability theory that relates an unconditional expectation to an
expectation over conditional expectations.  As a rule, it says that, to compute
the expectation of a random expression $E$, one can proceed in two stages:
first, compute the conditional expectation of $E$ given $X=x$, yielding some
deterministic expression $e$ in terms of the conditioned $x$; then, compute the
desired unconditional expectation by putting the random $X$ back into $e$ and
taking the expectation of the resulting expression $e[X/x]$.
Section <ref> will give an example illustrating this
rule's use.

§.§ Semantics of the conditioning modality

The rules stated in Figure <ref> give a powerful and intuitive
framework for reasoning about conditioning that would be familiar to an
experienced probability theorist.
Our goal in this section is to identify a model that validates
these rules.
Intuitively, a model for entering the conditioning modality involves
reasoning under a new conditioned space:
$(\gamma, D, \calP) \vDash \D_{x\ofty A\gets X}P$
holds if for all $x\in A$ there exists some conditioned space $\calP_{X=x}$
such that $\gamma, D, \calP|_{X=x} \vDash P$.
We would like to define $\calP|_{X=x}$ using the standard definition of conditional probability:
let $\calP = (\Omega, \calF, \mu)$ and
define $\calP|_{X=x} = (\Omega, \calF, \mu|_{X=x})$ where
$\mu|_{X=x}(E) = \mu(E \cap \{X=x\})/\mu(\{X=x\})$.
This definition for the conditioned space $\calP|_{X=x}$ is
useful for discrete random variables $X$, where it is
practical to disregard conditioned spaces over null events where $\mu(\{X=x\}) = 0$.
However, if $X$ is a continuous random variable, then by definition $\mu(\{X=x\}) = 0$
for all $x$, so these null events cannot be ignored.

In probability theory, disintegrations were developed in order to resolve
this issue and give a natural notion of conditioned spaces for
continuous random variables <cit.>.
A disintegration for a probability space $\calP$
with respect to a random variable $X$ is defined as a collection
of all conditioned spaces $\{\calP|_{X=x}\}_{x\in A}$ satisfying certain measurability
and concentration properties <cit.>. The existence of a
disintegration for a probability space and random variable is a very strong condition,
and not all probability spaces $\calP$ will have a well-defined
disintegration for all random variables $X$. The study of disintegrations
has formally characterized some of the conditions under which
there exist well-defined notions of disintegration <cit.>.
We leverage
this knowledge here to design a model for $\D$.

Our strategy will be to identify a suitable class of probability spaces that is
both large enough to accommodate all of our design criteria and examples, and
well-behaved enough to admit all reasonable disintegrations.
Our starting point in
this search is the Hilbert cube, the countable product of
unit intervals $[0,1]^\N$. The Hilbert cube is disintegrable with respect to a large
class of random variables (those whose codomain has a well-behaved $\sigma$-algebra):

Let $X : [0,1]^\N \rightarrow (A,\mathcal{A})$ be a random variable and $\calP$ be a
probability space on the Hilbert cube. If $\mathcal{A}$ is countably-generated and contains all
singletons, then there exists a disintegration of $\calP$ with respect to $X$.

The Hilbert cube is a complete separable metric space <cit.>
so any probability measure on it is finite Borel; the result follows from Theorem 1.4 of

The class of spaces $(A,\mathcal{A})$ required by Lemma <ref> includes
many familiar examples, such as $\R^n$, $\N$, and all finite spaces with the usual powerset
Since the Hilbert cube is the sample space $\Omega$ underlying Lilac's semantic model,
this result allows us to disintegrate configurations $(\gamma,D,\calP)$
whenever $\calP$ is a probability space whose $\sigma$-algebra is
exactly the Borel $\sigma$-algebra on the Hilbert cube, and whose measure $\mu$ is correspondingly a
Borel measure. However, our configurations are not quite of this form: $\mu$
may be a probability measure on a sub-$\sigma$-algebra on the Hilbert cube,
and such measures unfortunately cannot in general be extended to a Borel measure <cit.>.
This motivates the next step in our search for suitably-well-behaved probability spaces:

Let $\mathcal{M}_\textrm{Borel}$ be the set of probability spaces on the
Hilbert cube of the form $(\Omega,\calF,\mu)$, where $\mu$ can be extended to
a Borel measure.  The restriction of the KRM given by
Theorem <ref> to $\calM_\textrm{Borel}$ is still a KRM.

A proof of this theorem is in Appendix <ref>.
The upshot of Theorem <ref> is that
configurations of the form $(\gamma,D,\calP)$ where
$\calP\in\calM_\textrm{Borel}$ can be extended to the Hilbert cube, where they
are disintegrable with respect to suitably-well-behaved random variables
following Lemma <ref>.  The final step in our
search is motivated by the desire to validate rule   in
Figure <ref>. The soundness of   requires the ability
to show that a union of negligible sets (a set with measure 0) remains
negligible.  In general this is not the case, so we need to further specialize
our model.  We force these unions to be countable – from which the result
follows straightforwardly from the axioms of probability – by restricting
ourselves to probability spaces with countably-generated
$\sigma$-algebras. Putting this all together yields the final Kripke resource
monoid underlying Lilac's semantic model:

Let $\Mdis$ be the set of countably-generated probability spaces $\calP$ that have finite footprint
and can be extended to a Borel measure on the entire Hilbert cube.
The restriction of the KRM given by Theorem <ref> to $\Mdis$ is still a KRM.

For a proof see Appendix <ref>.
Using Theorem <ref>, we can finally give an interpretation to $\D$:

The following interpretation of $\D_{x\ofty A\gets E}P$ is validates
the rules in Figure <ref>:

$\displaystyle\gamma,D,(\calF,\mu)\vDash \D_{x\ofty A\gets E} P$

for all $(\Sigma_\Omega,\mu')\sqsupseteq (\calF,\mu)$

and all disintegrations of $\mu'$ along $E(\gamma)\circ D$ into $\{\nu_x\}_{x\in A}$,

and almost all $x\in A$, it holds that $(\gamma,x),D,(\calF,\nu_x|_\calP)\vDash P$.

For a detailed proof, see Appendix <ref>.

§ FURTHER EXAMPLES OF APPLYING LILAC

An essential component of evaluating any new program logic is applying it to
validate interesting correctness properties of programs.  Our goal in
this section is to further establish (1) that Lilac can validate examples that
existing probabilistic separation logic approaches can
handle <cit.>; and (2) give an example
that goes beyond these existing approaches.

§.§ Proving a Weighted Sampling Algorithm Correct

To exercise Lilac's support for conditional reasoning, continuous random variables,
and substructural handling of independence, we now prove a sophisticated
constant-space weighted sampling algorithm correct using Lilac.  Suppose
you are given a collection of items $\{x_1, \dots, x_n\}$ each with associated
weight $w_i \in \mathbb{R}^+$.  The task is to draw a sample from the collection
$\{x_i\}$ in a manner where each item is drawn with probability proportional to
its weight. This problem is an instance of reservoir
sampling <cit.>.

\begin{equation*}
\text{\footnotesize $\begin{aligned}
&1~\,\appllet W \appleq \applret\applarray{w_1,\dots,w_n} \applin \\
&2~\,\appllet M \appleq \applret (-\infty) \applin \appllet K \appleq \applret(0)\applin \\
&{\color{gray}\texttt{ // for i from 1 to n with accumulator (M,K),}}\\
&3~\,\applforopen n{\appltuple{M,K}}i{\appltuple{M,K}}{\\
&4~\,\hspace{1em}\appllet S \appleq\applunif \applin \\
&5~\,\hspace{1em}\appllet U \appleq \applret(S\applexp\applpar{1/\applindex Wi})\applin \\
&7~\,\hspace{1em}\applthen~\applret \appltuple{U,i}\\
&8~\,\hspace{1em}\applelse~\applret \appltuple{M,K}}
\applforclose
\end{aligned}$}
\end{equation*}

Constant-space reservoir sampling.

A naive solution might first normalize the weights so that they sum to $1$
and then sample from the resulting probability distribution.
Such an approach is inappropriate for application in large-scale systems: it requires storing
all previously encountered weights and scanning over them before a single sample can be
drawn, and so does not scale to a streaming setting where new weights are acquired
one at a time (for instance, as each user visits a website). To fix this,
<cit.> proposed the
constant-space solution in Figure <ref>.

The core idea is to generate a value $S$ uniformly at random from $[0,1]$ on every
iteration (Line 3), perturb $S$ according to the next weight $w_i$ in the stream
(Line 4), and store only the greatest perturbed sample (Lines 5–8).
It is a surprising fact that this program is equivalent to the naive one.
To prove it, we will establish the postcondition
$\forall k. \Pr(K=k) = w_k/\sum_j w_j$.
First, mechanically applying the rules given in Section <ref>
allows us to conclude the following at exit (for details,
which involve a loop invariant, see Appendix <ref>):

\begin{align}
\existsrv S_1 \dots S_n.~\hugestar_i S_i \sim \mathrm{Unif}~[0,1] ~~*~~
K \asequal \argmax_i S_i^{1/w_i}
\label{eq:post1}
\end{align}

Here $\{S_i\}_i$ are i.i.d. random variables with $S_i$ denoting the value sampled by Line 4 on the $i$th
iteration, and $K$ denotes the final result.
The rest of the proof is devoted to showing that (<ref>) entails the desired postcondition.
Given arbitrary $k$, note that
$\Pr(K=k) = \Pr\big(S_k^{1/w_k} > S_j^{1/w_j} \text{ for all } j \ne k\big)$,
since $K$ is defined to be the $\argmax$ of $j$ over all $S_j^{1/w_j}$.
To make computing this probability tractable, we condition on $S_k$:
fixing $S_k$ to a deterministic $s_k$,

\begin{align}
\Pr(K=k \mid S_k = s_k) &= \Pr\big(s_k^{1/w_k} > S_j^{1/w_j} \text{ for all } j \ne k\big) \label{eq:eqset1:start} \\
&= \Pr\big(s_k^{w_j/w_k} > S_j \text{ for all } j \ne k\big) & \text{Exponentiating} \\
&= \prod_{j \ne k} \Pr\big(s_k^{w_j/w_k} > S_j\big) & \text{By conditional independence} \label{eq:indep-ex}
\end{align}

From Equation <ref> we proceed by calculation.
If $U \sim \unif[0,1]$, then $\Pr(u > U) = u$; this lets
us conclude that
$(\ref{eq:indep-ex}) = \prod_{j \ne k} s_k^{w_j/w_k} = \pow{s_k}{\frac{\sum_{j\ne k} w_j}{w_k}}$.

Formally, this calculation occurs under $\D_{s_k\gets S_k}$, which is introduced via .
The expression $\Pr(E)$ abbreviates $\Ex[\ind[E]]$, the expectation of the indicator random variable $\ind[E]$.[
If $E$ is an event then the random variable $\ind[E]$ is $1$ if $E$ holds and $0$ otherwise.]
The critical step occurs in Equation <ref>:
since $\indep_{j\ne k} S_j \mid S_k$, we can apply:

\begin{align}
\tag{\textsc{Indep-Prod}}
\hugestar_i \own E_i ~~~\vdash~~~ \Pr\Big( \bigcap_i E_i \Big) = \prod_i \Pr(E_i),
} \label{eq:indep-prod}
\end{align}

an immediate consequence of Lemma <ref>.

Finally, to complete the proof we connect the conditional
$\Pr(K=k \mid S_k = s_k)$ to the unconditional $\Pr(K=k)$
using the following instantiation of C-Total-Expectation:

\begin{align*}
\D_{s_k \gets S_k} \Big(\Ex[\underbrace{\ind[K=k]}_{E}]
= \underbrace{\Bigpow{s_k}{\frac{\sum_{j \ne k}{w_j}}{w_k}}}_{e} \Big)
\land
\Big(
\Ex\Big[\underbrace{\mathrm{pow}\Big(S_k, \frac{\sum_{j \ne k} w_j}{w_k} \Big)}_{e[S_k/s_k]}\Big]
\underbrace{\frac{w_k}{\sum_j w_j}}_{v}
\Big)
\Ex[\underbrace{\ind[K=k]}_{E}] = \underbrace{\frac{w_k}{\sum_j w_j}}_{v}
\end{align*}

In the left-hand side of this entailment,
the first conjunct follows from the above
and the second conjunct follows from a calculation.
For a detailed presentation of this proof, see Appendix <ref>.

To sum up, we have shown how Lilac can be used to verify a constant-space weighted sampling
algorithm whose correctness argument requires reasoning about conditional independence
of continuous random variables and imports several important results from probability theory,
including the law of total expectation and key properties of the uniform distribution.
Hopefully, the above example illustrates how Lilac's
substructural handling of independence, modal treatment of conditioning,
and semantic model grounded in familiar constructs from probability theory
allow for easy and natural formalizations of standard informal proofs.

§.§ An Example of Conditional Independence via Control Flow

For this example, we borrow
the <ref> program from Figure 6(b) of
<cit.> (translated into a functional style):

\begin{equation}
\tag{\textsc{CondSamples}}
\begin{aligned}
&\appllet Z \appleq \flip~1/2 \applin \\
&\appllet X_1 \appleq \flip~p \applin \\
&\appllet Y_1 \appleq \flip~p \applin \\
&\applret (Z,X_1,Y_1) \\
\end{aligned}\right)}
&\appllet X_2 \appleq \flip~q \applin \\
&\appllet Y_2 \appleq \flip~q \applin \\
&\applret (Z,X_2,Y_2)
\end{aligned}\right)}
\end{aligned}
\label{prog:condsamples}
\end{equation}

This program produces a tuple $(Z,X,Y)$ with $X$ and $Y$ conditionally independent given $Z$.
The random variables $X$ and $Y$ are sampled from different distributions
depending on the outcome $Z$ of a fair coin flip: if $Z=\vtrue$ then $X$ and $Y$
are Bernoulli random variables with parameter $p$, and if $Z=\vfalse$ then $X$
and $Y$ are Bernoulli random variables with parameter $q$.
The proof of conditional independence, as in the <ref> example,
goes by case analysis on $Z$.

Conditional independence of $X$ and $Y$ given $Z$ is expressed by the following triple:

\[
\lrtriple\top{\ref{prog:condsamples}}{(Z,X,Y)}{\D_{z\gets Z} (\own X * \own Y)}
\]

As usual, the proof begins by mechanically applying proof rules. This yields:

\begin{align*}
&Z \sim \ber 1/2 ~~*~~ \existsrv~X_1~Y_1~X_2~Y_2.~~
\left(\begin{aligned}
&X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p ~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q ~~*~~ \\
&X \asequal (\ite Z{X_1}{X_2}) ~~*~~ Y \asequal (\ite Z{Y_1}{Y_2})
\end{aligned}\right)
\end{align*}

This mechanically-derived postcondition makes use of existential quantification
over random variables, written $\existsrv$, in order to talk about the random
variables produced by the $\applthen$ and $\applelse$ branches.
The subformula $X_1\sim\ber p ~~*~~ Y_1\sim\ber p$ is the postcondition derived
for the $\applthen$ branch, and the subformula
$X_2\sim\ber p ~~*~~ Y_2\sim\ber p$ is the postcondition derived
for the $\applelse$ branch.
The almost-sure equalities $X\asequal (\ite Z{X_1}{X_2})$
and $Y\asequal (\ite Z{Y_1}{Y_2})$
combine the variables produced by the individual branches into the variables $X$ and $Y$
produced by the whole if-then-else.

We now proceed as in the <ref> example.
First, we condition on $Z$ and replace all occurrences of $Z$ with the newly introduced deterministic variable $z$,

\begin{align*}
&\D_{z\gets Z} \hspace{0.5em} \underbrace{\left(\existsrv~X_1~Y_1~X_2~Y_2.~~
\begin{aligned}
&X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p ~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q ~~*~~ \\
&X \asequal (\ite z{X_1}{X_2}) ~~*~~ Y \asequal (\ite z{Y_1}{Y_2})
\end{aligned}\right)}_{P(z)}.
\end{align*}

The goal is to show $\D_{z\gets Z} P(z) \vdash \D_{z\gets Z}(\own X*\own Y)$.
Because $\D$ respects entailment, it suffices to show
$P(z)\vdash \own X * \own Y$.
This follows by a case analysis on $z$.
If $z=\vtrue$ then $P(z)$ can be simplified to $X\sim\ber p ~~*~~ Y\sim\ber p$,
and if $z=\vfalse$ then $P(z)$ can be simplified to $X\sim \ber q ~~*~~ Y\sim \ber q$.
In both cases the simplified form entails $\own X ~~*~~ \own Y$ as desired.
See Appendix <ref> for a fully annotated program.
For more examples of applying Lilac, see Appendix <ref>.

§ DISCUSSION AND FUTURE WORK

In this section we explore various possible extensions to Lilac and
expound on the more subtle consequences of some of the design decisions we made
while validating certain proof rules.

Properties of the conditioning modality
Here we investigate further some formal properties of the conditioning
modality. Specifically, we compare $\D$ to modal necessity $\nec$ <cit.>.
The standard properties of $\nec$ are:

(a) If $\vdash P$ then $\vdash\nec P$ (necessitation).

(d) $\nec P \lor \nec Q \vdash \nec(P\lor Q)$.

(b) $\nec (P\to Q)\vdash \nec P\to\nec Q$ (distribution).

(e) $\nec P\vdash P$ (axiom M).

(c) $\nec (P\land Q)\vdashiff \nec P\land \nec Q$.

(f) $\nec P\vdash \nec\nec P$ (axiom 4).

The modality $\D_{x\gets X}$ satisfies (a)-(d); for proofs see
Appendix <ref>.
The similarity between $\D$ and modal
necessity is somewhat expected, due to the similarity in the logical structure of their
interpretations: $\D_{x\gets X}P$ requires
$P$ to hold in almost-all conditional probability spaces $\calP|_{X=x}$,
similar to how the usual interpretation of $\nec P$ in modal logic requires
that $P$ hold in all reachable worlds.
We are not sure whether
Axiom 4 holds. Axiom M however has a counterexample – this is to be expected, as Axiom M in
standard modal logic says that
what is necessary is the case, whereas we do not expect something that holds conditional on $X=x$ to
hold unconditionally, even if it holds conditional on $X=x$ for all $x$.

Embedding Lilac into Iris
In the future
we would like to embed Lilac in Iris, so that we can take advantage of Iris's
rich support for
reasoning about recursive and higher-order programs, and its
interface for carrying out interactive higher-order separation logic
proofs <cit.>.
To do so requires expressing Lilac's KRM as a camera <cit.>, which is an
algebraic structure similar to a KRM that additionally supports step-indexed reasoning.
One difference between cameras and KRMs is that cameras are not parameterized by
an extra ordering relation: for cameras, $(\plte)$ is implicitly defined to be
relation $x\plte y \Leftrightarrow \exists z. x\pdot z = y$.
However, Lilac's KRM includes ordering relations $\calP\sqsubseteq \calR$
that are not of the form $\calP\pdot\calQ=\calR$ for any $\calQ$.
Therefore, embedding Lilac into Iris would require finding a way to bridge this gap between
KRMs and cameras.
Additionally, a naive adaptation of Lilac's KRM into a camera
would not suffice for increasing its reasoning power:
making use of Iris's support for step-indexed reasoning requires
developing a suitable step-indexed generalization of the KRM in
Theorem <ref>
so that one can talk about equality of probability spaces “up to $k$ steps.”
We leave these problems for future work.

Formal structure of Lilac models In constructing a model for Lilac
that validates our proof rules we made a number of design decisions about what
sort of probability spaces to include. Following <cit.>, it would be
interesting future work to pursue a principled methodology for characterizing
the space of such valid probabilistic models of separation logic. Such a methodolgy
would potentially facilitate future extensions to support probabilistic
languages with more sophisticated features
such as higher-order functions, polymorphism, mutable state, and concurrency.

§ RELATED WORK

Verification of probabilistic programs has a long history going back to
<cit.>. In this section we sketch the broad themes
that are most closely related to program logics for probabilistic
programs. First, we discuss approaches that make use of separation logic.
Then, we discuss alternative approaches to probabilistic program verification,
based on expectations, logical relations, and denotational semantics.

Program Logics for Probability
The most closely related work is the probabilistic separation logic (PSL) introduced
by <cit.>, which gives the
first separation logic where separating conjunction explicitly models
probabilistic independence. Follow-on work extends PSL to support
dependence <cit.> and to settings beyond probabilistic
computation <cit.>. PSL interprets separating
conjunction as a combining operation on distributions over random stores with
disjoint domains, over-approximating the semantic notion of probabilistic
independence with a semi-syntactic criterion on stores.
As a consequence, PSL's notion of independence is linked
to the occurrences of free variables in logical formulas, and so statements
such as $\own (X + Y) * \own (X - Y)$ are inexpressible in PSL
due to the occurrence of the random variables $X$ and $Y$ on both sides
of $*$.
PSL also has a frame rule that imposes a number of extra side-conditions
capturing data-flow properties of the program.
This is in part a consequence of PSL's notion of separation,
and in part because PSL programs are written using mutable variables
whereas we have preferred to work with a purely functional language.
These side-conditions are nontrivial to check and make applying the frame rule
Lilac's frame rule is standard for separation logic, and
Lilac's interpretation of separating conjunction coincides with probabilistic
independence, as demonstrated by Lemma <ref>,
and its semantic model is defined in terms of standard objects of probability theory (i.e.,
probability spaces and random variables).
Moreover, Lilac has support for continuous random variables and a modality for reasoning about
conditioning; all of these features in combination seem difficult to add to PSL
without significant changes to its semantic model.
For those interested in a concrete comparison,
we have validated three of the five examples presented in <cit.>:
one-time pad, private information retrieval, and oblivious transfer;
we do not believe the remaining examples exercise Lilac in ways that go
beyond the ones we verified. Validating these examples required no changes to Lilac's semantic model;
it suffices to extend APPL with support for bitvectors
and to import facts about uniformity and independence via a handful of derived rules.
For details, see Appendix <ref>.

<cit.> extends PSL to handle conditional independence by
extending the standard logic of bunched implications underlying separation logic
with a family of specially-designed connectives
in a new logic called doubly-bunched implications (DIBI). The corresponding
model required for proving soundness of DIBI deviates significantly from the usual model
of separation logic. Lilac handles conditional
independence via the conditioning modality, and this extension does not require
any changes to the standard model beyond the restriction to well-behaved probability
spaces (Theorem <ref>).
a consequence, Lilac behaves very similarly to existing separation logics while
still having facilities for handling conditional independence.
For those interested in a concrete comparison, the <ref>
example presented in Section <ref>
gives a Lilac proof of conditional independence for one of the examples from <cit.>;
Section <ref> gives a description of the other example.

A separate line of probabilistic program logics seeks to verify probabilistic
programs correct without a substructural notion of independence.  An example of
this style of logic is Ellora <cit.>.  In Ellora,
independence is encoded as an assertion about factorization of probabilities.
This is similar to how in program logics without separating conjunction,
aliasing can be ruled out by assertions stating the pairwise-disjointness of
heap locations. This
limited the modularity of Ellora proofs significantly, since independence is
often a key notion in simplifying an argument for correctness.  To address this
limitation Ellora is equipped with the ability to embed logics such as a law
and independence logic, which makes it capable of reasoning about mutual independence
relationships. However, these embedded logics are rather limited:
<cit.> note that the resulting independence logic
cannot handle conditional control flow and that it is more ergonomic to use a
substructural logic to implicitly handle probabilistic independence. This limitation
was a primary motivation for developing PSL.

Another strategy for designing a separation logic for probabilistic programs is
to identify a notion of separation other than probabilistic independence.
<cit.> introduced Polaris, an extension of Iris for
verifying concurrent randomized algorithms.  The goal of Polaris is very
different from Lilac's, and so it makes different design choices.  The notion of
separation in Polaris is the standard one in separation logic enforcing
ownership of disjoint heap fragments. To reason about probability, Polaris
enriches base Iris with the ability to make coupling-style arguments. As a
consequence, Polaris has no substructural treatment of independence or
method for stating facts involving conditioning. Additionally, Polaris does not support continuous random variables.
Yet another way to generalize separation logic to the probabilistic setting
is given by <cit.> who introduced quantitative separation
logic (QSL). QSL generalizes the meaning of assertions: rather than interpreting
assertions as predicates on configurations, i.e. functions from configurations to
Boolean values, QSL interprets predicates as functions from configurations to
expectations. In QSL, separating conjunction does not model independence as
in Lilac or PSL.

Expectation-based approaches
Classically the dominant approach to verifying randomized algorithms has been
expectation-based techniques such as PPDL <cit.> and
pGCL <cit.>. These approaches reason about
expected quantities of probabilistic programs, and design a weakest-pre-expectation
operator that propagates information about expected values backwards
through the program. These methods have been widely-used in practice, verifying
properties such as probabilistic bounds and running-times of
randomized algorithms <cit.>.
However, expectation-based approaches verify a single property about expectations
at a time. As a consequence, verifying multiple interwoven properties of expectations can require
repeated separate verification passes, leading to cumbersome and non-modular proofs.
These limitations in expectation-based approaches were an important motivation
for the development of probabilistic program logics like Ellora <cit.>.

Logical Relations for Probabilistic Programs
A separate method for reasoning about probabilistic programs recasts the
reasoning problem as a relational one, seeking to verify that two programs
are equivalent.
Logical relations are a proof-technique for establishing equivalence of programs,
and recent work has generalized this strategy to the probabilistic
setting <cit.>.
<cit.> and <cit.>
characterize contextual equivalence of a language with higher-order functions,
continuous random variables, and scoring via a biorthogonal logical relation.
<cit.> characterize contextual equivalence of a language that additionally
supports nested queries via a step-indexed biorthogonal logical relation.
These models are all based on an operational semantics defined using the Hilbert cube, and serve as the
inspiration for our use of the Hilbert cube in Lilac's semantic model.
Though logical relations are well-suited for proving the validity of
program rewrite rules, they are less
well-suited for proving intricate post-conditions that can be stated
in a program logic.

Probabilistic Denotational Semantics
An entirely separate method for verifying properties of probabilistic programs
seeks to associate programs with a well-behaved mathematical model and perform all
reasoning in the model. For example, <cit.> gives a
denotational model for validating intuitive commutativity and rewrite rules for
programs by associating them with an appropriate category that witnesses the
correctness of these transformations.
Recently there have been significant developments towards designing
general-purpose models for probabilistic programs that are convenient
for proving various
properties <cit.>.
The drawbacks of using denotational approaches to verify probabilistic
programs are similar to the drawbacks of using denotational approaches for
verifying non-probabilistic programs: extensions to the language often require
drastic changes to the denotational model. Nonetheless there are interesting
connections between Lilac and denotational semantics due to our use of the Giry
monad in giving a semantics to
our $\weakpre$-modality. One possible avenue for future work is to
replace this with a richer domain such as quasi-Borel spaces <cit.> in order to enrich Lilac with
capability for reasoning about higher-order functions.

§ CONCLUSION

Lilac is a probabilistic separation logic with support for
continuous random variables and conditional reasoning
whose interpretation of separating conjunction coincides with the ordinary
notion of probabilistic independence.
The core contributions of Lilac are (1) a novel notion
of separation based on independent combination of probability spaces; and (2) a
modal treatment of conditional probability, which includes a set of proof rules for
reasoning about conditioning that would be intuitive to an
experienced probability theorist.
To demonstrate Lilac, we derived proof rules for reasoning about
a simple probabilistic programming language
and showed how they can be used in combination with Lilac's other features
to prove a sophisticated weighted sampling algorithm correct.
Notably, the derived proof rules mirror those of ordinary separation logic:
rules for sampling resemble the usual rules for allocation,
and our frame rule is completely standard.
Ultimately, we envision Lilac becoming a standard tool
in the toolkit for verifying probabilistic programs. For future work, we
are curious if Lilac can be extended to the quantum programming setting
in a style similar to <cit.>, or if it can
handle the exotic forms of negative dependence studied in <cit.>.

§ ACKNOWLEDGMENTS

We thank the anonymous reviewers for their careful feedback and suggestions.
This work was supported by the National Science Foundation under Grant No.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Bao et al(2021)]
authorpersonJialu Bao, personSimon
Docherty, personJustin Hsu, and personAlexandra
Silva. year2021.
A bunched logic for conditional independence. In
booktitle2021 36th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS). IEEE, pages1–14.

[Bao et al(2022)]
authorpersonJialu Bao, personMarco
Gaboardi, personJustin Hsu, and personJoseph
Tassarotti. year2022.
A separation logic for negative dependence.
journalProceedings of the ACM on Programming
Languages volume6, numberPOPL
(year2022), pages1–29.

[Barthe et al(2018)]
authorpersonGilles Barthe, personThomas
Espitau, personMarco Gaboardi, personBenjamin
Grégoire, personJustin Hsu, and
personPierre-Yves Strub. year2018.
An assertion-based program logic for probabilistic
programs. In booktitleEuropean Symposium on Programming.
Springer, Cham, pages117–144.

[Barthe et al(2019)]
authorpersonGilles Barthe, personJustin
Hsu, and personKevin Liao. year2019.
A Probabilistic Separation Logic.
journalProc. ACM Program. Lang.
volume4, numberPOPL, Article articleno55
(datedec year2019), numpages30 pages.

[Batz et al(2019)]
authorpersonKevin Batz,
personBenjamin Lucien Kaminski, personJoost-Pieter
Katoen, personChristoph Matheja, and personThomas
Noll. year2019.
Quantitative separation logic: a logic for
reasoning about probabilistic pointer programs.
journalProceedings of the ACM on Programming
Languages volume3, numberPOPL
(year2019), pages1–29.

[Biering et al(2007)]
authorpersonBodil Biering, personLars
Birkedal, and personNoah Torp-Smith.
BI-hyperdoctrines, higher-order separation logic,
and abstraction.
journalACM Transactions on Programming Languages and
Systems (TOPLAS) volume29, number5
(year2007), pages24–es.

[Bizjak and Birkedal(2015)]
authorpersonAleš Bizjak and
personLars Birkedal. year2015.
Step-indexed logical relations for probability. In
booktitleFoundations of Software Science and Computation
Structures: 18th International Conference, FOSSACS 2015, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS 2015,
London, UK, April 11-18, 2015, Proceedings 18. Springer,

[Chang and Pollard(1997)]
authorpersonJoseph T Chang and personDavid
Pollard. year1997.
Conditioning as disintegration.
journalStatistica Neerlandica
volume51, number3 (year1997),

[Culpepper and Cobb(2017)]
authorpersonRyan Culpepper and
personAndrew Cobb. year2017.
Contextual equivalence for probabilistic programs
with continuous random variables and scoring. In
booktitleEuropean Symposium on Programming. Springer,

[Distefano et al(2019)]
authorpersonDino Distefano, personManuel
Fähndrich, personFrancesco Logozzo, and
personPeter W O'Hearn. year2019.
Scaling static analyses at Facebook.
journalCommun. ACM volume62,
number8 (year2019), pages62–70.

[Efraimidis and Spirakis(2006)]
authorpersonPavlos S Efraimidis and
personPaul G Spirakis. year2006.
Weighted random sampling with a reservoir.
journalInformation processing letters
volume97, number5 (year2006),

authorpersonMP Ershov.
Extension of measures and stochastic equations.
journalTheory of Probability & Its Applications
volume19, number3 (year1975),

authorpersonTobias Fritz.
A synthetic approach to Markov kernels, conditional
independence and theorems on sufficient statistics.
journalAdvances in Mathematics
volume370 (year2020), pages107239.

[Galmiche et al(2005)]
authorpersonDidier Galmiche, personDaniel
Méry, and personDavid Pym.
The semantics of BI and resource tableaux.
journalMathematical Structures in Computer Science
volume15, number6 (year2005),

[Gehr et al(2018)]
authorpersonTimon Gehr, personSasa
Misailovic, personPetar Tsankov, personLaurent
Vanbever, personPascal Wiesmann, and personMartin
Vechev. year2018.
Bayonet: probabilistic inference for networks.
journalACM SIGPLAN Notices volume53,
number4 (year2018), pages586–602.

authorpersonMichele Giry.
A categorical approach to probability theory.
In booktitleCategorical aspects of topology and
analysis. publisherSpringer, pages68–85.

[Gretz et al(2014)]
authorpersonFriedrich Gretz,
personJoost-Pieter Katoen, and personAnnabelle
McIver. year2014.
Operational versus weakest pre-expectation
semantics for the probabilistic guarded command language.
journalPerformance Evaluation
volume73 (year2014), pages110–132.

[Harel et al(2001)]
authorpersonDavid Harel, personDexter
Kozen, and personJerzy Tiuryn.
Dynamic logic.
In booktitleHandbook of philosophical logic.
publisherSpringer, pages99–217.

[Heunen et al(2017)]
authorpersonChris Heunen, personOhad
Kammar, personSam Staton, and personHongseok
Yang. year2017.
A convenient category for higher-order probability
theory. In booktitle2017 32nd Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS). IEEE, pages1–12.

[Holtzen et al(2021)]
authorpersonSteven Holtzen, personSebastian
Junges, personMarcell Vazquez-Chanlatte, personTodd
Millstein, personSanjit A Seshia, and personGuy
Van den Broeck. year2021.
Model checking finite-horizon Markov chains with
probabilistic inference. In booktitleInternational
Conference on Computer Aided Verification. Springer,

[Ishtiaq and O'Hearn(2001)]
authorpersonSamin S Ishtiaq and
personPeter W O'Hearn. year2001.
BI as an assertion language for mutable data
structures. In booktitleProceedings of the 28th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages.

[Jung et al(2018)]
authorpersonRalf Jung, personRobbert
Krebbers, personJacques-Henri Jourdan,
personAleš Bizjak, personLars Birkedal, and
personDerek Dreyer. year2018.
Iris from the ground up: A modular foundation for
higher-order concurrent separation logic.
journalJournal of Functional Programming
volume28 (year2018).

authorpersonOlav Kallenberg.
booktitleFoundations of modern probability.
Vol. volume2.

[Kaminski et al(2016)]
authorpersonBenjamin Lucien Kaminski,
personJoost-Pieter Katoen, and personChristoph
Matheja. year2016.
Inferring covariances for probabilistic programs.
In booktitleInternational Conference on Quantitative
Evaluation of Systems. Springer, pages191–206.

authorpersonDexter Kozen.
A probabilistic pdl. In
booktitleProceedings of the fifteenth annual ACM symposium
on Theory of computing. pages291–297.

[Krebbers et al(2017)]
authorpersonRobbert Krebbers, personAmin
Timany, and personLars Birkedal.
Interactive proofs in higher-order concurrent
separation logic. In booktitleProceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages.

authorpersonSaul A Kripke.
Naming and necessity.
In booktitleSemantics of natural language.
publisherSpringer, pages253–355.

[Lee and Seshia(2016)]
authorpersonEdward Ashford Lee and
personSanjit Arunkumar Seshia. year2016.
booktitleIntroduction to embedded systems: A
cyber-physical systems approach.
publisherMit Press.

[Morgan et al(1996)]
authorpersonCarroll Morgan, personAnnabelle
McIver, and personKaren Seidel.
Probabilistic predicate transformers.
journalACM Transactions on Programming Languages and
Systems (TOPLAS) volume18, number3
(year1996), pages325–353.

authorpersonPeter W O'Hearn.
A Primer on Separation Logic (and Automatic Program
Verification and Analysis).
journalSoftware safety and security
volume33 (year2012), pages286–318.

[O'Hearn et al(2009)]
authorpersonPeter W O'Hearn, personHongseok
Yang, and personJohn C Reynolds.
Separation and information hiding.
journalACM Transactions on Programming Languages and
Systems (TOPLAS) volume31, number3
(year2009), pages1–50.

[Olmedo et al(2016)]
authorpersonFederico Olmedo,
personBenjamin Lucien Kaminski, personJoost-Pieter
Katoen, and personChristoph Matheja.
Reasoning about recursive probabilistic programs.
In booktitle2016 31st Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS). IEEE, pages1–10.

authorpersonJohn C Reynolds.
Separation logic: A logic for shared mutable data
structures. In booktitleProceedings 17th Annual IEEE
Symposium on Logic in Computer Science. IEEE, pages55–74.

authorpersonJohn C Reynolds.
An introduction to separation logic.
In booktitleEngineering Methods and Tools for
Software Safety and Security. publisherIOS Press,

[Shan and Ramsey(2017)]
authorpersonChung-chieh Shan and
personNorman Ramsey. year2017.
Exact Bayesian inference by symbolic
disintegration. In booktitleProceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages.

[Smolka et al(2019)]
authorpersonSteffen Smolka, personPraveen
Kumar, personDavid M Kahn, personNate Foster,
personJustin Hsu, personDexter Kozen, and
personAlexandra Silva. year2019.
Scalable verification of probabilistic networks.
In booktitleProceedings of the 40th ACM SIGPLAN Conference
on Programming Language Design and Implementation.

authorpersonSashi Mohan Srivastava.
booktitleA course on Borel sets.
Vol. volume180.
publisherSpringer Science & Business Media.

authorpersonSam Staton.
Commutative semantics for probabilistic
programming. In booktitleEuropean Symposium on
Programming. Springer, pages855–879.

authorpersonSam Staton.
Probabilistic programs as measures.
journalFoundations of Probabilistic Programming
(year2020), pages43.

[Staton et al(2016)]
authorpersonSam Staton, personHongseok
Yang, personFrank Wood, personChris Heunen, and
personOhad Kammar. year2016.
Semantics for probabilistic programming:
higher-order functions, continuous distributions, and soft constraints. In
booktitleProceedings of the 31st Annual ACM/IEEE Symposium
on Logic in Computer Science. pages525–534.

authorpersonDario Maximilian Stein.
Structural foundations for probabilistic
programming languages.
journalUniversity of Oxford

authorpersonTerence Tao.
title254A, notes 0: A review of probability theory.

[Tassarotti and Harper(2019)]
authorpersonJoseph Tassarotti and
personRobert Harper. year2019.
A separation logic for concurrent randomized
journalProceedings of the ACM on Programming
Languages volume3, numberPOPL
(year2019), pages1–30.

[Wand et al(2018)]
authorpersonMitchell Wand, personRyan
Culpepper, personTheophilos Giannakopoulos, and
personAndrew Cobb. year2018.
Contextual equivalence for a probabilistic language
with continuous random variables and recursion.
journalProceedings of the ACM on Programming
Languages volume2, numberICFP
(year2018), pages1–30.

[Zhang and Amin(2022)]
authorpersonYizhou Zhang and personNada
Amin. year2022.
Reasoning about “reasoning about reasoning”:
semantics and contextual equivalence for probabilistic programs with nested
queries and recursion.
journalProceedings of the ACM on Programming
Languages volume6, numberPOPL
(year2022), pages1–28.

[Zhou et al(2021)]
authorpersonLi Zhou, personGilles Barthe,
personJustin Hsu, personMingsheng Ying, and
personNengkun Yu. year2021.
A quantum interpretation of bunched logic &
quantum separation logic. In booktitle2021 36th Annual
ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE,

§ SYNTAX AND SEMANTICS OF APPL

§.§ Syntax

$p$      $\in$     $[0,1]$

$r$      $\in$     $\R$

$n$      $\in$     $\N$

$\oplus$     $\in$     $\mathrm{Arith} := \{+,-,\times,/,\string^\}$

$\prec$     $\in$     $\mathrm{Cmp} := \{<,\le,=\}$

$A,B$     $::=$     $A\times B\mid \boolty \mid \realty \mid A^n \mid \indexty \mid \applgiry A$

$M,N,O$     $::=$     $X\mid \applret M\mid \letin XMN \mid$

$\appltuple{M,N} \mid \applfst~M \mid \applsnd~M \mid$

$\vtrue \mid \vfalse \mid \applite MNO \mid \flip~p \mid $

$r \mid M \oplus N \mid M \prec N \mid \applunif \mid$

$\applarray{M,\dots,M} \mid \applindex MN \mid \applfor n{M_\textrm{init}}iX{M_\textrm{step}}$

§.§ Typing

ΓM : AΓM:A
ΓM:A×BΓ M:A
ΓM:A×BΓ M:B
Γ p:
ΓM_k:A for all 1≤k≤nΓM_1,…,M_n:A^n

§.§ Semantics

Types and typing contexts are interpreted as measurable spaces,
arithmetic operators as maps $\R\times\R\mto\R$,
and comparison operators as maps $\R\times\R\mto\sembr\boolty$.

\begin{align*}
\begin{aligned}
\sembr{A \times B }&= \sembr{A }\otimes\sembr{B } \\
\sembr\boolty &= (\{\vtrue,\vfalse\}, \calP(\{\vtrue,\vfalse\})) \\
\sembr\realty &= (\R, \calB(\R)) \\
\sembr{A ^n}&= \underbrace{\sembr{A }\otimes\cdots\otimes\sembr{A }}_{n\textrm{ times}} \\
\sembr{\indexty}&= (\N, \calP(\N)) \\
\sembr{\applgiry A} &= \giry \sembr A \\
\\
\sembr\cdot &= \textrm{the one-point space} \\
\sembr{\Gamma,X\ofty A } &= \sembr\Gamma\otimes \sembr A
\end{aligned}
\begin{aligned}
x\sembr{+}y &= x+y \\
x\sembr{-}y &= x-y \\
x\sembr{\times}y &= xy \\
x\sembr{/}y &= \begin{cases} x/y, & y\ne 0 \\ 0, & \textrm{otherwise} \end{cases} \\
x\sembr{\string^}y &= \begin{cases} x^y, & x>0 \\ 0, & \textrm{otherwise} \end{cases} \\
\end{aligned}
\begin{aligned}
x\sembr{<}y &= \begin{cases} \vtrue, & x < y \\ \vfalse, & \textrm{otherwise} \end{cases} \\
x\sembr{\le}y &= \begin{cases} \vtrue, & x \le y \\ \vfalse, & \textrm{otherwise} \end{cases} \\
x\sembr{=}y &= \begin{cases} \vtrue, & x = y \\ \vfalse, & \textrm{otherwise} \end{cases}
\end{aligned}
\end{align*}

Terms $\Gamma\vdash M:A$ are interpreted as maps $\sembr M:\sembr\Gamma\mto\sembr A$.

\begin{align*}
\sembr{X}\rho &~~=~~ \rho(X) \\
\sembr{\applret M}\rho &~~=~~ \ret\sembr M\rho\\
\sembr{\letin X{M}{N}}\rho &~~=~~ v\gets \sembr{M}\rho;~ \sembr{N}\rho[X\mapsto v] \\
\sembr{\appltuple{M,N}}\rho &~~=~~ (\sembr M\rho,\sembr N\rho)\\
\sembr{\applfst~M}\rho &~~=~~ \pi_1(\sembr M\rho) \\
\sembr{\applsnd~M}\rho &~~=~~ \pi_2(\sembr M\rho) \\
\sembr{\vtrue}\rho &~~=~~ \vtrue \\
\sembr{\vfalse}\rho &~~=~~ \vfalse \\
\sembr{\applite{M}{N}{O}}\rho &~~=~~ \begin{cases}
\sembr{N}\rho,& \sembr M\rho=\vtrue \\
\sembr{O}\rho,& \sembr M\rho=\vfalse
\end{cases}\\
\sembr{\flip~p}\rho &~~=~~ \ber p \\
\sembr{r}\rho &~~=~~ r \\
\sembr{M\oplus N}\rho &~~=~~ (\sembr{M}\rho)\sembr{\oplus}(\sembr{N}\rho) \\
\sembr{\applunif}\rho &~~=~~ \unif~[0,1]\\
\sembr{\applarray{M_1,\dots,M_n}}\rho &~~=~~ (\sembr{M_1}\rho,\dots,\sembr{M_n}\rho)\\
\sembr{\applindex MN:A }\rho &~~=~~ \begin{cases}
\pi_{\sembr{N}\rho}(\sembr{M}\rho), & 1\le \sembr{N}\rho\le n \\
\arbitrary(A ), & \textrm{otherwise}
\end{cases} \\
\sembr{\applfor n{M_\textrm{i}}iX{M_\textrm{s}}}\rho &~~=~~
\mathrm{loop}(1, \sembr{M_\textrm{i}}\rho, \lambda~k~v.~\sembr{M_\textrm{s}}\rho[i\mapsto k,X\mapsto v])\\
&\hspace{-9em}\textrm{where } \mathrm{loop}(k,v,f) = \begin{cases}
\ret v, & k>n \\
v'\gets f(k,v);~
\mathrm{loop}(k+1,v',f), & \textrm{otherwise}
\end{cases}
\end{align*}

To make array indexing total, $\arbitrary(A )$ produces an arbitrary inhabitant
of $\sembr A $.

\begin{align*}
\arbitrary(A \times B ) &= (\arbitrary(A ),\arbitrary(B )) \\
\arbitrary(\boolty) &= \vtrue \\
\arbitrary(\realty) &= 0 \\
\arbitrary(A ^n) &= \underbrace{(\arbitrary(A ),\dots,\arbitrary(A ))}_{n\textrm{ times}} \\
\arbitrary(\indexty) &= 0
\end{align*}

§ SYNTAX AND SEMANTICS OF LILAC

§.§ Syntax

\begin{align*}
S,T \,\in~ &\mathbf{Set} \\
A,B \,\in~ &\mathbf{Meas} \\
P,Q ::=~ &\top \mid \bot \mid P \land Q \mid P \lor Q \mid P\to Q \mid \\
&P * Q \mid P\wand Q \mid \nec P \mid \\
&\forall x\ofty S.P \mid \exists x\ofty S. P \mid
\forallrv X\ofty A.P \mid \existsrv X\ofty A.P \mid \\
&E \sim \mu \mid \own E \mid E\asequal E \mid \Ex[E] = e \mid \weakpre(M, X\ofty A. Q)
\end{align*}

§.§ Typing

\begin{align*}
\Gamma &::= \cdot \mid \Gamma,x:S\\
\Delta &::= \cdot \mid \Delta,X:A
\end{align*}

\begin{align*}
\sembr{x_1:S_1,\dots,x_n:S_n} &= S_1\times\cdots\times S_n \\
\sembr{X_1:A_1,\dots,X_n:A_n} &= A_1\otimes\cdots\otimes A_n
\end{align*}

E ∈Γ→ΔA
e ∈Γ→A

Γ,xS;Δ⊢PΓ;Δ⊢∀xS. P
Γ,xS;Δ⊢PΓ;Δ⊢∃xS. P
Γ;Δ,XA⊢PΓ;Δ⊢XA. P
Γ;Δ,XA⊢PΓ;Δ⊢XA. P

Γ;Δ⊢[E] = e

§.§ Independent combination of probability spaces

Suppose $(\Omega, \calG,\rho)$ and $(\Omega, \calG',\rho')$ are independent combinations of
$(\Omega, \calE,\mu)$ and $(\Omega, \calF,\nu)$.  Then $\calG = \calG'$ and $\rho=\rho'$.

It is straightforward to establish that $\calG = \calG'$: they are both the
smallest $\sigma$-algebra containing $\calE$ and $\calF$.
Showing $\rho = \rho'$ requires the use of more heavyweight machinery
from probability theory: we apply the well-known
Dynkin $\pi$-$\lambda$ theorem <cit.>.
The set of events on which $\rho$ and $\rho'$ agree forms a $\lambda$-system,
and the set $\{E\cap F\mid E\in\calE,F\in\calF\}$ of intersections of events in $\calE$ and
$\calF$ forms a $\pi$-system that generates $\angled{\calE,\calF} = \calG$. So the $\pi$-$\lambda$ theorem
states that it suffices to show
$\rho(E\cap F)=\rho'(E\cap F)$ for all $E\in\calE$ and $F\in\calF$; this follows since by
assumption both sides of the equation factorize into $\mu(E)\nu(F)$.

If $\calF$ and $\calG$ are $\sigma$-algebras on $\Omega$
then the set $\calE:=\{F\cap G\mid F\in\calF,G\in\calG\}$
of intersections of events in $\calF$ and $\calG$
is a $\pi$-system that generates $\angled{\calF,\calG}$.

First let's show that $\calE$ is a $\pi$-system.
The set $\calE$ is nonempty because it at least has to contain $\emptyset$.
It's closed under finite intersections because if $(F_1\cap G_1)\in\calE$ and $(F_2\cap
then $(F_1\cap G_1)\cap(F_2\cap G_2)=\underbrace{(F_1\cap F_2)}_{\in\calF}\cap\underbrace{(G_1\cap
G_2)}_{\in\calG}\in\calE$, where the last step follows from the fact that
$\mathcal F$ and $\mathcal G$ are both $\sigma$-algebras and hence closed under intersections.

Now we just have to show $\angled{\calE}=\angled{\calF,\calG}$.
As sets of generators, $\calE$ contains the union of $\calF$ and $\calG$: because $\calF$ and $\calG$
are $\sigma$-algebras $\calE$ includes intersections of the form $F\cap\Omega=F$ and $\Omega\cap G=G$ for all
$F\in\calF$ and $G\in\calG$. This implies $\angled{\calF,\calG}\subseteq\angled{\calE}$.
For the other direction, note that
every generator $(F\cap G)\in\calE$ is an
intersection of generators $F\in\calF,G\in\calG$.

If $(\calF,\mu)$ is a probability space then $\calF^\perp := \{E\mid E\perp\calF\}$[$E\perp\calF$ iff $\mu(E\cap F)=\mu(E)\mu(F)$ for all $F\in\calF$.] is a

Clearly $\emptyset\in\calF^\perp$ because $\emptyset\perp E$ for any $E$.
If $E\perp\calF$ then $E^c\perp\calF$, so $\calF$ is closed under complements.
Finally, if $\{A_n\}_{n\in\N}$ is a collection of disjoint sets in $\calF^\perp$
then $\mu(\bigcup_n A_n\cap E)=\sum_n\mu(A_n\cap E)=\sum_n\mu(A_n)\mu(E)=\mu(E)\mu(\bigcup_n A_n)$
for all $E$, so $\calF^\perp$ is closed under countable disjoint union.

Let $\calM$ be the set of probability spaces over a fixed sample space $\Omega$.
Let $(\pdot)$ be the partial function mapping two probability spaces to their independent
combination if it exists.
Let $(\plte)$ be the ordering such that $(\calF,\mu)\plte(\calG,\nu)$ iff
$\calF\subseteq\calG$ and $\mu=\nu|_\calF$.The tuple $(\calM,\plte,\pdot,\mathbf{1})$ is a Kripke resource monoid,
where $\mathbf{1}$ is the trivial probability space $(\calF_\pmbone,\mu_\pmbone)$
with $\calF_\pmbone=\{\emptyset,\Omega\}$ and $\mu_\pmbone(\Omega) = 1$.

$\bfone$ is indeed a unit: if $(\calF,\mu)$ is some other probability space on $\Omega$
then $\angled{\calF,\calF_\pmbone}=\calF$ and $\mu$ witnesses the independent
combination of itself with $\mu_\pmbone$.
And the relation “$\calP$ is an independent combination of $\calQ$ and $\calR$”
is clearly symmetric in $\calQ$ and $\calR$, so $(\pdot)$ is commutative.
We just need to show $(\pdot)$ is associative and respects $(\plte)$.

For associativity, suppose
and $(\calF_{12},\mu_{12})\pdot(\calF_3,\mu_3)=(\calF_{(12)3},\mu_{(12)3})$.
There are three things to check:

* Some $\mu_{23}$ witnesses the combination of $(\calF_2,\mu_2)$ and $(\calF_3,\mu_3)$.

* Some $\mu_{1(23)}$ witnesses the combination of $(\calF_1,\mu_1)$ and $(\calF_{23},\mu_{23})$.

* $(\angled{\calF_1,\angled{\calF_2,\calF_3}},\mu_{1(23)})=

We'll show this as follows:

* $\angled{\calF_1,\angled{\calF_2,\calF_3}}= \angled{\angled{\calF_1,\calF_2},\calF_3}$.

* Define $\mu_{23}:=\mu_{(12)3}|_{\calF_{23}}$.
This is a witness for $(\calF_2,\mu_2)$ and $(\calF_3,\mu_3)$.

* Define $\mu_{1(23)}:=\mu_{(12)3}$. This
is a witness for $(\calF_1,\mu_1)$ and $(\calF_{23},\mu_{23})$.

To show the left-to-right inclusion for (1): by the universal property of freely-generated
$\sigma$-algebras, we just need to show
$\angled{\angled{\calF_1,\calF_2},\calF_3}$ is a $\sigma$-algebra containing
$\calF_1$ and $\angled{\calF_2,\calF_3}$. It clearly contains $\calF_1$.
To show it contains $\angled{\calF_2,\calF_3}$, we just need to show it contains
$\calF_2$ and $\calF_3$ (by the universal property again), which it clearly does. The right-to-left
inclusion is similar.

For (2), if $E_2\in\mathcal F_2$ and $E_3\in\mathcal F_3$ then
$\mu_{23}(E_2\cap E_3)=\mu_{(12)3}(E_2\cap E_3)=\mu_{(12)3}((\Omega\cap E_2)\cap E_3)
E_2)\mu_3(E_3)=\mu_1(\Omega)\mu_2(E_2)\mu_3(E_3)=\mu_2(E_2)\mu_3(E_3)$ as desired.

For (3), we need
$\mu_{(12)3}(E_1\cap E_{23})=\mu_1(E_1)\mu_{23}(E_{23})$
for all $E_1\in\calF_1$ and $E_{23}\in\angled{\calF_2,\calF_3}$.
For this we use the $\pi$-$\lambda$ theorem.
Let $\calE$ be the set $\{E_2\cap E_3\mid E_2\in\calF_2,E_3\in\calF_3\}$ of intersections of
events in $\calF_2$ and $\calF_3$. $\calE$ is a $\pi$-system that generates
$\angled{\calF_2,\calF_3}$ (lemma <ref>).
Let $\calG$ be the set of events $E_{23}$ such that $\mu_{(12)3}(E_1\cap
E_{23})=\mu_1(E_1)\mu_{23}(E_{23})$ for all $E_1\in\calF_1$.
We are done if $\angled{\calE}\subseteq\calG$.
By the $\pi$-$\lambda$ theorem, we just need to check that $\calE\subseteq\calG$ and
that $\calG$ is a $\lambda$-system.
We have $\calE\subseteq\calG$ because if $E_2\in\calF_2$ and $E_3\in\calF_3$
then $\mu_{(12)3}(E_1\cap (E_2\cap E_3))=\mu_1(E_1)\mu_2(E_2)\mu_3(E_3)=\mu_1(E_1)\mu_{23}(E_2\cap
To see that $\calG$ is a $\lambda$-system, note that
and so $\calG$ is actually equal to $\calF_1^\perp$ (the set of events independent of $\calF_1$), a $\lambda$-system by Lemma

To show $(\pdot)$ respects $(\plte)$,
suppose $(\calF,\mu)\plte (\calF',\mu')$ and
$(\calG,\nu)\plte (\calG',\nu')$
and $(\calF',\mu')\pdot(\calG',\nu') =(\angled{\calF',\calG'},\rho')$.
We need to show (1) $(\calF,\mu)\pdot(\calG,\nu)
=(\angled{\calF,\calG},\rho)$ and
(2) $(\angled{\calF,\calG},\rho)\plte(\angled{\calF',\calG'},\rho')$
for some $\rho$. Define $\rho$ to be the restriction
of $\rho'$ to $\angled{\calF,\calG}$.
Now (1) holds because
$\rho(F\cap G)
=\rho'(F\cap G)
$ for all $F\in\calF$ and $G\in\calG$ (the second step follows from $\calF\subseteq\calF'$ and
$\calG\subseteq\calG'$). For (2),
because $\calF\subseteq\calF'$ and $\calG\subseteq\calG'$, and
$\rho=\rho'|_{\angled{\calF,\calG}}$ by

§.§ Semantics

Let $\Omega$ be the Hilbert cube $[0,1]^\N$,
and let $\Sigma_\Omega$ be the standard Borel $\sigma$-algebra on the Hilbert cube
generated by the product topology.

A sub-$\sigma$-algebra $\calF$ of $\Sigma_\Omega$
has finite footprint
if there is some $n$ such that every $F\in \calF$ is of the form
$F'\times\hilbertcube$ for some $F'\subseteq[0,1]^n$.

A random variable $X:(\Omega,\Sigma_\Omega)\to (A,\Sigma_A)$ has finite footprint
if the pullback $\sigma$-algebra $\{X^{-1}(E)\mid E\in\Sigma_A\}$ has finite footprint.

Let $\Mfin$ be the set of probability spaces $\calP$ with finite footprint whose
$\sigma$-algebras are sub-$\sigma$-algebras of the standard Borel $\sigma$-algebra on $[0,1]^\N$.
The restriction of the KRM given by Theorem <ref> to $\Mfin$ is still a KRM.

If $m$ and $n$ witness the finite footprints of independently-combinable
probability spaces $\calP$ and $\calQ$ then $\max(m,n)$ witnesses the finite footprint of
their independent combination $\calP\pdot\calQ$,
and if $\calF$ and $\calG$ are two sub-$\sigma$-algebras of the Borel $\sigma$-algebra on the
Hilbert cube, then so is the $\sigma$-algebra $\angled{\calF,\calG}$.
Thus $(\pdot)$ remains closed under $\Mfin$,
which suffices to show that it remains a KRM.

Let $\rv A$ be the set of measurable maps $[0,1]^\N\mto A$ with finite footprint.
Interpret propositions $\Gamma;\Delta\vdash P$ as sets of configurations
$(\gamma,D,\calP)$ where $\gamma\in\sembr\gamma$, $D\in\rv{\sembr\Delta}$,
and $\calP\in \Mfin$.

The following interpretations of basic connectives is well-formed:

$\gamma,D,\calP\vDash \top$             always

$\gamma,D,\calP\vDash \bot$             never

$\gamma,D,\calP\vDash P\land Q$         iff        $\gamma,D,\calP\vDash P$ and $\gamma,D,\calP\vDash Q$

$\gamma,D,\calP\vDash P\lor Q$          iff        $\gamma,D,\calP\vDash P$ or $\gamma,D,\calP\vDash Q$

$\gamma,D,\calP\vDash P\to Q$           iff        $\gamma,D,\calP'\vDash P$ implies $\gamma,D,\calP'\vDash Q$ for all $\calP'\sqsupseteq \calP$

$\gamma,D,\calP\vDash P*Q$              iff        $\gamma,D,\calP_P\vDash P$ and $\gamma,D,\calP_Q\vDash Q$ for some
$\calP_P\pdot\calP_Q\plte \calP$

$\gamma,D,\calP\vDash P\wand Q$         iff        $\gamma,D,\calP_P\vDash P$ implies
$\gamma,D,\calP_P\pdot\calP\vDash Q$ for all $\calP_P$ with $\calP_P\pdot\calP$ defined

$\gamma,D,\calP\vDash \nec P$           iff        $\gamma,D,1\vDash P$

$\gamma,D,\calP\vDash \forall x\ofty S.P$        iff        $(\gamma,x),D,\calP\vDash P$ for all $x\in S$

$\gamma,D,\calP\vDash \exists x\ofty S.P$        iff        $(\gamma,x),D,\calP\vDash P$ for some $x\in S$

$\gamma,D,\calP\vDash \forallrv X\ofty A.P$        iff        $\gamma,(D,X),\calP\vDash P$ for all
$X:\rv A$

$\gamma,D,\calP\vDash \existsrv X\ofty A.P$        iff        $\gamma,(D,X),\calP\vDash P$ for some
$X:\rv A$

$\gamma,D,(\calF,\mu)\vDash E\sim \mu'$            iff      $E(\gamma)\circ D$ is $\calF$-measurable and
&\omega\gets \mu;\\
&\ret (E(\gamma)(D(\omega)))

$\gamma,D,(\calF,\mu)\vDash \own E$                 iff      $E(\gamma)\circ D$ is $\calF$-measurable

$\gamma,D,(\calF,\mu)\vDash E_1\asequal E_2$        iff      $(E_1(\gamma)\circ D)|_F=(E_2(\gamma)\circ D)|_F$
for some $F\in\calF$ with $\mu(F)=1$

$\gamma,D,(\calF,\mu)\vDash \Ex[E] = e$        iff      $E(\gamma)\circ D$ is $\calF$-measurable and
$\Ex_{\omega\sim\mu}[E(\gamma)(D(\omega))] = e(\gamma)$

$\gamma,D,\calP\vDash \weakpre(M,X\ofty A.Q)$
iff      for all $\calP_\mathrm{frame}$ and $\mu$
with $\calP_\mathrm{frame}\pdot\calP
\plte(\Sigma_\Omega,\mu)$

and all $D_\textrm{ext}:\rv{\sembr{\Delta_\textrm{ext}}}$

there exists $X:\rv A$ and $\calP'$ and $\mu'$ with
$\calP_\mathrm{frame}\pdot \calP'
\plte(\Sigma_\Omega,\mu')$

such that
&\omega\gets \mu;\\
&v\gets M(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))

and $\gamma,(D,X),\calP'\vDash Q$

We must verify that the extended random substitutions
$(D,X)$ in the interpretations of $\forallrv$, $\existsrv$, and $\weakpre$
have finite footprint; in all cases this follows from the fact that $D$ and $X$ have finite footprint.

Fix a configuration $(\gamma,D,\calP)$.
Abbreviating $X_i(\gamma)\circ D$ as $X_i'$,
random variables $X_1',\dots,X_n'$ are mutually independent with respect to $\calP$
iff $\gamma,D,\calP\vDash \own X_1 * \dots * \own X_n$.

First suppose $\gamma,D,\calP\vDash \own X_1 * \dots * \own X_n$, so
each $X_i'$ is $\calP_i$-measurable for some $\calP_1\pdot\dots\pdot\calP_n\plte\calP$.
Write $\calP=(\calF,\mu)$ and $\calP_i=(\calF_i,\mu_i)$ for all $1\le i\le n$.
For any subset $J$ of $\{1,\dots,n\}$ and any collection of events
$\{E_j \in \calF_j\}_{j\in J}$,
we have
\[\Pr\left[\bigwedge_{j\in J} X_j'\in E_j\right] = \mu\left(\bigcap_{j\in J} X_j'^{-1}(E_j)\right)
\stackrel{(a)}=\prod_{j\in J} \mu_j(X_j'^{-1}(E_j)) \stackrel{(b)}= \prod_{j\in J} \mu(X_j'^{-1}(E_j))
= \prod_{j\in J} \Pr[X_j'\in E_j]\]

where $(a)$ and $(b)$ hold because $\calP_1\pdot\dots\pdot\calP_n\plte\calP$
and $X_j'^{-1}(E_j)\in\calF_j$ for all $j$. Hence $X_1',\dots,X_n'$ are mutually independent.

For the converse, suppose $X_1',\dots,X_n'$ are mutually independent with respect to some probability
space $\calP$.
For each $1\le i\le n$, let $\calP_i$ be the probability space $(\calF_i,\mu_i)$
where $\calF_i$ is the pullback $\sigma$-algebra along $X_i'$ and $\mu_i$ the restriction of $\mu$ to
It's enough to show that the composition
$\calP_1\pdot\dots\pdot\calP_n$ is defined, as
then $\calP_1\pdot\dots\pdot\calP_n\plte \calP$ by lemma
This follows by induction on $n$.
Cases $n=0$ and $n=1$ are immediate.
Now suppose $\calP_1\pdot\dots\pdot \calP_k$ is defined.
It's straightforward to show that $\calP_1\pdot\dots\pdot \calP_k$ is the pullback of the random variable
and $\calP_{k+1}$ is the pullback of $X_{k+1}'$ by definition.
Mutual independence of $X_1',\dots,X_k',X_{k+1}'$
implies independence of $(X_1',\dots,X_k')$ and $X_{k+1}'$: intersections of
events $X_1'^{-1}(E_1)\cap\dots\cap X_k'^{-1}(E_k)$ form a $\pi$-system that
generates $\calF_1\pdot\dots\pdot\calF_k$,
events independent of $\calF_{k+1}$ with respect to $\mu$ form a $\lambda$-system,
and each intersection $X_1'^{-1}(E_1)\cap\dots\cap X_k'^{-1}(E_k)$ is independent of $\calF_{k+1}$
because $X_1',\dots,X_k',X_{k+1}'$ are mutually independent.
Thus the pullback of $(X_1',\dots,X_k',X_{k+1}')$ is an independent combination
of $\calP_1\pdot\dots\pdot\calP_k$ and $\calP_{k+1}$, and $\calP_1\pdot\dots\pdot\calP_k\pdot\calP_{k+1}$
is defined.
This closes the induction, so $\gamma,D,\calP\vDash \own X_1'\pdot\dots\pdot X_n'$ as desired.

§.§.§ Substitution

Substitutions take the form $(s,S)$ where $s$ is a substitution
of deterministic values and $S$ a substitution of random variables.

$\fbox{\inferrule{\Gamma;\Delta\vdashrv E:A \\ \Gamma';\Delta'\vdash (s,S):\Gamma;\Delta}
{\Gamma';\Delta'\vdash E[s,S] : A}}$

$E[s,S](\gamma) = E(s(\gamma)) \circ S$

$\fbox{\inferrule{\Gamma\vdashdet e:A \\ \Gamma'\vdash s:\Gamma}
{\Gamma'\vdash e[s] : A}}$

$  e[s] = e \circ s $

$\fbox{\inferrule{\Gamma\vdashdet \mu:A \\ \Gamma'\vdash s:\Gamma}
{\Gamma'\vdash \mu[s] : A}}$

$ \mu[s] = \mu \circ s $

$\fbox{\inferrule{\Gamma;\Delta\vdashprog M:A \\ \Gamma';\Delta'\vdash (s,S):\Gamma;\Delta}
{\Gamma';\Delta'\vdash M[s,S] : A}}$

$ M[s,S](\gamma) = M(s(\gamma)) \circ S $

$\fbox{\inferrule{\Gamma;\Delta\vdash P \\ \Gamma';\Delta'\vdash (s,S):\Gamma;\Delta}
{\Gamma';\Delta'\vdash P[s,S]}}$

\top[s,S] &= \top \\
\bot[s,S] &= \bot \\
(P\land Q)[s,S] &= (P[s,S]\land Q[s,S]) \\
(P\lor Q)[s,S] &= (P[s,S]\lor Q[s,S]) \\
(P\to Q)[s,S] &= (P[s,S]\to Q[s,S]) \\
(P* Q)[s,S] &= (P[s,S]* Q[s,S]) \\
(P\wand Q)[s,S] &= (P[s,S]\wand Q[s,S]) \\
(\nec P)[s,S] &= \nec P[s,S] \\
(\forall x\ofty T.P)[s,S] &= \forall x\ofty T. P[s\times 1_T,S] \\
(\exists x\ofty T.P)[s,S] &= \exists x\ofty T. P[s\times 1_T,S] \\
(\forallrv X\ofty A.P)[s,S] &= \forallrv X\ofty A. P[s,S\times 1_A] \\
(\existsrv X\ofty A.P)[s,S] &= \existsrv X\ofty A. P[s,S\times 1_A] \\
(E\sim\mu)[s,S] &= E[s,S] \sim \mu[s] \\
(\own E)[s,S] &= \own E[s,S] \\
(E_1 \asequal E_2)[s,S] &= E_1[s,S] \asequal E_2[s,S]\\
(\Ex[E] = e)[s,S] &= \Ex[E[s,S]] = e[s] \\
\weakpre(M,X\ofty A.Q)[s,S] &= \weakpre(M[s,S],X\ofty A. Q[s,S\times 1_A])
\end{aligned}$

$\gamma,D,\calP\vDash P[s,S]$ iff $s(\gamma), S\circ D,\calP\vDash P$.

By induction on the syntax of propositions.
The interesting cases are:

* Case $E\sim \mu$:

\begin{align*}
&\gamma,D,\calP\vDash (E\sim \mu)[s,S]\\
&\textrm{iff } \gamma, D,\calP\vDash ((\gamma\mapsto E(\gamma)\circ S)\sim (\mu\circ S)) \\
&\textrm{iff } E(s(\gamma))\circ S\circ D \textrm{ is }\calP\textrm{-measurable and }
\mu(\gamma) = \monadic{&\omega\gets \calP\\ &\ret E(\gamma)(S(D(\omega)))} \\
&\textrm{iff } s(\gamma), S\circ D,\calP\vDash E\sim \mu
\end{align*}

* Case $\weakpre(M,X\ofty A.Q)$:
For the left-to-right direction,
suppose (1) $\gamma,D,\calP\vDash \weakpre(M[s,S], X\ofty A.  Q[s,S\times 1_A])$
and (2) $\calP_\textrm{frame}\pdot \calP\plte(\Sigma_\Omega,\mu)$
and (3) $D_\textrm{ext}:\rv{\sembr{\Delta_\textrm{ext}}}$.
By (1) there exist $\calP'$ and $\mu'$ with
and $X:\rv A$ such that

\[
\monadic{
&\omega\gets \mu;\\
&v\gets M[s,S](\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}, D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}, D(\omega), X(\omega))
\]

and $\gamma,(D,X),\calP\vDash Q[s,S\times 1_A]$.
By IH this is equivalent to $s(\gamma),(S\circ D,X),\calP\vDash Q$
and simplifying the above equation gives

\[
\monadic{
&\omega\gets \mu;\\
&v\gets M(s(\gamma))(S(D(\omega)));\\
&\ret (D_\textrm{ext}, D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}, D(\omega), X(\omega))
\]

Now postcomposing both sides with the map
$(\delta_\textrm{ext}, \delta,v)\mapsto (\delta_\textrm{ext}, S(\delta),v)$

\[
\monadic{
&\omega\gets \mu;\\
&v\gets M(s(\gamma))(S(D(\omega)));\\
&\ret (D_\textrm{ext}, S(D(\omega)), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}, S(D(\omega)), X(\omega))
\]

so that $(\calP',\mu',X)$ witnesses $s(\gamma),S\circ D,\calP\vDash \weakpre(M,X\ofty A. Q)$ as

For the right-to-left direction, suppose
(1) $s(\gamma),S\circ D,\calP\vDash \weakpre(M, X\ofty A.  Q)$
and (2) $\calP_\textrm{frame}\pdot \calP\plte(\Sigma_\Omega,\mu)$
and (3) $D_\textrm{ext}:\rv{\sembr{\Delta_\textrm{ext}}}$.
Specialize (1) with $D_\textrm{ext}:= (D_\textrm{ext},D)$
to get $\calP'$, $\mu'$ and $X:\rv A$ such that

\[
\monadic{
&\omega\gets \mu;\\
&v\gets M(s(\gamma))(S(D(\omega)));\\
&\ret ((D_\textrm{ext}, D), S(D(\omega)), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret ((D_\textrm{ext}, D), S(D(\omega)), X(\omega))
\]

and $s(\gamma),(S\circ D, X),\calP'\vDash Q$.
By IH this is equivalent to $\gamma,(D,X),\calP'\vDash Q[s,S\times 1_A]$,
and postcomposing both sides of the above equation with the map
$((\delta_\textrm{ext},\delta),\_,v) \mapsto (\delta_\textrm{ext},\delta,v)$
and rewriting $M(s(\gamma))(S(D(\omega)))$ in terms of $M[s,S]$ gives
\[
\monadic{
&\omega\gets \mu;\\
&v\gets M[s,S](\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}, D, v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}, D, X(\omega))
\]

so that $(\calP',\mu',X)$ witnesses
$\gamma,D,\calP\vDash \weakpre(M[s,S], X\ofty A.  Q[s,S\times 1_A])$
as desired.

§.§ Derived rules

The following structural rules hold:

*[lab=H-Frame,right=$(X\notin F)$]F*(M,X.Q)⊢(M,X.F * Q)

We show the proof of the frame rule; the others are standard.
Suppose (1)
$\gamma,D,\calP_F\pdot \calP_M\vDash F*\weakpre(M,X.Q)$
for some $\gamma,D,\calP_F\vDash F$ and $\gamma,D,\calP_M\vDash \weakpre(M,X.Q)$.
To show $\weakpre(M,X.F*Q)$, further suppose
and $D_\textrm{ext}:\rv{\sembr{\Delta_\textrm{ext}}}$.
By associativity, $\calP_\textrm{frame}\pdot(\calP_F\pdot\calP_M)
so specializing (1) with $\calP_\textrm{frame}:=\calP_\textrm{frame}\pdot\calP_F$
gives $(\calP_\textrm{frame}\pdot\calP_F)\pdot\calP'\plte(\Sigma_\Omega,\mu')$
and $X$ such that

\[
\monadic{
&\omega\gets \mu;\\
&v\gets M(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))
\]

and $\gamma,(D,X),\calP'\vDash Q$.
Since $X\notin F$, $F[\mathrm{weak}_X] = F$
so $\gamma,(D,X),\calP_F\vDash F$
by lemma <ref>.
And since the composition $(\calP_\textrm{frame}\pdot\calP_F)\pdot\calP'$ is defined,
the composition $\calP_F\pdot\calP'$ must be as well, so
$\gamma,(D,X),\calP_F\pdot\calP'\vDash F*Q$ as desired.

The following $\weakpre$ laws hold:

(M,X.(N,Y.Q)) ⊢((X M; N),Y.Q)

(XA.  X∼Unif[0,1]Q) ⊢( [0,1],XA.Q)

(XA.  X∼pQ) ⊢(p,XA.Q)

I(1,e) * (∀i. XA. I(i,X)MX'I(i+1,X'))
⊢(neM,XA. I(n+1,X))

(M,XA. (N,YA.  Q(EXY)))
⊢(EMN,XA. Q)

where $\forloop nef$ is defined by

\begin{align*}
&{\forloop nef} = \mathrm{loop}(1,e,f)
\textrm{where } \mathrm{loop}(k,e,f) = \begin{cases}
\ret e, & k>n \\
v\gets f(k,e);~
\mathrm{loop}(k+1,v,f), & \textrm{otherwise}
\end{cases}
\end{align*}

* Ret:
suppose $\gamma,D,\calP\vDash Q[e(\gamma)/X]$.
By lemma <ref> this is equivalent to $\gamma,(D,e(\gamma)),\calP\vDash Q$.
To show $\weakpre(\ret e,X.Q)$ suppose
and $D_\textrm{ext}:\rv\sembr{\Delta_\textrm{ext}}$.
Choose $\calP':=\calP$ and $\mu':=\mu$ and $X(\omega):=e(\gamma)$.

\[
\monadic{
&\omega\gets \mu;\\
&v\gets (\ret e)(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
= \monadic{
&\omega\gets \mu;\\
&\ret (D_\textrm{ext}(\omega), D(\omega), e(\gamma))
= \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))
\]

and $\gamma,(D,e(\Gamma)),\calP\vDash Q$ as desired.

* Let:
suppose $\gamma,D,\calP\vDash \weakpre(M,X.\weakpre(N,Y.Q))$.
To show $\weakpre((X\gets M; N),Y.Q)$ suppose
and $D_\textrm{ext}:\rv\sembr{\Delta_\textrm{ext}}$.
By assumption, there exist $\calP_\textrm{frame}\pdot\calP_X\plte(\Sigma_\Omega,\mu_X)$
and $X$ such that

\begin{align} \label{let-binding-step1}
\monadic{
&\omega\gets \mu;\\
&x\gets M(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), x)
} = \monadic{
&\omega\gets \mu_X;\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))
\end{align}

and $\gamma,(D,X),\calP_X\vDash \weakpre(N,Y.Q)$.
Applying this assumption gives $\calP_\textrm{frame}\pdot\calP_Y\plte(\Sigma_\Omega,\mu_Y)$
and $Y$ with

\begin{align} \label{let-binding-step2}
\monadic{
&\omega\gets \mu_X;\\
&y\gets N(\gamma)((D,X)(\omega));\\
&\ret (D_\textrm{ext}(\omega), (D,X)(\omega), y)
} = \monadic{
&\omega\gets \mu_Y;\\
&\ret (D_\textrm{ext}(\omega), (D,X)(\omega), Y(\omega))
\end{align}

and $\gamma,(D,X,Y),\calP_Y\vDash Q$.
Since $X\notin Q$, this implies $\gamma,(D,Y),\calP_Y\vDash Q$ by <ref>, so
it only remains to show

\[
\monadic{
&\omega\gets \mu;\\
&y\gets (X\gets M; N)(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), y)
} = \monadic{
&\omega\gets \mu_Y;\\
&\ret (D_\textrm{ext}(\omega), D(\omega), Y(\omega))
\]

\begin{align*}
&\omega\gets \mu;\\
&y\gets (X\gets M; N)(\gamma)(D(\omega));\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
= \monadic{
&\omega\gets \mu;\\
&x\gets M(\gamma)(D(\omega)); \\
&y\gets N(\gamma)(D(\omega), x);\\
&\ret (D_\textrm{ext}(\omega), D(\omega), y)
&= \monadic{
&\omega\gets \mu;\\
&x\gets M(\gamma)(D(\omega)); \\