Skip to content

Commit 4c07ce7

Browse files
committed
remove some columns from the sumcheck for precompile footprint
1 parent 7e8b93c commit 4c07ce7

File tree

3 files changed

+81
-20
lines changed

3 files changed

+81
-20
lines changed

crates/lean_prover/src/common.rs

Lines changed: 48 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,41 @@ pub struct PrecompileFootprint {
144144
pub multilinear_eval_powers: [EF; 6],
145145
}
146146

147+
const PRECOMP_INDEX_OPERAND_A: usize = 0;
148+
const PRECOMP_INDEX_OPERAND_B: usize = 1;
149+
const PRECOMP_INDEX_FLAG_A: usize = 2;
150+
const PRECOMP_INDEX_FLAG_B: usize = 3;
151+
const PRECOMP_INDEX_FLAG_C: usize = 4;
152+
const PRECOMP_INDEX_AUX: usize = 5;
153+
const PRECOMP_INDEX_POSEIDON_16: usize = 6;
154+
const PRECOMP_INDEX_POSEIDON_24: usize = 7;
155+
const PRECOMP_INDEX_DOT_PRODUCT: usize = 8;
156+
const PRECOMP_INDEX_MULTILINEAR_EVAL: usize = 9;
157+
const PRECOMP_INDEX_MEM_VALUE_A: usize = 10;
158+
const PRECOMP_INDEX_MEM_VALUE_B: usize = 11;
159+
const PRECOMP_INDEX_MEM_VALUE_C: usize = 12;
160+
const PRECOMP_INDEX_FP: usize = 13;
161+
162+
pub fn reorder_full_trace_for_precomp_foot_print<A: Copy>(full_trace: Vec<A>) -> Vec<A> {
163+
assert_eq!(full_trace.len(), N_TOTAL_COLUMNS);
164+
vec![
165+
full_trace[COL_INDEX_OPERAND_A],
166+
full_trace[COL_INDEX_OPERAND_B],
167+
full_trace[COL_INDEX_FLAG_A],
168+
full_trace[COL_INDEX_FLAG_B],
169+
full_trace[COL_INDEX_FLAG_C],
170+
full_trace[COL_INDEX_AUX],
171+
full_trace[COL_INDEX_POSEIDON_16],
172+
full_trace[COL_INDEX_POSEIDON_24],
173+
full_trace[COL_INDEX_DOT_PRODUCT],
174+
full_trace[COL_INDEX_MULTILINEAR_EVAL],
175+
full_trace[COL_INDEX_MEM_VALUE_A],
176+
full_trace[COL_INDEX_MEM_VALUE_B],
177+
full_trace[COL_INDEX_MEM_VALUE_C],
178+
full_trace[COL_INDEX_FP],
179+
]
180+
}
181+
147182
impl PrecompileFootprint {
148183
fn air_eval<
149184
PointF: PrimeCharacteristicRing + Copy,
@@ -153,36 +188,36 @@ impl PrecompileFootprint {
153188
point: &[PointF],
154189
mul_point_f_and_ef: impl Fn(PointF, EF) -> ResultF,
155190
) -> ResultF {
156-
let nu_a = (ResultF::ONE - point[COL_INDEX_FLAG_A]) * point[COL_INDEX_MEM_VALUE_A]
157-
+ point[COL_INDEX_FLAG_A] * point[COL_INDEX_OPERAND_A];
158-
let nu_b = (ResultF::ONE - point[COL_INDEX_FLAG_B]) * point[COL_INDEX_MEM_VALUE_B]
159-
+ point[COL_INDEX_FLAG_B] * point[COL_INDEX_OPERAND_B];
160-
let nu_c = (ResultF::ONE - point[COL_INDEX_FLAG_C]) * point[COL_INDEX_MEM_VALUE_C]
161-
+ point[COL_INDEX_FLAG_C] * point[COL_INDEX_FP];
191+
let nu_a = (ResultF::ONE - point[PRECOMP_INDEX_FLAG_A]) * point[PRECOMP_INDEX_MEM_VALUE_A]
192+
+ point[PRECOMP_INDEX_FLAG_A] * point[PRECOMP_INDEX_OPERAND_A];
193+
let nu_b = (ResultF::ONE - point[PRECOMP_INDEX_FLAG_B]) * point[PRECOMP_INDEX_MEM_VALUE_B]
194+
+ point[PRECOMP_INDEX_FLAG_B] * point[PRECOMP_INDEX_OPERAND_B];
195+
let nu_c = (ResultF::ONE - point[PRECOMP_INDEX_FLAG_C]) * point[PRECOMP_INDEX_MEM_VALUE_C]
196+
+ point[PRECOMP_INDEX_FLAG_C] * point[PRECOMP_INDEX_FP];
162197

163198
(nu_a * self.p16_powers[2]
164199
+ nu_b * self.p16_powers[3]
165200
+ nu_c * self.p16_powers[4]
166-
+ mul_point_f_and_ef(point[COL_INDEX_AUX], self.p16_powers[5])
201+
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.p16_powers[5])
167202
+ self.p16_powers[1])
168-
* point[COL_INDEX_POSEIDON_16]
203+
* point[PRECOMP_INDEX_POSEIDON_16]
169204
+ (nu_a * self.p24_powers[2]
170205
+ nu_b * self.p24_powers[3]
171206
+ nu_c * self.p24_powers[4]
172207
+ self.p24_powers[1])
173-
* point[COL_INDEX_POSEIDON_24]
208+
* point[PRECOMP_INDEX_POSEIDON_24]
174209
+ (nu_a * self.dot_product_powers[2]
175210
+ nu_b * self.dot_product_powers[3]
176211
+ nu_c * self.dot_product_powers[4]
177-
+ mul_point_f_and_ef(point[COL_INDEX_AUX], self.dot_product_powers[5])
212+
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.dot_product_powers[5])
178213
+ self.dot_product_powers[1])
179-
* point[COL_INDEX_DOT_PRODUCT]
214+
* point[PRECOMP_INDEX_DOT_PRODUCT]
180215
+ (nu_a * self.multilinear_eval_powers[2]
181216
+ nu_b * self.multilinear_eval_powers[3]
182217
+ nu_c * self.multilinear_eval_powers[4]
183-
+ mul_point_f_and_ef(point[COL_INDEX_AUX], self.multilinear_eval_powers[5])
218+
+ mul_point_f_and_ef(point[PRECOMP_INDEX_AUX], self.multilinear_eval_powers[5])
184219
+ self.multilinear_eval_powers[1])
185-
* point[COL_INDEX_MULTILINEAR_EVAL]
220+
* point[PRECOMP_INDEX_MULTILINEAR_EVAL]
186221
+ self.global_challenge
187222
}
188223
}

crates/lean_prover/src/prove_execution.rs

Lines changed: 26 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -466,13 +466,17 @@ pub fn prove_execution(
466466
multilinear_eval_powers: powers_const(grand_product_challenge_vm_multilinear_eval),
467467
};
468468

469-
let (grand_product_exec_sumcheck_point, grand_product_exec_sumcheck_inner_evals, _) =
469+
let (grand_product_exec_sumcheck_point, mut grand_product_exec_sumcheck_inner_evals, _) =
470470
info_span!("Grand product sumcheck for Execution").in_scope(|| {
471471
sumcheck_prove(
472472
1, // TODO univariate skip
473473
MleGroupRef::Base(
474-
// TODO not all columns re required
475-
full_trace.iter().map(|c| c.as_slice()).collect::<Vec<_>>(),
474+
reorder_full_trace_for_precomp_foot_print(
475+
full_trace.iter().collect::<Vec<_>>(),
476+
)
477+
.iter()
478+
.map(|c| c.as_slice())
479+
.collect::<Vec<_>>(),
476480
)
477481
.pack(),
478482
&precompile_foot_print_computation,
@@ -486,11 +490,28 @@ pub fn prove_execution(
486490
)
487491
});
488492

489-
prover_state.add_extension_scalars(&grand_product_exec_sumcheck_inner_evals);
493+
// TODO compute eq polynomial 1 time and then inner product with each column
494+
for col in [
495+
COL_INDEX_OPERAND_C,
496+
COL_INDEX_ADD,
497+
COL_INDEX_MUL,
498+
COL_INDEX_DEREF,
499+
COL_INDEX_JUMP,
500+
COL_INDEX_PC,
501+
COL_INDEX_MEM_ADDRESS_A,
502+
COL_INDEX_MEM_ADDRESS_B,
503+
COL_INDEX_MEM_ADDRESS_C,
504+
] {
505+
grand_product_exec_sumcheck_inner_evals.insert(
506+
col,
507+
full_trace[col].evaluate(&grand_product_exec_sumcheck_point),
508+
);
509+
}
490510
assert_eq!(
491511
N_TOTAL_COLUMNS,
492512
grand_product_exec_sumcheck_inner_evals.len()
493-
); // TODO open less columns
513+
);
514+
prover_state.add_extension_scalars(&grand_product_exec_sumcheck_inner_evals);
494515

495516
let grand_product_exec_evals_on_each_column =
496517
&grand_product_exec_sumcheck_inner_evals[..N_INSTRUCTION_COLUMNS];

crates/lean_prover/src/verify_execution.rs

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -300,7 +300,7 @@ pub fn verify_execution(
300300
}
301301

302302
let grand_product_exec_sumcheck_inner_evals =
303-
verifier_state.next_extension_scalars_vec(N_TOTAL_COLUMNS)?;
303+
verifier_state.next_extension_scalars_vec(N_TOTAL_COLUMNS)?; // TODO some of the values are unused
304304

305305
let grand_product_exec_evals_on_each_column =
306306
&grand_product_exec_sumcheck_inner_evals[..N_INSTRUCTION_COLUMNS];
@@ -319,7 +319,12 @@ pub fn verify_execution(
319319
grand_product_challenge_vm_multilinear_eval,
320320
),
321321
}
322-
.eval(&grand_product_exec_sumcheck_inner_evals, &[])
322+
.eval(
323+
&reorder_full_trace_for_precomp_foot_print(
324+
grand_product_exec_sumcheck_inner_evals.clone(),
325+
),
326+
&[],
327+
)
323328
}
324329
{
325330
return Err(ProofError::InvalidProof);

0 commit comments

Comments
 (0)