noname meets Ethereum: Integration with SnarkJS

We are thrilled to announce that noname, zkSecurity's programming language to write ZK circuits, now supports R1CS! This update allows developers to write ZK circuits in a rust-and-golang-inspired language and deploy them to Ethereum using SnarkJS. This offers an alternative to the widely-used Circom language for zk-SNARK proofs on Ethereum. In this post, you'll see the first noname circuit deployed on Ethereum, and we'll show you how to deploy one yourself.

The zero-knowledge field is evolving rapidly, with new proof systems and frameworks frequently emerging. Developers face a major challenge: fragmentation. Each proof system has its own language and quirks, often targeting specific projects and unavailable on other platforms. For example, Noir is for Aztec Network, Leo is for Aleo, Cairo is for Starknet, and O1js is for Mina.

What if there was a way to bridge this gap? A language that could unify the zk ecosystem, allowing developers to write circuits that work across different backends.

This is what we're doing! while noname was first created to compile programs to work with Mina's kimchi proof system, we are now updating it to work with Ethereum's SnarkJS.

The integration of noname with R1CS and SnarkJS is a pivotal step in the language's journey, and it's been made possible thanks to a grant from the Ethereum Foundation's Privacy & Scaling Explorations team.

A Sudoku as a noname program

Using Sudoku as an example demonstrates two benefits of zero-knowledge proofs:

1. Proving correctness of a Sudoku solution without revealing the solution itself.

2. Reducing on-chain computation costs. The verification cost on-chain is constant, regardless of the complexity of the off-chain computation.

The full code for the sudoku circuit is available here. Let's look at our main function:

fn main(pub grid: Sudoku, solution: Sudoku) {
    solution.matches(grid);
    solution.verify();
}

It receives two arguments: the Sudoku problem as a public input, and the solution as a secret.

At a high level, this sudoku circuit checks:

1. the solution grid matches with the sudoku problem (encoded in the public inputs)

2. verify the solution indeed follows the sudoku rules

In Noname, grid: Sudoku automatically interprets inputs as the Sudoku type:

struct Sudoku {
    inner: [Field; 81],
}

Here is how it checks if the solution matches with the grid of a solution problem.

// return the value in a given cell
fn Sudoku.cell(self, const row: Field, const col: Field) -> Field {
    return self.inner[(row * 9) + col];
}

// verifies that self matches the grid in places where the grid has numbers
fn Sudoku.matches(self, grid: Sudoku) {
    // for each cell
    for row in 0..9 {
        for col in 0..9 {
            // either the solution matches the grid
            // or the grid is zero
            let matches = self.cell(row, col) == grid.cell(row, col);
            let is_empty = grid.cell(row, col) == empty;
            assert(matches || is_empty);
        }
    }
}

Next, the program verifies the solution according to sudoku roles:

fn Sudoku.verify(self) {
    self.verify_rows();
    self.verify_cols();
    self.verify_diagonals();
}

fn Sudoku.verify_rows(self) {
    for row in 0..9 {
        for num in 1..10 {
            let mut found = false;
            for col in 0..9 {
                let found_one = self.cell(row, col) == num;
                found = found || found_one;
            }
            assert(found);
        }
    }
}

fn Sudoku.verify_cols(self) {
    for col in 0..9 {
        for num in 1..10 {
            let mut found = false;
            for row in 0..9 {
                let found_one = self.cell(row, col) == num;
                found = found || found_one;
            }
            assert(found);
        }
    }
}

fn Sudoku.verify_diagonals(self) {
    for num in 1..10 {

        // first diagonal
        let mut found1 = false;
        for row1 in 0..9 {
            let temp1 = self.cell(row1, row1) == num;
            found1 = found1 || temp1;
        }
        assert(found1);

        // second diagonal
        let mut found2 = false;
        for row2 in 0..9 {
            let temp2 = self.cell(8 - row2, row2) == num;
            found2 = found2 || temp2;
        }
        assert(found2);
    }
}

As it is shown above, the typing support behind the language makes circuit code straightforward, akin to writing in conventional languages.

Plugging into Snarkjs

Now that we have the sudoku code, we can use the noname CLI to generate and run circuits that are compatible with Snarkjs.

1. Install noname

   cargo install --git https://www.github.com/zksecurity/noname
   

2. The command guideline

3. Generate r1cs circuit and witness files compatible with snarkjs

noname run --backend r1cs-bn254 --path ../test/noname-sudoku \
--private-inputs '{"solution": { "inner": ["9", "5", "3", "6", "2", "1", "7", "8", "4", "1", "4", "8", "7", "5", "9", "2", "6", "3", "2", "7", "6", "8", "3", "4", "9", "5", "1", "3", "6", "9", "2", "7", "5", "4", "1", "8", "4", "8", "5", "9", "1", "6", "3", "7", "2", "7", "1", "2", "3", "4", "8", "6", "9", "5", "6", "3", "7", "1", "8", "2", "5", "4", "9", "5", "2", "1", "4", "9", "7", "8", "3", "6", "8", "9", "4", "5", "6", "3", "1", "2", "7"] }}' \
--public-inputs '{"grid": { "inner": ["0", "5", "3", "6", "2", "1", "7", "8", "4", "0", "4", "8", "7", "5", "9", "2", "6", "3", "2", "7", "6", "8", "3", "4", "9", "5", "1", "3", "6", "9", "2", "7", "0", "4", "1", "8", "4", "8", "5", "9", "1", "6", "3", "7", "2", "0", "1", "2", "3", "4", "8", "6", "9", "5", "6", "3", "0", "1", "8", "2", "5", "4", "9", "5", "2", "1", "4", "9", "0", "8", "3", "6", "8", "9", "4", "5", "6", "3", "1", "2", "7"] }}'

Then it should generate the .r1cs and .wtns files and tell you where the files are located.

R1CS file generated at: ../test/noname-sudoku/output.r1cs
Witness file generated at: ../test/noname-sudoku/output.wtns

4. Test the generated r1cs circuit and witness files

There is a script to quickly test the compatibility of these outputs with the SnarkJS. The script automatically generates the proof and verifies it off-chain via SnarkJS.

Verify the proof on Ethereum

The snarkjs provides a command to export a solidity verifier. We have a deployed instance on Ethereum at 0x7c686a33ac3f2c911b03b9aa80e5175d3ab4152a.

To test a solution on-chain, you can use this SnarkJS command to generate the calldata.

Intuitively, the calldata contains the contract call arguments to represent a sudoku problem (the public inputs in the circuit) and a proof for the corresponding solution (without revealing it).

As the screenshot shown (from remix), if the proof(_pA, _pB, _pC) and the sudoku problem matches (_pubSignals), then the contract call to verifyProof should return true.

What's next?

noname is a work-in-progress language, and many features are missing! We're looking for help and contributions. If you're interested, check the issues.

To learn more about Noname, please check out the repo, or the following blog posts and videos:

• the noname language, a toy DSL for zkapps
• update #1: learning about zero-knowledge apps and circuits using the noname educational DSL
• update #2: structs are working!
• update #3: user-defined functions