Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
addressing.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 tracegen::ExecutionTraceBuilder;
22using tracegen::TestTraceContainer;
24using C = Column;
25using addressing = bb::avm2::addressing<FF>;
26
27// Across all tests, bear in mind that
28// pol SEL_RESOLVE_ADDRESS = sel_bytecode_retrieval_success * sel_instruction_fetching_success;
29
30TEST(AddressingConstrainingTest, EmptyRow)
31{
32 check_relation<addressing>(testing::empty_trace());
33}
34
35/**************************************************************************************************
36 * Base Address Resolution
37 **************************************************************************************************/
38
39TEST(AddressingConstrainingTest, BaseAddressGating)
40{
41 // If there are no relative operands, it's ok that sel_do_base_check is 0.
42 TestTraceContainer trace({ {
43 // These set pol SEL_RESOLVE_ADDRESS.
44 // If this is off the whole subrelation is unconstrained.
45 { C::execution_sel_bytecode_retrieval_success, 1 },
46 { C::execution_sel_instruction_fetching_success, 1 },
47 } });
48 check_relation<addressing>(trace, addressing::SR_NUM_RELATIVE_INV_CHECK);
49
50 trace.set(0,
51 { {
52 // From spec.
53 { C::execution_sel_op_is_address_0_, 1 },
54 { C::execution_sel_op_is_address_1_, 1 },
55 { C::execution_sel_op_is_address_2_, 1 },
56 { C::execution_sel_op_is_address_3_, 1 },
57 { C::execution_sel_op_is_address_4_, 0 },
58 // Frmo indirect.
59 { C::execution_sel_op_is_relative_wire_0_, 1 },
60 { C::execution_sel_op_is_relative_wire_1_, 0 },
61 { C::execution_sel_op_is_relative_wire_2_, 1 },
62 { C::execution_sel_op_is_relative_wire_3_, 0 },
63 { C::execution_sel_op_is_relative_wire_4_, 1 }, // not an address
64 { C::execution_sel_op_is_relative_wire_5_, 0 },
65 { C::execution_sel_op_is_relative_wire_6_, 0 },
66 // should be 1
67 { C::execution_sel_do_base_check, 0 },
68 } });
71
72 // Even if we fix the inverse, sel_do_base_check should still be 1 and not 0.
73 trace.set(C::execution_num_relative_operands_inv, /*row=*/0, /*value=*/FF(2).invert());
76
77 // Now it should pass.
78 trace.set(C::execution_sel_do_base_check, /*row=*/0, /*value=*/1);
79 check_relation<addressing>(trace, addressing::SR_NUM_RELATIVE_INV_CHECK);
80}
81
82TEST(AddressingConstrainingTest, BaseAddressTagIsU32)
83{
84 FF base_address_tag = FF(static_cast<uint8_t>(MemoryTag::U32));
85 FF base_address_tag_diff_inv = 0;
86
87 TestTraceContainer trace({
88 {
89 { C::execution_base_address_tag, base_address_tag },
90 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
91 { C::execution_sel_base_address_failure, 0 },
92 // Selectors that enable the subrelation.
93 // These set pol SEL_RESOLVE_ADDRESS.
94 { C::execution_sel_bytecode_retrieval_success, 1 },
95 { C::execution_sel_instruction_fetching_success, 1 },
96 { C::execution_sel_do_base_check, 1 },
97 },
98 });
99
100 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
101
102 // Error selector cannot be cheated.
103 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/1);
104 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
106
107 // Inverse doesn't matter if the base address tag is U32.
108 trace.set(0,
109 { {
110 { C::execution_base_address_tag_diff_inv, 44 },
111 { C::execution_sel_base_address_failure, 0 },
112 } });
113 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
114}
115
116TEST(AddressingConstrainingTest, BaseAddressTagIsNotU32)
117{
118 FF base_address_tag = 1234567;
119 FF u32_tag = static_cast<uint8_t>(MemoryTag::U32);
120 FF base_address_tag_diff_inv = FF(base_address_tag - u32_tag).invert();
121
122 TestTraceContainer trace({
123 {
124 { C::execution_base_address_tag, base_address_tag },
125 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
126 { C::execution_sel_base_address_failure, 1 },
127 // Selectors that enable the subrelation.
128 // These set pol SEL_RESOLVE_ADDRESS.
129 { C::execution_sel_bytecode_retrieval_success, 1 },
130 { C::execution_sel_instruction_fetching_success, 1 },
131 { C::execution_sel_do_base_check, 1 },
132 },
133 });
134
135 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
136
137 // Error selector cannot be cheated.
138 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/0);
139 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
141
142 // Inverse cannot be cheated if the base address tag is not U32.
143 trace.set(0,
144 { {
145 { C::execution_base_address_tag_diff_inv, 0 },
146 { C::execution_sel_base_address_failure, 0 },
147 } });
148 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
150}
151
152TEST(AddressingConstrainingTest, BaseAddressTagNoCheckImpliesNoError)
153{
154 FF base_address_tag = 1234567;
155 FF u32_tag = static_cast<uint8_t>(MemoryTag::U32);
156 FF base_address_tag_diff_inv = FF(base_address_tag - u32_tag).invert();
157
158 TestTraceContainer trace({
159 {
160 { C::execution_base_address_tag, base_address_tag },
161 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
162 { C::execution_sel_base_address_failure, 0 },
163 // Selectors that enable the subrelation.
164 // These set pol SEL_RESOLVE_ADDRESS.
165 { C::execution_sel_bytecode_retrieval_success, 1 },
166 { C::execution_sel_instruction_fetching_success, 1 },
167 { C::execution_sel_do_base_check, 0 },
168 },
169 });
170
171 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
172
173 // Error selector cannot be cheated.
174 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/1);
175 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
177
178 // Check should not be done if sel_should_resolve_address is 0. Even if there are relative addresses.
179 // Therefore the above case that was failing should now pass.
180 trace.set(0,
181 { {
182 // These set pol SEL_RESOLVE_ADDRESS.
183 { C::execution_sel_bytecode_retrieval_success, 0 },
184 { C::execution_sel_instruction_fetching_success, 0 },
185 //
186 { C::execution_sel_do_base_check, 1 },
187 } });
188 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
189}
190
191/**************************************************************************************************
192 * Relative Address Resolution
193 **************************************************************************************************/
194
195TEST(AddressingConstrainingTest, RelativeAddressPropagation)
196{
197 FF base_address_val = 100;
198
199 TestTraceContainer trace({
200 {
201 { C::execution_base_address_val, base_address_val },
202 { C::execution_sel_base_address_failure, 0 },
203 // Original operands.
204 { C::execution_op_0_, 123 },
205 { C::execution_op_1_, 456 },
206 { C::execution_op_2_, /*2^32 - 1*/ 0xFFFFFFFF },
207 { C::execution_op_3_, 101112 },
208 { C::execution_op_4_, 131415 },
209 // After relative step.
210 { C::execution_op_after_relative_0_, FF(123) + base_address_val },
211 { C::execution_op_after_relative_1_, 456 },
212 { C::execution_op_after_relative_2_, FF(0xFFFFFFFF) + base_address_val },
213 { C::execution_op_after_relative_3_, 101112 },
214 { C::execution_op_after_relative_4_, FF(131415) + base_address_val },
215 // From spec.
216 { C::execution_sel_op_is_address_0_, 1 },
217 { C::execution_sel_op_is_address_1_, 1 },
218 { C::execution_sel_op_is_address_2_, 1 },
219 { C::execution_sel_op_is_address_3_, 1 },
220 { C::execution_sel_op_is_address_4_, 1 },
221 // Selectors that enable the subrelation.
222 { C::execution_sel_op_is_relative_wire_0_, 1 },
223 { C::execution_sel_op_is_relative_wire_1_, 0 },
224 { C::execution_sel_op_is_relative_wire_2_, 1 },
225 { C::execution_sel_op_is_relative_wire_3_, 0 },
226 { C::execution_sel_op_is_relative_wire_4_, 1 },
227 { C::execution_sel_op_is_relative_wire_5_, 0 },
228 { C::execution_sel_op_is_relative_wire_6_, 1 },
229 },
230 });
231
232 check_relation<addressing>(trace,
238
239 // We set wrong values.
240 trace.set(0,
241 { {
242 { C::execution_op_after_relative_0_, 7 },
243 { C::execution_op_after_relative_1_, FF(456) + base_address_val },
244 { C::execution_op_after_relative_2_, 0xFFFFFFFF },
245 { C::execution_op_after_relative_3_, 7 },
246 { C::execution_op_after_relative_4_, 7 },
247 } });
248 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_0),
250 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_1),
252 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_2),
254 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_3),
256 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_4),
258}
259
260TEST(AddressingConstrainingTest, RelativeAddressPropagationWhenBaseAddressIsInvalid)
261{
262 FF base_address_val = 0x123456789012345ULL;
263
264 TestTraceContainer trace({
265 {
266 { C::execution_base_address_val, base_address_val },
267 { C::execution_sel_base_address_failure, 1 },
268 // Original operands.
269 { C::execution_op_0_, 123 },
270 { C::execution_op_1_, 456 },
271 { C::execution_op_2_, 0xFFFFFFFF /*2^32 - 1*/ },
272 { C::execution_op_3_, 101112 },
273 { C::execution_op_4_, 131415 },
274 // After relative step. Base address was not added.
275 { C::execution_op_after_relative_0_, 123 },
276 { C::execution_op_after_relative_1_, 456 },
277 { C::execution_op_after_relative_2_, 0xFFFFFFFF },
278 { C::execution_op_after_relative_3_, 101112 },
279 { C::execution_op_after_relative_4_, 131415 },
280 // From spec.
281 { C::execution_sel_op_is_address_0_, 1 },
282 { C::execution_sel_op_is_address_1_, 1 },
283 { C::execution_sel_op_is_address_2_, 1 },
284 { C::execution_sel_op_is_address_3_, 1 },
285 { C::execution_sel_op_is_address_4_, 1 },
286 // Selectors that enable the subrelation.
287 { C::execution_sel_op_is_relative_wire_0_, 1 },
288 { C::execution_sel_op_is_relative_wire_1_, 0 },
289 { C::execution_sel_op_is_relative_wire_2_, 1 },
290 { C::execution_sel_op_is_relative_wire_3_, 0 },
291 { C::execution_sel_op_is_relative_wire_4_, 1 },
292 { C::execution_sel_op_is_relative_wire_5_, 0 },
293 { C::execution_sel_op_is_relative_wire_6_, 1 },
294 // These set pol SEL_RESOLVE_ADDRESS.
295 { C::execution_sel_bytecode_retrieval_success, 1 },
296 { C::execution_sel_instruction_fetching_success, 1 },
297 },
298 });
299
300 check_relation<addressing>(trace,
306
307 // If I try to add the base address, the relation should fail.
308 trace.set(C::execution_op_after_relative_0_, /*row=*/0, /*value=*/FF(123) + base_address_val);
309 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_0),
311}
312
313TEST(AddressingConstrainingTest, RelativeOverflowCheck)
314{
315 FF base_address_val = 100;
316
317 std::array<FF, 5> resolved_addrs = {
318 FF(123) + base_address_val, FF(456), FF(0xFFFFFFFF) + base_address_val, FF(101112),
319 FF(131415) + base_address_val,
320 };
321
322 TestTraceContainer trace({
323 {
324 // The operands which are "relative effective" are 0, 2, 4.
325 { C::execution_sel_op_is_relative_wire_0_, 1 },
326 { C::execution_sel_op_is_relative_wire_2_, 1 },
327 { C::execution_sel_op_is_relative_wire_4_, 1 },
328 { C::execution_sel_op_is_address_0_, 1 },
329 { C::execution_sel_op_is_address_2_, 1 },
330 { C::execution_sel_op_is_address_4_, 1 },
331 { C::execution_sel_op_do_overflow_check_0_, 1 },
332 { C::execution_sel_op_do_overflow_check_2_, 1 },
333 { C::execution_sel_op_do_overflow_check_4_, 1 },
334 // After relative step. Base address was added when applicable.
335 { C::execution_op_after_relative_0_, resolved_addrs[0] },
336 { C::execution_op_after_relative_1_, resolved_addrs[1] },
337 { C::execution_op_after_relative_2_, resolved_addrs[2] },
338 { C::execution_op_after_relative_3_, resolved_addrs[3] },
339 { C::execution_op_after_relative_4_, resolved_addrs[4] },
340 // Overflow bits.
341 { C::execution_sel_relative_overflow_0_, 0 },
342 { C::execution_sel_relative_overflow_1_, 0 },
343 { C::execution_sel_relative_overflow_2_, 1 },
344 { C::execution_sel_relative_overflow_3_, 0 },
345 { C::execution_sel_relative_overflow_4_, 0 },
346 // Required for the gt lookup.
347 { C::execution_highest_address, AVM_HIGHEST_MEM_ADDRESS },
348 },
349 });
350
351 // GT trace.
352 for (uint32_t i = 0; i < AVM_MAX_OPERANDS; i++) {
353 trace.set(C::gt_sel, i, 1);
354 trace.set(C::gt_input_a, i, resolved_addrs[i]);
355 trace.set(C::gt_input_b, i, AVM_HIGHEST_MEM_ADDRESS);
356 trace.set(C::gt_res, i, static_cast<uint128_t>(resolved_addrs[i]) > AVM_HIGHEST_MEM_ADDRESS ? 1 : 0);
357 }
358
359 check_relation<addressing>(trace,
365
366 check_interaction<ExecutionTraceBuilder,
372
373 // If we swap bits, a lookup or a relation should fail.
374 // If the address was not relative effective, the relation should fail. (lookup is inactive)
375 trace.set(0,
376 { {
377 { C::execution_sel_relative_overflow_0_, 1 }, // No overflow.
378 { C::execution_sel_relative_overflow_1_, 1 }, // Wasn't relative effective.
379 { C::execution_sel_relative_overflow_2_, 0 }, // Overflow.
380 { C::execution_sel_relative_overflow_3_, 1 }, // Wasn't relative effective.
381 { C::execution_sel_relative_overflow_4_, 1 }, // No overflow.
382 } });
383
385 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_0_settings>(trace)),
386 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_0.*Could not find tuple in destination.");
388 check_relation<addressing>(trace, addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1),
391 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_2_settings>(trace)),
392 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_2.*Could not find tuple in destination.");
394 check_relation<addressing>(trace, addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3),
397 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_4_settings>(trace)),
398 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_4.*Could not find tuple in destination.");
399}
400
401/**************************************************************************************************
402 * Indirect Resolution
403 **************************************************************************************************/
404
405TEST(AddressingConstrainingTest, IndirectReconstruction)
406{
407 TestTraceContainer trace({
408 {
409 { C::execution_addressing_mode, 0b11'00'01'00'01'11'01'01 },
410 { C::execution_sel_op_is_indirect_wire_0_, 1 },
411 { C::execution_sel_op_is_relative_wire_0_, 0 },
412 { C::execution_sel_op_is_indirect_wire_1_, 1 },
413 { C::execution_sel_op_is_relative_wire_1_, 0 },
414 { C::execution_sel_op_is_indirect_wire_2_, 1 },
415 { C::execution_sel_op_is_relative_wire_2_, 1 },
416 { C::execution_sel_op_is_indirect_wire_3_, 1 },
417 { C::execution_sel_op_is_relative_wire_3_, 0 },
418 { C::execution_sel_op_is_indirect_wire_4_, 0 },
419 { C::execution_sel_op_is_relative_wire_4_, 0 },
420 { C::execution_sel_op_is_indirect_wire_5_, 1 },
421 { C::execution_sel_op_is_relative_wire_5_, 0 },
422 { C::execution_sel_op_is_indirect_wire_6_, 0 },
423 { C::execution_sel_op_is_relative_wire_6_, 0 },
424 { C::execution_sel_op_is_relative_wire_7_, 1 },
425 { C::execution_sel_op_is_indirect_wire_7_, 1 },
426 // Selectors that enable the subrelation.
427 { C::execution_sel_bytecode_retrieval_success, 1 },
428 { C::execution_sel_instruction_fetching_success, 1 },
429 },
430 });
431
432 check_relation<addressing>(trace, addressing::SR_ADDRESSING_MODE_RECONSTRUCTION);
433}
434
435TEST(AddressingConstrainingTest, IndirectReconstructionZeroWhenAddressingDisabled)
436{
437 TestTraceContainer trace({
438 {
439 { C::execution_addressing_mode, 123456 },
440 // All sel_op_indirect and sel_op_is_relative are 0.
441 // Selectors that enable the subrelation.
442 // These set pol SEL_RESOLVE_ADDRESS.
443 { C::execution_sel_bytecode_retrieval_success, 0 },
444 { C::execution_sel_instruction_fetching_success, 0 },
445 },
446 });
447
448 check_relation<addressing>(trace, addressing::SR_ADDRESSING_MODE_RECONSTRUCTION);
449
450 // If we set any to non-zero, the relation should fail.
451 constexpr std::array<Column, 16> decomposition_columns = {
452 C::execution_sel_op_is_indirect_wire_0_, C::execution_sel_op_is_relative_wire_0_,
453 C::execution_sel_op_is_indirect_wire_1_, C::execution_sel_op_is_relative_wire_1_,
454 C::execution_sel_op_is_indirect_wire_2_, C::execution_sel_op_is_relative_wire_2_,
455 C::execution_sel_op_is_indirect_wire_3_, C::execution_sel_op_is_relative_wire_3_,
456 C::execution_sel_op_is_indirect_wire_4_, C::execution_sel_op_is_relative_wire_4_,
457 C::execution_sel_op_is_indirect_wire_5_, C::execution_sel_op_is_relative_wire_5_,
458 C::execution_sel_op_is_indirect_wire_6_, C::execution_sel_op_is_relative_wire_6_,
459 C::execution_sel_op_is_relative_wire_7_, C::execution_sel_op_is_indirect_wire_7_
460 };
461 for (Column sel_on : decomposition_columns) {
462 // First set everything to 0
463 for (Column c : decomposition_columns) {
464 trace.set(c, /*row=*/0, /*value=*/0);
465 }
466 // Enable one column.
467 trace.set(sel_on, /*row=*/0, /*value=*/1);
470 }
471}
472
473TEST(AddressingConstrainingTest, IndirectGating)
474{
475 TestTraceContainer trace({
476 {
477 // Selectors that enable the subrelation.
478 // These set pol SEL_RESOLVE_ADDRESS.
479 { C::execution_sel_bytecode_retrieval_success, 1 },
480 { C::execution_sel_instruction_fetching_success, 1 },
481 // From wire.
482 { C::execution_sel_op_is_indirect_wire_0_, 0 },
483 { C::execution_sel_op_is_indirect_wire_1_, 1 },
484 { C::execution_sel_op_is_indirect_wire_2_, 0 },
485 { C::execution_sel_op_is_indirect_wire_3_, 1 },
486 { C::execution_sel_op_is_indirect_wire_4_, 0 },
487 { C::execution_sel_op_is_indirect_wire_5_, 1 },
488 { C::execution_sel_op_is_indirect_wire_6_, 1 },
489 // From spec.
490 { C::execution_sel_op_is_address_0_, 1 },
491 { C::execution_sel_op_is_address_1_, 1 },
492 { C::execution_sel_op_is_address_2_, 1 },
493 { C::execution_sel_op_is_address_3_, 1 },
494 { C::execution_sel_op_is_address_4_, 1 },
495 // From relative step.
496 { C::execution_sel_relative_overflow_0_, 0 },
497 { C::execution_sel_relative_overflow_1_, 0 },
498 { C::execution_sel_relative_overflow_2_, 1 },
499 { C::execution_sel_relative_overflow_3_, 1 },
500 { C::execution_sel_relative_overflow_4_, 0 },
501 // Expected.
502 { C::execution_sel_apply_indirection_0_, 0 }, // no indirect bit
503 { C::execution_sel_apply_indirection_1_, 1 }, // indirect
504 { C::execution_sel_apply_indirection_2_, 0 }, // no indirect and relative overflowed
505 { C::execution_sel_apply_indirection_3_, 0 }, // indirect and relative overflowed
506 { C::execution_sel_apply_indirection_4_, 0 }, // no indirect and no relative overflow
507 },
508 });
509
510 check_relation<addressing>(trace,
516
517 // Expect failures if we switch bits.
518 trace.set(0,
519 { {
520 // Opposite of above.
521 { C::execution_sel_apply_indirection_0_, 1 },
522 { C::execution_sel_apply_indirection_1_, 0 },
523 { C::execution_sel_apply_indirection_2_, 1 },
524 { C::execution_sel_apply_indirection_3_, 1 },
525 { C::execution_sel_apply_indirection_4_, 1 },
526 } });
527 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0),
529 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1),
531 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2),
533 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3),
535 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4),
537
538 // Bits are still constrained if SEL_RESOLVE_ADDRESS is 0.
539 // This just simplifies the relation.
540 trace.set(C::execution_sel_bytecode_retrieval_success, /*row=*/0, /*value=*/0);
541 trace.set(C::execution_sel_instruction_fetching_success, /*row=*/0, /*value=*/0);
542 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0),
544 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1),
546 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2),
548 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3),
550 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4),
552}
553
554TEST(AddressingConstrainingTest, IndirectGatingIfBaseAddressIsInvalid)
555{
556 TestTraceContainer trace({
557 {
558 // Selectors that enable the subrelation.
559 // These set pol SEL_RESOLVE_ADDRESS.
560 { C::execution_sel_bytecode_retrieval_success, 1 },
561 { C::execution_sel_instruction_fetching_success, 1 },
562 //
563 { C::execution_sel_base_address_failure, 1 },
564 // From wire.
565 { C::execution_sel_op_is_indirect_wire_0_, 0 },
566 { C::execution_sel_op_is_indirect_wire_1_, 1 },
567 { C::execution_sel_op_is_indirect_wire_2_, 0 },
568 { C::execution_sel_op_is_indirect_wire_3_, 1 },
569 { C::execution_sel_op_is_indirect_wire_4_, 0 },
570 { C::execution_sel_op_is_indirect_wire_5_, 1 },
571 { C::execution_sel_op_is_indirect_wire_6_, 1 },
572 // From spec.
573 { C::execution_sel_op_is_address_0_, 1 },
574 { C::execution_sel_op_is_address_1_, 1 },
575 { C::execution_sel_op_is_address_2_, 1 },
576 { C::execution_sel_op_is_address_3_, 0 }, // Disable indirect check
577 { C::execution_sel_op_is_address_4_, 1 },
578 // From relative step.
579 // These selectors are mutually exclusive
580 // with base address failure. We can toggle _2 and _3
581 // because "_2" is not indirect and "_3" not an address.
582 { C::execution_sel_relative_overflow_0_, 0 },
583 { C::execution_sel_relative_overflow_1_, 0 },
584 { C::execution_sel_relative_overflow_2_, 1 },
585 { C::execution_sel_relative_overflow_3_, 1 },
586 { C::execution_sel_relative_overflow_4_, 0 },
587 // The are all expected to be 0 because the base address is invalid.
588 { C::execution_sel_apply_indirection_0_, 0 },
589 { C::execution_sel_apply_indirection_1_, 0 },
590 { C::execution_sel_apply_indirection_2_, 0 },
591 { C::execution_sel_apply_indirection_3_, 0 },
592 { C::execution_sel_apply_indirection_4_, 0 },
593 },
594 });
595
596 check_relation<addressing>(trace,
602
603 // Expect failures if we switch bits.
604 trace.set(0,
605 { {
606 // Opposite of above.
607 { C::execution_sel_apply_indirection_0_, 1 },
608 { C::execution_sel_apply_indirection_1_, 1 },
609 { C::execution_sel_apply_indirection_2_, 1 },
610 { C::execution_sel_apply_indirection_3_, 1 },
611 { C::execution_sel_apply_indirection_4_, 1 },
612 } });
613 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0),
615 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1),
617 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2),
619 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3),
621 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4),
623}
624
625TEST(AddressingConstrainingTest, IndirectPropagationWhenNoIndirection)
626{
627 // Note: The subrelations under test do NOT constrain the result of memory reads.
628 // They only constrain that non-indirect operands are propagated from the previous step.
629 TestTraceContainer trace({
630 {
631 { C::execution_sel_apply_indirection_0_, 0 },
632 { C::execution_sel_apply_indirection_1_, 1 },
633 { C::execution_sel_apply_indirection_2_, 0 },
634 { C::execution_sel_apply_indirection_3_, 1 },
635 { C::execution_sel_apply_indirection_4_, 0 },
636 // From relative step.
637 { C::execution_op_after_relative_0_, 123 },
638 { C::execution_op_after_relative_1_, 456 },
639 { C::execution_op_after_relative_2_, 789 },
640 { C::execution_op_after_relative_3_, 101112 },
641 { C::execution_op_after_relative_4_, 131415 },
642 // After memory load (or nothing).
643 { C::execution_rop_0_, 123 },
644 { C::execution_rop_1_, 99001 }, // from mem
645 { C::execution_rop_2_, 789 },
646 { C::execution_rop_3_, 99002 }, // from mem
647 { C::execution_rop_4_, 131415 },
648 // Selectors that enable the subrelation.
649 // These set pol SEL_RESOLVE_ADDRESS.
650 { C::execution_sel_bytecode_retrieval_success, 1 },
651 { C::execution_sel_instruction_fetching_success, 1 },
652 },
653 });
654
655 check_relation<addressing>(trace,
661
662 // These subrelations do not pay attention to SEL_RESOLVE_ADDRESS.
663 trace.set(C::execution_sel_bytecode_retrieval_success, /*row=*/0, /*value=*/0);
664 trace.set(C::execution_sel_instruction_fetching_success, /*row=*/0, /*value=*/0);
665 check_relation<addressing>(trace,
671
672 // Expect failures if we change values (only the non-indirect ones).
673 trace.set(0,
674 { {
675 { C::execution_rop_0_, 7 },
676 { C::execution_rop_2_, 7 },
677 { C::execution_rop_4_, 7 },
678 } });
679 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_0),
681 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_2),
683 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_4),
685}
686
687TEST(AddressingConstrainingTest, IndirectPropagationWhenIndirection)
688{
689 // TODO(fcarreiro): test memory interaction.
690}
691
692/**************************************************************************************************
693 * Final Guarantees
694 **************************************************************************************************/
695
696TEST(AddressingConstrainingTest, FinalCheckNoFailure)
697{
698 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 0, 0, 0, 1 };
699 MemoryTag rop_tag[AVM_MAX_OPERANDS] = {
701 };
702
703 auto get_tag_diff_inv = [&]() {
704 FF batched_tags_diff = 0;
705 FF power_of_2 = 1;
706 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
707 batched_tags_diff +=
708 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
709 power_of_2 *= 8; // 2^3
710 }
711 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
712 };
713
714 TestTraceContainer trace({
715 {
716 // From indirect resolution.
717 { C::execution_sel_apply_indirection_0_, should_apply_indirection[0] },
718 { C::execution_sel_apply_indirection_1_, should_apply_indirection[1] },
719 { C::execution_sel_apply_indirection_2_, should_apply_indirection[2] },
720 { C::execution_sel_apply_indirection_3_, should_apply_indirection[3] },
721 { C::execution_sel_apply_indirection_4_, should_apply_indirection[4] },
722 // From indirection.
723 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter
724 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter
725 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // shouldn't matter
726 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // shouldn't matter
727 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // NO FAILURE
728
729 // From final check.
730 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
731 { C::execution_sel_some_final_check_failed, 0 },
732 },
733 });
734
735 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
736
737 // Should fail if I try to trick the selector.
738 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/1);
739 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
741}
742
743TEST(AddressingConstrainingTest, FinalCheckSingleFailure)
744{
745 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 0, 1, 0, 1 };
746 MemoryTag rop_tag[AVM_MAX_OPERANDS] = {
748 };
749
750 auto get_tag_diff_inv = [&]() {
751 FF batched_tags_diff = 0;
752 FF power_of_2 = 1;
753 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
754 batched_tags_diff +=
755 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
756 power_of_2 *= 8; // 2^3
757 }
758 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
759 };
760
761 TestTraceContainer trace({
762 {
763 // From indirect resolution.
764 { C::execution_sel_apply_indirection_0_, should_apply_indirection[0] },
765 { C::execution_sel_apply_indirection_1_, should_apply_indirection[1] },
766 { C::execution_sel_apply_indirection_2_, should_apply_indirection[2] },
767 { C::execution_sel_apply_indirection_3_, should_apply_indirection[3] },
768 { C::execution_sel_apply_indirection_4_, should_apply_indirection[4] },
769 // From indirection.
770 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter, not address
771 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter, not indirect
772 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // NO FAIlURE
773 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // shouldn't matter, not indirect
774 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // FAILURE
775
776 // From final check.
777 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
778 { C::execution_sel_some_final_check_failed, 1 },
779 },
780 });
781
782 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
783
784 // Should fail if I try to trick the selector.
785 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/0);
786 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
788 trace.set(C::execution_batched_tags_diff_inv, /*row=*/0, /*value=*/0);
789 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
791}
792
793TEST(AddressingConstrainingTest, FinalCheckMultipleFailures)
794{
795 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 0, 1, 1, 1 };
796 MemoryTag rop_tag[AVM_MAX_OPERANDS] = {
798 };
799
800 auto get_tag_diff_inv = [&]() {
801 FF batched_tags_diff = 0;
802 FF power_of_2 = 1;
803 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
804 batched_tags_diff +=
805 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
806 power_of_2 *= 8; // 2^3
807 }
808 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
809 };
810
811 TestTraceContainer trace({
812 {
813 // From indirect resolution.
814 { C::execution_sel_apply_indirection_0_, should_apply_indirection[0] },
815 { C::execution_sel_apply_indirection_1_, should_apply_indirection[1] },
816 { C::execution_sel_apply_indirection_2_, should_apply_indirection[2] },
817 { C::execution_sel_apply_indirection_3_, should_apply_indirection[3] },
818 { C::execution_sel_apply_indirection_4_, should_apply_indirection[4] },
819 // From indirection.
820 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter, not address
821 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter, not indirect
822 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // FAIlURE
823 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // shouldn't matter, not address
824 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // FAILURE
825
826 // From final check.
827 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
828 { C::execution_sel_some_final_check_failed, 1 },
829 },
830 });
831
832 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
833
834 // Should fail if I try to trick the selector.
835 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/0);
836 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
838 trace.set(C::execution_batched_tags_diff_inv, /*row=*/0, /*value=*/0);
839 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
841}
842
843} // namespace
844} // namespace bb::avm2::constraining
#define EXPECT_THROW_WITH_MESSAGE(code, expectedMessageRegex)
Definition assert.hpp:224
static constexpr size_t SR_RELATIVE_RESOLUTION_4
static constexpr size_t SR_INDIRECT_PROPAGATION_4
static constexpr size_t SR_BATCHED_TAGS_DIFF_CHECK
static constexpr size_t SR_INDIRECT_PROPAGATION_0
static constexpr size_t SR_INDIRECT_PROPAGATION_2
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_2
static constexpr size_t SR_RELATIVE_RESOLUTION_3
static constexpr size_t SR_BASE_ADDRESS_CHECK
static constexpr size_t SR_RELATIVE_RESOLUTION_2
static constexpr size_t SR_INDIRECT_GATING_0
static constexpr size_t SR_INDIRECT_GATING_3
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3
static constexpr size_t SR_ADDRESSING_MODE_RECONSTRUCTION
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1
static std::string get_subrelation_label(size_t index)
static constexpr size_t SR_RELATIVE_RESOLUTION_0
static constexpr size_t SR_INDIRECT_GATING_2
static constexpr size_t SR_INDIRECT_PROPAGATION_1
static constexpr size_t SR_INDIRECT_PROPAGATION_3
static constexpr size_t SR_INDIRECT_GATING_4
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_4
static constexpr size_t SR_INDIRECT_GATING_1
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_0
static constexpr size_t SR_RELATIVE_RESOLUTION_1
static constexpr size_t SR_NUM_RELATIVE_INV_CHECK
void set(Column col, uint32_t row, const FF &value, bool use_atomic_limbs=false)
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:156
lookup_settings< lookup_addressing_relative_overflow_result_1_settings_ > lookup_addressing_relative_overflow_result_1_settings
lookup_settings< lookup_addressing_relative_overflow_result_2_settings_ > lookup_addressing_relative_overflow_result_2_settings
lookup_settings< lookup_addressing_relative_overflow_result_4_settings_ > lookup_addressing_relative_overflow_result_4_settings
AvmFlavorSettings::FF FF
Definition field.hpp:10
lookup_settings< lookup_addressing_relative_overflow_result_0_settings_ > lookup_addressing_relative_overflow_result_0_settings
lookup_settings< lookup_addressing_relative_overflow_result_3_settings_ > lookup_addressing_relative_overflow_result_3_settings
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
unsigned __int128 uint128_t
Definition serialize.hpp:45
constexpr field invert() const noexcept