1
1
use std:: {
2
- array,
3
2
borrow:: { Borrow , BorrowMut } ,
4
- mem:: { align_of , size_of} ,
3
+ mem:: size_of,
5
4
sync:: { Arc , Mutex } ,
6
5
} ;
7
6
8
7
use openvm_circuit:: {
9
- arch:: * ,
10
- system:: { memory:: {
11
- offline_checker:: {
12
- MemoryBaseAuxCols , MemoryBaseAuxRecord , MemoryBridge , MemoryExtendedAuxRecord , MemoryReadAuxRecord , MemoryWriteAuxCols , MemoryWriteBytesAuxRecord
8
+ arch:: { ExecutionBridge , ExecutionState } ,
9
+ system:: {
10
+ memory:: {
11
+ offline_checker:: {
12
+ MemoryBaseAuxCols , MemoryBaseAuxRecord , MemoryBridge , MemoryExtendedAuxRecord ,
13
+ MemoryWriteAuxCols ,
14
+ } ,
15
+ MemoryAddress , MemoryAuxColsFactory ,
13
16
} ,
14
- online:: { GuestMemory , TracingMemory } ,
15
- MemoryAddress , MemoryAuxColsFactory ,
16
- } , SystemPort } ,
17
+ SystemPort ,
18
+ } ,
17
19
} ;
18
20
use openvm_circuit_primitives:: {
19
21
utils:: { not, or, select} ,
20
22
var_range:: { SharedVariableRangeCheckerChip , VariableRangeCheckerBus } ,
21
23
AlignedBytesBorrow ,
22
24
} ;
23
25
use openvm_circuit_primitives_derive:: AlignedBorrow ;
24
- use openvm_instructions:: {
25
- instruction:: Instruction ,
26
- program:: DEFAULT_PC_STEP ,
27
- riscv:: { RV32_MEMORY_AS , RV32_REGISTER_AS } ,
28
- LocalOpcode ,
29
- } ;
30
- use openvm_rv32im_circuit:: adapters:: { read_rv32_register, tracing_read, tracing_write} ;
26
+ use openvm_instructions:: riscv:: RV32_MEMORY_AS ;
27
+ use openvm_memcpy_transpiler:: Rv32MemcpyOpcode ;
31
28
use openvm_stark_backend:: {
32
- config:: { StarkGenericConfig , Val } , interaction:: InteractionBuilder , p3_air:: { Air , AirBuilder , BaseAir } , p3_field:: { Field , FieldAlgebra , PrimeField32 } , p3_matrix:: { dense:: RowMajorMatrix , Matrix } , prover:: { cpu:: CpuBackend , types:: AirProvingContext } , rap:: { get_air_name, BaseAirWithPublicValues , PartitionedBaseAir } , Chip , ChipUsageGetter
29
+ config:: { StarkGenericConfig , Val } ,
30
+ interaction:: InteractionBuilder ,
31
+ p3_air:: { Air , AirBuilder , BaseAir } ,
32
+ p3_field:: { Field , FieldAlgebra , PrimeField32 } ,
33
+ p3_matrix:: { dense:: RowMajorMatrix , Matrix } ,
34
+ prover:: { cpu:: CpuBackend , types:: AirProvingContext } ,
35
+ rap:: { get_air_name, BaseAirWithPublicValues , PartitionedBaseAir } ,
36
+ Chip , ChipUsageGetter ,
33
37
} ;
34
38
35
- use crate :: { bus:: MemcpyBus , MemcpyIterChip } ;
36
- use openvm_circuit:: arch:: {
37
- execution_mode:: { ExecutionCtxTrait , MeteredExecutionCtxTrait } ,
38
- get_record_from_slice, ExecuteFunc , ExecutionError , Executor , MeteredExecutor , RecordArena ,
39
- StaticProgramError , TraceFiller , VmExecState ,
40
- } ;
41
- use openvm_memcpy_transpiler:: Rv32MemcpyOpcode ;
42
-
39
+ use crate :: bus:: MemcpyBus ;
43
40
// Import constants from lib.rs
44
41
use crate :: {
45
42
A1_REGISTER_PTR , A2_REGISTER_PTR , A3_REGISTER_PTR , A4_REGISTER_PTR , MEMCPY_LOOP_LIMB_BITS ,
@@ -94,7 +91,8 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyLoopAir {
94
91
let mut timestamp_delta: u32 = 0 ;
95
92
let mut timestamp_pp = || {
96
93
timestamp_delta += 1 ;
97
- local. to_timestamp - AB :: Expr :: from_canonical_u32 ( MEMCPY_LOOP_NUM_WRITES + timestamp_delta - 1 )
94
+ local. to_timestamp
95
+ - AB :: Expr :: from_canonical_u32 ( MEMCPY_LOOP_NUM_WRITES + timestamp_delta - 1 )
98
96
} ;
99
97
100
98
let from_le_bytes = |data : [ AB :: Var ; 4 ] | {
@@ -257,7 +255,8 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyLoopAir {
257
255
258
256
// Make sure the request and response match
259
257
builder. assert_eq (
260
- local. to_timestamp - ( local. from_state . timestamp + AB :: Expr :: from_canonical_u32 ( timestamp_delta) ) ,
258
+ local. to_timestamp
259
+ - ( local. from_state . timestamp + AB :: Expr :: from_canonical_u32 ( timestamp_delta) ) ,
261
260
AB :: Expr :: TWO * ( len. clone ( ) - to_len) + is_shift_non_zero. clone ( ) ,
262
261
) ;
263
262
@@ -301,7 +300,13 @@ impl MemcpyLoopChip {
301
300
range_checker_chip : SharedVariableRangeCheckerChip ,
302
301
) -> Self {
303
302
Self {
304
- air : MemcpyLoopAir :: new ( system_port. memory_bridge , ExecutionBridge :: new ( system_port. execution_bus , system_port. program_bus ) , range_bus, memcpy_bus, pointer_max_bits) ,
303
+ air : MemcpyLoopAir :: new (
304
+ system_port. memory_bridge ,
305
+ ExecutionBridge :: new ( system_port. execution_bus , system_port. program_bus ) ,
306
+ range_bus,
307
+ memcpy_bus,
308
+ pointer_max_bits,
309
+ ) ,
305
310
records : Arc :: new ( Mutex :: new ( Vec :: new ( ) ) ) ,
306
311
pointer_max_bits,
307
312
range_checker_chip,
@@ -327,18 +332,24 @@ impl MemcpyLoopChip {
327
332
shift : u8 ,
328
333
register_aux : [ MemoryBaseAuxRecord ; 3 ] ,
329
334
) {
330
- let mut timestamp = from_timestamp + ( ( ( len - shift as u32 ) & !0x0f ) >> 1 ) + ( shift != 0 ) as u32 ;
331
- let write_aux = register_aux. iter ( ) . map ( |aux_record| {
332
- let mut aux_col = MemoryBaseAuxCols :: default ( ) ;
333
- mem_helper. fill ( aux_record. prev_timestamp , timestamp, & mut aux_col) ;
334
- timestamp += 1 ;
335
- MemoryExtendedAuxRecord :: from_aux_cols ( aux_col)
336
- } ) . collect :: < Vec < _ > > ( ) . try_into ( ) . unwrap ( ) ;
335
+ let mut timestamp =
336
+ from_timestamp + ( ( ( len - shift as u32 ) & !0x0f ) >> 1 ) + ( shift != 0 ) as u32 ;
337
+ let write_aux = register_aux
338
+ . iter ( )
339
+ . map ( |aux_record| {
340
+ let mut aux_col = MemoryBaseAuxCols :: default ( ) ;
341
+ mem_helper. fill ( aux_record. prev_timestamp , timestamp, & mut aux_col) ;
342
+ timestamp += 1 ;
343
+ MemoryExtendedAuxRecord :: from_aux_cols ( aux_col)
344
+ } )
345
+ . collect :: < Vec < _ > > ( )
346
+ . try_into ( )
347
+ . unwrap ( ) ;
337
348
338
349
let num_copies = ( len - shift as u32 ) & !0x0f ;
339
350
let to_dest = dest + num_copies;
340
351
let to_source = source + num_copies;
341
-
352
+
342
353
let word_to_u16 = |data : u32 | [ data & 0xffff , data >> 16 ] ;
343
354
let range_check_data = [
344
355
( word_to_u16 ( len) , false ) ,
@@ -379,7 +390,7 @@ impl MemcpyLoopChip {
379
390
380
391
/// Generates trace
381
392
pub fn generate_trace < F : PrimeField32 > ( & self ) -> RowMajorMatrix < F > {
382
- let mut rows = F :: zero_vec ( ( self . records . lock ( ) . unwrap ( ) . len ( ) as usize ) * NUM_MEMCPY_LOOP_COLS ) ;
393
+ let mut rows = F :: zero_vec ( self . records . lock ( ) . unwrap ( ) . len ( ) * NUM_MEMCPY_LOOP_COLS ) ;
383
394
384
395
for ( i, record) in self . records . lock ( ) . unwrap ( ) . iter ( ) . enumerate ( ) {
385
396
let row = & mut rows[ i * NUM_MEMCPY_LOOP_COLS ..( i + 1 ) * NUM_MEMCPY_LOOP_COLS ] ;
@@ -394,11 +405,22 @@ impl MemcpyLoopChip {
394
405
cols. dest = record. dest . to_le_bytes ( ) . map ( F :: from_canonical_u8) ;
395
406
cols. source = record. source . to_le_bytes ( ) . map ( F :: from_canonical_u8) ;
396
407
cols. len = record. len . to_le_bytes ( ) . map ( F :: from_canonical_u8) ;
397
- cols. shift = [ F :: from_canonical_u8 ( shift % 2 ) , F :: from_canonical_u8 ( shift / 2 ) ] ;
408
+ cols. shift = [
409
+ F :: from_canonical_u8 ( shift % 2 ) ,
410
+ F :: from_canonical_u8 ( shift / 2 ) ,
411
+ ] ;
398
412
cols. is_valid = F :: ONE ;
399
- // We have MEMCPY_LOOP_NUM_WRITES writes in the loop, (num_copies / 4 + shift != 0) reads and (num_copies / 4) writes in iterations
400
- cols. to_timestamp = F :: from_canonical_u32 ( record. from_timestamp + MEMCPY_LOOP_NUM_WRITES + ( num_copies >> 1 ) + ( shift != 0 ) as u32 ) ;
401
- cols. to_dest = ( record. dest + num_copies) . to_le_bytes ( ) . map ( F :: from_canonical_u8) ;
413
+ // We have MEMCPY_LOOP_NUM_WRITES writes in the loop, (num_copies / 4) writes
414
+ // and (num_copies / 4 + shift != 0) reads in iterations
415
+ cols. to_timestamp = F :: from_canonical_u32 (
416
+ record. from_timestamp
417
+ + MEMCPY_LOOP_NUM_WRITES
418
+ + ( num_copies >> 1 )
419
+ + ( shift != 0 ) as u32 ,
420
+ ) ;
421
+ cols. to_dest = ( record. dest + num_copies)
422
+ . to_le_bytes ( )
423
+ . map ( F :: from_canonical_u8) ;
402
424
cols. to_source = to_source. to_le_bytes ( ) . map ( F :: from_canonical_u8) ;
403
425
cols. to_len = F :: from_canonical_u32 ( record. len - num_copies) ;
404
426
cols. write_aux = record. write_aux . clone ( ) . map ( |aux| aux. to_aux_cols ( ) ) ;
@@ -426,10 +448,10 @@ impl ChipUsageGetter for MemcpyLoopChip {
426
448
get_air_name ( & self . air )
427
449
}
428
450
fn constant_trace_height ( & self ) -> Option < usize > {
429
- Some ( self . records . lock ( ) . unwrap ( ) . len ( ) as usize )
451
+ Some ( self . records . lock ( ) . unwrap ( ) . len ( ) )
430
452
}
431
453
fn current_trace_height ( & self ) -> usize {
432
- self . records . lock ( ) . unwrap ( ) . len ( ) as usize
454
+ self . records . lock ( ) . unwrap ( ) . len ( )
433
455
}
434
456
fn trace_width ( & self ) -> usize {
435
457
NUM_MEMCPY_LOOP_COLS
0 commit comments