Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
memory.test.cpp
Go to the documentation of this file.
1#include <gmock/gmock.h>
2#include <gtest/gtest.h>
3
4#include <cstdint>
5
17
18namespace bb::avm2::constraining {
19namespace {
20
21using simulation::MemoryEvent;
22using simulation::RangeCheckEvent;
23
24using tracegen::MemoryTraceBuilder;
25using tracegen::PrecomputedTraceBuilder;
26using tracegen::RangeCheckTraceBuilder;
27using tracegen::TestTraceContainer;
29using C = Column;
31
32TEST(MemoryConstrainingTest, EmptyRow)
33{
34 check_relation<memory>(testing::empty_trace());
35}
36
37// Several memory events with trace generation.
38TEST(MemoryConstrainingTest, MultipleEventsWithTraceGen)
39{
40 TestTraceContainer trace;
41 MemoryTraceBuilder memory_trace_builder;
42 PrecomputedTraceBuilder precomputed_trace_builder;
43 RangeCheckTraceBuilder range_check_trace_builder;
44
45 std::vector<MemoryEvent> mem_events = {
46 // 1) READ: space_id = 17, addr = 120, clk = 13787, value = 0, tag = FF
47 {
48 .execution_clk = 13787,
50 .addr = 120,
52 .space_id = 17,
53 },
54 // 2) WRITE: space_id = 17, addr = 120, clk = 13787, value = 12345, tag = U16
55 {
56 .execution_clk = 13787,
58 .addr = 120,
60 .space_id = 17,
61 },
62 // 3) WRITE: space_id = 17, addr = 120, clk = 13788, value = 123, tag = U32
63 {
64 .execution_clk = 13788,
66 .addr = 120,
68 .space_id = 17,
69 },
70 // 4) READ: space_id = 17, addr = 120, clk = 25000, value = 123, tag = U32
71 {
72 .execution_clk = 25000,
74 .addr = 120,
76 .space_id = 17,
77 },
78 // 5) WRITE: space_id = 17, addr = 121, clk = 45, value = 99999, tag = U128
79 {
80 .execution_clk = 45,
82 .addr = 121,
84 .space_id = 17,
85 },
86 // 6) READ: space_id = 17, addr = 121, clk = 49, value = 99999, tag = U128
87 {
88 .execution_clk = 49,
90 .addr = 121,
92 .space_id = 17,
93 },
94 // 7) READ: space_id = 17, addr = 121, clk = 49, value = 99999, tag = U128
95 {
96 .execution_clk = 49,
98 .addr = 121,
100 .space_id = 17,
101 },
102 // 8) READ: space_id = 17, addr = 121, clk = 765, value = 99999, tag = U128
103 {
104 .execution_clk = 765,
106 .addr = 121,
108 .space_id = 17,
109 },
110 // 9) WRITE: space_id = 18, addr = 2, clk = 10, value = p-1, tag = FF
111 {
112 .execution_clk = 10,
114 .addr = 2,
116 .space_id = 18,
117 },
118 };
119
120 // Range check event per non-FF memory write event.
121 std::vector<RangeCheckEvent> range_check_events = {
122 {
123 .value = 12345,
124 .num_bits = 16,
125 },
126 {
127 .value = 123,
128 .num_bits = 32,
129 },
130 {
131 .value = 99999,
132 .num_bits = 128,
133 },
134 };
135
136 precomputed_trace_builder.process_sel_range_8(trace);
137 precomputed_trace_builder.process_sel_range_16(trace);
138 precomputed_trace_builder.process_misc(trace, 1 << 16);
139 precomputed_trace_builder.process_tag_parameters(trace);
140 range_check_trace_builder.process(range_check_events, trace);
141 memory_trace_builder.process(mem_events, trace);
142
143 // For the selector consistency, we need to make the read/write come from some trace.
144 trace.visit_column(Column::memory_sel,
145 [&](uint32_t row, const FF&) { trace.set(Column::memory_sel_register_op_0_, row, 1); });
146
147 check_relation<memory>(trace);
148 check_all_interactions<MemoryTraceBuilder>(trace);
149}
150
151// Trace must be contiguous.
152TEST(MemoryConstrainingTest, ContiguousTrace)
153{
154 TestTraceContainer trace({
155 { { C::precomputed_first_row, 1 }, { C::memory_sel, 0 } },
156 { { C::memory_sel, 1 } },
157 { { C::memory_sel, 1 } },
158 { { C::memory_sel, 1 } },
159 { { C::memory_sel, 0 } },
160 });
161
162 check_relation<memory>(trace, memory::SR_MEM_CONTINUITY);
163
164 // Mutate the trace to make it non-contiguous.
165 trace.set(C::memory_sel, 2, 0);
166 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_MEM_CONTINUITY), "MEM_CONTINUITY");
167}
168
169// Boolean selector for range check is active at all active rows except the last one.
170TEST(MemoryConstrainingTest, SelRngChk)
171{
172 TestTraceContainer trace({
173 { { C::memory_sel, 1 }, { C::memory_sel_rng_chk, 1 } },
174 { { C::memory_sel, 1 }, { C::memory_sel_rng_chk, 1 } },
175 { { C::memory_sel, 1 }, { C::memory_sel_rng_chk, 0 } },
176 { { C::memory_sel, 0 }, { C::memory_sel_rng_chk, 0 } },
177 });
178
179 check_relation<memory>(trace, memory::SR_SEL_RNG_CHK);
180
181 // Disable the range check for the penultimate row.
182 trace.set(C::memory_sel_rng_chk, 1, 0);
183 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_SEL_RNG_CHK), "SEL_RNG_CHK");
184
185 // Reset
186 trace.set(C::memory_sel_rng_chk, 1, 1);
187
188 // Disable the range check at the first row.
189 trace.set(C::memory_sel_rng_chk, 0, 0);
190 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_SEL_RNG_CHK), "SEL_RNG_CHK");
191
192 // Reset
193 trace.set(C::memory_sel_rng_chk, 0, 1);
194
195 // Enable the range check at the last active row.
196 trace.set(C::memory_sel_rng_chk, 2, 1);
197 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_SEL_RNG_CHK), "SEL_RNG_CHK");
198}
199
200// last_access is derived from whether the next row has the same (space_id, address).
201TEST(MemoryConstrainingTest, LastAccess)
202{
203 // global_addr = space_id * 2^32 + address. Using space_id=0 so global_addr == address.
204 TestTraceContainer trace({
205 { { C::memory_sel_rng_chk, 1 },
206 { C::memory_address, 12345 },
207 { C::memory_last_access, 1 },
208 { C::memory_glob_addr_diff_inv, 1 } },
209 { { C::memory_sel_rng_chk, 1 }, { C::memory_address, 12346 }, { C::memory_last_access, 0 } },
210 { { C::memory_sel_rng_chk, 1 }, { C::memory_address, 12346 }, { C::memory_last_access, 0 } },
211 { { C::memory_sel_rng_chk, 1 },
212 { C::memory_address, 12346 },
213 { C::memory_last_access, 1 },
214 { C::memory_glob_addr_diff_inv, 1 } },
215 { { C::memory_sel_rng_chk, 0 },
216 { C::memory_address, 12347 },
217 { C::memory_last_access, 1 },
218 { C::memory_glob_addr_diff_inv, 1 } },
219 });
220
221 check_relation<memory>(trace, memory::SR_LAST_ACCESS);
222
223 // Mutate the trace to make the last access incorrect (last_access == 0 instead of 1).
224 trace.set(C::memory_last_access, 0, 0);
225 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_LAST_ACCESS), "LAST_ACCESS");
226
227 // Reset
228 trace.set(C::memory_last_access, 0, 1);
229 check_relation<memory>(trace, memory::SR_LAST_ACCESS);
230
231 // Mutate glob_addr_diff_inv == 0.
232 trace.set(C::memory_glob_addr_diff_inv, 0, 0);
233 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_LAST_ACCESS), "LAST_ACCESS");
234
235 // Reset
236 trace.set(C::memory_glob_addr_diff_inv, 0, 1);
237 check_relation<memory>(trace, memory::SR_LAST_ACCESS);
238
239 // Mutate the trace to make the last access == 1, instead of 0.
240 trace.set(C::memory_last_access, 2, 1);
241 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_LAST_ACCESS), "LAST_ACCESS");
242}
243
244// diff is derived as GLOBAL_ADDR_DIFF when last_access == 1.
245TEST(MemoryConstrainingTest, DiffWithLastAccess)
246{
247 // We set some dummy values for clk and rw to ensure that they do not interfere with diff derivation.
248 // global_addr = space_id * 2^32 + address. Using space_id=0 so global_addr == address.
249 TestTraceContainer trace({
250 { { C::memory_sel_rng_chk, 1 },
251 { C::memory_address, 12345 },
252 { C::memory_last_access, 1 },
253 { C::memory_diff, 10000 },
254 { C::memory_clk, 38 },
255 { C::memory_rw, 1 } },
256 { { C::memory_sel_rng_chk, 1 },
257 { C::memory_address, 22345 },
258 { C::memory_last_access, 1 },
259 { C::memory_diff, 12 },
260 { C::memory_clk, 127 },
261 { C::memory_rw, 1 } },
262 { { C::memory_sel_rng_chk, 1 },
263 { C::memory_address, 22357 },
264 { C::memory_last_access, 1 },
265 { C::memory_diff, FF(-22357) },
266 { C::memory_clk, 130 },
267 { C::memory_rw, 1 } },
268 { { C::memory_sel_rng_chk, 0 }, { C::memory_last_access, 0 } },
269 });
270
271 check_relation<memory>(trace, memory::SR_DIFF);
272
273 // Mutate the trace to make the diff incorrect.
274 trace.set(C::memory_diff, 1, trace.get(C::memory_diff, 1) + 1);
275 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF), "DIFF");
276}
277
278// diff is derived as TIMESTAMP_DIFF - rw' * rw when last_access == 0.
279// TIMESTAMP_DIFF = 2*(clk' - clk) + (rw' - rw).
280TEST(MemoryConstrainingTest, DiffWithoutLastAccess)
281{
282 // Choose clk/rw such that timestamps are consistent:
283 // Row 0: clk=38, rw=1 -> ts=77. diff = (79-77) - 1*1 = 1
284 // Row 1: clk=39, rw=1 -> ts=79. diff = (8780-79) - 0*1 = 8701
285 // Row 2: clk=4390, rw=0 -> ts=8780. diff = (18780-8780) - 0*0 = 10000
286 // Row 3: clk=9390, rw=0 -> ts=18780. diff = (18781-18780) - 1*0 = 1
287 // Row 4: clk=9390, rw=1 -> ts=18781. diff = (0-18781) - 0*1 = -18781
288 TestTraceContainer trace({
289 { { C::memory_sel_rng_chk, 1 }, { C::memory_clk, 38 }, { C::memory_rw, 1 }, { C::memory_diff, 1 } },
290 { { C::memory_sel_rng_chk, 1 }, { C::memory_clk, 39 }, { C::memory_rw, 1 }, { C::memory_diff, 8701 } },
291 { { C::memory_sel_rng_chk, 1 }, { C::memory_clk, 4390 }, { C::memory_rw, 0 }, { C::memory_diff, 10000 } },
292 { { C::memory_sel_rng_chk, 1 }, { C::memory_clk, 9390 }, { C::memory_rw, 0 }, { C::memory_diff, 1 } },
293 { { C::memory_sel_rng_chk, 1 }, { C::memory_clk, 9390 }, { C::memory_rw, 1 }, { C::memory_diff, FF(-18781) } },
294 { { C::memory_sel_rng_chk, 0 }, { C::memory_last_access, 0 } },
295 });
296
297 check_relation<memory>(trace, memory::SR_DIFF);
298
299 // Mutate the trace to make the diff incorrect.
300 trace.set(C::memory_diff, 0, trace.get(C::memory_diff, 0) + 1);
301 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF), "DIFF");
302
303 // Reset
304 trace.set(C::memory_diff, 0, trace.get(C::memory_diff, 0) - 1);
305 check_relation<memory>(trace, memory::SR_DIFF);
306
307 // Mutate the trace to make the diff incorrect.
308 trace.set(C::memory_diff, 1, trace.get(C::memory_diff, 1) + 1);
309 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF), "DIFF");
310}
311
312// diff correct decomposition into 3 16-bit limbs.
313TEST(MemoryConstrainingTest, DiffDecomp)
314{
315 TestTraceContainer trace({
316 { { C::memory_diff, 87 }, { C::memory_limb_0_, 87 }, { C::memory_limb_1_, 0 }, { C::memory_limb_2_, 0 } },
317 { { C::memory_diff, 1ULL << 16 },
318 { C::memory_limb_0_, 0 },
319 { C::memory_limb_1_, 1 },
320 { C::memory_limb_2_, 0 } },
321 { { C::memory_diff, 1ULL << 32 },
322 { C::memory_limb_0_, 0 },
323 { C::memory_limb_1_, 0 },
324 { C::memory_limb_2_, 1 } },
325 { { C::memory_diff, UINT64_MAX >> 16 },
326 { C::memory_limb_0_, UINT16_MAX },
327 { C::memory_limb_1_, UINT16_MAX },
328 { C::memory_limb_2_, UINT16_MAX } },
329 });
330
331 check_relation<memory>(trace, memory::SR_DIFF_DECOMP);
332
333 // Mutate the trace to make the diff decomposition incorrect.
334 trace.set(C::memory_limb_0_, 0, trace.get(C::memory_limb_0_, 0) + 1);
335 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF_DECOMP), "DIFF_DECOMP");
336
337 // Reset
338 trace.set(C::memory_limb_0_, 0, trace.get(C::memory_limb_0_, 0) - 1);
339 check_relation<memory>(trace, memory::SR_DIFF_DECOMP);
340
341 // Mutate the trace to make the diff decomposition incorrect.
342 trace.set(C::memory_limb_1_, 1, trace.get(C::memory_limb_1_, 1) + 1);
343 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF_DECOMP), "DIFF_DECOMP");
344
345 // Reset
346 trace.set(C::memory_limb_1_, 1, trace.get(C::memory_limb_1_, 1) - 1);
347 check_relation<memory>(trace, memory::SR_DIFF_DECOMP);
348
349 // Mutate the trace to make the diff decomposition incorrect.
350 trace.set(C::memory_limb_2_, 2, trace.get(C::memory_limb_2_, 2) + 1);
351 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_DIFF_DECOMP), "DIFF_DECOMP");
352}
353
354// Correct memory value (and tag) initialization after first row.
355TEST(MemoryConstrainingTest, MemoryInitValueFirstRow)
356{
357 TestTraceContainer trace({
358 { { C::precomputed_first_row, 1 } },
359 { { C::memory_sel, 1 }, { C::memory_value, 0 }, { C::memory_tag, static_cast<uint8_t>(MemoryTag::FF) } },
360 });
361
362 check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE, memory::SR_MEMORY_INIT_TAG);
363
364 // Mutate the trace to make the memory value incorrect.
365 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) + 1);
366 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE), "MEMORY_INIT_VALUE");
367
368 // Reset
369 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) - 1);
370 check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE, memory::SR_MEMORY_INIT_TAG);
371
372 // Mutate the trace to make the memory tag incorrect.
373 trace.set(C::memory_tag, 1, static_cast<uint8_t>(MemoryTag::U16));
374 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_MEMORY_INIT_TAG), "MEMORY_INIT_TAG");
375}
376
377// Correct memory value (and tag) initialization after last_access == 1.
378TEST(MemoryConstrainingTest, MemoryInitValueLastAccess)
379{
380 TestTraceContainer trace({
381 { { C::memory_sel, 1 }, { C::memory_last_access, 1 } },
382 { { C::memory_sel, 1 }, { C::memory_value, 0 }, { C::memory_tag, static_cast<uint8_t>(MemoryTag::FF) } },
383 });
384
385 check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE, memory::SR_MEMORY_INIT_TAG);
386
387 // Mutate the trace to make the memory value incorrect.
388 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) + 1);
389 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE), "MEMORY_INIT_VALUE");
390
391 // Reset
392 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) - 1);
393 check_relation<memory>(trace, memory::SR_MEMORY_INIT_VALUE, memory::SR_MEMORY_INIT_TAG);
394
395 // Mutate the trace to make the memory tag incorrect.
396 trace.set(C::memory_tag, 1, static_cast<uint8_t>(MemoryTag::U1));
397 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_MEMORY_INIT_TAG), "MEMORY_INIT_TAG");
398}
399
400// Correct read-write consistency for memory value (and tag).
401TEST(MemoryConstrainingTest, ReadWriteConsistency)
402{
403 TestTraceContainer trace({
404 { { C::memory_sel, 1 },
405 { C::memory_rw, 1 },
406 { C::memory_value, 12 },
407 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U8) } }, // Write U8(12)
408 { { C::memory_sel, 1 },
409 { C::memory_rw, 0 },
410 { C::memory_value, 12 },
411 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U8) } }, // Read U8(12)
412 { { C::memory_sel, 1 },
413 { C::memory_rw, 1 },
414 { C::memory_value, 17 },
415 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U64) } }, // Write U64(17)
416 { { C::memory_sel, 1 },
417 { C::memory_rw, 1 },
418 { C::memory_value, 12345 },
419 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U128) } }, // Write U128(12345)
420 { { C::memory_sel, 1 },
421 { C::memory_rw, 0 },
422 { C::memory_value, 12345 },
423 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U128) } }, // Read U128(12345)
424 { { C::memory_sel, 1 },
425 { C::memory_last_access, 1 },
426 { C::memory_rw, 0 },
427 { C::memory_value, 12345 },
428 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U128) } }, // Read U128(12345)
429 });
430
432
433 // Mutate the trace to make the first read value (row 1) incorrect.
434 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) + 1);
436 "READ_WRITE_CONSISTENCY_VALUE");
437
438 // Reset
439 trace.set(C::memory_value, 1, trace.get(C::memory_value, 1) - 1);
441
442 // Mutate the trace to make the first read tag (row 1) incorrect.
443 trace.set(C::memory_tag, 1, static_cast<uint8_t>(MemoryTag::U16));
445 "READ_WRITE_CONSISTENCY_TAG");
446}
447
448// Selector on tag == FF.
449TEST(MemoryConstrainingTest, TagIsFF)
450{
451 TestTraceContainer trace({
452 { { C::memory_sel, 1 },
453 { C::memory_tag, static_cast<uint8_t>(MemoryTag::FF) },
454 { C::memory_sel_tag_is_ff, 1 } },
455 { { C::memory_sel, 1 },
456 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U1) },
457 { C::memory_sel_tag_is_ff, 0 },
458 { C::memory_tag_ff_diff_inv,
459 (FF(static_cast<uint8_t>(MemoryTag::U1)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
460 { { C::memory_sel, 1 },
461 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U8) },
462 { C::memory_sel_tag_is_ff, 0 },
463 { C::memory_tag_ff_diff_inv,
464 (FF(static_cast<uint8_t>(MemoryTag::U8)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
465 { { C::memory_sel, 1 },
466 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U16) },
467 { C::memory_sel_tag_is_ff, 0 },
468 { C::memory_tag_ff_diff_inv,
469 (FF(static_cast<uint8_t>(MemoryTag::U16)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
470 { { C::memory_sel, 1 },
471 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U32) },
472 { C::memory_sel_tag_is_ff, 0 },
473 { C::memory_tag_ff_diff_inv,
474 (FF(static_cast<uint8_t>(MemoryTag::U32)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
475 { { C::memory_sel, 1 },
476 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U64) },
477 { C::memory_sel_tag_is_ff, 0 },
478 { C::memory_tag_ff_diff_inv,
479 (FF(static_cast<uint8_t>(MemoryTag::U64)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
480 { { C::memory_sel, 1 },
481 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U128) },
482 { C::memory_sel_tag_is_ff, 0 },
483 { C::memory_tag_ff_diff_inv,
484 (FF(static_cast<uint8_t>(MemoryTag::U128)) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() } },
485 });
486
487 check_relation<memory>(trace, memory::SR_TAG_IS_FF);
488
489 // Attempt to de-activate sel_tag_is_ff when tag == FF.
490 trace.set(C::memory_sel_tag_is_ff, 0, 0);
491 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_TAG_IS_FF), "TAG_IS_FF");
492
493 // Try to change value for diff_inv
494 trace.set(C::memory_tag_ff_diff_inv, 0, 1);
495 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_TAG_IS_FF), "TAG_IS_FF");
496
497 // Reset
498 trace.set(C::memory_sel_tag_is_ff, 0, 1);
499 trace.set(C::memory_tag_ff_diff_inv, 0, 0);
500 check_relation<memory>(trace, memory::SR_TAG_IS_FF);
501
502 // Attempt to activate sel_tag_is_ff when tag != FF.
503 trace.set(C::memory_sel_tag_is_ff, 1, 1);
504 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_TAG_IS_FF), "TAG_IS_FF");
505
506 // Try to modify value for tag_ff_diff_inv
507 trace.set(C::memory_tag_ff_diff_inv, 1, 0);
508 EXPECT_THROW_WITH_MESSAGE(check_relation<memory>(trace, memory::SR_TAG_IS_FF), "TAG_IS_FF");
509}
510
511// Boolean selector sel_rng_write is active for write operations and tag != FF.
512TEST(MemoryConstrainingTest, SelRngWrite)
513{
514 TestTraceContainer trace({
515 { { C::memory_sel, 1 }, { C::memory_rw, 1 }, { C::memory_sel_tag_is_ff, 1 }, { C::memory_sel_rng_write, 0 } },
516 { { C::memory_sel, 1 }, { C::memory_rw, 1 }, { C::memory_sel_tag_is_ff, 0 }, { C::memory_sel_rng_write, 1 } },
517 { { C::memory_sel, 1 }, { C::memory_rw, 0 }, { C::memory_sel_tag_is_ff, 1 }, { C::memory_sel_rng_write, 0 } },
518 { { C::memory_sel, 1 }, { C::memory_rw, 0 }, { C::memory_sel_tag_is_ff, 0 }, { C::memory_sel_rng_write, 0 } },
519 });
520
521 check_relation<memory>(trace, memory::SR_SEL_RNG_WRITE);
522}
523
524// Negative test: attempts to write a value which is not present in the range check trace.
525TEST(MemoryConstrainingTest, NegativeWriteValueOutOfRange)
526{
527 TestTraceContainer trace({
528 { { C::memory_sel, 1 },
529 { C::memory_rw, 1 },
530 { C::memory_value, 12345 },
531 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U16) },
532 { C::memory_sel_rng_write, 1 },
533 { C::memory_max_bits, 128 },
534 { C::range_check_sel, 1 },
535 { C::range_check_value, 12345 },
536 { C::range_check_rng_chk_bits, 128 } },
537 });
538
539 check_interaction<MemoryTraceBuilder, lookup_memory_range_check_write_tagged_value_settings>(trace);
540
541 // Mutate the trace to make the value incorrect in range check.
542 trace.set(C::range_check_value, 0, trace.get(C::range_check_value, 1) + 1);
544 (check_interaction<MemoryTraceBuilder, lookup_memory_range_check_write_tagged_value_settings>(trace)),
545 "Failed.*RANGE_CHECK_WRITE_TAGGED_VALUE. Could not find tuple in destination.");
546}
547
548// Negative test: retrieve wrong max_bits value from precomputed table.
549TEST(MemoryConstrainingTest, NegativeMaxBitsOutOfRange)
550{
551 TestTraceContainer trace({
552 { { C::memory_sel, 1 },
553 { C::memory_sel_rng_write, 1 },
554 { C::memory_tag, static_cast<uint8_t>(MemoryTag::U32) },
555 { C::memory_max_bits, 32 } },
556 });
557
558 PrecomputedTraceBuilder precomputed_trace_builder;
559 precomputed_trace_builder.process_tag_parameters(trace);
560 precomputed_trace_builder.process_misc(trace, 100); // 100 is an arbitrary upper bound for the number of tags.
561
562 check_interaction<MemoryTraceBuilder, lookup_memory_tag_max_bits_settings>(trace);
563
564 // Mutate the trace to make the max_bits incorrect.
565 trace.set(C::memory_max_bits, 0, trace.get(C::memory_max_bits, 0) + 1);
566 EXPECT_THROW_WITH_MESSAGE((check_interaction<MemoryTraceBuilder, lookup_memory_tag_max_bits_settings>(trace)),
567 "Failed.*LOOKUP_MEMORY_TAG_MAX_BITS. Could not find tuple in destination.");
568}
569
570// Negative test: limbs of diff cannot be larger than 16 bits.
571TEST(MemoryConstrainingTest, NegativeDiffLimbOutOfRange)
572{
573 TestTraceContainer trace({
574 { { C::memory_sel, 1 },
575 { C::memory_sel_rng_chk, 1 },
576 { C::memory_limb_0_, UINT16_MAX },
577 { C::memory_limb_1_, UINT16_MAX },
578 { C::memory_limb_2_, UINT16_MAX } },
579 });
580
581 PrecomputedTraceBuilder precomputed_trace_builder;
582 precomputed_trace_builder.process_misc(trace, 1 << 16);
583 precomputed_trace_builder.process_sel_range_16(trace);
584
585 check_interaction<MemoryTraceBuilder,
589
590 // Mutate the trace to make the limb_0 incorrect.
591 trace.set(C::memory_limb_0_, 0, UINT16_MAX + 1);
592 EXPECT_THROW_WITH_MESSAGE((check_interaction<MemoryTraceBuilder, lookup_memory_range_check_limb_0_settings>(trace)),
593 "Failed.*RANGE_CHECK_LIMB_0. Could not find tuple in destination.");
594
595 check_interaction<MemoryTraceBuilder, lookup_memory_range_check_limb_1_settings>(trace);
596
597 // Mutate the trace to make the limb_1 incorrect.
598 trace.set(C::memory_limb_1_, 0, UINT16_MAX + 1);
599 EXPECT_THROW_WITH_MESSAGE((check_interaction<MemoryTraceBuilder, lookup_memory_range_check_limb_1_settings>(trace)),
600 "Failed.*RANGE_CHECK_LIMB_1. Could not find tuple in destination.");
601
602 check_interaction<MemoryTraceBuilder, lookup_memory_range_check_limb_2_settings>(trace);
603
604 // Mutate the trace to make the limb_2 incorrect.
605 trace.set(C::memory_limb_2_, 0, UINT16_MAX + 1);
606 EXPECT_THROW_WITH_MESSAGE((check_interaction<MemoryTraceBuilder, lookup_memory_range_check_limb_2_settings>(trace)),
607 "Failed.*RANGE_CHECK_LIMB_2. Could not find tuple in destination.");
608}
609
610} // namespace
611} // namespace bb::avm2::constraining
#define EXPECT_THROW_WITH_MESSAGE(code, expectedMessageRegex)
Definition assert.hpp:193
static TaggedValue from_tag(ValueTag tag, FF value)
static constexpr size_t SR_TAG_IS_FF
Definition memory.hpp:51
static constexpr size_t SR_READ_WRITE_CONSISTENCY_TAG
Definition memory.hpp:50
static constexpr size_t SR_DIFF
Definition memory.hpp:45
static constexpr size_t SR_LAST_ACCESS
Definition memory.hpp:44
static constexpr size_t SR_READ_WRITE_CONSISTENCY_VALUE
Definition memory.hpp:49
static constexpr size_t SR_MEMORY_INIT_TAG
Definition memory.hpp:48
static constexpr size_t SR_MEMORY_INIT_VALUE
Definition memory.hpp:47
static constexpr size_t SR_SEL_RNG_WRITE
Definition memory.hpp:52
static constexpr size_t SR_DIFF_DECOMP
Definition memory.hpp:46
static constexpr size_t SR_MEM_CONTINUITY
Definition memory.hpp:42
static constexpr size_t SR_SEL_RNG_CHK
Definition memory.hpp:43
const FF & get(Column col, uint32_t row) const
void visit_column(Column col, const std::function< void(uint32_t, const FF &)> &visitor) const
void set(Column col, uint32_t row, const FF &value)
TestTraceContainer trace
void check_interaction(tracegen::TestTraceContainer &trace)
TEST(AvmFixedVKTests, FixedVKCommitments)
Test that the fixed VK commitments agree with the ones computed from precomputed columns.
TestTraceContainer empty_trace()
Definition fixtures.cpp:153
lookup_settings< lookup_memory_range_check_limb_0_settings_ > lookup_memory_range_check_limb_0_settings
lookup_settings< lookup_memory_range_check_limb_1_settings_ > lookup_memory_range_check_limb_1_settings
AvmFlavorSettings::FF FF
Definition field.hpp:10
lookup_settings< lookup_memory_range_check_limb_2_settings_ > lookup_memory_range_check_limb_2_settings
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
MemoryStore memory
static constexpr uint256_t modulus