Witgen annotations in PIL

[georgwiese]

Motivation

For the most part, automatic witgen is a fairly generic solver for a given set of constraints. But there are some "ugly" machine detection parts: For example, the Double-sorted witness machine (aka read-write memory) relies on specific column names.

This appears to get worse when we implement permutation and lookup arguments in PIL. For example, what used to be:

lhs_selector { a1, a2 } is rhs_selector { b1, b2 };

then compiles to:

col witness stage(1) z;
(is_first * (main.z - 1)) = 0;
((beta1 - (rhs_selector * ((alpha1 * b1) + b2))) * z') = ((beta1 - (lhs_selector * ((alpha1 * a1) + a2))) * z);

(and that's in the simple case, where we're not working over extension fields (#1306))

It is not obvious how to robustly extract the information explicit in the native permutation constraint from the new constraints.

Another example is LogUp (#1374): Here, witgen actually has to do extra work (keep track of the multiplicities, which a generic solver would not know how to do). This is kind of similar to the double-sorted witness machine mentioned above.

PIL annotations

We could allow the user to pass information like this explicitly to witgen in PIL and ASM. I'm not sure what the exact syntax should be, but it could be some struct with the following fields:

• lhs_selector, lhs, rhs_selector, rhs: Just like the native permutation / lookup constraints today
• connection_type: permutation or lookup, just like the native constraints. For example, for permutations, witgen would set the RHS selector to 0 in the default block.
• custom_machine (optional): For example double_sorted_witness_machine; basically any string that witgen can recognize / parse. In the future, we could allow the user to define its own custom machines that need custom witness generation.
• custom_machine_args (optional): For example (addr, step, change, value, is_write), so that the custom machine implementation can find the witness columns it should know about.
• custom_connection (optional): For example logup; this indicates that witgen needs to do extra work (in this case keep track of multiplicities) when processing this connection. In the future, we could allow the user to define its own custom connections that need custom witness generation.
• custom_connection_args (optional): For example (multiplicities), so that the custom connection implementation can find the witness columns it should know about.

With this approach, users would be able to mix and match custom machines with custom connection arguments.

It should be possible to return these annotation from PIL functions, just like it's possible to return constraints!

Assembly annotations

We should also be able to specify this in assembly already. Again, I'm not sure about the exact syntax, but it would makes sense that a machine's operations can have a custom_machine and custom_machine_args annotation.

[chriseth]

About the custom machine annotation: I think there should be some special statement inside the namespace that does this, like

prover {
  std::prover::suggest_machine("memory");
  // and now potentially some hints
}

For the lookups and multiplicities: The lookup information itself could be kept by just storing the original lookup struct somewhere. How to handle the multiplicities i don't know yet.