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

Jump to bottom

feat(avm): propagate tag err to the main trace for op_return and internal_return #4615

Merged
merged 3 commits into from
Feb 15, 2024
Merged

feat(avm): propagate tag err to the main trace for op_return and internal_return #4615

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
4343bb1
4598 - remove superfluous trace builder constructor
jeanmon Feb 15, 2024
28b1f78
4598 - propagate tag err to the main trace for return_op and
jeanmon Feb 15, 2024
cb08f8c
4598 - refactor: move op_not and op_eq routines
jeanmon Feb 15, 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
188 changes: 102 additions & 86 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 @@ -227,6 +227,98 @@ void AvmTraceBuilder::op_div(uint32_t a_offset, uint32_t b_offset, uint32_t dst_
});
}

/**
* @brief Bitwise not with direct memory access.
*
* @param a_offset An index in memory pointing to the only operand of Not.
* @param dst_offset An index in memory pointing to the output of Not.
* @param in_tag The instruction memory tag of the operands.
*/
void AvmTraceBuilder::op_not(uint32_t a_offset, uint32_t dst_offset, AvmMemoryTag in_tag)
{
auto clk = static_cast<uint32_t>(main_trace.size());

// Reading from memory and loading into ia.
auto read_a = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IA, a_offset, in_tag);

// ~a = c
FF a = read_a.tag_match ? read_a.val : FF(0);
// TODO(4613): If tag_match == false, then the value of c
// will not be zero which would not satisfy the constraint that
// ic == 0 whenever tag_err == 1. This constraint might be removed
// as part of #4613.
FF c = alu_trace_builder.op_not(a, in_tag, clk);

// Write into memory value c from intermediate register ic.
mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag);

main_trace.push_back(Row{
.avm_main_clk = clk,
.avm_main_pc = FF(pc++),
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_op_not = FF(1),
.avm_main_in_tag = FF(static_cast<uint32_t>(in_tag)),
.avm_main_tag_err = FF(static_cast<uint32_t>(!read_a.tag_match)),
.avm_main_ia = a,
.avm_main_ic = c,
.avm_main_mem_op_a = FF(1),
.avm_main_mem_op_c = FF(1),
.avm_main_rwc = FF(1),
.avm_main_mem_idx_a = FF(a_offset),
.avm_main_mem_idx_c = FF(dst_offset),
});
};

/**
* @brief Equality with direct memory access.
*
* @param a_offset An index in memory pointing to the first operand of the equality.
* @param b_offset An index in memory pointing to the second operand of the equality.
* @param dst_offset An index in memory pointing to the output of the equality.
* @param in_tag The instruction memory tag of the operands.
*/
void AvmTraceBuilder::op_eq(uint32_t a_offset, uint32_t b_offset, uint32_t dst_offset, AvmMemoryTag in_tag)
{
auto clk = static_cast<uint32_t>(main_trace.size());

// Reading from memory and loading into ia resp. ib.
auto read_a = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IA, a_offset, in_tag);
auto read_b = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IB, b_offset, in_tag);
bool tag_match = read_a.tag_match && read_b.tag_match;

// c = a == b ? 1 : 0
FF a = tag_match ? read_a.val : FF(0);
FF b = tag_match ? read_b.val : FF(0);

// TODO(4613): If tag_match == false, then the value of c
// will not be zero which would not satisfy the constraint that
// ic == 0 whenever tag_err == 1. This constraint might be removed
// as part of #4613.
FF c = alu_trace_builder.op_eq(a, b, in_tag, clk);

// Write into memory value c from intermediate register ic.
mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag);

main_trace.push_back(Row{
.avm_main_clk = clk,
.avm_main_pc = FF(pc++),
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_op_eq = FF(1),
.avm_main_in_tag = FF(static_cast<uint32_t>(in_tag)),
.avm_main_tag_err = FF(static_cast<uint32_t>(!tag_match)),
.avm_main_ia = a,
.avm_main_ib = b,
.avm_main_ic = c,
.avm_main_mem_op_a = FF(1),
.avm_main_mem_op_b = FF(1),
.avm_main_mem_op_c = FF(1),
.avm_main_rwc = FF(1),
.avm_main_mem_idx_a = FF(a_offset),
.avm_main_mem_idx_b = FF(b_offset),
.avm_main_mem_idx_c = FF(dst_offset),
});
}

// TODO: Finish SET opcode implementation. This is a partial implementation
// facilitating testing of arithmetic operations over non finite field types.
// We add an entry in the memory trace and a simplified one in the main trace
Expand Down Expand Up @@ -404,6 +496,8 @@ std::vector<FF> AvmTraceBuilder::return_op(uint32_t ret_offset, uint32_t ret_siz

// Reading and loading to Ia
auto read_a = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IA, mem_idx_a, AvmMemoryTag::FF);
bool tag_match = read_a.tag_match;

FF ia = read_a.val;
returnMem.push_back(ia);

Expand All @@ -414,6 +508,7 @@ std::vector<FF> AvmTraceBuilder::return_op(uint32_t ret_offset, uint32_t ret_siz
// Reading and loading to Ib
auto read_b =
mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IB, mem_idx_b, AvmMemoryTag::FF);
tag_match = tag_match && read_b.tag_match;
FF ib = read_b.val;
returnMem.push_back(ib);
}
Expand All @@ -425,6 +520,7 @@ std::vector<FF> AvmTraceBuilder::return_op(uint32_t ret_offset, uint32_t ret_siz
// Reading and loading to Ic
auto read_c =
mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IC, mem_idx_c, AvmMemoryTag::FF);
tag_match = tag_match && read_c.tag_match;
FF ic = read_c.val;
returnMem.push_back(ic);
}
Expand All @@ -435,9 +531,10 @@ std::vector<FF> AvmTraceBuilder::return_op(uint32_t ret_offset, uint32_t ret_siz
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_halt = FF(1),
.avm_main_in_tag = FF(static_cast<uint32_t>(AvmMemoryTag::FF)),
.avm_main_ia = ia,
.avm_main_ib = ib,
.avm_main_ic = ic,
.avm_main_tag_err = FF(static_cast<uint32_t>(!tag_match)),
.avm_main_ia = tag_match ? ia : FF(0),
.avm_main_ib = tag_match ? ib : FF(0),
.avm_main_ic = tag_match ? ic : FF(0),
.avm_main_mem_op_a = FF(mem_op_a),
.avm_main_mem_op_b = FF(mem_op_b),
.avm_main_mem_op_c = FF(mem_op_c),
Expand Down Expand Up @@ -565,7 +662,8 @@ void AvmTraceBuilder::internal_return()
.avm_main_pc = pc,
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_internal_return = FF(1),
.avm_main_ia = read_a.val,
.avm_main_tag_err = FF(static_cast<uint32_t>(!read_a.tag_match)),
.avm_main_ia = read_a.tag_match ? read_a.val : FF(0),
.avm_main_mem_op_a = FF(1),
.avm_main_rwa = FF(0),
.avm_main_mem_idx_a = FF(internal_return_ptr - 1),
Expand Down Expand Up @@ -702,86 +800,4 @@ std::vector<Row> AvmTraceBuilder::finalize()
return trace;
}

/**
* @brief Bitwise not with direct memory access.
*
* @param a_offset An index in memory pointing to the only operand of Not.
* @param dst_offset An index in memory pointing to the output of Not.
* @param in_tag The instruction memory tag of the operands.
*/
void AvmTraceBuilder::op_not(uint32_t a_offset, uint32_t dst_offset, AvmMemoryTag in_tag)
{
auto clk = static_cast<uint32_t>(main_trace.size());

// Reading from memory and loading into ia.
auto read_a = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IA, a_offset, in_tag);

// ~a = c
FF a = read_a.tag_match ? read_a.val : FF(0);
FF c = alu_trace_builder.op_not(a, in_tag, clk);

// Write into memory value c from intermediate register ic.
mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag);

main_trace.push_back(Row{
.avm_main_clk = clk,
.avm_main_pc = FF(pc++),
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_op_not = FF(1),
.avm_main_in_tag = FF(static_cast<uint32_t>(in_tag)),
.avm_main_tag_err = FF(static_cast<uint32_t>(!read_a.tag_match)),
.avm_main_ia = a,
.avm_main_ic = c,
.avm_main_mem_op_a = FF(1),
.avm_main_mem_op_c = FF(1),
.avm_main_rwc = FF(1),
.avm_main_mem_idx_a = FF(a_offset),
.avm_main_mem_idx_c = FF(dst_offset),
});
};

/**
* @brief Equality with direct memory access.
*
* @param a_offset An index in memory pointing to the first operand of the equality.
* @param b_offset An index in memory pointing to the second operand of the equality.
* @param dst_offset An index in memory pointing to the output of the equality.
* @param in_tag The instruction memory tag of the operands.
*/
void AvmTraceBuilder::op_eq(uint32_t a_offset, uint32_t b_offset, uint32_t dst_offset, AvmMemoryTag in_tag)
{
auto clk = static_cast<uint32_t>(main_trace.size());

// Reading from memory and loading into ia resp. ib.
auto read_a = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IA, a_offset, in_tag);
auto read_b = mem_trace_builder.read_and_load_from_memory(clk, IntermRegister::IB, b_offset, in_tag);
bool tag_match = read_a.tag_match && read_b.tag_match;

// c = a == b ? 1 : 0
FF a = tag_match ? read_a.val : FF(0);
FF b = tag_match ? read_b.val : FF(0);
FF c = alu_trace_builder.op_eq(a, b, in_tag, clk);

// Write into memory value c from intermediate register ic.
mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag);

main_trace.push_back(Row{
.avm_main_clk = clk,
.avm_main_pc = FF(pc++),
.avm_main_internal_return_ptr = FF(internal_return_ptr),
.avm_main_sel_op_eq = FF(1),
.avm_main_in_tag = FF(static_cast<uint32_t>(in_tag)),
.avm_main_tag_err = FF(static_cast<uint32_t>(!tag_match)),
.avm_main_ia = a,
.avm_main_ib = b,
.avm_main_ic = c,
.avm_main_mem_op_a = FF(1),
.avm_main_mem_op_b = FF(1),
.avm_main_mem_op_c = FF(1),
.avm_main_rwc = FF(1),
.avm_main_mem_idx_a = FF(a_offset),
.avm_main_mem_idx_b = FF(b_offset),
.avm_main_mem_idx_c = FF(dst_offset),
});
}
} // namespace avm_trace
11 changes: 5 additions & 6 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_arithmetic.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,10 @@ void common_validate_arithmetic_op(Row const& main_row,
EXPECT_EQ(alu_row.avm_alu_alu_ia, a);
EXPECT_EQ(alu_row.avm_alu_alu_ib, b);
EXPECT_EQ(alu_row.avm_alu_alu_ic, c);

// Check that no error is raised
EXPECT_EQ(main_row.avm_main_tag_err, FF(0));
EXPECT_EQ(main_row.avm_main_op_err, FF(0));
}

Row common_validate_add(std::vector<Row> const& trace,
Expand Down Expand Up @@ -251,11 +255,7 @@ class AvmArithmeticTests : public ::testing::Test {

protected:
// TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test.
void SetUp() override
{
srs::init_crs_factory("../srs_db/ignition");
trace_builder = AvmTraceBuilder(); // Clean instance for every run.
};
void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); };
};

class AvmArithmeticTestsFF : public AvmArithmeticTests {};
Expand Down Expand Up @@ -303,7 +303,6 @@ class AvmArithmeticNegativeTestsU128 : public AvmArithmeticTests {};
// Test on basic addition over finite field type.
TEST_F(AvmArithmeticTestsFF, addition)
{
// trace_builder
trace_builder.calldata_copy(0, 3, 0, std::vector<FF>{ 37, 4, 11 });

// Memory layout: [37,4,11,0,0,0,....]
Expand Down
6 changes: 1 addition & 5 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_bitwise.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,11 +81,7 @@ class AvmBitwiseTests : public ::testing::Test {

protected:
// TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test.
void SetUp() override
{
srs::init_crs_factory("../srs_db/ignition");
trace_builder = AvmTraceBuilder(); // Clean instance for every run.
};
void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); };
};

class AvmBitwiseTestsU8 : public AvmBitwiseTests {};
Expand Down
6 changes: 1 addition & 5 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_control_flow.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,7 @@ class AvmControlFlowTests : public ::testing::Test {

protected:
// TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test.
void SetUp() override
{
srs::init_crs_factory("../srs_db/ignition");
trace_builder = AvmTraceBuilder(); // Clean instance for every run.
};
void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); };
};

/******************************************************************************
Expand Down
6 changes: 1 addition & 5 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,7 @@ class AvmExecutionTests : public ::testing::Test {

protected:
// TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test.
void SetUp() override
{
srs::init_crs_factory("../srs_db/ignition");
trace_builder = AvmTraceBuilder(); // Clean instance for every run.
};
void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); };
};

// Basic positive test with an ADD and RETURN opcode.
Expand Down
6 changes: 1 addition & 5 deletions barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,7 @@ class AvmMemoryTests : public ::testing::Test {

protected:
// TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test.
void SetUp() override
{
srs::init_crs_factory("../srs_db/ignition");
trace_builder = AvmTraceBuilder(); // Clean instance for every run.
};
void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); };
};

/******************************************************************************
Expand Down
Loading