From 13678be4e1c76d20a804a04b0fa82f68aeca38ae Mon Sep 17 00:00:00 2001 From: Jean M <132435771+jeanmon@users.noreply.github.com> Date: Fri, 21 Jun 2024 11:49:15 +0200 Subject: [PATCH] fix: bug fixing bench prover test (#7135) Resolves #7080 --- barretenberg/cpp/pil/avm/main.pil | 5 +++++ barretenberg/cpp/pil/avm/mem.pil | 8 ++++++-- .../src/barretenberg/relations/generated/avm/mem.hpp | 6 +++--- .../src/barretenberg/vm/avm_trace/avm_mem_trace.cpp | 2 +- .../cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp | 11 ++++++++--- .../barretenberg/vm/tests/avm_mem_opcodes.test.cpp | 9 ++++++--- 6 files changed, 29 insertions(+), 12 deletions(-) diff --git a/barretenberg/cpp/pil/avm/main.pil b/barretenberg/cpp/pil/avm/main.pil index 36b2b6e2b97..618dc585d7e 100644 --- a/barretenberg/cpp/pil/avm/main.pil +++ b/barretenberg/cpp/pil/avm/main.pil @@ -487,6 +487,11 @@ namespace main(256); sel_gas_accounting_active - OPCODE_SELECTORS - SEL_ALL_CTRL_FLOW - sel_op_sload - sel_op_sstore - sel_mem_op_activate_gas = 0; // Program counter must increment if not jumping or returning + // TODO: support for muli-rows opcode in execution trace such as + // radix, hash gadgets operations. At the moment, we have to increment + // the pc in witness generation for all rows pertaining to the original + // opcode. This is misleading. Ultimately, we want the pc to be incremented + // just after the last row of a given opcode. #[PC_INCREMENT] (1 - sel_first) * (1 - sel_op_halt) * OPCODE_SELECTORS * (pc' - (pc + 1)) = 0; diff --git a/barretenberg/cpp/pil/avm/mem.pil b/barretenberg/cpp/pil/avm/mem.pil index a5aa3080f03..0cb9d7c491a 100644 --- a/barretenberg/cpp/pil/avm/mem.pil +++ b/barretenberg/cpp/pil/avm/mem.pil @@ -171,10 +171,14 @@ namespace mem(256); // instead of (r_in_tag - tag)^(-1) as this allows to store zero by default (i.e., when tag_err == 0). // The new column one_min_inv is set to 1 - (r_in_tag - tag)^(-1) when tag_err == 1 // but must be set to 0 when tags are matching and tag_err = 0 + // Relaxation: This relation is relaxed when skip_check_tag is enabled or for + // uninitialized memory, i.e. tag == 0. #[MEM_IN_TAG_CONSISTENCY_1] - (1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0; + tag * (1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0; + // TODO: Try to decrease the degree of the above relation, e.g., skip_check_tag might be consolidated + // with tag == 0 and rw == 1. #[MEM_IN_TAG_CONSISTENCY_2] - (1 - tag_err) * one_min_inv = 0; + tag * (1 - tag_err) * one_min_inv = 0; #[NO_TAG_ERR_WRITE_OR_SKIP] (skip_check_tag + rw) * tag_err = 0; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/mem.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/mem.hpp index ea5a125887f..6e4c4fdd982 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/mem.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/mem.hpp @@ -112,7 +112,7 @@ template class memImpl { static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 3, 4, 3, 4, 3, 4, 3, 3, - 3, 4, 4, 4, 4, 4, 5, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 4, 4, 4, 4, 4, 6, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, }; template @@ -365,7 +365,7 @@ template class memImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = ((((-mem_skip_check_tag + FF(1)) * (-mem_rw + FF(1))) * + auto tmp = ((((mem_tag * (-mem_skip_check_tag + FF(1))) * (-mem_rw + FF(1))) * (((mem_r_in_tag - mem_tag) * (-mem_one_min_inv + FF(1))) - mem_tag_err)) - FF(0)); tmp *= scaling_factor; @@ -375,7 +375,7 @@ template class memImpl { { Avm_DECLARE_VIEWS(28); - auto tmp = (((-mem_tag_err + FF(1)) * mem_one_min_inv) - FF(0)); + auto tmp = (((mem_tag * (-mem_tag_err + FF(1))) * mem_one_min_inv) - FF(0)); tmp *= scaling_factor; std::get<28>(evals) += tmp; } diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp index 8ee4f02595f..e46fb93d670 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp @@ -150,7 +150,7 @@ bool AvmMemTraceBuilder::load_from_mem_trace(uint8_t space_id, AvmMemoryTag m_tag = mem_space.contains(addr) ? mem_space.at(addr).tag : AvmMemoryTag::U0; if (m_tag == AvmMemoryTag::U0 || m_tag == r_in_tag) { - insert_in_mem_trace(space_id, clk, sub_clk, addr, val, r_in_tag, r_in_tag, w_in_tag, false); + insert_in_mem_trace(space_id, clk, sub_clk, addr, val, m_tag, r_in_tag, w_in_tag, false); return true; } diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp index c97c71eccb2..49503c35afb 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -2678,7 +2678,7 @@ void AvmTraceBuilder::op_call([[maybe_unused]] uint8_t indirect, .main_mem_addr_a = read_ind_gas_offset.val, .main_mem_addr_b = addr_offset, .main_mem_addr_c = read_ind_args_offset.val, - .main_pc = FF(pc++), + .main_pc = FF(pc), .main_r_in_tag = FF(static_cast(AvmMemoryTag::FF)), .main_sel_mem_op_a = FF(1), .main_sel_mem_op_b = FF(1), @@ -2725,10 +2725,13 @@ void AvmTraceBuilder::op_call([[maybe_unused]] uint8_t indirect, AvmMemoryTag::FF, internal_return_ptr, hint.return_data); - clk++; + + // The last call to write_slice_to_memory() might have written more than one row. + clk = static_cast(main_trace.size()) + 1; write_slice_to_memory( call_ptr, clk, success_offset, AvmMemoryTag::U0, AvmMemoryTag::U8, internal_return_ptr, { hint.success }); external_call_counter++; + pc++; } void AvmTraceBuilder::op_get_contract_instance(uint8_t indirect, uint32_t address_offset, uint32_t dst_offset) @@ -3685,7 +3688,7 @@ void AvmTraceBuilder::op_variable_msm(uint8_t indirect, .main_internal_return_ptr = FF(internal_return_ptr), .main_mem_addr_a = FF(direct_points_offset), .main_mem_addr_b = FF(direct_scalars_offset), - .main_pc = FF(pc++), + .main_pc = FF(pc), .main_r_in_tag = FF(static_cast(AvmMemoryTag::FF)), .main_sel_mem_op_a = FF(1), .main_sel_mem_op_b = FF(1), @@ -3882,6 +3885,8 @@ void AvmTraceBuilder::op_variable_msm(uint8_t indirect, .main_sel_mem_op_a = FF(1), .main_w_in_tag = FF(static_cast(AvmMemoryTag::U8)), }); + + pc++; } // Finalise Lookup Counts // diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp index 3f0538411a2..102d00a57ca 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp @@ -173,7 +173,8 @@ class AvmMemOpcodeTests : public ::testing::Test { uint32_t dst_offset, AvmMemoryTag tag, uint32_t dir_src_offset = 0, - uint32_t dir_dst_offset = 0) + uint32_t dir_dst_offset = 0, + bool indirect_uninitialized = false) { compute_mov_indices(indirect); FF const val_ff = uint256_t::from_uint128(val); @@ -220,7 +221,9 @@ class AvmMemOpcodeTests : public ::testing::Test { EXPECT_THAT(mem_ind_a_row, AllOf(MEM_ROW_FIELD_EQ(tag_err, 0), MEM_ROW_FIELD_EQ(r_in_tag, static_cast(AvmMemoryTag::U32)), - MEM_ROW_FIELD_EQ(tag, static_cast(AvmMemoryTag::U32)), + MEM_ROW_FIELD_EQ(tag, + indirect_uninitialized ? static_cast(AvmMemoryTag::U0) + : static_cast(AvmMemoryTag::U32)), MEM_ROW_FIELD_EQ(addr, src_offset), MEM_ROW_FIELD_EQ(val, dir_src_offset), MEM_ROW_FIELD_EQ(sel_resolve_ind_addr_a, 1))); @@ -376,7 +379,7 @@ TEST_F(AvmMemOpcodeTests, indUninitializedValueMov) trace_builder.return_op(0, 0, 0); trace = trace_builder.finalize(); - validate_mov_trace(true, 0, 2, 3, AvmMemoryTag::U0, 0, 1); + validate_mov_trace(true, 0, 2, 3, AvmMemoryTag::U0, 0, 1, true); } TEST_F(AvmMemOpcodeTests, indirectMov)