LogUp-based Virtual Bus

[Al-Kindi-0]

Describe your changes

An initial version of the GKR prover for the LogUp-based global virtual bus for Miden VM.

A few remarks:

1. Only the range checker sub-bus is implemented at the moment.
2. Memory handling is pretty primitive as there are many .clone() instances that could and should be avoided.
3. There is an optimization where we can reuse the evaluation of the merged polynomials in the last sum-check. This is not implemented but we should comeback to it.
4. There are many places where the code could easily benefit from mult-threading. This is left for latter.

A note about the usage in the context of the overall STARK. After the prover commits to the main-trace and sends the commitment to the verifier, the verifier replies with the LogUp randomness (i.e., the $\alpha$ values). At this point, and as part of the auxiliary trace building logic (see here), the prover initializes and runs

let vb_prover = VirtualBusProver::new(alphas)?;
let gkr_proof = vb_prover.prove(&trace, &mut transcript);

The above gkr_proof should be attached to the usual STARK proof so that the STARK verifier can call a GKR verifier to verify it as part of its proof verification. As part of the auxiliary trace building logic still, the prover then uses

let FinalOpeningClaim{ eval_point, openings } = proof.get_final_opening_claim();

To get the randomness defining the Lagrange kernel auxiliary trace column and the openings which will be used to define a boundary constraint against the multi-linear opening helper column (column s here) and before that the batching randomness $\lambda$ as

transcript.reseed(Rpo256::hash_elements(&openings));
let lambda = transcript.draw();// TODO: should draw a vector

At this point the constraints, both boundary and transition, are updated and both multi-linear opening helper columns of the auxiliary trace are constructed. This concludes the auxiliary trace building stage and at this point the protocol continues as before.

Checklist before requesting a review

• Repo forked and branch created from next according to naming convention.
• Commit messages and codestyle follow conventions.
• Relevant issues are linked in the PR description.
• Tests added for new functionality.
• Documentation/comments updated according to changes.

[Al-Kindi-0]

In addition to the main suggestion I made in the last comment, I'm confused about our use of CompositionPolynomial and MultiLinearPoly. We make a MultiLinearPoly for each column in our trace, and then use CompositionPolynomials to encode looking up these columns to build the numerators and denominators. This confuses me, since MultiLinearPoly is supposed to be the fi's, but it no longer is in the implementation.

MultiLinearPoly stands for the MLE of a map from the Boolean hyper-cube to the field. In the code MultiLinearPoly is used for the trace columns (these are maps from the hyper-cube to the (base) field) and is also use for numerators/ denominators in in all sum-checks except the last one. CompositionPolynomial stands for a non-linear multi-variate polynomial. This is used when there is a non-linear expression involving MLEs. So, one can have a linear combination of CompositionPolynomial all of the same arity and composed with the same set of MLEs. We can also have a Merge operation on such linear combinations and we can multiply such expressions. The result of these operations is again a CompositionPolynomial. Now if this last CompositionPolynomial is the one corresponding to the g in the sum-check docs and the multi-linears it is composed with are the f_is therein.

I haven't read through the entire PR, but could we do away with CompositionPolynomials? It seems like they come with a lot of boilerplate (a different type for each numerator/denominator expression, use of Arc<dyn ...>, etc), and are usually little more than accessing 1-3 trace columns. Basically we could make MultiLinearPoly actually represent the f_is, and then use functions to represent the various numerator/denominators (haven't thought too much exactly how to best model this yet)?

I would love to simplify this also. Indeed, the use of so much boilerplate is a bit irritating. I have spent some time thinking about it and I think that there might be a simpler way to do things. Will update this comment soon...

[plafer]

Note: changed the base to logup-gkr so that we may merge follow-up PRs before merging into next