1
1
use crate :: tower_verifier:: binding:: PointAndEvalVariable ;
2
2
use crate :: zkvm_verifier:: binding:: ZKVMOpcodeProofInputVariable ;
3
- use ceno_zkvm :: expression:: { Expression , Fixed , Instance } ;
3
+ use ceno_mle :: expression:: { Expression , Fixed , Instance } ;
4
4
use ceno_zkvm:: structs:: { ChallengeId , WitnessId } ;
5
5
use ff_ext:: ExtensionField ;
6
6
use ff_ext:: { BabyBearExt4 , SmallField } ;
@@ -10,11 +10,13 @@ use openvm_native_recursion::challenger::ChallengerVariable;
10
10
use openvm_native_recursion:: challenger:: {
11
11
duplex:: DuplexChallengerVariable , CanObserveVariable , FeltChallenger ,
12
12
} ;
13
+ use itertools:: Either ;
13
14
use p3_field:: { FieldAlgebra , FieldExtensionAlgebra } ;
14
15
type E = BabyBearExt4 ;
15
16
const HASH_RATE : usize = 8 ;
17
+ const MAX_NUM_VARS : usize = 25 ;
16
18
17
- pub fn _print_ext_arr < C : Config > ( builder : & mut Builder < C > , arr : & Array < C , Ext < C :: F , C :: EF > > ) {
19
+ pub fn print_ext_arr < C : Config > ( builder : & mut Builder < C > , arr : & Array < C , Ext < C :: F , C :: EF > > ) {
18
20
iter_zip ! ( builder, arr) . for_each ( |ptr_vec, builder| {
19
21
let e = builder. iter_ptr_get ( arr, ptr_vec[ 0 ] ) ;
20
22
builder. print_e ( e) ;
@@ -28,7 +30,7 @@ pub fn print_felt_arr<C: Config>(builder: &mut Builder<C>, arr: &Array<C, Felt<C
28
30
} ) ;
29
31
}
30
32
31
- pub fn _print_usize_arr < C : Config > ( builder : & mut Builder < C > , arr : & Array < C , Usize < C :: N > > ) {
33
+ pub fn print_usize_arr < C : Config > ( builder : & mut Builder < C > , arr : & Array < C , Usize < C :: N > > ) {
32
34
iter_zip ! ( builder, arr) . for_each ( |ptr_vec, builder| {
33
35
let n = builder. iter_ptr_get ( arr, ptr_vec[ 0 ] ) ;
34
36
builder. print_v ( n. get_var ( ) ) ;
@@ -87,20 +89,91 @@ pub fn is_smaller_than<C: Config>(
87
89
RVar :: from ( v)
88
90
}
89
91
90
- pub fn evaluate_at_point < C : Config > (
92
+ pub fn evaluate_at_point_degree_1 < C : Config > (
91
93
builder : & mut Builder < C > ,
92
94
evals : & Array < C , Ext < C :: F , C :: EF > > ,
93
95
point : & Array < C , Ext < C :: F , C :: EF > > ,
94
96
) -> Ext < C :: F , C :: EF > {
95
- // TODO: Dynamic length
96
- // TODO: Sanity checks
97
97
let left = builder. get ( & evals, 0 ) ;
98
98
let right = builder. get ( & evals, 1 ) ;
99
99
let r = builder. get ( point, 0 ) ;
100
100
101
101
builder. eval ( r * ( right - left) + left)
102
102
}
103
103
104
+ pub struct PolyEvaluator < C : Config > {
105
+ powers_of_2 : Array < C , Usize < C :: N > > ,
106
+ }
107
+
108
+ impl < C : Config > PolyEvaluator < C > {
109
+ pub fn new ( builder : & mut Builder < C > ) -> Self {
110
+ let powers_of_2: Array < C , Usize < C :: N > > = builder. dyn_array ( MAX_NUM_VARS ) ;
111
+ builder. set ( & powers_of_2, 0 , Usize :: from ( 16777216 ) ) ;
112
+ builder. set ( & powers_of_2, 1 , Usize :: from ( 8388608 ) ) ;
113
+ builder. set ( & powers_of_2, 2 , Usize :: from ( 4194304 ) ) ;
114
+ builder. set ( & powers_of_2, 3 , Usize :: from ( 1048576 ) ) ;
115
+ builder. set ( & powers_of_2, 4 , Usize :: from ( 2097152 ) ) ;
116
+ builder. set ( & powers_of_2, 5 , Usize :: from ( 524288 ) ) ;
117
+ builder. set ( & powers_of_2, 6 , Usize :: from ( 262144 ) ) ;
118
+ builder. set ( & powers_of_2, 7 , Usize :: from ( 131072 ) ) ;
119
+ builder. set ( & powers_of_2, 8 , Usize :: from ( 65536 ) ) ;
120
+ builder. set ( & powers_of_2, 9 , Usize :: from ( 32768 ) ) ;
121
+ builder. set ( & powers_of_2, 10 , Usize :: from ( 16384 ) ) ;
122
+ builder. set ( & powers_of_2, 11 , Usize :: from ( 8192 ) ) ;
123
+ builder. set ( & powers_of_2, 12 , Usize :: from ( 4096 ) ) ;
124
+ builder. set ( & powers_of_2, 13 , Usize :: from ( 2048 ) ) ;
125
+ builder. set ( & powers_of_2, 14 , Usize :: from ( 1024 ) ) ;
126
+ builder. set ( & powers_of_2, 15 , Usize :: from ( 512 ) ) ;
127
+ builder. set ( & powers_of_2, 16 , Usize :: from ( 256 ) ) ;
128
+ builder. set ( & powers_of_2, 17 , Usize :: from ( 128 ) ) ;
129
+ builder. set ( & powers_of_2, 18 , Usize :: from ( 64 ) ) ;
130
+ builder. set ( & powers_of_2, 19 , Usize :: from ( 32 ) ) ;
131
+ builder. set ( & powers_of_2, 20 , Usize :: from ( 16 ) ) ;
132
+ builder. set ( & powers_of_2, 21 , Usize :: from ( 8 ) ) ;
133
+ builder. set ( & powers_of_2, 22 , Usize :: from ( 4 ) ) ;
134
+ builder. set ( & powers_of_2, 23 , Usize :: from ( 2 ) ) ;
135
+ builder. set ( & powers_of_2, 24 , Usize :: from ( 1 ) ) ;
136
+
137
+ Self { powers_of_2 }
138
+ }
139
+
140
+ pub fn evaluate_base_poly_at_point (
141
+ & self ,
142
+ builder : & mut Builder < C > ,
143
+ evals : & Array < C , Felt < C :: F > > ,
144
+ point : & Array < C , Ext < C :: F , C :: EF > > ,
145
+ ) -> Ext < C :: F , C :: EF > {
146
+ let num_var = point. len ( ) ;
147
+
148
+ let evals_ext: Array < C , Ext < C :: F , C :: EF > > = builder. dyn_array ( evals. len ( ) ) ;
149
+ iter_zip ! ( builder, evals, evals_ext) . for_each ( |ptr_vec, builder| {
150
+ let f = builder. iter_ptr_get ( & evals, ptr_vec[ 0 ] ) ;
151
+ let e = builder. ext_from_base_slice ( & [ f] ) ;
152
+ builder. iter_ptr_set ( & evals_ext, ptr_vec[ 1 ] , e) ;
153
+ } ) ;
154
+
155
+ let pwr_slice_idx: Usize < C :: N > = builder. eval ( Usize :: from ( 25 ) - num_var) ;
156
+ let pwrs = self . powers_of_2 . slice ( builder, pwr_slice_idx, MAX_NUM_VARS ) ;
157
+
158
+ iter_zip ! ( builder, point, pwrs) . for_each ( |ptr_vec, builder| {
159
+ let pt = builder. iter_ptr_get ( & point, ptr_vec[ 0 ] ) ;
160
+ let idx_bound = builder. iter_ptr_get ( & pwrs, ptr_vec[ 1 ] ) ;
161
+
162
+ builder. range ( 0 , idx_bound) . for_each ( |idx_vec, builder| {
163
+ let left_idx: Usize < C :: N > = builder. eval ( idx_vec[ 0 ] * Usize :: from ( 2 ) ) ;
164
+ let right_idx: Usize < C :: N > = builder. eval ( idx_vec[ 0 ] * Usize :: from ( 2 ) + Usize :: from ( 1 ) ) ;
165
+ let left = builder. get ( & evals_ext, left_idx) ;
166
+ let right = builder. get ( & evals_ext, right_idx) ;
167
+
168
+ let e: Ext < C :: F , C :: EF > = builder. eval ( pt * ( right - left) + left) ;
169
+ builder. set ( & evals_ext, idx_vec[ 0 ] , e) ;
170
+ } ) ;
171
+ } ) ;
172
+
173
+ builder. get ( & evals_ext, 0 )
174
+ }
175
+ }
176
+
104
177
pub fn dot_product < C : Config > (
105
178
builder : & mut Builder < C > ,
106
179
a : & Array < C , Ext < C :: F , C :: EF > > ,
@@ -221,6 +294,24 @@ pub fn product<C: Config>(
221
294
acc
222
295
}
223
296
297
+ // Multiply all elements in a nested Array
298
+ pub fn nested_product < C : Config > (
299
+ builder : & mut Builder < C > ,
300
+ arr : & Array < C , Array < C , Ext < C :: F , C :: EF > > > ,
301
+ ) -> Ext < C :: F , C :: EF > {
302
+ let acc = builder. constant ( C :: EF :: ONE ) ;
303
+ iter_zip ! ( builder, arr) . for_each ( |ptr_vec, builder| {
304
+ let inner_arr = builder. iter_ptr_get ( arr, ptr_vec[ 0 ] ) ;
305
+
306
+ iter_zip ! ( builder, inner_arr) . for_each ( |ptr_vec, builder| {
307
+ let el = builder. iter_ptr_get ( & inner_arr, ptr_vec[ 0 ] ) ;
308
+ builder. assign ( & acc, acc * el) ;
309
+ } ) ;
310
+ } ) ;
311
+
312
+ acc
313
+ }
314
+
224
315
// Add all elements in the Array
225
316
pub fn sum < C : Config > (
226
317
builder : & mut Builder < C > ,
@@ -286,12 +377,13 @@ pub fn eq_eval_less_or_equal_than<C: Config>(
286
377
a : & Array < C , Ext < C :: F , C :: EF > > ,
287
378
b : & Array < C , Ext < C :: F , C :: EF > > ,
288
379
) -> Ext < C :: F , C :: EF > {
380
+ builder. cycle_tracker_start ( "Compute eq_eval_less_or_equal_than" ) ;
289
381
let eq_bit_decomp: Array < C , Felt < C :: F > > = opcode_proof
290
382
. num_instances_minus_one_bit_decomposition
291
383
. slice ( builder, 0 , b. len ( ) ) ;
292
384
293
385
let one_ext: Ext < C :: F , C :: EF > = builder. constant ( C :: EF :: ONE ) ;
294
- let rp_len = builder. eval_expr ( RVar :: from ( b. len ( ) ) + RVar :: from ( 1 ) ) ;
386
+ let rp_len = builder. eval_expr ( b. len ( ) + C :: N :: ONE ) ;
295
387
let running_product: Array < C , Ext < C :: F , C :: EF > > = builder. dyn_array ( rp_len) ;
296
388
builder. set ( & running_product, 0 , one_ext) ;
297
389
@@ -305,49 +397,29 @@ pub fn eq_eval_less_or_equal_than<C: Config>(
305
397
builder. set ( & running_product, next_idx, next_v) ;
306
398
} ) ;
307
399
308
- let running_product2: Array < C , Ext < C :: F , C :: EF > > = builder. dyn_array ( rp_len) ;
309
- builder. set ( & running_product2, b. len ( ) , one_ext) ;
310
-
311
- let eq_bit_decomp_rev = reverse ( builder, & eq_bit_decomp) ;
312
- let idx_arr = gen_idx_arr ( builder, b. len ( ) ) ;
313
- let idx_arr_rev = reverse ( builder, & idx_arr) ;
314
- builder. assert_usize_eq ( eq_bit_decomp_rev. len ( ) , idx_arr_rev. len ( ) ) ;
315
-
316
- iter_zip ! ( builder, idx_arr_rev, eq_bit_decomp_rev) . for_each ( |ptr_vec, builder| {
317
- let i = builder. iter_ptr_get ( & idx_arr_rev, ptr_vec[ 0 ] ) ;
318
- let bit = builder. iter_ptr_get ( & eq_bit_decomp_rev, ptr_vec[ 1 ] ) ;
319
- let bit_ext = builder. ext_from_base_slice ( & [ bit] ) ;
320
- let last_idx = builder. eval_expr ( i. clone ( ) + RVar :: from ( 1 ) ) ;
321
-
322
- let v = builder. get ( & running_product2, last_idx) ;
323
- let a_i = builder. get ( a, i. clone ( ) ) ;
324
- let b_i = builder. get ( b, i. clone ( ) ) ;
325
-
326
- let next_v: Ext < C :: F , C :: EF > = builder. eval (
327
- v * ( a_i * b_i * bit_ext + ( one_ext - a_i) * ( one_ext - b_i) * ( one_ext - bit_ext) ) ,
328
- ) ;
329
- builder. set ( & running_product2, i, next_v) ;
330
- } ) ;
331
-
332
- // Here is an example of how this works:
333
- // Suppose max_idx = (110101)_2
334
- // Then ans = eq(a, b)
335
- // - eq(11011, a[1..6], b[1..6])eq(a[0..1], b[0..1])
336
- // - eq(111, a[3..6], b[3..6])eq(a[0..3], b[0..3])
337
400
let ans = builder. get ( & running_product, b. len ( ) ) ;
338
- builder. range ( 0 , b. len ( ) ) . for_each ( |idx_vec, builder| {
339
- let bit = builder. get ( & eq_bit_decomp, idx_vec[ 0 ] ) ;
401
+ let running_product2: Ext < C :: F , C :: EF > = builder. constant ( C :: EF :: ONE ) ;
402
+ let idx: Var < C :: N > = builder. uninit ( ) ;
403
+ builder. assign ( & idx, b. len ( ) - C :: N :: ONE ) ;
404
+ builder. range ( 0 , b. len ( ) ) . for_each ( |_, builder| {
405
+ let bit = builder. get ( & eq_bit_decomp, idx) ;
340
406
let bit_rvar = RVar :: from ( builder. cast_felt_to_var ( bit) ) ;
407
+ let bit_ext: Ext < C :: F , C :: EF > = builder. eval ( bit * SymbolicExt :: from_f ( C :: EF :: ONE ) ) ;
341
408
342
- builder. if_ne ( bit_rvar, RVar :: from ( 1 ) ) . then ( |builder| {
343
- let next_idx = builder. eval_expr ( idx_vec[ 0 ] + RVar :: from ( 1 ) ) ;
344
- let v1 = builder. get ( & running_product, idx_vec[ 0 ] ) ;
345
- let v2 = builder. get ( & running_product2, next_idx) ;
346
- let a_i = builder. get ( a, idx_vec[ 0 ] ) ;
347
- let b_i = builder. get ( b, idx_vec[ 0 ] ) ;
409
+ let a_i = builder. get ( a, idx) ;
410
+ let b_i = builder. get ( b, idx) ;
348
411
349
- builder. assign ( & ans, ans - v1 * v2 * a_i * b_i) ;
412
+ // Suppose max_idx = (110101)_2
413
+ // Then ans = eq(a, b)
414
+ // - eq(11011, a[1..6], b[1..6])eq(a[0..1], b[0..1])
415
+ // - eq(111, a[3..6], b[3..6])eq(a[0..3], b[0..3])
416
+ builder. if_ne ( bit_rvar, RVar :: from ( 1 ) ) . then ( |builder| {
417
+ let v1 = builder. get ( & running_product, idx) ;
418
+ builder. assign ( & ans, ans - v1 * running_product2 * a_i * b_i) ;
350
419
} ) ;
420
+
421
+ builder. assign ( & running_product2, running_product2 * ( a_i * b_i * bit_ext + ( one_ext - a_i) * ( one_ext - b_i) * ( one_ext - bit_ext) ) ) ;
422
+ builder. assign ( & idx, idx - C :: N :: ONE ) ;
351
423
} ) ;
352
424
353
425
let a_remainder_arr: Array < C , Ext < C :: F , C :: EF > > = a. slice ( builder, b. len ( ) , a. len ( ) ) ;
@@ -356,6 +428,8 @@ pub fn eq_eval_less_or_equal_than<C: Config>(
356
428
builder. assign ( & ans, ans * ( one_ext - a) ) ;
357
429
} ) ;
358
430
431
+ builder. cycle_tracker_end ( "Compute eq_eval_less_or_equal_than" ) ;
432
+
359
433
ans
360
434
}
361
435
@@ -460,9 +534,14 @@ pub fn eval_ceno_expr_with_instance<C: Config>(
460
534
res
461
535
} ,
462
536
& |builder, scalar| {
463
- let res: Ext < C :: F , C :: EF > =
464
- builder. constant ( C :: EF :: from_canonical_u32 ( scalar. to_canonical_u64 ( ) as u32 ) ) ;
465
- res
537
+ let scalar_base_slice = scalar
538
+ . as_bases ( )
539
+ . iter ( )
540
+ . map ( |b| C :: F :: from_canonical_u64 ( b. to_canonical_u64 ( ) ) )
541
+ . collect :: < Vec < C :: F > > ( ) ;
542
+ let scalar_ext: Ext < C :: F , C :: EF > =
543
+ builder. constant ( C :: EF :: from_base_slice ( & scalar_base_slice) ) ;
544
+ scalar_ext
466
545
} ,
467
546
& |builder, challenge_id, pow, scalar, offset| {
468
547
let challenge = builder. get ( & challenges, challenge_id as usize ) ;
@@ -510,7 +589,7 @@ pub fn evaluate_ceno_expr<C: Config, T>(
510
589
wit_in : & impl Fn ( & mut Builder < C > , WitnessId ) -> T , // witin id
511
590
structural_wit_in : & impl Fn ( & mut Builder < C > , WitnessId , usize , u32 , usize ) -> T ,
512
591
instance : & impl Fn ( & mut Builder < C > , Instance ) -> T ,
513
- constant : & impl Fn ( & mut Builder < C > , < E as ExtensionField > :: BaseField ) -> T ,
592
+ constant : & impl Fn ( & mut Builder < C > , E ) -> T ,
514
593
challenge : & impl Fn ( & mut Builder < C > , ChallengeId , usize , E , E ) -> T ,
515
594
sum : & impl Fn ( & mut Builder < C > , T , T ) -> T ,
516
595
product : & impl Fn ( & mut Builder < C > , T , T ) -> T ,
@@ -523,7 +602,16 @@ pub fn evaluate_ceno_expr<C: Config, T>(
523
602
structural_wit_in ( builder, * witness_id, * max_len, * offset, * multi_factor)
524
603
}
525
604
Expression :: Instance ( i) => instance ( builder, * i) ,
526
- Expression :: Constant ( scalar) => constant ( builder, * scalar) ,
605
+ Expression :: Constant ( scalar) => {
606
+ match scalar {
607
+ Either :: Left ( s) => {
608
+ constant ( builder, E :: from_base ( * s) )
609
+ } ,
610
+ Either :: Right ( s) => {
611
+ constant ( builder, * s)
612
+ } ,
613
+ }
614
+ } ,
527
615
Expression :: Sum ( a, b) => {
528
616
let a = evaluate_ceno_expr (
529
617
builder,
0 commit comments