ZK app developers should be able to see down to the constraints
written by David Wong on

noname

As we’ve explained before, zero-knowledge apps (or ZK apps) will come in two different shapes: VM instructions and arithmetic circuits.

VM instructions should sound familiar. Reading them is like reading assembly, and they’re a level of abstraction higher than arithmetic circuits (as pointed out by this post).

Whatever they’re writing, real programmers need to see what their programs compile down to (according to John Carmack). That’s how you find unoptimized bits as a low-level code monkey, but it’s also how you find some security issues and bugs. It’s not just that compilers have bugs, it’s also that ZK developers are facing a new kind of programming. That is, when they’ll be writing circuits (the VM-side of the ZK coin is not so new after all).

When writing zkApps, or ZK programs, that compile down to circuits, developers will be faced with a restricted and unsafe environment. Restricted because they will have to optimize their code to fit into the circuit size limits, and unsafe because they will need to ensure that what needs to be constrained is correctly constrained (we’ll be writing more on that!).

Low-level developers know exactly what this means: they need access to the machine-generated code, the “assembly”, the lowest possible layer. They need the source of truth.

For zkApps in proof systems like PlonK, that source of truth is the list of gates, and the wires, that describe the circuit. This list of gates and the wiring is often obtained by compiling a program written in a higher-level language or framework.

SnarkyJS is one example of a framework that helps developers write circuits in typescript without having to think about or understand circuits, or having to learn a new language.

snarkyjs

As you can see, it mostly looks like typescript decorators and library function calls. On the other hand, Leo is one example of a made-up programming language that offers the same thing.

leo

Both of these approaches offer different benefits and downsides. The framework approach can rely on the preexisting tooling of the language the framework is written in. On the other hand the DSL approach prevents developers from making some types of mistakes by mixing in logic that does not get constrained (but that’s not always true depending on the DSL, as Circom has shown us).

What the children of both approaches all seem to be lacking though, is a way to see the “assembly” a program compiles down to.

Better toolings need to become available.

At zksecurity.xyz, we’ve experimented with a new programming language called noname (initially meant as a placeholder name). noname allows developers to write zkApps in a high-level language that looks like a mix of Golang and Rust:

use std::crypto;

fn main(pub public_input: Field, private_input: [Field; 2]) {
    // checks that they add up to 2
    let res = private_input[0] + private_input[1];
    assert_eq(res, 2);
    
    // checks that one is the hash of the other
    let digest = crypto::poseidon(private_input);
    assert_eq(digest[0], public_input);
}

The particularity of noname is that you get extensive debug information on how such programs compile down to gates. For example, passing the --debug argument to noname gets you an output describing the “assembly”. A list of gates, where each gate is accompanied with an explanation as to why it exists and what line of code it comes from.

In addition, the wiring is also displayed at the end with similar information about the source of their existence:

noname, at the moment, is more of a toy language that we’ve used to understand other compilers, and the type of compiler bugs that can occur. We’ve also used it to teach how to read ZK circuits!

While the project is still experimental, we’re excited to see if this will inspire more people to build better debugging tools, as well as lead to students (in school or at heart) using noname to learn about how arithmetic circuits are constructed.

Head over to our repo to try it out!