Skip to content

Commit 84bb711

Browse files
MaillewMaillew
committed
chore: some green ? when copying data[i] = i
1 parent c9df95b commit 84bb711

File tree

2 files changed

+148
-70
lines changed

2 files changed

+148
-70
lines changed

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

Lines changed: 115 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -71,15 +71,9 @@ pub struct MemcpyIterCols<T> {
7171
pub data_4: [T; MEMCPY_LOOP_NUM_LIMBS],
7272
pub read_aux: [MemoryReadAuxCols<T>; 4],
7373
pub write_aux: [MemoryWriteAuxCols<T, MEMCPY_LOOP_NUM_LIMBS>; 4],
74-
} // number of columns is 68
75-
// other air constraints not that confident, check myself to see if confident with correctness
76-
77-
/*
78-
talk about bug in #zk-circuits the same way that previous comment was made
79-
- after have concrete idea of what the bug is, and why its failing
80-
- i mean i kinda do tho lol? just making sure that the AIR constraints are correct and make sense
81-
82-
*/
74+
// 1-hot encoding for source = 0, 4, 8
75+
pub is_source_0_4_8: [T; 3],
76+
}
8377

8478
pub const NUM_MEMCPY_ITER_COLS: usize = size_of::<MemcpyIterCols<u8>>();
8579

@@ -122,22 +116,27 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
122116
.fold(AB::Expr::ZERO, |acc, (i, x)| {
123117
acc + (*x) * AB::Expr::from_canonical_u32(i as u32 + 1)
124118
});
125-
let is_shift_non_zero = local.shift.iter().fold(AB::Expr::ZERO, |acc, x| acc + (*x));
119+
let is_shift_non_zero = local
120+
.shift
121+
.iter()
122+
.fold(AB::Expr::ZERO, |acc: <AB as AirBuilder>::Expr, x| {
123+
acc + (*x)
124+
});
126125
let is_shift_zero = not::<AB::Expr>(is_shift_non_zero.clone());
127126
let is_shift_one = local.shift[0];
128127
let is_shift_two = local.shift[1];
129128
let is_shift_three = local.shift[2];
130129

130+
let is_source_0 = local.is_source_0_4_8[0];
131+
let is_source_4 = local.is_source_0_4_8[1];
132+
let is_source_8 = local.is_source_0_4_8[2];
133+
let is_source_small = or::<AB::Expr>(is_source_0, or::<AB::Expr>(is_source_4, is_source_8));
131134
let is_end =
132135
(local.is_boundary + AB::Expr::ONE) * local.is_boundary * (AB::F::TWO).inverse();
133136
let is_not_start = (local.is_boundary + AB::Expr::ONE)
134137
* (AB::Expr::TWO - local.is_boundary)
135138
* (AB::F::TWO).inverse();
136139

137-
let prev_is_not_start = (prev.is_boundary + AB::Expr::ONE)
138-
* (AB::Expr::TWO - prev.is_boundary)
139-
* (AB::F::TWO).inverse();
140-
141140
let prev_is_not_end = not::<AB::Expr>(
142141
// returns 0 if prev.isBoundary == 1, 1 otherwise, since we take the not
143142
(prev.is_boundary + AB::Expr::ONE) * prev.is_boundary * (AB::F::TWO).inverse(),
@@ -153,6 +152,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
153152
// (local.data_2[shift..4], local.data_1[0..shift]),
154153
// (local.data_3[shift..4], local.data_2[0..shift]),
155154
// (local.data_4[shift..4], local.data_3[0..shift])
155+
// local.data-1 = tracing_read data
156156
let write_data_pairs = [
157157
(prev.data_4, local.data_1),
158158
(local.data_1, local.data_2),
@@ -163,25 +163,26 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
163163
let write_data = write_data_pairs
164164
.iter()
165165
.map(|(prev_data, next_data)| {
166+
// iterate i from 0 ... 3
166167
array::from_fn::<_, MEMCPY_LOOP_NUM_LIMBS, _>(|i| {
167168
is_shift_zero.clone() * (next_data[i])
168169
+ is_shift_one.clone()
169-
* (if i < 3 {
170-
next_data[i + 1]
170+
* (if i < 1 {
171+
prev_data[i + 3]
171172
} else {
172-
prev_data[i - 3]
173+
next_data[i - 1]
173174
})
174175
+ is_shift_two.clone()
175176
* (if i < 2 {
176-
next_data[i + 2]
177+
prev_data[i + 2]
177178
} else {
178-
prev_data[i - 2]
179+
next_data[i - 2]
179180
})
180181
+ is_shift_three.clone()
181-
* (if i < 1 {
182-
next_data[i + 3]
182+
* (if i < 3 {
183+
prev_data[i + 1]
183184
} else {
184-
prev_data[i - 1]
185+
next_data[i - 3]
185186
})
186187
})
187188
})
@@ -197,7 +198,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
197198
// is_valid_not_start = is_valid and is_not_start:
198199
builder.assert_eq(
199200
local.is_valid_not_start,
200-
and::<AB::Expr>(local.is_valid, is_not_start),
201+
and::<AB::Expr>(local.is_valid, is_not_start.clone()),
201202
);
202203

203204
// is_shift_non_zero_or_not_start is correct
@@ -206,13 +207,26 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
206207
or::<AB::Expr>(is_shift_non_zero.clone(), local.is_valid_not_start),
207208
);
208209

210+
// builder.assert_eq(
211+
// is_valid_is_start.clone() * (is_shift_zero.clone() * local.source),
212+
// is_valid_is_start.clone()
213+
// * (is_shift_zero.clone() * (prev.source + AB::Expr::from_canonical_u32(16))),
214+
// );
215+
216+
// builder.assert_eq(
217+
// is_not_start.clone() * local.source,
218+
// is_not_start.clone() * (prev.source + AB::Expr::from_canonical_u32(16)),
219+
// );
220+
209221
// if !is_valid, then is_boundary = 0, shift = 0 (we will use this assumption later)
210-
let mut is_not_valid_when = builder.when(not::<AB::Expr>(local.is_valid));
211-
is_not_valid_when.assert_zero(local.is_boundary);
212-
is_not_valid_when.assert_zero(shift.clone());
222+
// let mut is_not_valid_when = builder.when(not::<AB::Expr>(local.is_valid));
223+
// is_not_valid_when.assert_zero(local.is_boundary);
224+
// is_not_valid_when.assert_zero(shift.clone());
213225

214226
// if is_valid_not_start, then len = prev_len - 16, source = prev_source + 16,
215227
// and dest = prev_dest + 16, shift = prev_shift
228+
229+
// is_valid_not_start is degree 1, since it uses the variable as a precondition
216230
let mut is_valid_not_start_when = builder.when(local.is_valid_not_start);
217231
is_valid_not_start_when.assert_eq(len.clone(), prev_len - AB::Expr::from_canonical_u32(16));
218232

@@ -223,12 +237,15 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
223237
error is if the initial source value is < 12, then -16, we do a saturating sub so its bounded below by 0
224238
then, it results in a mismatch of values
225239
*/
226-
is_valid_not_start_when.assert_eq(
227-
prev_is_not_start.clone() * local.source,
228-
prev_is_not_start.clone() * (prev.source + AB::Expr::from_canonical_u32(16)),
229-
);
240+
// degree 1 * deg 2 * deg 1 = deg 4
241+
242+
// is_valid_not_start_when.assert_eq(
243+
// prev_is_not_start.clone() * local.source,
244+
// prev_is_not_start.clone() * (prev.source + AB::Expr::from_canonical_u32(16)),
245+
// );
230246

231247
is_valid_not_start_when.assert_eq(local.dest, prev.dest + AB::Expr::from_canonical_u32(16));
248+
232249
local
233250
.shift
234251
.iter()
@@ -246,7 +263,7 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
246263
// since is_shift_non_zero degree is 2, we need to keep the degree of the condition to 1
247264
builder
248265
.when(not::<AB::Expr>(prev.is_valid_not_start) - not::<AB::Expr>(prev.is_valid))
249-
.assert_eq(local.timestamp, prev.timestamp + is_shift_non_zero);
266+
.assert_eq(local.timestamp, prev.timestamp + is_shift_non_zero.clone());
250267

251268
// if prev.is_valid_not_start and local.is_valid_not_start, then timestamp=prev_timestamp+8
252269
// prev.is_valid_not_start is the opposite of previous condition
@@ -269,10 +286,20 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
269286
we only send if is_boundary = -1 or 1
270287
start or end
271288
*/
289+
290+
// local_source_0_4_8
291+
eprintln!("is_source_small: {:?}", is_source_small);
292+
eprintln!("is_shift_non_zero: {:?}", is_shift_non_zero);
293+
eprintln!(
294+
"current timestamp: {:?}",
295+
local.timestamp * AB::Expr::from_canonical_u32(1)
296+
);
297+
272298
self.memcpy_bus
273299
.send(
274300
local.timestamp
275301
+ (local.is_boundary + AB::Expr::ONE) * AB::Expr::from_canonical_usize(4),
302+
// - (is_shift_non_zero.clone() * is_source_small.clone()),
276303
local.dest,
277304
local.source,
278305
len.clone(),
@@ -291,6 +318,23 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
291318
local.is_valid_not_start
292319
};
293320

321+
/*
322+
7 values go:
323+
address sspace
324+
pointer to address
325+
data (4)
326+
timestamp
327+
data chosen is wrong lol
328+
*/
329+
// memory bridge data is tracing_read
330+
// based off of the unshifted data values
331+
332+
// tracing_write writes the corectly shifted values
333+
334+
eprintln!(
335+
"memory bridge read_data: {:?}",
336+
data.clone().map(|x| x * (AB::Expr::from_canonical_u32(1)))
337+
);
294338
self.memory_bridge
295339
.read(
296340
MemoryAddress::new(
@@ -303,8 +347,21 @@ impl<AB: InteractionBuilder> Air<AB> for MemcpyIterAir {
303347
)
304348
.eval(builder, is_valid_read.clone());
305349
});
306-
350+
eprintln!(
351+
"memory bridge data write_data: {:?}",
352+
write_data
353+
.iter()
354+
.map(|x| x.clone().map(|y| y * (AB::Expr::from_canonical_u32(1))))
355+
.collect::<Vec<_>>()
356+
);
307357
// Write final data to registers
358+
write_data_pairs.iter().for_each(|(prev_data, next_data)| {
359+
eprintln!(
360+
"prev_data: {:?}, next_data: {:?}",
361+
prev_data.map(|x| x * (AB::Expr::from_canonical_u32(1))),
362+
next_data.map(|x| x * (AB::Expr::from_canonical_u32(1))),
363+
);
364+
});
308365
write_data.iter().enumerate().for_each(|(idx, data)| {
309366
self.memory_bridge
310367
.write(
@@ -531,19 +588,29 @@ where
531588
// );
532589
source = source.saturating_sub(12 * (shift != 0) as u32);
533590
if shift != 0 {
534-
if source >= 4 {
535-
record.var[0].data[3] = tracing_read(
536-
state.memory,
537-
RV32_MEMORY_AS,
538-
source - 4, // correct seed for mixing
539-
&mut record.var[0].read_aux[3].prev_timestamp,
540-
);
541-
// eprintln!("record.var[0].data[3]: {:?}", record.var[0].data[3]);
542-
} else {
543-
record.var[0].data[3] = [0; 4];
544-
}
591+
// if source >= 4 {
592+
record.var[0].data[3] = tracing_read(
593+
state.memory,
594+
RV32_MEMORY_AS,
595+
source - 4 * (source >= 4) as u32, // correct seed for mixing
596+
&mut record.var[0].read_aux[3].prev_timestamp,
597+
);
598+
// eprintln!("record.var[0].data[3]: {:?}", record.var[0].data[3]);
599+
// } else {
600+
// record.var[0].data[3] = tracing_read(
601+
// state.memory,
602+
// RV32_MEMORY_AS,
603+
// source,
604+
// &mut record.var[0].read_aux[3].prev_timestamp,
605+
// );
606+
// }
545607
} else {
546-
record.var[0].data[3] = [0; 4];
608+
record.var[0].data[3] = tracing_read(
609+
state.memory,
610+
RV32_MEMORY_AS,
611+
source,
612+
&mut record.var[0].read_aux[3].prev_timestamp,
613+
);
547614
}
548615

549616
// Fill record.var for the rest of the rows of iteration trace
@@ -571,23 +638,10 @@ where
571638
record.var[idx].data[i][j - shift as usize]
572639
}
573640
});
574-
// let mut good = true;
575-
// for t in 0..1 {
576-
// if write_data[t + 1] != write_data[t] + 1 {
577-
// good = false;
578-
// }
579-
// }
580-
// if !good {
581-
// eprintln!("write_data: {:?}", write_data);
582-
// eprintln!(
583-
// "source, dest, num_iters, first_word: {:?}, {:?}, {:?}, {:?}",
584-
// source, dest, num_iters, first_word
585-
// );
586-
// eprintln!("record.var[0].data[3]: {:?}", record.var[0].data[3]);
587-
// eprintln!("idx: {:?}", idx);
588-
// }
641+
eprintln!("execute write_data: {:?}", write_data);
589642
write_data
590643
});
644+
eprintln!("record.var[idx].data: {:?}", record.var[idx].data);
591645
writes_data.iter().enumerate().for_each(|(i, write_data)| {
592646
tracing_write(
593647
state.memory,
@@ -850,7 +904,8 @@ impl<F: PrimeField32> TraceFiller<F> for MemcpyIterFiller {
850904
cols.source = F::from_canonical_u32(source);
851905
cols.dest = F::from_canonical_u32(dest);
852906
cols.timestamp = F::from_canonical_u32(get_timestamp(false));
853-
907+
cols.is_source_0_4_8 =
908+
[source == 0, source == 4, source == 8].map(F::from_bool);
854909
dest = dest.saturating_sub(16);
855910

856911
if source < 16 {

0 commit comments

Comments
 (0)