Gilles Barthe

Charlie Jacomme

Steve Kremer

Universal equivalence and majority of probabilistic programs over finite fields

Keywords: Security and privacy → Logic and verification;, Theory of computation → Program reasoning program equivalence, probabilistic programs, finite fields, decidability and complexity

We study decidability problems for equivalence of probabilistic programs, for a core probabilistic programming language over finite fields of fixed characteristic. The programming language supports uniform sampling, addition, multiplication and conditionals and thus is sufficiently expressive to encode boolean and arithmetic circuits. We consider two variants of equivalence: the first one considers an interpretation over the finite field F 𝑞 , while the second one, which we call universal equivalence, verifies 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 first 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 differential privacy.

CCS Concepts:

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 specificity of our language is that it operates over finite fields 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 defined by assertions, and branching and conditioning are relative to assertions.

We consider two relational properties, equivalence and majority, which we define below, and several related properties, which we explain in the next paragraph. For each property, we consider two variants of the problem. In the first variant, which we call the fixed case, the value of 𝑘 is fixed. 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

[[𝑃 1 ]] 𝑞 𝑘 , [[𝑃 2 ]]
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 field, i.e.,

𝑃 1 ≺ 𝑟 𝑞 ∞ 𝑃 2 iff ∀𝑘. 𝑃 1 ≺ 𝑟 𝑞 𝑘 𝑃 2
The following two boolean programs illustrate the difference between equivalence and universal equivalence. 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

𝑥 $ ← -F; return (𝑥) 𝑥 $ ← -F; return (𝑥 + 1)
are 𝑞 ∞ -equivalent as both programs define the uniform distribution over F, whatever finite field is used for the interpretation of F. These examples also illustrate the difference with the well-studied polynomial identity testing (PIT) problem, as the first 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 fixed and universal variants of the equivalence and majority problems are directly inspired from applications in security and privacy. In the fixed setting, the equivalence and majority problems are related to probabilistic noninterference and differential privacy. The relationships between probabilistic non-interference and equivalence and between differential 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 iff for every 𝑥 1 and 𝑥 2 , the two programs 𝑃 𝑥 1 and 𝑃 𝑥 2 are equivalent. • differential privacy: for simplicity consider the case where the base field is F 2 . For every program 𝑃 with 𝑛 inputs, define the residual programs 𝑃 𝑖,0 and 𝑃 𝑖,1 obtained by fixing the 𝑖-th output to 0 and 1 respectively. Then the program 𝑃 is 𝑙𝑜𝑔(𝑟 )-differentially private iff 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 first contribution of the paper is a systematic study of the complexity of the aforementioned problems in the fixed setting. We prove that the 𝑞 𝑘 -equivalence problem is coNP C = P -complete for any fixed 𝑘. 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 first, unless PH ⊂ PP1 . 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 finite case, since we only derive easy consequences of equivalence. These results complement recent work on the complexity of checking differential privacy for arithmetic circuits [START_REF] Gaboardi | The Complexity of Verifying Circuits as Differentially 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 finite field. Lauder and Wan [START_REF] Alan | Counting points on varieties over finite fields 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 specific 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 simpler methods fail or only provide sufficient conditions. Our decidability result significantly 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 loworder 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 satisfies 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 efficient solution. Using the results from [START_REF] Kiefe | Sets definable over finite fields: their zetafunctions[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 finite case to the universal case. It remains an interesting open question whether the universal case is strictly harder than the finite 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 Refinement[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 verification of probabilistic programs[END_REF] prove decidability of equivalence for a probabilistic programming language over finite 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 certification 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 differential privacy or for quantifying information flow.

Frederikson and Jha [START_REF] Fredrikson | Satisfiability modulo counting: A new approach for analyzing privacy properties[END_REF] develop an abstract decision procedure for satisfiability 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 Differential Privacy[END_REF] show decidability of 𝜖-differential 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 𝜖-differential 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 polynomialtranscendental problems[END_REF]. Gaboardi, Nissim and Purser [START_REF] Gaboardi | The Complexity of Verifying Circuits as Differentially Private[END_REF] study the complexity of verifying pure and approximate (𝜖, 𝛿)-differential privacy for arithmetic programs, as well as approximations of the parameters 𝜖 and 𝛿. The parameter 𝛿 quantifies the approximation and 𝛿 = 0 corresponds to the pure case. Our majority problem can be seen as a subcase of differential privacy, where 𝑟 corresponds to 𝜖, and 𝛿 = 0. In particular, the complexity class they obtain for pure differential 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 verification problem. Also, while they consider arithmetic programs, we consider the more general case of programs with conditioning.

𝑥-(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
Chistikov, Murawski and Purser [START_REF] Chistikov | Asymmetric Distances for Approximate Differential Privacy[END_REF] also study the complexity of approximating differential privacy, but in the case of Markov Chains.

Theory of fields.

A celebrated result by Ax [START_REF] Ax | The elementary theory of finite fields[END_REF] shows that the theory of finite fields is decidable. In a recent development based on Ax's result, Johnson [START_REF] Andrew | Fun with fields[END_REF] proves decidability of the theory of rings extended with quantifiers 𝜇 𝑛 𝑘 𝑥 . 𝑃, 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 define its formal semantics.

𝑃 ::= polynomials | 𝑖 ∈ F 𝑞 fixed value | 𝑥 variable | 𝑃 1 + 𝑃 2 field addition | 𝑃 1 × 𝑃 2 field 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 𝑏 then 𝑒 1 else 𝑒 2 conditional branching | return (𝑃 1 , . . . , 𝑃 𝑛 ) return of arity 𝑛 Figure 3. Program syntax

Syntax and informal semantics

We define in Figure 3 the syntax for simple probabilistic programs (without loops nor recursion2 ). Our programs will operate on finite fields. We denote by F 𝑞 the (unique) finite field with 𝑞 elements, where 𝑞 = 𝑝 𝑠 for some integer 𝑠 and prime 𝑝. Programs are parametrized by a finite field 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 first one is not 0. Note that the use of polynomial conditions allows to express any rational distribution over the base field 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.

if 𝑖 = 0 then return 0 else 𝑟 $ ← -F; observe 𝑟 × 𝑖 = 1; return 𝑟
This program defines a probabilistic algorithm for computing the inverse of a field 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 , replacing "𝑟 $ ← -F; observe 𝑟 × 𝑖 = 1;" by

"𝑟 $ ← -{𝑥 ∈ F | 𝑥 × 𝑖 = 1};".

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 define this core language, we add an explicit failure instruction ⊥, similarly to [START_REF] Bichsel | Fine-grained Semantics for Probabilistic Programs[END_REF]

← -{𝑋 ∈ 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 simplified expressions (𝑒 1 , . . . , 𝑒 𝑛 ) defined as follows.

𝑒 ::= simplified expressions | 𝑃 polynomial | ⊥ failure | if 𝑏 then 𝑒 1 else 𝑒 2 conditional branching
We suppose that all nested tuples are flattened 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 define 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 first define a deterministic semantics where all random samplings have already been defined. For a set 𝑋 of variables, with 𝑃 ∈ F 𝑞 [𝑋 ]

𝑞 𝑘 ì 𝑣 = 𝑃 (ì 𝑣) where 𝑃 ∈ F 𝑞 [𝐼 ⊎ 𝑅] [⊥] 𝑞 𝑘 ì 𝑣 = ⊥ if 𝑏 then 𝑒 1 else 𝑒 2 𝑞 𝑘 ì 𝑣 = [𝑒 1 ] 𝑞 𝑘 ì 𝑣 if 𝑏 (ì 𝑣) holds on F 𝑞 𝑘 [𝑒 2 ] 𝑞 𝑘 ì 𝑣 else [(𝑒 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 define 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 define 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 defined as we supposed that programs do not always fail.

The fixed case

We start by studying the complexity of several problems over a given finite field. In this case we only manipulate finite 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 defined by counting quantifiers[END_REF]. We also define 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

| = |𝑄 1 | = 𝑛. We denote 𝑃 1 | 𝑃 2 ≈ 𝑞 𝑘 𝑄 1 | 𝑄 2 , if: ∀ ì 𝑖 ∈ F |𝐼 | 𝑞 𝑘 . ∀ì 𝑐 ∈ F 𝑛 𝑞 𝑘 . [[(𝑃 1 , 𝑃 2 )]] 𝑞 𝑘 ì 𝑖 (ì 𝑐, ì 0) = [[(𝑄 1 , 𝑄 2 )]] 𝑞 𝑘 ì 𝑖 (ì 𝑐, ì 0)
The universal version 𝑞 ∞ -conditional equivalence is defined similarly to 𝑞 ∞ -equivalence . 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 first define precisely the decision problems associated to our questions, for 𝑘 ∈ N ∪ {∞}:

𝑞 𝑘 -conditional equivalence input: 𝑃 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.

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 problem: is a CNF boolean formula 𝜙 satisfied 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: given a CNF boolean formula 𝜙 (𝑋, 𝑌 ), for all valuations of 𝑋 is the formula satisfied 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 first study the complexity of deciding if the distributions of two programs are equal on a specific 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 3.2. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence reduces to 𝑞 𝑘 -conditional equivalence restricted to programs without inputs in polynomial time.

Omitted proofs can be found in [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF]. 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 specific 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 3.3. 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)
As C = P is closed under finite 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 fixed size are equal, by testing the equality over all points. When we only consider inputless programs of fixed arity, the set of points to test is constant, and the equivalence problem is in C = P (see [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF] 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 3.4. 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence are in coNP C = P for any 𝑘 ∈ N.

To conclude completeness for both 𝑞 𝑘 -equivalence and 𝑞 𝑘 -conditional equivalence, it is sufficient 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 [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF]). Lemma 3.5. 2-equivalence is coNP C = P -hard.

The results about 𝑞 𝑘 -conditional equivalence naturally translate to the independence problem: are the distribution of multiple programs independent? We obtain the same complexity class by proving that the problems are interreducible. These results are detailed in [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF].

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 finite intersection, it yields the complexity of 𝑞 𝑘 -majority, which can be decided using 𝑞 𝑘 times 𝑞 𝑘 -0-majority.

3.2.1

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 differential 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 difference between equivalence and majority is that the presence of inputs actually changes the complexity of the majority problem.

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

𝑞 𝑘 -majority input: 𝑃, 𝑄 ∈ 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.

We recall that PP is the set of languages accepted by a polynomial time non-deterministic Turing Machine where the acceptance condition is that a majority of paths are accepting. A natural PP-complete problem is MAJSAT: is a boolean CNF formula satisfied 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] , which given a CNF boolean formula 𝜙 (𝑋, 𝑌 ), asks if there is a valuation of 𝑋 such that 𝜙 (𝑋, 𝑌 ) is satisfied for at least half of the valuation of 𝑌 .

The complexity of 𝑞 𝑘 -0-majority over inputless programs is derived in a similar way as for equivalence. (j'ai remplacé un paragraphe par ça) The only difficulty is that we are comparing with a rational. We thus briefly 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 3.6. 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 3.7. For any 𝑘 ∈ N, 𝑞 𝑘 -0-majority restricted to inputless programs is PP-complete.

Finally, as PP is closed under finite intersection, we also get that 𝑞 𝑘 -majority over inputless programs with a fixed 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 3.8. 𝑞 𝑘 -majority is coNP PP complete.

The universal case

In this section we first give some general insights on universal equivalence showing important differences with the case of a fixed field. Then we provide our main decidability result, first for arithmetic programs, then arithmetic programs enriched with conditionals, and finally 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 difficulty of deciding 𝑞 ∞ -equivalence. First of all, we note that equivalence and universal equivalence do not coincide.

Example 4.1. 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 finite field, 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 | Unification 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 field (i.e., 𝑋 𝑞 = 𝑋 ).

𝑃 ≈ 𝑞 𝑄 ⇔ ∃𝜎 ∈ bij F 𝑚 𝑞 , 𝑃 = F 𝑞 𝑄𝜎
However, there are universally equivalent programs such that there does not exist a universal 𝜎 suitable for all extensions.

Example 4.2. Consider, 𝑃 = 𝑥𝑦+𝑦𝑥+𝑧𝑥, with 𝜎 : (𝑥, 𝑦, 𝑧) ↦ → (𝑥, 𝑦 + 𝑥, 𝑧 + 𝑥), we get that 𝑃 ≈ 2 ∞ 𝑥 2 + 𝑦𝑧. Now, 𝑥 ↦ → 𝑥 2 is a bijection over all F 2 𝑘 , so we also have 𝑃 ≈ 2 ∞ 𝑥 + 𝑦𝑧 and finally 𝑃 ≈ 2 ∞ 𝑥.

But here, a bijection between 𝑥 2 + 𝑦𝑧 and 𝑥 must use the inverse of 𝑥 2 whose expression depends on the size of the field. 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 finite field, 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. Moreover, building on results from [START_REF] Maubach | The automorphism group over finite fields[END_REF] on Tame automorphisms, we can use the above characterization to design a sufficient condition which implies universal equivalence for general programs. Even though not complete this sufficient condition may be useful to verify universal equivalence more efficiently in practice. These results are detailed in [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF].

Decidability of universal equivalence

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

1

(𝑃) = { ì 𝑥 ∈ F 𝑛 𝑞 𝑘 | 1≤𝑖 ≤𝑚 𝑃 𝑖 ( ì 𝑥) = 0}.
Weil's conjecture [START_REF] Weil | Numbers of solutions of equations in finite fields[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 coefficients-recall that 𝑍 (𝑇 ) is a rational function iff there exist polynomials 𝑅(𝑇 ) and 𝑆 (𝑇 ) such that 𝑍 (𝑇 ) = 𝑅(𝑇 )/𝑆 (𝑇 ). Bombieri [START_REF] Bombieri | On exponential sums in finite fields[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 suffice 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 different 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 effectively be computed [START_REF] Alan | Counting points on varieties over finite fields 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 field. Moreover, thanks to [START_REF] Kiefe | Sets definable over finite fields: their zetafunctions[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 first order formula over finite fields. Corollary 4.4. Let 𝜙 and 𝜓 be two first 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 first order formula over finite field one can verify if they happen with the same probability over all extensions of the base field. Remark that this cannot be used to decide universal equivalence, as equivalence cannot be expressed inside a first order formula.

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

4.5. 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 char- acterizes the distribution of 𝑇 |𝑇 ′ , as 𝑃 1 | 𝑃 2 ≈ 𝑞 ∞ 𝑄 1 | 𝑄 2 if and only if ∀𝑘 ∈ N. -------→ (𝑃 1 , 𝑃 2 ) 𝑘 = -------→ (𝑄 1 , 𝑄 2 ) 𝑘 . Using the classi- cal 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 [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF], we provide a variant of this result for the specific 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 [START_REF] Alan | Counting points on varieties over finite fields of small characteristic[END_REF]Corollary 2] we obtain the following corollary.

Corollary 4.6. 𝑞 ∞ -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 first idea is to use a classical encoding inside finite fields:

[[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 field, i.e., it must be independent of 𝑘. The key idea is that for any variable 𝑡 and polynomial 𝐵:

(𝐵(𝐵𝑡 -1) = 0 ∧ 𝑡 (𝐵𝑡 -1) = 0) ⇔ 𝑡 = 𝐵 𝑞 𝑘 -2
We can then encode conditionals as a multiplication by some fresh variable 𝑡, where 𝑡 is conditioned by the previous conditions. An induction on the number of conditionals yields our second lemma. Lemma 4.7. For any 𝑘 ∈ N ∪ {∞}, 𝑞 𝑘 -conditional equivalence restricted to programs without failures reduces in exponential time to 𝑞 𝑘 -conditional equivalence restricted to arithmetic programs.

Recall that failures define 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 difficult 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 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 different from zero. We can thus have:

if

𝑏 = 0 then 𝑃 1 else ⊥ | 𝑃 2 ≈ 𝑞 𝑘 𝑄 | 0 ⇔ 𝑃 1 | 𝑃 2 , 𝑏 ≈ 𝑞 𝑘 𝑄 | 𝑡𝑏 -1
Using those techniques, we obtain: Lemma 4.8. 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 4.9. 𝑞 ∞ -equivalence and 𝑞 ∞ -conditional equivalence are in 2-EXP.

And using once again [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF], we obtain the same complexity results for the independence problem. Corollary 4.10. 𝑞 ∞ -conditional independence is in 2-EXP.

Moreover, we can also extend the lower bound obtained for 𝑞-equivalence. Lemma 4.11. 𝑞-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). Definition 4.12. 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 input: 𝑃, 𝑄 ∈ 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 [START_REF] Barthe | Universal equivalence and majority on probabilistic programs over finite fields[END_REF]. From the bound on the number of contexts and the decidability of universal equivalence, one can derive the decidability of bounded simulatability.

  ; return (𝑥 2 + 𝑥)

Figure 1 .

 1 Figure 1. Summary of results related to equivalence

Figure 2 .

 2 Figure 2. Summary of results related to majority

Example 2 . 1 .

 21 Consider the following simple program :

Lemma 4 . 3 .

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

Lemma

  [[𝑃]] 𝑞 𝑘 (ì 𝑐) × 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 ⇔ ∀ì 𝑐.[[𝑃 1 , 𝑃 2 , 𝑏]] 𝑞 𝑘 (ì 𝑐, ì 0) = P{¬(𝑏 = 0)}[[𝑄]] 𝑞 𝑘 (ì 𝑐)

  𝑞 𝑘 : F 𝑚 𝑞 𝑘 → Distr(F 𝑛 𝑞 𝑘 ). • 𝑞 𝑘 -equivalence (denoted 𝑃 1 ≈ 𝑞 𝑘 𝑃 2 ) requires that 𝑃 1 and 𝑃 2 define the same distributions: [[𝑃 1 ]] 𝑞 𝑘 = [[𝑃 2 ]] 𝑞 𝑘 𝑞 𝑘 -majority requires that for a fixed 𝑟 ∈ Q, and for every input ì 𝑎 ∈ F 𝑚 𝑞 𝑘 and output ì 𝑏 ∈ F 𝑛 𝑞 𝑘 , we have

	•
	. Equiva-
	lently, for every input ì 𝑎 ∈ F 𝑚 𝑞 𝑘 and output ì 𝑏 ∈ F 𝑛 𝑞 𝑘 ,
	P{ ì 𝑥 = ì 𝑏 | ì 𝑥

  . 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 , . . . , 𝑟 𝑚 $

  𝑞 𝑘 . We also denote 𝑏 (ì 𝑣) the evaluation of a boolean test, where all polynomials are evaluated according to ì 𝑣. For a program 𝑒 ∈ P 𝑞 (𝐼, 𝑅) and ì 𝑣 ∈ F |𝐼 ∪𝑅 | 𝑞 𝑘 , we define a natural evaluation of 𝑒, denoted [𝑒]

	𝑞 𝑘 ì 𝑣 , which is a value inside F |𝑃 | 𝑞 𝑘 × {⊥}:
	[𝑃]

and ì 𝑥 ∈ F |𝑋 | 𝑞 𝑘 , 𝑃 ( ì 𝑥) classicaly denotes the evaluation of 𝑃 inside F

  . 𝑞 ∞ -conditional equivalence is decidable for arithmetic programs; (Lemma 4.5) 2. it is also decidable for programs with conditionals; (Lemma 4.7) 3. it is finally decidable for programs with conditioning, e.g. failures. (Lemma 4.8) We first recall the definition 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 𝑁 𝑘

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

Universal equivalence for programs over finite fields with loops becomes undecidable.

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

Acknowledgements. We wish to thank the anonymous reviewers for their useful comments, as well as Martin Grohe, Bruce Kapron, David Mestel, Joël Ouaknine, Pierre-Jean Spaenlehauer, Emmanuel Thomé and Mehdi Tibouchi for interesting discussions. We are grateful for the support by the ERC under the EU's Horizon 2020 research and innovation program (grant agreement No 645865-SPOOC) as well as ONR (grant N000141512750).

Theorem 4.13. l,q-simulatability is decidable.

As a lower bound, we prove that 𝑙, 𝑞-simulatability is as hard as universal equivalence: Lemma 4.14. 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 infinite sequence of reals 𝑢 = 𝑢 1 , 𝑢 2 , . . . such that there exist real constants 𝑎 1 , . . . , 𝑎 𝑘 such that for all 𝑛 ≥ 0,

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 coefficients of the first 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 4.15. 𝑞 ∞ -0-majority restricted to linear programs is in PTIME.

The general case has yet to be proven decidable. Theorem 4.16. 𝑞 ∞ -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 simplifications 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 coefficients of Z (𝑃) -Z (𝑄) are 𝑁 𝑘 (𝑃) -𝑁 𝑘 (𝑄), we have that ∀𝑘, 𝑁 𝑘 (𝑃) ≥ 𝑁 𝑘 (𝑄) if and only if Z (𝑃) -Z (𝑄) only has positive coefficients.

It is well known that the coefficients 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 coefficients of Z (𝑃) -Z (𝑄) form an LRS, which we denote 𝑧 𝑃𝑄 . We finally get that 𝑄 ≺ 𝑞 ∞ 𝑃 if and only if ∀𝑛, 𝑧 𝑃𝑄 𝑛 ≥ 0. □ This reduction can also be applied with the generalization of [START_REF] Kiefe | Sets definable over finite fields: their zetafunctions[END_REF], and thus, for any two events about programs over finite fields, one can, given an oracle for the POSITIVITY problem, decide if the probability of the first event is greater than the second one for all extensions of the base field.

Similarly to the equivalence case, we can derive some hardness from the non universal case, but we do not obtain any completeness result. Lemma 4.17. 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 verification. 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.


Baochen Ma

Qing Jiao

Yeting Zhang

Changgui Lin

Xianghua Zhang

Hongli Ma

Shixun Dai

Conductivity and Structural Properties of Fast Ag-Ion-Conducting GaGeSbS-AgI glassy Electrolytes

Keywords: Sulfide solid electrolyte, Superionic conductor, Electrochemical behavior, AC impedances spectroscopy

The use of ion-conducting chalcogenide glass, a promising solid electrolyte, is encouraged at higher conductivity for all-solid-state rechargeable battery. Herein, a new quaternary glass of GaGeSbS-AgI system was successfully prepared, and its structural and electrochemical properties were investigated by XRD, Raman, and AC impendence measurement. The relatively high conductivity of 2.955 × 10 -3 S/cm and low activation energy of 0.07 eV were obtained after optimized structure regulation. The short-range schematic of the glass structure was explored to determine the fast-migrating mechanism involved in conducting Ag + ions. By controlling the proper ratio of Ga(Ge) and Sb cations, the loose and porous layer structure of [SbS x I 3-x ] linking by the [Ga(Ge)S 4 ] tetrahedron was formed, resulting in the rapid transport of Ag + ions with a reduced migration energy barrier. The current work is the first time that a sulfide solid electrolyte in quaternary glass system with desirable electrochemical characteristics was used to address energy and safety issues.

Introduction

The improvement of global human living standards has led to a huge demand for energy consumption, especially for hybrid electric vehicles and portable energy storage devices [START_REF] Chen | Approaching Practically Accessible So lid -State Batteries: Stability Issues Related to Solid Electro lytes and Interfaces[END_REF][START_REF] Kato | High-power all-solid-state batteries using sulfide superionic conductors[END_REF][START_REF] Yang | Towards high-performance solid-state Li-S batteries: fro m fundamental understanding to engineering design[END_REF][START_REF] Zhou | Engineering Materials for Progressive All-So lid-State Na Batteries[END_REF]. Traditional lithium-ion liquid batteries have been widely used in the commercial market due to their qualified energy density (≈ 250 Wh/kg) [START_REF] Zhang | Sulfide-Based Solid-State Electro lytes: Synthesis, Stability, and Potential for A ll-Solid-State Batteries[END_REF][START_REF] Lian | Inorganic sulfide solid electrolytes for all-solid-state lithiu m secondary batteries[END_REF][START_REF] Fit | The effects of mechanical constriction on the operation of sulfide based solid-state batteries[END_REF]. Nevertheless, owing to the frequent reports of liquid electrolyte leakage and thermal instability, the simultaneous achievement of high power and safety in current electrochemical devices seemed impossible [START_REF] Wan | Status, promises, and challenges of nanocomposite solid-state electrolytes for safe and high performance lithiu m batteries[END_REF][START_REF] Zhu | Role o f Na + Interstitials and Dopants in Enhancing the Na + Conductivity of the Cubic Na3PS4 Superionic Conductor[END_REF]. Therefore, A c c e p t e d m a n u s c r i p t all-solid-state batteries with inorganic electrolytes have the potential to solve the problems related to safety and high energy density [START_REF] Sakuda | Metastable Materials for All-Solid-State Batteries[END_REF]. Sulfide solid glass electrolytes have become the focus of research because of their superior properties, such as high polarization and large ionic radius of S 2-, which effectively improve ionic diffusion and room temperature conductivity. Meanwhile, the conduction pathways are isotropic and flexible due to the absence of crystalline passageways in the network. Ionic transport is accelerated by the amorphous network without grain boundary, contributing to the increase in ionic conductivity by several orders of magnitude compared with crystallines [START_REF] Zhao | Designing solid-state electrolytes for safe, energy-dense batteries[END_REF]. Moreover, sulfide glass with loosened transport channels and low binding energy is considered a candidate ionic conductor in producing efficient solid electrolytes [START_REF] Lin | Fast Ag-ion-conducting GeS2-Sb2S3-AgI glassy electrolytes with exceptionally low act ivation energy[END_REF].

However, the low ionic conductivity of solid electrolytes hinders the performance of solid-state batteries. Hence, the exploration of sulfide electrolytes with excellent room-temperature ionic conductivity has become a significant challenge in terms of system design and structural optimization in recent years. The glass former (GeS 2 , As 2 S 3 , Sb 2 S 3 ) doped with metal compounds, including alkali-metal ions Li + , Na + , and K + and transition-metal ions Ag + and Cu + , was chosen for the solid electrolyte because of its good glass-forming ability and electrochemical properties [START_REF] Fan | Ionic conductive GeS2-Ga 2S3-Li2S-LiI glass powders prepared by mechanical synthesis[END_REF][START_REF] Hayashi | A sodium-ion sulfide solid electro lyte with unprecedented conductivity at room temperature[END_REF][START_REF] Marp Le | Superionic conduction of silver in ho mogeneous chalcogenide glasses[END_REF]. The ternary glass system formed by aliovalent cations doping, such as GeGaS and GeSbS, is widely studied. In 2008, the conductivity of (100-2x)GeS 2 -xGa 2 S 3 -xAgI (1.2 × 10 -6 S/cm) was reported by Stehilk et al. [START_REF] Stehlik | Diffusion of Ag ions under rando m potential barriers in silver-containing chalcogenide glasses[END_REF]. Then, the conductivity of AgI-doped GeSbS ternary glass system was raised to the commercially available magnitude of 10 -3 S/cm through the regulation of the Ge/Sb ratios in the glass matrix [START_REF] Lin | Fast Ag-ion-conducting GeS2-Sb2S3-AgI glassy electrolytes with exceptionally low act ivation energy[END_REF]. One of the effective ways to improve ionic conductivity is aliovalent ion substitution. The charge-compensating induction vacancies or interstitials increased the degree of disorder in the matrix, which benefits the carrier's long-range diffusion through the glass network. The control preparation of the sulfide glass materials and the design of the ions' migration pathways are promising measures that can be used to achieve higher ion conductivity for secondary batteries.

A c c e p t e d m a n u s c r i p t

In this work, two series of glass samples 60[x(Ga 2 S 3 -3GeS 2 )-(1-4x)Sb 2 S 3 ]-40AgI and (100-y)(0.1Ga 2 S 3 -0.3GeS 2 -0.6Sb 2 S 3 )-yAgI were prepared by melt quenching method. The optimized ionic channel was expected to obtain from the composition design aiming to achieve the high ionic conductivity with increasing silver dopant concentration. Germanium sulfide is used as a virtuous network former to easily form glasses with or without other alloy compounds. The mixed-cation effect, such as that in Sb 2 S 3 and Ga 2 S 3 sulfides, further enhances conductivity and stability with controlled coordination polyhedrons in the Ag ion conductive glass. The GaGeSbS-AgI glass system in the current work has a wide glass-forming region and favorable ionic conductivity of 2.95 × 10 -3 S/cm, which is higher than those of most sulfide electrolytes doped with halide salt. This work is our first attempt to synthesize a sulfide solid electrolyte in a quaternary glass system with desirable electrochemical characteristics.

Experimental

The samples of the system 60[x(Ga 2 S 3 -3GeS 2 )-(1-4x)Sb 2 S 3 ]-40AgI (A-series, x = 0.1, 0.15, 0.2 mol%) and (100-y)(0.1Ga 2 S 3 -0.3GeS 2 -0.6Sb 2 S 3 )-yAgI (B-series, y = 50, 55, 60 mol%) were prepared by conventional melt quenching technique in sealed silica ampules (∼10 -3 Pa) with high-purity materials including Ga, Ge, Sb, S, and AgI compounds [START_REF] Hilton | Chalcogenide Glasses for infrared optics[END_REF]. The batches of about 15 g were heated to 950 °C for 12 h, quenched and then annealed. The obtained rod-like glass was processed into 10-and 2 mm-thick discs. The samples of A-series were abbreviated as (GG)Sb z (z = 0.2, 0.4, 0.6).

Confirmation of crystallographic and amorphous state of the prepared sample was performed by XRD measurement (Bruker D2 Phaser; Cu Kα; 10 mA, 30 kV). The calorimetric measurement was performed using DSC (TA Q2000 Thermal Analysis) with a scan rate of 10 °C/min. The prepared disc was polished optically and then sputtered with Au for electrochemical tests. The as-prepared samples were evaluated using AC impedance method for ionic conductivity at 30 °C-100 °C and 1 Hz-1 MHz. Structure detection was conducted at room temperature using a Raman spectrometer with a 785 nm LD laser (Renishaw inVia, Thermodynamic properties of as-prepared samples were investigated by DSC detection in Fig. 2. In the case of A-series, the values of T g presented a rising trend with increasing addition of Sb 2 S 3 component, and this trend was related to the intensified degree of cross-linking network.

A c c e p t e d m a n u s c r i p t

The tetra-coordinated [Ga(Ge)S 4 ] units in the matrix provided more covalent bonding connections than tri-coordinated [SbS 3 ] units, resulting in a higher degree of network linkages. Meanwhile, the elimination of non-bridging sulfurs (NBS) in the network enhanced the interconnections between the structural units. However, in the case of the B-series, I -ions were introduced into the matrix to serve as network terminator, which reduced the compactness of the glass network [START_REF] Li | Fo rmation and properties of chalcogenide glasses based on GeS2-Sb2S3-AgI system[END_REF]. Eventually, the T g of the 60 mol%-doped AgI sample became well maintained at 166 °C, indicating that a high operating temperature can be realized in this glass electrolyte. Fig. 3 presented the ionic conductivity of A-series samples as a function of temperature. The calculated conductivity of each sample was obtained from the relationship of σ=R -1 D/S, where D is the sample thickness, and S represents the gold-coated area of the electrodes. High room temperature conductivity (2 × 10 -5 S/cm) was obtained in (GG)Sb 0.6 sample of A-series, which reveals the optimized component for the improvement of ionic conductivity. With increasing temperature, the conductivity of all the A-series samples showed a significant enhancement. However, the differences in the increase in amplitude indicated the intrinsic differences of the ionic channels for the designed samples. The representative Nyquist plot of B-series samples with different concentrations of AgI is given in Fig. 4, where Zre′ and -Zim′′ represent the resistance and reactance of bulk-samples, respectively. The presence of a semicircle (or half) and a spike, which indicated the typical behavior of an ionic conductor, was observed in the high-and low-frequency regions of the current. Lower resistance was realized with increasing ionic Ag + content, leading to an excellent room temperature conductivity of 2.955×10 -3 S/cm in the 60 mol% AgI sample. In general, the samples showed good fitting according to the Arrhenius Law, which was expressed as follows:

𝜎 = 𝐴𝑒𝑥𝑝 (- 𝐸 𝑎 𝑅𝑇 )
where A is the pre-exponential factor, R is the Boltzmann constant, T is the absolute temperature, and E a is the activation energy. In theory, the barrier energy associated with optimized migration path was characterized by the magnitude of the E a. The E a values of samples doped with 50, 55, and 60 mol% AgI were calculated to be 0.1, 0.08, and 0.07 eV, respectively, which were relatively lower value compared with those of other sulfide solid electrolytes, such as GeSbSe-Ag (0.32 eV) and GeGaSe-AgI (0.28 eV) glass systems [START_REF] Marp Le | Superionic conduction of silver in ho mogeneous chalcogenide glasses[END_REF][START_REF] Tang | Thermal properties, microstructure, and conductivity of new glasses based on the GeSe2-Ga2Se3-AgI system[END_REF]. To explore the effect of the structure nature of the sample on the conductivity characteristic, the samples were subjected to the Raman test. The obtained Raman spectrum of A-series samples is shown in Fig. 5; it consists of a broad band between 100 and 500 cm -1 . Considering the significant changes of the ionic channels, the detailed analysis of the spectra was divided into Sb-related and Ga(Ge)-related vibrations. For (GG)Sb 0.2 sample, the primary peak near 308 cm -1 was attributed to the vibrations of [SbSI] units. However, the peak position shifted to a higher wavenumber at 318 cm -1 with increasing Sb 2 S 3 in the network. Moreover, the band near 162 cm -1 , which belongs to [SbI 3 ] units, appeared with the increased substitution of the Sb 2 S 3 component. On the contrary, the peak shoulder from 230 cm -1 to 260 cm -1 represented the structural units of [GeS x I 4-x ], thereby increasing the vibration dependence of the Ge(Ga) ratios. The band around 265 cm -1 is related to the metal bonds of [Ga(Ge)-Ga(Ge)] and occurred at x = 0.2 but not at x = 0.1, indicating the formation of a sulfur-deficient environment in the glass network. The increasing bands near 345 and 408 cm -1 were associated with the vibrations of edge-or corner-shared [Ga(Ge)S 4 ] units. Interestingly, the band at 212 cm -1 was related to the covalent bonds of Ag-S and was observed at x = 0.1. This band then disappeared with decreasing amount of Sb component and Ga(Ge) units. The results indicated that a high A c c e p t e d m a n u s c r i p t number of defect sites correlated with Ag + migration were possibly provided by the S-rich network [START_REF] Guo | Structural evolution study of additions of Sb2S3 and CdS into GeS2 chalcogenide glass by Raman spectroscopy[END_REF][START_REF] Zhang | The effects of germaniu m addition on properties of Ga-Sb-S chalcogenide glasses[END_REF][START_REF] Lin | Network Structure in GeS2-Sb2S3 Chalcogenide Glasses: Raman Spectroscopy and Phase Transformation Study[END_REF][START_REF] Ichikawa | Glass formation, physico -chemical p roperties, and structure of glasses based on Ga2S3-GeS2-Sb2S3 system[END_REF]. Based on the evolution of network caused by the substitution, the specific formation of ionic channel and its effect on the ion's diffusion were reasonably evaluated. When a large amount of Sb was introduced into the network, I -ions were more likely to combine with Sb ions, thereby forming the units of [SbS x I 3-x ], which enlarged the channel size and volume due to the large ionic radius. Meanwhile, the Ga(Ge) preferred to form the [Ga(Ge)S 4 ] tetrahedron in the S-rich environment, and their shared S -bonds were expected to present two different behaviors in the network. First, the [SbS x I 3-x ] units were coordinated with bridging sulfur bonds given by [Ga(Ge)S 4 ] tetrahedron, which effectively prevented the aggregation of [SbSI] units, thereby preventing devitrification. However, abundant defect sites (i.e., unstable and active Ag-S bonds), which reduced the distance among the Ag + ions and decreased the activation energy, were provided by the non-bridging sulfur of [Ga(Ge)S 4 ] tetrahedron [START_REF] Pat Il | Percolation behavior of Ag in Ge16Sb12Se72 glassy matrix and its impact on corresponding ionic conductivity[END_REF]. Accordingly, the [SbSI] units provided a ribbon stacking framework with chains connected by weak van der Waals forces. The chains in the same dimension were expected to intertwine into a net-like structure. Therefore, the entire ionic channel can be described A c c e p t e d m a n u s c r i p t as the stacked structure formed by the loose and porous "net" layer-by-layer, as shown in Fig. 6. The pseudo tetrahedron of [SbS x I 3-x ] was assumed to be the planer structure, because its bond angle was close to 120°. Hence, in the short-range order, the interconnection of Sb-related units caused by bond energy and van der Waals can be regarded as the monolayers, as shown in Fig. 6 (a). The infinitely extended [SbS x I 3-x ] was linked by Ga(Ge) tetrahedron in three dimensions, as shown in Fig. 6 (b). Most of the Ag + ions were trapped in the defective sites created by NBS units of Ga(Ge) tetrahedron, whereas the rest occupied the interstitial sites and were randomly distributed around the I ions. These free carriers easily passed through the ionic channels because of their low activation energy. The Coulomb force attraction of anions was weakened by the defect sites, which were sufficiently close one another. The enlarged channel volume was caused by the loose multilayered structure. With continued incorporation of AgI in the optimized component, the concentration of conductive silver ions improved, further enhanc ing the conductive property of the glass electrolytes.

Conclusion

A-series samples of 60[x(Ga 2 S 3 -3GeS 2 )-(1-4x)Sb 2 S 3 ]-40AgI and B-series samples of (100-y)(0.1Ga 2 S 3 -0.3GeS 2 -0.6Sb 2 S 3 )-yAgI were prepared by vacuum melt method, and the solubility of AgI dopant was as high as 60 mol% in the optimized (GG)Sb 0.6 sample. The ion transport behavior and channel structures of Ag + conductors were studied. Notable superionic transport behavior and good thermal stability were shown by the B-series glasses. A relatively high room temperature conductivity of 2.955 × 10 -3 S/cm was reported. The low activation energy (0.07 eV) of glassy samples confirmed the effectiveness of the migrating path in the optimized sample. Raman analysis suggested that the ion transmission channel was formed by the loose nets, which consisted of infinite connection of [SbS 3-x I x ] units, and the [Ga(Ge)S 4-x I x ] units conjoined single layers. Hence, the conductive ions of Ag + were easily activated to the concerted transport by occupying the defective and interstitial sites with a reduced migrating energy barrier. This work proposed a new quaternary structure of glassy electrolytes and provided insights into Ag +

  A c c e p t e d m a n u s c r i p t

Fig. 1 .

 1 Fig.1. XRD patterns of the as-prepared 60[x(Ga2S3-3GeS2)-(1-4x)Sb2S3]-40AgI samples in the A-series (a), and (100-y)(0.1Ga2S3-0.3GeS2-0.6Sb2S3)-yAgI samples in the B-series (b).

Fig. 1

 1 Fig. 1 shows the XRD patterns of all the samples. Three diffraction spectral lines with typical halo pattern are shown in Fig. 1 (a), thereby confirming the amorphous state of the A-series samples. In the Fig. 1 (b), an extensive crystalline peak occurred in the B-series when 65 mol% AgI was added into the matrix. Several peaks appeared at the diffraction locations following 22.5°, 23.7°, 25.2°, 39.3°, and 46.3°, which can be ascribed to the standard β/γ-AgI crystals (JCPDF card of no.1-502).

Fig. 2 .

 2 Fig. 2. The variation tendency of Tg obtained from the DSC measurement.

Fig. 3 .

 3 Fig. 3. The conductivity of A-series sample with different temperatures from 30 °C to 100 °C.

Fig. 4 .

 4 Fig. 4. Typical Nyquist diagram of the (100-y)(0.1Ga2S3-0.3GeS2-0.6Sb2S3)-yAgI samples in the B-series (y = 50, 55, 60 mol %).

A c c e p t e d m a n u s c r i p tFig. 5 .

 5 Fig. 5. Raman spectra of 60[x(Ga2S3-3GeS2)-(1-4x)Sb2S3]-40AgI (A-series, x = 0.1, 0.15, 0.2 mol) samples.

Fig. 6 .

 6 Fig. 6. Schematic diagram of the detailed ion transmission channel, top view of the "layer" structure in the ball stick model (a) and side view of the stack structure in the atomistic model (b).

A

  c c e p t e d m a n u s c r i p t ions migration in the network for further research on solid-state batteries.

Acknowledgments

This work was financially supported by National Natural Science Foundation of China (Grant no. 51972176).