Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 1 addition & 3 deletions barretenberg/cpp/pil/vm2/bytecode/instr_fetching.pil
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,7 @@ pol PARSING_ERROR_EXCEPT_TAG_ERROR = pc_out_of_range + opcode_out_of_range + ins

// If any error occurs, we toggle the following boolean:
pol commit sel_parsing_err;
// FIXME: constrain this again once all execution opcodes are supported.
// See InstrDeserializationError::INVALID_EXECUTION_OPCODE.
// sel_parsing_err = PARSING_ERROR_EXCEPT_TAG_ERROR + tag_out_of_range;
sel_parsing_err = PARSING_ERROR_EXCEPT_TAG_ERROR + tag_out_of_range;
sel_parsing_err * (1 - sel_parsing_err) = 0; // enforces disjoint errors


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -829,5 +829,105 @@ TEST(InstrFetchingConstrainingTest, NegativeTogglingPcInRange)
"PC_OUT_OF_RANGE_TOGGLE");
}

TEST(InstrFetchingConstrainingTest, ErrorFlagSetButSelParsingErrIsZero)
{
// Create a minimal trace that satisfies all constraints EXCEPT the (commented out) one
// that should enforce sel_parsing_err = pc_out_of_range + opcode_out_of_range + instr_out_of_range +
// tag_out_of_range
TestTraceContainer trace({
{ { C::precomputed_first_row, 1 } },
{
{ C::instr_fetching_sel, 1 },
// Error flags - pc_out_of_range is SET to 1
{ C::instr_fetching_pc_out_of_range, 1 },
{ C::instr_fetching_opcode_out_of_range, 0 },
{ C::instr_fetching_instr_out_of_range, 0 },
{ C::instr_fetching_tag_out_of_range, 0 },
// sel_parsing_err should be 1 (since pc_out_of_range = 1) but we set it to 0
{ C::instr_fetching_sel_parsing_err, 0 },
// Values to satisfy PC_OUT_OF_RANGE_TOGGLE constraint (subrelation 4):
// pc_abs_diff = sel * ((2 * pc_out_of_range - 1) * (pc - bytecode_size) - 1 + pc_out_of_range)
// With pc_out_of_range = 1: pc_abs_diff = (2*1-1) * (pc - bytecode_size) - 1 + 1 = pc - bytecode_size
{ C::instr_fetching_bytecode_size, 10 },
{ C::instr_fetching_pc, 15 }, // pc > bytecode_size
{ C::instr_fetching_pc_abs_diff, 5 }, // pc - bytecode_size = 15 - 10 = 5
{ C::instr_fetching_pc_size_in_bits, 32 }, // AVM_PC_SIZE_IN_BITS constant
// Values to satisfy INSTR_OUT_OF_RANGE_TOGGLE constraint (subrelation 6):
// instr_abs_diff = (2 * instr_out_of_range - 1) * (instr_size - bytes_to_read) - instr_out_of_range
// With instr_out_of_range = 0: instr_abs_diff = (-1) * (instr_size - bytes_to_read) = bytes_to_read -
// instr_size
{ C::instr_fetching_bytes_to_read, 10 },
{ C::instr_fetching_instr_size, 5 },
{ C::instr_fetching_instr_abs_diff, 5 }, // bytes_to_read - instr_size = 10 - 5 = 5
},
});

EXPECT_THROW_WITH_MESSAGE(check_relation<instr_fetching>(trace),
"Relation instr_fetching, subrelation 3 failed at row 1");
}

/**
* This test verifies that when sel_parsing_err is correctly set to 1 when errors occur,
* the relation passes. This should continue to pass after the fix.
*/
TEST(InstrFetchingConstrainingTest, CorrectBehavior_SelParsingErrMatchesErrors)
{
TestTraceContainer trace({
{ { C::precomputed_first_row, 1 } },
{
{ C::instr_fetching_sel, 1 },
{ C::instr_fetching_pc_out_of_range, 1 },
{ C::instr_fetching_opcode_out_of_range, 0 },
{ C::instr_fetching_instr_out_of_range, 0 },
{ C::instr_fetching_tag_out_of_range, 0 },
{ C::instr_fetching_sel_parsing_err, 1 }, // Correctly set to 1
// Supporting values
{ C::instr_fetching_bytecode_size, 10 },
{ C::instr_fetching_pc, 15 },
{ C::instr_fetching_pc_abs_diff, 5 },
{ C::instr_fetching_pc_size_in_bits, 32 },
{ C::instr_fetching_bytes_to_read, 10 },
{ C::instr_fetching_instr_size, 5 },
{ C::instr_fetching_instr_abs_diff, 5 }, // bytes_to_read - instr_size = 10 - 5 = 5
},
});

// This should pass both before and after the fix.
check_relation<instr_fetching>(trace);
}

/**
* No errors means sel_parsing_err should be 0
*/
TEST(InstrFetchingConstrainingTest, CorrectBehavior_NoErrorsMeansSelParsingErrIsZero)
{
TestTraceContainer trace({
{ { C::precomputed_first_row, 1 } },
{
{ C::instr_fetching_sel, 1 },
{ C::instr_fetching_pc_out_of_range, 0 },
{ C::instr_fetching_opcode_out_of_range, 0 },
{ C::instr_fetching_instr_out_of_range, 0 },
{ C::instr_fetching_tag_out_of_range, 0 },
{ C::instr_fetching_sel_parsing_err, 0 }, // Correctly set to 0
{ C::instr_fetching_sel_pc_in_range, 1 }, // sel * (1 - pc_out_of_range) = 1 * 1 = 1
// pc_abs_diff = sel * ((2 * pc_out_of_range - 1) * (pc - bytecode_size) - 1 + pc_out_of_range)
// With pc_out_of_range = 0: pc_abs_diff = (2*0-1) * (pc - bytecode_size) - 1 + 0
// = -(pc - bytecode_size) - 1 = bytecode_size - pc - 1
{ C::instr_fetching_bytecode_size, 20 },
{ C::instr_fetching_pc, 5 },
{ C::instr_fetching_pc_abs_diff, 14 }, // bytecode_size - pc - 1 = 20 - 5 - 1 = 14
{ C::instr_fetching_pc_size_in_bits, 32 },
// instr_abs_diff = bytes_to_read - instr_size (when instr_out_of_range = 0)
{ C::instr_fetching_bytes_to_read, 15 },
{ C::instr_fetching_instr_size, 10 },
{ C::instr_fetching_instr_abs_diff, 5 }, // bytes_to_read - instr_size = 15 - 10 = 5
},
});

// This should pass both before and after the fix.
check_relation<instr_fetching>(trace);
}

} // namespace
} // namespace bb::avm2::constraining
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ template <typename FF_> class instr_fetchingImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 17> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 3, 4, 3, 3, 3, 3,
4, 4, 4, 4, 4, 4, 4, 4 };
static constexpr std::array<size_t, 18> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 2, 3, 4, 3, 3, 3,
3, 4, 4, 4, 4, 4, 4, 4, 4 };

template <typename AllEntities> inline static bool skip(const AllEntities& in)
{
Expand All @@ -36,17 +36,17 @@ template <typename FF> class instr_fetching : public Relation<instr_fetchingImpl
static constexpr const std::string_view NAME = "instr_fetching";

// Subrelation indices constants, to be used in tests.
static constexpr size_t SR_PC_OUT_OF_RANGE_TOGGLE = 4;
static constexpr size_t SR_INSTR_OUT_OF_RANGE_TOGGLE = 6;
static constexpr size_t SR_TAG_VALUE = 7;
static constexpr size_t SR_INDIRECT_BYTES_DECOMPOSITION = 9;
static constexpr size_t SR_OP1_BYTES_DECOMPOSITION = 10;
static constexpr size_t SR_OP2_BYTES_DECOMPOSITION = 11;
static constexpr size_t SR_OP3_BYTES_DECOMPOSITION = 12;
static constexpr size_t SR_OP4_BYTES_DECOMPOSITION = 13;
static constexpr size_t SR_OP5_BYTES_DECOMPOSITION = 14;
static constexpr size_t SR_OP6_BYTES_DECOMPOSITION = 15;
static constexpr size_t SR_OP7_BYTES_DECOMPOSITION = 16;
static constexpr size_t SR_PC_OUT_OF_RANGE_TOGGLE = 5;
static constexpr size_t SR_INSTR_OUT_OF_RANGE_TOGGLE = 7;
static constexpr size_t SR_TAG_VALUE = 8;
static constexpr size_t SR_INDIRECT_BYTES_DECOMPOSITION = 10;
static constexpr size_t SR_OP1_BYTES_DECOMPOSITION = 11;
static constexpr size_t SR_OP2_BYTES_DECOMPOSITION = 12;
static constexpr size_t SR_OP3_BYTES_DECOMPOSITION = 13;
static constexpr size_t SR_OP4_BYTES_DECOMPOSITION = 14;
static constexpr size_t SR_OP5_BYTES_DECOMPOSITION = 15;
static constexpr size_t SR_OP6_BYTES_DECOMPOSITION = 16;
static constexpr size_t SR_OP7_BYTES_DECOMPOSITION = 17;

static std::string get_subrelation_label(size_t index)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,67 +42,74 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
}
{
using View = typename std::tuple_element_t<3, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_sel_parsing_err)) -
(CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR) +
static_cast<View>(in.get(C::instr_fetching_tag_out_of_range))));
std::get<3>(evals) += (tmp * scaling_factor);
}
{
using View = typename std::tuple_element_t<4, ContainerOverSubrelations>::View;
auto tmp = static_cast<View>(in.get(C::instr_fetching_sel_parsing_err)) *
(FF(1) - static_cast<View>(in.get(C::instr_fetching_sel_parsing_err)));
std::get<3>(evals) += (tmp * scaling_factor);
std::get<4>(evals) += (tmp * scaling_factor);
}
{ // PC_OUT_OF_RANGE_TOGGLE
using View = typename std::tuple_element_t<4, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<5, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_pc_abs_diff)) -
static_cast<View>(in.get(C::instr_fetching_sel)) *
(((FF(2) * static_cast<View>(in.get(C::instr_fetching_pc_out_of_range)) - FF(1)) *
(static_cast<View>(in.get(C::instr_fetching_pc)) -
static_cast<View>(in.get(C::instr_fetching_bytecode_size))) -
FF(1)) +
static_cast<View>(in.get(C::instr_fetching_pc_out_of_range))));
std::get<4>(evals) += (tmp * scaling_factor);
std::get<5>(evals) += (tmp * scaling_factor);
}
{
using View = typename std::tuple_element_t<5, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<6, ContainerOverSubrelations>::View;
auto tmp =
static_cast<View>(in.get(C::instr_fetching_sel)) *
(static_cast<View>(in.get(C::instr_fetching_pc_size_in_bits)) - CView(constants_AVM_PC_SIZE_IN_BITS));
std::get<5>(evals) += (tmp * scaling_factor);
std::get<6>(evals) += (tmp * scaling_factor);
}
{ // INSTR_OUT_OF_RANGE_TOGGLE
using View = typename std::tuple_element_t<6, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<7, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_instr_abs_diff)) -
((FF(2) * static_cast<View>(in.get(C::instr_fetching_instr_out_of_range)) - FF(1)) *
(static_cast<View>(in.get(C::instr_fetching_instr_size)) -
static_cast<View>(in.get(C::instr_fetching_bytes_to_read))) -
static_cast<View>(in.get(C::instr_fetching_instr_out_of_range))));
std::get<6>(evals) += (tmp * scaling_factor);
std::get<7>(evals) += (tmp * scaling_factor);
}
{ // TAG_VALUE
using View = typename std::tuple_element_t<7, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<8, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_tag_value)) -
((static_cast<View>(in.get(C::instr_fetching_sel_has_tag)) -
static_cast<View>(in.get(C::instr_fetching_sel_tag_is_op2))) *
static_cast<View>(in.get(C::instr_fetching_op3)) +
static_cast<View>(in.get(C::instr_fetching_sel_tag_is_op2)) *
static_cast<View>(in.get(C::instr_fetching_op2))));
std::get<7>(evals) += (tmp * scaling_factor);
std::get<8>(evals) += (tmp * scaling_factor);
}
{
using View = typename std::tuple_element_t<8, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<9, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_sel_pc_in_range)) -
static_cast<View>(in.get(C::instr_fetching_sel)) *
(FF(1) - static_cast<View>(in.get(C::instr_fetching_pc_out_of_range))));
std::get<8>(evals) += (tmp * scaling_factor);
std::get<9>(evals) += (tmp * scaling_factor);
}
{ // INDIRECT_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<9, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<10, ContainerOverSubrelations>::View;
auto tmp =
(static_cast<View>(in.get(C::instr_fetching_indirect)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
(static_cast<View>(in.get(C::instr_fetching_sel_op_dc_0)) *
(static_cast<View>(in.get(C::instr_fetching_bd1)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd2)) * FF(1)) +
CView(instr_fetching_SEL_OP_DC_17) * static_cast<View>(in.get(C::instr_fetching_bd1)) * FF(1)));
std::get<9>(evals) += (tmp * scaling_factor);
std::get<10>(evals) += (tmp * scaling_factor);
}
{ // OP1_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<10, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<11, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op1)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
(static_cast<View>(in.get(C::instr_fetching_sel_op_dc_0)) *
Expand All @@ -118,10 +125,10 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
static_cast<View>(in.get(C::instr_fetching_bd2)) * FF(65536) +
static_cast<View>(in.get(C::instr_fetching_bd3)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd4)) * FF(1))));
std::get<10>(evals) += (tmp * scaling_factor);
std::get<11>(evals) += (tmp * scaling_factor);
}
{ // OP2_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<11, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<12, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op2)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
(static_cast<View>(in.get(C::instr_fetching_sel_op_dc_0)) *
Expand All @@ -139,10 +146,10 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
static_cast<View>(in.get(C::instr_fetching_bd5)) * FF(65536) +
static_cast<View>(in.get(C::instr_fetching_bd6)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd7)) * FF(1))));
std::get<11>(evals) += (tmp * scaling_factor);
std::get<12>(evals) += (tmp * scaling_factor);
}
{ // OP3_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<12, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<13, ContainerOverSubrelations>::View;
auto tmp =
(static_cast<View>(in.get(C::instr_fetching_op3)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
Expand Down Expand Up @@ -237,10 +244,10 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
static_cast<View>(in.get(C::instr_fetching_bd6)) * FF(1)) +
static_cast<View>(in.get(C::instr_fetching_sel_op_dc_14)) *
static_cast<View>(in.get(C::instr_fetching_bd4)) * FF(1)));
std::get<12>(evals) += (tmp * scaling_factor);
std::get<13>(evals) += (tmp * scaling_factor);
}
{ // OP4_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<13, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<14, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op4)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
(static_cast<View>(in.get(C::instr_fetching_sel_op_dc_0)) *
Expand All @@ -249,10 +256,10 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
static_cast<View>(in.get(C::instr_fetching_sel_op_dc_5)) *
(static_cast<View>(in.get(C::instr_fetching_bd8)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd9)) * FF(1))));
std::get<13>(evals) += (tmp * scaling_factor);
std::get<14>(evals) += (tmp * scaling_factor);
}
{ // OP5_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<14, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<15, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op5)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
(static_cast<View>(in.get(C::instr_fetching_sel_op_dc_0)) *
Expand All @@ -261,25 +268,25 @@ void instr_fetchingImpl<FF_>::accumulate(ContainerOverSubrelations& evals,
static_cast<View>(in.get(C::instr_fetching_sel_op_dc_5)) *
(static_cast<View>(in.get(C::instr_fetching_bd10)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd11)) * FF(1))));
std::get<14>(evals) += (tmp * scaling_factor);
std::get<15>(evals) += (tmp * scaling_factor);
}
{ // OP6_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<15, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<16, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op6)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
static_cast<View>(in.get(C::instr_fetching_sel_op_dc_1)) *
(static_cast<View>(in.get(C::instr_fetching_bd13)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd14)) * FF(1)));
std::get<15>(evals) += (tmp * scaling_factor);
std::get<16>(evals) += (tmp * scaling_factor);
}
{ // OP7_BYTES_DECOMPOSITION
using View = typename std::tuple_element_t<16, ContainerOverSubrelations>::View;
using View = typename std::tuple_element_t<17, ContainerOverSubrelations>::View;
auto tmp = (static_cast<View>(in.get(C::instr_fetching_op7)) -
(FF(1) - CView(instr_fetching_PARSING_ERROR_EXCEPT_TAG_ERROR)) *
static_cast<View>(in.get(C::instr_fetching_sel_op_dc_1)) *
(static_cast<View>(in.get(C::instr_fetching_bd15)) * FF(256) +
static_cast<View>(in.get(C::instr_fetching_bd16)) * FF(1)));
std::get<16>(evals) += (tmp * scaling_factor);
std::get<17>(evals) += (tmp * scaling_factor);
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,6 @@ enum class InstrDeserializationEventError : uint8_t {
OPCODE_OUT_OF_RANGE,
INSTRUCTION_OUT_OF_RANGE,
TAG_OUT_OF_RANGE,
// FIXME: remove this once all execution opcodes are supported.
// Also uncomment proper constraining of error in instr_fetching.pil.
INVALID_EXECUTION_OPCODE,
};

struct InstrDeserializationError {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -509,7 +509,7 @@ TxSimulationResult AvmSimulationHelper::simulate_fast_internal(ContractDBInterfa
*debug_log_component,
merkle_db,
*call_stack_metadata_collector,
cancellation_token);
std::move(cancellation_token));
TxExecution tx_execution(execution,
context_provider,
contract_db,
Expand Down
Loading