Skip to content

Commit 125b787

Browse files
pjabbarzadepjabbarzade
committed
only increase timestamp on actual read
1 parent 7e259eb commit 125b787

File tree

5 files changed

+126
-36
lines changed

5 files changed

+126
-36
lines changed

‎Cargo.lock‎

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎extensions/memcpy/circuit/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,4 @@ derive-new.workspace = true
2222
derive_more = { workspace = true, features = ["from"] }
2323
serde.workspace = true
2424
strum = { workspace = true }
25+
tracing.workspace = true

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

Lines changed: 95 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ pub struct MemcpyIterCols<T> {
6161
pub shift: [T; 2],
6262
pub is_valid: T,
6363
pub is_valid_not_start: T,
64-
pub is_shift_zero: T,
64+
pub is_shift_non_zero: T,
6565
// -1 for the first iteration, 1 for the last iteration, 0 for the middle iterations
6666
pub is_boundary: T,
6767
pub data_1: [T; MEMCPY_LOOP_NUM_LIMBS],
@@ -99,14 +99,14 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
9999
let local: &MemcpyIterCols<AB::Var> = (*local).borrow();
100100

101101
let timestamp: AB::Var = local.timestamp;
102-
let mut timestamp_delta: usize = 0;
103-
let mut timestamp_pp = || {
104-
timestamp_delta += 1;
105-
timestamp + AB::Expr::from_canonical_usize(timestamp_delta - 1)
102+
let mut timestamp_delta: AB::Expr = AB::Expr::ZERO;
103+
let mut timestamp_pp = |timestamp_increase_value: AB::Expr| {
104+
timestamp_delta += timestamp_increase_value.clone();
105+
timestamp + timestamp_delta.clone() - timestamp_increase_value.clone()
106106
};
107107

108108
let shift = local.shift[0] * AB::Expr::TWO + local.shift[1];
109-
let is_shift_non_zero = not::<AB::Expr>(local.is_shift_zero);
109+
let is_shift_zero = not::<AB::Expr>(local.is_shift_non_zero);
110110
let is_shift_one = and::<AB::Expr>(local.shift[0], not::<AB::Expr>(local.shift[1]));
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]);
@@ -141,7 +141,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
141141
.iter()
142142
.map(|(prev_data, next_data)| {
143143
array::from_fn::<_, MEMCPY_LOOP_NUM_LIMBS, _>(|i| {
144-
local.is_shift_zero.clone() * (next_data[i])
144+
is_shift_zero.clone() * (next_data[i])
145145
+ is_shift_one.clone()
146146
* (if i < 3 {
147147
next_data[i + 1]
@@ -167,7 +167,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
167167
builder.assert_bool(local.is_valid);
168168
local.shift.iter().for_each(|x| builder.assert_bool(*x));
169169
builder.assert_bool(local.is_valid_not_start);
170-
builder.assert_bool(local.is_shift_zero);
170+
builder.assert_bool(local.is_shift_non_zero);
171171
// is_boundary is either -1, 0 or 1
172172
builder.assert_tern(local.is_boundary + AB::Expr::ONE);
173173

@@ -178,7 +178,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
178178
);
179179

180180
// is_shift_non_zero is correct
181-
builder.assert_eq(local.is_shift_zero, not::<AB::Expr>(or::<AB::Expr>(local.shift[0], local.shift[1])));
181+
builder.assert_eq(local.is_shift_non_zero, or::<AB::Expr>(local.shift[0], local.shift[1]));
182182

183183
// if !is_valid, then is_boundary = 0, shift = 0 (we will use this assumption later)
184184
let mut is_not_valid_when = builder.when(not::<AB::Expr>(local.is_valid));
@@ -205,7 +205,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
205205
// since is_shift_non_zero degree is 2, we need to keep the degree of the condition to 1
206206
builder
207207
.when(not::<AB::Expr>(prev.is_valid_not_start) - not::<AB::Expr>(prev.is_valid))
208-
.assert_eq(local.timestamp, prev.timestamp + is_shift_non_zero.clone());
208+
.assert_eq(local.timestamp, prev.timestamp + local.is_shift_non_zero);
209209

210210
// if prev.is_valid_not_start and local.is_valid_not_start, then timestamp=prev_timestamp+8
211211
// prev.is_valid_not_start is the opposite of previous condition
@@ -247,7 +247,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
247247
.enumerate()
248248
.for_each(|(idx, (data, read_aux))| {
249249
let is_valid_read = if idx == 3 {
250-
or::<AB::Expr>(is_shift_non_zero.clone(), local.is_valid_not_start)
250+
or::<AB::Expr>(local.is_shift_non_zero, local.is_valid_not_start)
251251
} else {
252252
local.is_valid_not_start.into()
253253
};
@@ -259,10 +259,10 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
259259
local.source - AB::Expr::from_canonical_usize(16 - idx * 4),
260260
),
261261
*data,
262-
timestamp_pp(),
262+
timestamp_pp(is_valid_read.clone()),
263263
read_aux,
264264
)
265-
.eval(builder, is_valid_read);
265+
.eval(builder, is_valid_read.clone());
266266
});
267267

268268
// Write final data to registers
@@ -274,7 +274,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
274274
local.dest - AB::Expr::from_canonical_usize(16 - idx * 4),
275275
),
276276
data.clone(),
277-
timestamp_pp(),
277+
timestamp_pp(local.is_valid_not_start.into()),
278278
&local.write_aux[idx],
279279
)
280280
.eval(builder, local.is_valid_not_start);
@@ -294,10 +294,10 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
294294
),
295295
];
296296
self.range_bus
297-
.push(local.len[0].clone(), len_bits_limit[0].clone(), true)
297+
.push(local.len[0], len_bits_limit[0].clone(), true)
298298
.eval(builder, local.is_valid);
299299
self.range_bus
300-
.push(local.len[1].clone(), len_bits_limit[1].clone(), true)
300+
.push(local.len[1], len_bits_limit[1].clone(), true)
301301
.eval(builder, local.is_valid);
302302
}
303303
}
@@ -560,19 +560,26 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
560560
let mut sizes = Vec::with_capacity(rows_used >> 1);
561561
let mut chunks = Vec::with_capacity(rows_used >> 1);
562562

563+
let mut num_loops: usize = 0;
564+
let mut num_iters: usize = 0;
565+
563566
while !trace.is_empty() {
564567
let record: &MemcpyIterRecordHeader = unsafe { get_record_from_slice(&mut trace, ()) };
565568
let num_rows = ((record.len - record.shift as u32) >> 4) as usize + 1;
566569
let (chunk, rest) = trace.split_at_mut(width * num_rows as usize);
567570
sizes.push(num_rows);
568571
chunks.push(chunk);
569572
trace = rest;
573+
num_loops += 1;
574+
num_iters += num_rows;
570575
}
571-
576+
tracing::info!("num_loops: {:?}, num_iters: {:?}", num_loops, num_iters);
577+
572578
chunks
573579
.par_iter_mut()
574580
.zip(sizes.par_iter())
575-
.for_each(|(chunk, &num_rows)| {
581+
.enumerate()
582+
.for_each(|(row_idx, (chunk, &num_rows))| {
576583
let record: MemcpyIterRecordMut = unsafe {
577584
get_record_from_slice(
578585
chunk,
@@ -694,7 +701,7 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
694701
} else {
695702
F::ZERO
696703
};
697-
cols.is_shift_zero = F::from_canonical_u8((record.inner.shift == 0) as u8);
704+
cols.is_shift_non_zero = F::from_canonical_u8((record.inner.shift != 0) as u8);
698705
cols.is_valid_not_start = F::from_canonical_u8(1 - is_start as u8);
699706
cols.is_valid = F::ONE;
700707
cols.shift = [record.inner.shift & 1, record.inner.shift >> 1]
@@ -707,8 +714,77 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
707714
dest -= 16;
708715
source -= 16;
709716
len += 16;
717+
718+
if row_idx == 0 && is_start {
719+
tracing::info!("first_roooooow, timestamp: {:?}, dest: {:?}, source: {:?}, len_0: {:?}, len_1: {:?}, shift: {:?}, is_valid: {:?}, is_valid_not_start: {:?}, is_shift_non_zero: {:?}, is_boundary: {:?}, data_1: {:?}, data_2: {:?}, data_3: {:?}, data_4: {:?}, read_aux: {:?}, read_aux_lt: {:?}",
720+
cols.timestamp.as_canonical_u32(),
721+
cols.dest.as_canonical_u32(),
722+
cols.source.as_canonical_u32(),
723+
cols.len[0].as_canonical_u32(),
724+
cols.len[1].as_canonical_u32(),
725+
cols.shift[1].as_canonical_u32() * 2 + cols.shift[0].as_canonical_u32(),
726+
cols.is_valid.as_canonical_u32(),
727+
cols.is_valid_not_start.as_canonical_u32(),
728+
cols.is_shift_non_zero.as_canonical_u32(),
729+
cols.is_boundary.as_canonical_u32(),
730+
cols.data_1.map(|x| x.as_canonical_u32()).to_vec(),
731+
cols.data_2.map(|x| x.as_canonical_u32()).to_vec(),
732+
cols.data_3.map(|x| x.as_canonical_u32()).to_vec(),
733+
cols.data_4.map(|x| x.as_canonical_u32()).to_vec(),
734+
cols.read_aux.map(|x| x.get_base().prev_timestamp.as_canonical_u32()).to_vec(),
735+
cols.read_aux.map(|x| x.get_base().timestamp_lt_aux.lower_decomp.iter().map(|x| x.as_canonical_u32()).collect::<Vec<_>>()).to_vec());
736+
}
710737
});
711738
});
739+
chunks.iter().enumerate().map(|(row_idx, chunk)| {
740+
chunk.chunks_exact(width)
741+
.enumerate()
742+
.for_each(|(idx, row)| {
743+
let cols: &MemcpyIterCols<F> = row.borrow();
744+
let is_valid_not_start = cols.is_valid_not_start.as_canonical_u32() != 0;
745+
let is_shift_non_zero = cols.is_shift_non_zero.as_canonical_u32() != 0;
746+
let mut bad_col = false;
747+
cols.read_aux.iter().enumerate().for_each(|(idx, aux)| {
748+
if is_valid_not_start || (is_shift_non_zero && idx == 3) {
749+
let prev_t = aux.get_base().prev_timestamp.as_canonical_u32();
750+
let curr_t = cols.timestamp.as_canonical_u32();
751+
let ts_lt = aux.get_base().timestamp_lt_aux.lower_decomp.iter()
752+
.enumerate()
753+
.fold(F::ZERO, |acc, (i, &val)| {
754+
acc + val * F::from_canonical_usize(1 << (i * 17))
755+
}).as_canonical_u32();
756+
if curr_t + idx as u32 != ts_lt + prev_t + 1 {
757+
bad_col = true;
758+
}
759+
}
760+
});
761+
if bad_col {
762+
tracing::info!("row_idx: {:?}, idx: {:?}, timestamp: {:?}, dest: {:?}, source: {:?}, len_0: {:?}, len_1: {:?}, shift_0: {:?}, shift_1: {:?}, is_valid: {:?}, is_valid_not_start: {:?}, is_shift_non_zero: {:?}, is_boundary: {:?}, data_1: {:?}, data_2: {:?}, data_3: {:?}, data_4: {:?}, read_aux: {:?}, read_aux_lt: {:?}",
763+
row_idx,
764+
idx,
765+
cols.timestamp.as_canonical_u32(),
766+
cols.dest.as_canonical_u32(),
767+
cols.source.as_canonical_u32(),
768+
cols.len[0].as_canonical_u32(),
769+
cols.len[1].as_canonical_u32(),
770+
cols.shift[0].as_canonical_u32(),
771+
cols.shift[1].as_canonical_u32(),
772+
cols.is_valid.as_canonical_u32(),
773+
cols.is_valid_not_start.as_canonical_u32(),
774+
cols.is_shift_non_zero.as_canonical_u32(),
775+
cols.is_boundary.as_canonical_u32(),
776+
cols.data_1.map(|x| x.as_canonical_u32()).to_vec(),
777+
cols.data_2.map(|x| x.as_canonical_u32()).to_vec(),
778+
cols.data_3.map(|x| x.as_canonical_u32()).to_vec(),
779+
cols.data_4.map(|x| x.as_canonical_u32()).to_vec(),
780+
cols.read_aux.map(|x| x.get_base().prev_timestamp.as_canonical_u32()).to_vec(),
781+
cols.read_aux.map(|x| x.get_base().timestamp_lt_aux.lower_decomp.iter().map(|x| x.as_canonical_u32()).collect::<Vec<_>>()).to_vec());
782+
// cols.write_aux.map(|x| x.get_base().prev_timestamp.as_canonical_u32()).to_vec(),
783+
// cols.write_aux.map(|x| x.prev_data.map(|x| x.as_canonical_u32()).to_vec()).to_vec());
784+
}
785+
});
786+
});
787+
// assert!(false);
712788
}
713789
}
714790

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -432,6 +432,20 @@ impl MemcpyLoopChip {
432432
});
433433
cols.source_minus_twelve_carry = F::from_bool((record.source & 0x0ffff) < 12);
434434
cols.to_source_minus_twelve_carry = F::from_bool((to_source & 0x0ffff) < 12);
435+
436+
// tracing::info!("timestamp: {:?}, pc: {:?}, dest: {:?}, source: {:?}, len: {:?}, shift: {:?}, is_valid: {:?}, to_timestamp: {:?}, to_dest: {:?}, to_source: {:?}, to_len: {:?}, write_aux: {:?}",
437+
// cols.from_state.timestamp.as_canonical_u32(),
438+
// cols.from_state.pc.as_canonical_u32(),
439+
// u32::from_le_bytes(cols.dest.map(|x| x.as_canonical_u32() as u8)),
440+
// u32::from_le_bytes(cols.source.map(|x| x.as_canonical_u32() as u8)),
441+
// u32::from_le_bytes(cols.len.map(|x| x.as_canonical_u32() as u8)),
442+
// cols.shift[1].as_canonical_u32() * 2 + cols.shift[0].as_canonical_u32(),
443+
// cols.is_valid.as_canonical_u32(),
444+
// cols.to_timestamp.as_canonical_u32(),
445+
// u32::from_le_bytes(cols.to_dest.map(|x| x.as_canonical_u32() as u8)),
446+
// u32::from_le_bytes(cols.to_source.map(|x| x.as_canonical_u32() as u8)),
447+
// cols.to_len.as_canonical_u32(),
448+
// cols.write_aux.map(|x| x.prev_timestamp.as_canonical_u32()).to_vec());
435449
}
436450
RowMajorMatrix::new(rows, NUM_MEMCPY_LOOP_COLS)
437451
}

‎extensions/memcpy/tests/src/lib.rs‎

Lines changed: 15 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ mod tests {
1313
SharedVariableRangeCheckerChip, VariableRangeCheckerAir, VariableRangeCheckerBus,
1414
VariableRangeCheckerChip,
1515
};
16-
use openvm_instructions::{instruction::Instruction, LocalOpcode, VmOpcode};
16+
use openvm_instructions::{instruction::Instruction, riscv::{RV32_MEMORY_AS, RV32_REGISTER_AS}, LocalOpcode, VmOpcode};
1717
use openvm_memcpy_circuit::{
1818
MemcpyBus, MemcpyIterAir, MemcpyIterChip, MemcpyIterExecutor, MemcpyIterFiller,
1919
MemcpyLoopAir, MemcpyLoopChip, A1_REGISTER_PTR, A2_REGISTER_PTR, A3_REGISTER_PTR,
@@ -108,13 +108,13 @@ mod tests {
108108
}
109109
}
110110

111-
tester.write(2, (source_offset + word_idx as u32 * 4) as usize, word_data);
111+
tester.write(RV32_MEMORY_AS as usize, (source_offset + word_idx as u32 * 4) as usize, word_data);
112112
}
113113

114114
// Set up registers that the memcpy instruction will read from
115115
// destination address
116116
tester.write::<4>(
117-
1,
117+
RV32_REGISTER_AS as usize,
118118
if shift == 0 {
119119
A3_REGISTER_PTR
120120
} else {
@@ -124,13 +124,13 @@ mod tests {
124124
);
125125
// length
126126
tester.write::<4>(
127-
1,
127+
RV32_REGISTER_AS as usize,
128128
A2_REGISTER_PTR,
129129
len.to_le_bytes().map(F::from_canonical_u8),
130130
);
131131
// source address
132132
tester.write::<4>(
133-
1,
133+
RV32_REGISTER_AS as usize,
134134
if shift == 0 {
135135
A4_REGISTER_PTR
136136
} else {
@@ -177,11 +177,11 @@ mod tests {
177177
// passes all constraints.
178178
//////////////////////////////////////////////////////////////////////////////////////
179179

180-
#[test_case(0, 1)]
181-
#[test_case(1, 100)]
182-
#[test_case(2, 100)]
183-
#[test_case(3, 100)]
184-
fn rand_memcpy_iter_test(shift: u32, num_ops: usize) {
180+
#[test_case(0, 1, 20)]
181+
#[test_case(1, 100, 20)]
182+
#[test_case(2, 100, 20)]
183+
#[test_case(3, 100, 20)]
184+
fn rand_memcpy_iter_test(shift: u32, num_ops: usize, len: u32) {
185185
let mut rng = create_seeded_rng();
186186

187187
let mut tester = VmChipTestBuilder::default();
@@ -190,7 +190,6 @@ mod tests {
190190
for _ in 0..num_ops {
191191
let source_offset = rng.gen_range(0..250) * 4; // Ensure word alignment
192192
let dest_offset = rng.gen_range(500..750) * 4; // Ensure word alignment
193-
let len: u32 = rng.gen_range(100..=200);
194193
let source_data: Vec<u8> = (0..len.div_ceil(4) * 4)
195194
.map(|_| rng.gen_range(0..=u8::MAX))
196195
.collect();
@@ -222,11 +221,11 @@ mod tests {
222221
tester.simple_test().expect("Verification failed");
223222
}
224223

225-
#[test_case(0, 100)]
226-
#[test_case(1, 100)]
227-
#[test_case(2, 100)]
228-
#[test_case(3, 100)]
229-
fn rand_memcpy_iter_test_persistent(shift: u32, num_ops: usize) {
224+
#[test_case(0, 100, 20)]
225+
#[test_case(1, 100, 20)]
226+
#[test_case(2, 100, 20)]
227+
#[test_case(3, 100, 20)]
228+
fn rand_memcpy_iter_test_persistent(shift: u32, num_ops: usize, len: u32) {
230229
let mut rng = create_seeded_rng();
231230

232231
let mut tester = VmChipTestBuilder::default_persistent();
@@ -235,7 +234,6 @@ mod tests {
235234
for _ in 0..num_ops {
236235
let source_offset = rng.gen_range(0..250) * 4; // Ensure word alignment
237236
let dest_offset = rng.gen_range(500..750) * 4; // Ensure word alignment
238-
let len: u32 = rng.gen_range(100..=200);
239237
let source_data: Vec<u8> = (0..len.div_ceil(4) * 4)
240238
.map(|_| rng.gen_range(0..=u8::MAX))
241239
.collect();

0 commit comments

Comments
 (0)