Description
Logup-GKR Integration in STARK Provers
Context
I have been researching how different implementations integrate Logup-GKR with STARK proofs. My focus is on two implementations:
- Miden VM, which uses Winterfell (Facebook’s STARK prover).
- Stwo Logup-GKR implementation.
Current Progress
- GKR prove function skeleton
- One lookup: prove only the denominator MLE evaluation of GKR input layer (with dummy lookup challenge)
- One lookup: verification function for the above
- One lookup: prove both the denominator and numerator
- Verification function for the above
- Multi lookup
- Sound challenge
Cost of using GKR
- 8 extra trace commitments, regardless of how many logups
- for machines with less than 16 logup accumulators, batching accumulator by pair ends up less than 8 batched accumulator columns to be committed, this is less than the cost of using GKR, so it make more sense to use GKR when there are more than 16 logup accumulator to batch.
- GKR circuit works on traces with same degree. with this and the above limitation, I will only make GKR on main machine for now.
- it is possible to make GKR work on different size of the trace: concatenate all the input layer traces together to make a very long trace, then how to build constraint to express "a long trace is concatenated from some short traces" is open question.
- trace degree is at least 32, this is limited by the SIMD implementation of stwo
Performance
after the initial implementation of logup-GKR #2579 , the observations are:
- GKR prove is costly, the cost is linear to the size of the circuit, the size of the circuit in common implementation is linear to the number of buses. These cost include linear interpolation in sumcheck, rounds of sumcheck, which involves many hash operations.
- If using blake hash, the GKR overhead for fraction accumulation surpasses the overhead of logup accumulators commitment, probably more than 10x, as blake hash is fast, making more commitments in STARK is less expensive. if using Poseidon, using GKR is more profitable, as Poseidon is slow, making more commitment in STARK can be more expensive than GKR.
- A potential optimization can "batching GKR instance", may lead to better performance, details are needed to be documented and discussed.
History notes
The main challenge is understanding how these implementations use a univariate polynomial IOP (STARK) to integrate GKR, which requires a multivariate polynomial IOP.
-
Miden VM provides a clear approach to this integration (detailed in [this doc] and [this doc]). However, its GKR and related APIs are from Winterfell (logup-gkr branch), making direct application to the Stwo backend difficult. - This may not be a blocker, as Stwo already implements GKR and sumcheck, meaning integration could be possible with modifications.
-
Stwo's GKR implementation is clear for proving a logup lookup alone, but its integration with STARK is less clear.
- One key aspect is understanding the "univariate IOP for multilinear evaluation at a point" in this example, which seems central to the integration.
- My current research is focused on understanding this component.