Skip to content

Commit d405568

Browse files
committed
get_poseidon_lookup_statements
1 parent bf393ab commit d405568

File tree

3 files changed

+115
-194
lines changed

3 files changed

+115
-194
lines changed

crates/lean_prover/src/common.rs

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -274,3 +274,102 @@ impl SumcheckComputationPacked<EF> for DotProductFootprint {
274274
self.air_eval(point, |p, c| EFPacking::<EF>::from(p) * c)
275275
}
276276
}
277+
278+
pub fn get_poseidon_lookup_statements(
279+
(p16_air_width, p24_air_width): (usize, usize),
280+
(log_n_p16, log_n_p24): (usize, usize),
281+
(p16_evals, p24_evals): (&[EF], &[EF]),
282+
(p16_air_point, p24_air_point): (&MultilinearPoint<EF>, &MultilinearPoint<EF>),
283+
memory_folding_challenges: &MultilinearPoint<EF>,
284+
) -> Vec<Evaluation<EF>> {
285+
let p16_folded_eval_addr_a = (&p16_evals[..8]).evaluate(memory_folding_challenges);
286+
let p16_folded_eval_addr_b = (&p16_evals[8..16]).evaluate(memory_folding_challenges);
287+
let p16_folded_eval_addr_res_a =
288+
(&p16_evals[p16_air_width - 16..p16_air_width - 8]).evaluate(memory_folding_challenges);
289+
let p16_folded_eval_addr_res_b =
290+
(&p16_evals[p16_air_width - 8..]).evaluate(memory_folding_challenges);
291+
292+
let p24_folded_eval_addr_a = (&p24_evals[..8]).evaluate(memory_folding_challenges);
293+
let p24_folded_eval_addr_b = (&p24_evals[8..16]).evaluate(memory_folding_challenges);
294+
let p24_folded_eval_addr_c = (&p24_evals[16..24]).evaluate(memory_folding_challenges);
295+
let p24_folded_eval_addr_res =
296+
(&p24_evals[p24_air_width - 8..]).evaluate(memory_folding_challenges);
297+
298+
let padding_p16 = EF::zero_vec(log_n_p16.max(log_n_p24) - log_n_p16);
299+
let padding_p24 = EF::zero_vec(log_n_p16.max(log_n_p24) - log_n_p24);
300+
301+
vec![
302+
Evaluation::new(
303+
[
304+
vec![EF::ZERO; 3],
305+
padding_p16.clone(),
306+
p16_air_point.0.clone(),
307+
]
308+
.concat(),
309+
p16_folded_eval_addr_a,
310+
),
311+
Evaluation::new(
312+
[
313+
vec![EF::ZERO, EF::ZERO, EF::ONE],
314+
padding_p16.clone(),
315+
p16_air_point.0.clone(),
316+
]
317+
.concat(),
318+
p16_folded_eval_addr_b,
319+
),
320+
Evaluation::new(
321+
[
322+
vec![EF::ZERO, EF::ONE, EF::ZERO],
323+
padding_p16.clone(),
324+
p16_air_point.0.clone(),
325+
]
326+
.concat(),
327+
p16_folded_eval_addr_res_a,
328+
),
329+
Evaluation::new(
330+
[
331+
vec![EF::ZERO, EF::ONE, EF::ONE],
332+
padding_p16.clone(),
333+
p16_air_point.0.clone(),
334+
]
335+
.concat(),
336+
p16_folded_eval_addr_res_b,
337+
),
338+
Evaluation::new(
339+
[
340+
vec![EF::ONE, EF::ZERO, EF::ZERO],
341+
padding_p24.clone(),
342+
p24_air_point.0.clone(),
343+
]
344+
.concat(),
345+
p24_folded_eval_addr_a,
346+
),
347+
Evaluation::new(
348+
[
349+
vec![EF::ONE, EF::ZERO, EF::ONE],
350+
padding_p24.clone(),
351+
p24_air_point.0.clone(),
352+
]
353+
.concat(),
354+
p24_folded_eval_addr_b,
355+
),
356+
Evaluation::new(
357+
[
358+
vec![EF::ONE, EF::ONE, EF::ZERO],
359+
padding_p24.clone(),
360+
p24_air_point.0.clone(),
361+
]
362+
.concat(),
363+
p24_folded_eval_addr_c,
364+
),
365+
Evaluation::new(
366+
[
367+
vec![EF::ONE, EF::ONE, EF::ONE],
368+
padding_p24.clone(),
369+
p24_air_point.0.clone(),
370+
]
371+
.concat(),
372+
p24_folded_eval_addr_res,
373+
),
374+
]
375+
}

crates/lean_prover/src/prove_execution.rs

Lines changed: 9 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,9 @@ pub fn prove_execution(
7171
let log_n_cycles = log2_strict_usize(n_cycles);
7272
assert!(full_trace.iter().all(|col| col.len() == 1 << log_n_cycles));
7373

74+
let log_n_p16 = log2_ceil_usize(n_poseidons_16);
75+
let log_n_p24 = log2_ceil_usize(n_poseidons_24);
76+
7477
let dft = EvalsDft::default();
7578

7679
let mut exec_columns = full_trace[..N_INSTRUCTION_COLUMNS_IN_AIR]
@@ -528,106 +531,14 @@ pub fn prove_execution(
528531
let poseidon_logup_star_alpha = prover_state.sample();
529532
let memory_folding_challenges = MultilinearPoint(prover_state.sample_vec(LOG_VECTOR_LEN));
530533

531-
let p16_folded_eval_addr_a =
532-
(&p16_evals_to_prove[..8]).evaluate(&memory_folding_challenges);
533-
let p16_folded_eval_addr_b =
534-
(&p16_evals_to_prove[8..16]).evaluate(&memory_folding_challenges);
535-
let p16_folded_eval_addr_res_a = (&p16_evals_to_prove
536-
[p16_air.width() - 16..p16_air.width() - 8])
537-
.evaluate(&memory_folding_challenges);
538-
let p16_folded_eval_addr_res_b =
539-
(&p16_evals_to_prove[p16_air.width() - 8..]).evaluate(&memory_folding_challenges);
540-
541-
let p24_folded_eval_addr_a =
542-
(&p24_evals_to_prove[..8]).evaluate(&memory_folding_challenges);
543-
let p24_folded_eval_addr_b =
544-
(&p24_evals_to_prove[8..16]).evaluate(&memory_folding_challenges);
545-
let p24_folded_eval_addr_c =
546-
(&p24_evals_to_prove[16..24]).evaluate(&memory_folding_challenges);
547-
let p24_folded_eval_addr_res =
548-
(&p24_evals_to_prove[p24_air.width() - 8..]).evaluate(&memory_folding_challenges);
549-
550-
let padding_p16 = EF::zero_vec(
551-
log2_ceil_usize(n_poseidons_24).saturating_sub(log2_ceil_usize(n_poseidons_16)),
552-
);
553-
let padding_p24 = EF::zero_vec(
554-
log2_ceil_usize(n_poseidons_16).saturating_sub(log2_ceil_usize(n_poseidons_24)),
534+
let poseidon_lookup_statements = get_poseidon_lookup_statements(
535+
(p16_air.width(), p24_air.width()),
536+
(log_n_p16, log_n_p24),
537+
(&p16_evals_to_prove, &p24_evals_to_prove),
538+
(&p16_air_point, &p24_air_point),
539+
&memory_folding_challenges,
555540
);
556541

557-
let poseidon_lookup_statements = vec![
558-
Evaluation::new(
559-
[
560-
vec![EF::ZERO; 3],
561-
padding_p16.clone(),
562-
p16_air_point.0.clone(),
563-
]
564-
.concat(),
565-
p16_folded_eval_addr_a,
566-
),
567-
Evaluation::new(
568-
[
569-
vec![EF::ZERO, EF::ZERO, EF::ONE],
570-
padding_p16.clone(),
571-
p16_air_point.0.clone(),
572-
]
573-
.concat(),
574-
p16_folded_eval_addr_b,
575-
),
576-
Evaluation::new(
577-
[
578-
vec![EF::ZERO, EF::ONE, EF::ZERO],
579-
padding_p16.clone(),
580-
p16_air_point.0.clone(),
581-
]
582-
.concat(),
583-
p16_folded_eval_addr_res_a,
584-
),
585-
Evaluation::new(
586-
[
587-
vec![EF::ZERO, EF::ONE, EF::ONE],
588-
padding_p16.clone(),
589-
p16_air_point.0.clone(),
590-
]
591-
.concat(),
592-
p16_folded_eval_addr_res_b,
593-
),
594-
Evaluation::new(
595-
[
596-
vec![EF::ONE, EF::ZERO, EF::ZERO],
597-
padding_p24.clone(),
598-
p24_air_point.0.clone(),
599-
]
600-
.concat(),
601-
p24_folded_eval_addr_a,
602-
),
603-
Evaluation::new(
604-
[
605-
vec![EF::ONE, EF::ZERO, EF::ONE],
606-
padding_p24.clone(),
607-
p24_air_point.0.clone(),
608-
]
609-
.concat(),
610-
p24_folded_eval_addr_b,
611-
),
612-
Evaluation::new(
613-
[
614-
vec![EF::ONE, EF::ONE, EF::ZERO],
615-
padding_p24.clone(),
616-
p24_air_point.0.clone(),
617-
]
618-
.concat(),
619-
p24_folded_eval_addr_c,
620-
),
621-
Evaluation::new(
622-
[
623-
vec![EF::ONE, EF::ONE, EF::ONE],
624-
padding_p24.clone(),
625-
p24_air_point.0.clone(),
626-
]
627-
.concat(),
628-
p24_folded_eval_addr_res,
629-
),
630-
];
631542
let max_n_poseidons = poseidons_16
632543
.len()
633544
.max(poseidons_24.len())
@@ -987,8 +898,6 @@ pub fn prove_execution(
987898
{
988899
// index opening for poseidon lookup
989900

990-
let log_n_p16 = log2_ceil_usize(n_poseidons_16);
991-
let log_n_p24 = log2_ceil_usize(n_poseidons_24);
992901
let correcting_factor = poseidon_logup_star_statements.on_indexes.point
993902
[3..3 + log_n_p16.abs_diff(log_n_p24)]
994903
.iter()

crates/lean_prover/src/verify_execution.rs

Lines changed: 7 additions & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -493,100 +493,13 @@ pub fn verify_execution(
493493
)
494494
.unwrap();
495495

496-
let max_n_poseidons = n_poseidons_16.max(n_poseidons_24).next_power_of_two();
497-
498-
let p16_folded_eval_addr_a = (&p16_evals_to_verify[..8]).evaluate(&memory_folding_challenges);
499-
let p16_folded_eval_addr_b = (&p16_evals_to_verify[8..16]).evaluate(&memory_folding_challenges);
500-
let p16_folded_eval_addr_res_a = (&p16_evals_to_verify
501-
[p16_air.width() - 16..p16_air.width() - 8])
502-
.evaluate(&memory_folding_challenges);
503-
let p16_folded_eval_addr_res_b =
504-
(&p16_evals_to_verify[p16_air.width() - 8..]).evaluate(&memory_folding_challenges);
505-
506-
let p24_folded_eval_addr_a = (&p24_evals_to_verify[..8]).evaluate(&memory_folding_challenges);
507-
let p24_folded_eval_addr_b = (&p24_evals_to_verify[8..16]).evaluate(&memory_folding_challenges);
508-
let p24_folded_eval_addr_c =
509-
(&p24_evals_to_verify[16..24]).evaluate(&memory_folding_challenges);
510-
let p24_folded_eval_addr_res =
511-
(&p24_evals_to_verify[p24_air.width() - 8..]).evaluate(&memory_folding_challenges);
512-
513-
let padding_p16 = EF::zero_vec(log2_ceil_usize(max_n_poseidons) - log_n_p16);
514-
let padding_p24 = EF::zero_vec(log2_ceil_usize(max_n_poseidons) - log_n_p24);
515-
516-
let poseidon_lookup_statements = vec![
517-
Evaluation::new(
518-
[
519-
vec![EF::ZERO; 3],
520-
padding_p16.clone(),
521-
p16_air_point.0.clone(),
522-
]
523-
.concat(),
524-
p16_folded_eval_addr_a,
525-
),
526-
Evaluation::new(
527-
[
528-
vec![EF::ZERO, EF::ZERO, EF::ONE],
529-
padding_p16.clone(),
530-
p16_air_point.0.clone(),
531-
]
532-
.concat(),
533-
p16_folded_eval_addr_b,
534-
),
535-
Evaluation::new(
536-
[
537-
vec![EF::ZERO, EF::ONE, EF::ZERO],
538-
padding_p16.clone(),
539-
p16_air_point.0.clone(),
540-
]
541-
.concat(),
542-
p16_folded_eval_addr_res_a,
543-
),
544-
Evaluation::new(
545-
[
546-
vec![EF::ZERO, EF::ONE, EF::ONE],
547-
padding_p16.clone(),
548-
p16_air_point.0.clone(),
549-
]
550-
.concat(),
551-
p16_folded_eval_addr_res_b,
552-
),
553-
Evaluation::new(
554-
[
555-
vec![EF::ONE, EF::ZERO, EF::ZERO],
556-
padding_p24.clone(),
557-
p24_air_point.0.clone(),
558-
]
559-
.concat(),
560-
p24_folded_eval_addr_a,
561-
),
562-
Evaluation::new(
563-
[
564-
vec![EF::ONE, EF::ZERO, EF::ONE],
565-
padding_p24.clone(),
566-
p24_air_point.0.clone(),
567-
]
568-
.concat(),
569-
p24_folded_eval_addr_b,
570-
),
571-
Evaluation::new(
572-
[
573-
vec![EF::ONE, EF::ONE, EF::ZERO],
574-
padding_p24.clone(),
575-
p24_air_point.0.clone(),
576-
]
577-
.concat(),
578-
p24_folded_eval_addr_c,
579-
),
580-
Evaluation::new(
581-
[
582-
vec![EF::ONE, EF::ONE, EF::ONE],
583-
padding_p24.clone(),
584-
p24_air_point.0.clone(),
585-
]
586-
.concat(),
587-
p24_folded_eval_addr_res,
588-
),
589-
];
496+
let poseidon_lookup_statements = get_poseidon_lookup_statements(
497+
(p16_air.width(), p24_air.width()),
498+
(log_n_p16, log_n_p24),
499+
(&p16_evals_to_verify, &p24_evals_to_verify),
500+
(&p16_air_point, &p24_air_point),
501+
&memory_folding_challenges,
502+
);
590503

591504
let poseidon_lookup_log_length = 3 + log_n_p16.max(log_n_p24);
592505
let poseidon_logup_star_statements = verify_logup_star(

0 commit comments

Comments
 (0)