Skip to content

Commit e147c84

Browse files
committed
simplify grand product
1 parent e480793 commit e147c84

File tree

6 files changed

+177
-162
lines changed

6 files changed

+177
-162
lines changed

crates/lean_prover/src/common.rs

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -150,11 +150,11 @@ pub fn add_memory_statements_for_dot_product_precompile(
150150
}
151151

152152
pub struct PrecompileFootprint {
153-
pub grand_product_challenge_global: EF,
154-
pub grand_product_challenge_p16: [EF; 5],
155-
pub grand_product_challenge_p24: [EF; 5],
156-
pub grand_product_challenge_dot_product: [EF; 6],
157-
pub grand_product_challenge_vm_multilinear_eval: [EF; 6],
153+
pub global_challenge: EF,
154+
pub p16_powers: [EF; 5],
155+
pub p24_powers: [EF; 5],
156+
pub dot_product_powers: [EF; 6],
157+
pub multilinear_eval_powers: [EF; 6],
158158
}
159159

160160
impl<N: ExtensionField<PF<EF>>> SumcheckComputation<N, EF> for PrecompileFootprint
@@ -174,28 +174,28 @@ where
174174
let nu_c = (EF::ONE - point[COL_INDEX_FLAG_C]) * point[COL_INDEX_MEM_VALUE_C]
175175
+ point[COL_INDEX_FLAG_C] * point[COL_INDEX_FP];
176176

177-
self.grand_product_challenge_global
178-
+ (self.grand_product_challenge_p16[1]
179-
+ self.grand_product_challenge_p16[2] * nu_a
180-
+ self.grand_product_challenge_p16[3] * nu_b
181-
+ self.grand_product_challenge_p16[4] * nu_c)
177+
self.global_challenge
178+
+ (self.p16_powers[1]
179+
+ self.p16_powers[2] * nu_a
180+
+ self.p16_powers[3] * nu_b
181+
+ self.p16_powers[4] * nu_c)
182182
* point[COL_INDEX_POSEIDON_16]
183-
+ (self.grand_product_challenge_p24[1]
184-
+ self.grand_product_challenge_p24[2] * nu_a
185-
+ self.grand_product_challenge_p24[3] * nu_b
186-
+ self.grand_product_challenge_p24[4] * nu_c)
183+
+ (self.p24_powers[1]
184+
+ self.p24_powers[2] * nu_a
185+
+ self.p24_powers[3] * nu_b
186+
+ self.p24_powers[4] * nu_c)
187187
* point[COL_INDEX_POSEIDON_24]
188-
+ (self.grand_product_challenge_dot_product[1]
189-
+ self.grand_product_challenge_dot_product[2] * nu_a
190-
+ self.grand_product_challenge_dot_product[3] * nu_b
191-
+ self.grand_product_challenge_dot_product[4] * nu_c
192-
+ self.grand_product_challenge_dot_product[5] * point[COL_INDEX_AUX])
188+
+ (self.dot_product_powers[1]
189+
+ self.dot_product_powers[2] * nu_a
190+
+ self.dot_product_powers[3] * nu_b
191+
+ self.dot_product_powers[4] * nu_c
192+
+ self.dot_product_powers[5] * point[COL_INDEX_AUX])
193193
* point[COL_INDEX_DOT_PRODUCT]
194-
+ (self.grand_product_challenge_vm_multilinear_eval[1]
195-
+ self.grand_product_challenge_vm_multilinear_eval[2] * nu_a
196-
+ self.grand_product_challenge_vm_multilinear_eval[3] * nu_b
197-
+ self.grand_product_challenge_vm_multilinear_eval[4] * nu_c
198-
+ self.grand_product_challenge_vm_multilinear_eval[5] * point[COL_INDEX_AUX])
194+
+ (self.multilinear_eval_powers[1]
195+
+ self.multilinear_eval_powers[2] * nu_a
196+
+ self.multilinear_eval_powers[3] * nu_b
197+
+ self.multilinear_eval_powers[4] * nu_c
198+
+ self.multilinear_eval_powers[5] * point[COL_INDEX_AUX])
199199
* point[COL_INDEX_MULTILINEAR_EVAL]
200200
}
201201
}
@@ -215,8 +215,8 @@ impl SumcheckComputationPacked<EF> for PrecompileFootprint {
215215
}
216216

217217
pub struct DotProductFootprint {
218-
pub grand_product_challenge_global: EF,
219-
pub grand_product_challenge_dot_product: [EF; 6],
218+
pub global_challenge: EF,
219+
pub dot_product_challenge: [EF; 6],
220220
}
221221

222222
impl<N: ExtensionField<PF<EF>>> SumcheckComputation<N, EF> for DotProductFootprint
@@ -228,12 +228,12 @@ where
228228
}
229229

230230
fn eval(&self, point: &[N], _: &[EF]) -> EF {
231-
self.grand_product_challenge_global
232-
+ self.grand_product_challenge_dot_product[1]
233-
+ (self.grand_product_challenge_dot_product[2] * point[2]
234-
+ self.grand_product_challenge_dot_product[3] * point[3]
235-
+ self.grand_product_challenge_dot_product[4] * point[4]
236-
+ self.grand_product_challenge_dot_product[5] * point[1])
231+
self.global_challenge
232+
+ self.dot_product_challenge[1]
233+
+ (self.dot_product_challenge[2] * point[2]
234+
+ self.dot_product_challenge[3] * point[3]
235+
+ self.dot_product_challenge[4] * point[4]
236+
+ self.dot_product_challenge[5] * point[1])
237237
* point[0]
238238
}
239239
}

crates/lean_prover/src/prove_execution.rs

Lines changed: 56 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use lookup::prove_gkr_product;
66
use lookup::{compute_pushforward, prove_logup_star};
77
use p3_air::BaseAir;
88
use p3_field::ExtensionField;
9+
use p3_field::Field;
910
use p3_field::PrimeCharacteristicRing;
1011
use p3_util::{log2_ceil_usize, log2_strict_usize};
1112
use packed_pcs::*;
@@ -172,13 +173,9 @@ pub fn prove_execution(
172173
full_trace[COL_INDEX_MEM_ADDRESS_A].as_slice(),
173174
full_trace[COL_INDEX_MEM_ADDRESS_B].as_slice(),
174175
full_trace[COL_INDEX_MEM_ADDRESS_C].as_slice(),
175-
p16_indexes[0].as_slice(),
176-
p16_indexes[1].as_slice(),
177-
p16_indexes[2].as_slice(),
178-
p24_indexes[0].as_slice(),
179-
p24_indexes[1].as_slice(),
180-
p24_indexes[2].as_slice(),
181176
],
177+
p16_indexes.iter().map(Vec::as_slice).collect::<Vec<_>>(),
178+
p24_indexes.iter().map(Vec::as_slice).collect::<Vec<_>>(),
182179
p16_columns[16..p16_air.width() - 16]
183180
.iter()
184181
.map(Vec::as_slice)
@@ -213,50 +210,38 @@ pub fn prove_execution(
213210

214211
// Grand Product for consistency with precompiles
215212
let grand_product_challenge_global = prover_state.sample();
216-
let grand_product_challenge_p16 = prover_state.sample().powers().collect_n(5);
217-
let grand_product_challenge_p24 = prover_state.sample().powers().collect_n(5);
218-
let grand_product_challenge_dot_product = prover_state.sample().powers().collect_n(6);
219-
let grand_product_challenge_vm_multilinear_eval = prover_state.sample().powers().collect_n(6);
213+
let grand_product_challenge_p16 = prover_state.sample();
214+
let grand_product_challenge_p24 = prover_state.sample();
215+
let grand_product_challenge_dot_product = prover_state.sample();
216+
let grand_product_challenge_vm_multilinear_eval = prover_state.sample();
220217
let mut exec_column_for_grand_product = vec![grand_product_challenge_global; n_cycles];
221-
for pos16 in &poseidons_16 {
222-
let Some(cycle) = pos16.cycle else {
218+
for pos_16 in &poseidons_16 {
219+
let Some(cycle) = pos_16.cycle else {
223220
break;
224221
};
225222
exec_column_for_grand_product[cycle] = grand_product_challenge_global
226-
+ grand_product_challenge_p16[1]
227-
+ grand_product_challenge_p16[2] * F::from_usize(pos16.addr_input_a)
228-
+ grand_product_challenge_p16[3] * F::from_usize(pos16.addr_input_b)
229-
+ grand_product_challenge_p16[4] * F::from_usize(pos16.addr_output);
223+
+ finger_print(&pos_16.addresses_field_repr(), grand_product_challenge_p16);
230224
}
231-
for pos24 in &poseidons_24 {
232-
let Some(cycle) = pos24.cycle else {
225+
for pos_24 in &poseidons_24 {
226+
let Some(cycle) = pos_24.cycle else {
233227
break;
234228
};
235229
exec_column_for_grand_product[cycle] = grand_product_challenge_global
236-
+ grand_product_challenge_p24[1]
237-
+ grand_product_challenge_p24[2] * F::from_usize(pos24.addr_input_a)
238-
+ grand_product_challenge_p24[3] * F::from_usize(pos24.addr_input_b)
239-
+ grand_product_challenge_p24[4] * F::from_usize(pos24.addr_output);
230+
+ finger_print(&pos_24.addresses_field_repr(), grand_product_challenge_p24);
240231
}
241232
for dot_product in &dot_products {
242233
exec_column_for_grand_product[dot_product.cycle] = grand_product_challenge_global
243-
+ grand_product_challenge_dot_product[1]
244-
+ grand_product_challenge_dot_product[2] * F::from_usize(dot_product.addr_0)
245-
+ grand_product_challenge_dot_product[3] * F::from_usize(dot_product.addr_1)
246-
+ grand_product_challenge_dot_product[4] * F::from_usize(dot_product.addr_res)
247-
+ grand_product_challenge_dot_product[5] * F::from_usize(dot_product.len);
234+
+ finger_print(
235+
&dot_product.addresses_and_len_field_repr(),
236+
grand_product_challenge_dot_product,
237+
);
248238
}
249239
for multilinear_eval in &vm_multilinear_evals {
250240
exec_column_for_grand_product[multilinear_eval.cycle] = grand_product_challenge_global
251-
+ grand_product_challenge_vm_multilinear_eval[1]
252-
+ grand_product_challenge_vm_multilinear_eval[2]
253-
* F::from_usize(multilinear_eval.addr_coeffs)
254-
+ grand_product_challenge_vm_multilinear_eval[3]
255-
* F::from_usize(multilinear_eval.addr_point)
256-
+ grand_product_challenge_vm_multilinear_eval[4]
257-
* F::from_usize(multilinear_eval.addr_res)
258-
+ grand_product_challenge_vm_multilinear_eval[5]
259-
* F::from_usize(multilinear_eval.n_vars());
241+
+ finger_print(
242+
&multilinear_eval.addresses_and_n_vars_field_repr(),
243+
grand_product_challenge_vm_multilinear_eval,
244+
);
260245
}
261246

262247
let (grand_product_exec_res, grand_product_exec_statement) = prove_gkr_product(
@@ -268,10 +253,7 @@ pub fn prove_execution(
268253
.par_iter()
269254
.map(|pos_16| {
270255
grand_product_challenge_global
271-
+ grand_product_challenge_p16[1]
272-
+ grand_product_challenge_p16[2] * F::from_usize(pos_16.addr_input_a)
273-
+ grand_product_challenge_p16[3] * F::from_usize(pos_16.addr_input_b)
274-
+ grand_product_challenge_p16[4] * F::from_usize(pos_16.addr_output)
256+
+ finger_print(&pos_16.addresses_field_repr(), grand_product_challenge_p16)
275257
})
276258
.collect::<Vec<_>>();
277259

@@ -284,10 +266,7 @@ pub fn prove_execution(
284266
.par_iter()
285267
.map(|pos_24| {
286268
grand_product_challenge_global
287-
+ grand_product_challenge_p24[1]
288-
+ grand_product_challenge_p24[2] * F::from_usize(pos_24.addr_input_a)
289-
+ grand_product_challenge_p24[3] * F::from_usize(pos_24.addr_input_b)
290-
+ grand_product_challenge_p24[4] * F::from_usize(pos_24.addr_output)
269+
+ finger_print(&pos_24.addresses_field_repr(), grand_product_challenge_p24)
291270
})
292271
.collect::<Vec<_>>();
293272

@@ -300,28 +279,30 @@ pub fn prove_execution(
300279
.into_par_iter()
301280
.map(|i| {
302281
grand_product_challenge_global
303-
+ grand_product_challenge_dot_product[1]
304-
+ (grand_product_challenge_dot_product[2] * dot_product_columns[2][i]
305-
+ grand_product_challenge_dot_product[3] * dot_product_columns[3][i]
306-
+ grand_product_challenge_dot_product[4] * dot_product_columns[4][i]
307-
+ grand_product_challenge_dot_product[5] * dot_product_columns[1][i])
308-
* dot_product_columns[0][i]
282+
+ if dot_product_columns[0][i].is_zero() {
283+
grand_product_challenge_dot_product
284+
} else {
285+
finger_print(
286+
&[
287+
dot_product_columns[2][i],
288+
dot_product_columns[3][i],
289+
dot_product_columns[4][i],
290+
dot_product_columns[1][i],
291+
],
292+
grand_product_challenge_dot_product,
293+
)
294+
}
309295
})
310296
.collect::<Vec<_>>();
311297

312298
let vm_multilinear_eval_grand_product_res = vm_multilinear_evals
313-
.iter()
299+
.par_iter()
314300
.map(|vm_multilinear_eval| {
315301
grand_product_challenge_global
316-
+ grand_product_challenge_vm_multilinear_eval[1]
317-
+ grand_product_challenge_vm_multilinear_eval[2]
318-
* F::from_usize(vm_multilinear_eval.addr_coeffs)
319-
+ grand_product_challenge_vm_multilinear_eval[3]
320-
* F::from_usize(vm_multilinear_eval.addr_point)
321-
+ grand_product_challenge_vm_multilinear_eval[4]
322-
* F::from_usize(vm_multilinear_eval.addr_res)
323-
+ grand_product_challenge_vm_multilinear_eval[5]
324-
* F::from_usize(vm_multilinear_eval.n_vars())
302+
+ finger_print(
303+
&vm_multilinear_eval.addresses_and_n_vars_field_repr(),
304+
grand_product_challenge_vm_multilinear_eval,
305+
)
325306
})
326307
.product::<EF>();
327308

@@ -340,22 +321,22 @@ pub fn prove_execution(
340321
);
341322
let corrected_prod_p16 = grand_product_p16_res
342323
/ (grand_product_challenge_global
343-
+ grand_product_challenge_p16[1]
344-
+ grand_product_challenge_p16[4] * F::from_usize(POSEIDON_16_NULL_HASH_PTR))
324+
+ grand_product_challenge_p16
325+
+ grand_product_challenge_p16.exp_u64(4) * F::from_usize(POSEIDON_16_NULL_HASH_PTR))
345326
.exp_u64((n_poseidons_16.next_power_of_two() - n_poseidons_16) as u64);
346327

347328
let corrected_prod_p24 = grand_product_p24_res
348329
/ (grand_product_challenge_global
349-
+ grand_product_challenge_p24[1]
350-
+ grand_product_challenge_p24[4] * F::from_usize(POSEIDON_24_NULL_HASH_PTR))
330+
+ grand_product_challenge_p24
331+
+ grand_product_challenge_p24.exp_u64(4) * F::from_usize(POSEIDON_24_NULL_HASH_PTR))
351332
.exp_u64((n_poseidons_24.next_power_of_two() - n_poseidons_24) as u64);
352333

353334
let corrected_dot_product = grand_product_dot_product_res
354335
/ ((grand_product_challenge_global
355-
+ grand_product_challenge_dot_product[1]
356-
+ grand_product_challenge_dot_product[5])
357-
.exp_u64(dot_product_padding_len as u64)
358-
* (grand_product_challenge_global + grand_product_challenge_dot_product[1]).exp_u64(
336+
+ grand_product_challenge_dot_product
337+
+ grand_product_challenge_dot_product.exp_u64(5))
338+
.exp_u64(dot_product_padding_len as u64)
339+
* (grand_product_challenge_global + grand_product_challenge_dot_product).exp_u64(
359340
((1 << log_n_rows_dot_product_table) - dot_product_padding_len - dot_products.len())
360341
as u64,
361342
));
@@ -419,11 +400,8 @@ pub fn prove_execution(
419400
)];
420401

421402
let dot_product_footprint_computation = DotProductFootprint {
422-
grand_product_challenge_global,
423-
grand_product_challenge_dot_product: grand_product_challenge_dot_product
424-
.clone()
425-
.try_into()
426-
.unwrap(),
403+
global_challenge: grand_product_challenge_global,
404+
dot_product_challenge: powers_const(grand_product_challenge_dot_product),
427405
};
428406

429407
let (
@@ -474,15 +452,11 @@ pub fn prove_execution(
474452
);
475453

476454
let precompile_foot_print_computation = PrecompileFootprint {
477-
grand_product_challenge_global,
478-
grand_product_challenge_p16: grand_product_challenge_p16.try_into().unwrap(),
479-
grand_product_challenge_p24: grand_product_challenge_p24.try_into().unwrap(),
480-
grand_product_challenge_dot_product: grand_product_challenge_dot_product
481-
.try_into()
482-
.unwrap(),
483-
grand_product_challenge_vm_multilinear_eval: grand_product_challenge_vm_multilinear_eval
484-
.try_into()
485-
.unwrap(),
455+
global_challenge: grand_product_challenge_global,
456+
p16_powers: powers_const(grand_product_challenge_p16),
457+
p24_powers: powers_const(grand_product_challenge_p24),
458+
dot_product_powers: powers_const(grand_product_challenge_dot_product),
459+
multilinear_eval_powers: powers_const(grand_product_challenge_vm_multilinear_eval),
486460
};
487461

488462
let (grand_product_exec_sumcheck_point, grand_product_exec_sumcheck_inner_evals, _) =

0 commit comments

Comments
 (0)