We can do sumcheck of the form .
Formally, is defined as , where are coordinate polynomials of . and can be expressed through Frobenius twists of and , but it is only needed for verifier on the last stage, so prover does not keep twists of and ever.
2.1. Prover does it in phases. In 1st phase, taking rounds, it works roughly normally, but operates over the quadratic polynomial , computed on the subset .
On i-th round, it keeps the restriction .
When it needs to answer the query - i.e. send univariate polynomial it exploits the fact that is split as
This allows us to not manipulate with polynomials of degree directly until the last stage - terms do not depend on , and so can be evicted from the sum. I.e. we compute the sum
and then adjust it as . This last stage is done in coefficient form, and the summation itself is done in evaluation form - i.e. it is just 3 sums
for - which we can compute because we have the evaluations of for .
2.2 After phases, prover no longer has required data (as we have computed extension only on subset), and can not proceed further. This is when we change strategy, and compute and (using RESTRICT functionality).
2.3 Optimality considerations. First phase requires work roughly proportional to . Second phase requires work roughly proportional to . By trial and error, I have found that the optimal inflection point is , however, are somewhat close.
Normal sumcheck would end with prover's claims about values of . We employ an additional argument to convince verifier in this values. Namely, for any number a, its i-th coordinate satisfies where , and is a dual basis to our standard basis w.r.t. to the bilinear form
Therefore, our prover actually communicates values of , and verifier locally recovers intended -s.
Moreover, as we assume that actually verifier only has access to , we recall that and thus it is equivalent to querying polynomial in an inverse Frobenius orbit of .
In order for our system to be useful, we need to provide an additional argument, which will, for a polynomial , reduce the statements to a single opening in some different point . There is a very classic, standard multiopening argument, working as follows:
Crucially, for arbitrary set of opening points , this argument requires from the prover in order to compute . In our case, however, this is unacceptable, as we have opening points. But they are not random, and is actually (Frobenius is a homomorphism, and coefficients of eq are just some algebraic expressions of ). Therefore, we can write
This means, that we can just compute , and then apply to its values a single boolean matrix . This is definitely cheaper than computing separately! However, matrix application is still a heavy operation (much heavier than multiplication).
There is an alternative path, which suggests to instead operate with polynomials
The main feature here is that because has values in , and hence is invariant under Frobenius mapping.
Now, for the reason which will be clear very soon, we will run the sumcheck in a reverse order of variables.
Claim. On -th round of sumcheck, with previous challenges denoted as it is enough to compute sums
The sum over -s can then be compressed into
This is very efficient, because we already know polynomials from the second phase of our previous algorithm (we currently do not save them, but we can). This allows us to skip first few rounds almost completely - the remaining sum is proportional in size to . Which is exactly the reason why we want to run this sumcheck in reverse order of variables!
After skipping first few rounds (and not later than when reaches ) we can just compute by replacing , and computing
Optimization from Improvement 1 can be used here, though it is not strictly necessary, as this is already very efficient.
The system described above is enough to build ANDplonk - a version of PlonK, which supports, together with normal additions and multiplications, a bitwise AND operation. This, however, is not efficient for hashes, the main reason being that additions (XOR operations) will not be free in such arithmetization.
Sumchecks, however, do allow us to do very efficient linear operations.
Assume we are given some linear matrix (with some efficiency assumptions, stated later). Then, application of this matrix to the vector of values is, by definition, a following sum:
This allows us to reduce claims about to claims about , using the sumcheck:
Efficiency requirements:
In particular, let us assume that our linear transforms are slightly vectorized, i.e. matrix actually works on chunks of size and not whole . Then, we can even compute the following reduced sumcheck:
which reduces the claim about evaluation of to the evaluation of .
This is somewhat better for verifier (less rounds), and much better for the prover if it knows in advance - which, funnily enough, exactly what happens in our scenario, due to
We construct a succinct proof system with efficient vectorized boolean operations.
While it can, potentially, be used for a lot of different application, the most obvious one is an efficient non-arithmetic hashes. Considering that the resulting proofs are still quite large, we believe that in many cases it will be embedded into some sort of external SNARK.
This motivates our name choice - we call our system Hashcaster, for its ability to turn non-arithmetic hashes into arithmetic ones (required for its verification in the embedding SNARK).
Recently, starting from Binius, there was a lot of attention related to extension fields of . Creating proof systems over such fields is challenging, however, they do, by default, provide us at least with a very efficient vectorized XOR operator (linear addition over ).
Our main insight is the idea that we can also express AND operator (coordinate-wise multiplication) in appropriate basis through algebraic operations: additions, multiplications and, crucially, Frobenius morphism.
We adapt the sumcheck protocol for Frobenius twists of polynomials.
In what follows, we will mainly consider the field . This is done mainly for simplicity, and we believe that our result extends to other extensions. This can be done if the need arises.
Let's consider a quadratic extension, .
Definition. Artin-Schreier mapping is defined by formula .
Lemma.
Proof. Clearly, for every it holds that (by generalized Fermat little theorem). Conversely, it no other element satisfies such property, because equation can not have more than roots. This proves that the kernel of is indeed .
Now, the image of the mapping has dimension , so to prove that it coincides with it is enough to see that every element has a preimage: . But this is a quadratic polynomial, so it has a root in a quadratic extension of , and there is a single quadratic extension for each finite field - in this case, .
Definition. Now, we compose -s through the tower of extensions:
Lemma.
Proof obvious (applying facts that we already know about ).
We will frequently abuse the notation and treat as -valued linear function on space .
Now, pick any -basis in . We define linear functions .
Note that these are also linearly independent.
Definition. Chosen basis is a dual basis to -s, i.e. satisfying .
Lemma. Actually, any basis can be chosen for appropriate choices of -s, because the mapping is an isomorphism with dual space.
Proof. Assume converse. Then, there is such that linear function is . However, we know that is nonzero, and substituting we recover original . Therefore, it is an isomorphism, and so for any basis the corresponding collection can be found.
We will normally choose basis to correspond with our main computation basis, and find -s using this procedure.
This allows us to express bitwise AND (in basis ) through an algebraic formula:
Moreover, this formula is actually quadratic in and their Frobenius twists.
We observe, that actually admits a rather simple expression:
i.e. it is a sum over whole Frobenius orbit. One can show that composition of these mappings for a sequence of extensions is once again mapping of this form.
Consider a polynomial (potentially, multivariate), given in coefficient form. Let us denote the application of -th power of Frobenius mapping to it. Then, it is well known that (or, explicitly, ).
Note, that this operation also applies Frobenius mapping to the values of a polynomial on points defined over . This is extremely important, as sumcheck will operate on a boolean hypercube .
In what follows, we will frequently need to compute values of a polynomial in Frobenius orbit. We give an efficient prover for this subroutine:
Suppose we are given a multilinear polynomial in evaluation form (and we will denote corresponding table of values ). We want to compute it in points
Using formulas from previous section, we know that .
Naively, this would require us to compute all Frobenius shifts of , and evaluate them.
Naive cost (counting only asymptotic terms):
This cost is very significant, and would render protocol completely impractical. We suggest the following improved method:
Then, we can estimate the improved cost:
This makes such evaluation comparable in costs with single evaluations.
Assume that we are given a polynomial , and are trying to convince verifier that . Polynomial is committed, so we can open it in any a single point. Then, there is a standard sumcheck argument, reducing multiple openings (in points ) to a single one:
Verifier sends challenge value , and we perform the sumcheck for the following equation:
In the end of sumcheck, will be specialized to some single random value , and verifier will only need to check single opening , and compute some constant amount of values .
So, this sumcheck is very efficient for the verifier, the question is how to make it efficient for the prover. Naively evaluating is out of question.
We suggest the following improved method.
This method is efficient provided that , which happens in all realistic scenarios.
Important prover subroutine is evaluating a quadratic polynomial in a point. Simplest approach is just computing its coefficients (there are terms), and evaluating it directly. There are somewhat better approaches if is large enough: one can compute , , evaluate them in (which requires 256 N additions, because these polynomials are over , and compute ).
For very small -s this method is worse, because it hides the constant multiplications to combine the evaluation and into a single answer.
We would like compute the following sumcheck on a boolean hypercube:
which is treated as quadratic formula depending on Frobenius twists of and
Let's recall that the prover response is a univariate polynomial of degree defined as:
Which can be reaaranged as
which drops the degree in under summation to 2.
Our main problem now is computing the restriction of , for which we have discussed some approaches in the previous section.
We split our protocol in phases:
Phase 1:
This phase consists of rounds, and we start by computing the table of evaluations of , in the extended set of size , namely .
This requires us to compute additions (XORs).
Then, we also evaluate on this whole subset, which requires evaluations of (and , presumably, were already done).
Note: this work will be insignificant compared to what is done next, however, this tradeoff might change if instead of we are using a more involved arithmetic circuit with multiple inputs and multiple arithmetic operations.
Next, we are ready to respond to verifier challenges. Prover enters the first round and does the following:
Phase 2
In Phase 2, we explicitly maintain polynomials , . This slowdowns us a lot, so it makes sense to search for some balance. We believe should provide a reasonable tradeoff.