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]

Should be changed

[Al-Kindi-0]

Should be changed

[plafer]

Right, putting the EqFunction as the last ml is very brittle, and makes the code harder to follow. Ultimately, we need the EqFunction evaluation in the GkrComposition::evaluate(); couldn't we just evaluate it there directly?

And then SimpleGkrFinalClaimBuilder wouldn't need to remove the last opening.

[Al-Kindi-0]

Should use multi-threads

[Al-Kindi-0]

Only the columns which figure in the virtual bus relation should be used here. At the moment all of the trace is used but this should changed in the future

[plafer]

Thank you for this - it will really help to clear up any remaining confusions for me!

(Not a full review yet)

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 $f_i$'s, but it no longer is in the implementation.

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)?

[plafer]

Why do we zero out the last row?

Also we could use the slice last_mut() method instead of [trace_len - 1]

[Al-Kindi-0]

This is because we randomize the last row of the trace here

miden-vm/processor/src/trace/mod.rs

Line 332 in 3e74f9c

column[i] = rng.draw().expect("failed to draw a random value");

This is mainly because of some quirks regarding degree validation in Winterfell.
Will change to last_mut()

[plafer]

This yields a "tangled" circuit, which is to draw out and reason about. If we view each gate of the circuit as performing a sum over projective coordinates (p0, q0) + (p1, q1) (the interpretation in the paper)

• out_p_0 is the vector of all p0s of the next layer (gates' left numerator)
• out_p_1 is the vector of all p1s of the next layer (gates' right numerator)
• out_q_0 is the vector of all q0s of the next layer (gates' left denom)
• out_q_1 is the vector of all q1s of the next layer (gates' right denom)

However, out_p_1 is defined to start at index len/2, i.e. in the next layer, the first gate's right numerator is halfway down the first layer. I would have expected out_p_1[0] to be made up of indices 2 and 3 from the first layer instead.

But more generally, I find keeping track of the p's and q's like this very difficult. It would seem more natural to me to have some ProjectiveCoordinate type, with addition defined (p0, q0) + (p1, q1) = (p0*q1 + p1*q0, q0*q1), and encode the circuit as a list of ProjectiveCoordinates. Then, to get the next layer, we just apply the sum to neighbors: [layer[0] + layer[1], layer[2] + layer[3], ...], where layer is a vector of all projective coordinates for a given layer.

[Al-Kindi-0]

To describe what is happening in the code above, we can do the following instead of lines 121-126

        let mut out_p = (0..len)
            .map(|i| inp_p_0[i] * inp_q_1[i] + inp_p_1[i] * inp_q_0[i])
            .collect::<Vec<E>>();
        let outp_p_1 = out_p.split_off(len/2);
        let outp_p_0 = out_p;

The use of "projective coordinate" in the paper is just to give some intuition on the technique. However, and this is why the code avoids its mention or use, the numerator (or denominators) should be viewed as multi-linear extension polynomials (especially for the deeper layers). With this view, if we denote by $p(x_0, \cdots, x_{\nu - 1})$ the multi-linear extension of all of the numerators at a certain layer, then $p(x_0, \cdots, x_{\nu - 2}, 0)$ is exactly our *_p_0 and $p(x_0, \cdots, x_{\nu - 2}, 1)$ is our *_p_1 vector. This translates directly to the formulas given in the paper for the sum-checks at a given layer.
If you still think that the use of projective coordinates is more intuitive, I would suggest that we create an issue for it and tackle it once we are decided on the bigger issues.

[plafer]

As I understand it, this doesn't yield the same circuit as in the paper. IIUC, it should be:

let mut out_p_0 = Vec::new();
let mut out_p_1 = Vec::new();
let mut out_q_0 = Vec::new();
let mut out_q_1 = Vec::new();

for i in 0..len/2 {
  out_p_0[i] = in_p_0[2*i] * in_q_1[2*i] + in_p_1[2*i] * in_q_0[2*i];
  out_p_1[i] = in_p_0[2*i + 1] * in_q_1[2*i + 1] + in_p_1[2*i + 1] * in_q_0[2*i + 1];
  out_q_0[i] = in_q_0[2*i] * in_q_1[2*i];
  out_q_1[i] = in_q_0[2*i + 1] * in_q_1[2*i + 1];
}

[plafer]

Upon closer inspection, I see that your implementation is consistent with how you defined the input layer here. However, I would change that too, so that it corresponds to expanding the LogUp sum for the range checker bus. Specifically, the sum expression is:

$$ \sum_{x \in \{0 , 1\}^{\nu}} \frac{\mathrm{rc_multiplicity}(x)}{(\alpha - \mathrm{rc_value})(x)} + \frac{-\mathrm{f_s}(x)}{(\alpha - \mathrm{sv_0})(x)} + \frac{-\mathrm{f_s}(x)}{(\alpha - \mathrm{sv_1})(x)} + \frac{-\mathrm{f_s}(x)}{(\alpha - \mathrm{sv_2})(x)} + \frac{-\mathrm{f_s}(x)}{(\alpha - \mathrm{sv_3})(x)} + \frac{-\mathrm{f_m}(x)}{(\alpha - \mathrm{mv_0})(x)} + \frac{-\mathrm{f_m}(x)}{(\alpha - \mathrm{mv_1})(x)} + \frac{0(x)}{1(x)} $$

Expanded out, we get

$$ \frac{\mathrm{rc_multiplicity}(0)}{(\alpha - \mathrm{rc_value})(0)} + \frac{-\mathrm{f_s}(0)}{(\alpha - \mathrm{sv_0})(0)} + \frac{-\mathrm{f_s}(0)}{(\alpha - \mathrm{sv_1})(0)} + \frac{-\mathrm{f_s}(0)}{(\alpha - \mathrm{sv_2})(0)} + \frac{-\mathrm{f_s}(0)}{(\alpha - \mathrm{sv_3})(0)} + \frac{-\mathrm{f_m}(0)}{(\alpha - \mathrm{mv_0})(0)} + \frac{-\mathrm{f_m}(0)}{(\alpha - \mathrm{mv_1})(0)} + \frac{0(0)}{1(0)} + \cdots $$

Given the tree we would build with these as the leaves, I would expect our 4 numerator/denominators to be defined as:

$$ \begin{align*} p0 &= [\mathrm{rc_multiplicity}(0), -\mathrm{f_s}(0), -\mathrm{f_s}(0), -\mathrm{f_m}(0)] \\ p1 &= [-\mathrm{f_s}(0), -\mathrm{f_s}(0), -\mathrm{f_m}(0), 0(0)]\\ q0 &= [(\alpha - \mathrm{rc_value})(0), (\alpha - \mathrm{sv_1})(0), (\alpha - \mathrm{sv_3})(0), (\alpha - \mathrm{mv_1})(0)]\\ q1 &= [(\alpha - \mathrm{sv_0})(0), (\alpha - \mathrm{sv_2})(0), (\alpha - \mathrm{mv_0})(0), 1(0)]\\ \end{align*} $$

compared to how they are currently defined:

$$ \begin{align*} p0 &= [ \mathrm{rc_multiplicity}(0), -\mathrm{f_s}(0), -\mathrm{f_s}(0), -\mathrm{f_s}(0)] \\ p1 &= [ -\mathrm{f_s}(0), -\mathrm{f_m}(0), -\mathrm{f_m}(0), 0(0)] \\ q0 &= [ (\alpha - \mathrm{rc_value})(0), (\alpha - \mathrm{sv_0})(0), (\alpha - \mathrm{sv_1})(0), (\alpha - \mathrm{sv_2})(0)] \\ q1 &= [ (\alpha - \mathrm{sv_3})(0), (\alpha - \mathrm{mv_0})(0), (\alpha - \mathrm{mv_1})(0), 1(0)] \\ \end{align*} $$

[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]

We could make

pub enum ProverError {
    // ...
    FailedToGenerateMl(#[from] RandomCoinError)
    // ...
}

and change this line to

let r_batch = transcript.draw()?;

[Al-Kindi-0]

That would be nice. I tried it and I think we need to modify RandomCoinError as well. Here is the error:
missing #[error("...")] display attribute

[plafer]

Is there a reason why claims at the GKR level are not reduced the same way as the sum-check level? Given 2 claims c0 and c1, and some randomness r,

• GKR: c = c0 + r * (c1 - c0)
• sum-check: c = c0 + r * c1

[Al-Kindi-0]

The reason for the expression used in the GKR claim reduction is due to the use of linear interpolation formula to evaluate a multi-linear.
We could use the same for batching the two sum-checks but we don't need to afais. There is a slight advantage of having a subtraction less in the currently used batching expression.

[bobbinth]

Why do we introduce new_round_claim variable here? Seems like the following should be equivalent:

for i in 1..num_rounds {
    // generate random challenge r_i for the i-th round
    let round_challenge = coin.draw().map_err(|_| Error::FailedToGenerateChallenge)?;

    // compute the new reduced round claim
    current_round_claim =
        reduce_claim(&round_proofs[i - 1], current_round_claim, round_challenge);

    // fold each multi-linear using the round challenge
    mls.iter_mut().for_each(|ml| ml.bind(round_challenge));

    // run the i-th round of the protocol using the folded multi-linears for the new reduced
    // claim. This basically computes the s_i polynomial.
    let round_poly_evals = sumcheck_round(&self.composition_poly, mls);
    let round_poly_coefs = round_poly_evals.to_poly(current_round_claim.claim);

    // reseed with the s_i polynomial
    coin.reseed(H::hash_elements(&round_poly_coefs.coefficients));
    let round_proof = RoundProof { round_poly_coefs };
    round_proofs.push(round_proof);
}

[Al-Kindi-0]

That's mainly for readability. No strong preference from my side though

[bobbinth]

A few questions here:

1. Why do we need dynamic objects here (i.e., dyn)? Could we not just use simple generics?
2. It seems like invocation of sumcheck_round() is always followed by .to_poly() call on the result. Would it make sense to move .to_poly() call into the sumcheck_round() function.
3. Why mls parameter needs to be passed in as mut? It doesn't seem like we are mutating it in the function.

Applying all 3 changes above, the signature of the function could look like so:

fn sumcheck_round<E: FieldElement, P: CompositionPolynomial<E>>(
    composition_poly: &P,
    mls: &[MultiLinearPoly<E>],
) -> UnivariatePolyCoef<E> 

[Al-Kindi-0]

1. Probably a remnant from a previous approach. Changed.
2. We can, but then we would have to pass claim so that we can call to_poly. I think keeping sumcheck_round clean is a good idea but, again, no strong preference from my side.
3. I doesn't. Changed

[bobbinth]

2. We can, but then we would have to pass claim so that we can call to_poly. I think keeping sumcheck_round clean is a good idea but, again, no strong preference from my side.

Ah - I see. Let's keep it as is for now.

[bobbinth]

It seems like RoundProof and UnivariatePolyCoef are basically the same thing and are always used together. I'm wondering if we need two separate structs for it. Alternatives could be:

1. Keep RoundProof and get rid of UnivariatePolyCoef. To do this, we'll need to move evaluate_using_claim() method into the RoundProof struct.
2. Keep UnivariatePolyCoef and get rid of RoundProof - this would take even fewer changes than option 1 above.

[bobbinth]

Another option (especially if we go with the changes to the sumcheck_round() function described in #1307 (comment)) could be to get rid of RoundProof and UnivariatePolyEvals and keep just UnivariatePolyCoef (and maybe rename it to just UnivariatePoly). This struct then could look like this:

pub struct UnivariatePoly<E> {
    coefficients: Vec<E>,
}

impl<E: FieldElement> UnivariatePoly<E> {

    pub fn from_evaluations(evaluations: Vec<E>, round_claim: E) -> Self {
        // this would be basically the same method as UnivariatePolyEvals::to_poly()
    }

    pub fn evaluate_using_claim(&self, claim: E, challenge: E) -> E {
       // this method would be the same as now
    }

    pub fn hash<H: ElementHasher<BaseField = E::BaseField>>(&self) -> H::Digest {
        // compute the hash of coefficients
    }
}

[Al-Kindi-0]

I think keeping RoundProof is nice from a clarity point of view but on the other hand it is no different than a polynomial for all practical purposes.
If we are willing to pass claim to sumcheck_round then the above should work

[plafer]

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

[bobbinth]

Are we using this somewhere? I think standard thiserror requires stdblib and we should probably use the one forked by @bitwalker as we do in the assembler. Though, we should probably move it into this org - probably as miden-thiserror.

[bitwalker]

Yeah we should use the fork anywhere in this workspace that we depend on thiserror, at least temporarily - the error_in_core feature is stabilized in 1.80, and I expect that the mainline thiserror will support no-std shortly thereafter. With that in mind, it probably is not worth moving the thiserror fork to our org for such a short time. That said, I'll double check and see what the plan is though for thiserror, and if it looks like it'll be a month or two, then moving it makes more sense (I don't actually care whether we move it now or not, but didn't want to overcomplicate things for what amounts to a temporary workaround).

We probably should move the miette fork to our org though, since that will likely stick around for awhile longer, even once the thiserror fork goes away. I can try to find some time to do that.

[bobbinth]

the error_in_core feature is stabilized in 1.80

Ah - I didn't realize it is already slated for 1.80. In this case, no need to create miden-thiserror - we can just rely on your fork until the canonical thiserror is updated.

[bobbinth]

Is this basically the only place where we have logic specific to Miden VM? Not for this PR, but I'm wondering if everything else is generic logic that could be a part of Winterfell rather than Miden VM. For example, we could introduce a method on the Air trait that would basically do the job of this function and look something like this:

fn build_gkr_input_layer<F, E>(&self, row: &[F], logup_rands: &[E) -> [Vec<E>; 2]
where
  F: FieldElement<BaseField = Self::BaseField>,
  E: FieldElement<BaseField = Self::BaseField> + ExtensionOf<F>,

And then both GKR prover and verifier would be able to use this to build and verify the proof respectively.

A couple of other questions:

• What is log_up_randomness here? Is it a set of random values generated from the main trace commitment root? Are these the "lambdas" referenced in this issue or is it something else?
  • I'm assuming we are using only the first element from log_up_randomness because of the nature of the constraints. If we had more complicated tables (e.g., where multiple columns needed to be merged into a single value per row), we'd need to use more random elements - right?
• Where would we specify "boundary" constraints for the buses? Specifically, for sub-busses which do not start and/or end with 0, what would be the way to specify initial/final values?

[Al-Kindi-0]

Yes, that makes sense. This will require however that Winterfell is able to handle the logic for building the s-column similar to how it does for the l-column (i.e., Lagrange column).

To this end we would need to introduce the concept of an oracle. This is basically a wrapper around CompositionPolynomial with information about the index of the columns appearing in the algebraic expression encoded in the CompositionPolynomial as well as additional information needed to verify the final evaluation claim e.g., whether a column is periodic (or more generally transparent) and thus can be computed by the verifier un-assisted and hence does not need to be included in the s-column, whether a column is a shift as this is important when building the s-column...

• What is log_up_randomness here? Is it a set of random values generated from the main trace commitment root?

Yes, these are the randomness generated from the main trace commitment, usually called the $\alpha$'s and indeed if we had more column to merge we would use more than one.

Where would we specify "boundary" constraints for the buses? Specifically, for sub-busses which do not start and/or end with 0, what would be the way to specify initial/final values?

The verifier will compute all of the boundary values in order to get a single claim value. The verifier will then check that the output of the LogUp circuit equals that claim. More precisely this would be done here

pub fn verify<
    E: FieldElement<BaseField = Felt>,
    C: RandomCoin<Hasher = H, BaseField = Felt>,
    H: ElementHasher<BaseField = Felt>,
>(
    claim: E,
    proof: GkrCircuitProof<E>,
    log_up_randomness: Vec<E>,
    transcript: &mut C,
) -> Result<FinalOpeningClaim<E>, VerifierError> {
...
// check that the output matches the expected `claim`
    if (p0 * q1 + p1 * q0) / (q0 * q1) != claim {
        return Err(VerifierError::MismatchingCircuitOutput);
    }
...
}

At the moment, claim is set to zero but if we want to go with the proposal of delegating everything to Winterfell, then we would need to add a method to the GKR verifier so that it can compute claim from the public inputs.

[bobbinth]

Question: how big can we expect the proof to be (e.g., in KB) and what are the primary drivers? I'm guessing the primary driver is the complexity of the bus constraints - but does trace length also make a big difference?

[Al-Kindi-0]

The proof is composed of two parts:

1. The round polynomials: The number of these is dependent on the trace length as well as the complexity of the bus. The degree of these is dependent on the max selector degree.
2. The opening points: The number of this dependent on the trace length and the complexity of the bus.

To give a concrete formula, suppose that the trace length is $2^{\nu}$ and the number of fractions defining the bus is $2^{\mu + 1}$, then:

1. The number of field elements defining the round polynomials is given by $$\frac{3\cdot(\mu + \nu - 1)\cdot(\mu + \nu)}{2} + 3\cdot\mu + d\cdot\nu,$$ the $3$ represents the degree of the round polynomials in the sum-checks appearing in all but the final sum-check, while the $d$ represent the degree of the round polynomial for the final sum-check (which depends as stated above on the degree of the selectors).
2. The number of opening points is given by $$4\cdot (\mu + \nu - 1) + k,$$ where $k$ is the number of trace columns, as well as their shifts, appearing in the bus.

Note that all elements in the above are extension field elements.

To give some concrete numbers, suppose that $\nu = 20$, $\mu = 5$ and $k = 5$ (max selector degree is 3), then:

1. The proof size due to round polynomials is: 1015 extension field elements which translates in the case of a quadratic extension degree to about 16Kb.
2. The proof size due to opening points is: 136 extension field elements assuming we open 40 columns and column-shifts. This translates in the case of a quadratic extension degree to about 2Kb.

[plafer]

Suggested change

	log_up_randomness: &[E],
	log_up_randomness: &E,

log_up_randomness is guaranteed to be a single element, so we should change it everywhere to only be &E