Skip to content

Commit

Permalink
feat(avm): propagate tag err to the main trace for op_return and inte…
Browse files Browse the repository at this point in the history
…rnal_return (#4615)

Resolves #4598
  • Loading branch information
jeanmon committed Feb 15, 2024
1 parent e63f022 commit 427f1d8
Show file tree
Hide file tree
Showing 6 changed files with 111 additions and 112 deletions.
188 changes: 102 additions & 86 deletions barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp
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
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
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
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
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
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

0 comments on commit 427f1d8

Please sign in to comment.