hint function design

Goals

Optimize constraints via non-deterministic functions
Flexible to experiment with ideas that are not possible with existing builtins

How hint works in circom

Its compiler folds arithmetic expressions into one expression until it encounter the non-deterministic operations. The process also involve constant folding. There are some more details about this process in how circom works.

Take the following circuit for example:

template Example () {
	signal input a;
	signal output b;
	b <== a >> 2 & 1;
}

The arithmetic expression folding detects that a >> 2 is not a deterministic operation, while the result of the expression is being constrained to equal to output b. In order to make the user aware of what they are doing with the non-deterministic assignment, it throws error:

error[T3001]: Non quadratic constraints are not allowed! 
┌─ "main.circom":10:5 
│ 10 │ b <== a >> 2 & 1; 
│      ^^^^^^^^^^^^^^^^ found here

This is actually an warning instead of an error in my opinion. This warning is to tell there is likely a soundness issue in this statement.

The programmer has to use <-- in the place of <== to acknowledge they know it is an non-deterministic calculation.

By default, circom compiler adds constraints for a number of operations that are too implicit to understand the pattern.

For example, this code with a input var as divisor is non-deterministic operation

template Example () {
	signal input a;
	signal input b;
	signal output c;
	c <== a / b;
}

On the other hand, replacing the input var b with a constant value makes it a deterministic expression. This implicit way to automate constraints without clear rule is hard for the programmers to get a grid of what it means by non-deterministic.

Thus it is hard to plan and design a circuit without running into a number of warning forcing them to use <-- in practice, which can contribute to a lot of soundness issue especially they are running out of time in dev to reflect what they are doing.

How zkVM works?

I guess they compile the codes to opcodes, then adds constrains for each of the opcodes in general.

srli t0, val, nth # t0 = val >> nth 
and b, t0, 1 # b = t0 & 1

In contrast to circom, the zkVM takes care of all the non-deterministic calculations by constraining them automatically in a builtin way.

This is nice, because the programmers don't need to take care of these non-deterministic "problem" anymore. But the price is the performance, due to the number of constraints can be significantly higher.

How unconstrained fn works in noir

nargo execute cmd

It has a nice command nargo info, which print out the how many opcodes are generated for a code. This is helpful to peek how it generates the opcodes for unconstrained functions by observing the differences among the these opcodes.

opcode category

It has two categories of opcodes:

ACIR for defining arithmetic circuits.
Brillig opcodes Brillig is the ACIR uses for non-determinism, aka for general calculations.

default mode

The default mode is constrained mode. For example:

fn main(x: Field, y: Field) {
    div(x, y);
}

fn div(x: Field, y: Field) -> Field {
    x / y
}

It yields 2 ACIR Opcodes in the main function. I guess one of the these ACIR opcode introduces a call to directive_invert brillig_inverse to invert the value of the variable before applying constraints to it. This looks similar to creating a inverse symbolic value and apply constraints to this symbolic value in noname.

Package	Function	Expression Width	ACIR Opcodes	Brillig Opcodes
func	main	Bounded	2	9
func	directive_invert	N/A	N/A	9

uses of unsafe and unconstrained

Let's see what happens when marking the function as unconstrained

fn main(x: Field, y: Field) {
    div(x, y);
}

unconstrained fn div(x: Field, y: Field) -> Field {
    x / y
}

It throws a warning:

warning: Call to unconstrained function is unsafe and must be in an unconstrained function or unsafe block
  ┌─ src/main.nr:3:5
  │
3 │     div(x, y);
  │     ---------
  │

This makes senses as it requires the programmers to acknowledge that part is unconstrained. Similar to how circom ask the programmers to acknowledge that by <--, here it can use an unsafe block to silent the warning.

fn main(x: Field, y: Field) {
    unsafe {
        div(x, y);
    }
}

unconstrained fn div(x: Field, y: Field) -> Field {
    x / y
}

It yields the same set of opcodes, no matter if the unsafe block is used.

Package	Function	Expression Width	ACIR Opcodes	Brillig Opcodes
func	main	Bounded	1	13
func	div	N/A	N/A	13

Compared with the default mode, the number of ACIR opcodes is decreased to 1, while the number brillig opcodes is increased to 13.

The 1 removed ACIR opcode is probably for constraining the div function. The remaining 1 ACIR opcode is probably for constraining the input arguments in the main function.

Note that the number brillig opcodes is increased. Not sure why it is increased when it is unconstrained though. Maybe it is due to less precompiles used compared with constrained mode, thus need more brillig opcodes.

detect potential soundness bug via graph

Furthermore, it throws bug warning when the hint output is not constrained with the other parts of circuit, trying to constrain the hint output using assert function.

bug: Input to brillig function is in a separate subgraph to output
  ┌─ src/main.nr:4:21
  │
4 │         assert(1 == div(x, y));
  │                     --------- There is no path from the output of this brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability

Interestingly, it kind of having a graph to detect if a variable or expression is part of a graph. This graph seems to represent the circuit.

How might noname hint function work

I think it makes sense to have the similar modes like noir has in noname. In the default mode, noname can use builtins to constrain the non-deterministic calculations, such as /, %, <<, >>, & etc in addition to the * currently supported.

Similarly, noname may allow unconstrained functions for optimization or experimenting with ideas that are not yet possible via builtin.

example

unconstrained fn nth_bit(val: Field, const nth: Field) -> Field {
	// if val is a constant, then
	// - it can proceed as the this function defined,
	// - it is deterministic and return a constant.
	// otherwise, it will be a cell var, and the following code will be marked as
	// - non-deterministic,
	// - thus unsafe.
	// non-deterministic also means 
	// - it can't determine its constant value at compiler time
	// - or it can't be directly translated to a constraint
	// 
	return (val >> nth) & 1;
}

fn main(pub xx: Field) {
   let unsafe bit = nth_bit(xx, 9);
}

To compose the symbolic values for the unconstrained function in a way that can generate witness values while being compatible with the current arrange in the compiler. We may need to refactor the symbolic Value enum and the ConstOrVar. They are responsible for generating witnesses and propagating the variables respectively.

how does the current vars (ConstOrVar) are pass around and wire up with Value?

Initially the main function inputs create cell vars to store in witness vector, and then pass down the stream as ConstOrCell.

ConstOrCell is a wrapper to represent either a constant or a cell var. It is seen as a front end var.

It can be passed into builtin functions, which may return newly constructed ConstOrCell.

The relationship between two ConstOrCell can be represented by a symbolic Value, which can be stored as a cell var in the witness vector and point to another cell var.

enum Value<B>
{
	ConstantField,
	LinearCombinationField, B::Var)>, B::Field /* cst */,
	MulVar, B::Var,
...

When generating the witnesses, it recursively computes the Value by loading the chained cell vars.

For the case of running a hint function, it would need to recursively compute the Value without having to store the intermediate values as cell vars in the witness vector.

Take x >> 2 & 1 for example, assume it has the new variant Value:right_shift(B:Var, B:Field), the current enum Value requires it to store an intermediate cell var for x << 2 before being passed to calculate with & 1.

The another problem is the Value variants can become too verbose for certain combinations of its arguments. For example, it requires the following variants for division:

CstDivVarField, B::Var,
VarDivCstVar, B::Field,
VarDivVarVar, B::Var,
CstDivCstField, B::Field,

new symbolic value enum

To resolve these issues, we may just make the Value enum being recursive by itself.

enum Value {
  Cellvar, 
  ConstField, 
  LinearCombination([(Value, factor)]),
  Mul(lhs: Value, rhs: Value),
  Divide(lhs: Value, rhs: Value),
  ...
}

So that:

doesn't have to create cell var for chaining the calculations.
it can represent either const or a cell var, so won't need to create all the different variants for the different combinations of arguments for an operation.

unconstrained mode

In noir, excluding the inputs and outputs type constraints, it only generate brillig opcodes for the unconstrained functions.

Similarly, noname can only generate a Value that chain up the calculations and represent a function's return value, without triggering the builtin function calls.

It is also important to have unsafe attribute, which can either be applied to a block or a statement, to prompt the programmers to acknowledge potential risks.

default mode

When there is no unconstrained attribute to a function, it is always in default mode, which is to trigger builtin functions for all the non-deterministic calculations.

comparison in execution trace

default mode (via builtin)

builtin to constrain `val >> cst`

calculate the result of >>
create s1 Value:right_shift(val, cst), where val is Value:cell()
add the s1 to backend, which returns v1 Value:cell(rsv), where the v1 points to the index of s1 in witness vector
range check to_bits(bit_len, res), where bit_len = bit_len(val) - cst
return res Value:cell(rsv)

builtin to constrain `res & 1`

constraints needed:

$b * (b - 1) = 0$
$r e s - 2 q - b = 0$

workflow:

create s2 Value::div(res, 2) for $r e s / 2 = q$
store s2 as witness var v2
create s3 Value:LinearCombination([(res, 1),(v2, -2)]) for b
store s3 as witness var v3
constrain v3 * (v3 - 1)
constrain $v 1 - 2 * v 2 - v 3 = 0$

hint mode

create rsv Value::right_shift(val, cst)
create and return Value::and(rsv, Value:const(1))

This returned symbolic value can be passed around, and it may be added to witness vector at certain point if it got constrained.

should hint function be evaluated at mast phase?

it should, so as to propagate generic values.
this also also applies to the builtin functions, so they can propagated computed constant values.

Goals

How hint works in circom

How zkVM works?

How unconstrained fn works in noir

nargo execute cmd

opcode category

default mode

uses of unsafe and unconstrained

detect potential soundness bug via graph

How might noname hint function work

example

how does the current vars (ConstOrVar) are pass around and wire up with Value?

new symbolic value enum

unconstrained mode

default mode

comparison in execution trace

default mode (via builtin)

builtin to constrain val >> cst

builtin to constrain res & 1

hint mode

should hint function be evaluated at mast phase?

builtin to constrain `val >> cst`

builtin to constrain `res & 1`