From db9b5917ae5784b5a1ae3b1f325600cc4a6e8665 Mon Sep 17 00:00:00 2001 From: kunxian xia Date: Tue, 27 Jan 2026 23:02:27 +0800 Subject: [PATCH 1/6] wip --- ceno_recursion/src/tower_verifier/program.rs | 150 ++++++------------- 1 file changed, 45 insertions(+), 105 deletions(-) diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index cf38b3f27..f4e236412 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -224,88 +224,59 @@ pub fn verify_tower_proof( let prod_spec_point_n_eval: Array> = builder.dyn_array(num_prod_spec.clone()); - iter_zip!(builder, prod_out_evals, prod_spec_point_n_eval).for_each(|ptr_vec, builder| { - let ptr = ptr_vec[0]; - let evals = builder.iter_ptr_get(&prod_out_evals, ptr); - let e = evaluate_at_point_degree_1(builder, &evals, &initial_rt); - let p_ptr = ptr_vec[1]; - builder.iter_ptr_set( - &prod_spec_point_n_eval, - p_ptr, - PointAndEvalVariable { - point: PointVariable { - fs: initial_rt.clone(), - }, - eval: e, - }, - ); - }); - let logup_spec_p_point_n_eval: Array> = builder.dyn_array(num_logup_spec.clone()); let logup_spec_q_point_n_eval: Array> = builder.dyn_array(num_logup_spec.clone()); - iter_zip!( - builder, - logup_out_evals, - logup_spec_p_point_n_eval, - logup_spec_q_point_n_eval - ) - .for_each(|ptr_vec, builder| { - let ptr = ptr_vec[0]; - let evals = builder.iter_ptr_get(&prod_out_evals, ptr); - - let p_slice = evals.slice(builder, 0, 2); - let q_slice = evals.slice(builder, 2, 4); - - let e1 = evaluate_at_point_degree_1(builder, &p_slice, &initial_rt); - let e2 = evaluate_at_point_degree_1(builder, &q_slice, &initial_rt); - - let p_ptr = ptr_vec[1]; - let q_ptr = ptr_vec[2]; - - builder.iter_ptr_set( - &logup_spec_p_point_n_eval, - p_ptr, - PointAndEvalVariable { - point: PointVariable { - fs: initial_rt.clone(), - }, - eval: e1, - }, - ); - builder.iter_ptr_set( - &logup_spec_q_point_n_eval, - q_ptr, - PointAndEvalVariable { - point: PointVariable { - fs: initial_rt.clone(), - }, - eval: e2, - }, + let next_layer_evals_output_len: Usize = builder + .eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone()); + let next_layer_evals: Array> = + builder.dyn_array(next_layer_evals_output_len); + let input_ctx: Array> = builder.dyn_array(NATIVE_SUMCHECK_CTX_LEN); + builder.set(&input_ctx, 0, Usize::from(0)); + builder.set(&input_ctx, 1, num_prod_spec.clone()); + builder.set(&input_ctx, 2, num_logup_spec.clone()); + builder.set( + &input_ctx, + 3, + Usize::from(proof.prod_specs_eval.inner_length), + ); + builder.set( + &input_ctx, + 4, + Usize::from(proof.prod_specs_eval.inner_inner_length), + ); + builder.set( + &input_ctx, + 5, + Usize::from(proof.logup_specs_eval.inner_length), + ); + builder.set( + &input_ctx, + 6, + Usize::from(proof.logup_specs_eval.inner_inner_length), + ); + let n_v = builder.get(&num_variables, 0); + builder.set(&input_ctx, 8, n_v); + // compute expected sum + builder.set(&input_ctx, 7, Usize::from(0)); + + let rt = builder.get(&initial_rt, 0); + let challenges: Array> = builder.dyn_array(3); + builder.set(&challenges, 0, alpha); + builder.set(&challenges, 1, one - rt); + builder.set(&challenges, 2, rt); + + builder.sumcheck_layer_eval( + &input_ctx, + &challenges, + &prod_out_evals,// TODO: convert from 2d array to 1d array + &logup_out_evals, + &next_layer_evals, ); - }); - let initial_claim: Ext = builder.eval(zero + zero); - iter_zip!(builder, prod_spec_point_n_eval).for_each(|ptr_vec, builder| { - let ptr = ptr_vec[0]; - let prod_eval = builder.iter_ptr_get(&prod_spec_point_n_eval, ptr); - builder.assign(&initial_claim, initial_claim + prod_eval.eval * alpha_acc); - builder.assign(&alpha_acc, alpha_acc * alpha); - }); - - builder - .range(0, num_logup_spec.clone()) - .for_each(|i_vec, builder| { - let p = builder.get(&logup_spec_p_point_n_eval, i_vec[0]); - builder.assign(&initial_claim, initial_claim + p.eval * alpha_acc); - builder.assign(&alpha_acc, alpha_acc * alpha); - let q = builder.get(&logup_spec_q_point_n_eval, i_vec[0]); - builder.assign(&initial_claim, initial_claim + q.eval * alpha_acc); - builder.assign(&alpha_acc, alpha_acc * alpha); - }); builder.cycle_tracker_end("initial sum"); let curr_pt = initial_rt.clone(); @@ -318,11 +289,6 @@ pub fn verify_tower_proof( eval: initial_claim, }; - let next_layer_evals_output_len: Usize = builder - .eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone()); - let next_layer_evals: Array> = - builder.dyn_array(next_layer_evals_output_len); - builder.range(0, op_range).for_each(|i_vec, builder| { let round_var = i_vec[0]; let out_rt = &curr_pt; @@ -349,35 +315,9 @@ pub fn verify_tower_proof( builder.cycle_tracker_start("check expected evaluation"); let eq_e = eq_eval(builder, out_rt, &sub_rt, one, zero); - let input_ctx: Array> = builder.dyn_array(NATIVE_SUMCHECK_CTX_LEN); builder.set(&input_ctx, 0, round_var); - builder.set(&input_ctx, 1, num_prod_spec.clone()); - builder.set(&input_ctx, 2, num_logup_spec.clone()); - builder.set( - &input_ctx, - 3, - Usize::from(proof.prod_specs_eval.inner_length), - ); - builder.set( - &input_ctx, - 4, - Usize::from(proof.prod_specs_eval.inner_inner_length), - ); - builder.set( - &input_ctx, - 5, - Usize::from(proof.logup_specs_eval.inner_length), - ); - builder.set( - &input_ctx, - 6, - Usize::from(proof.logup_specs_eval.inner_inner_length), - ); builder.set(&input_ctx, 7, Usize::from(1)); - let n_v = builder.get(&num_variables, 0); - builder.set(&input_ctx, 8, n_v); - let challenges: Array> = builder.dyn_array(3); builder.set(&challenges, 0, alpha); builder.sumcheck_layer_eval( From d26996367d1fb16e1c62ee882b61a7be61818706 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 27 Jan 2026 19:29:00 -0500 Subject: [PATCH 2/6] replace initial sum calculation with sumcheck --- .gitignore | 1 + ceno_recursion/src/tower_verifier/program.rs | 111 ++++++++++++------- 2 files changed, 70 insertions(+), 42 deletions(-) diff --git a/.gitignore b/.gitignore index c123c75a3..ab2d346ba 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,4 @@ docs/book # ceno serialized files *.bin *.json +*.srs diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index f4e236412..97e6fadbe 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -202,9 +202,7 @@ pub fn verify_tower_proof( transcript_observe_label(builder, challenger, b"combine subset evals"); let alpha = challenger.sample_ext(builder); - - let alpha_acc: Ext = builder.eval(zero + one); - + // initial_claim = \sum_j alpha^j * out_j[rt] // out_j[rt] := (record_{j}[rt]) // out_j[rt] := (logup_p{j}[rt]) @@ -223,58 +221,64 @@ pub fn verify_tower_proof( let prod_spec_point_n_eval: Array> = builder.dyn_array(num_prod_spec.clone()); - let logup_spec_p_point_n_eval: Array> = builder.dyn_array(num_logup_spec.clone()); let logup_spec_q_point_n_eval: Array> = builder.dyn_array(num_logup_spec.clone()); - let next_layer_evals_output_len: Usize = builder - .eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone()); - let next_layer_evals: Array> = - builder.dyn_array(next_layer_evals_output_len); + let initial_evals_len: Usize = + builder.eval(num_prod_spec.clone() + num_logup_spec.clone() + num_logup_spec.clone()); + let initial_evals = builder.dyn_array(initial_evals_len); + let prod_idx: Usize = builder.eval(C::N::ZERO); + let logup_idx: Usize = builder.eval(num_prod_spec.clone()); + builder + .range(0, prod_out_evals.len()) + .for_each(|idx_vec, builder| { + let evals = builder.get(&prod_out_evals, idx_vec[0]); + + let e = evaluate_at_point_degree_1(builder, &evals, &initial_rt); + builder.set(&initial_evals, prod_idx.clone(), e); + builder.assign(&prod_idx, prod_idx.clone() + C::N::ONE); + + let p_slice = evals.slice(builder, 0, 2); + let q_slice = evals.slice(builder, 2, 4); + + let e1 = evaluate_at_point_degree_1(builder, &p_slice, &initial_rt); + let e2 = evaluate_at_point_degree_1(builder, &q_slice, &initial_rt); + + builder.set(&initial_evals, logup_idx.clone(), e1); + builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); + builder.set(&initial_evals, logup_idx.clone(), e2); + builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); + }); + let input_ctx: Array> = builder.dyn_array(NATIVE_SUMCHECK_CTX_LEN); builder.set(&input_ctx, 0, Usize::from(0)); - builder.set(&input_ctx, 1, num_prod_spec.clone()); - builder.set(&input_ctx, 2, num_logup_spec.clone()); - builder.set( - &input_ctx, - 3, - Usize::from(proof.prod_specs_eval.inner_length), - ); - builder.set( - &input_ctx, - 4, - Usize::from(proof.prod_specs_eval.inner_inner_length), - ); - builder.set( - &input_ctx, - 5, - Usize::from(proof.logup_specs_eval.inner_length), - ); - builder.set( - &input_ctx, - 6, - Usize::from(proof.logup_specs_eval.inner_inner_length), - ); + builder.set(&input_ctx, 1, initial_evals.len()); + builder.set(&input_ctx, 2, Usize::from(0)); + builder.set(&input_ctx, 3, Usize::from(1)); + builder.set(&input_ctx, 4, Usize::from(1)); + builder.set(&input_ctx, 5, Usize::from(0)); + builder.set(&input_ctx, 6, Usize::from(0)); + builder.set(&input_ctx, 7, Usize::from(0)); let n_v = builder.get(&num_variables, 0); builder.set(&input_ctx, 8, n_v); - // compute expected sum - builder.set(&input_ctx, 7, Usize::from(0)); - let rt = builder.get(&initial_rt, 0); - let challenges: Array> = builder.dyn_array(3); + let challenges: Array> = builder.dyn_array(1); builder.set(&challenges, 0, alpha); - builder.set(&challenges, 1, one - rt); - builder.set(&challenges, 2, rt); + let next_layer_evals_output_len: Usize = builder + .eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone()); + let next_layer_evals: Array> = + builder.dyn_array(next_layer_evals_output_len); + let empty_logup_evals: Array> = builder.dyn_array(0); builder.sumcheck_layer_eval( - &input_ctx, - &challenges, - &prod_out_evals,// TODO: convert from 2d array to 1d array - &logup_out_evals, - &next_layer_evals, - ); + &input_ctx, + &challenges, + &initial_evals, + &empty_logup_evals, + &next_layer_evals, + ); let initial_claim: Ext = builder.eval(zero + zero); builder.cycle_tracker_end("initial sum"); @@ -316,8 +320,31 @@ pub fn verify_tower_proof( let eq_e = eq_eval(builder, out_rt, &sub_rt, one, zero); builder.set(&input_ctx, 0, round_var); + builder.set(&input_ctx, 1, num_prod_spec.clone()); + builder.set(&input_ctx, 2, num_logup_spec.clone()); + builder.set( + &input_ctx, + 3, + Usize::from(proof.prod_specs_eval.inner_length), + ); + builder.set( + &input_ctx, + 4, + Usize::from(proof.prod_specs_eval.inner_inner_length), + ); + builder.set( + &input_ctx, + 5, + Usize::from(proof.logup_specs_eval.inner_length), + ); + builder.set( + &input_ctx, + 6, + Usize::from(proof.logup_specs_eval.inner_inner_length), + ); builder.set(&input_ctx, 7, Usize::from(1)); + let challenges: Array> = builder.dyn_array(3); builder.set(&challenges, 0, alpha); builder.sumcheck_layer_eval( From 40873f1b988fa46488389bac6ffa9f8ef748cd69 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 27 Jan 2026 19:32:18 -0500 Subject: [PATCH 3/6] retrieve sum --- ceno_recursion/src/tower_verifier/program.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index 97e6fadbe..9af96deca 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -279,7 +279,7 @@ pub fn verify_tower_proof( &empty_logup_evals, &next_layer_evals, ); - let initial_claim: Ext = builder.eval(zero + zero); + let initial_claim: Ext = builder.get(&next_layer_evals, 0); builder.cycle_tracker_end("initial sum"); From add4ffbca9cdac06c5d52cc3b8f5771629b5f69a Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 27 Jan 2026 19:35:40 -0500 Subject: [PATCH 4/6] fmt --- ceno_recursion/src/tower_verifier/program.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index 9af96deca..35201eb10 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -202,7 +202,7 @@ pub fn verify_tower_proof( transcript_observe_label(builder, challenger, b"combine subset evals"); let alpha = challenger.sample_ext(builder); - + // initial_claim = \sum_j alpha^j * out_j[rt] // out_j[rt] := (record_{j}[rt]) // out_j[rt] := (logup_p{j}[rt]) From c11df595d17cb92a18ca184fa9c5f2371331e13b Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 27 Jan 2026 19:54:33 -0500 Subject: [PATCH 5/6] correct mode --- ceno_recursion/src/tower_verifier/program.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index 35201eb10..97d9a47fc 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -260,7 +260,7 @@ pub fn verify_tower_proof( builder.set(&input_ctx, 4, Usize::from(1)); builder.set(&input_ctx, 5, Usize::from(0)); builder.set(&input_ctx, 6, Usize::from(0)); - builder.set(&input_ctx, 7, Usize::from(0)); + builder.set(&input_ctx, 7, Usize::from(1)); let n_v = builder.get(&num_variables, 0); builder.set(&input_ctx, 8, n_v); From ce90ee5e6d2efe9a2a8001e468bb1013e228a9a1 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 27 Jan 2026 20:18:08 -0500 Subject: [PATCH 6/6] adjust sumcheck --- ceno_recursion/src/tower_verifier/program.rs | 26 ++++++++++++++------ 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/ceno_recursion/src/tower_verifier/program.rs b/ceno_recursion/src/tower_verifier/program.rs index 97d9a47fc..71d1a70db 100644 --- a/ceno_recursion/src/tower_verifier/program.rs +++ b/ceno_recursion/src/tower_verifier/program.rs @@ -226,11 +226,19 @@ pub fn verify_tower_proof( let logup_spec_q_point_n_eval: Array> = builder.dyn_array(num_logup_spec.clone()); - let initial_evals_len: Usize = - builder.eval(num_prod_spec.clone() + num_logup_spec.clone() + num_logup_spec.clone()); + let input_ctx: Array> = builder.dyn_array(NATIVE_SUMCHECK_CTX_LEN); + builder.set(&input_ctx, 0, Usize::from(0)); + builder.set( + &input_ctx, + 1, + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone(), + ); + + let initial_evals_len: Usize = builder + .eval(Usize::from(2) * (num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone())); let initial_evals = builder.dyn_array(initial_evals_len); let prod_idx: Usize = builder.eval(C::N::ZERO); - let logup_idx: Usize = builder.eval(num_prod_spec.clone()); + let logup_idx: Usize = builder.eval(num_prod_spec.clone() * Usize::from(2)); builder .range(0, prod_out_evals.len()) .for_each(|idx_vec, builder| { @@ -239,6 +247,8 @@ pub fn verify_tower_proof( let e = evaluate_at_point_degree_1(builder, &evals, &initial_rt); builder.set(&initial_evals, prod_idx.clone(), e); builder.assign(&prod_idx, prod_idx.clone() + C::N::ONE); + builder.set(&initial_evals, prod_idx.clone(), C::F::ONE); + builder.assign(&prod_idx, prod_idx.clone() + C::N::ONE); let p_slice = evals.slice(builder, 0, 2); let q_slice = evals.slice(builder, 2, 4); @@ -248,16 +258,16 @@ pub fn verify_tower_proof( builder.set(&initial_evals, logup_idx.clone(), e1); builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); + builder.set(&initial_evals, logup_idx.clone(), C::F::ONE); + builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); builder.set(&initial_evals, logup_idx.clone(), e2); builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); + builder.set(&initial_evals, logup_idx.clone(), C::F::ONE); + builder.assign(&logup_idx, logup_idx.clone() + C::N::ONE); }); - - let input_ctx: Array> = builder.dyn_array(NATIVE_SUMCHECK_CTX_LEN); - builder.set(&input_ctx, 0, Usize::from(0)); - builder.set(&input_ctx, 1, initial_evals.len()); builder.set(&input_ctx, 2, Usize::from(0)); builder.set(&input_ctx, 3, Usize::from(1)); - builder.set(&input_ctx, 4, Usize::from(1)); + builder.set(&input_ctx, 4, Usize::from(2)); builder.set(&input_ctx, 5, Usize::from(0)); builder.set(&input_ctx, 6, Usize::from(0)); builder.set(&input_ctx, 7, Usize::from(1));