[ZK Learning Group 2] Circom workshop #1

Circom serves 2 primary purposes:

1. Lets you define a set of constraints that implicitly is equivalent to some function.

2. Define at proving-time, how you should fill in the nodes of your Arithemtic circuit - intermediate variables. (witness generation).

pragma circom 2.0.3;

template Main() {
  //private 
  signal input x; 
  signal x_squared;
  signal x_cubed;
  signal output out;
  
  // witness generation: IR gen
  x_squared <-- x * x;
  x_cubed <-- x_squared * x;
  out <-- x_cubed - x + 7;

  // constraint definition
  x_squared === x * x;
  x_cubed === x_squared * x;
  out === x_cubed - x + 7;
}

component main = Main();

On signals

• they are not bits.

• they are prime field elements. modulo p, where p is the babyjubjub prime.

On witness generation

• You know some x that results in some public out, such that f(x) = y (y = out)

• For convenience, circom allows you to generate the intermediate witnesses, as opposed to having the user to supply them.

• This is done with the <-- notation

Constraints

• constraints are done with === notation

• can only use * or + operators

• must look like either"

a * b === c;
d === f + e;

Compilation

Comilation gives up a number of files, including the .r1cs file.

R1CS

• Compiling the circuit gives us an R1CS file, that can be used with different toolstacks, that implement the Groth16 protocol.

• Think of it as a IR representation; like your compiled bytecode.

.wasm file

• a wasm exceutable program that implements the single arrow stuff - witness generation.

• witness generation program that allows derivation of the intermediate signals (x_squared, x_cubed) just from the single input, x.

vkey: verification key

• goes into your smart contract for verification.

• a .sol file is also created, whjich is a contract based on the vk that serves as the verification component.

• .sol file would expose a verifyProof function

.zkey: proving key

• goes into your client, Dapp Front-end.

• used in proof generation.

When can't you simply just <== for all constraints/intermediates?

// I know some x1,x2,x3,x4 such tt
Eq: f(x) = (x1 + x2)/ x3 - x4 

Intermediate Rep: 
y1 / x3 - x4 
y2 - x4

y1 = (x1 + x2)
y2 = y1/x3

• Input signals: x1,..x4

• Intermediates : y1, y2

pragma circom 2.0.3;

template Main() {
  signal input x1;
  signal input x2;
  signal input x3;
  signal input x4;

  signal y1;
  signal y2;

  signal output out;

//witness generation
  y1 <-- x1 + x2;
  y2 <-- y1 / x3;
  out <-- y2 - x4;

// constraints can only have quadratic expressions
// can only use + or *
  y1 === x1 + x2;
  y1 === y2 * x3;
  out === y2 - x4;
}

component main { public [ x2 ] } = Main();

Notice that in this example we cannot simply use <=== to combine out witness generation and constraint definition.

The reason we have to seperate is cos' of the y2 <-- y1 / x3;

• In witness generation you are allowed to use arbitrary operations like division.

• But in defining constraints, we can only use quadratic expressions.

• So instead of y2 <-- y1 / x3; >>> it becomes y1 === y2 * x3;

// the following would be a valid circuit:
  y1 <== x1 + x2;

  y2 <-- y1 / x3;
  y1 === y2 * x3;

  out <== y2 - x4;

You are only allowed quadratic constraints: a+b*c

• can't do x*x*x

Include

pragma circom 2.0.3;

include "../node_modules/circomlib/circuits/mimcsponge.circom";

template Main() {
  signal input x;
  // signal input hash;

  signal output out;

  component mimc = MiMCSponge(1, 220, 1);
  mimc.ins[0] <== x;
  mimc.k <== 0;

  out <== mimc.outs[0];

  // out === hash;
}

component main = Main();

// include for importing
// be it dir or direct from github
// allows re-use of circuits to build larger circuits

Paranthesis

Allows you to enter values that are params

• params are for dynamic parts of the circuit

• like counter of a for loop

• must be specified by compile time. cos the compiled circuit cannot have such dynamic parts like loops.

• At compile time, circuits must be bounded.

• n must be known at compile time.

• For loops just serve as a kind of syntatic sugar - they get unrolled into individuals lines of code.