miden-crypto/src/gkr/circuit/mod.rs
src/gkr/circuit/mod.rsRaw
1use alloc::sync::Arc;
2use winter_crypto::{ElementHasher, RandomCoin};
3use winter_math::fields::f64::BaseElement;
4use winter_math::FieldElement;
5
6use crate::gkr::multivariate::{
7 ComposedMultiLinearsOracle, EqPolynomial, GkrCompositionVanilla, MultiLinearOracle,
8};
9use crate::gkr::sumcheck::{sum_check_verify, Claim};
10
11use super::multivariate::{
12 gen_plain_gkr_oracle, gkr_composition_from_composition_polys, ComposedMultiLinears,
13 CompositionPolynomial, MultiLinear,
14};
15use super::sumcheck::{
16 sum_check_prove, sum_check_verify_and_reduce, FinalEvaluationClaim,
17 PartialProof as SumcheckInstanceProof, RoundProof as SumCheckRoundProof, Witness,
18};
19
20/// Layered circuit for computing a sum of fractions.
21///
22/// The circuit computes a sum of fractions based on the formula a / c + b / d = (a * d + b * c) / (c * d)
23/// which defines a "gate" ((a, b), (c, d)) --> (a * d + b * c, c * d) upon which the `FractionalSumCircuit`
24/// is built.
25/// TODO: Swap 1 and 0
26#[derive(Debug)]
27pub struct FractionalSumCircuit<E: FieldElement> {
28 p_1_vec: Vec<MultiLinear<E>>,
29 p_0_vec: Vec<MultiLinear<E>>,
30 q_1_vec: Vec<MultiLinear<E>>,
31 q_0_vec: Vec<MultiLinear<E>>,
32}
33
34impl<E: FieldElement> FractionalSumCircuit<E> {
35 /// Computes The values of the gates outputs for each of the layers of the fractional sum circuit.
36 pub fn new_(num_den: &Vec<MultiLinear<E>>) -> Self {
37 let mut p_1_vec: Vec<MultiLinear<E>> = Vec::new();
38 let mut p_0_vec: Vec<MultiLinear<E>> = Vec::new();
39 let mut q_1_vec: Vec<MultiLinear<E>> = Vec::new();
40 let mut q_0_vec: Vec<MultiLinear<E>> = Vec::new();
41
42 let num_layers = num_den[0].len().ilog2() as usize;
43
44 p_1_vec.push(num_den[0].to_owned());
45 p_0_vec.push(num_den[1].to_owned());
46 q_1_vec.push(num_den[2].to_owned());
47 q_0_vec.push(num_den[3].to_owned());
48
49 for i in 0..num_layers {
50 let (output_p_1, output_p_0, output_q_1, output_q_0) =
51 FractionalSumCircuit::compute_layer(
52 &p_1_vec[i],
53 &p_0_vec[i],
54 &q_1_vec[i],
55 &q_0_vec[i],
56 );
57 p_1_vec.push(output_p_1);
58 p_0_vec.push(output_p_0);
59 q_1_vec.push(output_q_1);
60 q_0_vec.push(output_q_0);
61 }
62
63 FractionalSumCircuit { p_1_vec, p_0_vec, q_1_vec, q_0_vec }
64 }
65
66 /// Compute the output values of the layer given a set of input values
67 fn compute_layer(
68 inp_p_1: &MultiLinear<E>,
69 inp_p_0: &MultiLinear<E>,
70 inp_q_1: &MultiLinear<E>,
71 inp_q_0: &MultiLinear<E>,
72 ) -> (MultiLinear<E>, MultiLinear<E>, MultiLinear<E>, MultiLinear<E>) {
73 let len = inp_q_1.len();
74 let outp_p_1 = (0..len / 2)
75 .map(|i| inp_p_1[i] * inp_q_0[i] + inp_p_0[i] * inp_q_1[i])
76 .collect::<Vec<E>>();
77 let outp_p_0 = (len / 2..len)
78 .map(|i| inp_p_1[i] * inp_q_0[i] + inp_p_0[i] * inp_q_1[i])
79 .collect::<Vec<E>>();
80 let outp_q_1 = (0..len / 2).map(|i| inp_q_1[i] * inp_q_0[i]).collect::<Vec<E>>();
81 let outp_q_0 = (len / 2..len).map(|i| inp_q_1[i] * inp_q_0[i]).collect::<Vec<E>>();
82
83 (
84 MultiLinear::new(outp_p_1),
85 MultiLinear::new(outp_p_0),
86 MultiLinear::new(outp_q_1),
87 MultiLinear::new(outp_q_0),
88 )
89 }
90
91 /// Computes The values of the gates outputs for each of the layers of the fractional sum circuit.
92 pub fn new(poly: &MultiLinear<E>) -> Self {
93 let mut p_1_vec: Vec<MultiLinear<E>> = Vec::new();
94 let mut p_0_vec: Vec<MultiLinear<E>> = Vec::new();
95 let mut q_1_vec: Vec<MultiLinear<E>> = Vec::new();
96 let mut q_0_vec: Vec<MultiLinear<E>> = Vec::new();
97
98 let num_layers = poly.len().ilog2() as usize - 1;
99 let (output_p, output_q) = poly.split(poly.len() / 2);
100 let (output_p_1, output_p_0) = output_p.split(output_p.len() / 2);
101 let (output_q_1, output_q_0) = output_q.split(output_q.len() / 2);
102
103 p_1_vec.push(output_p_1);
104 p_0_vec.push(output_p_0);
105 q_1_vec.push(output_q_1);
106 q_0_vec.push(output_q_0);
107
108 for i in 0..num_layers - 1 {
109 let (output_p_1, output_p_0, output_q_1, output_q_0) =
110 FractionalSumCircuit::compute_layer(
111 &p_1_vec[i],
112 &p_0_vec[i],
113 &q_1_vec[i],
114 &q_0_vec[i],
115 );
116 p_1_vec.push(output_p_1);
117 p_0_vec.push(output_p_0);
118 q_1_vec.push(output_q_1);
119 q_0_vec.push(output_q_0);
120 }
121
122 FractionalSumCircuit { p_1_vec, p_0_vec, q_1_vec, q_0_vec }
123 }
124
125 /// Given a value r, computes the evaluation of the last layer at r when interpreted as (two)
126 /// multilinear polynomials.
127 pub fn evaluate(&self, r: E) -> (E, E) {
128 let len = self.p_1_vec.len();
129 assert_eq!(self.p_1_vec[len - 1].num_variables(), 0);
130 assert_eq!(self.p_0_vec[len - 1].num_variables(), 0);
131 assert_eq!(self.q_1_vec[len - 1].num_variables(), 0);
132 assert_eq!(self.q_0_vec[len - 1].num_variables(), 0);
133
134 let mut p_1 = self.p_1_vec[len - 1].clone();
135 p_1.extend(&self.p_0_vec[len - 1]);
136 let mut q_1 = self.q_1_vec[len - 1].clone();
137 q_1.extend(&self.q_0_vec[len - 1]);
138
139 (p_1.evaluate(&[r]), q_1.evaluate(&[r]))
140 }
141}
142
143/// A proof for reducing a claim on the correctness of the output of a layer to that of:
144///
145/// 1. Correctness of a sumcheck proof on the claimed output.
146/// 2. Correctness of the evaluation of the input (to the said layer) at a random point when
147/// interpreted as multilinear polynomial.
148///
149/// The verifier will then have to work backward and:
150///
151/// 1. Verify that the sumcheck proof is valid.
152/// 2. Recurse on the (claimed evaluations) using the same approach as above.
153///
154/// Note that the following struct batches proofs for many circuits of the same type that
155/// are independent i.e., parallel.
156#[derive(Debug)]
157pub struct LayerProof<E: FieldElement> {
158 pub proof: SumcheckInstanceProof<E>,
159 pub claims_sum_p1: E,
160 pub claims_sum_p0: E,
161 pub claims_sum_q1: E,
162 pub claims_sum_q0: E,
163}
164
165#[allow(dead_code)]
166impl<E: FieldElement<BaseField = BaseElement> + 'static> LayerProof<E> {
167 /// Checks the validity of a `LayerProof`.
168 ///
169 /// It first reduces the 2 claims to 1 claim using randomness and then checks that the sumcheck
170 /// protocol was correctly executed.
171 ///
172 /// The method outputs:
173 ///
174 /// 1. A vector containing the randomness sent by the verifier throughout the course of the
175 /// sum-check protocol.
176 /// 2. The (claimed) evaluation of the inner polynomial (i.e., the one being summed) at the this random vector.
177 /// 3. The random value used in the 2-to-1 reduction of the 2 sumchecks.
178 pub fn verify_sum_check_before_last<
179 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
180 H: ElementHasher<BaseField = BaseElement>,
181 >(
182 &self,
183 claim: (E, E),
184 num_rounds: usize,
185 transcript: &mut C,
186 ) -> ((E, Vec<E>), E) {
187 // Absorb the claims
188 let data = vec![claim.0, claim.1];
189 transcript.reseed(H::hash_elements(&data));
190
191 // Squeeze challenge to reduce two sumchecks to one
192 let r_sum_check: E = transcript.draw().unwrap();
193
194 // Run the sumcheck protocol
195
196 // Given r_sum_check and claim, we create a Claim with the GKR composer and then call the generic sum-check verifier
197 let reduced_claim = claim.0 + claim.1 * r_sum_check;
198
199 // Create vanilla oracle
200 let oracle = gen_plain_gkr_oracle(num_rounds, r_sum_check);
201
202 // Create sum-check claim
203 let transformed_claim = Claim {
204 sum_value: reduced_claim,
205 polynomial: oracle,
206 };
207
208 let reduced_gkr_claim =
209 sum_check_verify_and_reduce(&transformed_claim, self.proof.clone(), transcript);
210
211 (reduced_gkr_claim, r_sum_check)
212 }
213}
214
215#[derive(Debug)]
216pub struct GkrClaim<E: FieldElement + 'static> {
217 evaluation_point: Vec<E>,
218 claimed_evaluation: (E, E),
219}
220
221#[derive(Debug)]
222pub struct CircuitProof<E: FieldElement + 'static> {
223 pub proof: Vec<LayerProof<E>>,
224}
225
226impl<E: FieldElement<BaseField = BaseElement> + 'static> CircuitProof<E> {
227 pub fn prove<
228 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
229 H: ElementHasher<BaseField = BaseElement>,
230 >(
231 circuit: &mut FractionalSumCircuit<E>,
232 transcript: &mut C,
233 ) -> (Self, Vec<E>, Vec<Vec<E>>) {
234 let mut proof_layers: Vec<LayerProof<E>> = Vec::new();
235 let num_layers = circuit.p_0_vec.len();
236
237 let data = vec![
238 circuit.p_1_vec[num_layers - 1][0],
239 circuit.p_0_vec[num_layers - 1][0],
240 circuit.q_1_vec[num_layers - 1][0],
241 circuit.q_0_vec[num_layers - 1][0],
242 ];
243 transcript.reseed(H::hash_elements(&data));
244
245 // Challenge to reduce p1, p0, q1, q0 to pr, qr
246 let r_cord = transcript.draw().unwrap();
247
248 // Compute the (2-to-1 folded) claim
249 let mut claim = circuit.evaluate(r_cord);
250 let mut all_rand = Vec::new();
251
252 let mut rand = Vec::new();
253 rand.push(r_cord);
254 for layer_id in (0..num_layers - 1).rev() {
255 let len = circuit.p_0_vec[layer_id].len();
256
257 // Construct the Lagrange kernel evaluated at previous GKR round randomness.
258 // TODO: Treat the direction of doing sum-check more robustly.
259 let mut rand_reversed = rand.clone();
260 rand_reversed.reverse();
261 let eq_evals = EqPolynomial::new(rand_reversed.clone()).evaluations();
262 let mut poly_x = MultiLinear::from_values(&eq_evals);
263 assert_eq!(poly_x.len(), len);
264
265 let num_rounds = poly_x.len().ilog2() as usize;
266
267 // 1. A is a polynomial containing the evaluations `p_1`.
268 // 2. B is a polynomial containing the evaluations `p_0`.
269 // 3. C is a polynomial containing the evaluations `q_1`.
270 // 4. D is a polynomial containing the evaluations `q_0`.
271 let poly_a: &mut MultiLinear<E>;
272 let poly_b: &mut MultiLinear<E>;
273 let poly_c: &mut MultiLinear<E>;
274 let poly_d: &mut MultiLinear<E>;
275 poly_a = &mut circuit.p_1_vec[layer_id];
276 poly_b = &mut circuit.p_0_vec[layer_id];
277 poly_c = &mut circuit.q_1_vec[layer_id];
278 poly_d = &mut circuit.q_0_vec[layer_id];
279
280 let poly_vec_par = (poly_a, poly_b, poly_c, poly_d, &mut poly_x);
281
282 // The (non-linear) polynomial combining the multilinear polynomials
283 let comb_func = |a: &E, b: &E, c: &E, d: &E, x: &E, rho: &E| -> E {
284 (*a * *d + *b * *c + *rho * *c * *d) * *x
285 };
286
287 // Run the sumcheck protocol
288 let (proof, rand_sumcheck, claims_sum) = sum_check_prover_gkr_before_last::<E, _, _>(
289 claim,
290 num_rounds,
291 poly_vec_par,
292 comb_func,
293 transcript,
294 );
295
296 let (claims_sum_p1, claims_sum_p0, claims_sum_q1, claims_sum_q0, _claims_eq) =
297 claims_sum;
298
299 let data = vec![claims_sum_p1, claims_sum_p0, claims_sum_q1, claims_sum_q0];
300 transcript.reseed(H::hash_elements(&data));
301
302 // Produce a random challenge to condense claims into a single claim
303 let r_layer = transcript.draw().unwrap();
304
305 claim = (
306 claims_sum_p1 + r_layer * (claims_sum_p0 - claims_sum_p1),
307 claims_sum_q1 + r_layer * (claims_sum_q0 - claims_sum_q1),
308 );
309
310 // Collect the randomness used for the current layer in order to construct the random
311 // point where the input multilinear polynomials were evaluated.
312 let mut ext = rand_sumcheck;
313 ext.push(r_layer);
314 all_rand.push(rand);
315 rand = ext;
316
317 proof_layers.push(LayerProof {
318 proof,
319 claims_sum_p1,
320 claims_sum_p0,
321 claims_sum_q1,
322 claims_sum_q0,
323 });
324 }
325
326 (CircuitProof { proof: proof_layers }, rand, all_rand)
327 }
328
329 pub fn prove_virtual_bus<
330 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
331 H: ElementHasher<BaseField = BaseElement>,
332 >(
333 composition_polys: Vec<Vec<Arc<dyn CompositionPolynomial<E>>>>,
334 mls: &mut Vec<MultiLinear<E>>,
335 transcript: &mut C,
336 ) -> (Vec<E>, Self, super::sumcheck::FullProof<E>) {
337 let num_evaluations = 1 << mls[0].num_variables();
338
339 // I) Evaluate the numerators and denominators over the boolean hyper-cube
340 let mut num_den: Vec<Vec<E>> = vec![vec![]; 4];
341 for i in 0..num_evaluations {
342 for j in 0..4 {
343 let query: Vec<E> = mls.iter().map(|ml| ml[i]).collect();
344
345 composition_polys[j].iter().for_each(|c| {
346 let evaluation = c.as_ref().evaluate(&query);
347 num_den[j].push(evaluation);
348 });
349 }
350 }
351
352 // II) Evaluate the GKR fractional sum circuit
353 let input: Vec<MultiLinear<E>> =
354 (0..4).map(|i| MultiLinear::from_values(&num_den[i])).collect();
355 let mut circuit = FractionalSumCircuit::new_(&input);
356
357 // III) Run the GKR prover for all layers except the last one
358 let (gkr_proofs, GkrClaim { evaluation_point, claimed_evaluation }) =
359 CircuitProof::prove_before_final(&mut circuit, transcript);
360
361 // IV) Run the sum-check prover for the last GKR layer counting backwards i.e., first layer
362 // in the circuit.
363
364 // 1) Build the EQ polynomial (Lagrange kernel) at the randomness sampled during the previous
365 // sum-check protocol run
366 let mut rand_reversed = evaluation_point.clone();
367 rand_reversed.reverse();
368 let eq_evals = EqPolynomial::new(rand_reversed.clone()).evaluations();
369 let poly_x = MultiLinear::from_values(&eq_evals);
370
371 // 2) Add the Lagrange kernel to the list of MLs
372 mls.push(poly_x);
373
374 // 3) Absorb the final sum-check claims and generate randomness for 2-to-1 sum-check reduction
375 let data = vec![claimed_evaluation.0, claimed_evaluation.1];
376 transcript.reseed(H::hash_elements(&data));
377 // Squeeze challenge to reduce two sumchecks to one
378 let r_sum_check = transcript.draw().unwrap();
379 let reduced_claim = claimed_evaluation.0 + claimed_evaluation.1 * r_sum_check;
380
381 // 4) Create the composed ML representing the numerators and denominators of the topmost GKR layer
382 let gkr_final_composed_ml = gkr_composition_from_composition_polys(
383 &composition_polys,
384 r_sum_check,
385 1 << mls[0].num_variables,
386 );
387 let composed_ml =
388 ComposedMultiLinears::new(Arc::new(gkr_final_composed_ml.clone()), mls.to_vec());
389
390 // 5) Create the composed ML oracle. This will be used for verifying the FinalEvaluationClaim downstream
391 // TODO: This should be an input to the current function.
392 // TODO: Make MultiLinearOracle a variant in an enum so that it is possible to capture other types of oracles.
393 // For example, shifts of polynomials, Lagrange kernels at a random point or periodic (transparent) polynomials.
394 let left_num_oracle = MultiLinearOracle { id: 0 };
395 let right_num_oracle = MultiLinearOracle { id: 1 };
396 let left_denom_oracle = MultiLinearOracle { id: 2 };
397 let right_denom_oracle = MultiLinearOracle { id: 3 };
398 let eq_oracle = MultiLinearOracle { id: 4 };
399 let composed_ml_oracle = ComposedMultiLinearsOracle {
400 composer: (Arc::new(gkr_final_composed_ml.clone())),
401 multi_linears: vec![
402 eq_oracle,
403 left_num_oracle,
404 right_num_oracle,
405 left_denom_oracle,
406 right_denom_oracle,
407 ],
408 };
409
410 // 6) Create the claim for the final sum-check protocol.
411 let claim = Claim {
412 sum_value: reduced_claim,
413 polynomial: composed_ml_oracle.clone(),
414 };
415
416 // 7) Create the witness for the sum-check claim.
417 let witness = Witness { polynomial: composed_ml };
418 let output = sum_check_prove(&claim, composed_ml_oracle, witness, transcript);
419
420 // 8) Create the claimed output of the circuit.
421 let circuit_outputs = vec![
422 circuit.p_1_vec.last().unwrap()[0],
423 circuit.p_0_vec.last().unwrap()[0],
424 circuit.q_1_vec.last().unwrap()[0],
425 circuit.q_0_vec.last().unwrap()[0],
426 ];
427
428 // 9) Return:
429 // 1. The claimed circuit outputs.
430 // 2. GKR proofs of all circuit layers except the initial layer.
431 // 3. Output of the final sum-check protocol.
432 (circuit_outputs, gkr_proofs, output)
433 }
434
435 pub fn prove_before_final<
436 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
437 H: ElementHasher<BaseField = BaseElement>,
438 >(
439 sum_circuits: &mut FractionalSumCircuit<E>,
440 transcript: &mut C,
441 ) -> (Self, GkrClaim<E>) {
442 let mut proof_layers: Vec<LayerProof<E>> = Vec::new();
443 let num_layers = sum_circuits.p_0_vec.len();
444
445 let data = vec![
446 sum_circuits.p_1_vec[num_layers - 1][0],
447 sum_circuits.p_0_vec[num_layers - 1][0],
448 sum_circuits.q_1_vec[num_layers - 1][0],
449 sum_circuits.q_0_vec[num_layers - 1][0],
450 ];
451 transcript.reseed(H::hash_elements(&data));
452
453 // Challenge to reduce p1, p0, q1, q0 to pr, qr
454 let r_cord = transcript.draw().unwrap();
455
456 // Compute the (2-to-1 folded) claim
457 let mut claims_to_verify = sum_circuits.evaluate(r_cord);
458 let mut all_rand = Vec::new();
459
460 let mut rand = Vec::new();
461 rand.push(r_cord);
462 for layer_id in (1..num_layers - 1).rev() {
463 let len = sum_circuits.p_0_vec[layer_id].len();
464
465 // Construct the Lagrange kernel evaluated at previous GKR round randomness.
466 // TODO: Treat the direction of doing sum-check more robustly.
467 let mut rand_reversed = rand.clone();
468 rand_reversed.reverse();
469 let eq_evals = EqPolynomial::new(rand_reversed.clone()).evaluations();
470 let mut poly_x = MultiLinear::from_values(&eq_evals);
471 assert_eq!(poly_x.len(), len);
472
473 let num_rounds = poly_x.len().ilog2() as usize;
474
475 // 1. A is a polynomial containing the evaluations `p_1`.
476 // 2. B is a polynomial containing the evaluations `p_0`.
477 // 3. C is a polynomial containing the evaluations `q_1`.
478 // 4. D is a polynomial containing the evaluations `q_0`.
479 let poly_a: &mut MultiLinear<E>;
480 let poly_b: &mut MultiLinear<E>;
481 let poly_c: &mut MultiLinear<E>;
482 let poly_d: &mut MultiLinear<E>;
483 poly_a = &mut sum_circuits.p_1_vec[layer_id];
484 poly_b = &mut sum_circuits.p_0_vec[layer_id];
485 poly_c = &mut sum_circuits.q_1_vec[layer_id];
486 poly_d = &mut sum_circuits.q_0_vec[layer_id];
487
488 let poly_vec = (poly_a, poly_b, poly_c, poly_d, &mut poly_x);
489
490 let claim = claims_to_verify;
491
492 // The (non-linear) polynomial combining the multilinear polynomials
493 let comb_func = |a: &E, b: &E, c: &E, d: &E, x: &E, rho: &E| -> E {
494 (*a * *d + *b * *c + *rho * *c * *d) * *x
495 };
496
497 // Run the sumcheck protocol
498 let (proof, rand_sumcheck, claims_sum) = sum_check_prover_gkr_before_last::<E, _, _>(
499 claim, num_rounds, poly_vec, comb_func, transcript,
500 );
501
502 let (claims_sum_p1, claims_sum_p0, claims_sum_q1, claims_sum_q0, _claims_eq) =
503 claims_sum;
504
505 let data = vec![claims_sum_p1, claims_sum_p0, claims_sum_q1, claims_sum_q0];
506 transcript.reseed(H::hash_elements(&data));
507
508 // Produce a random challenge to condense claims into a single claim
509 let r_layer = transcript.draw().unwrap();
510
511 claims_to_verify = (
512 claims_sum_p1 + r_layer * (claims_sum_p0 - claims_sum_p1),
513 claims_sum_q1 + r_layer * (claims_sum_q0 - claims_sum_q1),
514 );
515
516 // Collect the randomness used for the current layer in order to construct the random
517 // point where the input multilinear polynomials were evaluated.
518 let mut ext = rand_sumcheck;
519 ext.push(r_layer);
520 all_rand.push(rand);
521 rand = ext;
522
523 proof_layers.push(LayerProof {
524 proof,
525 claims_sum_p1,
526 claims_sum_p0,
527 claims_sum_q1,
528 claims_sum_q0,
529 });
530 }
531 let gkr_claim = GkrClaim {
532 evaluation_point: rand.clone(),
533 claimed_evaluation: claims_to_verify,
534 };
535
536 (CircuitProof { proof: proof_layers }, gkr_claim)
537 }
538
539 pub fn verify<
540 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
541 H: ElementHasher<BaseField = BaseElement>,
542 >(
543 &self,
544 claims_sum_vec: &[E],
545 transcript: &mut C,
546 ) -> ((E, E), Vec<E>) {
547 let num_layers = self.proof.len() as usize - 1;
548 let mut rand: Vec<E> = Vec::new();
549
550 let data = claims_sum_vec;
551 transcript.reseed(H::hash_elements(&data));
552
553 let r_cord = transcript.draw().unwrap();
554
555 let p_poly_coef = vec![claims_sum_vec[0], claims_sum_vec[1]];
556 let q_poly_coef = vec![claims_sum_vec[2], claims_sum_vec[3]];
557
558 let p_poly = MultiLinear::new(p_poly_coef);
559 let q_poly = MultiLinear::new(q_poly_coef);
560 let p_eval = p_poly.evaluate(&[r_cord]);
561 let q_eval = q_poly.evaluate(&[r_cord]);
562
563 let mut reduced_claim = (p_eval, q_eval);
564
565 rand.push(r_cord);
566 for (num_rounds, i) in (0..num_layers).enumerate() {
567 let ((claim_last, rand_sumcheck), r_two_sumchecks) = self.proof[i]
568 .verify_sum_check_before_last::<_, _>(reduced_claim, num_rounds + 1, transcript);
569
570 let claims_sum_p1 = &self.proof[i].claims_sum_p1;
571 let claims_sum_p0 = &self.proof[i].claims_sum_p0;
572 let claims_sum_q1 = &self.proof[i].claims_sum_q1;
573 let claims_sum_q0 = &self.proof[i].claims_sum_q0;
574
575 let data = vec![
576 claims_sum_p1.clone(),
577 claims_sum_p0.clone(),
578 claims_sum_q1.clone(),
579 claims_sum_q0.clone(),
580 ];
581 transcript.reseed(H::hash_elements(&data));
582
583 assert_eq!(rand.len(), rand_sumcheck.len());
584
585 let eq: E = (0..rand.len())
586 .map(|i| {
587 rand[i] * rand_sumcheck[i] + (E::ONE - rand[i]) * (E::ONE - rand_sumcheck[i])
588 })
589 .fold(E::ONE, |acc, term| acc * term);
590
591 let claim_expected: E = (*claims_sum_p1 * *claims_sum_q0
592 + *claims_sum_p0 * *claims_sum_q1
593 + r_two_sumchecks * *claims_sum_q1 * *claims_sum_q0)
594 * eq;
595
596 assert_eq!(claim_expected, claim_last);
597
598 // Produce a random challenge to condense claims into a single claim
599 let r_layer = transcript.draw().unwrap();
600
601 reduced_claim = (
602 *claims_sum_p1 + r_layer * (*claims_sum_p0 - *claims_sum_p1),
603 *claims_sum_q1 + r_layer * (*claims_sum_q0 - *claims_sum_q1),
604 );
605
606 // Collect the randomness' used for the current layer in order to construct the random
607 // point where the input multilinear polynomials were evaluated.
608 let mut ext = rand_sumcheck;
609 ext.push(r_layer);
610 rand = ext;
611 }
612 (reduced_claim, rand)
613 }
614
615 pub fn verify_virtual_bus<
616 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
617 H: ElementHasher<BaseField = BaseElement>,
618 >(
619 &self,
620 composition_polys: Vec<Vec<Arc<dyn CompositionPolynomial<E>>>>,
621 final_layer_proof: super::sumcheck::FullProof<E>,
622 claims_sum_vec: &[E],
623 transcript: &mut C,
624 ) -> (FinalEvaluationClaim<E>, Vec<E>) {
625 let num_layers = self.proof.len() as usize;
626 let mut rand: Vec<E> = Vec::new();
627
628 // Check that a/b + d/e is equal to 0
629 assert_ne!(claims_sum_vec[2], E::ZERO);
630 assert_ne!(claims_sum_vec[3], E::ZERO);
631 assert_eq!(
632 claims_sum_vec[0] * claims_sum_vec[3] + claims_sum_vec[1] * claims_sum_vec[2],
633 E::ZERO
634 );
635
636 let data = claims_sum_vec;
637 transcript.reseed(H::hash_elements(&data));
638
639 let r_cord = transcript.draw().unwrap();
640
641 let p_poly_coef = vec![claims_sum_vec[0], claims_sum_vec[1]];
642 let q_poly_coef = vec![claims_sum_vec[2], claims_sum_vec[3]];
643
644 let p_poly = MultiLinear::new(p_poly_coef);
645 let q_poly = MultiLinear::new(q_poly_coef);
646 let p_eval = p_poly.evaluate(&[r_cord]);
647 let q_eval = q_poly.evaluate(&[r_cord]);
648
649 let mut reduced_claim = (p_eval, q_eval);
650
651 // I) Verify all GKR layers but for the last one counting backwards.
652 rand.push(r_cord);
653 for (num_rounds, i) in (0..num_layers).enumerate() {
654 let ((claim_last, rand_sumcheck), r_two_sumchecks) = self.proof[i]
655 .verify_sum_check_before_last::<_, _>(reduced_claim, num_rounds + 1, transcript);
656
657 let claims_sum_p1 = &self.proof[i].claims_sum_p1;
658 let claims_sum_p0 = &self.proof[i].claims_sum_p0;
659 let claims_sum_q1 = &self.proof[i].claims_sum_q1;
660 let claims_sum_q0 = &self.proof[i].claims_sum_q0;
661
662 let data = vec![
663 claims_sum_p1.clone(),
664 claims_sum_p0.clone(),
665 claims_sum_q1.clone(),
666 claims_sum_q0.clone(),
667 ];
668 transcript.reseed(H::hash_elements(&data));
669
670 assert_eq!(rand.len(), rand_sumcheck.len());
671
672 let eq: E = (0..rand.len())
673 .map(|i| {
674 rand[i] * rand_sumcheck[i] + (E::ONE - rand[i]) * (E::ONE - rand_sumcheck[i])
675 })
676 .fold(E::ONE, |acc, term| acc * term);
677
678 let claim_expected: E = (*claims_sum_p1 * *claims_sum_q0
679 + *claims_sum_p0 * *claims_sum_q1
680 + r_two_sumchecks * *claims_sum_q1 * *claims_sum_q0)
681 * eq;
682
683 assert_eq!(claim_expected, claim_last);
684
685 // Produce a random challenge to condense claims into a single claim
686 let r_layer = transcript.draw().unwrap();
687
688 reduced_claim = (
689 *claims_sum_p1 + r_layer * (*claims_sum_p0 - *claims_sum_p1),
690 *claims_sum_q1 + r_layer * (*claims_sum_q0 - *claims_sum_q1),
691 );
692
693 let mut ext = rand_sumcheck;
694 ext.push(r_layer);
695 rand = ext;
696 }
697
698 // II) Verify the final GKR layer counting backwards.
699
700 // Absorb the claims
701 let data = vec![reduced_claim.0, reduced_claim.1];
702 transcript.reseed(H::hash_elements(&data));
703
704 // Squeeze challenge to reduce two sumchecks to one
705 let r_sum_check = transcript.draw().unwrap();
706 let reduced_claim = reduced_claim.0 + reduced_claim.1 * r_sum_check;
707
708 let gkr_final_composed_ml = gkr_composition_from_composition_polys(
709 &composition_polys,
710 r_sum_check,
711 1 << (num_layers + 1),
712 );
713
714 // TODO: refactor
715 let composed_ml_oracle = {
716 let left_num_oracle = MultiLinearOracle { id: 0 };
717 let right_num_oracle = MultiLinearOracle { id: 1 };
718 let left_denom_oracle = MultiLinearOracle { id: 2 };
719 let right_denom_oracle = MultiLinearOracle { id: 3 };
720 let eq_oracle = MultiLinearOracle { id: 4 };
721 ComposedMultiLinearsOracle {
722 composer: (Arc::new(gkr_final_composed_ml.clone())),
723 multi_linears: vec![
724 eq_oracle,
725 left_num_oracle,
726 right_num_oracle,
727 left_denom_oracle,
728 right_denom_oracle,
729 ],
730 }
731 };
732
733 let claim = Claim {
734 sum_value: reduced_claim,
735 polynomial: composed_ml_oracle.clone(),
736 };
737
738 let final_eval_claim = sum_check_verify(&claim, final_layer_proof, transcript);
739
740 (final_eval_claim, rand)
741 }
742}
743
744fn sum_check_prover_gkr_before_last<
745 E: FieldElement<BaseField = BaseElement>,
746 C: RandomCoin<Hasher = H, BaseField = BaseElement>,
747 H: ElementHasher<BaseField = BaseElement>,
748>(
749 claim: (E, E),
750 num_rounds: usize,
751 ml_polys: (
752 &mut MultiLinear<E>,
753 &mut MultiLinear<E>,
754 &mut MultiLinear<E>,
755 &mut MultiLinear<E>,
756 &mut MultiLinear<E>,
757 ),
758 comb_func: impl Fn(&E, &E, &E, &E, &E, &E) -> E,
759 transcript: &mut C,
760) -> (SumcheckInstanceProof<E>, Vec<E>, (E, E, E, E, E)) {
761 // Absorb the claims
762 let data = vec![claim.0, claim.1];
763 transcript.reseed(H::hash_elements(&data));
764
765 // Squeeze challenge to reduce two sumchecks to one
766 let r_sum_check = transcript.draw().unwrap();
767
768 let (poly_a, poly_b, poly_c, poly_d, poly_x) = ml_polys;
769
770 let mut e = claim.0 + claim.1 * r_sum_check;
771
772 let mut r: Vec<E> = Vec::new();
773 let mut round_proofs: Vec<SumCheckRoundProof<E>> = Vec::new();
774
775 for _j in 0..num_rounds {
776 let evals: (E, E, E) = {
777 let mut eval_point_0 = E::ZERO;
778 let mut eval_point_2 = E::ZERO;
779 let mut eval_point_3 = E::ZERO;
780
781 let len = poly_a.len() / 2;
782 for i in 0..len {
783 // The interpolation formula for a linear function is:
784 // z * A(x) + (1 - z) * A (y)
785 // z * A(1) + (1 - z) * A(0)
786
787 // eval at z = 0: A(1)
788 eval_point_0 += comb_func(
789 &poly_a[i << 1],
790 &poly_b[i << 1],
791 &poly_c[i << 1],
792 &poly_d[i << 1],
793 &poly_x[i << 1],
794 &r_sum_check,
795 );
796
797 let poly_a_u = poly_a[(i << 1) + 1];
798 let poly_a_v = poly_a[i << 1];
799 let poly_b_u = poly_b[(i << 1) + 1];
800 let poly_b_v = poly_b[i << 1];
801 let poly_c_u = poly_c[(i << 1) + 1];
802 let poly_c_v = poly_c[i << 1];
803 let poly_d_u = poly_d[(i << 1) + 1];
804 let poly_d_v = poly_d[i << 1];
805 let poly_x_u = poly_x[(i << 1) + 1];
806 let poly_x_v = poly_x[i << 1];
807
808 // eval at z = 2: 2 * A(1) - A(0)
809 let poly_a_extrapolated_point = poly_a_u + poly_a_u - poly_a_v;
810 let poly_b_extrapolated_point = poly_b_u + poly_b_u - poly_b_v;
811 let poly_c_extrapolated_point = poly_c_u + poly_c_u - poly_c_v;
812 let poly_d_extrapolated_point = poly_d_u + poly_d_u - poly_d_v;
813 let poly_x_extrapolated_point = poly_x_u + poly_x_u - poly_x_v;
814 eval_point_2 += comb_func(
815 &poly_a_extrapolated_point,
816 &poly_b_extrapolated_point,
817 &poly_c_extrapolated_point,
818 &poly_d_extrapolated_point,
819 &poly_x_extrapolated_point,
820 &r_sum_check,
821 );
822
823 // eval at z = 3: 3 * A(1) - 2 * A(0) = 2 * A(1) - A(0) + A(1) - A(0)
824 // hence we can compute the evaluation at z + 1 from that of z for z > 1
825 let poly_a_extrapolated_point = poly_a_extrapolated_point + poly_a_u - poly_a_v;
826 let poly_b_extrapolated_point = poly_b_extrapolated_point + poly_b_u - poly_b_v;
827 let poly_c_extrapolated_point = poly_c_extrapolated_point + poly_c_u - poly_c_v;
828 let poly_d_extrapolated_point = poly_d_extrapolated_point + poly_d_u - poly_d_v;
829 let poly_x_extrapolated_point = poly_x_extrapolated_point + poly_x_u - poly_x_v;
830
831 eval_point_3 += comb_func(
832 &poly_a_extrapolated_point,
833 &poly_b_extrapolated_point,
834 &poly_c_extrapolated_point,
835 &poly_d_extrapolated_point,
836 &poly_x_extrapolated_point,
837 &r_sum_check,
838 );
839 }
840
841 (eval_point_0, eval_point_2, eval_point_3)
842 };
843
844 let eval_0 = evals.0;
845 let eval_2 = evals.1;
846 let eval_3 = evals.2;
847
848 let evals = vec![e - eval_0, eval_2, eval_3];
849 let compressed_poly = SumCheckRoundProof { poly_evals: evals };
850
851 // append the prover's message to the transcript
852 transcript.reseed(H::hash_elements(&compressed_poly.poly_evals));
853
854 // derive the verifier's challenge for the next round
855 let r_j = transcript.draw().unwrap();
856 r.push(r_j);
857
858 poly_a.bind_assign(r_j);
859 poly_b.bind_assign(r_j);
860 poly_c.bind_assign(r_j);
861 poly_d.bind_assign(r_j);
862
863 poly_x.bind_assign(r_j);
864
865 e = compressed_poly.evaluate(e, r_j);
866
867 round_proofs.push(compressed_poly);
868 }
869 let claims_sum = (poly_a[0], poly_b[0], poly_c[0], poly_d[0], poly_x[0]);
870
871 (SumcheckInstanceProof { round_proofs }, r, claims_sum)
872}
873
874#[cfg(test)]
875mod sum_circuit_tests {
876 use crate::rand::RpoRandomCoin;
877
878 use super::*;
879 use rand::Rng;
880 use rand_utils::rand_value;
881 use BaseElement as Felt;
882
883 /// The following tests the fractional sum circuit to check that \sum_{i = 0}^{log(m)-1} m / 2^{i} = 2 * (m - 1)
884 #[test]
885 fn sum_circuit_example() {
886 let n = 4; // n := log(m)
887 let mut inp: Vec<Felt> = (0..n).map(|_| Felt::from(1_u64 << n)).collect();
888 let inp_: Vec<Felt> = (0..n).map(|i| Felt::from(1_u64 << i)).collect();
889 inp.extend(inp_.iter());
890
891 let summation = MultiLinear::new(inp);
892
893 let expected_output = Felt::from(2 * ((1_u64 << n) - 1));
894
895 let mut circuit = FractionalSumCircuit::new(&summation);
896
897 let seed = [BaseElement::ZERO; 4];
898 let mut transcript = RpoRandomCoin::new(seed.into());
899
900 let (proof, _evals, _) = CircuitProof::prove(&mut circuit, &mut transcript);
901
902 let (p1, q1) = circuit.evaluate(Felt::from(1_u8));
903 let (p0, q0) = circuit.evaluate(Felt::from(0_u8));
904 assert_eq!(expected_output, (p1 * q0 + q1 * p0) / (q1 * q0));
905
906 let seed = [BaseElement::ZERO; 4];
907 let mut transcript = RpoRandomCoin::new(seed.into());
908 let claims = vec![p0, p1, q0, q1];
909 proof.verify(&claims, &mut transcript);
910 }
911
912 // Test the fractional sum GKR in the context of LogUp.
913 #[test]
914 fn log_up() {
915 use rand::distributions::Slice;
916
917 let n: usize = 16;
918 let num_w: usize = 31; // This should be of the form 2^k - 1
919 let rng = rand::thread_rng();
920
921 let t_table: Vec<u32> = (0..(1 << n)).collect();
922 let mut m_table: Vec<u32> = (0..(1 << n)).map(|_| 0).collect();
923
924 let t_table_slice = Slice::new(&t_table).unwrap();
925
926 // Construct the witness columns. Uses sampling with replacement in order to have multiplicities
927 // different from 1.
928 let mut w_tables = Vec::new();
929 for _ in 0..num_w {
930 let wi_table: Vec<u32> =
931 rng.clone().sample_iter(&t_table_slice).cloned().take(1 << n).collect();
932
933 // Construct the multiplicities
934 wi_table.iter().for_each(|w| {
935 m_table[*w as usize] += 1;
936 });
937 w_tables.push(wi_table)
938 }
939
940 // The numerators
941 let mut p: Vec<Felt> = m_table.iter().map(|m| Felt::from(*m as u32)).collect();
942 p.extend((0..(num_w * (1 << n))).map(|_| Felt::from(1_u32)).collect::<Vec<Felt>>());
943
944 // Sample the challenge alpha to construct the denominators.
945 let alpha = rand_value();
946
947 // Construct the denominators
948 let mut q: Vec<Felt> = t_table.iter().map(|t| Felt::from(*t) - alpha).collect();
949 for w_table in w_tables {
950 q.extend(w_table.iter().map(|w| alpha - Felt::from(*w)).collect::<Vec<Felt>>());
951 }
952
953 // Build the input to the fractional sum GKR circuit
954 p.extend(q);
955 let input = p;
956
957 let summation = MultiLinear::new(input);
958
959 let expected_output = Felt::from(0_u8);
960
961 let mut circuit = FractionalSumCircuit::new(&summation);
962
963 let seed = [BaseElement::ZERO; 4];
964 let mut transcript = RpoRandomCoin::new(seed.into());
965
966 let (proof, _evals, _) = CircuitProof::prove(&mut circuit, &mut transcript);
967
968 let (p1, q1) = circuit.evaluate(Felt::from(1_u8));
969 let (p0, q0) = circuit.evaluate(Felt::from(0_u8));
970 assert_eq!(expected_output, (p1 * q0 + q1 * p0) / (q1 * q0)); // This check should be part of verification
971
972 let seed = [BaseElement::ZERO; 4];
973 let mut transcript = RpoRandomCoin::new(seed.into());
974 let claims = vec![p0, p1, q0, q1];
975 proof.verify(&claims, &mut transcript);
976 }
977}