Are proofs deterministic?

[matthiasgoergens]

Given the same Miden Assembly program and the same public inputs, and running the prover multiple times, will the proofs that are generated be the same bit-for-bit?

If not, what else does it depend on? Non-deterministic hints? Extra random bits we inject? Random variations we get from concurrent proving of winterfell?

I can imagine that having extra randomness is useful for zero knowledge properties? So that would suggest we want different bits in the proofs when we run the prover multiple times.

For applications where succinct verification of computation is the focus, and not hiding knowledge, determinism would be useful.

[bobbinth]

The short answer is that proofs could be deterministic but frequently are not. You've listed the sources of non-determinism correctly, but let me cover each in a bit more detail.

Winterfell

The first source of nondeterminism is concurrent proof generation in Winterfell. There, when we perform grinding, we search for the right seed in multiple threads and we don't know which thread will find the right seed first. There are a couple of ways to remove this source of nondeterminism:

• Set grinding factor to 0.
• Run proof generation in a single thread.
• Update Winterfell grinding code to somehow produce deterministic results (not sure if this is possible).

Zero knowledge

To generate truly ZK proofs, we need to mix in randomness into proof generation process. There are a few places where this needs to be done, though Winterfell doesn't support all of them yet. One such place is injecting random values at end of each trace column. In Miden, we kind of do it here - though in our case, randomness is based on program hash and thus is fully deterministic (and also not really useful for ZK properties).

If you don't care about perfect ZK, then this source of nondeterminism can be eliminated.

Program-specific

As you pointed out, we could write programs which rely on all sorts of nondeterministic inputs (e.g., we could branch on the input provided via the advice tape). There is no good way to handle this generically - but it is definitely possible to write programs which will always produce deterministic results. This is really up to the developer to decide.

[matthiasgoergens]

Thanks for the write-up! I have to look into Winterfell's grinding.