Hammer home that you can't pull out the JS values of variables in a circuit

[mitschabaude]

I'm increasingly of the opinion that this is the number 1 rule about how (not) to write circuits, that we have to make extremely obvious to developers:
Don't ever read out the JavaScript value of a Field (Bool, CircuitValue, ...) inside a circuit
It subsumes all the other gotchas like if-statements, branching using errors, etc but in a more precise way. An example for reading out the JS value is doing field.toString(). It's a frequent gotcha that people try to use the value of a Field / Bool to determine what constraints to add to the circuit. Example: an if-statement that depends on the value of a Bool --

if (bool.toBoolean()) {
  ...
}

It might be good to know that reading the value of variables like this will throw an error if you're compiling the smart contract. That's because they're variables - they don't have a value attached to them at compile time. .toBoolean() is supposed to be used on constants / outside the circuit. Because usage on variables would throw during compile, there isn't currently the risk that these contracts get deployed. However, since compiling of smart contracts is relatively new and takes long, many developers write large amounts of code before actually trying to compile. So in this case we should take measures to provide this feedback earlier, and also make it clearer what causes the error.

See this discord thread for more context:
From here https://discord.com/channels/484437221055922177/915745847692636181/981662842161877052
until here https://discord.com/channels/484437221055922177/915745847692636181/981822004346904606

I see two immediate action items which could become their own issues:

• Rewrite all the different error messages when you're trying to do things like field.toString(), bool.toBoolean(), field.toBigInt(), field.toConstant() during compile. These error messages should all be very clear, and refer to the common theme that reading values of variables can't be possible
• Add linter rules for all of these methods, that tell you they can't be done inside a circuit. IMO, these rules should replace the existing rules about if statements and errors, because those are not very precise (we actually use lots of if-statements and errors in our code base, which is confusing people).

Other items TBD:

• It would be very nice to have a version of Circuit.runAndCheck() which also quickly runs the circuit, but in an environment that behaves like compile. The current runAndCheck behaves like prove, where values of variables are available, and thus doesn't help preventing this gotcha. If we had this, we could use it in more places, e.g. as a sanity check when running a method in a transaction block, to catch errors early.
• Should we separate the classes of variables and constants? E.g. Field.Variable vs Field? Or Field vs Field.Constant? This would make the distinction so much clearer. Then we could establish this rule simply by, say, not having a .toString() method on Field.Variable. This would be a big project that has implications across the code base.
• There is currently the Circuit.asProver(() => {...}) feature, which lets you read values from variables without error because the asProver callback is not run during compile. However, when we mentioned this during our first workshop, people got confused and started to write their circuit completely inside asProver blocks! Maybe we should just rename it to runOutsideCircuit(() => {...}). If we move to separate types for variables, they could have a method like fieldVariable.toStringOutsideCircuit(s => {...}) which gives you the string in a callback which isn't run during compile.

[bkase]

It would be very nice to have a version of Circuit.runAndCheck() which also quickly runs the circuit, but in an environment that behaves like compile. The current runAndCheck behaves like prove, where values of variables are available, and thus doesn't help preventing this gotcha. If we had this, we could use it in more places, e.g. as a sanity check when running a method in a transaction block, to catch errors early.

There is a way to do this via OCaml (at least there was with a past version of the underlying proof-system). I don't think it would be too much effort to expose this to SnarkyJS, and this is a really good idea.

Should we separate the classes of variables and constants? E.g. Field.Variable vs Field? Or Field vs Field.Constant? This would make the distinction so much clearer. Then we could establish this rule simply by, say, not having a .toString() method on Field.Variable. This would be a big project that has implications across the code base.

I think it's certain that the current design of the API isn't working and we should explore more drastic changes like this. Now is the time to do it. Before there are too many zkApps in the wild. This is one potential approach; I think the design space is big and we should brainstorm a bit before implementing this.

[MartinMinkov]

Rewrite all the different error messages when you're trying to do things like field.toString(), bool.toBoolean(), field.toBigInt(), field.toConstant() during compile. These error messages should all be very clear, and refer to the common theme that reading values of variables can't be possible

To me, this sounds like the right approach, I really like it! I don't think it's good enough to rely on developer experience to catch these themselves, there should be a safeguard in place that SnarkyJS can catch and warn. Totally agree about changing the linter to accomplish this as well.

Should we separate the classes of variables and constants? E.g. Field.Variable vs Field? Or Field vs Field.Constant? This would make the distinction so much clearer. Then we could establish this rule simply by, say, not having a .toString() method on Field.Variable. This would be a big project that has implications across the code base.

I'm not sure what the implications are across the code base but I really like this idea! I'm really in favour of having a more verbose API given the complexity of zk programming.

It would be very nice to have a version of Circuit.runAndCheck() which also quickly runs the circuit, but in an environment that behaves like compile. The current runAndCheck behaves like prove, where values of variables are available, and thus doesn't help preventing this gotcha. If we had this, we could use it in more places, e.g. as a sanity check when running a method in a transaction block, to catch errors early.

This is great too! If this was available, could we build tooling inside the zkapp-cli to make debugging circuits as easy as running a command?

[mitschabaude]

This is great too! If this was available, could we build tooling inside the zkapp-cli to make debugging circuits as easy as running a command?

Yeah that's a neat idea! I imagine we could capture most errors that would occur during compiling and proving in a quick-to-run command. zk check maybe?

[mitschabaude]

partially addressed by #998