Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
alu_trace.cpp
Go to the documentation of this file.
2
3#include <cstddef>
4#include <cstdint>
5#include <ranges>
6#include <stdexcept>
7
17
18namespace bb::avm2::tracegen {
19
20namespace {
21
22// TODO(MW): Rename to something useful! Helper fn to get operation specific values.
23std::vector<std::pair<Column, FF>> get_operation_columns(const simulation::AluEvent& event)
24{
25 bool is_ff = event.a.get_tag() == MemoryTag::FF;
26 bool is_u128 = event.a.get_tag() == MemoryTag::U128;
27 bool no_tag_err = event.error != simulation::AluError::TAG_ERROR;
28 switch (event.operation) {
30 return { { Column::alu_sel_op_add, 1 },
31 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::ADD).subtrace_operation_id },
32 // I think the only situation in which a + b != c as fields is when c overflows the bit size
33 // if this in unclear, I can use > or actually check bit sizes:
34 { Column::alu_cf, event.a.as_ff() + event.b.as_ff() != event.c.as_ff() } };
36 return { { Column::alu_sel_op_sub, 1 },
37 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::SUB).subtrace_operation_id },
38 { Column::alu_cf, event.a.as_ff() - event.b.as_ff() != event.c.as_ff() } };
40 uint256_t a_int = static_cast<uint256_t>(event.a.as_ff());
41 uint256_t b_int = static_cast<uint256_t>(event.b.as_ff());
42 // Columns shared for all tags in a MUL:
44 { Column::alu_sel_op_mul, 1 },
45 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::MUL).subtrace_operation_id },
46 { Column::alu_constant_64, 64 },
47 { Column::alu_sel_is_u128, is_u128 },
48 { Column::alu_tag_u128_diff_inv,
49 is_u128 ? 0
50 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::U128)))
51 .invert() },
52 };
53 if (is_u128) {
54 // For u128s, we decompose a and b into 64 bit chunks:
55 auto a_decomp = simulation::decompose(static_cast<uint128_t>(event.a.as_ff()));
56 auto b_decomp = simulation::decompose(static_cast<uint128_t>(event.b.as_ff()));
57 // c_hi = old_c_hi - a_hi * b_hi % 2^64
58 auto hi_operand = static_cast<uint256_t>(a_decomp.hi) * static_cast<uint256_t>(b_decomp.hi);
59 res.insert(res.end(),
60 {
61 { Column::alu_sel_mul_u128, 1 },
62 { Column::alu_sel_mul_div_u128, 1 },
63 { Column::alu_sel_decompose_a, 1 },
64 { Column::alu_a_lo, a_decomp.lo },
65 { Column::alu_a_lo_bits, 64 },
66 { Column::alu_a_hi, a_decomp.hi },
67 { Column::alu_a_hi_bits, 64 },
68 { Column::alu_b_lo, b_decomp.lo },
69 { Column::alu_b_hi, b_decomp.hi },
70 { Column::alu_c_hi, (((a_int * b_int) >> 128) - hi_operand) % (uint256_t(1) << 64) },
71 { Column::alu_cf, hi_operand == 0 ? 0 : 1 },
72 });
73 } else {
74 // For non-u128s, we just take the top bits of a*b:
75 res.insert(res.end(),
76 { { Column::alu_c_hi, is_ff ? 0 : (a_int * b_int) >> get_tag_bits(event.a.get_tag()) } });
77 }
78 return res;
79 }
81 bool div_0_error = event.error == simulation::AluError::DIV_0_ERROR;
82 auto remainder =
83 no_tag_err && !div_0_error ? event.a - event.b * event.c : MemoryValue::from_tag(event.a.get_tag(), 0);
84 // Columns shared for all tags in a DIV:
86 { Column::alu_sel_op_div, 1 },
87 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::DIV).subtrace_operation_id },
88 { Column::alu_helper1, remainder },
89 { Column::alu_constant_64, 64 },
90 { Column::alu_sel_is_ff, is_ff },
91 { Column::alu_tag_ff_diff_inv,
92 is_ff
93 ? 0
94 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
95 { Column::alu_sel_is_u128, is_u128 },
96 { Column::alu_tag_u128_diff_inv,
97 is_u128 ? 0
98 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::U128)))
99 .invert() },
100 { Column::alu_b_inv, div_0_error ? 0 : event.b.as_ff().invert() },
101 { Column::alu_sel_div_no_0_err, div_0_error ? 0 : 1 },
102 };
103 if (is_u128) {
104 // For u128s, we decompose c and b into 64 bit chunks:
105 auto c_decomp = simulation::decompose(static_cast<uint128_t>(event.c.as_ff()));
106 auto b_decomp = simulation::decompose(static_cast<uint128_t>(event.b.as_ff()));
107 res.insert(res.end(),
108 {
109 { Column::alu_sel_mul_div_u128, 1 },
110 { Column::alu_sel_decompose_a, 1 },
111 { Column::alu_a_lo, c_decomp.lo },
112 { Column::alu_a_lo_bits, 64 },
113 { Column::alu_a_hi, c_decomp.hi },
114 { Column::alu_a_hi_bits, 64 },
115 { Column::alu_b_lo, b_decomp.lo },
116 { Column::alu_b_hi, b_decomp.hi },
117 });
118 }
119 return res;
120 }
122 bool div_0_error = event.error == simulation::AluError::DIV_0_ERROR;
123 return {
124 { Column::alu_sel_op_fdiv, 1 },
125 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::FDIV).subtrace_operation_id },
126 { Column::alu_sel_is_ff, is_ff },
127 { Column::alu_tag_ff_diff_inv,
128 is_ff
129 ? 0
130 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
131 { Column::alu_b_inv, div_0_error ? 0 : event.b.as_ff().invert() },
132 };
133 }
135 const FF diff = event.a.as_ff() - event.b.as_ff();
136 return { { Column::alu_sel_op_eq, 1 },
137 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::EQ).subtrace_operation_id },
138 { Column::alu_helper1, diff == 0 ? 0 : diff.invert() } };
139 }
141 return {
142 { Column::alu_lt_ops_input_a, event.b },
143 { Column::alu_lt_ops_input_b, event.a },
144 { Column::alu_lt_ops_result_c, event.c },
145 { Column::alu_sel_op_lt, 1 },
146 { Column::alu_sel_lt_ops, no_tag_err },
147 { Column::alu_op_id,
148 static_cast<uint8_t>(SUBTRACE_INFO_MAP.at(ExecutionOpCode::LT).subtrace_operation_id) },
149 { Column::alu_sel_is_ff, is_ff },
150 { Column::alu_sel_ff_lt_ops, is_ff && no_tag_err },
151 { Column::alu_sel_int_lt_ops, !is_ff && no_tag_err },
152 { Column::alu_tag_ff_diff_inv,
153 is_ff
154 ? 0
155 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
156 };
158 return {
159 { Column::alu_lt_ops_input_a, event.a },
160 { Column::alu_lt_ops_input_b, event.b },
161 { Column::alu_lt_ops_result_c, MemoryValue::from<uint1_t>(event.c.as_ff() == 0 && no_tag_err ? 1 : 0) },
162 { Column::alu_sel_op_lte, 1 },
163 { Column::alu_sel_lt_ops, no_tag_err },
164 { Column::alu_op_id,
165 static_cast<uint8_t>(SUBTRACE_INFO_MAP.at(ExecutionOpCode::LTE).subtrace_operation_id) },
166 { Column::alu_sel_is_ff, is_ff },
167 { Column::alu_sel_ff_lt_ops, is_ff && no_tag_err },
168 { Column::alu_sel_int_lt_ops, !is_ff && no_tag_err },
169 { Column::alu_tag_ff_diff_inv,
170 is_ff
171 ? 0
172 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
173 };
174 case simulation::AluOperation::NOT: {
175 const FF tag_diff = static_cast<uint8_t>(event.a.get_tag()) - static_cast<uint8_t>(MemoryTag::FF);
176 return {
177 { Column::alu_sel_op_not, 1 },
178 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::NOT).subtrace_operation_id },
179 { Column::alu_sel_is_ff, is_ff },
180 { Column::alu_tag_ff_diff_inv, is_ff ? 0 : tag_diff.invert() },
181 };
182 }
183 case simulation::AluOperation::SHL: {
184 auto a_num = static_cast<uint128_t>(event.a.as_ff());
185 auto b_num = static_cast<uint128_t>(event.b.as_ff());
186 auto tag_bits = get_tag_bits(event.a.get_tag());
187 // Whether we shift by more than the bit size (=> result is 0):
188 bool overflow = b_num > tag_bits;
189 // The bit size of the low limb of decomposed input a (if overflow, assigned as max_bits to range check
190 // b - max_bits):
191 auto shift_lo_bits = overflow ? tag_bits : tag_bits - b_num;
192 // The low limb of decomposed input a (if overflow, assigned as b - max_bits to range check and
193 // prove b > max_bits):
194 auto a_lo = overflow ? b_num - tag_bits : a_num % (static_cast<uint128_t>(1) << shift_lo_bits);
195 return {
196 { Column::alu_sel_op_shl, 1 },
197 { Column::alu_sel_shift_ops, 1 },
198 { Column::alu_sel_shift_ops_no_overflow, overflow ? 0 : 1 },
199 { Column::alu_sel_decompose_a, is_ff ? 0 : 1 },
200 { Column::alu_a_lo, a_lo },
201 { Column::alu_a_lo_bits, shift_lo_bits },
202 { Column::alu_a_hi, a_num >> shift_lo_bits },
203 { Column::alu_a_hi_bits, overflow ? tag_bits : b_num },
204 { Column::alu_shift_lo_bits, shift_lo_bits },
205 { Column::alu_two_pow_shift_lo_bits, static_cast<uint128_t>(1) << shift_lo_bits },
206 { Column::alu_sel_is_ff, is_ff },
207 { Column::alu_tag_ff_diff_inv,
208 is_ff
209 ? 0
210 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
211 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::SHL).subtrace_operation_id },
212 { Column::alu_helper1, static_cast<uint128_t>(1) << b_num },
213 };
214 }
215 case simulation::AluOperation::SHR: {
216 auto a_num = static_cast<uint128_t>(event.a.as_ff());
217 auto b_num = static_cast<uint128_t>(event.b.as_ff());
218 auto tag_bits = get_tag_bits(event.a.get_tag());
219 // Whether we shift by more than the bit size (=> result is 0):
220 bool overflow = b_num > tag_bits;
221 // The bit size of the low limb of decomposed input a (if overflow, assigned as max_bits to range check
222 // b - max_bits):
223 auto shift_lo_bits = overflow ? tag_bits : b_num;
224 // The low limb of decomposed input a (if overflow, assigned as b - max_bits to range check and
225 // prove b > max_bits):
226 auto a_lo = overflow ? b_num - tag_bits : a_num % (static_cast<uint128_t>(1) << shift_lo_bits);
227 return {
228 { Column::alu_sel_op_shr, 1 },
229 { Column::alu_sel_shift_ops, 1 },
230 { Column::alu_sel_shift_ops_no_overflow, overflow ? 0 : 1 },
231 { Column::alu_sel_decompose_a, is_ff ? 0 : 1 },
232 { Column::alu_a_lo, a_lo },
233 { Column::alu_a_lo_bits, shift_lo_bits },
234 { Column::alu_a_hi, a_num >> shift_lo_bits },
235 { Column::alu_a_hi_bits, overflow ? tag_bits : tag_bits - b_num },
236 { Column::alu_shift_lo_bits, shift_lo_bits },
237 { Column::alu_two_pow_shift_lo_bits, static_cast<uint128_t>(1) << shift_lo_bits },
238 { Column::alu_sel_is_ff, is_ff },
239 { Column::alu_tag_ff_diff_inv,
240 is_ff
241 ? 0
242 : (FF(static_cast<uint8_t>(event.a.get_tag())) - FF(static_cast<uint8_t>(MemoryTag::FF))).invert() },
243 { Column::alu_op_id, SUBTRACE_INFO_MAP.at(ExecutionOpCode::SHR).subtrace_operation_id },
244 };
245 }
246 case simulation::AluOperation::TRUNCATE: {
247 const uint256_t value = static_cast<uint256_t>(event.a.as_ff());
248 const MemoryTag dst_tag = static_cast<MemoryTag>(static_cast<uint8_t>(event.b.as_ff()));
249 bool is_trivial = dst_tag == MemoryTag::FF || value <= get_tag_max_value(dst_tag);
250 bool is_lt_128 = !is_trivial && value < (static_cast<uint256_t>(1) << 128);
251 bool is_gte_128 = !is_trivial && !is_lt_128;
252 const uint256_t lo_128 = is_trivial ? 0 : value & ((static_cast<uint256_t>(1) << 128) - 1);
253 const uint8_t dst_bits = get_tag_bits(dst_tag);
254 const uint256_t mid = is_trivial ? 0 : lo_128 >> dst_bits;
255
256 return {
257 { Column::alu_sel_op_truncate, 1 },
258 { Column::alu_sel_trunc_trivial, is_trivial },
259 { Column::alu_sel_trunc_lt_128, is_lt_128 },
260 { Column::alu_sel_trunc_gte_128, is_gte_128 },
261 { Column::alu_sel_trunc_non_trivial, !is_trivial },
262 { Column::alu_a_lo, lo_128 },
263 { Column::alu_a_hi, is_gte_128 ? value >> 128 : 0 },
264 { Column::alu_mid, mid },
265 { Column::alu_op_id, AVM_EXEC_OP_ID_ALU_TRUNCATE },
266 { Column::alu_mid_bits, is_trivial ? 0 : 128 - dst_bits },
267 };
268 }
269 default:
270 throw std::runtime_error("Unknown ALU operation");
271 break;
272 }
273}
274
275std::vector<std::pair<Column, FF>> get_tag_error_columns(const simulation::AluEvent& event)
276{
277 const MemoryTag a_tag = event.a.get_tag();
278 const FF a_tag_ff = static_cast<FF>(static_cast<uint8_t>(a_tag));
279 const MemoryTag b_tag = event.b.get_tag();
280 const FF b_tag_ff = static_cast<FF>(static_cast<uint8_t>(b_tag));
281 // Tag errors currently have cases:
282 // 1. Input tagged as a field for NOT or DIV operations
283 // 2. Mismatched tags for inputs a and b for all opcodes apart from TRUNC
284
285 // Case 1:
286 bool ff_tag_err =
287 ((event.a.get_tag() == MemoryTag::FF) &&
288 (event.operation == simulation::AluOperation::NOT || event.operation == simulation::AluOperation::DIV ||
289 event.operation == simulation::AluOperation::SHL || event.operation == simulation::AluOperation::SHR)) ||
290 ((event.a.get_tag() != MemoryTag::FF) && (event.operation == simulation::AluOperation::FDIV));
291 // Case 2:
292 bool ab_tags_mismatch = (a_tag_ff != b_tag_ff) && (event.operation != simulation::AluOperation::TRUNCATE);
293 // Note: both cases can occur at the same time. Case 1 only requires sel_tag_error to be on, so we
294 // check ab_tags_mismatch first:
295 if (ab_tags_mismatch) {
296 return { { Column::alu_sel_tag_err, 1 },
297 { Column::alu_sel_ab_tag_mismatch, 1 },
298 { Column::alu_ab_tags_diff_inv, (a_tag_ff - b_tag_ff).invert() } };
299 }
300 if (ff_tag_err) {
301 // Note: There is no 'alu_sel_ff_tag_err' because we can handle this with existing selectors:
302 // (sel_op_div + sel_op_not) * sel_is_ff
303 return { { Column::alu_sel_tag_err, 1 } };
304 }
305 // We shouldn't have emitted an event with a tag error when one doesn't exist:
306 assert(false && "ALU Event emitted with tag error, but none exists");
307 return {};
308}
309
310} // namespace
311
314{
315 using C = Column;
317
318 uint32_t row = 0;
319 for (const auto& event : events) {
320 // For TRUNCATE, the destination tag is passed through b in the event, but will be
321 // set to ia_tag in the ALU subtrace. (See alu.pil for more details.).
322 const uint8_t a_tag_u8 = event.operation == simulation::AluOperation::TRUNCATE
323 ? static_cast<uint8_t>(event.b.as_ff())
324 : static_cast<uint8_t>(event.a.get_tag());
325 const FF b_tag = static_cast<FF>(static_cast<uint8_t>(event.b.get_tag()));
326 const FF c_tag = static_cast<FF>(static_cast<uint8_t>(event.c.get_tag()));
327 bool tag_check_failed = event.error.has_value() && event.error == AluError::TAG_ERROR;
328 if (tag_check_failed) {
329 // Tag error specific columns:
330 trace.set(row, get_tag_error_columns(event));
331 }
332 bool div_0_error = event.error.has_value() && event.error == AluError::DIV_0_ERROR;
333 if (div_0_error) {
334 // TODO(MW): Below needed?
335 // Should not emit a divide by 0 error if we are not in DIV or FDIV or have no 0 divisor:
336 assert((event.b.as_ff() == FF(0)) &&
337 ((event.operation == simulation::AluOperation::DIV) ||
338 (event.operation == simulation::AluOperation::FDIV)) &&
339 "ALU Event emitted with divide by zero error, but none exists");
340 }
341
342 // Operation specific columns:
343 trace.set(row, get_operation_columns(event));
344
345 trace.set(row,
346 { {
347 { C::alu_sel, 1 },
348 { C::alu_ia, event.a },
349 { C::alu_ib, event.b },
350 { C::alu_ic, event.c },
351 { C::alu_ia_tag, a_tag_u8 },
352 { C::alu_ib_tag, b_tag },
353 { C::alu_ic_tag, c_tag },
354 { C::alu_max_bits, get_tag_bits(static_cast<MemoryTag>(a_tag_u8)) },
355 { C::alu_max_value, get_tag_max_value(static_cast<MemoryTag>(a_tag_u8)) },
356 { C::alu_sel_div_0_err, div_0_error ? 1 : 0 },
357 { C::alu_sel_err, tag_check_failed || div_0_error ? 1 : 0 },
358 } });
359
360 row++;
361 }
362}
363
364const InteractionDefinition AluTraceBuilder::interactions =
366 .add<lookup_alu_tag_max_bits_value_settings, InteractionType::LookupIntoIndexedByClk>()
367 .add<lookup_alu_range_check_decomposition_a_lo_settings, InteractionType::LookupGeneric>()
368 .add<lookup_alu_range_check_decomposition_a_hi_settings, InteractionType::LookupGeneric>()
369 .add<lookup_alu_range_check_decomposition_b_lo_settings, InteractionType::LookupGeneric>()
370 .add<lookup_alu_range_check_decomposition_b_hi_settings, InteractionType::LookupGeneric>()
371 .add<lookup_alu_range_check_mul_u128_c_hi_settings, InteractionType::LookupGeneric>()
372 .add<lookup_alu_gt_div_remainder_settings, InteractionType::LookupGeneric>()
373 .add<lookup_alu_ff_gt_settings, InteractionType::LookupGeneric>()
374 .add<lookup_alu_int_gt_settings, InteractionType::LookupGeneric>()
375 .add<lookup_alu_shifts_two_pow_settings, InteractionType::LookupIntoIndexedByClk>()
376 .add<lookup_alu_range_check_trunc_mid_settings, InteractionType::LookupGeneric>()
377 .add<lookup_alu_large_trunc_canonical_dec_settings, InteractionType::LookupGeneric>();
378} // namespace bb::avm2::tracegen
MemoryTag dst_tag
#define AVM_EXEC_OP_ID_ALU_TRUNCATE
bb::fr FF
static TaggedValue from_tag(ValueTag tag, FF value)
InteractionDefinition & add(auto &&... args)
TestTraceContainer trace
U256Decomposition decompose(const uint256_t &x)
const std::unordered_map< ExecutionOpCode, SubtraceInfo > SUBTRACE_INFO_MAP
uint8_t get_tag_bits(ValueTag tag)
uint256_t get_tag_max_value(ValueTag tag)
ValueTag MemoryTag
AvmFlavorSettings::FF FF
Definition field.hpp:10
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
simulation::PublicDataTreeReadWriteEvent event
unsigned __int128 uint128_t
Definition serialize.hpp:44
constexpr field invert() const noexcept