Hi everybody, my name is Charlie and I'm here to tell you a little bit about some work we did with Gilles and Steve about probabilistic programs of our finite fields and some of their relational properties.

So let's get right on to it. What kind of programs are we looking at? So we see basic programs, inputs, random samplings, some operations, conditional branchings, multiplication and addition and at the end you return some values. We don't support loops because in fact if you add them, our problems become indecidable, so that's that.

But for this kind of programs, there are some classical verification questions for such programs and the most classical one being equivalence between programs. As we are probabilistic, it means equality of the distributions produced by the program and in fact we come from the context of security, computer security

and we want to look at other properties that can be of interest for us. Independence, because often we want to prove that a program, the distribution of a program is independent from the distribution of some secret value, else it is not secret. And also we want to be able to bound the probability of some event inside a program

notably when some event is bad for the security, we like the probability of this event to be low. So first question, are those problems decidable? When in fact we have our finite fields, they are finite, you can simply compute the distribution and that's it.

Everything is decidable. But an open question was the exact complexity and still coming from the world of security we actually introduced a variation of those questions which we dubbed universal because in fact when you have a boolean program, when you have a program that operates over booleans

you can actually see it as a program that operates over bit strings and you can choose to use any length of bit strings for your program you still have xor and and over those bit strings and given such programs, you can actually ask if two programs are equivalent for all possible length of bit strings

and that's a new question that we call universal equivalence and it's not so clear if it's decidable because now we have an infinite number of cases to check so that's one of our big questions also and this in our paper we start by showing some first predictions between the problems

so actually independence, equivalence, and equivalence 3-th order inputs are all three integrable decibels in polynomial time so they are the same essentially and then we look at the complexity in the finite case of those three problems so for finite field Fq, we have exact complexity for each of the problems that we want to look at

but secondly, and probably more importantly our second contribution is that in the universal case, equivalence is decidable so that's it, let's look at the formal definitions before seeing a little bit the complexity

and how we prove the decidability of universal equivalence I won't delve into details about finite fields essentially you just need to know that you have usually a Bayes finite field which is a set of integers of size p for some prime p

and then you can consider extensions of this finite field for each p to the power of some k that's all you need to know based on this we look at programs and in fact we can see the Bayes expressions of a program first as polynomials

where we distinguish the set of variables of the polynomial into two sets i is for the inputs and r for the random samplings then we add conditionals over such polynomials and in the end the program is essentially a tuple returning n expressions depending on the conditional branches

so let's take a look at two very simple programs this one is simply returning three values taking as input two possible values x and y and sampling uniformly some u this one sample uniformly three values

and return a single one by completing this big operation that's it so to give the semantics of our programs we need to define the probability distribution that they follow in fact so for our program p and some sequence of input inside f q to the power of k

we can define the distribution of the program such that for each possible value c that the program may take as output we associate to it the probability that p evaluated given i

the value given as input to the distribution and some value r for the random variables the probability that p is equal to c when we sample uniformly r inside f q to the power of k and that's it so using those distributions we can start to reason about our problems

over f q, so that's why we have this q here r, the small program that returns r will simply be equal to zero with probability one half and to one with probability one half i times r

when i is equal to one it's simply equal to r so we have the same distribution probability but when i is equal to zero i times r is in fact always equal to zero

so the probability that the distribution is such that the probability that it is equal to zero is equal to one and the probability that it is equal to one is equal to zero so equivalence for some q to the power of k simply acts that for all possible inputs of the program the two programs produces the same distribution exactly

and universal equivalence we ask that for all possible k for all possible program k p is equivalent to q when we are looking at f q to the power of k so now that we have those definitions we can look at the complexity of equivalence

and i'm going to give a brief reminder because as you may have noticed when i gave you the contributions we are going inside non-classical complexity classes so let's start with basics SAT, you gave me a boolean formula

and i should tell you if phi can become true for some valuation does there exist a valuation such that phi is true and this is the classical problem used to define NP problems you consider a non-deterministic Turing machine and a problem is inside this class

is there exist a Turing machine that recognizes exactly all the elements of the language and for each element of the language the Turing machine will have at least one accepting path and for SAT the idea is that you have at least one valuation

that satisfies the formula you can see it in terms of probabilities the Turing machine accepts with none the probability when you give it the formula as input we can then consider from SAT multiple variations of this problem and obtain new complexity classes

that such that half SAT is complete for this complexity classes for instance, half SAT is well named because we just expect that phi should be true for exactly half of its valuations this is called the exact counting complexity class

c equal p half of the paces of the Turing machine should be accepting ones so you can compare with NP where we asked that at least one path was accepting and in terms of probabilities the Turing machine should accept with probability one path

and essentially you can start to see the links with our problems because if you see phi as a Boolean formula if you consider that you sample at random the values of the variables inside phi then it turns out that the formula will be true with probability one half

if and only if it is in half SAT so you start to see the link between probabilities equivalence between programs and this kind of class of complexity classes the thing is that we need to go higher inside the complexity classes

we need to consider formulas depending on two sets of variables and for any possible valuation of one of the set of variables phi should be true for exactly half of the valuation of the other set of variables this is the problem which is complete for coin p

with an oracle that solves problems inside c equal p and this is essentially the definition what we want to be able to do for this complexity class is show that our problem equivalence is complete

and first question the hardness can we solve our half SAT using equivalence actually I already told you that we can because as I said the formula phi is going to be equivalent to r recall that r is simply the program that is equal to 0 with probability one half

and phi should be equivalent to this if and only if it is in half SAT the idea is that we see x as random variables y as input variables and then you see the half SAT appearing because for all possible values of the input variables

there exist exactly half of the valuations of x so that phi is equivalent to r basic Equivalence in the case of fq is coin p with oracle c equal p hard for the membership it's not overly complicated

we start, we can describe a Turing machine parameterized by p and q programs c some possible output value of the two programs and i a sequence of inputs for the two programs then what we do is that we sample some x in 0 and 1

and then what we do is that with probability one half we accept if p is equal to c and with probability one half we accept if q is equal to c why is this Turing machine interesting? essentially it accepts

with this probability which is with probability one half x equals 0 we accept with the probability that p is equal to c and with one half of the probability we accept if q is equal to c that's not exactly what we want but what we want is that we can easily obtain it by replacing

just this q equals c by q distinct from c because then this small part of the equation it changes it becomes 1 minus q 1 minus the previous probability and now the probability that p that the Turing machine accept

is exactly one half plus probability that p equals c minus probability that q equals c so in fact our Turing machine accepts with probability one half if and only if the probability that p is equal to c is equal to the probability that q is equal to c

and that's the basic building block if we can do it for all possible c for all possible output value we can check if the two programs are equivalent and this is typically what we can do using co-NP complexity

by simply going over all possible inputs and all possible output values and checking the c equals p problem so that's it for the completeness and let's go to the more interesting equation universal equivalence

so we're going to look at the base case we only have programs without conditionals and in fact those programs are essentially tuples of polynomials we also consider that we don't have inputs because recall that I said previously that equivalence is equivalent

is interreducible to equivalence for programs without inputs so I won't show the reduction but we don't have to consider inputs so the mathematical formulation of the problem for this kind of polynomials

can be written in this way we simply ask that for all possible output values and for all k the number of random valuations the number of valuations of the random variables inside f q to the power of k so that's the link between the k and the k, it's here

so the number of random valuations such that p equals c is equal to the number of valuations such that q equals c we simply went from probabilities to counting the number of points which is exactly the same thing so why is this nice? because mathematicians are quite good at what they do

and notably they defined this mathematical object the local zeta function so given a polynomial p we can express some quantity over it which is the exponential of the sum of something quite interesting this small nk of p

and you're quickly going to understand why nk of p is defined as the number of r such that pr equals 0 so we can see the link with the previous writing of equivalence and in fact this sum

because it goes over all possible k's exactly captures this nkp for all possible k it contains all the information about all those nkp so the main idea is simply this big observation

q polynomials have the same local zeta function if and only if the number of r such that pr equals 0 is equal to the number of r such that q of r equals 0 and actually thanks to the mathematicians we can compute z of p and z of q

and this we can check this what does it mean to check this? it means that we can decide given two programs if they are equal to zero with the same probability over all extensions of a finite field and from this

we do a bit of encoding I won't describe it here but by computing three well-chosen local zeta functions we can actually check the equality not just on zero of the distributions but we can check the equality of the distributions over all possible values

and thus we can decide universal equivalence so one of the questions is how to handle conditionals because what we can classically do in finite fields

is encode conditional branchings because for a fixed finite field q to the power of k we can write these kind of things we can say that if b is not equal to zero then p is q it's actually completely equivalent to this arithmetic expression why is that?

because b to the power of q power k minus one it's simply an expression thanks to the rules of the finite fields which is equal to zero if b equals zero and one if b is not equal to zero and this when b equals zero you simply get q when b is equal to one you get q plus q minus q

you get p so the thing is it depends on k so we cannot use this to remove the conditionals inside our problem for universal equivalence so I'm thinking use this reaction because I find it quite funny

there is actually a nice solution to this problem which is that b has an inverse if and only if b is not equal to zero and then we can play a bit around and introduce a fresh variable

that will be meant to represent the inverse of b and we can in fact encode the fact that the fresh variable t is equal to this quantity over b if and only if those two equations are satisfied

and we can count recall that this is what the local zeta function is doing it's counting the number of points so that something is equal to zero in fact and this something can be a tuple of polynomials so from q plus t b, p minus q

which is meant to represent the if b not equal to zero then p else q from this expression we add two equations and those equations ensure that all the valuations that we consider here are such that t is equal to b to the power of q power k minus q

and then t times b is equal to what we wanted on the previous slide b to the power of q power k minus one and thus this indeed does follow the distribution of if b not equal to zero then p else q

so we did remove the dependencies the dependency on the k and we can use this inside nk and inside the local zeta function so to conclude universal equivalence is decidable

and because it's equivalent to independence both of those problems are decidable independence and equivalence are quen p with oracle c equal p complete which is considered to be non-tractable sadly and I don't talk about it at all but for the majority problem

it's quen p to the power of p p where p p is equivalent of c equal p where we ask that the probability of the Turing machine to accept is greater than one than half rather than exactly half and we are able to obtain a reduction to a registry problem notably atlix

which is the positivity problem it asks given a linear recurrence sequence so that's essentially a sequence of integers defined by recurrence relation it asks if all the terms of the sequence of the linear sequence are positive

if positivity is decidable then majority will be decidable well universal majority will be decidable

actually I have given you a small subset of what we do because our probabilistic program inside the paper actually supports the observe primitive which is one of the classical constructs of probabilistic programs and you can also sample variables inside not just the whole field

but any set which is defined by a condition of a polynomial not that you can only perform uniform samplings over such sets so if you want more complex distributions you need to build them by combining multiple variables and of course conditionals

as I said if you add loops to a program universal equivalence becomes decidable so we don't really know how to extend the polynomial one of the big open questions for our work

it's a bit frustrating we were not able to prove that the universal question is strictly harder than the non-universal one we don't have a better lower complexity bound for the universal equivalence than just the lower complexity bound of equivalence

so it's a bit frustrating because intuitively we want to believe that universal equivalence is really harder but for the moment we haven't been able to prove it so open question and of course is positivity decidable? then we will get the decidability of our moderate question

and finally it might be interesting to look at other probabilistic properties some of them are linked to security for instance similatability questions thank you for your attention and bye