@@ -93,6 +93,7 @@ impl<F: Field> BaseAirWithPublicValues<F> for MemcpyIterAir {}
93
93
impl < F : Field > PartitionedBaseAir < F > for MemcpyIterAir { }
94
94
95
95
impl < AB : InteractionBuilder > Air < AB > for MemcpyIterAir {
96
+ // assertions for AIR constraints
96
97
fn eval ( & self , builder : & mut AB ) {
97
98
let main = builder. main ( ) ;
98
99
let ( prev, local) = ( main. row_slice ( 0 ) , main. row_slice ( 1 ) ) ;
@@ -377,6 +378,8 @@ impl<'a> CustomBorrow<'a, MemcpyIterRecordMut<'a>, MemcpyIterLayout> for [u8] {
377
378
unsafe fn extract_layout ( & self ) -> MemcpyIterLayout {
378
379
let header: & MemcpyIterRecordHeader = self . borrow ( ) ;
379
380
let num_rows = ( ( header. len - header. shift as u32 ) >> 4 ) as usize + 1 ;
381
+ MultiRowLayout :: new ( MemcpyIterMetadata { num_rows } ) ;
382
+ let num_rows = ( ( header. len - header. shift as u32 ) >> 4 ) as usize + 1 ;
380
383
MultiRowLayout :: new ( MemcpyIterMetadata { num_rows } )
381
384
}
382
385
}
@@ -420,7 +423,7 @@ where
420
423
) -> Result < ( ) , ExecutionError > {
421
424
let Instruction { opcode, c, .. } = instruction;
422
425
debug_assert_eq ! ( * opcode, Rv32MemcpyOpcode :: MEMCPY_LOOP . global_opcode( ) ) ;
423
- let shift = c. as_canonical_u32 ( ) as u8 ;
426
+ let shift = c. as_canonical_u32 ( ) as u8 ; // written into c slot
424
427
debug_assert ! ( [ 0 , 1 , 2 , 3 ] . contains( & shift) ) ;
425
428
426
429
let mut dest = read_rv32_register (
@@ -440,17 +443,25 @@ where
440
443
} as u32 ,
441
444
) ;
442
445
let mut len = read_rv32_register ( state. memory . data ( ) , A2_REGISTER_PTR as u32 ) ;
446
+ debug_assert ! (
447
+ shift == 0 || ( dest % 4 == 0 ) ,
448
+ "dest must be 4-byte aligned in MEMCPY_LOOP"
449
+ ) ;
450
+ debug_assert ! ( len >= shift as u32 ) ;
443
451
444
452
// Create a record sized to the exact number of 16-byte iterations (header + iterations)
445
453
// This calculation must match extract_layout and fill_trace
446
454
447
- // FIX 1: prevent underflow when len < shift
448
- let effective_len = len. saturating_sub ( shift as u32 ) ;
455
+ let effective_len = len. saturating_sub ( shift as u32 ) ; // n >= 16 + shift
449
456
let num_iters = ( effective_len >> 4 ) as usize ;
450
- eprintln ! ( "num_iters = {:?}" , num_iters) ;
451
- // eprintln!("state.pc = {:?}", state.pc);
452
- // eprintln!("state.memory.timestamp = {:?}", state.memory.timestamp);
453
- // eprintln!("state.memory.data() = {:?}", state.memory.data());
457
+ // eprintln!(
458
+ // "PREFLIGHT: len={}, shift={}, effective_len={}, num_iters={}, allocated_rows={}",
459
+ // len,
460
+ // shift,
461
+ // effective_len,
462
+ // num_iters,
463
+ // num_iters + 1
464
+ // );
454
465
let record: MemcpyIterRecordMut < ' _ > =
455
466
state. ctx . alloc ( MultiRowLayout :: new ( MemcpyIterMetadata {
456
467
//allocating based on number of rows needed
@@ -464,15 +475,16 @@ where
464
475
record. inner . dest = dest;
465
476
record. inner . source = source;
466
477
record. inner . len = len;
467
- eprintln ! (
468
- "shift = {:?}, len = {:?}, source = {:?}, source%16 = {:?}, dest = {:?}, dest%16 = {:?}" ,
469
- shift, len, source, source % 16 , dest, dest % 16
470
- ) ;
478
+ // eprintln!(
479
+ // "shift = {:?}, len = {:?}, source = {:?}, source%16 = {:?}, dest = {:?}, dest%16 = {:?}",
480
+ // shift, len, source, source % 16, dest, dest % 16
481
+ // );
471
482
472
483
// Fill record.var for the first row of iteration trace
473
484
// FIX 2: read source-4 (the word ending at s[-1]); zero if out-of-bounds.
474
485
if shift != 0 {
475
486
if source >= 4 {
487
+ // read the previous word from memory
476
488
record. var [ 0 ] . data [ 3 ] = tracing_read (
477
489
state. memory ,
478
490
RV32_MEMORY_AS ,
@@ -494,13 +506,14 @@ where
494
506
source + 4 * i as u32 ,
495
507
& mut record. var [ idx] . read_aux [ i] . prev_timestamp ,
496
508
) ;
509
+ //use shifted data, to construct the write data for each given word
497
510
let write_data: [ u8 ; MEMCPY_LOOP_NUM_LIMBS ] = array:: from_fn ( |j| {
498
511
if j < shift as usize {
499
512
if i > 0 {
500
- // First s bytes come from previous 4-byte word tail
513
+ // First s bytes come from previous 4-byte word tail, take from previous word, in our 16 byte chunk
501
514
record. var [ idx] . data [ i - 1 ] [ j + ( 4 - shift as usize ) ]
502
515
} else {
503
- // For i == 0, take from previous chunk's last word tail
516
+ // For i == 0, take from previous chunk's last word tail; otherwise, take last word of previous chunk
504
517
record. var [ idx - 1 ] . data [ 3 ] [ j + ( 4 - shift as usize ) ]
505
518
}
506
519
} else {
@@ -570,7 +583,7 @@ where
570
583
debug_assert_eq ! ( record. inner. len, u32 :: from_le_bytes( len_data) ) ;
571
584
572
585
* state. pc = state. pc . wrapping_add ( DEFAULT_PC_STEP ) ;
573
-
586
+ eprintln ! ( "PREFLIGHT: done" ) ;
574
587
Ok ( ( ) )
575
588
}
576
589
}
@@ -936,6 +949,7 @@ unsafe fn execute_e12_impl<F: PrimeField32, CTX: ExecutionCtxTrait>(
936
949
) -> u32 {
937
950
let shift = pre_compute. c ;
938
951
let mut height = 1 ;
952
+ eprintln ! ( "RUNTIME: Starting with height={}, shift={}" , height, shift) ;
939
953
// Read dest and source from registers
940
954
let ( dest, source) = if shift == 0 {
941
955
(
@@ -955,6 +969,11 @@ unsafe fn execute_e12_impl<F: PrimeField32, CTX: ExecutionCtxTrait>(
955
969
let mut source = u32:: from_le_bytes ( source) - 12 * ( shift != 0 ) as u32 ;
956
970
let mut len = u32:: from_le_bytes ( len) ;
957
971
972
+ eprintln ! (
973
+ "RUNTIME: Initial values: dest={}, source={}, len={}" ,
974
+ dest, source, len
975
+ ) ;
976
+
958
977
// Check address ranges are valid
959
978
debug_assert ! ( dest < ( 1 << POINTER_MAX_BITS ) ) ;
960
979
debug_assert ! ( ( source - 4 * ( shift != 0 ) as u32 ) < ( 1 << POINTER_MAX_BITS ) ) ;
@@ -994,28 +1013,8 @@ unsafe fn execute_e12_impl<F: PrimeField32, CTX: ExecutionCtxTrait>(
994
1013
height += 1 ;
995
1014
}
996
1015
997
- // Handle remaining bytes (len in [0, 15]) so that total `copy_len == original len`.
998
- if len > 0 {
999
- let remaining_words = ( ( len + 3 ) >> 2 ) as usize ;
1000
- for i in 0 ..remaining_words. min ( 4 ) {
1001
- let data = vm_state. vm_read :: < u8 , 4 > ( RV32_MEMORY_AS , source + 4 * i as u32 ) ;
1002
- let write_data: [ u8 ; 4 ] = array:: from_fn ( |j| {
1003
- if j < shift as usize {
1004
- prev_data[ j + ( 4 - shift as usize ) ]
1005
- } else {
1006
- data[ j - shift as usize ]
1007
- }
1008
- } ) ;
1009
- vm_state. vm_write ( RV32_MEMORY_AS , dest + 4 * i as u32 , & write_data) ;
1010
- prev_data = data;
1011
- }
1012
- // Advance pointers to reflect bytes written
1013
- let advanced = ( remaining_words as u32 ) << 2 ;
1014
- source += advanced;
1015
- dest += advanced;
1016
- len = 0 ;
1017
- height += 1 ;
1018
- }
1016
+ // Note: remaining bytes (len in [0, 15]) are handled by surrounding code,
1017
+ // not by this executor. The height calculation must match the trace exactly.
1019
1018
1020
1019
// Write the result back to memory
1021
1020
if shift == 0 {
@@ -1046,6 +1045,7 @@ unsafe fn execute_e12_impl<F: PrimeField32, CTX: ExecutionCtxTrait>(
1046
1045
1047
1046
* vm_state. pc_mut ( ) = vm_state. pc ( ) . wrapping_add ( DEFAULT_PC_STEP ) ;
1048
1047
* vm_state. instret_mut ( ) = vm_state. instret ( ) + 1 ;
1048
+ eprintln ! ( "RUNTIME: Returning height={}" , height) ;
1049
1049
height
1050
1050
}
1051
1051
0 commit comments