Skip to content

Commit 4427531

Browse files
sai-dengsai-deng
authored
Refactor recursion quotient helpers (#160)
* refactor * remove config
1 parent 9999dcf commit 4427531

File tree

5 files changed

+187
-131
lines changed

5 files changed

+187
-131
lines changed

‎circuit/src/tables/mmcs.rs‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,7 @@ impl<F: Field + Clone + Default> MmcsPrivateData<F> {
168168
return Err(CircuitError::IncorrectNonPrimitiveOpPrivateData {
169169
op: NonPrimitiveOpType::MmcsVerify,
170170
expected: "[]".to_string(),
171-
got: format!("{:?}", last),
171+
got: format!("{last:?}"),
172172
operation_index: NonPrimitiveOpId(0), //TODO: What's the index of this op?
173173
});
174174
}
@@ -616,8 +616,7 @@ mod tests {
616616
let result = run_test(&leaves_value, correct_root, &correct_private_data);
617617
assert!(
618618
result.is_ok(),
619-
"Valid witness should be accepted but got {:?}",
620-
result
619+
"Valid witness should be accepted but got {result:?}"
621620
);
622621

623622
// Test 2: Invalid witness (wrong root) should be rejected

‎recursion/src/pcs/fri/verifier.rs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -538,8 +538,7 @@ where
538538
// Check the final polynomial length.
539539
if actual_final_poly_len != expected_final_poly_len {
540540
return Err(VerificationError::InvalidProofShape(format!(
541-
"Final polynomial length mismatch: expected 2^{} = {}, got {}",
542-
log_final_poly_len, expected_final_poly_len, actual_final_poly_len
541+
"Final polynomial length mismatch: expected 2^{log_final_poly_len} = {expected_final_poly_len}, got {actual_final_poly_len}"
543542
)));
544543
}
545544

‎recursion/src/verifier/mod.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,10 @@
22
33
mod errors;
44
mod observable;
5+
mod quotient;
56
mod stark;
67

78
pub use errors::VerificationError;
89
pub use observable::ObservableCommitment;
10+
pub use quotient::recompose_quotient_from_chunks_circuit;
911
pub use stark::verify_circuit;

‎recursion/src/verifier/quotient.rs‎

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
use alloc::vec::Vec;
2+
3+
use itertools::Itertools;
4+
use p3_circuit::CircuitBuilder;
5+
use p3_field::{BasedVectorSpace, Field, PrimeCharacteristicRing};
6+
use p3_uni_stark::StarkGenericConfig;
7+
8+
use crate::Target;
9+
use crate::traits::{Recursive, RecursivePcs};
10+
11+
/// Circuit analogue of `recompose_quotient_from_chunks`, returning quotient(zeta).
12+
pub fn recompose_quotient_from_chunks_circuit<
13+
SC: StarkGenericConfig,
14+
InputProof: Recursive<SC::Challenge>,
15+
OpeningProof: Recursive<SC::Challenge>,
16+
Comm: Recursive<SC::Challenge>,
17+
Domain: Copy,
18+
>(
19+
circuit: &mut CircuitBuilder<SC::Challenge>,
20+
quotient_chunks_domains: &[Domain],
21+
quotient_chunks: &[Vec<Target>],
22+
zeta: Target,
23+
pcs: &SC::Pcs,
24+
) -> Target
25+
where
26+
<SC as StarkGenericConfig>::Pcs: RecursivePcs<SC, InputProof, OpeningProof, Comm, Domain>,
27+
SC::Challenge: PrimeCharacteristicRing,
28+
{
29+
let zero = circuit.add_const(SC::Challenge::ZERO);
30+
let one = circuit.add_const(SC::Challenge::ONE);
31+
32+
let zps = compute_quotient_chunk_products::<SC, InputProof, OpeningProof, Comm, Domain>(
33+
circuit,
34+
quotient_chunks_domains,
35+
zeta,
36+
one,
37+
pcs,
38+
);
39+
40+
compute_quotient_evaluation::<SC>(circuit, quotient_chunks, &zps, zero)
41+
}
42+
43+
/// Compute the product terms for quotient chunk reconstruction.
44+
///
45+
/// For each chunk i, computes: ∏_{j≠i} (Z_{domain_j}(zeta) / Z_{domain_j}(first_point_i))
46+
fn compute_quotient_chunk_products<
47+
SC: StarkGenericConfig,
48+
InputProof: Recursive<SC::Challenge>,
49+
OpeningProof: Recursive<SC::Challenge>,
50+
Comm: Recursive<SC::Challenge>,
51+
Domain: Copy,
52+
>(
53+
circuit: &mut CircuitBuilder<SC::Challenge>,
54+
quotient_chunks_domains: &[Domain],
55+
zeta: Target,
56+
one: Target,
57+
pcs: &<SC as StarkGenericConfig>::Pcs,
58+
) -> Vec<Target>
59+
where
60+
<SC as StarkGenericConfig>::Pcs: RecursivePcs<SC, InputProof, OpeningProof, Comm, Domain>,
61+
{
62+
quotient_chunks_domains
63+
.iter()
64+
.enumerate()
65+
.map(|(i, domain)| {
66+
quotient_chunks_domains
67+
.iter()
68+
.enumerate()
69+
.filter(|(j, _)| *j != i)
70+
.fold(one, |total, (_, other_domain)| {
71+
let vp_zeta = vanishing_poly_at_point_circuit::<
72+
SC,
73+
InputProof,
74+
OpeningProof,
75+
Comm,
76+
Domain,
77+
>(pcs, *other_domain, zeta, circuit);
78+
79+
let first_point = circuit.add_const(pcs.first_point(domain));
80+
let vp_first_point = vanishing_poly_at_point_circuit::<
81+
SC,
82+
InputProof,
83+
OpeningProof,
84+
Comm,
85+
Domain,
86+
>(
87+
pcs, *other_domain, first_point, circuit
88+
);
89+
let div = circuit.div(vp_zeta, vp_first_point);
90+
91+
circuit.mul(total, div)
92+
})
93+
})
94+
.collect_vec()
95+
}
96+
97+
/// Compute the quotient polynomial evaluation from chunks.
98+
///
99+
/// quotient(zeta) = ∑_i (∑_j e_j · chunk_i[j]) · zps[i]
100+
fn compute_quotient_evaluation<SC: StarkGenericConfig>(
101+
circuit: &mut CircuitBuilder<SC::Challenge>,
102+
opened_quotient_chunks: &[Vec<Target>],
103+
zps: &[Target],
104+
zero: Target,
105+
) -> Target
106+
where
107+
SC::Challenge: PrimeCharacteristicRing,
108+
{
109+
opened_quotient_chunks
110+
.iter()
111+
.enumerate()
112+
.fold(zero, |quotient, (i, chunk)| {
113+
let zp = zps[i];
114+
115+
// Sum chunk elements weighted by basis elements: ∑_j e_j · chunk[j]
116+
let inner_result = chunk.iter().enumerate().fold(zero, |cur_s, (e_i, c)| {
117+
let e_i_target = circuit.add_const(SC::Challenge::ith_basis_element(e_i).unwrap());
118+
let inner_mul = circuit.mul(e_i_target, *c);
119+
circuit.add(cur_s, inner_mul)
120+
});
121+
122+
let mul = circuit.mul(inner_result, zp);
123+
circuit.add(quotient, mul)
124+
})
125+
}
126+
127+
/// Compute the vanishing polynomial Z_H(point) = point^n - 1 at a given point.
128+
///
129+
/// # Parameters
130+
/// - `pcs`: Polynomial commitment scheme for domain metadata
131+
/// - `domain`: The domain (defines n)
132+
/// - `point`: The evaluation point
133+
/// - `circuit`: Circuit builder
134+
///
135+
/// # Returns
136+
/// Target representing Z_H(point)
137+
fn vanishing_poly_at_point_circuit<
138+
SC: StarkGenericConfig,
139+
InputProof: Recursive<SC::Challenge>,
140+
OpeningProof: Recursive<SC::Challenge>,
141+
Comm: Recursive<SC::Challenge>,
142+
Domain,
143+
>(
144+
pcs: &<SC as StarkGenericConfig>::Pcs,
145+
domain: Domain,
146+
point: Target,
147+
circuit: &mut CircuitBuilder<SC::Challenge>,
148+
) -> Target
149+
where
150+
<SC as StarkGenericConfig>::Pcs: RecursivePcs<SC, InputProof, OpeningProof, Comm, Domain>,
151+
{
152+
// Normalize point: point' = point / first_point
153+
let inv = circuit.add_const(pcs.first_point(&domain).inverse());
154+
let mul = circuit.mul(point, inv);
155+
156+
// Compute (point')^n
157+
let exp = circuit.exp_power_of_2(mul, pcs.log_size(&domain));
158+
159+
// Return (point')^n - 1
160+
let one = circuit.add_const(SC::Challenge::ONE);
161+
circuit.sub(exp, one)
162+
}

‎recursion/src/verifier/stark.rs‎

Lines changed: 20 additions & 126 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,11 @@ use p3_circuit::CircuitBuilder;
88
use p3_circuit::op::{NonPrimitiveOpConfig, NonPrimitiveOpType};
99
use p3_circuit::utils::ColumnsTargets;
1010
use p3_commit::Pcs;
11-
use p3_field::{BasedVectorSpace, Field, PrimeCharacteristicRing};
11+
use p3_field::{BasedVectorSpace, PrimeCharacteristicRing};
1212
use p3_uni_stark::StarkGenericConfig;
1313
use p3_util::zip_eq::zip_eq;
1414

15-
use super::{ObservableCommitment, VerificationError};
15+
use super::{ObservableCommitment, VerificationError, recompose_quotient_from_chunks_circuit};
1616
use crate::Target;
1717
use crate::challenger::CircuitChallenger;
1818
use crate::traits::{Recursive, RecursiveAir, RecursivePcs};
@@ -31,6 +31,11 @@ type PcsVerifierParams<SC, InputProof, OpeningProof, Comm> =
3131
>>::Domain,
3232
>>::VerifierParams;
3333

34+
type PcsDomain<SC> = <<SC as StarkGenericConfig>::Pcs as Pcs<
35+
<SC as StarkGenericConfig>::Challenge,
36+
<SC as StarkGenericConfig>::Challenger,
37+
>>::Domain;
38+
3439
/// Verifies a STARK proof within a circuit.
3540
///
3641
/// This function adds constraints to the circuit builder that verify a STARK proof.
@@ -205,14 +210,19 @@ where
205210
)?;
206211

207212
// Compute quotient polynomial evaluation from chunks
208-
let zero = circuit.add_const(SC::Challenge::ZERO);
209-
let one = circuit.add_const(SC::Challenge::ONE);
210-
211-
let zps =
212-
compute_quotient_chunk_products(circuit, config, &quotient_chunks_domains, zeta, one, pcs);
213-
214-
let quotient =
215-
compute_quotient_evaluation::<SC>(circuit, opened_quotient_chunks_targets, &zps, zero);
213+
let quotient = recompose_quotient_from_chunks_circuit::<
214+
SC,
215+
InputProof,
216+
OpeningProof,
217+
Comm,
218+
PcsDomain<SC>,
219+
>(
220+
circuit,
221+
&quotient_chunks_domains,
222+
opened_quotient_chunks_targets,
223+
zeta,
224+
pcs,
225+
);
216226

217227
// Evaluate AIR constraints at out-of-domain point
218228
let sels = pcs.selectors_at_point_circuit(circuit, &init_trace_domain, &zeta);
@@ -349,119 +359,3 @@ where
349359

350360
Ok(())
351361
}
352-
353-
/// Compute the product terms for quotient chunk reconstruction.
354-
///
355-
/// For each chunk i, computes: ∏_{j≠i} (Z_{domain_j}(zeta) / Z_{domain_j}(first_point_i))
356-
fn compute_quotient_chunk_products<
357-
SC: StarkGenericConfig,
358-
InputProof: Recursive<SC::Challenge>,
359-
OpeningProof: Recursive<SC::Challenge>,
360-
Comm: Recursive<SC::Challenge>,
361-
Domain: Copy,
362-
>(
363-
circuit: &mut CircuitBuilder<SC::Challenge>,
364-
config: &SC,
365-
quotient_chunks_domains: &[Domain],
366-
zeta: Target,
367-
one: Target,
368-
pcs: &<SC as StarkGenericConfig>::Pcs,
369-
) -> Vec<Target>
370-
where
371-
<SC as StarkGenericConfig>::Pcs: RecursivePcs<SC, InputProof, OpeningProof, Comm, Domain>,
372-
{
373-
quotient_chunks_domains
374-
.iter()
375-
.enumerate()
376-
.map(|(i, domain)| {
377-
quotient_chunks_domains
378-
.iter()
379-
.enumerate()
380-
.filter(|(j, _)| *j != i)
381-
.fold(one, |total, (_, other_domain)| {
382-
let vp_zeta =
383-
vanishing_poly_at_point_circuit(config, *other_domain, zeta, circuit);
384-
385-
let first_point = circuit.add_const(pcs.first_point(domain));
386-
let vp_first_point = vanishing_poly_at_point_circuit(
387-
config,
388-
*other_domain,
389-
first_point,
390-
circuit,
391-
);
392-
let div = circuit.div(vp_zeta, vp_first_point);
393-
394-
circuit.mul(total, div)
395-
})
396-
})
397-
.collect_vec()
398-
}
399-
400-
/// Compute the quotient polynomial evaluation from chunks.
401-
///
402-
/// quotient(zeta) = ∑_i (∑_j e_j · chunk_i[j]) · zps[i]
403-
fn compute_quotient_evaluation<SC: StarkGenericConfig>(
404-
circuit: &mut CircuitBuilder<SC::Challenge>,
405-
opened_quotient_chunks: &[Vec<Target>],
406-
zps: &[Target],
407-
zero: Target,
408-
) -> Target
409-
where
410-
SC::Challenge: PrimeCharacteristicRing,
411-
{
412-
opened_quotient_chunks
413-
.iter()
414-
.enumerate()
415-
.fold(zero, |quotient, (i, chunk)| {
416-
let zp = zps[i];
417-
418-
// Sum chunk elements weighted by basis elements: ∑_j e_j · chunk[j]
419-
let inner_result = chunk.iter().enumerate().fold(zero, |cur_s, (e_i, c)| {
420-
let e_i_target = circuit.add_const(SC::Challenge::ith_basis_element(e_i).unwrap());
421-
let inner_mul = circuit.mul(e_i_target, *c);
422-
circuit.add(cur_s, inner_mul)
423-
});
424-
425-
let mul = circuit.mul(inner_result, zp);
426-
circuit.add(quotient, mul)
427-
})
428-
}
429-
430-
/// Compute the vanishing polynomial Z_H(point) = point^n - 1 at a given point.
431-
///
432-
/// # Parameters
433-
/// - `config`: STARK configuration
434-
/// - `domain`: The domain (defines n)
435-
/// - `point`: The evaluation point
436-
/// - `circuit`: Circuit builder
437-
///
438-
/// # Returns
439-
/// Target representing Z_H(point)
440-
fn vanishing_poly_at_point_circuit<
441-
SC: StarkGenericConfig,
442-
InputProof: Recursive<SC::Challenge>,
443-
OpeningProof: Recursive<SC::Challenge>,
444-
Comm: Recursive<SC::Challenge>,
445-
Domain,
446-
>(
447-
config: &SC,
448-
domain: Domain,
449-
point: Target,
450-
circuit: &mut CircuitBuilder<SC::Challenge>,
451-
) -> Target
452-
where
453-
<SC as StarkGenericConfig>::Pcs: RecursivePcs<SC, InputProof, OpeningProof, Comm, Domain>,
454-
{
455-
let pcs = config.pcs();
456-
457-
// Normalize point: point' = point / first_point
458-
let inv = circuit.add_const(pcs.first_point(&domain).inverse());
459-
let mul = circuit.mul(point, inv);
460-
461-
// Compute (point')^n
462-
let exp = circuit.exp_power_of_2(mul, pcs.log_size(&domain));
463-
464-
// Return (point')^n - 1
465-
let one = circuit.add_const(SC::Challenge::ONE);
466-
circuit.sub(exp, one)
467-
}

0 commit comments

Comments
 (0)