Skip to content

Commit 40b7a86

Browse files
TomWambsgansTomWambsgans
committed
more elegant Grand Product Consistency check
1 parent 7a85172 commit 40b7a86

File tree

7 files changed

+149
-83
lines changed

7 files changed

+149
-83
lines changed

‎crates/lean_prover/src/common.rs‎

Lines changed: 36 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -146,10 +146,7 @@ pub fn add_memory_statements_for_dot_product_precompile(
146146

147147
pub struct PrecompileFootprint {
148148
pub global_challenge: EF,
149-
pub p16_powers: [EF; 6],
150-
pub p24_powers: [EF; 5],
151-
pub dot_product_powers: [EF; 6],
152-
pub multilinear_eval_powers: [EF; 6],
149+
pub fingerprint_challenge_powers: [EF; 5],
153150
}
154151

155152
const PRECOMP_INDEX_OPERAND_A: usize = 0;
@@ -203,28 +200,37 @@ impl PrecompileFootprint {
203200
let nu_c = (ResultF::ONE - point[PRECOMP_INDEX_FLAG_C]) * point[PRECOMP_INDEX_MEM_VALUE_C]
204201
+ point[PRECOMP_INDEX_FLAG_C] * point[PRECOMP_INDEX_FP];
205202

206-
(nu_a * self.p16_powers[2]
207-
+ nu_b * self.p16_powers[3]
208-
+ nu_c * self.p16_powers[4]
209-
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.p16_powers[5])
210-
+ self.p16_powers[1])
203+
(nu_a * self.fingerprint_challenge_powers[1]
204+
+ nu_b * self.fingerprint_challenge_powers[2]
205+
+ nu_c * self.fingerprint_challenge_powers[3]
206+
+ mul_point_f_and_ef(
207+
point[PRECOMP_INDEX_AUX],
208+
self.fingerprint_challenge_powers[4],
209+
)
210+
+ ResultF::from_usize(TABLE_INDEX_POSEIDONS_16))
211211
* point[PRECOMP_INDEX_POSEIDON_16]
212-
+ (nu_a * self.p24_powers[2]
213-
+ nu_b * self.p24_powers[3]
214-
+ nu_c * self.p24_powers[4]
215-
+ self.p24_powers[1])
212+
+ (nu_a * self.fingerprint_challenge_powers[1]
213+
+ nu_b * self.fingerprint_challenge_powers[2]
214+
+ nu_c * self.fingerprint_challenge_powers[3]
215+
+ ResultF::from_usize(TABLE_INDEX_POSEIDONS_24))
216216
* point[PRECOMP_INDEX_POSEIDON_24]
217-
+ (nu_a * self.dot_product_powers[2]
218-
+ nu_b * self.dot_product_powers[3]
219-
+ nu_c * self.dot_product_powers[4]
220-
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.dot_product_powers[5])
221-
+ self.dot_product_powers[1])
217+
+ (nu_a * self.fingerprint_challenge_powers[1]
218+
+ nu_b * self.fingerprint_challenge_powers[2]
219+
+ nu_c * self.fingerprint_challenge_powers[3]
220+
+ mul_point_f_and_ef(
221+
point[PRECOMP_INDEX_AUX],
222+
self.fingerprint_challenge_powers[4],
223+
)
224+
+ ResultF::from_usize(TABLE_INDEX_DOT_PRODUCTS))
222225
* point[PRECOMP_INDEX_DOT_PRODUCT]
223-
+ (nu_a * self.multilinear_eval_powers[2]
224-
+ nu_b * self.multilinear_eval_powers[3]
225-
+ nu_c * self.multilinear_eval_powers[4]
226-
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.multilinear_eval_powers[5])
227-
+ self.multilinear_eval_powers[1])
226+
+ (nu_a * self.fingerprint_challenge_powers[1]
227+
+ nu_b * self.fingerprint_challenge_powers[2]
228+
+ nu_c * self.fingerprint_challenge_powers[3]
229+
+ mul_point_f_and_ef(
230+
point[PRECOMP_INDEX_AUX],
231+
self.fingerprint_challenge_powers[4],
232+
)
233+
+ ResultF::from_usize(TABLE_INDEX_MULTILINEAR_EVAL))
228234
* point[PRECOMP_INDEX_MULTILINEAR_EVAL]
229235
+ self.global_challenge
230236
}
@@ -258,7 +264,7 @@ impl SumcheckComputationPacked<EF> for PrecompileFootprint {
258264

259265
pub struct DotProductFootprint {
260266
pub global_challenge: EF,
261-
pub dot_product_challenge: [EF; 6],
267+
pub fingerprint_challenge_powers: [EF; 5],
262268
}
263269

264270
impl DotProductFootprint {
@@ -270,12 +276,12 @@ impl DotProductFootprint {
270276
point: &[PointF],
271277
mul_point_f_and_ef: impl Fn(PointF, EF) -> ResultF,
272278
) -> ResultF {
273-
(mul_point_f_and_ef(point[2], self.dot_product_challenge[2])
274-
+ mul_point_f_and_ef(point[3], self.dot_product_challenge[3])
275-
+ mul_point_f_and_ef(point[4], self.dot_product_challenge[4])
276-
+ mul_point_f_and_ef(point[1], self.dot_product_challenge[5]))
277-
* point[0]
278-
+ self.dot_product_challenge[1]
279+
ResultF::from_usize(TABLE_INDEX_DOT_PRODUCTS)
280+
+ (mul_point_f_and_ef(point[2], self.fingerprint_challenge_powers[1])
281+
+ mul_point_f_and_ef(point[3], self.fingerprint_challenge_powers[2])
282+
+ mul_point_f_and_ef(point[4], self.fingerprint_challenge_powers[3])
283+
+ mul_point_f_and_ef(point[1], self.fingerprint_challenge_powers[4]))
284+
* point[0]
279285
+ self.global_challenge
280286
}
281287
}

‎crates/lean_prover/src/lib.rs‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,3 +25,8 @@ pub fn whir_config_builder() -> WhirConfigBuilder {
2525
starting_log_inv_rate: 1,
2626
}
2727
}
28+
29+
const TABLE_INDEX_POSEIDONS_16: usize = 1; // should be != 0
30+
const TABLE_INDEX_POSEIDONS_24: usize = 2;
31+
const TABLE_INDEX_DOT_PRODUCTS: usize = 3;
32+
const TABLE_INDEX_MULTILINEAR_EVAL: usize = 4;

‎crates/lean_prover/src/prove_execution.rs‎

Lines changed: 56 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -209,37 +209,44 @@ pub fn prove_execution(
209209

210210
// Grand Product for consistency with precompiles
211211
let grand_product_challenge_global = prover_state.sample();
212-
let grand_product_challenge_p16 = prover_state.sample();
213-
let grand_product_challenge_p24 = prover_state.sample();
214-
let grand_product_challenge_dot_product = prover_state.sample();
215-
let grand_product_challenge_vm_multilinear_eval = prover_state.sample();
212+
let fingerprint_challenge = prover_state.sample();
216213
let mut exec_column_for_grand_product = vec![grand_product_challenge_global; n_cycles];
217214
for pos_16 in &poseidons_16 {
218215
let Some(cycle) = pos_16.cycle else {
219216
break;
220217
};
221218
exec_column_for_grand_product[cycle] = grand_product_challenge_global
222-
+ finger_print(&pos_16.addresses_field_repr(), grand_product_challenge_p16);
219+
+ finger_print(
220+
TABLE_INDEX_POSEIDONS_16,
221+
&pos_16.addresses_field_repr(),
222+
fingerprint_challenge,
223+
);
223224
}
224225
for pos_24 in &poseidons_24 {
225226
let Some(cycle) = pos_24.cycle else {
226227
break;
227228
};
228229
exec_column_for_grand_product[cycle] = grand_product_challenge_global
229-
+ finger_print(&pos_24.addresses_field_repr(), grand_product_challenge_p24);
230+
+ finger_print(
231+
TABLE_INDEX_POSEIDONS_24,
232+
&pos_24.addresses_field_repr(),
233+
fingerprint_challenge,
234+
);
230235
}
231236
for dot_product in &dot_products {
232237
exec_column_for_grand_product[dot_product.cycle] = grand_product_challenge_global
233238
+ finger_print(
239+
TABLE_INDEX_DOT_PRODUCTS,
234240
&dot_product.addresses_and_len_field_repr(),
235-
grand_product_challenge_dot_product,
241+
fingerprint_challenge,
236242
);
237243
}
238244
for multilinear_eval in &vm_multilinear_evals {
239245
exec_column_for_grand_product[multilinear_eval.cycle] = grand_product_challenge_global
240246
+ finger_print(
247+
TABLE_INDEX_MULTILINEAR_EVAL,
241248
&multilinear_eval.addresses_and_n_vars_field_repr(),
242-
grand_product_challenge_vm_multilinear_eval,
249+
fingerprint_challenge,
243250
);
244251
}
245252

@@ -252,7 +259,11 @@ pub fn prove_execution(
252259
.par_iter()
253260
.map(|pos_16| {
254261
grand_product_challenge_global
255-
+ finger_print(&pos_16.addresses_field_repr(), grand_product_challenge_p16)
262+
+ finger_print(
263+
TABLE_INDEX_POSEIDONS_16,
264+
&pos_16.addresses_field_repr(),
265+
fingerprint_challenge,
266+
)
256267
})
257268
.collect::<Vec<_>>();
258269

@@ -265,7 +276,11 @@ pub fn prove_execution(
265276
.par_iter()
266277
.map(|pos_24| {
267278
grand_product_challenge_global
268-
+ finger_print(&pos_24.addresses_field_repr(), grand_product_challenge_p24)
279+
+ finger_print(
280+
TABLE_INDEX_POSEIDONS_24,
281+
&pos_24.addresses_field_repr(),
282+
fingerprint_challenge,
283+
)
269284
})
270285
.collect::<Vec<_>>();
271286

@@ -279,16 +294,17 @@ pub fn prove_execution(
279294
.map(|i| {
280295
grand_product_challenge_global
281296
+ if dot_product_columns[0][i].is_zero() {
282-
grand_product_challenge_dot_product
297+
EF::from_usize(TABLE_INDEX_DOT_PRODUCTS)
283298
} else {
284299
finger_print(
300+
TABLE_INDEX_DOT_PRODUCTS,
285301
&[
286302
dot_product_columns[2][i],
287303
dot_product_columns[3][i],
288304
dot_product_columns[4][i],
289305
dot_product_columns[1][i],
290306
],
291-
grand_product_challenge_dot_product,
307+
fingerprint_challenge,
292308
)
293309
}
294310
})
@@ -299,8 +315,9 @@ pub fn prove_execution(
299315
.map(|vm_multilinear_eval| {
300316
grand_product_challenge_global
301317
+ finger_print(
318+
TABLE_INDEX_MULTILINEAR_EVAL,
302319
&vm_multilinear_eval.addresses_and_n_vars_field_repr(),
303-
grand_product_challenge_vm_multilinear_eval,
320+
fingerprint_challenge,
304321
)
305322
})
306323
.product::<EF>();
@@ -320,23 +337,37 @@ pub fn prove_execution(
320337
);
321338
let corrected_prod_p16 = grand_product_p16_res
322339
/ (grand_product_challenge_global
323-
+ grand_product_challenge_p16
324-
+ grand_product_challenge_p16.exp_u64(4) * F::from_usize(POSEIDON_16_NULL_HASH_PTR)
325-
+ grand_product_challenge_p16.exp_u64(5) * F::ONE) // compression = 1 by default
326-
.exp_u64((n_poseidons_16.next_power_of_two() - n_poseidons_16) as u64);
340+
+ finger_print(
341+
TABLE_INDEX_POSEIDONS_16,
342+
&WitnessPoseidon16::default_addresses_field_repr(POSEIDON_16_NULL_HASH_PTR),
343+
fingerprint_challenge,
344+
))
345+
.exp_u64((n_poseidons_16.next_power_of_two() - n_poseidons_16) as u64);
327346

328347
let corrected_prod_p24 = grand_product_p24_res
329348
/ (grand_product_challenge_global
330-
+ grand_product_challenge_p24
331-
+ grand_product_challenge_p24.exp_u64(4) * F::from_usize(POSEIDON_24_NULL_HASH_PTR))
349+
+ finger_print(
350+
TABLE_INDEX_POSEIDONS_24,
351+
&WitnessPoseidon24::default_addresses_field_repr(POSEIDON_24_NULL_HASH_PTR),
352+
fingerprint_challenge,
353+
))
332354
.exp_u64((n_poseidons_24.next_power_of_two() - n_poseidons_24) as u64);
333355

334356
let corrected_dot_product = grand_product_dot_product_res
335357
/ ((grand_product_challenge_global
336-
+ grand_product_challenge_dot_product
337-
+ grand_product_challenge_dot_product.exp_u64(5))
358+
+ finger_print(
359+
TABLE_INDEX_DOT_PRODUCTS,
360+
&[F::ZERO, F::ZERO, F::ZERO, F::ONE],
361+
fingerprint_challenge,
362+
))
338363
.exp_u64(dot_product_padding_len as u64)
339-
* (grand_product_challenge_global + grand_product_challenge_dot_product).exp_u64(
364+
* (grand_product_challenge_global
365+
+ finger_print(
366+
TABLE_INDEX_DOT_PRODUCTS,
367+
&[F::ZERO, F::ZERO, F::ZERO, F::ZERO],
368+
fingerprint_challenge,
369+
))
370+
.exp_u64(
340371
((1 << log_n_rows_dot_product_table) - dot_product_padding_len - dot_products.len())
341372
as u64,
342373
));
@@ -402,7 +433,7 @@ pub fn prove_execution(
402433

403434
let dot_product_footprint_computation = DotProductFootprint {
404435
global_challenge: grand_product_challenge_global,
405-
dot_product_challenge: powers_const(grand_product_challenge_dot_product),
436+
fingerprint_challenge_powers: powers_const(fingerprint_challenge),
406437
};
407438

408439
let (
@@ -455,10 +486,7 @@ pub fn prove_execution(
455486

456487
let precompile_foot_print_computation = PrecompileFootprint {
457488
global_challenge: grand_product_challenge_global,
458-
p16_powers: powers_const(grand_product_challenge_p16),
459-
p24_powers: powers_const(grand_product_challenge_p24),
460-
dot_product_powers: powers_const(grand_product_challenge_dot_product),
461-
multilinear_eval_powers: powers_const(grand_product_challenge_vm_multilinear_eval),
489+
fingerprint_challenge_powers: powers_const(fingerprint_challenge),
462490
};
463491

464492
let (grand_product_exec_sumcheck_point, mut grand_product_exec_sumcheck_inner_evals, _) =
@@ -715,7 +743,7 @@ pub fn prove_execution(
715743

716744
assert!(
717745
padded_dot_product_indexes_spread.len() <= 1 << log_n_cycles,
718-
"TODO a more general commitment structure"
746+
"Currently the number of dot products must be < num_cycles / 32 (TODO relax this)"
719747
);
720748

721749
let unused_1 = evaluate_as_larger_multilinear_pol(

0 commit comments

Comments
 (0)