@@ -3,7 +3,7 @@ use std::borrow::Borrow;
33use openvm_circuit:: {
44 arch:: { ExecutionBridge , ExecutionState } ,
55 system:: memory:: {
6- offline_checker:: MemoryBridge ,
6+ offline_checker:: { MemoryBridge , MemoryReadAuxCols } ,
77 MemoryAddress ,
88 } ,
99} ;
@@ -26,6 +26,9 @@ use crate::{
2626 } ,
2727} ;
2828
29+ pub const NUM_RWS_FOR_PRODUCT : usize = 2 ;
30+ pub const NUM_RWS_FOR_LOGUP : usize = 3 ;
31+
2932#[ derive( Clone , Debug ) ]
3033pub struct NativeSumcheckAir {
3134 pub execution_bridge : ExecutionBridge ,
@@ -102,7 +105,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
102105 within_round_limit,
103106 should_acc,
104107 eval_acc,
105- is_writeback ,
108+ is_hint_src_id ,
106109 specific,
107110 } = local;
108111
@@ -232,6 +235,22 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
232235 next. start_timestamp ,
233236 start_timestamp + AB :: F :: from_canonical_usize ( 8 ) ,
234237 ) ;
238+ builder
239+ . when ( prod_row)
240+ . when ( next. prod_row + next. logup_row )
241+ . assert_eq (
242+ next. start_timestamp ,
243+ start_timestamp
244+ + within_round_limit * AB :: F :: from_canonical_usize ( NUM_RWS_FOR_PRODUCT ) ,
245+ ) ;
246+ builder
247+ . when ( logup_row)
248+ . when ( next. prod_row + next. logup_row )
249+ . assert_eq (
250+ next. start_timestamp ,
251+ start_timestamp
252+ + within_round_limit * AB :: F :: from_canonical_usize ( NUM_RWS_FOR_LOGUP ) ,
253+ ) ;
235254
236255 // Termination condition
237256 assert_array_eq (
@@ -330,7 +349,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
330349 native_as,
331350 register_ptrs[ 0 ] + AB :: F :: from_canonical_usize ( CONTEXT_ARR_BASE_LEN ) ,
332351 ) ,
333- [ max_round, is_writeback ] ,
352+ [ max_round, is_hint_src_id ] ,
334353 first_timestamp + AB :: F :: from_canonical_usize ( 7 ) ,
335354 & header_row_specific. read_records [ 7 ] ,
336355 )
@@ -373,6 +392,21 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
373392 ) ;
374393 builder. assert_eq ( prod_row * should_acc, prod_acc) ;
375394
395+ // Read p1, p2 from witness arrays
396+ self . memory_bridge
397+ . read (
398+ MemoryAddress :: new ( native_as, register_ptrs[ 2 ] + prod_row_specific. data_ptr ) ,
399+ prod_row_specific. p ,
400+ start_timestamp,
401+ & MemoryReadAuxCols {
402+ base : prod_row_specific. ps_record . base ,
403+ } ,
404+ )
405+ . eval (
406+ builder,
407+ ( prod_in_round_evaluation + prod_next_round_evaluation) * not ( is_hint_src_id) ,
408+ ) ;
409+
376410 // Obtain p1, p2 from hint space and write back to witness arrays
377411 self . memory_bridge
378412 . write (
@@ -383,7 +417,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
383417 )
384418 . eval (
385419 builder,
386- ( prod_in_round_evaluation + prod_next_round_evaluation) * is_writeback ,
420+ ( prod_in_round_evaluation + prod_next_round_evaluation) * is_hint_src_id ,
387421 ) ;
388422
389423 let p1: [ AB :: Var ; EXT_DEG ] = prod_row_specific. p [ 0 ..EXT_DEG ] . try_into ( ) . unwrap ( ) ;
@@ -398,7 +432,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
398432 register_ptrs[ 4 ] + curr_prod_n * AB :: F :: from_canonical_usize ( EXT_DEG ) ,
399433 ) ,
400434 prod_row_specific. p_evals ,
401- start_timestamp + is_writeback * AB :: F :: ONE ,
435+ start_timestamp + AB :: F :: ONE ,
402436 & prod_row_specific. write_record ,
403437 )
404438 . eval ( builder, prod_row * within_round_limit) ;
@@ -465,6 +499,21 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
465499 ) ;
466500 builder. assert_eq ( logup_row * should_acc, logup_acc) ;
467501
502+ // Read p1, p2, q1, q2 from witness arrays
503+ self . memory_bridge
504+ . read (
505+ MemoryAddress :: new ( native_as, register_ptrs[ 3 ] + logup_row_specific. data_ptr ) ,
506+ logup_row_specific. pq ,
507+ start_timestamp,
508+ & MemoryReadAuxCols {
509+ base : logup_row_specific. pqs_record . base ,
510+ } ,
511+ )
512+ . eval (
513+ builder,
514+ ( logup_in_round_evaluation + logup_next_round_evaluation) * not ( is_hint_src_id) ,
515+ ) ;
516+
468517 // Obtain p1, p2, q1, q2 from hint space
469518 self . memory_bridge
470519 . write (
@@ -475,7 +524,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
475524 )
476525 . eval (
477526 builder,
478- ( logup_in_round_evaluation + logup_next_round_evaluation) * is_writeback ,
527+ ( logup_in_round_evaluation + logup_next_round_evaluation) * is_hint_src_id ,
479528 ) ;
480529 let p1: [ _ ; EXT_DEG ] = logup_row_specific. pq [ 0 ..EXT_DEG ] . try_into ( ) . unwrap ( ) ;
481530 let p2: [ _ ; EXT_DEG ] = logup_row_specific. pq [ EXT_DEG ..( EXT_DEG * 2 ) ]
@@ -497,7 +546,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
497546 + ( num_prod_spec + curr_logup_n) * AB :: F :: from_canonical_usize ( EXT_DEG ) ,
498547 ) ,
499548 logup_row_specific. p_evals ,
500- start_timestamp + is_writeback * AB :: F :: ONE ,
549+ start_timestamp + AB :: F :: ONE ,
501550 & logup_row_specific. write_records [ 0 ] ,
502551 )
503552 . eval ( builder, logup_row * within_round_limit) ;
@@ -512,7 +561,7 @@ impl<AB: InteractionBuilder> Air<AB> for NativeSumcheckAir {
512561 * AB :: F :: from_canonical_usize ( EXT_DEG ) ,
513562 ) ,
514563 logup_row_specific. q_evals ,
515- start_timestamp + is_writeback * AB :: F :: ONE + AB :: F :: ONE ,
564+ start_timestamp + AB :: F :: TWO ,
516565 & logup_row_specific. write_records [ 1 ] ,
517566 )
518567 . eval ( builder, logup_row * within_round_limit) ;
0 commit comments