Skip to content

Commit df92fec

Browse files
pjabbarzadepjabbarzade
committed
fix some bugs
1 parent f745481 commit df92fec

File tree

6 files changed

+154
-126
lines changed

6 files changed

+154
-126
lines changed

‎crates/vm/src/system/memory/offline_checker/mod.rs

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -32,13 +32,10 @@ impl MemoryExtendedAuxRecord {
3232
}
3333
}
3434

35-
pub fn to_aux_cols<F: PrimeField32>(&self) -> MemoryBaseAuxCols<F> {
36-
MemoryBaseAuxCols {
37-
prev_timestamp: F::from_canonical_u32(self.prev_timestamp),
38-
timestamp_lt_aux: LessThanAuxCols {
39-
lower_decomp: self.timestamp_lt_aux.map(|x| F::from_canonical_u32(x)),
40-
},
41-
}
35+
pub fn to_aux_cols<F: PrimeField32>(&self, aux_cols: &mut MemoryBaseAuxCols<F>) {
36+
aux_cols.prev_timestamp = F::from_canonical_u32(self.prev_timestamp);
37+
aux_cols.timestamp_lt_aux.lower_decomp =
38+
self.timestamp_lt_aux.map(|x| F::from_canonical_u32(x));
4239
}
4340
}
4441

‎extensions/memcpy/circuit/src/bus.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -29,21 +29,21 @@ impl MemcpyBus {
2929
timestamp: impl Into<T>,
3030
dest: impl Into<T>,
3131
source: impl Into<T>,
32-
n: impl Into<T>,
32+
len: impl Into<T>,
3333
shift: impl Into<T>,
3434
) -> MemcpyBusInteraction<T> {
35-
self.push(true, timestamp, dest, source, n, shift)
35+
self.push(true, timestamp, dest, source, len, shift)
3636
}
3737

3838
pub fn receive<T: Clone>(
3939
&self,
4040
timestamp: impl Into<T>,
4141
dest: impl Into<T>,
4242
source: impl Into<T>,
43-
n: impl Into<T>,
43+
len: impl Into<T>,
4444
shift: impl Into<T>,
4545
) -> MemcpyBusInteraction<T> {
46-
self.push(false, timestamp, dest, source, n, shift)
46+
self.push(false, timestamp, dest, source, len, shift)
4747
}
4848

4949
fn push<T: Clone>(
@@ -52,7 +52,7 @@ impl MemcpyBus {
5252
timestamp: impl Into<T>,
5353
dest: impl Into<T>,
5454
source: impl Into<T>,
55-
n: impl Into<T>,
55+
len: impl Into<T>,
5656
shift: impl Into<T>,
5757
) -> MemcpyBusInteraction<T> {
5858
MemcpyBusInteraction {
@@ -61,7 +61,7 @@ impl MemcpyBus {
6161
timestamp: timestamp.into(),
6262
dest: dest.into(),
6363
source: source.into(),
64-
n: n.into(),
64+
len: len.into(),
6565
shift: shift.into(),
6666
}
6767
}
@@ -74,7 +74,7 @@ pub struct MemcpyBusInteraction<T> {
7474
pub timestamp: T,
7575
pub dest: T,
7676
pub source: T,
77-
pub n: T,
77+
pub len: T,
7878
pub shift: T,
7979
}
8080

@@ -87,7 +87,7 @@ impl<T: FieldAlgebra> MemcpyBusInteraction<T> {
8787
.chain(iter::once(self.timestamp))
8888
.chain(iter::once(self.dest))
8989
.chain(iter::once(self.source))
90-
.chain(iter::once(self.n))
90+
.chain(iter::once(self.len))
9191
.chain(iter::once(self.shift));
9292

9393
if self.is_send {

‎extensions/memcpy/circuit/src/extension.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ impl<F> VmExecutionExtension<F> for Memcpy {
4040
&self,
4141
inventory: &mut ExecutorInventoryBuilder<F, MemcpyExecutor>,
4242
) -> Result<(), ExecutorInventoryError> {
43-
let memcpy_iter = MemcpyIterExecutor::new();
43+
let memcpy_iter = MemcpyIterExecutor::new(Rv32MemcpyOpcode::CLASS_OFFSET);
4444

4545
inventory.add_executor(
4646
memcpy_iter,
@@ -71,6 +71,7 @@ impl<SC: StarkGenericConfig> VmCircuitExtension<SC> for Memcpy {
7171
range_bus,
7272
memcpy_bus,
7373
pointer_max_bits,
74+
Rv32MemcpyOpcode::CLASS_OFFSET,
7475
);
7576
inventory.add_air(memcpy_loop);
7677

@@ -113,6 +114,7 @@ where
113114
inventory.airs().system().port(),
114115
range_bus,
115116
memcpy_bus,
117+
Rv32MemcpyOpcode::CLASS_OFFSET,
116118
pointer_max_bits,
117119
range_checker.clone(),
118120
));
@@ -127,11 +129,11 @@ where
127129
);
128130
// Add MemcpyLoop chip
129131
inventory.next_air::<MemcpyLoopAir>()?;
130-
inventory.add_executor_chip(memcpy_loop_chip);
132+
inventory.add_periphery_chip(memcpy_loop_chip);
131133

132134
// Add MemcpyIter chip
133135
inventory.next_air::<MemcpyIterAir>()?;
134-
inventory.add_periphery_chip(memcpy_iter_chip);
136+
inventory.add_executor_chip(memcpy_iter_chip);
135137

136138
Ok(())
137139
}

‎extensions/memcpy/circuit/src/iteration.rs

Lines changed: 61 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -111,15 +111,17 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
111111
let is_shift_two = and::<AB::Expr>(not::<AB::Expr>(local.shift[0]), local.shift[1]);
112112
let is_shift_three = and::<AB::Expr>(local.shift[0], local.shift[1]);
113113

114-
// TODO:since if is_valid = 0, then is_boundary = 0, we can reduce the degree of the following expressions by removing the is_valid term
115114
let is_end =
116115
(local.is_boundary + AB::Expr::ONE) * local.is_boundary * (AB::F::TWO).inverse();
117116
let is_not_start = (local.is_boundary + AB::Expr::ONE)
118117
* (AB::Expr::TWO - local.is_boundary)
119118
* (AB::F::TWO).inverse();
119+
let prev_is_not_end = not::<AB::Expr>(
120+
(prev.is_boundary + AB::Expr::ONE) * prev.is_boundary * (AB::F::TWO).inverse(),
121+
);
120122

121123
let len = local.len[0]
122-
+ local.len[1] * AB::F::from_canonical_u32(1 << (2 * MEMCPY_LOOP_LIMB_BITS));
124+
+ local.len[1] * AB::Expr::from_canonical_u32(1 << (2 * MEMCPY_LOOP_LIMB_BITS));
123125

124126
// write_data =
125127
// (local.data_1[shift..4], prev.data_4[0..shift]),
@@ -136,7 +138,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
136138
let write_data = write_data_pairs
137139
.iter()
138140
.map(|(prev_data, next_data)| {
139-
array::from_fn(|i| {
141+
array::from_fn::<_, MEMCPY_LOOP_NUM_LIMBS, _>(|i| {
140142
is_shift_zero.clone() * (next_data[i])
141143
+ is_shift_one.clone()
142144
* (if i < 3 {
@@ -161,35 +163,44 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
161163
.collect::<Vec<_>>();
162164

163165
builder.assert_bool(local.is_valid);
164-
for i in 0..2 {
165-
builder.assert_bool(local.shift[i]);
166-
}
166+
local.shift.iter().for_each(|x| builder.assert_bool(*x));
167167
builder.assert_bool(local.is_valid_not_start);
168168
// is_boundary is either -1, 0 or 1
169169
builder.assert_tern(local.is_boundary + AB::Expr::ONE);
170170

171171
// is_valid_not_start = is_valid and is_not_start:
172-
builder.assert_eq(local.is_valid_not_start, local.is_valid * is_not_start);
172+
builder.assert_eq(
173+
local.is_valid_not_start,
174+
and::<AB::Expr>(local.is_valid, is_not_start),
175+
);
173176

174-
// if is_valid = 0, then is_boundary = 0, shift = 0
177+
// if !is_valid, then is_boundary = 0, shift = 0 (we will use this assumption later)
175178
let mut is_not_valid_when = builder.when(not::<AB::Expr>(local.is_valid));
176179
is_not_valid_when.assert_zero(local.is_boundary);
177180
is_not_valid_when.assert_zero(shift.clone());
178181

179-
// if is_valid_not_start = 1, then len = prev_len - 16, source = prev_source + 16,
180-
// and dest = prev_dest + 16
182+
// if is_valid_not_start, then len = prev_len - 16, source = prev_source + 16,
183+
// and dest = prev_dest + 16, shift = prev_shift
181184
let mut is_valid_not_start_when = builder.when(local.is_valid_not_start);
182185
is_valid_not_start_when
183186
.assert_eq(local.len[0], prev.len[0] - AB::Expr::from_canonical_u32(16));
184187
is_valid_not_start_when
185188
.assert_eq(local.source, prev.source + AB::Expr::from_canonical_u32(16));
186189
is_valid_not_start_when.assert_eq(local.dest, prev.dest + AB::Expr::from_canonical_u32(16));
190+
is_valid_not_start_when.assert_eq(local.shift[0], prev.shift[0]);
191+
is_valid_not_start_when.assert_eq(local.shift[1], prev.shift[1]);
192+
193+
// make sure if previous row is valid and not end, then local.is_valid = 1
194+
builder
195+
.when(prev_is_not_end - not::<AB::Expr>(prev.is_valid))
196+
.assert_one(local.is_valid);
187197

188198
// if prev.is_valid_start, then timestamp = prev_timestamp + is_shift_non_zero
189199
// since is_shift_non_zero degree is 2, we need to keep the degree of the condition to 1
190200
builder
191201
.when(not::<AB::Expr>(prev.is_valid_not_start) - not::<AB::Expr>(prev.is_valid))
192202
.assert_eq(local.timestamp, prev.timestamp + is_shift_non_zero.clone());
203+
193204
// if prev.is_valid_not_start and local.is_valid_not_start, then timestamp=prev_timestamp+8
194205
// prev.is_valid_not_start is the opposite of previous condition
195206
builder
@@ -239,7 +250,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
239250
.read(
240251
MemoryAddress::new(
241252
AB::Expr::from_canonical_u32(RV32_MEMORY_AS),
242-
local.source + AB::Expr::from_canonical_usize(idx * 4),
253+
local.source - AB::Expr::from_canonical_usize(16 - idx * 4),
243254
),
244255
*data,
245256
timestamp_pp(),
@@ -254,7 +265,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
254265
.write(
255266
MemoryAddress::new(
256267
AB::Expr::from_canonical_u32(RV32_MEMORY_AS),
257-
local.dest + AB::Expr::from_canonical_usize(idx * 4),
268+
local.dest - AB::Expr::from_canonical_usize(16 - idx * 4),
258269
),
259270
data.clone(),
260271
timestamp_pp(),
@@ -286,7 +297,9 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
286297
}
287298

288299
#[derive(derive_new::new, Clone, Copy)]
289-
pub struct MemcpyIterExecutor {}
300+
pub struct MemcpyIterExecutor {
301+
pub offset: usize,
302+
}
290303

291304
#[derive(Copy, Clone, Debug)]
292305
pub struct MemcpyIterMetadata {
@@ -378,12 +391,6 @@ pub struct MemcpyIterFiller {
378391

379392
pub type MemcpyIterChip<F> = VmChipWrapper<F, MemcpyIterFiller>;
380393

381-
#[derive(AlignedBytesBorrow, Clone)]
382-
#[repr(C)]
383-
struct MemcpyIterPreCompute {
384-
c: u8,
385-
}
386-
387394
impl<F, RA> PreflightExecutor<F, RA> for MemcpyIterExecutor
388395
where
389396
F: PrimeField32,
@@ -452,6 +459,8 @@ where
452459
let write_data: [u8; MEMCPY_LOOP_NUM_LIMBS] = array::from_fn(|j| {
453460
if j < 4 - shift as usize {
454461
record.var[idx].data[i][j + shift as usize]
462+
} else if i > 0 {
463+
record.var[idx].data[i - 1][j - (4 - shift as usize)]
455464
} else {
456465
record.var[idx - 1].data[i][j - (4 - shift as usize)]
457466
}
@@ -565,6 +574,18 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
565574
)
566575
};
567576

577+
// Fill memcpy loop record
578+
self.memcpy_loop_chip.add_new_loop(
579+
mem_helper,
580+
record.inner.from_pc,
581+
record.inner.from_timestamp,
582+
record.inner.dest,
583+
record.inner.source,
584+
record.inner.len,
585+
record.inner.shift,
586+
record.inner.register_aux.clone(),
587+
);
588+
568589
// 4 reads + 4 writes per iteration + (shift != 0) read for the loop header
569590
let timestamp = record.inner.from_timestamp
570591
+ ((num_rows - 1) << 3) as u32
@@ -583,27 +604,15 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
583604
let mut len =
584605
record.inner.len - ((num_rows - 1) << 4) as u32 - record.inner.shift as u32;
585606

586-
// Fill memcpy loop record
587-
self.memcpy_loop_chip.add_new_loop(
588-
mem_helper,
589-
record.inner.from_pc,
590-
record.inner.from_timestamp,
591-
record.inner.dest,
592-
record.inner.source,
593-
record.inner.len,
594-
record.inner.shift,
595-
record.inner.register_aux.clone(),
596-
);
597-
598607
// We are going to fill row in the reverse order
599608
chunk
600609
.rchunks_exact_mut(width)
601610
.zip(record.var.iter().enumerate().rev())
602611
.for_each(|(row, (idx, var))| {
603612
let cols: &mut MemcpyIterCols<F> = row.borrow_mut();
604613

605-
let is_end = idx == 0;
606-
let is_start = idx == num_rows - 1;
614+
let is_start = idx == 0;
615+
let is_end = idx == num_rows - 1;
607616

608617
// Range check len
609618
let len_u16_limbs = [len & 0xffff, len >> 16];
@@ -621,8 +630,6 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
621630

622631
// Fill memory read/write auxiliary columns
623632
if is_start {
624-
debug_assert_eq!(get_timestamp(false), record.inner.from_timestamp);
625-
626633
cols.write_aux.iter_mut().rev().for_each(|aux_col| {
627634
mem_helper.fill_zero(aux_col.as_mut());
628635
});
@@ -632,18 +639,20 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
632639
} else {
633640
mem_helper.fill(
634641
var.read_aux[3].prev_timestamp,
635-
timestamp,
642+
get_timestamp(true),
636643
cols.read_aux[3].as_mut(),
637644
);
638645
}
639646
cols.read_aux[..2].iter_mut().rev().for_each(|aux_col| {
640647
mem_helper.fill_zero(aux_col.as_mut());
641648
});
649+
650+
debug_assert_eq!(get_timestamp(false), record.inner.from_timestamp);
642651
} else {
643652
var.write_aux
644653
.iter()
654+
.zip(cols.write_aux.iter_mut())
645655
.rev()
646-
.zip(cols.write_aux.iter_mut().rev())
647656
.for_each(|(aux_record, aux_col)| {
648657
mem_helper.fill(
649658
aux_record.prev_timestamp,
@@ -657,8 +666,8 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
657666

658667
var.read_aux
659668
.iter()
669+
.zip(cols.read_aux.iter_mut())
660670
.rev()
661-
.zip(cols.read_aux.iter_mut().rev())
662671
.for_each(|(aux_record, aux_col)| {
663672
mem_helper.fill(
664673
aux_record.prev_timestamp,
@@ -672,10 +681,16 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
672681
cols.data_3 = var.data[2].map(F::from_canonical_u8);
673682
cols.data_2 = var.data[1].map(F::from_canonical_u8);
674683
cols.data_1 = var.data[0].map(F::from_canonical_u8);
675-
cols.is_boundary = F::from_canonical_u8(is_end as u8 - is_start as u8);
684+
cols.is_boundary = if is_end {
685+
F::ONE
686+
} else if is_start {
687+
F::NEG_ONE
688+
} else {
689+
F::ZERO
690+
};
676691
cols.is_valid_not_start = F::from_canonical_u8(1 - is_start as u8);
677692
cols.is_valid = F::ONE;
678-
cols.shift = [record.inner.shift % 2, record.inner.shift / 2]
693+
cols.shift = [record.inner.shift & 1, record.inner.shift >> 1]
679694
.map(F::from_canonical_u8);
680695
cols.len = [len & 0xffff, len >> 16].map(F::from_canonical_u32);
681696
cols.source = F::from_canonical_u32(source);
@@ -690,6 +705,12 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
690705
}
691706
}
692707

708+
#[derive(AlignedBytesBorrow, Clone)]
709+
#[repr(C)]
710+
struct MemcpyIterPreCompute {
711+
c: u8,
712+
}
713+
693714
impl<F: PrimeField32> Executor<F> for MemcpyIterExecutor {
694715
fn pre_compute_size(&self) -> usize {
695716
size_of::<MemcpyIterPreCompute>()

0 commit comments

Comments
 (0)