Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
alu.test.cpp
Go to the documentation of this file.
1#include <gmock/gmock.h>
2#include <gtest/gtest.h>
3
4#include <cstdint>
5#include <utility>
6#include <vector>
7
33
34namespace bb::avm2::constraining {
35namespace {
36
37using tracegen::TestTraceContainer;
39using C = Column;
40using alu = bb::avm2::alu<FF>;
41using simulation::RangeCheckEvent;
42using tracegen::AluTraceBuilder;
43using tracegen::ExecutionTraceBuilder;
44using tracegen::FieldGreaterThanTraceBuilder;
45using tracegen::GreaterThanTraceBuilder;
46using tracegen::PrecomputedTraceBuilder;
47using tracegen::RangeCheckTraceBuilder;
48
49constexpr uint8_t NUM_OF_TAGS = static_cast<uint8_t>(MemoryTag::MAX) + 1;
50
51// Generic structure for three-operand opcodes
52using ThreeOperandTestParams = std::tuple<MemoryValue, MemoryValue, MemoryValue>;
53
54// Generic structure for two-operand opcodes
55using TwoOperandTestParams = std::tuple<MemoryValue, MemoryValue>;
56
58 {
61 },
62 {
65 },
66 {
69 },
70 {
73 },
74 {
77 },
78 {
81 },
82 {
85 },
86};
87
88const std::unordered_map<MemoryTag, MemoryTag> TAG_ERROR_TEST_VALUES = {
92};
93
95{
97 uint32_t i = 0;
98 for (const auto c : out) {
99 ThreeOperandTestParams params = tuple_cat(TEST_VALUES_IN.at(i), std::make_tuple(c));
100 res.push_back(params);
101 i++;
102 }
103 return res;
104}
105
107{
109 uint32_t i = 0;
110 for (const auto c : out) {
111 TwoOperandTestParams params = std::make_tuple(std::get<0>(TEST_VALUES_IN.at(i)), c);
112 res.push_back(params);
113 i++;
114 }
115 return res;
116}
117
118class AluConstrainingTest : public ::testing::Test {
119 public:
120 PrecomputedTraceBuilder precomputed_builder;
121 RangeCheckTraceBuilder range_check_builder;
122 FieldGreaterThanTraceBuilder field_gt_builder;
123 GreaterThanTraceBuilder gt_builder;
124 AluTraceBuilder builder;
125};
126
127TEST_F(AluConstrainingTest, EmptyRow)
128{
129 check_relation<alu>(testing::empty_trace());
130}
131
132TEST_F(AluConstrainingTest, NegativeAluWrongOpId)
133{
134 auto trace = TestTraceContainer({
135 {
136 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_ADD + 1 },
137 { C::alu_sel_op_add, 1 },
138 },
139 });
140
141 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace, alu::SR_DISPATCH_OPERATION),
143}
144
145// Two operation selectors active on the same row must violate the mutual exclusion of the operations.
146TEST_F(AluConstrainingTest, NegativeAluTwoOperationsActive)
147{
148 auto trace = TestTraceContainer({
149 {
150 { C::alu_sel, 1 },
151 { C::alu_sel_op_div, 1 },
152 { C::alu_sel_op_not, 1 },
153 },
154 });
155
158}
159
160// On an inactive row (sel == 0), no operation selector may be toggled.
161TEST_F(AluConstrainingTest, NegativeAluOperationActiveOnInactiveRow)
162{
163 auto trace = TestTraceContainer({
164 {
165 { C::alu_sel, 0 },
166 { C::alu_sel_op_add, 1 },
167 },
168 });
169
172}
173
174// ADD TESTS
175
176const std::vector<MemoryValue> TEST_VALUES_ADD_OUT = {
184};
185
186const std::vector<ThreeOperandTestParams> TEST_VALUES_ADD = zip_helper(TEST_VALUES_ADD_OUT);
187
188class AluAddConstrainingTest : public AluConstrainingTest,
189 public ::testing::WithParamInterface<ThreeOperandTestParams> {
190 public:
191 TestTraceContainer process_basic_add_trace(ThreeOperandTestParams params)
192 {
193 auto [a, b, c] = params;
194 auto tag = static_cast<uint8_t>(a.get_tag());
195 auto trace = TestTraceContainer({
196 {
197 { C::alu_ia, a },
198 { C::alu_ia_tag, tag },
199 { C::alu_ib, b },
200 { C::alu_ib_tag, tag },
201 { C::alu_ic, c },
202 { C::alu_ic_tag, tag },
203 { C::alu_max_bits, get_tag_bits(a.get_tag()) },
204 { C::alu_max_value, get_tag_max_value(a.get_tag()) },
205 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_ADD },
206 { C::alu_sel, 1 },
207 { C::alu_sel_op_add, 1 },
208 { C::alu_sel_is_ff, tag == 0 ? 1 : 0 },
209 { C::alu_tag_ff_diff_inv, tag == 0 ? 0 : FF(tag).invert() },
210 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
211 { C::alu_tag_u128_diff_inv,
212 tag == static_cast<uint8_t>(MemoryTag::U128)
213 ? 0
214 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
215 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
216 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
217 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
218 { C::execution_register_0_, a }, // = ia
219 { C::execution_register_1_, b }, // = ib
220 { C::execution_register_2_, c }, // = ic
221 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
222 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_ADD }, // = alu_op_id
223 },
224 });
225
226 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
227 precomputed_builder.process_tag_parameters(trace);
228 return trace;
229 }
230
231 TestTraceContainer process_basic_add_with_tracegen(ThreeOperandTestParams params, bool error = false)
232 {
233 TestTraceContainer trace;
234 auto [a, b, c] = params;
235
236 builder.process(
237 {
238 { .operation = simulation::AluOperation::ADD, .a = a, .b = b, .c = c, .error = error },
239 },
240 trace);
241
242 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
243 precomputed_builder.process_tag_parameters(trace);
244 return trace;
245 }
246
247 TestTraceContainer process_carry_add_trace(ThreeOperandTestParams params)
248 {
249 auto [a, b, c] = params;
250 auto mem_tag = a.get_tag();
251 b = MemoryValue::from_tag(mem_tag, get_tag_max_value(mem_tag));
252 c = a - MemoryValue::from_tag(mem_tag, 1);
253 auto tag = static_cast<uint8_t>(mem_tag);
254 auto trace = TestTraceContainer({
255 {
256 { C::alu_cf, 1 },
257 { C::alu_ia, a },
258 { C::alu_ia_tag, tag },
259 { C::alu_ib, b },
260 { C::alu_ib_tag, tag },
261 { C::alu_ic, c },
262 { C::alu_ic_tag, tag },
263 { C::alu_max_bits, get_tag_bits(mem_tag) },
264 { C::alu_max_value, get_tag_max_value(mem_tag) },
265 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_ADD },
266 { C::alu_sel, 1 },
267 { C::alu_sel_op_add, 1 },
268 { C::alu_sel_is_ff, tag == 0 ? 1 : 0 },
269 { C::alu_tag_ff_diff_inv, tag == 0 ? 0 : FF(tag).invert() },
270 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
271 { C::alu_tag_u128_diff_inv,
272 tag == static_cast<uint8_t>(MemoryTag::U128)
273 ? 0
274 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
275 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
276 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
277 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
278 { C::execution_register_0_, a }, // = ia
279 { C::execution_register_1_, b }, // = ib
280 { C::execution_register_2_, c }, // = ic
281 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
282 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_ADD }, // = alu_op_id
283 },
284 });
285
286 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
287 precomputed_builder.process_tag_parameters(trace);
288 return trace;
289 }
290
291 TestTraceContainer process_carry_add_with_tracegen(ThreeOperandTestParams params)
292 {
293 TestTraceContainer trace;
294 auto [a, b, c] = params;
295 auto mem_tag = a.get_tag();
296 b = MemoryValue::from_tag(mem_tag, get_tag_max_value(mem_tag));
297 c = a - MemoryValue::from_tag(mem_tag, 1);
298
299 builder.process(
300 {
301 { .operation = simulation::AluOperation::ADD, .a = a, .b = b, .c = c },
302 },
303 trace);
304
305 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
306 precomputed_builder.process_tag_parameters(trace);
307 return trace;
308 }
309};
310
311INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluAddConstrainingTest, ::testing::ValuesIn(TEST_VALUES_ADD));
312
313TEST_P(AluAddConstrainingTest, AluBasicAdd)
314{
315 auto trace = process_basic_add_trace(GetParam());
316 check_all_interactions<AluTraceBuilder>(trace);
317 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
318 check_relation<alu>(trace);
319}
320
321TEST_P(AluAddConstrainingTest, AluBasicAddTraceGen)
322{
323 auto trace = process_basic_add_with_tracegen(GetParam());
324 check_all_interactions<AluTraceBuilder>(trace);
325 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
326 check_relation<alu>(trace);
327}
328
329TEST_P(AluAddConstrainingTest, AluCarryAdd)
330{
331 auto trace = process_carry_add_trace(GetParam());
332 check_all_interactions<AluTraceBuilder>(trace);
333 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
334 check_relation<alu>(trace);
335}
336
337TEST_P(AluAddConstrainingTest, AluCarryAddTraceGen)
338{
339 auto trace = process_carry_add_with_tracegen(GetParam());
340 check_all_interactions<AluTraceBuilder>(trace);
341 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
342 check_relation<alu>(trace);
343}
344
345TEST_P(AluAddConstrainingTest, NegativeBasicAdd)
346{
347 auto trace = process_basic_add_trace(GetParam());
348 check_relation<alu>(trace);
349 trace.set(Column::alu_ic, 0, trace.get(Column::alu_ic, 0) + 1);
351}
352
353TEST_P(AluAddConstrainingTest, NegativeAluCarryAdd)
354{
355 auto params = GetParam();
356 auto trace = process_carry_add_trace(params);
357 auto correct_max_value = trace.get(Column::alu_max_value, 0);
358 auto is_ff = std::get<0>(params).get_tag() == MemoryTag::FF;
359 check_all_interactions<AluTraceBuilder>(trace);
360 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
361 check_relation<alu>(trace);
362 // We get the correct overflowed result 'for free' with FF whether cf is on or not
363 if (!is_ff) {
364 trace.set(Column::alu_cf, 0, 0);
365 // If we are overflowing, we need to set the carry flag...
367
368 trace.set(Column::alu_cf, 0, 1);
369 trace.set(Column::alu_max_value, 0, 0);
370 // ...and the correct max_value:
372 EXPECT_THROW_WITH_MESSAGE(check_all_interactions<AluTraceBuilder>(trace), "LOOKUP_ALU_TAG_MAX_BITS_VALUE");
373 trace.set(Column::alu_max_value, 0, correct_max_value);
374 }
375
376 // TODO(MW): The below should fail the range check on c in memory, but we cannot test this yet.
377 // Instead, we assume the carry flag is correct and show an overflow fails:
378 trace.set(Column::alu_ic, 0, correct_max_value + 2);
380}
381
382TEST_P(AluAddConstrainingTest, NegativeAddWrongTagABMismatch)
383{
384 auto params = GetParam();
385 auto tag = static_cast<uint8_t>(std::get<0>(params).get_tag());
386 auto trace = process_basic_add_trace(params);
387 trace.set(Column::alu_ib_tag, 0, tag - 1);
388 // ab_tags_diff_inv = inv(a_tag - b_tag) = inv(1) = 1:
389 trace.set(Column::alu_ab_tags_diff_inv, 0, 1);
390 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 1);
391 // If we set the mismatch error, we need to make sure the ALU tag error selector is correct:
393 trace.set(Column::alu_sel_tag_err, 0, 1);
394 // If we set one error, we need to make sure the overall ALU error selector is correct:
396 trace.set(Column::alu_sel_err, 0, 1);
397 // Though the tags don't match, with error handling we can return the error rather than fail:
398 check_relation<alu>(trace);
399 // Correctly using the error, but injecting the wrong inverse will fail:
400 trace.set(Column::alu_ab_tags_diff_inv, 0, 0);
402 trace.set(Column::alu_ab_tags_diff_inv, 0, 1);
403 // Correcting the inverse, but removing the error will fail:
404 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 0);
405 trace.set(Column::alu_sel_tag_err, 0, 0);
406 trace.set(Column::alu_sel_err, 0, 0);
408}
409
410TEST_P(AluAddConstrainingTest, NegativeAddTraceGenWrongTagABMismatch)
411{
412 auto [a, b, c] = GetParam();
413 auto trace = process_basic_add_with_tracegen(
414 { a, MemoryValue::from_tag(TAG_ERROR_TEST_VALUES.at(b.get_tag()), b.as_ff()), c }, true);
415 check_all_interactions<AluTraceBuilder>(trace);
416 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
417 check_relation<alu>(trace);
418}
419
420TEST_P(AluAddConstrainingTest, NegativeAddWrongTagCMismatch)
421{
422 auto params = GetParam();
423 auto tag = static_cast<uint8_t>(std::get<0>(params).get_tag());
424 auto trace = process_basic_add_trace(params);
425 check_relation<alu>(trace);
426 trace.set(Column::alu_ic_tag, 0, tag - 1);
428}
429
430// SUB TESTS
431
432const std::vector<MemoryValue> TEST_VALUES_SUB_OUT = {
440};
441
442const std::vector<ThreeOperandTestParams> TEST_VALUES_SUB = zip_helper(TEST_VALUES_SUB_OUT);
443
444class AluSubConstrainingTest : public AluConstrainingTest,
445 public ::testing::WithParamInterface<ThreeOperandTestParams> {
446 public:
447 TestTraceContainer process_sub_trace(ThreeOperandTestParams params)
448 {
449 auto [a, b, c] = params;
450 auto tag = static_cast<uint8_t>(a.get_tag());
451 auto trace = TestTraceContainer({
452 {
453 { C::alu_cf, a.as_ff() - b.as_ff() != c.as_ff() ? 1 : 0 },
454 { C::alu_ia, a },
455 { C::alu_ia_tag, tag },
456 { C::alu_ib, b },
457 { C::alu_ib_tag, tag },
458 { C::alu_ic, c },
459 { C::alu_ic_tag, tag },
460 { C::alu_max_bits, get_tag_bits(a.get_tag()) },
461 { C::alu_max_value, get_tag_max_value(a.get_tag()) },
462 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_SUB },
463 { C::alu_sel, 1 },
464 { C::alu_sel_op_sub, 1 },
465 { C::alu_sel_is_ff, tag == 0 ? 1 : 0 },
466 { C::alu_tag_ff_diff_inv, tag == 0 ? 0 : FF(tag).invert() },
467 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
468 { C::alu_tag_u128_diff_inv,
469 tag == static_cast<uint8_t>(MemoryTag::U128)
470 ? 0
471 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
472 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
473 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
474 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
475 { C::execution_register_0_, a }, // = ia
476 { C::execution_register_1_, b }, // = ib
477 { C::execution_register_2_, c }, // = ic
478 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
479 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_SUB }, // = alu_op_id
480 },
481 });
482
483 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
484 precomputed_builder.process_tag_parameters(trace);
485 return trace;
486 }
487
488 TestTraceContainer process_sub_with_tracegen(ThreeOperandTestParams params)
489 {
490 TestTraceContainer trace;
491 auto [a, b, c] = params;
492
493 builder.process(
494 {
495 { .operation = simulation::AluOperation::SUB, .a = a, .b = b, .c = c },
496 },
497 trace);
498
499 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
500 precomputed_builder.process_tag_parameters(trace);
501 return trace;
502 }
503};
504
505INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluSubConstrainingTest, ::testing::ValuesIn(TEST_VALUES_SUB));
506
507TEST_P(AluSubConstrainingTest, AluSub)
508{
509 auto trace = process_sub_trace(GetParam());
510 check_all_interactions<AluTraceBuilder>(trace);
511 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
512 check_relation<alu>(trace);
513}
514
515TEST_P(AluSubConstrainingTest, AluSubTraceGen)
516{
517 auto trace = process_sub_with_tracegen(GetParam());
518 check_all_interactions<AluTraceBuilder>(trace);
519 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
520 check_relation<alu>(trace);
521}
522
523TEST_P(AluSubConstrainingTest, AluSubNegative)
524{
525 auto params = GetParam();
526 auto is_ff = std::get<0>(params).get_tag() == MemoryTag::FF;
527 auto trace = process_sub_trace(GetParam());
528 check_all_interactions<AluTraceBuilder>(trace);
529 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
530 check_relation<alu>(trace);
531
532 auto c = trace.get(Column::alu_ic, 0);
533
534 trace.set(Column::alu_ic, 0, c + 1);
535 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ALU_ADD_SUB));
536
537 trace.set(Column::alu_ic, 0, c);
538 check_relation<alu>(trace);
539
540 // We get the correct underflowed result 'for free' with FF whether cf is on or not
541 if (!is_ff) {
542 trace.set(Column::alu_cf, 0, trace.get(Column::alu_cf, 0) == 1 ? 0 : 1);
543 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ALU_ADD_SUB));
544 }
545}
546
547// MUL TESTS
548
549const std::vector<MemoryValue> TEST_VALUES_MUL_OUT = {
550 MemoryValue::from_tag(MemoryTag::U1, 0),
551 MemoryValue::from_tag(MemoryTag::U8, 16),
552 MemoryValue::from_tag(MemoryTag::U16, 64456),
553 MemoryValue::from_tag(MemoryTag::U32, (uint256_t(1) << 32) - 50),
554 MemoryValue::from_tag(MemoryTag::U64, (uint256_t(1) << 64) - 50),
555 MemoryValue::from_tag(MemoryTag::U128, (uint256_t(1) << 128) - 50),
556 MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 8),
557};
558
559const std::vector<ThreeOperandTestParams> TEST_VALUES_MUL = zip_helper(TEST_VALUES_MUL_OUT);
560
561class AluMulConstrainingTest : public AluConstrainingTest,
562 public ::testing::WithParamInterface<ThreeOperandTestParams> {
563 public:
564 TestTraceContainer process_mul_trace(ThreeOperandTestParams params)
565 {
566 auto [a, b, c] = params;
567 auto mem_tag = a.get_tag();
568 auto tag = static_cast<uint8_t>(mem_tag);
569
570 auto is_u128 = mem_tag == MemoryTag::U128;
571
572 auto c_int = static_cast<uint256_t>(a.as_ff()) * static_cast<uint256_t>(b.as_ff());
573
574 uint256_t c_hi = 0;
575 if (mem_tag != MemoryTag::FF && mem_tag != MemoryTag::U128) {
576 c_hi = c_int >> static_cast<uint256_t>(get_tag_bits(mem_tag));
577 }
578
579 auto trace = TestTraceContainer({
580 {
581 { C::alu_c_hi, c_hi },
582 { C::alu_constant_64, 64 },
583 { C::alu_ia, a },
584 { C::alu_ia_tag, tag },
585 { C::alu_ib, b },
586 { C::alu_ib_tag, tag },
587 { C::alu_ic, c },
588 { C::alu_ic_tag, tag },
589 { C::alu_max_bits, get_tag_bits(mem_tag) },
590 { C::alu_max_value, get_tag_max_value(mem_tag) },
591 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_MUL },
592 { C::alu_sel, 1 },
593 { C::alu_sel_decompose_a, is_u128 ? 1 : 0 },
594 { C::alu_sel_is_ff, mem_tag == MemoryTag::FF ? 1 : 0 },
595 { C::alu_tag_ff_diff_inv, tag == 0 ? 0 : FF(tag).invert() },
596 { C::alu_sel_is_u128, is_u128 ? 1 : 0 },
597 { C::alu_sel_mul_div_u128, is_u128 ? 1 : 0 },
598 { C::alu_sel_op_mul, 1 },
599 { C::alu_sel_mul_no_err_non_ff, mem_tag == MemoryTag::FF ? 0 : 1 },
600 { C::alu_tag_u128_diff_inv, is_u128 ? 0 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
601 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
602 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
603 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
604 { C::execution_register_0_, a }, // = ia
605 { C::execution_register_1_, b }, // = ib
606 { C::execution_register_2_, c }, // = ic
607 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
608 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_MUL }, // = alu_op_id
609 },
610 });
611
612 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
613 precomputed_builder.process_tag_parameters(trace);
614
615 std::vector<RangeCheckEvent> range_check_events;
616
617 if (is_u128) {
618 auto a_decomp = simulation::decompose_128(a.as<uint128_t>());
619 auto b_decomp = simulation::decompose_128(b.as<uint128_t>());
620 // c_hi = (c_hi_full - a_hi * b_hi) % 2^64
621 auto hi_operand = static_cast<uint256_t>(a_decomp.hi) * static_cast<uint256_t>(b_decomp.hi);
622 c_hi = ((c_int >> 128) - hi_operand) % (uint256_t(1) << 64);
623 trace.set(0,
624 { { { Column::alu_a_lo, a_decomp.lo },
625 { Column::alu_a_lo_bits, 64 },
626 { Column::alu_a_hi, a_decomp.hi },
627 { Column::alu_a_hi_bits, 64 },
628 { Column::alu_b_lo, b_decomp.lo },
629 { Column::alu_b_hi, b_decomp.hi },
630 { Column::alu_c_hi, c_hi },
631 { Column::alu_cf, hi_operand > (uint256_t(1) << 64) ? 1 : 0 } } });
632
633 range_check_events.insert(range_check_events.end(),
634 { { .value = a_decomp.lo, .num_bits = 64 },
635 { .value = a_decomp.hi, .num_bits = 64 },
636 { .value = b_decomp.lo, .num_bits = 64 },
637 { .value = b_decomp.hi, .num_bits = 64 } });
638 }
639
640 range_check_events.push_back({ .value = static_cast<uint128_t>(c_hi), .num_bits = 64 });
641 range_check_builder.process(range_check_events, trace);
642
643 return trace;
644 }
645
646 TestTraceContainer process_mul_with_tracegen(ThreeOperandTestParams params)
647 {
648 TestTraceContainer trace;
649 auto [a, b, c] = params;
650 auto mem_tag = a.get_tag();
651
652 builder.process(
653 {
654 { .operation = simulation::AluOperation::MUL, .a = a, .b = b, .c = c },
655 },
656 trace);
657
658 uint256_t a_int = static_cast<uint256_t>(a.as_ff());
659 uint256_t b_int = static_cast<uint256_t>(b.as_ff());
660 auto c_hi = mem_tag == MemoryTag::FF ? 0 : (a_int * b_int) >> get_tag_bits(mem_tag);
661 if (mem_tag == MemoryTag::U128) {
662 auto a_decomp = simulation::decompose_128(a.as<uint128_t>());
663 auto b_decomp = simulation::decompose_128(b.as<uint128_t>());
664 // c_hi = (c_hi_full - a_hi * b_hi) % 2^64
665 auto c_hi_full = (a_int * b_int) >> 128;
666 auto hi_operand = static_cast<uint256_t>(a_decomp.hi) * static_cast<uint256_t>(b_decomp.hi);
667 c_hi = (c_hi_full - hi_operand) % (uint256_t(1) << 64);
668 range_check_builder.process({ { .value = a_decomp.lo, .num_bits = 64 },
669 { .value = a_decomp.hi, .num_bits = 64 },
670 { .value = b_decomp.lo, .num_bits = 64 },
671 { .value = b_decomp.hi, .num_bits = 64 },
672 { .value = static_cast<uint128_t>(c_hi), .num_bits = 64 } },
673 trace);
674 } else {
675 range_check_builder.process({ { .value = static_cast<uint128_t>(c_hi), .num_bits = 64 } }, trace);
676 }
677 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
678 precomputed_builder.process_tag_parameters(trace);
679 return trace;
680 }
681};
682
683INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluMulConstrainingTest, ::testing::ValuesIn(TEST_VALUES_MUL));
684
685TEST_P(AluMulConstrainingTest, AluMul)
686{
687 auto trace = process_mul_trace(GetParam());
688 check_all_interactions<AluTraceBuilder>(trace);
689 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
690 check_relation<alu>(trace);
691}
692
693TEST_P(AluMulConstrainingTest, AluMulTraceGen)
694{
695 auto trace = process_mul_with_tracegen(GetParam());
696 check_all_interactions<AluTraceBuilder>(trace);
697 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
698 check_relation<alu>(trace);
699}
700
701TEST_F(AluConstrainingTest, AluMulU128Carry)
702{
703 auto a = MemoryValue::from_tag(MemoryTag::U128, get_tag_max_value(MemoryTag::U128)); // = -1
704 auto b = MemoryValue::from_tag(MemoryTag::U128, get_tag_max_value(MemoryTag::U128) - 2); // = -3
705 auto c = a * b; // = 3
706 auto overflow_c_int = static_cast<uint256_t>(a.as_ff()) * static_cast<uint256_t>(b.as_ff());
707
708 auto tag = static_cast<uint8_t>(MemoryTag::U128);
709
710 auto a_decomp = simulation::decompose_128(a.as<uint128_t>());
711 auto b_decomp = simulation::decompose_128(b.as<uint128_t>());
712
713 // c_hi = old_c_hi - a_hi * b_hi % 2^64
714 uint256_t hi_operand =
715 ((overflow_c_int >> 128) - static_cast<uint256_t>(a_decomp.hi) * static_cast<uint256_t>(b_decomp.hi));
716 auto c_hi = hi_operand % (uint256_t(1) << 64);
717 auto cf = hi_operand >> 64;
718 auto trace = TestTraceContainer({
719 {
720 { C::alu_a_hi, a_decomp.hi },
721 { C::alu_a_hi_bits, 64 },
722 { C::alu_a_lo, a_decomp.lo },
723 { C::alu_a_lo_bits, 64 },
724 { C::alu_b_hi, b_decomp.hi },
725 { C::alu_b_lo, b_decomp.lo },
726 { C::alu_c_hi, c_hi },
727 { C::alu_cf, cf },
728 { C::alu_constant_64, 64 },
729 { C::alu_ia, a },
730 { C::alu_ia_tag, tag },
731 { C::alu_ib, b },
732 { C::alu_ib_tag, tag },
733 { C::alu_ic, c },
734 { C::alu_ic_tag, tag },
735 { C::alu_max_bits, get_tag_bits(MemoryTag::U128) },
736 { C::alu_max_value, get_tag_max_value(MemoryTag::U128) },
737 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_MUL },
738 { C::alu_sel, 1 },
739 { C::alu_sel_decompose_a, 1 },
740 { C::alu_sel_is_u128, 1 },
741 { C::alu_sel_mul_div_u128, 1 },
742 { C::alu_sel_op_mul, 1 },
743 { C::alu_sel_mul_no_err_non_ff, 1 },
744 { C::alu_tag_u128_diff_inv, 0 },
745 { C::alu_tag_ff_diff_inv, FF(tag).invert() },
746 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
747 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
748 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
749 { C::execution_register_0_, a }, // = ia
750 { C::execution_register_1_, b }, // = ib
751 { C::execution_register_2_, c }, // = ic
752 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
753 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_MUL }, // = alu_op_id
754 },
755 });
756
757 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
758 precomputed_builder.process_tag_parameters(trace);
759 range_check_builder.process({ { .value = a_decomp.lo, .num_bits = 64 },
760 { .value = a_decomp.hi, .num_bits = 64 },
761 { .value = b_decomp.lo, .num_bits = 64 },
762 { .value = b_decomp.hi, .num_bits = 64 },
763 { .value = static_cast<uint128_t>(c_hi), .num_bits = 64 } },
764 trace);
765
766 check_all_interactions<AluTraceBuilder>(trace);
767 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
768 check_relation<alu>(trace);
769
770 // Below = (a * b mod p) mod 2^128
771 auto should_fail_overflowed = MemoryValue::from_tag_truncating(MemoryTag::U128, a.as_ff() * b.as_ff());
772 trace.set(Column::alu_ic, 0, should_fail_overflowed);
773 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ALU_MUL_U128));
774}
775
776TEST_P(AluMulConstrainingTest, NegativeAluMul)
777{
778 auto trace = process_mul_trace(GetParam());
779 check_all_interactions<AluTraceBuilder>(trace);
780 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
781 check_relation<alu>(trace);
782 trace.set(Column::alu_ic, 0, trace.get(Column::alu_ic, 0) + 1);
783 // U128 multiplication is constrained by a dedicated subrelation; all other tags share another.
784 auto expected_subrelation =
785 std::get<0>(GetParam()).get_tag() == MemoryTag::U128 ? alu::SR_ALU_MUL_U128 : alu::SR_ALU_MUL_NON_U128;
786 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(expected_subrelation));
787}
788
789// DIV TESTS
790
791const std::vector<MemoryValue> TEST_VALUES_DIV_OUT = {
792 MemoryValue::from_tag(MemoryTag::U1, 0), // Dividing by zero, so expecting an error
793 MemoryValue::from_tag(MemoryTag::U8, 4),
794 MemoryValue::from_tag(MemoryTag::U16, 0),
795 MemoryValue::from_tag(MemoryTag::U32, 0x33333331),
796 MemoryValue::from_tag(MemoryTag::U64, 0x3333333333333331ULL),
797 MemoryValue::from_tag(MemoryTag::U128, (((uint256_t(1) << 128) - 11) / 5)), // 0x3333333333333333333333333333331
798};
799
800const std::vector<ThreeOperandTestParams> TEST_VALUES_DIV = zip_helper(TEST_VALUES_DIV_OUT);
801
802class AluDivConstrainingTest : public AluConstrainingTest,
803 public ::testing::WithParamInterface<ThreeOperandTestParams> {
804 public:
805 TestTraceContainer process_div_trace(ThreeOperandTestParams params)
806 {
807 auto [a, b, c] = params;
808 auto mem_tag = a.get_tag();
809 auto tag = static_cast<uint8_t>(mem_tag);
810 auto remainder = a - b * c;
811
812 auto div_0_error = b.as_ff() == FF(0);
813 auto is_u128 = mem_tag == MemoryTag::U128;
814
815 auto trace = TestTraceContainer({
816 {
817 { C::alu_b_inv, div_0_error ? 0 : b.as_ff().invert() },
818 { C::alu_constant_64, 64 },
819 { C::alu_helper1, div_0_error ? 0 : remainder.as_ff() },
820 { C::alu_ia, a },
821 { C::alu_ia_tag, tag },
822 { C::alu_ib, b },
823 { C::alu_ib_tag, tag },
824 { C::alu_ic, c },
825 { C::alu_ic_tag, tag },
826 { C::alu_max_bits, get_tag_bits(mem_tag) },
827 { C::alu_max_value, get_tag_max_value(mem_tag) },
828 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_DIV },
829 { C::alu_sel, 1 },
830 { C::alu_sel_decompose_a, is_u128 ? 1 : 0 },
831 { C::alu_sel_div_0_err, div_0_error ? 1 : 0 },
832 { C::alu_sel_div_no_err, div_0_error ? 0 : 1 },
833 { C::alu_sel_int_gt, div_0_error ? 0 : 1 },
834 { C::alu_gt_input_a, b.as_ff() },
835 { C::alu_gt_input_b, div_0_error ? 0 : remainder.as_ff() },
836 { C::alu_gt_result_c, div_0_error ? 0 : 1 },
837 { C::alu_sel_err, div_0_error ? 1 : 0 },
838 { C::alu_sel_is_u128, is_u128 ? 1 : 0 },
839 { C::alu_sel_mul_div_u128, is_u128 ? 1 : 0 },
840 { C::alu_sel_op_div, 1 },
841 { C::alu_tag_ff_diff_inv, FF(tag - static_cast<uint8_t>(MemoryTag::FF)).invert() },
842 { C::alu_tag_u128_diff_inv, is_u128 ? 0 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
843 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
844 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
845 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
846 { C::execution_register_0_, a }, // = ia
847 { C::execution_register_1_, b }, // = ib
848 { C::execution_register_2_, c }, // = ic
849 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
850 { C::execution_sel_opcode_error, div_0_error ? 1 : 0 }, // = sel_err
851 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_DIV }, // = alu_op_id
852 },
853 });
854
855 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
856 precomputed_builder.process_tag_parameters(trace);
857 gt_builder.process({ { .a = static_cast<uint128_t>(b.as_ff()),
858 .b = static_cast<uint128_t>(remainder.as_ff()),
859 .result = true } },
860 trace);
861
862 if (is_u128) {
863 auto c_decomp = simulation::decompose_128(c.as<uint128_t>());
864 auto b_decomp = simulation::decompose_128(b.as<uint128_t>());
865
866 trace.set(0,
867 { { { Column::alu_a_lo, c_decomp.lo },
868 { Column::alu_a_lo_bits, 64 },
869 { Column::alu_a_hi, c_decomp.hi },
870 { Column::alu_a_hi_bits, 64 },
871 { Column::alu_b_lo, b_decomp.lo },
872 { Column::alu_b_hi, b_decomp.hi } } });
873
874 // Combine remainder range check with U128 decomposition range checks in a single
875 // process call, since process() always starts from row 0.
876 if (!div_0_error) {
877 range_check_builder.process(
878 { { .value = static_cast<uint128_t>(remainder.as_ff()), .num_bits = get_tag_bits(mem_tag) },
879 { .value = c_decomp.lo, .num_bits = 64 },
880 { .value = c_decomp.hi, .num_bits = 64 },
881 { .value = b_decomp.lo, .num_bits = 64 },
882 { .value = b_decomp.hi, .num_bits = 64 } },
883 trace);
884 } else {
885 range_check_builder.process({ { .value = c_decomp.lo, .num_bits = 64 },
886 { .value = c_decomp.hi, .num_bits = 64 },
887 { .value = b_decomp.lo, .num_bits = 64 },
888 { .value = b_decomp.hi, .num_bits = 64 } },
889 trace);
890 }
891 } else if (!div_0_error) {
892 // Range check the remainder fits within max_bits.
893 range_check_builder.process(
894 { { .value = static_cast<uint128_t>(remainder.as_ff()), .num_bits = get_tag_bits(mem_tag) } }, trace);
895 }
896
897 return trace;
898 }
899
900 TestTraceContainer process_div_with_tracegen(ThreeOperandTestParams params)
901 {
902 TestTraceContainer trace;
903 auto [a, b, c] = params;
904 bool div_0_error = b.as_ff() == FF(0);
905 auto mem_tag = a.get_tag();
906
907 MemoryValue remainder = MemoryValue::from_tag(MemoryTag::FF, 0);
908 if (!div_0_error && mem_tag == b.get_tag() && mem_tag != MemoryTag::FF) {
909 remainder = a - b * c;
910 }
911
912 builder.process(
913 {
914 { .operation = simulation::AluOperation::DIV, .a = a, .b = b, .c = c, .error = div_0_error },
915 },
916 trace);
917
918 if (mem_tag == MemoryTag::U128) {
919 auto c_decomp = simulation::decompose_128(static_cast<uint128_t>(c.as_ff()));
920 auto b_decomp = simulation::decompose_128(static_cast<uint128_t>(b.as_ff()));
921
922 // Combine remainder range check with U128 decomposition range checks in a single
923 // process call, since process() always starts from row 0.
924 if (!div_0_error) {
925 range_check_builder.process(
926 { { .value = static_cast<uint128_t>(remainder.as_ff()), .num_bits = get_tag_bits(mem_tag) },
927 { .value = c_decomp.lo, .num_bits = 64 },
928 { .value = c_decomp.hi, .num_bits = 64 },
929 { .value = b_decomp.lo, .num_bits = 64 },
930 { .value = b_decomp.hi, .num_bits = 64 } },
931 trace);
932 } else {
933 range_check_builder.process({ { .value = c_decomp.lo, .num_bits = 64 },
934 { .value = c_decomp.hi, .num_bits = 64 },
935 { .value = b_decomp.lo, .num_bits = 64 },
936 { .value = b_decomp.hi, .num_bits = 64 } },
937 trace);
938 }
939 } else if (!div_0_error) {
940 // Range check the remainder fits within max_bits.
941 range_check_builder.process(
942 { { .value = static_cast<uint128_t>(remainder.as_ff()), .num_bits = get_tag_bits(mem_tag) } }, trace);
943 }
944 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
945 precomputed_builder.process_tag_parameters(trace);
946 gt_builder.process({ { .a = static_cast<uint128_t>(b.as_ff()),
947 .b = static_cast<uint128_t>(remainder.as_ff()),
948 .result = true } },
949 trace);
950 return trace;
951 }
952};
953
954INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluDivConstrainingTest, ::testing::ValuesIn(TEST_VALUES_DIV));
955
956TEST_P(AluDivConstrainingTest, AluDiv)
957{
958 auto trace = process_div_trace(GetParam());
959 check_all_interactions<AluTraceBuilder>(trace);
960 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
961 check_relation<alu>(trace);
962}
963
964TEST_P(AluDivConstrainingTest, AluDivTraceGen)
965{
966 auto trace = process_div_with_tracegen(GetParam());
967 check_all_interactions<AluTraceBuilder>(trace);
968 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
969 check_relation<alu>(trace);
970}
971
972TEST_F(AluDivConstrainingTest, AluDivByZeroMismatchTagsTraceGen)
973{
974 auto a = MemoryValue::from_tag(MemoryTag::U128, 2);
975 auto b = MemoryValue::from_tag(MemoryTag::U64, 0);
976 auto c = MemoryValue::from_tag(MemoryTag::FF, 0);
977
978 auto trace = process_div_with_tracegen({ a, b, c });
979 check_relation<alu>(trace);
980 check_all_interactions<AluTraceBuilder>(trace);
981}
982
983TEST_F(AluDivConstrainingTest, AluDivByZeroTagFFAndMismatchTagsTraceGen)
984{
985 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
986 auto b = MemoryValue::from_tag(MemoryTag::U32, 0);
987 auto c = MemoryValue::from_tag(MemoryTag::FF, 0);
988
989 auto trace = process_div_with_tracegen({ a, b, c });
990 check_relation<alu>(trace);
991 check_all_interactions<AluTraceBuilder>(trace);
992}
993
994TEST_F(AluDivConstrainingTest, NegativeAluDivUnderflow)
995{
996 // Test that for a < b, the circuit does not accept c != 0
997 auto a = MemoryValue::from_tag(MemoryTag::U32, 2);
998 auto b = MemoryValue::from_tag(MemoryTag::U32, 5);
999 auto c = a / b;
1000 auto trace = process_div_trace({ a, b, c });
1001 check_all_interactions<AluTraceBuilder>(trace);
1002 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1003 check_relation<alu>(trace);
1004
1005 // Good path: 2/5 gives 0 with remainder = 2
1006 // Bad path: 5 * c = 2 - r => set c = 2, so r = p - 8:
1007
1008 c = MemoryValue::from_tag(MemoryTag::U32, 2);
1009 auto wrong_remainder = a.as_ff() - b.as_ff() * c.as_ff();
1010
1011 trace.set(Column::alu_ic, 0, c);
1012 trace.set(Column::alu_helper1, 0, wrong_remainder);
1013 trace.set(Column::alu_gt_input_b, 0, wrong_remainder);
1014
1015 // All relations will pass...
1016 check_relation<alu>(trace);
1017 // ... but the remainder (p - 8) is not in range, so the range check fails:
1019 (check_interaction<AluTraceBuilder, lookup_alu_range_check_div_remainder_settings>(trace)),
1020 "RANGE_CHECK_DIV_REMAINDER");
1021 // ... and r > b, so the gt lookup also fails:
1022 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_int_gt_settings>(trace)),
1023 "LOOKUP_ALU_INT_GT");
1024}
1025
1026TEST_F(AluDivConstrainingTest, NegativeAluDivU128Carry)
1027{
1028 // Test that for a < b, the circuit does not accept c != 0
1029 auto a = MemoryValue::from_tag(MemoryTag::U128, 2);
1030 auto b = MemoryValue::from_tag(MemoryTag::U128, (uint256_t(1) << 64) + 2);
1031 auto c = a / b;
1032
1033 auto trace = process_div_trace({ a, b, c });
1034
1035 check_all_interactions<AluTraceBuilder>(trace);
1036 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1037 check_relation<alu>(trace);
1038
1039 // Check we cannot provide a c s.t. a - r = b * c over/underflows
1040
1041 c = MemoryValue::from_tag(MemoryTag::U128, (uint256_t(1) << 64) + 3);
1042 auto wrong_remainder = a.as_ff() - FF(static_cast<uint256_t>(b.as_ff()) * static_cast<uint256_t>(c.as_ff()));
1043
1044 // We now have c and wrong_remainder s.t. a - wrong_remainder == b * c in the field...
1045
1046 trace.set(Column::alu_ic, 0, c);
1047 trace.set(Column::alu_helper1, 0, wrong_remainder);
1048
1049 // ...but we haven't provided a correct decomposition of the new bad c:
1050 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_A_DECOMPOSITION));
1051
1052 auto c_decomp = simulation::decompose_128(c.as<uint128_t>());
1053 trace.set(Column::alu_a_lo, 0, c_decomp.lo);
1054 trace.set(Column::alu_a_hi, 0, c_decomp.hi);
1055
1056 // Setting the decomposed values still (correctly) fails:
1057 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ALU_DIV_U128_CHECK));
1058}
1059
1060TEST_F(AluDivConstrainingTest, NegativeAluDivByZero)
1061{
1062 auto a = MemoryValue::from_tag(MemoryTag::U32, 2);
1063 auto b = MemoryValue::from_tag(MemoryTag::U32, 5);
1064 auto c = a / b;
1065
1066 for (const bool with_tracegen : { false, true }) {
1067 auto trace = with_tracegen ? process_div_with_tracegen({ a, b, c }) : process_div_trace({ a, b, c });
1068 check_all_interactions<AluTraceBuilder>(trace);
1069 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1070 check_relation<alu>(trace);
1071
1072 // Set b, b_inv to 0...
1073 trace.set(Column::alu_ib, 0, 0);
1074 trace.set(Column::alu_b_inv, 0, 0);
1075 // ...and since we haven't set the error correctly, we expect the below to fail:
1076 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1077 // We need to set the div_0_err and...
1078 trace.set(Column::alu_sel_div_0_err, 0, 1);
1079 trace.set(Column::alu_sel_div_no_err, 0, 0);
1080 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ERR_CHECK));
1081 // ...the overall sel_err:
1082 trace.set(Column::alu_sel_err, 0, 1);
1083 trace.set(Column::alu_sel_int_gt, 0, 0);
1084 trace.set(Column::alu_gt_input_a, 0, 0);
1085 trace.set(Column::alu_gt_input_b, 0, 0);
1086 trace.set(Column::alu_gt_result_c, 0, 0);
1087 check_relation<alu>(trace);
1088
1089 // If we try and have div_0_err on without doing a div, the below should fail:
1090 trace.set(Column::alu_sel_op_div, 0, 0);
1091 trace.set(Column::alu_sel_op_mul, 0, 1);
1092 trace.set(Column::alu_op_id, 0, AVM_EXEC_OP_ID_ALU_MUL);
1093 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace),
1094 alu::get_subrelation_label(alu::SR_ONLY_RELEVANT_CHECK_DIV_0_ERR_ERROR));
1095
1096 trace.set(Column::alu_sel_op_div, 0, 1);
1097 trace.set(Column::alu_sel_op_mul, 0, 0);
1098 trace.set(Column::alu_op_id, 0, AVM_EXEC_OP_ID_ALU_DIV);
1099 check_relation<alu>(trace);
1100
1101 // If we try and set b != 0 with div_0_err on, the below should fail:
1102 trace.set(Column::alu_ib, 0, b);
1103 trace.set(Column::alu_b_inv, 0, b.as_ff().invert());
1104 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1105 }
1106}
1107
1108TEST_F(AluDivConstrainingTest, NegativeAluDivFF)
1109{
1110 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
1111 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
1112 auto c = a / b;
1113 auto trace = process_div_with_tracegen({ a, b, c });
1114 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
1115 // This case should be recoverable, so we set the tag err selectors:
1116 trace.set(Column::alu_sel_tag_err, 0, 1);
1117 trace.set(Column::alu_sel_err, 0, 1);
1118 trace.set(Column::alu_sel_div_no_err, 0, 0);
1119 trace.set(Column::alu_sel_int_gt, 0, 0);
1120 trace.set(Column::alu_gt_input_a, 0, 0);
1121 trace.set(Column::alu_gt_input_b, 0, 0);
1122 trace.set(Column::alu_gt_result_c, 0, 0);
1123 check_relation<alu>(trace);
1124 check_all_interactions<AluTraceBuilder>(trace);
1125 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1126}
1127
1128TEST_F(AluDivConstrainingTest, NegativeAluDivByZeroFF)
1129{
1130 // For DIV, we can have both FF and dividing by zero errors:
1131 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
1132 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
1133 auto c = a / b;
1134 auto trace = process_div_with_tracegen({ a, b, c });
1135 trace.set(Column::alu_sel_tag_err, 0, 1);
1136 trace.set(Column::alu_sel_err, 0, 1);
1137 trace.set(Column::alu_sel_div_no_err, 0, 0);
1138 trace.set(Column::alu_sel_int_gt, 0, 0);
1139 trace.set(Column::alu_gt_input_a, 0, 0);
1140 trace.set(Column::alu_gt_input_b, 0, 0);
1141 trace.set(Column::alu_gt_result_c, 0, 0);
1142 check_relation<alu>(trace);
1143 // Set b, b_inv to 0 with dividing by 0 errors:
1144 trace.set(Column::alu_ib, 0, 0);
1145 trace.set(Column::alu_b_inv, 0, 0);
1146 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1147 trace.set(Column::alu_sel_div_0_err, 0, 1);
1148 check_relation<alu>(trace);
1149 check_all_interactions<AluTraceBuilder>(trace);
1150 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1151}
1152
1153TEST_F(AluDivConstrainingTest, NegativeAluDivByZeroFFTagMismatch)
1154{
1155 // For DIV, we can have FF, tag mismatch, and dividing by zero errors:
1156 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
1157 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
1158 auto c = a / b;
1159 auto trace = process_div_with_tracegen({ a, b, c });
1160 trace.set(Column::alu_sel_tag_err, 0, 1);
1161 trace.set(Column::alu_sel_err, 0, 1);
1162 trace.set(Column::alu_sel_div_no_err, 0, 0);
1163 trace.set(Column::alu_sel_int_gt, 0, 0);
1164 trace.set(Column::alu_gt_input_a, 0, 0);
1165 trace.set(Column::alu_gt_input_b, 0, 0);
1166 trace.set(Column::alu_gt_result_c, 0, 0);
1167 check_relation<alu>(trace);
1168 // Setting b to u8 also creates a tag mismatch:
1169 trace.set(Column::alu_ib_tag, 0, static_cast<uint8_t>(MemoryTag::U8));
1170 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
1171 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 1);
1172 trace.set(Column::alu_ab_tags_diff_inv,
1173 0,
1174 (FF(static_cast<uint8_t>(MemoryTag::FF)) - FF(static_cast<uint8_t>(MemoryTag::U8))).invert());
1175 check_relation<alu>(trace);
1176 // We can also handle dividing by 0:
1177 trace.set(Column::alu_ib, 0, 0);
1178 trace.set(Column::alu_b_inv, 0, 0);
1179 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1180 trace.set(Column::alu_sel_div_0_err, 0, 1);
1181 trace.set(Column::alu_sel_div_no_err, 0, 0);
1182 check_relation<alu>(trace);
1183 check_all_interactions<AluTraceBuilder>(trace);
1184 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1185}
1186
1187// FDIV TESTS
1188
1189// Note: The test framework below converts all inputs to FF values to allow for many happy path tests without adding
1190// new vectors. Non-FF values are tested separately.
1191const std::vector<MemoryValue> TEST_VALUES_FDIV_OUT = {
1192 MemoryValue::from_tag(MemoryTag::FF, 0), // Dividing by zero, so expecting an error
1193 MemoryValue::from_tag(MemoryTag::FF, 4),
1194 MemoryValue::from_tag(MemoryTag::FF, FF("0x1e980ebbc51694827ee20074ac28b250a037a43eb44b38e6aa367c57a05e6d48")),
1195 MemoryValue::from_tag(MemoryTag::FF, FF("0x135b52945a13d9aa49b9b57c33cd568ba9ae5ce9ca4a2d06e7f3fbd4f9999998")),
1196 MemoryValue::from_tag(MemoryTag::FF, FF("0x135b52945a13d9aa49b9b57c33cd568ba9ae5ce9ca4a2d071b272f07f9999998")),
1197 MemoryValue::from_tag(MemoryTag::FF, FF("0x135b52945a13d9aa49b9b57c33cd568bdce1901cfd7d603a1b272f07f9999998")),
1198 MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 2),
1199};
1200
1201const std::vector<ThreeOperandTestParams> TEST_VALUES_FDIV = zip_helper(TEST_VALUES_FDIV_OUT);
1202
1203class AluFDivConstrainingTest : public AluConstrainingTest,
1204 public ::testing::WithParamInterface<ThreeOperandTestParams> {
1205 public:
1206 TestTraceContainer process_fdiv_trace(ThreeOperandTestParams params)
1207 {
1208 auto [a, b, c] = params;
1209 a = MemoryValue::from_tag(MemoryTag::FF, a);
1210 b = MemoryValue::from_tag(MemoryTag::FF, b);
1211 c = MemoryValue::from_tag(MemoryTag::FF, c);
1212 auto div_0_error = b.as_ff() == FF(0);
1213
1214 auto mem_tag = a.get_tag();
1215 auto tag = static_cast<uint8_t>(mem_tag);
1216
1217 auto trace = TestTraceContainer({
1218 {
1219 { C::alu_b_inv, div_0_error ? 0 : b.as_ff().invert() },
1220 { C::alu_ia, a },
1221 { C::alu_ia_tag, tag },
1222 { C::alu_ib, b },
1223 { C::alu_ib_tag, tag },
1224 { C::alu_ic, c },
1225 { C::alu_ic_tag, tag },
1226 { C::alu_max_bits, get_tag_bits(mem_tag) },
1227 { C::alu_max_value, get_tag_max_value(mem_tag) },
1228 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_FDIV },
1229 { C::alu_sel, 1 },
1230 { C::alu_sel_div_0_err, div_0_error ? 1 : 0 },
1231 { C::alu_sel_err, div_0_error ? 1 : 0 },
1232 { C::alu_sel_is_ff, 1 },
1233 { C::alu_sel_op_fdiv, 1 },
1234 { C::alu_tag_u128_diff_inv, FF(-static_cast<uint8_t>(MemoryTag::U128)).invert() },
1235 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
1236 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
1237 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
1238 { C::execution_register_0_, a }, // = ia
1239 { C::execution_register_1_, b }, // = ib
1240 { C::execution_register_2_, c }, // = ic
1241 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
1242 { C::execution_sel_opcode_error, div_0_error ? 1 : 0 }, // = sel_err
1243 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_FDIV }, // = alu_op_id
1244 },
1245 });
1246
1247 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1248 precomputed_builder.process_tag_parameters(trace);
1249
1250 return trace;
1251 }
1252
1253 TestTraceContainer process_fdiv_with_tracegen(ThreeOperandTestParams params, bool upcast_to_ff = false)
1254 {
1255 TestTraceContainer trace;
1256 auto [a, b, c] = params;
1257
1258 if (upcast_to_ff) {
1259 a = MemoryValue::from_tag(MemoryTag::FF, a);
1260 b = MemoryValue::from_tag(MemoryTag::FF, b);
1261 c = MemoryValue::from_tag(MemoryTag::FF, c);
1262 }
1263
1264 bool div_0_error = b.as_ff() == FF(0);
1265
1266 builder.process(
1267 {
1268 { .operation = simulation::AluOperation::FDIV, .a = a, .b = b, .c = c, .error = div_0_error },
1269 },
1270 trace);
1271
1272 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1273 precomputed_builder.process_tag_parameters(trace);
1274
1275 return trace;
1276 }
1277};
1278
1279INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluFDivConstrainingTest, ::testing::ValuesIn(TEST_VALUES_FDIV));
1280
1281TEST_P(AluFDivConstrainingTest, AluFDiv)
1282{
1283 auto trace = process_fdiv_trace(GetParam());
1284 check_all_interactions<AluTraceBuilder>(trace);
1285 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1286 check_relation<alu>(trace);
1287}
1288
1289TEST_P(AluFDivConstrainingTest, AluFDivTraceGen)
1290{
1291 auto trace = process_fdiv_with_tracegen(GetParam(), true);
1292 // InteractiveDebugger debugger(trace);
1293 // debugger.run();
1294 check_all_interactions<AluTraceBuilder>(trace);
1295 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1296 check_relation<alu>(trace);
1297}
1298
1299TEST_F(AluFDivConstrainingTest, AluFDivByZeroNonFFTagTraceGen)
1300{
1301 auto a = MemoryValue::from_tag(MemoryTag::U8, 2);
1302 auto b = MemoryValue::from_tag(MemoryTag::U8, 0);
1303 auto c = MemoryValue::from_tag(MemoryTag::FF, 0);
1304
1305 auto trace = process_fdiv_with_tracegen({ a, b, c });
1306 check_relation<alu>(trace);
1307 check_all_interactions<AluTraceBuilder>(trace);
1308}
1309
1310TEST_F(AluFDivConstrainingTest, AluFDivByZeroNonFFTagMismatchTraceGen)
1311{
1312 auto a = MemoryValue::from_tag(MemoryTag::U8, 2);
1313 auto b = MemoryValue::from_tag(MemoryTag::U16, 0);
1314 auto c = MemoryValue::from_tag(MemoryTag::FF, 0);
1315 auto trace = process_fdiv_with_tracegen({ a, b, c });
1316 check_relation<alu>(trace);
1317 check_all_interactions<AluTraceBuilder>(trace);
1318}
1319
1320TEST_F(AluFDivConstrainingTest, NegativeAluFDivByZero)
1321{
1322 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
1323 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
1324 auto c = a / b;
1325 auto trace = process_fdiv_trace({ a, b, c });
1326 check_all_interactions<AluTraceBuilder>(trace);
1327 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1328 check_relation<alu>(trace);
1329
1330 // Set b, b_inv to 0...
1331 trace.set(Column::alu_ib, 0, 0);
1332 trace.set(Column::alu_b_inv, 0, 0);
1333 // ...and since we haven't set the error correctly, we expect the below to fail:
1334 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1335 // We need to set the div_0_err and...
1336 trace.set(Column::alu_sel_div_0_err, 0, 1);
1337 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_ERR_CHECK));
1338 // ...the overall sel_err:
1339 trace.set(Column::alu_sel_err, 0, 1);
1340 check_relation<alu>(trace);
1341
1342 // If we try and set b != 0 with div_0_err on, the below should fail:
1343 trace.set(Column::alu_ib, 0, b);
1344 trace.set(Column::alu_b_inv, 0, b.as_ff().invert());
1345 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1346}
1347
1348TEST_F(AluFDivConstrainingTest, NegativeAluFDivByZeroNonFFTagMismatch)
1349{
1350 auto a = MemoryValue::from_tag(MemoryTag::U8, 4);
1351 auto b = MemoryValue::from_tag(MemoryTag::U8, 2);
1352 // An incorrect c_tag fails the relation rather than throwing a tag error - we want to test the throw here, so
1353 // setting c to be the correct tag:
1354 auto c = MemoryValue::from_tag(MemoryTag::FF, 2);
1355 auto tag = static_cast<uint8_t>(MemoryTag::U8);
1356
1357 auto trace = TestTraceContainer({
1358 {
1359 { C::alu_b_inv, b.as_ff().invert() },
1360 { C::alu_ia, a },
1361 { C::alu_ia_tag, tag },
1362 { C::alu_ib, b },
1363 { C::alu_ib_tag, tag },
1364 { C::alu_ic, c },
1365 { C::alu_ic_tag, static_cast<uint8_t>(MemoryTag::FF) },
1366 { C::alu_max_bits, get_tag_bits(MemoryTag::U8) },
1367 { C::alu_max_value, get_tag_max_value(MemoryTag::U8) },
1368 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_FDIV },
1369 { C::alu_sel, 1 },
1370 { C::alu_sel_op_fdiv, 1 },
1371 { C::alu_sel_tag_err, 1 },
1372 { C::alu_sel_err, 1 },
1373 { C::alu_tag_ff_diff_inv, (FF(tag) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
1374 { C::alu_tag_u128_diff_inv, (FF(tag) - FF(static_cast<uint8_t>(MemoryTag::U128))).invert() },
1375 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
1376 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
1377 { C::execution_mem_tag_reg_2_, static_cast<uint8_t>(MemoryTag::FF) }, // = ic_tag
1378 { C::execution_register_0_, a }, // = ia
1379 { C::execution_register_1_, b }, // = ib
1380 { C::execution_register_2_, c }, // = ic
1381 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
1382 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_FDIV }, // = alu_op_id
1383 { C::execution_sel_opcode_error, 1 }, // = sel_err
1384 },
1385 });
1386
1387 // Every column is set up correctly. All checks should pass:
1388 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1389 precomputed_builder.process_tag_parameters(trace);
1390 check_relation<alu>(trace);
1391 check_all_interactions<AluTraceBuilder>(trace);
1392 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1393
1394 // We un-toggle sel_tag_err and sel_err and expect the following failure:
1395 trace.set(Column::alu_sel_tag_err, 0, 0);
1396 trace.set(Column::alu_sel_err, 0, 0);
1397 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
1398
1399 // We try to cheat by setting the tag diff inverse to 0 and claiming a is FF, but expect the following failure:
1400 trace.set(Column::alu_tag_ff_diff_inv, 0, 0);
1401 trace.set(Column::alu_sel_is_ff, 0, 1);
1402 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_IS_FF));
1403
1404 // Reset to the correct values:
1405 trace.set(Column::alu_tag_ff_diff_inv, 0, (FF(tag) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert());
1406 trace.set(Column::alu_sel_is_ff, 0, 0);
1407 trace.set(Column::alu_sel_tag_err, 0, 1);
1408 trace.set(Column::alu_sel_err, 0, 1);
1409 check_relation<alu>(trace);
1410
1411 // For FDIV, we can have both FF and dividing by zero errors:
1412 trace.set(Column::alu_ib, 0, 0);
1413 trace.set(Column::alu_b_inv, 0, 0);
1414 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_DIV_0_ERR));
1415 trace.set(Column::alu_sel_div_0_err, 0, 1);
1416 check_relation<alu>(trace);
1417 check_all_interactions<AluTraceBuilder>(trace);
1418 trace.set(Column::execution_register_1_, 0, 0);
1419 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1420
1421 // Setting b to u16 also creates a tag mismatch we can handle with the same selectors:
1422 trace.set(Column::alu_ib_tag, 0, static_cast<uint8_t>(MemoryTag::U16));
1423 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
1424 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 1);
1425 trace.set(Column::alu_ab_tags_diff_inv, 0, (FF(tag) - FF(static_cast<uint8_t>(MemoryTag::U16))).invert());
1426 check_relation<alu>(trace);
1427}
1428
1429// EQ TESTS
1430
1431const std::vector<MemoryValue> TEST_VALUES_EQ_OUT(NUM_OF_TAGS, MemoryValue::from_tag(MemoryTag::U1, 0));
1432
1433const std::vector<ThreeOperandTestParams> TEST_VALUES_EQ = zip_helper(TEST_VALUES_EQ_OUT);
1434
1435class AluEQConstrainingTest : public AluConstrainingTest, public ::testing::WithParamInterface<ThreeOperandTestParams> {
1436 public:
1437 TestTraceContainer process_eq_with_tracegen(const ThreeOperandTestParams& params)
1438 {
1439 TestTraceContainer trace;
1440 auto [a, b, c] = params;
1441
1442 builder.process(
1443 {
1444 { .operation = simulation::AluOperation::EQ, .a = a, .b = b, .c = c },
1445 },
1446 trace);
1447
1448 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1449 precomputed_builder.process_tag_parameters(trace);
1450 return trace;
1451 }
1452};
1453
1454INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluEQConstrainingTest, ::testing::ValuesIn(TEST_VALUES_EQ));
1455
1456TEST_P(AluEQConstrainingTest, AluEQTraceGen)
1457{
1458 const MemoryValue& param = std::get<0>(GetParam());
1459 auto trace =
1460 process_eq_with_tracegen(ThreeOperandTestParams{ param, param, MemoryValue::from_tag(MemoryTag::U1, 1) });
1461 check_all_interactions<AluTraceBuilder>(trace);
1462 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1463 check_relation<alu>(trace);
1464}
1465
1466TEST_P(AluEQConstrainingTest, AluInEQTraceGen)
1467{
1468 auto trace = process_eq_with_tracegen(GetParam());
1469 check_all_interactions<AluTraceBuilder>(trace);
1470 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1471 check_relation<alu>(trace);
1472}
1473
1474TEST_P(AluEQConstrainingTest, NegativeAluEqResult)
1475{
1476 auto params = GetParam();
1477 for (const bool is_eq : { false, true }) {
1478 auto trace = process_eq_with_tracegen(is_eq ? ThreeOperandTestParams{ std::get<0>(params),
1479 std::get<0>(params),
1480 MemoryValue::from_tag(MemoryTag::U1, 1) }
1481 : params);
1482 check_relation<alu>(trace);
1483 check_all_interactions<AluTraceBuilder>(trace);
1484 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1485 bool c = trace.get(Column::alu_ic, 0) == 1;
1486 // Swap the result bool:
1487 trace.set(Column::alu_ic, 0, static_cast<uint8_t>(!c));
1488 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_EQ_OP_MAIN));
1489 }
1490}
1491
1492TEST_P(AluEQConstrainingTest, NegativeAluEqHelper)
1493{
1494 auto trace = process_eq_with_tracegen(GetParam());
1495 check_relation<alu>(trace);
1496 check_all_interactions<AluTraceBuilder>(trace);
1497 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1498 auto ab_diff_inv = trace.get(Column::alu_ab_diff_inv, 0);
1499 trace.set(Column::alu_ab_diff_inv, 0, ab_diff_inv + 1);
1500 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_EQ_OP_MAIN));
1501}
1502
1503// LT TESTS
1504
1505const std::vector<MemoryValue> TEST_VALUES_LT_OUT = {
1506 MemoryValue::from_tag(MemoryTag::U1, 0), MemoryValue::from_tag(MemoryTag::U1, 0),
1507 MemoryValue::from_tag(MemoryTag::U1, 0), MemoryValue::from_tag(MemoryTag::U1, 1),
1508 MemoryValue::from_tag(MemoryTag::U1, 0), MemoryValue::from_tag(MemoryTag::U1, 0),
1509 MemoryValue::from_tag(MemoryTag::U1, 0),
1510};
1511
1512const std::vector<ThreeOperandTestParams> TEST_VALUES_LT = zip_helper(TEST_VALUES_LT_OUT);
1513
1514class AluLTConstrainingTest : public AluConstrainingTest, public ::testing::WithParamInterface<ThreeOperandTestParams> {
1515 public:
1516 TestTraceContainer process_lt_trace(ThreeOperandTestParams params)
1517 {
1518 auto [a, b, c] = params;
1519 auto mem_tag = a.get_tag();
1520 auto tag = static_cast<uint8_t>(mem_tag);
1521 auto is_ff = mem_tag == MemoryTag::FF;
1522
1523 auto trace = TestTraceContainer({
1524 {
1525 { C::alu_ia, a },
1526 { C::alu_ia_tag, tag },
1527 { C::alu_ib, b },
1528 { C::alu_ib_tag, tag },
1529 { C::alu_ic, c },
1530 { C::alu_ic_tag, static_cast<uint8_t>(MemoryTag::U1) },
1531 { C::alu_gt_input_a, b },
1532 { C::alu_gt_input_b, a },
1533 { C::alu_gt_result_c, c },
1534 { C::alu_max_bits, get_tag_bits(mem_tag) },
1535 { C::alu_max_value, get_tag_max_value(mem_tag) },
1536 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_LT },
1537 { C::alu_sel, 1 },
1538 { C::alu_sel_ff_gt, static_cast<uint8_t>(is_ff) },
1539 { C::alu_sel_int_gt, static_cast<uint8_t>(!is_ff) },
1540 { C::alu_sel_is_ff, static_cast<uint8_t>(is_ff) },
1541 { C::alu_sel_op_lt, 1 },
1542 { C::alu_tag_ff_diff_inv, is_ff ? 0 : FF(tag - static_cast<uint8_t>(MemoryTag::FF)).invert() },
1543 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
1544 { C::alu_tag_u128_diff_inv,
1545 tag == static_cast<uint8_t>(MemoryTag::U128)
1546 ? 0
1547 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
1548 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
1549 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
1550 { C::execution_mem_tag_reg_2_, static_cast<uint8_t>(MemoryTag::U1) }, // = ic_tag
1551 { C::execution_register_0_, a }, // = ia
1552 { C::execution_register_1_, b }, // = ib
1553 { C::execution_register_2_, c }, // = ic
1554 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
1555 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_LT }, // = alu_op_id
1556 },
1557 });
1558
1559 if (is_ff) {
1560 field_gt_builder.process({ { .a = b, .b = a, .gt_result = c.as_ff() == 1 } }, trace);
1561 } else {
1562 gt_builder.process({ { .a = static_cast<uint128_t>(b.as_ff()),
1563 .b = static_cast<uint128_t>(a.as_ff()),
1564 .result = c.as_ff() == 1 } },
1565 trace);
1566 }
1567
1568 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1569 precomputed_builder.process_tag_parameters(trace);
1570 return trace;
1571 }
1572
1573 TestTraceContainer process_lt_with_tracegen(ThreeOperandTestParams params)
1574 {
1575 TestTraceContainer trace;
1576 auto [a, b, c] = params;
1577 auto is_ff = a.get_tag() == MemoryTag::FF;
1578
1579 builder.process(
1580 {
1581 { .operation = simulation::AluOperation::LT, .a = a, .b = b, .c = c },
1582 },
1583 trace);
1584
1585 if (is_ff) {
1586 field_gt_builder.process({ { .a = b, .b = a, .gt_result = c.as_ff() == 1 } }, trace);
1587 } else {
1588 gt_builder.process({ { .a = static_cast<uint128_t>(b.as_ff()),
1589 .b = static_cast<uint128_t>(a.as_ff()),
1590 .result = c.as_ff() == 1 } },
1591 trace);
1592 }
1593 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1594 precomputed_builder.process_tag_parameters(trace);
1595 return trace;
1596 }
1597};
1598
1599INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluLTConstrainingTest, ::testing::ValuesIn(TEST_VALUES_LT));
1600
1601TEST_P(AluLTConstrainingTest, AluLT)
1602{
1603 auto trace = process_lt_trace(GetParam());
1604 check_all_interactions<AluTraceBuilder>(trace);
1605 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1606 check_relation<alu>(trace);
1607}
1608
1609TEST_P(AluLTConstrainingTest, AluLTTraceGen)
1610{
1611 auto trace = process_lt_with_tracegen(GetParam());
1612 check_all_interactions<AluTraceBuilder>(trace);
1613 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1614 check_relation<alu>(trace);
1615}
1616
1617TEST_P(AluLTConstrainingTest, NegativeAluLT)
1618{
1619 auto params = GetParam();
1620 auto trace = process_lt_trace(params);
1621 auto is_ff = std::get<0>(params).get_tag() == MemoryTag::FF;
1622 check_relation<alu>(trace);
1623 check_all_interactions<AluTraceBuilder>(trace);
1624 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1625 bool c = trace.get(Column::alu_ic, 0) == 1;
1626 // Swap the result bool:
1627 trace.set(Column::alu_ic, 0, static_cast<uint8_t>(!c));
1628 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_GT_ASSIGN_RESULT_C));
1629 trace.set(Column::alu_gt_result_c, 0, static_cast<uint8_t>(!c));
1630
1631 if (is_ff) {
1632 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_ff_gt_settings>(trace)),
1633 "LOOKUP_ALU_FF_GT");
1634 } else {
1635 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_int_gt_settings>(trace)),
1636 "LOOKUP_ALU_INT_GT");
1637 }
1638}
1639
1640// LTE TESTS
1641
1642const std::vector<ThreeOperandTestParams> TEST_VALUES_LTE = zip_helper(TEST_VALUES_LT_OUT);
1643
1644class AluLTEConstrainingTest : public AluConstrainingTest,
1645 public ::testing::WithParamInterface<ThreeOperandTestParams> {
1646 public:
1647 TestTraceContainer process_lte_trace(ThreeOperandTestParams params, bool eq = false)
1648 {
1649 auto [a, b, c] = params;
1650 auto mem_tag = a.get_tag();
1651 auto tag = static_cast<uint8_t>(mem_tag);
1652 auto is_ff = mem_tag == MemoryTag::FF;
1653 b = eq ? a : b;
1654 c = eq ? MemoryValue::from_tag(MemoryTag::U1, 1) : c;
1655
1656 auto trace = TestTraceContainer({
1657 {
1658 { C::alu_ia, a },
1659 { C::alu_ia_tag, tag },
1660 { C::alu_ib, b },
1661 { C::alu_ib_tag, tag },
1662 { C::alu_ic, c },
1663 { C::alu_ic_tag, static_cast<uint8_t>(MemoryTag::U1) },
1664 { C::alu_gt_input_a, a },
1665 { C::alu_gt_input_b, b },
1666 { C::alu_gt_result_c, c.as_ff() == 0 ? 1 : 0 },
1667 { C::alu_max_bits, get_tag_bits(mem_tag) },
1668 { C::alu_max_value, get_tag_max_value(mem_tag) },
1669 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_LTE },
1670 { C::alu_sel, 1 },
1671 { C::alu_sel_ff_gt, static_cast<uint8_t>(is_ff) },
1672 { C::alu_sel_int_gt, static_cast<uint8_t>(!is_ff) },
1673 { C::alu_sel_is_ff, static_cast<uint8_t>(is_ff) },
1674 { C::alu_sel_op_lte, 1 },
1675 { C::alu_tag_ff_diff_inv, is_ff ? 0 : FF(tag - static_cast<uint8_t>(MemoryTag::FF)).invert() },
1676 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
1677 { C::alu_tag_u128_diff_inv,
1678 tag == static_cast<uint8_t>(MemoryTag::U128)
1679 ? 0
1680 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
1681 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
1682 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
1683 { C::execution_mem_tag_reg_2_, static_cast<uint8_t>(MemoryTag::U1) }, // = ic_tag
1684 { C::execution_register_0_, a }, // = ia
1685 { C::execution_register_1_, b }, // = ib
1686 { C::execution_register_2_, c }, // = ic
1687 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
1688 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_LTE }, // = alu_op_id
1689 },
1690 });
1691
1692 if (is_ff) {
1693 field_gt_builder.process({ { .a = a, .b = b, .gt_result = c.as_ff() == 0 } }, trace);
1694 } else {
1695 gt_builder.process({ { .a = static_cast<uint128_t>(a.as_ff()),
1696 .b = static_cast<uint128_t>(b.as_ff()),
1697 .result = c.as_ff() == 0 } },
1698 trace);
1699 }
1700 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1701 precomputed_builder.process_tag_parameters(trace);
1702 return trace;
1703 }
1704
1705 TestTraceContainer process_lte_with_tracegen(ThreeOperandTestParams params, bool eq = false)
1706 {
1707 TestTraceContainer trace;
1708 auto [a, b, c] = params;
1709 auto is_ff = a.get_tag() == MemoryTag::FF;
1710 b = eq ? a : b;
1711 c = eq ? MemoryValue::from_tag(MemoryTag::U1, 1) : c;
1712
1713 builder.process(
1714 {
1715 { .operation = simulation::AluOperation::LTE, .a = a, .b = b, .c = c },
1716 },
1717 trace);
1718
1719 if (is_ff) {
1720 field_gt_builder.process({ { .a = a, .b = b, .gt_result = c.as_ff() == 0 } }, trace);
1721 } else {
1722 gt_builder.process({ { .a = static_cast<uint128_t>(a.as_ff()),
1723 .b = static_cast<uint128_t>(b.as_ff()),
1724 .result = c.as_ff() == 0 } },
1725 trace);
1726 }
1727 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1728 precomputed_builder.process_tag_parameters(trace);
1729 return trace;
1730 }
1731};
1732
1733INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluLTEConstrainingTest, ::testing::ValuesIn(TEST_VALUES_LTE));
1734
1735TEST_P(AluLTEConstrainingTest, AluLTE)
1736{
1737 auto trace = process_lte_trace(GetParam());
1738 check_all_interactions<AluTraceBuilder>(trace);
1739 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1740 check_relation<alu>(trace);
1741}
1742
1743TEST_P(AluLTEConstrainingTest, AluLTEEq)
1744{
1745 auto trace = process_lte_trace(GetParam(), true);
1746 check_all_interactions<AluTraceBuilder>(trace);
1747 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1748 check_relation<alu>(trace);
1749}
1750
1751TEST_P(AluLTEConstrainingTest, AluLTETraceGen)
1752{
1753 auto trace = process_lte_with_tracegen(GetParam());
1754 check_all_interactions<AluTraceBuilder>(trace);
1755 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1756 check_relation<alu>(trace);
1757}
1758
1759TEST_P(AluLTEConstrainingTest, AluLTEEqTraceGen)
1760{
1761 auto trace = process_lte_with_tracegen(GetParam(), true);
1762 check_all_interactions<AluTraceBuilder>(trace);
1763 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1764 check_relation<alu>(trace);
1765}
1766
1767TEST_P(AluLTEConstrainingTest, NegativeAluLTEResult)
1768{
1769 auto params = GetParam();
1770
1771 for (const bool is_eq : { false, true }) {
1772 auto trace = process_lte_trace(params, is_eq);
1773 auto is_ff = std::get<0>(params).get_tag() == MemoryTag::FF;
1774 check_relation<alu>(trace);
1775 check_all_interactions<AluTraceBuilder>(trace);
1776 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1777 bool c = trace.get(Column::alu_ic, 0) == 1;
1778 // Swap the result bool:
1779 trace.set(Column::alu_ic, 0, static_cast<uint8_t>(!c));
1780 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_GT_ASSIGN_RESULT_C));
1781 trace.set(Column::alu_gt_result_c, 0, static_cast<uint8_t>(c));
1782
1783 if (is_ff) {
1784 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_ff_gt_settings>(trace)),
1785 "LOOKUP_ALU_FF_GT");
1786 } else {
1787 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_int_gt_settings>(trace)),
1788 "LOOKUP_ALU_INT_GT");
1789 }
1790 }
1791}
1792
1793TEST_P(AluLTEConstrainingTest, NegativeAluLTEInput)
1794{
1795 auto params = GetParam();
1796
1797 for (const bool is_eq : { false, true }) {
1798 auto trace = process_lte_trace(params, is_eq);
1799 auto is_ff = std::get<0>(params).get_tag() == MemoryTag::FF;
1800 check_relation<alu>(trace);
1801 check_all_interactions<AluTraceBuilder>(trace);
1802 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1803 bool c = trace.get(Column::alu_ic, 0) == 1;
1804 auto a = trace.get(Column::alu_ia, 0);
1805 auto wrong_b = c ? a - 1 : a + 1;
1806 trace.set(Column::alu_ib, 0, wrong_b);
1807 trace.set(Column::alu_gt_input_b, 0, wrong_b);
1808 // We rely on lookups, so we expect the relations to still pass...
1809 check_relation<alu>(trace);
1810
1811 // ... but the lookup will fail (TODO(MW): properly add a gt and => range check events so it fails because c
1812 // is wrong, rather than because this test has not processed the events):
1813 if (is_ff) {
1814 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_ff_gt_settings>(trace)),
1815 "LOOKUP_ALU_FF_GT");
1816 } else {
1817 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_int_gt_settings>(trace)),
1818 "LOOKUP_ALU_INT_GT");
1819 }
1820 }
1821}
1822
1823// NOT Opcode TESTS
1824
1825const std::vector<MemoryValue> TEST_VALUES_NOT_OUT = {
1826 MemoryValue::from_tag(MemoryTag::U1, 0),
1827 MemoryValue::from_tag(MemoryTag::U8, 55),
1828 MemoryValue::from_tag(MemoryTag::U16, 65505),
1829 MemoryValue::from_tag(MemoryTag::U32, 9),
1830 MemoryValue::from_tag(MemoryTag::U64, 9),
1831 MemoryValue::from_tag(MemoryTag::U128, 9),
1832 MemoryValue::from_tag(static_cast<MemoryTag>(0), 0), // For FF, b is the default value of 0 with tag 0
1833};
1834
1835const std::vector<TwoOperandTestParams> TEST_VALUES_NOT = zip_helper_two_op(TEST_VALUES_NOT_OUT);
1836
1837class AluNotConstrainingTest : public AluConstrainingTest, public ::testing::WithParamInterface<TwoOperandTestParams> {
1838 public:
1839 TestTraceContainer process_not_with_tracegen(const TwoOperandTestParams& params, bool error = false)
1840 {
1841 TestTraceContainer trace;
1842 auto [a, b] = params;
1843 auto is_ff = a.get_tag() == MemoryTag::FF;
1844
1845 builder.process(
1846 {
1847 { .operation = simulation::AluOperation::NOT, .a = a, .b = b, .error = error || is_ff },
1848 },
1849 trace);
1850
1851 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
1852 precomputed_builder.process_tag_parameters(trace);
1853 return trace;
1854 }
1855};
1856
1857INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluNotConstrainingTest, ::testing::ValuesIn(TEST_VALUES_NOT));
1858
1859TEST_P(AluNotConstrainingTest, AluNotTraceGen)
1860{
1861 auto trace = process_not_with_tracegen(GetParam());
1862 check_all_interactions<AluTraceBuilder>(trace);
1863 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1864 check_relation<alu>(trace);
1865}
1866
1867TEST_P(AluNotConstrainingTest, NegativeAluNotTraceGen)
1868{
1869 auto params = GetParam();
1870 auto trace = process_not_with_tracegen(params);
1871 check_all_interactions<AluTraceBuilder>(trace);
1872 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1873 check_relation<alu>(trace);
1874 trace.set(Column::alu_ib, 0, trace.get(Column::alu_ib, 0) + 1); // Mutate output
1875 // The FF case <==> tag_err for NOT, so NOT_OP_MAIN is gated:
1876 if (std::get<0>(params).get_tag() != MemoryTag::FF) {
1877 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_NOT_OP_MAIN));
1878 }
1879}
1880
1881// Unconditional check for AB_TAGS_CHECK error for NOT opcode. This cannot satsify the constraints.
1882TEST_P(AluNotConstrainingTest, AluNotTraceGenTagError)
1883{
1884 auto [a, b] = GetParam();
1885 auto trace = process_not_with_tracegen(
1886 TwoOperandTestParams{ a, MemoryValue::from_tag(TAG_ERROR_TEST_VALUES.at(b.get_tag()), b.as_ff()) }, true);
1887 check_all_interactions<AluTraceBuilder>(trace);
1888 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1889 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace),
1890 alu::get_subrelation_label(alu::SR_ONLY_RELEVANT_CHECK_AB_TAGS_ERROR));
1891}
1892
1893// Supported TAG error when a is of FF type.
1894TEST_F(AluNotConstrainingTest, AluNotTraceGenTagErrorFF)
1895{
1896 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
1897 auto b = MemoryValue::from_tag(MemoryTag::FF, 253);
1898 auto trace = process_not_with_tracegen(TwoOperandTestParams{ a, b }, true);
1899 check_all_interactions<AluTraceBuilder>(trace);
1900 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
1901 check_relation<alu>(trace);
1902}
1903
1904// SHL TESTS
1905
1906const std::vector<MemoryValue> TEST_VALUES_SHL_OUT = {
1907 MemoryValue::from_tag(MemoryTag::U1, 1),
1908 MemoryValue::from_tag(MemoryTag::U8, 0),
1909 MemoryValue::from_tag(MemoryTag::U16, 0),
1910 MemoryValue::from_tag(MemoryTag::U32, 0xfffffec0),
1911 MemoryValue::from_tag(MemoryTag::U64, 0xfffffffffffffec0ULL),
1912 MemoryValue::from_tag(MemoryTag::U128, (uint256_t(1) << 128) - 320), // 0xfffffffffffffffffffffffffffffec0
1913};
1914
1915const std::vector<ThreeOperandTestParams> TEST_VALUES_SHL = zip_helper(TEST_VALUES_SHL_OUT);
1916
1917class AluShlConstrainingTest : public AluConstrainingTest,
1918 public ::testing::WithParamInterface<ThreeOperandTestParams> {
1919 public:
1920 TestTraceContainer process_shl_trace(ThreeOperandTestParams params)
1921 {
1922 auto [a, b, c] = params;
1923
1924 auto mem_tag = a.get_tag();
1925 auto tag = static_cast<uint8_t>(mem_tag);
1926 auto tag_bits = get_tag_bits(mem_tag);
1927 auto a_num = static_cast<uint128_t>(a.as_ff());
1928 auto b_num = static_cast<uint128_t>(b.as_ff());
1929
1930 auto overflow = b_num > tag_bits;
1931 uint128_t shift_lo_bits = overflow ? tag_bits : tag_bits - b_num;
1932 uint128_t shift_hi_bits = overflow ? tag_bits : b_num;
1933 auto two_pow_shift_lo_bits = static_cast<uint128_t>(1) << shift_lo_bits;
1934 auto a_lo = overflow ? b_num - tag_bits : a_num % two_pow_shift_lo_bits;
1935 auto a_hi = a_num >> shift_lo_bits;
1936
1937 auto trace = TestTraceContainer({
1938 {
1939 { C::alu_a_hi, a_hi },
1940 { C::alu_a_hi_bits, shift_hi_bits },
1941 { C::alu_a_lo, a_lo },
1942 { C::alu_a_lo_bits, shift_lo_bits },
1943 { C::alu_helper1, static_cast<uint128_t>(1) << b_num },
1944 { C::alu_ia, a },
1945 { C::alu_ia_tag, tag },
1946 { C::alu_ib, b },
1947 { C::alu_ib_tag, tag },
1948 { C::alu_ic, c },
1949 { C::alu_ic_tag, tag },
1950 { C::alu_max_bits, tag_bits },
1951 { C::alu_max_value, get_tag_max_value(mem_tag) },
1952 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_SHL },
1953 { C::alu_sel, 1 },
1954 { C::alu_sel_decompose_a, 1 },
1955 { C::alu_sel_op_shl, 1 },
1956 { C::alu_sel_shift_ops_no_overflow, overflow ? 0 : 1 },
1957 { C::alu_shift_lo_bits, shift_lo_bits },
1958 { C::alu_tag_ff_diff_inv, FF(tag - static_cast<uint8_t>(MemoryTag::FF)).invert() },
1959 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
1960 { C::alu_tag_u128_diff_inv,
1961 tag == static_cast<uint8_t>(MemoryTag::U128)
1962 ? 0
1963 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
1964 { C::alu_two_pow_shift_lo_bits, two_pow_shift_lo_bits },
1965 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
1966 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
1967 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
1968 { C::execution_register_0_, a }, // = ia
1969 { C::execution_register_1_, b }, // = ib
1970 { C::execution_register_2_, c }, // = ic
1971 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
1972 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_SHL }, // = alu_op_id
1973
1974 },
1975 });
1976
1977 precomputed_builder.process_misc(trace, std::max(NUM_OF_TAGS, static_cast<uint8_t>(shift_lo_bits + 1)));
1978 precomputed_builder.process_tag_parameters(trace);
1979 precomputed_builder.process_power_of_2(trace);
1980 range_check_builder.process({ { .value = a_lo, .num_bits = static_cast<uint8_t>(shift_lo_bits) },
1981 { .value = a_hi, .num_bits = static_cast<uint8_t>(shift_hi_bits) } },
1982 trace);
1983
1984 return trace;
1985 }
1986
1987 TestTraceContainer process_shl_with_tracegen(ThreeOperandTestParams params, bool error = false)
1988 {
1989 TestTraceContainer trace;
1990 auto [a, b, c] = params;
1991 auto b_num = static_cast<uint128_t>(b.as_ff());
1992 auto tag_bits = get_tag_bits(a.get_tag());
1993 auto overflow = b_num > tag_bits;
1994 uint128_t shift_lo_bits = overflow ? tag_bits : tag_bits - b_num;
1995 auto a_lo = overflow ? b_num - tag_bits
1996 : static_cast<uint128_t>(a.as_ff()) % (static_cast<uint128_t>(1) << shift_lo_bits);
1997
1998 builder.process(
1999 {
2000 { .operation = simulation::AluOperation::SHL, .a = a, .b = b, .c = c, .error = error },
2001 },
2002 trace);
2003
2004 precomputed_builder.process_misc(trace, std::max(NUM_OF_TAGS, static_cast<uint8_t>(shift_lo_bits + 1)));
2005 precomputed_builder.process_tag_parameters(trace);
2006 precomputed_builder.process_power_of_2(trace);
2007 range_check_builder.process({ { .value = a_lo, .num_bits = static_cast<uint8_t>(shift_lo_bits) },
2008 { .value = static_cast<uint128_t>(a.as_ff()) >> shift_lo_bits,
2009 .num_bits = static_cast<uint8_t>(overflow ? tag_bits : b_num) } },
2010 trace);
2011 return trace;
2012 }
2013};
2014
2015INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluShlConstrainingTest, ::testing::ValuesIn(TEST_VALUES_SHL));
2016
2017TEST_P(AluShlConstrainingTest, AluShl)
2018{
2019 auto trace = process_shl_trace(GetParam());
2020 check_all_interactions<AluTraceBuilder>(trace);
2021 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
2022 check_relation<alu>(trace);
2023}
2024
2025TEST_P(AluShlConstrainingTest, AluShlTraceGen)
2026{
2027 auto trace = process_shl_with_tracegen(GetParam());
2028 check_all_interactions<AluTraceBuilder>(trace);
2029 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
2030 check_relation<alu>(trace);
2031}
2032
2033TEST_F(AluShlConstrainingTest, NegativeAluShlFF)
2034{
2035 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
2036 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
2037 auto c = MemoryValue::from_tag(MemoryTag::FF, 2 << 5);
2038 auto trace = process_shl_with_tracegen({ a, b, c }, true);
2039 check_relation<alu>(trace);
2040 check_all_interactions<AluTraceBuilder>(trace);
2041
2042 // Check the edge case of FF tag (=> max_bits = 0) and b = 0:
2043 trace.set(Column::alu_ib, 0, 0);
2044 check_relation<alu>(trace);
2045 check_all_interactions<AluTraceBuilder>(trace);
2046
2047 // Disable tag and error selectors:
2048 trace.set(Column::alu_sel_tag_err, 0, 0);
2049 trace.set(Column::alu_sel_err, 0, 0);
2050 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
2051}
2052
2053TEST_F(AluShlConstrainingTest, NegativeAluShlTagMismatchOverflow)
2054{
2055 auto a = MemoryValue::from_tag(MemoryTag::U8, 2);
2056 auto b = MemoryValue::from_tag(MemoryTag::U32, 256);
2057 auto c = MemoryValue::from_tag(MemoryTag::U8, 0);
2058 auto trace = process_shl_with_tracegen({ a, b, c }, true);
2059 check_relation<alu>(trace);
2060 check_all_interactions<AluTraceBuilder>(trace);
2061
2062 // Disable tag and error selectors:
2063 trace.set(Column::alu_sel_tag_err, 0, 0);
2064 trace.set(Column::alu_sel_err, 0, 0);
2065 // Disable ab tag mismatch error:
2066 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 0);
2067 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
2068
2069 // Second attempt with setting the ab tags diff inverse to zero:
2070 trace.set(Column::alu_ab_tags_diff_inv, 0, 0);
2071 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
2072
2073 // Reset only ab tag diff related columns:
2074 trace.set(Column::alu_ab_tags_diff_inv,
2075 0,
2076 (FF(static_cast<uint8_t>(MemoryTag::U8)) - FF(static_cast<uint8_t>(MemoryTag::U32))).invert());
2077 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 1);
2078 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
2079}
2080
2081// SHR TESTS
2082
2083const std::vector<MemoryValue> TEST_VALUES_SHR_OUT = {
2084 MemoryValue::from_tag(MemoryTag::U1, 1),
2085 MemoryValue::from_tag(MemoryTag::U8, 0),
2086 MemoryValue::from_tag(MemoryTag::U16, 0),
2087 MemoryValue::from_tag(MemoryTag::U32, 0x7ffffff),
2088 MemoryValue::from_tag(MemoryTag::U64, 0x7ffffffffffffffULL),
2089 MemoryValue::from_tag(MemoryTag::U128,
2090 (uint256_t(1) << 128) - 1 - (uint256_t(248) << 120)), // 0x7ffffffffffffffffffffffffffffff
2091};
2092
2093const std::vector<ThreeOperandTestParams> TEST_VALUES_SHR = zip_helper(TEST_VALUES_SHR_OUT);
2094
2095class AluShrConstrainingTest : public AluConstrainingTest,
2096 public ::testing::WithParamInterface<ThreeOperandTestParams> {
2097 public:
2098 TestTraceContainer process_shr_trace(ThreeOperandTestParams params)
2099 {
2100 auto [a, b, c] = params;
2101
2102 auto mem_tag = a.get_tag();
2103 auto tag = static_cast<uint8_t>(mem_tag);
2104 auto tag_bits = get_tag_bits(mem_tag);
2105 auto a_num = static_cast<uint128_t>(a.as_ff());
2106 auto b_num = static_cast<uint128_t>(b.as_ff());
2107
2108 auto overflow = b_num > tag_bits;
2109 uint128_t shift_lo_bits = overflow ? tag_bits : b_num;
2110 uint128_t shift_hi_bits = overflow ? tag_bits : tag_bits - b_num;
2111 auto two_pow_shift_lo_bits = static_cast<uint128_t>(1) << shift_lo_bits;
2112 auto a_lo = overflow ? b_num - tag_bits : a_num % two_pow_shift_lo_bits;
2113 auto a_hi = a_num >> shift_lo_bits;
2114
2115 auto trace = TestTraceContainer({
2116 {
2117 { C::alu_a_hi, a_hi },
2118 { C::alu_a_hi_bits, shift_hi_bits },
2119 { C::alu_a_lo, a_lo },
2120 { C::alu_a_lo_bits, shift_lo_bits },
2121 { C::alu_ia, a },
2122 { C::alu_ia_tag, tag },
2123 { C::alu_ib, b },
2124 { C::alu_ib_tag, tag },
2125 { C::alu_ic, c },
2126 { C::alu_ic_tag, tag },
2127 { C::alu_max_bits, tag_bits },
2128 { C::alu_max_value, get_tag_max_value(mem_tag) },
2129 { C::alu_op_id, AVM_EXEC_OP_ID_ALU_SHR },
2130 { C::alu_sel, 1 },
2131 { C::alu_sel_decompose_a, 1 },
2132 { C::alu_sel_op_shr, 1 },
2133 { C::alu_sel_shift_ops_no_overflow, overflow ? 0 : 1 },
2134 { C::alu_shift_lo_bits, shift_lo_bits },
2135 { C::alu_tag_ff_diff_inv, FF(tag - static_cast<uint8_t>(MemoryTag::FF)).invert() },
2136 { C::alu_sel_is_u128, tag == static_cast<uint8_t>(MemoryTag::U128) ? 1 : 0 },
2137 { C::alu_tag_u128_diff_inv,
2138 tag == static_cast<uint8_t>(MemoryTag::U128)
2139 ? 0
2140 : FF(tag - static_cast<uint8_t>(MemoryTag::U128)).invert() },
2141 { C::alu_two_pow_shift_lo_bits, two_pow_shift_lo_bits },
2142 { C::execution_mem_tag_reg_0_, tag }, // = ia_tag
2143 { C::execution_mem_tag_reg_1_, tag }, // = ib_tag
2144 { C::execution_mem_tag_reg_2_, tag }, // = ic_tag
2145 { C::execution_register_0_, a }, // = ia
2146 { C::execution_register_1_, b }, // = ib
2147 { C::execution_register_2_, c }, // = ic
2148 { C::execution_sel_exec_dispatch_alu, 1 }, // = sel
2149 { C::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_SHR }, // = alu_op_id
2150
2151 },
2152 });
2153
2154 precomputed_builder.process_misc(trace, std::max(NUM_OF_TAGS, static_cast<uint8_t>(shift_lo_bits + 1)));
2155 precomputed_builder.process_tag_parameters(trace);
2156 precomputed_builder.process_power_of_2(trace);
2157 range_check_builder.process({ { .value = a_lo, .num_bits = static_cast<uint8_t>(shift_lo_bits) },
2158 { .value = a_hi, .num_bits = static_cast<uint8_t>(shift_hi_bits) } },
2159 trace);
2160
2161 return trace;
2162 }
2163
2164 TestTraceContainer process_shr_with_tracegen(ThreeOperandTestParams params, bool error = false)
2165 {
2166 TestTraceContainer trace;
2167 auto [a, b, c] = params;
2168 auto b_num = static_cast<uint128_t>(b.as_ff());
2169 auto tag_bits = get_tag_bits(a.get_tag());
2170 auto overflow = b_num > tag_bits;
2171 uint128_t shift_lo_bits = overflow ? tag_bits : b_num;
2172 auto a_lo = overflow ? b_num - tag_bits
2173 : static_cast<uint128_t>(a.as_ff()) % (static_cast<uint128_t>(1) << shift_lo_bits);
2174
2175 builder.process(
2176 {
2177 { .operation = simulation::AluOperation::SHR, .a = a, .b = b, .c = c, .error = error },
2178 },
2179 trace);
2180
2181 precomputed_builder.process_misc(trace, std::max(NUM_OF_TAGS, static_cast<uint8_t>(shift_lo_bits + 1)));
2182 precomputed_builder.process_tag_parameters(trace);
2183 precomputed_builder.process_power_of_2(trace);
2184 range_check_builder.process({ { .value = a_lo, .num_bits = static_cast<uint8_t>(shift_lo_bits) },
2185 { .value = static_cast<uint128_t>(a.as_ff()) >> shift_lo_bits,
2186 .num_bits = static_cast<uint8_t>(overflow ? tag_bits : tag_bits - b_num) } },
2187 trace);
2188 return trace;
2189 }
2190};
2191
2192INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluShrConstrainingTest, ::testing::ValuesIn(TEST_VALUES_SHR));
2193
2194TEST_P(AluShrConstrainingTest, AluShr)
2195{
2196 auto trace = process_shr_trace(GetParam());
2197 check_all_interactions<AluTraceBuilder>(trace);
2198 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
2199 check_relation<alu>(trace);
2200}
2201
2202TEST_P(AluShrConstrainingTest, AluShrTraceGen)
2203{
2204 auto trace = process_shr_with_tracegen(GetParam());
2205 check_all_interactions<AluTraceBuilder>(trace);
2206 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_alu_settings>(trace);
2207 check_relation<alu>(trace);
2208}
2209
2210TEST_F(AluShrConstrainingTest, NegativeAluShrFF)
2211{
2212 auto a = MemoryValue::from_tag(MemoryTag::FF, 2);
2213 auto b = MemoryValue::from_tag(MemoryTag::FF, 5);
2214 auto c = MemoryValue::from_tag(MemoryTag::FF, 2 << 5);
2215 auto trace = process_shr_with_tracegen({ a, b, c }, true);
2216 check_relation<alu>(trace);
2217 check_all_interactions<AluTraceBuilder>(trace);
2218
2219 // Check the edge case of FF tag (=> max_bits = 0) and b = 0:
2220 trace.set(Column::alu_ib, 0, 0);
2221 check_relation<alu>(trace);
2222 check_all_interactions<AluTraceBuilder>(trace);
2223
2224 // Disable tag and error selectors:
2225 trace.set(Column::alu_sel_tag_err, 0, 0);
2226 trace.set(Column::alu_sel_err, 0, 0);
2227 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
2228}
2229
2230TEST_F(AluShrConstrainingTest, NegativeAluShrTagMismatchOverflow)
2231{
2232 auto a = MemoryValue::from_tag(MemoryTag::U16, 2);
2233 auto b = MemoryValue::from_tag(MemoryTag::U64, 123456);
2234 auto c = MemoryValue::from_tag(MemoryTag::U16, 0);
2235 auto trace = process_shr_with_tracegen({ a, b, c }, true);
2236 check_relation<alu>(trace);
2237 check_all_interactions<AluTraceBuilder>(trace);
2238 // Disable tag and error selectors:
2239 trace.set(Column::alu_sel_tag_err, 0, 0);
2240 trace.set(Column::alu_sel_err, 0, 0);
2241 // Disable ab tag mismatch error:
2242 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 0);
2243 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
2244
2245 // Second attempt with setting the ab tags diff inverse to zero:
2246 trace.set(Column::alu_ab_tags_diff_inv, 0, 0);
2247 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_AB_TAGS_CHECK));
2248
2249 // Reset only ab tag diff related columns:
2250 trace.set(Column::alu_ab_tags_diff_inv,
2251 0,
2252 (FF(static_cast<uint8_t>(MemoryTag::U16)) - FF(static_cast<uint8_t>(MemoryTag::U64))).invert());
2253 trace.set(Column::alu_sel_ab_tag_mismatch, 0, 1);
2254 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TAG_ERR_CHECK));
2255}
2256
2257// TRUNCATE operation (SET/CAST opcodes)
2258
2259// Truncation is a special case as we always have FF MemoryValue inputs:
2260const std::vector<ThreeOperandTestParams> TEST_VALUES_TRUNCATE = {
2261 // Trivial truncation cases
2262 { MemoryValue::from_tag(MemoryTag::FF, 1),
2263 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U1)),
2264 MemoryValue::from_tag(MemoryTag::U1, 1) },
2265 { MemoryValue::from_tag(MemoryTag::FF, 42),
2266 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U8)),
2267 MemoryValue::from_tag(MemoryTag::U8, 42) },
2268 { MemoryValue::from_tag(MemoryTag::FF, 12345),
2269 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U16)),
2270 MemoryValue::from_tag(MemoryTag::U16, 12345) },
2271 { MemoryValue::from_tag(MemoryTag::FF, 123456789),
2272 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2273 MemoryValue::from_tag(MemoryTag::U32, 123456789) },
2274 { MemoryValue::from_tag(MemoryTag::FF, 1234567890123456789ULL),
2275 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U64)),
2276 MemoryValue::from_tag(MemoryTag::U64, 1234567890123456789ULL) },
2277 { MemoryValue::from_tag(MemoryTag::FF, (uint256_t(1) << 127) + 23423429816234ULL),
2278 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U128)),
2279 MemoryValue::from_tag(MemoryTag::U128, (uint256_t(1) << 127) + 23423429816234ULL) },
2280 { MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 3),
2281 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::FF)),
2282 MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 3) },
2283 // Truncation cases (< 128 bits)
2284 { MemoryValue::from_tag(MemoryTag::FF, 212),
2285 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U1)),
2286 MemoryValue::from_tag(MemoryTag::U1, 0) },
2287 { MemoryValue::from_tag(MemoryTag::FF, 257),
2288 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U8)),
2289 MemoryValue::from_tag(MemoryTag::U8, 1) },
2290 { MemoryValue::from_tag(MemoryTag::FF, 65540),
2291 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U16)),
2292 MemoryValue::from_tag(MemoryTag::U16, 4) },
2293 { MemoryValue::from_tag(MemoryTag::FF, 4294967298ULL),
2294 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2295 MemoryValue::from_tag(MemoryTag::U32, 2) },
2296 { MemoryValue::from_tag(MemoryTag::FF, 18446744073709551615ULL + 4),
2297 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U64)),
2298 MemoryValue::from_tag(MemoryTag::U64, 3) },
2299 // Truncation cases (>= 128 bits)
2300 { MemoryValue::from_tag(MemoryTag::FF, (uint256_t(134534) << 129) + 986132),
2301 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U1)),
2302 MemoryValue::from_tag(MemoryTag::U1, 0) },
2303 { MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 128735618772ULL),
2304 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U8)),
2305 MemoryValue::from_tag(MemoryTag::U8, 45) },
2306 { MemoryValue::from_tag(MemoryTag::FF, (uint256_t(999) << 128) - 986132ULL),
2307 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U16)),
2308 MemoryValue::from_tag(MemoryTag::U16, 62444) },
2309 { MemoryValue::from_tag(MemoryTag::FF, (uint256_t(134534) << 198) + 986132ULL),
2310 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2311 MemoryValue::from_tag(MemoryTag::U32, 986132ULL) },
2312 { MemoryValue::from_tag(MemoryTag::FF, (uint256_t(134534) << 198) - 986132ULL),
2313 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U64)),
2314 MemoryValue::from_tag(MemoryTag::U64, static_cast<uint64_t>(-986132ULL)) },
2315 { MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 8723),
2316 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U128)),
2317 MemoryValue::from_tag(MemoryTag::U128, static_cast<uint128_t>(FF::modulus - 8723)) },
2318};
2319
2320class AluTruncateConstrainingTest : public AluConstrainingTest,
2321 public ::testing::WithParamInterface<ThreeOperandTestParams> {
2322 public:
2323 TestTraceContainer process_truncate_with_tracegen(const ThreeOperandTestParams& params, TestTraceContainer& trace)
2324 {
2325 auto [a, b, c] = params;
2326
2327 builder.process(
2328 {
2329 { .operation = simulation::AluOperation::TRUNCATE, .a = a, .b = b, .c = c },
2330 },
2331 trace);
2332
2333 precomputed_builder.process_misc(trace, NUM_OF_TAGS);
2334 precomputed_builder.process_tag_parameters(trace);
2335
2336 auto is_non_trivial = trace.get(Column::alu_sel_trunc_non_trivial, 0) == 1;
2337
2338 if (is_non_trivial) {
2339 auto a_decomp = simulation::decompose_256(static_cast<uint256_t>(a.as_ff()));
2340 auto dst_tag = c.get_tag();
2341 uint8_t bits = get_tag_bits(dst_tag);
2342 range_check_builder.process({ { .value = dst_tag == MemoryTag::U128 ? 0 : a_decomp.lo >> bits,
2343 .num_bits = static_cast<uint8_t>(128 - bits) } },
2344 trace);
2345 auto is_gte_128 = trace.get(Column::alu_sel_trunc_gte_128, 0) == 1;
2346 if (is_gte_128) {
2347 auto p_limbs = simulation::decompose_256(FF::modulus);
2348 simulation::LimbsComparisonWitness p_sub_a_witness = { .lo = p_limbs.lo - a_decomp.lo,
2349 .hi = p_limbs.hi - a_decomp.hi,
2350 .borrow = false };
2351 field_gt_builder.process({ { .operation = simulation::FieldGreaterOperation::CANONICAL_DECOMPOSITION,
2352 .a = a,
2353 .a_limbs = a_decomp,
2354 .p_sub_a_witness = p_sub_a_witness } },
2355 trace);
2356 }
2357 }
2358
2359 return trace;
2360 }
2361
2362 TestTraceContainer process_set_with_tracegen(const ThreeOperandTestParams& params)
2363 {
2364 TestTraceContainer trace;
2365 auto [a, b, _c] = params;
2366 auto dst_tag = static_cast<MemoryTag>(static_cast<uint8_t>(b.as_ff()));
2367 auto c = MemoryValue::from_tag_truncating(dst_tag, a);
2368 trace.set(0,
2369 { {
2370 { Column::execution_sel_exec_dispatch_set, 1 },
2371 { Column::execution_rop_2_, a },
2372 { Column::execution_rop_1_, static_cast<uint8_t>(dst_tag) },
2373 { Column::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_TRUNCATE },
2374 { Column::execution_register_0_, c.as_ff() },
2375 { Column::execution_mem_tag_reg_0_, static_cast<uint8_t>(dst_tag) },
2376 } });
2377
2378 process_truncate_with_tracegen(params, trace);
2379
2380 return trace;
2381 }
2382
2383 TestTraceContainer process_cast_with_tracegen(const ThreeOperandTestParams& params)
2384 {
2385 TestTraceContainer trace;
2386 auto [a, b, _c] = params;
2387 auto dst_tag = static_cast<MemoryTag>(static_cast<uint8_t>(b.as_ff()));
2388 auto c = MemoryValue::from_tag_truncating(dst_tag, a);
2389 trace.set(0,
2390 { {
2391 { Column::execution_sel_exec_dispatch_cast, 1 },
2392 { Column::execution_register_0_, a },
2393 { Column::execution_rop_2_, static_cast<uint8_t>(dst_tag) },
2394 { Column::execution_subtrace_operation_id, AVM_EXEC_OP_ID_ALU_TRUNCATE },
2395 { Column::execution_register_1_, c.as_ff() },
2396 { Column::execution_mem_tag_reg_1_, static_cast<uint8_t>(dst_tag) },
2397 } });
2398
2399 process_truncate_with_tracegen(params, trace);
2400
2401 return trace;
2402 }
2403};
2404
2405INSTANTIATE_TEST_SUITE_P(AluConstrainingTest, AluTruncateConstrainingTest, ::testing::ValuesIn(TEST_VALUES_TRUNCATE));
2406
2407TEST_P(AluTruncateConstrainingTest, AluSet)
2408{
2409 auto trace = process_set_with_tracegen(GetParam());
2410 check_all_interactions<AluTraceBuilder>(trace);
2411 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace);
2412 check_relation<alu>(trace);
2413}
2414
2415TEST_P(AluTruncateConstrainingTest, AluCast)
2416{
2417 auto trace = process_cast_with_tracegen(GetParam());
2418 check_all_interactions<AluTraceBuilder>(trace);
2419 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace);
2420 check_relation<alu>(trace);
2421}
2422
2423TEST_P(AluTruncateConstrainingTest, NegativeTruncateWrongTrivialCase)
2424{
2425 TestTraceContainer trace;
2426 process_truncate_with_tracegen(GetParam(), trace);
2427 check_relation<alu>(trace);
2428 bool is_trivial = trace.get(Column::alu_sel_trunc_trivial, 0) == 1;
2429 trace.set(Column::alu_sel_trunc_trivial, 0, static_cast<uint8_t>(!is_trivial));
2430 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_SEL_TRUNCATE));
2431 trace.set(Column::alu_sel_trunc_trivial, 0, static_cast<uint8_t>(is_trivial));
2432 trace.set(Column::alu_sel_trunc_non_trivial, 0, static_cast<uint8_t>(is_trivial));
2433 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_SEL_TRUNC_NON_TRIVIAL));
2434}
2435
2436TEST_P(AluTruncateConstrainingTest, NegativeTruncateWrong128BitsCase)
2437{
2438 TestTraceContainer trace;
2439 process_truncate_with_tracegen(GetParam(), trace);
2440 check_relation<alu>(trace);
2441 bool is_lt_128 = trace.get(Column::alu_sel_trunc_lt_128, 0) == 1;
2442 trace.set(Column::alu_sel_trunc_lt_128, 0, static_cast<uint8_t>(!is_lt_128));
2443 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_SEL_TRUNC_NON_TRIVIAL));
2444 trace.set(Column::alu_sel_trunc_lt_128, 0, static_cast<uint8_t>(is_lt_128));
2445 check_relation<alu>(trace);
2446 bool is_gte_128 = trace.get(Column::alu_sel_trunc_gte_128, 0) == 1;
2447 trace.set(Column::alu_sel_trunc_gte_128, 0, static_cast<uint8_t>(!is_gte_128));
2448 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_SEL_TRUNC_NON_TRIVIAL));
2449}
2450
2451TEST_F(AluTruncateConstrainingTest, NegativeTruncateWrongMid)
2452{
2453 TestTraceContainer trace;
2454 process_truncate_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, 4294967298ULL),
2455 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2456 MemoryValue::from_tag(MemoryTag::U32, 2) },
2457 trace);
2458 check_relation<alu>(trace);
2459 trace.set(Column::alu_mid, 0, 1234ULL);
2460 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace),
2461 alu::get_subrelation_label(alu::SR_TRUNC_LO_128_DECOMPOSITION));
2462}
2463
2464TEST_F(AluTruncateConstrainingTest, NegativeTruncateWrongMidBits)
2465{
2466 TestTraceContainer trace;
2467 process_truncate_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, FF::modulus - 2),
2468 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U1)),
2469 MemoryValue::from_tag(MemoryTag::U1, 1) },
2470 trace);
2471 check_relation<alu>(trace);
2472 trace.set(Column::alu_mid_bits, 0, 32);
2473 EXPECT_THROW_WITH_MESSAGE(check_relation<alu>(trace), alu::get_subrelation_label(alu::SR_TRUNC_MID_BITS));
2474}
2475
2476TEST_F(AluTruncateConstrainingTest, NegativeTruncateWrongLo128FromCanonDec)
2477{
2478 TestTraceContainer trace;
2479 process_truncate_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, (uint256_t(134534) << 198) - 986132ULL),
2480 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U64)),
2481 MemoryValue::from_tag(MemoryTag::U64, static_cast<uint64_t>(-986132ULL)) },
2482 trace);
2483 check_relation<alu>(trace);
2484 check_all_interactions<AluTraceBuilder>(trace);
2485 trace.set(Column::alu_a_lo, 0, 1234ULL);
2487 (check_interaction<AluTraceBuilder, lookup_alu_large_trunc_canonical_dec_settings>(trace)),
2488 "Failed.*LARGE_TRUNC_CANONICAL_DEC. Could not find tuple in destination.");
2489}
2490
2491TEST_F(AluTruncateConstrainingTest, NegativeTruncateWrongMidIntoRangeCheck)
2492{
2493 TestTraceContainer trace;
2494 process_truncate_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, (uint256_t(134534) << 198) - 986132ULL),
2495 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U64)),
2496 MemoryValue::from_tag(MemoryTag::U64, static_cast<uint64_t>(-986132ULL)) },
2497 trace);
2498 check_relation<alu>(trace);
2499 check_all_interactions<AluTraceBuilder>(trace);
2500 trace.set(Column::alu_mid, 0, 1234ULL);
2501 EXPECT_THROW_WITH_MESSAGE((check_interaction<AluTraceBuilder, lookup_alu_range_check_trunc_mid_settings>(trace)),
2502 "Failed.*RANGE_CHECK_TRUNC_MID. Could not find tuple in destination.");
2503}
2504
2505TEST_F(AluTruncateConstrainingTest, NegativeCastWrongDispatching)
2506{
2507 auto trace =
2508 process_cast_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, 4294967298ULL),
2509 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2510 MemoryValue::from_tag(MemoryTag::U32, 2) });
2511 check_relation<alu>(trace);
2512 check_all_interactions<AluTraceBuilder>(trace);
2513 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_cast_settings>(trace);
2514 trace.set(Column::execution_register_0_, 0, trace.get(Column::execution_register_0_, 0) + 1);
2516 (check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_cast_settings>(trace)),
2517 "Failed.*EXECUTION_DISPATCH_TO_CAST. Could not find tuple in destination.");
2518}
2519
2520TEST_F(AluTruncateConstrainingTest, NegativeSetWrongDispatching)
2521{
2522 auto trace = process_set_with_tracegen({ MemoryValue::from_tag(MemoryTag::FF, 4294967298ULL),
2523 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::U32)),
2524 MemoryValue::from_tag(MemoryTag::U32, 2) });
2525 check_relation<alu>(trace);
2526 check_all_interactions<AluTraceBuilder>(trace);
2527 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace);
2528 trace.set(Column::execution_rop_2_, 0, trace.get(Column::execution_rop_2_, 0) + 1);
2530 (check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace)),
2531 "Failed.*EXECUTION_DISPATCH_TO_SET. Could not find tuple in destination.");
2532}
2533
2534// Demonstrates that a malicious prover can silently replace a field element with its lower 128 bits
2535// when performing SET_FF with a value >= 2^128. The honest trace uses sel_trunc_trivial (since any FF
2536// value is <= p-1 = max_value for FF). The exploit switches to sel_trunc_gte_128, which decomposes
2537// ia into a_lo (128 bits) + 2^128 * a_hi via ff_gt.sel_dec. The decomposition constraint
2538// ic + mid * (max_value + 1) = a_lo degenerates because max_value + 1 = p = 0 in the field,
2539// forcing ic = a_lo (the lower 128 bits only). All relations and lookups pass.
2540TEST_F(AluTruncateConstrainingTest, ExploitSetFFTruncationTo128Bits)
2541{
2542 // Use p - 1 as the test value. It is >= 2^128 and its lower 128 bits differ from itself.
2543 const FF large_value = FF::modulus - 1;
2544 const uint256_t large_value_u256 = static_cast<uint256_t>(large_value);
2545 const auto a_decomp = simulation::decompose_256(large_value_u256);
2546 // Sanity: value is indeed >= 2^128 and truncation would lose data.
2547 ASSERT_NE(a_decomp.hi, 0);
2548 const FF a_lo_ff = FF(uint256_t(a_decomp.lo));
2549 ASSERT_NE(a_lo_ff, large_value); // a_lo != ia: the exploit changes the output
2550
2551 // ---------------------------------------------------------------
2552 // Step 1: Generate the honest trace for SET_FF with this value.
2553 // ---------------------------------------------------------------
2554 const auto params = ThreeOperandTestParams{
2555 MemoryValue::from_tag(MemoryTag::FF, large_value_u256),
2556 MemoryValue::from_tag(MemoryTag::FF, static_cast<uint8_t>(MemoryTag::FF)),
2557 MemoryValue::from_tag(MemoryTag::FF, large_value_u256),
2558 };
2559 auto trace = process_set_with_tracegen(params);
2560
2561 // Verify the honest trace: trivial path, ic == ia == large_value.
2562 EXPECT_EQ(trace.get(C::alu_sel_trunc_trivial, 0), 1);
2563 EXPECT_EQ(trace.get(C::alu_sel_trunc_gte_128, 0), 0);
2564 EXPECT_EQ(trace.get(C::alu_ic, 0), large_value);
2565
2566 // The honest trace passes all checks.
2567 check_relation<alu>(trace);
2568 check_all_interactions<AluTraceBuilder>(trace);
2569 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace);
2570
2571 // ---------------------------------------------------------------
2572 // Step 2: Mutate the trace to exploit the truncation bug.
2573 // Switch from trivial path to sel_trunc_gte_128 path.
2574 // ---------------------------------------------------------------
2575
2576 // 2a. Flip the ALU selectors: trivial -> gte_128.
2577 trace.set(C::alu_sel_trunc_trivial, 0, 0);
2578 trace.set(C::alu_sel_trunc_gte_128, 0, 1);
2579 trace.set(C::alu_sel_trunc_non_trivial, 0, 1);
2580
2581 // 2b. Set the decomposition columns.
2582 // a_lo = lower 128 bits of ia. mid can be anything 128-bit (mid * 0 = 0).
2583 trace.set(C::alu_a_lo, 0, FF(uint256_t(a_decomp.lo)));
2584 trace.set(C::alu_mid, 0, 0);
2585 trace.set(C::alu_mid_bits, 0, 128); // 128 - max_bits = 128 - 0 = 128
2586
2587 // 2c. Set the exploited output: ic = a_lo (lower 128 bits, NOT the full value).
2588 trace.set(C::alu_ic, 0, a_lo_ff);
2589
2590 // 2d. Update the execution side to match the exploited ic.
2591 trace.set(C::execution_register_0_, 0, a_lo_ff);
2592
2593 // 2e. Add the ff_gt canonical decomposition sub-trace that sel_trunc_gte_128 requires.
2594 // This proves ia = a_lo + 2^128 * a_hi with both limbs range-checked.
2595 auto p_limbs = simulation::decompose_256(FF::modulus);
2596 bool borrow = a_decomp.lo >= p_limbs.lo;
2597 simulation::LimbsComparisonWitness p_sub_a_witness = {
2598 .lo = static_cast<uint128_t>(
2599 (uint256_t(p_limbs.lo) - uint256_t(a_decomp.lo) - 1 + (borrow ? (uint256_t(1) << 128) : 0))),
2600 .hi = static_cast<uint128_t>(uint256_t(p_limbs.hi) - uint256_t(a_decomp.hi) - (borrow ? 1 : 0)),
2601 .borrow = borrow,
2602 };
2603 field_gt_builder.process({ { .operation = simulation::FieldGreaterOperation::CANONICAL_DECOMPOSITION,
2604 .a = MemoryValue::from_tag(MemoryTag::FF, large_value_u256),
2605 .a_limbs = a_decomp,
2606 .p_sub_a_witness = p_sub_a_witness } },
2607 trace);
2608
2609 // 2f. Add the range check sub-trace for mid (0 bits to check, value 0, 128 bits).
2610 range_check_builder.process({ { .value = 0, .num_bits = 128 } }, trace);
2611
2612 // ---------------------------------------------------------------
2613 // Step 3: Verify the exploited trace passes ALL checks.
2614 // ---------------------------------------------------------------
2615
2616 // ALU relation constraints pass.
2617 EXPECT_THROW_WITH_MESSAGE((check_relation<alu>(trace)), alu::get_subrelation_label(alu::SR_DEST_FF_IS_TRIVIAL));
2618 // check_relation<alu>(trace);
2619
2620 /* EXPLOIT TESTING NOTE:
2621 * To test the exploit, we need to comment out the check_relation<alu>(trace) above
2622 * and remove the EXPECT_THROW_WITH_MESSAGE() line.
2623 */
2624
2625 // All ALU child lookups pass (including LARGE_TRUNC_CANONICAL_DEC into ff_gt, RANGE_CHECK_TRUNC_MID).
2626 check_all_interactions<AluTraceBuilder>(trace);
2627
2628 // The execution -> ALU dispatch lookup passes with the tampered ic.
2629 check_interaction<ExecutionTraceBuilder, lookup_execution_dispatch_to_set_settings>(trace);
2630
2631 // The exploit is complete: the prover proved that SET_FF(p-1) = a_lo (lower 128 bits)
2632 // instead of p-1. The value written to the destination register is wrong.
2633 EXPECT_NE(trace.get(C::alu_ic, 0), large_value);
2634 EXPECT_EQ(trace.get(C::alu_ic, 0), a_lo_ff);
2635}
2636
2637} // namespace
2638} // namespace bb::avm2::constraining
MemoryTag dst_tag
#define EXPECT_THROW_WITH_MESSAGE(code, expectedMessageRegex)
Definition assert.hpp:224
bb::field< bb::Bn254FrParams > FF
Definition field.cpp:24
INSTANTIATE_TEST_SUITE_P(All, KernelIOTamperingTests, testing::Values(KernelIOField::PAIRING_INPUTS, KernelIOField::ACCUMULATOR_HASH, KernelIOField::KERNEL_RETURN_DATA, KernelIOField::APP_RETURN_DATA, KernelIOField::ECC_OP_HASH), [](const testing::TestParamInfo< KernelIOField > &info) { switch(info.param) { case KernelIOField::PAIRING_INPUTS:return "PairingInputs";case KernelIOField::ACCUMULATOR_HASH:return "AccumulatorHash";case KernelIOField::KERNEL_RETURN_DATA:return "KernelReturnData";case KernelIOField::APP_RETURN_DATA:return "AppReturnData";case KernelIOField::ECC_OP_HASH:return "EccOpHash";} return "Unknown";})
TEST_P(KernelIOTamperingTests, CausesVerificationFailure)
static TaggedValue from_tag(ValueTag tag, FF value)
static constexpr size_t SR_EXACTLY_ONE_OPERATION_ACTIVE
Definition alu.hpp:41
static constexpr size_t SR_AB_TAGS_CHECK
Definition alu.hpp:46
static constexpr size_t SR_C_TAG_CHECK
Definition alu.hpp:50
static constexpr size_t SR_ERR_CHECK
Definition alu.hpp:44
static std::string get_subrelation_label(size_t index)
Definition alu.hpp:78
static constexpr size_t SR_TAG_ERR_CHECK
Definition alu.hpp:45
static constexpr size_t SR_DISPATCH_OPERATION
Definition alu.hpp:40
static constexpr size_t SR_ALU_ADD_SUB
Definition alu.hpp:55
TEST_F(AcirComponentsCheckTest, SingleLinearConstraintLinksTwoWitnesses)
RangeCheckTraceBuilder range_check_builder
Definition alu.test.cpp:121
PrecomputedTraceBuilder precomputed_builder
Definition alu.test.cpp:120
FieldGreaterThanTraceBuilder field_gt_builder
Definition alu.test.cpp:122
AluTraceBuilder builder
Definition alu.test.cpp:124
GreaterThanTraceBuilder gt_builder
Definition alu.test.cpp:123
TestTraceContainer trace
FF a
FF b
TEST_F(AvmRecursiveTests, TwoLayerAvmRecursion)
A test of the Two Layer AVM recursive verifier.
TestTraceContainer empty_trace()
Definition fixtures.cpp:156
TaggedValue MemoryValue
AvmFlavorSettings::FF FF
Definition field.hpp:10
uint8_t get_tag_bits(ValueTag tag)
uint256_t get_tag_max_value(ValueTag tag)
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
constexpr auto tuple_cat(T &&... ts)
Definition tuplet.hpp:1101
bb::VectorAffineElementPushSpan< BaseParams > out
unsigned __int128 uint128_t
Definition serialize.hpp:45
static constexpr uint256_t modulus
constexpr field invert() const noexcept
VectorField result