@@ -7,6 +7,7 @@ use crate::tower_verifier::binding::IOPProverMessageVecVariable;
77use crate :: transcript:: transcript_observe_label;
88use crate :: zkvm_verifier:: binding:: TowerProofInputVariable ;
99use ceno_zkvm:: scheme:: constants:: NUM_FANIN ;
10+ use itertools:: izip;
1011use openvm_native_compiler:: prelude:: * ;
1112use openvm_native_compiler_derive:: iter_zip;
1213use openvm_native_recursion:: challenger:: {
@@ -318,6 +319,9 @@ pub fn verify_tower_proof<C: Config>(
318319 eval : initial_claim,
319320 } ;
320321
322+ 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 ( ) ) ;
323+ let next_layer_evals: Array < C , Ext < C :: F , C :: EF > > = builder. dyn_array ( next_layer_evals_output_len) ;
324+
321325 builder
322326 . range ( 0 , op_range. clone ( ) )
323327 . for_each ( |i_vec, builder| {
@@ -452,8 +456,7 @@ pub fn verify_tower_proof<C: Config>(
452456 builder. assert_ext_eq ( expected_evaluation, sub_e) ;
453457 builder. cycle_tracker_end ( "check expected evaluation" ) ;
454458
455- // _debug
456- // builder.cycle_tracker_start("derive next layer's expected sum");
459+ builder. cycle_tracker_start ( "derive next layer's expected sum" ) ;
457460 // derive single eval
458461 // rt' = r_merge || rt
459462 // r_merge.len() == ceil_log2(num_product_fanin)
@@ -465,7 +468,6 @@ pub fn verify_tower_proof<C: Config>(
465468
466469 let c1: Ext < <C as Config >:: F , <C as Config >:: EF > = builder. eval ( one - r_merge. clone ( ) ) ;
467470 let c2: Ext < <C as Config >:: F , <C as Config >:: EF > = builder. eval ( r_merge. clone ( ) ) ;
468- let coeffs = vec ! [ c1, c2] ;
469471
470472 let rt_prime = extend ( builder, & sub_rt, & r_merge) ;
471473 // _debug
@@ -477,39 +479,50 @@ pub fn verify_tower_proof<C: Config>(
477479 builder. assign ( & alpha, new_alpha) ;
478480 builder. assign ( & alpha_acc, zero + one) ;
479481
480- let next_round = builder. eval_expr ( round_var + RVar :: from ( 1 ) ) ;
482+ // Use native opcode
483+ // [round_var, num_prod_spec, num_logup_spec, num_variables]
484+ let input_ctx_len: Usize < C :: N > = Usize :: Var ( builder. uninit ( ) ) ;
485+ builder. assign ( & input_ctx_len, Usize :: from ( 8 ) + num_variables_len. clone ( ) ) ;
486+ let input_ctx: Array < C , Usize < C :: N > > = builder. dyn_array ( input_ctx_len) ;
487+
488+ builder. set ( & input_ctx, 0 , round_var) ;
489+ builder. set ( & input_ctx, 1 , num_prod_spec. clone ( ) ) ;
490+ builder. set ( & input_ctx, 2 , num_logup_spec. clone ( ) ) ;
491+ builder. set ( & input_ctx, 3 , Usize :: from ( proof. prod_specs_eval . inner_length ) ) ;
492+ builder. set ( & input_ctx, 4 , Usize :: from ( proof. prod_specs_eval . inner_inner_length ) ) ;
493+ builder. set ( & input_ctx, 5 , Usize :: from ( proof. logup_specs_eval . inner_length ) ) ;
494+ builder. set ( & input_ctx, 6 , Usize :: from ( proof. logup_specs_eval . inner_inner_length ) ) ;
495+
496+ let input_ctx_variables_slice = input_ctx. slice ( builder, 8 , input_ctx. len ( ) ) ;
497+ iter_zip ! ( builder, input_ctx_variables_slice, num_variables) . for_each ( |ptr_vec, builder| {
498+ let n_v = builder. iter_ptr_get ( & num_variables, ptr_vec[ 1 ] ) ;
499+ builder. iter_ptr_set ( & input_ctx_variables_slice, ptr_vec[ 0 ] , n_v) ;
500+ } ) ;
501+
502+ let challenges: Array < C , Ext < C :: F , C :: EF > > = builder. dyn_array ( 3 ) ;
503+ builder. set ( & challenges, 0 , alpha. clone ( ) ) ;
504+ builder. set ( & challenges, 1 , c1. clone ( ) ) ;
505+ builder. set ( & challenges, 2 , c2. clone ( ) ) ;
506+
507+ builder. sumcheck_layer_eval ( input_ctx, challenges, & proof. prod_specs_eval . data , & proof. logup_specs_eval . data , & next_layer_evals) ;
481508
482- let next_prod_spec_evals: Ext < <C as Config >:: F , <C as Config >:: EF > =
483- builder. eval ( zero + zero) ; // simple trick to avoid AddEI
509+ let next_round = builder. eval_expr ( round_var + RVar :: from ( 1 ) ) ;
484510 builder
485511 . range ( 0 , num_prod_spec. clone ( ) )
486512 . for_each ( |i_vec, builder| {
487- // _debug
488- // builder.cycle_tracker_start("derive next layer for prod specs");
489513 let spec_index = i_vec[ 0 ] ;
490514 let skip = builder. get ( & should_skip, spec_index. clone ( ) ) ;
491515 let max_round = builder. get ( & num_variables, spec_index. clone ( ) ) ;
492516 let round_limit: RVar < C :: N > = builder. eval_expr ( max_round - RVar :: from ( 1 ) ) ;
493517
494518 // now skip is 0 if and only if current round_var is smaller than round_limit.
495519 builder. if_eq ( skip, var_zero. clone ( ) ) . then ( |builder| {
496- let prod_round_slice = proof. prod_specs_eval . get_inner (
497- builder,
498- spec_index. variable ( ) ,
499- round_var. variable ( ) ,
500- ) ;
501- let evals = fixed_dot_product ( builder, & coeffs, & prod_round_slice, zero) ;
502-
503- builder. if_ne ( next_round, round_limit) . then_or_else (
504- |builder| {
505- let new_subsum: Ext < C :: F , C :: EF > = builder. eval ( evals * alpha_acc) ;
506- builder. assign (
507- & next_prod_spec_evals,
508- next_prod_spec_evals + new_subsum,
509- ) ;
510- } ,
511- // update point and eval only for last layer
520+
521+ builder. if_eq ( next_round, round_limit) . then (
512522 |builder| {
523+ let evals_idx: Usize < C :: N > = builder. eval ( spec_index + Usize :: from ( 1 ) ) ;
524+ let evals = builder. get ( & next_layer_evals, evals_idx) ;
525+
513526 let point_and_eval: PointAndEvalVariable < C > =
514527 builder. eval ( PointAndEvalVariable {
515528 point : PointVariable {
@@ -522,67 +535,33 @@ pub fn verify_tower_proof<C: Config>(
522535 spec_index,
523536 point_and_eval,
524537 ) ;
525- } ,
538+ }
526539 ) ;
527540 } ) ;
528-
529- builder. assign ( & alpha_acc, alpha_acc * alpha. clone ( ) ) ;
530- // _debug
531- // builder.cycle_tracker_end("derive next layer for prod specs");
532541 } ) ;
533542
534- let next_logup_spec_evals: Ext < <C as Config >:: F , <C as Config >:: EF > =
535- builder. eval ( zero + zero) ;
536543 let logup_num_variables_slice =
537544 num_variables. slice ( builder, num_prod_spec. clone ( ) , num_variables_len. clone ( ) ) ;
538545
539546 builder
540547 . range ( 0 , num_logup_spec. clone ( ) )
541548 . for_each ( |i_vec, builder| {
542- // _debug
543- // builder.cycle_tracker_start("derive next layer for logup specs");
544549 let spec_index = i_vec[ 0 ] ;
545550 let max_round = builder. get ( & logup_num_variables_slice, spec_index) ;
546551 let round_limit: RVar < C :: N > = builder. eval_expr ( max_round - RVar :: from ( 1 ) ) ;
547552 let idx: Var < C :: N > =
548553 builder. eval ( spec_index. variable ( ) + num_prod_spec. get_var ( ) ) ;
549554 let skip = builder. get ( & should_skip, idx) ;
550555
551- let alpha_numerator: Ext < C :: F , C :: EF > = builder. eval ( alpha_acc * one) ;
552- builder. assign ( & alpha_acc, alpha_acc * alpha. clone ( ) ) ;
553- let alpha_denominator: Ext < C :: F , C :: EF > = builder. eval ( alpha_acc * one) ;
554- builder. assign ( & alpha_acc, alpha_acc * alpha. clone ( ) ) ;
555-
556556 // now skip is 0 if and only if current round_var is smaller than round_limit.
557557 builder. if_eq ( skip, var_zero) . then ( |builder| {
558- let prod_round_slice = proof. logup_specs_eval . get_inner (
559- builder,
560- spec_index. variable ( ) ,
561- round_var. variable ( ) ,
562- ) ;
563- let p1 = builder. get ( & prod_round_slice, 0 ) ;
564- let p2 = builder. get ( & prod_round_slice, 1 ) ;
565- let q1 = builder. get ( & prod_round_slice, 2 ) ;
566- let q2 = builder. get ( & prod_round_slice, 3 ) ;
567-
568- let p_eval: Ext < <C as Config >:: F , <C as Config >:: EF > =
569- builder. eval ( zero + zero) ;
570- let q_eval: Ext < <C as Config >:: F , <C as Config >:: EF > =
571- builder. eval ( zero + zero) ;
572- builder. assign ( & p_eval, p1 * coeffs[ 0 ] + p2 * coeffs[ 1 ] ) ;
573- builder. assign ( & q_eval, q1 * coeffs[ 0 ] + q2 * coeffs[ 1 ] ) ;
574-
575- builder. if_ne ( next_round, round_limit) . then_or_else (
576- |builder| {
577- builder. assign (
578- & next_logup_spec_evals,
579- next_logup_spec_evals
580- + alpha_numerator * p_eval
581- + alpha_denominator * q_eval,
582- ) ;
583- } ,
584- // update point and eval only for last layer
558+ builder. if_eq ( next_round, round_limit) . then (
585559 |builder| {
560+ let p_idx: Usize < C :: N > = builder. eval ( idx + Usize :: from ( 1 ) ) ;
561+ let q_idx: Usize < C :: N > = builder. eval ( idx + Usize :: from ( 1 ) + num_logup_spec. clone ( ) ) ;
562+ let p_eval = builder. get ( & next_layer_evals, p_idx) ;
563+ let q_eval = builder. get ( & next_layer_evals, q_idx) ;
564+
586565 let p_eval: PointAndEvalVariable < C > =
587566 builder. eval ( PointAndEvalVariable {
588567 point : PointVariable {
@@ -599,19 +578,17 @@ pub fn verify_tower_proof<C: Config>(
599578 } ) ;
600579 builder. set_value ( & logup_spec_p_point_n_eval, spec_index, p_eval) ;
601580 builder. set_value ( & logup_spec_q_point_n_eval, spec_index, q_eval) ;
602- } ,
581+ }
603582 ) ;
604583 } ) ;
605- // _debug
606- // builder.cycle_tracker_end("derive next layer for logup specs");
607584 } ) ;
608585
586+ let output_eval = builder. get ( & next_layer_evals, 0 ) ;
609587 builder. assign ( & curr_pt, rt_prime. clone ( ) ) ;
610- builder. assign ( & curr_eval, next_prod_spec_evals + next_logup_spec_evals ) ;
588+ builder. assign ( & curr_eval, output_eval ) ;
611589 builder. assign ( & round, round + C :: F :: ONE ) ;
612590
613- // _debug
614- // builder.cycle_tracker_end("derive next layer's expected sum");
591+ builder. cycle_tracker_end ( "derive next layer's expected sum" ) ;
615592
616593 builder. assign (
617594 & next_rt,
0 commit comments