Gilles Barthe

Charlie Jacomme

Steve Kremer

Universal equivalence and majority of probabilistic programs over nite elds

We study decidability problems for equivalence of probabilistic programs, for a core probabilistic programming language over nite elds of xed characteristic. The programming language supports uniform sampling, addition, multiplication and conditionals and thus is su ciently expressive to encode boolean and arithmetic circuits. We consider two variants of equivalence: the rst one considers an interpretation over the nite eld F 𝑞 , while the second one, which we call universal equivalence, veri es equivalence over all extensions F 𝑞 𝑘 of F 𝑞 . The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of F 2 𝑘 for any 𝑘. While the rst problem is obviously decidable, we establish its exact complexity which lies in the counting hierarchy. To show decidability, and a doubly exponential upper bound, of the universal variant we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. Finally we study several variants of the equivalence problem, including a problem we call majority, motivated by di erential privacy.

Introduction

Program equivalence is one of the most fundamental tools in the theory of programming languages and arguably the most important example of relational property. Program equivalence has been studied extensively, leading to numerous decidability results and sound proof methods. This paper is concerned with the decidability of equivalence and relational properties for a core imperative probabilistic programming language. Like many other probabilistic programming languages, our language supports sampling from distributions, and conditioning distributions on an event. The speci city of our language is that it operates over nite elds of the form F 𝑞 𝑘 . Therefore, expressions are interpreted as polynomials and assertions are boolean combinations of polynomial identities. Sampling is interpreted using the uniform distributions over sets de ned by assertions, and branching and conditioning are relative to assertions.

We consider two relational properties, equivalence and majority, which we de ne below, and several related properties, which we explain in the next paragraph. For each property, we consider two variants of the problem. In the rst variant, which we call the xed case, the value of 𝑘 is xed. In the second variant, which we call the universal variant, we require the property to hold for all possible values of 𝑘. Consider two programs 𝑃 1 and 𝑃 2 with 𝑚 inputs and 𝑛 outputs. These programs are interpreted as functions [

P{ ì 𝑥 = ì 𝑏 | ì 𝑥 $ ← -[[𝑃 1 ]] 𝑞 𝑘 ( ì 𝑎)} = P{𝑥 = ì 𝑏 | ì 𝑥 $ ← -[[𝑃 2 ]] 𝑞 𝑘 ( ì 𝑎)}.
𝑞 ∞ -equivalence requires the property to hold on all extensions of a eld, i.e.,

𝑃 1 ≈ 𝑞 ∞ 𝑃 2 i ∀𝑘. 𝑃 1 ≈ 𝑞 𝑘 𝑃 2
• 𝑞 𝑘 -majority requires that for a xed 𝑟 ∈ Q, and for every input ì 𝑎 ∈ F 𝑚 𝑞 𝑘 and output ì 𝑏 ∈ F 𝑛 𝑞 𝑘 , we have

P{ ì 𝑥 = ì 𝑏 | ì 𝑥 $ ← -[[𝑃 1 ]] 𝑞 𝑘 ( ì 𝑎)} ≤ 𝑟 • P{ ì 𝑥 = ì 𝑏 | ì 𝑥 $ ← -[[𝑃 2 ]] 𝑞 𝑘 ( ì 𝑎)}.
𝑞 𝑘 -0-majority (denoted 𝑃 1 ≺ 𝑟 𝑞 𝑘 𝑃 2 ) is a variant of majority, where we only consider the output 𝑏 = 0 𝑛 , rather than quantifying over all outputs. 𝑞 ∞ -0-majority requires the property to hold on all extensions of a eld, i.e.,

𝑃 1 ≺ 𝑟 𝑞 ∞ 𝑃 2 i ∀𝑘. 𝑃 1 ≺ 𝑟 𝑞 𝑘 𝑃 2
The following two boolean programs illustrate the di erence between equivalence and universal equivalence.

Example 1.

𝑃 1 = 𝑥 $ ← -F; return (𝑥 2 + 𝑥) 𝑃 2 = return 0 are 2-but not 2 2 -equivalent, and hence not 2 ∞ -equivalent. Indeed, when instantiating F with F 2 , the left hand side program simply evaluates to zero, which is not the case with F 4 . On the other hand, the programs

𝑄 1 = 𝑥 $ ← -F; return (𝑥) 𝑄 2 = 𝑥 $ ← -F; return (𝑥 + 1)
are 𝑞 ∞ -equivalent as both programs de ne the uniform distribution over F, whatever nite eld is used for the interpretation of F. These examples also illustrate the di erence with the well-studied polynomial identity testing (PIT) problem, as the rst two programs are 2-equivalent, while PIT does not consider 𝑥 2 + 𝑥 and 0 to be equal on F 2 , nor would 𝑄 1 and 𝑄 2 be considered identical.

The xed and universal variants of the equivalence and majority problems are directly inspired from applications in security and privacy. In the xed setting, the equivalence and majority problems are related to probabilistic non-interference and di erential privacy. The relationships between probabilistic non-interference and equivalence and between di erential privacy and majority are explained informally as follows:

• probabilistic non-interference: for simplicity, assume that 𝑃 has two inputs 𝑥 (secret) and 𝑦 (public), and a single (public) output. For every 𝑥, let 𝑃 𝑥 be the unique program such that 𝑃 𝑥 (𝑦) = 𝑃 (𝑥, 𝑦). Then 𝑃 is non-interfering i for every 𝑥 1 and 𝑥 2 , the two programs 𝑃 𝑥 1 and 𝑃 𝑥 2 are equivalent.

• di erential privacy: for simplicity consider the case where the base eld is F 2 . For every program 𝑃 with 𝑛 inputs, de ne the residual programs 𝑃 𝑖,0 and 𝑃 𝑖,1 obtained by xing the 𝑖-th output to 0 and 1 respectively. Then the program 𝑃 is 𝑙𝑜𝑔(𝑟 )-di erentially private i for every 𝑖, 𝑃 𝑖,0 and 𝑃 𝑖,1 (and 𝑃 𝑖,1 and 𝑃 𝑖,0 ) satisfy 𝑟 -majority.

In the universal setting, the parameter 𝑘 can loosely be understood as the security parameter. Universal equivalence is a special case of statistical indistinguishability and as such arises naturally in provable security, where the goal is to prove (depending on applications either as end goal, or as an intermediate goal) that two programs are equivalent for all possible interpretations (e.g. for all possible lengths of bitstrings, i.e. for all F 2 𝑘 ).

Summary of results

We also consider the following problems, which are also motivated by security and privacy and are directly related to equivalence:

• (bounded) simulatability: given programs 𝑃 1 and 𝑃 2 , does there exist a context 𝐶 [•] (of bounded degree) such that 𝐶 [𝑃 1 ] is equivalent to 𝑃 2 ;

• independence: are outputs 𝑌 and 𝑌 of program 𝑃 independent conditioned on 𝑍 , i.e. for every input 𝑥, is the distribution of 𝑌 independent from the distribution of 𝑌 , when conditioning on the value of 𝑍 ? Although independence is not naturally expressed as a relational property, it has been shown in [START_REF] Barthe | Symbolic methods in computational cryptography proofs[END_REF] that relational methods are useful for proving independence.

The rst contribution of the paper is a systematic study of the complexity of the aforementioned problems in the xed setting. We prove that the 𝑞 𝑘 -equivalence problem is coNP C = P -complete for any xed 𝑘. We also study the special case of linear programs, i.e. multiplication, conditional and conditioning free, for which the problem can be decided in polynomial time. For the majority problem, we consider two settings: programs with and without inputs. We show that the 𝑘-majority problem for inputless programs is PP-complete, whereas the 𝑘-majority for arbitrary programs is coNP PP -complete-thus the second problem is strictly harder than the rst, unless PH ⊂ PP 1 . The proofs are given by reductions to MAJSAT and E-MAJSAT respectively. Note that we do not include any result about bounded simulatability in the nite case, since we only derive easy consequences of equivalence. These results complement recent work on the complexity of checking di erential privacy for arithmetic circuits [START_REF] Gaboardi | The complexity of verifying circuits as di erentially private[END_REF], see Related Work below.

The second, and main contribution, is the study of universal equivalence, 𝑞 ∞ -equivalence for short, and universal (0-)majority, 𝑞 ∞ -(0-)majority for short. First, we show that the 𝑞 ∞ -equivalence problem is in 2-EXP and coNP C = P -hard.

Our proof is based on local zeta Riemann functions, a powerful tool from algebraic geometry, that characterize the number of zeros of a tuple of polynomials in all extensions of a nite eld. Lauder and Wan [START_REF] Alan | Counting points on varieties over nite elds of small characteristic[END_REF] notably propose an algorithm to compute such functions, whose complexity is however exponential. Based on this result, our proof proceeds in three steps.

First, we give a reduction for arithmetic programs (no conditionals, nor conditioning) from universal equivalence to checking that some speci c local zeta Riemann functions are always null. Then, we reduce the general case to programs without conditioning, and programs without conditioning to arithmetic programs. To justify the use of the local zeta Riemman functions, we also provide counterexamples why

𝑥-(conditional)-{equivalence, independence, uniformity} 𝑞 ∞ -simulatability linear arithmetic general decidable coNP C = P -hard 𝑥 = 𝑞 𝑘 PTIME coNP C = P -complete coNP C = P -complete 𝑥 = 𝑞 ∞ PTIME EXP coNP C = P -hard 2-EXP coNP C = P -hard
𝑞 𝑘 -0-majority 𝑞 𝑘 -majority 𝑞 ∞ -0-majority 𝑞 ∞ -majority without inputs PP-complete coNP PP -complete PP-hard ≤ EXP POSITIVITY
with inputs coNP PP -complete ? coNP PP -hard Figure 2: Summary of results related to majority simpler methods fail or only provide su cient conditions. Our decidability result signi cantly generalize prior work on universal equivalence [START_REF] Barthe | On the equality of probabilistic terms[END_REF], which considers the case of linear programs, see Related Work below. In the special case of arithmetic programs, i.e., programs without conditionals nor conditioning, equivalence can be decided in EXP-time, rather than 2-EXP.

Second, we give an exponential reduction from the universal 0-majority problem to the positivity problem for Linear Recurrence Sequences (LRS), which given a LRS, asks whether it is always positive.

Despite its apparent simplicity, the positivity problem remains open. Decidability has been obtained independently by Mignotte et al [START_REF] Mignotte | The distance between terms of an algebraic recurrence sequence[END_REF] and by Vereshchagin [START_REF] Nk Vereshchagin | The problem of appearance of a zero in a linear recurrence sequence[END_REF] for LRS of order ≤ 4 and later by Ouaknine and Worrell [START_REF] Ouaknine | Positivity problems for low-order linear recurrence sequences[END_REF] for LRS with order ≤ 5. Moreover, Ouaknine and Worrell prove in the same paper that deciding positivity for LRS of order 6 would allow to solve hard open problems in Diophantine approximation. In the general case, the best known lower bound for the positivity problem is NP-hardness [START_REF] Ouaknine | Decision problems for linear recurrence sequences[END_REF].

Our reduction is based on the observation that the Taylor series of any rational functional satis es a linear recurrence sequence. Therefore, every tuple of polynomials yields a linear recurrence sequence via its local zeta Riemann function. Unfortunately, the order of the linear reccurence sequence is related to the degree of the local zeta Riemann function, and thus decidability results for small orders do not apply. This suggests that the problem may not have an e cient solution. Using the results from [START_REF] Kiefe | Sets de nable over nite elds: their zeta-functions[END_REF], we observe that the reduction extends to a more general form of universal majority problem.

Finally, we obtain lower complexity bounds by reducing the nite case to the universal case. It remains an interesting open question whether the universal case is strictly harder than the nite case.

Figures 1 and2 summarize our results for the equivalence and majority problems.

Related work

Universal equivalence The case of linear programs is studied in [START_REF] Barthe | On the equality of probabilistic terms[END_REF]. The authors propose a decision procedure for universal equivalence based on the classic XOR-lemma [START_REF] Chor | The bit extraction problem of t-resilient functions (preliminary version)[END_REF]. We give an alternative decision procedure and analyze its complexity. The case of linear programs with random oracles is considered in [START_REF] Carmer | Linicrypt: a model for practical cryptography[END_REF]. The authors give a polynomial time decision procedure for computational indistinguishability of two inputless programs. Informally, computational indistinguishability is an approximate notion of universal equivalence, stating that the statistical distance between the output of two programs on the same input is upper bounded by a negligible function of the parameter 𝑘. Their proof is based on linear algebra.

The case of pseudo-linear (i.e. linear with conditionals) programs is considered in [START_REF] Charanjit | Decision procedures for simulatability[END_REF]. The authors consider the universal simulatability problem, rather than the universal equivalence problem. The crux of their analysis is a completeness theorem for pseudo-linear functions. In Section 4.3, we show that universal equivalence reduces to universal simulatability. As [START_REF] Charanjit | Decision procedures for simulatability[END_REF] shows the decidability of universal simulatability for pseudo-linear programs, it therefore follows that universal equivalence of pseudo-linear programs is decidable.

Fixed equivalence There is a vast amount of literature on proving equivalence of probabilistic programs. We only review the most relevant work here.

Murawski and Ouaknine [START_REF] Murawski | On probabilistic program equivalence and re nement[END_REF] prove decidability of equivalence of second-order terms in probabilistic ALGOL. Their proof is based on a fully abstract game semantics and a connection between program equivalence and equivalence of probabilistic automata.

Legay et al [START_REF] Legay | On automated veri cation of probabilistic programs[END_REF] prove decidability of equivalence for a probabilistic programming language over nite sets. Their language supports sampling from non-uniform distributions, loops, procedure calls, and open code, but not conditioning. They show that program equivalence can be reduced to language equivalence for probabilistic automata, which can be decided in polynomial time.

Barthe et al [START_REF] Barthe | Formal certi cation of code-based cryptographic proofs[END_REF] develop a relational program logic for probabilistic programs without conditioning. Their logic has been used extensively for proving program equivalence, with applications in provable security and side-channel analysis.

Majority problems

The closest related work develops methods for proving di erential privacy or for quantifying information ow.

Frederikson and Jha [START_REF] Fredrikson | Satis ability modulo counting: A new approach for analyzing privacy properties[END_REF] develop an abstract decision procedure for satis ability modulo counting, and then use a concrete instantiatiation of their procedure for checking representative examples from multi-party computation.

Barthe et al [START_REF] Barthe | Automated methods for checking di erential privacy[END_REF] show decidability of 𝜖-di erential privacy for a restricted class of programs. They allow loops and sampling from Laplace distributions, but impose several other constraints on programs. An important aspect of their work is that programs are parametrized by 𝜖 > 0, so their decision procedure establishes 𝜖-di erential privacy for all values of 𝜖. Technically, their decision procedure relies on the decidability of a fragment of the reals with exponentials by McCallum and Weispfenning [START_REF] Mccallum | Deciding polynomial-transcendental problems[END_REF].

Gaboardi, Nissim and Purser [START_REF] Gaboardi | The complexity of verifying circuits as di erentially private[END_REF] study the complexity of verifying pure and approximate (𝜖, 𝛿)di erential privacy for arithmetic programs, as well as approximations of the parameters 𝜖 and 𝛿. The parameter 𝛿 quanti es the approximation and 𝛿 = 0 corresponds to the pure case. Our majority problem can be seen as a subcase of di erential privacy, where 𝑟 corresponds to 𝜖, and 𝛿 = 0. In particular, the complexity class they obtain for pure di erential privacy coincides with the complexity of our 0-majority problem, even when restricted to the case 𝑟 = 1. This means that the 𝜖 parameter does not essentially contribute to the complexity of the veri cation problem. Also, while they consider arithmetic programs, we consider the more general case of programs with conditioning.

Chistikov, Murawski and Purser [START_REF] Chistikov | Asymmetric distances for approximate di erential privacy[END_REF] also study the complexity of approximating di erential privacy, but in the case of Markov Chains.

Theory of elds A celebrated result by Ax [START_REF] Ax | The elementary theory of nite elds[END_REF] shows that the theory of nite elds is decidable. In a recent development based on Ax's result, Johnson [START_REF] Andrew | Fun with elds[END_REF] proves decidability of the theory of rings extended with quanti ers 𝜇 𝑛 𝑘 𝑥 . 𝑃, stating that the number of 𝑥 such that 𝑃 holds is equal to 𝑘 modulo 𝑛. Although closely related, these results do not immediately apply to the problem of equivalence.

Programming Language

We consider a high-level probabilistic programming language with sampling from semi-algebraic sets and conditioning, as well as a more pure, yet equi-expressive, core language that can encode all previous constructs and de ne its formal semantics.

𝑃 ::= polynomials | 𝑖 ∈ F 𝑞 xed value | 𝑥 variable | 𝑃 1 + 𝑃 2 eld addition | 𝑃 1 ×

Syntax and informal semantics

We de ne in Figure 3 the syntax for simple probabilistic programs (without loops nor recursion2 ). Our programs will operate on nite elds. We denote by F 𝑞 the (unique) nite eld with 𝑞 elements, where 𝑞 = 𝑝 𝑠 for some integer 𝑠 and prime 𝑝. Programs are parametrized by a nite eld F, which will be instantiated by some F 𝑞 𝑘 during the intepretation. Given a polynomial 𝑃 ∈ F 𝑞 [𝑥 1 , . . . , 𝑥 𝑚 ] and 𝑋 ∈ F 𝑚 𝑞 𝑘 , we denote by 𝑃 (𝑋 ) the evaluation of 𝑃 given 𝑋 inside F 𝑞 𝑘 .

The expressions of our programs provide constructs for assigning a polynomial 𝑃 to a variable (𝑥 := 𝑃), as well as, for randomly sampling values. With for instance ì 𝑟 = 𝑟 1 , . . . , 𝑟 𝑚 , the expression 𝑟 1 , . . . , 𝑟 𝑚 $ ← -{𝑋 ∈ F 𝑚 | 𝑏} uniformly samples 𝑚 values from the set of 𝑚-tuples of values in F such that the condition 𝑏 holds, and assigns them to variables 𝑟 1 , . . . , 𝑟 𝑚 . For example, 𝑟 $ ← -{𝑥 ∈ F | 0 = 0} (which we often simply write 𝑟 $ ← -F) uniformly samples a random element in F, while 𝑟 1 , 𝑟 2 $ ← -{𝑥 1 , 𝑥 2 ∈ F 2 | ¬(𝑥 1 = 0)} samples two random variables, ensuring that the rst one is not 0. Note that the use of polynomial conditions allows to express any rational distribution over the base eld F 𝑞 .

The construct observe 𝑏 allows to condition the continuation by 𝑏: if 𝑏 evaluates to false the program fails; the semantics of a program is the conditional distribution where 𝑏 holds. Expressions also allow classical constructs for sequential composition, conditional branching and returning a result.

In a well-formed program we suppose that every variable is bound at most once, and if it is bound, then it is only used after the binding. Unbound variables correspond to the inputs of the program. We moreover suppose that each branch of a program 𝑃 ends with a return instruction that returns the same number 𝑛 of elements; 𝑛 is then called the arity of the program and denoted |𝑃 |. Given two sets of variables 𝐼 and 𝑅, we denote by P 𝑞 (𝐼, 𝑅) the set of such well-formed programs, where 𝐼 is the set of unbound variables (intuitively, the set of input variables) and 𝑅 the set of variables sampled by the program. This program de nes a probabilistic algorithm for computing the inverse of a eld element 𝑖. If 𝑖 is 0, by convention the algorithm returns 0. Otherwise, the algorithm uniformly samples an element 𝑟 . This is obviously not a practical procedure for computing an inverse, but we use it to illustrate the semantics of conditioning. The observe instruction checks whether 𝑟 is the inverse of 𝑖. If this is the case we return 𝑟 , otherwise the program fails. As we will see below, our semantics normalizes the probability distribution to only account for non-failing executions. Hence, this algorithm will return the inverse of any positive 𝑖 with probability 1. Equivalently, this program can be written by directly conditioning the sample .

𝑖𝑛𝑣 (𝑖) ::= if 𝑖 = 0 then return 0 else 𝑟 $ ← -{𝑥 ∈ F | 𝑥 × 𝑖 = 1}; return 𝑟

A core language

While the above introduced syntax is convenient for writing programs, we introduce a more pure, core language that is actually equally expressive and will ease the technical developments in the remaining of the paper. To de ne this core language, we add an explicit failure instruction ⊥, similarly to [START_REF] Bichsel | Fine-grained semantics for probabilistic programs[END_REF]. It allows us to get rid of conditioning in random samples and observe instructions. Looking ahead, and denoting by [[𝑃]] 𝑞 𝑘 the semantics of the program 𝑃 inside F 𝑞 𝑘 , we will have that

[[𝑟 1 , . . . , 𝑟 𝑚 $ ← -{𝑋 ∈ F 𝑚 | 𝑏}; 𝑒]] 𝑞 𝑘 = [[𝑟 1 , . . . , 𝑟 𝑚 $ ← -F 𝑚 ; if 𝑏 then 𝑒 else ⊥]] 𝑞 𝑘 and [[observe 𝑏; 𝑒]] 𝑞 𝑘 = [[if 𝑏 then 𝑒 else ⊥]] 𝑞 𝑘
Without loss of generality, we can inline deterministic assignments, and use code motion to perform all samplings eagerly, i.e., all random samplings are performed upfront. Therefore we can simply consider that each variable in 𝑅 is implicitly uniformly sampled in F 𝑞 𝑘 . Programs are then tuples of simpli ed expressions (𝑒 1 , . . . , 𝑒 𝑛 ) de ned as follows.

𝑒 ::= simpli ed expressions | 𝑃 polynomial | ⊥ failure | if 𝑏 then 𝑒 1 else 𝑒 2 conditional branching
We suppose that all nested tuples are attened and write (𝑃, 𝑄) to denote the program which simply concatenates the outputs of 𝑃 and 𝑄. When clear from the context, we may also simply write ì 0 instead of the all zero tuple (0, . . . , 0). We denote by P 𝑞 (𝐼, 𝑅) the set of arithmetic programs, that are simply tuples of polynomials. Remark that arithmetic programs cannot fail.

One may note that the translation from the surface language to the core language is not polynomial in general. Indeed, constructs of the form (if 𝑏 then 𝑥 := 𝑡 1 else 𝑥 := 𝑡 2 ; 𝑃), i.e. sequential composition after a conditional, implies to propagate the branching over the assignment to all branches of 𝑃, and doubles the number of conditional branchings of 𝑃. All complexity results will be given for the size of the program given inside the core language. Remark that in a functional style version of the surface language, where we replace 𝑥 := 𝑡 by let 𝑥 = 𝑡 in and removed sequential composition, the translation would however be polynomial. Similarly, for the class of programs without sequential composition after conditional branchings, the translation is also polynomial.

Semantics

We now de ne the semantics of our core language. The precise translation from the high level syntax previously presented and our core language is standard and omitted.

Deterministic semantics. We rst de ne a deterministic semantics where all random samplings have already been de ned. For a set 𝑋 of variables, with 𝑃 ∈ F 𝑞 [𝑋 ] and ì 𝑥 ∈ F |𝑋 | 𝑞 𝑘 , 𝑃 ( ì 𝑥) classicaly denotes the evaluation of 𝑃 inside F 𝑞 𝑘 . We also denote 𝑏 (ì 𝑣) the evaluation of a boolean test, where all polynomials are evaluated according to ì 𝑣. For a program 𝑒 ∈ P 𝑞 (𝐼, 𝑅) and ì 𝑣 ∈ F |𝐼 ∪𝑅 | 𝑞 𝑘 , we de ne a natural evaluation of

𝑒, denoted [𝑒] 𝑞 𝑘 ì 𝑣 , which is a value inside F |𝑃 | 𝑞 𝑘 × {⊥}: [𝑃] 𝑞 𝑘 ì 𝑣 = 𝑃 (ì 𝑣) where 𝑃 ∈ F 𝑞 [𝐼 𝑅] [⊥] 𝑞 𝑘 ì 𝑣 = ⊥ if 𝑏 then 𝑒 1 else 𝑒 2 𝑞 𝑘 ì 𝑣 = [𝑒 1 ] 𝑞 𝑘 ì 𝑣 if 𝑏 (ì 𝑣) holds on F 𝑞 𝑘 [𝑒 2 ] 𝑞 𝑘 ì 𝑣 if 𝑏 (ì 𝑣) does not hold on F 𝑞 𝑘 [(𝑒 1 , . . . , 𝑒 𝑛 )] 𝑞 𝑘 ì 𝑣 = ⊥ if [𝑒 𝑖 ] 𝑞 𝑘 ì 𝑣 = ⊥ for some 𝑖 ([𝑒 1 ] 𝑞 𝑘 ì 𝑣 , . . . , [𝑒 𝑛 ] 𝑞 𝑘 ì 𝑣 ) else
Intuitively, the set of executions corresponding to non failure executions represent the set of possible executions of the program. We next de ne probabilistic semantics by sampling uniformly the valuations of the random variables while conditioning on the fact that the program does not fail.

Probabilistic semantics. For any 𝑛, the set of distributions over F 𝑛 𝑞 is denoted by Distr(F 𝑛 𝑞 ). For a program 𝑃 ∈ P 𝑞 (𝐼, 𝑅) with |𝑃 | = 𝑛, and |𝐼 | = 𝑚, we de ne its semantics to be a function from inputs to a distribution over the outputs:

[[𝑃]] 𝑞 𝑘 : F 𝑚 𝑞 𝑘 → Distr(F 𝑛 𝑞 𝑘 )
We assume that programs inside 𝑃 ∈ P 𝑞 (𝐼, 𝑅) do not fail all the time, i.e., for any possible input and any program its probability of failure is strictly less than

1. For program 𝑃, input ì 𝑖 ∈ F 𝑚 𝑞 𝑘 and output ì 𝑜 ∈ F 𝑛 𝑞 𝑘 we set P{ ì 𝑥 = ì 𝑜 | ì 𝑥 $ ← -[[𝑃]] 𝑞 𝑘 ( ì 𝑖)} to P{[𝑃] 𝑞 𝑘 ì 𝑖,ì 𝑟 = ì 𝑜 | ì 𝑟 $ ← -F |𝑅 | 𝑞 𝑘 } P{[𝑃] 𝑞 𝑘 ì 𝑖,ì 𝑟 ≠ ⊥ | ì 𝑟 $ ← -F |𝑅 |
𝑞 𝑘 } Note that the normalization by conditioning on non-failing programs is well de ned as we supposed that programs do not always fail.

The xed case

We start by studying the complexity of several problems over a given nite eld. In this case we only manipulate nite objects, and hence all problems are obviously decidable, by explicitly computing the distributions. We however provide precise complexity results and show that these problems have complexities in the counting hierarchy [START_REF] Torán | Complexity classes de ned by counting quanti ers[END_REF]. We also de ne the universal variant and state some results that are common to both variants of the problems.

Conditional equivalence

In this section, we prove that for any 𝑘 ∈ N, the 𝑞 𝑘 -equivalence problem is coNP C = P -complete. To this end, we introduce a technical generalization of the equivalence problem, that we call 𝑞 𝑘 -conditional equivalence, and we proceed in four steps, showing that:

1. without loss of generality, we can consider programs without inputs; (Lemma 4)

verifying if the conditioned distributions of two inputless programs coincide on a xed point is in

C = P; (Lemma 5)
3. verifying if the conditioned distribution of inputless programs coincide on all points is in coNP C = P ; (Corollary 6)

4. and nally, even equivalence for programs over F 2 is coNP C = P -hard. (Lemma 7)

De ning conditional equivalence

𝑞 𝑘 -conditional equivalence is a generalization of equivalence, where we require programs to be equivalent when the distributions are conditioned by some other program being equal to zero. Conditional equivalence is a technical generalisation, that is interesting because it is self-reducible when removing for instance the conditionals.

De nition 3 (𝑞 𝑘 -conditional equivalence). Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (𝐼, 𝑅) and 𝑃 2 , 𝑄 2 ∈ P 𝑞 (𝐼, 𝑅) with

|𝑃 1 | = |𝑄 1 | = 𝑛. We denote 𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 , if: ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . ∀ì 𝑐 ∈ F 𝑛 𝑞 𝑘 . [[(𝑃 1 , 𝑃 2 )]] 𝑞 𝑘 ì 𝑖 (ì 𝑐, ì 0) = [[(𝑄 1 , 𝑄 2 )]] 𝑞 𝑘 ì 𝑖 (ì 𝑐, ì 0)
The universal version 𝑞 ∞ -conditional equivalence is de ned similarly to 𝑞 ∞ -equivalence , i.e.,

𝑃 1 | 𝑃 2 ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2 i ∀𝑘 ∈ N. 𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 .
Note that conditional equivalence is a direct generalization of equivalence, as for 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅), 𝑃

≈ 𝑞 𝑘 𝑄 if and only if 𝑃 | 0 ≈ 𝑞 𝑘 𝑄 | 0.
We also remark that equivalence over Z is undecidable, which is a consequence of Hilbert's 10th problem, as a polynomial over randomly sampled variables will be equivalent to zero if and only if it does not have any solutions.

We rst de ne precisely the decision problems associated to our questions, for 𝑘 ∈ N ∪ {∞}:

𝑞 𝑘 -conditional equivalence : 𝑃 1 , 𝑄 1 ∈ P 𝑞 (𝐼, 𝑅), 𝑃 2 , 𝑄 2 ∈ P 𝑞 (𝐼, 𝑅) : 𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ?
The decision problem for 𝑞 𝑘 -equivalence simply corresponds to 𝑞 𝑘 -conditional equivalence with 𝑃 2 and 𝑄 2 being equal to 0. In the following we will show that both problems are interreducible, and that 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence are both coNP C = P -complete.

Complexity results for conditional equivalence

Recall that C = P-complete is the set of decision problems solvable by a NP Turing Machine whose number of accepting paths is equal to the number of rejecting paths. halfSAT is the natural C = P-complete problemde ned as follows.

halfSAT : CNF boolean formula 𝜙 : Is 𝜙 true for exactly half of its valuations?

coNP C = P is the set of decision problems whose complement can be solved by a NP Turing Machine with access to an oracle deciding problems in C = P. The canonical coNP C = P problem is (using the results from [START_REF] Toràn | An oracle characterization of the counting hierarchy[END_REF]Sec. 4] and [START_REF] Michael L Littman | The computational complexity of probabilistic planning[END_REF]) :

A-halfSAT : CNF boolean formula 𝜙 (𝑋, 𝑌 ) : For all valuations of 𝑋 , is 𝜙 (𝑋, 𝑌 ) true for exactly half of the valuations of 𝑌 ? Also, recall that conditional equivalence is a direct generalization of equivalence. We thus trivially have, for any 𝑘 ∈ N ∪ {∞}, that 𝑞 𝑘 -equivalence reduces in polynomial time to 𝑞 𝑘 -conditional equivalence.

We rst study the complexity of deciding if the distributions of two programs are equal on a speci c point. To do so, we remark that it is not necessary to consider inputs when considering equivalence or conditional equivalence. The intuition is that inputs can be seen as random values, that must be synchronized on both sides. This synchronization is achieved by explicitly adding these random variables to the output, forcing them to have the same value on both side. The following Lemma is a generalization to conditional equivalence of a Lemma from [START_REF] Barthe | Symbolic methods in computational cryptography proofs[END_REF]. Lemma 4. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence reduces to 𝑞 𝑘 -conditional equivalence restricted to programs without inputs in polynomial time.

Omitted proofs can be found in Appendix A. As we can without loss of generality ignore the inputs, we study the complexity of deciding if the distributions of two inputless programs coincide on a speci c point. To this end, we build a Turing Machine, such that it will accept half of the time if and only if the programs given as input have the same probability to be equal to some given value. Essentially, it is based on the fact that over

F 2 , if 𝑟 = 0 then 𝑃 else (𝑄 + 1) ≈ 2 𝑟 if and only if 𝑃 ≈ 2 𝑄. Lemma 5. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (∅, 𝑅) and 𝑃 2 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅) with |𝑃 1 | = |𝑄 1 | = 𝑛. For any ì 𝑐 ∈ F 𝑛 𝑞 𝑘 , we can decide in C = P if: [[(𝑃 1 , 𝑃 2 )]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄 1 , 𝑄 2 ]] 𝑞 𝑘 (ì 𝑐, ì 0) Proof.
𝑥 $ ← -{0, 1}; ì 𝑟 $ ← -F |𝑅 | 𝑞 ; ì 𝑟 $ ← -F |𝑅 | 𝑞 ; if 𝑥 = 0 then if ¬(𝑃 1 (ì 𝑟 ) = ì 𝑐 ∧ 𝑃 2 (ì 𝑟 ) = ì 0 ∧ 𝑄 1 ( ì 𝑟 ) ≠ ⊥) then ACCEPT else REJECT else if(𝑄 1 (ì 𝑟 ) = ì 𝑐 ∧ 𝑄 2 (ì 𝑟 ) = ì 0 ∧ 𝑃 1 ( ì 𝑟 ) ≠ ⊥) then ACCEPT else REJECT Let 𝑃 = (𝑃 1 , 𝑃 2 )
and 𝑄 = (𝑄 1 , 𝑄 2 ). The probability that 𝑀 accepts is, by case disjunction on the value of 𝑥:

1 2 (1 -P ( ì 𝑐, ì 0) (1 -Q1 ⊥ )) + 1 2 ( Q ( ì 𝑐, ì 0) (1 -P1 ⊥ )) = 1 2 + Q ( ì 𝑐,ì 0) (1-P1 ⊥ )-P ( ì 𝑐,ì 0) (1-Q1 ⊥ ) 2
And thus:

[[𝑃]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄]] 𝑞 𝑘 (ì 𝑐, ì 0) ⇔ P{ [𝑃 ] 𝑞 𝑘 ì 𝑖,ì 𝑟 =( ì 𝑐, ì 0) |ì 𝑟 $ ← -F |𝑅| 𝑞 } P{ [𝑃 ] 𝑞 𝑘 ì 𝑖,ì 𝑟 ≠⊥|ì 𝑟 $ ← -F |𝑅| 𝑞 } = P{ [𝑄 ] 𝑞 𝑘 ì 𝑖,ì 𝑟 =(𝑐, ì 0) |ì 𝑟 $ ← -F 𝑅 𝑞 } P{ [𝑄 ] 𝑞 𝑘 ì 𝑖,ì 𝑟 ≠⊥|ì 𝑟 $ ← -F 𝑅 𝑞 } ⇔ P ( ì 𝑐,ì 0) 1-P1 ⊥ = Q ( ì 𝑐,ì 0) 1-Q1 ⊥ ⇔ Q ( ì 𝑐, ì 0) (1 -P1 ⊥ ) -P ( ì 𝑐, ì 0) (1 -Q1 ⊥ ) = 0
⇔ 𝑀 accepts exactly half of the time As C = P is closed under nite intersection [START_REF] Toràn | An oracle characterization of the counting hierarchy[END_REF], we can decide in C = P if two distributions over a set of xed size are equal, by testing the equality over all points. When we only consider inputless programs of xed arity, the set of points to test is constant, and the equivalence problem is in C = P (see Corollary 38 for details). However, when we extend to inputs, or to programs of variable arity, we need to be able to check for all possible points if the distribution are equal over this point. (Note that our encoding that allows to only consider inputless programs increases the arity.) Checking all possible points is typically in coNP. We thus obtain that: Corollary 6. 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence are in coNP C = P for any 𝑘 ∈ N.

To conclude completeness for both 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence, it is su cient to show the hardness of 2-equivalence, which we do by reducing A-halfSAT. We simply transform a CNF boolean formula into a polynomial over F 2 , such that the polynomial is uniform if the formula is in A-halfSAT. This is a purely technical operation (see Lemma 39). Lemma 7. 2-equivalence is coNP C = P -hard.

Independence

We show here that equivalence and (conditional) indepence have the same complexity. Conditional independence asks if for any xed value of some variables 𝑌 , the programs are independent, i.e if the product of their distributions is equal to the distribution of their product. De nition 8 (𝑞 𝑘 -conditional independence). Let 𝑃 1 , . . . , 𝑃 𝑛 ∈ P 𝑞 (𝐼, 𝑅). Given 𝑌 ⊂ 𝑅, we say that 𝑃 1 , . . . , 𝑃 𝑛 are independent conditioned by 𝑌 , denoted ⊥ 𝑌 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ), if:

∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . ∀ ì 𝑖 ∈ F |𝑌 | 𝑞 . [[(𝑃 1 , . . . , 𝑃 𝑛 )]] 𝑞 𝑘 ì 𝑖, ì 𝑖 = ( [[𝑃 1 ]] 𝑞 𝑘 ì 𝑖, ì 𝑖 , . . . , [[𝑃 𝑛 ]] 𝑞 𝑘 ì 𝑖, ì 𝑖 )
We write ⊥ 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) for ⊥ ∅ 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ), which simply denotes independence of the programs. Example 9. Independence implies that the distribution of one of the programs does not provide any information about the distribution of the other one. In particular, considering programs in P 2 ({𝑖 1 , 𝑖 2 }, {𝑟 }), we have that ⊥ 2 (𝑖 1 (𝑖 2 + 𝑟 ), 𝑖 2 ), which means that 𝑖 1 (𝑖 2 + 𝑟 ) leaks no information about 𝑖 2 . However, ⊥ 2 (𝑖 1 (𝑖 2 + 𝑟 ), 𝑖 1 ).

We de ne the decision problem associated to independence, for 𝑘 ∈ N ∪ {∞}:

𝑞 𝑘 -conditional independence : 𝑃 ∈ P 𝑞 (𝐼, 𝑅), 𝑌 ⊂ 𝑅 : ⊥ 𝑌 𝑞 𝑘 𝑃?
The universal version, 𝑞 ∞ -conditional independence, is de ned as expected. We now prove that 𝑞 𝑘 -conditional independence is also coNP C = P -complete in two steps: rst, we reduce conditional independence to indenpence, and, second, we reduce independence to equivalence.

To reduce to non conditional independence, we show that we can replace the conditionned random variable by some fresh input variable. Lemma 10. Let 𝑃 1 , . . . , 𝑃 𝑛 be programs over P 𝑞 𝑘 (𝐼, 𝑅), and 𝑌 ⊂ 𝑅.

⊥ 𝑌

𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔⊥ 𝑞 𝑘 (𝑃 1 𝜎, . . . , 𝑃 𝑛 𝜎) where 𝜎 : 𝑌 → 𝐼 𝑌 is the substitution that replaces each variable in 𝑌 by a fresh input variable in 𝐼 𝑌 .

To reduce independence to equivalence, the idea is that if 𝑛 programs (as a tuple) are equivalent to a copy of the 𝑛 programs where they all sample independently there randomness, they are independent. This translates into the following Lemma. Lemma 11. Let 𝑃 1 , . . . , 𝑃 𝑛 be programs over P 𝑞 𝑘 (𝐼, {𝑟 1 , . . . , 𝑟 𝑚 })

⊥ 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔ (𝑃 1 , . . . , 𝑃 𝑛 ) ≈ 𝑞 (𝑃 1 𝜎1, . . . , 𝑃 𝑛 𝜎 𝑛 )
where 𝜎 𝑖 is the substitution that to any 𝑟 𝑗 associates a fresh random variable 𝑟 𝑖 𝑗 . The two previous Lemmas directly yield the following corollary. Corollary 12. 𝑞 𝑘 -conditional independence is in coNP C = P .

It remains to show the hardness of conditional independence. The key idea is that for any program 𝑃 and fresh random 𝑟 , we have that ⊥ ∅ 2 (𝑃 +𝑟, 𝑟 ) if and only if 𝑃 follows the uniform distribution. Intuitively, 𝑃 perfectly masks the dependance in 𝑟 only if it is a uniform value. Then, we reduce uniformity to independence, and as we previously reduced A-halfSAT to uniformity, we conclude. Theorem 13. 𝑞 𝑘 -conditional independence is coNP C = P -complete.

Majority

The goal of this section is to show that the majority problem is coNP PP -complete. To this end, we study the complexity of 𝑞 𝑘 -0-majority, showing:

• PP-completeness for inputless programs;

• coNP PP -completeness in general.

The proof in both cases uses similar ideas as for equivalence. Note that we actually use the same Turing Machine for the Membership. As both complexity classes are closed under nite intersection, it yields the complexity of 𝑞 𝑘 -majority, which can be decided using 𝑞 𝑘 times 𝑞 𝑘 -0-majority.

The majority problem

𝑞 𝑘 -majority asks if, given two programs, the quotient of their distribution is bounded on all points by some rational 𝑟 . 𝑞 𝑘 -0-majority is a subcase, where we only ask if the quotient of their distribution is bounded on a single point. This problem allows to estimate the distance between two distributions. It is close to the di erential privacy question, which asks, when 𝛿 = 0, if the quotient of two distributions is bounded over all points by some 𝑒 𝜖 .

We observe that the majority problem is harder than equivalence, as majority for 𝑟 = 1 implies equivalence. An important di erence between equivalence and majority is that the presence of inputs actually changes the complexity of the majority problem.

Let us de ne the decision problem associated to 𝑞 𝑘 -majority, with 𝑘 ∈ N ∪ {∞}:

𝑞 𝑘 -majority : 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅), 𝑟 ∈ Q : 𝑃 ≺ 𝑟 𝑞 𝑘 𝑄?
We consider that 𝑟 is given in input as two integers written in unary. Essentially, this is because if one whishes to encode any 𝑟 , it requires an exponential blow up, but in practice, we tend to use some particular rationals such as 𝑟 = 𝑞 𝑙 , for which there is no exponential blow up.

Complexity results for the majority problem

We recall that PP is the set of languages accepted by a probabilistic polynomial-time Turing Machine with an error probability of less than 1/2 for each instance, i.e., a word in the language is accepted with probability at least 1/2, and a word not in the language is accepted with probability less than 1/2. Alternatively, one can de ne PP as the set of languages accepted by a non-deterministic Turing Machine where the acceptance condition is that a majority of paths are accepting. Notably, PP contains both NP and coNP, as well as C = P. Also, PP is closed uner nite intersection. A natural PP-complete problem is MAJSAT: is a boolean CNF formula satis ed for at least half of its valuations:

MAJSAT

: CNF boolean formula 𝜙 : Is 𝜙 true for at least half of its valuations?

coNP PP is the class of of problems whose complement is decided by a NP Turing Machine with access to an oracle deciding problems in PP. The classical NP PP problem is E-MAJSAT [START_REF] Michael L Littman | The computational complexity of probabilistic planning[END_REF] :

E-MAJSAT

: CNF boolean formula 𝜙 (𝑋, 𝑌 ) : Is there a valuation of 𝑋 such that, 𝜙 (𝑋, 𝑌 ) is true for at least half of the valuation of 𝑌 ?

Its complement, A-MINSAT is then the classical coNP PP problem.

To obtain the complexity of 𝑞 𝑘 -0-majority over inputless programs, we notice that the Turing Machine we used to obtain the complexity of the equivalence problem are easily adapted for our purpose. Indeed, it accepted half of the time if the two distributions were equal on a single point, but it actually accepts with probability greater than half only if the value of the rst distribution is greater than the second one on the given point.

The only di culty is that we are comparing with a rational. We thus brie y show how one can assume without loss of generality that 𝑟 = 1 (in which case we omit 𝑟 from the notation). The idea is , given 𝑟, 𝑠 ∈ N, that 𝑃 ≺ 𝑟 𝑠 𝑞 𝑘 𝑄 ⇔ (𝑃,𝑇 𝑟 ) ≺ 𝑞 𝑘 (𝑄,𝑇 𝑠 ), if 𝑇 𝑗 is a machine which is equal to zero with probability 1 𝑗 . Lemma 14. For any 𝑘 ∈ N, 𝑞 𝑘 -0-majority reduces in polynomial time to 𝑞 𝑘 -0-majority with 𝑟 = 1.

The proof showing that 𝑞 𝑘 -0-majority is in PP is similar to proving that testing if two distributions are equal over a point is in C = P. We prove PP-completeness by deriving the hardness from MAJSAT.

Lemma 15. For any 𝑘 ∈ N, 𝑞 𝑘 -0-majority restricted to inputless programs is PP-complete.

Finally, as PP is closed under nite intersection, we also get that 𝑞 𝑘 -majority over inputless programs with a xed arity is PP-complete.

Let us now turn to the general version, for programs with inputs. By using some fresh inputs variables, let us remark that one can easily reduce 𝑞 𝑘 -majority to 𝑞 𝑘 -0-majority. Indeed, for 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅) and 𝑐 ∈ F |𝑃 | 𝑞 , with a fresh 𝑥 ∈ 𝐼 :

∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . [[𝑃]] 𝑞 𝑘 ì 𝑖 (𝑐) ≤ 𝑟 [[𝑄]] 𝑞 𝑘 ì 𝑖 (𝑐) ⇔ (𝑃 -𝑥) ≺ 𝑟 𝑞 𝑘 (𝑄 -𝑥)
We show that 𝑞 𝑘 -majority is coNP PP complete, and thus is most likely3 harder than its version without inputs. The membership and hardness proofs are similar to the equivalence problem when going from C = P to coNP C = P .

Lemma 16. 𝑞 𝑘 -majority is coNP PP complete.

The universal case

In this section we rst give some general insights on universal equivalence showing important di erences with the case of a xed eld. Then we provide our main decidability result, rst for arithmetic programs, then arithmetic programs enriched with conditionals, and nally for general programs. We continue by studying two other problems in the universal case: simulatability and 0-majority.

General remarks

In this section we try to provide some insights on the di culty of deciding 𝑞 ∞ -equivalence. First of all, we note that equivalence and universal equivalence do not coincide.

Example 17. The program 𝑥 2 + 𝑥 and the program 0 are equivalent over F 2 (they are then both equal to zero), but not over F 4 .

In the case of a given nite eld, equivalence can be characterized by the existence of a bijection, see for instance [START_REF] Barthe | Symbolic methods in computational cryptography proofs[END_REF]. We denote by bij F 𝑚 𝑞 the set of bijections over F 𝑚 𝑞 . Any element 𝜎 ∈ bij F 𝑚 𝑞 can be expressed as a tuple of polynomials (see e.g. [START_REF] Nipkow | Uni cation in primal algebras, their powers and their varieties[END_REF]), and can be applied as a substitution. The characterization can then be stated as follows, where we denote by = F 𝑞 equality between polynomials modulo the rule of the eld (i.e., 𝑋 𝑞 = 𝑋 ). 𝑃 ≈ 𝑞 𝑄 ⇔ ∃𝜎 ∈ bij F 𝑚 𝑞 , 𝑃 = F 𝑞 𝑄𝜎 However, there are universally equivalent programs such that there does not exist a universal 𝜎 suitable for all extensions.

Example 18. Consider, 𝑃 = 𝑥𝑦 + 𝑦𝑥 + 𝑧𝑥, with 𝜎 : (𝑥, 𝑦, 𝑧) ↦ → (𝑥, 𝑦 + 𝑥, 𝑧 + 𝑥), we get that 𝑃 ≈ 2 ∞ 𝑥 2 + 𝑦𝑧. Now, 𝑥 ↦ → 𝑥 2 is a bijection over all F 2 𝑘 , so we also have 𝑃 ≈ 2 ∞ 𝑥 + 𝑦𝑧 and nally 𝑃 ≈ 2 ∞ 𝑥. But here, a bijection between 𝑥 2 + 𝑦𝑧 and 𝑥 must use the inverse of 𝑥 2 whose expression depends on the size of the eld. Thus, there isn't a universal polynomial 𝜎 which is a bijection such that on all F 2 𝑘 , 𝑃 = F 2 𝑘 𝑄 • 𝜎. Nevertheless, we can note that for linear programs this characterization allows us to show that 𝑞-equivalence and 𝑞 ∞ -equivalence are equivalent. Intuitively, the bijection allowing to obtain the equality between two linear programs is also a bijection valid for all extensions of the nite eld, as the bijection is linear, and is thus a witness of equivalence over all extensions. For linear programs, there exists a polynomial time decision procedure for equivalence, and hence for universal equivalence.

Lemma 19. 𝑞 ∞ -equivalence restricted to linear programs is in PTIME.

Moreover, building on results from [START_REF] Maubach | The automorphism group over nite elds[END_REF] on Tame automorphisms, we can use the above characterization to design a su cient condition which implies universal equivalence for general programs. Even though not complete this su cient condition may be useful to verify universal equivalence more eciently in practice.

A Su cient Condition

In the univariate case, our notion is also strongly linked to what mathematicians calls exceptional polynomials, permutation polynomials over F 𝑞 [𝑥] that are permutations over in nitely many

F 𝑞 𝑘 [𝑥].
A univariate polynomial which is uniform is then an exceptional polynomial of F 𝑞 [𝑥]. They have been fully characterized [26, p237]. However, the multivariate case appears unsolved.

With the previous characterization, we can however easily obtain the following condition, for any function 𝜎:

𝜎

∈ 𝑘 bij F 𝑚 𝑞 𝑘 ⇒ 𝑃 ≈ 𝑞 ∞ 𝑃𝜎
To better understand this condition, we now provide some results provinding some insights about functions that are bijections over all extensions of a nite eld.

We rst use Theorem 3.2 of [START_REF] Maubach | The automorphism group over nite elds[END_REF] to classify what are the bijections over F 𝑚 𝑞 𝑘 . For a nite eld F, bij F 𝑛 denotes the set of bijections over F 𝑛 , and E (𝑇 (F, 𝑛)) denotes the set of bijections obtained through permutations, scalar multiplications ( for any 𝑎 ∈ F * , (𝑥 1 , . . . , 𝑥 𝑛 ) ↦ → (𝑎𝑥 1 , . . . , 𝑥 𝑛 )) and linear transformations (for any 𝑃 ∈ 𝑘 [𝑥 2 , . . . , 𝑥 𝑛 ], (𝑥 1 , . . . , 𝑥 𝑛 ) ↦ → (𝑥 1 + 𝑃 (𝑥 2 , . . . , 𝑥 𝑛 ), . . . , 𝑥 𝑛 ) ) , which are called the tame automorphisms.

Theorem 20 (2.3 of [START_REF] Maubach | The automorphism group over nite elds[END_REF]). We have:

• if 𝑛 = 1, and F = F 2 or F 3 , then E (𝑇 (F, 𝑛)) = bij F 𝑛 , • if 𝑛 ≥ 2 and F ≠ F 2 𝑚 for 𝑚 > 1 , E (𝑇 (F, 𝑛)) = bij F 𝑛 , • else, E (𝑇 (F, 𝑛)) ≠ bij F 𝑛 .
This allows us to obtain that:

Lemma 21. For any 𝑘 ≥ 1 and 𝑛 > 1, for any function 𝑓 :

𝑓 ∈ bij F 𝑛 𝑝 𝑘 ⇒ ∀𝑘 > 𝑘.𝑓 ∈ bij F 𝑛 𝑝 𝑘 Proof. Let 𝑓 ∈ bij F 𝑝 𝑘 .
With Theorem 20, we have that for all prime 𝑝: E (𝑇 (F 𝑝 𝑘 , 𝑛)) = B (F 𝑛 𝑝 𝑘 ) Thus, 𝑓 can be written as a composition of substitutions, scalar multiplications linear transformations. All those operations are directly bijections over any F 𝑛 𝑝 𝑘 , we thus conclude:

∀𝑘 > 𝑘.𝑓 ∈ bij F 𝑛 𝑝 𝑘
The case 𝑝 = 2 must be handled di erently:

Lemma 22. For any 𝑘 > 1 and 𝑛 > 1, for any function 𝑓 :

𝑓 ∈ bij F 𝑛 2 2(2𝑘+1) ⇒ ∀𝑘 > 2(2𝑘 + 1).𝑓 ∈ bij F 𝑛 2 𝑘
Proof. For any 𝑚, we denote F (𝑇 (F 2 𝑚 , 𝑛)) the set generated by E (𝑇 (F 2 𝑚 , 𝑛)) and the permutation 𝜎 = (𝑋 1 , . . . , 𝑋 𝑛 ) ↦ → (𝑋 2 1 , . . . , 𝑋 𝑛 ). It is shown in [20, p. 351] that 𝑥 𝑛 is a bijection in F 𝑞 if 𝑛 and 𝑞 -1 are coprime. We have that for any 𝑘, 2 and 2 𝑘 -1 are coprime, and then, we have that 𝜎 is a bijection over all

F 𝑛 2 𝑚 .
If 𝜎 is of signature -1, has E (𝑇 (F 2 𝑚 , 𝑛)) contains all elements with a positive signature of B (F 2 𝑚 ), then we have F (𝑇 (F 2 𝑚 , 𝑛)) = B (F 2 𝑚 ).

We have 𝜎 𝑚 = 𝐼𝑑, so 𝜎 is made of 𝑚 cycles, and 𝜎 only leaves 0 and 1 invariants. Thus, 𝜎 has 𝑉 = 2 𝑚 -2 𝑚 cycles. For the 𝑚 cycles to be of sign -1, 𝑚 must be pair, i.e 𝑚 = 2𝑙. Now, if 𝑙 is odd, i.e 𝑚 = 2(2𝑘 + 1), 𝑉 = 2 𝑚-1 -1 2𝑘+1 is odd, and then 𝜎 is of sign -1. Thus, we have proven that for any 𝑘:

F (𝑇 (F 2 2(2𝑘+1) , 𝑛)) = B (F 2 2(2𝑘+1) )
Let us x 𝑘 and let 𝑓 ∈ bij F 2 2(2𝑘+1) . Thus, 𝑓 can be written as a composition of substitutions, scalar multiplications, linear transformations and 𝜎. Recall that 𝜎 is a bijection over all F 𝑛 2 𝑘 , and the others trivially are. We thus conclude:

∀𝑘 > 2(2𝑘 + 1).𝑓 ∈ bij F 𝑛 2 𝑘
Those two lemmas provides an easy way to generate bijections which are bijections over all extension of the nite eld, and can thus serve as a witness for a universal equivalence.

Decidability of universal equivalence

We show decidability of 𝑞 ∞ -equivalence, leveraging tools from algebraic geometry, showing that:

1. 𝑞 ∞ -conditional equivalence is decidable for arithmetic programs; (Lemma 24) 2. it is also decidable for programs with conditionals; (Lemma 26) 3. it is nally decidable for programs with conditioning, e.g. failures. (Lemma 27)

We rst recall the de nition and relevant properties of local zeta Riemann functions. For a tuple 𝑃 of polynomials 𝑃 1 , . . . , 𝑃 𝑚 ∈ F 𝑞 [𝑋 1 , . . . , 𝑋 𝑛 ], the local zeta Riemann function over 𝑇 is the formal series

𝑍 (𝑃,𝑇 ) = exp ∑ 𝑘 ∈N * |𝑁 𝑘 (𝑃)| 𝑘 𝑇 𝑘 where 𝑁 𝑘 (𝑃) = { ì 𝑥 ∈ F 𝑛 𝑞 𝑘 | 1≤𝑖 ≤𝑚 𝑃 𝑖 ( ì 𝑥) = 0}.
Weil's conjecture [START_REF] Weil | Numbers of solutions of equations in nite elds[END_REF] states several fundamental properties of local zeta Riemann functions over algebraic varieties. Dwork [START_REF] Dwork | On the rationality of the zeta function of an algebraic variety[END_REF] proves part of Weil's conjecture stating that the local zeta Riemann functions over algebraic varieties is a rational function with integer coe cients-recall that 𝑍 (𝑇 ) is a rational function i there exist polynomials 𝑅(𝑇 ) and 𝑆 (𝑇 ) such that 𝑍 (𝑇 ) = 𝑅(𝑇 )/𝑆 (𝑇 ). Bombieri [START_REF] Bombieri | On exponential sums in nite elds[END_REF] shows that the sum of the degrees of 𝑅 and 𝑆 is upper bounded by 4(𝑑 + 9) 𝑛+1 , where 𝑑 is the total degree of (𝑃 1 , . . . , 𝑃 𝑚 ). It follows that the values of 𝑁 𝑘 for 𝑘 ≤ 4(𝑑 + 9) 𝑛+1 su ce for computing 𝑍 ; since these values can be computed by brute force, this yields an algorithm for computing 𝑍 . We will by abuse of notations write 𝑍 (𝑃) instead of 𝑍 (𝑃,𝑇 ) for the local zeta function of 𝑃. 𝑍 (𝑃) completely characterizes the number of times 𝑃 is equal to zero on all the di erent extensions. For instance, 𝑍 (𝑃) = 𝑍 (𝑄) allows us to conclude that 𝑃 and 𝑄 always evaluate to zero for the same number of valuations, and this over any F 𝑞 𝑘 . As 𝑍 can e ectively be computed [START_REF] Alan | Counting points on varieties over nite elds of small characteristic[END_REF], we can use it to decide 𝑞 ∞ -equivalence.

Notice that, given two programs 𝑃 and 𝑄, the local zeta function directly allow us to conclude if they are equal to some value with the same probability for all extensions of the base eld. Moreover, thanks to [START_REF] Kiefe | Sets de nable over nite elds: their zeta-functions[END_REF], the computability of the local zeta function can be extended from counting the number of points such that 𝑃 = 0 for a tuple of polynomials, to counting the number of points such that 𝜙 holds, where 𝜙 is an arbitrary rst order formula over nite elds.

Corollary 23. Let 𝜙 and 𝜓 be two rst order formulae built over atoms of the form 𝑃 = 0 with 𝑃 ∈ F 𝑞 [𝑋 ], and with free variables 𝐹 ⊂ 𝑋 . One can decide if for all 𝑘 ∈ N:

{ ì 𝑓 ∈ F |𝐹 | 𝑞 𝑘 | 𝜙 ( ì 𝑓 ) = 1} = { ì 𝑓 ∈ F |𝐹 | 𝑞 𝑘 | 𝜓 ( ì 𝑓 ) = 1}
Thus, for any two events which can be expressed as a rst order formula over nite eld one can verify if they happen with the same probability over all extensions of the base eld. Remark that this cannot be used to decide universal equivalence, as equivalence cannot be expressed inside a rst order formula.

We rst show that, thanks to the local zeta functions, 𝑞 ∞ -equivalence is decidable for arithemic programs, i.e programs without conditionals or conditioning.

Lemma 24. Let 𝑃 1 , 𝑃 2 , 𝑄 1 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅). 𝑃 1 | 𝑃 2 ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2 ⇔ 𝑍 ((𝑄 1 -𝑄 1 𝜎, 𝑄 2 , 𝑄 2 𝜎)) = 𝑍 ((𝑃 1 -𝑄 1 𝜎, 𝑃 2 , 𝑄 2 𝜎)) = 𝑍 ((𝑃 1 -𝑃 1 𝜎, 𝑃 2 , 𝑃 2 𝜎))
where 𝜎 : 𝑅 ↦ → 𝑅 maps each variable to a fresh one.

Proof. We assimilate 𝑃 1 𝑃 2 , 𝑄 1 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅) of size 𝑚 with polynomials, denoting 𝑃 (𝑋 ) the value of 𝑃 given 𝑋 ∈ F 𝑚 𝑞 𝑘 . Given an enumeration 1 ≤ 𝑗 ≤ 𝑠 of the elements 𝑐 𝑗 of F 𝑛 𝑞 𝑘 , for any programs 𝑇 ,𝑇 , we let

(𝑇 ,𝑇 ) 𝑘 𝑖 = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑇 (𝑋 ) = 𝑐 𝑖 ∧ 𝑇 (𝑋 ) = ì 0}
Then, if we denote ------→ (𝑇 ,𝑇 ) 𝑘 = (𝑇 ,𝑇 ) 𝑘 1 , . . . , (𝑇 ,𝑇 ) 𝑘 𝑠 , that characterizes the distribution of 𝑇 |𝑇 ,

𝑃 1 | 𝑃 2 ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2 ⇔ ∀𝑘 ∈ N. -------→ (𝑃 1 , 𝑃 2 ) 𝑘 = -------→ (𝑄 1 , 𝑄 2 ) 𝑘
Using the classical inner product ì 𝑥 • ì 𝑦 = 𝑖 𝑥 𝑖 𝑦 𝑖 , for any 𝑘 and programs 𝑈 , 𝑉 , 𝑈 , 𝐻 ∈ P 𝑞 , we have:

𝑁 𝑘 ((𝑈 -𝑉 𝜎, 𝑈 , 𝑉 )) = 𝑋, 𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑈 (𝑋 ) = 𝑉 (𝑋 ) ∧ (𝑈 (𝑋 ), 𝑉 (𝑋 )) = ì 0 = 𝑐 ∈F 𝑛 𝑞 𝑘 {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑈 (𝑋 ) = 𝑐 ∧ 𝑈 (𝑋 ) = ì 0} {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑉 (𝑋 ) = 𝑐 ∧ 𝑉 (𝑋 ) = ì 0} = 𝑖 (𝑈 , 𝑈 ) 𝑘 𝑖 (𝑉 , 𝑉 ) 𝑘 𝑖 = -------→ (𝑈 , 𝑈 ) 𝑘 • ------→ (𝑉 , 𝑉 ) 𝑘
Using scalar operations, we have that:

𝑁 𝑘 (𝑄 1 -𝑄 1 𝜎, 𝑄 2 , 𝑄 2 𝜎) = 𝑁 𝑘 (𝑃 1 -𝑄 1 𝜎, 𝑃 2 , 𝑄 2 𝜎) = 𝑁 𝑘 (𝑃 1 -𝑃 1 𝜎, 𝑃 2 , 𝑃 2 𝜎) ⇔ -------→ (𝑄 1 , 𝑄 2 ) 𝑘 • -------→ (𝑄 1 , 𝑄 2 ) 𝑘 = -------→ (𝑃 1 , 𝑃 2 ) 𝑘 • -→ 𝑄 𝑘 = -------→ (𝑃 1 , 𝑃 2 ) 𝑘 • -------→ (𝑃 1 , 𝑃 2 ) 𝑘 ⇔ ( -------→ (𝑃 1 , 𝑃 2 ) 𝑘 - -→ 𝑄 𝑘 ) • ( -------→ (𝑃 1 , 𝑃 2 ) 𝑘 - -------→ (𝑄 1 , 𝑄 2 ) 𝑘 ) = ì 0 ⇔ -------→ (𝑃 1 , 𝑃 2 ) 𝑘 = -------→ (𝑄 1 , 𝑄 2 ) 𝑘 Hence, ∀𝑘 ∈ N.∀𝑐 ∈ F 𝑛 𝑞 𝑘 . {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑃 1 (𝑋 ) = 𝑐 ∧ 𝑃 2 (𝑋 ) = ì 0} = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑄 1 (𝑋 ) = 𝑐 ∧ 𝑄 2 (𝑋 ) = ì 0} ⇔ ∀𝑘 ∈ N.𝑁 𝑘 ((𝑄 1 -𝑄 1 𝜎, 𝑄 2 , 𝑄 2 𝜎)) = 𝑁 𝑘 ((𝑃 1 -𝑄 1 𝜎, 𝑃 2 , 𝑄 2 𝜎)) = 𝑁 𝑘 ((𝑃 1 -𝑃 1 𝜎, 𝑃 2 , 𝑃 2 𝜎))
This concludes the proof, as for all 𝑈 , 𝑉 ,

𝑍 (𝑈 ) = 𝑍 (𝑉 ) ⇔ ∀𝑘. 𝑁 𝑘 (𝑈 ) = 𝑁 𝑘 (𝑉 )
In ??, we provide a variant of this result for the speci c case of verifying if a program follows the uniform distribution over all extensions, where only one computation of a local zeta function is required.

Using the complexity for the computation of the local zeta function provided by [18, Corollary 2] we obtain the following corollary.

Corollary 25. 𝑞 ∞ -equivalence and 𝑞 ∞ -conditional equivalence restricted to arithmetic programs are in EXP.

We now wish to remove conditionals, in order to reduce equivalence for programs with conditional to arithmetic programs (which are simply tuples of polynomials). To remove the conditionals, the rst idea is to use a classical encoding inside nite elds:

[[if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ]] 𝑞 𝑘 = [[𝑃 𝑓 1 + 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1
)]] 𝑞 𝑘 . This works nicely as 𝐵 𝑞 𝑘 -1 is equal to 0 if 𝐵 = 0, else to 1. However, for the universal case, we need to have an encoding which does not depend on the size of the eld, i.e., it must be independent of 𝑘. The key idea is that for any variable 𝑡 and polynomial 𝐵:

(𝐵(𝐵𝑡 -1) = 0 ∧ 𝑡 (𝐵𝑡 -1) = 0) ⇔ 𝑡 = 𝐵 𝑞 𝑘 -2
And thus, we can for instance write, with some program 𝑄 and ì 𝑐:

[[if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ]] 𝑞 𝑘 (ì 𝑐) = [[𝑄]] 𝑞 𝑘 (ì 𝑐) ⇔ [[𝑃 𝑓 1 + 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1 )]] 𝑞 𝑘 (ì 𝑐) = [[𝑄]] 𝑞 𝑘 (ì 𝑐) ⇔ [[𝑃 𝑓 1 + 𝐵𝑡 (𝑃 𝑡 1 -𝑃 𝑓 1 ), (𝐵(𝐵𝑡 -1), 𝑡 (𝐵𝑡 -1))]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄]] 𝑞 𝑘 (ì 𝑐)
An induction on the number of conditionals yields our second lemma.

Lemma 26. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence restricted to programs without failures reduces in exponential time to 𝑞 𝑘 -conditional equivalence restricted to arithmetic programs.

Recall that failures de ne the probablisitic semantics by normalization. And for instance, for some program (if 𝑏 = 0 then 𝑃 1 else ⊥, 𝑃 2 ) where 𝑃 1 and 𝑃 2 do not fail and 𝑏 is a polynomial, for any ì 𝑐, we have:

[[(if 𝑏 = 0 then 𝑃 1 else ⊥, 𝑃 2 )]] 𝑞 𝑘 (ì 𝑐, ì 0) = P{𝑃 1 =ì 𝑐∧𝑃 2 = ì 0∧𝑏=0} P{¬(𝑏=0) }
Handling this division by itself would be di cult if we wanted to compute the distribution. However, in our setting, we are comparing the equality of two distributions, so we can simply multiply on both side by the denominator, and try to express once again all factors as an instance of conditional equivalence. We will be able to push inside conditional equivalence some probabilities, as

[[𝑃]] 𝑞 𝑘 (ì 𝑐) × P{𝑏 = 0} = [[𝑃, 𝑏]] 𝑞 𝑘 (ì 𝑐, 0) when all variables in 𝑏 do not appear in 𝑃.
As an illustration of how to remove the failures, with some program 𝑄, we have:

if 𝑏 = 0 then 𝑃 1 else ⊥ | 𝑃 2 ≈ 𝑞 𝑘 𝑄 | 0 ⇔ ∀ì 𝑐.[[(if 𝑏 then 𝑃 1 else ⊥, 𝑃 2 )]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄]] 𝑞 𝑘 (ì 𝑐) ⇔ ∀ì 𝑐.P{𝑃 1 = ì 𝑐 ∧ 𝑃 2 = ì 0 ∧ 𝑏 = 0} = P{¬(𝑏 = 0)}[[𝑄]] 𝑞 𝑘 (ì 𝑐, ì 0) ⇔ ∀ì 𝑐.[[𝑃 1 , 𝑃 2 , 𝑏]] 𝑞 𝑘 (ì 𝑐, ì 0) = P{¬(𝑏 = 0)}[[𝑄]] 𝑞 𝑘 (ì 𝑐)
To reduce to an instance of conditional equivalence, the issue is that we need to express as an equality the disequality 𝑏 ≠ 0. With some fresh variable 𝑡, multiplying by P{¬(𝑏 = 0)} or conditioning on 𝑡𝑏-1 = 0 is equivalent, as 𝑏 has an inverse if and only if it is di erent from zero. We can thus have:

if 𝑏 = 0 then 𝑃 1 else ⊥ | 𝑃 2 ≈ 𝑞 𝑘 𝑄 | 0 ⇔ ∀ì 𝑐.[[𝑃 1 , 𝑃 2 , 𝑏]] 𝑞 𝑘 (ì 𝑐, ì 0) = P{¬(𝑏 = 0)}[[𝑄]] 𝑞 𝑘 (ì 𝑐) ⇔ ∀ì 𝑐.[[𝑃 1 , 𝑃 2 , 𝑏]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄, 𝑡𝑏 -1]] 𝑞 𝑘 (ì 𝑐, 0) ⇔ 𝑃 1 | 𝑃 2 , 𝑏 ≈ 𝑞 𝑘 𝑄 | 𝑡𝑏 -1
Using those techniques, we obtain: Lemma 27. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence reduces to 𝑞 𝑘 -conditional equivalence restricted to programs without failures in exponential time.

The previous Lemmas allows us to conclude.

Theorem 28. 𝑞 ∞ -equivalence and 𝑞 ∞ -conditional equivalence are in 2-EXP.

And using once again Lemmas 10 and 11, we obtain the same complexity results for the independence problem.

Corollary 29. 𝑞 ∞ -conditional independence is in 2-EXP.
Moreover, we can also extend the lower bound obtained for 𝑞-equivalence.

Lemma 30. 𝑞-equivalence reduces in polynomial time to 𝑞 ∞ -equivalence.

Bounded Universal Simulatability

Simulation-based proofs [START_REF] Lindell | How to simulate it -A tutorial on the simulation proof technique[END_REF] are one main cornerstone of cryptography. Informally, simulation-based proofs consider a real and an ideal world, and require showing the existence of a simulator, such that no adversary can distinguish the composition of the simulator and of the ideal world from the real world. This can be modelled in our context by requiring the existence of a program 𝑆 (the simulator) such that "plugging in" the ideal world into 𝑆 is equivalent to the real world. In this section, we consider a simpler task, where the size of the simulator is bounded. Given a program 𝐶, we denote deg(𝐶) the maximum degree of a progam, i.e the maximum degree of any polynomial appearing in 𝐶 (the degree of a polynomial is the maximum over the sum of the degrees of each monomial).

De nition 31.

[Bounded (universal) simulatability] Let 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅), 𝑅 such that ♯𝑅 = ♯𝑅 and 𝑙 ∈ N. We denote 𝑃 𝑙 𝑞 [∞] 𝑄, if there exists 𝑆 ∈ P 𝑞 ({𝑖 1 , . . . , 𝑖 𝑛 }, 𝑅 }) such that deg(𝑆) ≤ 𝑙, and

𝑆 [ 𝑄 / ì 𝑖 ] ≈ 𝑞 [∞] 𝑃
The associated decision problem is: l,q-simulatability : 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅) : 𝑃 𝑙 𝑞 ∞ 𝑄?

Thanks to the bound on the degree coming from 𝑙, we can easily obtain a bound on the number of such possible contexts. This is shown in Lemma 42. From the bound on the number of contexts and the decidability of universal equivalence, one can derive the decidability of bounded simulatability. Theorem 32. l,q-simulatability is decidable.

As a lower bound, we prove that 𝑙, 𝑞-simulatability is as hard as universal equivalence: Lemma 33. For any 𝑙 ∈ N, 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -equivalence reduces in polynomial time to 𝑙, 𝑞 𝑘 -simulatability.

We conclude this section by noting that our notion of bounded simulatability is more restricted than the general paradigm of simulation-based proofs but could be a good starting point for automating simulation-based proofs.

Universal zero-majority without inputs

For arbitrary programs, we reduce 𝑞 ∞ -0-majority to the POSITIVITY problem. We recall that a Linear Recurrence Sequence (LRS) is an in nite sequence of reals 𝑢 = 𝑢 1 , 𝑢 2 , . . . such that there exist real constants 𝑎 1 , . . . , 𝑎 𝑘 such that for all 𝑛 ≥ 0,

𝑢 𝑛+𝑘 = 𝑎 1 𝑢 𝑛+𝑘-1 + • • • + 𝑎 𝑘 𝑢 𝑛
The order of a LRS 𝑢 = 𝑢 1 , 𝑢 2 , . . . is the smallest 𝑘 such that the equation above holds. A LRS 𝑢 = 𝑢 1 , 𝑢 2 , . . . is positive if 𝑢 𝑛 ≥ 0 for every 𝑛 ∈ N. The positivity problem consists in deciding whether a LRS is positive.

We use the fact that from a local zeta function, which is rational, we can obtain a Linear Recurrence Sequence. Then, by considering the POSITIVITY of the LRS obtained by susbtracting two local zeta function, we actually check if the coe cients of the rst one are always greater than the second one. We remark that the complexity of the problem strongly relies on the presence of multiplications, as for 𝑞 ∞ -equivalence. Indeed, in the linear case, majority implies equivalence and we obtain the following.

Lemma 34. 𝑞 ∞ -0-majority restricted to linear programs is in PTIME.

The general case has yet to be proven decidable.

Theorem 35. 𝑞 ∞ -0-majority for inputless programs reduces in exponential time to POSITIVITY.

Proof. Let 𝑃, 𝑄 ∈ P 𝑞 (∅, 𝑅). We assume without loss of generality that we only have to consider arithmetic programs, using the same simpli cations for observe and conditionals as we did for universal equivalence.

Recall that for any 𝑃, the local zeta function 𝑍 (𝑃) (over indeterminate 𝑇 ) is rational thanks to Weil's conjecture [START_REF] Dwork | On the rationality of the zeta function of an algebraic variety[END_REF]. Moreover, with 𝑁 𝑘 (𝑃) = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑃 (𝑋 ) = 0} , we have that:

𝑑 𝑑𝑇 𝑙𝑜𝑔(𝑍 (𝑃)) = 𝑍 (𝑃) 𝑍 (𝑃) = ∑ 𝑘 𝑁 𝑘 (𝑃)𝑇 𝑘
Let us call Z (𝑃) = 𝑘 𝑁 𝑘 (𝑃)𝑇 𝑘 , which is also a rational function as 𝑍 is (and so is 𝑍 ). As the coe cients of Z (𝑃) -Z (𝑄) are 𝑁 𝑘 (𝑃) -𝑁 𝑘 (𝑄), we have that ∀𝑘, 𝑁 𝑘 (𝑃) ≥ 𝑁 𝑘 (𝑄) if and only if Z (𝑃) -Z (𝑄) only has positive coe cients. It is well known that the coe cients of the Taylor serie of a rational function form a LRS (see e.g. [START_REF] Everest | Exponential functions, linear recurrence sequences, and their applications[END_REF]). This means that the coe cients of Z (𝑃) -Z (𝑄) form an LRS, which we denote 𝑧 𝑃𝑄 . Finally: This reduction can also be applied with the generalization of [START_REF] Kiefe | Sets de nable over nite elds: their zeta-functions[END_REF], and thus, for any two events about programs over nite elds, one can, given an oracle for the POSITIVITY problem, decide if the probability of the rst event is greater than the second one for all extensions of the base eld.

𝑄 ≺ ∞ 𝑞 𝑃 ⇔ ∀𝑘,
Similarly to the equivalence case, we can derive some hardness from the non universal case, but we do not obtain any completeness result.

Lemma 36. 2 ∞ -0-majority is PP-hard.

Conclusion

We have introduced universal equivalence and majority problems and studied their complexity and decidability. Our work could notably be used as a building block to design a decidable logic for universal probabilistic program veri cation. It leaves several questions of interest open:

• the exact complexity of universal equivalence is open. It is even unknown whether the universal problem strictly harder than the non-universal one;

• the decidability of universal majority is open. The decidability of POSITIVITY would yield decidability of universal 0-majority and equivalently, undecidability of universal majority would also solve negatively the POSITIVITY problem;

• the decidability of universal approximate equivalence is open. Approximate equivalence asks whether the statistical distance between the distributions of two programs is negligible in 𝑘. This notion has direct applications in provable security.

A Proofs

The following Lemma is essentialy a generalization to conditional equivalence of a Lemma from [START_REF] Barthe | Symbolic methods in computational cryptography proofs[END_REF].

Lemma 37. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (𝐼, 𝑅), 𝑃 2 , 𝑄 2 ∈ P 𝑞 (𝐼, 𝑅). When 𝜎 : 𝐼 → 𝑅 𝐼 is the substitution that replaces each variable in 𝐼 by a fresh random variable in 𝑅 𝐼 , we have:

𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ (𝑃 1 𝜎, 𝑅 𝐼 ) | 𝑃 2 𝜎 ≈ 𝑞 𝑘 (𝑄 1 𝜎, 𝑅 𝐼 ) | 𝑄 2 𝜎
Proof. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (𝐼, 𝑅),𝑃 2 , 𝑄 2 ∈ P 𝑞 (𝐼, 𝑅), we have:

𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 .∀𝑐 ∈ F 𝑛 𝑞 𝑘 [[(𝑃 1 , 𝑃 2 )]] 𝑞 𝑘 ì 𝑖 (𝑐, ì 0) = [[(𝑄 1 , 𝑄 2 )]] 𝑞 𝑘 ì 𝑖 (𝑐, ì 0) ⇔ ∀𝑡 ∈ F | {𝐼 } | 𝑞 𝑘 .∀𝑐 ∈ F 𝑛 𝑞 𝑘 [[(𝑃 1 𝜎, 𝑃 2 𝜎, 𝑅 𝐼 )]] 𝑞 𝑘 ì 𝑖 (𝑐, ì 0, 𝑡) = [[(𝑄 1 𝜎, 𝑄 2 𝜎, 𝑅 𝐼 )]] 𝑞 𝑘 ì 𝑖 (𝑐, ì 0, 𝑡) ⇔ ∀𝑐 ∈ F 𝑛+| {𝐼 } | 𝑞 𝑘 [[((𝑃 1 𝜎, 𝑅 𝐼 ), 𝑃 2 𝜎)]] 𝑞 𝑘 ì 𝑖 (𝑐 , ì 0) = [[((𝑄 1 𝜎, 𝑅 𝐼 ), 𝑄 2 𝜎)]] 𝑞 𝑘 ì 𝑖 (𝑐 , ì 0) ⇔ (𝑃 1 𝜎, 𝑅 𝐼 ) | 𝑃 2 𝜎 ≈ 𝑞 𝑘 (𝑄 1 𝜎, 𝑅 𝐼 ) | 𝑄 2 𝜎
Corollary 38. For any 𝑘 ∈ N, 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence restricted to programs of xed arity and without inputs are in C = P.

Proof. We only have to consider 𝑞 𝑘 -conditional equivalence as it is harder than 𝑞 𝑘 -equivalence. Let 𝑃 1 , 𝑄

1 ∈ P 𝑞 (∅, 𝑅),𝑃 2 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅) with |𝑃 1 | = |𝑄 1 | = 1.
For some 𝑐, we have that verifying if

[[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (𝑐, ì 0) = [[𝑄 1 , 𝑄 2 ]] 𝑞 𝑘 (𝑐, ì 0)
is in C = P. As C = P is closed under nite intersection [START_REF] Toràn | An oracle characterization of the counting hierarchy[END_REF], we can decide in C = P if:

𝑐 ∈F 𝑞 [[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (𝑐, ì 0) = [[𝑄 1 , 𝑄 2 ]] 𝑞 𝑘 (𝑐, ì 0)
This is exactly the de nition of conditional equivalence, and thus it concludes the proof.

Corollary 6. 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence are in coNP C = P for any 𝑘 ∈ N.

Proof. First, we only have to consider C-EQUIV 𝑞 as it is a generalization of equivalence. Next, we only have to consider C-EQUIV 𝑞 restricted to program without inputs with Lemma 4. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (∅, 𝑅),𝑃 2 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅) with

|𝑃 1 | = |𝑄 1 | = 𝑛. Now, 𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ ∀𝑐 ∈ F 𝑛 𝑞 𝑘 [[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (𝑐, ì 0) = [[𝑄 1 , 𝑄 2 ]] 𝑞 𝑘 (𝑐, ì 0)
For some 𝑐 ∈ F 𝑛 𝑞 𝑘 , we have that deciding if

[[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (𝑐, ì 0) = [[𝑄 1 , 𝑄 2 ]] 𝑞 𝑘 (𝑐, ì 0) is in C = P.
The decision problem is then directly inside coNP

𝑞 𝑘 ì 𝑖 = ( [[𝑒 1 ]] 𝑞 𝑘 ì 𝑖 , . . . , [[𝑃 𝑛 ]] 𝑞 𝑘 ì 𝑖 ) ⇔ ∀ ì 𝑖 ∈ F |𝑋 | 𝑞 𝑘 . [[𝑃 1 , . . . , 𝑃 𝑛 ]] 𝑞 𝑘 ì 𝑖 = ( [[𝑃 1 𝜎 1 ]] 𝑞 𝑘 ì 𝑖 , . . . , [[𝑃 𝑛 𝜎 𝑛 ]] 𝑞 𝑘 ì 𝑖 ) ⇔ ∀ ì 𝑖 ∈ F |𝑋 | 𝑞 𝑘 . [[𝑃 1 , . . . , 𝑃 𝑛 ]] 𝑞 𝑘 ì 𝑖 = [[(𝑃 1 𝜎 1 , . . . , 𝑃 𝑛 𝜎 𝑛 )]] 𝑞 𝑘 ì 𝑖 ⇔ (𝑃 1 , . . . , 𝑃) ≈ 𝑞 𝑘 (𝑃 1 𝜎 1 , . . . , 𝑃 𝑛 𝜎 𝑛 ) Indeed, for any ì 𝑖 ∈ F |𝑋 | 𝑞 𝑘 we have that [[𝑃 𝑖 ]] 𝑞 𝑘 ì 𝑖 = [[𝑃 𝑖 𝜎 𝑖 ]] 𝑞 𝑘 ì 𝑖
as we are only performing renaming. Moreover, 𝑃 1 𝜎 1 , . . . , 𝑃 𝑛 𝜎 𝑛 do not share any variable, and thus trivially verify:

( [[𝑃 1 𝜎 1 ]] 𝑞 𝑘 ì 𝑖 , . . . , [[𝑃 𝑛 𝜎 𝑛 ]] 𝑞 𝑘 ì 𝑖 ) = [[(𝑃 1 𝜎 1 , . . . , 𝑃 𝑛 𝜎 𝑛 )]] 𝑞 𝑘 ì 𝑖 Theorem 13. 𝑞 𝑘 -conditional independence is coNP C = P -complete.
Proof. Only the hardness remains. Given a CNF formula 𝜙 (𝐼, 𝑅) over two sets of variables and (∨, ∧) we set 𝑃 = 𝜙 ∈ P 2 (𝐼, 𝑅) obtained according to Lemma 39. With 𝑟 a fresh random variable, recall that: 𝑃 ≈ 2 𝑟 ⇔ for all valuation of 𝐼 , 𝜙 is true for half of the valuation of 𝑅 ⇔ 𝜙 (𝐼, 𝑅) ∈ A-halfSAT But, with 𝑥 a fresh deterministic variable and 𝑟 a fresh random variable:

𝑃 ≈ 2 𝑟 ⇔ 𝑃 + 𝑥 ≈ 2 𝑟 + 𝑥 ⇔ 𝑃 + 𝑥 ≈ 2 𝑟 ⇔ (𝑃 + 𝑟 , 𝑟 ) ≈ 2 (𝑟, 𝑟 ) ⇔⊥ ∅ 2 (𝑃 + 𝑟 , 𝑟 )
And thus, we conclude with:

⊥ ∅ 2 (𝑃 + 𝑟, 𝑟 ) ⇔ 𝜙 (𝐼, 𝑅) ∈ A-halfSAT Lemma
← -{𝑥 ∈ F 𝑚 𝑞 | 𝑑 ∈𝐷 𝑛 𝑥 = 𝑑 } if (𝑟 1 , . . . , 𝑟 𝑚 ) = 𝑑 𝑛 then return ì 0 else return ì 1 Notice that by construction [[𝑇 𝑛 ]] 𝑞 𝑘 ( ì 0) = 1
𝑛 . This is only the most naive version of this encoding, simpler polynomials can be found for many speci c cases. And nally, for any 𝑟, 𝑠 ∈ N, assuming the probabilities are non zero, we have:

∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . [[𝑃 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) [[𝑄 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) ≤ 𝑟 𝑠 ⇔ ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . [[𝑃 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) 𝑟 ≤ [[𝑄 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) 𝑠 ⇔ ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . [[𝑃]] 𝑞 𝑘 ì 𝑖 ( ì 0) [[𝑇 𝑟 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) ≤ [[𝑄]] 𝑞 𝑘 ì 𝑖 ( ì 0) [[𝑇 𝑠 ]] 𝑞 𝑘 ì 𝑖 ( ì 0) ⇔ ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . [[(𝑃,𝑇 𝑟 )]] 𝑞 𝑘 ì 𝑖 ( ì 0) ≤ [[(𝑄,𝑇 𝑠 )]] 𝑞 𝑘 ì 𝑖 ( ì 0) ⇔ (𝑃,𝑇 𝑟 ) ≺ 𝑞 𝑘 (𝑄,𝑇 𝑠 )
Lemma 15. For any 𝑘 ∈ N, 𝑞 𝑘 -0-majority restricted to inputless programs is PP-complete.

Proof. Membership

Let 𝑃, 𝑄 ∈ P 𝑞 (∅, 𝑅). Let us reuse the polynomial time Turing Machine 𝑀 de ned in Lemma 5. Given 𝑃 1 , 𝑃 2 , 𝑄 1 , 𝑄 2 and ì 𝑐, it was such that:

[[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (ì 𝑐, ì 0) = [[𝑄 1 , 𝑄 2
]] 𝑞 𝑘 (ì 𝑐, ì 0) ⇔ 𝑀 accepts exactly half of the time Now, by replacing equals by > signs in the proof, we directly have that:

[[𝑃 1 , 𝑃 2 ]] 𝑞 𝑘 (ì 𝑐, ì 0) ≤ [[𝑄 1 , 𝑄 2
]] 𝑞 𝑘 (ì 𝑐, ì 0) ⇔ 𝑀 accepts at least half of the time Thus, we do have:

𝑃 ≺ 𝑞 𝑘 𝑄 ⇔ [[𝑃, 0]] 𝑞 𝑘 ( ì 0, 0) ≤ [[𝑄]] 𝑞 𝑘 (0, ì 0
) ⇔ 𝑀 accepts at least half of the time on input (𝑃, 0, 𝑄, 0, ì 0)

Hardness

We show PP-hardness by reduction from MAJSAT. Given a CNF formula 𝜙 (𝑅) over two sets of variables and (∨, ∧) we set 𝑃 = 𝜙 ∈ P 2 (𝑅) obtained according to Lemma 39. We then have:

𝜙 ∈ MAJSAT ⇔ {𝑋 ∈ F 𝑚 2 | 𝑃 (𝑋 ) = ì 0} ≤ 2 𝑚-1 ⇔ {𝑋 ∈ F 𝑚 2 | 𝑃 (𝑋 ) = ì 0} ≤ {𝑋 ∈ F 𝑚 2 | 𝑥 1 = 0} ⇔ 𝑃 ≺ 2 𝑥 1 Lemma 16. 𝑞 𝑘 -majority is coNP PP complete.
Proof. Hardness Let 𝜙 a CNF formula built over two sets of variables 𝐼 and 𝑅. We use the same construction as in Lemma 15 to obtain a polynomial 𝑃 ∈ P 2 (𝐼, 𝑅) whose truth value is equivalent of 𝜙.

We have, for some variable 𝑟 inside 𝑅:

𝜙 ∈ A-MINSAT ⇔ 𝑟 ≺ 2 𝑃

Membership

Let 𝑃, 𝑄 ∈ P 𝑞 𝑘 (𝐼, 𝑅). We slightly modify 𝑀 from Lemma 15, so that it takes as extra argument a valuation for the variables in 𝐼 , and every evaluation of 𝑃 or 𝑄 is made according to the valuation.

Then, we directly have:

𝑃 ≺ 𝑞 𝑄 ⇔ ∀ ì 𝑖 ∈ F |𝐼 |
𝑝 , 𝑀 accepts with probability greater than half on input ì 𝑖 This problem is then directly inside coNP PP .

Lemma 19. 𝑞 ∞ -equivalence restricted to linear programs is in PTIME.

Proof. Without loss of generality, we only consider programs without input variables (Lemma 4). Given a set of variables 𝑅, we assume that there is an ordering over the variables in 𝑅. We say that an expression is in normal form if it is of one of the following form: 0 or 1, or 𝑒, or 1 ⊕ 𝑒, where e is built from variables and ⊕ (but no constants), and variables appear at most once in increasing order.

Every linear expression can easily be put in normal form, using the commutativity of ⊕, and the normal form is indeed unique thanks to the ordering on variables.

We now assume that all polynomials are in normal form.

Given 𝑃 1 , . . . , 𝑃 𝑛 ∈ P 𝑞 (∅, 𝑅) without multiplications, we iterate over each 𝑃 𝑖 , where, after initializing a set 𝑆 to the emptyset:

• if vars(𝑃 𝑖 ) ∩ 𝑆 ≠ ∅, let 𝑟 = min(vars(𝑃 𝑖 ) ∩ 𝑆) and:

replace 𝑃 𝑖 by 𝑟 ;

-set 𝑆 := 𝑆 ∪ {𝑟 }; -for each 𝑗 ≥ 𝑖, replace 𝑃 𝑗 by 𝑃 𝑗 [𝑃 𝑖 ⊕ 𝑟 /𝑟 ].
• else, continue. This produces a normal form for any tuple (𝑃 1 , . . . , 𝑃 𝑛 ), where each 𝑃 𝑖 is either a fresh random variable (not appearing in the previous 𝑃s), or a linear combination of the previous 𝑃 1 , . . . , 𝑃 𝑖-1 .

Finally, two programs are universally equivalent if and only if they have the same normal form (up to 𝛼-renaming). Indeed, if they have the same normal form, they are trivially universally equivalent. Now, if they do not have the same normal form, there exists some 𝑖 such that 𝑃 𝑖 and 𝑄 𝑖 are two di erent expressions, and this imply non equivalence.

This basic decision prodcedures gives us a O (𝑛 × |𝑅|) complexity. Indeed, we treat each polynomial 𝑃 𝑖 or 𝑄 𝑖 only once, rst to apply the currenly known substitutions, and then to transform it into a fresh random if required. Applying the currently known susbtitutions may take up to |𝑅| loops, hence the considered complexity.

Corollary 25. 𝑞 ∞ -equivalence and 𝑞 ∞ -conditional equivalence restricted to arithmetic programs are in EXP.

Proof. [18, Corollary 2] provides a precise complexity for the evaluation of 𝑍 (𝑃). They provide an algorithm to compute 𝑍 (𝑃) for which there exist an explicit polynomial 𝑅 such that it runs in time 𝑅(𝑝 𝑚 𝑘 𝑚 𝑑 𝑚 2 2 𝑛 )), where 𝑑 is the sum of the degrees of the 𝑃 𝑖 . It is then polynomial in the degrees of the polynomials and the size of the nite elds, but exponential in the number of variables. In our, case, we need to compute three times 𝑍 , on polynomials depending over 2𝑚 variables (has we duplicate variables), which gives us en exponential in the size of our arithmetic programs.

Lemma 39. Given a CNF formula 𝜙 (𝐼, 𝑅) over two sets of variables and (∨, ∧), we can produce in polynomial time a program 𝑃 ∈ P 2 (𝐼, 𝑅) equivalent to 𝜙. ⇒ As outlined in [START_REF] Barthe | On the equality of probabilistic terms[END_REF], one can decide if 𝑃 ≈ 2 𝑄 by constructing a bijection represented by only linear terms (thanks to the weak primality of F 2 restricted to addition). We thus have a bijection 𝜎 without multiplication such that 𝑃 = 𝑄𝜎. 𝜎 is then a bijection over all F 2 𝑘 , and we do have 𝑃 ≈ 2 ∞ 𝑄.

Lemma 41. Let 𝑏 be a propositional formula built over built over atoms of the form 𝐵 = 0 or 𝐵 ≠ 0 with 𝐵 ∈ F 𝑞 [𝑋 ]. There exists 𝑋 ⊃ 𝑋 and polynomials 𝐵 1 , . . . , 𝐵 𝑛 ∈ F 𝑞 [𝑋 ] so that:

{𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑏} = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 1≤𝑖 ≤𝑛 𝐵 𝑖 = 0}
Those polynomials can be computed in exponential time.

Proof. We prove by induction of the formula that for any formula 𝑏, there exists polynomials 𝐵 1 , . . . , 𝐵 𝑛 so that:

{𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑏} = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 1≤𝑖 ≤𝑛 𝐵 𝑖 = 0}
We will assume that the formula are in conjunctive normal form, hence the exponential time. 𝑏 := 𝐵 = 0 Direct, with 𝑋 = 𝑋 and 𝐵 1 = 𝐵. 𝑏 := 𝐵 ≠ 0 For any 𝑘 and 𝑐 we have that: We reason by induction on the total number 𝑛 of conditional branching inside 𝑃 1 and 𝑄 1 . By basic transformations of the conditionals, we can assume that all conditions are of the form 𝐵 ≠ 0 (one can easily encode negations, conjunction and disjunction using conditionals branching). 𝑛 = 0 If there are no conditionals branching, the result is trivial. A di culty of this encoding is that it depends on the 𝑘, so it cannot be lifted to universal conditional equivalence. However, we can remove this di culty by using an extra variable 𝑡 to encode the 𝐵 𝑞 𝑘 -1 .

{𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝐵 ≠ 0} = {𝑋 ∈ F 𝑚 𝑞 𝑘 , 𝑡 ∈ F 𝑞 𝑘 | 𝑡𝐵 -1 = 0} Indeed,
𝑛 > 1
With 𝑡 a fresh variable, we denote ite(𝐵, 𝑃 𝑡 1 , 𝑃 Putting everything together, we get that: Conclusion We have shown by induction that we can remove all conditional branching. Each removal produces a new instance of polynomial size, and there is necessarily a polynomial number of conditional branching inside the programs. We thus reduces in exponential time C-EQUIV 𝑞 ∞ to C-EQUIV 𝑞 ∞ over programs without conditionals (recall that removing the failure cost an exponential).

𝐶 [if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ] | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ 𝐶 [𝑃 𝑓 1 + 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1 )] | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ 𝐶 [𝑃

Figure 1 :

 1 Figure 1: Summary of results related to equivalence

Figure 3 :

 3 Figure 3: Program syntax

Example 2 .

 2 Consider the following simple program 𝑖𝑛𝑣 (𝑖) ::= if 𝑖 = 0 then return 0 else 𝑟 $ ← -F; observe 𝑟 × 𝑖 = 1; return 𝑟

  𝑁 𝑘 (𝑄) ≤ 𝑁 𝑘 (𝑃) ⇔ Z (𝑃) -Z (𝑄) only has positive coe cients ⇔ ∀𝑛, 𝑧 𝑃𝑄 𝑛 ≥ 0

Proof.

  Given a CNF formula 𝜙 (𝐼, 𝑅) over two sets of variables and (∨, ∧) we transform 𝜙 into an equivalent formula 𝜙 over 𝐼 𝑅 and ⊕, ∧ in polynomial time w.r.t the size of the formula. Indeed, given a clause of 𝜙 of the form 𝑥 ∨ 𝑦 ∨ 𝑧, we have that 𝑥 ∨ 𝑦 ∨ 𝑧 = (𝑥 ⊕ 𝑦 ⊕ 𝑥𝑦) ∨ 𝑧 = (𝑥 ⊕ 𝑦 ⊕ 𝑥𝑦) ⊕ 𝑧 ⊕ (𝑥 ⊕ 𝑦 ⊕ 𝑥𝑦)𝑧 = 𝑥 ⊕𝑦 ⊕𝑥𝑦 ⊕𝑧 ⊕𝑥𝑧 ⊕𝑦𝑧 ⊕𝑥𝑦𝑧 = 𝑥 ⊕𝑦 ⊕𝑧 ⊕𝑥𝑦 ⊕𝑦𝑧 ⊕𝑥𝑧 ⊕𝑥𝑦𝑧. With this transformation, we have |𝜙 | ≤ 5×|𝜙 |. And then, 𝑃 = 𝜙 ∈ P 2 (𝐼, 𝑅) is a program equivalent to 𝜙. Lemma 40. Let 𝑃, 𝑄 ∈ P 2 (∅, 𝑅) without any multiplication. 𝑃 ≈ 2 𝑄 ⇔ 𝑃 ≈ 2 ∞ 𝑄 Proof. ⇐ Trivial direction.

𝑓 1 ) 1 + 1 + 1 + 1 ) 2 Finally 1 + 1 +

 11111211 = (𝑃 𝑓 𝑡𝐵(𝑃 𝑡 1 -𝑃 𝑓 1), 𝐵(𝐵𝑡 -1), 𝑡 (𝐵𝑡 -1)) Now, for any 𝑘 and 𝑐 we have that:[[(𝑃 𝑓 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1 ), 𝑃 2 )]] 𝑞 𝑘 (𝑐, ì 0) = {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑃 𝑓 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 = 𝑐 ∧ 𝑃 2 = ì 0} × 1 {F 𝑚 𝑞 𝑘 } = {𝑋 ∈ F 𝑚 𝑞 𝑘 , 𝑡 ∈ F 𝑞 𝑘 | ite(𝐵, 𝑃 𝑡 1 , 𝑃 𝑓 1 ) = (𝑐, ì 0) ∧ 𝑃 2 = ì 0} × 1 {F 𝑚 𝑞 𝑘 }Indeed, for any variable 𝑡 and polynomial 𝐵:(𝐵(𝐵𝑡 -1) = 0 ∧ 𝑡 (𝐵𝑡 -1) = 0) ⇔ 𝑡 = 𝐵 𝑞 𝑘 -𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1 ), 𝑃 2 )]] 𝑞 𝑘 (𝑐, ì 0) = {𝑋 ∈ F 𝑚 𝑞 𝑘 , 𝑡 ∈ F 𝑞 𝑘 | ite(𝐵, 𝑃 𝑡 1 , 𝑃 𝑓 1 ) = (𝑐, ì 0) ∧ 𝑃 2 = ì 0} × 1 {F 𝑚 𝑞 𝑘 } +| {F 𝑞 }| = [[(𝑃 𝑓 𝑡𝐵(𝑃 𝑡 1 -𝑃 𝑓 1), 𝐵(𝐵𝑡 -1), 𝑡 (𝐵𝑡 -1), 𝑃 2 )]] 𝑞 𝑘 (𝑐, ì 0)

𝑓 1 + 1 +

 11 𝑡𝐵(𝑃 𝑡 1 -𝑃 𝑓 1 )] | (𝐵(𝐵𝑡 -1), 𝑡 (𝐵𝑡 -1), 𝑃 2 ) ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2And we nally have:𝑃 1 | 𝑃 2 ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2 ⇔ 𝐶 [𝑃 𝑓 𝑡𝐵(𝑃 𝑡 1 -𝑃 𝑓 1 )] | (𝐵(𝐵𝑡 -1), 𝑡 (𝐵𝑡 -1), 𝑃 2 ) ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2The conditional equivalence on the right-side contains strictly one less conditional, we thus conclude by induction hypothesis.

  [𝑃 1 ]] 𝑞 𝑘 , [[𝑃 2 ]] 𝑞 𝑘 : F 𝑚 𝑞 𝑘 → Distr(F 𝑛 𝑞 𝑘 ).• 𝑞 𝑘 -equivalence (denoted 𝑃 1 ≈ 𝑞 𝑘 𝑃 2 ) requires that 𝑃 1 and 𝑃 2 de ne the same distributions:[[𝑃 1 ]] 𝑞 𝑘 = [[𝑃 2 ]] 𝑞 𝑘 .Equivalently, for every input ì 𝑎 ∈ F 𝑚 𝑞 𝑘 and output ì 𝑏 ∈ F 𝑛 𝑞 𝑘 ,

  𝑏 then 𝑒 1 else 𝑒 2 conditional branching | return (𝑃 1 , . . . , 𝑃 𝑛 ) return of arity 𝑛

		𝑃 2	eld multiplication
	𝑏 ::=		boolean conditions
	| 𝑃 = 0	atomic formula
	| 𝑏 1 ∧ 𝑏 2	and
	| 𝑏 1 ∨ 𝑏 2	or
	| ¬𝑏	not
	𝑒 ::=		program expressions
	| 𝑥 := 𝑃	assignment
	| ì 𝑟	$ ← -{𝑋 ∈ F 𝑚 | 𝑏}	sampling
	| observe 𝑏	observe
	| 𝑒 1 ; 𝑒 2	sequential composition
	| if

  C = P . Lemma 7. 2-equivalence is coNP C = P -hard. Proof. Given a CNF formula 𝜙 (𝐼, 𝑅) over two sets of variables and (∨, ∧) we set 𝑃 = 𝜙 ∈ P 2 (𝐼, 𝑅) obtained according to Lemma 39. Given a fresh random variable 𝑟 : 𝑃 (𝐼, 𝑅) ≈ 2 𝑟 ⇔ for all valuations of 𝐼 , 𝜙 is true for half of the valuations of 𝑅 ⇔ 𝜙 (𝐼, 𝑅) ∈ A-halfSAT Lemma 10. Let 𝑃 1 , . . . , 𝑃 𝑛 be programs over P 𝑞 𝑘 (𝐼, 𝑅), and 𝑌 ⊂ 𝑅. ⊥ 𝑌 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔⊥ 𝑞 𝑘 (𝑃 1 𝜎, . . . , 𝑃 𝑛 𝜎) where 𝜎 : 𝑌 → 𝐼 𝑌 is the substitution that replaces each variable in 𝑌 by a fresh input variable in 𝐼 𝑌 . 𝑞 𝑘 . [[𝑃 1 , . . . , 𝑃 𝑛 ]] 𝑞 𝑘 (𝑃 1 𝜎, . . . , 𝑃 𝑛 𝜎) Lemma 11. Let 𝑃 1 , . . . , 𝑃 𝑛 be programs over P 𝑞 𝑘 (𝐼, {𝑟 1 , . . . , 𝑟 𝑚 }) ⊥ 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔ (𝑃 1 , . . . , 𝑃 𝑛 ) ≈ 𝑞 (𝑃 1 𝜎1, . . . , 𝑃 𝑛 𝜎 𝑛 ) where 𝜎 𝑖 is the substitution that to any 𝑟 𝑗 associates a fresh random variable 𝑟 𝑖 𝑗 . Proof. ⊥ 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔ ∀ ì 𝑖 ∈ F |𝑋 | 𝑞 𝑘 . [[𝑃 1 , . . . , 𝑃 𝑛 ]]

	Proof.
	⊥ 𝑌 𝑞 𝑘 (𝑃 1 , . . . , 𝑃 𝑛 ) ⇔ ∀ ì 𝑖 ∈ F |𝑋 | 𝑞 𝑘 , ∀ ì 𝑖 ∈ F |𝑌 |		𝑞 𝑘 ì 𝑖, ì 𝑖	= ( [[𝑃 1 ]]	𝑞 𝑘 ì 𝑖, ì 𝑖	, . . . , [[𝑃 𝑛 ]]	𝑞 𝑘 ì 𝑖 𝑖, ì	)
	⇔ ∀ ì 𝑖 ∈ F |𝐼 𝐼 𝑌 | 𝑞 𝑘	. [[(𝑃 1 , . . . , 𝑃 𝑛 )𝜎]]	𝑞 𝑘 ì 𝑖	= ( [[𝑃 1 𝜎]]	𝑞 𝑘 ì 𝑖	, . . . , [[𝑃 𝑛 𝜎]]	𝑞 𝑘 𝑖 ì	)
	⇔⊥

  Proof. Indeed, for any 𝑛, let us denote 𝐷 𝑛 any subset of F 𝑚 𝑞 , where 𝑚 = | 𝑛 𝑞 |, such that |{𝐷 𝑛 }| = 𝑛. If we denote 𝑑 𝑛 a xed element of 𝐷 𝑚 , let 𝑇 𝑛 be the program: 𝑟 1 , . . . , 𝑟 𝑚

	$

[START_REF] Gaboardi | The complexity of verifying circuits as di erentially private[END_REF]

. For any 𝑘 ∈ N, 𝑞 𝑘 -0-majority reduces in polynomial time to 𝑞 𝑘 -0-majority with 𝑟 = 1.

  𝐵 is di erent from zero if and only if it is invertible, and thus if and only if there exist a single value 𝑡 such that 𝑡𝐵 = 1.𝑏 := 1≤𝑖 ≤𝑙 𝐵 𝑖 = 0 {𝑋 ∈ F 𝑚 𝑞 𝑘 | 1≤𝑖 ≤𝑙 𝐵 𝑖 = 0} = {𝑋 ∈ F 𝑚 𝑞 𝑘 | ( 1≤𝑖 ≤𝑙 𝐵 𝑖 ) = 0}𝑏 := 1≤𝑖 ≤𝑘 𝑏 𝑖 By induction hypothesis on each 𝑏 𝑖 we get 𝐵 𝑖 1 , . . . , 𝐵 𝑖 𝑛 𝑖 so that all of them verify:{𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑏} = {𝑋 ∈ F 𝑚 𝑞 𝑘 , 𝑡 ∈ F 𝑞 𝑘 | 1≤𝑖 ≤𝑘 1≤ 𝑗 ≤𝑛 𝑖 𝐵 𝑖 𝑗 = 0} 𝑏 := 𝑏 1 ∨𝑏 2 By induction hypothesis on 𝑏 1 we get 𝐵 1 , . . . , 𝐵 𝑛 , and on 𝑏 2 𝐵 1 , . . . , 𝐵 𝑛 , which satis es {𝑋 ∈ F 𝑚 𝑞 𝑘 | 𝑏} = {𝑋 ∈ F 𝑚 𝑞 𝑘 , 𝑡 ∈ F 𝑞 𝑘 | For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence restricted to programs without failures reduces in exponential time to 𝑞 𝑘 -conditional equivalence restricted to arithmetic programs. Proof. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (∅, 𝑅),𝑃 2 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅), without failures.

	Lemma 26.
	𝐵 𝑖 = 0 ∨	𝐵 𝑖 = 0}
	1≤𝑖 ≤𝑛	1≤𝑖 ≤𝑛

  We consider one of the inner most branching inside 𝑃 1 , i.e 𝑃 1 := 𝐶 [if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ] for some context 𝐶, and 𝑃 𝑡 1 , 𝑃 𝑓 1 arithmetic programs. For a xed 𝑘, we have a classical encoding of the if then else inside polynomials (cf CSF19):[[if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ]] 𝑞 𝑘 = [[𝑃 𝑓 1 + 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓1)]] 𝑞 𝑘 We then have that:𝐶 [if 𝐵 ≠ 0 then 𝑃 𝑡 1 else 𝑃 𝑓 1 ] | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 ⇔ 𝐶 [𝑃 𝑓 1 + 𝐵 𝑞 𝑘 -1 (𝑃 𝑡 1 -𝑃 𝑓 1 )] | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2

As PH ⊂ coNP PP , PP = coNP PP would imply PH ⊂ PP which is commonly believed to be false.

Universal equivalence for programs over nite elds with loops becomes undecidable.

As PH ⊂ coNP PP , PP = coNP PP would imply PH ⊂ PP which is commonly believed to be false.

Lemma 27. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence reduces to 𝑞 𝑘 -conditional equivalence restricted to programs without failures in exponential time.

Proof. Let 𝑃 1 , 𝑄 1 ∈ P 𝑞 (∅, 𝑅),𝑃 2 , 𝑄 2 ∈ P 𝑞 (∅, 𝑅).

Recall that observe are expressed using conditionals with a failure branch, and that sampling inside some speci c set can be encoded using the observe primitive. Without loss of generality, we can consider that ⊥ appears only once, as we can merge the conditions of the di erent failure branches inside a single one.

Then, 𝑃 1 is of the form 𝑃 1 := if 𝑏 then 𝑃 𝑡 1 else ⊥ for some program 𝑃 𝑡 1 which cannot fail. Now, with Lemma 41, we have 𝑅 ⊃ 𝑅 and polynomials 𝐵 1 , . . . , 𝐵 𝑛 ∈ F 𝑞 [𝑅 ] so that:

And then:

This allows us to conclude, when 𝜎 maps random variables to fresh ones, that:

We thus removed the failure on the left side of the conditional equivalence. Proceeding similarly on the right side yield the expected result.

Lemma 30. 𝑞-equivalence reduces in polynomial time to 𝑞 ∞ -equivalence.

Proof. Let 𝑃, 𝑄 ∈ P 𝑞 (∅, {𝑟 1 , . . . , 𝑟 𝑚 }). We directly have:

Proof. There exists 𝑙 𝑛 possible monomials (choosing the degree of each variable). Choosing the coe cient in {0, . . . , 𝑞 -1} for each monomials yeilds that the number of polynomials is bounded by 𝑞 𝑙 𝑛 . A program can, for each possible polynomial, performs a branching over it. There exists thus 𝑞 𝑙 𝑛 possible conditions, which when true may yield a polynomial (𝑞 𝑙 𝑛 possible choices) or ⊥. We nally obtain the expected result.

Lemma 33. For any 𝑙 ∈ N, 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -equivalence reduces in polynomial time to 𝑙, 𝑞 𝑘 -simulatability.

Proof. Let 𝑃, 𝑄 ∈ P 𝑞 (𝐼, 𝑅). Given two fresh variable 𝑎 and 𝑏, we set 𝐼 = 𝐼 {𝑎, 𝑏}. As previously, we lift additions and multiplications to tuples. Then,

Indeed, if 𝑃 ≈ 𝑞 𝑘 𝑄, then we trivially have 𝑎 + 𝑏𝑃 1 𝑞 𝑘 𝑎 + 𝑏𝑄 with 𝑆 as the identity. Let us assume that we have 𝑆 ∈ P 𝑞 ({𝑖}, 𝑅 ) such that deg(𝑆) ≤ 𝑙 and 𝑆 [ 𝑎+𝑏𝑄 / 𝑖 ] ≈ 𝑞 𝑘 𝑎 + 𝑏𝑃. We actually have the equivalence for any possible values we choose to give to 𝑎 and 𝑏. For instance, with 𝑏 = 0, we get that 𝑆 [ 𝑎 / 𝑖 ] ≈ 𝑞 𝑘 𝑎, which direclty implies that 𝑆 is the identity. Thus, with 𝑎 = 0 and 𝑏 = 1, we have that 𝑃 ≈ 𝑞 𝑘 𝑄. This concludes the proof.

Lemma 34. 𝑞 ∞ -0-majority restricted to linear programs is in PTIME.

Proof. We show that for linear programs 𝑃 ≺ 𝑟 𝑞 𝑘 𝑄 implies that 𝑃 ≈ 𝑞 𝑘 𝑄. Thus, universal majority is decidable, as universal equivalence is decidable for linear programs (and in PTIME).

Given 𝑃 1 , . . . , 𝑃 𝑛 ∈ P 𝑞 (∅, 𝑅) without multiplications, let us consider once again the normal form for linear programs. In this normal form, each 𝑃 𝑖 is either a random 𝑟 𝑖 , or a linear combination of some 𝑟 𝑗 , with 𝑗 < 𝑖. Let 𝐼 𝑃 be the set of indices 𝑖 such that 𝑃 𝑖 = 𝑟 𝑖 . We denote 𝑃 = (𝑃

Now, let us assume that there exists 𝑣𝑒𝑐𝑐 such that

We have proven that 𝑃 ≺ 𝑟 𝑞 ∞ 𝑄 ⇔ 𝑃 ≈ 𝑞 ∞ 𝑄, when restricted to linear programs without multiplications.

Lemma 36. 2 ∞ -0-majority is PP-hard.

Proof. We prove that 2-0-majority reduces to 2 ∞ -0-majority in polynomial time.

Let 𝑃, 𝑄 ∈ P 2 (∅, 𝑅).