Skip to content

Commit caf9ce6

Browse files
TomWambsgansTomWambsgans
committed
add_poseidon_lookup_statements_on_indexes
1 parent 6e34c56 commit caf9ce6

File tree

3 files changed

+92
-108
lines changed

3 files changed

+92
-108
lines changed

‎crates/lean_prover/src/common.rs‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,3 +373,48 @@ pub fn get_poseidon_lookup_statements(
373373
),
374374
]
375375
}
376+
377+
pub fn poseidon_lookup_correcting_factors(
378+
log_n_p16: usize,
379+
log_n_p24: usize,
380+
index_lookup_point: &MultilinearPoint<EF>,
381+
) -> (EF, EF) {
382+
let correcting_factor = index_lookup_point[3..3 + log_n_p16.abs_diff(log_n_p24)]
383+
.iter()
384+
.map(|&x| EF::ONE - x)
385+
.product::<EF>();
386+
if log_n_p16 > log_n_p24 {
387+
(EF::ONE, correcting_factor)
388+
} else {
389+
(correcting_factor, EF::ONE)
390+
}
391+
}
392+
393+
pub fn add_poseidon_lookup_statements_on_indexes(
394+
log_n_p16: usize,
395+
log_n_p24: usize,
396+
index_lookup_point: &MultilinearPoint<EF>,
397+
inner_values: &[EF],
398+
p16_indexe_statements: [&mut Vec<Evaluation<EF>>; 3], // a, b, res
399+
p24_indexe_statements: [&mut Vec<Evaluation<EF>>; 3], // a, b, res
400+
) {
401+
assert_eq!(inner_values.len(), 6);
402+
let mut idx_point_right_p16 = MultilinearPoint(index_lookup_point[3..].to_vec());
403+
let mut idx_point_right_p24 =
404+
MultilinearPoint(index_lookup_point[3 + log_n_p16.abs_diff(log_n_p24)..].to_vec());
405+
if log_n_p16 < log_n_p24 {
406+
std::mem::swap(&mut idx_point_right_p16, &mut idx_point_right_p24);
407+
}
408+
for (i, stmt) in p16_indexe_statements.into_iter().enumerate() {
409+
stmt.push(Evaluation::new(
410+
idx_point_right_p16.clone(),
411+
inner_values[i],
412+
));
413+
}
414+
for (i, stmt) in p24_indexe_statements.into_iter().enumerate() {
415+
stmt.push(Evaluation::new(
416+
idx_point_right_p24.clone(),
417+
inner_values[i + 3],
418+
));
419+
}
420+
}

‎crates/lean_prover/src/prove_execution.rs‎

Lines changed: 20 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -854,26 +854,11 @@ pub fn prove_execution(
854854
{
855855
// index opening for poseidon lookup
856856

857-
let correcting_factor = poseidon_logup_star_statements.on_indexes.point
858-
[3..3 + log_n_p16.abs_diff(log_n_p24)]
859-
.iter()
860-
.map(|&x| EF::ONE - x)
861-
.product::<EF>();
862-
let (correcting_factor_p16, correcting_factor_p24) = if n_poseidons_16 > n_poseidons_24 {
863-
(EF::ONE, correcting_factor)
864-
} else {
865-
(correcting_factor, EF::ONE)
866-
};
867-
let mut idx_point_right_p16 =
868-
MultilinearPoint(poseidon_logup_star_statements.on_indexes.point[3..].to_vec());
869-
let mut idx_point_right_p24 = MultilinearPoint(
870-
poseidon_logup_star_statements.on_indexes.point[3 + log_n_p16.abs_diff(log_n_p24)..]
871-
.to_vec(),
857+
let (correcting_factor_p16, correcting_factor_p24) = poseidon_lookup_correcting_factors(
858+
log_n_p16,
859+
log_n_p24,
860+
&poseidon_logup_star_statements.on_indexes.point,
872861
);
873-
if n_poseidons_16 < n_poseidons_24 {
874-
std::mem::swap(&mut idx_point_right_p16, &mut idx_point_right_p24);
875-
}
876-
877862
let poseidon_index_evals = fold_multilinear(
878863
&all_poseidon_indexes,
879864
&MultilinearPoint(poseidon_logup_star_statements.on_indexes.point[3..].to_vec()),
@@ -889,48 +874,23 @@ pub fn prove_execution(
889874
poseidon_index_evals[7] / correcting_factor_p24,
890875
];
891876

892-
assert_eq!(
893-
poseidon_index_evals[3] / correcting_factor_p16,
894-
poseidon_index_evals[2] / correcting_factor_p16 + F::ONE
895-
);
896-
897-
assert_eq!(
898-
poseidon_index_evals[5] / correcting_factor_p24,
899-
poseidon_index_evals[4] / correcting_factor_p24 + F::ONE
900-
);
901-
902877
prover_state.add_extension_scalars(&inner_values);
903-
p16_indexes_a_statements.push(Evaluation::new(
904-
idx_point_right_p16.clone(),
905-
inner_values[0],
906-
));
907-
p16_indexes_b_statements.push(Evaluation::new(
908-
idx_point_right_p16.clone(),
909-
inner_values[1],
910-
));
911-
p16_indexes_res_statements.push(Evaluation::new(
912-
idx_point_right_p16.clone(),
913-
inner_values[2],
914-
));
915-
p24_indexes_a_statements.push(Evaluation::new(
916-
idx_point_right_p24.clone(),
917-
inner_values[3],
918-
));
919-
p24_indexes_b_statements.push(Evaluation::new(
920-
idx_point_right_p24.clone(),
921-
inner_values[4],
922-
));
923-
p24_indexes_res_statements.push(Evaluation::new(
924-
idx_point_right_p24.clone(),
925-
inner_values[5],
926-
));
927-
928-
// sanity check
929-
assert_eq!(
930-
poseidon_index_evals.evaluate(&MultilinearPoint(
931-
poseidon_logup_star_statements.on_indexes.point[..3].to_vec()
932-
)),
933-
poseidon_logup_star_statements.on_indexes.value
878+
879+
add_poseidon_lookup_statements_on_indexes(
880+
log_n_p16,
881+
log_n_p24,
882+
&poseidon_logup_star_statements.on_indexes.point,
883+
&inner_values,
884+
[
885+
&mut p16_indexes_a_statements,
886+
&mut p16_indexes_b_statements,
887+
&mut p16_indexes_res_statements,
888+
],
889+
[
890+
&mut p24_indexes_a_statements,
891+
&mut p24_indexes_b_statements,
892+
&mut p24_indexes_res_statements,
893+
],
934894
);
935895
}
936896

‎crates/lean_prover/src/verify_execution.rs‎

Lines changed: 27 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -543,51 +543,30 @@ pub fn verify_execution(
543543
{
544544
// index opening for poseidon lookup
545545

546-
let correcting_factor = poseidon_logup_star_statements.on_indexes.point
547-
[3..3 + log_n_p16.abs_diff(log_n_p24)]
548-
.iter()
549-
.map(|&x| EF::ONE - x)
550-
.product::<EF>();
551-
let (correcting_factor_p16, correcting_factor_p24) = if n_poseidons_16 > n_poseidons_24 {
552-
(EF::ONE, correcting_factor)
553-
} else {
554-
(correcting_factor, EF::ONE)
555-
};
556-
let mut idx_point_right_p16 =
557-
MultilinearPoint(poseidon_logup_star_statements.on_indexes.point[3..].to_vec());
558-
let mut idx_point_right_p24 = MultilinearPoint(
559-
poseidon_logup_star_statements.on_indexes.point[3 + log_n_p16.abs_diff(log_n_p24)..]
560-
.to_vec(),
546+
let (correcting_factor_p16, correcting_factor_p24) = poseidon_lookup_correcting_factors(
547+
log_n_p16,
548+
log_n_p24,
549+
&poseidon_logup_star_statements.on_indexes.point,
561550
);
562-
if n_poseidons_16 < n_poseidons_24 {
563-
std::mem::swap(&mut idx_point_right_p16, &mut idx_point_right_p24);
564-
}
565551

566552
let mut inner_values = verifier_state.next_extension_scalars_vec(6)?;
567-
p16_indexes_a_statements.push(Evaluation::new(
568-
idx_point_right_p16.clone(),
569-
inner_values[0],
570-
));
571-
p16_indexes_b_statements.push(Evaluation::new(
572-
idx_point_right_p16.clone(),
573-
inner_values[1],
574-
));
575-
p16_indexes_res_statements.push(Evaluation::new(
576-
idx_point_right_p16.clone(),
577-
inner_values[2],
578-
));
579-
p24_indexes_a_statements.push(Evaluation::new(
580-
idx_point_right_p24.clone(),
581-
inner_values[3],
582-
));
583-
p24_indexes_b_statements.push(Evaluation::new(
584-
idx_point_right_p24.clone(),
585-
inner_values[4],
586-
));
587-
p24_indexes_res_statements.push(Evaluation::new(
588-
idx_point_right_p24.clone(),
589-
inner_values[5],
590-
));
553+
554+
add_poseidon_lookup_statements_on_indexes(
555+
log_n_p16,
556+
log_n_p24,
557+
&poseidon_logup_star_statements.on_indexes.point,
558+
&inner_values,
559+
[
560+
&mut p16_indexes_a_statements,
561+
&mut p16_indexes_b_statements,
562+
&mut p16_indexes_res_statements,
563+
],
564+
[
565+
&mut p24_indexes_a_statements,
566+
&mut p24_indexes_b_statements,
567+
&mut p24_indexes_res_statements,
568+
],
569+
);
591570

592571
inner_values.insert(3, inner_values[2] + EF::ONE);
593572
inner_values.insert(5, inner_values[4] + EF::ONE);
@@ -599,12 +578,12 @@ pub fn verify_execution(
599578
*v *= correcting_factor_p24;
600579
}
601580

602-
assert_eq!(
603-
inner_values.evaluate(&MultilinearPoint(
604-
poseidon_logup_star_statements.on_indexes.point[..3].to_vec()
605-
)),
606-
poseidon_logup_star_statements.on_indexes.value
607-
);
581+
if inner_values.evaluate(&MultilinearPoint(
582+
poseidon_logup_star_statements.on_indexes.point[..3].to_vec(),
583+
)) != poseidon_logup_star_statements.on_indexes.value
584+
{
585+
return Err(ProofError::InvalidProof);
586+
}
608587
}
609588

610589
let (initial_pc_statement, final_pc_statement) =

0 commit comments

Comments
 (0)