28 switch (
event.operation) {
30 return { { Column::alu_sel_op_add, 1 },
34 { Column::alu_cf,
event.a.as_ff() +
event.b.as_ff() !=
event.c.as_ff() } };
36 return { { Column::alu_sel_op_sub, 1 },
38 { Column::alu_cf,
event.a.as_ff() -
event.b.as_ff() !=
event.c.as_ff() } };
44 { Column::alu_sel_op_mul, 1 },
46 { Column::alu_constant_64, 64 },
47 { Column::alu_sel_is_u128, is_u128 },
48 { Column::alu_tag_u128_diff_inv,
58 auto hi_operand =
static_cast<uint256_t>(a_decomp.hi) *
static_cast<uint256_t>(b_decomp.hi);
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 },
76 { { Column::alu_c_hi, is_ff ? 0 : (a_int * b_int) >>
get_tag_bits(
event.a.get_tag()) } });
86 { Column::alu_sel_op_div, 1 },
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,
95 { Column::alu_sel_is_u128, is_u128 },
96 { Column::alu_tag_u128_diff_inv,
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 },
107 res.insert(res.end(),
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 },
124 { Column::alu_sel_op_fdiv, 1 },
126 { Column::alu_sel_is_ff, is_ff },
127 { Column::alu_tag_ff_diff_inv,
131 { Column::alu_b_inv, div_0_error ? 0 :
event.b.as_ff().invert() },
135 const FF diff =
event.a.as_ff() -
event.b.as_ff();
136 return { { Column::alu_sel_op_eq, 1 },
138 { Column::alu_helper1, diff == 0 ? 0 : diff.
invert() } };
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 },
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,
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 },
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,
172 : (
FF(
static_cast<uint8_t
>(
event.a.get_tag())) -
FF(
static_cast<uint8_t
>(MemoryTag::FF))).invert() },
174 case simulation::AluOperation::NOT: {
175 const FF tag_diff =
static_cast<uint8_t
>(
event.a.get_tag()) -
static_cast<uint8_t
>(MemoryTag::FF);
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() },
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());
188 bool overflow = b_num > tag_bits;
191 auto shift_lo_bits = overflow ? tag_bits : tag_bits - b_num;
194 auto a_lo = overflow ? b_num - tag_bits : a_num % (
static_cast<uint128_t>(1) << shift_lo_bits);
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,
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 },
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());
220 bool overflow = b_num > tag_bits;
223 auto shift_lo_bits = overflow ? tag_bits : b_num;
226 auto a_lo = overflow ? b_num - tag_bits : a_num % (
static_cast<uint128_t>(1) << shift_lo_bits);
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,
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 },
246 case simulation::AluOperation::TRUNCATE: {
250 bool is_lt_128 = !is_trivial && value < (static_cast<uint256_t>(1) << 128);
251 bool is_gte_128 = !is_trivial && !is_lt_128;
254 const uint256_t mid = is_trivial ? 0 : lo_128 >> dst_bits;
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 },
266 { Column::alu_mid_bits, is_trivial ? 0 : 128 - dst_bits },
270 throw std::runtime_error(
"Unknown ALU operation");
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));
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));
292 bool ab_tags_mismatch = (a_tag_ff != b_tag_ff) && (
event.operation != simulation::AluOperation::TRUNCATE);
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() } };
303 return { { Column::alu_sel_tag_err, 1 } };
306 assert(
false &&
"ALU Event emitted with tag error, but none exists");
319 for (
const auto&
event : events) {
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) {
332 bool div_0_error =
event.error.has_value() &&
event.error == AluError::DIV_0_ERROR;
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");
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 },
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 },
367 .add<lookup_alu_range_check_decomposition_a_lo_settings, InteractionType::LookupGeneric>()
369 .add<lookup_alu_range_check_decomposition_b_lo_settings, InteractionType::LookupGeneric>()
371 .add<lookup_alu_range_check_mul_u128_c_hi_settings, InteractionType::LookupGeneric>()
373 .add<lookup_alu_ff_gt_settings, InteractionType::LookupGeneric>()
375 .add<lookup_alu_shifts_two_pow_settings, InteractionType::LookupIntoIndexedByClk>()
377 .add<lookup_alu_large_trunc_canonical_dec_settings, InteractionType::LookupGeneric>();
#define AVM_EXEC_OP_ID_ALU_TRUNCATE
static TaggedValue from_tag(ValueTag tag, FF value)
std::vector< Event > Container
InteractionDefinition & add(auto &&... args)
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)
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
simulation::PublicDataTreeReadWriteEvent event
unsigned __int128 uint128_t
constexpr field invert() const noexcept