Proving things about functions using a PRNG.

Stream: general

[Alex Zani]

I am trying to implement a differentially private algorithm and prove something about the statistical properties of its output. Long story short, it takes a pseudo-random number generator, some other inputs and returns an output based on these two.

If I was trying to prove something about this on paper, I would call the pseudorandom number generator a random variable and it would "infect" everything it touches with randomness, ultimately giving me my output as a random variable about which I could prove things. But from the point of view of lean, my PRNG is just another function that deterministically spits out bits based upon the updated state I feed to it when it advances. There's nothing random about it.

Intuitively, I want to define a PDF as the limit behavior of a function which accepts a PRNG and then prove something about the PDF of my output.

I'm wondering if others have experience dealing with this and how they approached the problem.

[Aaron Liu]

You could use a monad.

[Alex Zani]

Aaron Liu said:

You could use a monad.

I do plan to wrap my generator in a monad in my implementation, but I don't think that really solves my problem. The monad will still be wrapping a generator and some values, so I still can't treat it as a random variable.

[Aaron Liu]

Don't wrap a concrete generator, wrap an abstract generator.

[Alex Zani]

Aaron Liu said:

Don't wrap a concrete generator, wrap an abstract generator.

Like a Generator class?

[Julian Berman]

(It doesn't relate directly to your question, but just on the off chance you haven't already seen it, there's https://github.com/leanprover/SampCert/ for some differential privacy primitives I think)

[Alex Zani]

Julian Berman said:

(It doesn't relate directly to your question, but just on the off chance you haven't already seen it, there's https://github.com/leanprover/SampCert/ for some differential privacy primitives I think)

Oh thanks, that should be very helpful.