: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
(Extended Version)

Jialu Bao
Cornell University
NY, US

Emanuele D'Osualdo
Saarland Informatics Campus

Azadeh Farzan
University of Toronto

We present , a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools.
Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning.
The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs
(e.g. when proving differential privacy)
managing to avoid having to characterize the output distributions of the individual programs.
So far, the two styles of reasoning
have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs.
In , we unify these styles of reasoning through the introduction of a new modality called “” that can encode and illuminate the rich interaction between conditional independence and relational liftings;
the two powerhouses from the two styles of reasoning.

§ INTRODUCTION

Probabilistic programs are pervasive, appearing as
machine learned subsystems,
implementations of randomized algorithms,
cryptographic protocols, and
differentially private components,
among many more.
Ensuring reliability of such programs requires formal frameworks
in which correctness requirements can be formalized and verified
for such programs.
Similarly to the history of classical program verification,
a lot of progress in this has come in the form of program logics
for probabilistic programs.
In the program logic literature,
there are two main styles of reasoning for probabilistic programs:
unary and relational,
depending on the nature of the property of interest.
For instance, for differential privacy or cryptographic protocols correctness,
the property of interest is naturally expressible relationally.
In contrast, specifying properties of output distributions (expected cost)
of randomized algorithms is naturally unary.

Unary goals are triples $ \{P\}\ t\ \{Q\}$ where
$t$ is a probabilistic program,
$P$ and $Q$ are the pre- and post-conditions,
predicates over distributions of stores.
Such triples assert that
running $t$ on an input store drawn from a distribution satisfying $P$
results in a distribution over output stores which satisfies $Q$.
Unary reasoning for probabilistic programs has made great strides,
producing logics for reasoning about
expectations [Kozen, 1983, Morgan et al, 1996, Kaminski et al, 2016, Kaminski, 2019, Aguirre et al, 2021, Moosbrugger et al, 2022],
probabilistic independence [Barthe et al, 2019] and
conditional independence [Li et al, 2023, Bao et al, 2021].
Lilac [Li et al, 2023], which is the most recent,
made a strong case for adding power to reason
about conditioning and independence.
Intuitively, conditioning on some random variable x
allows to focus on the distribution of other variables
assuming $\p{x}$ is some deterministic outcome $v$;
two variables are (conditionally) independent if
knowledge of one does not give any knowledge of the other (under conditioning).
Lilac argued for (conditional) independence as the fundamental source of
modularity in the probabilistic setting.

Relational program logics like pRHL [Barthe et al, 2009]
and its successors [Barthe et al, 2009, Barthe et al, 2015, Hsu, 2017, Gregersen et al, 2023, Aguirre et al, 2019],
in contrast, focus on two programs $t_1$ and $t_2$, and study whether
they produce output distributions that are related in some way;
for example, whether $t_1$ and $t_2$ produce the same output distribution.
Clearly, if the output distributions can be characterized
individually for each program,
then they can be compared after the fact.
Hence, relational reasoning can be done in theory in the unary style.
More often than not, however,
precisely characterizing the output distribution of a program
can be extremely challenging.
Relational proofs allow instead to analyze the two programs side-by-side
so that one can build arguments that examine the executions
of $t_1$ and of $t_2$ in lockstep,
and keep track of the relation between the distributions as the two runs unfold.
At any point in the proof,
the individual distributions may be
only partially constrained by the assertions,
but just enough so that their reciprocal relation is ensured.

The fundamental proof principle at play in these logics is the idea of
coupling proofs [Barthe et al, 2009, Barthe et al, 2015].
The two programs are conceptually considered to execute in
two “parallel universes”, where they are oblivious to each others' randomness.
It is therefore sound to correlate their executions
in a way that eases the argument,
as long as the marginal distribution of the correlated runs in each universe
coincides with the original one.
For example, if both programs flip a fair coin,
one can decide that the outcomes of the coin flips are the same
(or the opposite of each other,
depending on which serves the particular line of argument better).
Relating the samples in a specific way helps with
relating the distributions step by step, to support a relational goal.
Couplings, when applicable, permit relational logics to elegantly sidestep
the need to characterize the output distributions precisely.
As such, relational logics hit an ergonomic sweet spot in reasoning style
by restricting the form of the proofs that can be carried out.

Consider the example in
The BelowMax($x, S$) procedure takes $N$ samples
from a non-empy set $S \subs \Int$,
according to an (arbitrary) distribution $\prob_S \of \Dist(S)$;
if any of the samples is larger than the given input $x$
it declares $x$ to be below the maximum of $S$.
The AboveMin($x, S$) approximates in the same way
whether $x$ above the minimum of $S$.
These are Monte Carlo style algorithms with a false bias;
if the answer is false, they always correctly produce it,
and if the answer is true, then they correctly classify it
with a probability that depends on $N$
(i.e. the number of samples).
It is a well-known fact that Monte Carlo style algorithms can be composed.
For example, BETW_SEQ runs
BelowMax($x, S$) and AboveMin($x, S$)
to produce a false-biased Monte Carlo algorithm
for approximately deciding whether $x$ lie within the extrema of $S$.
Now, imagine a programmer proposed BETW,
as a way of getting more milage out of the number of samples drawn;
both procedures take $2N$ samples,
but BETW performs more computation for each sample.
Such optimisations are not really concerned about
what the precise output distributions of each code is,
but rather that a true answer is produced
with higher probability by BETW;
in other words, its stochastic dominance over BETW_SEQ.

A unary program logic has only one way of reasoning
about this type of stochastic-dominance:
It has to analyze each code in isolation,
characterize its output distribution,
and finally assert/prove that one dominates the other.
In contrast, there is a natural relational strategy
for proving this goal:
the intuition is that we can couple the $N$ samples of BelowMax
with $N$ of the samples of BETW, and the $N$ samples of AboveMin
with the remaining samples of BETW,
and argue that for each of these coupled samplings,
BETW has more chances of turning l and r to 1
(and they can only grow).

def BelowMax($x$,$S$):
repeat $N$:
q :  $\prob_S$
r := r || q >= $x$

def AboveMin($x$,$S$):
repeat $N$:
p :  $\prob_S$
l := l || p <= $x$

def BETW_SEQ($x$, $S$):
d := r        l

def BETW($x$,$S$):
repeat $2 N$:
s :  $\prob_S$
l := l || s <= $x$
r := r || s >= $x$
d := r        l

A stochastic dominance example: composing Monte Carlo algorithms two different ways. All variables are initially 0.

Unary logics can express information about distributions
with arbitrary levels of precision;
yet none can encode the simple natural proof idea outlined above.
This suggests an opportunity:
Bring native relational reasoning support to an expressive unary logic,
like Lilac.
Such a logic can be based on assertions over distributions,
thus able to be as precise and expressive as unary logics,
yet it can support relational reasoning natively
and as such can encode the argument outlined above
at the appropriate level of abstraction.
To explore this idea,
let us first underline the important differences
between unary and relational reasoning styles.

Relational logics use variants of judgments of the form
$ \{R_1\} \m[\I1: t_1, \I2: t_2] \{R_2\}$:
$t_1$ and $t_2$ are the two programs we are comparing;
$R_1$ and $R_2$ are the relational pre- and post-conditions.
$R_1$ and $R_2$ differ from unary assertions in two ways:
first they are used to relate two distributions
instead of constraining a single one.
Second, they are predicates over pairs of stores,
and not of distributions directly.
Let us call predicates of this type “deterministic relations”.
Couplings are the tool that allows lifting deterministic relations to
relations about distributions, an operation called
relational lifting.
If $R$ was a deterministic predicate over a single store,
requiring it to hold with probability 1 would naturally lift it
to a predicate $\sure{R_2}$ over distributions of stores.
When $R$ is a deterministic relation between pairs of stores,
its relational lifting $\cpl{R_2}$
will relate two distributions over stores
$\prob_1,\prob_2 \of \Dist(\Store)$,
if there is a distribution over pairs of stores
$\prob \of \Dist(\Store\times\Store)$
such that its marginal distributions on the first and second store
coincide with $\prob_1$ and $\prob_2$ respectively,
($\prob$ is a coupling of $\prob_1$ and $\prob_2$)
and is such that with probability 1 it produces pairs of stores
satisfying the relation $R_2$.

For example, assume $\p{x}$ is distributed as a fair coin flip
in both distributions $\prob_1$ and $\prob_1$.
Then we can couple the distributions to a coupling
$\prob$ which flips a single coin and returns the pair of stores
with the outcome stored in x in both stores,
so that the marginals of $\prob$ are $\prob_1$ and $\prob_2$.
The existence of such $\prob$
implies that $(\prob_1, \prob_2)$ satisfies $\cpl{\Ip{x}{1} = \Ip{x}{2}}$.
More generally, by a well-known property of couplings,
$\cpl{\Ip{x}{1} = \Ip{x}{2}}$ will relate precisely the distributions
that distribute x in the same way.
It is possible to encode a variety of useful relations between distributions
as relational liftings.

To sum up, unary logics use predicates over single distributions,
and relational reasoning uses predicates over pairs of stores.
To bring relational reasoning to unary logics,
we want to preserve the fact that assertions are over distributions,
and yet support relational lifting as the key abstraction
to do relational reasoning.
This new logic can equally be viewed as a relational logic
with assertions over distributions (rather than the pairs of stores).
With such a view, seeing relational lifting as one of the constructs
to build assertions seems like a very natural, yet completely unexplored, idea.

It is easy enough to introduce relational lifting.
What is entirely non-obvious is whether relational lifting
works well as an abstraction together with the other key “unary” constructs,
such as independence and conditioning,
that are the source of expressive power of unary logics.
For example, from the properties of couplings, we know that
establishing $\cpl{\Ip{x}{1} = \Ip{x}{2}}$ implies that
$\Ip{x}{1}$ and $\Ip{x}{2}$ are identically distributed;
this can be expressed as an entailment:

\begin{equation}
\cpl{\Ip{x}{1} = \Ip{x}{2}}
\lequiv
\E \prob.
\distAs{\Ip{x}{1}}{\prob}
\land
\distAs{\Ip{x}{2}}{\prob}.
\label{eq:rl-id-conv}
\end{equation}

The equivalence says that establishing a coupling that can
(almost surely) equate the values of $\Ip{x}{1}$ and $\Ip{x}{2}$,
amounts to establishing that the two variables are identically distributed.
The equivalence can be seen as a way to interface “unary” facts
and relational liftings.

Probability theory is full of lemmas of this sort and it is clearly undesirable to admit any lemma that is needed for one proof or another as an axiom in the program logic.
Can we have logic in which they are derivable without having to abandon its nice abstractions?
Can the two styles be interoperable at the level of the logic?
In this paper, we provide an affirmative answer to this question by proposing a new program logic .

We propose that relational lifting does in fact have non-trivial and useful
interactions with independence and conditioning.
Remarkably, 's development is unlocked by
a more fundamental observation:
once an appropriate notion of conditioning is defined in ,
relational lifting and its laws can be derived from this foundational
conditioning construct.

The key idea is a new characterization of relational lifting as a form of
whilst relational lifting is usually seen as a way to induce a relation over distributions from a deterministic relation,
sees it as a way to go from
a tuple of distributions to a relation between the values of some conditioned variables.
More precisely:

* We introduce a new  modality in     which can be seen, in hindsight,
as a natural way to condition when dealing with tuples of distributions.

* We show that  can represent uniformly
both, conditioning à la Lilac,
and relational lifting as derived notions in .

* We prove a rich set of general rules for ,
from which we can derive both known and novel proof principles
for conditioning and for relational liftings in .

Interestingly, our  modality can replicate the same reasoning
style of Lilac's modality, while having a different semantics
(and validating an overlapping but different set of rules as a result).
This deviation in the semantics is a stepping stone to obtain an
adequate generalization to the n-ary case (unifying unary and binary as special cases).
We expand on these ideas in <ref>, using a running example.
More importantly, our   enables  to

* accommodate unary and relational reasoning
in a fundamentally interoperable way: For instance, we showcase the interaction between lifting and conditioning in the derivation of our running example in <ref>.

* illuminate known reasoning principles: For instance, we discuss how  emulates pRHL-style reasoning
in <ref>.

* propose new tools to build program proofs: For instance, we discuss out-of-order coupling of samples through <ref> in <ref>.
* enable the exploration of the theory of high-level constructs
like relational lifting (via the laws of independence and ): For instance, novel broadly useful rules <ref> and <ref>, discussed in <ref> can be derived within .

§ A TOUR OF

In this section we will highlight the main key ideas behind
, using a running example.

§.§ The Alliance

def encrypt():
k :  Ber(1/2)
m :  Ber($p$)
c := k xor m
One time pad.

We work with a first-order imperative probabilistic programming language
consisting of programs $t\in\Term$ that mutate a variable store $\store\in\Store$
(a finite map from variable names $\Var$ to values $\Val$).
We only consider discrete distributions
(but with possibly infinite support).
In <ref> we show a simple example adapted from [Barthe et al, 2019]:
the encrypt procedure uses a fair coin flip to generate an encryption key
k, generates a plaintext message in boolean variable m
(using a coin flip with some bias $p$)
and produces the ciphertext c by XORing the key and the message.
A desired property of the program is that the ciphertext should be
indistinguishable from an unbiased coin flip; as a binary triple:

\begin{equation}
\{\True\}
\m[
\I1: \code{encrypt()},
\I2: \code{c:~Ber(1/2)}
\{
\cpl{ \Ip{c}{1}=\Ip{c}{2} }
\}
\label{ex:xor:goal}
\end{equation}

In <ref>, we discuss a unary-style proof of this goal in . Here, we focus on a relational argument, as a running example. The natural (relational) argument goes as follows.
When computing the final XOR,
if $\p{m}=0$ then c=k,
if $\p{m}=1$ then c=!k.
Since both $\Ip{k}{1}$ and $\Ip{c}{2}$ are distributed as unbiased coins,
they can be coupled either so that they get the same value,
or so that they get opposite values (the marginals are the same).
One or the other coupling must be established
conditionally on $\Ip{m}{1}$, to formalize this argument.
Doing so in pRHL faces the problem that the logic is too rigid to permit one to
condition on $\Ip{m}{1}$ before $\Ip{k}{1}$ is sampled; rather it forces one to establish a coupling of $\Ip{k}{1}$ and $\Ip{c}{2}$ right when the two samplings happen.
This rigidity is a well-known limitation of relational logics,
which we can easily overcome by “immersing” relational lifting
in a logic with assertions on distributions.
Recent work [Gregersen et al, 2023]
proposed workarounds based on ghost code for pre-sampling
(see <ref>).
We present a different solution based on framing, to the generic problem of out-of-order coupling, in <ref>.

Unconstrained by the default assumption of relational logics, that every assertion has to be represented as a relational lifting, we can observe three crucial components in the proof idea:

* Probabilistic independence
between the sampling of $\Ip{k}{1}$ and $\Ip{m}{1}$,
which makes conditioning on $\Ip{m}{1}$ preserve the
distribution of $\Ip{k}{1}$;

* Conditioning to perform case analysis
on the possible values of $\Ip{m}{1}$;

* Relational lifting
to represent the existence of couplings imposing the desired
correlation between $\Ip{k}{1}$ and $\Ip{c}{2}$.

Unary logics like
Probabilistic Separation Logics (PSL)
[Barthe et al, 2019] and
explored how probabilistic independence
can be represented as separating conjunction,
obtaining remarkably expressive and elegant reasoning principles.
In , we import the notion of independence from Lilac:
's assertions are interpreted over
tuples of probability spaces $\m{\psp}$,
and $ Q_1 * Q_2 $  holds on $\m{\psp}$ if
$\m{\psp}(i)$ can be seen as the independent product
of $ \m{\psp}_1(i) $ and $\m{\psp}_2(i)$,
for each $i$,
such that the tuples $\m{\psp}_1$ and $\m{\psp}_2$ satisfy $Q_1$ and $Q_2$
This means that
$\distAs{\Ip{x}{1}}{\prob} * \distAs{\Ip{y}{1}}{\prob}$
states that $\Ip{x}{1}$ and $\Ip{y}{1}$ are independent and identically distributed,
as opposed to
$\distAs{\Ip{x}{1}}{\prob} \land \distAs{\Ip{y}{1}}{\prob}$
which merely declares the two variables as identically distributed
(but possibly correlated).
We use the $\at{i}$ notation to indicate the index of the component
that an expression references;
for a unary predicate over stores $R$
we write $\sure{R\at{i}}$ to mean that
the predicate $R$ holds with probability 1
in the distribution at index $i$.

With these tools it is easy to get through the first two assignments
of encrypt and the one on component $\I2$ and get to a state
satisfying the assertion

\begin{equation}
P =
\distAs{\Ip{k}{1}}{\Ber{\onehalf}}
\distAs{\Ip{m}{1}}{\Ber{p}}
\distAs{\Ip{c}{2}}{\Ber{\onehalf}}
\label{ex:xor:start}
\end{equation}

The next ingredient we need is conditioning.
We introduce a new modality $\CMod{\prob}$ for conditioning,
in the spirit of Lilac.
Let us illustrate how we would represent conditioning on $\Ip{m}{1}$
in this example. Roughly speaking, an assertion
$\CC{\Ber{p}} v.K(v)$
states that the current distribution $\prob_0$
can be seen as the convex combination (with coefficients given by $\Ber{p}$)
of a v-indexed family of distributions $ \krnl(v) $:
\prob_0 = p \cdot \krnl(1) + (1-p) \cdot \krnl(0).
Moreover, $ \krnl(v) $ is such that it satisfies $K(v)$ for each $v$.
By letting $K(v) = \sure{\Ip{m}{1}=v} * K'(v)$ we can make sure
that $ \krnl(v) $ is such that it sees $\Ip{m}{1}$ as a deterministic variable
with value $v$; in other words, $\krnl(v)$ is now $\prob_0$ conditioned on

Combining independence and conditioning with the third ingredient,
relational lifting $\cpl{R}$, we can now express with an assertion the desired
conditional coupling we outlined in the beginning:

\begin{equation}
Q =
\CC{\Ber{p}} v.
\left(
\sure{\Ip{m}{1}=v}
\begin{cases}
\cpl{ \Ip{k}{1} = \Ip{c}{2} }     \CASE v=0 \\
\cpl{ \Ip{k}{1} = \neg\Ip{c}{2} } \CASE v=1
\end{cases}
\right)
\label{ex:xor:ccouple}
\end{equation}

The idea is that we first condition on $\Ip{m}{1}$
so that we can see it as the deterministic value $v$,
and then we couple $\Ip{k}{1}$ and $\Ip{c}{2}$ differently
depending on $v$.

To perform the proof idea formally we are left with two subgoals.
The first is to formally prove the entailment
P \proves Q.
Then, it is possible to prove that after
the final assignment to c, the program is in a state that satisfies
$Q * \sure{\Ip{c}{1} = \Ip{k}{1} \xor \Ip{m}{1}}$.
To finish the proof we would need to prove that
Q * \sure{\Ip{c}{1} = \Ip{k}{1} \xor \Ip{m}{1}}
\proves
\cpl{ \Ip{c}{1} = \Ip{c}{2} }.
These missing steps need laws
governing the interaction between independence conditioning and relational lifting in this n-ary setting.

A crucial observation of
is that, by choosing an appropriate definition for the
modality $\CMod{\prob}$,
relational lifting can be encoded as a form of conditioning.
Consequently, the laws governing relational lifting can be derived
from the more primitive laws for .
Moreover, the interactions between relational lifting and independence can be derived through the primitive laws for the interactions between  and independence.

§.§  and Relational Lifting

Let us elaborate on the definition of the  modality and its general n-ary version.
$\prob \of \Dist(A)$ and
a function $\krnl \from A \to \Dist(B)$ (called a Markov kernel),
define the distribution $\bind(\prob, \krnl) \of \Dist(B)$ as
\bind(\prob, \krnl) =
\fun b.\Sum*_{a\in A} \prob(a) \cdot \krnl(a)(b)
$ and $
\return(v) = \dirac{v}.
The $\bind$ operation represents a convex combination with coefficients in
$\prob$, while $\dirac{v}$ is the Dirac distribution, which assigns probability 1
to the outcome $v$.
These operations form a monad with the distribution functor $\Dist(\hole)$,
a special case of the Giry monad [Giry, 1982].
Given a distribution $\prob \of \Dist(A)$,
and a predicate $K(a)$ over pairs of distributions
parametrized by values $a\in A$,
we define
\CMod{\prob} a\st K(a)
to hold on some $(\prob_1,\prob_2)$ if

\begin{align*}
\exists \krnl_1,\krnl_2 \st
\forall i \in \set{1,2} \st
\prob_i = \bind(\prob, \krnl_i)
\land
\forall a \in \psupp(\prob) \st
K(a) \text{ holds on }
(\krnl_1(a), \krnl_2(a))
\end{align*}

Namely, we decompose the pair $(\prob_1,\prob_2)$ component wise
into convex compositions of $\prob$ and some kernel $\krnl_1,\krnl_2$,
one per component.
Then we require the predicate $K(a)$ to hold for the pair of distributions
$ (\krnl_1(a), \krnl_2(a)) $ for every $a$ with non-zero probability in $\prob$.
The definition naturally extends to any number of indices.

Imagine we want to express the (relational) assertion $\cpl{ \Ip{k}{1} = \Ip{c}{2} }$
in terms of .
Our proposal is to encode it as the existence of some
distribution $\prob \of \Dist(\Val\times\Val)$ over pairs of values,
such that
\CC\prob (v_1,v_2).\bigl(
\sure{\Ip{k}{1} = v_1} \land
\sure{\Ip{c}{2} = v_2} \land
\pure{v_1=v_2}
\bigr)
The assertion conditions both components getting pairs of
conditioned probabilities for each $(v_1,v_2)$ and then checks
that in each of these, both $\Ip{k}{1}$ and $\Ip{c}{2}$
become deterministic (with value $v_1$ and $v_2$ respectively)
and, finally, that the relation being lifted
(here, equality)
holds between their deterministic values.[Here the notation $\pure{\phi}$ denotes the embedding into the logic of a pure fact $\phi$ (a meta-level statement).]

The encoding hinges on the crucial decision in the design of the modality,
of using the same distribution $\prob$ to
decompose the distributions at all indices.
Depending on how the inner predicate $K(a)$ constrains the resulting
conditional probabilities, $\prob$ can induce an (imaginary) correlation
between the conditioning at each index.

The remarkable fact is that our formulation of
relational lifting directly explains:

* How the relational lifting can be established:
that is, by providing some joint distribution $\prob$ for
$\Ip{k}{1}$ and $\Ip{c}{2}$ ensuring $R$ (the relation being lifted)
holds for their joint outcomes;

* How the relational lifting can be used in entailments:
that is, it guarantees that if one conditions on the store,
$R$ holds between the (now deterministic) variables.

To make these definitions and connections come to fruition we need to
study which laws are supported by the  modality
and whether they are expressive enough to reason about distributions
without having to drop down to the level of semantics.

§.§ The Laws of

We survey the key laws for  in this section, and explore a vital consequence of defining both conditioning and relational lifting based on : the laws of both can be derived from a set of expressive laws about  alone. To keep the exposition concrete,
we focus on a small subset of laws that are enough to prove the example
of <ref>.
Let us focus first on proving:

\begin{equation}
\distAs{\Ip{k}{1}}{\Ber{\onehalf}}
\distAs{\Ip{m}{1}}{\Ber{p}}
\distAs{\Ip{c}{2}}{\Ber{\onehalf}}
\proves
\CC{\Ber{p}} v.
\left(
\sure{\Ip{m}{1}=v}
\begin{cases}
\cpl{ \Ip{k}{1} = \Ip{c}{2} }     \CASE v=0 \\
\cpl{ \Ip{k}{1} = \neg\Ip{c}{2} } \CASE v=1
\end{cases}
\right)
\label{ex:xor:entail1}
\end{equation}

We need the following primitive laws of :

P * v.K(v)
v.(P * K(v))

∀vK_1(v) K_2(v)

<Ref> can convert back and forth from
ownership of an expression $E$ at $i$ distributed as $\prob$,
and the conditioning on $\prob$ that makes $E$ look deterministic.
<Ref> allows to bring inside conditioning
any resource that is independent from it.
<Ref> simply allows to apply entailments inside .
We can use these laws to perform conditioning on $\Ip{m}{1}$:

(p v.m1=v)
p v.

Here we use <ref> to convert ownership of $\Ip{m}{1}$
into its conditioned form.
Then we can bring the other independent variables inside the conditioning
with <ref>.
This derivation follows closely in spirit the way in which Lilac
introduces conditioning, thus inheriting its ergonomic elegance.
Our rules however differ from Lilac's in both form and substance;
first, Lilac's C-Indep rule, used to introduce conditioning,
is a combination of our <ref> and <ref>,
which are independently useful.
Specifically, <ref> is bidirectional,
which makes it useful to recover unconditional facts from conditional ones.
Furthermore we recognize that <ref> is nothing but
a reflection of the right unit law of the monadic structure of distributions
(which we elaborate on in <ref>).
This connection prompted us to provide rules that reflect the remaining
monadic laws (left unit <ref> and associativity <ref>). It is noteworthy that these rules do not follow from Lilac's proofs:
our modality has a different semantics, and our rules seamlessly apply to
assertions of any arity.

To establish the conditional relational liftings of the entailment in (<ref>),
needs a way to introduce couplings from ownership of the distributions
of some variables:

∘_1 = _1

∘_2 = _2

(R) = 1

x_11_1 *
R(x_11, x_22)

The rule asks to provide a coupling of $\prob_1$ and $\prob_2$
which assigns probability 1 to a (binary) relation $R$.
If $\p{x}_1\at{\I1}$ and $\p{x}_2\at{\I2}$ are distributed as $\prob_1$ and $\prob_2$, respectively, then the relational lifting of $R$ holds between them.
Note that for the rule to apply, the two variables need to live in distinct

Interestingly, <ref> can be derived from the
encoding of relational lifting and the laws of .

Remarkably, although the rule mirrors the
step of coupling two samplings in a pRHL proof,
it does not apply to the code doing the sampling itself,
but to the assertions representing the effects of those samplings.
This allows us to delay the forming of coupling to until
all necessary information is available (here, the outcome of $\Ip{m}{1}$).
We can use <ref> to prove both entailments:

\begin{equation}
\distAs{\Ip{k}{1}}{\Ber{\onehalf}} *
\distAs{\Ip{c}{2}}{\Ber{\onehalf}}
\proves
\cpl{ \Ip{k}{1} = \Ip{c}{2} }
\text{\; and \; }
\distAs{\Ip{k}{1}}{\Ber{\onehalf}} *
\distAs{\Ip{c}{2}}{\Ber{\onehalf}}
\proves
\cpl{ \Ip{k}{1} = \neg\Ip{c}{2} }
\label{ex:xor-two-cpl}
\end{equation}

In the first case we use the coupling which flips a single coin and returns
the same outcome for both components, in the second we flip a single coin
but return opposite outcomes.
Thus we can now prove:

\[
\CC{\Ber{p}} v.
\left(
\sure{\Ip{m}{1}=v} *
\begin{pmatrix}
\distAs{\Ip{k}{1}}{\Ber{\onehalf}}
\\ {}*
\distAs{\Ip{c}{2}}{\Ber{\onehalf}}
\end{pmatrix}
\right)
\proves
\CC{\Ber{p}} v.
\left(
\sure{\Ip{m}{1}=v}
\begin{cases}
\cpl{ \Ip{k}{1} = \Ip{c}{2} }     \CASE v=0 \\
\cpl{ \Ip{k}{1} = \neg\Ip{c}{2} } \CASE v=1
\end{cases}
\right)
\]

by using <ref>,
and using the two couplings of (<ref>) in the $v=0$ and $v=1$ respectively.
Finally, the assignment to c in encrypt generates the fact
$\sure{\Ip{c}{1} = \Ip{k}{1} \xor \Ip{m}{1}}$.
By routine propagation of this fact we can establish
\CC{\Ber{p}} v. \cpl{ \Ip{c}{1} = \Ip{c}{2} }.
To get an unconditional lifting,
we need a principle explaining the interaction between lifting and conditioning.
can derive the general rule:

.R R

which states that relational liftings are convex,
closed under convex combinations.

<ref> is an instance of many rules on the interaction between relational lifting
and the other connectives (conditioning in this case)
that can be derived in  by exploiting the encoding of liftings as .

Let us see how this is done for <ref> based on two other primitive rules of :

v. x X. Q(v, x)
f A →X. v. Q(v, f(v))

_0 = (,v.(((v), w.(v,w))))

v.(v) w.K(v,w)
_0 (v,w).K(v,w)

<Ref> follows from Skolemization of the implicit universal
quantification used on $v$ by the modality.
<Ref> is a reflection of the associativity of the $\bind$ operation.
At the assertion level, the rule reads like a way to merge two nested modalities,
which is exactly what is needed to perform the crucial step.
We start by unfolding the definition of relational lifting
(we write $K(v)$ for the part of the encoding inside the conditioning):

v. R

w. K(w)
(v) w. K(w)
_0 (v,w). K(w)

The application of <ref> commutes the existential
quantification of the joint distribution $\hat{\prob}$ and the outer modality.
By <ref> we are able to merge the two modalities and obtain again
something of the same form as the encoding of relational liftings.

§.§ Outside the Box of Relational Lifting

One of the well-known limitations of pRHL is that it requires
a very strict structural alignment between the order of samplings
to be coupled in the two programs. The pattern from our running example, where two blocks of code
run in the reverse order does not change the output distribution, is a commonly occurring one in other proof arguments.
In , we can establish this pattern as a derived general rule:

{P_1} [1: t_1, 2: t_1'] {R_1}

{P_2} [1: t_2, 2: t_2'] {R_2}

{P_1 * P_2}
1: (t_1; t_2),
2: (t_2'; t_1')

The rule assumes that the lifting of $R_1$ (resp. $R_2$) can be established
by analyzing $t_1$ and $t_1'$ ($t_2$ and $t_2'$)
side by side from precondition $P_1$ ($P_2)$.
The standard sequential rule of pRHL would force an alignment
between the wrong pairs ($t_1$ with $t_2'$, and $t_2$ with $t_1'$) in the conclusion of the rule.
Crucial to the soundness of the rule is the assumption
(expressed by the precondition in the conclusion)
that $P_1$ and $P_2$ are probabilistically independent;
note that because of this, the rule cannot be just added to pRHL since
it lacks the construct of independence.

's treatment of relational lifting enables the study of the interaction
between lifting and independence,
unlocking a breakthrough solution for forfeiting strict structural similarities between components required by relational logics.

Two ingredients of  cooperate to prove
the adoption of a weakest precondition (WP) formulation of triples
(and associated rules)
and a novel property of relational lifting. Let us start with WP.
In , a triple $\{P\}\ \m{t}\ \{Q\}$ is actually encoded as
the entailment
$ P \proves \WP {\m{t}} {Q} $
between the precondition and a WP assertion.
Roughly speaking,
the assertion $\WP {\m{t}} {Q}$ takes an indexed tuple of terms $\m{t}$
and a postcondition $Q$ and holds on
a (indexed) tuple of distributions $\m{\prob}_0$,
if the tuple of output distributions
obtained by running the programs in $\m{t}$ on $\m{\prob}_0$,
satisfies $Q$.
provides a number of rules for manipulating WP;
here is a selection needed for deriving <ref>:

Q Q'

P Q
P Q

[i: t][]
*[i: t'] Q

[i: (t; t')] Q

(t_1 . t_2)Q

<Ref> are the usual consequence and framing rules
of Separation Logic, in WP form.
By adopting Lilac's measure-theoretic notion of independence as the interpretation for separating conjunction, we obtain a clean frame rule.[By using a “variables as resource” model, our <ref> rule
does not need side-conditions (see <ref>).
Among the WP rules for program constructs,
<ref> takes care of sequential composition.
Notably, we only need to state it for unary WPs,
in contrast to other logics where supporting relational proofs
requires building the lockstep strategy into the rules.
We use LHC's more flexible approach [D'Osualdo et al, 2022],
here surfacing as the <ref> rule,
where a handful of arity-changing rules allow seamless integration
of unary and relational judgments.
The <ref> rule, for instance,
establishes the equivalence of a WP with many components,
that is $ \m{t}_1 \m. \m{t}_2 $, where $(\m.)$ is union of indexed tuples with disjoint indexes,
and two nested WPs involving only some of the components
($\m{t}_1$, and $\m{t}_2$ individually).
This for instance allows us to lift the unary <ref>
to a binary lockstep rule:

P [1: t_1]
[2: t_2]Q'

Q' [1: t_1']
[2: t_2'] Q

P [1: t_1]
[2: t_2]
[1: t_1']
[2: t_2'] Q

P [1: t_1]
[1: t_1']
[2: t_2]
[2: t_2'] Q

P [1: (t_1; t_1')]
[2: (t_2;t_2')] Q

P [1: (t_1; t_1'), 2: (t_2;t_2')] Q

The crucial idea behind <ref> is that the two programs
$t_1$ and $t_2$ we want to swap rely on independent resources,
which is done through framing in Separation Logic:
while executing $t_1$ frame the resources
needed for $t_2$ which remain intact in the state left by $t_1$.
Here, however, we want to frame a conjunct of the relation
inside a relational lifting, say $R_1$, which is accommodated by:

R_1 * R_2
R_1 R_2

We do not show the derivation here for space constraints,
but essentially it consists in unfolding the encoding of lifting,
and using <ref> and <ref>
to merge the two  modalities.

Using these rules we can construct the following derivation:
P_1 [1: t_1, 2: t_1']R_1

P_2 [1: t_2, 2: t_2']R_2

P_1 * P_2
[1: t_1,2: t_1']

[1: t_2, 2: t_2' ]

P_1 * P_2
[1: t_1][]
1: t_2,
2: t_2'
[2: t_1']

P_1 * P_2
[1: t_1][]
1: t_2,
2: t_2'
R_2 *
[2: t_1']

P_1 * P_2
[1: t_1][]
1: t_2,
2: t_2'
[2: t_1']
R_1 *

P_1 * P_2
[1: (t_1; t_2)][]
[2: (t_2'; t_1')]
R_1 *

P_1 * P_2
1: (t_1; t_2),
2: (t_2'; t_1')
R_1 *

P_1 * P_2
1: (t_1; t_2),
2: (t_2'; t_1')
R_1 R_2

We explain the proof strategy from bottom to top.
We first apply <ref> to the postcondition
(thanks to <ref>).
This step reduces the goal to proving the two relational liftings
can be established independently from each other.
Then we apply <ref> and <ref>
to separate the two indices, break the sequential compositions and recombine
the two inner WPs.
We then proceed by three applications of the <ref> rule:
the first brings $\cpl{R_2}$ out of the innermost WP;
the second brings the WP on $\m[\I1:t_1']$ outside the middle WP;
the last brings the WP on $\m[\I1:t_2,\I2:t_2']$ outside the topmost WP.
An application of <ref> merges the resulting nested WPs
on $t_1$ and $t_1'$.
We thus effectively reduced the problem to showing that the two WPs
can be established independently, which was our original goal.

The <ref> rule is not only an elegant way of overcoming
a long-standing issue with relational lifting;
it also shows how fundamental the role of probabilistic independence
as a construct is for compositional reasoning:
the same rule with standard conjunction is unsound!
Intuitively, if we just had $ \cpl{R_1} \land \cpl{R_2} $,
we would know there exist two couplings
$\prob_1$ and $\prob_2$,
justifying $\cpl{R_1}$ and $\cpl{R_2}$ respectively,
but the desired consequence $\cpl{R_1 \land R_2}$
requires the construction of a single coupling that justifies both relations
at the same time.
We can see this is not always possible by looking back at
for two fair coins we can establish
\cpl{ \Ip{k}{1} = \Ip{c}{2} }
\land
\cpl{ \Ip{k}{1} = \neg\Ip{c}{2} }
\cpl{
\Ip{k}{1} = \Ip{c}{2}
\land
\Ip{k}{1} = \neg\Ip{c}{2}
$ is equivalent to false.

§ PRELIMINARIES: PROGRAMS AND PROBABILITY SPACES

To formally define the model of  and validate its rules,
we introduce a number of preliminary notions.
Our starting point is the measure-theoretic approach of
[Li et al, 2023] in defining probabilistic separation.
We recall the main definitions here.
The main additional assumption we will make throughout
is that the set of outcomes of distributions is countable.

Given a set of possible outcomes $\Outcomes$,
a  $ \salg \in \SigAlg(\Outcomes) $ is
a set of subsets of $\Outcomes$ such that
$\Outcomes \in \salg$ and
is closed under countable unions and
The full  over $\Outcomes$ is
$ \Full{\Outcomes} = \powerset(\Outcomes) $,
the powerset of $\Outcomes$.
For $F \subs \powerset(\Outcomes)$, we write $\sigcl{F} \in \SigAlg(\Outcomes)$
for the smallest  containing $F$.
Given $\salg \in \SigAlg(\Outcomes)$,
a probability distribution $\prob \in \Dist(\salg)$,
is a countably additive function $ \prob \from \salg \to [0,1] $
with $\prob(\Outcomes)=1$.
The support of a distribution $\prob \in \Dist(\Full{\Outcomes})$
is the set of outcomes with non-zero probability
$ \psupp(\prob) \is \set{ a \in \Outcomes | \prob(a) > 0 } $,
where $\prob(a)$ abbreviates $\prob(\set{a})$.

A probability space $ \psp \in \ProbSp(\Outcomes) $ is
a pair $ \psp = (\salg, \prob) $ of
a  $\salg \in \SigAlg(\Outcomes)$ and
a probability distribution $\prob \in \Dist(\salg)$.
The trivial probability space $\Triv{\Outcomes} \in \ProbSp(\Outcomes)$
is the trivial  $ \set{\Outcomes,\emptyset} $
equipped with the trivial probability distribution.
Given $\salg_1 \subs \salg_2$ and $\prob \in \Dist(\salg_2)$,
the distribution $ \restr{\prob}{\salg_1} \in \Dist(\salg_1) $
is the restriction of $\prob$ to $\salg_1$.
The extension pre-order $(\extTo)$ over probability spaces is defined as
(\salg_1, \prob_1) \extTo (\salg_2, \prob_2) \is
\salg_1 \subs \salg_2 \land \prob_1 = \restr{\prob_2}{\salg_1}.

A function $f \from \Outcomes_1 \to \Outcomes_2$ is
measurable on
$ \salg_1\in\SigAlg(\Outcomes_1)$ and $\salg_2\in\SigAlg(\Outcomes_2) $
$ \forall \event \in \salg_2 \st {\inv{f}(\event) \in \salg_1} $.
When $\salg_2 = \Full{\Outcomes_2}$
we simply say $f$ is measurable in $\salg_1$.

Given $ \salg_1 \in \SigAlg(\Outcomes_1),\salg_2 \in \SigAlg(\Outcomes_2) $,
their product is the
$ \salg_1 \pprod \salg_2 \in \SigAlg(\Outcomes_1 \times \Outcomes_2) $
defined as
$ \salg_1 \pprod \salg_2 \is \sigcl{\set{\event_1 \times \event_2 | \event_1 \in \salg_1, \event_2 \in \salg_2}} $,
and their union is the
$ \salg_1 \punion \salg_2 \is \sigcl{\salg_1 \union \salg_2} $.
The product of two probability distributions
$ \prob_1 \in \Dist(\salg_1) $ and
$ \prob_2 \in \Dist(\salg_2) $ is
the distribution
$ (\prob_1 \pprod \prob_2) \in \Dist(\salg_1 \pprod \salg_2) $
defined by
$ (\prob_1 \pprod \prob_2)(\event_1 \times \event_2) = \prob_1(\event_1)\prob_2(\event_2) $
for all $\event_1 \in \salg_1$, $\event_2 \in \salg_2$.

Given $ (\salg_1, \prob_1),(\salg_2, \prob_2) \in \ProbSp(\Outcomes) $,
their independent product is
the probability space
$(\salg_1 \punion \salg_2, \prob) \in \ProbSp(\Outcomes)$
where for all $ \event_1 \in \salg_1, \event_2 \in \salg_2 $,
\prob(\event_1 \inters \event_2) = \prob_1(\event_1)\prob_2(\event_2)
$. It is unique, if it exists <cit.>. Let $ \psp_1 \iprod \psp_2 $ be the unique independent product
of $\psp_1$ and $\psp_2$ when it exists, and be undefined otherwise.

Indexed tuples
To deal uniformly with unary and higher-arity relational assertions,
will consider finite sets of indices $I \subs \Nat$,
and I-indexed tuples of objects of type $X$,
represented as (finite) functions $\Hyp[I]{X}$.
We use boldface to range over such functions.
The syntax $ \m{x} = \m[i_0: x_0,\dots,i_n: x_n] $ denotes the function
$ \m{x} \in \Hyp[\set{i_0,\dots,i_n}]{X} $ with $\m{x}(i_k) = x_k$.
We often use comprehension-style notation $\m{x} = \m[i: x_i | i\in I]$.
For $\m{x} \in \Hyp[I]{A}$ we let $\supp{\m{x}} \is I$.
Given some $ \m{x} \in \Hyp[I]{A} $ and some $J \subs I$,
the operation $ \m{x} \setminus J \is \m[i: \m{x}(i) | i \in I \setminus J] $
removes the components with indices in $J$ from $\m{x}$.

We consider a simple first-order imperative language.
We fix a finite set of program variables $\p{x} \in \Var$
and countable set of values $\val \in \Val \is \Int$
and define the program stores to be
$ \store \in \Store \is \Var \to \Val $
(note that $\Store$ is countable).

∋| x | ()
+ | - | < | …    Ber | Unif | …

| x
| | _1_2
| _1_2

Syntax of program terms.

Program terms $ \term \in \Term $ are formed according to the
grammar in <ref>.
For simplicity,
booleans are encoded by using $0 \in \Val$ as false and any other value as true.
We will use the events
$\false \is \set{0}$ and
$\true \is \set{n \in \Val | n\ne 0}$.
Programs use standard deterministic primitives $\prim$,
which are interpreted as expected as functions
$ \sem{\prim} \from \Val^n \to \Val $, where $n$ is the arity of $\prim$.
Expressions $\expr$ are effect-free deterministic numeric expressions,
and denote, as is standard, a function
$ \sem{\expr} \from \Store \to \Val $,
a random variable of $\Full{\Store}$.
We write $\pvar(\expr)$ for the set of program variables that occur
in $\expr$.
Programs can refer to some collection of known
discrete distributions $\dist$,
each allowing a certain number of parameters.
Sampling assignments $ \code{x:~$\dist$($\vec{v}$)} $
sample from the distribution $\Sem{\dist}(\vec{v}) \from \Dist(\Full{\Val})$.
The distribution $ \Sem{\p{Ber}}(p) = \Ber{p} \of\Dist(\Full{\set{0,1}}) $
is the Bernoulli distribution assigning probability $p$ to outcome 1.

Similarly to Lilac, we consider a simple iteration construct
$ \code{repeat}\; e\; t $ which evaluates $e$ to a value $n \in \Val$
and, if $n>0$, executes $t$ in sequence $n$ times.
This means we will only consider almost surely terminating programs.
Programs semantics,
entirely standard and defined in sec:appendix:definition,
associates to each term $t$ a function
\sem{t} \from \Dist(\Full{\Store}) \to \Dist(\Full{\Store})
from distributions of input stores to
distributions of output stores.

In the relational reasoning setting, one would consider multiple
programs at the same time and relate their semantics.
Following LHC [D'Osualdo et al, 2022],
we define hyper-terms as $ \m{t} \in \Hyp[J]{\Term} $
for some finite set of indices $J$.
Let $I$ be such that $\supp{\m{t}} \subs I$; the semantics
\sem{\m{t}}_I \from
\Hyp[I]{\Dist(\Full{\Store})} \to \Hyp[I]{\Dist(\Full{\Store})}
takes a I-indexed family of distributions as input and outputs
another I-indexed family of distributions:

\[
\sem{\m{t}}_I(\m{\prob}) \is
\fun i.
\ITE{i \in \supp{\m{t}}}{
\sem{\m{t}(i)}(\m{\prob}(i))
\m{\prob}(i)
\]

Note that the store distributions at indices in $ I \setminus \supp{t} $
are preserved as is.
We omit $I$ when it can be inferred from context.
To refer to program variables in a specific component we will use
elements of $I\times \Var$, writing $\ip{x}{i}$ for $(i,\p{x})$.

§ THE  LOGIC

We are now ready to define 's semantic model,
and formally prove its laws.

§.§ A Model of (Probabilistic) Resources

As a model for our assertions we use a modern presentation of
partial commutative monoids, adapted from [Krebbers et al, 2018],
called “ordered unital resource algebras” (henceforth RA).

An ordered unital resource algebra (RA) is a tuple
(M, \raLeq, \raValid, \raOp, \raUnit)
$ \raLeq \from M \times M \to \Prop $ is the reflexive and transitive
resource order,
$ \raValid \from M \to \Prop $ is the validity predicate,
$ (\raOp) \from M \to M \to M $ is the resource composition,
a commutative and associative binary operation on $M$,
$ \raUnit \in M $ is the unit of $M$,
satisfying, for all $a,b,c\in M$:

a = a

(a b)

a b

a b

a c b c

We define some basic RA constructions, that combined, construct 's RA.
The main component is the Probability Spaces RA,
which uses independent product as the RA operation.

The probability spaces RA
$ \PSpRA_\Outcomes $
is the RA
$(\ProbSp(\Outcomes) \dunion \set{\invalid}, \raLeq, \raValid, \raOp, \Triv{\Outcomes})$
$\raLeq$ is the extension order with $\invalid$ added as the top element,
$ \psp_1 \raLeq \psp_2 \is \psp_1 \extTo \psp_2 $ and
$ \forall a \in \PSpRA_\Outcomes\st
a \raLeq \invalid$;
$\raValid(a) \is a \neq \invalid$;
composition is independent product:
\[
a \raOp b \is
\begin{cases}
\psp_1 \iprod \psp_2
\CASE a=\psp_1, b=\psp_2, \text{ and }
\psp_1 \iprod \psp_2 \text{ is defined}
\\
\invalid \OTHERWISE
\end{cases}
\]

The fact that $\PSpRA_\Outcomes$ satisfies the axioms of RAs is
established in sec:appendix:model and builds on the analogous
construction in Lilac.
In comparison with the coarser model of PSL,
independent product represents a more sophisticated way of separating
probability spaces.
In PSL separation of distributions requires the distributions to
involve disjoint sets of variables, ruling out
assertions like
$ \distAs{\p{x}}{\prob} * \sure{\p{x}=\p{y}} $
$ \distAs{(\p{x}+\p{y})}{\prob_1} * \distAs{(\p{x}-\p{y})}{\prob_2} $,
which are satisfiable in Lilac's and 's model.

There is however an obstacle in adopting independent product in a language
with mutable state (whereas Lilac uses a functional language).
When assigning to a variable x, we need to make sure no frame
can remember facts about the current distribution of x,
as these could be invalidated after the assignment (making framing unsound).
We solve this problem by combining $\PSpRA$ with an RA of permissions over variables.

The permissions RA
$(\Perm, \raLeq, \raValid, \raOp, \raUnit)$
is defined as
$ \Perm \is \Var \to \PosRat $,
$ a \raLeq b \is \forall \p{x} \in \Var \st a(\p{x}) \leq b(\p{x}) $,
$ \raValid(a) \is (\forall \p{x} \in \Var \st a(\p{x}) \leq 1) $,
$ a_1 \raOp a_2 \is \fun \p{x}. a_1(\p{x}) + a_2(\p{x})$ and
$ \raUnit = \fun \wtv.0 $.

The idea is that to be able to assign to x one needs
permission $1$ on x, which implies any frame would have
no permission over it.
To make this a meaningful restriction over the probability space information,
we define a notion of compatibility between permissions and probability spaces.

Given a probability space $\psp \in \ProbSp(\Store)$ and
a permission map $\permap \in \Perm$,
we say that $\psp$ is compatible with $\permap$,
written $\psp\compat\permap$,
if there exists
$\psp' \in \ProbSp((\Var \setminus S) \to \Val)$
such that
$\psp = \psp' \pprod \Triv{S \to \Val}$,
$S = \set{x \in \Var | \permap(x) = 0}.$
Note that we are exploiting the isomorphism
\Store \iso
((\Var \setminus S) \to \Val)
\times
(S \to \Val).
We extend the notion to $ \PSpRA_{\Store} $
by declaring $ \invalid \compat \permap \is \True$.

\PSpPmRA \is
\set{
(\maybePsp, \permap)
| \maybePsp \in \PSpRA_{\Store},
\permap \in \Perm,
\maybePsp \compat \permap
We associate with $\PSpPmRA$ the
Probability Spaces with Permissions RA
(\PSpPmRA, \raLeq, \raValid, \raOp, \raUnit)

\begin{align*}
\raValid((\maybePsp, \permap)) &\is
\maybePsp \neq \invalid
\land \forall\p{x}.\permap(\p{x}) \leq 1
(\maybePsp, \permap) \raOp (\maybePsp', \permap') &\is
(\maybePsp \raOp \maybePsp', \permap \raOp \permap')
\\
(\maybePsp, \permap) \raLeq (\maybePsp', \permap') &\is
\maybePsp \raLeq \maybePsp'
\text{ and }
\permap \raLeq \permap'
\raUnit &\is ( \Triv{\Store}, \fun \p{x}. 0)
\end{align*}

What this RA achieves is to link the fact of having permission 0
on some x to necessarily owning a probability space that is trivial
on x.
This allows
\distAs{\p{x}}{\prob} * \sure{\p{x}=\p{y}}
to still be satisfiable since we can distribute half permissions on x
to the first assertion an the other half to the second one.
Yet we can disallow frames with information about x
by simply asserting we own permission 1 on x.
While this allows for a clean semantic treatment of mutation and independence,
it does incur in practice into some bookkeeping of permissions,
which we omitted in the examples of <ref>.
The necessary permissions are however very easy to infer
from the variables used in the triples.

To build 's model we only need to construct an RA
of I-indexed tuples of probability spaces with permissions.

Given a set of indices $I$ and a RA $M$,
the product RA $ \Hyp[I]{M} $ is the pointwise lifting
of the components of $M$.
's model is $\Model_I \is \Hyp{\PSpPmRA}$.

§.§ Probabilistic Hyper-Assertions

Now we turn to the assertions in our logic.
We take a semantic approach to assertions:
we do not insist on a specific syntax and instead characterize
what constitutes an assertion by its type.
In Separation Logic, assertions are defined relative to some RA $M$,
as the upward closed functions $ M \to \Prop $.
An assertion $ P \from M \to \Prop $ is upward closed if
$ \forall a, a' \in M\st a \raLeq[M] a' \implies P(a) \implies P(a'). $
We write $ M \ucto \Prop $ for the type of upward closed assertions on $M$.
We define hyper-assertions to be assertions over $\Model_I$,
$P \in \HAssrt_I \is \Model_I \ucto \Prop $.
Entailment is defined as
(P \proves Q) \is
\forall a \in M\st
\raValid(a) \implies (P(a) \implies Q(a)).
Logical equivalence is defined as entailment in both directions:
$ P \lequiv Q \is (P \proves Q) \land (Q \proves P) $.
We inherit the basic connectives
(conjunction, disjunction, separation, quantification)
from SL, which are well-defined on arbitrary RAs, including $\Model_I$.
In particular:

\begin{align*}
P * Q &\is \fun a.
\exists b_1,b_2 \st
(b_1 \raOp b_2) \raLeq a \land
P(b_1) \land
\pure{\varphi} &\is \fun \wtv. \varphi
\Own{b} &\is \fun a. b \raLeq a
\end{align*}

Pure assertions $\pure{\varphi}$ lift meta-level propositions $\varphi$
to assertions (by ignoring the resource).
$\Own{b}$ holds on resources that are greater or equal than $b$ in the RA order;
this means $b$ represents a lower bound on the available resources.

We now turn to assertions
that are specific to probabilistic reasoning in ,
the ones that can only be interpreted in $\Model_I$.
We use the following two abbreviations:

\begin{align*}
\Own{\m{\salg}, \m{\prob}, \m{\permap}} &\is
\Own{((\m{\salg}, \m{\prob}), \m{\permap})}
\Own{\m{\salg}, \m{\prob}} &\is
\E \m{\permap}. \Own{\m{\salg}, \m{\prob}, \m{\permap}}
\end{align*}

To start, we define A-typed assertion expressions $ \aexpr $
which are of type
$ \aexpr \from \Store \to A $.
Note that the type of the semantics of a program expression $\sem{\expr} \from \Store \to \Val$ is a -typed assertion expression; because of this we seamlessly use program expressions in assertions, implicitly coercing them to their semantics.
Since in general we deal with hyper-stores $\m{\store} \in \Hyp{\Store}$,
we use the notation $\aexpr\at{i}$ to denote the application of $\aexpr$ to the
store $\m{\store}(i)$.
Notationally, it may be confusing to read composite expressions like
$ (\p{x}-\p{z})\at{i} $, so we write them for clarity with each program variable annotated with the index, as in $\ip{x}{i} - \ip{z}{i}$.

The meaning of owning $ \distAs{\Ip{x}{1}}{\prob} $
A function $ f \from A \to B $ is measurable in a
$ \salg \of \SigAlg(A) $ if $ \inv{f}(b) = \set{a \in A | f(a) = b} \in \salg $.
An expression $\aexpr$ always defines a measurable function
(a random variable)
in $\Full{\Store}$,
but might not be measurable in some sub-algebras of $\Full{\Store}$.
Lilac proposed to use measurability as the notion of ownership:
a certain $\aexpr$ is locally owned if it is measurable in the local sub-algebra.
While this makes sense conceptually,
we discovered it made another important connective of Lilac,
almost sure equality, slightly flawed
(in that it would not support the necessary laws).[In fact, a later revision [Li et al, 2023] corrected the issue,
although with a different solution from ours.
See <ref>.]
We propose a slight weakening of the notion of measurability which solves
those issues while still retaining the intent behind the meaning of ownership in relation to independence and conditioning.
We call this weaker notion “almost measurability”.

Given a probability space $ (\salg,\prob) \in \ProbSp(\Outcomes) $
and a set $\event \subs \Outcomes$,
we say $ \event $ is almost measurable in $(\salg, \prob)$,
written $ \almostM{\event}{(\salg, \prob)} $,
\[
\exists \event_1,\event_2 \in \salg \st
\event_1 \subs \event \subs \event_2
\land
\prob(\event_1)=\prob(\event_2).
\]

We say a function $ \aexpr \from \Outcomes \to A $,
is almost measurable in $(\salg, \prob)$,
written $ \almostM{\aexpr}{(\salg, \prob)} $,
if $
{\almostM{\inv{\aexpr}(a)}{(\salg, \prob)}}
for all $a \in A$.
$ \event_1 \subs \event \subs \event_2$
$ \prob(\event_1)=\prob(\event_2)=p $,
we can unambiguously assign probability $p$ to $\event$,
as any extension of $\prob$ to $\Full{\Outcomes}$ must
assign $p$ to $\event$;
then we write $\prob(\event)$ for $p$.

While almost-measurability does not imply measurability,
it constrains the current probability space to contain enough information
to uniquely determine the distribution of $\aexpr$ in any
extension where $\aexpr$ becomes measurable.
For example let $X=\set{\store | \store(\p{x}) = 42}$ and
$ \salg = \sigma(\set{\event}) = \set{\Store,\emptyset,X,\Store\setminus X}$.
If $ \prob(X) = 1 $, then $ \almostM{\p{x}}{(\salg,\prob)} $
holds but $\p{x}$ is not measurable in $\salg$, as $\salg$ lacks events
for $\p{x}=v$ for all $v$ except $42$.
Nevertheless, any extension $(\salg',\prob') \extOf (\salg,\prob)$
where $\p{x}$ is measurable,
would need to assign $\prob'(X) = 1$ and
$\prob(\p{x}=v) = 0$ for every $v \ne 42$.

We arrive at the definition of the assertion
$\distAs{\aexpr\at{i}}{\prob}$ which requires
$\aexpr\at{i}$ to be almost-measurable,
determining its distribution as $\prob$ in any extension
of the local probability space.
Formally, given $ \prob \of \Dist(\Full{A}) $ and $\aexpr \from \Store \to A$,
we define:

\begin{align*}
\distAs{\aexpr\at{i}}{\prob} & \is
\E \m{\salg},\m{\prob}.
\Own{\m{\salg},\m{\prob}} *
\pure{
\almostM{\aexpr}{(\m{\salg}(i),\m{\prob}(i))}
\land
\prob = \m{\prob}(i) \circ \inv{\aexpr}
\end{align*}

The assertion states that we own just enough information about the probability
space at index $i$, so that its distribution is uniquely determined as $\prob$ in any extension of the space.

Using this connective we can define a number of useful derived assertions:

\begin{align*}
\expectOf{\aexpr\at{i}} = r & \is
\E \prob.
\distAs{\aexpr\at{i}}{\prob} *
\pure{
r = \Sum*_{a\in\psupp(\prob)} \prob(a) \cdot a
\sure{\aexpr\at{i}} &\is
\distAs{(\aexpr \in \true)\at{i}}{\dirac{\True}}
\\
\probOf{\aexpr\at{i}} = r & \is
\E \prob.
\distAs{\aexpr\at{i}}{\prob} *
\pure{
\prob(\true) = r
\own{\aexpr\at{i}} &\is
\E \prob. \distAs{\aexpr\at{i}}{\prob}
\end{align*}

Assertions about
expectations ($\expectOf{\aexpr\at{i}}$) and
probabilities ($\probOf{\aexpr\at{i}}$),
simply assert ownership of some distribution with the desired (pure) property.
The “almost surely” assertion
$\sure{\aexpr\at{i}}$ takes a boolean-valued expression $\aexpr$ and
asserts that it holds (at $i$) with probability 1.
Note that, for example, an assertion like
$\sure{\Ip{x}{1}\geq v}$ owns the expression $(\Ip{x}{1}\geq v)$ but not necessarily $\Ip{x}{1}$:
the only events needed to make the expression almost measurable are
$ (\Ip{x}{1}\geq v) $ and its negation, which would be not enough to
make $\Ip{x}{1}$ itself almost measurable.
This means that an assertion like
$ \distAs{\Ip{x}{1}}{\prob} * \sure{\Ip{x}{1}\geq v} $ is satisfiable.

The previous example highlights the difficulty with supporting mutable state:
owning $ \distAs{\Ip{x}{1}}{\prob} $ is not enough to allow safe mutation,
because the frame can record information like $\sure{\Ip{x}{1}\geq v}$,
which could be invalidated by an assignment to $\p{x}$.
Our solution uses permissions, for which we define the assertion:
\perm{\ip{x}{i}:q} \is
\E\m{\permap}.
\Own{\m{\permap}}
* \pure{\m{\permap}(i)(\p{x}) = q}.
Now owning $\perm{\Ip{x}{1}:1}$ forbids any frame to retain information
about $\Ip{x}{1}$.
Define for brevity the assertion
P\withp{\m{\permap}} \is
P \land \E\m{\psp}.\Own{\m{\psp}, \m{\permap}}.
In practice, preconditions are always of the form
$ P\withp{\m{\permap}} $ where $\m{\permap}$ contains full permissions
for every variable the relevant program mutates.
When framing, one would distribute evenly the permissions to each separated
conjunct, according to the variables mentioned in the assertions.
This is completely analogous to the “variables as resource”
technique in SL [Bornat et al, 2005].
To avoid cluttering derivations with this tedious bookkeeping,
we omit permission information from assertions.

\let\LabTirName\RuleNameLbl \infer*[lab=and-to-star]{
\idx(P) \inters \idx(Q) = \emptyset
P \land Q \proves P \sepand Q
}   \label{rule:and-to-star}

Relevant indices
Sometimes it is useful to determine which indices are relevant for an assertion.
Semantically, we can determine if the indices $J \subs I$ are irrelevant to $P$
\irrel_J(P) \is
\forall a \in \Model_I \st
\bigl(
\exists \pr{a} \st
\raValid(\pr{a})
\land
a = \pr{a} \setminus J
\land P(\pr{a})
\bigr)
\implies P(a).
The set $\idx(P)$ is the smallest subset of $I$ so that
$ \irrel_{I\setminus \idx(P)}(P) $ holds.
<Ref> states that separation between resources
that live in different indexes is the same as normal conjunction:
distributions at different indexes are neither independent nor correlated;
they simply live in “parallel universes” and can be related as needed.

As we discussed in <ref>,
the centerpiece of  is the  modality,
which we can now define fully formally.

Let $ \prob \in \Dist(\Full{A}) $
and $ K \from A \to \HAssrt_I $,
then we define the assertion
$ \CMod{\prob} K \of \HAssrt_I $
as follows
(where $ \m{\krnl}(I)(v) \is \m[i: \m{\krnl}(i)(v) | i \in I] $):

\begin{align*}
\CMod{\prob} K &\is
\fun a.
\begin{array}[t]{@{}r@{\,}l@{}}
\E \m{\sigmaF}, \m{\mu}, \m{\permap}, \m{\krnl}.
& (\m{\sigmaF}, \m{\mu}, \m{\permap}) \raLeq a
\land
\forall i\in I\st
\m{\mu}(i) = \bind(\prob, \m{\krnl}(i))
\\ & \land \;
\forall v \in \psupp(\prob).
K(v)(\m{\sigmaF}, \m{\krnl}(I)(v), \m{\permap})
\end{array}
\end{align*}

The definition follows the principle we explained in
$ \CMod{\prob} K $ holds on resources where we own some
tuple of probability spaces which we can all be seen
as the convex combinations of the same $\prob$ and some kernel.
Then the conditional assertion $K(a)$ is required to hold on the
tuple of kernels evaluated at $a$.
Note that the definition is upward-closed by construction.

v_0 v.K(v)

f (') →()

∀b ∈(') '(b) = (f(b))

' b.K(f(b))

(K_1) (K_2) = ∅
v. K_1(v)
v. K_2(v)
(K_1(v) K_2(v))

v.(K(v) * i)
i * v.K(v)

()=1 * v.K(v)
v.(v ∈ * K(v))

Primitive Conditioning Laws.

We discussed a number of  laws in <ref>.
<Ref> shows some important primitive laws
that were left out.
<Ref> allows to introduce a trivial modality;
together with <ref> this allows for the introduction
of the modality around any assertion.
<Ref> is a reflection of the left unit rule of the underlying
monad: conditioning on the Dirac distribution can be eliminated.
<Ref> allows for the transformation of the
convex combination using $\prob$
into using $\prob'$ by applying a bijection between their support
in a way that does not affect the weights of each outcome.
<Ref> allows to merge two modalities using the same $\prob$,
provided the inner conditioned assertions do not overlap
in their relevant indices.
The rule is unsound without the side condition:
The two modalities might use in general different kernels
to bind $\prob$.
In contrast, Lilac's unary modality validates
$ \LC{x}{X} P_1 \land \LC{x}{X} P_2 \proves \LC{x}{X} (P_1 \land P_2) $,
underlining the fact that their semantics differs from ours.

<Ref> internalizes a stronger version of convexity of
$ \sure{\aexpr\at{i}} $ assertions.
When $K(v) = \True$ we obtain convexity
\CC\prob v.\sure{\aexpr\at{i}}
\proves
\sure{\aexpr\at{i}}.
Additionally the rule asserts that the unconditional $\sure{\aexpr\at{i}}$
keeps being independent of the conditional $K$.

Finally, <ref> allows to translate facts that hold with probability 1 in $\prob$ to predicates that hold on every $v$ bound by conditioning on $\prob$.

We can now give the general encoding of relational lifting
in terms of .

Let $X \subs \Idx \times \Var$;
given a relation $R$ between variables in $X$,
$R \subs \Val^{X}$,
we define
\sure{\ip{x}{i} = \m{v}(\ip{x}{i})}_{\ip{x}{i}\in X} \is
\LAnd_{\ip{x}{i}\in X}
\sure{\ip{x}{i} = \m{v}(\ip{x}{i})}

\begin{align*}
\cpl{R} &\is
\E \prob.
\pure{\prob(R) = 1} *
\CC\prob \m{v}.
\sure{\ip{x}{i} = \m{v}(\ip{x}{i})}_{\ip{x}{i}\in X}
\end{align*}

In <ref>,
the two relations might refer to different indexed variables,
$R_1\in \Val^{X_1}$ and $R_2\in \Val^{X_2}$;
the notation $R_1 \land R_2$ is defined as
R_1 \land R_2 \is
\set*{ \m{s} \in \Val^{X_1\union X_2}
| \restr{\m{s}}{X_1} \in R_1 \land \restr{\m{s}}{X_2} \in R_2

§.§ Weakest Precondition

To reason about (hyper-)programs,
we introduce a weakest-precondition assertion (WP)
$\WP {\m{t}} {Q}$, which intuitively states:
given the current input distributions (at each index),
if we run the programs in $\m{t}$ at their corresponding index
we obtain output distributions that satisfy $Q$;
furthermore, every frame is preserved.
We refer to the number of indices of $\m{t}$ as the arity of the WP.

For $a\in\Model_I$ and $\m{\prob} \of \Dist(\Full{\Hyp{\Store}})$
let $ a \raLeq \m{\prob} $ mean
a \raLeq (\Full{\Hyp{\Store}},\m{\prob},\fun x.1).

\[
\WP {\m{t}} {Q} \is
\fun a.
\forall \m{\prob}_0.
\forall c \st
(a \raOp c) \raLeq \m{\prob}_0
\implies
\exists b \st
\bigl(
(b \raOp c) \raLeq \sem{\m{t}}(\m{\prob}_0)
\land
\bigr)
\]

The assertion holds on the resources $a$ such that
if, together with some frame $c$,
they can be seen as a fragment of the global distribution
$\m{\prob}_0$, then it is possible to update the resource
to some $b$ which still composes with the frame $c$,
and $b\raOp c$ can be seen as a fragment of the output distribution
Moreover, such $b$ needs to satisfy the postcondition $Q$.

We discussed some of the WP rules of  in <ref>;
the full set of rules is produced in sec:appendix:rules.
Let us briefly mention the axioms for assignments:
xi : 1
[i: x: $\dist$($\vec{v}$)]

x ∉()

∀y ∈() (yi) > 0

[i: x:=][]
xi = i

<Ref> is the expected “small footprint” rule for
sampling; the precondition only requires full permission on the variable
being assigned, to forbid any frame to record information about it.
<Ref> requires full permission on x,
and non-zero permission on the variables on the RHS of the assignment.
This allows the postcondition to assert that x and the expression $\expr$
assigned to it are equal with probability 1.
The condition $\p{x} \notin \pvar(\vec{\expr})$ ensures $\expr$ has the same
meaning before and after the assignment, but is not restrictive:
if needed the old value of x can be stored in a temporary variable,
or the proof can condition on x to work with its pure value.

§ CASE STUDIES FOR

Within the space limits, we use three case studies to highlight the
novel features of , complementing the tour of <ref>.
First we sketch the proof of the Monte Carlo algorithm of <ref>
and a variant of it,
highlighting how  can deal with relational proofs on programs with very different structure.

is not only well-suited for analyzing programs,
but also able to derive more high-level proof principles.
Our second example explains how pRHL-style reasoning can be
effectively embedded and extended in , highlighting this fact.
The third example illustrates how  can carry out
unary reasoning in the style of Lilac,
but enabling proofs that in Lilac would require
ad hoc lemmas proven at the semantic level.

Full deductive proofs are long, and not all details are interesting.
Details of derivations and additional examples can be
found in sec:appendix:examples.

§.§ Monte Carlo Algorithms

Recall the example in Figure <ref> and the goal
outlined in <ref> of comparing the accuracy of the two
Monte Carlo algorithms BETW_SEQ and BETW.
This goal can be encoded as

\[
\begin{conj}
\sure{\Ip{l}{1}=\Ip{r}{1}=0} *{}\\
\sure{\Ip{l}{2}=\Ip{r}{2}=0}
\end{conj}
\withp{\m{\permap}}
\proves
\WP {\m<
\I1: \code{BETW_SEQ($x$, $S$)},
\I2: \code{BETW($x$, $S$)}
>} {
\cpl{\Ip{d}{1} \leq \Ip{d}{2}}
\]

(where $\m{\permap}$ contains full permissions for all the variables)
which, through the relational lifting, states that it is more likely
to get a positive answer from BETW than from BETW_SEQ.
The challenge is implementing the intuitive relational argument
sketched in <ref>,
in the presence of very different looping structures.
More precisely, we want to compare the sequential composition of two loops
$ l_1 = (\Loop{N}{\tA}\p;\Loop{N}{\tB}) $
with a single loop
$ l_2 = \Loop{(2N)}{t} $
considering the $N$ iterations of $\tA$ in lockstep with the first $N$ iterations of $l_2$, and the $N$ iterations of $\tB$ with the remaining $N$ iterations of $l_2$.
It is not possible to perform such proof purely in pRHL, which can only handle loops that are perfectly aligned, and tools based on pRHL overcome this limitation by offering a number of code transformations, proved correct externally to the logic, with which one can rewrite the loops so that they syntactically align. In this case such a transformation could look like
$ \Loop{(M+N)}{t} \equiv \Loop{M}{t}\p;\Loop{N}{t} $,
using which one can rewrite $l_2$ so it aligns with the two shorter loops.
What  can achieve is to avoid the use of such ad-hoc syntactic transformations, and produce a proof structured in two steps: first, one can prove, within the logic, that it is sound to align the loops as described; and then proceed with the proof of the aligned loops.

The key idea is that the desired alignment of loops can be expressed
as a (derived) rule, encoding the net effect of the syntactic loop splitting,
without having to manipulate the syntax:

P_1(N_1) P_2(0)

∀i < N_1 P_1(i) [1: t_1, 2: t]P_1(i+1)

∀j < N_2 P_2(j) [1: t_2, 2: t]P_2(j+1)

P_1(0) [
1: (N_1t_1;N_2t_2),
2: (N_1+N_2)t

The rule considers two programs: a sequence of two loops, and a single loop
with the same cumulative number of iterations.
It asks the user to produce two relational loop invariants $P_1$ and $P_2$
which are used to relate $N_1$ iterations of $t_1$ and $t$ together,
and $N_2$ iterations of $t_2$ and $t$ together.

such rule is derivable
from the primitive rules of looping of :
∀i < nP(i) [j: t] P(i+1)

P(0) [j: nt] P(n)

[i: nt]
[i: t]  Q

[i: (n+1)t] Q

<Ref> is a standard unary invariant-based rule;
<ref> simply reflects the
semantics of a loop in terms of its unfoldings.
Using these
we can prove <ref>
avoiding semantic reasoning all together,
and fully generically on the loop bodies,
allowing it to be reused in any situation fitting the pattern.

In our example, we can prove our goal by instanting it with the loop invariants:

\begin{align*}
P_1(i) &\is
\cpl{
\Ip{r}{1}\leq\Ip{r}{2}
\land
\Ip{l}{1}=0\leq\Ip{l}{2}
P_2(j) &\is
\cpl{
\Ip{r}{1}\leq\Ip{r}{2}
\land
\Ip{l}{1}\leq\Ip{l}{2}
\end{align*}

def BETW_MIX($x$,$S$):
repeat $N$:
p :  $\prob_S$
l := l || p <= $x$
q :  $\prob_S$
r := r || q >= $x$
d := r        l

def prog1:
x :  $d_0$
y :  $d_1$(x)
z :  $d_2$(x)

def prog2:
x :  $d_0$
z :  $d_2$(x)
y :  $d_1$(x)

A variant of the BETW program.

Conditional Swapping

This handling of structural differences as derived proof patterns
is more powerful than syntactic transformations:
it can, for example, handle transformations that are sound only under some
assumptions about state.
To show an instance of this,
we consider a variant of the previous example:
BETW_MIX (in <ref>)
is another variant of BETW_SEQ
which still makes $2N$ samples but interleaves sampling
for the minimum and for the maximum.
We want to prove that this is equivalent to BETW_SEQ.
Letting $\m{\permap}$ contain full permissions for the relevant variables,
the goal is $
\proves
\WP {\m[
\I1: \code{BETW_SEQ($x, S$)},
\I2: \code{BETW_MIX($x, S$)}
]} {
\cpl{\Ip{d}{1} = \Ip{d}{2}}
with $P_0 = \sure{\Ip{l}{1}=\Ip{r}{1}=0}*\sure{\Ip{l}{2}=\Ip{r}{2}=0}$.

Call $\tBet{1}$ and $\tBet{2}$ the first and second half of the body of the loop
of BETW_MIX, respectively.
The strategy
is to consider together one execution of $\tA$
(the body of the loop of AboveMin),
and $\tBet{1}$;
and one of $\tB$ (of BelowMax),
and $\tBet{2}$.
The strategy relies on the observation that every iteration of the three loops
is independent from the others.
To formalize the proof idea we thus first prove a derived proof pattern
encoding the desired alignment, which we can state for generic $t_1,t_2,t_1',t_2'$:

∀i < N P_1(i) [1: t_1, 2: t_1']P_1(i+1)

∀i < N P_2(i) [1: t_2, 2: t_2']P_2(i+1)

P_1(0) * P_2(0)
1: (Nt_1;Nt_2),
2: N(t_1';t_2')
]P_1(N) * P_2(N)

The rule matches on two programs: a sequence of two loops,
and a single loop with a body split into two parts.
The premises require a proof that $t_1$ together with $t_1'$ (the first half of the body of the second loop) preserve the invariant $P_1$;
and that the same is true for $t_2$ and $t_2'$ with respect to an invariant $P_2$.
The precondition $P_1(0)*P_2(0)$ in the conclusion ensures that the two
loop invariants are independent.

As for the previous example, this proof pattern can be entirely derived
from 's primitive rules.
We can then apply <ref> to our example
using as invariants:

\begin{align*}
P_1 &\is \cpl{\Ip{l}{1} = \Ip{l}{2}}\withp{\m{p}_{\p{l}}}
P_2 &\is \cpl{\Ip{r}{1} = \Ip{r}{2}}\withp{\m{p}_{\p{r}}}
\end{align*}

contains full permissions for
l and p on both indices, and
contains full permissions for
r and q on both indices.
Then, to close the proof we can invoke <ref> to
merge the two independent relational liftings.

§.§ pRHL-style Reasoning

In pRHL, the semantics of triples implicitly always conditions
on the input store,
so that programs are always seen as running from a pair of
deterministic input store satisfying the relational precondition.
Triples in the pRHL style can be encoded in  as:

\begin{equation}
\cpl{R_0}
\proves
\E \prob.
\CC\prob \m{s}.(
\var{St}(\m{s}) \land
\WP {\m{t}} {\cpl{R_1}}
\quad
\text{where}
\quad
\var{St}(\m{s}) \is
\sure{\ip{x}{i}=\m{s}(\ip{x}{i})}_{\ip{x}{i}\in I\times\Var}.
\label{triple:prhl}
\end{equation}

As the input state is always conditioned,
and the precondition is always a relational lifting,
one is always in the position of applying <ref>
to eliminate the implicit conditioning of the lifting and the one wrapping the
WP, reducing the problem to a goal where the state is deterministic
(and thus where the primitive rules of WP laws apply without need for
further conditioning).
As noted in <ref>,
using LHC-style WPs allows us to lift our unary WP rules
to binary with little effort.

An interesting property of the encoding in (<ref>) is that
anything of the form $ \CC\prob \m{s}.(\var{St}(\m{s}) \land \dots) $
has ownership of the full store (as it conditions on every variable).
We observe that WPs (of any arity) which have this property
enjoy an extremely powerful rule.
Let $ \ownall \is \A \ip{x}{i} \in I\times\Var.\own{\ip{x}{i}} $.
The following is a valid (primitive) rule in :

allows the shift of the conditioning on the input to the conditioning of the output.
This rule can be seen as a powerful way to make progress in lifting
a conditional statement to an unconditional one.
To showcase <ref>,
consider the two programs in <ref>, which
are equivalent:
if we couple the x in both programs,
the other two samplings can be coupled under conditioning on x.
Formally, let $ P \gproves Q \is P \land \ownall \proves Q \land \ownall $.
We process the two assignments to $\p{x}$, which we can couple
\distAs{\Ip{x}{1}}{d_0} *
\distAs{\Ip{x}{2}}{d_0}
\proves
\CC{d_0} v.(\sure{\Ip{x}{1}=v} \land \sure{\Ip{x}{2}=v})
Then, let $t_1$ ($t_2$) be the rest of prog1 (prog2).
We can then derive:

∀vx1=v x2=v
[1: t_1, 2: t_2]*
x1 = x2 *
y1d_1(v) *
y2d_1(v) *

z1d_2(v) *

∀vx1=v x2=v
[1: t_1, 2: t_2]
x1 = x2 *
y1 = y2 *
z1 = z2

∀vx1=v x2=v
[1: t_1, 2: t_2]
x1 = x2 y1 = y2 z1 = z2

d_0 v.(x1=v x2=v)
d_0 v.
[1: t_1, 2: t_2]
x1 = x2 y1 = y2 z1 = z2

d_0 v.(x1=v x2=v)
[1: t_1, 2: t_2]
d_0 v.
x1 = x2 y1 = y2 z1 = z2

d_0 v.(x1=v x2=v)
[1: t_1, 2: t_2]
x1 = x2 y1 = y2 z1 = z2

Where the top triple can be easily derived using standard steps.
Reading it from bottom to top, we start by invoking convexity of
relational lifting to introduce a conditioning modality in the postcondition
matching the one in the precondition.
<Ref> allows us to bring the whole WP under the modality,
allowing <ref> to remove it on both sides.
From then it is a matter of establishing and combining
the couplings on y and z.
Note that these couplings are only possible because the coupling
on x made the parameters of $d_1$ and of $d_2$ coincide on both indices.
In sec:appendix:examples we show this kind of derivation can be useful
for unary reasoning too.

While the $\ownall$ condition is restricting, without it the rule is unsound.
We leave it as future work to study whether there is a model
that validates this rule without requiring $\ownall$.

§.§ One Time Pad Revisited

In <ref>, we prove the encrypt program correct relationally
(missing details are in sec:appendix:examples:onetimerel).
An alternative way of stating and proving the correctness of encrypt
is to establish that in the output distribution c and m are independent,
which can be expressed as the unary goal (also studied in [Barthe et al, 2019]):
\proves
\WP {\m[\I1: \code{encrypt()}]} {
\distAs{\Ip{c}{1}}{\Ber{1/2}} *
\distAs{\Ip{m}{1}}{\Ber{p}}
(where $\m{\permap} = \m[\Ip{k}{1}:1,\Ip{m}{1}:1,\Ip{c}{1}:1]$).
The triple states that after running encrypt,
the ciphertext c is distributed as a fair coin,
and—importantly—is not correlated with the plaintext in m.
The PSL proof in [Barthe et al, 2019] performs some of the steps
within the logic, but needs to carry out some crucial entailments at the meta-level. The same applies to the Lilac proof in [Li et al, 2023] which requires  ad-hoc lemmas proven on the semantic model.
The stumbling block is proving the valid entailment:

\[
\distAs{\Ip{k}{1}}{\Ber{\onehalf}} *
\distAs{\Ip{m}{1}}{\Ber{p}} *
\sure{\Ip{c}{1} = \Ip{k}{1} \xor \Ip{m}{1}}
\proves
\distAs{\Ip{m}{1}}{\Ber{p}} *
\distAs{\Ip{c}{1}}{\Ber{\onehalf}}
\]

In  we can prove the entailment in two steps:
(1) we condition on m and k to compute the result of
the xor operation and obtain that c is distributed as $\Ber{\onehalf}$;
(2) we carefully eliminate the conditioning while preserving the independence
of m and c.

The first step starts by conditioning on m and k and proceeds as follows:

p m.
m1=m *
(k1=k *
c1 = k m)
p m.
m1=m *

k. c1=k m=0

k. c1=k m=1

p m.
m1=m *
k. c1=k
The crucial entailment is the application of <ref> to the $m=1$ branch,
by using negation as the bijection
(which satisfies the premises of the rules since $\Ber{\onehalf}$ is unbiased).

The second step uses the following primitive rule of :

(_1i, _2i)_1 ⊗_2
_1i_1 *

with which we can prove:

p m.
m1=m *
k. c1=k
p m.
m1=m c1=k
p  (m,k).
(m1,c1)(p )
m1p *

§ RELATED WORK

Research on deductive verification of probabilistic programs has developed a
wide range of techniques that employ unary and  relational styles of reasoning.  advances the state of the art in both styles, by coherently unifying the strengths of both. We limit our comparison here to deductive techniques only, and focus most of our attention on explaining how  offers new  reasoning tools compared to these.

Unary-style Reasoning.
Early work in this line focuses more on analyzing marginal distributions and probabilities, and features like harnessing the power of  probabilistic independence and conditioning have been more recently added to make more expressive program logics [Ramshaw, 1979, Rand and Zdancewic, 2015, Barthe et al, 2016, Barthe et al, 2019, Bao et al, 2022, Li et al, 2023].

Much work in this line has been inspired by Separation Logic (SL),
a powerful tool
for reasoning about pointer-manipulating programs,
known for its support of local reasoning
of separated program components [Reynolds, 2000].
PSL [Barthe et al, 2019] was the first logic to present a SL model for reasoning about the probabilistic independence of program variables, which facilitates modular reasoning about independent components within a probabilistic program.
In [Bao et al, 2021] and [Bao et al, 2022] SL variants are used for reasoning about conditional independence and negative dependence, respectively;
both are used in algorithm analysis as relaxations of probabilistic independence.
Lilac [Li et al, 2023] is the most recent addition to this group and introduces a new foundation of probabilistic separation logic based on measure theory.
It enables reasoning about independence and conditional independence uniformly in one logic and also has support for continuous distributions.
It is noteworthy, however, that Lilac works with immutable programs [Staton, 2020], which simplifies reasoning in certain contexts (e.g., the frame rule and the if rule).

also uses a measure-theory based model, similar to Lilac, with two important distinctions:
(1) it works with a language with mutability, going back to the tradition of previous separation logics, and
(2) it is restricted to discrete distributions to prove a wider range of proof rules.
An extension of  to the continuous case, and study of which rules would continue to be sound is an interesting direction for future research.
This measure theory based model, in contrast to the more primitive probability reasoning in earlier work [Barthe et al, 2019], is vital to maintaining expressivity for both  and Lilac.

Relational Reasoning
Barthe et al, 2009 extend relational Hoare logic [Benton, 2004] to reason about probabilistic programs in a logic called pRHL (probabilistic Relational Hoare Logic).
In pRHL, assertions on pairs of deterministic program states are lifted to assertions on pairs of distributions, and on the surface, the logic simply manipulates the deterministic assertions.
A number of variants of pRHL were successfully applied to proving various cryptographic protocols and differential privacy algorithms [Barthe et al, 2009, Barthe et al, 2015, Hsu, 2017, Wang et al, 2019, Zhang and Kifer, 2017].
When a natural relational proof for an argument exists, these logics are simple and elegant to use. However, they fundamentally
trade expressiveness for ease of use.
A persisting problem with them has been that they rely on a strict structural alignment between the order of samples in the two programs. Recall our discussion in <ref> for an example of this that  can handle.
Gregersen et al, 2023 recently proposed
asynchronous probabilistic coupling
inspired by prophecy variables [Jung et al, 2019]
to allow for “out of order” couplings between samplings,
for proving contextual refinement in a functional higher-order language.
In <ref> we showed how  can resolve the issue
in the context of first-order imperative programs by using framing creatively.
Our n-ary WP is inspired by LHC [D'Osualdo et al, 2022],
which shows how arity-changing rules (like <ref>)
can accommodate modular and flexible relational proofs of deterministic programs.

Polaris [Tassarotti and Harper, 2019], a logic for verifying concurrent probabilistic programs, is an isolated instance of a relational separation logic.
However, separation in Polaris is based on the classic disjointness of heaps and is not related to (conditional) independence.

Other Techniques.
Expectation-based approaches, which reason about expected quantities of probabilistic programs via a weakest-pre-expectation operator that propagates information about expected values backwards through the program, have been classically used to verify randomized algorithms [Kozen, 1983, Morgan et al, 1996, Kaminski et al, 2016, Kaminski, 2019, Aguirre et al, 2021, Moosbrugger et al, 2022]. Since these focus on a single expectation-based property at a time and as such are non-modular, we do not consider them in the same category as program logics like Lilac or pRHL.
Ellora [Barthe et al, 2018] proposes an assertion-based logic (without separation nor conditioning) to overcome the limitation of working only with expectations.

§ CONCLUSIONS AND FUTURE WORK

's journey started as a quest to integrate unary and relational
probabilistic reasoning and ended up uncovering
as a key fundational tool.
Remarkably, to achieve our goal we had to deviate from Lilac's previous
proposal in both the definition of conditioning,
to enable the encoding of relational lifting,
and of ownership (with almost measurability),
to resolve an issue with almost sure assertions
(recently corrected [Li et al, 2023] in a different way).
In addition, our model supports mutable state without sacrificing
One limitation of our current model is lack of support for continuous
Lilac's model could suggest a pathway for a continuous extension of ,
but it is unclear if all our rules would be still valid;
for example <ref>'s soundness hinges on properties of discrete distributions that we could not extend to the general case in an obvious way.
's encoding of relational lifting and the novel proof principles it uncovered for it are a demonstration of the potential
of  as a basis for deriving high-level logics on top of an ergonomic
core logic.
An obvious candidate for such scheme is variations of relational liftings
for approximate couplings (which has been used for differential privacy),
or expectation based calculi (à la Ellora).

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

[Aguirre et al, 2019]
authorpersonAlejandro Aguirre, personGilles
Barthe, personMarco Gaboardi, personDeepak Garg,
and personPierre-Yves Strub.
A relational logic for higher-order programs.
journalJ. Funct. Program.  volume29
(year2019), pagese16.

[Aguirre et al, 2021]
authorpersonAlejandro Aguirre, personGilles
Barthe, personJustin Hsu, personBenjamin Lucien
Kaminski, personJoost-Pieter Katoen, and
personChristoph Matheja. year2021.
A pre-expectation calculus for probabilistic
journalProceedings of the ACM on Programming
Languages volume5, numberPOPL
(year2021), pages1–28.

[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, 2016]
authorpersonGilles Barthe, personThomas
Espitau, personMarco Gaboardi, personBenjamin
Grégoire, personJustin Hsu, and
personPierre-Yves Strub. year2016.
A program logic for probabilistic programs.
journalAvailable at justinh. su/files/papers/ellora.
pdf (year2016).

[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 booktitleProgramming Languages and Systems,
editorpersonAmal Ahmed (Ed.).
publisherSpringer International Publishing,
addressCham, pages117–144.

[Barthe et al, 2015]
authorpersonGilles Barthe, personThomas
Espitau, personBenjamin Grégoire, personJustin
Hsu, personLéo Stefanesco, and
personPierre-Yves Strub. year2015.
Relational reasoning via probabilistic coupling.
In booktitleLogic for Programming, Artificial Intelligence,
and Reasoning: 20th International Conference, LPAR-20 2015, Suva, Fiji,
November 24-28, 2015, Proceedings 20. Springer, pages387–401.

[Barthe et al, 2009]
authorpersonGilles Barthe, personBenjamin
Grégoire, and personSantiago Zanella Béguelin.
Formal certification of code-based cryptographic
proofs. In booktitleProceedings of the 36th annual ACM
SIGPLAN-SIGACT symposium on Principles of programming languages.

[Barthe et al, 2019]
authorpersonGilles Barthe, personJustin
Hsu, and personKevin Liao. year2019.
A probabilistic separation logic.
journalarXiv preprint arXiv:1907.10708

[Benton, 2004]
authorpersonNick Benton.
Simple relational correctness proofs for static
analyses and program transformations.
journalACM SIGPLAN Notices volume39,
number1 (year2004), pages14–25.

[Bornat et al, 2005]
authorpersonRichard Bornat, personCristiano
Calcagno, and personHongseok Yang.
Variables as Resource in Separation Logic. In
booktitleMFPS (seriesElectronic Notes
in Theoretical Computer Science, Vol. volume155).
publisherElsevier, pages247–276.

[D'Osualdo et al, 2022]
authorpersonEmanuele D'Osualdo,
personAzadeh Farzan, and personDerek Dreyer.
Proving hypersafety compositionally.
journalProceedings of the ACM on Programming
Languages volume6, numberOOPSLA2
(year2022), pages289–314.

[Giry, 1982]
authorpersonMichele Giry.
A categorical approach to probability theory. In
booktitleCategorical Aspects of Topology and Analysis:
Proceedings of an International Conference Held at Carleton University,
Ottawa, August 11–15, 1981. Springer, pages68–85.

[Gregersen et al, 2023]
authorpersonSimon Oddershede Gregersen,
personAlejandro Aguirre, personPhilipp Haselwarter,
personJoseph Tassarotti, and personLars Birkedal.
Asynchronous Probabilistic Couplings in
Higher-Order Separation Logic.
journalarXiv preprint arXiv:2301.10061

[Hsu, 2017]
authorpersonJustin Hsu.
booktitleProbabilistic couplings for probabilistic
publisherUniversity of Pennsylvania.

[Jung et al, 2019]
authorpersonRalf Jung, personRodolphe
Lepigre, personGaurav Parthasarathy, personMarianna
Rapoport, personAmin Timany, personDerek Dreyer,
and personBart Jacobs. year2019.
The future is ours: prophecy variables in
separation logic.
journalProceedings of the ACM on Programming
Languages volume4, numberPOPL
(year2019), pages1–32.

[Kaminski, 2019]
authorpersonBenjamin Lucien Kaminski.
titleAdvanced weakest precondition calculi for
probabilistic programs.
thesistypePh. D. Dissertation. schoolRWTH
Aachen University.

[Kaminski et al, 2016]
authorpersonBenjamin Lucien Kaminski,
personJoost-Pieter Katoen, personChristoph Matheja,
and personFederico Olmedo. year2016.
Weakest precondition reasoning for expected
run–times of probabilistic programs. In
booktitleProgramming Languages and Systems: 25th European
Symposium on Programming, ESOP 2016, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The
Netherlands, April 2–8, 2016, Proceedings 25. Springer,

[Kozen, 1983]
authorpersonDexter Kozen.
A Probabilistic PDL. In
booktitleProceedings of the fifteenth annual ACM symposium
on Theory of computing. pages291–297.

[Krebbers et al, 2018]
authorpersonRobbert Krebbers,
personJacques-Henri Jourdan, personRalf Jung,
personJoseph Tassarotti, personJan-Oliver Kaiser,
personAmin Timany, personArthur Charguéraud,
and personDerek Dreyer. year2018.
MoSeL: a general, extensible modal framework for
interactive proofs in separation logic.
journalProc. ACM Program. Lang.
volume2, numberICFP (year2018),

[Li et al, 2023]
authorpersonJohn M. Li, personAmal Ahmed,
and personSteven Holtzen. year2023a.
Lilac: a Modal Separation Logic for Conditional
journalCoRR  volumeabs/2304.01339

[Li et al, 2023]
authorpersonJohn M. Li, personAmal Ahmed,
and personSteven Holtzen. year2023b.
titleLilac: A Modal Separation Logic for Conditional
[arxiv]2304.01339v2 [cs.PL]

[Moosbrugger et al, 2022]
authorpersonMarcel Moosbrugger,
personMiroslav Stankovič, personEzio Bartocci,
and personLaura Kovács. year2022.
This is the moment for probabilistic loops.
journalProceedings of the ACM on Programming
Languages volume6, numberOOPSLA2
(year2022), pages1497–1525.

[Morgan et al, 1996]
authorpersonCarroll Morgan, personAnnabelle
McIver, and personKaren Seidel.
Probabilistic Predicate Transformers.
journalTOPLAS (year1996).

[Ramshaw, 1979]
authorpersonLyle Harold Ramshaw.
booktitleFormalizing the analysis of algorithms.
Vol. volume75.
publisherXerox Palo Alto Research Center.

[Rand and Zdancewic, 2015]
authorpersonRobert Rand and personSteve
Zdancewic. year2015.
VPHL: A verified partial-correctness logic for
probabilistic programs.
journalElectronic Notes in Theoretical Computer
Science  volume319 (year2015),

[Reynolds, 2000]
authorpersonJohn C Reynolds.
Intuitionistic reasoning about shared mutable data
journalMillennial perspectives in computer science
volume2, number1 (year2000),

[Rosenthal, 2006]
authorpersonJeffrey S Rosenthal.
booktitleA First Look At Rigorous Probability
publisherWorld Scientific Publishing Company.

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

[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.

[Wang et al, 2019]
authorpersonYuxin Wang, personZeyu Ding,
personGuanhong Wang, personDaniel Kifer, and
personDanfeng Zhang. year2019.
Proving differential privacy with shadow
execution. In booktitleProceedings of the 40th ACM SIGPLAN
Conference on Programming Language Design and Implementation.

[Zhang and Kifer, 2017]
authorpersonDanfeng Zhang and personDaniel
Kifer. year2017.
LightDP: Towards automating differential privacy
proofs. In booktitleProceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages.

§ THE RULES OF

In this section we list all the rules of ,
including some omitted (but useful) rules in addition to those
that appear in the main text.
Since our treatment is purely semantic,
rules are simply lemmas that hold in the model.
Although we do not aim for a full axiomatization,
we try to identify the key proof principles that apply to each of our connectives.
For brevity, we omit the rules that apply to the basic connectives of separation logic, as they are well-known and have been proven correct for any model that is an RA. For those we refer to [Krebbers et al, 2018].

We make a distinction between
“primitive” and “derived” rules.
The primitive rules require proofs that manipulate the semantic model definitions directly; these are the ones we would consider part of a proper axiomatization.
The derived rules can be proved sound by staying at the level of the logic,
by using the primitive rules of .

<Ref> lists the primitive rules for distribution ownership assertions and for the  modality.
<Ref> lists the primitive rules for the weakest precondition modality.
In <ref> we list some useful derived rules.

We provide proofs for each rule in the form of lemmas in <ref>.
The name labelling each rule is a link to the proof of soundness of the rule.

*Distribution ownership rules

(P) (Q) = ∅
P Q P Q

_1i *
(_1 _2)i

(P, (Ei))

Ei P
Ei ∗P

(_1i, _2i)_1 ⊗_2
_1i_1 *

.     rule:c-true

∀vK_1(v) K_2(v)

P * v.K(v)
v.(P * K(v))

v_0 v.K(v)

_0 = (,v.(((v), w.(v,w))))

v.(v) w.K(v,w)
_0 (v,w).K(v,w)

(,) w.K(w)
v. (v) w.K(w)

(K_1) (K_2) = ∅
v. K_1(v)
v. K_2(v)
(K_1(v) K_2(v))

v. x X. Q(v, x)
f A →X. v. Q(v, f(v))

f (') →()

∀b ∈(') '(b) = (f(b))

' b.K(f(b))

v.(K(v) * i)
i * v.K(v)

v. x X. Q(v, x)
x X. v. Q(v, x)

()=1 * v.K(v)
v.(v ∈ * K(v))

(v, w).(v)i
∘_1 v.(v)i

The primitive rules of .

*Structural WP rules

Q Q'

P Q
P Q

(t_1 . t_2)Q

(Q_1) t_2 t_1

(Q_2) t_1 t_2

(t_1 + t_2)Q_1 Q_2

Program WP rules

P [i: skip] P

[i: t][]
*[i: t'] Q

[i: (t; t')] Q

x ∉()

∀y ∈() (yi) > 0

[i: x:=][]
xi = i

xi : 1
[i: x: $\dist$($\vec{v}$)]

[i: t_1]Q(1)
[i: t_2]Q(0)

[i: if $\;v\;$ then $\;t_1\;$ else $\;t_2$]

i=v *
*[i: [v]]Q
*[i: []]Q

[i: nt]
[i: t]  Q

[i: (n+1)t] Q

∀i < nP(i) [j: t] P(i+1)

P(0) [j: nt] P(n)

The primitive WP rules of .

*Ownership and distributions

i = v
i = v'

(_2 = f(_1))i

iv *

i * i ∈()

_1i_1 *
(_1i, _2i)_1 ⊗_2

_1 v_1.
_2 v_2.
K(v_1, v_2)
_2 v_2.
_1 v_1.
K(v_1, v_2)

(v, w).
∘_1 v.

Relational Lifting

R_1 R_2

R_1 R_2

R ^x_1i,…,x_ni

R R(x_1i,…,x_ni)

*[lab=cpl-eq-dist]i j

.R R

R_1 * R_2
R_1 R_2

R ^X

(i) X

R * xi = i
R xi = i

∘_1 = _1

∘_2 = _2

(R) = 1

x_11_1 *
R(x_11, x_22)

Weakest Precondition

P [i: 0t] P

∀k < nP(k) [i: t, j: t']P(k+1)

P(0) [i: (nt), j: (nt')] P(n)

R ^X

xi ∉(i) X

∀y ∈() (yi) > 0

[i: x:=][]
R xi = i

Derived rules.

§ AUXILIARY DEFINITIONS

Let $A$ be a countable set and $\salg$ a .
We define the following functions:

\begin{align*}
\return &\from A \to \Dist(\Full{A})
\bind &\from
\Dist(\Full{A}) \to
(A \to \Dist(\salg))
\to \Dist(\salg)
\\
\return&(a) \is \dirac{a}
\bind&(\prob, \krnl) \is
\fun \event \in \salg.
\sum_{a\in A} \prob(a) \cdot \krnl(a)(\event)
\end{align*}

We will use throughout Haskell-style notation for monadic expressions,
for instance:

\[
\bigl(\DO{x <- \prob; y <- f(x); \return(x+y)}\bigr)
\equiv
\bind(\prob,
\fun x.
\bind(f(x),
\fun y.
\return(x+y)
\]

The $\bind$ and $\return$ operators form a well-known monad with
$\Dist$, and thus satisfy the monadic laws:

\begin{align*}
\bind(\prob,\fun x.\return(x)) &= \prob
\tag{\textsc{unit-r}}
\label{prop:bind-unit-r}
\\
\bind(\return(v),\krnl) &= \krnl(v)
\tag{\textsc{unit-l}}
\label{prop:bind-unit-l}
\\
\bind(\bind(\prob,\krnl_1),\krnl_2) &=
\bind(\prob,\fun x.\bind(\krnl_1(x),\krnl_2))
\tag{\textsc{assoc}}
\label{prop:bind-assoc}
\end{align*}

It is known that for any sigma algebra $\sigmaF'$ on countable underlying set, there exists
a partition $S$ of the underlying space that generated it, so we can transform
any such $\sigmaF'$ to a full sigma algebra over $S$.
Since we are working with countable underlying set throughout,
the requirement of $\prob$ to be over the full sigma algebra $\Full{A}$ is not an extra restriction.

We assume each primitive operator $\prim \in \set{\p+,\p-,\p<,\dots}$
has an associated arity $\arity(\prim) \in \Nat$, and
is given semantics as some function
$ \sem{\prim} \from \Val^{\arity(\prim)} \to \Val. $
Expressions $\expr \in \Expr$ are given semantics as a function
$ \sem{\expr} \from \Store \to \Val $
as standard:

\begin{align*}
\sem{v}(s) &\is v
\sem{\p{x}}(s) &\is s(\p{x})
\sem{\prim(\expr_1,\dots,\expr_{\arity(\prim)})}(s) &\is
\sem{\prim}(\sem{\expr_1},\dots,\sem{\expr_{\arity(\prim)}})
\end{align*}

§.§ Program semantics

Given $\term \in \Term$ we define its kernel semantics
$\Sem[K]{\term} \from \Store \to \Dist(\Full{\Store}) $
as follows:

\begin{align*}
\Sem[K]{\code{skip}}(s) &\is
\return(s)
\\
\Sem[K]{\code{x:=}\expr}(s) &\is
\return(s\upd{\p{x}->\sem{\expr}(s)})
\\
\Sem[K]{\code{x:~$\dist$($\expr_1,\dots,\expr_n$)}}(s) &\is
\DO{
v <- \sem{\dist}(\sem{\expr_1}(s),\dots,\sem{\expr_n}(s));
\return(s\upd{\p{x}->v})
\\
\Sem[K]{\term_1\p;\term_2}(s) &\is
\DO{
s' <- \Sem[K]{\term_1}(s);
\Sem[K]{\term_2}(s')
\\
\Sem[K]{\code{if$\;\expr\;$then$\;\term_1\;$else$\;\term_2\;$}}(s) &\is
\DO{
\ITE{\sem{\expr}(s) \ne 0}
\\
\Sem[K]{\Loop{\expr}{\term}}(s) &\is
\var{loop}_{\term}(\sem{\expr}(s), s)
\end{align*}

where $\var{loop}_{\term}$ simply iterates $\term$:

\[
\var{loop}_{\term}(n, s) \is
\begin{cases}
\return(s) \CASE n \leq 0 \\
\DO{s' <- \var{loop}_{\term}(n-1, s); \Sem[K]{\term}(s')} \OTHERWISE
\end{cases}
\]

The semantics of a term is then defined as:

\begin{align*}
\sem{\term} &\from \Dist(\Full{\Store}) \to \Dist(\Full{\Store})
\\
\sem{\term}(\prob) &\is \DO{s <- \prob; \Sem[K]{\term}(s)}
\end{align*}

Evaluation contexts $\Ectxt$ are defined by the following grammar:

| x_1,,_2
| _1_2

| (_1,,_2)

A simple property holds for evaluation contexts.

$\Sem[K]{\Ectxt[\expr]}(s) = \Sem[K]{\Ectxt[\sem{\expr}(s)]}(s).$

Easy by induction on the structure of evaluation contexts.

§.§ Permissions

needs a side-condition on assertions which concerns how
an assertion constrains permission ownership.
In , most manipulations do not concern permissions,
except for when a mutation takes place, where permissions are used
to make sure the frame forgets all information about the variable to be mutated.
The notion of permission-scaling-invariant assertion we now define
characterises the assertions which are not chiefly concerned about permissions.

An assertion $P \in \HAssrt_I$ is permission-scaling-invariant
with respect to some $X \subs I \times \Var$,
written $\psinv(P, X)$, if it is invariant under scaling of permission of $X$;
that is:

\[
\psinv(P, X) \is
\forall \m{\salg},\m{\prob},\m{\permap}, q, n\in \Nat\setminus\set{0}.
P(\m{\salg},\m{\prob},\m{\permap}\m[\ip{x}{i}: q])
\implies
P(\m{\salg},\m{\prob},\m{\permap}\m[\ip{x}{i}: q/n]).
\]

For example,
fixing $X=\set{\ip{x}{i}}$ then
$ \distAs{\ip{x}{i}}{\prob} $,
$ \sure{\ip{x}{i}=v} $, and
$ \perm{\ip{y}{i}: 1} $
are permission-scaling-invariant,
but $ \perm{\ip{x}{i}: \onehalf} $ is not.

§ MEASURE THEORY LEMMAS

In the following, for any natural number $n> 1$, we will use $\numlist{n}$
to denote the list of numbers $\{1, \dots, n\}$.

First, we present the key lemma that uses the fact that
underlying set is countable.

Let $\Outcomes$ be as countable set, and $\salg$ to be an arbitrary sigma algebra
on $\Outcomes$. Then there exists a countable partition $S$ of $\Outcomes$
such that $\salg = \closure{S}$.

For every element $x \in \Outcomes$,
we identify the smallest event $E_x \in \salg$ such that $x \in E_x$,
and show that for $x, z \in \Outcomes$,
either $E_x = E_z$ or $E_x \cap E_z = 0$.
Then the set $S = \set{E_x \mid x \in \Outcomes}$ is a partition of $\Outcomes$,
and any event $E \in \salg$ can be represented as
$\Union_{x \in E} E_x$, which suffices to show that $\salg$ is
generated by $S$.

For every $x, y$, let

\begin{align*}
A_{x, y} &=
\begin{cases}
\Outcomes \CASE \text{$\forall E \in \salg$, either $x , y$ both in~$E$ or $x , y$ both not in~$E$} \\
E \OTHERWISE, \text{pick any $E \in \salg$ such that $x \in E$ and $y \notin E$}
\end{cases}
\end{align*}

Then we show that, for all $x$,
$E_x = \cap_{y \in \Outcomes} A_{x, y}$ is the smallest
event in $\salg$ such that $x \in E_x$ in the following.
If there exists $E_x'$ such that $x \in E_x'$ and $E_x' \subset E_x$,
then $E_x \setminus E_x'$ is not empty. Let $y$ be an element of
$E_x \setminus E_x'$, and by the definition of $A_{x, y}$, we have
$y \notin A_{x,y}$. Thus, $y \notin \cap_{y \in \Outcomes} A_{x, y} = E_x$,
which contradicts with $y \in E_x \setminus E_x'$.

Next, for any  $x, z \in \Outcomes$,
since $E_x$ is the smallest event containing $x$ and
$E_z$ is the smallest event containing $z$,
the smaller event $E_z \setminus E_x$ is either equivalent to
$E_z$ or not containing $z$.

* If $E_z \setminus E_x = E_z$, then $E_x$ and $E_z$ are

* If $z \not\in E_z \setminus E_x$, then it must $z \in E_x$,
which implies that there exists no $E \in \salg$ such that
$x \in E$ and $z \notin E$. Because $\salg$ is closed under
complement, then there exists no $E \in \salg$ such that
$x \notin E$ and $z \in E$ as well. Therefore,
we have $x \in  \cap_{y \in \Outcomes} A_{z, y} = E_z$ as well.
Furthermore, because $E_z$ is the smallest event in
$\salg$ that contains $z$ and $E_x$ also contains $z$,
we have $E_z \subseteq E_x$; symmetrically, we have
$E_x \subseteq E_z$.
Thus, $E_x = E_z$.

Hence,  the set $S = \set{E_x \mid x \in \Outcomes}$ is a partition of $\Outcomes$.

If $S = \{A_1, A_2, \dots, A_n\}$ is a partition on $\Outcomes$,
and $\salg$ is a sigma algebra generated by $S$,
then every element of $\salg$ can be written as
$\Union_{i \in I} A_i$ for some $I$ subset of $\numlist{n}$.

In other words,

\[
\closure{S} = \set*{ \Union_{i \in I} A_i | I \subseteq \numlist{n} }
\]

Because sigma algebra is closed under countable union,
for any $I \subseteq \numlist{n}$,
$ \Union_{i \in I} A_i \in \closure{S} $.
Thus, $\closure{S} \supseteq \{ \Union_{i \in I} A_i \mid I \subseteq \numlist{n} \}$.

Also, $\{ \Union_{i \in I} A_i \mid I \subseteq \numlist{n}\}$ is
a sigma algebra:

* $\emptyset = \Union_{i \in \emptyset} A_i$.

* $\Outcomes = \Union_{i \in \numlist{n}} A_i$.

* If $E_1 = \Union_{i \in I} A_i$ and
$E_2 = \Union_{i \in I'} A_i $ and
then $E_1 \cap E_2 = \Union_{i \in I \cap I'} A_i$.
So it is closed under intersections.

* If $E = \Union_{i \in I} A_i$, then
the complement of $E$ is $\Union_{i \in (\numlist{n} \setminus I)} A_i$.

Then, $\{ \Union_{i \in I} A_i \mid I \subseteq \numlist{n}\}$ is
a sigma algebra that contains $S$, which implies that
$\{ \Union_{i \in I} A_i \mid I \subseteq \numlist{n}\} = \closure{S}$.

Therefore, $\closure{S} = \{\Union_{i \in I} A_i \mid I \subseteq \numlist{n} \}$.

Let $\Outcomes$ be as countable set.
If $S_1$ and $S_2$ are both partitions of $\Outcomes$,
then $\closure{S_1} \subseteq \closure{S_2}$ implies that
for any $q_j \in S_2$,
we can find $p_i \in S_1$ such that $q_j \subseteq p_i$.

We pick an arbitrary element $s \in q_j$ and
denote the element of $S_1$ that contains $s$ as $p'$.
Because $p' \in S_1$ and $S_1 \subset  \closure{S_1} \subseteq \closure{S_2}$,  we have $p' \in  \closure{S_2}$.
Note that $s \in q_j$ and $q_j$ is an element of the partition $S_2$
that generates $\closure{S_2}$, $q_j$ must be the smallest event
in $\closure{S_2}$ that contains $s$.
Because $s \in p'$ as well, $q_j$ being the smallest event containing $s$
implies that $q_j \subseteq p'$.

Suppose that we are given a sigma algebra $\sigmaF_1$ over a countable underlying set $\Outcomes$
and a measure $\mu_1$ over $\sigmaF_1$,
and some $A, \mu \in \Full{A}, \krnl_1 \colon A \to \giry(\sigmaF_1)$ such that $\mu_1 = \bind(\mu, \krnl_1)$.
Then, for any probability space $(\sigmaF_2, \mu_2)$ such that
$(\sigmaF_1, \mu_1) \extTo (\sigmaF_2, \mu_2)$,
there exists $\krnl_2$ such that $\mu_2 = \bind(\mu, \krnl_2)$.
Furthermore, for any $a \in \psupp(\mu)$,
$(\sigmaF_1, \krnl_1(a)) \extTo (\sigmaF_2, \krnl_2(a))$.

By <ref>,
$\sigmaF_i$ is generated by a countable partition over $\Outcomes_i$.
Say $\sigmaF_i$ is generated by $S_i$, i.e. $\sigmaF_i = \closure{S_i}$.
Also, $(\sigmaF_1, \mu_1) \extTo (\sigmaF_2, \mu_2)$ implies that
$\sigmaF_1 \subseteq \sigmaF_2$.
So we have $\closure{S_1} \subseteq \closure{S_2}$,
which by <ref> implies that
for any $q \in S_2$,
we can find a $p \in S_1$ such that $q \subseteq p$.
Let $f$ to be the mapping such that this $p = f(q)$ .

Then, we define $\krnl_2$ as follows:
for any $a \in A$, $E \in \sigmaF_2$,
there exists $S \subseteq S_2$ such that
$E = \Dunion_{q \in S} q$,
then define

\begin{align*}
\krnl_2(a)(E) = \sum_{q \in S} \krnl_1(a)(f(q)) \cdot h(q),
\end{align*}

$h(q) = \mu_2(q) / \mu_2(f(q))$ if $ \mu_2(f(q)) \neq 0$
and $h(q) = 0$ otherwise.

Then for any $E \in \sigmaF_2$,

\begin{align}
&\bind(\mu, \krnl_2)(E) \notag\\
&=  \sum_{a\in A} \mu(a) \cdot \krnl_2(\event) \notag \\
&=  \sum_{a\in A} \mu(a) \cdot \sum_{q \in S} \krnl_1(a)(f(q)) \cdot h(q) \notag \\
&=  \sum_{q \in S}  \sum_{a\in A} \mu(a) \cdot \krnl_1(a)(f(q)) \cdot h(q)  \notag \\
&=  \sum_{q \in S}  \bind(\mu, \krnl_1)(f(q)) \cdot h(q) \notag  \\
&=  \sum_{q \in S}  \mu_1(f(q)) \cdot h(q) \notag \\
&=  \sum_{q \in S, \mu_2(f(q)) \neq 0}  \mu_1(f(q)) \cdot \frac{\mu_2(q)}{ \mu_2(f(q))} \notag \\
&=  \sum_{q \in S,  \mu_2(f(q)) \neq 0}  \mu_2(f(q)) \cdot \frac{\mu_2(q)}{\mu_2(f(q))} \tag{$\mu_1(E') = \mu_2(E')$ for any $E' \in \sigmaF_1$}\\
&=  \sum_{q \in S, \mu_2(f(q)) \neq 0}  \mu_2(q)  \notag \\
&=  \sum_{q \in S, \mu_2(f(q)) \neq 0}  \mu_2(q) +  \sum_{q \in S,  \mu_2(f(q)) = 0}  \mu_2(q)  \tag{Because $\mu_2(f(q)) = 0$ implies $\mu_2(q) = 0$} \\
&= \sum_{q \in S}  \mu_2(q) \notag \\
&= \mu_2(\Dunion_{q \in S} q ) \notag \\
&= \mu_2(E) \notag
\end{align}

Thus, $\bind(\mu, \krnl_2)= \mu_2$.

Also, for any $a \in A_{\mu}$, for any $E \in \sigmaF_1$,
there exists $S' \subseteq S_1$
such that $E=\Dunion_{p \in S'} p$.

\begin{align*}
\krnl_2(a)(E)
&= \krnl_2(a)(\Dunion_{p \in S'} p) \\
&= \sum_{p \in S'} \krnl_2(a)(p) \\
&= \sum_{p \in S'} \sum_{q \subseteq p, q \in \sigmaF_2} \krnl_2(a)(q)\\
&= \sum_{p \in S'} \sum_{q \subseteq p, q \in \sigmaF_2, \mu_2(f(q)) \neq 0} \krnl_1(a)(f(q)) \cdot \frac{\mu_2(q)}{\mu_2(f(q))} \\
&= \sum_{p \in S', \mu_2(p) \neq 0} \krnl_1(a)(p) \cdot \frac{\left(\sum_{q \subseteq p, q \in \sigmaF_2}  \mu_2(q) \right) }{\mu_2(p)} \\
&= \sum_{p \in S', \mu_2(p) \neq 0} \krnl_1(a)(p) \cdot \frac{ \mu_2(p)}{ \mu_2(p)} \\
&= \sum_{p \in S', \mu_2(p) \neq 0} \krnl_1(a)(p)  \\
&= \sum_{p \in S'} \krnl_1(a)(p)  \\
&= \krnl_1(a)(\Dunion_{p \in S'} p)  \\
&= \krnl_1(a)(E)
\end{align*}

Thus, for any $a$, $(\sigma_1, \krnl_1(a)) \extTo (\sigma_2, \krnl_2(a))$.

Given two sigma algebras $\sigmaF_1$ and $\sigmaF_2$
over two countable underlying sets $\Outcomes_1, \Outcomes_2$,
then a general element in the product sigma algebra
$\sigmaF_1 \otimes \sigmaF_2$ can
be expressed as $\Union_{i, j \subseteq I} A_{i} \times B_{i}$
for some  $A_{i} \in \sigmaF_{1}, B_{j} \in \sigmaF_{2}, I \subseteq \mathbb{N}^2$.

By <ref>, the sigma algebra
$\sigmaF_i$ is generated by a countable partition over $\Outcomes_i$.
Let $C_1 = \{A_{i}\}_{i \in \mathbb{N}}$ be the countable partition that generates $\sigmaF_1$,
$C_2 = \{B_{i}\}_{i \in \mathbb{N}}$ be the countable partition that generates $\sigmaF_2$.
By <ref>,
a general element in $\sigmaF_1$ can be written as
$\Union_{j \in J} A_{j}$ for some $J \subseteq \mathbb{N}$,
and similarly,
a general element in $\sigmaF_2$ can be written as
$\Union_{k \in K} B_{k}$ for some $K \subseteq \mathbb{N}$.

Note that $\{A_j \times B_k \}_{j, k \in \mathbb{N}}$ is a partition because:
if $(A_j \times B_k)  \cap (A_{j'} \times B_{k'}) \neq \emptyset$ for some
$j \neq j'$ and $k \neq k'$,
then it must $A_j \cap A_{j'} \neq \emptyset$ and $B_k \cap B_{k'} \neq \emptyset$,
and that imply that $A_j =A_{j'}$ and $B_j =B_{j'}$;
therefore, $A_j \times B_k = A_{j'} \times B_{k'}$.

We next show that $\sigmaF_1 \otimes \sigmaF_2$ is generated by
partition $\{A_j \times B_k \}_{j, k \in \mathbb{N}}$.

\begin{align*}
\sigmaF_1 \otimes \sigmaF_2
&= \closure*{\sigmaF_1 \times \sigmaF_2} \\
&= \closure*{\set*{\Union_{j \in J_1} A_{j} \times \Union_{j \in J_2} B_{j} | J_1, J_2 \subseteq \mathbb{N}}} \\
&= \closure*{\set*{\Union_{j \in J_1, k \in J_2}  A_{j} \times B_{k} | J_1, J_2 \subseteq \mathbb{N} }} \\
&= \closure*{\set*{ A_{j} \times B_{k} | j, k\subseteq \mathbb{N} }}
\end{align*}

Since each $A_j \in C_1 \subseteq \sigmaF_1$ and $B_k \in C_2 \subseteq \sigmaF_2$
a general element in $\sigmaF_1 \otimes \sigmaF_2$ can
be expressed as $\set*{\Union_{j, k \subseteq I} A_{j} \times B_{k} \mid
A_{j} \in \sigmaF_{1}, B_{k} \in \sigmaF_{2}, I \subseteq \mathbb{N}^2}$.

Given two probability spaces
$(\sigmaF_a, \mu_a), (\sigmaF_b, \mu_b) \in \ProbSp(\Outcomes)$,
their independent product
$(\sigmaF_a, \mu_a) \iprod (\sigmaF_b, \mu_b)$ exists
if $\mu_a(E_a) \cdot \mu_b(E_b) = 0 $
for any $E_a \in \sigmaF_a, E_b \in \sigmaF_b$ such that
$E_a \cap E_b = \emptyset$.

We first define $\mu: \set{E_a \cap E_b \mid E_a \in \sigmaF_a, E_b \in \sigmaF_b}
\to [0,1]$ by $\mu(E_a \cap E_b) = \mu_a(E_a) \cdot \mu_b(E_b)$
for any $E_a \in \sigmaF_a, E_b \in \sigmaF_b$,
and then show that $\mu$ could be extended to a probability
measure on $\sigmaF_a \punion \sigmaF_b$.

* We first need to show that $\mu$ is well-defined.
That is,
$E_a \cap E_b = E_a' \cap E_b'$
implies $\mu_a(E_a) \cdot \mu_b(E_b) = \mu_a(E'_a) \cdot \mu_b(E'_b)$.

When $E_a \cap E_b = E_a' \cap E_b'$, it must $E_a \cap E_a' \supseteq
E_a \cap E_b = E_a' \cap E_b'$, Thus, $E_a \setminus E_a' \subseteq E_a
\setminus E_b$, and then $E_a \setminus E_a'$ is disjoint from $E_b$;
symmetrically, $E_a' \setminus E_a$ is disjoint from $E_b'$.
Since $E_a, E_a'$ are both in $\sigmaF_{a}$, we have $E_a \setminus E_a'$
and $E_a' \setminus E_a$ both measurable in $\sigmaF_a$.
Their disjointness and the result above implies that
$\mu_a(E_a \setminus E_a') \cdot \mu_b(E_b) = 0$ and
$\mu_a(E'_a \setminus E_a) \cdot \mu_b(E'_b) = 0$.
Then there are four possibilities:

* If $\mu_b(E_b) = 0$ and $\mu'_b(E_b') = 0$,
then $\mu_a(E_a) \cdot \mu_b(E_b) = 0 = \mu_a(E_a') \cdot \mu_b(E_b')$.

* If $\mu_a(E_a \setminus E'_a) = 0$ and $\mu_b(E'_a \setminus E_a) = 0$.

\begin{align*}
\mu_a(E_a) \cdot \mu_b(E_b) &=
\mu_a((E'_a \setminus E_a) \disjunion (E'_a \cap E_a)) \cdot \mu_b(E_b) \\
&= (\mu_a(E'_a \setminus E_a) + \mu_a(E'_a \cap E_a)) \cdot \mu_b(E_b) \\
&= \mu_a(E'_a \cap E_a) \cdot \mu_b(E_b) \\
&= (\mu_a(E_a \setminus E'_a) + \mu_a(E'_a \cap E_a)) \cdot \mu_b(E_b) \\
&= \mu_a(E'_a) \cdot \mu_b(E_b)
\end{align*}

Note that $E'_b \setminus E_b$ is also disjoint from $E'_a \cap E_a$,
and  $E_b \setminus E'_b$ is also disjoint from $E'_a \cap E_a$.
Thus,  either $\mu_a(E'_a \cap E_a) = 0$, which implies that

\[
\mu_a(E_a) \cdot \mu_b(E_b)  = (0 + 0) \cdot  \mu_b(E_b) = 0 =(0+0) \cdot \mu_b(E_b) = \mu_a(E'_a) \cdot \mu_b(E'_b),
\]

or we have both $\mu_b(E'_b \setminus E_b) = 0$ and $\mu_b(E_b \setminus E'_b) = 0$, which imply that

\begin{align*}
\mu_a(E_a) \cdot \mu_b(E_b)
&= \mu_a(E'_a) \cdot \mu_b(E_b)\\
&= \mu_a(E'_a) \cdot \mu_b((E_b \cap E'_b ) \disjunion (E_b \setminus E'_b)) \\
&= \mu_a(E'_a) \cdot (\mu_b(E_b \cap E'_b ) + 0) \\
&= \mu_a(E'_a) \cdot (\mu_b(E_b \cap E'_b ) + \mu_b(E'_b \setminus E_b)) \\
&= \mu_a(E'_a) \cdot \mu_b(E'_b ).
\end{align*}

* If $\mu_b(E'_b) = 0$ and $\mu_b(E_a \setminus E'_a) = 0$,

\begin{align*}
\mu_a(E_a) \cdot \mu_b(E_b)
&= (\mu_a(E_a \cap E'_a) + \mu_a(E_a \setminus E'_a)) \cdot (\mu_b(E_b \cap E'_b) + \mu_b(E_b \setminus E'_b)) \\
&= \mu_a(E_a \cap E'_a)  \cdot \mu_b(E_b \setminus E'_b)
\end{align*}

The set $E_b \setminus E'_b$ is  disjoint from $E'_a \cap E_a$,
so $\mu_a(E_a \cap E'_a)  \cdot \mu_b(E_b \setminus E'_b) = 0$.
Thus, $\mu_a(E_a) \cdot \mu_b(E_b) =0 = \mu_a(E'_a) \cdot \mu_b(E'_b)$.

* If $\mu_b(E_b) = 0$ and $\mu_b(E'_a \setminus E_a) = 0$,
then symmetric as above.

In all these cases,
$\mu_a(E_a) \cdot \mu_b(E_b) = \mu_a(E'_a) \cdot \mu_b(E'_b)$ as desired.

* Show that $\mu$ satisfy countable additivity in $\{E_a \cap E_b \mid E_a \in \sigmaF_a,
E_b \in  \sigmaF_b\}$.

We start with showing that $\mu$ is finite-additive.
Suppose $E_a^n \cap E_b^n = \Disjunion_{i \in [n]}(A_i \cap B_i)$ where
each $A_i \in \sigmaF_a$ and $B_i \in \sigmaF_b$.
Fix any $A_i \cap B_i$, there is unique minimal $A \in \sigmaF_a$ containing
$A_i \cap B_i$, because if $A \supseteq A_i \cap B_i$ and  $A' \supseteq
A_i \cap B_i$, then  $A \cap A' \supseteq A_i \cap B_i$
and $A \cap A' \sigmaF_A$ too, and $A \cap A'$ is smaller.
Because we have shown that $\mu$ is well-defined, in the following proof,
we can assume without loss of generality that $A_i$ is the smallest set in $\sigmaF_a$ containing $A_i \cap B_i$.
Similarly, we let $B_i$ to be the smallest set in $\sigmaF_b$ containing $A_i \cap B_i$.
Thus,  $E_a^n \cap E_b^n = \Disjunion_{i \in [n]}(A_i \cap B_i)$ implies
every $A_i$ is smaller than $E_a^n$ and every $B_i$ is smaller than $E_b^n$.
$E_a^n \supseteq \cup_{i \in [n]} A_i$ and
$E_b^n \supseteq \cup_{i \in [n]} B_i$,
which implies that

\[
E_a^n \cap E_b^n \supseteq (\cup_{i \in [n]} A_i) \cap (\cup_{i \in [n]} B_i) \supseteq \cup_{i \in [n] } (A_i \cap B_i) = E_a^n \cap E_b^n,
\]

which implies that the $\supseteq$ in the inequalities all collapse to $=$.

For any $I \subseteq [n]$, define
$\alpha_I = \cap_{i \in I} A_i \setminus (\cup_{i \in [n] \setminus I} A_i)$, and $\beta_I = \cap_{i \in I} B_i \setminus (\cup_{i \in [n] \setminus I} B_i)$.
For any $I \neq I'$, $\alpha_I \cap \alpha_{I'} = \emptyset$.
Thus, $\{\alpha_I\}_{I \subseteq [n]}$ is a set of disjoint sets in $\cup_{i \in [n]} A_i$,
and similarly, $\{\beta_I\}_{I \subseteq [n]}$ is a set of disjoint sets in $\cup_{i \in [n]} B_i$.
Also, for any $i \in [n]$,
we have
$A_i = \cup_{I \subseteq [n] \mid i \in I} \alpha_I $
$B_i = \cup_{I \subseteq [n] \mid i \in I} \beta_I $.
Furthermore, for any $I$,

\begin{align*}
\alpha_I \cap \cup_{i \in [n]} B_i
\subseteq (\cup_{i \in [n]} A_i) \cap (\cup_{i \in [n]} B_i)
= \Dunion_{i \in [n]]} A_i \cap B_i ,
\end{align*}

and thus,

\begin{align}
\alpha_I \cap \cup_{i \in [n]} B_i
& = (\Dunion_{i \in [n]} A_i \cap B_i) \cap (\alpha_I \cap \cup_{i \in [n]} B_i) \notag \\
& = \Dunion_{i \in [n]} \left( A_i \cap B_i \cap \alpha_I \cap \cup_{j \in [n]} B_j \right) \notag \\
& = \Dunion_{i \in I} \left( A_i \cap B_i \cap \alpha_I \cap \cup_{j \in [n]} B_j \right)  \tag{$A_i \cap \alpha_I = \emptyset$ if $i \notin I$} \\
& = \Dunion_{i \in I} \left( A_i \cap B_i \cap \alpha_I\right)
\tag{$B_i \cap \cup_{j \in [n]} B_j = B_i$ for any $i$}\\
& = \Dunion_{i \in I} \left( B_i \cap \alpha_I\right)
\tag{$A_i \cap \alpha_I = \alpha_I$ for any $i \in I$ }\\
& = \alpha_I \cap \cup_{i \in I } B_i
\label{eq:finite-add-alpha}
\end{align}

\begin{align}
&\mu(E^n_a \cap E^n_b) \notag \\
&= \mu((\cup_{i \in [n]} A_i) \cap (\cup_{i \in [n]} B_i)) \notag \\
&= \mu((\Dunion_{I \subseteq [n]} \alpha_I) \cap (\cup_{i \in [n]} B_i)) \tag{By definition of $\alpha_I$}\\
&= \mu_a(\Dunion_{I \subseteq [n]} \alpha_I) \cdot  \mu_b(\cup_{i \in [n]} B_i)  \tag{By definition of $\mu$} \\
&= \left(\sum_{I \subseteq [n]} \mu_a (\alpha_I) \right) \cdot  \mu_b(\cup_{i \in [n]} B_i)  \tag{By finite-additivity of $\mu_a$} \\
&= \sum_{I \subseteq [n]} \mu_a (\alpha_I) \cdot  \mu_b(\cup_{i \in [n]} B_i) \notag\\
&= \sum_{I \subseteq [n]}  \mu(\alpha_I \cap (\cup_{i \in [n]} B_i)) \tag{By definition of $\mu$} \\
&= \sum_{I \subseteq [n]}  \mu(\alpha_I \cap (\cup_{i \in I} B_i))
\tag{By~\cref{eq:finite-add-alpha}}\\
&= \sum_{I \subseteq [n]}  \mu_a(\alpha_I) \cdot \mu_b (\cup_{i \in I} B_i)\tag{By definition of $\mu$} \\
&= \sum_{i \in [n]}  \mu_b ( B_i) \cdot \left(\sum_{I \subseteq [n] \text{ s.t. } i \in I}  \mu_a(\alpha_I) \right)\notag \\
&= \sum_{i \in [n]}  \mu_b ( B_i) \cdot \mu_a(A_i) \notag \\
&= \sum_{i \in [n]}  \mu ( A_i \cap B_i) \label{eq:finite-add}
\end{align}

Thus, we established the finite additivity.
For countable additivity, suppose $E_a \cap E_b = \Disjunion_{i \in \mathbb{N}}(A_i \cap B_i)$. By the same reason as above, we also have

\[
E_a \cap E_b = (\cup_{i \in \mathbb{N}} A_i) \cap (\cup_{i \in \mathbb{N}} B_i) = \cup_{i \in \mathbb{N}} (A_i \cap B_i) = E_a \cap E_b.
\]

\begin{align}
&\mu(E_a \cap E_b) \notag \\
&= \mu((\cup_{i \in \mathbb{N}} A_i) \cap (\cup_{i \in \mathbb{N}} B_i)) \notag \\
&= \mu_a(\cup_{i \in \mathbb{N}} A_i) \cdot \mu_b(\cup_{i \in \mathbb{N}} B_i) \notag \\
&= \mu_a(\lim_{n \to \infty} \cup_{i \in [n]} A_i) \cdot \mu_b(\lim_{n \to \infty} \cup_{i \in [n]} B_i) \notag \\
&= \lim_{n \to \infty} \mu_a(\cup_{i \in [n]} A_i) \cdot \lim_{n \to \infty} \mu_b( \cup_{i \in [n]} B_i) \tag{By continuity of $\mu_a$ and $\mu_b$} \\
&= \lim_{n \to \infty} \mu_a(\cup_{i \in [n]} A_i) \cdot \mu_b( \cup_{i \in [n]} B_i) \tag{$\dagger$} \\
&= \lim_{n \to \infty} \sum_{i \in [n]}  \mu_b ( B_i) \cdot \mu_a(A_i) \tag{By~\cref{eq:finite-add}} \\
&= \sum_{i \in \mathbb{N}}  \mu_b ( B_i) \cdot \mu_a(A_i),
\end{align}

where $\dagger$ is because that the product of limits equals to the limit of
the product when both $\lim_{n \to \infty} \mu_a(\cup_{i \in [n]} A_i)$ and
$\lim_{n \to \infty} \mu_b( \cup_{i \in [n]} B_i)$ are finite.
Thus, we proved countable additivity as well.

* Next we show that we can extend $\mu$ to a measure on
$\sigmaF_a \punion \sigmaF_b$.

So far, we proved that $\mu$ is a sub-additive measure on the
$\{E_a \cap E_b \mid E_a \in \sigmaF_a, E_b \in \sigmaF_b\}$,
which forms a $\pi$-system.
By known theorem in probability theory
(e.g., corollary 2.5.4 of [Rosenthal, 2006]),
we can extend a sub-additive measure on a
$\pi$-system to the sigma algebra it generates if the $\pi$-system is
a semi-algebra.
Thus, we can extend $\mu$ to a measure on $\closure{\{E_a \cap E_b \mid E_a \in \sigmaF_a,\ E_b \in \sigmaF_b\}}$ if we can prove $J = \{E_a \cap E_b \mid E_a \in \sigmaF_a,\ E_b \in \sigmaF_b\}$ is a semi-algebra.

* $J$ contains $\emptyset$ and $\Outcomes$: trivial.

* $J$ is closed under finite intersection:
$(E_a \cap E_b) \cap (E'_a \cap E'_b) = (E_a \cap E'_a) \cap (E_b \cap E'_b)$, where $E_a \cap E'_a \in \sigmaF_a$, and $E_b \cap E'_b \in \sigmaF_b$.

* The complement of any element of $J$ is equal to a finite disjoint
union of elements of $J$:

\begin{align*}
(E_a \cap E_b)^C &= E_a^C \cup E_b^C \\
&= (E_a^C \cap \Outcomes) \disjunion (E_a \cap E_b^C)
\end{align*}

where $E_a^C, E_a \in \sigmaF_a$, and $E_b^C, \Outcomes \in \sigmaF_b$.

As shown in [Li et al, 2023],

\begin{align}
\closure{\{E_a \cap E_b \mid E_a \in \sigmaF_a, E_b \in \sigmaF_b\}}
= \sigmaF_a \punion \sigmaF_b
\end{align}

Thus, the extension of $\mu$ is a measure on $\sigmaF_a \punion \sigmaF_b$.

* Last, we show that $\mu$ is a probability measure on
$\sigmaF_a \punion \sigmaF_b$:
$\mu(\Outcomes) = \mu_a(\Outcomes) \cdot \mu_b(\Outcomes) = 1$.

Consider two probability spaces
$(\sigmaF_1, \mu_1), (\sigmaF_2, \prob_2) \in \ProbSp(\Outcomes)$,
and some other probability space $(\Full{A}, \prob)$ and kernel $\krnl$
such that $\prob_1 = \bind(\prob, \krnl)$.

Then, the independent product
$(\sigmaF_1, \mu_1) \iprod (\sigmaF_2, \mu_2)$
exists if and only if
for any $a \in \psupp(\prob)$,
the independent product
$(\sigmaF_1, \krnl(a)) \iprod (\sigmaF_2, \prob_2)$ exists.
When they both exist,

\[
(\sigmaF_1, \prob_1) \iprod (\sigmaF_2, \prob_2)
= (\sigmaF_1 \punion \sigmaF_2,
\bind(\prob, \fun a. \krnl(a) \iprod \prob_2))
\]

We first show the backwards direction.
By <ref>,
for any $a \in \psupp(\prob)$, to show that the independent product
$(\sigmaF_1, \krnl(a)) \iprod (\sigmaF_1, \prob_1)$ exists,
it suffices to show that for any $E_1 \in \sigmaF_1, E_2 \in \sigmaF_2$
such that $E_1 \cap E_2 = \emptyset$,
$\krnl(a)(E_1) \cdot \prob_2(E_2) = 0$.

Fix any such $E_1, E_2$,
because $(\sigmaF_1, \prob_1) \iprod (\sigmaF_2, \prob_2)$ is defined,
we have $\prob_1(E_1) \cdot \prob_2(E_2) = 0$, then either $\prob_1(E_1) = 0$
or $\prob_2(E_2) = 0$.

* If $\prob_1(E_1) = 0$:
Recall that

\[
\prob_1(E_1) = \bind(\prob, \krnl)(E_1)
= \sum_{a \in A} \prob(a) \cdot \krnl(a) (E_1)
= \sum_{\mathclap{a \in \psupp(\prob)}} \prob(a) \cdot \krnl(a) (E_1)
\]

Because all $\prob(a) > 0$ and $\krnl(a) (E_1) \geq 0$ for all $a \in \psupp(\prob)$
$\sum_{a \in \psupp(\prob)} \prob(a) \cdot \krnl(a) (E_1) = 0$ implies that
$\prob(a) \cdot \krnl(a) (E_1) = 0$ for all $a \in \psupp(\prob)$.
Thus, for all $a \in \psupp(\prob)$, it must $\krnl(a) (E_1) = 0$.
Therefore, $\krnl(a)(E_1) \cdot \prob_2(E_2) = 0$ for all  $a \in \psupp(\prob)$
with this $E_1, E_2$.

* If $\prob_2(E_2) = 0$, then it is also clear that
$\krnl(a)(E_1) \cdot \prob_2(E_2) = 0$ for all  $a \in \psupp(\prob)$.

Thus, we have $\krnl(a)(E_1) \cdot \prob_2(E_2) = 0$ for any
$E_1 \cap E_2 = \emptyset$ and $a \in \psupp(\prob)$.
By <ref>,
the independent product $(\sigmaF_1, \krnl(a)) \iprod (\sigmaF_1, \prob_1)$ exists.

For the forward direction:
for any $E_1 \in \sigmaF_1$ and $E_2 \in \sigmaF_2$ such that $E_1 \cap E_2 = \emptyset$,
the independent product $(\sigmaF_1, \krnl(a)) \iprod (\sigmaF_2, \mu_2)$ exists implies that

\begin{align*}
\krnl(a) (E_1) \cdot \mu_2(E_2) = 0.
\end{align*}

\begin{align*}
\mu_1(E_1) \cdot \mu_2(E_2)
&= \bind(\mu, \krnl)(E_1)  \cdot \mu_2(E_2) \\
&= \left(\sum_{a \in A} \mu(a) \cdot \krnl(a) (E_1) \right)  \cdot \mu_2(E_2) \\
&= \sum_{a \in A_{\mu}} \mu(a) \cdot \left(\krnl(a) (E_1)  \cdot \mu_2(E_2) \right) \\
&= \sum_{a \in A_{\mu}} \mu(a) \cdot 0 \\
&= 0
\end{align*}

Thus, by <ref>,
the independent product $(\sigmaF_1, \mu_1) \iprod (\sigmaF_2, \mu_2)$ exists.
For any $E_1 \in \sigmaF_1$ and $E_2 \in \sigmaF_2$,

\begin{align*}
\bind(\prob, \fun a. \krnl(a) \iprod \prob_2 ) (E_1 \inters E_2)
&= \sum_{\mathclap{a \in \psupp(\prob)}}
\prob(a) \cdot
\left(\krnl(a) \iprod  \m{\prob_2}\right)(E_1 \inters E_2) \\
&= \sum_{\mathclap{a \in \psupp(\prob)}}
\prob(a) \cdot \krnl(a)(E_1) \cdot \prob_2(E_2) \\
&= \left(
\sum_{a \in \psupp(\prob)}
\prob(a) \cdot \krnl(a)(E_1)
\right) \cdot \prob_2(E_2) \\
&= \bind(\prob, \krnl)(E_1) \cdot \prob_2(E_2) \\
&= \prob_1(E_1) \cdot \prob_2(E_2) \\
&= \prob_1(E_1) \cdot \prob_2(E_2) \\
&= (\prob_1 \iprod \prob_2)(E_1 \inters E_2)
\end{align*}

(\sigmaF_1, \prob_1) \iprod (\sigmaF_2, \prob_2)
= (\sigmaF_1 \punion \sigmaF_2,
\bind(\prob, \fun a. \krnl(a) \iprod \prob_2)).

§ MODEL

§.§ Basic connectives

The following are the definitions of the standard SL connectives
we use in :

\begin{align*}
\pure{\phi} &\is \fun \wtv. \phi
P * Q &\is \fun a.
\exists b_1,b_2 \st
(b_1 \raOp b_2) \raLeq a \land
P(b_1) \land
\\
\Own{b} &\is \fun a. b \raLeq a
P \wand Q &\is \fun a.
\forall b\st
\raValid(a \raOp b)
\implies
\implies
Q(a \raOp b)
\\
P \land Q &\is \fun a. P(a) \land Q(a)
\A x \of X.P(x) &\is \fun a.
\forall x \in X\st P(x)(a)
\\
P \lor Q &\is \fun a. P(a) \lor Q(a)
\E x \of X.P(x) &\is \fun a.
\exists x \in X\st P(x)(a)
\end{align*}

§.§ Construction of the  model

The structure $\PSpRA$ is an ordered unital resource algebra (RA) as defined
in <ref>.

We defined $\raOp$ and $\raLeq$ the same way as in [Li et al, 2023],
and they have proved that $\raOp$ is associative and commutative,
and $\raLeq$ is transitive and reflexive.
We check the rest of conditions one by one.

[Condition $a \raOp b = b \raOp a$]
The independent product is proved to be commutative in  [Li et al, 2023].
[Condition $(a \raOp b) \raOp c = a \raOp (b \raOp c)$]
The independent product is proved to be associative in [Li et al, 2023].
[Condition $a \raLeq b \implies b \raLeq c \implies a \raLeq c$]
The order $\raLeq$ is proved to be transitive in [Li et al, 2023].
[Condition $a \raLeq a$]
The order $\raLeq$ is proved to be reflexive in [Li et al, 2023].
[Condition $\raValid(a \raOp b) \implies \raValid(a)$]
Pattern matching on $a \raOp b$,
either there exists probability spaces $\psp_1, \psp_2$ such that
$a = \psp_1$, $b = \psp_2$ and $\psp_1 \iprod \psp_2$ is defined,
or $a \raOp b = \invalid$.

[$a \raOp b = \invalid$] Note that
$\raValid(a \raOp b)$ does not hold when $a \raOp b = \invalid$,
so we can eliminate this case by ex falso quodlibet.
[$a \raOp b = \psp_1 \iprod \psp_2$] Then
$a = \psp_1$, and thus $\raValid(a)$.

[Condition $\raValid(\raUnit)$]
Clear because $\raUnit \neq \invalid$.
[Condition $a \raLeq b \implies \raValid(b) \implies \raValid(a)$]
Pattern matching on $a$ and $b$,
either there exists probability spaces $\psp_1, \psp_2$ such that
$a = \psp_1$, $b = \psp_2$ and $\psp_1 \extTo \psp_2$ is defined,
or $b = \invalid$.

[$b = \invalid$] Then $\raValid(b)$ does not hold,
and we can eliminate this case by ex falso quodlibet.
[$a = \psp_1$, $b = \psp_2$ and
$\psp_1 \extTo \psp_2$]  We clearly have $\raValid(a)$.

[Condition $\raUnit \raOp a = a$]
Pattern matching on $a$,
either $a = \invalid$
or there exists some probability space $\psp$ such that $a = \psp$.

[$a = \invalid$] Then $\raUnit \raOp a = \invalid = a$.
[$a = \psp$] Then $\raUnit \raOp a = a$.

[Condition $a \raLeq b \implies a \raOp c \raLeq b \raOp c$]
Pattern matching on $a$ and $b$.
If $a \raLeq b $,
then either $b = \invalid$ or there exists
$\psp, \psp'$ such that $a = \psp$ and $b = \psp'$.

[$b = \invalid$] Then $b \raOp c = \invalid$ is the top element,
and then $a \raOp c \raLeq b \raOp c$.
$a \raLeq b$ iff $\psp \raLeq \psp'$,
then either $b \raOp c = \invalid$ and $a \raOp c \raLeq b \raOp c$ follows,
or  $b \raOp c = \psp' \iprod \psp''$
for some probability space $c = \psp''$.
Then $\psp \raLeq \psp'$ implies that
$\psp \raOp \psp''$ is also defined and
$\psp \raOp \psp' \raLeq \psp \raOp \psp''$.
Thus, $a \raOp c \raLeq b \raOp c$ too.

\[
\salg_1\compat\permap_1
\implies
\salg_2\compat\permap_2
\implies
(\salg_1 \punion \salg_2)\compat(\permap_1 \raOp \permap_2)
\]

Let $S_1 = \set{x \in \Var \mid \permap_1(x) = 0}$,
$S_2 = \set{x \in \Var \mid \permap_2(x) = 0}$.
If $\salg_1\compat\permap_1$, then there exists
$\psp_1' \in \ProbSp((\Var \setminus S_1) \to \Val)$
such that
$\psp_1 = \psp_1' \pprod \Triv{S_1 \to \Val}$
In addition, if $\salg_2\compat\permap_2$, then there exists
$\psp_2' \in \ProbSp((\Var \setminus S_2) \to \Val)$
such that
$\psp_2 = \psp_2' \pprod \Triv{S_2 \to \Val}$.

\begin{align*}
\psp_1 \raOp \psp_2
&= \psp_1 \iprod \psp_2 \\
&= (\psp_1' \pprod \Triv{S_1 \to \Val}) \iprod
(\psp_2' \pprod \Triv{S_2 \to \Val})
\end{align*}

Say $(\salg_1', \prob_1') = \psp_1'$,
and  $(\salg_2', \prob_2') = \psp_2'$.
Then the sigma algebra of $\psp_1 \raOp \psp_2$

\begin{align*}
&\closure{\set{(E_1 \times S_1 \to \Val) \cap (E_2 \times S_2 \to \Val) \mid E_1 \in \salg_1', E_2 \in \salg_2'}} \\
= & \closure{\set{\left( (E_1 \times (S_1 \setminus S_2) \to \Val) \cap (E_2 \times (S_2 \setminus E_1) \to \Val) \right) \times (S_1 \cap S_2) \mid E_1 \in \salg_1', E_2 \in \salg_2'}}
\end{align*}

Then, there exists $\psp'' \in \ProbSp((\Var \setminus (S_1 \cap S_2)) \to \Val)$ such that
$\psp_1 \raOp \psp_2 = \psp'' \pprod  \Triv{(S_1 \cap S_2) \to \Val})$.

\begin{align*}
&\set{x \in \Var \mid (\permap_1 \raOp \permap_2)(x) = 0} \\
=&\set{x \in \Var \mid \permap_1(x) + \permap_2(x) = 0} \\
=&\set{x \in \Var \mid \permap_1(x) = 0 \text{ and } \permap_2(x) = 0} \\
=& S_1 \cap S_2
\end{align*}

Therefore, $\salg_1 \punion \salg_2$ is compatible with $\permap_1 \raOp \permap_2$

The structure $(\Perm, \raLeq, \raValid, \raOp, \raUnit)$ is an ordered unital resource algebra (RA) as defined
in <ref>.

We check the conditions one by one.

[Condition $a \raOp b = b \raOp a$]
Follows from the commutativity of addition.

[Condition $(a \raOp b) \raOp c = a \raOp (b \raOp c)$]
Follows from the associativity of addition.

[Condition $a \raLeq b \implies b \raLeq c \implies a \raLeq c$]
$\raLeq$ is a point-wise lifting of the order $\leq$ on arithmetics,
so it follows from the transitivity of $\leq$.

[Condition $a \raLeq a$]
$\raLeq$ is a point-wise lifting of the order $\leq$ on arithmetics,
so it follows from the reflexivity of $\leq$.

[Condition $\raValid(a \raOp b) \implies \raValid(a)$]
By definition,

\begin{align*}
\raValid(a \raOp b)
&\implies \forall x \in \Var, (a \raOp b)(x) \leq 1 \\
&\implies \forall x \in \Var, a(x) + b(x) \leq 1 \\
&\implies \forall x \in \Var, a(x) \leq 1 \\
&\implies \raValid(a)
\end{align*}

[Condition $\raValid(\raUnit)$]
Note that $\raUnit = \fun \wtv. 0$ satisfies that
$\forall x \in \Var, \raUnit(x) \leq 1$,
so $\raValid(\raUnit)$.

[Condition $a \raLeq b \implies \raValid(b) \implies \raValid(a)$]
By definition,
$a \raLeq b$ means
$\forall x \in \Var. a(x) \leq b(x)$,
and $\raValid(b)$ means that
$\forall x \in \Var. b(x) \leq 1$.
Thus, $a \raLeq b$ and $\raValid(b)$ implies that
$\forall x \in \Var. a(x) \leq b(x) \leq 1$,
which implies $\raValid(a)$.

[Condition $\raUnit \raOp a = a$]
By definition,

\begin{align*}
\raUnit \raOp a
&= \fun x. (\fun \wtv. 0)(x) + a(x) \\
&= \fun x. 0 + a(x) \\
&= a.
\end{align*}