Skip to content

Commit

Permalink
7080: repair unit tests related to unitialized indirect memory in a MOV
Browse files Browse the repository at this point in the history
  • Loading branch information
jeanmon committed Jun 20, 2024
1 parent 3d5e13e commit ed5b34d
Show file tree
Hide file tree
Showing 4 changed files with 18 additions and 6 deletions.
5 changes: 5 additions & 0 deletions barretenberg/cpp/pil/avm/main.pil
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
6 changes: 5 additions & 1 deletion barretenberg/cpp/pil/avm/mem.pil
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]
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
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, 6, 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 @@ -373,7 +373,7 @@ template <typename FF_> class memImpl {
{
Avm_DECLARE_VIEWS(28);

auto tmp = ((-mem_tag_err + FF(1)) * mem_one_min_inv);
auto tmp = ((mem_tag * (-mem_tag_err + FF(1))) * mem_one_min_inv);
tmp *= scaling_factor;
std::get<28>(evals) += tmp;
}
Expand Down
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 ed5b34d

Please sign in to comment.