diff --git a/barretenberg/cpp/pil/avm/avm_mini.pil b/barretenberg/cpp/pil/avm/avm_mini.pil index 3bd9bc11b86..1fca367bf95 100644 --- a/barretenberg/cpp/pil/avm/avm_mini.pil +++ b/barretenberg/cpp/pil/avm/avm_mini.pil @@ -21,8 +21,12 @@ namespace avmMini(256); // DIV pol commit sel_op_div; - // Error boolean flag pertaining to an operation - pol commit op_err; + // Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field) + pol commit in_tag; + + // Errors + pol commit op_err; // Boolean flag pertaining to an operation error + pol commit tag_err; // Boolean flag (foreign key to memTrace.m_tag_err) // A helper witness being the inverse of some value // to show a non-zero equality @@ -49,8 +53,8 @@ namespace avmMini(256); pol commit mem_idx_a; pol commit mem_idx_b; pol commit mem_idx_c; - - + + // Track the last line of the execution trace. It does NOT correspond to the last row of the whole table // of size N. As this depends on the supplied bytecode, this polynomial cannot be constant. pol commit last; @@ -63,6 +67,7 @@ namespace avmMini(256); sel_op_div * (1 - sel_op_div) = 0; op_err * (1 - op_err) = 0; + tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)? mem_op_a * (1 - mem_op_a) = 0; mem_op_b * (1 - mem_op_b) = 0; @@ -72,23 +77,38 @@ namespace avmMini(256); rwb * (1 - rwb) = 0; rwc * (1 - rwc) = 0; + // TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6 + + // Set intermediate registers to 0 whenever tag_err occurs + tag_err * ia = 0; + tag_err * ib = 0; + tag_err * ic = 0; + // Relation for addition over the finite field + #[SUBOP_ADDITION_FF] sel_op_add * (ia + ib - ic) = 0; // Relation for subtraction over the finite field + #[SUBOP_SUBTRACTION_FF] sel_op_sub * (ia - ib - ic) = 0; // Relation for multiplication over the finite field + #[SUBOP_MULTIPLICATION_FF] sel_op_mul * (ia * ib - ic) = 0; // Relation for division over the finite field + // If tag_err == 1 in a division, then ib == 0 and op_err == 1. + #[SUBOP_DIVISION_FF] sel_op_div * (1 - op_err) * (ic * ib - ia) = 0; // When sel_op_div == 1, we want ib == 0 <==> op_err == 1 // This can be achieved with the 2 following relations. // inv is an extra witness to show that we can invert ib, i.e., inv = ib^(-1) - // If ib == 0, we have to set inv = 1 to satisfy the second relation. + // If ib == 0, we have to set inv = 1 to satisfy the second relation, + // because op_err == 1 from the first relation. + #[SUBOP_DIVISION_ZERO_ERR1] sel_op_div * (ib * inv - 1 + op_err) = 0; + #[SUBOP_DIVISION_ZERO_ERR2] sel_op_div * op_err * (1 - inv) = 0; // op_err cannot be maliciously activated for a non-relevant @@ -97,9 +117,10 @@ namespace avmMini(256); // Note that the above is even a stronger constraint, as it shows // that exactly one sel_op_XXX must be true. // At this time, we have only division producing an error. + #[SUBOP_ERROR_RELEVANT_OP] op_err * (sel_op_div - 1) = 0; - // TODO: constraint that we stop execution at the first error + // TODO: constraint that we stop execution at the first error (tag_err or op_err) // An error can only happen at the last sub-operation row. // OPEN/POTENTIAL OPTIMIZATION: Dedicated error per relevant operation? @@ -108,4 +129,10 @@ namespace avmMini(256); // Same for the relations related to the error activation: // (ib * inv - 1 + op_div_err) = 0 && op_err * (1 - inv) = 0 // This works in combination with op_div_err * (sel_op_div - 1) = 0; - // Drawback is the need to paralllelize the latter. \ No newline at end of file + // Drawback is the need to paralllelize the latter. + + // Inter-table Constraints + + // TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk} + // TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like: + // mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw} \ No newline at end of file diff --git a/barretenberg/cpp/pil/avm/avm_mini_opt.pil b/barretenberg/cpp/pil/avm/avm_mini_opt.pil index 56019fb7197..f3a75411a99 100644 --- a/barretenberg/cpp/pil/avm/avm_mini_opt.pil +++ b/barretenberg/cpp/pil/avm/avm_mini_opt.pil @@ -2,13 +2,24 @@ namespace memTrace(256); col witness m_clk; col witness m_sub_clk; col witness m_addr; + col witness m_tag; col witness m_val; col witness m_lastAccess; + col witness m_last; col witness m_rw; + col witness m_in_tag; + col witness m_tag_err; + col witness m_one_min_inv; (memTrace.m_lastAccess * (1 - memTrace.m_lastAccess)) = 0; + (memTrace.m_last * (1 - memTrace.m_last)) = 0; (memTrace.m_rw * (1 - memTrace.m_rw)) = 0; - (((1 - avmMini.first) * (1 - memTrace.m_lastAccess)) * (memTrace.m_addr' - memTrace.m_addr)) = 0; - (((((1 - avmMini.first) * (1 - avmMini.last)) * (1 - memTrace.m_lastAccess)) * (1 - memTrace.m_rw')) * (memTrace.m_val' - memTrace.m_val)) = 0; + (memTrace.m_tag_err * (1 - memTrace.m_tag_err)) = 0; + ((1 - memTrace.m_lastAccess) * (memTrace.m_addr' - memTrace.m_addr)) = 0; + (((1 - memTrace.m_lastAccess) * (1 - memTrace.m_rw')) * (memTrace.m_val' - memTrace.m_val)) = 0; + (((1 - memTrace.m_lastAccess) * (1 - memTrace.m_rw')) * (memTrace.m_tag' - memTrace.m_tag)) = 0; + ((memTrace.m_lastAccess * (1 - memTrace.m_rw')) * memTrace.m_val') = 0; + ((memTrace.m_in_tag - memTrace.m_tag) * (1 - memTrace.m_one_min_inv)) = memTrace.m_tag_err; + ((1 - memTrace.m_tag_err) * memTrace.m_one_min_inv) = 0; namespace avmMini(256); col fixed clk(i) { i }; col fixed first = [1] + [0]*; @@ -16,7 +27,9 @@ namespace avmMini(256); col witness sel_op_sub; col witness sel_op_mul; col witness sel_op_div; + col witness in_tag; col witness op_err; + col witness tag_err; col witness inv; col witness ia; col witness ib; @@ -36,12 +49,16 @@ namespace avmMini(256); (avmMini.sel_op_mul * (1 - avmMini.sel_op_mul)) = 0; (avmMini.sel_op_div * (1 - avmMini.sel_op_div)) = 0; (avmMini.op_err * (1 - avmMini.op_err)) = 0; + (avmMini.tag_err * (1 - avmMini.tag_err)) = 0; (avmMini.mem_op_a * (1 - avmMini.mem_op_a)) = 0; (avmMini.mem_op_b * (1 - avmMini.mem_op_b)) = 0; (avmMini.mem_op_c * (1 - avmMini.mem_op_c)) = 0; (avmMini.rwa * (1 - avmMini.rwa)) = 0; (avmMini.rwb * (1 - avmMini.rwb)) = 0; (avmMini.rwc * (1 - avmMini.rwc)) = 0; + (avmMini.tag_err * avmMini.ia) = 0; + (avmMini.tag_err * avmMini.ib) = 0; + (avmMini.tag_err * avmMini.ic) = 0; (avmMini.sel_op_add * ((avmMini.ia + avmMini.ib) - avmMini.ic)) = 0; (avmMini.sel_op_sub * ((avmMini.ia - avmMini.ib) - avmMini.ic)) = 0; (avmMini.sel_op_mul * ((avmMini.ia * avmMini.ib) - avmMini.ic)) = 0; diff --git a/barretenberg/cpp/pil/avm/mem_trace.pil b/barretenberg/cpp/pil/avm/mem_trace.pil index 38cc0813d2c..33a8a20ad06 100644 --- a/barretenberg/cpp/pil/avm/mem_trace.pil +++ b/barretenberg/cpp/pil/avm/mem_trace.pil @@ -7,29 +7,50 @@ namespace memTrace(256); pol commit m_clk; pol commit m_sub_clk; pol commit m_addr; + pol commit m_tag; // Memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field) pol commit m_val; pol commit m_lastAccess; // Boolean (1 when this row is the last of a given address) + pol commit m_last; // Boolean indicating the last row of the memory trace (not execution trace) pol commit m_rw; // Enum: 0 (read), 1 (write) - + + pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avmMini.in_tag) + + // Error columns + pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected) + + // Helper columns + pol commit m_one_min_inv; // Extra value to prove m_in_tag != m_tag with error handling + // Type constraints m_lastAccess * (1 - m_lastAccess) = 0; + m_last * (1 - m_last) = 0; m_rw * (1 - m_rw) = 0; - + m_tag_err * (1 - m_tag_err) = 0; + + // TODO: m_addr is u32 and 0 <= m_tag <= 6 + // (m_in_tag will be constrained through inclusion check to main trace) + + // Remark: m_lastAccess == 1 on first row and therefore any relation with the + // multiplicative term (1 - m_lastAccess) implicitly includes (1 - avmMini.first) + // Similarly, this includes (1 - m_last) as well. + // m_lastAccess == 0 ==> m_addr' == m_addr - (1 - avmMini.first) * (1 - m_lastAccess) * (m_addr' - m_addr) = 0; + // Optimization: We removed the term (1 - avmMini.first) + #[MEM_LAST_ACCESS_DELIMITER] + (1 - m_lastAccess) * (m_addr' - m_addr) = 0; // We need: m_lastAccess == 1 ==> m_addr' > m_addr // The above implies: m_addr' == m_addr ==> m_lastAccess == 0 // This condition does not apply on the last row. // clk + 1 used as an expression for positive integers // TODO: Uncomment when lookups are supported - // (1 - first) * (1 - last) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported? + // (1 - first) * (1 - m_last) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported? // TODO: following constraint // m_addr' == m_addr && m_clk == m_clk' ==> m_sub_clk' - m_sub_clk > 0 - // Can be enforced with (1 - first) * (1 - last) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1 + // Can be enforced with (1 - first) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1 - // Alternatively to the above, one could require + // Alternatively to the above, one could require // that m_addr' - m_addr is 0 or 1 (needs to add placeholders m_addr values): // (m_addr' - m_addr) * (m_addr' - m_addr) - (m_addr' - m_addr) = 0; // if m_addr' - m_addr is 0 or 1, the following is equiv. to m_lastAccess @@ -40,8 +61,46 @@ namespace memTrace(256); // Note: in barretenberg, a shifted polynomial will be 0 on the last row (shift is not cyclic) // Note2: in barretenberg, if a poynomial is shifted, its non-shifted equivalent must be 0 on the first row - (1 - avmMini.first) * (1 - avmMini.last) * (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0; + // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last) + #[MEM_READ_WRITE_VAL_CONSISTENCY] + (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0; - // TODO: Constraint the first load from a given adress has value 0. (Consistency of memory initialization.) + // m_lastAccess == 0 && m_rw' == 0 ==> m_tag == m_tag' + // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last) + #[MEM_READ_WRITE_TAG_CONSISTENCY] + (1 - m_lastAccess) * (1 - m_rw') * (m_tag' - m_tag) = 0; + + // Constrain that the first load from a given address has value 0. (Consistency of memory initialization.) + // We do not constrain that the m_tag == 0 as the 0 value is compatible with any memory type. + // If we set m_lastAccess = 1 on the first row, we can enforce this (should be ok as long as we do not shift m_lastAccess): + #[MEM_ZERO_INIT] + m_lastAccess * (1 - m_rw') * m_val' = 0; + + // Memory tag consistency check + // We want to prove that m_in_tag == m_tag <==> m_tag_err == 0 + // We want to show that we can invert (m_in_tag - m_tag) when m_tag_err == 1, + // i.e., m_tag_err == 1 ==> m_in_tag != m_tag + // For this purpose, we need an extra column to store a witness + // which can be used to show that (m_in_tag - m_tag) is invertible (non-zero). + // We re-use the same zero (non)-equality technique as in SUBOP_DIVISION_ZERO_ERR1/2 applied + // to (m_in_tag - m_tag) by replacing m_tag_err by 1 - m_tag_err because here + // the equality to zero is not an error. Another modification + // consists in storing 1 - (m_in_tag - m_tag)^(-1) in the extra witness column + // instead of (m_in_tag - m_tag)^(-1) as this allows to store zero by default (i.e., when m_tag_err == 0). + // The new column m_one_min_inv is set to 1 - (m_in_tag - m_tag)^(-1) when m_tag_err == 1 + // but must be set to 0 when tags are matching and m_tag_err = 0 + #[MEM_IN_TAG_CONSISTENCY_1] + (m_in_tag - m_tag) * (1 - m_one_min_inv) - m_tag_err = 0; + #[MEM_IN_TAG_CONSISTENCY_2] + (1 - m_tag_err) * m_one_min_inv = 0; + + // Correctness of two above checks MEM_IN_TAG_CONSISTENCY_1/2: + // m_in_tag == m_tag ==> m_tag_err == 0 (first relation) + // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 0 + // TODO: when introducing load/store as sub-operations, we will have to add consistency of intermediate - // register values ia, ib, ic \ No newline at end of file + // register values ia, ib, ic + + // Inter-table Constraints + + // TODO: {m_clk, m_in_tag} IN {avmMini.clk, avmMini.in_tag} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index 99b7f32f207..f986f97f168 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -36,11 +36,11 @@ class AvmMiniFlavor { using VerifierCommitmentKey = pcs::VerifierCommitmentKey; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; - static constexpr size_t NUM_WITNESS_ENTITIES = 25; + static constexpr size_t NUM_WITNESS_ENTITIES = 32; static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES; // We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for // the unshifted and one for the shifted - static constexpr size_t NUM_ALL_ENTITIES = 30; + static constexpr size_t NUM_ALL_ENTITIES = 38; using Relations = std::tuple, AvmMini_vm::avm_mini>; @@ -79,14 +79,21 @@ class AvmMiniFlavor { memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, + memTrace_m_tag, memTrace_m_val, memTrace_m_lastAccess, + memTrace_m_last, memTrace_m_rw, + memTrace_m_in_tag, + memTrace_m_tag_err, + memTrace_m_one_min_inv, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div, + avmMini_in_tag, avmMini_op_err, + avmMini_tag_err, avmMini_inv, avmMini_ia, avmMini_ib, @@ -104,13 +111,38 @@ class AvmMiniFlavor { RefVector get_wires() { - return { - memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, memTrace_m_val, memTrace_m_lastAccess, - memTrace_m_rw, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div, - avmMini_op_err, avmMini_inv, avmMini_ia, avmMini_ib, avmMini_ic, - avmMini_mem_op_a, avmMini_mem_op_b, avmMini_mem_op_c, avmMini_rwa, avmMini_rwb, - avmMini_rwc, avmMini_mem_idx_a, avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last - }; + return { memTrace_m_clk, + memTrace_m_sub_clk, + memTrace_m_addr, + memTrace_m_tag, + memTrace_m_val, + memTrace_m_lastAccess, + memTrace_m_last, + memTrace_m_rw, + memTrace_m_in_tag, + memTrace_m_tag_err, + memTrace_m_one_min_inv, + avmMini_sel_op_add, + avmMini_sel_op_sub, + avmMini_sel_op_mul, + avmMini_sel_op_div, + avmMini_in_tag, + avmMini_op_err, + avmMini_tag_err, + avmMini_inv, + avmMini_ia, + avmMini_ib, + avmMini_ic, + avmMini_mem_op_a, + avmMini_mem_op_b, + avmMini_mem_op_c, + avmMini_rwa, + avmMini_rwb, + avmMini_rwc, + avmMini_mem_idx_a, + avmMini_mem_idx_b, + avmMini_mem_idx_c, + avmMini_last }; }; RefVector get_sorted_polynomials() { return {}; }; }; @@ -123,14 +155,21 @@ class AvmMiniFlavor { memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, + memTrace_m_tag, memTrace_m_val, memTrace_m_lastAccess, + memTrace_m_last, memTrace_m_rw, + memTrace_m_in_tag, + memTrace_m_tag_err, + memTrace_m_one_min_inv, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div, + avmMini_in_tag, avmMini_op_err, + avmMini_tag_err, avmMini_inv, avmMini_ia, avmMini_ib, @@ -145,9 +184,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_rw_shift, + memTrace_m_val_shift, memTrace_m_addr_shift, - memTrace_m_val_shift) + memTrace_m_rw_shift, + memTrace_m_tag_shift) RefVector get_wires() { @@ -156,14 +196,21 @@ class AvmMiniFlavor { memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, + memTrace_m_tag, memTrace_m_val, memTrace_m_lastAccess, + memTrace_m_last, memTrace_m_rw, + memTrace_m_in_tag, + memTrace_m_tag_err, + memTrace_m_one_min_inv, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div, + avmMini_in_tag, avmMini_op_err, + avmMini_tag_err, avmMini_inv, avmMini_ia, avmMini_ib, @@ -178,9 +225,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_rw_shift, + memTrace_m_val_shift, memTrace_m_addr_shift, - memTrace_m_val_shift }; + memTrace_m_rw_shift, + memTrace_m_tag_shift }; }; RefVector get_unshifted() { @@ -189,14 +237,21 @@ class AvmMiniFlavor { memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, + memTrace_m_tag, memTrace_m_val, memTrace_m_lastAccess, + memTrace_m_last, memTrace_m_rw, + memTrace_m_in_tag, + memTrace_m_tag_err, + memTrace_m_one_min_inv, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div, + avmMini_in_tag, avmMini_op_err, + avmMini_tag_err, avmMini_inv, avmMini_ia, avmMini_ib, @@ -212,10 +267,13 @@ class AvmMiniFlavor { avmMini_mem_idx_c, avmMini_last }; }; - RefVector get_to_be_shifted() { return { memTrace_m_rw, memTrace_m_addr, memTrace_m_val }; }; + RefVector get_to_be_shifted() + { + return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag }; + }; RefVector get_shifted() { - return { memTrace_m_rw_shift, memTrace_m_addr_shift, memTrace_m_val_shift }; + return { memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_tag_shift }; }; }; @@ -228,13 +286,9 @@ class AvmMiniFlavor { RefVector get_to_be_shifted() { - return { - memTrace_m_rw, - memTrace_m_addr, - memTrace_m_val, - - }; + return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag }; }; + // The plookup wires that store plookup read data. std::array get_table_column_wires() { return {}; }; }; @@ -261,7 +315,7 @@ class AvmMiniFlavor { ProverPolynomials(ProverPolynomials&& o) noexcept = default; ProverPolynomials& operator=(ProverPolynomials&& o) noexcept = default; ~ProverPolynomials() = default; - [[nodiscard]] size_t get_polynomial_size() const { return avmMini_clk.size(); } + [[nodiscard]] size_t get_polynomial_size() const { return memTrace_m_clk.size(); } /** * @brief Returns the evaluations of all prover polynomials at one point on the boolean hypercube, which * represents one row in the execution trace. @@ -275,6 +329,7 @@ class AvmMiniFlavor { return result; } }; + using RowPolynomials = AllEntities; class PartiallyEvaluatedMultivariates : public AllEntities { @@ -313,14 +368,21 @@ class AvmMiniFlavor { Base::memTrace_m_clk = "MEMTRACE_M_CLK"; Base::memTrace_m_sub_clk = "MEMTRACE_M_SUB_CLK"; Base::memTrace_m_addr = "MEMTRACE_M_ADDR"; + Base::memTrace_m_tag = "MEMTRACE_M_TAG"; Base::memTrace_m_val = "MEMTRACE_M_VAL"; Base::memTrace_m_lastAccess = "MEMTRACE_M_LASTACCESS"; + Base::memTrace_m_last = "MEMTRACE_M_LAST"; Base::memTrace_m_rw = "MEMTRACE_M_RW"; + Base::memTrace_m_in_tag = "MEMTRACE_M_IN_TAG"; + Base::memTrace_m_tag_err = "MEMTRACE_M_TAG_ERR"; + Base::memTrace_m_one_min_inv = "MEMTRACE_M_ONE_MIN_INV"; Base::avmMini_sel_op_add = "AVMMINI_SEL_OP_ADD"; Base::avmMini_sel_op_sub = "AVMMINI_SEL_OP_SUB"; Base::avmMini_sel_op_mul = "AVMMINI_SEL_OP_MUL"; Base::avmMini_sel_op_div = "AVMMINI_SEL_OP_DIV"; + Base::avmMini_in_tag = "AVMMINI_IN_TAG"; Base::avmMini_op_err = "AVMMINI_OP_ERR"; + Base::avmMini_tag_err = "AVMMINI_TAG_ERR"; Base::avmMini_inv = "AVMMINI_INV"; Base::avmMini_ia = "AVMMINI_IA"; Base::avmMini_ib = "AVMMINI_IB"; @@ -357,14 +419,21 @@ class AvmMiniFlavor { Commitment memTrace_m_clk; Commitment memTrace_m_sub_clk; Commitment memTrace_m_addr; + Commitment memTrace_m_tag; Commitment memTrace_m_val; Commitment memTrace_m_lastAccess; + Commitment memTrace_m_last; Commitment memTrace_m_rw; + Commitment memTrace_m_in_tag; + Commitment memTrace_m_tag_err; + Commitment memTrace_m_one_min_inv; Commitment avmMini_sel_op_add; Commitment avmMini_sel_op_sub; Commitment avmMini_sel_op_mul; Commitment avmMini_sel_op_div; + Commitment avmMini_in_tag; Commitment avmMini_op_err; + Commitment avmMini_tag_err; Commitment avmMini_inv; Commitment avmMini_ia; Commitment avmMini_ib; @@ -401,14 +470,21 @@ class AvmMiniFlavor { memTrace_m_clk = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); memTrace_m_sub_clk = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); memTrace_m_addr = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + memTrace_m_tag = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); memTrace_m_val = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); memTrace_m_lastAccess = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + memTrace_m_last = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); memTrace_m_rw = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + memTrace_m_in_tag = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + memTrace_m_tag_err = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + memTrace_m_one_min_inv = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_sel_op_add = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_sel_op_sub = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_sel_op_mul = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_sel_op_div = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + avmMini_in_tag = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_op_err = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); + avmMini_tag_err = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_inv = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_ia = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); avmMini_ib = deserialize_from_buffer(Transcript::proof_data, num_bytes_read); @@ -449,14 +525,21 @@ class AvmMiniFlavor { serialize_to_buffer(memTrace_m_clk, Transcript::proof_data); serialize_to_buffer(memTrace_m_sub_clk, Transcript::proof_data); serialize_to_buffer(memTrace_m_addr, Transcript::proof_data); + serialize_to_buffer(memTrace_m_tag, Transcript::proof_data); serialize_to_buffer(memTrace_m_val, Transcript::proof_data); serialize_to_buffer(memTrace_m_lastAccess, Transcript::proof_data); + serialize_to_buffer(memTrace_m_last, Transcript::proof_data); serialize_to_buffer(memTrace_m_rw, Transcript::proof_data); + serialize_to_buffer(memTrace_m_in_tag, Transcript::proof_data); + serialize_to_buffer(memTrace_m_tag_err, Transcript::proof_data); + serialize_to_buffer(memTrace_m_one_min_inv, Transcript::proof_data); serialize_to_buffer(avmMini_sel_op_add, Transcript::proof_data); serialize_to_buffer(avmMini_sel_op_sub, Transcript::proof_data); serialize_to_buffer(avmMini_sel_op_mul, Transcript::proof_data); serialize_to_buffer(avmMini_sel_op_div, Transcript::proof_data); + serialize_to_buffer(avmMini_in_tag, Transcript::proof_data); serialize_to_buffer(avmMini_op_err, Transcript::proof_data); + serialize_to_buffer(avmMini_tag_err, Transcript::proof_data); serialize_to_buffer(avmMini_inv, Transcript::proof_data); serialize_to_buffer(avmMini_ia, Transcript::proof_data); serialize_to_buffer(avmMini_ib, Transcript::proof_data); diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp index 401ad709c43..e3ee39cff93 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp @@ -23,13 +23,25 @@ void log_avmMini_trace(std::vector const& trace, size_t beg, size_t end) info("== ROW ", i); info("================================================================================"); + info("=======MEMORY TRACE============================================================="); info("m_addr: ", trace.at(i).memTrace_m_addr); info("m_clk: ", trace.at(i).memTrace_m_clk); info("m_sub_clk: ", trace.at(i).memTrace_m_sub_clk); info("m_val: ", trace.at(i).memTrace_m_val); - info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess); info("m_rw: ", trace.at(i).memTrace_m_rw); + info("m_tag: ", trace.at(i).memTrace_m_tag); + info("m_in_tag: ", trace.at(i).memTrace_m_in_tag); + info("m_tag_err: ", trace.at(i).memTrace_m_tag_err); + info("m_one_min_inv:", trace.at(i).memTrace_m_one_min_inv); + + info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess); + info("m_last: ", trace.at(i).memTrace_m_last); info("m_val_shift: ", trace.at(i).memTrace_m_val_shift); + + info("=======MAIN TRACE==============================================================="); + info("ia: ", trace.at(i).avmMini_ia); + info("ib: ", trace.at(i).avmMini_ib); + info("ic: ", trace.at(i).avmMini_ic); info("first: ", trace.at(i).avmMini_first); info("last: ", trace.at(i).avmMini_last); @@ -37,19 +49,16 @@ void log_avmMini_trace(std::vector const& trace, size_t beg, size_t end) info("clk: ", trace.at(i).avmMini_clk); info("mem_op_a: ", trace.at(i).avmMini_mem_op_a); info("mem_idx_a: ", trace.at(i).avmMini_mem_idx_a); - info("ia: ", trace.at(i).avmMini_ia); info("rwa: ", trace.at(i).avmMini_rwa); info("=======MEM_OP_B================================================================="); info("mem_op_b: ", trace.at(i).avmMini_mem_op_b); info("mem_idx_b: ", trace.at(i).avmMini_mem_idx_b); - info("ib: ", trace.at(i).avmMini_ib); info("rwb: ", trace.at(i).avmMini_rwb); info("=======MEM_OP_C================================================================="); info("mem_op_c: ", trace.at(i).avmMini_mem_op_c); info("mem_idx_c: ", trace.at(i).avmMini_mem_idx_c); - info("ic: ", trace.at(i).avmMini_ic); info("rwc: ", trace.at(i).avmMini_rwc); info("\n"); } diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.cpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.cpp index 8562a72c41c..fd4c46ffef5 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.cpp @@ -31,7 +31,7 @@ void AvmMiniTraceBuilder::reset() { mainTrace.clear(); memTrace.clear(); - ffMemory.fill(FF(0)); + memory.fill(FF(0)); } /** @@ -68,127 +68,135 @@ bool AvmMiniTraceBuilder::compareMemEntries(const MemoryTraceEntry& left, const * @param m_sub_clk Sub-clock used to order load/store sub operations * @param m_addr Address pertaining to the memory operation * @param m_val Value (FF) pertaining to the memory operation + * @param m_in_tag Memory tag pertaining to the instruction * @param m_rw Boolean telling whether it is a load (false) or store operation (true). */ -void AvmMiniTraceBuilder::insertInMemTrace(uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, bool m_rw) +void AvmMiniTraceBuilder::insertInMemTrace( + uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, AvmMemoryTag m_in_tag, bool m_rw) { memTrace.emplace_back(MemoryTraceEntry{ .m_clk = m_clk, .m_sub_clk = m_sub_clk, .m_addr = m_addr, .m_val = m_val, + .m_tag = m_in_tag, + .m_in_tag = m_in_tag, .m_rw = m_rw, }); } -// Memory operations need to be performed before the addition of the corresponding row in -// ainTrace, otherwise the m_clk value will be wrong.This applies to : loadAInMemTrace, loadBInMemTrace, -// loadCInMemTrace -// storeAInMemTrace, storeBInMemTrace, storeCInMemTrace -/** - * @brief Add a memory trace entry corresponding to a memory load into the intermediate - * register Ia. - * - * @param addr The memory address - * @param val The value to be loaded - */ -void AvmMiniTraceBuilder::loadAInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::loadMismatchTagInMemTrace( + uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, AvmMemoryTag m_in_tag, AvmMemoryTag m_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_A, addr, val, false); + FF one_min_inv = FF(1) - (FF(static_cast(m_in_tag)) - FF(static_cast(m_tag))).invert(); + memTrace.emplace_back(MemoryTraceEntry{ .m_clk = m_clk, + .m_sub_clk = m_sub_clk, + .m_addr = m_addr, + .m_val = m_val, + .m_tag = m_tag, + .m_in_tag = m_in_tag, + .m_tag_err = true, + .m_one_min_inv = one_min_inv }); } -/** - * @brief Add a memory trace entry corresponding to a memory load into the intermediate - * register Ib. - * - * @param addr The memory address - * @param val The value to be loaded - */ -void AvmMiniTraceBuilder::loadBInMemTrace(uint32_t addr, FF val) -{ - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_B, addr, val, false); -} +// Memory operations need to be performed before the addition of the corresponding row in +// MainTrace, otherwise the m_clk value will be wrong. This applies to loadInMemTrace and +// storeInMemTrace. /** * @brief Add a memory trace entry corresponding to a memory load into the intermediate - * register Ic. + * passed register. * + * @param intermReg The intermediate register * @param addr The memory address * @param val The value to be loaded + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::loadCInMemTrace(uint32_t addr, FF val) +bool AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_C, addr, val, false); -} + uint32_t sub_clk = 0; + switch (intermReg) { + case IntermRegister::ia: + sub_clk = SUB_CLK_LOAD_A; + break; + case IntermRegister::ib: + sub_clk = SUB_CLK_LOAD_B; + break; + case IntermRegister::ic: + sub_clk = SUB_CLK_LOAD_C; + break; + } -/** - * @brief Add a memory trace entry corresponding to a memory store from the intermediate - * register Ia. - * - * @param addr The memory address - * @param val The value to be stored - */ -void AvmMiniTraceBuilder::storeAInMemTrace(uint32_t addr, FF val) -{ - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_A, addr, val, true); -} + auto m_tag = memoryTag.at(addr); + if (m_tag == AvmMemoryTag::u0 || m_tag == m_in_tag) { + insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, false); + return true; + } -/** - * @brief Add a memory trace entry corresponding to a memory store from the intermediate - * register Ib. - * - * @param addr The memory address - * @param val The value to be stored - */ -void AvmMiniTraceBuilder::storeBInMemTrace(uint32_t addr, FF val) -{ - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_B, addr, val, true); + // Handle memory tag inconsistency + loadMismatchTagInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, m_tag); + return false; } /** * @brief Add a memory trace entry corresponding to a memory store from the intermediate - * register Ic. + * register. * + * @param intermReg The intermediate register * @param addr The memory address * @param val The value to be stored + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::storeCInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::storeInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_C, addr, val, true); + uint32_t sub_clk = 0; + switch (intermReg) { + case IntermRegister::ia: + sub_clk = SUB_CLK_STORE_A; + break; + case IntermRegister::ib: + sub_clk = SUB_CLK_STORE_B; + break; + case IntermRegister::ic: + sub_clk = SUB_CLK_STORE_C; + break; + } + + insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, true); } -/** - * @brief Addition over finite field with direct memory access. +/** TODO: Implement for non finite field types + * @brief Addition with direct memory access. * - * @param aOffset An index in ffMemory pointing to the first operand of the addition. - * @param bOffset An index in ffMemory pointing to the second operand of the addition. - * @param dstOffset An index in ffMemory pointing to the output of the addition. + * @param aOffset An index in memory pointing to the first operand of the addition. + * @param bOffset An index in memory pointing to the second operand of the addition. + * @param dstOffset An index in memory pointing to the output of the addition. + * @param inTag The instruction memory tag of the operands. */ -void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset) +void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag) { // a + b = c - FF a = ffMemory.at(aOffset); - FF b = ffMemory.at(bOffset); + FF a = memory.at(aOffset); + FF b = memory.at(bOffset); FF c = a + b; - ffMemory.at(dstOffset) = c; - - auto clk = mainTrace.size(); + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; - // Loading into Ia - loadAInMemTrace(aOffset, a); + // Loading into Ia, Ib and storing into Ic + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ib - loadBInMemTrace(bOffset, b); - - // Storing from Ic - storeCInMemTrace(dstOffset, c); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, .avmMini_sel_op_add = FF(1), - .avmMini_ia = a, - .avmMini_ib = b, - .avmMini_ic = c, + .avmMini_in_tag = FF(static_cast(inTag)), + .avmMini_tag_err = FF(static_cast(!tagMatch)), + .avmMini_ia = tagMatch ? a : FF(0), + .avmMini_ib = tagMatch ? b : FF(0), + .avmMini_ic = tagMatch ? c : FF(0), .avmMini_mem_op_a = FF(1), .avmMini_mem_op_b = FF(1), .avmMini_mem_op_c = FF(1), @@ -199,38 +207,38 @@ void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf }); }; -/** - * @brief Subtraction over finite field with direct memory access. +/** TODO: Implement for non finite field types + * @brief Subtraction with direct memory access. * - * @param aOffset An index in ffMemory pointing to the first operand of the subtraction. - * @param bOffset An index in ffMemory pointing to the second operand of the subtraction. - * @param dstOffset An index in ffMemory pointing to the output of the subtraction. + * @param aOffset An index in memory pointing to the first operand of the subtraction. + * @param bOffset An index in memory pointing to the second operand of the subtraction. + * @param dstOffset An index in memory pointing to the output of the subtraction. + * @param inTag The instruction memory tag of the operands. */ -void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset) +void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag) { // a - b = c - FF a = ffMemory.at(aOffset); - FF b = ffMemory.at(bOffset); + FF a = memory.at(aOffset); + FF b = memory.at(bOffset); FF c = a - b; - ffMemory.at(dstOffset) = c; + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); - - // Loading into Ia - loadAInMemTrace(aOffset, a); + // Loading into Ia, Ib and storing into Ic + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ib - loadBInMemTrace(bOffset, b); - - // Storing from Ic - storeCInMemTrace(dstOffset, c); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, .avmMini_sel_op_sub = FF(1), - .avmMini_ia = a, - .avmMini_ib = b, - .avmMini_ic = c, + .avmMini_in_tag = FF(static_cast(inTag)), + .avmMini_tag_err = FF(static_cast(!tagMatch)), + .avmMini_ia = tagMatch ? a : FF(0), + .avmMini_ib = tagMatch ? b : FF(0), + .avmMini_ic = tagMatch ? c : FF(0), .avmMini_mem_op_a = FF(1), .avmMini_mem_op_b = FF(1), .avmMini_mem_op_c = FF(1), @@ -241,38 +249,38 @@ void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf }); }; -/** - * @brief Multiplication over finite field with direct memory access. +/** TODO: Implement for non finite field types + * @brief Multiplication with direct memory access. * - * @param aOffset An index in ffMemory pointing to the first operand of the multiplication. - * @param bOffset An index in ffMemory pointing to the second operand of the multiplication. - * @param dstOffset An index in ffMemory pointing to the output of the multiplication. + * @param aOffset An index in memory pointing to the first operand of the multiplication. + * @param bOffset An index in memory pointing to the second operand of the multiplication. + * @param dstOffset An index in memory pointing to the output of the multiplication. + * @param inTag The instruction memory tag of the operands. */ -void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset) +void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag) { // a * b = c - FF a = ffMemory.at(aOffset); - FF b = ffMemory.at(bOffset); + FF a = memory.at(aOffset); + FF b = memory.at(bOffset); FF c = a * b; - ffMemory.at(dstOffset) = c; - - auto clk = mainTrace.size(); + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; - // Loading into Ia - loadAInMemTrace(aOffset, a); + // Loading into Ia, Ib and storing into Ic + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ib - loadBInMemTrace(bOffset, b); - - // Storing from Ic - storeCInMemTrace(dstOffset, c); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, .avmMini_sel_op_mul = FF(1), - .avmMini_ia = a, - .avmMini_ib = b, - .avmMini_ic = c, + .avmMini_in_tag = FF(static_cast(inTag)), + .avmMini_tag_err = FF(static_cast(!tagMatch)), + .avmMini_ia = tagMatch ? a : FF(0), + .avmMini_ib = tagMatch ? b : FF(0), + .avmMini_ic = tagMatch ? c : FF(0), .avmMini_mem_op_a = FF(1), .avmMini_mem_op_b = FF(1), .avmMini_mem_op_c = FF(1), @@ -283,18 +291,19 @@ void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf }); } -/** - * @brief Division over finite field with direct memory access. +/** TODO: Implement for non finite field types + * @brief Division with direct memory access. * - * @param aOffset An index in ffMemory pointing to the first operand of the division. - * @param bOffset An index in ffMemory pointing to the second operand of the division. - * @param dstOffset An index in ffMemory pointing to the output of the division. + * @param aOffset An index in memory pointing to the first operand of the division. + * @param bOffset An index in memory pointing to the second operand of the division. + * @param dstOffset An index in memory pointing to the output of the division. + * @param inTag The instruction memory tag of the operands. */ -void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset) +void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag) { // a * b^(-1) = c - FF a = ffMemory.at(aOffset); - FF b = ffMemory.at(bOffset); + FF a = memory.at(aOffset); + FF b = memory.at(bOffset); FF c; FF inv; FF error; @@ -310,27 +319,26 @@ void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf error = 1; } - ffMemory.at(dstOffset) = c; + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); + // Loading into Ia, Ib and storing into Ic + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ia - loadAInMemTrace(aOffset, a); - - // Loading into Ib - loadBInMemTrace(bOffset, b); - - // Storing from Ic - storeCInMemTrace(dstOffset, c); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, .avmMini_sel_op_div = FF(1), - .avmMini_op_err = error, - .avmMini_inv = inv, - .avmMini_ia = a, - .avmMini_ib = b, - .avmMini_ic = c, + .avmMini_in_tag = FF(static_cast(inTag)), + .avmMini_op_err = tagMatch ? error : FF(1), + .avmMini_tag_err = FF(static_cast(!tagMatch)), + .avmMini_inv = tagMatch ? inv : FF(1), + .avmMini_ia = tagMatch ? a : FF(0), + .avmMini_ib = tagMatch ? b : FF(0), + .avmMini_ic = tagMatch ? c : FF(0), .avmMini_mem_op_a = FF(1), .avmMini_mem_op_b = FF(1), .avmMini_mem_op_c = FF(1), @@ -389,8 +397,9 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, uint32_t rwa = 1; // Storing from Ia - ffMemory.at(mem_idx_a) = ia; - storeAInMemTrace(mem_idx_a, ia); + memory.at(mem_idx_a) = ia; + memoryTag.at(mem_idx_a) = AvmMemoryTag::ff; + storeInMemTrace(IntermRegister::ia, mem_idx_a, ia, AvmMemoryTag::ff); if (copySize - pos > 1) { ib = callDataMem.at(cdOffset + pos + 1); @@ -399,8 +408,9 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, rwb = 1; // Storing from Ib - ffMemory.at(mem_idx_b) = ib; - storeBInMemTrace(mem_idx_b, ib); + memory.at(mem_idx_b) = ib; + memoryTag.at(mem_idx_b) = AvmMemoryTag::ff; + storeInMemTrace(IntermRegister::ib, mem_idx_b, ib, AvmMemoryTag::ff); } if (copySize - pos > 2) { @@ -410,12 +420,14 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, rwc = 1; // Storing from Ic - ffMemory.at(mem_idx_c) = ic; - storeCInMemTrace(mem_idx_c, ic); + memory.at(mem_idx_c) = ic; + memoryTag.at(mem_idx_c) = AvmMemoryTag::ff; + storeInMemTrace(IntermRegister::ic, mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ .avmMini_clk = clk, + .avmMini_in_tag = FF(static_cast(AvmMemoryTag::ff)), .avmMini_ia = ia, .avmMini_ib = ib, .avmMini_ic = ic, @@ -474,34 +486,35 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi uint32_t mem_op_a(1); uint32_t mem_idx_a = retOffset + pos; - FF ia = ffMemory.at(mem_idx_a); + FF ia = memory.at(mem_idx_a); // Loading from Ia returnMem.push_back(ia); - loadAInMemTrace(mem_idx_a, ia); + loadInMemTrace(IntermRegister::ia, mem_idx_a, ia, AvmMemoryTag::ff); if (retSize - pos > 1) { mem_op_b = 1; mem_idx_b = retOffset + pos + 1; - ib = ffMemory.at(mem_idx_b); + ib = memory.at(mem_idx_b); // Loading from Ib returnMem.push_back(ib); - loadBInMemTrace(mem_idx_b, ib); + loadInMemTrace(IntermRegister::ib, mem_idx_b, ib, AvmMemoryTag::ff); } if (retSize - pos > 2) { mem_op_c = 1; mem_idx_c = retOffset + pos + 2; - ic = ffMemory.at(mem_idx_c); + ic = memory.at(mem_idx_c); // Loading from Ic returnMem.push_back(ic); - loadCInMemTrace(mem_idx_c, ic); + loadInMemTrace(IntermRegister::ic, mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ .avmMini_clk = clk, + .avmMini_in_tag = FF(static_cast(AvmMemoryTag::ff)), .avmMini_ia = ia, .avmMini_ib = ib, .avmMini_ic = ic, @@ -523,12 +536,13 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi } /** - * @brief Helper to initialize ffMemory. (Testing purpose mostly.) + * @brief Helper to initialize memory. (Testing purpose mostly.) * */ -void AvmMiniTraceBuilder::setFFMem(size_t idx, FF el) +void AvmMiniTraceBuilder::setFFMem(size_t idx, FF el, AvmMemoryTag tag) { - ffMemory.at(idx) = el; + memory.at(idx) = el; + memoryTag.at(idx) = tag; }; /** @@ -559,8 +573,7 @@ std::vector AvmMiniTraceBuilder::finalize() mainTrace.push_back(Row{}); } - size_t lastIndex = (memTraceSize > mainTraceSize) ? memTraceSize - 1 : mainTraceSize - 1; - mainTrace.at(lastIndex).avmMini_last = FF(1); + mainTrace.at(mainTraceSize - 1).avmMini_last = FF(1); for (size_t i = 0; i < memTraceSize; i++) { auto const& src = memTrace.at(i); @@ -571,17 +584,22 @@ std::vector AvmMiniTraceBuilder::finalize() dest.memTrace_m_addr = FF(src.m_addr); dest.memTrace_m_val = src.m_val; dest.memTrace_m_rw = FF(static_cast(src.m_rw)); + dest.memTrace_m_in_tag = FF(static_cast(src.m_in_tag)); + dest.memTrace_m_tag = FF(static_cast(src.m_tag)); + dest.memTrace_m_tag_err = FF(static_cast(src.m_tag_err)); + dest.memTrace_m_one_min_inv = src.m_one_min_inv; if (i + 1 < memTraceSize) { auto const& next = memTrace.at(i + 1); dest.memTrace_m_lastAccess = FF(static_cast(src.m_addr != next.m_addr)); } else { dest.memTrace_m_lastAccess = FF(1); + dest.memTrace_m_last = FF(1); } } // Adding extra row for the shifted values at the top of the execution trace. - Row first_row = Row{ .avmMini_first = 1 }; + Row first_row = Row{ .avmMini_first = FF(1), .memTrace_m_lastAccess = FF(1) }; mainTrace.insert(mainTrace.begin(), first_row); return std::move(mainTrace); diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp index a4621c22e19..5f5f7e8353d 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp @@ -15,6 +15,9 @@ using Row = proof_system::AvmMiniFullRow; namespace proof_system { +enum class IntermRegister : uint32_t { ia = 0, ib = 1, ic = 2 }; +enum class AvmMemoryTag : uint32_t { u0 = 0, u8 = 1, u16 = 2, u32 = 3, u64 = 4, u128 = 5, ff = 6 }; + // This is the internal context that we keep along the lifecycle of bytecode execution // to iteratively build the whole trace. This is effectively performing witness generation. // At the end of circuit building, mainTrace can be moved to AvmMiniCircuitBuilder by calling @@ -36,22 +39,22 @@ class AvmMiniTraceBuilder { AvmMiniTraceBuilder(); // Temporary helper to initialize memory. - void setFFMem(size_t idx, FF el); + void setFFMem(size_t idx, FF el, AvmMemoryTag tag); std::vector finalize(); void reset(); - // Addition over finite field with direct memory access. - void add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset); + // Addition with direct memory access. + void add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag); - // Subtraction over finite field with direct memory access. - void sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset); + // Subtraction with direct memory access. + void sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag); - // Multiplication over finite field with direct memory access. - void mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset); + // Multiplication with direct memory access. + void mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag); - // Division over finite field with direct memory access. - void div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset); + // Division with direct memory access. + void div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag); // CALLDATACOPY opcode with direct memory access, i.e., // M[dstOffset:dstOffset+copySize] = calldata[cdOffset:cdOffset+copySize] @@ -66,22 +69,26 @@ class AvmMiniTraceBuilder { uint32_t m_clk; uint32_t m_sub_clk; uint32_t m_addr; - FF m_val; - bool m_rw; + FF m_val{}; + AvmMemoryTag m_tag; + AvmMemoryTag m_in_tag; + bool m_rw = false; + bool m_tag_err = false; + FF m_one_min_inv{}; }; std::vector mainTrace; - std::vector memTrace; // Entries will be sorted by m_clk, m_sub_clk after finalize(). - std::array ffMemory{}; // Memory table for finite field elements - // Used for simulation of memory table + std::vector memTrace; // Entries will be sorted by m_clk, m_sub_clk after finalize(). + std::array memory{}; // Memory table (used for simulation) + std::array memoryTag{}; // The tag of the corresponding memory + // entry (aligned with the memory array). static bool compareMemEntries(const MemoryTraceEntry& left, const MemoryTraceEntry& right); - void insertInMemTrace(uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, bool m_rw); - void loadAInMemTrace(uint32_t addr, FF val); - void loadBInMemTrace(uint32_t addr, FF val); - void loadCInMemTrace(uint32_t addr, FF val); - void storeAInMemTrace(uint32_t addr, FF val); - void storeBInMemTrace(uint32_t addr, FF val); - void storeCInMemTrace(uint32_t addr, FF val); + void insertInMemTrace( + uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, AvmMemoryTag m_in_tag, bool m_rw); + void loadMismatchTagInMemTrace( + uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF m_val, AvmMemoryTag m_in_tag, AvmMemoryTag m_tag); + bool loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void storeInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag); }; } // namespace proof_system 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 fbcba45b8f5..02aaed70a5a 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 @@ -24,14 +24,21 @@ template struct AvmMiniFullRow { FF memTrace_m_clk{}; FF memTrace_m_sub_clk{}; FF memTrace_m_addr{}; + FF memTrace_m_tag{}; FF memTrace_m_val{}; FF memTrace_m_lastAccess{}; + FF memTrace_m_last{}; FF memTrace_m_rw{}; + FF memTrace_m_in_tag{}; + FF memTrace_m_tag_err{}; + FF memTrace_m_one_min_inv{}; FF avmMini_sel_op_add{}; FF avmMini_sel_op_sub{}; FF avmMini_sel_op_mul{}; FF avmMini_sel_op_div{}; + FF avmMini_in_tag{}; FF avmMini_op_err{}; + FF avmMini_tag_err{}; FF avmMini_inv{}; FF avmMini_ia{}; FF avmMini_ib{}; @@ -46,9 +53,10 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; - FF memTrace_m_rw_shift{}; - FF memTrace_m_addr_shift{}; FF memTrace_m_val_shift{}; + FF memTrace_m_addr_shift{}; + FF memTrace_m_rw_shift{}; + FF memTrace_m_tag_shift{}; }; class AvmMiniCircuitBuilder { @@ -61,8 +69,8 @@ class AvmMiniCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 30; - static constexpr size_t num_polys = 27; + static constexpr size_t num_fixed_columns = 38; + static constexpr size_t num_polys = 34; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -83,14 +91,21 @@ class AvmMiniCircuitBuilder { polys.memTrace_m_clk[i] = rows[i].memTrace_m_clk; polys.memTrace_m_sub_clk[i] = rows[i].memTrace_m_sub_clk; polys.memTrace_m_addr[i] = rows[i].memTrace_m_addr; + polys.memTrace_m_tag[i] = rows[i].memTrace_m_tag; polys.memTrace_m_val[i] = rows[i].memTrace_m_val; polys.memTrace_m_lastAccess[i] = rows[i].memTrace_m_lastAccess; + polys.memTrace_m_last[i] = rows[i].memTrace_m_last; polys.memTrace_m_rw[i] = rows[i].memTrace_m_rw; + polys.memTrace_m_in_tag[i] = rows[i].memTrace_m_in_tag; + polys.memTrace_m_tag_err[i] = rows[i].memTrace_m_tag_err; + polys.memTrace_m_one_min_inv[i] = rows[i].memTrace_m_one_min_inv; polys.avmMini_sel_op_add[i] = rows[i].avmMini_sel_op_add; polys.avmMini_sel_op_sub[i] = rows[i].avmMini_sel_op_sub; polys.avmMini_sel_op_mul[i] = rows[i].avmMini_sel_op_mul; polys.avmMini_sel_op_div[i] = rows[i].avmMini_sel_op_div; + polys.avmMini_in_tag[i] = rows[i].avmMini_in_tag; polys.avmMini_op_err[i] = rows[i].avmMini_op_err; + polys.avmMini_tag_err[i] = rows[i].avmMini_tag_err; polys.avmMini_inv[i] = rows[i].avmMini_inv; polys.avmMini_ia[i] = rows[i].avmMini_ia; polys.avmMini_ib[i] = rows[i].avmMini_ib; @@ -107,19 +122,22 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } - polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted()); - polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted()); polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted()); + polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted()); + polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted()); + polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); return polys; } [[maybe_unused]] bool check_circuit() { - ProverPolynomials polys = compute_polynomials(); + + auto polys = compute_polynomials(); const size_t num_rows = polys.get_polynomial_size(); - const auto evaluate_relation = [&](const std::string& relation_name) { + const auto evaluate_relation = [&](const std::string& relation_name, + std::string (*debug_label)(int)) { typename Relation::SumcheckArrayOfValuesOverSubrelations result; for (auto& r : result) { r = 0; @@ -132,8 +150,9 @@ class AvmMiniCircuitBuilder { bool x = true; for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) { if (result[j] != 0) { + std::string row_name = debug_label(static_cast(j)); throw_or_abort( - format("Relation ", relation_name, ", subrelation index ", j, " failed at row ", i)); + format("Relation ", relation_name, ", subrelation index ", row_name, " failed at row ", i)); x = false; } } @@ -144,10 +163,12 @@ class AvmMiniCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("mem_trace")) { + if (!evaluate_relation.template operator()>( + "mem_trace", AvmMini_vm::get_relation_label_mem_trace)) { return false; } - if (!evaluate_relation.template operator()>("avm_mini")) { + if (!evaluate_relation.template operator()>("avm_mini", + AvmMini_vm::get_relation_label_avm_mini)) { return false; } 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 bb4a3242ae0..d590365b76a 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,29 +7,57 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { - FF avmMini_sel_op_div{}; - FF avmMini_ia{}; - FF avmMini_rwa{}; FF avmMini_sel_op_sub{}; - FF avmMini_rwb{}; + FF avmMini_rwa{}; FF avmMini_ic{}; - FF avmMini_inv{}; - FF avmMini_sel_op_add{}; FF avmMini_op_err{}; + FF avmMini_rwb{}; + FF avmMini_ia{}; + FF avmMini_inv{}; + FF avmMini_sel_op_div{}; + FF avmMini_tag_err{}; FF avmMini_sel_op_mul{}; + FF avmMini_sel_op_add{}; + FF avmMini_mem_op_c{}; FF avmMini_rwc{}; FF avmMini_ib{}; - FF avmMini_mem_op_b{}; FF avmMini_mem_op_a{}; - FF avmMini_mem_op_c{}; + FF avmMini_mem_op_b{}; }; +inline std::string get_relation_label_avm_mini(int index) +{ + switch (index) { + case 18: + return "SUBOP_DIVISION_FF"; + + case 17: + return "SUBOP_MULTIPLICATION_FF"; + + case 16: + return "SUBOP_SUBTRACTION_FF"; + + case 19: + return "SUBOP_DIVISION_ZERO_ERR1"; + + case 20: + return "SUBOP_DIVISION_ZERO_ERR2"; + + case 21: + return "SUBOP_ERROR_RELEVANT_OP"; + + case 15: + return "SUBOP_ADDITION_FF"; + } + return std::to_string(index); +} + template class avm_miniImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4, 3, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 4, 4, 3, }; template @@ -83,7 +111,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(5); - auto tmp = (avmMini_mem_op_a * (-avmMini_mem_op_a + FF(1))); + auto tmp = (avmMini_tag_err * (-avmMini_tag_err + FF(1))); tmp *= scaling_factor; std::get<5>(evals) += tmp; } @@ -91,7 +119,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(6); - auto tmp = (avmMini_mem_op_b * (-avmMini_mem_op_b + FF(1))); + auto tmp = (avmMini_mem_op_a * (-avmMini_mem_op_a + FF(1))); tmp *= scaling_factor; std::get<6>(evals) += tmp; } @@ -99,7 +127,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(7); - auto tmp = (avmMini_mem_op_c * (-avmMini_mem_op_c + FF(1))); + auto tmp = (avmMini_mem_op_b * (-avmMini_mem_op_b + FF(1))); tmp *= scaling_factor; std::get<7>(evals) += tmp; } @@ -107,7 +135,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(8); - auto tmp = (avmMini_rwa * (-avmMini_rwa + FF(1))); + auto tmp = (avmMini_mem_op_c * (-avmMini_mem_op_c + FF(1))); tmp *= scaling_factor; std::get<8>(evals) += tmp; } @@ -115,7 +143,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(9); - auto tmp = (avmMini_rwb * (-avmMini_rwb + FF(1))); + auto tmp = (avmMini_rwa * (-avmMini_rwa + FF(1))); tmp *= scaling_factor; std::get<9>(evals) += tmp; } @@ -123,7 +151,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(10); - auto tmp = (avmMini_rwc * (-avmMini_rwc + FF(1))); + auto tmp = (avmMini_rwb * (-avmMini_rwb + FF(1))); tmp *= scaling_factor; std::get<10>(evals) += tmp; } @@ -131,7 +159,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(11); - auto tmp = (avmMini_sel_op_add * ((avmMini_ia + avmMini_ib) - avmMini_ic)); + auto tmp = (avmMini_rwc * (-avmMini_rwc + FF(1))); tmp *= scaling_factor; std::get<11>(evals) += tmp; } @@ -139,7 +167,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(12); - auto tmp = (avmMini_sel_op_sub * ((avmMini_ia - avmMini_ib) - avmMini_ic)); + auto tmp = (avmMini_tag_err * avmMini_ia); tmp *= scaling_factor; std::get<12>(evals) += tmp; } @@ -147,7 +175,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(13); - auto tmp = (avmMini_sel_op_mul * ((avmMini_ia * avmMini_ib) - avmMini_ic)); + auto tmp = (avmMini_tag_err * avmMini_ib); tmp *= scaling_factor; std::get<13>(evals) += tmp; } @@ -155,7 +183,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(14); - auto tmp = ((avmMini_sel_op_div * (-avmMini_op_err + FF(1))) * ((avmMini_ic * avmMini_ib) - avmMini_ia)); + auto tmp = (avmMini_tag_err * avmMini_ic); tmp *= scaling_factor; std::get<14>(evals) += tmp; } @@ -163,7 +191,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(15); - auto tmp = (avmMini_sel_op_div * (((avmMini_ib * avmMini_inv) - FF(1)) + avmMini_op_err)); + auto tmp = (avmMini_sel_op_add * ((avmMini_ia + avmMini_ib) - avmMini_ic)); tmp *= scaling_factor; std::get<15>(evals) += tmp; } @@ -171,7 +199,7 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(16); - auto tmp = ((avmMini_sel_op_div * avmMini_op_err) * (-avmMini_inv + FF(1))); + auto tmp = (avmMini_sel_op_sub * ((avmMini_ia - avmMini_ib) - avmMini_ic)); tmp *= scaling_factor; std::get<16>(evals) += tmp; } @@ -179,10 +207,42 @@ template class avm_miniImpl { { AvmMini_DECLARE_VIEWS(17); - auto tmp = (avmMini_op_err * (avmMini_sel_op_div - FF(1))); + auto tmp = (avmMini_sel_op_mul * ((avmMini_ia * avmMini_ib) - avmMini_ic)); tmp *= scaling_factor; std::get<17>(evals) += tmp; } + // Contribution 18 + { + AvmMini_DECLARE_VIEWS(18); + + auto tmp = ((avmMini_sel_op_div * (-avmMini_op_err + FF(1))) * ((avmMini_ic * avmMini_ib) - avmMini_ia)); + tmp *= scaling_factor; + std::get<18>(evals) += tmp; + } + // Contribution 19 + { + AvmMini_DECLARE_VIEWS(19); + + auto tmp = (avmMini_sel_op_div * (((avmMini_ib * avmMini_inv) - FF(1)) + avmMini_op_err)); + tmp *= scaling_factor; + std::get<19>(evals) += tmp; + } + // Contribution 20 + { + AvmMini_DECLARE_VIEWS(20); + + auto tmp = ((avmMini_sel_op_div * avmMini_op_err) * (-avmMini_inv + FF(1))); + tmp *= scaling_factor; + std::get<20>(evals) += tmp; + } + // Contribution 21 + { + AvmMini_DECLARE_VIEWS(21); + + auto tmp = (avmMini_op_err * (avmMini_sel_op_div - FF(1))); + tmp *= scaling_factor; + std::get<21>(evals) += tmp; + } } }; 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 e2abc409ea4..9d23bb0f8f1 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -7,14 +7,21 @@ [[maybe_unused]] auto memTrace_m_clk = View(new_term.memTrace_m_clk); \ [[maybe_unused]] auto memTrace_m_sub_clk = View(new_term.memTrace_m_sub_clk); \ [[maybe_unused]] auto memTrace_m_addr = View(new_term.memTrace_m_addr); \ + [[maybe_unused]] auto memTrace_m_tag = View(new_term.memTrace_m_tag); \ [[maybe_unused]] auto memTrace_m_val = View(new_term.memTrace_m_val); \ [[maybe_unused]] auto memTrace_m_lastAccess = View(new_term.memTrace_m_lastAccess); \ + [[maybe_unused]] auto memTrace_m_last = View(new_term.memTrace_m_last); \ [[maybe_unused]] auto memTrace_m_rw = View(new_term.memTrace_m_rw); \ + [[maybe_unused]] auto memTrace_m_in_tag = View(new_term.memTrace_m_in_tag); \ + [[maybe_unused]] auto memTrace_m_tag_err = View(new_term.memTrace_m_tag_err); \ + [[maybe_unused]] auto memTrace_m_one_min_inv = View(new_term.memTrace_m_one_min_inv); \ [[maybe_unused]] auto avmMini_sel_op_add = View(new_term.avmMini_sel_op_add); \ [[maybe_unused]] auto avmMini_sel_op_sub = View(new_term.avmMini_sel_op_sub); \ [[maybe_unused]] auto avmMini_sel_op_mul = View(new_term.avmMini_sel_op_mul); \ [[maybe_unused]] auto avmMini_sel_op_div = View(new_term.avmMini_sel_op_div); \ + [[maybe_unused]] auto avmMini_in_tag = View(new_term.avmMini_in_tag); \ [[maybe_unused]] auto avmMini_op_err = View(new_term.avmMini_op_err); \ + [[maybe_unused]] auto avmMini_tag_err = View(new_term.avmMini_tag_err); \ [[maybe_unused]] auto avmMini_inv = View(new_term.avmMini_inv); \ [[maybe_unused]] auto avmMini_ia = View(new_term.avmMini_ia); \ [[maybe_unused]] auto avmMini_ib = View(new_term.avmMini_ib); \ @@ -29,6 +36,7 @@ [[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 memTrace_m_rw_shift = View(new_term.memTrace_m_rw_shift); \ + [[maybe_unused]] auto memTrace_m_val_shift = View(new_term.memTrace_m_val_shift); \ [[maybe_unused]] auto memTrace_m_addr_shift = View(new_term.memTrace_m_addr_shift); \ - [[maybe_unused]] auto memTrace_m_val_shift = View(new_term.memTrace_m_val_shift); + [[maybe_unused]] auto memTrace_m_rw_shift = View(new_term.memTrace_m_rw_shift); \ + [[maybe_unused]] auto memTrace_m_tag_shift = View(new_term.memTrace_m_tag_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 7bfb1b223cd..9880acfa631 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -7,26 +7,51 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { - FF memTrace_m_rw_shift{}; + FF memTrace_m_rw{}; + FF memTrace_m_addr{}; + FF memTrace_m_val_shift{}; + FF memTrace_m_last{}; + FF memTrace_m_tag_err{}; FF memTrace_m_addr_shift{}; FF memTrace_m_val{}; - FF memTrace_m_addr{}; - FF memTrace_m_rw{}; - FF avmMini_first{}; FF memTrace_m_lastAccess{}; - FF avmMini_last{}; - FF memTrace_m_val_shift{}; + FF memTrace_m_tag{}; + FF memTrace_m_in_tag{}; + FF memTrace_m_rw_shift{}; + FF memTrace_m_one_min_inv{}; + FF memTrace_m_tag_shift{}; }; +inline std::string get_relation_label_mem_trace(int index) +{ + switch (index) { + case 4: + return "MEM_LAST_ACCESS_DELIMITER"; + + case 6: + return "MEM_READ_WRITE_TAG_CONSISTENCY"; + + case 9: + return "MEM_IN_TAG_CONSISTENCY_2"; + + case 5: + return "MEM_READ_WRITE_VAL_CONSISTENCY"; + + case 7: + return "MEM_ZERO_INIT"; + + case 8: + return "MEM_IN_TAG_CONSISTENCY_1"; + } + return std::to_string(index); +} + template class mem_traceImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, - 3, - 4, - 6, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 4, 4, 4, 3, 3, }; template @@ -48,7 +73,7 @@ template class mem_traceImpl { { AvmMini_DECLARE_VIEWS(1); - auto tmp = (memTrace_m_rw * (-memTrace_m_rw + FF(1))); + auto tmp = (memTrace_m_last * (-memTrace_m_last + FF(1))); tmp *= scaling_factor; std::get<1>(evals) += tmp; } @@ -56,8 +81,7 @@ template class mem_traceImpl { { AvmMini_DECLARE_VIEWS(2); - auto tmp = (((-avmMini_first + FF(1)) * (-memTrace_m_lastAccess + FF(1))) * - (memTrace_m_addr_shift - memTrace_m_addr)); + auto tmp = (memTrace_m_rw * (-memTrace_m_rw + FF(1))); tmp *= scaling_factor; std::get<2>(evals) += tmp; } @@ -65,12 +89,61 @@ template class mem_traceImpl { { AvmMini_DECLARE_VIEWS(3); - auto tmp = (((((-avmMini_first + FF(1)) * (-avmMini_last + FF(1))) * (-memTrace_m_lastAccess + FF(1))) * - (-memTrace_m_rw_shift + FF(1))) * - (memTrace_m_val_shift - memTrace_m_val)); + auto tmp = (memTrace_m_tag_err * (-memTrace_m_tag_err + FF(1))); tmp *= scaling_factor; std::get<3>(evals) += tmp; } + // Contribution 4 + { + AvmMini_DECLARE_VIEWS(4); + + auto tmp = ((-memTrace_m_lastAccess + FF(1)) * (memTrace_m_addr_shift - memTrace_m_addr)); + tmp *= scaling_factor; + std::get<4>(evals) += tmp; + } + // Contribution 5 + { + AvmMini_DECLARE_VIEWS(5); + + auto tmp = (((-memTrace_m_lastAccess + FF(1)) * (-memTrace_m_rw_shift + FF(1))) * + (memTrace_m_val_shift - memTrace_m_val)); + tmp *= scaling_factor; + std::get<5>(evals) += tmp; + } + // Contribution 6 + { + AvmMini_DECLARE_VIEWS(6); + + auto tmp = (((-memTrace_m_lastAccess + FF(1)) * (-memTrace_m_rw_shift + FF(1))) * + (memTrace_m_tag_shift - memTrace_m_tag)); + tmp *= scaling_factor; + std::get<6>(evals) += tmp; + } + // Contribution 7 + { + AvmMini_DECLARE_VIEWS(7); + + auto tmp = ((memTrace_m_lastAccess * (-memTrace_m_rw_shift + FF(1))) * memTrace_m_val_shift); + tmp *= scaling_factor; + std::get<7>(evals) += tmp; + } + // Contribution 8 + { + AvmMini_DECLARE_VIEWS(8); + + auto tmp = + (((memTrace_m_in_tag - memTrace_m_tag) * (-memTrace_m_one_min_inv + FF(1))) - memTrace_m_tag_err); + tmp *= scaling_factor; + std::get<8>(evals) += tmp; + } + // Contribution 9 + { + AvmMini_DECLARE_VIEWS(9); + + auto tmp = ((-memTrace_m_tag_err + FF(1)) * memTrace_m_one_min_inv); + tmp *= scaling_factor; + std::get<9>(evals) += tmp; + } } }; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp index 4014eec57bb..ff07a075419 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp @@ -60,10 +60,19 @@ bool AvmMiniVerifier::verify_proof(const plonk::proof& proof) transcript->template receive_from_prover(commitment_labels.memTrace_m_sub_clk); commitments.memTrace_m_addr = transcript->template receive_from_prover(commitment_labels.memTrace_m_addr); + commitments.memTrace_m_tag = transcript->template receive_from_prover(commitment_labels.memTrace_m_tag); commitments.memTrace_m_val = transcript->template receive_from_prover(commitment_labels.memTrace_m_val); commitments.memTrace_m_lastAccess = transcript->template receive_from_prover(commitment_labels.memTrace_m_lastAccess); + commitments.memTrace_m_last = + transcript->template receive_from_prover(commitment_labels.memTrace_m_last); commitments.memTrace_m_rw = transcript->template receive_from_prover(commitment_labels.memTrace_m_rw); + commitments.memTrace_m_in_tag = + transcript->template receive_from_prover(commitment_labels.memTrace_m_in_tag); + commitments.memTrace_m_tag_err = + transcript->template receive_from_prover(commitment_labels.memTrace_m_tag_err); + commitments.memTrace_m_one_min_inv = + transcript->template receive_from_prover(commitment_labels.memTrace_m_one_min_inv); commitments.avmMini_sel_op_add = transcript->template receive_from_prover(commitment_labels.avmMini_sel_op_add); commitments.avmMini_sel_op_sub = @@ -72,7 +81,10 @@ bool AvmMiniVerifier::verify_proof(const plonk::proof& proof) transcript->template receive_from_prover(commitment_labels.avmMini_sel_op_mul); commitments.avmMini_sel_op_div = transcript->template receive_from_prover(commitment_labels.avmMini_sel_op_div); + commitments.avmMini_in_tag = transcript->template receive_from_prover(commitment_labels.avmMini_in_tag); commitments.avmMini_op_err = transcript->template receive_from_prover(commitment_labels.avmMini_op_err); + commitments.avmMini_tag_err = + transcript->template receive_from_prover(commitment_labels.avmMini_tag_err); commitments.avmMini_inv = transcript->template receive_from_prover(commitment_labels.avmMini_inv); commitments.avmMini_ia = transcript->template receive_from_prover(commitment_labels.avmMini_ia); commitments.avmMini_ib = transcript->template receive_from_prover(commitment_labels.avmMini_ib); 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 1a94d54816e..ad7b4342469 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp @@ -7,6 +7,7 @@ #include "barretenberg/vm/generated/AvmMini_composer.hpp" #include "barretenberg/vm/generated/AvmMini_prover.hpp" #include "barretenberg/vm/generated/AvmMini_verifier.hpp" +#include "helpers.test.hpp" #include #include @@ -33,67 +34,6 @@ class AvmMiniArithmeticTests : public ::testing::Test { class AvmMiniArithmeticNegativeTests : public AvmMiniArithmeticTests {}; -// We add some helper functions in the anonymous namespace. -namespace { - -/** - * @brief Helper routine proving and verifying a proof based on the supplied trace - * - * @param trace The execution trace - */ -void validateTraceProof(std::vector&& trace) -{ - auto circuit_builder = AvmMiniCircuitBuilder(); - circuit_builder.set_trace(std::move(trace)); - - EXPECT_TRUE(circuit_builder.check_circuit()); - - auto composer = honk::AvmMiniComposer(); - auto prover = composer.create_prover(circuit_builder); - auto proof = prover.construct_proof(); - - auto verifier = composer.create_verifier(circuit_builder); - bool verified = verifier.verify_proof(proof); - - if (!verified) { - log_avmMini_trace(circuit_builder.rows, 0, 10); - } -}; - -/** - * @brief Helper routine for the negative tests. It mutates the output value of an operation - * located in the Ic intermediate register. The memory trace is adapted consistently. - * - * @param trace Execution trace - * @param selectRow Lambda serving to select the row in trace - * @param newValue The value that will be written in intermediate register Ic at the selected row. - */ -void mutateIcInTrace(std::vector& trace, std::function&& selectRow, FF const& newValue) -{ - // Find the first row matching the criteria defined by selectRow - auto row = std::ranges::find_if(trace.begin(), trace.end(), selectRow); - - // Check that we found one - EXPECT_TRUE(row != trace.end()); - - // Mutate the correct result in the main trace - row->avmMini_ic = newValue; - - // Adapt the memory trace to be consistent with the wrongly computed addition - auto const clk = row->avmMini_clk; - auto const addr = row->avmMini_mem_idx_c; - - // Find the relevant memory trace entry. - auto memRow = std::ranges::find_if(trace.begin(), trace.end(), [clk, addr](Row r) { - return r.memTrace_m_clk == clk && r.memTrace_m_addr == addr; - }); - - EXPECT_TRUE(memRow != trace.end()); - memRow->memTrace_m_val = newValue; -}; - -} // anonymous namespace - /****************************************************************************** * * POSITIVE TESTS - Finite Field Type @@ -123,8 +63,8 @@ TEST_F(AvmMiniArithmeticTests, additionFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 37, 4, 11 }); - // Memory layout: [37,4,11,0,0,0,....] - trace_builder.add(0, 1, 4); // [37,4,11,0,41,0,....] + // Memory layout: [37,4,11,0,0,0,....] + trace_builder.add(0, 1, 4, AvmMemoryTag::ff); // [37,4,11,0,41,0,....] trace_builder.returnOP(0, 5); auto trace = trace_builder.finalize(); @@ -146,8 +86,8 @@ TEST_F(AvmMiniArithmeticTests, subtractionFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 8, 4, 17 }); - // Memory layout: [8,4,17,0,0,0,....] - trace_builder.sub(2, 0, 1); // [8,9,17,0,0,0....] + // Memory layout: [8,4,17,0,0,0,....] + trace_builder.sub(2, 0, 1, AvmMemoryTag::ff); // [8,9,17,0,0,0....] trace_builder.returnOP(0, 3); auto trace = trace_builder.finalize(); @@ -169,8 +109,8 @@ TEST_F(AvmMiniArithmeticTests, multiplicationFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 5, 0, 20 }); - // Memory layout: [5,0,20,0,0,0,....] - trace_builder.mul(2, 0, 1); // [5,100,20,0,0,0....] + // Memory layout: [5,0,20,0,0,0,....] + trace_builder.mul(2, 0, 1, AvmMemoryTag::ff); // [5,100,20,0,0,0....] trace_builder.returnOP(0, 3); auto trace = trace_builder.finalize(); @@ -192,8 +132,8 @@ TEST_F(AvmMiniArithmeticTests, multiplicationByZeroFF) { trace_builder.callDataCopy(0, 1, 0, std::vector{ 127 }); - // Memory layout: [127,0,0,0,0,0,....] - trace_builder.mul(0, 1, 2); // [127,0,0,0,0,0....] + // Memory layout: [127,0,0,0,0,0,....] + trace_builder.mul(0, 1, 2, AvmMemoryTag::ff); // [127,0,0,0,0,0....] trace_builder.returnOP(0, 3); auto trace = trace_builder.finalize(); @@ -215,8 +155,8 @@ TEST_F(AvmMiniArithmeticTests, divisionFF) { trace_builder.callDataCopy(0, 2, 0, std::vector{ 15, 315 }); - // Memory layout: [15,315,0,0,0,0,....] - trace_builder.div(1, 0, 2); // [15,315,21,0,0,0....] + // Memory layout: [15,315,0,0,0,0,....] + trace_builder.div(1, 0, 2, AvmMemoryTag::ff); // [15,315,21,0,0,0....] trace_builder.returnOP(0, 3); auto trace = trace_builder.finalize(); @@ -238,8 +178,8 @@ TEST_F(AvmMiniArithmeticTests, divisionNumeratorZeroFF) { trace_builder.callDataCopy(0, 1, 0, std::vector{ 15 }); - // Memory layout: [15,0,0,0,0,0,....] - trace_builder.div(1, 0, 0); // [0,0,0,0,0,0....] + // Memory layout: [15,0,0,0,0,0,....] + trace_builder.div(1, 0, 0, AvmMemoryTag::ff); // [0,0,0,0,0,0....] trace_builder.returnOP(0, 3); auto trace = trace_builder.finalize(); @@ -262,8 +202,30 @@ TEST_F(AvmMiniArithmeticTests, divisionByZeroErrorFF) { trace_builder.callDataCopy(0, 1, 0, std::vector{ 15 }); - // Memory layout: [15,0,0,0,0,0,....] - trace_builder.div(0, 1, 2); // [15,0,0,0,0,0....] + // Memory layout: [15,0,0,0,0,0,....] + trace_builder.div(0, 1, 2, AvmMemoryTag::ff); // [15,0,0,0,0,0....] + auto trace = trace_builder.finalize(); + + // Find the first row enabling the division selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_div == FF(1); }); + + // Check that the correct result is stored at the expected memory location. + EXPECT_TRUE(row != trace.end()); + EXPECT_EQ(row->avmMini_ic, FF(0)); + EXPECT_EQ(row->avmMini_mem_idx_c, FF(2)); + EXPECT_EQ(row->avmMini_mem_op_c, FF(1)); + EXPECT_EQ(row->avmMini_rwc, FF(1)); + EXPECT_EQ(row->avmMini_op_err, FF(1)); + + validateTraceProof(std::move(trace)); +} + +// Test on division of zero by zero over finite field type. +// We check that the operator error flag is raised. +TEST_F(AvmMiniArithmeticTests, divisionZeroByZeroErrorFF) +{ + // Memory layout: [0,0,0,0,0,0,....] + trace_builder.div(0, 1, 2, AvmMemoryTag::ff); // [0,0,0,0,0,0....] auto trace = trace_builder.finalize(); // Find the first row enabling the division selector @@ -288,16 +250,17 @@ TEST_F(AvmMiniArithmeticTests, arithmeticFFWithError) { trace_builder.callDataCopy(0, 3, 2, std::vector{ 45, 23, 12 }); - // Memory layout: [0,0,45,23,12,0,0,0,....] - trace_builder.add(2, 3, 4); // [0,0,45,23,68,0,0,0,....] - trace_builder.add(4, 5, 5); // [0,0,45,23,68,68,0,0,....] - trace_builder.add(5, 5, 5); // [0,0,45,23,68,136,0,0,....] - trace_builder.add(5, 6, 7); // [0,0,45,23,68,136,0,136,0....] - trace_builder.sub(7, 6, 8); // [0,0,45,23,68,136,0,136,136,0....] - trace_builder.mul(8, 8, 8); // [0,0,45,23,68,136,0,136,136^2,0....] - trace_builder.div(3, 5, 1); // [0,23*136^(-1),45,23,68,136,0,136,136^2,0....] - trace_builder.div(1, 1, 9); // [0,23*136^(-1),45,23,68,136,0,136,136^2,1,0....] - trace_builder.div(9, 0, 4); // [0,23*136^(-1),45,23,1/0,136,0,136,136^2,1,0....] Error: division by 0 + // Memory layout: [0,0,45,23,12,0,0,0,....] + trace_builder.add(2, 3, 4, AvmMemoryTag::ff); // [0,0,45,23,68,0,0,0,....] + trace_builder.add(4, 5, 5, AvmMemoryTag::ff); // [0,0,45,23,68,68,0,0,....] + trace_builder.add(5, 5, 5, AvmMemoryTag::ff); // [0,0,45,23,68,136,0,0,....] + trace_builder.add(5, 6, 7, AvmMemoryTag::ff); // [0,0,45,23,68,136,0,136,0....] + trace_builder.sub(7, 6, 8, AvmMemoryTag::ff); // [0,0,45,23,68,136,0,136,136,0....] + trace_builder.mul(8, 8, 8, AvmMemoryTag::ff); // [0,0,45,23,68,136,0,136,136^2,0....] + trace_builder.div(3, 5, 1, AvmMemoryTag::ff); // [0,23*136^(-1),45,23,68,136,0,136,136^2,0....] + trace_builder.div(1, 1, 9, AvmMemoryTag::ff); // [0,23*136^(-1),45,23,68,136,0,136,136^2,1,0....] + trace_builder.div( + 9, 0, 4, AvmMemoryTag::ff); // [0,23*136^(-1),45,23,1/0,136,0,136,136^2,1,0....] Error: division by 0 auto trace = trace_builder.finalize(); validateTraceProof(std::move(trace)); @@ -329,16 +292,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, additionFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 37, 4, 11 }); - // Memory layout: [37,4,11,0,0,0,....] - trace_builder.add(0, 1, 4); // [37,4,11,0,41,0,....] - trace_builder.returnOP(0, 5); + // Memory layout: [37,4,11,0,0,0,....] + trace_builder.add(0, 1, 4, AvmMemoryTag::ff); // [37,4,11,0,41,0,....] auto trace = trace_builder.finalize(); auto selectRow = [](Row r) { return r.avmMini_sel_op_add == FF(1); }; mutateIcInTrace(trace, std::move(selectRow), FF(40)); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_ADDITION_FF"); } // Test on basic incorrect subtraction over finite field type. @@ -346,16 +307,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, subtractionFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 8, 4, 17 }); - // Memory layout: [8,4,17,0,0,0,....] - trace_builder.sub(2, 0, 1); // [8,9,17,0,0,0....] - trace_builder.returnOP(0, 3); + // Memory layout: [8,4,17,0,0,0,....] + trace_builder.sub(2, 0, 1, AvmMemoryTag::ff); // [8,9,17,0,0,0....] auto trace = trace_builder.finalize(); auto selectRow = [](Row r) { return r.avmMini_sel_op_sub == FF(1); }; mutateIcInTrace(trace, std::move(selectRow), FF(-9)); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_SUBTRACTION_FF"); } // Test on basic incorrect multiplication over finite field type. @@ -363,16 +322,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, multiplicationFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 5, 0, 20 }); - // Memory layout: [5,0,20,0,0,0,....] - trace_builder.mul(2, 0, 1); // [5,100,20,0,0,0....] - trace_builder.returnOP(0, 3); + // Memory layout: [5,0,20,0,0,0,....] + trace_builder.mul(2, 0, 1, AvmMemoryTag::ff); // [5,100,20,0,0,0....] auto trace = trace_builder.finalize(); auto selectRow = [](Row r) { return r.avmMini_sel_op_mul == FF(1); }; mutateIcInTrace(trace, std::move(selectRow), FF(1000)); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_MULTIPLICATION_FF"); } // Test on basic incorrect division over finite field type. @@ -380,16 +337,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionFF) { trace_builder.callDataCopy(0, 2, 0, std::vector{ 15, 315 }); - // Memory layout: [15,315,0,0,0,0,....] - trace_builder.div(1, 0, 2); // [15,315,21,0,0,0....] - trace_builder.returnOP(0, 3); + // Memory layout: [15,315,0,0,0,0,....] + trace_builder.div(1, 0, 2, AvmMemoryTag::ff); // [15,315,21,0,0,0....] auto trace = trace_builder.finalize(); auto selectRow = [](Row r) { return r.avmMini_sel_op_div == FF(1); }; mutateIcInTrace(trace, std::move(selectRow), FF(0)); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_FF"); } // Test where division is not by zero but an operation error is wrongly raised @@ -398,19 +353,24 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionNoZeroButErrorFF) { trace_builder.callDataCopy(0, 2, 0, std::vector{ 15, 315 }); - // Memory layout: [15,315,0,0,0,0,....] - trace_builder.div(1, 0, 2); // [15,315,21,0,0,0....] - trace_builder.returnOP(0, 3); + // Memory layout: [15,315,0,0,0,0,....] + trace_builder.div(1, 0, 2, AvmMemoryTag::ff); // [15,315,21,0,0,0....] auto trace = trace_builder.finalize(); // Find the first row enabling the division selector auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_div == FF(1); }); + size_t const index = static_cast(row - trace.begin()); + // Activate the operator error - row->avmMini_op_err = FF(1); + trace[index].avmMini_op_err = FF(1); + auto trace2 = trace; - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_ZERO_ERR1"); + + // Even more malicious, one makes the first relation passes by setting the inverse to zero. + trace2[index].avmMini_inv = FF(0); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace2)), "SUBOP_DIVISION_ZERO_ERR2"); } // Test with division by zero occurs and no error is raised (remove error flag) @@ -418,8 +378,24 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionByZeroNoErrorFF) { trace_builder.callDataCopy(0, 1, 0, std::vector{ 15 }); - // Memory layout: [15,0,0,0,0,0,....] - trace_builder.div(0, 1, 2); // [15,0,0,0,0,0....] + // Memory layout: [15,0,0,0,0,0,....] + trace_builder.div(0, 1, 2, AvmMemoryTag::ff); // [15,0,0,0,0,0....] + auto trace = trace_builder.finalize(); + + // Find the first row enabling the division selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_div == FF(1); }); + + // Remove the operator error flag + row->avmMini_op_err = FF(0); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_FF"); +} + +// Test with division of zero by zero occurs and no error is raised (remove error flag) +TEST_F(AvmMiniArithmeticNegativeTests, divisionZeroByZeroNoErrorFF) +{ + // Memory layout: [0,0,0,0,0,0,....] + trace_builder.div(0, 1, 2, AvmMemoryTag::ff); // [0,0,0,0,0,0....] auto trace = trace_builder.finalize(); // Find the first row enabling the division selector @@ -428,8 +404,7 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionByZeroNoErrorFF) // Remove the operator error flag row->avmMini_op_err = FF(0); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_ZERO_ERR1"); } // Test that error flag cannot be raised for a non-relevant operation such as @@ -438,8 +413,8 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) { trace_builder.callDataCopy(0, 3, 0, std::vector{ 37, 4, 11 }); - // Memory layout: [37,4,11,0,0,0,....] - trace_builder.add(0, 1, 4); // [37,4,11,0,41,0,....] + // Memory layout: [37,4,11,0,0,0,....] + trace_builder.add(0, 1, 4, AvmMemoryTag::ff); // [37,4,11,0,41,0,....] trace_builder.returnOP(0, 5); auto trace = trace_builder.finalize(); @@ -449,15 +424,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) // Activate the operator error row->avmMini_op_err = FF(1); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_ERROR_RELEVANT_OP"); trace_builder.reset(); trace_builder.callDataCopy(0, 3, 0, std::vector{ 8, 4, 17 }); - // Memory layout: [8,4,17,0,0,0,....] - trace_builder.sub(2, 0, 1); // [8,9,17,0,0,0....] + // Memory layout: [8,4,17,0,0,0,....] + trace_builder.sub(2, 0, 1, AvmMemoryTag::ff); // [8,9,17,0,0,0....] trace_builder.returnOP(0, 3); trace = trace_builder.finalize(); @@ -467,15 +441,14 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) // Activate the operator error row->avmMini_op_err = FF(1); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_ERROR_RELEVANT_OP"); trace_builder.reset(); trace_builder.callDataCopy(0, 3, 0, std::vector{ 5, 0, 20 }); - // Memory layout: [5,0,20,0,0,0,....] - trace_builder.mul(2, 0, 1); // [5,100,20,0,0,0....] + // Memory layout: [5,0,20,0,0,0,....] + trace_builder.mul(2, 0, 1, AvmMemoryTag::ff); // [5,100,20,0,0,0....] trace_builder.returnOP(0, 3); trace = trace_builder.finalize(); @@ -485,8 +458,7 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) // Activate the operator error row->avmMini_op_err = FF(1); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_ERROR_RELEVANT_OP"); } } // namespace tests_avm \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp new file mode 100644 index 00000000000..31c3355a5ee --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp @@ -0,0 +1,252 @@ +#include "barretenberg/ecc/curves/bn254/fr.hpp" +#include "barretenberg/flavor/generated/AvmMini_flavor.hpp" +#include "barretenberg/numeric/uint256/uint256.hpp" +#include "barretenberg/proof_system/circuit_builder/AvmMini_helper.hpp" +#include "barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp" +#include "barretenberg/sumcheck/sumcheck_round.hpp" +#include "barretenberg/vm/generated/AvmMini_composer.hpp" +#include "barretenberg/vm/generated/AvmMini_prover.hpp" +#include "barretenberg/vm/generated/AvmMini_verifier.hpp" +#include "helpers.test.hpp" + +#include +#include +#include +#include +#include + +using namespace proof_system; + +namespace tests_avm { + +class AvmMiniMemoryTests : public ::testing::Test { + public: + AvmMiniTraceBuilder trace_builder; + + protected: + // TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test. + void SetUp() override + { + barretenberg::srs::init_crs_factory("../srs_db/ignition"); + trace_builder = AvmMiniTraceBuilder(); // Clean instance for every run. + }; +}; + +/****************************************************************************** + * + * MEMORY TESTS + * + ****************************************************************************** + * This test suite focuses on non-trivial memory-related tests which are + * not implicitly covered by other tests such as AvmMiniArithmeticTests. + * + * For instance, tests on checking error conditions related to memory or + * violation of memory-related relations in malicious/malformed execution + * trace is the focus. + ******************************************************************************/ + +// Testing an operation with a mismatched memory tag. +// The proof must pass and we check that the AVM error is raised. +TEST_F(AvmMiniMemoryTests, mismatchedTag) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 98, 12 }); + + trace_builder.add(0, 1, 4, AvmMemoryTag::u8); + auto trace = trace_builder.finalize(); + + // Find the first row enabling the addition selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_add == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + + // All intermediate registers should be set to zero. + EXPECT_EQ(row->avmMini_ia, FF(0)); + EXPECT_EQ(row->avmMini_ib, FF(0)); + EXPECT_EQ(row->avmMini_ic, FF(0)); + + auto clk = row->avmMini_clk; + + // Find the memory trace position corresponding to the add sub-operation of register ia. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + EXPECT_TRUE(row != trace.end()); + + EXPECT_EQ(row->memTrace_m_tag_err, FF(1)); // Error is raised + EXPECT_EQ(row->memTrace_m_in_tag, FF(static_cast(AvmMemoryTag::u8))); + EXPECT_EQ(row->memTrace_m_tag, FF(static_cast(AvmMemoryTag::ff))); + + // Find the memory trace position corresponding to the add sub-operation of register ib. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_B; + }); + + EXPECT_TRUE(row != trace.end()); + + EXPECT_EQ(row->memTrace_m_tag_err, FF(1)); // Error is raised + EXPECT_EQ(row->memTrace_m_in_tag, FF(static_cast(AvmMemoryTag::u8))); + EXPECT_EQ(row->memTrace_m_tag, FF(static_cast(AvmMemoryTag::ff))); + + validateTraceProof(std::move(trace)); +} + +// Testing violation that m_lastAccess is a delimiter for two different addresses +// in the memory trace +TEST_F(AvmMiniMemoryTests, mLastAccessViolation) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 4, 9 }); + + // Memory layout: [4,9,0,0,0,0,....] + trace_builder.sub(1, 0, 2, AvmMemoryTag::u8); // [4,9,5,0,0,0.....] + auto trace = trace_builder.finalize(); + + // Find the row with subtraction operation + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_sub == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + auto clk = row->avmMini_clk; + + // Find the row for memory trace with last memory entry for address 1 (read for subtraction) + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_addr == FF(1) && + r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + EXPECT_TRUE(row != trace.end()); + + row->memTrace_m_lastAccess = FF(0); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_LAST_ACCESS_DELIMITER"); +} + +// Testing violation that a memory read operation must read the same value which was +// written into memory +TEST_F(AvmMiniMemoryTests, readWriteConsistencyValViolation) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 4, 9 }); + + // Memory layout: [4,9,0,0,0,0,....] + trace_builder.mul(1, 0, 2, AvmMemoryTag::u8); // [4,9,36,0,0,0.....] + trace_builder.returnOP(2, 1); // Return single memory word at position 2 (36) + auto trace = trace_builder.finalize(); + + // Find the row with multiplication operation + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_mul == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + auto clk = row->avmMini_clk + 1; // return operation is just after the multiplication + + // Find the row for memory trace with last memory entry for address 2 (read for multiplication) + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_addr == FF(2) && + r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + EXPECT_TRUE(row != trace.end()); + + row->memTrace_m_val = FF(35); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_READ_WRITE_VAL_CONSISTENCY"); +} + +// Testing violation that memory read operation must read the same tag which was +// written into memory +TEST_F(AvmMiniMemoryTests, readWriteConsistencyTagViolation) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 4, 9 }); + + // Memory layout: [4,9,0,0,0,0,....] + trace_builder.mul(1, 0, 2, AvmMemoryTag::u8); // [4,9,36,0,0,0.....] + trace_builder.returnOP(2, 1); // Return single memory word at position 2 (36) + auto trace = trace_builder.finalize(); + + // Find the row with multiplication operation + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_mul == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + auto clk = row->avmMini_clk + 1; // return operation is just after the multiplication + + // Find the row for memory trace with last memory entry for address 2 (read for multiplication) + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_addr == FF(2) && + r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + EXPECT_TRUE(row != trace.end()); + + row->memTrace_m_tag = static_cast(AvmMemoryTag::u16); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_READ_WRITE_TAG_CONSISTENCY"); +} + +// Testing violation that a memory read at uninitialized location must have value 0. +TEST_F(AvmMiniMemoryTests, readUninitializedMemoryViolation) +{ + trace_builder.returnOP(1, 1); // Return single memory word at position 1 + auto trace = trace_builder.finalize(); + + trace[1].memTrace_m_val = 9; + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_ZERO_INIT"); +} + +// Testing violation that an operation with a mismatched memory tag +// must raise a VM error. +TEST_F(AvmMiniMemoryTests, mismatchedTagErrorViolation) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 98, 12 }); + + trace_builder.sub(0, 1, 4, AvmMemoryTag::u8); + auto trace = trace_builder.finalize(); + + // Find the first row enabling the subtraction selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_sub == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + + auto clk = row->avmMini_clk; + + // Find the memory trace position corresponding to the subtraction sub-operation of register ia. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + row->memTrace_m_tag_err = FF(0); + auto index = static_cast(row - trace.begin()); + auto trace2 = trace; + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_IN_TAG_CONSISTENCY_1"); + + // More sophisticated attempt by adapting witness "on_min_inv" to make pass the above constraint + trace2[index].memTrace_m_one_min_inv = FF(1); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace2)), "MEM_IN_TAG_CONSISTENCY_2"); +} + +// Testing violation that an operation with a consistent memory tag +// must not set a VM error. +TEST_F(AvmMiniMemoryTests, consistentTagNoErrorViolation) +{ + trace_builder.callDataCopy(0, 2, 0, std::vector{ 84, 7 }); + + trace_builder.div(0, 1, 4, AvmMemoryTag::ff); + auto trace = trace_builder.finalize(); + + // Find the first row enabling the division selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_div == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + + auto clk = row->avmMini_clk; + + // Find the memory trace position corresponding to the div sub-operation of register ia. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_sub_clk == AvmMiniTraceBuilder::SUB_CLK_LOAD_A; + }); + + row->memTrace_m_tag_err = FF(1); + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "MEM_IN_TAG_CONSISTENCY_1"); +} +} // namespace tests_avm \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.cpp new file mode 100644 index 00000000000..9cfb6fe7a17 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.cpp @@ -0,0 +1,69 @@ +#include "barretenberg/vm/tests/helpers.test.hpp" +#include "barretenberg/flavor/generated/AvmMini_flavor.hpp" +#include "barretenberg/proof_system/circuit_builder/AvmMini_helper.hpp" +#include "barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp" +#include "barretenberg/vm/generated/AvmMini_composer.hpp" +#include "barretenberg/vm/generated/AvmMini_prover.hpp" +#include "barretenberg/vm/generated/AvmMini_verifier.hpp" +#include + +namespace tests_avm { +using namespace proof_system; + +/** + * @brief Helper routine proving and verifying a proof based on the supplied trace + * + * @param trace The execution trace + */ +void validateTraceProof(std::vector&& trace) +{ + auto circuit_builder = AvmMiniCircuitBuilder(); + circuit_builder.set_trace(std::move(trace)); + + EXPECT_TRUE(circuit_builder.check_circuit()); + + auto composer = honk::AvmMiniComposer(); + auto prover = composer.create_prover(circuit_builder); + auto proof = prover.construct_proof(); + + auto verifier = composer.create_verifier(circuit_builder); + bool verified = verifier.verify_proof(proof); + + if (!verified) { + log_avmMini_trace(circuit_builder.rows, 0, 10); + } +}; + +/** + * @brief Helper routine for the negative tests. It mutates the output value of an operation + * located in the Ic intermediate register. The memory trace is adapted consistently. + * + * @param trace Execution trace + * @param selectRow Lambda serving to select the row in trace + * @param newValue The value that will be written in intermediate register Ic at the selected row. + */ +void mutateIcInTrace(std::vector& trace, std::function&& selectRow, FF const& newValue) +{ + // Find the first row matching the criteria defined by selectRow + auto row = std::ranges::find_if(trace.begin(), trace.end(), selectRow); + + // Check that we found one + EXPECT_TRUE(row != trace.end()); + + // Mutate the correct result in the main trace + row->avmMini_ic = newValue; + + // Adapt the memory trace to be consistent with the wrongly computed addition + auto const clk = row->avmMini_clk; + auto const addr = row->avmMini_mem_idx_c; + + // Find the relevant memory trace entry. + auto memRow = std::ranges::find_if(trace.begin(), trace.end(), [clk, addr](Row r) { + return r.memTrace_m_clk == clk && r.memTrace_m_addr == addr; + }); + + EXPECT_TRUE(memRow != trace.end()); + memRow->memTrace_m_val = newValue; +}; + +} // namespace tests_avm \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.hpp b/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.hpp new file mode 100644 index 00000000000..36732908f89 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.hpp @@ -0,0 +1,19 @@ +#pragma once + +#include "barretenberg/proof_system/circuit_builder/AvmMini_trace.hpp" + +#define EXPECT_THROW_WITH_MESSAGE(code, expectedMessage) \ + try { \ + code; \ + FAIL() << "An exception was expected"; \ + } catch (const std::exception& e) { \ + std::string message = e.what(); \ + EXPECT_TRUE(message.find(expectedMessage) != std::string::npos); \ + } + +namespace tests_avm { + +void validateTraceProof(std::vector&& trace); +void mutateIcInTrace(std::vector& trace, std::function&& selectRow, FF const& newValue); + +} // namespace tests_avm \ No newline at end of file