{'fraction_non_alphanumeric': 0.04864748290097973, 'fraction_numerical': 0.010012939799125023, 'mean_word_length': 3.8635001498351813, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 37, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Proving uniformity and independence by self-composition and coupling

Proof by coupling is a powerful technique for proving probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. Couplings have also proved to be a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be also used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL---whose proofs correspond to proofs by coupling---can be used for proving uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.


Introduction
Uniformity and probabilistic independence are two of the most useful and commonly encountered properties when analyzing randomized computations. Uniform distributions are a central building block of randomized algorithms-arguably the simplest non-trivial distribution, the coin flip, is a uniform distribution over two values. Given access to uniform samples, there are known transformations for converting the samples to simulate more complex distributions, like the Gaussian or Laplace distributions. In the other direction, turning samples from various nonuniform distributions into uniform samples is an active area of research.
Probabilistic independence is no less central, enabling a property involving two random variables to be split into two properties involving a single random variable. For instance, we can decompose the probability of a conjunction as the product of the marginal probabilities. Independent random variables can also be analyzed with the help of more sophisticated tools, like concentration inequalities.
Given these and other applications, it is not surprising that researchers have investigated different methods of reasoning about uniformity and independence. For instance, Pearl and Paz [17] develop an axiomatic theory based on graphoids for modeling conditional independence in probability theory. However, proving uniformity and independence in program verification remains a challenging task. Most program logics for probabilistic programs do not treat these properties as first-class assertions, and provide reasoning principles that are cumbersome to use. Often, one must prove exact values for the probability of specific events.
For example, consider any logical formalism for proving properties of the form Pr s m [E] = p, which capture the fact that the event E has probability p in the distribution obtained by executing the randomized program s on some initial memory m; many proposed systems fall into this class [8,12,14,16,18,19]. Suppose that we want to prove that the program variable x of finite type A is uniformly distributed w.r.t. the output distribution s m . The most direct way to show this property is to analyze the probability of each output: for every a ∈ A, Pr s m [x = a] = 1 |A| .

arXiv:1701.06477v1 [cs.PL] 23 Jan 2017
For independence, the situation is similar. Assume that we want to prove that the two program variables x and y of respective types A and B are probabilistically independent w.r.t. the output distribution s m . This can be done by exhibiting functions f, g, h such that for every a ∈ A and b ∈ B, we have: Pr s m [x = a] = f (a), Pr s m [y = b] = g(b), Pr s m [x = a ∧ y = b] = h(a, b). Then, independence between x and y holds iff h(a, b) = f (a) · g(b) for every a ∈ A and b ∈ B.
While these approaches can work, they can be laborious in practice. It may be awkward to directly compute the probability of x = a, and the functions f , g and h may be difficult to produce. We propose an alternative method based on probabilistic couplings for proving uniformity and independence. Probabilistic couplings are a classical method for proving sophisticated probabilistic properties (e.g., stochastic dominance, rapid mixing of Markov chains, and more [15,20,21]). More recently, couplings have been used to reason about relational properties of probabilistic programs, notably differential privacy [3,4]. Here we show that uniformity and independence properties can also be verified using coupling, despite being non-relational properties. As a consequence, our verification method inherits the advantages of reasoning by couplings: compositional reasoning, and no need to reason directly about probabilistic events. More specifically, we demonstrate that uniformity and independence can be captured in the relational program logic pRHL [1].
Uniformity. Suppose we have a program s with a program variable x ranging over a finite set A, and we want to show that x is distributed uniformly over A after executing s. Rather than computing the probability of Pr s m [x = a] for each a ∈ A, it suffices to show that the probabilities of any two outputs are equal: Now, we can view uniformity as a relational property: if we consider two runs of s, then the probability of x being a 1 in the first run should be equal to the probability of x being a 2 in the second run. In pRHL, this property is described by the following judgment: where the assertion φ asserts that the initial states are equal.
Independence. Proving probabilistic independence is more involved, as it is unclear how to encode independence in pRHL. Nevertheless, we can prove independence in two different ways. Assume that we want to prove that the program variables x and y of respective finite types A and B are independent. First, if the distribution of x, y is uniformly distributed over A × B, then x and y are independent (and themselves uniformly distributed). Indeed, assume that for all a ∈ A and b ∈ B we have Pr A similar argument applies to the probability that y = b, from which independence follows. Thus, our first method of proving independence is by reduction to uniformity.
This approach is simple to use, but it only applies to proving independence of uniform random variables. A different approach is to express probabilistic independence as a property of a modified version of the program, without any requirement on uniformity. More specifically, independence of x and y can be derived from the equality between the probabilities of x = a ∧ y = b and x 1 = a ∧ y 2 = b, where in the first case the probability is taken over the output of the original program s, and in the second case the probability is taken over the output of the program s 1 ; s 2 , where s 1 and s 2 are renamings of s; we call s 1 ; s 2 a self-composition of s [2,11]. The reason is not hard to see. Since the composed programs operate on disjoint memory, the final combined output distribution models two independent runs of the original program s. So, the probability Pr s1;s2 m 1 m 2 [x 1 = a ∧ y 2 = b]-m 1 m 2 is the disjoint union of two copies of m-is equal to the product of Pr s1 m 1 [x 1 = a] and Pr s2 m 2 [y 2 = b]. Since s 1 and s 2 both model the original program s, this probability is in turn equal to Pr s m [x = a] and Pr s m [y = b] in the original program.
Our encoding casts independence as a relational property between a program s and its self-composition s 1 ; s 2 , a property which can be directly expressed in the relational program logic pRHL [1]: where the precondition φ captures the initial conditions. We show that our approach extends to independence and conditional independence of sets of program variables.
Outline Sections 2 and 3 provide the relevant mathematical background and introduce the setting of our work. Section 4, 5 and 6 respectively address the case of uniformity, independence, and conditional independence. In each case we demonstrate our method using classic examples of randomized algorithms. We conclude the paper with a discussion of alternative frameworks for verifying these properties.

Mathematical background
For the sake of simplicity, we restrict ourselves to discrete (countable) sub-distributions.
Definition 1. A sub-distribution over a set A is defined by a mass function µ : A → R + , which gives the probability of the unitary events a ∈ A. This mass function must be s.t. a∈A µ(a) is well-defined and the weight satisfies |µ| = a∈A µ(a) ≤ 1. In particular, the support of the sub-distribution supp(µ) = {a ∈ A | µ(a) = 0} is discrete. When |µ| is equal to 1, we call µ a distribution. We let D(A) denote the set of sub-distributions over A. An event over A is a predicate over A. The probability of an event E w.r.t. a sub-distribution µ, written Pr x∼µ [E], is defined as {x∈A|E(x)} µ(x).
In addition to the general definition, we shall also consider a special case of coupling: specifically, we say that (µ 1 , µ 2 ) are f -coupled if f : A 1 → A 2 is a bijection such that µ 1 (x) = µ 2 (f (x)) for every x ∈ A 1 . In this case, we write f µ 1 & µ 2 . One useful consequence of couplings is that they can show that one event has smaller probability than another.
Lemma 3 (Fundamental lemma of coupling). Let E 1 and E 2 be predicates over A 1 and A 2 , and One can immediately derive a variant of the lemma where ⇐⇒ and = are used in place of ⇒ and ≤ respectively. The following lemma provides a converse to the fundamental lemma of coupling in the special case where we are interested in proving the equality of two distributions.
Lemma 4. For every µ 1 , µ 2 ∈ D(A), the following are equivalent: We note that the third item (existence of liftings for pointwise equality) is often easier to establish than the last item (existence of lifting for equality), since one can choose the coupling for each possible value of a, rather than showing a single coupling for all values of a.

Setting
We will work with a simple probabilistic imperative language. Probabilistic assignments are of the form x $ ← g, which assigns a value sampled according to the distribution g to the program variable x. The syntax of statements is defined by the grammar: where x, e and g respectively range over (typed) variables in X , expressions in E and distributions in D. To ensure that the set of states is countable, we require that there are finitely many variables X . As usual E is defined inductively from X and a set F of simply typed function symbols. In this paper, distributions used for sampling are either uniform distributions over a finite type A, or the Bernoulli distribution with parameter p, which we denote by Bern(p). We assume that expressions and statements are typed in the usual way. We assume we are given a set-theoretical interpretation for every type and operator of the language. We define a state as a type-preserving mapping from variables to values, and we let State denote the set of states. The set of states is equipped with the usual functions for reading and writing a value; we use m(x) to denote the value of x in m, and m[x := v] to denote state update, in this case the state obtained from m by updating the value of x with v.
One can equip D(State) with a monadic structure, using the Dirac distributions δ x for the unit and distribution expectation E x∼µ [M (x)] for the bind, where The semantics of expressions and distribution expressions is parametrized by a state m, and is defined in the usual way where we require all distribution expressions to be interpreted as distributions (rather than sub-distributions).

Definition 5 (Semantics of statements).
• The semantics s m of a statement s w.r.t. to some initial state m is a sub-distribution over states, and is defined by the clauses of Figure 1.
n times s; . . . ; s. • The (lifted) semantics s µ of a statement s w.r.t. to some initial sub-distribution µ over states is a sub-distribution over states, and is defined as A basic and highly important property of probabilistic programs is termination. We say that a program s is lossless if for every initial memory m, | s m | = 1. By now, there are many sophisticated techniques for proving losslessness even for languages that allow both probabilistic sampling and non-determinism (including recent advances by Chatterjee et al. [9,10], Ferrer Fioriti and Hermanns [13]). These techniques are capable of showing losslessness for all of our examples (in some cases with a high degree of automation), so throughout the paper, we assume that all programs are lossless. This assumption is used in the rules of pRHL and the characterizations of uniformity and independence.

Self-composition of programs
For every program s and n ∈ N, we let s n denote the n-fold self-composition of s, i.e. s n = s 1 ; . . . , s n , where each s ı is a copy of s where all variables are tagged with a superscript ı. In order to state the main property of self-composition, we define the self-composition of a state; given a state m, we define its n-fold self-composition m n as the state from X n to values, where X n = {x ı | x ∈ X , 1 ≤ ı ≤ n} such that for every x and ı, m n (x ı ) = m(x). Given a state m from X n , we denote by m ı the ı-th projection of m. Proposition 6. For every program s and state m where the event E ı is defined by E ı (m n ) = E(π ı (m )) for every ı and π ı is the projection from a self-composed state to its ı-th component.

Probabilistic Relational Hoare Logic
Probabilistic Relational Hoare Logic (pRHL) is a program logic for reasoning about relational properties of probabilistic programs. Its judgments are of the form s 1 ∼ s 2 : φ =⇒ ψ, where s 1 and s 2 are commands and the pre-condition φ and the post-condition ψ are relational assertions, i.e. first-order formulae built over generalized expressions. The latter are similar to expressions, except that each variable is tagged with 1 or 2 to indicate the execution that it belongs to; we call the two executions left and right. Generalized expressions are interpreted w.r.t. a pair (m 1 , m 2 ) of states, where the interpretation of the tagged variables x 1 and x 2 m 1 (x) and m 2 (x) respectively. We write (m 1 , m 2 ) φ to denote that the interpretation of the assertion φ w.r.t. (m 1 , m 2 ) is valid. Figure 2 presents the main rules of the logic. This includes two-sided rules, which operate on both programs, and one-sided rules, which operate on a single program (left or right). Note that the rule [Struct] uses an auxiliary judgment that captures program equivalence and is defined in Figure 3. Note that structural rules include rules for loop splitting and swapping programs that operate on disjoint parts of the state, where var(s) denotes the set of variables read and written by the statement s. We refer to Barthe et al. [1,6] for an explanation of the rules.
Throughout the paper, we often assert that the left and the right copies of a state are equal. This is captured by the relational assertion EqMem = x∈X x 1 = x 2 . We also often assert cross-equality on n-fold composition of states EqMem p , q = x∈X ,1≤ı≤p,1≤≤q x ı 1 = x  2 .

Uniformity
Reasoning about probabilistic programs often requires establishing that a set of program variables (each ranging over a finite type) is uniformly distributed: Note that the definition of uniformity (and in later sections of independence) naturally extends to sets of expressions, and so do our characterizations.

Characterization
The following proposition characterizes uniformity in terms of couplings. Proposition 9 (Uniformity by coupling). Let X = {x 1 , . . . , x n } be a set of variables of respective finite types A 1 , . . . , A n . For every program s, the following are equivalent: 1. for every state m, X is uniformly distributed w.r.t. s m ; 2. for every two tuples (a 1 , . . . , a n ), (a 1 , . . . , a n ) ∈ A 1 × . . . × A n , Proof. Follows directly from properties of coupling.
By expressing uniformity as a coupling property, we can use pRHL to prove uniformity. To demonstrate the technique, we consider classical examples randomized algorithms.

Simulating a fair coin
ret ← (l, l + 1) Figure 5: Cyclic random walk This example considers a process for simulating a fair coin using a biased coin. The idea is simple: 1) toss the coin twice; 2) if the two outcomes differ, return the value of the first coin; 3) if the two outcomes match, repeat from step 1. The algorithm does not require the bias of the coin to be known, as long as it is some constant bias and there is positive probability of returning 0 and 1. This process can be modelled by the program s from Figure 4, where 0 < p < 1 is a real parameter modeling the probability of the biased coin to return 0 (tail). Our goal is to establish the trivial judgment { } s { } and the following pRHL judgment: By the fundamental lemma of the coupling, this implies that Pr s m [x = 1] = Pr s m [x = 0], and hence that x is uniformly distributed upon termination. The proof proceeds by establishing the following invariant: x 2 = if x 1 = y 1 then y 2 else ¬x 1 Validity of the invariant entails that the desired postcondition holds on program exit, as the invariant and the negation of the loop guard hold. The invariant holds on entering the loop, so we only need to prove that it is preserved by the loop body. The proof proceeds as follows: first, we swap the two random assignments on the right, leading to the judgment: where φ denotes the loop invariant and φ denotes its strengthening by the loop guard-we do not need the precondition, since the values are freshly sampled in the body. Next, we apply the [Rand] rule twice, with the identity bijection. This yields as precondition the tautology:

Cyclic random walk
Consider a random walk over a cyclic path composed of n nodes labeled 0, 1, . . . , n − 1: starting from position 0, at each step, we flip a fair coin over {−1, 1} and update the position accordingly to the result of the coin flip. To take into account that we are on a cyclic structure, all arithmetical operations are in the cyclic ring Z/ nZ -i.e. are performed modulo n. At each iteration, when moving between two contiguous positions over the circle, we consider that the random walk visited the arc between the two nodes. We want to show that the last visited arc is uniformly distributed. Figure 5 (left) gives a graphical representation of the random walk, where c is the random walk position and the red arc is the last visited arc when c moved from 0 to 1. This random walk can be seen as a simple version of sampling a uniformly random spanning tree on a graph. While Broder [7] analyzes the general problem, we can verify uniformity for the cyclic random walk with couplings. The proof proceeds as follows. We first execute asynchronously the two random walks until they eventually synchronize respectively on the arcs (a, a+1) and (b, b+1). At that point, we are in one of the following cases: either the random walks synchronize on the same side of the arcs (a, a + 1) and (b, b + 1); either they synchronize on opposite sides. (These cases are examplified in the diagrams on the left, where the arc we want to synchronize on is in red). From that point, we execute the two processes resp. in lock-step (if they synchronized on the same side) or anti-lock-step (if they did not). At some point, both processes will visit the other side of the arcs (a, a + 1) and (b, b + 1), and since they execute in (anti)-lock-step, these events will occur synchronously. At that point, either the processes finished their walk and they resp. return the arcs (a, a + 1) and (b, b + 1) as their result (case (i) of the right diagram below); either they have other nodes to visit and they will not resp. return the arcs (a, a + 1) and (b, b + 1) (case (ii) of the same diagram). We now detail the formal proof. Consider the program of Figure 5, where all arithmetical operations are done modulo n. This algorithm instruments the random walk with two points f and l representing the range [f, l] (using clockwise ordering) of all the points that have been visited by the walk. When all nodes of the cycle have been visited (i.e. when l + 1 = f ), the arc between l and l + 1 is the only arc that has not been visited by the walk. Let s be the program of Figure 5 and s the loop body of the single loop of s. We want to show that the final arc ret-the only arc that has not been marked-is uniformly distributed among all arcs. Uniformity of ret is entailed by the following judgment: First, we make use of the loop splitting equivalence rules to transform the main loop into three pieces. We transform the loop in the left program into:  (c 1 , c 2 ) are contained in the range of visited arcs. Next, we show that after the two second loops the following relational invariant is satisfied: After the second loop, there are two cases for the third loop. If l 1 = a, we have l 2 = b, f 1 = a + 1 (since a + 1 is visited in 1 ) and f 2 = b + 1. In that case, which correspond to the case (i) of the last diagram, the third loops both exit immediately and the random walks resp. return the arcs (a, a + 1) and (b, b + 1). Otherwise, we have l 1 = a and l 2 = b, and we can show, using the rules [While-L] and [While-R], that l 1 (resp. l 2 ) will never be set to a (resp. b). In that case, which correspond to the case (ii) of the last diagram, we can show that the walks resp. return arcs distinct from (a, a + 1) and (b, b + 1).
We now focus on the the second loops, relating them with the two-sided variant of the [While] rule. The particular coupling we choose will depend on the the current positions in the two sides at the start of the second loops. If a ∈ [f, l] 1 and b ∈ [f, l] 2 then we have l 1 = a and l 2 = b (since a + 1 / ∈ [f, l] 1 ) and we couple the walks to make identical moves. In that case, the key part of the loop invariant is: The first line enforces some structural invariant and the second line enforces that both walks make identical moves, relatively to a and b. The main difficulty is to show that both loops are synchronized. Note that there are two reasons the loop may exit. If l has been incremented, then the increment will be done on both side. Otherwise, if f has been decremented to a + 1, then we have c 1 = f 1 = a + 2, so c 1 − a = c 2 − b = 2 and c 2 = b + 2 and the right loop will also decrement f to b + 1. The case a + 1 ∈ [f, l] 1 and b + 1 ∈ [f, l] 2 is very similar, by reversing the roles of f and l. The remaining two cases, a + 1 ∈ [f, l] 1 and b ∈ [f, l] 2 or a ∈ [f, l] 1 and b + 1 ∈ [f, l] 2 is similar except that we force the walks to be execute in anti-lock-step. Using the rule [Case], we put together these four cases and we conclude by application of the rule for sequence.

Ballot Theorem
So far, we have shown how couplings can be used to prove that a set of program variables is uniformly distributed. Couplings can also be used for showing that two events have the same probability, as shown by the following example.
Example 10 (Ballot Theorem). Assume that voters must choose between two candidates A and B. The outcome of the vote is n A votes for A and n B votes for B, with n A > n B . Assuming that the order in which the votes are cast is uniformly random, the probability that A is always strictly ahead in partial counts is (n A −n B ) /(n A +n b ).
The process can be formalized by the program from Figure 6. Here we use the list l to store intermediate results. Using l i to denote the i-th element of the list l, the Ballot Theorem is captured by the statement: There exist many proofs of the Ballot's Theorem; we focus on the so-called Andre's reflection method. The crux of the method is a coupling proof of the following fact: "bad" sequences starting with a vote to to the loser are equiprobable with "bad" sequences starting with a vote to the winner, where a sequence of votes is "bad" if there is a tie at some point in the partial counts. Let φ = ( 1≤i≤n l i = 0) and ψ = x A = n A ∧x B = n B . The above facts are captured by the pRHL judgment (universally quantified over n A and n B such that n A > n B ): s ∼ s : It follows from the properties of coupling that for every n A and n B such that n A > n B , In terms of conditional probabilities, we have Pr . Now observe that any sequence that starts with a vote to B (i.e. the loser) is necessarily bad. Therefore, By the above and elementary properties of conditional independence: Note that the probability in the right-hand side of the last equation represents the probability that the first vote goes to the loser, conditional on ψ. This turns out to be exactly n B n A +n B , so we conclude that Pr s m [φ | ψ] = 2 · n B n A +n B or equivalently Pr s m [¬φ | ψ] = n A −n B n A +n B as desired. We now turn to the proof of the pRHL judgments. By symmetry it suffices to consider the first judgment. Using the rule of consequence and the elimination rule for universal quantification, it suffices to prove for every i: We couple the samplings of x using the negation function until |l| = i, and then with the identity bijection. This establishes the following loop invariant, from which we can conclude:

Independence
We now turn to characterizing probabilistic independence using couplings. We focus on probabilistic independence of program variables, a common task when reasoning about randomized computations. In our setting, the textbook definition of probabilistic independence can be cast as follows: Definition 11. A set X = {x 1 , . . . , x n } of program variables of types A 1 , . . . , A n is probabilistically independent w.r.t. a distribution µ ∈ D(State) iff for every (a 1 , . . . , a n ) ∈∈ A 1 × . . . × A n :

Characterization
Our first characterization of independence is based on the observation that uniformity entails independence.
Fact 12 (Independence from uniformity). From every state m, if X is uniform w.r.t. s m then X is independent w.r.t. s m .
This observation enables proving independence by coupling, in the special case where variables are uniform and independent. For the general case, we will use an alternative characterization based on self-composition.
Proposition 13 (Independence by coupling). The following are equivalent: 1. for every state m, X is independent w.r.t. s m ; 2. the following judgment, between a single copy of the program on the one hand and a n-fold copy on the other hand, is derivable for every (a 1 , . . . , a n ) ∈ A 1 × . . . × A n : Proof. The validity of the universally quantified pRHL judgment is equivalent to the following statement: for every a 1 , . . . , a n and n-fold copy m n of some initial state m, The last equality comes from the property of n-fold self-composition 6.

Figure 7: Pairwise independence
Our first example is a well-known algorithm for generating 2 n pairwise independent bits. The algorithm first samples n independent bits b 1 . . . b n , and then defines for every subset X ⊆ {1, . . . , n} the bit z X = i∈X b i . We can prove pairwise independence of the computed bits, i.e. for every X = Y , z X and z Y are independent. Since there are 2 n subsets of {1, . . . , n}, this gives us 2 n pairwise independent bits constructed from n independants bits. The algorithm is encoded by the program s in Figure 7, where bits maps {0, . . . , 2 n − 1} to a subset in P({1, . . . , n}) of positions that are 1 in the binary representation, and for i = a to b do s is usual syntactic sugar for while loop with an incrementing counter i. By our characterization based on self-composition, pairwise independence of z j and z j for every j = j is equivalent to the (universally quantified) pRHL judgment: Since j = j , the two sets bits(j) and bits(j ) must differ in at least one element. Let k 0 be the smallest element in which they differ. Without loss of generality, we can assume that k 0 / ∈ bits(j) and k 0 ∈ bits(j ). The crux of the proof is to establish the following judgment: where z = k∈bits(j) b k , z = k∈bits(j ) b k and z = k∈bits(j ) b k and This is proved coupling the variables of the two programs in an appropriate way. We couple the random samplings as follows: • for every k = k 0 , we couple b k 1 and b k 2 using the identity sampling; • we use the Rnd-R rule for b k 2 for every k = k 0 ; • we couple b k0 1 and b k0 2 with the bijection which ensures: Putting everything together, we obtain a proof obligation whose validity follows from the algebraic properties of ⊕. The previous example can be generalized to achieve k-wise independence for general k. Suppose we wish to generate n random variables that are k-wise independent. We will work in Z/pZ, the field of integers modulo a prime p, such that k ≤ p. Let a 0 , . . . , a k−1 be drawn uniformly at random from Z/pZ and define the family of random variables for every m ∈ {1, . . . , n}:

k-wise independence
where we take 0 0 = 1 by convention. The corresponding code is given in Figure 8. Then, we can show that any collection of k distinct variables {x i } i is independent.
For simplicity, we will show that the first k elements x 0 , . . . , x k−1 are uniform, and hence independent. Let v 0 , . . . , v k−1 ∈ Z/ nZ be arbitrary elements of the field. Then the probability that (x 0 , . . . , x k−1 ) = (v 0 , . . . , v k−1 ) is equal to p −k . Indeed, the equations define a system of linear equations with variables a 0 , . . . , a k−1 . By basic linear algebra the system of equations has a unique solution for the variables a 0 , . . . , a k−1 , 1 which we denote (v * 0 , . . . , v * k−1 ). Now consider the pRHL judgment that establishes uniformity: By applying (relational) weakest precondition on the deterministic fragments of the program, the judgment is reduced to We then repeatedly apply the rule for random sampling, with the permutation on Z/pZ that exchanges (v * i , w * i ).

Conditional independence
We also consider conditional independence. Recall that the conditional probability Definition 14. Let X = {x 1 , . . . , x n } be a set of program variables of types A 1 , . . . , A n and let E be an event. We say that X probabilistically independent conditionally on E w.r.t. a distribution µ ∈ D(State) iff for every (a 1 , . . . , a n ) ∈ A 1 × . . . × A n : In the above definition, we are implicitly assuming that Pr µ [E] = 0.
The following lemma unfolds the definition of conditional independence and is useful for the characterization of the next section. i! Note that p does not divide the determinant by Gauss' lemma, since n can't divide any of the terms i! for any i < n. Therefore, the system of equations has a unique solution.
Lemma 15. A set of variables X is conditionally independent on an event E w.r.t. µ iff for every a 1 ∈ A 1 , . . . , a n ∈ A n :

Characterization
The characterization of independence based on self-composition can be extended as follows.
Proposition 16 (Conditional independence by coupling). The following are equivalent: 1. for every state m, X is independent conditionally on E w.r.t. s m ; 2. s n ∼ s n : EqMem n , n =⇒ ( Proof. The proof is similar to the case of independence.

Example: conditional independence
x $ ← µ; y $ ← µ ; z $ ← µ ; w ← f (x, y); w ← g(y, z); We consider a simple example often used to illustrate Bayesian networks models. Let y, w, and w be random variables. y is sampled from a fixed distribution µ. Both w and w depend on y, along with independent sources of randomness, respectively x and z. While w and w are not independent-they share dependence on y-if we condition on a particular value of y, then w and w are independent.
The code of the corresponding program s is given in Figure 9. We want to show that w and w are independent conditioned on y = c for every c. Using our characterization based on self-composition, it amounts to proving the following (universally quantified) pRHL judgment: The proof proceeds by moving the samplings of z 1 and z 2 in both programs to the front of the program, and then swapping samplings in the left program only (we can use the rule [Swap] to reorder the instructions). Then, we couple z 1 1 to be equal to z 2 2 , and z 2 1 to be equal to z 1 2 . We apply the identity coupling to all other random samplings.

Conclusion
We have proposed a new lightweight method based on probabilistic couplings for proving uniformity and independence properties of probabilistic programs. An interesting direction for future work would be to combine our method with recent work for proving accuracy bounds for deferentially private computations [5]. The combined techniques could verify more precise accuracy bounds, by using independence and concentration bounds.