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
6#include "barretenberg/vm2/common/memory_types.hpp"
7#include "barretenberg/vm2/constraining/flavor_settings.hpp"
8#include "barretenberg/vm2/constraining/testing/check_relation.hpp"
9#include "barretenberg/vm2/generated/columns.hpp"
10#include "barretenberg/vm2/generated/relations/addressing.hpp"
11#include "barretenberg/vm2/simulation/events/gt_event.hpp"
12#include "barretenberg/vm2/testing/fixtures.hpp"
13#include "barretenberg/vm2/testing/macros.hpp"
14#include "barretenberg/vm2/tracegen/execution_trace.hpp"
15#include "barretenberg/vm2/tracegen/lib/lookup_builder.hpp"
16#include "barretenberg/vm2/tracegen/test_trace_container.hpp"
17
18namespace bb::avm2::constraining {
19namespace {
20
21using tracegen::ExecutionTraceBuilder;
22using tracegen::TestTraceContainer;
23using FF = AvmFlavorSettings::FF;
24using C = Column;
25using addressing = bb::avm2::addressing<FF>;
26
27// Across all tests, bear in mind that
28// pol SEL_SHOULD_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_SHOULD_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 { C::execution_sel_op_is_address_5_, 0 },
59 { C::execution_sel_op_is_address_6_, 0 },
60 // Frmo indirect.
61 { C::execution_sel_op_is_relative_wire_0_, 1 },
62 { C::execution_sel_op_is_relative_wire_1_, 0 },
63 { C::execution_sel_op_is_relative_wire_2_, 1 },
64 { C::execution_sel_op_is_relative_wire_3_, 0 },
65 { C::execution_sel_op_is_relative_wire_4_, 1 }, // not an address
66 { C::execution_sel_op_is_relative_wire_5_, 0 },
67 { C::execution_sel_op_is_relative_wire_6_, 0 },
68 // should be 1
69 { C::execution_sel_do_base_check, 0 },
70 } });
71 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_NUM_RELATIVE_INV_CHECK),
72 "NUM_RELATIVE_INV_CHECK");
73
74 // Even if we fix the inverse, sel_do_base_check should still be 1 and not 0.
75 trace.set(C::execution_num_relative_operands_inv, /*row=*/0, /*value=*/FF(2).invert());
76 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_NUM_RELATIVE_INV_CHECK),
77 "NUM_RELATIVE_INV_CHECK");
78
79 // Now it should pass.
80 trace.set(C::execution_sel_do_base_check, /*row=*/0, /*value=*/1);
81 check_relation<addressing>(trace, addressing::SR_NUM_RELATIVE_INV_CHECK);
82}
83
84TEST(AddressingConstrainingTest, BaseAddressTagIsU32)
85{
86 FF base_address_tag = FF(static_cast<uint8_t>(MemoryTag::U32));
87 FF base_address_tag_diff_inv = 0;
88
89 TestTraceContainer trace({
90 {
91 { C::execution_base_address_tag, base_address_tag },
92 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
93 { C::execution_sel_base_address_failure, 0 },
94 // Selectors that enable the subrelation.
95 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
96 { C::execution_sel_bytecode_retrieval_success, 1 },
97 { C::execution_sel_instruction_fetching_success, 1 },
98 { C::execution_sel_do_base_check, 1 },
99 },
100 });
101
102 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
103
104 // Error selector cannot be cheated.
105 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/1);
106 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
107 "BASE_ADDRESS_CHECK");
108
109 // Inverse doesn't matter if the base address tag is U32.
110 trace.set(0,
111 { {
112 { C::execution_base_address_tag_diff_inv, 44 },
113 { C::execution_sel_base_address_failure, 0 },
114 } });
115 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
116}
117
118TEST(AddressingConstrainingTest, BaseAddressTagIsNotU32)
119{
120 FF base_address_tag = 1234567;
121 FF u32_tag = static_cast<uint8_t>(MemoryTag::U32);
122 FF base_address_tag_diff_inv = FF(base_address_tag - u32_tag).invert();
123
124 TestTraceContainer trace({
125 {
126 { C::execution_base_address_tag, base_address_tag },
127 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
128 { C::execution_sel_base_address_failure, 1 },
129 // Selectors that enable the subrelation.
130 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
131 { C::execution_sel_bytecode_retrieval_success, 1 },
132 { C::execution_sel_instruction_fetching_success, 1 },
133 { C::execution_sel_do_base_check, 1 },
134 },
135 });
136
137 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
138
139 // Error selector cannot be cheated.
140 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/0);
141 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
142 "BASE_ADDRESS_CHECK");
143
144 // Inverse cannot be cheated if the base address tag is not U32.
145 trace.set(0,
146 { {
147 { C::execution_base_address_tag_diff_inv, 0 },
148 { C::execution_sel_base_address_failure, 0 },
149 } });
150 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
151 "BASE_ADDRESS_CHECK");
152}
153
154TEST(AddressingConstrainingTest, BaseAddressTagNoCheckImpliesNoError)
155{
156 FF base_address_tag = 1234567;
157 FF u32_tag = static_cast<uint8_t>(MemoryTag::U32);
158 FF base_address_tag_diff_inv = FF(base_address_tag - u32_tag).invert();
159
160 TestTraceContainer trace({
161 {
162 { C::execution_base_address_tag, base_address_tag },
163 { C::execution_base_address_tag_diff_inv, base_address_tag_diff_inv },
164 { C::execution_sel_base_address_failure, 0 },
165 // Selectors that enable the subrelation.
166 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
167 { C::execution_sel_bytecode_retrieval_success, 1 },
168 { C::execution_sel_instruction_fetching_success, 1 },
169 { C::execution_sel_do_base_check, 0 },
170 },
171 });
172
173 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
174
175 // Error selector cannot be cheated.
176 trace.set(C::execution_sel_base_address_failure, /*row=*/0, /*value=*/1);
177 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK),
178 "BASE_ADDRESS_CHECK");
179
180 // Check should not be done if sel_should_resolve_address is 0. Even if there are relative addresses.
181 // Therefore the above case that was failing should now pass.
182 trace.set(0,
183 { {
184 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
185 { C::execution_sel_bytecode_retrieval_success, 0 },
186 { C::execution_sel_instruction_fetching_success, 0 },
187 //
188 { C::execution_sel_do_base_check, 1 },
189 } });
190 check_relation<addressing>(trace, addressing::SR_BASE_ADDRESS_CHECK);
191}
192
193/**************************************************************************************************
194 * Relative Address Resolution
195 **************************************************************************************************/
196
197TEST(AddressingConstrainingTest, RelativeAddressPropagation)
198{
199 FF base_address_val = 100;
200
201 TestTraceContainer trace({
202 {
203 { C::execution_base_address_val, base_address_val },
204 { C::execution_sel_base_address_failure, 0 },
205 // Original operands.
206 { C::execution_op_0_, 123 },
207 { C::execution_op_1_, 456 },
208 { C::execution_op_2_, /*2^32 - 1*/ 0xFFFFFFFF },
209 { C::execution_op_3_, 101112 },
210 { C::execution_op_4_, 131415 },
211 { C::execution_op_5_, 161718 },
212 { C::execution_op_6_, 192021 },
213 // After relative step.
214 { C::execution_op_after_relative_0_, FF(123) + base_address_val },
215 { C::execution_op_after_relative_1_, 456 },
216 { C::execution_op_after_relative_2_, FF(0xFFFFFFFF) + base_address_val },
217 { C::execution_op_after_relative_3_, 101112 },
218 { C::execution_op_after_relative_4_, FF(131415) + base_address_val },
219 { C::execution_op_after_relative_5_, 161718 },
220 { C::execution_op_after_relative_6_, FF(192021) + base_address_val },
221 // From spec.
222 { C::execution_sel_op_is_address_0_, 1 },
223 { C::execution_sel_op_is_address_1_, 1 },
224 { C::execution_sel_op_is_address_2_, 1 },
225 { C::execution_sel_op_is_address_3_, 1 },
226 { C::execution_sel_op_is_address_4_, 1 },
227 { C::execution_sel_op_is_address_5_, 1 },
228 { C::execution_sel_op_is_address_6_, 1 },
229 // Selectors that enable the subrelation.
230 { C::execution_sel_op_is_relative_wire_0_, 1 },
231 { C::execution_sel_op_is_relative_wire_1_, 0 },
232 { C::execution_sel_op_is_relative_wire_2_, 1 },
233 { C::execution_sel_op_is_relative_wire_3_, 0 },
234 { C::execution_sel_op_is_relative_wire_4_, 1 },
235 { C::execution_sel_op_is_relative_wire_5_, 0 },
236 { C::execution_sel_op_is_relative_wire_6_, 1 },
237 },
238 });
239
240 check_relation<addressing>(trace,
241 addressing::SR_RELATIVE_RESOLUTION_0,
242 addressing::SR_RELATIVE_RESOLUTION_1,
243 addressing::SR_RELATIVE_RESOLUTION_2,
244 addressing::SR_RELATIVE_RESOLUTION_3,
245 addressing::SR_RELATIVE_RESOLUTION_4,
246 addressing::SR_RELATIVE_RESOLUTION_5,
247 addressing::SR_RELATIVE_RESOLUTION_6);
248
249 // We set wrong values.
250 trace.set(0,
251 { {
252 { C::execution_op_after_relative_0_, 7 },
253 { C::execution_op_after_relative_1_, FF(456) + base_address_val },
254 { C::execution_op_after_relative_2_, 0xFFFFFFFF },
255 { C::execution_op_after_relative_3_, 7 },
256 { C::execution_op_after_relative_4_, 7 },
257 { C::execution_op_after_relative_5_, FF(161718) + base_address_val },
258 { C::execution_op_after_relative_6_, 192021 },
259 } });
260 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_0),
261 "RELATIVE_RESOLUTION_0");
262 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_1),
263 "RELATIVE_RESOLUTION_1");
264 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_2),
265 "RELATIVE_RESOLUTION_2");
266 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_3),
267 "RELATIVE_RESOLUTION_3");
268 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_4),
269 "RELATIVE_RESOLUTION_4");
270 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_5),
271 "RELATIVE_RESOLUTION_5");
272 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_6),
273 "RELATIVE_RESOLUTION_6");
274}
275
276TEST(AddressingConstrainingTest, RelativeAddressPropagationWhenBaseAddressIsInvalid)
277{
278 FF base_address_val = 0x123456789012345ULL;
279
280 TestTraceContainer trace({
281 {
282 { C::execution_base_address_val, base_address_val },
283 { C::execution_sel_base_address_failure, 1 },
284 // Original operands.
285 { C::execution_op_0_, 123 },
286 { C::execution_op_1_, 456 },
287 { C::execution_op_2_, 0xFFFFFFFF /*2^32 - 1*/ },
288 { C::execution_op_3_, 101112 },
289 { C::execution_op_4_, 131415 },
290 { C::execution_op_5_, 161718 },
291 { C::execution_op_6_, 192021 },
292 // After relative step. Base address was not added.
293 { C::execution_op_after_relative_0_, 123 },
294 { C::execution_op_after_relative_1_, 456 },
295 { C::execution_op_after_relative_2_, 0xFFFFFFFF },
296 { C::execution_op_after_relative_3_, 101112 },
297 { C::execution_op_after_relative_4_, 131415 },
298 { C::execution_op_after_relative_5_, 161718 },
299 { C::execution_op_after_relative_6_, 192021 },
300 // From spec.
301 { C::execution_sel_op_is_address_0_, 1 },
302 { C::execution_sel_op_is_address_1_, 1 },
303 { C::execution_sel_op_is_address_2_, 1 },
304 { C::execution_sel_op_is_address_3_, 1 },
305 { C::execution_sel_op_is_address_4_, 1 },
306 { C::execution_sel_op_is_address_5_, 1 },
307 { C::execution_sel_op_is_address_6_, 1 },
308 // Selectors that enable the subrelation.
309 { C::execution_sel_op_is_relative_wire_0_, 1 },
310 { C::execution_sel_op_is_relative_wire_1_, 0 },
311 { C::execution_sel_op_is_relative_wire_2_, 1 },
312 { C::execution_sel_op_is_relative_wire_3_, 0 },
313 { C::execution_sel_op_is_relative_wire_4_, 1 },
314 { C::execution_sel_op_is_relative_wire_5_, 0 },
315 { C::execution_sel_op_is_relative_wire_6_, 1 },
316 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
317 { C::execution_sel_bytecode_retrieval_success, 1 },
318 { C::execution_sel_instruction_fetching_success, 1 },
319 },
320 });
321
322 check_relation<addressing>(trace,
323 addressing::SR_RELATIVE_RESOLUTION_0,
324 addressing::SR_RELATIVE_RESOLUTION_1,
325 addressing::SR_RELATIVE_RESOLUTION_2,
326 addressing::SR_RELATIVE_RESOLUTION_3,
327 addressing::SR_RELATIVE_RESOLUTION_4,
328 addressing::SR_RELATIVE_RESOLUTION_5,
329 addressing::SR_RELATIVE_RESOLUTION_6);
330
331 // If I try to add the base address, the relation should fail.
332 trace.set(C::execution_op_after_relative_0_, /*row=*/0, /*value=*/FF(123) + base_address_val);
333 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_RELATIVE_RESOLUTION_0),
334 "RELATIVE_RESOLUTION_0");
335}
336
337TEST(AddressingConstrainingTest, RelativeOverflowCheck)
338{
339 FF base_address_val = 100;
340
341 std::array<FF, 7> resolved_addrs = {
342 FF(123) + base_address_val, FF(456), FF(0xFFFFFFFF) + base_address_val, FF(101112),
343 FF(131415) + base_address_val, FF(161718), FF(192021) + base_address_val,
344 };
345
346 TestTraceContainer trace({
347 {
348 // The operands which are "relative effective" are 0, 2, 4, 6.
349 { C::execution_sel_op_is_relative_wire_0_, 1 },
350 { C::execution_sel_op_is_relative_wire_2_, 1 },
351 { C::execution_sel_op_is_relative_wire_4_, 1 },
352 { C::execution_sel_op_is_relative_wire_6_, 1 },
353 { C::execution_sel_op_is_address_0_, 1 },
354 { C::execution_sel_op_is_address_2_, 1 },
355 { C::execution_sel_op_is_address_4_, 1 },
356 { C::execution_sel_op_is_address_6_, 1 },
357 { C::execution_sel_op_do_overflow_check_0_, 1 },
358 { C::execution_sel_op_do_overflow_check_2_, 1 },
359 { C::execution_sel_op_do_overflow_check_4_, 1 },
360 { C::execution_sel_op_do_overflow_check_6_, 1 },
361 // After relative step. Base address was added when applicable.
362 { C::execution_op_after_relative_0_, resolved_addrs[0] },
363 { C::execution_op_after_relative_1_, resolved_addrs[1] },
364 { C::execution_op_after_relative_2_, resolved_addrs[2] },
365 { C::execution_op_after_relative_3_, resolved_addrs[3] },
366 { C::execution_op_after_relative_4_, resolved_addrs[4] },
367 { C::execution_op_after_relative_5_, resolved_addrs[5] },
368 { C::execution_op_after_relative_6_, resolved_addrs[6] },
369 // Overflow bits.
370 { C::execution_sel_relative_overflow_0_, 0 },
371 { C::execution_sel_relative_overflow_1_, 0 },
372 { C::execution_sel_relative_overflow_2_, 1 },
373 { C::execution_sel_relative_overflow_3_, 0 },
374 { C::execution_sel_relative_overflow_4_, 0 },
375 { C::execution_sel_relative_overflow_5_, 0 },
376 { C::execution_sel_relative_overflow_6_, 0 },
377 // Required for the gt lookup.
378 { C::execution_highest_address, AVM_HIGHEST_MEM_ADDRESS },
379 },
380 });
381
382 // GT trace.
383 for (uint32_t i = 0; i < 7; i++) {
384 trace.set(C::gt_sel, i, 1);
385 trace.set(C::gt_input_a, i, resolved_addrs[i]);
386 trace.set(C::gt_input_b, i, AVM_HIGHEST_MEM_ADDRESS);
387 trace.set(C::gt_res, i, static_cast<uint128_t>(resolved_addrs[i]) > AVM_HIGHEST_MEM_ADDRESS ? 1 : 0);
388 }
389
390 check_relation<addressing>(trace,
391 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_0,
392 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1,
393 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_2,
394 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3,
395 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_4,
396 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_5,
397 addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_6);
398
399 check_interaction<ExecutionTraceBuilder,
400 lookup_addressing_relative_overflow_result_0_settings,
401 lookup_addressing_relative_overflow_result_1_settings,
402 lookup_addressing_relative_overflow_result_2_settings,
403 lookup_addressing_relative_overflow_result_3_settings,
404 lookup_addressing_relative_overflow_result_4_settings,
405 lookup_addressing_relative_overflow_result_5_settings,
406 lookup_addressing_relative_overflow_result_6_settings>(trace);
407
408 // If we swap bits, a lookup or a relation should fail.
409 // If the address was not relative effective, the relation should fail. (lookup is inactive)
410 trace.set(0,
411 { {
412 { C::execution_sel_relative_overflow_0_, 1 }, // No overflow.
413 { C::execution_sel_relative_overflow_1_, 1 }, // Wasn't relative effective.
414 { C::execution_sel_relative_overflow_2_, 0 }, // Overflow.
415 { C::execution_sel_relative_overflow_3_, 1 }, // Wasn't relative effective.
416 { C::execution_sel_relative_overflow_4_, 1 }, // No overflow.
417 { C::execution_sel_relative_overflow_5_, 1 }, // Wasn't relative effective.
418 { C::execution_sel_relative_overflow_6_, 1 }, // No overflow.
419 } });
420
421 EXPECT_THROW_WITH_MESSAGE(
422 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_0_settings>(trace)),
423 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_0.*Could not find tuple in destination.");
424 EXPECT_THROW_WITH_MESSAGE(
425 check_relation<addressing>(trace, addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1),
426 "NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1");
427 EXPECT_THROW_WITH_MESSAGE(
428 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_2_settings>(trace)),
429 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_2.*Could not find tuple in destination.");
430 EXPECT_THROW_WITH_MESSAGE(
431 check_relation<addressing>(trace, addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3),
432 "NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3");
433 EXPECT_THROW_WITH_MESSAGE(
434 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_4_settings>(trace)),
435 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_4.*Could not find tuple in destination.");
436 EXPECT_THROW_WITH_MESSAGE(
437 check_relation<addressing>(trace, addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_5),
438 "NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_5");
439 EXPECT_THROW_WITH_MESSAGE(
440 (check_interaction<ExecutionTraceBuilder, lookup_addressing_relative_overflow_result_6_settings>(trace)),
441 "Failed.*LOOKUP_ADDRESSING_RELATIVE_OVERFLOW_RESULT_6.*Could not find tuple in destination.");
442}
443
444/**************************************************************************************************
445 * Indirect Resolution
446 **************************************************************************************************/
447
448TEST(AddressingConstrainingTest, IndirectReconstruction)
449{
450 TestTraceContainer trace({
451 {
452 { C::execution_indirect, 0b11'00'01'00'01'11'01'01 },
453 { C::execution_sel_op_is_indirect_wire_0_, 1 },
454 { C::execution_sel_op_is_relative_wire_0_, 0 },
455 { C::execution_sel_op_is_indirect_wire_1_, 1 },
456 { C::execution_sel_op_is_relative_wire_1_, 0 },
457 { C::execution_sel_op_is_indirect_wire_2_, 1 },
458 { C::execution_sel_op_is_relative_wire_2_, 1 },
459 { C::execution_sel_op_is_indirect_wire_3_, 1 },
460 { C::execution_sel_op_is_relative_wire_3_, 0 },
461 { C::execution_sel_op_is_indirect_wire_4_, 0 },
462 { C::execution_sel_op_is_relative_wire_4_, 0 },
463 { C::execution_sel_op_is_indirect_wire_5_, 1 },
464 { C::execution_sel_op_is_relative_wire_5_, 0 },
465 { C::execution_sel_op_is_indirect_wire_6_, 0 },
466 { C::execution_sel_op_is_relative_wire_6_, 0 },
467 { C::execution_sel_op_is_relative_wire_7_, 1 },
468 { C::execution_sel_op_is_indirect_wire_7_, 1 },
469 // Selectors that enable the subrelation.
470 { C::execution_sel_bytecode_retrieval_success, 1 },
471 { C::execution_sel_instruction_fetching_success, 1 },
472 },
473 });
474
475 check_relation<addressing>(trace, addressing::SR_INDIRECT_RECONSTRUCTION);
476}
477
478TEST(AddressingConstrainingTest, IndirectReconstructionZeroWhenAddressingDisabled)
479{
480 TestTraceContainer trace({
481 {
482 { C::execution_indirect, 123456 },
483 // All sel_op_indirect and sel_op_is_relative are 0.
484 // Selectors that enable the subrelation.
485 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
486 { C::execution_sel_bytecode_retrieval_success, 0 },
487 { C::execution_sel_instruction_fetching_success, 0 },
488 },
489 });
490
491 check_relation<addressing>(trace, addressing::SR_INDIRECT_RECONSTRUCTION);
492
493 // If we set any to non-zero, the relation should fail.
494 constexpr std::array<Column, 16> decomposition_columns = {
495 C::execution_sel_op_is_indirect_wire_0_, C::execution_sel_op_is_relative_wire_0_,
496 C::execution_sel_op_is_indirect_wire_1_, C::execution_sel_op_is_relative_wire_1_,
497 C::execution_sel_op_is_indirect_wire_2_, C::execution_sel_op_is_relative_wire_2_,
498 C::execution_sel_op_is_indirect_wire_3_, C::execution_sel_op_is_relative_wire_3_,
499 C::execution_sel_op_is_indirect_wire_4_, C::execution_sel_op_is_relative_wire_4_,
500 C::execution_sel_op_is_indirect_wire_5_, C::execution_sel_op_is_relative_wire_5_,
501 C::execution_sel_op_is_indirect_wire_6_, C::execution_sel_op_is_relative_wire_6_,
502 C::execution_sel_op_is_relative_wire_7_, C::execution_sel_op_is_indirect_wire_7_
503 };
504 for (Column sel_on : decomposition_columns) {
505 // First set everything to 0
506 for (Column c : decomposition_columns) {
507 trace.set(c, /*row=*/0, /*value=*/0);
508 }
509 // Enable one column.
510 trace.set(sel_on, /*row=*/0, /*value=*/1);
511 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_RECONSTRUCTION),
512 "INDIRECT_RECONSTRUCTION");
513 }
514}
515
516TEST(AddressingConstrainingTest, IndirectGating)
517{
518 TestTraceContainer trace({
519 {
520 // Selectors that enable the subrelation.
521 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
522 { C::execution_sel_bytecode_retrieval_success, 1 },
523 { C::execution_sel_instruction_fetching_success, 1 },
524 // From wire.
525 { C::execution_sel_op_is_indirect_wire_0_, 0 },
526 { C::execution_sel_op_is_indirect_wire_1_, 1 },
527 { C::execution_sel_op_is_indirect_wire_2_, 0 },
528 { C::execution_sel_op_is_indirect_wire_3_, 1 },
529 { C::execution_sel_op_is_indirect_wire_4_, 0 },
530 { C::execution_sel_op_is_indirect_wire_5_, 1 },
531 { C::execution_sel_op_is_indirect_wire_6_, 1 },
532 // From spec.
533 { C::execution_sel_op_is_address_0_, 1 },
534 { C::execution_sel_op_is_address_1_, 1 },
535 { C::execution_sel_op_is_address_2_, 1 },
536 { C::execution_sel_op_is_address_3_, 1 },
537 { C::execution_sel_op_is_address_4_, 1 },
538 { C::execution_sel_op_is_address_5_, 1 },
539 { C::execution_sel_op_is_address_6_, 0 },
540 // From relative step.
541 { C::execution_sel_relative_overflow_0_, 0 },
542 { C::execution_sel_relative_overflow_1_, 0 },
543 { C::execution_sel_relative_overflow_2_, 1 },
544 { C::execution_sel_relative_overflow_3_, 1 },
545 { C::execution_sel_relative_overflow_4_, 0 },
546 { C::execution_sel_relative_overflow_5_, 0 },
547 { C::execution_sel_relative_overflow_6_, 0 },
548 // Expected.
549 { C::execution_sel_should_apply_indirection_0_, 0 }, // no indirect bit
550 { C::execution_sel_should_apply_indirection_1_, 1 }, // indirect
551 { C::execution_sel_should_apply_indirection_2_, 0 }, // no indirect and relative overflowed
552 { C::execution_sel_should_apply_indirection_3_, 0 }, // indirect and relative overflowed
553 { C::execution_sel_should_apply_indirection_4_, 0 }, // no indirect and no relative overflow
554 { C::execution_sel_should_apply_indirection_5_, 1 }, // indirect and no relative overflow
555 { C::execution_sel_should_apply_indirection_6_, 0 }, // indirect and no overflow but also not an address
556 },
557 });
558
559 check_relation<addressing>(trace,
560 addressing::SR_INDIRECT_GATING_0,
561 addressing::SR_INDIRECT_GATING_1,
562 addressing::SR_INDIRECT_GATING_2,
563 addressing::SR_INDIRECT_GATING_3,
564 addressing::SR_INDIRECT_GATING_4,
565 addressing::SR_INDIRECT_GATING_5,
566 addressing::SR_INDIRECT_GATING_6);
567
568 // Expect failures if we switch bits.
569 trace.set(0,
570 { {
571 // Opposite of above.
572 { C::execution_sel_should_apply_indirection_0_, 1 },
573 { C::execution_sel_should_apply_indirection_1_, 0 },
574 { C::execution_sel_should_apply_indirection_2_, 1 },
575 { C::execution_sel_should_apply_indirection_3_, 1 },
576 { C::execution_sel_should_apply_indirection_4_, 1 },
577 { C::execution_sel_should_apply_indirection_5_, 0 },
578 { C::execution_sel_should_apply_indirection_6_, 1 },
579 } });
580 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0), "INDIRECT_GATING_0");
581 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1), "INDIRECT_GATING_1");
582 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2), "INDIRECT_GATING_2");
583 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3), "INDIRECT_GATING_3");
584 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4), "INDIRECT_GATING_4");
585 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_5), "INDIRECT_GATING_5");
586 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_6), "INDIRECT_GATING_6");
587
588 // Bits are still constrained if SEL_SHOULD_RESOLVE_ADDRESS is 0.
589 // This just simplifies the relation.
590 trace.set(C::execution_sel_bytecode_retrieval_success, /*row=*/0, /*value=*/0);
591 trace.set(C::execution_sel_instruction_fetching_success, /*row=*/0, /*value=*/0);
592 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0), "INDIRECT_GATING_0");
593 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1), "INDIRECT_GATING_1");
594 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2), "INDIRECT_GATING_2");
595 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3), "INDIRECT_GATING_3");
596 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4), "INDIRECT_GATING_4");
597 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_5), "INDIRECT_GATING_5");
598 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_6), "INDIRECT_GATING_6");
599}
600
601TEST(AddressingConstrainingTest, IndirectGatingIfBaseAddressIsInvalid)
602{
603 TestTraceContainer trace({
604 {
605 // Selectors that enable the subrelation.
606 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
607 { C::execution_sel_bytecode_retrieval_success, 1 },
608 { C::execution_sel_instruction_fetching_success, 1 },
609 //
610 { C::execution_sel_base_address_failure, 1 },
611 // From wire.
612 { C::execution_sel_op_is_indirect_wire_0_, 0 },
613 { C::execution_sel_op_is_indirect_wire_1_, 1 },
614 { C::execution_sel_op_is_indirect_wire_2_, 0 },
615 { C::execution_sel_op_is_indirect_wire_3_, 1 },
616 { C::execution_sel_op_is_indirect_wire_4_, 0 },
617 { C::execution_sel_op_is_indirect_wire_5_, 1 },
618 { C::execution_sel_op_is_indirect_wire_6_, 1 },
619 // From spec.
620 { C::execution_sel_op_is_address_0_, 1 },
621 { C::execution_sel_op_is_address_1_, 1 },
622 { C::execution_sel_op_is_address_2_, 1 },
623 { C::execution_sel_op_is_address_3_, 1 },
624 { C::execution_sel_op_is_address_4_, 1 },
625 { C::execution_sel_op_is_address_5_, 1 },
626 { C::execution_sel_op_is_address_6_, 0 },
627 // From relative step.
628 { C::execution_sel_relative_overflow_0_, 0 },
629 { C::execution_sel_relative_overflow_1_, 0 },
630 { C::execution_sel_relative_overflow_2_, 1 },
631 { C::execution_sel_relative_overflow_3_, 1 },
632 { C::execution_sel_relative_overflow_4_, 0 },
633 { C::execution_sel_relative_overflow_5_, 0 },
634 { C::execution_sel_relative_overflow_6_, 0 },
635 // The are all expected to be 0 because the base address is invalid.
636 { C::execution_sel_should_apply_indirection_0_, 0 },
637 { C::execution_sel_should_apply_indirection_1_, 0 },
638 { C::execution_sel_should_apply_indirection_2_, 0 },
639 { C::execution_sel_should_apply_indirection_3_, 0 },
640 { C::execution_sel_should_apply_indirection_4_, 0 },
641 { C::execution_sel_should_apply_indirection_5_, 0 },
642 { C::execution_sel_should_apply_indirection_6_, 0 },
643 },
644 });
645
646 check_relation<addressing>(trace,
647 addressing::SR_INDIRECT_GATING_0,
648 addressing::SR_INDIRECT_GATING_1,
649 addressing::SR_INDIRECT_GATING_2,
650 addressing::SR_INDIRECT_GATING_3,
651 addressing::SR_INDIRECT_GATING_4,
652 addressing::SR_INDIRECT_GATING_5,
653 addressing::SR_INDIRECT_GATING_6);
654
655 // Expect failures if we switch bits.
656 trace.set(0,
657 { {
658 // Opposite of above.
659 { C::execution_sel_should_apply_indirection_0_, 1 },
660 { C::execution_sel_should_apply_indirection_1_, 1 },
661 { C::execution_sel_should_apply_indirection_2_, 1 },
662 { C::execution_sel_should_apply_indirection_3_, 1 },
663 { C::execution_sel_should_apply_indirection_4_, 1 },
664 { C::execution_sel_should_apply_indirection_5_, 1 },
665 { C::execution_sel_should_apply_indirection_6_, 1 },
666 } });
667 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_0), "INDIRECT_GATING_0");
668 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_1), "INDIRECT_GATING_1");
669 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_2), "INDIRECT_GATING_2");
670 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_3), "INDIRECT_GATING_3");
671 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_4), "INDIRECT_GATING_4");
672 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_5), "INDIRECT_GATING_5");
673 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_GATING_6), "INDIRECT_GATING_6");
674}
675
676TEST(AddressingConstrainingTest, IndirectPropagationWhenNoIndirection)
677{
678 // Note: The subrelations under test do NOT constrain the result of memory reads.
679 // They only constrain that non-indirect operands are propagated from the previous step.
680 TestTraceContainer trace({
681 {
682 { C::execution_sel_should_apply_indirection_0_, 0 },
683 { C::execution_sel_should_apply_indirection_1_, 1 },
684 { C::execution_sel_should_apply_indirection_2_, 0 },
685 { C::execution_sel_should_apply_indirection_3_, 1 },
686 { C::execution_sel_should_apply_indirection_4_, 0 },
687 { C::execution_sel_should_apply_indirection_5_, 1 },
688 { C::execution_sel_should_apply_indirection_6_, 0 },
689 // From relative step.
690 { C::execution_op_after_relative_0_, 123 },
691 { C::execution_op_after_relative_1_, 456 },
692 { C::execution_op_after_relative_2_, 789 },
693 { C::execution_op_after_relative_3_, 101112 },
694 { C::execution_op_after_relative_4_, 131415 },
695 { C::execution_op_after_relative_5_, 161718 },
696 { C::execution_op_after_relative_6_, 192021 },
697 // After memory load (or nothing).
698 { C::execution_rop_0_, 123 },
699 { C::execution_rop_1_, 99001 }, // from mem
700 { C::execution_rop_2_, 789 },
701 { C::execution_rop_3_, 99002 }, // from mem
702 { C::execution_rop_4_, 131415 },
703 { C::execution_rop_5_, 99003 }, // from mem
704 { C::execution_rop_6_, 192021 },
705 // Selectors that enable the subrelation.
706 // These set pol SEL_SHOULD_RESOLVE_ADDRESS.
707 { C::execution_sel_bytecode_retrieval_success, 1 },
708 { C::execution_sel_instruction_fetching_success, 1 },
709 },
710 });
711
712 check_relation<addressing>(trace,
713 addressing::SR_INDIRECT_PROPAGATION_0,
714 addressing::SR_INDIRECT_PROPAGATION_1,
715 addressing::SR_INDIRECT_PROPAGATION_2,
716 addressing::SR_INDIRECT_PROPAGATION_3,
717 addressing::SR_INDIRECT_PROPAGATION_4,
718 addressing::SR_INDIRECT_PROPAGATION_5,
719 addressing::SR_INDIRECT_PROPAGATION_6);
720
721 // These subrelations do not pay attention to SEL_SHOULD_RESOLVE_ADDRESS.
722 trace.set(C::execution_sel_bytecode_retrieval_success, /*row=*/0, /*value=*/0);
723 trace.set(C::execution_sel_instruction_fetching_success, /*row=*/0, /*value=*/0);
724 check_relation<addressing>(trace,
725 addressing::SR_INDIRECT_PROPAGATION_0,
726 addressing::SR_INDIRECT_PROPAGATION_1,
727 addressing::SR_INDIRECT_PROPAGATION_2,
728 addressing::SR_INDIRECT_PROPAGATION_3,
729 addressing::SR_INDIRECT_PROPAGATION_4,
730 addressing::SR_INDIRECT_PROPAGATION_5,
731 addressing::SR_INDIRECT_PROPAGATION_6);
732
733 // Expect failures if we change values (only the non-indirect ones).
734 trace.set(0,
735 { {
736 { C::execution_rop_0_, 7 },
737 { C::execution_rop_2_, 7 },
738 { C::execution_rop_4_, 7 },
739 { C::execution_rop_6_, 7 },
740 } });
741 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_0),
742 "INDIRECT_PROPAGATION_0");
743 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_2),
744 "INDIRECT_PROPAGATION_2");
745 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_4),
746 "INDIRECT_PROPAGATION_4");
747 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_INDIRECT_PROPAGATION_6),
748 "INDIRECT_PROPAGATION_6");
749}
750
751TEST(AddressingConstrainingTest, IndirectPropagationWhenIndirection)
752{
753 // TODO(fcarreiro): test memory interaction.
754}
755
756/**************************************************************************************************
757 * Final Guarantees
758 **************************************************************************************************/
759
760TEST(AddressingConstrainingTest, FinalCheckNoFailure)
761{
762 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 0, 0, 1, 0, 1, 1 };
763 MemoryTag rop_tag[AVM_MAX_OPERANDS] = { MemoryTag::FF, MemoryTag::U8, MemoryTag::U16, MemoryTag::U32,
764 MemoryTag::U1, MemoryTag::U32, MemoryTag::U32 };
765
766 auto get_tag_diff_inv = [&]() {
767 FF batched_tags_diff = 0;
768 FF power_of_2 = 1;
769 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
770 batched_tags_diff +=
771 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
772 power_of_2 *= 8; // 2^3
773 }
774 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
775 };
776
777 TestTraceContainer trace({
778 {
779 // From indirect resolution.
780 { C::execution_sel_should_apply_indirection_0_, should_apply_indirection[0] },
781 { C::execution_sel_should_apply_indirection_1_, should_apply_indirection[1] },
782 { C::execution_sel_should_apply_indirection_2_, should_apply_indirection[2] },
783 { C::execution_sel_should_apply_indirection_3_, should_apply_indirection[3] },
784 { C::execution_sel_should_apply_indirection_4_, should_apply_indirection[4] },
785 { C::execution_sel_should_apply_indirection_5_, should_apply_indirection[5] },
786 { C::execution_sel_should_apply_indirection_6_, should_apply_indirection[6] },
787 // From indirection.
788 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter
789 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter
790 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // shouldn't matter
791 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // NO FAIlURE
792 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // shouldn't matter
793 { C::execution_rop_tag_5_, static_cast<uint8_t>(rop_tag[5]) }, // NO FAILURE
794 { C::execution_rop_tag_6_, static_cast<uint8_t>(rop_tag[6]) }, // NO FAILURE
795
796 // From final check.
797 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
798 { C::execution_sel_some_final_check_failed, 0 },
799 },
800 });
801
802 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
803
804 // Should fail if I try to trick the selector.
805 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/1);
806 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
807 "BATCHED_TAGS_DIFF_CHECK");
808}
809
810TEST(AddressingConstrainingTest, FinalCheckSingleFailure)
811{
812 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 1, 0, 1, 0, 1, 1 };
813 MemoryTag rop_tag[AVM_MAX_OPERANDS] = { MemoryTag::FF, MemoryTag::U8, MemoryTag::U16, MemoryTag::U32,
814 MemoryTag::U1, MemoryTag::U32, MemoryTag::U1 };
815
816 auto get_tag_diff_inv = [&]() {
817 FF batched_tags_diff = 0;
818 FF power_of_2 = 1;
819 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
820 batched_tags_diff +=
821 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
822 power_of_2 *= 8; // 2^3
823 }
824 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
825 };
826
827 TestTraceContainer trace({
828 {
829 // From indirect resolution.
830 { C::execution_sel_should_apply_indirection_0_, should_apply_indirection[0] },
831 { C::execution_sel_should_apply_indirection_1_, should_apply_indirection[1] },
832 { C::execution_sel_should_apply_indirection_2_, should_apply_indirection[2] },
833 { C::execution_sel_should_apply_indirection_3_, should_apply_indirection[3] },
834 { C::execution_sel_should_apply_indirection_4_, should_apply_indirection[4] },
835 { C::execution_sel_should_apply_indirection_5_, should_apply_indirection[5] },
836 { C::execution_sel_should_apply_indirection_6_, should_apply_indirection[6] },
837 // From indirection.
838 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter, not address
839 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter, not address
840 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // shouldn't matter, not indirect
841 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // NO FAIlURE
842 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // shouldn't matter, not indirect
843 { C::execution_rop_tag_5_, static_cast<uint8_t>(rop_tag[5]) }, // shouldn't matter, not address
844 { C::execution_rop_tag_6_, static_cast<uint8_t>(rop_tag[6]) }, // FAILURE
845
846 // From final check.
847 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
848 { C::execution_sel_some_final_check_failed, 1 },
849 },
850 });
851
852 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
853
854 // Should fail if I try to trick the selector.
855 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/0);
856 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
857 "BATCHED_TAGS_DIFF_CHECK");
858 trace.set(C::execution_batched_tags_diff_inv, /*row=*/0, /*value=*/0);
859 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
860 "BATCHED_TAGS_DIFF_CHECK");
861}
862
863TEST(AddressingConstrainingTest, FinalCheckMultipleFailures)
864{
865 FF should_apply_indirection[AVM_MAX_OPERANDS] = { 0, 1, 0, 1, 0, 1, 1 };
866 MemoryTag rop_tag[AVM_MAX_OPERANDS] = { MemoryTag::FF, MemoryTag::U8, MemoryTag::U16, MemoryTag::U8,
867 MemoryTag::U1, MemoryTag::U32, MemoryTag::U1 };
868
869 auto get_tag_diff_inv = [&]() {
870 FF batched_tags_diff = 0;
871 FF power_of_2 = 1;
872 for (size_t i = 0; i < AVM_MAX_OPERANDS; ++i) {
873 batched_tags_diff +=
874 should_apply_indirection[i] * power_of_2 * (FF(static_cast<uint8_t>(rop_tag[i])) - FF(MEM_TAG_U32));
875 power_of_2 *= 8; // 2^3
876 }
877 return batched_tags_diff != 0 ? batched_tags_diff.invert() : 0;
878 };
879
880 TestTraceContainer trace({
881 {
882 // From indirect resolution.
883 { C::execution_sel_should_apply_indirection_0_, should_apply_indirection[0] },
884 { C::execution_sel_should_apply_indirection_1_, should_apply_indirection[1] },
885 { C::execution_sel_should_apply_indirection_2_, should_apply_indirection[2] },
886 { C::execution_sel_should_apply_indirection_3_, should_apply_indirection[3] },
887 { C::execution_sel_should_apply_indirection_4_, should_apply_indirection[4] },
888 { C::execution_sel_should_apply_indirection_5_, should_apply_indirection[5] },
889 { C::execution_sel_should_apply_indirection_6_, should_apply_indirection[6] },
890 // From indirection.
891 { C::execution_rop_tag_0_, static_cast<uint8_t>(rop_tag[0]) }, // shouldn't matter, not address
892 { C::execution_rop_tag_1_, static_cast<uint8_t>(rop_tag[1]) }, // shouldn't matter, not address
893 { C::execution_rop_tag_2_, static_cast<uint8_t>(rop_tag[2]) }, // shouldn't matter, not indirect
894 { C::execution_rop_tag_3_, static_cast<uint8_t>(rop_tag[3]) }, // FAIlURE
895 { C::execution_rop_tag_4_, static_cast<uint8_t>(rop_tag[4]) }, // shouldn't matter, not indirect
896 { C::execution_rop_tag_5_, static_cast<uint8_t>(rop_tag[5]) }, // shouldn't matter, not address
897 { C::execution_rop_tag_6_, static_cast<uint8_t>(rop_tag[6]) }, // FAILURE
898
899 // From final check.
900 { C::execution_batched_tags_diff_inv, get_tag_diff_inv() },
901 { C::execution_sel_some_final_check_failed, 1 },
902 },
903 });
904
905 check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK);
906
907 // Should fail if I try to trick the selector.
908 trace.set(C::execution_sel_some_final_check_failed, /*row=*/0, /*value=*/0);
909 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
910 "BATCHED_TAGS_DIFF_CHECK");
911 trace.set(C::execution_batched_tags_diff_inv, /*row=*/0, /*value=*/0);
912 EXPECT_THROW_WITH_MESSAGE(check_relation<addressing>(trace, addressing::SR_BATCHED_TAGS_DIFF_CHECK),
913 "BATCHED_TAGS_DIFF_CHECK");
914}
915
916} // namespace
917} // namespace bb::avm2::constraining
MEM_TAG_U32
#define MEM_TAG_U32
Definition aztec_constants.hpp:41
AVM_MAX_OPERANDS
#define AVM_MAX_OPERANDS
Definition aztec_constants.hpp:177
AVM_HIGHEST_MEM_ADDRESS
#define AVM_HIGHEST_MEM_ADDRESS
Definition aztec_constants.hpp:44
check_relation.hpp
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_4
static constexpr size_t SR_RELATIVE_RESOLUTION_4
Definition addressing.hpp:57
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_6
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_6
Definition addressing.hpp:52
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_4
static constexpr size_t SR_INDIRECT_PROPAGATION_4
Definition addressing.hpp:71
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_5
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_5
Definition addressing.hpp:51
bb::avm2::addressing::SR_INDIRECT_RECONSTRUCTION
static constexpr size_t SR_INDIRECT_RECONSTRUCTION
Definition addressing.hpp:43
bb::avm2::addressing::SR_BATCHED_TAGS_DIFF_CHECK
static constexpr size_t SR_BATCHED_TAGS_DIFF_CHECK
Definition addressing.hpp:74
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_0
static constexpr size_t SR_INDIRECT_PROPAGATION_0
Definition addressing.hpp:67
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_2
static constexpr size_t SR_INDIRECT_PROPAGATION_2
Definition addressing.hpp:69
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_5
static constexpr size_t SR_RELATIVE_RESOLUTION_5
Definition addressing.hpp:58
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_2
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_2
Definition addressing.hpp:48
bb::avm2::addressing::SR_INDIRECT_GATING_5
static constexpr size_t SR_INDIRECT_GATING_5
Definition addressing.hpp:65
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_3
static constexpr size_t SR_RELATIVE_RESOLUTION_3
Definition addressing.hpp:56
bb::avm2::addressing::SR_BASE_ADDRESS_CHECK
static constexpr size_t SR_BASE_ADDRESS_CHECK
Definition addressing.hpp:45
bb::avm2::addressing::SR_INDIRECT_GATING_6
static constexpr size_t SR_INDIRECT_GATING_6
Definition addressing.hpp:66
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_2
static constexpr size_t SR_RELATIVE_RESOLUTION_2
Definition addressing.hpp:55
bb::avm2::addressing::SR_INDIRECT_GATING_0
static constexpr size_t SR_INDIRECT_GATING_0
Definition addressing.hpp:60
bb::avm2::addressing::SR_INDIRECT_GATING_3
static constexpr size_t SR_INDIRECT_GATING_3
Definition addressing.hpp:63
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_6
static constexpr size_t SR_INDIRECT_PROPAGATION_6
Definition addressing.hpp:73
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_3
Definition addressing.hpp:49
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_1
Definition addressing.hpp:47
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_0
static constexpr size_t SR_RELATIVE_RESOLUTION_0
Definition addressing.hpp:53
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_6
static constexpr size_t SR_RELATIVE_RESOLUTION_6
Definition addressing.hpp:59
bb::avm2::addressing::SR_INDIRECT_GATING_2
static constexpr size_t SR_INDIRECT_GATING_2
Definition addressing.hpp:62
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_5
static constexpr size_t SR_INDIRECT_PROPAGATION_5
Definition addressing.hpp:72
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_1
static constexpr size_t SR_INDIRECT_PROPAGATION_1
Definition addressing.hpp:68
bb::avm2::addressing::SR_INDIRECT_PROPAGATION_3
static constexpr size_t SR_INDIRECT_PROPAGATION_3
Definition addressing.hpp:70
bb::avm2::addressing::SR_INDIRECT_GATING_4
static constexpr size_t SR_INDIRECT_GATING_4
Definition addressing.hpp:64
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_4
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_4
Definition addressing.hpp:50
bb::avm2::addressing::SR_INDIRECT_GATING_1
static constexpr size_t SR_INDIRECT_GATING_1
Definition addressing.hpp:61
bb::avm2::addressing::SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_0
static constexpr size_t SR_NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_0
Definition addressing.hpp:46
bb::avm2::addressing::SR_RELATIVE_RESOLUTION_1
static constexpr size_t SR_RELATIVE_RESOLUTION_1
Definition addressing.hpp:54
bb::avm2::addressing::SR_NUM_RELATIVE_INV_CHECK
static constexpr size_t SR_NUM_RELATIVE_INV_CHECK
Definition addressing.hpp:44
bb::avm2::tracegen::TraceContainer::set
void set(Column col, uint32_t row, const FF &value)
Definition trace_container.cpp:39
trace
TestTraceContainer trace
Definition data_copy.test.cpp:62
execution_trace.hpp
flavor_settings.hpp
gt_event.hpp
lookup_builder.hpp
EXPECT_THROW_WITH_MESSAGE
#define EXPECT_THROW_WITH_MESSAGE(code, expectedMessage)
Definition macros.hpp:7
memory_types.hpp
bb::avm2::constraining::check_interaction
void check_interaction(tracegen::TestTraceContainer &trace)
Definition check_relation.hpp:76
bb::avm2::constraining::TEST
TEST(TxExecutionConstrainingTest, WriteTreeValue)
Definition tx.test.cpp:402
bb::avm2::testing::empty_trace
TestTraceContainer empty_trace()
Definition fixtures.cpp:153
bb::avm2::lookup_addressing_relative_overflow_result_1_settings
lookup_settings< lookup_addressing_relative_overflow_result_1_settings_ > lookup_addressing_relative_overflow_result_1_settings
Definition lookups_addressing.hpp:61
bb::avm2::lookup_addressing_relative_overflow_result_2_settings
lookup_settings< lookup_addressing_relative_overflow_result_2_settings_ > lookup_addressing_relative_overflow_result_2_settings
Definition lookups_addressing.hpp:87
bb::avm2::lookup_addressing_relative_overflow_result_4_settings
lookup_settings< lookup_addressing_relative_overflow_result_4_settings_ > lookup_addressing_relative_overflow_result_4_settings
Definition lookups_addressing.hpp:139
bb::avm2::lookup_addressing_relative_overflow_result_5_settings
lookup_settings< lookup_addressing_relative_overflow_result_5_settings_ > lookup_addressing_relative_overflow_result_5_settings
Definition lookups_addressing.hpp:165
bb::avm2::lookup_addressing_relative_overflow_result_0_settings
lookup_settings< lookup_addressing_relative_overflow_result_0_settings_ > lookup_addressing_relative_overflow_result_0_settings
Definition lookups_addressing.hpp:35
bb::avm2::lookup_addressing_relative_overflow_result_6_settings
lookup_settings< lookup_addressing_relative_overflow_result_6_settings_ > lookup_addressing_relative_overflow_result_6_settings
Definition lookups_addressing.hpp:191
bb::avm2::lookup_addressing_relative_overflow_result_3_settings
lookup_settings< lookup_addressing_relative_overflow_result_3_settings_ > lookup_addressing_relative_overflow_result_3_settings
Definition lookups_addressing.hpp:113
bb::avm2::MemoryTag
ValueTag MemoryTag
Definition memory_types.hpp:9
bb::avm2::FF
AvmFlavorSettings::FF FF
Definition field.hpp:10
bb::FF
typename Flavor::FF FF
Definition protogalaxy.bench.cpp:15
std::get
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
uint128_t
unsigned __int128 uint128_t
Definition serialize.hpp:44
test_trace_container.hpp