stdlib.hasRandom in tutorials about reach-lang HOT 4 CLOSED

Reach computations are deterministic, and thus Reach does not support a native random function. However, Reach can interact with participants to, for example, "provide a number". The frontend is then responsible for how exactly to get this number. The Reach program cannot rely on the number being generated in an particular way.

This is a really common occurrence, so we want to make it is easy for people to specify that the frontend can provide a random number and we want to make it easy for the frontend to actually do so, although we don't want to mandate our particular implementation, because random number generation is a sensitive security topic.

So, your "If I am correct" is correct and this is as-intended and it can't really be another way. However, I think we can motivate this a bit more in the hasRandom documentation and xref it with the stdlib.hasRandom helper --- https://docs.reach.sh/ref-programs-compute.html#%28part._has.Random%29 --- What do you think?

from reach-lang.

Okay, I think this is the premise: Reach, by design, does not natively provide a way to generate random numbers, but at least one Reach function (i.e. makeCommitment) (1) requires this capability and (2) relies on the frontend participant to supply a random() method which, I assume, can be the default stdlib method or a custom method.

Here, then, I think, is what the developer needs to self-talk: "I need to include a random() method in my frontend participant object not because I need to access it in my backend code explicitly, but because at least one Reach function needs it."

If so, do we want to avoid the necessity of developers needing to make this leap? For example, I think makeCommitment has access to the default stdlib.hasRandom.random() method without the frontend supplying it, just as the backend, in general, has access to stdlib methods. Then, only developers who want to supply custom random methods would need to supply them. Am I seeing this right?

from reach-lang.

Just like Reach wants to force people to declassify, require, and consider invariants, it is part of its security consciousness to have them in charge of their own randomness. Many many applications have been attacked through their random generators, so we don't want to make it so that Reach will only do randomness one way.

from reach-lang.

I've updated the documentation regarding hasRandom

from reach-lang.