How Circ generates witnesses

Circ 's IR is based on SMT-LIB. The IR is inspired from LLVM for CPU, but is for EQC(Existential Quantified Circuit), which is in the similar domain of SMT. The framework provides the facilities to translate frontend language to the IR, from IR to different arithmetic backends, and can be used to prove and verify zk program written in its supported frontend languages.

This note is to explore how it compiles an IR to a circuit and generate witnesses in its proving process, so as to evaluate the feasibility of Circ integration in noname for certain purposes, such as hint calculation.

Zokrate example

Let's use this zokrate example to see how Circ eventually generate circuit and witness for it.

def main(private field x, private field y) -> field:
	return if x == 10 then x + y else x * y fi

Generated IR:

(computation
  (metadata
    (parties prover verifier)
    (inputs
      (return (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
      (x (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513) (party 0))
      (y (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513) (party 0))
    )
    (commitments)
  )

  (precompute
    (
    )
    (
      (return (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
    )

    (set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
      (declare
        (
          (y (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
          (x (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
        )
        (tuple
          (ite
            (= x #f10)
            (+ x y)
            (* x y)
          )
        )
      )
    )
  )

  (set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
    (declare
      (
        (return (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
        (y (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
        (x (mod 52435875175126190479447740508185965837690552500527637822603658699938581184513))
      )
      (=
        (ite
          (= x #f10)
          (+ x y)
          (* x y)
        )
        return
      )
    )
  )
)

There are 3 sections in this generate IR: metadata, pre-computions, and assertions sections.

• Assertions will be used to generate constraints.
• Pre-computations are for witness generations.
• Metadata seems to be related to proof systems.

Generate constraints

In circ, the assertion is expressed in IR, explicitly in the code, or implicitly for return value.

These assertions are a list of IR terms that can be pipelined in order, and bubble up to the final value to equal to return for example.

Assertions are then pushed to the Computation cs.outputs.

When compiling the circuits, it creates witness variables (called fresh var) when necessary and use them in the subsequent constraints.

for example:

(=
  (ite
	(= x #f10)
	(+ x y)
	(* x y)
  )
  return
)

It generates the constraints like the following order:

1. var1 = x == 10
2. var2 = x + y
3. var3 = x * y
4. var4 = ite(var1, var2, var3)
5. var4 == return, where return is an public instance

Generate witnesses

Note that the IR also has a precompute term, corresponding to the constraints listed above. It is used to evaluate witnesses in a proving process.

Pre-compute IR:

(
	precompute
	...
		(tuple
		  (ite
			(= x #f10)
			(+ x y)
			(* x y)
		  )
		)
	...
)

Opcode view:
this could be helpful to understand how precompute IR plays the similar role as a virtual machine.
note that precompute serve as a witness generator, so it would execute every branches.

In the same order as the constraint generation, it generate evaluations for the expressions. These evaluations correspond to the witness variables above.

Because Circ supports RAM checking or I-R1CS (Interactive R1CS), the constraint/witness generation processes need to take care of multiple rounds / stages.

#[derive(Debug)]
/// A variable type
pub enum VarType {
	/// x
	Inst,
	/// cw_i
	CWit,
	/// w_i
	RoundWit,
	/// r_i
	Chall,
	/// w
	FinalWit,
}

Without using the RAM checking feature in a frontend language, the process only needs to handle the two var types (witness variable type): VarType:Inst and VarType:FinalWit.

In the example at the beginning, the return is a public instance (VarType:Inst), while the private variables x, y and all the intermediate variables will be the type of VarType:FinalWit.

Before witness generation, it categorize the variables into different stages:

/// Returns a list of (signal list, challenge list) pairs.
/// The prove computes the values of signals.
/// The proof system computes the values of challenges.
/// All signals are computed from (a) prover inputs and (b) challenge values.
fn stage_vars(&self) -> Vec<(Vec<Var>, Vec<Var>)> {
	let mut out = Vec::new();
	out.push((
		self.insts_iter().chain(self.cwits_iter()).collect(),
		Vec::new(),
	));
	
	for round_idx in 0..self.round_chall_ends.len() {
		out.push((
			self.round_wits_iter(round_idx).collect(),
			self.challs_iter(round_idx).collect(),
		));
	}
	out.push((self.final_wits_iter().collect(), Vec::new()));
	out
}

The instance variables are arranged at first, the private or intermediate at the end, while the ones used for RAM checking at the middle.
These are the details of how it maps the variables to the witness evaluations. I think in practice, the witness generation API can be treated as a black box, as it encapsulates these stages.

To generate witnesses, it evaluates the variables in stages in order.

noname hint function

From the above observation, it seems feasible to integrate the Circ lib for hint calculation. The workflow would be like:

1. Translate noname AST to Circ pre-computation IR for a hint function
2. Store the pre-computation IR as a witness variable in noname
3. Evaluate the pre-computation IR using the circ API (we only care about the final value) for witness generation

The outcomes of this potential integration would be:

• Pave the way to integrate with Circ for other features, such as R1CS optimization, SMT, and potential ecosystem etc.
• Potentially plug into its language features, such as breakable branches.
• Potentially plug into its proving facility, such as RAM checking.

IR term store

The IR does constant folding even before the actual optimization process.
For example:

// add
def add(field x, field y) -> field:
	return x + y

// mul
def mul(field x, field y) -> field:
	return x * y

def cond(field x, field y) -> field:
	return if x == 10 then add(x, y) else mul(x, y) fi

def main(private field x, private field y)-> field:
	field res = 0
	for field i in 1..10 do
		res = cond(x, y) + i
	endfor
return res

Instead of naively unrolling the forloop, it does constant folding for the IR terms and provide the precompute:

(tuple (+ (ite (= x #f10) (+ x y) (* x y)) #f9)))

This is achieved via its hash table for IR terms. (pending to understand how it works)

Embeddable interface

The Circ embeddable trait provides interfaces for frontend languages to map their data types to variable terms in circ IR.

Take z# for example, the major mappings needed are for the z# types.

While it would be convenient to use the same interface as circ framework recommended, it is possible to create the IR terms without the embeddable interfaces.

At the low level, the declare_input embeddable interface does the following to create a new variable IR term for an input:

1. Determine the data type
2. Visibility. This seems to be related to indicate whether it is public or private inputs. Also it could be related to MPC.
3. Precompute. Assigning a propagated IR term to this newly created variable. This precompute term is similar to symbolic value in noname (a mini VM to calculate a witness)
4. Create Var term. Calling the Computation::new_var(..) will generate a Var term.

Each var IR term keep track of the variable name and the recomputation.

Generate circ IR in noname

The z# frontend implemented in circ repo keeps track of the variables in different scopes, and propagate the corresponding IR terms.
noname already has its own way to store these variables and do the expression(corresponding to IR term) propagation.
So the minimal changes needed to generate circ IR from noname code would be:

1. Create a new compile_native_function_call called compile_hint_function_call to translate a function mast to IR
2. Create a mapping between the IR var terms and function argument variables passed from noname, stored as HintIR
3. Add a new symbolic value Value::IR(HintIR)
4. When the HintIR is returned from compile_hint_function_call, store it as a symbolic value via backend.new_internal_var
5. In compute_val, it loads all values for the argument variables via noname backend, and use these values to evaluate the HintIR

Simple noname example to make for a POC:

hint fn add(lhs: Field, rhs: Field) -> Field {
	return lhs + rhs;
}

hint fn mul(lhs: Field, rhs: Field) -> Field {
	return lhs * rhs;
}

fn main(pub public_input: Field, private_input: Field) {
	let xx = add(public_input, private_input); 
	let yy = mul(public_input, private_input);
	assert_eq(xx, yy); // builtin call
}