-
Notifications
You must be signed in to change notification settings - Fork 303
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unified Recursion Circuit for Multi-Degree Starky Proof Verification #1635
Conversation
870bbe7
to
1e3c8b9
Compare
I would like to provide some clarification based on my offline discussion with @hratoanina Currently, we only support maximum degree bits of {30, 26, 22, 18, …} in the recursive verifier circuit, as they generate the max final polynomial length when using the default configuration We will always pad the proof with smaller degree bits (than the circuit’s degree bits) with zeros to Merkle proofs and final polynomials and "skip" some FRI steps or hashing steps in Merkle verification. Compared to the previous method, degree bits are now variables instead of constants. This PR does not affect the speed of the provers or alter any security assumptions of STARK. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Globally, I think it would be better to have more comments, and I think it would be beneficial to have one big paragraph explaining how the multiple degrees work. So it would be nice to explain the verifier has a max number of folding steps and some are skipped if the actual degree is lower.
In addition, saying the FRI strategy has to be the same across proofs using this multi-degree circuit would be nice.
Finally, I think the degrees you mentioned above (and in the test) are off by one, aren't they? (Shouldn't it be 29, 25, ... instead of 30, 26, ...?)
Thanks for this work though, it is really great!
let zero_cap = vec![F::ZERO; cap_len]; | ||
for _ in fri_params.reduction_arity_bits.len()..step_count { | ||
challenger.observe_elements(&zero_cap); | ||
challenger.get_extension_challenge::<D>(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why do we need this? We just need to observe, but we don't need a challenge, do we?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, we need to observe and get a challenge here, as we want the challenger to be in sync with the verifier.
let log_n = params.config.rate_bits + params.degree_bits; | ||
let mut current_log_n = self.constant(F::from_canonical_usize(params.config.rate_bits)); | ||
current_log_n = self.add(current_log_n, current_degree_bits); | ||
let min_log_n_to_support = log_n - (params.degree_bits - min_degree_bits_to_support); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: I think it would be a tad clearer to write it like this instead:
let min_log_n_to_support = log_n - (params.degree_bits - min_degree_bits_to_support); | |
let min_log_n_to_support = params.config.rate_bits + min_degree_bits_to_support; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
|
||
let mut index_in_degree_sub_one_bits_vec = { | ||
let mut degree_bits_len = degree_sub_one_bits_vec.len(); | ||
for artity_bits in ¶ms.reduction_arity_bits { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit
for artity_bits in ¶ms.reduction_arity_bits { | |
for arity_bits in ¶ms.reduction_arity_bits { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
plonky2/src/gadgets/random_access.rs
Outdated
@@ -39,6 +41,20 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> { | |||
claimed_element | |||
} | |||
|
|||
/// Like `random_access`, but padding `v` with the last element to a power of two. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add that this is necessary because random_access
requires a power of two? (I'm not sure whether it would be better to add it here or to random_access
directly)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good, I modified random_access directly.
plonky2/src/fri/challenges.rs
Outdated
@@ -28,6 +32,8 @@ impl<F: RichField, H: Hasher<F>> Challenger<F, H> { | |||
pow_witness: F, | |||
degree_bits: usize, | |||
config: &FriConfig, | |||
final_poly_coeff_len: Option<usize>, | |||
query_round_step_count: Option<usize>, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I find this name unclear: maybe say that it's the max number of steps? So something like max_number_steps
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
renamed to max_num_query_steps
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same comments as Linda, very nice work!
I have a general question about the method: it seems that an arbitrary reduction strategy for the multi-verifier is supported, as long as the prover correctly follows the same strategy, and skips steps as needed. Is it in the scope of this PR, or do you want to restrict it to ConstantArityBits
strategies? In any case this should be clearly stated somewhere in the code.
We don’t have to, but I added checks to restrict it to |
The degrees are correct, as the final poly's |
Thanks for the reviews! All comments have been addressed. Additionally, we already have a |
This PR introduces an enhanced recursion circuit that supports Starky proof verification across multiple degrees. This work significantly reduces the number of recursion circuits needed for zkVM/zkEVM proof recursion. Although the new circuit adds approximately 1000-4000 more gates compared to the previous fixed-degree recursion circuit, the padded circuit size remains unchanged for commonly used cases within the 2^22 - 2^26 range (fibonacci_stark). Additionally, the extra gates added for the more complex recursive circuit (e.g. Keccak STARK) can be considered negligible.
Circuit Size Comparison (fibonacci_stark):
Example: In the previous setup, the recursion circuit supported proof verification at degree bits 22 with a final degree of 16384. The updated recursion circuit supports proof verification across degree bits from 4 to 22 while retaining the final degree of 16384.
Old Circuit Details:
New Circuit Details: