Sudoku might seem like a simple puzzle, but it offers a great example to grasp the fundamental concepts behind Zero Knowledge Proofs (ZKPs). In this blog post, we’ll explore how to prove that a Sudoku solution is correct without revealing the solution itself, and we'll use Noir to implement this idea.

Let’s start by stating the problem: imagine someone (the prover) has a solution to a Sudoku puzzle and wants to prove to someone else (the verifier) that the solution is correct, but without revealing the actual solution.

I recently read an article that explains this problem using a card analogy. Here’s the full article link, but I’ll summarize it below.

The prover places 3 cards with values from 1 to 9 into each cell of the Sudoku board. Then, the prover creates one stack of cards for each row, column, and 3x3 square, shuffles the stacks, and gives all 27 stacks (9 rows, 9 columns, 9 squares) to the verifier. The verifier checks that each stack contains all numbers from 1 to 9, verifying that the solution is correct. Because the stacks were shuffled, the verifier doesn't know the exact positions of the numbers, thus keeping the solution hidden, but can be sure that the solution is correct.

This trick mirrors the core principle of Zero Knowledge Proofs: proving you know something (in this case, the Sudoku solution) without revealing the actual information.

There’s a full implementation of a Sudoku validator using the Circom language (Circom is another language used to build zk-SNARK circuits, similar to Noir), with a blog explaining everything behind it here.

But today, we’re going to use Noir to implement a similar solution.

Noir is a Rust-like language designed to simplify writing zk-SNARK circuits. When using Noir, you write high-level logic, and it compiles your code into efficient circuits behind the scenes. This abstraction allows developers to focus on solving problems without worrying about low-level circuit design. Its Rust-inspired syntax makes it accessible to a big audience, enabling developers familiar with Rust to quickly adapt to Noir language.

By using Noir, you’re writing circuits without realizing it, the code feels like you’re solving the problem in a normal programming language, but behind the scenes you’re generating zero knowledge circuits. It also provides a syntax similar to Rust, making it accessible to more developers.

Let’s dive into the logic of building the Sudoku validator in Noir. Our goal is to validate a Sudoku solution by proving:

1. The solution corresponds to the given puzzle

2. Every row, column and 3x3 square contains the numbers from 1 to 9 without duplicates

3. Every number in the solution is in the valid range (from 1 to 9)

To start, we’ll define a main function with two parameters: a public one corresponding to the puzzle with the empty places, and a private one corresponding to the solution. Both are arrays of 81 elements.

fn main(puzzle: pub [Field; 81], solution: [Field; 81]) {...}

Let’s start by checking that the solution corresponds to the given puzzle:

for i in 0..81 {
    if puzzle[i] != 0 {
        assert (puzzle[i] == solution[i]);
    }
}

This ensures that any pre-filled values in the puzzle are enforced in the solution.

Next, let’s check in the same loop that all the numbers are valid, this means from 1 to 9. We do this by adding these two lines:

    assert(solution[i] as u8 >= 1);
    assert(solution[i] as u8 <= 9);

Now let’s start checking the rows, columns and 3x3 squares. This helper function ensures that each group of nine values (whether a row, column, or subgrid) contains unique values from 1 to 9.

fn check_all_unique(numbers: [Field; 9]) -> bool {
    let mut all_unique: bool = true;
    for i in 0..9 {
        for j in (i + 1)..9 {
            if numbers[i] == numbers[j] {
                all_unique = false;
            }
        }
    }
    all_unique
}

Let’s construct the arrays corresponding to each row, column and square, and assert that all the values are unique:

    // rows:
    let mut row_values: [Field; 9] = [0; 9];
    for row in 0..9 {
        row_values = [0; 9];
        for col in 0..9 {
            row_values[col] = solution[row * 9 + col];
        }
        assert(check_all_unique(row_values));
    }

    // columns:
    let mut col_values: [Field; 9] = [0; 9];
    for col in 0..9 {
        col_values = [0; 9];
        for row in 0..9 {
            col_values[row] = solution[row * 9 + col];
        }
        assert(check_all_unique(col_values));
    }

    // 3x3 subgrids
    let mut box_values: [Field; 9] = [0; 9];
    for box_row in [0, 3, 6] {
        for box_col in [0, 3, 6] {
            box_values = [0; 9];
            let mut index = 0;
            for i in 0..3 {
                for j in 0..3 {
                    box_values[index] = solution[(box_row + i) * 9 + (box_col + j)];
                    index += 1;
                }
            }
            assert(check_all_unique(box_values));
        }
    }

And that’s it! We’ve just written a Noir program that can be compiled to circuits and checks a solution for a Sudoku puzzle, without having to implement anything related to circuits. It seems as if we’re just writing a normal program.

Let’s add some test cases to ensure our function behaves as expected:

#[test]
fn test_valid_solution() {
    let (puzzle, solution) = valid_puzzle();
    main(puzzle, solution);
}

#[test(should_fail)]
fn test_invalid_solution() {
    // The same number twice in a row
    let (puzzle, invalid_solution) = invalid_solution();
    main(puzzle, invalid_solution);
}

#[test(should_fail)]
fn test_out_of_range_solution() {
    // Solution with invalid number 10
    let (puzzle, invalid_solution) = out_of_range_solution();
    main(puzzle, invalid_solution);
}

For the proof and verification we’ll use Aztec’s Barrentberg, which is an optimized elliptic curve library for the bn128 curve, and a PLONK SNARK prover. You can read more about it here. This is just one option, more proving backends can be used.

For installing Noir, check this. For installing bb, check this.

You can check the compatibility of Noir and Barrentberg versions here I’m using Noir version 0.33.0 and bb version 0.47.1.

First, we need to compile the circuit

nargo compile

After running this command, a Prover.toml file will be generated along with a target folder containing a noir_sudoku.json file.

In the Prover.toml, we need to fill in the puzzle and solution variables with an example. Here’s an example you can use so that you don’t have to solve a puzzle yourself:

puzzle = [
  5, 3, 0, 0, 7, 0, 0, 0, 0,
  6, 0, 0, 1, 9, 5, 0, 0, 0,
  0, 9, 8, 0, 0, 0, 0, 6, 0,
  8, 0, 0, 0, 6, 0, 0, 0, 3,
  4, 0, 0, 8, 0, 3, 0, 0, 1,
  7, 0, 0, 0, 2, 0, 0, 0, 6,
  0, 6, 0, 0, 0, 0, 2, 8, 0,
  0, 0, 0, 4, 1, 9, 0, 0, 5,
  0, 0, 0, 0, 8, 0, 0, 7, 9
]

solution = [
  5, 3, 4, 6, 7, 8, 9, 1, 2,
  6, 7, 2, 1, 9, 5, 3, 4, 8,
  1, 9, 8, 3, 4, 2, 5, 6, 7,
  8, 5, 9, 7, 6, 1, 4, 2, 3,
  4, 2, 6, 8, 5, 3, 7, 9, 1,
  7, 1, 3, 9, 2, 4, 8, 5, 6,
  9, 6, 1, 5, 3, 7, 2, 8, 4,
  2, 8, 7, 4, 1, 9, 6, 3, 5,
  3, 4, 5, 2, 8, 6, 1, 7, 9
]

After filling it, we create the witness file:

nargo execute witness

Instead of witness, you can name it whatever you want. I just want to keep it simple. After this step, a witness.gz file will be created in the target folder.

The witness in a zk-SNARK proof is the set of secret values that the prover uses to satisfy the circuit. In our case, the solution to the Sudoku puzzle is the witness because it is used to prove that the conditions of the puzzle are met, without revealing the exact values to the verifier.

The witness must be generated before creating the proof because the proof process uses the witness as input to demonstrate that all the constraints of the circuit are satisfied. Without the witness, the prover would have no secret values to use, making it impossible to proceed to proof generation.

Now it’s time to create the proof using both files that were created in the target folder, and we’ll write the proof to a proof file.

bb prove -b ./target/noir_sudoku.json -w ./target/witness.gz -o ./target/proof

The verification key (vk) is an essential part of a zk-SNARK system. It is used by the verifier to check the validity of the proof. The vk contains necessary information derived from the circuit to determine if the proof generated by the prover is valid without revealing the witness.

We generate the verification key with the following command:

bb write_vk -b ./target/noir_sudoku.json -o ./target/vk

A vk file will be created. Now we can verify the proof with:

bb verify -k ./target/vk -p ./target/proof

If verification succeeds, there will be no output message, indicating success.

If we modify something in the Prover.toml file to make the Sudoku solution invalid, the process will fail when trying to create the witness:

Failed to solve program: 'Cannot satisfy constraint'

This error indicates that the solution no longer satisfies the Sudoku rules, confirming the ZKP system’s reliability.

We successfully created a program that checks a Sudoku solution’s validity without revealing the solution, by writing high-level logic in Noir and compiling it to zk-SNARK circuits.

Let’s reflect on the fact that we created a ZKP without thinking in circuits, just using a higher-level language, but in the backend circuits were used.

As Zero Knowledge technology continues to grow, tools like Noir make it possible for developers to build privacy-preserving applications with ease, whether in games, identity verification, or financial transactions.

Noir’s ease of use and powerful abstraction make it an amazing tool for building zk-SNARK applications. Whether you’re building a simple puzzle validator or complex privacy-preserving systems, Noir opens up possibilities without requiring you to dive deep into the underlying cryptographic math.

Next step: turning these circuits into a Solidity smart contract, bringing zero-knowledge Sudoku to the blockchain! Stay tuned 👀 🔜