diff --git a/barretenberg/cpp/pil/avm/alu_chip.pil b/barretenberg/cpp/pil/avm/alu_chip.pil index c3eaa6f5fc2..0de5c559681 100644 --- a/barretenberg/cpp/pil/avm/alu_chip.pil +++ b/barretenberg/cpp/pil/avm/alu_chip.pil @@ -186,7 +186,7 @@ namespace aluChip(256); // b = b_l + b_h * 2^64 // We show that c satisfies: a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 = R * 2^128 + c // for a R < 2^65. Equivalently: - // a * b_l + a_l * b_h * 2^64 = (CF * 2^65 + R') * 2^128 + c + // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c // for a bit carry flag CF and R' range constrained to 64 bits. // We use two lines in the execution trace. First line represents a // as decomposed over 16-bit registers. Second line represents b. @@ -209,6 +209,6 @@ namespace aluChip(256); alu_u128_tag * alu_op_mul * ( alu_ia * sum_shifted_64 + sum_64 * sum_high_shifted_64 * 2**64 - - (alu_cf * 2**65 + alu_u64_r0) * 2**128 + - (alu_cf * 2**64 + alu_u64_r0) * 2**128 - alu_ic ) = 0; diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index 5b97550ac3a..05e7de9640f 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -43,7 +43,7 @@ class AvmMiniFlavor { // the unshifted and one for the shifted static constexpr size_t NUM_ALL_ENTITIES = 80; - using Relations = std::tuple, AvmMini_vm::alu_chip, AvmMini_vm::mem_trace>; + using Relations = std::tuple, AvmMini_vm::avm_mini, AvmMini_vm::mem_trace>; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); @@ -281,19 +281,19 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - avmMini_pc_shift, - avmMini_internal_return_ptr_shift, - aluChip_alu_u16_r0_shift, - aluChip_alu_u16_r7_shift, aluChip_alu_u16_r6_shift, + aluChip_alu_u16_r2_shift, aluChip_alu_u16_r3_shift, aluChip_alu_u16_r4_shift, - aluChip_alu_u16_r2_shift, + aluChip_alu_u16_r0_shift, aluChip_alu_u16_r1_shift, aluChip_alu_u16_r5_shift, - memTrace_m_addr_shift, + aluChip_alu_u16_r7_shift, + avmMini_internal_return_ptr_shift, + avmMini_pc_shift, memTrace_m_val_shift, memTrace_m_tag_shift, + memTrace_m_addr_shift, memTrace_m_rw_shift) RefVector get_wires() @@ -364,19 +364,19 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - avmMini_pc_shift, - avmMini_internal_return_ptr_shift, - aluChip_alu_u16_r0_shift, - aluChip_alu_u16_r7_shift, aluChip_alu_u16_r6_shift, + aluChip_alu_u16_r2_shift, aluChip_alu_u16_r3_shift, aluChip_alu_u16_r4_shift, - aluChip_alu_u16_r2_shift, + aluChip_alu_u16_r0_shift, aluChip_alu_u16_r1_shift, aluChip_alu_u16_r5_shift, - memTrace_m_addr_shift, + aluChip_alu_u16_r7_shift, + avmMini_internal_return_ptr_shift, + avmMini_pc_shift, memTrace_m_val_shift, memTrace_m_tag_shift, + memTrace_m_addr_shift, memTrace_m_rw_shift }; }; RefVector get_unshifted() @@ -450,23 +450,19 @@ class AvmMiniFlavor { }; RefVector get_to_be_shifted() { - return { avmMini_pc, avmMini_internal_return_ptr, - aluChip_alu_u16_r0, aluChip_alu_u16_r7, - aluChip_alu_u16_r6, aluChip_alu_u16_r3, - aluChip_alu_u16_r4, aluChip_alu_u16_r2, - aluChip_alu_u16_r1, aluChip_alu_u16_r5, - memTrace_m_addr, memTrace_m_val, - memTrace_m_tag, memTrace_m_rw }; + return { aluChip_alu_u16_r6, aluChip_alu_u16_r2, aluChip_alu_u16_r3, + aluChip_alu_u16_r4, aluChip_alu_u16_r0, aluChip_alu_u16_r1, + aluChip_alu_u16_r5, aluChip_alu_u16_r7, avmMini_internal_return_ptr, + avmMini_pc, memTrace_m_val, memTrace_m_tag, + memTrace_m_addr, memTrace_m_rw }; }; RefVector get_shifted() { - return { avmMini_pc_shift, avmMini_internal_return_ptr_shift, - aluChip_alu_u16_r0_shift, aluChip_alu_u16_r7_shift, - aluChip_alu_u16_r6_shift, aluChip_alu_u16_r3_shift, - aluChip_alu_u16_r4_shift, aluChip_alu_u16_r2_shift, - aluChip_alu_u16_r1_shift, aluChip_alu_u16_r5_shift, - memTrace_m_addr_shift, memTrace_m_val_shift, - memTrace_m_tag_shift, memTrace_m_rw_shift }; + return { aluChip_alu_u16_r6_shift, aluChip_alu_u16_r2_shift, aluChip_alu_u16_r3_shift, + aluChip_alu_u16_r4_shift, aluChip_alu_u16_r0_shift, aluChip_alu_u16_r1_shift, + aluChip_alu_u16_r5_shift, aluChip_alu_u16_r7_shift, avmMini_internal_return_ptr_shift, + avmMini_pc_shift, memTrace_m_val_shift, memTrace_m_tag_shift, + memTrace_m_addr_shift, memTrace_m_rw_shift }; }; }; @@ -479,13 +475,11 @@ class AvmMiniFlavor { RefVector get_to_be_shifted() { - return { avmMini_pc, avmMini_internal_return_ptr, - aluChip_alu_u16_r0, aluChip_alu_u16_r7, - aluChip_alu_u16_r6, aluChip_alu_u16_r3, - aluChip_alu_u16_r4, aluChip_alu_u16_r2, - aluChip_alu_u16_r1, aluChip_alu_u16_r5, - memTrace_m_addr, memTrace_m_val, - memTrace_m_tag, memTrace_m_rw }; + return { aluChip_alu_u16_r6, aluChip_alu_u16_r2, aluChip_alu_u16_r3, + aluChip_alu_u16_r4, aluChip_alu_u16_r0, aluChip_alu_u16_r1, + aluChip_alu_u16_r5, aluChip_alu_u16_r7, avmMini_internal_return_ptr, + avmMini_pc, memTrace_m_val, memTrace_m_tag, + memTrace_m_addr, memTrace_m_rw }; }; // The plookup wires that store plookup read data. diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp index 48a77acbb64..e7ac9b48c96 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp @@ -86,19 +86,19 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; - FF avmMini_pc_shift{}; - FF avmMini_internal_return_ptr_shift{}; - FF aluChip_alu_u16_r0_shift{}; - FF aluChip_alu_u16_r7_shift{}; FF aluChip_alu_u16_r6_shift{}; + FF aluChip_alu_u16_r2_shift{}; FF aluChip_alu_u16_r3_shift{}; FF aluChip_alu_u16_r4_shift{}; - FF aluChip_alu_u16_r2_shift{}; + FF aluChip_alu_u16_r0_shift{}; FF aluChip_alu_u16_r1_shift{}; FF aluChip_alu_u16_r5_shift{}; - FF memTrace_m_addr_shift{}; + FF aluChip_alu_u16_r7_shift{}; + FF avmMini_internal_return_ptr_shift{}; + FF avmMini_pc_shift{}; FF memTrace_m_val_shift{}; FF memTrace_m_tag_shift{}; + FF memTrace_m_addr_shift{}; FF memTrace_m_rw_shift{}; }; @@ -197,19 +197,19 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } - polys.avmMini_pc_shift = Polynomial(polys.avmMini_pc.shifted()); - polys.avmMini_internal_return_ptr_shift = Polynomial(polys.avmMini_internal_return_ptr.shifted()); - polys.aluChip_alu_u16_r0_shift = Polynomial(polys.aluChip_alu_u16_r0.shifted()); - polys.aluChip_alu_u16_r7_shift = Polynomial(polys.aluChip_alu_u16_r7.shifted()); polys.aluChip_alu_u16_r6_shift = Polynomial(polys.aluChip_alu_u16_r6.shifted()); + polys.aluChip_alu_u16_r2_shift = Polynomial(polys.aluChip_alu_u16_r2.shifted()); polys.aluChip_alu_u16_r3_shift = Polynomial(polys.aluChip_alu_u16_r3.shifted()); polys.aluChip_alu_u16_r4_shift = Polynomial(polys.aluChip_alu_u16_r4.shifted()); - polys.aluChip_alu_u16_r2_shift = Polynomial(polys.aluChip_alu_u16_r2.shifted()); + polys.aluChip_alu_u16_r0_shift = Polynomial(polys.aluChip_alu_u16_r0.shifted()); polys.aluChip_alu_u16_r1_shift = Polynomial(polys.aluChip_alu_u16_r1.shifted()); polys.aluChip_alu_u16_r5_shift = Polynomial(polys.aluChip_alu_u16_r5.shifted()); - polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted()); + polys.aluChip_alu_u16_r7_shift = Polynomial(polys.aluChip_alu_u16_r7.shifted()); + polys.avmMini_internal_return_ptr_shift = Polynomial(polys.avmMini_internal_return_ptr.shifted()); + polys.avmMini_pc_shift = Polynomial(polys.avmMini_pc.shifted()); polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted()); polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); + polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted()); polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted()); return polys; @@ -248,14 +248,14 @@ class AvmMiniCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("avm_mini", - AvmMini_vm::get_relation_label_avm_mini)) { - return false; - } if (!evaluate_relation.template operator()>("alu_chip", AvmMini_vm::get_relation_label_alu_chip)) { return false; } + if (!evaluate_relation.template operator()>("avm_mini", + AvmMini_vm::get_relation_label_avm_mini)) { + return false; + } if (!evaluate_relation.template operator()>( "mem_trace", AvmMini_vm::get_relation_label_mem_trace)) { return false; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/alu_chip.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/alu_chip.hpp index 13c95170b5f..9cf23c14ff1 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/alu_chip.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/alu_chip.hpp @@ -7,51 +7,51 @@ namespace proof_system::AvmMini_vm { template struct Alu_chipRow { - FF aluChip_alu_op_sub{}; - FF aluChip_alu_u8_r0{}; - FF aluChip_alu_u16_r0_shift{}; - FF aluChip_alu_cf{}; - FF aluChip_alu_ic{}; - FF aluChip_alu_u16_r7_shift{}; - FF aluChip_alu_u128_tag{}; - FF aluChip_alu_u16_r1{}; FF aluChip_alu_u16_r4{}; + FF aluChip_alu_u16_r1{}; + FF aluChip_alu_u16_tag{}; + FF aluChip_alu_u8_tag{}; + FF aluChip_alu_u8_r0{}; FF aluChip_alu_u16_r6{}; + FF aluChip_alu_u8_r1{}; + FF aluChip_alu_u16_r5{}; FF aluChip_alu_u16_r6_shift{}; - FF aluChip_alu_op_add{}; - FF aluChip_alu_u64_tag{}; - FF aluChip_alu_ff_tag{}; - FF aluChip_alu_u16_r3{}; + FF aluChip_alu_u16_r0{}; + FF aluChip_alu_u16_r2_shift{}; + FF aluChip_alu_ib{}; + FF aluChip_alu_ic{}; FF aluChip_alu_u16_r3_shift{}; FF aluChip_alu_u16_r7{}; - FF aluChip_alu_u16_tag{}; - FF aluChip_alu_op_mul{}; - FF aluChip_alu_u16_r5{}; - FF aluChip_alu_u8_tag{}; + FF aluChip_alu_op_sub{}; + FF aluChip_alu_ff_tag{}; + FF aluChip_alu_u16_r2{}; + FF aluChip_alu_u16_r4_shift{}; + FF aluChip_alu_u64_tag{}; FF aluChip_alu_u32_tag{}; FF aluChip_alu_ia{}; FF aluChip_alu_u64_r0{}; - FF aluChip_alu_u16_r4_shift{}; - FF aluChip_alu_u16_r2_shift{}; - FF aluChip_alu_u16_r2{}; - FF aluChip_alu_ib{}; - FF aluChip_alu_u8_r1{}; + FF aluChip_alu_u16_r0_shift{}; + FF aluChip_alu_u16_r3{}; + FF aluChip_alu_op_mul{}; FF aluChip_alu_u16_r1_shift{}; + FF aluChip_alu_u128_tag{}; FF aluChip_alu_u16_r5_shift{}; - FF aluChip_alu_u16_r0{}; + FF aluChip_alu_op_add{}; + FF aluChip_alu_cf{}; + FF aluChip_alu_u16_r7_shift{}; }; inline std::string get_relation_label_alu_chip(int index) { switch (index) { + case 6: + return "SUBOP_ADDITION_FF"; + case 17: return "SUBOP_SUBTRACTION_FF"; case 28: return "SUBOP_MULTIPLICATION_FF"; - - case 6: - return "SUBOP_ADDITION_FF"; } return std::to_string(index); } @@ -507,7 +507,7 @@ template class alu_chipImpl { (aluChip_alu_u16_r6_shift * FF(4294967296UL))) + (aluChip_alu_u16_r7_shift * FF(281474976710656UL)))) * FF(uint256_t{ 0, 1, 0, 0 }))) - - (((aluChip_alu_cf * FF(uint256_t{ 0, 2, 0, 0 })) + aluChip_alu_u64_r0) * + (((aluChip_alu_cf * FF(uint256_t{ 0, 1, 0, 0 })) + aluChip_alu_u64_r0) * FF(uint256_t{ 0, 0, 1, 0 }))) - aluChip_alu_ic)); tmp *= scaling_factor; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp index f4b48ef9ab8..414370a3dd7 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,61 +7,61 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { - FF avmMini_mem_idx_a{}; - FF avmMini_tag_err{}; - FF avmMini_sel_op_sub{}; - FF avmMini_rwc{}; + FF avmMini_ia{}; + FF avmMini_pc{}; + FF avmMini_inv{}; FF avmMini_internal_return_ptr{}; FF avmMini_first{}; - FF avmMini_ib{}; - FF avmMini_mem_op_c{}; - FF avmMini_mem_op_a{}; - FF avmMini_sel_internal_return{}; - FF avmMini_sel_halt{}; - FF avmMini_mem_idx_b{}; - FF avmMini_pc{}; FF avmMini_sel_op_div{}; - FF avmMini_sel_op_mul{}; - FF avmMini_sel_op_add{}; - FF avmMini_rwa{}; - FF avmMini_ia{}; - FF avmMini_sel_internal_call{}; + FF avmMini_internal_return_ptr_shift{}; + FF avmMini_mem_idx_a{}; + FF avmMini_mem_op_a{}; FF avmMini_mem_op_b{}; - FF avmMini_sel_jump{}; FF avmMini_op_err{}; + FF avmMini_sel_op_add{}; + FF avmMini_rwa{}; + FF avmMini_rwc{}; FF avmMini_ic{}; + FF avmMini_sel_internal_call{}; FF avmMini_rwb{}; - FF avmMini_inv{}; + FF avmMini_ib{}; + FF avmMini_sel_op_sub{}; + FF avmMini_sel_op_mul{}; + FF avmMini_sel_internal_return{}; + FF avmMini_tag_err{}; + FF avmMini_sel_jump{}; + FF avmMini_mem_op_c{}; FF avmMini_pc_shift{}; - FF avmMini_internal_return_ptr_shift{}; + FF avmMini_mem_idx_b{}; + FF avmMini_sel_halt{}; }; inline std::string get_relation_label_avm_mini(int index) { switch (index) { - case 24: - return "RETURN_POINTER_INCREMENT"; + case 20: + return "SUBOP_DIVISION_ZERO_ERR1"; - case 30: - return "RETURN_POINTER_DECREMENT"; + case 21: + return "SUBOP_DIVISION_ZERO_ERR2"; + + case 36: + return "INTERNAL_RETURN_POINTER_CONSISTENCY"; case 35: return "PC_INCREMENT"; + case 24: + return "RETURN_POINTER_INCREMENT"; + case 19: return "SUBOP_DIVISION_FF"; - case 20: - return "SUBOP_DIVISION_ZERO_ERR1"; - case 22: return "SUBOP_ERROR_RELEVANT_OP"; - case 36: - return "INTERNAL_RETURN_POINTER_CONSISTENCY"; - - case 21: - return "SUBOP_DIVISION_ZERO_ERR2"; + case 30: + return "RETURN_POINTER_DECREMENT"; } return std::to_string(index); } diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp index 32e3626e5ee..a4c0c2355da 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -68,17 +68,17 @@ [[maybe_unused]] auto avmMini_mem_idx_b = View(new_term.avmMini_mem_idx_b); \ [[maybe_unused]] auto avmMini_mem_idx_c = View(new_term.avmMini_mem_idx_c); \ [[maybe_unused]] auto avmMini_last = View(new_term.avmMini_last); \ - [[maybe_unused]] auto avmMini_pc_shift = View(new_term.avmMini_pc_shift); \ - [[maybe_unused]] auto avmMini_internal_return_ptr_shift = View(new_term.avmMini_internal_return_ptr_shift); \ - [[maybe_unused]] auto aluChip_alu_u16_r0_shift = View(new_term.aluChip_alu_u16_r0_shift); \ - [[maybe_unused]] auto aluChip_alu_u16_r7_shift = View(new_term.aluChip_alu_u16_r7_shift); \ [[maybe_unused]] auto aluChip_alu_u16_r6_shift = View(new_term.aluChip_alu_u16_r6_shift); \ + [[maybe_unused]] auto aluChip_alu_u16_r2_shift = View(new_term.aluChip_alu_u16_r2_shift); \ [[maybe_unused]] auto aluChip_alu_u16_r3_shift = View(new_term.aluChip_alu_u16_r3_shift); \ [[maybe_unused]] auto aluChip_alu_u16_r4_shift = View(new_term.aluChip_alu_u16_r4_shift); \ - [[maybe_unused]] auto aluChip_alu_u16_r2_shift = View(new_term.aluChip_alu_u16_r2_shift); \ + [[maybe_unused]] auto aluChip_alu_u16_r0_shift = View(new_term.aluChip_alu_u16_r0_shift); \ [[maybe_unused]] auto aluChip_alu_u16_r1_shift = View(new_term.aluChip_alu_u16_r1_shift); \ [[maybe_unused]] auto aluChip_alu_u16_r5_shift = View(new_term.aluChip_alu_u16_r5_shift); \ - [[maybe_unused]] auto memTrace_m_addr_shift = View(new_term.memTrace_m_addr_shift); \ + [[maybe_unused]] auto aluChip_alu_u16_r7_shift = View(new_term.aluChip_alu_u16_r7_shift); \ + [[maybe_unused]] auto avmMini_internal_return_ptr_shift = View(new_term.avmMini_internal_return_ptr_shift); \ + [[maybe_unused]] auto avmMini_pc_shift = View(new_term.avmMini_pc_shift); \ [[maybe_unused]] auto memTrace_m_val_shift = View(new_term.memTrace_m_val_shift); \ [[maybe_unused]] auto memTrace_m_tag_shift = View(new_term.memTrace_m_tag_shift); \ + [[maybe_unused]] auto memTrace_m_addr_shift = View(new_term.memTrace_m_addr_shift); \ [[maybe_unused]] auto memTrace_m_rw_shift = View(new_term.memTrace_m_rw_shift); diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp index 62a871802cb..0d3b2804c07 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -8,40 +8,40 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { FF memTrace_m_last{}; - FF memTrace_m_rw{}; + FF memTrace_m_tag_err{}; + FF memTrace_m_val_shift{}; + FF memTrace_m_val{}; FF memTrace_m_tag{}; FF memTrace_m_lastAccess{}; - FF memTrace_m_addr_shift{}; - FF memTrace_m_in_tag{}; FF memTrace_m_one_min_inv{}; - FF memTrace_m_val_shift{}; FF memTrace_m_tag_shift{}; + FF memTrace_m_in_tag{}; + FF memTrace_m_rw{}; + FF memTrace_m_addr_shift{}; FF memTrace_m_addr{}; - FF memTrace_m_val{}; - FF memTrace_m_tag_err{}; FF memTrace_m_rw_shift{}; }; inline std::string get_relation_label_mem_trace(int index) { switch (index) { - case 6: - return "MEM_READ_WRITE_TAG_CONSISTENCY"; + case 8: + return "MEM_IN_TAG_CONSISTENCY_1"; + + case 4: + return "MEM_LAST_ACCESS_DELIMITER"; case 9: return "MEM_IN_TAG_CONSISTENCY_2"; - case 7: - return "MEM_ZERO_INIT"; - case 5: return "MEM_READ_WRITE_VAL_CONSISTENCY"; - case 8: - return "MEM_IN_TAG_CONSISTENCY_1"; + case 7: + return "MEM_ZERO_INIT"; - case 4: - return "MEM_LAST_ACCESS_DELIMITER"; + case 6: + return "MEM_READ_WRITE_TAG_CONSISTENCY"; } return std::to_string(index); } diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_alu_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_alu_trace.cpp index 9167405cbde..50979a08ba1 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_alu_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_alu_trace.cpp @@ -398,11 +398,11 @@ FF AvmMiniAluTraceBuilder::mul(FF const& a, FF const& b, AvmMemoryTag in_tag, ui uint256_t c_high = ((a_u256 >> 64) * (b_u256 >> 64)) << 128; // From PIL relation in alu_chip.pil, we need to determine the bit CF and 64-bit value R' in - // a * b_l + a_l * b_h * 2^64 = (CF * 2^65 + R') * 2^128 + c + // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c // LHS is c_u256 - c_high // CF bit - carry = ((c_u256 - c_high) >> 193) > 0; + carry = ((c_u256 - c_high) >> 192) > 0; // R' value uint64_t alu_u64_r0 = static_cast(((c_u256 - c_high) >> 128) & uint256_t(UINT64_MAX)); diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp index 09341399934..9248cbb8519 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp @@ -98,14 +98,14 @@ Row common_validate_sub(std::vector const& trace, return *alu_row; } -Row common_validate_mul(std::vector const& trace, - FF const& a, - FF const& b, - FF const& c, - FF const& addr_a, - FF const& addr_b, - FF const& addr_c, - avm_trace::AvmMemoryTag const tag) +size_t common_validate_mul(std::vector const& trace, + FF const& a, + FF const& b, + FF const& c, + FF const& addr_a, + FF const& addr_b, + FF const& addr_c, + avm_trace::AvmMemoryTag const tag) { // Find the first row enabling the multiplication selector auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_mul == FF(1); }); @@ -124,7 +124,7 @@ Row common_validate_mul(std::vector const& trace, EXPECT_EQ(row->avmMini_sel_op_mul, FF(1)); EXPECT_EQ(alu_row->aluChip_alu_op_mul, FF(1)); - return *alu_row; + return static_cast(alu_row - trace.begin()); } } // anonymous namespace @@ -231,7 +231,8 @@ TEST_F(AvmMiniArithmeticTestsFF, multiplication) trace_builder.return_op(0, 3); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(20), FF(5), FF(100), FF(2), FF(0), FF(1), AvmMemoryTag::ff); + auto alu_row_index = common_validate_mul(trace, FF(20), FF(5), FF(100), FF(2), FF(0), FF(1), AvmMemoryTag::ff); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_ff_tag, FF(1)); EXPECT_EQ(alu_row.aluChip_alu_cf, FF(0)); @@ -250,7 +251,8 @@ TEST_F(AvmMiniArithmeticTestsFF, multiplicationByZero) trace_builder.return_op(0, 3); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(127), FF(0), FF(0), FF(0), FF(1), FF(2), AvmMemoryTag::ff); + auto alu_row_index = common_validate_mul(trace, FF(127), FF(0), FF(0), FF(0), FF(1), FF(2), AvmMemoryTag::ff); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_ff_tag, FF(1)); EXPECT_EQ(alu_row.aluChip_alu_cf, FF(0)); @@ -478,7 +480,8 @@ TEST_F(AvmMiniArithmeticTestsU8, multiplication) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(13), FF(15), FF(195), FF(0), FF(1), FF(2), AvmMemoryTag::u8); + auto alu_row_index = common_validate_mul(trace, FF(13), FF(15), FF(195), FF(0), FF(1), FF(2), AvmMemoryTag::u8); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u8_tag, FF(1)); @@ -500,7 +503,8 @@ TEST_F(AvmMiniArithmeticTestsU8, multiplicationOverflow) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(200), FF(170), FF(208), FF(0), FF(1), FF(2), AvmMemoryTag::u8); + auto alu_row_index = common_validate_mul(trace, FF(200), FF(170), FF(208), FF(0), FF(1), FF(2), AvmMemoryTag::u8); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u8_tag, FF(1)); @@ -612,7 +616,9 @@ TEST_F(AvmMiniArithmeticTestsU16, multiplication) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(200), FF(245), FF(49000), FF(0), FF(1), FF(2), AvmMemoryTag::u16); + auto alu_row_index = + common_validate_mul(trace, FF(200), FF(245), FF(49000), FF(0), FF(1), FF(2), AvmMemoryTag::u16); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u16_tag, FF(1)); @@ -634,7 +640,8 @@ TEST_F(AvmMiniArithmeticTestsU16, multiplicationOverflow) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(512), FF(1024), FF(0), FF(0), FF(1), FF(2), AvmMemoryTag::u16); + auto alu_row_index = common_validate_mul(trace, FF(512), FF(1024), FF(0), FF(0), FF(1), FF(2), AvmMemoryTag::u16); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u16_tag, FF(1)); @@ -754,8 +761,9 @@ TEST_F(AvmMiniArithmeticTestsU32, multiplication) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = + auto alu_row_index = common_validate_mul(trace, FF(11111), FF(11111), FF(123454321), FF(0), FF(1), FF(2), AvmMemoryTag::u32); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u32_tag, FF(1)); @@ -780,8 +788,9 @@ TEST_F(AvmMiniArithmeticTestsU32, multiplicationOverflow) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = + auto alu_row_index = common_validate_mul(trace, FF(11 << 25), FF(13 << 22), FF(0), FF(0), FF(1), FF(2), AvmMemoryTag::u32); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u32_tag, FF(1)); @@ -923,8 +932,9 @@ TEST_F(AvmMiniArithmeticTestsU64, multiplication) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul( + auto alu_row_index = common_validate_mul( trace, FF(999888777), FF(555444333), FF(555382554814950741LLU), FF(0), FF(1), FF(2), AvmMemoryTag::u64); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u64_tag, FF(1)); @@ -953,7 +963,8 @@ TEST_F(AvmMiniArithmeticTestsU64, multiplicationOverflow) trace_builder.return_op(2, 1); auto trace = trace_builder.finalize(); - auto alu_row = common_validate_mul(trace, FF(a), FF(b), FF(1), FF(0), FF(1), FF(2), AvmMemoryTag::u64); + auto alu_row_index = common_validate_mul(trace, FF(a), FF(b), FF(1), FF(0), FF(1), FF(2), AvmMemoryTag::u64); + auto alu_row = trace.at(alu_row_index); EXPECT_EQ(alu_row.aluChip_alu_u64_tag, FF(1)); @@ -978,9 +989,9 @@ TEST_F(AvmMiniArithmeticTestsU64, multiplicationOverflow) // Test on basic addition over u128 type. TEST_F(AvmMiniArithmeticTestsU128, addition) { - uint128_t const a = (uint128_t(0x5555222233334444LLU) << 64) + uint128_t(0x88889999AAAABBBBLLU); - uint128_t const b = (uint128_t(0x3333222233331111LLU) << 64) + uint128_t(0x5555111155553333LLU); - uint128_t const c = (uint128_t(0x8888444466665555LLU) << 64) + uint128_t(0xDDDDAAAAFFFFEEEELLU); + uint128_t const a = (uint128_t{ 0x5555222233334444LLU } << 64) + uint128_t{ 0x88889999AAAABBBBLLU }; + uint128_t const b = (uint128_t{ 0x3333222233331111LLU } << 64) + uint128_t{ 0x5555111155553333LLU }; + uint128_t const c = (uint128_t{ 0x8888444466665555LLU } << 64) + uint128_t{ 0xDDDDAAAAFFFFEEEELLU }; // trace_builder trace_builder.set(a, 8, AvmMemoryTag::u128); @@ -1016,10 +1027,10 @@ TEST_F(AvmMiniArithmeticTestsU128, addition) // Test on basic addition over u128 type with carry. TEST_F(AvmMiniArithmeticTestsU128, additionCarry) { - uint128_t const a = (uint128_t(UINT64_MAX) << 64) + uint128_t(UINT64_MAX) - uint128_t(72948899); - uint128_t const b = (uint128_t(UINT64_MAX) << 64) + uint128_t(UINT64_MAX) - uint128_t(36177344); + uint128_t const a = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX } - uint128_t{ 72948899 }; + uint128_t const b = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX } - uint128_t{ 36177344 }; uint128_t const c = - (uint128_t(UINT64_MAX) << 64) + uint128_t(UINT64_MAX) - uint128_t(36177345) - uint128_t(72948899); + (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX } - uint128_t{ 36177345 } - uint128_t{ 72948899 }; // trace_builder trace_builder.set(a, 8, AvmMemoryTag::u128); @@ -1055,8 +1066,8 @@ TEST_F(AvmMiniArithmeticTestsU128, additionCarry) // Test on basic subtraction over u128 type. TEST_F(AvmMiniArithmeticTestsU128, subtraction) { - uint128_t const a = (uint128_t(UINT64_MAX) << 64) + uint128_t(UINT64_MAX) - uint128_t(36177344); - uint128_t const b = (uint128_t(UINT64_MAX) << 64) + uint128_t(UINT64_MAX) - uint128_t(72948899); + uint128_t const a = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX } - uint128_t{ 36177344 }; + uint128_t const b = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX } - uint128_t{ 72948899 }; uint128_t const c = 36771555; // 72948899 - 36177344 // trace_builder @@ -1096,9 +1107,9 @@ TEST_F(AvmMiniArithmeticTestsU128, subtraction) // Test on basic subtraction over u128 type with carry. TEST_F(AvmMiniArithmeticTestsU128, subtractionCarry) { - uint128_t const a = (uint128_t(0x5555222233334444LLU) << 64) + uint128_t(0x88889999AAAABBBBLLU); - uint128_t const b = (uint128_t(0x3333222233331111LLU) << 64) + uint128_t(0x5555111155553333LLU); - uint128_t const c = (uint128_t(0x2222000000003333LLU) << 64) + uint128_t(0x3333888855558888LLU); + uint128_t const a = (uint128_t{ 0x5555222233334444LLU } << 64) + uint128_t{ 0x88889999AAAABBBBLLU }; + uint128_t const b = (uint128_t{ 0x3333222233331111LLU } << 64) + uint128_t{ 0x5555111155553333LLU }; + uint128_t const c = (uint128_t{ 0x2222000000003333LLU } << 64) + uint128_t{ 0x3333888855558888LLU }; // trace_builder trace_builder.set(a, 8, AvmMemoryTag::u128); @@ -1133,6 +1144,100 @@ TEST_F(AvmMiniArithmeticTestsU128, subtractionCarry) validate_trace_proof(std::move(trace)); } +// Test on basic multiplication over u128 type. +TEST_F(AvmMiniArithmeticTestsU128, multiplication) +{ + // trace_builder + trace_builder.set(0x38D64BF685FFBLLU, 0, AvmMemoryTag::u128); + trace_builder.set(0x1F92C762C98DFLLU, 1, AvmMemoryTag::u128); + // Integer multiplication output in HEX: 70289AEB0A7DDA0BAE60CA3A5 + FF c{ uint256_t{ 0xA7DDA0BAE60CA3A5, 0x70289AEB0, 0, 0 } }; + + trace_builder.mul(0, 1, 2, AvmMemoryTag::u128); + trace_builder.return_op(2, 1); + auto trace = trace_builder.finalize(); + + auto alu_row_index = common_validate_mul( + trace, FF(0x38D64BF685FFBLLU), FF(555444333222111LLU), c, FF(0), FF(1), FF(2), AvmMemoryTag::u128); + auto alu_row_first = trace.at(alu_row_index); + + EXPECT_EQ(alu_row_first.aluChip_alu_u128_tag, FF(1)); + + // Decomposition of the first operand in 16-bit registers + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r0, FF(0x5FFB)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r1, FF(0xBF68)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r2, FF(0x8D64)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r3, FF(0x3)); + + // Decomposition of the second operand in 16-bit registers + auto alu_row_second = trace.at(alu_row_index + 1); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r0, FF(0x98DF)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r1, FF(0x762C)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r2, FF(0xF92C)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r3, FF(0x1)); + validate_trace_proof(std::move(trace)); +} + +// Test on multiplication over u128 type with overflow. +TEST_F(AvmMiniArithmeticTestsU128, multiplicationOverflow) +{ + // (2^128 - 2) * (2^128 - 4) = 2^256 - 2^130 - 2^129 + 2^3 + // The above modulo 2^128 = 8 + uint128_t const a = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX - 1 }; + uint128_t const b = (uint128_t{ UINT64_MAX } << 64) + uint128_t{ UINT64_MAX - 3 }; + + // trace_builder + trace_builder.set(a, 0, AvmMemoryTag::u128); + trace_builder.set(b, 1, AvmMemoryTag::u128); + + trace_builder.mul(0, 1, 2, AvmMemoryTag::u128); + trace_builder.return_op(2, 1); + auto trace = trace_builder.finalize(); + + auto alu_row_index = common_validate_mul(trace, + FF{ uint256_t::from_uint128(a) }, + FF{ uint256_t::from_uint128(b) }, + FF{ 8 }, + FF(0), + FF(1), + FF(2), + AvmMemoryTag::u128); + auto alu_row_first = trace.at(alu_row_index); + + EXPECT_EQ(alu_row_first.aluChip_alu_u128_tag, FF(1)); + + // Decomposition of the first operand in 16-bit registers + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r0, FF(0xFFFE)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r1, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r2, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r3, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r4, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r5, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r6, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.aluChip_alu_u16_r7, FF(UINT16_MAX)); + + // Decomposition of the second operand in 16-bit registers + auto alu_row_second = trace.at(alu_row_index + 1); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r0, FF(0xFFFC)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r1, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r2, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r3, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r4, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r5, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r6, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_second.aluChip_alu_u16_r7, FF(UINT16_MAX)); + + // Other registers involved in the relevant relations + // PIL relation (alu_chip.pil): a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c + // (2^128 - 2) * (2^64 - 4) + (2^64 - 2) * (2^64 - 1) * 2^64 = + // 2 * 2^192 + (- 4 - 2 - 1) * 2^128 + (-2 + 2) * 2^64 + 8 = (2^65 - 7) * 2^128 + 8 + // Therefore, CF = 1 and R' = 2^64 - 7 + EXPECT_EQ(alu_row_first.aluChip_alu_u64_r0, FF{ UINT64_MAX - 6 }); // 2^64 - 7 + EXPECT_EQ(alu_row_first.aluChip_alu_cf, FF(1)); + + validate_trace_proof(std::move(trace)); +} + /****************************************************************************** * * NEGATIVE TESTS - Finite Field Type