From 569171bf782b46451dcf4c95bba29690256b86dd Mon Sep 17 00:00:00 2001 From: jeanmon Date: Mon, 11 Dec 2023 16:29:44 +0000 Subject: [PATCH 01/12] 3644 - add tag in memory trace, adapt relations --- barretenberg/cpp/pil/avm/avm_mini_opt.pil | 9 +- barretenberg/cpp/pil/avm/mem_trace.pil | 34 ++++-- .../flavor/generated/AvmMini_flavor.hpp | 114 +++++++----------- .../circuit_builder/AvmMini_helper.cpp | 10 +- .../circuit_builder/AvmMini_trace.cpp | 6 +- .../generated/AvmMini_circuit_builder.hpp | 14 ++- .../relations/generated/AvmMini/avm_mini.hpp | 20 +-- .../generated/AvmMini/declare_views.hpp | 5 +- .../relations/generated/AvmMini/mem_trace.hpp | 55 ++++++--- .../vm/generated/AvmMini_composer.cpp | 2 + .../vm/generated/AvmMini_prover.cpp | 5 + .../vm/generated/AvmMini_verifier.cpp | 3 + .../vm/tests/AvmMini_arithmetic.test.cpp | 2 +- 13 files changed, 161 insertions(+), 118 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_mini_opt.pil b/barretenberg/cpp/pil/avm/avm_mini_opt.pil index 56019fb7197f..131545c84392 100644 --- a/barretenberg/cpp/pil/avm/avm_mini_opt.pil +++ b/barretenberg/cpp/pil/avm/avm_mini_opt.pil @@ -2,13 +2,18 @@ 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; (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; + ((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; namespace avmMini(256); col fixed clk(i) { i }; col fixed first = [1] + [0]*; diff --git a/barretenberg/cpp/pil/avm/mem_trace.pil b/barretenberg/cpp/pil/avm/mem_trace.pil index 38cc0813d2c9..5c45c5cac494 100644 --- a/barretenberg/cpp/pil/avm/mem_trace.pil +++ b/barretenberg/cpp/pil/avm/mem_trace.pil @@ -7,29 +7,38 @@ 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) - + // Type constraints m_lastAccess * (1 - m_lastAccess) = 0; + m_last * (1 - m_last) = 0; m_rw * (1 - m_rw) = 0; - + // TODO: m_addr is u32 and 0 <= m_tag <= 6 + + // 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) + (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 +49,17 @@ 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) + (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) + (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): + m_lastAccess * (1 - m_rw') * m_val' = 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 diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index c3b00281f706..c0e14282db02 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -34,13 +34,13 @@ 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 = 27; 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 = 33; - using Relations = std::tuple, AvmMini_vm::mem_trace>; + using Relations = std::tuple, AvmMini_vm::avm_mini>; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); @@ -77,8 +77,10 @@ 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, avmMini_sel_op_add, avmMini_sel_op_sub, @@ -102,13 +104,13 @@ 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, + 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 }; }; RefVector get_sorted_polynomials() { return {}; }; }; @@ -121,8 +123,10 @@ 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, avmMini_sel_op_add, avmMini_sel_op_sub, @@ -145,75 +149,39 @@ class AvmMiniFlavor { avmMini_last, memTrace_m_rw_shift, memTrace_m_val_shift, - memTrace_m_addr_shift) + memTrace_m_addr_shift, + memTrace_m_tag_shift) RefVector get_wires() { - return { avmMini_clk, - avmMini_first, - 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, - memTrace_m_rw_shift, - memTrace_m_val_shift, - memTrace_m_addr_shift }; + return { avmMini_clk, avmMini_first, 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, 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, memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, + memTrace_m_tag_shift }; }; RefVector get_unshifted() { - return { avmMini_clk, - avmMini_first, - 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, + return { avmMini_clk, avmMini_first, 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, 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 }; }; - RefVector get_to_be_shifted() { return { memTrace_m_rw, memTrace_m_val, memTrace_m_addr }; }; + RefVector get_to_be_shifted() + { + return { memTrace_m_rw, memTrace_m_val, memTrace_m_addr, memTrace_m_tag }; + }; RefVector get_shifted() { - return { memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift }; + return { memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_tag_shift }; }; }; @@ -291,8 +259,10 @@ 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::avmMini_sel_op_add = "AVMMINI_SEL_OP_ADD"; Base::avmMini_sel_op_sub = "AVMMINI_SEL_OP_SUB"; @@ -335,8 +305,10 @@ 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 avmMini_sel_op_add; Commitment avmMini_sel_op_sub; @@ -379,8 +351,10 @@ 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); 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); @@ -427,8 +401,10 @@ 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(avmMini_sel_op_add, Transcript::proof_data); serialize_to_buffer(avmMini_sel_op_sub, 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 401ad709c435..fe80d44ed632 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,20 @@ 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_last: ", trace.at(i).memTrace_m_last); info("m_rw: ", trace.at(i).memTrace_m_rw); 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 +44,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 8562a72c41cf..03a92640200c 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 @@ -559,8 +559,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); @@ -577,11 +576,12 @@ std::vector AvmMiniTraceBuilder::finalize() 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/generated/AvmMini_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp index 46cabaa1a0e2..673f39f3ac61 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 @@ -21,8 +21,10 @@ 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 avmMini_sel_op_add{}; FF avmMini_sel_op_sub{}; @@ -46,6 +48,7 @@ template struct AvmMiniFullRow { FF memTrace_m_rw_shift{}; FF memTrace_m_val_shift{}; FF memTrace_m_addr_shift{}; + FF memTrace_m_tag_shift{}; }; class AvmMiniCircuitBuilder { @@ -58,8 +61,8 @@ class AvmMiniCircuitBuilder { using Polynomial = Flavor::Polynomial; using AllPolynomials = Flavor::AllPolynomials; - static constexpr size_t num_fixed_columns = 30; - static constexpr size_t num_polys = 27; + static constexpr size_t num_fixed_columns = 33; + static constexpr size_t num_polys = 29; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -80,8 +83,10 @@ 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.avmMini_sel_op_add[i] = rows[i].avmMini_sel_op_add; polys.avmMini_sel_op_sub[i] = rows[i].avmMini_sel_op_sub; @@ -107,6 +112,7 @@ class AvmMiniCircuitBuilder { polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.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_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); return polys; } @@ -141,10 +147,10 @@ class AvmMiniCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("avm_mini")) { + if (!evaluate_relation.template operator()>("mem_trace")) { return false; } - if (!evaluate_relation.template operator()>("mem_trace")) { + if (!evaluate_relation.template operator()>("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 5596bbc94cfd..1aa0c6f054f8 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,21 +7,21 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { - FF avmMini_mem_op_b{}; - FF avmMini_ib{}; - FF avmMini_ic{}; - FF avmMini_sel_op_sub{}; - FF avmMini_mem_op_c{}; - FF avmMini_op_err{}; FF avmMini_ia{}; - FF avmMini_inv{}; + FF avmMini_sel_op_mul{}; FF avmMini_sel_op_div{}; - FF avmMini_mem_op_a{}; + FF avmMini_ic{}; + FF avmMini_op_err{}; FF avmMini_rwa{}; - FF avmMini_sel_op_mul{}; FF avmMini_rwc{}; - FF avmMini_sel_op_add{}; + FF avmMini_mem_op_b{}; + FF avmMini_sel_op_sub{}; + FF avmMini_mem_op_c{}; + FF avmMini_ib{}; FF avmMini_rwb{}; + FF avmMini_mem_op_a{}; + FF avmMini_sel_op_add{}; + FF avmMini_inv{}; }; template class avm_miniImpl { 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 b5d9a61651e7..a3f6778ad41b 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -7,8 +7,10 @@ [[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 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); \ @@ -31,4 +33,5 @@ [[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_addr_shift = View(new_term.memTrace_m_addr_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 dde059dedc65..08dd66dfbb84 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,24 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { + FF memTrace_m_val{}; + FF memTrace_m_rw{}; FF memTrace_m_rw_shift{}; - FF memTrace_m_lastAccess{}; - FF memTrace_m_addr{}; FF memTrace_m_val_shift{}; - FF memTrace_m_rw{}; - FF avmMini_first{}; FF memTrace_m_addr_shift{}; - FF avmMini_last{}; - FF memTrace_m_val{}; + FF memTrace_m_lastAccess{}; + FF memTrace_m_last{}; + FF memTrace_m_tag_shift{}; + FF memTrace_m_addr{}; + FF memTrace_m_tag{}; }; 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, 4, 4, 4, }; template @@ -48,7 +46,7 @@ template class mem_traceImpl { { 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 +54,7 @@ template class mem_traceImpl { { 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 +62,36 @@ template class mem_traceImpl { { 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_lastAccess + FF(1)) * (memTrace_m_addr_shift - memTrace_m_addr)); tmp *= scaling_factor; std::get<3>(evals) += tmp; } + // Contribution 4 + { + DECLARE_VIEWS(4); + + 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<4>(evals) += tmp; + } + // Contribution 5 + { + DECLARE_VIEWS(5); + + 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<5>(evals) += tmp; + } + // Contribution 6 + { + DECLARE_VIEWS(6); + + auto tmp = ((memTrace_m_lastAccess * (-memTrace_m_rw_shift + FF(1))) * memTrace_m_val_shift); + tmp *= scaling_factor; + std::get<6>(evals) += tmp; + } } }; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp index d07684fc3eca..48b5ba4339fc 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp @@ -22,8 +22,10 @@ void AvmMiniComposer::compute_witness(CircuitConstructor& circuit) proving_key->memTrace_m_clk = polynomials.memTrace_m_clk; proving_key->memTrace_m_sub_clk = polynomials.memTrace_m_sub_clk; proving_key->memTrace_m_addr = polynomials.memTrace_m_addr; + proving_key->memTrace_m_tag = polynomials.memTrace_m_tag; proving_key->memTrace_m_val = polynomials.memTrace_m_val; proving_key->memTrace_m_lastAccess = polynomials.memTrace_m_lastAccess; + proving_key->memTrace_m_last = polynomials.memTrace_m_last; proving_key->memTrace_m_rw = polynomials.memTrace_m_rw; proving_key->avmMini_sel_op_add = polynomials.avmMini_sel_op_add; proving_key->avmMini_sel_op_sub = polynomials.avmMini_sel_op_sub; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp index da10ff83a406..d083f21b34bd 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp @@ -34,8 +34,10 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.memTrace_m_clk = key->memTrace_m_clk; prover_polynomials.memTrace_m_sub_clk = key->memTrace_m_sub_clk; prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; + prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; prover_polynomials.memTrace_m_val = key->memTrace_m_val; prover_polynomials.memTrace_m_lastAccess = key->memTrace_m_lastAccess; + prover_polynomials.memTrace_m_last = key->memTrace_m_last; prover_polynomials.memTrace_m_rw = key->memTrace_m_rw; prover_polynomials.avmMini_sel_op_add = key->avmMini_sel_op_add; prover_polynomials.avmMini_sel_op_sub = key->avmMini_sel_op_sub; @@ -66,6 +68,9 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; prover_polynomials.memTrace_m_addr_shift = key->memTrace_m_addr.shifted(); + prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; + prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); + // prover_polynomials.lookup_inverses = key->lookup_inverses; // key->z_perm = Polynomial(key->circuit_size); // prover_polynomials.z_perm = key->z_perm; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp index 4014eec57bb7..224e8384d4eb 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp @@ -60,9 +60,12 @@ 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.avmMini_sel_op_add = transcript->template receive_from_prover(commitment_labels.avmMini_sel_op_add); 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 1a94d54816e5..fd9fe44e57c3 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp @@ -484,7 +484,7 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) // Activate the operator error row->avmMini_op_err = FF(1); - + log_avmMini_trace(trace, 0, 10); // TODO: check that the expected sub-relation failed EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); } From c2818c75f6eadb638e5b7766e5c695e308c7eac1 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Mon, 11 Dec 2023 17:57:51 +0000 Subject: [PATCH 02/12] 3644 - enhance witness generation with memory type in the instructions and in memory trace --- .../circuit_builder/AvmMini_trace.cpp | 183 ++++++++++-------- .../circuit_builder/AvmMini_trace.hpp | 43 ++-- .../vm/tests/AvmMini_arithmetic.test.cpp | 87 +++++---- 3 files changed, 171 insertions(+), 142 deletions(-) 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 03a92640200c..f0b9e6b1ecb1 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,33 +68,37 @@ 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_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 +// MainTrace, 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 + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::loadAInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::loadAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_A, addr, val, false); + // TODO: Check that m_in_tag is compatible to that at addr. + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_A, addr, val, m_in_tag, false); } /** @@ -103,10 +107,12 @@ void AvmMiniTraceBuilder::loadAInMemTrace(uint32_t addr, FF val) * * @param addr The memory address * @param val The value to be loaded + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::loadBInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::loadBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_B, addr, val, false); + // TODO: Check that m_in_tag is compatible to that at addr. + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_B, addr, val, m_in_tag, false); } /** @@ -115,10 +121,12 @@ void AvmMiniTraceBuilder::loadBInMemTrace(uint32_t addr, FF val) * * @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) +void AvmMiniTraceBuilder::loadCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_C, addr, val, false); + // TODO: Check that m_in_tag is compatible to that at addr. + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_C, addr, val, m_in_tag, false); } /** @@ -127,10 +135,11 @@ void AvmMiniTraceBuilder::loadCInMemTrace(uint32_t addr, FF val) * * @param addr The memory address * @param val The value to be stored + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::storeAInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::storeAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_A, addr, val, true); + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_A, addr, val, m_in_tag, true); } /** @@ -139,10 +148,11 @@ void AvmMiniTraceBuilder::storeAInMemTrace(uint32_t addr, FF val) * * @param addr The memory address * @param val The value to be stored + * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::storeBInMemTrace(uint32_t addr, FF val) +void AvmMiniTraceBuilder::storeBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_B, addr, val, true); + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_B, addr, val, m_in_tag, true); } /** @@ -151,37 +161,40 @@ void AvmMiniTraceBuilder::storeBInMemTrace(uint32_t addr, FF val) * * @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::storeCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_C, addr, val, true); + insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_C, 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; + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; auto clk = mainTrace.size(); // Loading into Ia - loadAInMemTrace(aOffset, a); + loadAInMemTrace(aOffset, a, inTag); // Loading into Ib - loadBInMemTrace(bOffset, b); + loadBInMemTrace(bOffset, b, inTag); // Storing from Ic - storeCInMemTrace(dstOffset, c); + storeCInMemTrace(dstOffset, c, inTag); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -199,31 +212,33 @@ 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); + loadAInMemTrace(aOffset, a, inTag); // Loading into Ib - loadBInMemTrace(bOffset, b); + loadBInMemTrace(bOffset, b, inTag); // Storing from Ic - storeCInMemTrace(dstOffset, c); + storeCInMemTrace(dstOffset, c, inTag); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -241,31 +256,33 @@ 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; + memory.at(dstOffset) = c; + memoryTag.at(dstOffset) = inTag; auto clk = mainTrace.size(); // Loading into Ia - loadAInMemTrace(aOffset, a); + loadAInMemTrace(aOffset, a, inTag); // Loading into Ib - loadBInMemTrace(bOffset, b); + loadBInMemTrace(bOffset, b, inTag); // Storing from Ic - storeCInMemTrace(dstOffset, c); + storeCInMemTrace(dstOffset, c, inTag); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -283,18 +300,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,18 +328,19 @@ 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 - loadAInMemTrace(aOffset, a); + loadAInMemTrace(aOffset, a, inTag); // Loading into Ib - loadBInMemTrace(bOffset, b); + loadBInMemTrace(bOffset, b, inTag); // Storing from Ic - storeCInMemTrace(dstOffset, c); + storeCInMemTrace(dstOffset, c, inTag); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -389,8 +408,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; + storeAInMemTrace(mem_idx_a, ia, AvmMemoryTag::ff); if (copySize - pos > 1) { ib = callDataMem.at(cdOffset + pos + 1); @@ -399,8 +419,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; + storeBInMemTrace(mem_idx_b, ib, AvmMemoryTag::ff); } if (copySize - pos > 2) { @@ -410,8 +431,9 @@ 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; + storeCInMemTrace(mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ @@ -474,30 +496,30 @@ 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); + loadAInMemTrace(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); + loadBInMemTrace(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); + loadCInMemTrace(mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ @@ -523,12 +545,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; }; /** 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 a4621c22e199..e79a135dfc4a 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,8 @@ using Row = proof_system::AvmMiniFullRow; namespace proof_system { +enum class AvmMemoryTag { 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 +38,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] @@ -67,21 +69,24 @@ class AvmMiniTraceBuilder { uint32_t m_sub_clk; uint32_t m_addr; FF m_val; + AvmMemoryTag m_in_tag; bool m_rw; }; 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 loadAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void loadBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void loadCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void storeAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void storeBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void storeCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); }; } // namespace proof_system 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 fd9fe44e57c3..f38002fd94ef 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp @@ -123,8 +123,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 +146,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 +169,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 +192,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 +215,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 +238,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 +262,8 @@ 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 @@ -288,16 +288,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,8 +330,8 @@ 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,....] + // 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(); @@ -346,8 +347,8 @@ 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....] + // 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(); @@ -363,8 +364,8 @@ 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....] + // 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(); @@ -380,8 +381,8 @@ 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....] + // 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(); @@ -398,8 +399,8 @@ 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....] + // 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(); @@ -418,8 +419,8 @@ 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 @@ -438,8 +439,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(); @@ -456,8 +457,8 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) 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(); @@ -474,8 +475,8 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) 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(); @@ -484,7 +485,7 @@ TEST_F(AvmMiniArithmeticNegativeTests, operationWithErrorFlagFF) // Activate the operator error row->avmMini_op_err = FF(1); - log_avmMini_trace(trace, 0, 10); + // TODO: check that the expected sub-relation failed EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); } From 73a589ce1bcace1b61cf22f605a9264954d89004 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Tue, 12 Dec 2023 11:19:52 +0000 Subject: [PATCH 03/12] 3644 - minor comments in pil file --- barretenberg/cpp/pil/avm/avm_mini.pil | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/barretenberg/cpp/pil/avm/avm_mini.pil b/barretenberg/cpp/pil/avm/avm_mini.pil index 3bd9bc11b866..f7fb6c3ec648 100644 --- a/barretenberg/cpp/pil/avm/avm_mini.pil +++ b/barretenberg/cpp/pil/avm/avm_mini.pil @@ -72,6 +72,8 @@ namespace avmMini(256); rwb * (1 - rwb) = 0; rwc * (1 - rwc) = 0; + // TODO: Constrain rwa, rwb, rwc to u32 type + // Relation for addition over the finite field sel_op_add * (ia + ib - ic) = 0; @@ -87,7 +89,8 @@ namespace avmMini(256); // 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. sel_op_div * (ib * inv - 1 + op_err) = 0; sel_op_div * op_err * (1 - inv) = 0; From 1ff91418d1f6e09491d8ce5655e87ccb97e1e58e Mon Sep 17 00:00:00 2001 From: jeanmon Date: Tue, 12 Dec 2023 18:34:32 +0000 Subject: [PATCH 04/12] 3644 - add error handling for mismatch between in-tag and memory tag --- barretenberg/cpp/pil/avm/avm_mini.pil | 31 +++- barretenberg/cpp/pil/avm/avm_mini_opt.pil | 12 ++ barretenberg/cpp/pil/avm/mem_trace.pil | 30 +++- .../flavor/generated/AvmMini_flavor.hpp | 166 +++++++++++++++--- .../generated/AvmMini_circuit_builder.hpp | 22 ++- .../relations/generated/AvmMini/avm_mini.hpp | 83 ++++++--- .../generated/AvmMini/declare_views.hpp | 7 +- .../relations/generated/AvmMini/mem_trace.hpp | 52 ++++-- .../vm/generated/AvmMini_composer.cpp | 5 + .../vm/generated/AvmMini_prover.cpp | 11 +- .../vm/generated/AvmMini_verifier.cpp | 9 + 11 files changed, 345 insertions(+), 83 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_mini.pil b/barretenberg/cpp/pil/avm/avm_mini.pil index f7fb6c3ec648..e9c1189493de 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,7 +77,12 @@ namespace avmMini(256); rwb * (1 - rwb) = 0; rwc * (1 - rwc) = 0; - // TODO: Constrain rwa, rwb, rwc to u32 type + // 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 sel_op_add * (ia + ib - ic) = 0; @@ -84,6 +94,7 @@ namespace avmMini(256); 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. sel_op_div * (1 - op_err) * (ic * ib - ia) = 0; // When sel_op_div == 1, we want ib == 0 <==> op_err == 1 @@ -102,7 +113,7 @@ namespace avmMini(256); // At this time, we have only division producing an error. 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? @@ -111,4 +122,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 131545c84392..f3a75411a99d 100644 --- a/barretenberg/cpp/pil/avm/avm_mini_opt.pil +++ b/barretenberg/cpp/pil/avm/avm_mini_opt.pil @@ -7,13 +7,19 @@ namespace memTrace(256); 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; + (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]*; @@ -21,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; @@ -41,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 5c45c5cac494..ba6a6f7f4da7 100644 --- a/barretenberg/cpp/pil/avm/mem_trace.pil +++ b/barretenberg/cpp/pil/avm/mem_trace.pil @@ -13,11 +13,22 @@ namespace memTrace(256); 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) @@ -61,5 +72,22 @@ namespace memTrace(256); // 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): 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 introduce m_one_min_inv extra column to show that we can invert + // (m_in_tag - m_tag) when m_tag_err != 0 + // 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 + (m_in_tag - m_tag) * (1 - m_one_min_inv) - m_tag_err = 0; + (1 - m_tag_err) * m_one_min_inv = 0; + + // Correctness of above checks + // 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 c0e14282db02..d2c7e7930c49 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -34,13 +34,13 @@ class AvmMiniFlavor { using VerifierCommitmentKey = pcs::VerifierCommitmentKey; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; - static constexpr size_t NUM_WITNESS_ENTITIES = 27; + 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 = 33; + static constexpr size_t NUM_ALL_ENTITIES = 38; - using Relations = std::tuple, AvmMini_vm::avm_mini>; + using Relations = std::tuple, AvmMini_vm::mem_trace>; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); @@ -82,11 +82,16 @@ class AvmMiniFlavor { 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 +109,38 @@ class AvmMiniFlavor { RefVector get_wires() { - 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, - 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 {}; }; }; @@ -128,11 +158,16 @@ class AvmMiniFlavor { 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, @@ -147,41 +182,96 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, + memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_val_shift, - memTrace_m_addr_shift, memTrace_m_tag_shift) RefVector get_wires() { - return { avmMini_clk, avmMini_first, 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, 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, memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, + return { avmMini_clk, + avmMini_first, + 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, + memTrace_m_addr_shift, + memTrace_m_rw_shift, + memTrace_m_val_shift, memTrace_m_tag_shift }; }; RefVector get_unshifted() { - return { avmMini_clk, avmMini_first, 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, 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, + return { avmMini_clk, + avmMini_first, + 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_to_be_shifted() { - return { memTrace_m_rw, memTrace_m_val, memTrace_m_addr, memTrace_m_tag }; + return { memTrace_m_addr, memTrace_m_rw, memTrace_m_val, memTrace_m_tag }; }; RefVector get_shifted() { - return { memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_tag_shift }; + return { memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_tag_shift }; }; }; @@ -264,11 +354,16 @@ class AvmMiniFlavor { 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"; @@ -310,11 +405,16 @@ class AvmMiniFlavor { 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; @@ -356,11 +456,16 @@ class AvmMiniFlavor { 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); @@ -406,11 +511,16 @@ class AvmMiniFlavor { 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/generated/AvmMini_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp index 673f39f3ac61..be7f741ba664 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 @@ -26,11 +26,16 @@ template struct AvmMiniFullRow { 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{}; @@ -45,9 +50,9 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; + FF memTrace_m_addr_shift{}; FF memTrace_m_rw_shift{}; FF memTrace_m_val_shift{}; - FF memTrace_m_addr_shift{}; FF memTrace_m_tag_shift{}; }; @@ -61,8 +66,8 @@ class AvmMiniCircuitBuilder { using Polynomial = Flavor::Polynomial; using AllPolynomials = Flavor::AllPolynomials; - static constexpr size_t num_fixed_columns = 33; - static constexpr size_t num_polys = 29; + 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); } @@ -88,11 +93,16 @@ class AvmMiniCircuitBuilder { 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; @@ -109,9 +119,9 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } + 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_val_shift = Polynomial(polys.memTrace_m_val.shifted()); - polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted()); polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); return polys; @@ -147,10 +157,10 @@ class AvmMiniCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("mem_trace")) { + if (!evaluate_relation.template operator()>("avm_mini")) { return false; } - if (!evaluate_relation.template operator()>("avm_mini")) { + if (!evaluate_relation.template operator()>("mem_trace")) { 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 1aa0c6f054f8..1c212d840f10 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,30 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { - FF avmMini_ia{}; - FF avmMini_sel_op_mul{}; - FF avmMini_sel_op_div{}; + FF avmMini_inv{}; + FF avmMini_mem_op_a{}; + FF avmMini_rwb{}; + FF avmMini_ib{}; FF avmMini_ic{}; + FF avmMini_sel_op_div{}; FF avmMini_op_err{}; - FF avmMini_rwa{}; + FF avmMini_ia{}; FF avmMini_rwc{}; - FF avmMini_mem_op_b{}; - FF avmMini_sel_op_sub{}; + FF avmMini_sel_op_mul{}; FF avmMini_mem_op_c{}; - FF avmMini_ib{}; - FF avmMini_rwb{}; - FF avmMini_mem_op_a{}; + FF avmMini_rwa{}; FF avmMini_sel_op_add{}; - FF avmMini_inv{}; + FF avmMini_sel_op_sub{}; + FF avmMini_tag_err{}; + FF avmMini_mem_op_b{}; }; 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, 5, 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 +84,7 @@ template class avm_miniImpl { { 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 +92,7 @@ template class avm_miniImpl { { 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 +100,7 @@ template class avm_miniImpl { { 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 +108,7 @@ template class avm_miniImpl { { 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 +116,7 @@ template class avm_miniImpl { { 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 +124,7 @@ template class avm_miniImpl { { 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 +132,7 @@ template class avm_miniImpl { { 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 +140,7 @@ template class avm_miniImpl { { 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 +148,7 @@ template class avm_miniImpl { { 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 +156,7 @@ template class avm_miniImpl { { 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 +164,7 @@ template class avm_miniImpl { { 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 +172,7 @@ template class avm_miniImpl { { 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 +180,42 @@ template class avm_miniImpl { { 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 + { + 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 + { + 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 + { + 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 + { + 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 a3f6778ad41b..1514117f9bf3 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -12,11 +12,16 @@ [[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); \ @@ -31,7 +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_addr_shift = View(new_term.memTrace_m_addr_shift); \ [[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_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 08dd66dfbb84..fc939673acdf 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -7,24 +7,27 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { - FF memTrace_m_val{}; + FF memTrace_m_last{}; FF memTrace_m_rw{}; - FF memTrace_m_rw_shift{}; - FF memTrace_m_val_shift{}; + FF memTrace_m_val{}; + FF memTrace_m_one_min_inv{}; + FF memTrace_m_in_tag{}; FF memTrace_m_addr_shift{}; FF memTrace_m_lastAccess{}; - FF memTrace_m_last{}; + FF memTrace_m_tag{}; + FF memTrace_m_tag_err{}; + FF memTrace_m_rw_shift{}; + FF memTrace_m_val_shift{}; FF memTrace_m_tag_shift{}; FF memTrace_m_addr{}; - FF memTrace_m_tag{}; }; template class mem_traceImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, 3, 3, 3, 4, 4, 4, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 4, 4, 4, 3, 3, }; template @@ -62,7 +65,7 @@ template class mem_traceImpl { { DECLARE_VIEWS(3); - auto tmp = ((-memTrace_m_lastAccess + FF(1)) * (memTrace_m_addr_shift - memTrace_m_addr)); + auto tmp = (memTrace_m_tag_err * (-memTrace_m_tag_err + FF(1))); tmp *= scaling_factor; std::get<3>(evals) += tmp; } @@ -70,8 +73,7 @@ template class mem_traceImpl { { DECLARE_VIEWS(4); - auto tmp = (((-memTrace_m_lastAccess + FF(1)) * (-memTrace_m_rw_shift + FF(1))) * - (memTrace_m_val_shift - memTrace_m_val)); + auto tmp = ((-memTrace_m_lastAccess + FF(1)) * (memTrace_m_addr_shift - memTrace_m_addr)); tmp *= scaling_factor; std::get<4>(evals) += tmp; } @@ -80,7 +82,7 @@ template class mem_traceImpl { DECLARE_VIEWS(5); auto tmp = (((-memTrace_m_lastAccess + FF(1)) * (-memTrace_m_rw_shift + FF(1))) * - (memTrace_m_tag_shift - memTrace_m_tag)); + (memTrace_m_val_shift - memTrace_m_val)); tmp *= scaling_factor; std::get<5>(evals) += tmp; } @@ -88,10 +90,36 @@ template class mem_traceImpl { { DECLARE_VIEWS(6); - auto tmp = ((memTrace_m_lastAccess * (-memTrace_m_rw_shift + FF(1))) * memTrace_m_val_shift); + 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 + { + 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 + { + 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 + { + 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_composer.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp index 48b5ba4339fc..0d0209addd79 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_composer.cpp @@ -27,11 +27,16 @@ void AvmMiniComposer::compute_witness(CircuitConstructor& circuit) proving_key->memTrace_m_lastAccess = polynomials.memTrace_m_lastAccess; proving_key->memTrace_m_last = polynomials.memTrace_m_last; proving_key->memTrace_m_rw = polynomials.memTrace_m_rw; + proving_key->memTrace_m_in_tag = polynomials.memTrace_m_in_tag; + proving_key->memTrace_m_tag_err = polynomials.memTrace_m_tag_err; + proving_key->memTrace_m_one_min_inv = polynomials.memTrace_m_one_min_inv; proving_key->avmMini_sel_op_add = polynomials.avmMini_sel_op_add; proving_key->avmMini_sel_op_sub = polynomials.avmMini_sel_op_sub; proving_key->avmMini_sel_op_mul = polynomials.avmMini_sel_op_mul; proving_key->avmMini_sel_op_div = polynomials.avmMini_sel_op_div; + proving_key->avmMini_in_tag = polynomials.avmMini_in_tag; proving_key->avmMini_op_err = polynomials.avmMini_op_err; + proving_key->avmMini_tag_err = polynomials.avmMini_tag_err; proving_key->avmMini_inv = polynomials.avmMini_inv; proving_key->avmMini_ia = polynomials.avmMini_ia; proving_key->avmMini_ib = polynomials.avmMini_ib; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp index d083f21b34bd..1f937fcdbe28 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp @@ -39,11 +39,16 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.memTrace_m_lastAccess = key->memTrace_m_lastAccess; prover_polynomials.memTrace_m_last = key->memTrace_m_last; prover_polynomials.memTrace_m_rw = key->memTrace_m_rw; + prover_polynomials.memTrace_m_in_tag = key->memTrace_m_in_tag; + prover_polynomials.memTrace_m_tag_err = key->memTrace_m_tag_err; + prover_polynomials.memTrace_m_one_min_inv = key->memTrace_m_one_min_inv; prover_polynomials.avmMini_sel_op_add = key->avmMini_sel_op_add; prover_polynomials.avmMini_sel_op_sub = key->avmMini_sel_op_sub; prover_polynomials.avmMini_sel_op_mul = key->avmMini_sel_op_mul; prover_polynomials.avmMini_sel_op_div = key->avmMini_sel_op_div; + prover_polynomials.avmMini_in_tag = key->avmMini_in_tag; prover_polynomials.avmMini_op_err = key->avmMini_op_err; + prover_polynomials.avmMini_tag_err = key->avmMini_tag_err; prover_polynomials.avmMini_inv = key->avmMini_inv; prover_polynomials.avmMini_ia = key->avmMini_ia; prover_polynomials.avmMini_ib = key->avmMini_ib; @@ -59,15 +64,15 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.avmMini_mem_idx_c = key->avmMini_mem_idx_c; prover_polynomials.avmMini_last = key->avmMini_last; + prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; + prover_polynomials.memTrace_m_addr_shift = key->memTrace_m_addr.shifted(); + prover_polynomials.memTrace_m_rw = key->memTrace_m_rw; prover_polynomials.memTrace_m_rw_shift = key->memTrace_m_rw.shifted(); prover_polynomials.memTrace_m_val = key->memTrace_m_val; prover_polynomials.memTrace_m_val_shift = key->memTrace_m_val.shifted(); - prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; - prover_polynomials.memTrace_m_addr_shift = key->memTrace_m_addr.shifted(); - prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp index 224e8384d4eb..ff07a0754195 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_verifier.cpp @@ -67,6 +67,12 @@ bool AvmMiniVerifier::verify_proof(const plonk::proof& proof) 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 = @@ -75,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); From c54093e5ed7a005716774d11c7b54ace21e499dc Mon Sep 17 00:00:00 2001 From: jeanmon Date: Wed, 13 Dec 2023 10:32:32 +0000 Subject: [PATCH 05/12] 3644 - introduce an enum for intermediate registers and refactor load/store routines --- .../circuit_builder/AvmMini_trace.cpp | 161 +++++++----------- .../circuit_builder/AvmMini_trace.hpp | 11 +- 2 files changed, 64 insertions(+), 108 deletions(-) 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 f0b9e6b1ecb1..cd7727f0241d 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 @@ -85,87 +85,62 @@ void AvmMiniTraceBuilder::insertInMemTrace( } // 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 : 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 - * @param m_in_tag The memory tag of the instruction - */ -void AvmMiniTraceBuilder::loadAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) -{ - // TODO: Check that m_in_tag is compatible to that at addr. - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_A, addr, val, m_in_tag, false); -} +// 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 Ib. + * 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::loadBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) +void AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - // TODO: Check that m_in_tag is compatible to that at addr. - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_B, addr, val, m_in_tag, 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 load into the intermediate - * register Ic. - * - * @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, AvmMemoryTag m_in_tag) -{ // TODO: Check that m_in_tag is compatible to that at addr. - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_LOAD_C, addr, val, m_in_tag, false); + insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, false); } /** * @brief Add a memory trace entry corresponding to a memory store from the intermediate - * register Ia. + * 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::storeAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) +void AvmMiniTraceBuilder::storeInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) { - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_A, addr, val, m_in_tag, 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 - * @param m_in_tag The memory tag of the instruction - */ -void AvmMiniTraceBuilder::storeBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag) -{ - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_B, addr, val, m_in_tag, 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; + } -/** - * @brief Add a memory trace entry corresponding to a memory store from the intermediate - * register Ic. - * - * @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, AvmMemoryTag m_in_tag) -{ - insertInMemTrace(static_cast(mainTrace.size()), SUB_CLK_STORE_C, addr, val, m_in_tag, true); + insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, true); } /** TODO: Implement for non finite field types @@ -185,16 +160,12 @@ void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memory.at(dstOffset) = c; memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); - - // Loading into Ia - loadAInMemTrace(aOffset, a, inTag); + // Loading into Ia, Ib and storing into Ic + loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ib - loadBInMemTrace(bOffset, b, inTag); - - // Storing from Ic - storeCInMemTrace(dstOffset, c, inTag); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -229,16 +200,12 @@ void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memory.at(dstOffset) = c; memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); - - // Loading into Ia - loadAInMemTrace(aOffset, a, inTag); + // Loading into Ia, Ib and storing into Ic + loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ib - loadBInMemTrace(bOffset, b, inTag); - - // Storing from Ic - storeCInMemTrace(dstOffset, c, inTag); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -273,16 +240,12 @@ void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memory.at(dstOffset) = c; memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); - - // Loading into Ia - loadAInMemTrace(aOffset, a, inTag); - - // Loading into Ib - loadBInMemTrace(bOffset, b, inTag); + // Loading into Ia, Ib and storing into Ic + loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Storing from Ic - storeCInMemTrace(dstOffset, c, inTag); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -331,16 +294,12 @@ void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memory.at(dstOffset) = c; memoryTag.at(dstOffset) = inTag; - auto clk = mainTrace.size(); + // Loading into Ia, Ib and storing into Ic + loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); - // Loading into Ia - loadAInMemTrace(aOffset, a, inTag); - - // Loading into Ib - loadBInMemTrace(bOffset, b, inTag); - - // Storing from Ic - storeCInMemTrace(dstOffset, c, inTag); + auto clk = mainTrace.size(); mainTrace.push_back(Row{ .avmMini_clk = clk, @@ -410,7 +369,7 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, // Storing from Ia memory.at(mem_idx_a) = ia; memoryTag.at(mem_idx_a) = AvmMemoryTag::ff; - storeAInMemTrace(mem_idx_a, ia, AvmMemoryTag::ff); + storeInMemTrace(IntermRegister::ia, mem_idx_a, ia, AvmMemoryTag::ff); if (copySize - pos > 1) { ib = callDataMem.at(cdOffset + pos + 1); @@ -421,7 +380,7 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, // Storing from Ib memory.at(mem_idx_b) = ib; memoryTag.at(mem_idx_b) = AvmMemoryTag::ff; - storeBInMemTrace(mem_idx_b, ib, AvmMemoryTag::ff); + storeInMemTrace(IntermRegister::ib, mem_idx_b, ib, AvmMemoryTag::ff); } if (copySize - pos > 2) { @@ -433,7 +392,7 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, // Storing from Ic memory.at(mem_idx_c) = ic; memoryTag.at(mem_idx_c) = AvmMemoryTag::ff; - storeCInMemTrace(mem_idx_c, ic, AvmMemoryTag::ff); + storeInMemTrace(IntermRegister::ic, mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ @@ -500,7 +459,7 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi // Loading from Ia returnMem.push_back(ia); - loadAInMemTrace(mem_idx_a, ia, AvmMemoryTag::ff); + loadInMemTrace(IntermRegister::ia, mem_idx_a, ia, AvmMemoryTag::ff); if (retSize - pos > 1) { mem_op_b = 1; @@ -509,7 +468,7 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi // Loading from Ib returnMem.push_back(ib); - loadBInMemTrace(mem_idx_b, ib, AvmMemoryTag::ff); + loadInMemTrace(IntermRegister::ib, mem_idx_b, ib, AvmMemoryTag::ff); } if (retSize - pos > 2) { @@ -519,7 +478,7 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi // Loading from Ic returnMem.push_back(ic); - loadCInMemTrace(mem_idx_c, ic, AvmMemoryTag::ff); + loadInMemTrace(IntermRegister::ic, mem_idx_c, ic, AvmMemoryTag::ff); } mainTrace.push_back(Row{ 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 e79a135dfc4a..40213e84cc56 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,7 +15,8 @@ using Row = proof_system::AvmMiniFullRow; namespace proof_system { -enum class AvmMemoryTag { u0 = 0, u8 = 1, u16 = 2, u32 = 3, u64 = 4, u128 = 5, ff = 6 }; +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. @@ -82,11 +83,7 @@ class AvmMiniTraceBuilder { 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, AvmMemoryTag m_in_tag, bool m_rw); - void loadAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); - void loadBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); - void loadCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); - void storeAInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); - void storeBInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); - void storeCInMemTrace(uint32_t addr, FF val, AvmMemoryTag m_in_tag); + void 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 From 6e8d9d2719c808996533ea8d99bf8a7cb81f6b02 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 14 Dec 2023 11:05:06 +0000 Subject: [PATCH 06/12] 3644 - witness generation with error handling of tagged memory --- .../circuit_builder/AvmMini_trace.cpp | 86 +++++++++++++------ .../circuit_builder/AvmMini_trace.hpp | 9 +- 2 files changed, 68 insertions(+), 27 deletions(-) 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 cd7727f0241d..46f816f4235b 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 @@ -79,11 +79,26 @@ void AvmMiniTraceBuilder::insertInMemTrace( .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, }); } +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) +{ + 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 }); +} + // 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. @@ -97,7 +112,7 @@ void AvmMiniTraceBuilder::insertInMemTrace( * @param val The value to be loaded * @param m_in_tag The memory tag of the instruction */ -void AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) +bool AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag) { uint32_t sub_clk = 0; switch (intermReg) { @@ -112,8 +127,15 @@ void AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr break; } - // TODO: Check that m_in_tag is compatible to that at addr. - insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, false); + auto m_tag = memoryTag.at(addr); + if (m_tag == m_in_tag) { + insertInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, false); + return true; + } + + // Handle memory tag inconsistency + loadMismatchTagInMemTrace(static_cast(mainTrace.size()), sub_clk, addr, val, m_in_tag, m_tag); + return false; } /** @@ -161,8 +183,8 @@ void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memoryTag.at(dstOffset) = inTag; // Loading into Ia, Ib and storing into Ic - loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); - loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); auto clk = mainTrace.size(); @@ -170,9 +192,11 @@ void AvmMiniTraceBuilder::add(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf 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), @@ -201,8 +225,8 @@ void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memoryTag.at(dstOffset) = inTag; // Loading into Ia, Ib and storing into Ic - loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); - loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); auto clk = mainTrace.size(); @@ -210,9 +234,11 @@ void AvmMiniTraceBuilder::sub(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf 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,8 +267,8 @@ void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memoryTag.at(dstOffset) = inTag; // Loading into Ia, Ib and storing into Ic - loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); - loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); auto clk = mainTrace.size(); @@ -250,9 +276,11 @@ void AvmMiniTraceBuilder::mul(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf 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), @@ -295,8 +323,8 @@ void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf memoryTag.at(dstOffset) = inTag; // Loading into Ia, Ib and storing into Ic - loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); - loadInMemTrace(IntermRegister::ib, bOffset, b, inTag); + bool tagMatch = loadInMemTrace(IntermRegister::ia, aOffset, a, inTag); + tagMatch = loadInMemTrace(IntermRegister::ib, bOffset, b, inTag) && tagMatch; storeInMemTrace(IntermRegister::ic, dstOffset, c, inTag); auto clk = mainTrace.size(); @@ -304,11 +332,13 @@ void AvmMiniTraceBuilder::div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOf 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), @@ -397,6 +427,7 @@ void AvmMiniTraceBuilder::callDataCopy(uint32_t cdOffset, mainTrace.push_back(Row{ .avmMini_clk = clk, + .avmMini_in_tag = FF(static_cast(AvmMemoryTag::ff)), .avmMini_ia = ia, .avmMini_ib = ib, .avmMini_ic = ic, @@ -483,6 +514,7 @@ std::vector AvmMiniTraceBuilder::returnOP(uint32_t retOffset, uint32_t retSi mainTrace.push_back(Row{ .avmMini_clk = clk, + .avmMini_in_tag = FF(static_cast(AvmMemoryTag::ff)), .avmMini_ia = ia, .avmMini_ib = ib, .avmMini_ic = ic, @@ -552,6 +584,10 @@ 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); 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 40213e84cc56..f2ce26883d96 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 @@ -69,9 +69,12 @@ class AvmMiniTraceBuilder { uint32_t m_clk; uint32_t m_sub_clk; uint32_t m_addr; - FF m_val; + FF m_val{}; + AvmMemoryTag m_tag; AvmMemoryTag m_in_tag; bool m_rw; + bool m_tag_err; + FF m_one_min_inv{}; }; std::vector mainTrace; @@ -83,7 +86,9 @@ class AvmMiniTraceBuilder { 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, AvmMemoryTag m_in_tag, bool m_rw); - void loadInMemTrace(IntermRegister intermReg, uint32_t addr, FF val, AvmMemoryTag m_in_tag); + 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 From 56f96a296114f1bbbff5a5cc6eebd1522600b499 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 14 Dec 2023 17:30:37 +0000 Subject: [PATCH 07/12] 3644 - enhance negative unit tests with tagging the failing relations --- barretenberg/cpp/pil/avm/avm_mini.pil | 7 +++ .../flavor/generated/AvmMini_flavor.hpp | 16 +++--- .../generated/AvmMini_circuit_builder.hpp | 8 +-- .../relations/generated/AvmMini/avm_mini.hpp | 37 +++++++++++--- .../generated/AvmMini/declare_views.hpp | 6 +-- .../relations/generated/AvmMini/mem_trace.hpp | 18 +++---- .../vm/generated/AvmMini_prover.cpp | 10 ++-- .../vm/tests/AvmMini_arithmetic.test.cpp | 51 ++++++++++--------- 8 files changed, 92 insertions(+), 61 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_mini.pil b/barretenberg/cpp/pil/avm/avm_mini.pil index e9c1189493de..1fca367bf959 100644 --- a/barretenberg/cpp/pil/avm/avm_mini.pil +++ b/barretenberg/cpp/pil/avm/avm_mini.pil @@ -85,16 +85,20 @@ namespace avmMini(256); 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 @@ -102,7 +106,9 @@ namespace avmMini(256); // 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, // 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 @@ -111,6 +117,7 @@ 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 (tag_err or op_err) diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index 6bc0055f1250..45a3a8af91d0 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -184,10 +184,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_val_shift, + memTrace_m_tag_shift, memTrace_m_rw_shift, - memTrace_m_addr_shift, - memTrace_m_tag_shift) + memTrace_m_val_shift, + memTrace_m_addr_shift) RefVector get_wires() { @@ -225,10 +225,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_val_shift, + memTrace_m_tag_shift, memTrace_m_rw_shift, - memTrace_m_addr_shift, - memTrace_m_tag_shift }; + memTrace_m_val_shift, + memTrace_m_addr_shift }; }; RefVector get_unshifted() { @@ -269,11 +269,11 @@ class AvmMiniFlavor { }; RefVector get_to_be_shifted() { - return { memTrace_m_val, memTrace_m_rw, memTrace_m_addr, memTrace_m_tag }; + return { memTrace_m_tag, memTrace_m_rw, memTrace_m_val, memTrace_m_addr }; }; RefVector get_shifted() { - return { memTrace_m_val_shift, memTrace_m_rw_shift, memTrace_m_addr_shift, memTrace_m_tag_shift }; + return { memTrace_m_tag_shift, memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift }; }; }; 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 12fc00a256bb..2c47e1856bf1 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 @@ -53,10 +53,10 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; - FF memTrace_m_val_shift{}; + FF memTrace_m_tag_shift{}; FF memTrace_m_rw_shift{}; + FF memTrace_m_val_shift{}; FF memTrace_m_addr_shift{}; - FF memTrace_m_tag_shift{}; }; class AvmMiniCircuitBuilder { @@ -122,10 +122,10 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } - polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted()); + polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.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_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); return polys; } 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 8557381ea711..1788dcc187b7 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,19 +7,19 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { + FF avmMini_ib{}; + FF avmMini_sel_op_div{}; + FF avmMini_sel_op_add{}; FF avmMini_inv{}; + FF avmMini_ia{}; + FF avmMini_mem_op_c{}; + FF avmMini_sel_op_sub{}; FF avmMini_mem_op_b{}; FF avmMini_rwb{}; - FF avmMini_ia{}; - FF avmMini_sel_op_mul{}; - FF avmMini_sel_op_add{}; FF avmMini_tag_err{}; - FF avmMini_sel_op_div{}; - FF avmMini_mem_op_c{}; FF avmMini_mem_op_a{}; - FF avmMini_sel_op_sub{}; FF avmMini_rwc{}; - FF avmMini_ib{}; + FF avmMini_sel_op_mul{}; FF avmMini_rwa{}; FF avmMini_ic{}; FF avmMini_op_err{}; @@ -27,7 +27,28 @@ template struct Avm_miniRow { inline std::string get_relation_label_avm_mini(int index) { - switch (index) {} + switch (index) { + case 17: + return "SUBOP_MULTIPLICATION_FF"; + + case 19: + return "SUBOP_DIVISION_ZERO_ERR1"; + + case 15: + return "SUBOP_ADDITION_FF"; + + case 21: + return "SUBOP_ERROR_RELEVANT_OP"; + + case 16: + return "SUBOP_SUBTRACTION_FF"; + + case 18: + return "SUBOP_DIVISION_FF"; + + case 20: + return "SUBOP_DIVISION_ZERO_ERR2"; + } return std::to_string(index); } diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp index b097616dfdea..37691834554a 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -36,7 +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_val_shift = View(new_term.memTrace_m_val_shift); \ + [[maybe_unused]] auto memTrace_m_tag_shift = View(new_term.memTrace_m_tag_shift); \ [[maybe_unused]] auto memTrace_m_rw_shift = View(new_term.memTrace_m_rw_shift); \ - [[maybe_unused]] auto memTrace_m_addr_shift = View(new_term.memTrace_m_addr_shift); \ - [[maybe_unused]] auto memTrace_m_tag_shift = View(new_term.memTrace_m_tag_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); 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 c729454f9ded..4385c38018f0 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -7,19 +7,19 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { - FF memTrace_m_val_shift{}; - FF memTrace_m_one_min_inv{}; - FF memTrace_m_rw_shift{}; - FF memTrace_m_addr_shift{}; + FF memTrace_m_tag_shift{}; FF memTrace_m_in_tag{}; - FF memTrace_m_rw{}; + FF memTrace_m_last{}; + FF memTrace_m_rw_shift{}; FF memTrace_m_tag{}; - FF memTrace_m_tag_shift{}; - FF memTrace_m_addr{}; + FF memTrace_m_one_min_inv{}; + FF memTrace_m_val_shift{}; + FF memTrace_m_rw{}; + FF memTrace_m_tag_err{}; FF memTrace_m_lastAccess{}; + FF memTrace_m_addr_shift{}; + FF memTrace_m_addr{}; FF memTrace_m_val{}; - FF memTrace_m_last{}; - FF memTrace_m_tag_err{}; }; inline std::string get_relation_label_mem_trace(int index) diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp index e007d7c27356..040d844ac0c6 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp @@ -65,18 +65,18 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.avmMini_mem_idx_c = key->avmMini_mem_idx_c; prover_polynomials.avmMini_last = key->avmMini_last; - prover_polynomials.memTrace_m_val = key->memTrace_m_val; - prover_polynomials.memTrace_m_val_shift = key->memTrace_m_val.shifted(); + prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; + prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); prover_polynomials.memTrace_m_rw = key->memTrace_m_rw; prover_polynomials.memTrace_m_rw_shift = key->memTrace_m_rw.shifted(); + prover_polynomials.memTrace_m_val = key->memTrace_m_val; + prover_polynomials.memTrace_m_val_shift = key->memTrace_m_val.shifted(); + prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; prover_polynomials.memTrace_m_addr_shift = key->memTrace_m_addr.shifted(); - prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; - prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); - // prover_polynomials.lookup_inverses = key->lookup_inverses; // key->z_perm = Polynomial(key->circuit_size); // prover_polynomials.z_perm = key->z_perm; 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 f38002fd94ef..4338eb85ac0e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_arithmetic.test.cpp @@ -14,6 +14,15 @@ #include #include +#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); \ + } + using namespace proof_system; namespace tests_avm { @@ -332,14 +341,12 @@ TEST_F(AvmMiniArithmeticNegativeTests, additionFF) // 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(); 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. @@ -349,14 +356,12 @@ TEST_F(AvmMiniArithmeticNegativeTests, subtractionFF) // 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(); 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. @@ -366,14 +371,12 @@ TEST_F(AvmMiniArithmeticNegativeTests, multiplicationFF) // 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(); 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. @@ -383,14 +386,12 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionFF) // 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(); 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 @@ -401,17 +402,23 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionNoZeroButErrorFF) // 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(); // 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; + + EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_ZERO_ERR1"); - // TODO: check that the expected sub-relation failed - EXPECT_ANY_THROW(validateTraceProof(std::move(trace))); + // 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) @@ -429,8 +436,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 @@ -450,8 +456,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"); trace_builder.reset(); @@ -468,8 +473,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"); trace_builder.reset(); @@ -486,8 +490,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 From 193a38b77f2d2421110f1526f823c61df65ade8d Mon Sep 17 00:00:00 2001 From: jeanmon Date: Mon, 18 Dec 2023 13:08:48 +0000 Subject: [PATCH 08/12] 3644 - unit tests for tagged memory and various improvements --- barretenberg/cpp/pil/avm/mem_trace.pil | 6 + .../flavor/generated/AvmMini_flavor.hpp | 12 +- .../circuit_builder/AvmMini_helper.cpp | 7 +- .../circuit_builder/AvmMini_trace.cpp | 2 +- .../generated/AvmMini_circuit_builder.hpp | 4 +- .../relations/generated/AvmMini/avm_mini.hpp | 30 +-- .../generated/AvmMini/declare_views.hpp | 4 +- .../relations/generated/AvmMini/mem_trace.hpp | 38 ++- .../vm/generated/AvmMini_prover.cpp | 6 +- .../vm/tests/AvmMini_arithmetic.test.cpp | 110 +++----- .../vm/tests/AvmMini_memory.test.cpp | 252 ++++++++++++++++++ .../barretenberg/vm/tests/helpers.test.cpp | 69 +++++ .../barretenberg/vm/tests/helpers.test.hpp | 19 ++ 13 files changed, 448 insertions(+), 111 deletions(-) create mode 100644 barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp create mode 100644 barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.cpp create mode 100644 barretenberg/cpp/src/barretenberg/vm/tests/helpers.test.hpp diff --git a/barretenberg/cpp/pil/avm/mem_trace.pil b/barretenberg/cpp/pil/avm/mem_trace.pil index ba6a6f7f4da7..d472316c6fd1 100644 --- a/barretenberg/cpp/pil/avm/mem_trace.pil +++ b/barretenberg/cpp/pil/avm/mem_trace.pil @@ -36,6 +36,7 @@ namespace memTrace(256); // m_lastAccess == 0 ==> m_addr' == m_addr // 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 @@ -61,15 +62,18 @@ namespace memTrace(256); // Note2: in barretenberg, if a poynomial is shifted, its non-shifted equivalent must be 0 on the first row // 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; // 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 @@ -78,7 +82,9 @@ namespace memTrace(256); // (m_in_tag - m_tag) when m_tag_err != 0 // 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 above checks diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index 45a3a8af91d0..5c95ab95b92b 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -184,10 +184,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_tag_shift, memTrace_m_rw_shift, memTrace_m_val_shift, - memTrace_m_addr_shift) + memTrace_m_addr_shift, + memTrace_m_tag_shift) RefVector get_wires() { @@ -225,10 +225,10 @@ class AvmMiniFlavor { avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last, - memTrace_m_tag_shift, memTrace_m_rw_shift, memTrace_m_val_shift, - memTrace_m_addr_shift }; + memTrace_m_addr_shift, + memTrace_m_tag_shift }; }; RefVector get_unshifted() { @@ -269,11 +269,11 @@ class AvmMiniFlavor { }; RefVector get_to_be_shifted() { - return { memTrace_m_tag, memTrace_m_rw, memTrace_m_val, memTrace_m_addr }; + return { memTrace_m_rw, memTrace_m_val, memTrace_m_addr, memTrace_m_tag }; }; RefVector get_shifted() { - return { memTrace_m_tag_shift, memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift }; + return { memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_tag_shift }; }; }; 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 fe80d44ed632..e3ee39cff934 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 @@ -28,9 +28,14 @@ void log_avmMini_trace(std::vector const& trace, size_t beg, size_t end) 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_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_rw: ", trace.at(i).memTrace_m_rw); info("m_val_shift: ", trace.at(i).memTrace_m_val_shift); info("=======MAIN TRACE==============================================================="); 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 46f816f4235b..fd4c46ffef5f 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 @@ -128,7 +128,7 @@ bool AvmMiniTraceBuilder::loadInMemTrace(IntermRegister intermReg, uint32_t addr } auto m_tag = memoryTag.at(addr); - if (m_tag == m_in_tag) { + 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; } 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 2c47e1856bf1..4fb25042de3a 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 @@ -53,10 +53,10 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; - FF memTrace_m_tag_shift{}; FF memTrace_m_rw_shift{}; FF memTrace_m_val_shift{}; FF memTrace_m_addr_shift{}; + FF memTrace_m_tag_shift{}; }; class AvmMiniCircuitBuilder { @@ -122,10 +122,10 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } - polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.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_tag_shift = Polynomial(polys.memTrace_m_tag.shifted()); return polys; } 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 1788dcc187b7..d671e7285173 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,22 +7,22 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { + FF avmMini_mem_op_b{}; + FF avmMini_ia{}; FF avmMini_ib{}; - FF avmMini_sel_op_div{}; + FF avmMini_rwc{}; + FF avmMini_tag_err{}; FF avmMini_sel_op_add{}; - FF avmMini_inv{}; - FF avmMini_ia{}; - FF avmMini_mem_op_c{}; FF avmMini_sel_op_sub{}; - FF avmMini_mem_op_b{}; FF avmMini_rwb{}; - FF avmMini_tag_err{}; + FF avmMini_sel_op_div{}; + FF avmMini_rwa{}; FF avmMini_mem_op_a{}; - FF avmMini_rwc{}; + FF avmMini_op_err{}; FF avmMini_sel_op_mul{}; - FF avmMini_rwa{}; + FF avmMini_mem_op_c{}; + FF avmMini_inv{}; FF avmMini_ic{}; - FF avmMini_op_err{}; }; inline std::string get_relation_label_avm_mini(int index) @@ -31,18 +31,18 @@ inline std::string get_relation_label_avm_mini(int index) case 17: return "SUBOP_MULTIPLICATION_FF"; - case 19: - return "SUBOP_DIVISION_ZERO_ERR1"; - - case 15: - return "SUBOP_ADDITION_FF"; - case 21: return "SUBOP_ERROR_RELEVANT_OP"; + case 19: + return "SUBOP_DIVISION_ZERO_ERR1"; + case 16: return "SUBOP_SUBTRACTION_FF"; + case 15: + return "SUBOP_ADDITION_FF"; + case 18: return "SUBOP_DIVISION_FF"; 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 37691834554a..83b8f8975192 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -36,7 +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_tag_shift = View(new_term.memTrace_m_tag_shift); \ [[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_addr_shift = View(new_term.memTrace_m_addr_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 4385c38018f0..8d2ae9fe351f 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -7,24 +7,42 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { - FF memTrace_m_tag_shift{}; - FF memTrace_m_in_tag{}; - FF memTrace_m_last{}; + FF memTrace_m_lastAccess{}; + FF memTrace_m_tag_err{}; + FF memTrace_m_addr{}; FF memTrace_m_rw_shift{}; - FF memTrace_m_tag{}; - FF memTrace_m_one_min_inv{}; FF memTrace_m_val_shift{}; - FF memTrace_m_rw{}; - FF memTrace_m_tag_err{}; - FF memTrace_m_lastAccess{}; FF memTrace_m_addr_shift{}; - FF memTrace_m_addr{}; FF memTrace_m_val{}; + FF memTrace_m_tag_shift{}; + FF memTrace_m_tag{}; + FF memTrace_m_last{}; + FF memTrace_m_in_tag{}; + FF memTrace_m_one_min_inv{}; + FF memTrace_m_rw{}; }; inline std::string get_relation_label_mem_trace(int index) { - switch (index) {} + switch (index) { + case 5: + return "MEM_READ_WRITE_VAL_CONSISTENCY"; + + case 4: + return "MEM_LAST_ACCESS_DELIMITER"; + + case 6: + return "MEM_READ_WRITE_TAG_CONSISTENCY"; + + case 7: + return "MEM_ZERO_INIT"; + + case 8: + return "MEM_IN_TAG_CONSISTENCY_1"; + + case 9: + return "MEM_IN_TAG_CONSISTENCY_2"; + } return std::to_string(index); } diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp index 040d844ac0c6..cc9a6b0182dc 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/AvmMini_prover.cpp @@ -65,9 +65,6 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.avmMini_mem_idx_c = key->avmMini_mem_idx_c; prover_polynomials.avmMini_last = key->avmMini_last; - prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; - prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); - prover_polynomials.memTrace_m_rw = key->memTrace_m_rw; prover_polynomials.memTrace_m_rw_shift = key->memTrace_m_rw.shifted(); @@ -77,6 +74,9 @@ AvmMiniProver::AvmMiniProver(std::shared_ptr input_key, prover_polynomials.memTrace_m_addr = key->memTrace_m_addr; prover_polynomials.memTrace_m_addr_shift = key->memTrace_m_addr.shifted(); + prover_polynomials.memTrace_m_tag = key->memTrace_m_tag; + prover_polynomials.memTrace_m_tag_shift = key->memTrace_m_tag.shifted(); + // prover_polynomials.lookup_inverses = key->lookup_inverses; // key->z_perm = Polynomial(key->circuit_size); // prover_polynomials.z_perm = key->z_perm; 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 4338eb85ac0e..ad7b43424690 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 @@ -14,15 +15,6 @@ #include #include -#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); \ - } - using namespace proof_system; namespace tests_avm { @@ -42,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 @@ -289,6 +220,28 @@ TEST_F(AvmMiniArithmeticTests, divisionByZeroErrorFF) 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 + 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)); +} + // Testing an execution of the different arithmetic opcodes over finite field // and finishing with a division by zero. The chosen combination is arbitrary. // We only test that the proof can be correctly generated and verified. @@ -411,7 +364,6 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionNoZeroButErrorFF) // Activate the operator error trace[index].avmMini_op_err = FF(1); - auto trace2 = trace; EXPECT_THROW_WITH_MESSAGE(validateTraceProof(std::move(trace)), "SUBOP_DIVISION_ZERO_ERR1"); @@ -436,6 +388,22 @@ TEST_F(AvmMiniArithmeticNegativeTests, divisionByZeroNoErrorFF) // 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 + 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_ZERO_ERR1"); } 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 000000000000..887cd727f3f3 --- /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 addition 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 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; + }); + + 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 addition 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 000000000000..9cfb6fe7a17f --- /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 000000000000..36732908f899 --- /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 From 1c27b38dc36ff4fc2095266312c5c6201d93c33b Mon Sep 17 00:00:00 2001 From: jeanmon Date: Mon, 18 Dec 2023 13:23:36 +0000 Subject: [PATCH 09/12] 3644 - repair build --- .../proof_system/circuit_builder/AvmMini_trace.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 f2ce26883d96..5f5f7e8353db 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 @@ -72,8 +72,8 @@ class AvmMiniTraceBuilder { FF m_val{}; AvmMemoryTag m_tag; AvmMemoryTag m_in_tag; - bool m_rw; - bool m_tag_err; + bool m_rw = false; + bool m_tag_err = false; FF m_one_min_inv{}; }; From 08922cec6be42514a78ca517be67c71bac19b4b1 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Mon, 18 Dec 2023 14:55:20 +0000 Subject: [PATCH 10/12] 3644 - comments changes --- .../cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp index 887cd727f3f3..31c3355a5ee7 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/AvmMini_memory.test.cpp @@ -200,14 +200,14 @@ TEST_F(AvmMiniMemoryTests, mismatchedTagErrorViolation) trace_builder.sub(0, 1, 4, AvmMemoryTag::u8); auto trace = trace_builder.finalize(); - // Find the first row enabling the addition selector + // 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 add sub-operation of register ia. + // 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; }); @@ -233,7 +233,7 @@ TEST_F(AvmMiniMemoryTests, consistentTagNoErrorViolation) trace_builder.div(0, 1, 4, AvmMemoryTag::ff); auto trace = trace_builder.finalize(); - // Find the first row enabling the addition selector + // 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()); From 1db0c72e3b298efe2e3af34f21e2bbb9df3b4e17 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Tue, 19 Dec 2023 08:23:39 +0000 Subject: [PATCH 11/12] 3644 - fix after merge from avm-main --- .../flavor/generated/AvmMini_flavor.hpp | 19 ++++----- .../generated/AvmMini_circuit_builder.hpp | 7 ++-- .../relations/generated/AvmMini/avm_mini.hpp | 42 +++++++++---------- .../generated/AvmMini/declare_views.hpp | 2 +- .../relations/generated/AvmMini/mem_trace.hpp | 24 +++++------ 5 files changed, 46 insertions(+), 48 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp index a65f377cade6..f986f97f168c 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp @@ -184,9 +184,9 @@ 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_rw_shift, memTrace_m_tag_shift) RefVector get_wires() @@ -225,9 +225,9 @@ 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_rw_shift, memTrace_m_tag_shift }; }; RefVector get_unshifted() @@ -269,11 +269,11 @@ class AvmMiniFlavor { }; RefVector get_to_be_shifted() { - return { memTrace_m_rw, memTrace_m_val, memTrace_m_addr, memTrace_m_tag }; + return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag }; }; RefVector get_shifted() { - return { memTrace_m_rw_shift, memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_tag_shift }; + return { memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_tag_shift }; }; }; @@ -286,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 {}; }; }; @@ -319,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. @@ -333,6 +329,7 @@ class AvmMiniFlavor { return result; } }; + using RowPolynomials = AllEntities; class PartiallyEvaluatedMultivariates : public AllEntities { 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 2ec12145ccf1..02aaed70a5a1 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 @@ -53,9 +53,9 @@ template struct AvmMiniFullRow { FF avmMini_mem_idx_b{}; FF avmMini_mem_idx_c{}; FF avmMini_last{}; - FF memTrace_m_rw_shift{}; FF memTrace_m_val_shift{}; FF memTrace_m_addr_shift{}; + FF memTrace_m_rw_shift{}; FF memTrace_m_tag_shift{}; }; @@ -122,9 +122,9 @@ class AvmMiniCircuitBuilder { polys.avmMini_last[i] = rows[i].avmMini_last; } - polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.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; @@ -132,7 +132,8 @@ class AvmMiniCircuitBuilder { [[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, 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 d671e7285173..d590365b76a3 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp @@ -7,47 +7,47 @@ namespace proof_system::AvmMini_vm { template struct Avm_miniRow { - FF avmMini_mem_op_b{}; - FF avmMini_ia{}; - FF avmMini_ib{}; - FF avmMini_rwc{}; - FF avmMini_tag_err{}; - FF avmMini_sel_op_add{}; FF avmMini_sel_op_sub{}; - FF avmMini_rwb{}; - FF avmMini_sel_op_div{}; FF avmMini_rwa{}; - FF avmMini_mem_op_a{}; + FF avmMini_ic{}; 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_inv{}; - FF avmMini_ic{}; + FF avmMini_rwc{}; + FF avmMini_ib{}; + FF avmMini_mem_op_a{}; + 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 21: - return "SUBOP_ERROR_RELEVANT_OP"; + case 16: + return "SUBOP_SUBTRACTION_FF"; case 19: return "SUBOP_DIVISION_ZERO_ERR1"; - case 16: - return "SUBOP_SUBTRACTION_FF"; + case 20: + return "SUBOP_DIVISION_ZERO_ERR2"; + + case 21: + return "SUBOP_ERROR_RELEVANT_OP"; case 15: return "SUBOP_ADDITION_FF"; - - case 18: - return "SUBOP_DIVISION_FF"; - - case 20: - return "SUBOP_DIVISION_ZERO_ERR2"; } return std::to_string(index); } diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp index 83b8f8975192..9d23bb0f8f1b 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/declare_views.hpp @@ -36,7 +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_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 8d2ae9fe351f..9880acfa6316 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/mem_trace.hpp @@ -7,41 +7,41 @@ namespace proof_system::AvmMini_vm { template struct Mem_traceRow { - FF memTrace_m_lastAccess{}; - FF memTrace_m_tag_err{}; + FF memTrace_m_rw{}; FF memTrace_m_addr{}; - FF memTrace_m_rw_shift{}; 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_tag_shift{}; + FF memTrace_m_lastAccess{}; FF memTrace_m_tag{}; - FF memTrace_m_last{}; FF memTrace_m_in_tag{}; + FF memTrace_m_rw_shift{}; FF memTrace_m_one_min_inv{}; - FF memTrace_m_rw{}; + FF memTrace_m_tag_shift{}; }; inline std::string get_relation_label_mem_trace(int index) { switch (index) { - case 5: - return "MEM_READ_WRITE_VAL_CONSISTENCY"; - 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"; - - case 9: - return "MEM_IN_TAG_CONSISTENCY_2"; } return std::to_string(index); } From 3d0037b11a3566d7def35ab838e1ec6f85e1a9f5 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Tue, 19 Dec 2023 09:43:13 +0000 Subject: [PATCH 12/12] 3644 - enhance explanations for memory tag error handling --- barretenberg/cpp/pil/avm/mem_trace.pil | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/barretenberg/cpp/pil/avm/mem_trace.pil b/barretenberg/cpp/pil/avm/mem_trace.pil index d472316c6fd1..33a8a20ad067 100644 --- a/barretenberg/cpp/pil/avm/mem_trace.pil +++ b/barretenberg/cpp/pil/avm/mem_trace.pil @@ -78,16 +78,23 @@ namespace memTrace(256); // Memory tag consistency check // We want to prove that m_in_tag == m_tag <==> m_tag_err == 0 - // We introduce m_one_min_inv extra column to show that we can invert - // (m_in_tag - m_tag) when m_tag_err != 0 - // m_one_min_inv is set to 1 - (m_in_tag - m_tag)^(-1) when m_tag_err == 1 + // 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 above checks + // 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