Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: bug fixing bench prover test #7135

Merged
merged 3 commits into from
Jun 21, 2024
Merged

fix: bug fixing bench prover test #7135

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
927702a
7080: several bug fixes
jeanmon Jun 20, 2024
8ea2f1e
7080: repair unit tests related to unitialized indirect memory in a MOV
jeanmon Jun 20, 2024
474aae2
7080: fixes after rebase to master
jeanmon Jun 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions barretenberg/cpp/pil/avm/main.pil
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading