initial folding RFCs

0008-kimchi-polynomial-quadricization.md

@@ -0,0 +1,103 @@
+# Kimchi polynomial quadricization
+
+## Summary
+
+This RFC proposes a protocol for converting kimchi polynomial constraints (as defined by the expression framework) to polynomials of degree at most 2.
+
+## Motivation
+
+This RFC provides a mechanism for reducing an arbitrary-degree polynomial constraint to a polynomial with degree of at most 2, by inserting additional intermediate columns. This is essential for supporting a [Nova-style](https://eprint.iacr.org/2021/370) folding scheme with reasonable efficiency, since it depends on distributing an error term across the 'cross-terms' of a multiplication.
+
+This will form part of a general scheme in kimchi to provide 'folding' as a component of proofs. In particular, this will enable arbitrarily long circuits to be run against the bn128 curve backend, where we do not currently have a scheme for using recursion.
+
+The exit condition for this work is functionality in kimchi's expression framework that 'flattens' an expression into an expression of degree 2, synthesizing auxiliary columns to facilitate this as it does so. This work will be structured such that it can be used in the zkVM proposed for the OP zk RFP.
+
+## Detailed design
+
+In Nova-style folding, multiple witnesses are combined using the observation that
+
+```math
+(a_0 + r a_1) * (b_0 + r b_1) = (a_0 * b_0) + r^2 (a_1 * b_1) + r (a_0 * b_1 + a_1 * b_0)
+```
+
+We call the final term the 'cross-term', which accounts for the 'error' in the multiplication, while the other terms correspond to the 2 multiplication results that were desired, combined with some random challenge `r`.
+
+The cross-term gets more complex as the degree of expressions increase, by fixing the degree to be at most 2 we make folding simple by having a smaller degree and also by not having to handle different degrees.
+
+Considering this example, we have 3 columns a, b and c. We also have the next expression over them:
+
+```math
+a*b*c + a*b + a 
+```
+
+we can lower the degree by introducing an additional column ab, that is constrained to be $bc = b*c$ with a degree 1 constraint,
+now the expression can be rewritten as the next expression where the degree is lowered by 1:
+
+```math
+a*bc + a*b + a 
+```
+
+Notice how we could also have chosen ab and it could have even been more efficient if also used for the second term.
+
+For more complex expressions like this one:
+
+```math
+a*b*c + a*a*b + b*b*a + a*a
+```
+
+More columns will need to be added, and the choice is no longer trivial, we could do it with 3 columns $ac$, $aa$, and $bb$.
+Or we could also use a single column $ab$ that would work for all the terms
+
+To achieve an optimal quadratic expression we would do the next changes:
+
+- Most expressions are combined at the gates level, but the gates never combine into a single expression, thus we have to flatten
+in an optimal way through several expressions. The first change would be to identify the expressions we care about and extract them from
+the prover into a location in the codebase were we can reuse them without duplication.
+- Later at some point, could be just once at constraint system creation, we will run some algorithm to decide which extra columns to create,
+or which sub expressions to extract into a column in a way that optimizes for the lowest number of extra columns, the result will be some
+struct that records which sub expressions were extracted.
+- We will create a function that takes an expression of any degree and transforms it into an equivalent quadratic expression making use of the
+optimal flattening we created previously.
+- What remains would be to apply this function in the prover and other places were we need to flatten the expressions.
+
+The next example would likely require the generalized expression framework
+
+```rust
+fn reduce(self: E<F, Column>, flattening: &OptimalFlattening) -> E<F, WithAuxiliaries<Column>> {
+}
+```
+
+## Test plan and functional requirements
+
+1. Testing goals and objectives:
+
+    - The flattened expressions should be equivalent to the original expressions.
+    - The flattening algorithm should be optimal in terms of the number of columns added.
+
+2. Testing approach:
+
+    - For equivalence we can run evaluate the same expression twice with only one being flattened and check the equality of the results.
+    - The optimal flattening is in some way impossible to check without just duplicating the problem, it should be enough to measure it
+    and just check that it looks reasonable to us.
+
+## Drawbacks
+
+The main drawback of this is that we had a reason for high degree gates, they provided improvements that will be in some way lost, but given
+that this is optional it will be a question of choosing the best option for each, folding in particular will benefit from it.
+Proving time may increase, the size of proofs will increase, pickles recursive circuit (that won't likely be used together with this) will increase,
+the folding-based IVC circuit we will have to build will grow for each row we add, but it isn't trivial to know if it will outweigh the reduction
+due to the smaller degree.
+
+## Rationale and alternatives
+
+The alternative is not doing it, with the problems mentioned at the start.
+In a more general way we could use some PCD construction instead of folding-based IVC, pickles wouldn't work with the new curve without changing KZG for a commitment like the one we currently use in kimchi but decided to change by KZG due to the EVM running costs.
+We could make pickles support KZG, but that would require to implement some complex and potentially expensive cryptography inside of pickles.
+
+## Prior art
+
+The most similar to a prior art would pickles itself, which we can not use for VM mainly due to performance issues.
+
+## Unresolved questions
+
+- The specific algorithm to find an optimal flattening, it may be a problem without an efficient solution, but given that the degrees we find in practice are relatively small we can probably run even an exponential algorithm without any issue.

0009-folding.md

@@ -0,0 +1,113 @@
+# Folding
+
+## Summary
+
+This RFC proposes the addition of folding support to kimchi, folding is a technique which basically allows
+to verify two proofs for the price of one, enabling the development of efficient IVC.
+
+## Motivation
+
+The ZkVM currently supports running a fixed number of cycles, to support an arbitrary number of cycles we will
+need some kind of recursion that allows us to combine blocks of cycles in a way that will allow constant size
+proofs.
+Pickles is able to do it, but not while fulfilling the performance requirements for the ZkVM.
+Folding is a less powerful alternative, but powerful enough while offering superior performance, especially in
+the specific scenario where the ZkVM has to operate.
+It is not a goal to replace pickles, just provide an alternative for cases like where folding can be a better
+option.
+
+## Detailed design
+
+### Overview of folding
+
+The general idea of folding is a protocol which starts with 2 instance-witness pairs, the prover has access to
+everything, while the verifier only to the instance.
+At the end of the protocol, a new instance-witness pair will be created, with the property that verifying it implies
+verifying the 2 original pairs.
+That way, the prover only has to do 1 actual proof, and the verifier only has to verify 1 proof, the new pair can
+become an input of the protocol too, thus allowing to fold an arbitrary number of instance-witness pairs into a
+single one.
+
+### Folding in kimchi
+
+For kimchi, the witness is the same witness we already have: a list of columns/polynomials. And the instance is list of the
+commitments to those polynomial, plus the public inputs.  
+Additionally, to make folding work we need to add 2 things that will absorb errors generated during the folding, one is just
+a field element $u$, the other is an extra witness column $E$ with its corresponding commitment $\overline{E}$ in the instance.  
+We will call this new kind of instance a relaxed kimchi instance ( equivalent to the committed relaxed R1CS instance in nova,
+but we already had commitments so the only change is the relaxation ).  
+A normal kimchi instance-witness pair can be trivially converted into relaxed kimchi by just setting $U=1$ and $E=[0;N]$  
+The verifier part of the protocol is relatively simple, get some commitment for the errors generated, make a challenge, send
+the challenge to the prover and take a lineal combination of the instances using the challenge.
+For the prover is doing the same with the witness after computing the error and committing to them.
+
+### Implementation
+
+The implementation will just be a few functions, working with relaxed instances and witnesses:
+
+```rust
+struct Instance;
+struct Witness;
+struct Challenge;
+struct Error(Evals);
+
+fn compute_error(a: &Instance,b: &Instance) -> Error;
+fn fold_instance(a: Instance, b: Instance, error: Error) -> (Instance, Challenge);
+fn fold_witness(a: Instance,b: Instance) -> (Instance, Challenge);
+```
+
+Additionally, it may be necessary to create some transformation that will add the errors to the kimchi equation so that the
+verification will work again.
+Given that another RFC will make the degree fixed to 2, it should be possible to make a function that will map expressions
+to the their relaxed version and apply it to each expression used.
+
+### Transformation
+
+We can think that all kimchi expressions will ultimately aggregate into a multivariate polynomial, thanks to the quadricization
+RFC we can additionally assume it to be of degree 2 or less.  
+For each term we will have to do a change to the expression and add to the error, we have 3 cases for constant, degree 1 and
+degree 2 terms that will require different changes to the expression and contribute in a different way to the error.
+
+#### Expression changes
+
+- Constant: Will be multiplied by $u^2$
+- Degree 1: Will be multiplied by $u$
+- Degree 2: Unchanged.
+
+#### Error contribution
+
+In general, when taking the linear combination of a term, you will get 3 parts, each multiplied by $1$, $r$ or $r^2$. The
+part multiplied by $r$ is the error contribution.
+Here $u_1$ and $u_2$ are the scalar from each of the original instances that become the $u = u_1 * ru_2$ of the new folded
+instance, same notation is use when needed for witness columns.
+Also, $S$ will represent a selector, which can be multiplying in the term, but does not affect the degree.
+
+- Constant: For some term $P$, the contribution will be $r2u_1u_2P$, we can likely add all terms together and multiply by
+  $r2u_1u_2$ at the end.
+- Degree 1: For some term $P$, the contribution will be $r(u_1P_2 + u_2P_1)$, similar optimization as above should be possible.
+  here $P_1$ for example just means that for computing the expression we use a column from the first instance (the one with $u_1$).
+- Degree 2: For some term $P$, that contains $ab$ from the witness, the contribution will be $rS(a_1b_2 + a_2b_1)$
+
+Given that they all contain $r$, it can be omitted and multiplied to the entire $E$ at the end.
+
+## Test plan and functional requirements
+
+1. Testing goals and objectives:
+    - The only requirement would be for it to work, it doesn't need backwards compatibility given that it will be first used 
+    in the ZkVM.  
+2. Testing approach:
+    - Given that it is new and not a replacement for pickles, we are likely limited to unit test it.
+    - When the ZkVM is ready, just running it with folding would be an useful test.
+
+## Drawbacks
+
+There isn't much not already mentioned about the comparison with pickles.
+
+## Rationale and alternatives
+
+The alternative would be pickles, which as explain at the start, wouldn't meet the performance requirement for the ZkVM.
+
+## Unresolved questions
+
+- We should probably add the equations here to some detail.
+- It is probably better to explain in detail the process to convert the kimchi expressions in their relaxed version.