# On Separation Logic, Computational Independence, and Pseudorandomness
(Extended Version)

Ugo Dal Lago This author was partially supported by the MUR FARE project
”Compositional and Effectful Program Distances”, CAFFEINE Univeristà di
Bologna  Inria  Davide Davoli This author was supported by the French “Agence
Nationale de la Recherche” through the project UCA DS4H ANR-17-EURE-0004.
Inria  Université Côte d’Azur  Bruce M. Kapron This author was supported in
part by NSERC RGPIN 2021-02481 and by a Visiting Fellowship at the Institute
of Advanced Studies of the Alma Mater Studiorum - University of Bologna.
University of Victoria

###### Abstract

Separation logic is a substructural logic which has proved to have numerous
and fruitful applications to the verification of programs working on dynamic
data structures. Recently, Barthe, Hsu and Liao have proposed a new way of
giving semantics to separation logic formulas in which separating conjunction
is interpreted in terms of probabilistic independence. The latter is taken in
its exact form, i.e., two events are independent if and only if the joint
probability is the product of the probabilities of the two events. There is
indeed a literature on weaker notions of independence which are
_computational_ in nature, i.e. independence holds only against efficient
adversaries and modulo a negligible probability of success. The aim of this
work is to explore the nature of computational independence in a cryptographic
scenario, in view of the aforementioned advances in separation logic. We show
on the one hand that the semantics of separation logic can be adapted so as to
account for complexity bounded adversaries, and on the other hand that the
obtained logical system is useful for writing simple and compact proofs of
standard cryptographic results in which the adversary remains hidden.
Remarkably, this allows for a fruitful interplay between independence and
pseudorandomness, itself a crucial notion in cryptography.

##  1 Introduction

Cryptographic primitives and protocols can be defined and analyzed using two
distinct models, i.e. the _computational_ model [1, 2, 3] and the _symbolic_
model [4, 5]. While in the latter adversaries have unlimited computational
power, in the former they are assumed to be efficient (i.e. polytime)
randomized algorithms. In the last forty years, research concerning the
interactions between logic and cryptography has been intense, but while the
symbolic model, given its more qualitative nature, has been the object of many
systematic investigations [6, 7, 8, 9, 10], the same cannot be said about the
computational model, in relation to which the proposals for logical systems
are more scattered and mostly recent (see Section 9 for a more in-depth
discussion on related work).

Proposals concerning logical systems that capture _computational_
cryptographic reasoning are bound to face, at least in principle, some
challenges. The first is certainly the fact that adversaries have limited
complexity, and can have a non-null, albeit negligible, probability of
success. All that must be somehow reflected in the logical languages used,
which are often not standard. Similarly, the underlying notion of equivalence
between programs cannot be the standard, exact, one, but must be relaxed to
so-called computational indistinguishability, the logical nature of which has
been studied from different viewpoints [11, 12]. Finally, one should mention
pseudorandomness, the natural computational counterpart to randomness, whose
logical status has recently been scrutinized from the perspective of
descriptive complexity [13].

There is yet another aspect of the computational model which is deeply rooted
in probability theory, and which is known to be fruitful in cryptography.
Since the work by Shannon, indeed, it is well known that the perfect security
of a symmetric cipher can be formulated very elegantly as the _independence_
between the random variable modeling the message and the one modeling the
ciphertext. On the one hand, it is certainly worth noting that since Yao’s
pioneering work on the computational model, strong links are known between the
notion of computational security for symmetric encryption schemes and
appropriate variations of the concept of independence [3], all this thus
generalizing Shannon’s definition to the setting of complexity-bounded
adversaries. Such a view has remained outside mainstream cryptography, with
interesting but sporadic contributions [14, 15, 16]. On the other hand, it
must be said that a logical account of the notion of _statistical_
independence has indeed been proposed very recently by Barthe, Hsu and Liao
[17], based on separation logic. In this approach, dubbed _probabilistic
separation logic_ (PSL) in the following, separating conjunction is
interpreted in the sense of independence and not in the traditional sense of
dynamic data structures. Probabilistic separation logic is by its nature
information-theoretic, therefore not able to take into account computational
notions of independence. Nonetheless, not only Shannon’s proof, but also much
more complex ones, become very simple and straightforward, being based on some
basic principles regarding probabilistic independence.

It is therefore natural to ask whether and to what extent the approach of [17]
can be adapted to _computational_ notions of independence. This is exactly the
aim of this paper.

###  1.1 Contributions and Outline

The first thing we do, after briefly motivating our work through a couple of
examples, is to introduce in Section 3 a minimal imperative programming
language where all programs can be evaluated in polytime _by construction_.
The language consists only of assignments, sequential composition, and
conditional constructs. Notably, randomization is captured through function
symbols. We take this approach first of all because it allows the treatment of
some interesting examples, and secondly because the possibility of capturing
programs with loops turns out to be by no means trivial especially from the
point of view of managing the adversary’s advantage.

We then proceed, in Section 4, to a study of how Barthe et al.’s probabilistic
separation logic can be adapted so as to capture computational, rather than
information-theoretic, independence. The logic stays the same syntactically,
while the underlying semantics has to be modified in a crucial way. More
specifically, the partial Kripke resource monoid from [18] has to be modified
in its order-theoretic part, allowing computationally indistinguishable
distributions to be compared, and thus implicitly accounting for an
approximate notion of independence. These apparently innocuous modifications
have very deep consequences for the interpretation of separating conjunction.
We exclude from formulas both forms of implication, whose presence would
complicate considerably the underlying metatheory, and which are not
particularly useful in proofs. Remarkably, our novel semantic interpretation
naturally induces atomic formulas capturing computationally independent pairs
of expressions and pseudorandom expressions, this way dealing with fundamental
concepts in cryptography in a simple and natural way.

The next section, i.e. Section 5, instead, concerns the use of our separation
logic as a program logic. More specifically, we study how to define Hoare
triples for the language introduced in Section 3, and how to define sound
inference rules for such triples. Here, what is surprising is that the rules
are not too different from those presented in [17]. In other words,
computational notions can be treated similarly to the corresponding
information-theoretic notions. We apply the introduced formal system to a
couple of simple examples of cryptographic proofs, namely the security of the
encryption scheme induced by a pseudorandom generator, and the proof that
suitably composing pseudorandom generators preserve pseudorandomness, at the
same time allowing for an increase in the expansion factor.

Finally, Section 7 is concerned with motivating computational independence,
and with studying its role in cryptographic proofs. As mentioned above, such
an approach was already proposed by Yao [3] in some of the earliest work on
encryption security, although his work used the language of computational
entropy. An explicit notion of computational independence was introduced and
studied in [15]. We formulate a notion of computational independence which is
in some ways more closely related to the computational semantics of the
separating conjunction, and prove that it is equivalent to that of [15].
Finally, we solve an open problem posed in that paper, namely giving a
characterization of semantic security for private-key encryption against
_uniform_ adversaries [19]. Overall, the results of this section further
support the naturalness of computational independence in a cryptographic
setting as well as indicating its utility as an alternate approach to
characterizing cryptographic security. This also argues for the naturalness
and utility of cryptographic separation logic as a formal counterpart to this
computational approach.

##  2 A Cryptographic Viewpoint on (Probabilistic) Separation Logic

In this section, we give, without going into technical details the
introduction of which is deferred to the next section, a simple account of
separation logic, the probabilistic interpretation of the latter proposed by
Barthe et al., and the possibility of employing it to derive proofs in the so-
called computational model.

Consider the following simple probabilistic program, call it $\mathtt{OTP}$:

$\displaystyle k\leftarrow\mathit{rnd}();$ $\displaystyle
c\leftarrow\mathit{xor}(m,k)$

This program assigns to the variable $k$, a binary string of length $n$, one
of the $2^{n}$ possible values it can take, each with the same probability. It
then uses this value, seen as a key, to construct a ciphertext $c$ starting
from a message $m$ through the exclusive or operation, thus implementing the
well-known Vernam’s one-time pad, an encryption scheme that is established as
secure in the perfect sense [20]. This last property can be expressed in
various ways, e.g. by prescribing that the random variables $\mathcal{C}$ and
$\mathcal{M}$ which model the values of $c$ and $m$ after program execution,
respectively, are _independent_.

Would it be possible to (re)prove the security of such an encryption scheme
using Hoare’s logic? As already mentioned, Barthe et al. gave a positive
answer to this question a few years ago, based on separation logic [17]. In
their framework, one can derive the following triple

$\left\\{\mathbf{D}(m)\right\\}\;\mathtt{OTP}\;\left\\{\mathbf{D}(m)*\mathbf{U}(c)\right\\}$

This tells us that, whenever messages are distributed according to _any_
distribution (this is captured by the precondition $\mathbf{D}(m)$), the
ciphertexts will be uniformly distributed, $\mathbf{U}(c)$, and moreover (and
most importantly!) their distribution will be statistically independent from
that on messages. This latter condition is captured by the binary logical
operator $*$, the so-called _separating conjunction_.

The separating conjunction is a connective of _separation logic_ [21], which
is often interpreted in such a way as to enable reasoning about pointer-
manipulating programs: the elements of the domain are _heaps_ representing the
state of memory and the truth of a formula $\phi*\psi$ in a store $s$
indicates that $s$ may be split into two stores, the first satisfying $\phi$
and the second satisfying $\psi$. In Barthe et al.’s work, instead, there is
no heap, each variable contains a piece of data, and formulas are interpreted
over _distributions_ of states. In that setting, it is natural for separating
conjunction to model _independence_ : a distribution $s$ satisfying a formula
$\phi*\psi$ captures the fact that $s$ can be written as the _tensor product_
of two distributions, the first satisfying $\phi$ and the second satisfying
$\psi$. In the program above, then, $\mathbf{D}(m)*\mathbf{U}(c)$ correctly
captures the desired property: the distributions of states over $k,m,c$ one
obtains after executing $\mathtt{OTP}$ can be written as the tensor product of
two distributions, the value of $c$ being uniformly distributed in the second
distribution. As such, then, separation logic correctly captures the perfect
security of the OTP.

The question that arises naturally, at this point, is whether this way of
reasoning is also compatible with the computational model, whereas, as is well
known, adversaries are complexity bounded and their probability of success can
be strictly positive, although negligible. Is it possible, for example, to
prove something similar to the aforementioned independence result for the
following simple variation of Vernam’s cipher?

$\displaystyle r\leftarrow\mathit{rnd}();$ $\displaystyle
c\leftarrow\mathit{xor}(m,g(r))$

Here, we first pass a random seed $r$ to a pseudorandom generator $g$,
stretching it into a stream of bits that, although not random, looks so to any
PPT adversary. Then, we proceed as in Vernam’s cipher. In this way, we are
able to use a key of length $n$ to encrypt messages of greater length.

The first thing to observe is that it is simply _not_ true that for any
distribution on messages, the distributions on messages and ciphertexts are
statistically independent. In particular, far a distribution on messages
having full support, since there are fewer keys than messages, we can find a
ciphertext $c$ which has nonzero probability and a message $m$ such that the
joint probability of $c$ and $m$ is zero. This means independence does not
hold. As observed by Yao [3], and later studied by Fay [15], however, the
aforementioned random variables are independent in a _computational_ sense,
i.e. their joint distribution, even if impossible to be written as the tensor
product of two distributions, looks so, once again, to the eyes of efficient
adversaries.

This work can be seen as the first attempt to go _in the direction_ traced by
Yao and Fay _starting from_ Barthe et al.’s PSL. In particular, the latter
will be adapted to the fact that programs and adversaries are complexity-
bounded and that the notion of randomness is computational, i.e. equivalent to
_pseudorandomness_. Similarly, for separating conjunction and independence:
everything holds in an approximate sense, the approximation being invisible to
the eyes of efficient adversaries having nonnegligible probability of success.

While this adaptation may apparently seem straightforward, it brings with it a
series of complications. First of all, the class of programs to which this
reasoning can be applied must be drastically restricted, dealing with
conditionals and sequential compositions, but without loops. The very notion
of formula must be narrowed, getting rid of logical implication and
restricting attention to conjunctive formulas. Furthermore, in order to make
the splitting of the program unique, we will require formulas to be labeled
with type environments. These changes are not motivated by semantic reasons:
in fact, BI _can_ be given a complexity-conscious semantics in the form of a
partial resource monoid, therefore following a well-trodden path. The point is
that in BI and its standard semantics proving the soundness of some crucial
rules, and in particular the so-called frame rule, turns out to be very
difficult compared to doing so for PSL. It was therefore natural to move
towards a narrower definitional framework. That being said, simple examples
like the one above can be shown to have the desired independence properties.

A question naturally arises at this point: is computational independence
related in any way to mainstream cryptographic notions? Fortunately, the
answer is positive: security of symmetric-key ciphertext can be faithfully
captured this way, making our program logic useful. This represents the ideal
way to complete the picture, and Section 7 is devoted to proving this result.

##  3 Programs, and their Semantics

In this section, we define programs and their interpretation as transformers
of _efficiently samplable_ families of distributions [19, 20]. While doing
this, we also introduce other standard concepts such as sized types and with
the aim of describing their interplay and their notation.

We start by introducing basic notions from probability theory in Section
3.1.1. In Section 3.1.2, we define types, environments and stores. Later, in
Section 3.2 and in Section 3.3 we define the language of programs together
with its semantics. In Section 3.5.1, we show that the semantics of our
programs — when interpreted on ordinary distributions — is equivalent to that
of Kozen [23]. In section Section 3.4, we introduce some basics concepts of
computational cryprography including _computational indistinguishability_.
Finally, Section 3.5 is devoted to showing cryptographical properties of our
programs.

###  3.1 Preliminaries

####  3.1.1 Probabilities and Distributions

In the following, we restrict our analysis to probability distributions with
finite support. More precisely, each such object is a function
$\mathcal{D}:X\to\mathbb{R}_{[0,1]}$ that satisfies the following properties:

  * •

Its support ${\mathsf{supp}}(\mathcal{D})\mathrel{:=}\\{x\in
X\mid\mathcal{D}(x)>0\\}$ is finite.

  * •

$\sum_{x\in{\mathsf{supp}}(\mathcal{D})}\mathcal{D}(x)=1$.

We write $\mathbb{D}(X)$ for the set of all distributions over $X$.

The tensor product of two distributions
$\mathcal{D}\in\mathbb{D}(X),\mathcal{E}\in\mathbb{D}(Y)$ is another
distribution, this time over ($X\times Y$) that samples independently from
$\mathcal{D}$ and $\mathcal{E}$, i.e.,
$(\mathcal{D}\mathrel{\otimes}\mathcal{E})\mathrel{:=}(x,y)\mapsto\mathcal{D}(x)\cdot\mathcal{E}(y)$.

Probability distributions with finite support form a monad [22], where the
unit function ${\text{unit}_{X}(\cdot)}:X\to\mathbb{D}(X)$ associates to its
argument $x\in X$ the Dirac distribution centered on $x$ and the
multiplication
$\text{bind}_{X}(\cdot,\cdot):\mathbb{D}(X)\times(X\to\mathbb{D}(Z))\to\mathbb{D}(Z)$
sequences $\mathcal{D}\in\mathbb{D}(X)$ with a continuation
$f:X\to\mathbb{D}(Z)$. This property induces the existence of the Kleisli
extension of each function $f:X\to\mathbb{D}(Y)$: this is a function
$f^{\dagger}:\mathbb{D}(X)\to\mathbb{D}(Y)$ such that
$f^{\dagger}(\mathcal{D})=\text{bind}_{X}(\mathcal{D},f)$. Given a
distribution $\mathcal{D}\in\mathbb{D}(X)$ and a function $f:X\to Y$, we write
$f(\mathcal{D})$ to denote $y\mapsto\sum_{x\in f^{-1}(y)}\mathcal{D}(x)$.

####  3.1.2 Types

In this section, we define types and environments, together with their
interpretation as _families_ of distributions. Programs and stores are indeed
typed to enforce size bounds to variables, depending on the value of the so-
called _security parameter_. For instance, if the type associated to the
variable $r$ by the environment $\Delta$ is $\mathsf{Str}[2n]$, the size of
the binary string associated to $\Delta$ by a store of type $r$ must be
_exactly_ $2n$, i.e. two times the length of the security parameter. By
allowing only types whose size is polynomial in the size of the security
parameter, we ensure that the evaluation of _well-typed_ programs on _well-
typed_ stores is polytime with respect to the size of the security parameter.

_Univariate positive polynomials_ are indicated by metavariables like $p$ and
$q$; we write $p(n)$ for the natural number obtained by evaluating the
polynomial $p$ on the argument $n\in\mathbb{N}$. _Types_ are defined from the
following grammar:

$\tau::=\mathsf{Str}[p]\;\mbox{\Large{$\mid$}}\;\mathsf{Bool}.$

where $p$ is a univariate polynomial. Let $\mathsf{T}$ be the set of all
types. Given $\tau$ and $n\in\mathbb{N}$,
$\llbracket\mathsf{Str}[p]\rrbracket_{n}^{\mathtt{d}}=\mathbb{B}^{p(n)}$,
$\llbracket\mathsf{Bool}\rrbracket_{n}^{\mathtt{d}}=\mathbb{B}$, and
$\mathbb{B}=\\{0,1\\}$ is the set of binary digits.

The set of program variables is $\mathcal{V}$, and it is ranged over by
metavariables like $r,s$. An _environment_
$\Delta:\mathcal{V}\rightharpoonup\mathsf{T}$ is a partial function with
finite domain indicated as $\mathsf{dom}(\Delta)$. We write $\varepsilon$ for
the empty environment, and we also adopt standard abbreviations for
environments in the form of lists of assignments of types to variables, e.g.
$r_{1}:\tau_{1},\ldots,r_{k}:\tau_{k}$. We introduce a partial order relation
between environments: $\Xi\sqsubseteq\Delta$ holds whenever
$\mathsf{dom}(\Xi)\subseteq\mathsf{dom}(\Delta)$ and for every
$r\in\mathsf{dom}(\Xi)$ we have $\Xi(r)=\Delta(r)$. The (disjoint) union of
two environments $\Delta,\Xi$ is indicated as $\Delta\Join\Xi$ and is defined
_only_ if $\mathsf{dom}(\Delta)\cap\mathsf{dom}(\Xi)=\emptyset$; when this
happens, it is defined in the standard way.

It is now time to turn to the interpretation of types, which will be built
around the notion of an efficiently samplable distribution family. This is a
standard notion in complexity-based cryptography (see Subsection 3.4) and is
captured by the following definition:

######  Definition 1.

A family of distributions $\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}$ is
_efficiently samplable_ when there is _one_ probabilistic polytime algorithm
that outputs samples distributed according to $\mathcal{D}_{n}$ on input
$1^{n}$. In this case, we write
$\mathsf{ES}({\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}})$. $\hfill\qed$

The semantics of a type $\tau$, which we call $\llbracket\tau\rrbracket$ is
the class of (efficiently samplable) families
$\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}$ such that
$\mathcal{D}_{n}\in\mathbb{D}(\llbracket\tau\rrbracket_{n}^{\mathtt{d}})$ for
every $n\in\mathbb{N}$. Formally:

$\llbracket\tau\rrbracket\mathrel{:=}\\{\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}\mid\mathsf{ES}({\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}})\land\forall
n\in\mathbb{N}.\mathcal{D}_{n}\in\llbracket\tau\rrbracket_{n}\\}.$

In the following, we will often abbreviate
$\\{\mathcal{D}_{n}\\}_{n\in\mathbb{N}}$ as just $\mathcal{D}$.

We can extend the semantics above from types to environments. An environment
$\Delta$ is interpreted as a set of _distribution ensembles_ in the following
way:

$\displaystyle\llbracket\Delta\rrbracket$
$\displaystyle\mathrel{:=}\\{\\{\mathcal{R}_{n}\\}_{n}\mid\mathsf{ES}({\mathcal{R}})\land\forall
n\in\mathbb{N}.\mathcal{R}_{n}\in\llbracket\Delta\rrbracket_{n}\\}$

where
$\llbracket\Delta\rrbracket_{n}=\mathbb{D}(\llbracket\Delta\rrbracket_{n}^{\mathtt{d}})$,
and $\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}$ is the set of well-typed
maps from variables to values, i.e.,

$\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mathrel{:=}\\{m\in\left(\mathbb{B}^{*}\right)^{\mathsf{dom}(\Delta)}\mid\forall
r\in{\mathsf{dom}(\Delta)}.m(r)\in\llbracket\Delta(r)\rrbracket_{n}^{\mathtt{d}}\\}.$

######  Example 1.

If $\Delta=r:\mathsf{Str}[n],s:\mathsf{Str}[2n]$, then the semantics of
$\Delta$ is the set of all distribution ensembles
$\\{\mathcal{R}_{n}\\}_{n\in\mathbb{N}}$ such that, for each $n$,
$\mathcal{R}_{n}$ is a distribution in $\llbracket\Delta\rrbracket_{n}$. This
means that every member of this family $\mathcal{R}_{n}$ is a distribution of
functions $m:\\{r,s\\}\to{\mathbb{B}^{*}}$ such that $m(r)$ is a binary string
of length $n$ and $m(s)$ is a binary string of length $2n$. We also require
$\\{\mathcal{R}_{n}\\}_{n\in\mathbb{N}}$ to be _effectively samplable_ , so
there must be a polytime probabilistic algorithm that, on input $1^{n}$,
produces samples according to $\mathcal{R}_{n}$. ∎

In our logic, to state that some expression of type $\tau$ is pseudorandom, we
compare it against the family of uniform distributions of strings of that
type, and we impose that the advantage of any polytime distinguisher for the
two distributions is a negligible function (Definition 6). In turn, the
(effectively samplable) family of uniform distributions strings of a given
type $\tau$ is defined as follows:

$\displaystyle\mathsf{unif}(\mathsf{Bool})_{n}(b)$
$\displaystyle\mathrel{:=}\frac{1}{2}$ $\displaystyle\text{with
}b\in\mathbb{B}$ $\displaystyle\mathsf{unif}(\mathsf{Str}[p(n)])_{n}(x)$
$\displaystyle\mathrel{:=}{\frac{1}{2^{p(n)}}}$ $\displaystyle\text{with
}x\in\mathbb{B}^{p(n)}.$

####  3.1.3 Stores

Intuitively, stores can be defined just as elements of
$\llbracket\Delta\rrbracket$. But, since we want to reason about stores with
_different_ domains, we also make the domain $\Delta$ explicit in the notation
by defining _stores_ as pairs in the form ${(\mathcal{R})^{\Delta}}$ where
$\mathcal{R}\in\llbracket\Delta\rrbracket$. We write $\mathbf{0}$ for the
store ${(\\{\\{\varepsilon^{1}\\}\\}_{n\in\mathbb{N}})^{\varepsilon}}$ where
$\\{\varepsilon^{1}\\}$ is the distribution assigning probability $1$ to
$\varepsilon$, namely the only element of
$\llbracket\varepsilon\rrbracket_{n}$. The set $\mathcal{S}$ stands for the
set of all stores. In the following, we use metavariables like $s,r,t$ for
stores.

The partial order $\sqsubseteq$ can be lifted to distribution ensembles as
follows: we say that a probabilistic store $s={(\mathcal{R})^{\Delta}}$
extends a store $r={(\mathcal{Q})^{\Xi}}$, written $r\sqsubseteq s$, if and
only if $\Xi\sqsubseteq\Delta$ and $\mathcal{Q}$ can be obtained by computing
the marginal distribution of $\mathcal{R}$ on the domain of $\Xi$, itself
often indicated as $\mathcal{R}_{\Delta\to\Xi}$. In turn, the definition of
projection on distribution ensembles is lifted to stores by setting
$\left({(\mathcal{R})^{\Delta}}\right)_{\Delta\to\Xi}={(\mathcal{R}_{\Delta\to\Xi})^{\Xi}}$.

######  Definition 2 (Projection).

Given a store ${(\mathcal{R})^{\Delta}}$ and $\Xi$ such that
$\Xi\sqsubseteq\Delta$, we define the projection
$\left(\mathcal{R}\right)_{\Delta\to\Xi}\in\llbracket\Xi\rrbracket$, as
follows:

$\left(\mathcal{R}\right)_{\Delta\to\Xi}\mathrel{:=}\left\\{\text{bind}(\mathcal{R}_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Xi)})})\right\\}_{n\in\mathbb{N}}$

where for every set of random variables $\mathsf{S}$, $m_{\mathsf{S}}$ is the
function obtained by restricting the domain of $m$ to $\mathsf{S}$.

The relation $\sqsubseteq$ is widely employed in Section 4, because it allows
our logic to describe _local_ properties, i.e. properties that are valid in
_portions of stores_.

We can define the tensor product of two stores as follows:

######  Definition 3.

The pointwise tensor product of two distribution ensembles
${(\mathcal{R})^{\Delta}}$ and ${(\mathcal{Q})^{\Xi}}$ such that
$\mathsf{dom}(\Xi)\cap\mathsf{dom}(\Theta)=\emptyset$ is defined as a
distribution ensemble
${{(\mathcal{R})^{\Delta}}}\mathrel{\otimes}{{(\mathcal{Q})^{\Xi}}}$ in
$\llbracket\Delta\Join\Xi\rrbracket$, as follows:

$({{(\mathcal{R})^{\Delta}}}\mathrel{\otimes}{{(\mathcal{Q})^{\Xi}}})_{n}(m)\mathrel{:=}\mathcal{R}_{n}(m_{\mathsf{dom}(\Delta)})\cdot\mathcal{Q}_{n}(m_{\mathsf{dom}(\Xi)}).$

We write $s\otimes r\downarrow$ when the tensor product of two stores is
defined. ∎

###  3.2 Expressions

$\displaystyle\llparenthesis\Delta\vdash r:\tau\rrparenthesis_{n}(m)$
$\displaystyle\mathrel{:=}{m(r)}$ $\displaystyle\llparenthesis\Delta\vdash
f(d_{1},\ldots,d_{k}):\tau\rrparenthesis_{n}(m)$
$\displaystyle\mathrel{:=}\mathit{DetAlgoOf}(f)(1^{n})(\llparenthesis\Delta\vdash
d_{1}:\tau_{1}\rrparenthesis_{n}(m),\ldots,\llparenthesis\Delta\vdash
d_{k}:\tau_{k}\rrparenthesis_{n}(m))$ $\displaystyle\llbracket\Delta\vdash
d:\tau\rrbracket_{n}^{\mathtt{d}}(m)$
$\displaystyle\mathrel{:=}{\text{unit}(\llparenthesis\Delta\vdash
d:\tau\rrparenthesis_{n}(m))}$ $\displaystyle\llbracket\Delta\vdash
f(e_{1},\ldots,e_{k}):\tau\rrbracket_{n}^{\mathtt{d}}(m)$
$\displaystyle\mathrel{:=}\mathit{AlgoOf}(f){}(1^{n})^{\dagger}({\llbracket\Delta\vdash
e_{1}:\tau_{1}\rrbracket_{n}^{\mathtt{d}}(m)\mathrel{\otimes}\ldots\mathrel{\otimes}\llbracket\Delta\vdash
e_{k}:\tau_{k}\rrbracket_{n}^{\mathtt{d}}(m)})$
$\displaystyle\llbracket\Delta\vdash\mathtt{skip}\rrbracket_{n}$
$\displaystyle\mathrel{:=}\mathcal{D}\mapsto\mathcal{D}$
$\displaystyle\llbracket\Delta\vdash r\leftarrow e\rrbracket_{n}$
$\displaystyle\mathrel{:=}\mathcal{D}\mapsto\text{bind}(\mathcal{D},m\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto t])}))$
$\displaystyle\llbracket\Delta\vdash\mathtt{P};\mathtt{R}\rrbracket_{n}$
$\displaystyle\mathrel{:=}\mathcal{D}\mapsto\llbracket{\Delta\vdash\mathtt{R}}\rrbracket_{n}\left(\left(\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}\right)(\mathcal{D})\right)$
$\displaystyle\llbracket\Delta\vdash\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}$
$\displaystyle\mathrel{:=}\mathcal{D}\mapsto{\text{bind}\left(\mathcal{D},m\mapsto\begin{cases}\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=1\\\
\llbracket\Delta\vdash\mathtt{R}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=0\end{cases}\right)}$
Figure 1: Semantics of Expressions and Programs

Before introducing programs, we describe the _expressions_ that occur in them.
The set $\mathcal{F}$ of all _function symbols_ is assumed to be given, and
partitioned into two subsets $\mathcal{DF}$ and $\mathcal{RF}$, of
deterministic and randomized function symbols, respectively. The function
$\mathit{TypeOf}(\cdot)$ provides the type of every function symbol in
$\mathcal{F}$, i.e,

$\mathit{TypeOf}(f)=\tau_{1},\ldots,\tau_{k}\rightarrow\sigma.$

For every deterministic function symbol $f\in\mathcal{DF}$, such that
$\mathit{TypeOf}(f)=\tau_{1},\ldots,\tau_{k}\rightarrow\sigma$, we assume the
existence of a deterministic algorithm $\mathit{DetAlgoOf}(f)$ that, on input
$(1^{n},s)$ where
$s\in\llbracket\tau_{1}\rrbracket_{n}^{\mathtt{d}}\times\ldots\times\llbracket\tau_{k}\rrbracket_{n}^{\mathtt{d}}$,
returns a value $t\in\llbracket\sigma\rrbracket_{n}^{\mathtt{d}}$. In order
not to violate the time constraint, we assume that $\mathit{DetAlgoOf}(f)$ is
polytime in the size of its first argument for every $f\in\mathcal{DF}$.
Similarly, for every $f\in\mathcal{RF}$, we assume the existence of an
efficient _randomized_ algorithm $\mathit{AlgoOf}(f)$ that, on input
$(1^{n},s)$ where
$s\in\llbracket\tau_{1}\rrbracket_{n}^{\mathtt{d}}\times\ldots\times\llbracket\tau_{k}\rrbracket_{n}^{\mathtt{d}}$,
returns a distribution in $\llbracket\sigma\rrbracket_{n}$.

The following primitive operations, with self-explanatory behavior, will be
useful below:

$\displaystyle\begin{aligned}
\mathit{rnd}&:\varepsilon\rightarrow\mathsf{Str}[n]&\mathit{tail}_{p+1}&:\mathsf{Str}[p(n)+1]\rightarrow\mathsf{Str}[p(n)]\\\
\mathit{head}_{p}&:\mathsf{Str}[p(n)+1]\rightarrow\mathsf{Bool}&\mathit{xor}&:\mathsf{Str}[n]\times\mathsf{Str}[n]\rightarrow\mathsf{Str}[n]\\\
\end{aligned}$
$\displaystyle\mathit{concat}_{p,q}:\mathsf{Str}[p(n)]\times\mathsf{Str}[q(n)]\rightarrow\mathsf{Str}[p(n)+q(n)]$
$\displaystyle\mathit{setzero}_{p}:\varepsilon\rightarrow\mathsf{Str}[p(n)]$

The only randomized primitive operation among these is $\mathit{rnd}$, which
simply returns $n$ independently and uniformly distributed random bits.
Noticed that these functions may be indexed by some polynomials that describe
the size of their arguments. We omit these annotations, when the sizes of the
arguments are evident from the context.

_Deterministic and random expressions_ are defined through the following
grammars:

$\displaystyle d$
$\displaystyle::=r\;\mbox{\Large{$\mid$}}\;g(d_{1},\ldots,d_{k})$
$\displaystyle e$
$\displaystyle::=d\;\mbox{\Large{$\mid$}}\;f(e_{1},\ldots,e_{k})$

where $r\in\mathcal{V},g\in\mathcal{DF},f\in\mathcal{RF}$. A simple type
system with judgments in the form $\Delta\vdash e:\tau$ can be given as
follows:

$\displaystyle\Delta\vdash r:\tau\Delta(r)=\tau\quad\Delta\vdash
f(e_{1},\ldots,e_{k}):\sigma\mathit{TypeOf}(f)=\tau_{1},\ldots,\tau_{k}\rightarrow\sigma\left\\{\Delta\vdash
e_{i}:\tau_{i}\right\\}_{1\leq i\leq k}$

We write $\mathsf{FV}(e)$ for the set of free variables of $e$. One can define
the semantics of typed expressions in a standard way, as formalized in the
following definition.

######  Definition 4 (Semantics of Expressions).

The semantics of a _deterministic expression_ $d$ is a family of functions
$\\{\llparenthesis\Delta\vdash d:\tau\rrparenthesis_{n}\\}_{n\in\mathbb{N}}$
such that for every $n\in\mathbb{N}$, we have $\llparenthesis\Delta\vdash
d:\tau\rrparenthesis_{n}:\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\to\llbracket\tau\rrbracket_{n}^{\mathtt{d}}$.
The _pre-semantics_ of a general expression $\Delta\vdash e:\tau$, is a family
$\left\\{\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}\right\\}_{n\in\mathbb{N}}$ where for every
$n\in\mathbb{N}$, $\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}:{\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}}\to{\llbracket\tau\rrbracket_{n}}$,
see Figure 1. The semantics of a randomized expression $e$, indicated as
$\llbracket\Delta\vdash e:\tau\rrbracket$, is the family of functions
$\llbracket\Delta\vdash
e:\tau\rrbracket_{n}:\llbracket\Delta\rrbracket_{n}\to{\llbracket\tau\rrbracket_{n}}$,
indexed by $n\in\mathbb{N}$, where every $n\in\mathbb{N}$,
$\llbracket\Delta\vdash e:\tau\rrbracket_{n}$ is the Kleisli extension of
$\llbracket\Delta\vdash e:\tau\rrbracket_{n}^{\mathtt{d}}$. ∎

###  3.3 Programs

We work within a probabilistic imperative language without iteration. (We
discuss in Section 8 below why dealing with loops is nontrivial.)

_Programs_ are defined by the following grammar:

$\displaystyle\mathtt{P},\mathtt{R}::=\;\mathtt{skip}\;\mbox{\Large{$\mid$}}\;r\leftarrow
e\;\mbox{\Large{$\mid$}}\;\mathtt{P};\mathtt{P}\;\mbox{\Large{$\mid$}}\;\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{P}$

A type system with judgments in the form $\Delta\vdash\mathtt{P}$ for the just
defined programs can be given in a standard way. Programs can be endowed with
a denotational semantics.

######  Definition 5.

Whenever $\Delta\vdash\mathtt{P}$, the semantics of $\mathtt{P}$ is the family
$\left\\{\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}\right\\}_{n\in\mathbb{N}}$,
where for every $n\in\mathbb{N}$,
$\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}:\llbracket\Delta\rrbracket_{n}\to\llbracket\Delta\rrbracket_{n}$
as in Figure 1. This function induces an endofunction on
$\llbracket\Delta\rrbracket$, which we indicate as
$\llbracket\Delta\vdash\mathtt{P}\rrbracket$ and which is defined as
$\left(\llbracket\Delta\vdash\mathtt{P}\rrbracket(\mathcal{R})\right)_{n}\mathrel{:=}\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n})$.
Very often, $\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}$ (resp.
$\llbracket\Delta\vdash\mathtt{P}\rrbracket$) will be abbreviated just as
$\llbracket\mathtt{P}\rrbracket_{n}$ (resp. $\llbracket\mathtt{P}\rrbracket$).
∎

The interpretations of $\mathtt{skip}$ and of the composition
$\mathtt{P}\mathtt{R};$ are trivial. The interpretation of assignments is
similar to that of sampling statements in [17]; it composes the initial
distribution with the continuation that associates every $m$ in the support of
the initial distribution with the store that is obtained by evaluating $e$ on
$m$ and updating the value of $r$ in $m$ accordingly. Finally, the
interpretation of the conditional constructs composes the distribution with
the function that, given an element of its support, executes $\mathtt{P}$ on
it if this program satisfies the guard, and executes $\mathtt{R}$ otherwise.
Overall, the definition of our semantics is close to that of Kozen [23], but
that the semantics of the conditional construct is not given in terms of
conditional distributions. This is due to the need of having an endofunction
on _efficiently samplable_ distribution ensembles as the semantics of our
language. Specifically, we cannot use conditioned distributions because, given
a polytime sampler for the initial distribution ensemble $\mathcal{R}$, we may
not be able to identify a polytime sampler for the distribution ensemble
obtained by conditioning $\mathcal{R}$ on the value of the guard. For
instance, although a construction based on rejection sampling would produce
the desired output distribution, it would not be _polytime_ in general. In
Section 3.5.1 below, we show that the two definitions are equivalent when
evaluated _on distributions_.

Notice that, by construction, for every program $\mathtt{P}$,
$\llbracket\mathtt{P}\rrbracket$ can be seen as a family of circuits, and for
every $n\in\mathbb{N}$, the circuit $\llbracket{\mathtt{P}}\rrbracket_{n}$ has
polynomial size in $n$.

###  3.4 Notions from Computational Cryptography

One of our main goals is to provide a formal framework for reasoning about
definitions and constructions in complexity-based cryptography, in this work
we follow a standard approach (e.g., as presented in [20] or [19]). A
fundamental characteristic of this setting is that all parties, both honest
and adversarial, are modeled as efficient (randomized) agents, in particular
as _probabilistic polynomial time_ (PPT) algorithms. This framework underlies
the notion of samplablability given in Definition 1, as such distributions are
exactly those sampled by some PPT algorithm.

While it is well-known that under reasonable restrictions (e.g., on the length
of keys) it is impossible to provide absolute guarantees against adversarial
success, definitions of security in the computational setting require
_negligible_ adversarial advantage, where negligibilty is measured as a
function of a _security parameter_ $n\in\mathbb{N}$. This value measures the
size of the secret information used by honest parties (e.g. the length of a
secret key). In keeping with the asymptotic complexity bounds on adversaries,
this leads to the following:

######  Definition 6.

A function $\nu:\mathbb{N}\to\mathbb{N}$ is negligible if for any
$k\in\mathbb{N}$, for sufficiently large $n$, $\nu(n)\leq 1/n^{k}$. ∎

A fundamental concept in cryptography is a binary relation on distribution
ensembles called computational indistinguishability, by which we mean that no
probabilistic polynomial time algorithm can distinguish between the two
ensembles with non-negligible probability of success. Here, we can introduce
computational indistinguishability as a relation on stores:

######  Definition 7.

We say that two distribution ensembles
$\\{\mathcal{R}_{n}\\}_{n\in\mathbb{N}},\\{\mathcal{Q}_{n}\\}_{n\in\mathbb{N}}\in\llbracket\Delta\rrbracket$
(resp. in $\llbracket\tau\rrbracket$) are indistinguishable, and we write
$\\{\mathcal{R}_{n}\\}_{n}\approx\\{\mathcal{Q}_{n}\\}_{n}$, if and only if
for every probabilistic polynomial time algorithm ${\mathcal{A}}$, there is a
negligible function ${\mathit{negl}}:\mathbb{N}\to\mathbb{N}$ such that for
every $n\in\mathbb{N}$:

$\left|{\text{Pr}_{x\leftarrow\mathcal{R}_{n}}}\left[{\mathcal{A}}(1^{n},x)=1\right]-{\text{Pr}_{x\leftarrow\mathcal{Q}_{n}}}\left[{\mathcal{A}}(1^{n},x)=1\right]\right|\leq{\mathit{negl}}(n).$

With this definition at hand, we are able to define a central notion in
complexity-based cryptography: _pseudorandomness_. Let
$\\{\mathcal{U}_{n}\\}_{n\in\mathbb{N}}$ denote the distribution ensemble
where $\mathcal{U}_{n}$ is the uniform distribution on $\mathbb{B}^{n}$.

######  Definition 8.

A distribution ensemble $\\{\mathcal{R}_{n}\\}_{n\in\mathbb{N}}$ is
pseudorandom if $\\{\mathcal{R}_{n}\\}_{n}\approx\\{\mathcal{U}_{n}\\}_{n}$. A
(deterministic) poly-time function $f:\mathbb{B}^{*}\to\mathbb{B}^{*}$ is a
pseudorandom generator if there is a function $\ell:\mathbb{N}\to\mathbb{N}$
with $\ell(n)>n$ such that for $x\in\mathbb{B}^{n}$,
$f(x)\in\mathbb{B}^{\ell(n)}$ and
$\\{f(\mathcal{U}_{n})\\}_{n}\approx\\{\mathcal{U}_{\ell(n)}\\}_{n}$. ∎

Thus, a distribution ensemble is pseudorandom if no PPT algorithm can
distinguish between samples from the distribution and samples from a truly
random distribution.

A more detailed discussion of complexity-based cryptography is given in
Section 7.

###  3.5 Semantic Properties of Programs

This section is devoted to showing some remarkable properties of our programs’
semantics. We start by showing that it is equivalent to the one proposed by
Kozen [23].

In Sections 3.5.2 and 3.5.3, we show some other general properties of the
expression of expressions and programs, notably these include Lemmas 5 and 6,
stating that the outcome of the evaluation of expressions and programs does
not depend on those variables that do not appear in the program, and Lemmas 10
and 2, where we show that the distribution ensemble that is obtained by
evaluating the same program (resp. expression) on two computationally
indistinguishable ensembles are themselves computationally indistinguishable.

####  3.5.1 Equivalence with Kozen’s Semantics

In this subsection, we are interested in showing that our semantics is
equivalent to that by Kozen [23]. A subtle difference within these two
semantics is that, while that by Kozen is defined on _ordinary_ distributions,
ours is defined on efficiently samplable distributions. This means that, with
our semantics, if we take an efficiently samplable distribution, and we
compute the semantics of a program on it, we obtain another efficiently
samplable distribution. In contrast to our semantics, Kozen’s one is defined
on _ordinary_ distributions, so it does not provide any guarantee on the
existence of such a sampler. However, the equivalence between these two
semantics _seen on regular distributions_ has as a consequence that the
loopless fragment of Kozen’s language (and semantics) transforms efficiently
samplable distributions in other efficiently samplable distributions. This
result is not trivial because, on conditional statements, Kozen’s semantic of
the $\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$
computes the conditioned distributions of $s$ on the $r=1$ and $r=0$ obtaining
two states $s_{1}$ and $s_{0}$, Finally, it outputs the convex combination of
$\llbracket\mathtt{P}\rrbracket({s_{1}}){}$ and
$\llbracket\mathtt{P}\rrbracket({s_{0}}){}$ according to $\llbracket
r\rrbracket({s}){}$. In particular, as far as we know, it is not known whether
efficiently samplable distributions are closed under conditioning.

The first step we do in order to establish this claim, is to define the
conditioning operation: given a distribution ensemble
$\mathcal{R}\in\llbracket\Delta\rrbracket$, we write
${{\mathcal{R}_{n}}_{{}|r=b}}$ for the distribution that is obtained by
conditioning $\mathcal{R}_{n}$ on the event $m(r)=\mathsf{Bool}$. Formally,
this distribution is defined as follows:

${{\mathcal{R}_{n}}_{{}|r=b}}(m)\mathrel{:=}\begin{cases}\frac{{\mathcal{R}_{n}}(m)}{{\mathcal{R}_{n}}(S)}&\text{if
}m(r)=b\text{ and }S=\\{m\in{\mathsf{supp}}(\mathcal{R}_{n})\mid
m(r)=b\\}\neq\emptyset\\\ 0&\text{otherwise.}\end{cases}$

Finally, we define the convex combination of two distributions
$\mathcal{D},\mathcal{E}\in\mathbb{D}(X)$ for $n\in\mathbb{N}$ as follows:

$\left(\mathcal{D}\mathrel{\oplus_{d}}\mathcal{E}\right)(\vec{z})\mathrel{:=}d(1)\cdot\mathcal{D}(x)+d(0)\cdot\mathcal{E}(x).$

######  Definition 9.

The Kozen-style definition of the semantics of loopless program
($\llbracket\cdot\rrbracket^{\mathtt{K}}_{\cdot}$) is defined identically to
that ofFigure 1, except for
$\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$, which
is defined as follows:

$\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket^{\mathtt{K}}_{n}\mathrel{:=}\begin{cases}\llbracket\mathtt{P}\rrbracket^{\mathtt{K}}_{n}(\mathcal{R}_{n})&\text{if
}\llbracket r\rrbracket_{n}(\mathcal{R}_{n})(1)=1\\\
\llbracket\mathtt{R}\rrbracket^{\mathtt{K}}_{n}(\mathcal{R}_{n})&\text{if
}\llbracket r\rrbracket_{n}(\mathcal{R}_{n})(1)=0\\\
\llbracket\mathtt{P}\rrbracket^{\mathtt{K}}_{n}({{\mathcal{R}_{n}}_{{}|r=1}})\mathrel{\oplus_{\llbracket
r\rrbracket_{n}(\mathcal{R}_{n})}}\llbracket\mathtt{R}\rrbracket^{\mathtt{K}}_{n}({{\mathcal{R}_{n}}_{{}|r=0}})&\text{otherwise.}\end{cases}$

In order to show the equivalence we are aiming to, we also need to introduce
some results on measures: given two measures $\mu,\nu$, we write $\mu+\nu$ as
a shorthand for $x\mapsto\mu(x)+\nu(x)$, and for every $k\in[0,1]$, we write
$k\cdot\mu$ for $x\mapsto k\cdot\mu(n,x)$. By considering the extension of our
program’s semantics to measures, we obtain the following result:

######  Remark 1.

Let $\mathtt{P}$ be a program, and $n$ a natural number. It holds that:

  * •

$\llbracket\mathtt{P}\rrbracket(\mu+\nu)=\llbracket\mathtt{P}\rrbracket(\mu)+\llbracket\mathtt{P}\rrbracket(\nu)$

  * •

$\forall 0\leq k\leq
1.\llbracket\mathtt{P}\rrbracket(k\cdot\mu)=k\cdot\llbracket\mathtt{P}\rrbracket(\mu)$

###### Proof.

By induction on $\mathtt{P}$. ∎

Leveraging this Remark, it is possible to show the main result of this
section, the following lemma:

######  Lemma 1.

The semantics of programs, seen as in Definition 5, if interpreted on
_ordinary_ distributions, is equivalent to that by Kozen, [23].

###### Proof.

We go by induction on $\mathtt{P}$. Whenever $\mathtt{P}$ is not a
conditional, the conclusion is trivial because the two semantics are identical
by definition. For this reason, we take in exam only the case where the
program is
$\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$. We
first assume that the guard is identically 1 or 0. In those cases ewe are
required to verify that:

${\text{bind}\left(\mathcal{R}_{n},m\mapsto\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=1\\\ \llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=0\end{cases}\right)}$

Is equal to $\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n})$ or
respectively to $\llbracket\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n})$ we
assume without lack of generality that the distribution of the guard is
identically 1. In this case we are asked to show that:

$\text{bind}(\mathcal{R}_{n},m\mapsto\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)}))=\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n}).$

A formal proof of this result is in Lemma 12 below; notice that the proof of
that lemma does not rely on this lemma.

Now, we assume that the guard is not identically 1 or 0. In this case, the
claim is: $\forall\Delta.\forall
n\in\mathbb{N}.\forall\mathcal{R}_{n}\in\llbracket\Delta\rrbracket_{n}.\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n})=\llbracket\mathtt{P}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=1}})\mathrel{\oplus_{\llbracket
r\rrbracket_{n}(\mathcal{R}_{n})}}\llbracket\mathtt{R}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=0}})$.
We start by fixing $n\in\mathbb{N}$ and
$m\in{\mathsf{supp}}(\mathcal{R}_{n})$, and we observe that, by expanding the
definition of the semantics, we obtain that
$\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket(\mathcal{R})(n,m)$
is equal to:

$\displaystyle\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=1}^{}}\;\;{\mathcal{R}(n,l)}\cdot\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)})(m)+\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=0}^{}}\;\;{\mathcal{R}(n,l)}\cdot\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l)})(m)$

On the other hand, we can expand the definition of

$\left(\llbracket\mathtt{P}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=1}})\mathrel{\oplus_{\llbracket
r\rrbracket_{n}(\mathcal{R}_{n})}}\llbracket\mathtt{R}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=0}})\right)(m)$

as follows:

$\displaystyle\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=1}^{}}\;\;\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{P}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=1}})(m)+\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=0}^{}}\;\;\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{R}\rrbracket_{n}({{\mathcal{R}_{n}}_{{}|r=0}})(m)$

Now, we can simply show that for every program $\mathtt{P}$ and Boolean $b$:

$\displaystyle\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}^{}}\;\;\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)})(m)=\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}^{}}\;\;\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{P}\rrbracket_{n}({s_{{}|r=b}}(n))(m)$
($*$)

We start by simplifying the expression on the right. First, we observe that,
for Remark 1, ${{\mathcal{R}_{n}}_{{}|r=b}}(m)$ is equal to:

$\frac{1}{\sum_{w:w\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
w(r)=b}\mathcal{R}_{n}(w)}\cdot\begin{cases}{\mathcal{R}_{n}(m)}&\text{if
}m(r)=b\\\ 0&\text{otherwise}\end{cases}$

Let $k_{b}\in[0,1]$ and $\mathcal{T}_{b}$ be defined as follows:

$k_{b}\mathrel{:=}\frac{1}{\sum_{w:w\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
w(r)=b}\mathcal{R}_{n}(w)}\quad\quad\quad\mathcal{T}_{b}(m)\mathrel{:=}\begin{cases}{\mathcal{R}_{n}(m)}&\text{if
}m(r)=b\\\ 0&\text{otherwise.}\end{cases}$

With these definitions, the expression we were reducing can be rewritten as

$\ldots=\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{P}\rrbracket_{n}(k_{b}\cdot\mathcal{T}_{b})(m)\\\
$

from the observation above and Remark 1, we obtain

$\displaystyle\ldots=\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}\mathcal{R}_{n}(l)\cdot
k_{b}\cdot\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{T}_{b})(m)=\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{T}_{b})(m),$

from the definition of $k_{b}$. We call $\mathcal{Q}^{m}$ the distribution
ensemble defined as follows:

$\mathcal{Q}^{m}_{n}(w)\mathrel{:=}\begin{cases}\mathcal{R}_{n}({m})&\text{if
}m=w\\\ 0&\text{otherwise}\end{cases}$

Observe that:

$\mathcal{T}_{b}(w)=\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}^{}}\;\;\mathcal{Q}^{l}_{n}(w),$

so we can continue the reduction of the term observing that:

$\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{T}_{b})=\llbracket\mathtt{P}\rrbracket_{n}\left(\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}\mathcal{Q}^{l}_{n}\right)$

With an application of Remark 1 we can state the following equivalence:

$\displaystyle\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{T}_{b})=\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}^{}}\;\;\llbracket\mathtt{P}\rrbracket_{n}\left(\mathcal{Q}^{l}_{n}\right),$

finally, we observe that
$\mathcal{Q}^{l}_{n}(m)=\mathcal{R}_{n}(m)\cdot{\text{unit}(l)}(m)$ so, we
have:

$\displaystyle\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{T}_{b})=\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\land
l(r)=b}^{}}\;\;\llbracket\mathtt{P}\rrbracket_{n}\left(\mathcal{Q}^{l}_{n}\right)=\smashoperator[r]{\sum_{l:l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}};\land
l(r)=b}^{}}\;\;\llbracket\mathtt{P}\rrbracket_{n}\left(m\mapsto\mathcal{R}_{n}(m)\cdot{\text{unit}(l)}(m)\right).$

So, in order to show our claim, it suffices to observe that for every
$l\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}$ such that $l(r)=b$, we have:

$\llbracket\mathtt{P}\rrbracket_{n}\left(m\mapsto\mathcal{R}_{n}(m)\cdot{\text{unit}(l)}(m)\right)=\mathcal{R}_{n}(l)\cdot\llbracket\mathtt{P}\rrbracket_{n}\left({\text{unit}(l)}\right).$

But this is a consequence of
$m\mapsto\mathcal{R}_{n}(m)\cdot{\text{unit}(l)}(m)=m\mapsto\mathcal{R}_{n}(l)\cdot{\text{unit}(l)}(m)$
and of 1. ∎

####  3.5.2 Properties of Expressions

We start by showing that if $s\approx r$, then $\llbracket
e\rrbracket(s)\approx\llbracket e\rrbracket(r)$ (Lemma 2) and that, if
$s\sqsubseteq r$ then $\llbracket e\rrbracket(s)=\llbracket e\rrbracket(r)$
(Lemma 5). These properties in turn, are useful later to show that the
semantic of specific CSL’s formulas is closed with respect to
$\approx\sqsubseteq$ (Lemma 24). Leveraging this result, we show that our
model also enjoys a form Restriction Property (1), and that some standard
axiom schema for atomic formulas hold, Lemma 25.

######  Lemma 2 (Indistinguishability of Expressions’ Semantic).

For every expression $e$, and every pair of stores
${{(\mathcal{R})^{\Delta}}}\approx{{(\mathcal{Q})^{\Xi}}}$ such that
$\Delta\vdash e:\tau,\Xi\vdash e:\tau$ it holds that $\llbracket
e\rrbracket(\mathcal{R})\approx\llbracket e\rrbracket(\mathcal{Q})$.

###### Proof.

Assume the claim not to hold, this means that there is an adversary
${\mathcal{A}}$ which is capable to distinguish $\llbracket
e\rrbracket(\mathcal{R})$ and $\llbracket e\rrbracket(\mathcal{R})$ with non-
negligible advantage. This adversary can be used to define an adversary
${\mathcal{B}}$ with the same advantage on $\mathcal{R}$ and $\mathcal{Q}$. On
input $(1^{n},m)$, it samples from $\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m)$ and then executes ${\mathcal{A}}$ on this
sample. The advantage of ${\mathcal{B}}$ on $\Delta,\Xi$ is the same of
${\mathcal{A}}$ on $\llbracket e\rrbracket_{n}(\mathcal{R})$ and $\llbracket
e\rrbracket_{n}(\mathcal{Q})$. Notice that since $e$ is polytime computable,
${\mathcal{B}}$ is also polytime. ∎

Then, we show that evaluation expression $e$ such that $\Delta\vdash e:\tau$
in a state ${(\mathcal{R})^{\Delta}}$ yields the same result of evaluating it
in a state $({(\mathcal{R})^{\Delta}})_{\Delta\to\Xi}$ if $g\vdash e:\tau$.

######  Lemma 3.

For every deterministic expression $d$ each pair of environments
$\Delta\sqsubseteq\Xi$ such that $\Delta\vdash d:\tau$ and $\Xi\vdash d:\tau$,
every $n\in\mathbb{N}$ and every tuple
$m\in{\mathsf{supp}}(\llbracket\Xi\rrbracket_{n})$, it holds that
$\llparenthesis\Xi\vdash
d:\tau\rrparenthesis_{n}(m)=\llparenthesis\Delta\vdash
d:\tau\rrparenthesis_{n}(m_{\mathsf{dom}(\Delta)})$.

###### Proof.

The proof is by induction on the syntax of $d$

  * •

If $d$ is $r$, we observe that for every $n\in\mathbb{N}$,

$\displaystyle\llparenthesis\Delta\vdash
e:\tau\rrparenthesis_{n}(m_{\mathsf{dom}(\Delta)})$
$\displaystyle=(m_{\mathsf{dom}(\Delta)})(r)=m(r)$

because $r$ in $\mathsf{dom}(\Delta)$ from the assumption $\Delta\vdash
e:\tau$.

  * •

If $d$ is a complex expression, the claim is a consequence of the IHs.

∎

######  Lemma 4.

For every expression $e$ each pair of environments $\Delta\sqsubseteq\Xi$ such
that $\Delta\vdash e:\tau$ and $\Xi\vdash e:\tau$, and every tuple
$m\in{\mathsf{supp}}(\llbracket\Xi\rrbracket_{n})$, it holds that
$\llbracket\Xi\vdash e:\tau\rrbracket^{\mathtt{d}}(m)=\llbracket\Delta\vdash
e:\tau\rrbracket^{\mathtt{d}}(m_{\mathsf{dom}(\Delta)})$.

###### Proof.

The proof is by induction on the syntax of $e$

  * •

If $e$ is a deterministic expression, we observe that for every
$n\in\mathbb{N}$,

$\displaystyle\llbracket\Delta\vdash
d:\tau\rrbracket_{n}^{\mathtt{d}}(m_{\mathsf{dom}(\Delta)})$
$\displaystyle={\text{unit}(\llparenthesis\Delta\vdash
d:\tau\rrparenthesis_{n}(m_{\mathsf{dom}(\Delta)}))}$
$\displaystyle={\text{unit}(\llparenthesis\Xi\vdash
d:\tau\rrparenthesis_{n}(m))}.$

  * •

If $e$ is a complex expression, the claim is a consequence of the IHs.

∎

######  Lemma 5 (Expressions’ Semantic on projection).

For every expression $e$ such that $\Delta\vdash e:\tau$ and $\Xi\vdash
e:\tau$, and every store $\mathcal{R}\in\llbracket\Delta\rrbracket$,
$\llbracket e\rrbracket(\mathcal{R}_{\Delta\to\Xi})=\llbracket
e\rrbracket(\mathcal{R})$.

###### Proof.

We start by expanding the definition of $\llbracket
e\rrbracket_{n}(\mathcal{R}_{\Delta\to\Xi})$ for some
$t\in\llbracket\tau\rrbracket_{n}$:

$\displaystyle\ldots$
$\displaystyle=\text{bind}(\text{bind}(\mathcal{R}_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Xi)})}),\vec{y}\mapsto\llbracket
e\rrbracket_{n}^{\mathtt{d}}(\vec{y}))$
$\displaystyle=\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}({\text{unit}(m_{\mathsf{dom}(\Xi)})},\vec{y}\mapsto\llbracket
e\rrbracket_{n}^{\mathtt{d}}(\vec{y})))$
$\displaystyle=\text{bind}(\mathcal{R}_{n},m\mapsto{\llbracket
e\rrbracket_{n}^{\mathtt{d}}({m_{\mathsf{dom}(\Xi)}})})$

It holds that $\llbracket
e\rrbracket_{n}^{\mathtt{d}}({m_{\mathsf{dom}(\Xi)}})=\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m)$ for Lemma 4, so we can conclude the proof. ∎

We conclude this section by showing a technical result that is employed in the
proof of soundness of the rules

######  Remark 2.

For every $n\in\mathbb{N}$, deterministic expression $d$, every $\Delta$ such
that $\Delta\vdash d:\tau$, and every $r\in\mathsf{dom}(\Delta)$ such that
$r\notin\mathsf{FV}(d)$, every
$m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}$, and every
$t\in\llbracket\tau\rrbracket_{n}^{\mathtt{d}}$, we have that $\llparenthesis
d\rrparenthesis_{n}(m)=\llparenthesis d\rrparenthesis_{n}(m[r\mapsto t])$.

###### Proof.

We start by fixing $n\in\mathbb{N}$. The proof is by induction on $d$. If it
is a variable, we are sure that it must be different from $r$, so the
conclusion is trivial. In the inductive case, the conclusion is a direct
consequence of the IHs on the sub-expressions. ∎

####  3.5.3 Semantic Properties of Programs

In this section, we show some remarkable properties of our programs’
semantics. We start with Lemma 6, where we show that the semantic of a program
depends only on those variables that are used to type that program. In Lemmas
7 and 8, we show the soundness of the function $\mathsf{MV}(\cdot)$: in
particular, we show that the program variables that do not belong to
$\mathsf{MV}(\cdot)$ are not affected by the evaluation of $\mathtt{P}$.
Another result with the same spirit is Lemma 9, where we show that if a
program $\mathtt{P}$ is evaluated on the tensor product of two distribution
ensembles $\mathcal{R}$ and $\mathcal{Q}$, and the domain on one of them
contains only variables that $\mathtt{P}$ does not use, then in the resulting
distribution ensemble, these variables are still independent from the others.

Lemma 10 states that by evaluating the same program on two computationally
indistinguishable stores, we obtain two computationally indistinguishable
outputs. Crucially, it is possible to show this result because our programs
are polytime.

In Lemma 11, we show that after an assignment of an expression to a variable
$r$ , such that $r\notin\mathsf{FV}(e)$ the values obtained by evaluating $r$
and $e$ are the same. Lemmas 12, 13 and 14 are devoted to show a similar
claim, but for deterministic expressions. These results and Lemma 15 are
employed in the proof of soundness of the rules for assignments in Section 5.

######  Lemma 6.

For every program $\mathtt{P}$, and every store ${{(\mathcal{R})^{\Delta}}}$
such that $\Xi\sqsubseteq\Delta$, $\Xi\vdash\mathtt{P}$, it holds that
$\llbracket\mathtt{P}\rrbracket(\mathcal{R}_{\Delta\to\Xi})=\llbracket\mathtt{P}\rrbracket(\mathcal{R})_{\Delta\to\Xi}$.

###### Proof.

The proof goes by induction on the program.

  * •

If $\mathtt{P}=\mathtt{skip}$, the conclusion is trivial.

  * •

If $\mathtt{P}=r\leftarrow e$, observe that:

$\displaystyle(\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}))_{\Delta\to\Xi}$
$\displaystyle=\text{bind}(\llbracket r\leftarrow
e\rrbracket_{n}(\mathcal{R}),m\mapsto m_{\mathsf{dom}(\Xi)}).$

By expanding the definition of the semantics and applying some monadic laws,
it is possible to deduce that it is equal to:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket\Delta\vdash
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}({m[r\mapsto
t]}_{\mathsf{dom}(\Xi)})})),$

on the other hand, with similar expansions, we obtain that
$(\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{\Delta\to\Xi}))$ is equal
to:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket\Xi\vdash
e\rrbracket_{n}^{\mathtt{d}}(m_{\mathsf{dom}(\Xi)}),t\mapsto{\text{unit}({m_{\mathsf{dom}(\Xi)}[r\mapsto
t]})})),$

and with an application of Lemma 4, we observe that, this is equal to:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket\Delta\vdash
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}({m_{\mathsf{dom}(\Xi)}[r\mapsto
t]})})).$

By observing $\Xi\vdash\mathtt{P}$, we obtain that $r\in\mathsf{dom}(\Xi)$,
which is enough to state the equivalence.

  * •

The case of composition is a trivial consequence of the IH.

  * •

If $\mathtt{P}$ is a conditional we are required to show that:

$\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket(\mathcal{R})_{\Delta\to\Xi}=\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket(\mathcal{R}_{\Delta\to\Xi})$

The term on the right can be reduced as follows:

$\text{bind}(\text{bind}(\mathcal{R}_{n},m\mapsto
h(m)),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})})$

where

$h(m)=\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=1\\\ \llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=0\end{cases}$

which is equal to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(h(m),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})}))$

and, by definition of projection, to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto h(m)_{\Delta\to\Xi}).$

As we did of assignments, we can conclude the proof by assessing that the term
above is equal to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto h(m_{\mathsf{dom}(\Xi)}))$
($*$)

Observe that:

$h(m_{\mathsf{dom}(\Xi)})=\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)}_{\Delta\to\Xi})&\text{if
}m(r)=1\\\
\llbracket\mathtt{R}\rrbracket_{n}({{\text{unit}(m)}_{\Delta\to\Xi}})&\text{if
}m(r)=0\end{cases}$

We continue by proceed applying the IHs, to conclude that ($*$) is equal to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto h(m)_{\Delta\to\Xi}).$

∎

######  Lemma 7.

$\forall\Delta.\forall\Xi\sqsubseteq\Delta.\Delta\vdash r\leftarrow
e\Rightarrow
r\notin\mathsf{dom}(\Xi)\Rightarrow\forall\mathcal{R}\in\llbracket\Delta\rrbracket.{{{(\mathcal{R})^{\Delta}}}}_{\Delta\to\Xi}=({\llbracket
r\leftarrow e\rrbracket{{(\mathcal{R})^{\Delta}}}})_{\Delta\to\Xi}.$

###### Proof.

Observe that:

$\displaystyle(\llbracket r\leftarrow
e\rrbracket_{n}(\mathcal{R}))_{\Delta\to\Xi}$
$\displaystyle=\text{bind}(\llbracket r\leftarrow
e\rrbracket(\mathcal{R}),m\mapsto{\text{unit}(m_{\mathsf{dom}(\Xi)})}).$

By expanding the definition of the semantics and applying standard monads’
properties, it is possible to deduce that it is equal to:

$\text{bind}(\mathcal{R}(n),m\mapsto\text{bind}(\llbracket
e\rrbracket^{\mathtt{d}}(n,m),t\mapsto{\text{unit}({{m[r\mapsto
t]}_{\mathsf{dom}(\Xi)}})})),$

which, in turn, is equal to:

$\text{bind}(\mathcal{R}(n),m\mapsto\text{bind}(\llbracket
e\rrbracket^{\mathtt{d}}(n,m),t\mapsto{\text{unit}({m}_{\mathsf{dom}(\Xi)})}))$

for the assumption on $r$. It is easy to verify that, since
${t\mapsto{\text{unit}({m}_{\mathsf{dom}(\Xi)})}}$ is a constant function, the
expression above is equal to:

$\text{bind}(\mathcal{R}(n),m\mapsto{\text{unit}(m_{\mathsf{dom}(\Xi)})}).$

∎

######  Lemma 8 (Modified Variables and Projection).

It holds that:

$\forall\mathtt{P},\Delta.\forall\Xi\sqsubseteq\Delta.\Delta\vdash\mathtt{P}\Rightarrow\mathsf{dom}(\Xi)\cap\mathsf{MV}(\mathtt{P})=\emptyset\Rightarrow\forall\mathcal{R}\in\llbracket\Delta\rrbracket_{.}{{{(\mathcal{R})^{\Delta}}}}_{\Delta\to\Xi}={\llbracket\mathtt{P}\rrbracket({{(\mathcal{R})^{\Delta}}})}_{\Delta\to\Xi}.$

###### Proof.

This proof is by induction on $\mathtt{P}$.

  * •

If $\mathtt{P}$ is $\mathtt{skip}$, then the premise coincides with the
conclusion.

  * •

If $\mathtt{P}$ is $\mathtt{P};\mathtt{R}$, then the claim comes from the
application of the IH on $\mathtt{P}$ and of that on $\mathtt{R}$.

  * •

If the program is
$\mathtt{if}\;e\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$, we
start by expanding
$\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}(\mathcal{R})_{\Delta\to\Xi}$
as follows:

$\text{bind}(\text{bind}(\mathcal{R}_{n},m\mapsto
h(m)),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})})$

where

$h(m)=\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=1\\\ \llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=0\end{cases}$

which is equal to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(h(m),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})}))$

Now, it is possible to observe that
$\text{bind}(h(m),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})})$ is equal to:

$\begin{cases}\text{bind}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)}),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})})&\text{if
}m(r)=1\\\
\text{bind}(\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)}),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Xi)})})&\text{if
}m(r)=0,\end{cases}$

which in turn is equal to

$\begin{cases}{\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)})}_{\Delta\to\Xi}&\text{if
}m(r)=1\\\
{\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)})}_{\Delta\to\Xi}&\text{if
}m(r)=0.\end{cases}$

The conclusion follows from the IHs.

  * •

$\mathtt{P}$ is $r\leftarrow e$, the claim is a consequence of Lemma 7.

∎

######  Lemma 9.

For every program $\mathtt{P}$, and every pair of stores
$s={{(\mathcal{R})^{\Delta}}}$, $r={{(\mathcal{Q})^{\Xi}}}$ such that
$\Delta\vdash\mathtt{P}$ and $s\otimes r\downarrow$, it holds that
$\llbracket\mathtt{P}\rrbracket(s\otimes
r)=\llbracket\mathtt{P}\rrbracket(s)\otimes r$.

###### Proof.

We will show that

$\llbracket\Delta\Join\Xi\vdash\mathtt{P}\rrbracket_{n}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n})=\left(\llbracket\Delta\vdash\mathtt{P}\rrbracket(\mathcal{R})\mathrel{\otimes}\mathcal{Q}\right)_{n}.$

The proof goes by induction on $\mathtt{P}$.

  * •

The case where $\mathtt{P}=\mathtt{skip}$ is trivial.

  * •

When $\mathtt{P}=r\leftarrow e$, we observe that:

$\displaystyle\llbracket r\leftarrow
e\rrbracket_{n}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n})$
$\displaystyle=\text{bind}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n},m\mapsto\text{bind}(\llbracket\Delta\Join\Xi\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto t])}))$
$\displaystyle=\text{bind}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n},m\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(m_{\mathsf{dom}(\Delta)}),t\mapsto{\text{unit}(m[r\mapsto
t])}))$

Observe that ${\text{unit}(m[r\mapsto t])}$ is equal to
$l\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta)}[r\mapsto
t])}(l_{\mathsf{dom}(\Delta)}){\text{unit}(m_{\mathsf{dom}(\Xi)})}(l_{\mathsf{dom}(\Xi)})$,
so we can expand the expressions and obtain:

$l\mapsto\;\;\smashoperator[lr]{\sum_{m\in{\mathsf{supp}}(\llbracket\Delta\Join\Xi\rrbracket_{n})}^{}}\;\;\mathcal{R}_{n}(m_{\mathsf{dom}(\Delta)})\cdot\mathcal{Q}_{n}(m_{\mathsf{dom}(\Xi)})\cdot\\\
\sum_{t\in\llbracket\tau\rrbracket_{n}}\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m_{\mathsf{dom}(\Delta)})(t)\cdot{\text{unit}(m_{\mathsf{dom}(\Delta)}[r\mapsto
t])}(l_{\mathsf{dom}(\Delta)})\cdot\\\
{\text{unit}(m_{\mathsf{dom}(\Xi)})}(l_{\mathsf{dom}(\Xi)})$

By using the distributive property of multiplication, it is possible to
observe that this is equal to:

$\displaystyle l\mapsto\;\;\llbracket\Delta\vdash r\leftarrow
e\rrbracket_{n}(\mathcal{R}_{n})({l_{\mathsf{dom}(\Delta)}})\cdot\smashoperator[lr]{\sum_{m\in{\mathsf{supp}}(\llbracket\Xi\rrbracket_{n})}^{}}\;\;\mathcal{Q}_{n}(m)\cdot{\text{unit}(m)}(l_{\mathsf{dom}(\Xi)}),$

which, in turn, is equal to:

$l\mapsto\llbracket\Delta\vdash r\leftarrow
e\rrbracket_{n}(\mathcal{R}_{n})({l_{\mathsf{dom}(\Delta)}})\cdot\text{bind}(\mathcal{Q}_{n},{\text{unit}(\cdot)})(l_{\mathsf{dom}(\Xi)})=\\\
l\mapsto\llbracket\Delta\vdash r\leftarrow
e\rrbracket_{n}(\mathcal{R}_{n})({l_{\mathsf{dom}(\Delta)}})\cdot{\mathcal{Q}_{n}}(l_{\mathsf{dom}(\Xi)}).$

This, in turn, is equal to:

$\left(\llbracket\Delta\vdash r\leftarrow
e\rrbracket(\mathcal{R})\mathrel{\otimes}{\mathcal{Q}}\right)_{n}.$

  * •

When the program is $\mathtt{P};\mathtt{R}$, the claim is a direct consequence
of the IHs.

  * •

When the program is
$\mathtt{if}\;e\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$,
$\llbracket\mathtt{if}\;e\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n})$
is equivalent to:

$l\mapsto\smashoperator[r]{\sum_{m\in{\mathsf{supp}}{\llbracket\Delta\Join\Xi\rrbracket_{n}}}^{}}\;\;\mathcal{R}_{n}(m_{\mathsf{dom}(\Delta)})\cdot\mathcal{Q}_{n}(m_{\mathsf{dom}(\Xi)})\cdot
h(m)(l)$

where

$h(m)=\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=1\\\ \llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(m)})&\text{if
}m(r)=0\end{cases}$

Observe that
$h(m)=h^{\prime}(m_{\mathsf{dom}(\Delta)},m_{\mathsf{dom}(\Xi)})$, where

$h^{\prime}(l_{1},l_{2})=\
\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l_{1})}\mathrel{\otimes}{\text{unit}(l_{2})})&\text{if
}l_{1}(r)=1\\\
\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l_{1})}\mathrel{\otimes}{\text{unit}(l_{2})})&\text{if
}l_{1}(r)=0\\\ \end{cases}$

By using the IH, we conclude that this is equal to:

$h^{\prime}(l_{1},l_{2})=\
\begin{cases}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l_{1})})\mathrel{\otimes}{\text{unit}(l_{2})}&\text{if
}l_{1}(r)=1\\\
\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l_{1})})\mathrel{\otimes}{\text{unit}(l_{2})}&\text{if
}l_{1}(r)=0\\\ \end{cases}$

So we can rewrite the expression we wrote at the beginning as follows:

$l\mapsto\smashoperator[lr]{\sum_{m\in{\mathsf{supp}}{\llbracket\Delta\rrbracket_{n}}}^{}}\;\;\mathcal{R}_{n}(m)\cdot
h(m)(l_{\mathsf{dom}(\Delta)})\cdot\\\
\smashoperator[r]{\sum_{m\in{\mathsf{supp}}{\llbracket\Xi\rrbracket_{n}}}^{}}\;\;\mathcal{Q}_{n}(m)\cdot{\text{unit}(m)}(l_{\mathsf{dom}(\Xi)}),$

which is:

$l\mapsto\smashoperator[lr]{\sum_{m\in{\mathsf{supp}}{\llbracket\Delta\rrbracket_{n}}}^{}}\;\;\mathcal{R}_{n}(m)\cdot
h(m)(l_{\mathsf{dom}(\Delta)})\cdot\mathcal{Q}_{n}(m)(l_{\mathsf{dom}(\Xi)}).$

This last term is equal, by definition, to:

$\left(\llbracket\mathtt{if}\;e\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket(\mathcal{R})\mathrel{\otimes}\mathcal{Q}\right)_{n}.$

The conclusion comes by observing that
$\llbracket\Delta\Join\Xi\vdash\mathtt{P}\rrbracket(s\otimes
r)={(\llbracket\Delta\Join\Xi\vdash\mathtt{P}\rrbracket(\mathcal{R}\mathrel{\otimes}\mathcal{Q}))^{\Delta\Join\Xi}}$
and that $\llbracket\mathtt{P}\rrbracket(s)\otimes
r={(\llbracket\Delta\vdash\mathtt{P}\rrbracket(\mathcal{R})\mathrel{\otimes}\mathcal{Q})^{\Delta\Join\Xi}}$.
So, in particular:

$\llbracket\Delta\Join\Xi\vdash\mathtt{P}\rrbracket(\mathcal{R}\mathrel{\otimes}\mathcal{Q})=\llbracket\Delta\vdash\mathtt{P}\rrbracket(\mathcal{R})\mathrel{\otimes}\mathcal{Q}$

is a consequence of (C). ∎

######  Lemma 10 (Indistinguishability of Programs’ Semantic).

For every program $\mathtt{P}$, and every pair of stores
${{(\mathcal{R})^{\Delta}}}\approx{{(\mathcal{Q})^{\Xi}}}$such that
$\Delta\vdash\mathtt{P},\Xi\vdash\mathtt{P}$, it holds that
$\llbracket\mathtt{P}\rrbracket(\mathcal{R})\approx\llbracket\mathtt{P}\rrbracket(\mathcal{Q})$.

###### Proof.

Observe that the semantics of programs we gave can be defined in terms of the
Kleisli extension of a distribution ensemble with poly-time samplable
continuations. In particular, this can be shown by induction on the semantics
of programs observing that:

  * •

the claim is trivial for $\mathtt{skip}$

  * •

it is a consequence of the poly-time samplability property of the expressions’
semantics in the case of assignments, and on the observation that updating a
sample can be done in polynomial time

  * •

it is a direct consequence of the IH in the case of the composition,

  * •

in the case of the conditional statement, it is a consequence of the IHs, and
of the observation that testing a variable on that sample can be done in
polynomial time

This means that for every program $\mathtt{P}$, there is a polynomial
transformation on samples $t_{\mathtt{P}}$ such that:

$\llbracket\Delta\vdash\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n})={\text{bind}(\mathcal{R}_{n},t_{\mathtt{P}})}$

Assume the claim not to hold, this gives an adversary ${\mathcal{A}}$ which is
capable to distinguish $\llbracket\mathtt{P}\rrbracket(\mathcal{R})$ and
$\llbracket\mathtt{P}\rrbracket(\mathcal{Q})$ with non-negligible advantage.
This adversary can be used to define an adversary ${\mathcal{B}}$ with the
same advantage that given on input $\mathcal{R}$, it first computes the
continuation $t_{\mathtt{P}}$ on the sample
$\llbracket\mathtt{P}\rrbracket(\mathcal{R})$ and then feeds this value into
${\mathcal{A}}$. The advantage of ${\mathcal{B}}$ is the same of
${\mathcal{A}}$. ∎

######  Lemma 11.

If $\Delta\vdash r\leftarrow e$, $\mathcal{R}\in\llbracket\Delta\rrbracket$
and $r\notin\mathsf{FV}(e)$, it holds that:

$\displaystyle\llbracket r\rrbracket\left(\llbracket r\leftarrow
e\rrbracket(\mathcal{R})\right)=\llbracket e\rrbracket(\mathcal{R})=\llbracket
e\rrbracket\left(\llbracket r\leftarrow e\rrbracket(\mathcal{R})\right).$

###### Proof.

We start by fixing $n\in\mathbb{N}$ and by observing that:

$\displaystyle\llbracket r\rrbracket_{n}\left(\llbracket r\leftarrow
e\rrbracket(\mathcal{R}_{n})\right)$ $\displaystyle=\text{bind}(\llbracket
r\leftarrow e\rrbracket(\mathcal{R}_{n}),m\mapsto{\text{unit}(m(r))})$

the expression $\llbracket r\leftarrow e\rrbracket(\mathcal{R}_{n})$ can be
expanded as follows:

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{\text{unit}(l[r\mapsto t])}))$

using the associative property of the distribution monad and the property of
${\text{unit}(\cdot)}$, the whole expression can be rewritten as follows:

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto\text{bind}({\text{unit}(l[r\mapsto
t])},m\mapsto{\text{unit}(m(r))}))).$

The bind-unit pattern can be simplified as follows:

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{{\text{unit}(l[r\mapsto
t](r))}})).$

If we observe that ${l[r\mapsto t]}(r)=t$, it becomes

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{{\text{unit}(t)}})),$

which, in turn equals

$\text{bind}(\mathcal{R}_{n},l\mapsto{\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l)})=\llbracket
e\rrbracket_{n}(\mathcal{R}_{n}).$

With a similar chain of equivalences, it is possible to rewrite $\llbracket
e\rrbracket_{n}\left(\llbracket r\leftarrow e\rrbracket(\mathcal{R})\right)$
as follows::

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l[r\mapsto t]))).$

With an application of Lemma 4, we observe that this is equal to:

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l))).$

The assumptions of Lemma 4 can be matched by taking $\Xi$ as the environment
obtained removing $r$ from $\Delta$. The inner bind can be expanded as:

$\sum_{x\in\llbracket\tau\rrbracket_{n}}\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(t)\cdot\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l)=1\cdot\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l).$

For this reason the expression above can be rewritten as
$\text{bind}(\mathcal{R}_{n},l\mapsto{\llbracket\Delta\vdash
e:\tau\rrbracket_{n}^{\mathtt{d}}(l)})=\llbracket
e\rrbracket_{n}(\mathcal{R}_{n}).$ ∎

######  Lemma 12.

For every $n$, every $\mathtt{P}$ and every $\mathcal{R}_{n}$, we have
$\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n})=\text{bind}(\mathcal{R}_{n},m\mapsto\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(m)}))$.

###### Proof.

By induction on $\mathtt{P}$.

  * -

($\mathtt{skip}$). In this case, the claim is
$\mathcal{R}_{n}=\text{bind}(\mathcal{R}_{n},m\mapsto{\text{unit}(m)})$, which
is trivial.

  * -

($r\leftarrow e$). In this case, observe that:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto\llbracket r\leftarrow
e\rrbracket_{n}({\text{unit}(m)}))$

is equal to:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}({\text{unit}(m)},l\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto l[r\mapsto t]))),$

that, in turn, equals:

$\displaystyle\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto m[r\mapsto t]))=\llbracket
r\leftarrow e\rrbracket_{n}(\mathcal{R}_{n})$

  * -

($\mathtt{P};\mathtt{R}$). The claim is

$\llbracket\mathtt{P};\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n})=\text{bind}(\mathcal{R}_{n},m\mapsto\llbracket\mathtt{P};\mathtt{R}\rrbracket_{n}({\text{unit}(m)})).$

For the IH on $\mathtt{P}$, we can rewrite
$\llbracket\mathtt{P};\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n})$ as follows:

$\llbracket\mathtt{R}\rrbracket_{n}(\text{bind}(\mathcal{R}_{n},l\mapsto\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)})))$

For the IH on $\mathtt{R}$, this claim can be rewritten again as:

$\text{bind}(\text{bind}(\mathcal{R}_{n},l\mapsto\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)})),w\mapsto\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(w)}))$

That can be simplified as follows:

$\text{bind}(\mathcal{R}_{n},l\mapsto\text{bind}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)}),w\mapsto\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(w)})))$

With the application of the IH on $\mathtt{R}$, we conclude.

  * -

($\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$). The
claim is a direct consequence of the definition of the semantics of the
construct.

∎

######  Lemma 13.

For every $n\in\mathbb{N}$, and every
$m\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n}))$,
there is $\overline{m}\in{\mathsf{supp}}(\mathcal{R}_{n})$ such that
$m\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{m})}))$.

###### Proof.

The proof goes by induction on $\mathtt{P}$.

  * -

($\mathtt{skip}$). Trivial.

  * -

($r\leftarrow e$). Assume that the claim does not hold. This means that there
is $m\in{\mathsf{supp}}(\llbracket r\leftarrow
e\rrbracket_{n}(\mathcal{R}_{n}))$ such that for every
$l\in{\mathsf{supp}}(\mathcal{R}_{n})$, we have:

$\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{\text{unit}(l[r\mapsto t])})(m)=0.$

From this result we can deduce $\llbracket r\leftarrow
e\rrbracket_{n}(\mathcal{R}_{n})(m)=0$, but this contradicts the premise.

  * -

($\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}$).
Assume that the claim does not hold. This means there is
$m\in{\mathsf{supp}}(\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n}))$
such that for every $l\in{\mathsf{supp}}(\mathcal{R}_{n})$, we have:

$\displaystyle l(r)=0$
$\displaystyle\Rightarrow\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(l)})(m)=0$
$\displaystyle l(r)=1$
$\displaystyle\Rightarrow\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l)})(m)=0.$

This shows that
$\llbracket\mathtt{if}\;r\;\mathtt{then}\;\mathtt{P}\;\mathtt{else}\;\mathtt{R}\rrbracket_{n}(\mathcal{R}_{n})(m)=0$,
but this contradicts the premise.

  * -

($\mathtt{P};\mathtt{R}$). Assume
$m\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n}))$, we
must show that there is $\overline{m}$ is such that:

$m\in{\mathsf{supp}}(\llbracket\mathtt{R}\rrbracket_{n}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{m})})))$

From the IH on $\mathtt{R}$, we deduce that there is
$\overline{l}\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}(\mathcal{R}_{n}))$
such that

$m\in{\mathsf{supp}}(\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(\overline{l})})).$

With another application of this hypothesis, we deduce that there is
$\overline{w}\in{\mathsf{supp}}(\mathcal{R}_{n})$ such that:

$\overline{l}\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})})).$

With an application of Lemma 12, we observe that
$\llbracket\mathtt{R}\rrbracket_{n}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})}))(m)$
is equal to:

$\text{bind}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})}),l\mapsto\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l)}))(m),$

which in turn is equal to

$\sum_{l\in{\mathsf{supp}}(\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})}))}\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})})(l)\cdot\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(l)})(m)$

which is greater than:

$\llbracket\mathtt{P}\rrbracket_{n}({\text{unit}(\overline{w})})(\overline{l})\cdot\llbracket\mathtt{R}\rrbracket_{n}({\text{unit}(\overline{l})})(m)$

which is greater than $0$ for the assumptions above.

∎

######  Lemma 14.

If $\Delta\vdash r\leftarrow d$, $\mathcal{R}\in\llbracket\Delta\rrbracket$
and $r\notin\mathsf{FV}(d)$, it holds that:

$\displaystyle\forall n\in\mathbb{N}.\forall l\in{\mathsf{supp}}(\llbracket
r\leftarrow d\rrbracket_{n}(\mathcal{R}_{n})).\llparenthesis
d\rrparenthesis_{n}(l)=\llparenthesis r\rrparenthesis_{n}(l).$

###### Proof.

Assume this to be false for some $n$ and some $l\in\llbracket r\leftarrow
d\rrbracket_{n}(\mathcal{R}_{n})$. From Lemma 13, we deduce that there is that
there is $m\in{\mathsf{supp}}({\mathcal{R}})$ such that
$l\in{\mathsf{supp}}(\llbracket r\leftarrow
d\rrbracket_{n}({\text{unit}(m)}))$. Observe that:

$\displaystyle\llbracket r\leftarrow d\rrbracket_{n}({\text{unit}(m)})$
$\displaystyle=\text{bind}({\text{unit}(m)},m\mapsto\text{bind}(\llbracket
d\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto t])}))$
$\displaystyle=\text{bind}(\llbracket
d\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto t])})$
$\displaystyle=\text{bind}({\text{unit}(\llparenthesis
d\rrparenthesis_{n}(m))},t\mapsto{\text{unit}(m[r\mapsto t])})$
$\displaystyle={\text{unit}(m[r\mapsto\llparenthesis
d\rrparenthesis_{n}(m)])}.$

From this observation, we deduce that $l=m[r\mapsto\llparenthesis
d\rrparenthesis_{n}(m)]$. In particular, we have that $\llparenthesis
r\rrparenthesis_{n}(l)=l(r)=\llparenthesis d\rrparenthesis_{n}(m)$, and from
2, we also conclude that $\llparenthesis d\rrparenthesis_{n}(l)=\llparenthesis
d\rrparenthesis_{n}(m[r\mapsto\llparenthesis
d\rrparenthesis_{n}(m)])=\llparenthesis d\rrparenthesis_{n}(m)$, but this is
absurd because we were assuming that $\llparenthesis
r\rrparenthesis_{n}(l)\neq\llparenthesis d\rrparenthesis_{n}(l)$. ∎

######  Lemma 15.

Let $\Delta,\Xi$ and $\Theta$ be environments such that:

  * •

$\Delta\Join\Xi\downarrow$.

  * •

$\Delta\vdash e:\tau$.

  * •

$\Delta\Join\Xi\vdash r\leftarrow e$.

and let $\mathcal{R},\mathcal{Q}\in\llbracket\Delta\Join\Xi\rrbracket$, such
that
$\mathcal{R}_{\Delta\Join\Xi\to\Delta}=\mathcal{Q}_{\Delta\Join\Xi\to\Delta}$
it holds that $\llbracket r\leftarrow
e\rrbracket(\mathcal{R})_{\Delta\Join\Xi\to\Delta\cup\\{r:\tau\\}}=\llbracket
r\leftarrow
e\rrbracket(\mathcal{Q})_{\Delta\Join\Xi\to\Delta\cup\\{r:\tau\\}}$.

###### Proof.

We start by expanding $\llbracket r\leftarrow
e\rrbracket_{n}(\mathcal{R})_{\Delta\Join\Xi\to\Delta\cup\\{r:\tau\\}}$ as
$\text{bind}(\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto
t])})),l\mapsto{\text{unit}(l_{\mathsf{dom}(\Delta)\cup\\{r\\}})})$. This
rewrites as follows:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m[r\mapsto
t]_{\mathsf{dom}(\Delta)\cup\\{r\\}})})),$

which is equal to:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m),t\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta)}[r\mapsto
t])})),$

By Lemma 4, we deduce that, in turn, it equals:

$\text{bind}(\mathcal{R}_{n},m\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(m_{\mathsf{dom}(\Delta)}),t\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta)}[r\mapsto
t])})),$

We can also observe that this is equal to:

$\text{bind}({(\mathcal{R}_{\Delta\Join\Xi\to\Delta})}_{n},l\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{\text{unit}(l[r\mapsto t])}))$

by expanding the definition of projection and applying standard properties of
monads. From our premise, we deduce that it is equal to:

$\text{bind}({(\mathcal{Q}_{\Delta\Join\Xi\to\Delta})}_{n},l\mapsto\text{bind}(\llbracket
e\rrbracket_{n}^{\mathtt{d}}(l),t\mapsto{\text{unit}(l[r\mapsto t])})).$

By applying the same steps but in the reverse order, we are able to show the
claim that we are aiming at. ∎

##  4 Cryptographic Probabilistic Separation Logic

This section is devoted to introducing a variation on Barthe et al.’s
probabilistic separation logic called _cryptographic probabilistic separation
logic_ (CPSL in the following). Compared to PSL, but also to the logic of
bunched implications (BI) [24, 25], CPSL is simpler in that the only
connectives are multiplicative and additive conjunctions, i.e. $*$ and
$\land$. In addition, instead of working with plain, untyped formulas, we work
with _well-typed_ formulas. Thanks to this choice, the semantics of separating
conjunction is more precise than in PSL, and as a byproduct gives rise to a
lighter formulation of program logic rules in Section 5.

We first introduce the syntax of CSL and its formulas, then we proceed by
defining a semantics for it based on _efficiently samplable_ randomized
stores. Finally, we show that CSL enjoys some basic but useful properties.

###  4.1 The Syntax and Semantics of CSL

$\displaystyle\llbracket{(\mathbf{U}(e))^{\Delta}}\rrbracket\mathrel{:=}\\{{{(\mathcal{R})^{\Delta}}}\in\llbracket\Delta\rrbracket\mid$
$\displaystyle\;\llbracket\Delta\vdash
e:\tau\rrbracket(\mathcal{R})\approx\mathsf{unif}(\tau)\\}$
$\displaystyle\llbracket{(\mathbf{CI}(e,g))^{\Delta}}\rrbracket\mathrel{:=}\\{{{(\mathcal{R})^{\Delta}}}\in\llbracket\Delta\rrbracket\mid$
$\displaystyle\;\llbracket e\rrbracket(\mathcal{R})\approx\llbracket
g\rrbracket(\mathcal{R})\\}$
$\displaystyle\llbracket{(\mathbf{EQ}(e,g))^{\Delta}}\rrbracket\mathrel{:=}\\{{{(\mathcal{R})^{\Delta}}}\in\llbracket\Delta\rrbracket\mid$
$\displaystyle\;\llbracket e\rrbracket(\mathcal{R})=\llbracket
g\rrbracket(\mathcal{R})\\}$
$\displaystyle\llbracket{(\mathbf{IS}(d,c))^{\Delta}}\rrbracket\mathrel{:=}\\{{{(\mathcal{R})^{\Delta}}}\in\llbracket\Delta\rrbracket\mid$
$\displaystyle\;\forall n\in\mathbb{N}.\forall
m\in{\mathsf{supp}}(\mathcal{R}_{n}).\llparenthesis
d\rrparenthesis_{n}(m)=\llparenthesis c\rrparenthesis_{n}(m)\\}$

$s\models^{\Delta}{(A)^{\Delta}}$ | iff $s\in\llbracket{(A)^{\Delta}}\rrbracket$
---|---
$s\models^{\Delta}{(\top)^{\Delta}}$ | always
$s\models^{\Delta}{(\bot)^{\Delta}}$ | never
$s\models^{\Delta}{({(\phi)^{\Xi}}\land{(\psi)^{\Theta}})^{\Delta}}$ | iff there are $r\sqsubseteq s,t\sqsubseteq s$ such that $r\models^{\Xi}{(\phi)^{\Xi}}$ and $t\models^{\Theta}{(\psi)^{\Theta}}$
$s\models^{\Delta}{({(\phi)^{\Xi}}*{(\psi)^{\Theta}})^{\Delta}}$ | iff there are $r,t$ such that $r\otimes t\downarrow$, $r\otimes t\approx\sqsubseteq s$, $r\models^{\Xi}{(\phi)^{\Xi}}$ and $t\models^{\Theta}{(\psi)^{\Theta}}$

Figure 2: Semantics of CSL

####  4.1.1 Syntax

We write $\mathcal{AP}$ for the set of atomic formulas as defined in the
following grammar:

$\displaystyle
A::=\mathbf{U}(e)\;\mbox{\Large{$\mid$}}\;\mathbf{CI}(e,e)\;\mbox{\Large{$\mid$}}\;\mathbf{EQ}(e,e)\;\mbox{\Large{$\mid$}}\;\mathbf{IS}(d,d)$

The formula $\mathbf{U}(e)$, present in PSL, is interpreted differently here,
and indicates that the expression $e$ evaluates to a distribution that is
computationally indistinguishable from the uniform one. The three binary
atomic formulas $\mathbf{CI}(e,g)$, $\mathbf{EQ}(e,g)$ and $\mathbf{IS}(d,c)$
all speak of indistinguishability between the two expressions involved but at
different levels, and their semantics will be explained in detail later. We
also define a type system for atomic formulas in an environment. Judgments for
this type system are in the form $\Delta\vdash A$, and are proved valid by the
following rules:

$\displaystyle\Delta\vdash\mathbf{U}(e)\Delta\vdash
e:\tau\qquad\qquad\Delta\vdash\mathbf{CI}(e,g)\lx@proof@logical@and\Delta\vdash
e:\tau\Delta\vdash g:\tau$
$\displaystyle\Delta\vdash\mathbf{EQ}(e,g)\lx@proof@logical@and\Delta\vdash
e:\tau\Delta\vdash
g:\tau\qquad\Delta\vdash\mathbf{IS}(d,c)\lx@proof@logical@and\Delta\vdash
d:\tau\Delta\vdash c:\tau$

On top of the set of atomic formulas, one can build the set of generic
formulas, as follows:

######  Definition 10.

For a fixed environment $\Delta$, the set ${(\Phi)^{\Delta}}$ of _formulas for
$\Delta$_ is the smallest set of expressions closed under the following rules:

$\displaystyle{(A)^{\Delta}}\in{(\Phi)^{\Delta}}\Delta\vdash
A\quad{(\top)^{\Delta}}\in{(\Phi)^{\Delta}}\quad{(\bot)^{\Delta}}\in{(\Phi)^{\Delta}}$
$\displaystyle{({(\phi)^{\Xi}}*{(\psi)^{\Theta}})^{\Delta}}\in{(\Phi)^{\Delta}}\lx@proof@logical@and{(\phi)^{\Xi}}\in{(\Phi)^{\Xi}}{(\psi)^{\Theta}}\in{(\Phi)^{\Theta}}\Xi\Join\Theta\sqsubseteq\Delta$
$\displaystyle{({(\phi)^{\Xi}}\land{(\psi)^{\Theta}})^{\Delta}}\in{(\Phi)^{\Delta}}\lx@proof@logical@and{(\phi)^{\Xi}}\in{(\Phi)^{\Xi}}{(\psi)^{\Theta}}\in{(\Phi)^{\Theta}}\Xi\sqsubseteq\Delta\Theta\sqsubseteq\Delta$

The set of CSL formulas $\Phi$ is the union of all the sets
${(\Phi)^{\Delta}}$ over all possible environments $\Delta$. ∎

As already observed, the binary connectives we consider are just conjunctions.
On the other hand, formulas are typed and, crucially, the way in which a
separating conjunction splits the underlying environment is fixed by the
formula itself.

####  4.1.2 Semantics

The semantics of CSL formulas is a family of relations $\models^{\Delta}$ such
that, for every environment $\Delta$, we have that
$\models^{\Delta}\subseteq{\llbracket\Delta\rrbracket}\times{(\Phi)^{\Delta}}$.
The full semantics is in Figure 2 where, in particular, with
$\approx\sqsubseteq$ we denote the composition of $\approx$ and $\sqsubseteq$.

The role of the three different forms of binary atomic formulas should be now
clearer. Atomic propositions like ${(\mathbf{CI}(e,g))^{\Delta}}$ capture
computational indistinguishability:
${{(\mathcal{R})^{\Delta}}}\models^{\Delta}{(\mathbf{CI}(e,g))^{\Delta}}$
holds whenever $\llbracket\Delta\vdash
e:\tau\rrbracket({{(\mathcal{R})^{\Delta}}})$ is computationally
indistinguishable from $\llbracket\Delta\vdash
g:\tau\rrbracket({{(\mathcal{R})^{\Delta}}})$. The atomic formula
${(\mathbf{EQ}(e,g))^{\Delta}}$ captures a stronger form equivalence: it holds
in a state $\mathcal{R}$ if and only if $\llbracket\Delta\vdash
e:\tau\rrbracket({\mathcal{R}})$ and $\llbracket\Delta\vdash
g:\tau\rrbracket({\mathcal{R}})$ are equal — instead of being simply
indistinguishable. Finally, ${(\mathbf{IS}(d,c))^{\Delta}}$ states something
even stronger: $\mathcal{R}\models^{\Delta}{(\mathbf{IS}(d,c))^{\Delta}}$
holds if and only if for every $n\in\mathbb{N}$, every sample $m$ in the
support of the distribution $\mathcal{R}_{n}\in\llbracket\Delta\rrbracket$ is
such that $\llparenthesis\Delta\vdash
d:\tau\rrparenthesis_{n}(m)=\llparenthesis\Delta\vdash
c:\tau\rrparenthesis_{n}(m)$. The semantics of $\mathbf{IS}(d,c)$ differs from
that of $\mathbf{EQ}(e,g)$ for two main reasons: first, the atomic proposition
$\mathbf{IS}(d,c)$ applies only to _deterministic_ expressions, while
$\mathbf{EQ}(e,g)$ applies also to _probabilistic_ expressions. Second, we
have
${(\mathcal{R})^{\Delta}}\in\llbracket{(\mathbf{IS}(d,c))^{\Delta}}\rrbracket$
when the _values_ obtained by computing $d$ and $c$ on every sample of
${\mathsf{supp}}({\mathcal{R}_{n}})$ are identical independently of the
security parameter $n$; instead,
${(\mathcal{R})^{\Delta}}\in{(\mathbf{EQ}(e,g))^{\Delta}}$ requires the
_families of distributions_ obtained by evaluating $e$ and $g$ on the ensemble
${(\mathcal{R})^{\Delta}}$ are the same.

######  Example 2.

The distribution ensemble $\mathcal{R}\in\llbracket
r,s:\mathsf{Bool}\rrbracket$ that is defined as follows

$\mathcal{R}_{n}\mathrel{:=}\left\\{\\{r\mapsto 0,s\mapsto
1\\}^{\frac{1}{2}},\\{r\mapsto 1,s\mapsto 0\\}^{\frac{1}{2}}\right\\}$

satisfies $\mathbf{EQ}(r,s)$ because the marginal distributions of $r$ and $s$
are identical, but it does not satisfy $\mathbf{IS}(r,s)$ because there is a
value of the security parameter $n$ and a sample
$m\in{\mathsf{supp}}(\mathcal{R}_{n})$ where $m(r)\neq m(s)$ (actually this
happens for every sample, independently of $n$). ∎

The interpretation of the additive conjunction is the same as in PSL except
that it asks that the sub-formulas hold in specific parts of the stores.
Formally, we have that
${(\mathcal{R})^{\Delta}}\models^{\Delta}{({(\phi)^{\Xi}}\land{(\phi)^{\Theta}})^{\Delta}}$
whenever there are $\mathcal{Q},\mathcal{T}\sqsubseteq\mathcal{R}$ such that:
${(\mathcal{Q})^{\Xi}}\models^{\Xi}{(\phi)^{\Xi}}$ and
${(\mathcal{T})^{\Theta}}\models^{\Theta}{(\psi)^{\Theta}}$.

The crux of CSL is the way separating conjunction is interpreted, which now
refers to computational independence: we ask that
${(\mathcal{R})^{\Delta}}\models^{\Delta}{({(\phi)^{\Xi}}*{(\phi)^{\Theta}})^{\Delta}}$
holds whenever it is possible to find two ensembles
$\mathcal{Q}\in\llbracket\Xi\rrbracket$ and
$\mathcal{T}\in\llbracket\Theta\rrbracket$ such that
${(\mathcal{Q})^{\Xi}}\models^{\Xi}{(\phi)^{\Xi}},{(\mathcal{T})^{\Theta}}\models^{\Theta}{(\psi)^{\Theta}}$,
and the projection of ${(\mathcal{R})^{\Delta}}$ on the environment
$\Xi\Join\Theta$ is indistinguishable from the tensor product of
${{(\mathcal{Q})^{\Xi}}}$ and ${(\mathcal{T})^{\Theta}}$. As argued in Section
7 below, the last condition is a characterization of the standard notion of
computational independence given by Fay [15]. So, our interpretation of the
separating conjunction — which is based on that of BI — exactly captures
computational independence.

##### Notational Conventions

In the following, we often omit $\Delta$ from $\models^{\Delta}$ if it is
evident from the context, from ${(A)^{\Delta}}$ when $A$ mentions exactly the
variables of $\mathsf{dom}(\Delta)$, And from
${({(\phi)^{\Xi}}\odot{(\psi)^{\Theta}})^{\Delta}}$ for
$\odot\in\\{\land,*\\}$ when $\Delta$ is exactly $\Xi\Join\Delta$. In order to
simplify the presentation of the formulas, we write $\Delta_{S}$ for the
environment obtained by restricting the domain of $\Delta$ to $S$. We also
omit $\Delta$ when it is clear from the context. In particular, when
$s={(\mathcal{R})^{\Delta}}$ and $s\models^{\Delta}{(\phi)^{\Delta}}$ holds,
we write simply $s\models\phi$. Finally, we write
${(\phi)^{\Delta}}\models^{\Delta}{(\psi)^{\Delta}}$ as a shorthand for:

$\forall
s\in\llbracket\Delta\rrbracket.\left(s\models^{\Delta}{(\phi)^{\Delta}}\right)\Rightarrow
s\models^{\Delta}{(\psi)^{\Delta}}.$

####  4.1.3 Algebraic Properties of Efficiently Samplable Distribution
Ensembles

We model CSL on efficiently samplable distribution ensembles; this set, in
turn enjoys some remarkable algebraic properties with respect to the tensor
product $\mathrel{\otimes}$ and to the relations $\approx$ and $\sqsubseteq$.
In the following, we review some of them in order to prepare the ground for
showing, in the Section 4.4.2, that the structure
$(\mathcal{S},\mathrel{\otimes},\mathbf{0},\approx\sqsubseteq)$ is a _partial
Kripke resource monoid_ (Definition 11). This result, in turn, allows us to
compare the semantics of our logic with the standard interpretation the
conjunctive fragment of BI on _partial Kripke resource monoids_ in
Propositions 2 and 3.

######  Definition 11.

A partial Kripke resource monoid $(M,\bullet,e,\leq)$ consists of a set $M$
together with a partial binary operation $\bullet$, an element $e\in M$ and a
pre-order $\leq$ satisfying the following:

  * 1.

For every $x\in M$, both $x\bullet e$ and $e\bullet x$ are defined, and equal
to $x$.

  * 2.

The operation $\bullet$ is associative, in the following sense: $(x\bullet
y)\bullet z$ and $x\bullet(y\bullet z)$ are either both undefined or both
defined, and in the latter case, they are equal.

  * 3.

The pre-order $\leq$ is compatible with $\bullet$, i.e., if $x\leq y$ and
$x\bullet z,y\bullet z$ are both defined, then $x\bullet z\leq y\bullet z$
(and similarly for $z\bullet x,z\bullet y$). ∎

Showing that the relation $\approx\sqsubseteq$, is a pre-order and is
compatible with respect to $\otimes$, as required by Definition 11, requires
appreciable effort.

##### Properties of projection.

We start with the projection operation on stores. We start by observing that
the projection $\cdot_{\Delta\to\Delta}$ is the identity.

######  Remark 3 (Identity).

For every $\mathcal{R}\in\llbracket\Delta\rrbracket$,
$\mathcal{R}_{\Delta\to\Delta}=\mathcal{R}$.

###### Proof.

$(\mathcal{R}_{\Delta\to\Delta})_{n}=\text{bind}(\mathcal{R}_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta)})})=\text{bind}(\mathcal{R}_{n},m\mapsto{\text{unit}(m)})=\mathcal{R}.$

∎

We also observe that projections are closed under composition, when this
operation is defined.

######  Lemma 16 (Closure Under Composition of Projections).

Whenever $\Delta_{1}\sqsubseteq\Delta_{2}\sqsubseteq\Delta_{3}$, for every
$\mathcal{R}_{3}\in\llbracket\Delta_{3}\rrbracket$, it holds that:

$((\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{2}})_{\Delta_{2}\to\Delta_{1}}=(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}$

###### Proof.

$((\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{2}})_{\Delta_{2}\to\Delta_{1}}$
equals

$n\mapsto\text{bind}(\text{bind}({\mathcal{R}_{3}}_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta_{2})})}),m\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta_{1})})})$

which, in turn, equals:

$n\mapsto\text{bind}({\mathcal{R}_{3}}_{n},m\mapsto{\text{unit}({m_{\mathsf{dom}(\Delta_{2})}}_{\mathsf{dom}(\Delta_{1})})}).$

Observe that
${m_{\mathsf{dom}(\Delta_{2})}}_{\mathsf{dom}(\Delta_{1})}=m_{\mathsf{dom}(\Delta_{1})}$.
This concludes the proof. ∎

##### Properties of $\sqsubseteq$

The extension relation $\sqsubseteq$ is defined on top of the notion of
projection; for this reason, 3 and Lemma 16 can be used to show that
$\sqsubseteq$ is a pre-order.

######  Lemma 17 (Pre-order).

The relation $\sqsubseteq$ is a pre-order relation on $\mathcal{S}$.

###### Proof.

  * •

For reflexivity, we need to show that

${{(\mathcal{R})^{\Delta}}}\sqsubseteq{{(\mathcal{R})^{\Delta}}}.$

In particular, this requires to verify that $\Delta\sqsubseteq\Delta$ and that
$\mathcal{R}_{\Delta\to\Delta}=\mathcal{R}$, that is 3.

  * •

For transitivity, we need to show that:

$\displaystyle{(\mathcal{R}_{1})^{\Delta_{1}}}\sqsubseteq{(\mathcal{R}_{2})^{\Delta_{2}}}\sqsubseteq{(\mathcal{R}_{3})^{\Delta_{3}}}\Rightarrow$
$\displaystyle{(\mathcal{R}_{1})^{\Delta_{1}}}\sqsubseteq{(\mathcal{R}_{3})^{\Delta_{3}}}.$

The conclusion on the environments is a consequence of the transitivity of
$\subseteq$. Then we need to show that
$(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}=\mathcal{R}_{1}$. We also know
that $(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{2}}=\mathcal{R}_{2}$ and that
$(\mathcal{R}_{2})_{\Delta_{2}\to\Delta_{1}}=\mathcal{R}_{1}$; finally, due to
$\Delta_{1}\sqsubseteq\Delta_{2}$, we also know that
$\left((\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{2}}\right)_{\Delta_{2}\to\Delta_{1}}=(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}$.
Therefore:

$\mathcal{R}_{1}=(\mathcal{R}_{2})_{\Delta_{2}\to\Delta_{1}}=((\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{2}})_{\Delta_{2}\to\Delta_{1}}=(\mathcal{R}_{3})_{\Delta_{1}}.$

The last equivalence is a consequence of Lemma 16.

∎

##### Properties of $\approx$.

We start by showing that $\approx$ is an equivalence relation (Lemma 18). This
observation is crucial for showing that the composition of $\approx$ and
$\sqsubseteq$ is a pre-order. Then, we show that $\approx$ is compatible with
the tensor product (Lemma 19), and that $\approx$ and $\sqsubseteq$ enjoy a
form of distributivity (Lemma 20). These properties are respectively used to
show that the composition of $\approx$ and $\sqsubseteq$ is compatible with
the tensor product, and that it is transitive, and these are both crucial
properties for showing that
$(\mathcal{S},\mathrel{\otimes},\mathbf{0},\approx\sqsubseteq)$ is a _partial
Kripke resource monoid_.

######  Lemma 18.

The relation $\approx$ is an equivalence on $\mathcal{S}$.

###### Proof.

  * •

Reflexivity is trivial.

  * •

For symmetry we need to show that:

$\displaystyle{{(\mathcal{R})^{\Delta}}}\approx{{(\mathcal{Q})^{\Delta}}}\Rightarrow{{(\mathcal{Q})^{\Delta}}}\approx{{(\mathcal{R})^{\Delta}}},$

which is a consequence of the fact that for every $n\in\mathbb{N}$ and every
polytime distinguisher
${\mathcal{A}}:\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\to\llbracket\mathbb{B}\rrbracket_{n}^{\mathtt{d}}$:

$\displaystyle\left|{\text{Pr}_{m\leftarrow\mathcal{R}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow\mathcal{Q}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]\right|=$
$\displaystyle\left|{\text{Pr}_{m\leftarrow\mathcal{Q}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow\mathcal{R}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]\right|.$

  * •

For transitivity we need to show that:

$\displaystyle{(\mathcal{R}_{1})^{\Delta}}\approx{(\mathcal{R}_{2})^{\Delta}}\land{(\mathcal{R}_{2})^{\Delta}}\approx{(\mathcal{R}_{3})^{\Delta}}\Rightarrow$
$\displaystyle{(\mathcal{R}_{1})^{\Delta}}\approx{(\mathcal{R}_{3})^{\Delta}}.$

It holds that:

$\displaystyle\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{3}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\right|=$
$\displaystyle\begin{multlined}\big{|}{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{3}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]+\\\
{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\big{|}\leq\end{multlined}\big{|}{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{3}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]+\\\
{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\big{|}\leq$
$\displaystyle\begin{multlined}\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\right|+\\\
\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{3}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\right|\leq\end{multlined}\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\right|+\\\
\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{3}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{\mathcal{R}_{2}}_{n}}}\left[{\mathcal{A}}(n,m)=1\right]\right|\leq$
$\displaystyle{\mathit{negl}}_{1}(n)+{\mathit{negl}}_{2}(n)$

We know that ${\mathit{negl}}_{1}$ and ${\mathit{negl}}_{2}$ are two
negligible functions because of the indistinguishability of
${(\mathcal{R}_{1})^{\Delta}}$ and ${(\mathcal{R}_{2})^{\Delta}}$ and that of
${(\mathcal{R}_{2})^{\Delta}}$ and ${(\mathcal{R}_{3})^{\Delta}}$. The sum of
two negligible functions is a negligible function.

∎

######  Lemma 19 (Compatibility of $\approx$ and $\otimes$).

The relation $\approx$ and the function $\otimes$ are compatible, i.e.

$\forall s,r,t.s\approx r\Rightarrow(s\otimes t)\downarrow\Rightarrow(r\otimes
t)\downarrow\Rightarrow(s\otimes t)\approx(r\otimes t)$

and

$\forall s,r,t.s\approx r\Rightarrow(t\otimes s)\downarrow\Rightarrow(t\otimes
r)\downarrow\Rightarrow(t\otimes s)\approx(t\otimes r)$

###### Proof.

We only show the right compatibility. The proof of left compatibility is
analogous. Assume the statement not to hold, i.e. there are three stores
$s={{(\mathcal{R}_{1})^{\Delta_{1}}}},r={{(\mathcal{R}_{2})^{\Delta_{2}}}},t={{(\mathcal{R}_{3})^{\Delta_{3}}}}$
such that $s\approx r$, $(s\otimes t)$ is defined, $(r\otimes t)$ is defined
and finally that there is a distinguisher ${\mathcal{A}}$ which distinguishes
$s\otimes t$ and $s\otimes r$ with non-negligible advantage. We know that
$\mathcal{R}_{3}$ is efficiently samplable for every $n\in\mathbb{N}$, thus,
we can call $\mathit{R}$ the probabilistic polytime algorithm sampling
$(\mathcal{R}_{3})_{n}$. In particular, the distinguisher ${\mathcal{B}}$ can
be obtained by sampling from the poly-time algorithm for $\mathcal{R}_{3}$,
namely $\mathit{R}$ to obtain a sample $l$. Then, ${\mathcal{B}}$ combines its
input sample $m$ and $l$ in a unique sample and then invokes ${\mathcal{A}}$
on this sample. By polynomiality of ${\mathcal{A}}$ and of $\mathit{R}$,
${\mathcal{B}}$ is polynomial. Moreover, the advantage of ${\mathcal{B}}$ in
distinguishing $\mathcal{R}_{1}$ and $\mathcal{R}_{2}$ is the same of
${\mathcal{A}}$ on $(\mathcal{R}_{1}\mathrel{\otimes}\mathcal{R}_{3})$ and
$(\mathcal{R}_{2}\mathrel{\otimes}\mathcal{R}_{3})$. ∎

######  Lemma 20 (Distributivity of $\approx$ and $\sqsubseteq$).

If $s\sqsubseteq r\approx t$, then there exists $u$ such that $s\approx
u\sqsubseteq t$.

###### Proof.

The claim we are aiming to show is: for every $s,r,t\in\mathcal{S}$,
$s\sqsubseteq r\approx t$, then there is $u\in\mathcal{S}$ such that $s\approx
u\sqsubseteq t$. This claim can be equivalently restated as follows:

$\displaystyle{{(\mathcal{R}_{1})^{\Delta_{1}}}}\sqsubseteq{{(\mathcal{R}_{2})^{\Delta_{2}}}}\approx{{(\mathcal{R}_{3})^{\Delta_{3}}}}\Rightarrow$
$\displaystyle\exists\Delta_{4},\mathcal{R}_{4}.{{(\mathcal{R}_{1})^{\Delta_{1}}}}\approx{{(\mathcal{R}_{4})^{\Delta_{4}}}}\sqsubseteq{{(\mathcal{R}_{3})^{\Delta_{3}}}}$

Choosing $\Delta_{4}=\Delta_{1}$ and
$\mathcal{R}_{4}=(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}$, we are able to
show the claim.

  * •

To show $\Delta_{4}\sqsubseteq\Delta_{3}$, we can show that
$\Delta_{1}\sqsubseteq\Delta_{3}$. From our assumption, we know that
$\Delta_{1}\sqsubseteq\Delta_{2}=\Delta_{3}$, so
$\Delta_{1}\sqsubseteq\Delta_{3}$.

  * •

Similarly, to show
$\mathcal{R}_{4}=(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{4}}$ it suffices to
observe that $\Delta_{4}=\Delta_{1}$.

This concludes the proof that
${{(\mathcal{R}_{4})^{\Delta_{4}}}}\sqsubseteq{{(\mathcal{R}_{3})^{\Delta_{3}}}}$.
It remains to show that:

${{(\mathcal{R}_{1})^{\Delta_{1}}}}\approx{((\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}})^{\Delta_{1}}}$
($*$)

Assume that $(\mathcal{R}_{s})$ and
$(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}$ are distinguishable by
${\mathcal{A}}$, from Definition 7, this is equivalent to assuming that:

$\left|{\text{Pr}_{m\leftarrow{\mathcal{R}_{1}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}}_{n}}}\left[{\mathcal{A}}(1^{n},m)=1\right]\right|$

is not a negligible function. Let the distinguisher ${\mathcal{B}}$ which take
its input $1^{n}$ and a sample
$l\in\llbracket\Delta_{3}\rrbracket_{n}^{\mathtt{d}}$ and executes
${\mathcal{A}}$ on $(l_{\mathsf{dom}(\Delta_{1})},1^{n})$. ${\mathcal{B}}$ is
still a probabilistic polynomial time computable function. Due to
$\Delta_{1}\sqsubseteq\Delta_{3}$, the probability of returning 1 of
${\mathcal{B}}$ on samples taken from $\mathcal{R}_{3}$ is exactly that of
${\mathcal{A}}$ on samples taken from
$(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{1}}$, and similarly for
$\mathcal{R}_{2}$, the output distribution is the same of ${\mathcal{A}}$ on
$(\mathcal{R}_{2})_{\Delta_{2}\to\Delta_{1}}=\mathcal{R}_{1}$. For this
reason:

$\left|{\text{Pr}_{m\leftarrow{(\mathcal{R}_{3})}_{n}}}\left[{\mathcal{B}}(1^{n},m)=1\right]-{\text{Pr}_{m\leftarrow{(\mathcal{R}_{2})}_{n}}}\left[{\mathcal{B}}(1^{n},(\mathcal{R}_{2})(n))=1\right]\right|$

is not a negligible function, but this is absurd since we were assuming that:

${{(\mathcal{R}_{2})^{\Delta_{2}}}}\approx{{(\mathcal{R}_{3})^{\Delta_{3}}}},$

so ${\mathcal{A}}$ cannot exist, and thus $(*)$ holds. ∎

##### Compatibility of $\sqsubseteq$ and $\approx$.

The last property that we need to show is the compatibility of $\sqsubseteq$
and $\approx$. With Lemma 19, this property is useful to show that even the
relation $\approx\sqsubseteq$ is compatible with $\mathrel{\otimes}$, and
enabling us to show that
$(\mathcal{S},\mathrel{\otimes},\mathbf{0},\approx\sqsubseteq)$ is a _partial
Kripke resource monoid_. The compatibility of $\sqsubseteq$ and $\approx$ is
shown in Lemma 22 below, and it relies on showing that the projection is
distributive with the tensor product (Lemma 21).

######  Lemma 21 (Distributivity of Product over Restriction).

Whenever $\mathcal{R}\in\llbracket\Delta\rrbracket$,
$\mathcal{Q}\in\llbracket\Xi\rrbracket$,
$\Theta\sqsubseteq\Delta,\Omega\sqsubseteq\Xi$, and
$\Xi\Join\Delta\downarrow$, it holds that:

$({(\mathcal{Q})^{\Xi}}\mathrel{\otimes}{(\mathcal{R})^{\Delta}})_{\Xi\Join\Delta\to(\Theta\Join\Omega)}=({{(\mathcal{Q})^{\Xi}}}_{{\Xi}\to{\Theta}}\mathrel{\otimes}{{(\mathcal{R})^{\Delta}}}_{{\Delta}\to{\Omega}}).$

###### Proof.

Showing the identity of the final environments is trivial, so we will focus
only on the distribution ensembles. We start by expanding the definition of
$({(\mathcal{Q})^{\Xi}}\mathrel{\otimes}{(\mathcal{R})^{\Delta}})_{\Xi\Join\Delta\to(\Theta\Join\Omega)}$
for a given $n$:

$\displaystyle=\text{bind}((\mathcal{R}\mathrel{\otimes}\mathcal{Q})_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Theta\Join\Omega)})})$
$\displaystyle=u\mapsto\;\;\smashoperator[lr]{\sum_{m\in\llbracket\Xi\Join\Delta\rrbracket_{n}^{\mathtt{d}}}^{}}\;\;{\mathcal{Q}_{n}(m_{\mathsf{dom}(\Xi)})\cdot\mathcal{T}_{n}(m_{\mathsf{dom}(\Delta)})}\cdot{{\text{unit}(m_{\mathsf{dom}(\Theta\Join\Omega)})}}(u)$
$\displaystyle=u\mapsto\;\;\smashoperator[lr]{\sum_{l\in\llbracket{\Xi}\rrbracket_{n}^{\mathtt{d}},w\in\llbracket{\Delta}\rrbracket_{n}^{\mathtt{d}}}^{}}\;\;{\mathcal{Q}_{n}(l)\cdot\mathcal{T}_{n}(w)}\cdot{{\text{unit}((l\cup
w)_{\mathsf{dom}(\Theta\Join\Omega)})}}(u)$
$\displaystyle=u\mapsto\;\;\smashoperator[lr]{\sum_{l\in\llbracket{\Xi}\rrbracket_{n}^{\mathtt{d}},w\in\llbracket{\Delta}\rrbracket_{n}^{\mathtt{d}}}^{}}\;\;{\mathcal{Q}_{n}(l)\cdot\mathcal{T}_{n}(w)}\cdot{{\text{unit}((l_{\mathsf{dom}(\Theta)}\cup
w_{\mathsf{dom}(\Omega)}))}}(u)$

Observe that ${{\text{unit}((l_{\mathsf{dom}(\Theta)}\cup
w_{\mathsf{dom}(\Omega)}))}}(u)$ is equal to:

${{\text{unit}(l_{\mathsf{dom}(\Theta)})}(u_{\mathsf{dom}(\Theta)})\cdot{\text{unit}(w_{\mathsf{dom}(\Omega)})}}(u_{\mathsf{dom}(\Omega)})$

From this observation, the conclusion comes easily, by associativity property
and closing back the definition of projection. ∎

######  Lemma 22 (Compatibility of $\sqsubseteq$ and $\otimes$).

The relation $\sqsubseteq$ and the function $\otimes$ are compatible, i.e.

$\forall s,r,t.s\sqsubseteq r\Rightarrow(s\otimes
t)\downarrow\Rightarrow(r\otimes t)\downarrow\Rightarrow(s\otimes
t)\sqsubseteq(r\otimes t)$

and

$\forall s,r,t.s\sqsubseteq r\Rightarrow(t\otimes
s)\downarrow\Rightarrow(t\otimes r)\downarrow\Rightarrow(t\otimes
s)\sqsubseteq(t\otimes r)$

###### Proof.

We only show the right compatibility, the proof of left compatibility is
analogous. Assume that there are three stores
$s={{(\mathcal{R}_{1})^{\Delta_{1}}}},r={{(\mathcal{R}_{2})^{\Delta_{2}}}},t={{(\mathcal{R}_{3})^{\Delta_{3}}}}$
such that $s\sqsubseteq r$, $(s\otimes t)$ is defined, and $(r\otimes t)$ is
defined. We want to show that:

$\Delta_{1}\Join\Delta_{3}\sqsubseteq\Delta_{2}\Join\Delta_{3},$ (Claim 1)

and that:

$\left(\mathcal{R}_{2}\mathrel{\otimes}\mathcal{R}_{3}\right)_{\Delta_{2}\Join\Delta_{3}\to\Delta_{1}\Join\Delta_{3}}=\mathcal{R}_{1}\mathrel{\otimes}\mathcal{R}_{3}.$
(Claim 2)

Claim 1 is trivial. Claim 2 is a consequence of Lemma 21, which allows us to
show:

$\left(\mathcal{R}_{2}\mathrel{\otimes}\mathcal{R}_{3}\right)_{\Delta_{2}\Join\Delta_{3}\to\Delta_{1}\Join\Delta_{3}}={(\mathcal{R}_{1})}_{\Delta_{2}\to\Delta_{1}}\mathrel{\otimes}(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{3}}.$

By assumption we know that
$\left(\mathcal{R}_{2}\right)_{{\Delta_{2}}\to{\Delta_{1}}}=\mathcal{R}_{1}$,
from Lemma 17 we conclude that

$(\mathcal{R}_{3})_{\Delta_{3}\to\Delta_{3}}=\mathcal{R}_{3}.$

∎

###  4.2 Some Relevant Classes of Formulas

Some properties of CSL we prove in Section 4.3 below only hold for specific
classes of formulas within $\Phi$, which need to be appropriately defined. We
start by the notion of _exact formula_ : intuitively, these formulas describe
_statistical_ properties of distributions rather than _computational_ ones.

We write ${\Phi_{\mathsf{ex}}}$ for the set of exact formulas, i.e., the
smallest subset of $\Phi$ that for every $\Delta$ contains the formulas
${(\top)^{\Delta}}$, ${(\bot)^{\Delta}}$, ${(\mathbf{EQ}(e,g))^{\Delta}}$,
${(\mathbf{IS}(d,c))^{\Delta}}$ and which is closed under additive
conjunction. This means that if ${(\phi)^{\Delta}}$ and ${(\psi)^{\Xi}}$ are
exact, $\Delta\sqsubseteq\Theta$ and $\Xi\sqsubseteq\Theta$, then
${({(\phi)^{\Delta}}\land{(\psi)^{\Xi}})^{\Theta}}$ is also exact.

Crucially, the semantics of exact formulas is not closed with respect to
$\approx$, as shown by the following example:

######  Example 3.

The stores $\mathcal{R}=\left\\{\left\\{(r\mapsto
0^{n})^{1}\right\\}\right\\}_{n\in\mathbb{N}}$ and
$\mathcal{Q}=\left\\{\left\\{(r\mapsto 0^{n})^{1-2^{-n}},(r\mapsto
1^{n})^{2^{-n}}\right\\}\right\\}_{n\in\mathbb{N}}$ are computationally
indistinguishable, but they do not satisfy the same formulas. In particular,
we have $\mathcal{R}\models\mathbf{EQ}(\mathit{setzero}_{n},r)$, _but not_
$\mathcal{Q}\models\mathbf{EQ}(\mathit{setzero}_{n},r)$. More precisely, the
distribution corresponding to the expression ${\mathit{setzero}_{n}}$ is the
Dirac distribution centered on $0^{n}$, which is exactly the same distribution
obtained by evaluating $r$ in $\mathcal{R}$, but not in $\mathcal{Q}$. ∎

Also notice that, in the previous example, if we took
${\mathbf{CI}(\mathit{setzero}_{n},r)}$ instead of
${\mathbf{EQ}(\mathit{setzero}_{n},r)}$, we would have
$\mathcal{R}\models\mathbf{CI}(\mathit{setzero}_{n},r)$, _and_
$\mathcal{Q}\models\mathbf{CI}(\mathit{setzero}_{n},r)$. Specifically, this
would hold because the advantage of any distinguisher for the family of
distributions
$\\{\llbracket\mathit{setzero}_{n}\rrbracket_{n}(\mathcal{R}_{n})\\}_{n\in\mathbb{N}}$
and $\\{\llbracket r\rrbracket_{n}(\mathcal{R})\\}_{n\in\mathbb{N}}$ is 0, and
that of every adversary for the same two expressions evaluated in
$\mathcal{Q}$ is bounded by $2^{-n}$, which is a negligible function. Unlike
_exact formulas_ , formulas like $\mathbf{CI}(\cdot,\cdot)$ do not describe
exact statistical properties of distribution ensembles, but they express
computational properties. For this reason, we call these formulas
_approximate_. The set of _approximate formulas_ is ${\Phi_{\mathsf{ap}}}$,
and it is defined as the largest subset of $\Phi$ where the atomic formulas
$\mathbf{EQ}(e,g)$ and $\mathbf{IS}(d,c)$ do not occur as subformulas. Due to
their computational nature, the semantics of _approximate formulas_ is closed
with respect to $\approx$. This is shown in Lemma 24 below.

###  4.3 Properties of CSL

In this section, we discuss the meta-theoretical properties of CSL. In
particular its semantics enjoys some remarkable closure properties. The most
important is a form of monotonicity with respect to $\sqsubseteq$.
Intuitively, this property states that when two states $s,r$ are such that
$s\sqsubseteq r$, $s$ and $r$ satisfy _related_ formulas. It is not true that
they satisfy the _same_ set of formulas, simply because our semantics relates
states and formulas _on the same environment_ , so states that are defined on
different domains cannot be in relation with the same formulas. However, we
can say that whenever two states $s,r$ are such that $s\sqsubseteq r$ and $s$
satisfies ${(\phi)^{\Delta}}$, then $r$ satisfies a formula ${(\psi)^{\Xi}}$
which is structurally identical to ${(\phi)^{\Delta}}$, but which carries
different environments. This relation between formulas is induced by the store
extension relation $\sqsubseteq$ as follows:

${(A)^{\Delta}}\sqsubseteq{(A)^{\Xi}}\Delta\sqsubseteq\Xi{}\quad{({(\phi)^{\Delta}}*{(\psi)^{\Xi}})^{\Theta_{1}}}\sqsubseteq{({(\phi)^{\Delta}}*{(\psi)^{\Xi}})^{\Theta_{2}}}{\Theta_{1}}\sqsubseteq{\Theta_{2}}$
${({(\phi_{1})^{\Delta_{1}}}\land{(\psi_{1})^{\Xi_{1}}})^{\Theta_{1}}}\sqsubseteq{({(\phi_{2})^{\Delta_{2}}}\land{(\psi_{2})^{\Xi_{2}}})^{\Theta_{2}}}\lx@proof@logical@and{(\phi_{1})^{\Delta_{1}}}\sqsubseteq{(\phi_{2})^{\Delta_{2}}}{(\psi_{1})^{\Xi_{1}}}\sqsubseteq{(\psi_{2})^{\Xi_{2}}}\Theta_{1}\sqsubseteq\Theta_{2}$

By leveraging this relation, we can state the property we were discussing
above as follows:

######  Lemma 23.

For every pair of environments $\Delta,\Xi$, pair of formulas
${(\phi)^{\Delta}}\sqsubseteq{(\psi)^{\Xi}}{}$ and pair of states
$s\in\llbracket\Delta\rrbracket,r\in\llbracket\Xi\rrbracket$ such that
$s\sqsubseteq r$, it holds that
$s\models^{\Delta}{(\phi)^{\Delta}}\Leftrightarrow
r\models^{\Xi}{(\psi)^{\Xi}}$. ∎

The following observations turn out to be useful in the proof of Lemma 23:

######  Remark 4.

${(\phi)^{\Delta}}\sqsubseteq{(\psi)^{\Xi}}\Rightarrow\Delta\sqsubseteq\Xi$.

######  Remark 5.

If two distribution ensembles
$\mathcal{R}\in\llbracket\Delta\rrbracket,\mathcal{Q}\in\llbracket\Xi\rrbracket$
are such that $\mathcal{R}\sqsubseteq\mathcal{Q}$, then for every
$n\in\mathbb{N}$,
${\mathsf{supp}}(\mathcal{R}_{n})=\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\exists
l\in{\mathsf{supp}}(\mathcal{Q}).l_{\mathsf{dom}(\Delta)}=m\\}$.

###### Proof.

From $\mathcal{R}\sqsubseteq\mathcal{Q}$, we deduce that for every
$n\in\mathbb{N}$, $\mathcal{R}_{n}=\text{bind}(\mathcal{Q}_{n},m\mapsto
m_{\mathsf{dom}(\Delta)})$, so the claim becomes

${\mathsf{supp}}(\text{bind}(\mathcal{Q}_{n},m\mapsto{\text{unit}(m_{\mathsf{dom}(\Delta)})}))=\\\
\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\exists
l\in{\mathsf{supp}}(\mathcal{Q}).m_{\mathsf{dom}(\Delta)}=m\\},$

by definition of ${\mathsf{supp}}(\cdot)$, this is equivalent to:

$\left\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\;\;\smashoperator[lr]{\sum_{l\in{\mathsf{supp}}(\mathcal{Q})}^{}}\;\;\mathcal{Q}_{n}(l)\cdot{\text{unit}(l_{\mathsf{dom}(\Delta)})}(m)>0\right\\}=\\\
\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\exists
l\in{\mathsf{supp}}(\mathcal{Q}).l_{\mathsf{dom}(\Delta)}=m\\}.$

In turn, this rewrites as follows:

$\left\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\;\;\;\;\smashoperator[lr]{\sum_{l\in{\mathsf{supp}}(\mathcal{Q})\land
l_{\mathsf{dom}(\Delta)}=m}^{}}\;\;\;\;\mathcal{Q}_{n}(l)>0\right\\}=\\\
\\{m\in\llbracket\Delta\rrbracket_{n}^{\mathtt{d}}\mid\exists
l\in{\mathsf{supp}}(\mathcal{Q}).l_{\mathsf{dom}(\Delta)}=m\\}.$

The equality of these expressions is trivial. ∎

###### Proof of Lemma 23.

By induction on the proof that ${(\phi)^{\Delta}}\sqsubseteq{(\psi)^{\Xi}}{}$.

  * •

If these are atomic formulas, we go by cases on the atomic proposition. We
start by assuming that the proposition is $\mathbf{U}(e)$, and we start from
the left-to-right implication. We assume
$s\models^{\Delta}{(\mathbf{U}(e))^{\Delta}}$, which means that
$\llbracket\Delta\vdash e:\tau\rrbracket(s){}\approx\mathsf{unif}(\tau)$. From
$s\sqsubseteq r$ and Lemma 5, we deduce that $\llbracket\Xi\vdash
e:\tau\rrbracket(r){}=\llbracket\Delta\vdash
e:\tau\rrbracket(s){}\approx\mathsf{unif}(\tau)$, which concludes the proof.
For the opposite direction, if we assume $\llbracket\Xi\vdash
e:\tau\rrbracket(r){}\approx\mathsf{unif}(\tau)$, we can apply Lemma 5 and
conclude that $\llbracket\Delta\vdash
e:\tau\rrbracket(s){}=\llbracket\Xi\vdash
e:\tau\rrbracket(r){}\approx\mathsf{unif}(\tau)$. If the proposition is
$\mathbf{EQ}(e,g)$, from $s\sqsubseteq r$ and Lemma 5, we deduce that
$\llbracket\Xi\vdash e:\tau\rrbracket(r){}=\llbracket\Delta\vdash
e:\tau\rrbracket(s){}$ and that $\llbracket\Xi\vdash
g:\tau\rrbracket(r){}=\llbracket\Delta\vdash g:\tau\rrbracket(s){}$, so in
both the directions the conclusion is a consequence of the transitivity of
identity. The case where the proposition is $\mathbf{CI}(e,g)$ is analogous,
but applying the transitivity of $\approx$ (Lemma 18). Finally, we assume that
the proposition is $\mathbf{IS}(d,c)$. For the left-to-right implication, we
assume that $\mathcal{R}\in\llbracket\Delta\rrbracket$ and
$\mathcal{Q}\in\llbracket\Xi\rrbracket$ with
$\mathcal{R}\models{(\mathbf{IS}(d,c))^{\Delta}}$ and
$\mathcal{R}\sqsubseteq\mathcal{Q}$. The goal is to show
$\mathcal{Q}\models{(\mathbf{IS}(d,c))^{\Xi}}$. Assume this not to hold. This
means that there are $\overline{n}$ and
$\overline{m}\in{\mathsf{supp}}(\mathcal{Q}_{\overline{n}})$ such that
$\llparenthesis d\rrparenthesis_{\overline{n}}(\overline{m})\neq\llparenthesis
c\rrparenthesis_{\overline{n}}(\overline{m})$. Then, we apply 5 to observe
that $\overline{m}_{\mathsf{dom}(\Delta)}\in{\mathsf{supp}}(\mathcal{R})$.
From Lemma 3, we deduce $\llparenthesis
d\rrparenthesis_{\overline{n}}(\overline{m}_{\mathsf{dom}(\Delta)})\neq\llparenthesis
c\rrparenthesis_{\overline{n}}(\overline{m}_{\mathsf{dom}(\Delta)})$, which
contradicts the premise $\mathcal{R}\models{(\mathbf{IS}(d,c))^{\Delta}}$. For
the opposite direction, we assume that
$\mathcal{Q}\models{(\mathbf{IS}(d,c))^{\Xi}}$. To this aim, we fix $n$, and
we let $\overline{m}$ be an element of ${\mathsf{supp}}(\mathcal{R}_{n})$. The
goal is to show that we have $\llparenthesis
d\rrparenthesis_{n}(\overline{m})=\llparenthesis
c\rrparenthesis_{n}(\overline{m})$. From 5, we deduce that there is
$m\in{\mathsf{supp}}(\mathcal{Q}_{n})$ such that
$\overline{m}=m_{\mathsf{dom}(\Delta)}$. From the assumption, we deduce that
$\llparenthesis d\rrparenthesis_{n}(m)=\llparenthesis c\rrparenthesis_{n}(m)$,
so with Lemma 3, we conclude that $\llparenthesis
d\rrparenthesis_{n}(m_{\mathsf{dom}(\Delta)})=\llparenthesis
c\rrparenthesis_{n}(m_{\mathsf{dom}(\Delta)})$, which is equivalent to the
claim because we assumed that $\overline{m}=m_{\mathsf{dom}(\Delta)}$.

  * •

If these are ${(\top)^{\Delta}}$ or ${(\bot)^{\Delta}}$, the conclusion is
trivial.

  * •

If the two formulas are additive conjunctions, then we start from the left to
right implication. Assume
$s\models^{\Delta}{({(\phi_{1})^{\Delta_{1}}}\land{(\psi_{1})^{\Xi_{1}}})^{\Delta}}$,
so we deduce that $s_{1}\models^{\Delta_{1}}{(\phi_{1})^{\Delta_{1}}}$ and
$s_{2}\models^{\Xi_{1}}{(\psi_{1})^{\Xi_{1}}}$ with
$s_{1}=s_{\Delta\to\Delta_{1}}=(r_{\Xi\to\Delta})_{\Delta\to\Delta_{1}}=r_{\Xi\to\Delta_{1}}$,
and
$s_{2}=s_{\Delta\to\Xi_{1}}=(r_{\Xi\to\Delta})_{\Delta\to\Xi_{1}}=r_{\Xi\to\Xi_{1}}$
by definition of $\sqsubseteq$ and Lemma 16. From
${(\phi_{1})^{\Delta_{1}}}\sqsubseteq{(\phi_{2})^{\Delta_{2}}}$ and
${(\psi_{1})^{\Xi_{1}}}\sqsubseteq{(\psi_{2})^{\Xi_{2}}}$, we can conclude
that $\Xi_{1}\sqsubseteq\Xi_{2}$ and that $\Delta_{1}\sqsubseteq\Delta_{2}$
using 4. For this reason, we can apply the IHs to the rule’s premises, to
conclude $r_{\Xi\to\Delta_{2}}\models^{\Delta_{2}}{(\phi_{2})^{\Delta_{2}}}$
and $r_{\Xi\to\Xi_{2}}\models^{\Xi_{2}}{(\psi_{2})^{\Xi_{2}}}$, which
concludes the proof. For the opposite direction, we assume that
$r\models^{\Xi}{({(\phi_{2})^{\Delta_{2}}}\land{(\psi_{2})^{\Xi_{2}}})^{\Xi}}$,
By definition of the semantic relation and by definition of $\sqsubseteq$, we
deduce that:
$r_{\Xi\to\Delta_{2}}\models^{\Delta_{2}}{(\phi_{2})^{\Delta_{2}}}$ and
$r_{\Xi\to\Xi_{2}}\models^{\Xi_{2}}{(\psi_{2})^{\Xi_{2}}}$. From
${{({(\phi_{1})^{\Delta_{1}}}\land{(\psi_{1})^{\Xi_{1}}})^{\Delta}}}\sqsubseteq{{({(\phi_{2})^{\Delta_{2}}}\land{(\psi_{2})^{\Xi_{2}}})^{\Xi}}}$,
we deduce that ${(\phi_{1})^{\Delta_{1}}}\sqsubseteq{(\phi_{2})^{\Delta_{2}}}$
and ${(\psi_{1})^{\Xi_{1}}}\sqsubseteq{(\psi_{2})^{\Xi_{2}}}$, so we can
conclude that $\Xi_{1}\sqsubseteq\Xi_{2}$ and that
$\Delta_{1}\sqsubseteq\Delta_{2}$, 4. These observations allow us to apply the
IHs on the pair of states $(r_{\Xi\to\Delta_{2}},r_{\Xi\to\Delta_{1}})$, and
$(r_{\Xi\to\Xi_{2}},r_{\Xi\to\Xi_{1}})$, to show that
$r_{\Xi\to\Delta_{1}}\models^{\Delta_{1}}{(\phi_{1})^{\Delta_{1}}}$ and
$r_{\Xi\to\Xi_{1}}\models^{\Xi_{1}}{(\psi_{1})^{\Xi_{1}}}$. This also shows
that $s_{\Delta\to\Delta_{1}}\models^{\Delta_{1}}{(\phi_{1})^{\Delta_{1}}}$
and $s_{\Delta\to\Xi_{1}}\models^{\Xi_{1}}{(\psi_{1})^{\Xi_{1}}}$, because
$r_{\Xi\to\Delta_{1}}=(r_{\Xi\to\Delta})_{\Delta\to\Delta_{1}}=s_{\Delta\to\Delta_{1}}$
and
$r_{\Xi\to\Xi_{1}}=(r_{\Xi\to\Delta})_{\Delta\to\Xi_{1}}=s_{\Delta\to\Xi_{1}}$,
for Lemma 16. This concludes the proof.

  * •

If the two formulas are two separating conjunctions, then we start from the
left to right implication. Assume
$s\models^{\Delta}{({(\phi_{1})^{\Theta}}*{(\psi_{1})^{\Omega}})^{\Delta}}$,
so we deduce that $s_{1}\models^{\Theta}{(\phi_{1})^{\Theta}}$ and
$s_{2}\models^{\Omega}{(\psi_{1})^{\Omega}}$ with $s_{1}\otimes
s_{2}\approx\sqsubseteq s\sqsubseteq r$. So, we conclude
$r\models^{\Xi}{({(\phi)^{\Theta}}*{(\psi)^{\Omega}})^{\Xi}}$. For the
opposite direction, we assume that there are
$r_{1}\models^{\Theta}{(\phi_{1})^{\Theta}}$ and
$r_{2}\models^{\Omega}{(\psi_{1})^{\Omega}}$ with $r_{1}\otimes
r_{2}\approx\sqsubseteq r$. From the last observation and the definitions of
$\approx$ and $\sqsubseteq$, we can deduce that
$r_{\Xi\to\Theta\Join\Omega}\approx r_{1}\otimes r_{2}$. We also know that
${{({(\phi_{1})^{\Theta}}*{(\psi_{1})^{\Omega}})^{\Delta}}}$ is a formula,
which means that $\Theta\Join\Omega\sqsubseteq\Delta$. So, by applying Lemma
16 we can conclude that $r_{1}\otimes r_{2}\approx
r_{\Xi\to\Theta\Join\Omega}=(r_{\Xi\to\Delta})_{\Delta\to\Theta\Join\Omega}=(s)_{\Delta\to\Theta\Join\Omega}$
which concludes the proof.

∎

The approximate fragment of CSL also enjoys good properties with respect to
$\approx$. In particular, if two states $s$ and $r$ are cryptographically
indistinguishable, and one of these satisfies a formula
${(\phi)^{\Delta}}\in{\Phi_{\mathsf{ap}}}$, then also the other satisfies
${(\phi)^{\Delta}}$. This is stated in Lemma 24.

######  Lemma 24.

For every environment $\Delta$, and every _approximate formula_
${(\phi)^{\Delta}}\in{\Phi_{\mathsf{ap}}}$ and pair of states
$s,r\in\llbracket\Delta\rrbracket$ such that $s\approx r$, it holds that
$s\models^{\Delta}{(\phi)^{\Delta}}\Rightarrow
r\models^{\Delta}{(\phi)^{\Delta}}$. ∎

###### Proof of Lemma 24.

By induction on the proof that ${(\phi)^{\Delta}}$ is a formula.

  * •

If ${(\phi)^{\Delta}}$ is an atomic formula, we go by cases on the atomic
proposition. Now assume that the formula is ${(\mathbf{U}(e))^{\Delta}}$. We
assume $s\models^{\Delta}{(\mathbf{U}(e))^{\Delta}}$, which means that
$\llbracket\Delta\vdash e:\tau\rrbracket(s){}\approx\mathsf{unif}(\tau)$. From
$s\approx r$ and Lemma 2, we deduce that $\llbracket\Delta\vdash
e:\tau\rrbracket(r){}\approx\llbracket\Delta\vdash
e:\tau\rrbracket(s){}\approx\mathsf{unif}(\tau)$, which concludes the proof.

  * •

If ${(\phi)^{\Delta}}$ is ${(\top)^{\Delta}}$ or ${(\bot)^{\Delta}}$, the
conclusion is trivial.

  * •

If the formula is an additive conjunction, we assume