Skip to content

Commit bfedf5f

Browse files
darth-cydarth-cy
committed
Correct assertions
1 parent 4cc787c commit bfedf5f

File tree

3 files changed

+87
-61
lines changed

3 files changed

+87
-61
lines changed

‎ceno_recursion/src/aggregation/mod.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -540,7 +540,7 @@ mod tests {
540540
}
541541

542542
#[test]
543-
// #[ignore = "need to generate proof first"]
543+
#[ignore = "need to generate proof first"]
544544
pub fn test_single() {
545545
let stack_size = 256 * 1024 * 1024; // 64 MB
546546

@@ -553,7 +553,7 @@ mod tests {
553553
}
554554

555555
#[test]
556-
// #[ignore = "need to generate proof first"]
556+
#[ignore = "need to generate proof first"]
557557
pub fn test_single_rust_verifier() {
558558
let stack_size = 256 * 1024 * 1024; // 64 MB
559559

‎ceno_recursion/src/arithmetics/mod.rs‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use ceno_zkvm::structs::{ChallengeId, WitnessId};
66
use ff_ext::{BabyBearExt4, ExtensionField, SmallField};
77
use itertools::Either;
88
use multilinear_extensions::{Expression, Fixed, Instance};
9+
use openvm_native_circuit::EXT_DEG;
910
use openvm_native_compiler::prelude::*;
1011
use openvm_native_compiler_derive::iter_zip;
1112
use openvm_native_recursion::challenger::{FeltChallenger, duplex::DuplexChallengerVariable};
@@ -34,6 +35,20 @@ pub fn _print_usize_arr<C: Config>(builder: &mut Builder<C>, arr: &Array<C, Usiz
3435
});
3536
}
3637

38+
pub fn assert_ext_arr_eq<C: Config>(
39+
builder: &mut Builder<C>,
40+
arr1: &Array<C, Ext<C::F, C::EF>>,
41+
arr2: &Array<C, Ext<C::F, C::EF>>,
42+
) {
43+
let zero: Ext<C::F, C::EF> = builder.constant(C::EF::ZERO);
44+
iter_zip!(builder, arr1, arr2).for_each(|ptr_vec, builder| {
45+
let e1 = builder.iter_ptr_get(arr1, ptr_vec[0]);
46+
let e2 = builder.iter_ptr_get(arr2, ptr_vec[0]);
47+
let diff: Ext<C::F, C::EF> = builder.eval(e1 - e2);
48+
builder.assert_ext_eq(diff, zero);
49+
});
50+
}
51+
3752
pub unsafe fn exts_to_felts<C: Config>(
3853
builder: &mut Builder<C>,
3954
exts: &Array<C, Ext<C::F, C::EF>>,

‎ceno_recursion/src/zkvm_verifier/verifier.rs‎

Lines changed: 70 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@ use super::binding::{
44
};
55
use crate::{
66
arithmetics::{
7-
PolyEvaluator, UniPolyExtrapolator, challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse
7+
PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, challenger_multi_observe, eq_eval,
8+
eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse,
89
},
910
basefold_verifier::{
1011
basefold::{BasefoldCommitmentVariable, RoundOpeningVariable, RoundVariable},
@@ -373,9 +374,11 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
373374
builder.assign(&prod_w, prod_w * w_out_evals_prod);
374375

375376
builder.inc(&num_chips_verified);
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-
});
377+
builder
378+
.if_ne(chip_shard_ec_sum.is_infinity.clone(), Usize::from(1))
379+
.then(|builder| {
380+
add_septic_points_in_place(builder, &shard_ec_sum, &chip_shard_ec_sum);
381+
});
379382
});
380383
}
381384
builder.assert_eq::<Usize<_>>(num_chips_verified, chip_indices.len());
@@ -595,13 +598,6 @@ pub fn verify_chip_proof<C: Config>(
595598
});
596599
}
597600

598-
// _debug: constraint
599-
// debug_assert!(
600-
// chain!(&record_evals, &logup_p_evals, &logup_q_evals)
601-
// .map(|e| &e.point)
602-
// .all_equal()
603-
// );
604-
605601
let num_rw_records: Usize<C::N> = builder.eval(r_counts_per_instance + w_counts_per_instance);
606602
builder.assert_usize_eq(record_evals.len(), num_rw_records.clone());
607603
builder.assert_usize_eq(logup_p_evals.len(), lk_counts_per_instance.clone());
@@ -790,11 +786,17 @@ pub fn verify_gkr_circuit<C: Config>(
790786
);
791787

792788
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());
789+
builder.assert_usize_eq(
790+
Usize::from(layer.out_sel_and_eval_exprs.len() + 3),
791+
eval_and_dedup_points.len(),
792+
);
794793
} else {
795-
builder.assert_usize_eq(Usize::from(layer.out_sel_and_eval_exprs.len()), eval_and_dedup_points.len());
794+
builder.assert_usize_eq(
795+
Usize::from(layer.out_sel_and_eval_exprs.len()),
796+
eval_and_dedup_points.len(),
797+
);
796798
}
797-
799+
798800
// ZeroCheckLayer verification (might include other layer types in the future)
799801
let LayerProofVariable {
800802
main:
@@ -1532,8 +1534,12 @@ pub fn evaluate_gkr_expression<C: Config>(
15321534

15331535
assert_eq!(parts.len(), 1 << indices.len());
15341536

1535-
// _debug
1536-
// assert!(parts.iter().all(|part| part.point == parts[0].point));
1537+
if !parts.is_empty() {
1538+
let first_pt = parts[0].point.fs.clone();
1539+
for pt_eval in parts.iter().skip(1) {
1540+
assert_ext_arr_eq(builder, &first_pt, &pt_eval.point.fs);
1541+
}
1542+
}
15371543

15381544
// FIXME: this is WRONG. we should use builder.dyn_array();
15391545
let mut new_point: Vec<Ext<C::F, C::EF>> = vec![];
@@ -2168,54 +2174,59 @@ pub fn add_septic_points_in_place<C: Config>(
21682174
left: &SepticPointVariable<C>,
21692175
right: &SepticPointVariable<C>,
21702176
) {
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);
2182-
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);
2177+
builder
2178+
.if_eq(left.is_infinity.clone(), Usize::from(1))
2179+
.then_or_else(
2180+
|builder| {
2181+
builder.assign(&left.x, right.x.clone());
2182+
builder.assign(&left.y, right.y.clone());
2183+
builder.assign(&left.is_infinity, right.is_infinity.clone());
2184+
},
2185+
|builder| {
2186+
builder
2187+
.if_ne(right.is_infinity.clone(), Usize::from(1))
2188+
.then(|builder| {
2189+
let x_diff = septic_ext_sub(builder, &right.x, &left.x);
2190+
let y_diff = septic_ext_sub(builder, &right.y, &left.y);
2191+
let is_x_same = x_diff.is_zero(builder);
21862192

2187-
builder.if_eq(is_y_same, Usize::from(1)).then_or_else(
2193+
builder.if_eq(is_x_same, Usize::from(1)).then_or_else(
21882194
|builder| {
2189-
double_septic_points_in_place(builder, left);
2195+
let is_y_same = y_diff.is_zero(builder);
2196+
2197+
builder.if_eq(is_y_same, Usize::from(1)).then_or_else(
2198+
|builder| {
2199+
double_septic_points_in_place(builder, left);
2200+
},
2201+
|builder| {
2202+
let y_sum = septic_ext_add(builder, &right.y, &left.y);
2203+
let is_y_sum_zero = y_sum.is_zero(builder);
2204+
builder.assert_usize_eq(is_y_sum_zero, Usize::from(1));
2205+
let zero_ext_arr: Array<C, Ext<C::F, C::EF>> =
2206+
builder.dyn_array(SEPTIC_EXTENSION_DEGREE);
2207+
builder.assign(&left.x, zero_ext_arr.clone());
2208+
builder.assign(&left.y, zero_ext_arr.clone());
2209+
builder.assign(&left.is_infinity, Usize::from(1));
2210+
},
2211+
);
21902212
},
21912213
|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);
2214+
let x_diff_inv = invert(builder, &x_diff);
2215+
let slope = septic_ext_mul(builder, &y_diff, &x_diff_inv);
22062216

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);
2217+
let x_sum = septic_ext_add(builder, &right.x, &left.x);
2218+
let slope_squared = septic_ext_squared(builder, &slope);
2219+
let x = septic_ext_sub(builder, &slope_squared, &x_sum);
22102220

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);
2221+
let slope_mul_x_diff = septic_ext_mul(builder, &slope, &x_diff);
2222+
let y = septic_ext_sub(builder, &slope_mul_x_diff, &left.y);
22132223

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-
});
2224+
builder.assign(&left.x, x);
2225+
builder.assign(&left.y, y);
2226+
builder.assign(&left.is_infinity, Usize::from(0));
2227+
},
2228+
);
2229+
});
2230+
},
2231+
);
22212232
}

0 commit comments

Comments
 (0)