Skip to content

Commit

Permalink
fix: bug fixing bench prover test (#7135)
Browse files Browse the repository at this point in the history 
Resolves #7080
  • Loading branch information
@jeanmon
jeanmon authored Jun 21, 2024
1 parent cc664af commit 13678be
Show file tree
Hide file tree
Showing 6 changed files with 29 additions and 12 deletions.
5 changes: 5 additions & 0 deletions barretenberg/cpp/pil/avm/main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
8 changes: 6 additions & 2 deletions barretenberg/cpp/pil/avm/mem.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/mem.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ template <typename FF_> class memImpl {

static constexpr std::array<size_t, 41> 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 <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -365,7 +365,7 @@ template <typename FF_> 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;
Expand All @@ -375,7 +375,7 @@ template <typename FF_> 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;
}
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
11 changes: 8 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<uint32_t>(AvmMemoryTag::FF)),
.main_sel_mem_op_a = FF(1),
.main_sel_mem_op_b = FF(1),
Expand Down Expand Up @@ -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<uint32_t>(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)
Expand Down Expand Up @@ -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<uint32_t>(AvmMemoryTag::FF)),
.main_sel_mem_op_a = FF(1),
.main_sel_mem_op_b = FF(1),
Expand Down Expand Up @@ -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<uint32_t>(AvmMemoryTag::U8)),
});

pc++;
}
// Finalise Lookup Counts
//
Expand Down
9 changes: 6 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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<uint32_t>(AvmMemoryTag::U32)),
MEM_ROW_FIELD_EQ(tag, static_cast<uint32_t>(AvmMemoryTag::U32)),
MEM_ROW_FIELD_EQ(tag,
indirect_uninitialized ? static_cast<uint32_t>(AvmMemoryTag::U0)
: static_cast<uint32_t>(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)));
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 13678be

Please sign in to comment.