chancehudson/circom-stark

circom-stark's Issues

Reduce constraint degree to 2

In #8 the degree of constraints was reduced to 3. The remaining constraints that are degree 3 are the mul operator, inv operator, and eq2 check (ensuring that the output register does not change during the equality check).

To reduce to degree 2 a register should be added storing the result read1 * read2 in every step of the trace. This can be used to reduce the degree of the mul constraint.

To reduce the degree of the eq2 check we need to ensure that the value in the output register does not change. This is a problem we will have with other opcodes as well, most notably abc in #6. To solve this problem we can add a special memory register that is always 0 and constrain that the output register is this special 0 register for opcodes that do not mutate memory.

New opcode tracking issue

To prove large circom circuits we'll need some special opcodes and memory structures to more efficiently do calculations. This issue is meant to track discussion of these changes.

In r1cs systems there is an array of constraints of the form a*b - c = 0. The values a, b, and c are each multivariate linear equations. E.g. dx + ey + fz where x, y, and z are independent variables and d, e, f are constants. As a result the vm needs to do lots of multiplications and additions - potentially hundreds or thousands for a single constraint.

We want to achieve a favorable tradeoff between number of registers and trace length - generally preferring fewer memory registers.

mulsum

Multiply 2 registers and add them to the value in a third register.

abc

Constrain 3 registers such that a*b - c = 0

mulconst

Multiply a register by a constant in the free input register. Add the result to another register.

This could be expanded to do multiple operations in a single step. e.g. add more free input registers and multiply/add multiple values in a single step.

Note that if free inputs are used for r1cs constants the inputs must be either revealed or checksummed and verified to ensure the prover does not modify the constants.

Add `modinv` operator

To fully prove all circom circuits we need a modular inverse operator (similar to division). The operator should work as

inv 0x2 0x0 - Calculate the modular inverse of value in register 0x0 and store the result in 0x2. It should be possible for output and input register to be the same (e.g. modinv in place).

A constraint for this should look like opcode_selector * (out * r1 - 1). out is the output register and r1 is the input register.

A free input should be used to store an intermediate value to make this constraint <= degree 3.

Remove unused operators during compilation

During compilation of an assembly file we should look at what opcodes are being used. If we find that a certain opcode is not used at all (e.g. the neg opcode) we can avoid adding the selector column for this operator and avoid adding the constraint for this opcode.

This should be a good optimization once we have more opcodes that are more complex/specific.

Revealing what circuit is being proven

The current vm treats all memory as private. This means there is no way to effectively tell what program was executed to create a proof. In order for a user to make a proof for a third party then need to reveal what they are proving. e.g. which circuit.

To reveal this information the proof must reveal the following:

• opcode selectors
• memory selectors
• constraint constants

Only the witness signal values and intermediate values should be private.

Note that the data doesn't have to be revealed, but can instead be checksummed, to ensure the prover did not manipulate the parameters of the circuit.

Reduce the `mul` operator transition constraint degree

The transition constraint degree of the vm is currently 5. e.g. there constraint polynomial has a term of degree 5; this is caused by the multiplication operator.

To build this system we use selector columns that are either 0 or 1 to enable/disable constraints and select register variables. So for a given step we select registers by doing

let value
for (x < state.length)
  value += state[x] * selector[x]

So we end up with state[0]*selector[0] + state[1]*selector[1] + .... Each opcode uses two registers, r1 and r2, both are computed using the above equation.

To constraint multiplication we do r1 * r2 - out. Then we only enable this operator when the opcode is the multiplication opcode so opcode * (r1 * r2 - out). The multiplication opcode has it's own column (same as all others) that is either 0 or 1 indicating whether the current step of the trace is multiplication. So the multiplication constraint becomes

// degree 5, e.g. opcode * state * state * selector * selector
opcode * ((state[0]*selector[0] + state[1]*selector[1] + ...) * (state[0]*selector[0] + state[1]*selector[1] + ...) - out)

To reduce this we can use two free input registers to store the state values (r1 and r2). Note that we only have 1 free input register right now so a second one needs to be added to the trace generation logic.

// free input constraints
// store the selected register values in free in 0 and 1
(state[0]*selector[0] + state[1]*selector[1] + ...) - free_in

// constrain the values
opcode * (free_in0 * free_in1 - output)

This results in 3 constraints with a maximum degree of 3 (matching all other opcode constraints).

Witness solver does not handle unconstrained assignments correctly

The witness solver does not solve signal assignments that are not directly constrained, like in Num2Bits.

In this template the values of the array out are assigned without constraint (using -->). The values are then constrained individually and as a sum. The current witness solver calculates incorrect values for the entries of out.

To fix this we need to define a range of possible solutions for each variable (when possible). These solutions should be evaluated in other constraints that rely on them to determine correctness.