Skip to content

feat(recursion): cycle reduction #1245

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
kunxian-xia wants to merge 6 commits into from
Closed

feat(recursion): cycle reduction #1245

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
db9b591
wip
kunxian-xia Jan 27, 2026
d269963
replace initial sum calculation with sumcheck
darth-cy Jan 28, 2026
40873f1
retrieve sum
darth-cy Jan 28, 2026
add4ffb
fmt
darth-cy Jan 28, 2026
c11df59
correct mode
darth-cy Jan 28, 2026
ce90ee5
adjust sumcheck
darth-cy Jan 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,3 +15,4 @@ docs/book
# ceno serialized files
*.bin
*.json
*.srs
147 changes: 62 additions & 85 deletions ceno_recursion/src/tower_verifier/program.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,8 +203,6 @@ pub fn verify_tower_proof<C: Config>(
transcript_observe_label(builder, challenger, b"combine subset evals");
let alpha = challenger.sample_ext(builder);

let alpha_acc: Ext<C::F, C::EF> = 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])
Expand All @@ -223,89 +221,76 @@ pub fn verify_tower_proof<C: Config>(

let prod_spec_point_n_eval: Array<C, PointAndEvalVariable<C>> =
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<C, PointAndEvalVariable<C>> =
builder.dyn_array(num_logup_spec.clone());
let logup_spec_q_point_n_eval: Array<C, PointAndEvalVariable<C>> =
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 initial_claim: Ext<C::F, C::EF> = 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);
});
let input_ctx: Array<C, Usize<C::N>> = 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<C::N> = 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<C::N> = builder.eval(C::N::ZERO);
let logup_idx: Usize<C::N> = builder.eval(num_prod_spec.clone() * Usize::from(2));
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);
.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);
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);

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(), 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);
});
builder.set(&input_ctx, 2, Usize::from(0));
builder.set(&input_ctx, 3, 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));
let n_v = builder.get(&num_variables, 0);
builder.set(&input_ctx, 8, n_v);

let challenges: Array<C, Ext<C::F, C::EF>> = builder.dyn_array(1);
builder.set(&challenges, 0, alpha);

let next_layer_evals_output_len: Usize<C::N> = builder
.eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone());
let next_layer_evals: Array<C, Ext<C::F, C::EF>> =
builder.dyn_array(next_layer_evals_output_len);
let empty_logup_evals: Array<C, Ext<C::F, C::EF>> = builder.dyn_array(0);
builder.sumcheck_layer_eval(
&input_ctx,
&challenges,
&initial_evals,
&empty_logup_evals,
&next_layer_evals,
);
let initial_claim: Ext<C::F, C::EF> = builder.get(&next_layer_evals, 0);

builder.cycle_tracker_end("initial sum");

let curr_pt = initial_rt.clone();
Expand All @@ -318,11 +303,6 @@ pub fn verify_tower_proof<C: Config>(
eval: initial_claim,
};

let next_layer_evals_output_len: Usize<C::N> = builder
.eval(Usize::from(1) + num_prod_spec.clone() + Usize::from(2) * num_logup_spec.clone());
let next_layer_evals: Array<C, Ext<C::F, C::EF>> =
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;
Expand All @@ -349,7 +329,6 @@ pub fn verify_tower_proof<C: Config>(
builder.cycle_tracker_start("check expected evaluation");
let eq_e = eq_eval(builder, out_rt, &sub_rt, one, zero);

let input_ctx: Array<C, Usize<C::N>> = 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());
Expand All @@ -374,8 +353,6 @@ pub fn verify_tower_proof<C: Config>(
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<C, Ext<C::F, C::EF>> = builder.dyn_array(3);
builder.set(&challenges, 0, alpha);
Expand Down
Loading