From a079c7d9407a1171725190009c237e9942bf60d6 Mon Sep 17 00:00:00 2001 From: IlyasRidhuan Date: Fri, 3 May 2024 11:32:43 +0000 Subject: [PATCH] chore: comments + execution --- barretenberg/cpp/pil/avm/avm_alu.pil | 9 +++-- .../relations/generated/avm/avm_alu.hpp | 38 +++++++++++-------- .../vm/avm_trace/avm_execution.cpp | 6 +++ 3 files changed, 34 insertions(+), 19 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 7d37492a33a0..06fb4ad4f25a 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -654,24 +654,25 @@ namespace avm_alu(256); // To show this, we constrain ib - ia - 1 to be within 128-bits // Since we need a range check we use the existing a_lo column that is range checked over 128-bits op_div_a_lt_b * (a_lo - (ib - ia - 1)) = 0; - op_div_a_lt_b * ic * (ia - remainder) = 0; + op_div_a_lt_b * ic = 0; // ic = 0 + op_div_a_lt_b * (ia - remainder) = 0; // remainder = a, might not be needed. // ====== Handling ia > ib ===== pol commit op_div_std; op_div_std * (1 - op_div_std) = 0; - pol PRODUCT = ib * ic; // This can be up to a 256-bit number + pol PRODUCT = ib * ic; // This number can be up to 256-bits long // We need to check that this value has not overflowed the field. // (1) Decompose ib * ic into two 128-bit limbs, we will re-use the a_lo and a_hi columns. - // (2) Perform a 128-bit range check, over these two limbs. + // (2) Perform a 128-bit range check, over these two limbs. Again re-using the a_lo and a_hi columns. // (3) Perform the primality check, we re-use the p_sub_a_lo and p_sub_a_hi columns. // Check that a_lo and a_hi correctly represent PRODUCT #[ALU_PROD_DIV] op_div_std * (PRODUCT - (a_lo + 2 ** 128 * a_hi)) = 0; // Range checks already performed via a_lo and a_hi - // Primality checks already performed above p_sub_a_lo and p_sub_a_hi + // Primality checks already performed above via p_sub_a_lo and p_sub_a_hi //Range check remainder < ib and put the value in b_lo, it has to fit into a 128-bit range check // b_hi is zero, TODO: does it need to be enforced as zero? diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp index a54afe296ffe..b25a83910bd7 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -234,16 +234,16 @@ inline std::string get_relation_label_avm_alu(int index) case 64: return "SHL_OUTPUT"; - case 70: + case 71: return "ALU_PROD_DIV"; - case 71: + case 72: return "REMAINDER_RANGE_CHK"; - case 73: + case 74: return "CMP_CTR_REL_3"; - case 75: + case 76: return "DIVISION_RELATION"; } return std::to_string(index); @@ -253,10 +253,10 @@ template class avm_aluImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4, 3, 4, 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 2, 5, - 3, 3, 4, 4, 4, 4, 4, 3, 5, 5, 4, 5, 5, 2, 3, 3, 4, 3, 4, 3, 3, 3, 3, 4, + 3, 3, 4, 4, 4, 4, 4, 3, 5, 5, 4, 5, 5, 2, 3, 3, 3, 3, 3, 4, 3, 3, 3, 3, 4, }; template @@ -1009,7 +1009,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(68); - auto tmp = ((avm_alu_op_div_a_lt_b * avm_alu_ic) * (avm_alu_ia - avm_alu_remainder)); + auto tmp = (avm_alu_op_div_a_lt_b * avm_alu_ic); tmp *= scaling_factor; std::get<68>(evals) += tmp; } @@ -1017,7 +1017,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(69); - auto tmp = (avm_alu_op_div_std * (-avm_alu_op_div_std + FF(1))); + auto tmp = (avm_alu_op_div_a_lt_b * (avm_alu_ia - avm_alu_remainder)); tmp *= scaling_factor; std::get<69>(evals) += tmp; } @@ -1025,8 +1025,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(70); - auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - - (avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))))); + auto tmp = (avm_alu_op_div_std * (-avm_alu_op_div_std + FF(1))); tmp *= scaling_factor; std::get<70>(evals) += tmp; } @@ -1034,7 +1033,8 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(71); - auto tmp = (avm_alu_op_div_std * (avm_alu_b_lo - ((avm_alu_ib - avm_alu_remainder) - FF(1)))); + auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - + (avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))))); tmp *= scaling_factor; std::get<71>(evals) += tmp; } @@ -1042,7 +1042,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(72); - auto tmp = (avm_alu_op_div_std * avm_alu_b_hi); + auto tmp = (avm_alu_op_div_std * (avm_alu_b_lo - ((avm_alu_ib - avm_alu_remainder) - FF(1)))); tmp *= scaling_factor; std::get<72>(evals) += tmp; } @@ -1050,7 +1050,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(73); - auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(2)) * avm_alu_op_div_std); + auto tmp = (avm_alu_op_div_std * avm_alu_b_hi); tmp *= scaling_factor; std::get<73>(evals) += tmp; } @@ -1058,7 +1058,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(74); - auto tmp = (avm_alu_rng_chk_sel * avm_alu_op_div_std); + auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(2)) * avm_alu_op_div_std); tmp *= scaling_factor; std::get<74>(evals) += tmp; } @@ -1066,10 +1066,18 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(75); - auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - (avm_alu_ia - avm_alu_remainder))); + auto tmp = (avm_alu_rng_chk_sel * avm_alu_op_div_std); tmp *= scaling_factor; std::get<75>(evals) += tmp; } + // Contribution 76 + { + Avm_DECLARE_VIEWS(76); + + auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - (avm_alu_ia - avm_alu_remainder))); + tmp *= scaling_factor; + std::get<76>(evals) += tmp; + } } }; diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp index 7cf6154fac89..8386dfe738c8 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp @@ -110,6 +110,12 @@ std::vector Execution::gen_trace(std::vector const& instructio std::get(inst.operands.at(2)), std::get(inst.operands.at(3))); break; + case OpCode::DIV: + trace_builder.op_div(std::get(inst.operands.at(0)), + std::get(inst.operands.at(1)), + std::get(inst.operands.at(2)), + std::get(inst.operands.at(3))); + break; // Compute - Comparators case OpCode::EQ: trace_builder.op_eq(std::get(inst.operands.at(0)),