@@ -4,8 +4,7 @@ use super::binding::{
44} ;
55use crate :: {
66 arithmetics:: {
7- PolyEvaluator , UniPolyExtrapolator , challenger_multi_observe, eq_eval,
8- eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse,
7+ PolyEvaluator , UniPolyExtrapolator , challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse
98 } ,
109 basefold_verifier:: {
1110 basefold:: { BasefoldCommitmentVariable , RoundOpeningVariable , RoundVariable } ,
@@ -112,13 +111,6 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
112111 challenger_multi_observe ( builder, & mut challenger, & v) ;
113112 } ) ;
114113
115- // _debug
116- // check shard id
117- // assert_eq!(
118- // vm_proof.raw_pi[SHARD_ID_IDX],
119- // vec![E::BaseField::from_canonical_usize(shard_id)]
120- // );
121-
122114 iter_zip ! ( builder, zkvm_proof_input. raw_pi, zkvm_proof_input. pi_evals) . for_each (
123115 |ptr_vec, builder| {
124116 let raw = builder. iter_ptr_get ( & zkvm_proof_input. raw_pi , ptr_vec[ 0 ] ) ;
@@ -381,7 +373,9 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
381373 builder. assign ( & prod_w, prod_w * w_out_evals_prod) ;
382374
383375 builder. inc ( & num_chips_verified) ;
384- add_septic_points_in_place ( builder, & shard_ec_sum, & chip_shard_ec_sum) ;
376+ builder. if_ne ( chip_shard_ec_sum. is_infinity . clone ( ) , Usize :: from ( 1 ) ) . then ( |builder| {
377+ add_septic_points_in_place ( builder, & shard_ec_sum, & chip_shard_ec_sum) ;
378+ } ) ;
385379 } ) ;
386380 }
387381 builder. assert_eq :: < Usize < _ > > ( num_chips_verified, chip_indices. len ( ) ) ;
@@ -556,29 +550,9 @@ pub fn verify_chip_proof<C: Config>(
556550 is_infinity : Usize :: uninit ( builder) ,
557551 } ;
558552
559- // _debug
560553 if composed_cs. has_ecc_ops ( ) {
561554 builder. assert_nonzero ( & chip_proof. has_ecc_proof ) ;
562555 let ecc_proof = & chip_proof. ecc_proof ;
563-
564- // let expected_septic_xy = cs
565- // .ec_final_sum
566- // .iter()
567- // .map(|expr| {
568- // eval_by_expr_with_instance(&[], &[], &[], pi, challenges, expr)
569- // .right()
570- // .and_then(|v| v.as_base())
571- // .unwrap()
572- // })
573- // .collect_vec();
574- // let expected_septic_x: SepticExtension<E::BaseField> =
575- // expected_septic_xy[0..SEPTIC_EXTENSION_DEGREE].into();
576- // let expected_septic_y: SepticExtension<E::BaseField> =
577- // expected_septic_xy[SEPTIC_EXTENSION_DEGREE..].into();
578-
579- // assert_eq!(&ecc_proof.sum.x, &expected_septic_x);
580- // assert_eq!(&ecc_proof.sum.y, &expected_septic_y);
581-
582556 builder. assert_usize_eq ( ecc_proof. sum . is_infinity . clone ( ) , Usize :: from ( 0 ) ) ;
583557 verify_ecc_proof ( builder, challenger, ecc_proof, unipoly_extrapolator) ;
584558 builder. assign ( & shard_ec_sum, ecc_proof. sum . clone ( ) ) ;
@@ -814,9 +788,13 @@ pub fn verify_gkr_circuit<C: Config>(
814788 & layer_challenges,
815789 & layer_proof. has_rotation ,
816790 ) ;
817- // _debug
818- // builder.assert_usize_eq(Usize::from(layer.out_sel_and_eval_exprs.len()), eval_and_dedup_points.len());
819791
792+ if layer. rotation_sumcheck_expression . is_some ( ) {
793+ builder. assert_usize_eq ( Usize :: from ( layer. out_sel_and_eval_exprs . len ( ) + 3 ) , eval_and_dedup_points. len ( ) ) ;
794+ } else {
795+ builder. assert_usize_eq ( Usize :: from ( layer. out_sel_and_eval_exprs . len ( ) ) , eval_and_dedup_points. len ( ) ) ;
796+ }
797+
820798 // ZeroCheckLayer verification (might include other layer types in the future)
821799 let LayerProofVariable {
822800 main :
@@ -2190,48 +2168,54 @@ pub fn add_septic_points_in_place<C: Config>(
21902168 left : & SepticPointVariable < C > ,
21912169 right : & SepticPointVariable < C > ,
21922170) {
2193- builder
2194- . if_ne ( right. is_infinity . clone ( ) , Usize :: from ( 1 ) )
2195- . then ( |builder| {
2196- let x_diff = septic_ext_sub ( builder, & right. x , & left. x ) ;
2197- let y_diff = septic_ext_sub ( builder, & right. y , & left. y ) ;
2198- let is_x_same = x_diff. is_zero ( builder) ;
2171+ builder. if_eq ( left. is_infinity . clone ( ) , Usize :: from ( 1 ) ) . then_or_else ( |builder| {
2172+ builder. assign ( & left. x , right. x . clone ( ) ) ;
2173+ builder. assign ( & left. y , right. y . clone ( ) ) ;
2174+ builder. assign ( & left. is_infinity , right. is_infinity . clone ( ) ) ;
2175+ } , |builder| {
2176+ builder
2177+ . if_ne ( right. is_infinity . clone ( ) , Usize :: from ( 1 ) )
2178+ . then ( |builder| {
2179+ let x_diff = septic_ext_sub ( builder, & right. x , & left. x ) ;
2180+ let y_diff = septic_ext_sub ( builder, & right. y , & left. y ) ;
2181+ let is_x_same = x_diff. is_zero ( builder) ;
21992182
2200- builder. if_eq ( is_x_same, Usize :: from ( 1 ) ) . then_or_else (
2201- |builder| {
2202- let is_y_same = y_diff. is_zero ( builder) ;
2183+ builder. if_eq ( is_x_same, Usize :: from ( 1 ) ) . then_or_else (
2184+ |builder| {
2185+ let is_y_same = y_diff. is_zero ( builder) ;
22032186
2204- builder. if_eq ( is_y_same, Usize :: from ( 1 ) ) . then_or_else (
2205- |builder| {
2206- double_septic_points_in_place ( builder, left) ;
2207- } ,
2208- |builder| {
2209- let y_sum = septic_ext_add ( builder, & right. y , & left. y ) ;
2210- let is_y_sum_zero = y_sum. is_zero ( builder) ;
2211- builder. assert_usize_eq ( is_y_sum_zero, Usize :: from ( 1 ) ) ;
2212- let zero_ext_arr: Array < C , Ext < C :: F , C :: EF > > =
2213- builder. dyn_array ( SEPTIC_EXTENSION_DEGREE ) ;
2214- builder. assign ( & left. x , zero_ext_arr. clone ( ) ) ;
2215- builder. assign ( & left. y , zero_ext_arr. clone ( ) ) ;
2216- builder. assign ( & left. is_infinity , Usize :: from ( 1 ) ) ;
2217- } ,
2218- ) ;
2219- } ,
2220- |builder| {
2221- let x_diff_inv = invert ( builder, & x_diff) ;
2222- let slope = septic_ext_mul ( builder, & y_diff, & x_diff_inv) ;
2187+ builder. if_eq ( is_y_same, Usize :: from ( 1 ) ) . then_or_else (
2188+ |builder| {
2189+ double_septic_points_in_place ( builder, left) ;
2190+ } ,
2191+ |builder| {
2192+ let y_sum = septic_ext_add ( builder, & right. y , & left. y ) ;
2193+ let is_y_sum_zero = y_sum. is_zero ( builder) ;
2194+ builder. assert_usize_eq ( is_y_sum_zero, Usize :: from ( 1 ) ) ;
2195+ let zero_ext_arr: Array < C , Ext < C :: F , C :: EF > > =
2196+ builder. dyn_array ( SEPTIC_EXTENSION_DEGREE ) ;
2197+ builder. assign ( & left. x , zero_ext_arr. clone ( ) ) ;
2198+ builder. assign ( & left. y , zero_ext_arr. clone ( ) ) ;
2199+ builder. assign ( & left. is_infinity , Usize :: from ( 1 ) ) ;
2200+ } ,
2201+ ) ;
2202+ } ,
2203+ |builder| {
2204+ let x_diff_inv = invert ( builder, & x_diff) ;
2205+ let slope = septic_ext_mul ( builder, & y_diff, & x_diff_inv) ;
22232206
2224- let x_sum = septic_ext_add ( builder, & right. x , & left. x ) ;
2225- let slope_squared = septic_ext_squared ( builder, & slope) ;
2226- let x = septic_ext_sub ( builder, & slope_squared, & x_sum) ;
2207+ let x_sum = septic_ext_add ( builder, & right. x , & left. x ) ;
2208+ let slope_squared = septic_ext_squared ( builder, & slope) ;
2209+ let x = septic_ext_sub ( builder, & slope_squared, & x_sum) ;
22272210
2228- let slope_mul_x_diff = septic_ext_mul ( builder, & slope, & x_diff) ;
2229- let y = septic_ext_sub ( builder, & slope_mul_x_diff, & left. y ) ;
2211+ let slope_mul_x_diff = septic_ext_mul ( builder, & slope, & x_diff) ;
2212+ let y = septic_ext_sub ( builder, & slope_mul_x_diff, & left. y ) ;
22302213
2231- builder. assign ( & left. x , x) ;
2232- builder. assign ( & left. y , y) ;
2233- builder. assign ( & left. is_infinity , Usize :: from ( 0 ) ) ;
2234- } ,
2235- ) ;
2236- } ) ;
2214+ builder. assign ( & left. x , x) ;
2215+ builder. assign ( & left. y , y) ;
2216+ builder. assign ( & left. is_infinity , Usize :: from ( 0 ) ) ;
2217+ } ,
2218+ ) ;
2219+ } ) ;
2220+ } ) ;
22372221}
0 commit comments