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