Intro to Gnark
Gnark is a zkSNARK library developed by ConsenSys that allows developers to design and implement zero-knowledge circuits in Go. Unlike other circuit libraries that use domain-specific languages, Gnark lets you write circuits directly in Go, making it more accessible to developers already familiar with the language.
At its core, a zero-knowledge circuit defines a computational relationship between public inputs and private witness values. When we generate a proof, we're essentially proving that we know witness values that satisfy this relationship, without revealing those values.
When using Gnark, we define a struct that describes our computation, and as member fields, the inputs of our computation. Below we have a circuit which proves knowledge of Sudoku solutions. The two inputs are Challenge, which is the puzzle, and Solution, which is the completely filled in puzzle.
// SudokuCircuit represents a Sudoku circuit. It contains two grids: the
// challenge and solution grids (named Challenge and Solution respectively). The
// challenge grid is public, while the solution grid is private.
type SudokuCircuit struct {
Challenge SudokuGrid `gnark:"Challenge,public"`
Solution SudokuGrid `gnark:"Solution,secret"`
}
Our Sudokugrid type is just a simple 9x9 matrix:
// SudokuGrid represents a 9x9 Sudoku grid in-circuit.
type SudokuGrid [9][9]frontend.Variable
Next is where we define the actual circuit. In this book, we will not go into concepts such as arithmetization or rc1s, although we will see some of that in the actual code. For now it suffices to know, that we define rules that our inputs have to abide by. We refer to these rules as constraints.
For a sudoku solution to be checked, we have to verify the following:
- Each cell may only have a value from 1 to 9.
- Each row may only contain unique values.
- Each column may only contain unique values.
- Each 3x3 sub grid may only contain unique values.
- The solution is for the given puzzle.
Especially rule 5 is easy to forget. If we would not implement that, our checker would allow any valid solved sudoku to solve our puzzle.
We define the constraints inside the Define function, which accepts an api frontend.API, which is the object we use to actually define our circuit.
// Define defines the constraints of the Sudoku circuit.
func (circuit *SudokuCircuit) Define(api frontend.API) error {
For each rule, we call various assertions on the api. These assertions are not run immediately. Instead we are building a program under the hood, to be run later against actual variables. The actual for loop is not part of our circuit either, instead it is just execution each instruction one-by-one, effectively unrolling the loop.
// Constraint 1: Each cell value in the CompleteGrid must be between 1 and 9
for i := 0; i < 9; i++ {
for j := 0; j < 9; j++ {
api.AssertIsLessOrEqual(circuit.Solution[i][j], 9)
api.AssertIsLessOrEqual(1, circuit.Solution[i][j])
}
}
For rules 2, 3, and 4, the implementation is similar
// Constraint 2: Each row in the CompleteGrid must contain unique values
for i := 0; i < 9; i++ {
for j := 0; j < 9; j++ {
for k := j + 1; k < 9; k++ {
api.AssertIsDifferent(circuit.Solution[i][j], circuit.Solution[i][k])
}
}
}
// Constraint 3: Each column in the CompleteGrid must contain unique values
for j := 0; j < 9; j++ {
for i := 0; i < 9; i++ {
for k := i + 1; k < 9; k++ {
api.AssertIsDifferent(circuit.Solution[i][j], circuit.Solution[k][j])
}
}
}
// Constraint 4: Each 3x3 sub-grid in the CompleteGrid must contain unique values
for boxRow := 0; boxRow < 3; boxRow++ {
for boxCol := 0; boxCol < 3; boxCol++ {
for i := 0; i < 9; i++ {
for j := i + 1; j < 9; j++ {
row1 := boxRow*3 + i/3
col1 := boxCol*3 + i%3
row2 := boxRow*3 + j/3
col2 := boxCol*3 + j%3
api.AssertIsDifferent(circuit.Solution[row1][col1], circuit.Solution[row2][col2])
}
}
}
}
Rule 5 uses the Select method, which is how we can implement if statements in the circuit.
// Constraint 5: The values in the IncompleteGrid must match the CompleteGrid where provided
for i := 0; i < 9; i++ {
for j := 0; j < 9; j++ {
isCellGiven := api.IsZero(circuit.Challenge[i][j])
api.AssertIsEqual(api.Select(isCellGiven, circuit.Solution[i][j], circuit.Challenge[i][j]), circuit.Solution[i][j])
}
}
Actually generating a proof requires compiling and setting up the circuit.
// perform the setup. NB! In practice use MPC. This is currently UNSAFE
// approach.
pk, vk, err := groth16.Setup(ccs)
if err != nil {
return fmt.Errorf("failed to setup circuit: %v", err)
}
// compile the circuit
ccs, err := frontend.Compile(ecc.BN254.ScalarField(), r1cs.NewBuilder, &SudokuCircuit{})
if err != nil {
return fmt.Errorf("failed to compile circuit: %v", err)
}
In this code example, we are doing an unsafe setup, which makes the circuit unsafe for actual usage. Union ran a setup ceremony, where multiparty computation is used to make the setup safe and production ready. The circuit, vk and pk can be written to disk for later usage; we should only compile and setup once.
With these values, and some sample inputs, we can start generating proofs.
// create the circuit assignments
assignment := &SudokuCircuit{
Challenge: NewSudokuGrid(nativeChallenge),
Solution: NewSudokuGrid(nativeSolution),
}
// create the witness
witness, err := frontend.NewWitness(assignment, ecc.BN254.ScalarField())
if err != nil {
return fmt.Errorf("failed to create witness: %v", err)
}
// generate the proof
proof, err := groth16.Prove(&ccs, &pk, witness)
if err != nil {
return fmt.Errorf("failed to generate proof: %v", err)
}
We could now serialize the proof, and send it to a verifier (someone on a different machine).
// create the circuit assignments
assignment := &SudokuCircuit{
Challenge: NewSudokuGrid(nativeChallenge),
Solution: NewSudokuGrid(nativeSolution),
}
// create the witness
witness, err := frontend.NewWitness(assignment, ecc.BN254.ScalarField())
if err != nil {
return fmt.Errorf("failed to create witness: %v", err)
}
// generate the proof
proof, err := groth16.Prove(&ccs, &pk, witness)
if err != nil {
return fmt.Errorf("failed to generate proof: %v", err)
}
As you can see, they have only access to the challenge, not the solution. The proof will verify that the prover has a valid solution, without leaking information on that solution.
Now that we know the basics of Gnark, let's analyze the light client circuit. We will see that the applied techniques are very similar to the Sudoku grid. Effectively we are re-implmenenting cryptographic primitives using the frontend.API.