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
168 changes: 132 additions & 36 deletions barretenberg/cpp/pil/vm2/instr_fetching.pil
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this file got complex enough that it needs an explainer comment.
I was thinking something like

  • what this is trying to constrain (without error handling)
  • step by step explanation of the error "cascading" (eg the interdependencies)

something along the lines of...

The job of this trace is to constrain that the instruction fetching of a bytecode at a given pc is done correctly. That is, that the raw bytes are correctly translated into operands for the fetched opcode. In terms of columns and tables this means <....>

This trace also crucially handles errors. The possible kinds of errors are (from the enum maybe):
ERR_XXX: when xxxx
ERR_YYY: when yyyy

The errors and "deserialization" logic are interdependent, so the relations and lookups are cascaded to induce "temporality". The interrelationships are as follows

  • first we check if the pc is inside the range of the bytecode (the bytecode is assumed to exist in the bytecode retrieval table and to be non-empty)
  • then we check if the remaining length........ [or is it done in the same temporality group?]
  • the lookup is only done when...
  • we also check the tag but for that we need to correctly have deserialized all the operands so....

I think the above would also help me in reviewing whether the error handling is correct

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I restructured. Hopefully it is now more clear.

Large diffs are not rendered by default.

12 changes: 12 additions & 0 deletions barretenberg/cpp/pil/vm2/precomputed.pil
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,16 @@ pol constant integral_tag_length; // Columns for the byte length 1,1,2,...,16;
// However, it would extend this lookup table with pairs such as (0,0), (7,0), (8,0) which is
// not without any danger.

// Toggled at every row where clk is a byte and outside of memory tag
pol constant sel_mem_tag_out_of_range;

// WIRE INSTRUCTION SPEC table
// The WIRE_INSTRUCTION_SPEC maps a WireOpCode to different values related to the instruction format such as:
// - array of decomposition selectors: sel_op_dc_XX
// - corresponding execution opcode: exec_opcode
// - instruction size (in bytes): instr_size
// - Selector on whether the instruction has a tag: sel_has_tag
// - Selector on whether operand op2 is a tag: sel_tag_is_op2

// Selectors for operands decomposition into bytes (required by instr_fetching.pil)
// This table is populated by a map generated by a cpp test defined in op_decomposition.test.cpp.
Expand All @@ -76,6 +86,8 @@ pol constant sel_op_dc_17;

pol constant exec_opcode;
pol constant instr_size; // Instruction size in bytes
pol constant sel_has_tag; // With current instruction specs, tag can appear at op2 (SET_XXX) or op3 (CAST_8, CAST_16)
pol constant sel_tag_is_op2; // (sel_tag_is_op2 == 0 && sel_has_tag == 1) ==> op3 is a tag

// Toggled at rows whose clk interpreted as a byte does not correspond to a valid wire opcode
// Toggled only up to clk = 255. (within range specified by sel_range_8)
Expand Down
72 changes: 48 additions & 24 deletions barretenberg/cpp/src/barretenberg/vm2/common/instruction_spec.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -196,13 +196,19 @@ const std::unordered_map<WireOpCode, WireInstructionSpec> WIRE_INSTRUCTION_SPEC
.size_in_bytes = 8,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SHR_16) } },
{ WireOpCode::CAST_8,
{ .exec_opcode = ExecutionOpCode::CAST,
.size_in_bytes = 5,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::CAST_8) } },
{
.exec_opcode = ExecutionOpCode::CAST,
.size_in_bytes = 5,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::CAST_8),
.tag_operand_idx = 3, // op3
} },
{ WireOpCode::CAST_16,
{ .exec_opcode = ExecutionOpCode::CAST,
.size_in_bytes = 7,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::CAST_16) } },
{
.exec_opcode = ExecutionOpCode::CAST,
.size_in_bytes = 7,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::CAST_16),
.tag_operand_idx = 3, // op3
} },
{ WireOpCode::GETENVVAR_16,
{ .exec_opcode = ExecutionOpCode::GETENVVAR,
.size_in_bytes = 5,
Expand Down Expand Up @@ -240,29 +246,47 @@ const std::unordered_map<WireOpCode, WireInstructionSpec> WIRE_INSTRUCTION_SPEC
.size_in_bytes = 1,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::INTERNALRETURN) } },
{ WireOpCode::SET_8,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 5,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_8) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 5,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_8),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::SET_16,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 7,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_16) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 7,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_16),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::SET_32,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 9,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_32) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 9,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_32),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::SET_64,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 13,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_64) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 13,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_64),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::SET_128,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 21,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_128) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 21,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_128),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::SET_FF,
{ .exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 37,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_FF) } },
{
.exec_opcode = ExecutionOpCode::SET,
.size_in_bytes = 37,
.op_dc_selectors = WireOpCode_DC_SELECTORS.at(WireOpCode::SET_FF),
.tag_operand_idx = 2, // op2
} },
{ WireOpCode::MOV_8,
{ .exec_opcode = ExecutionOpCode::MOV,
.size_in_bytes = 4,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

#include <array>
#include <cstdint>
#include <optional>
#include <unordered_map>

#include "barretenberg/vm2/common/opcodes.hpp"
Expand Down Expand Up @@ -30,6 +31,8 @@ struct WireInstructionSpec {
ExecutionOpCode exec_opcode;
uint32_t size_in_bytes;
std::array<uint8_t, NUM_OP_DC_SELECTORS> op_dc_selectors;
std::optional<uint8_t>
tag_operand_idx; // Index of relevant operand in vector of operands as defined in WireOpCode_WIRE_FORMAT

bool operator==(const WireInstructionSpec& other) const = default;
};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,5 +35,30 @@ TEST(InstructionSpecTest, CheckAllInstructionSizes)
}
}

// Test checking that the hardcoded tag related fields in WIRE_INSTRUCTION_SPEC
// are correct. This test would fail only when we change the wire format of an instruction.
TEST(InstructionSpecTest, CheckAllInstructionsTagInformation)
{
const auto& wire_format = simulation::testonly::get_instruction_wire_formats();

for (int i = 0; i < static_cast<int>(WireOpCode::LAST_OPCODE_SENTINEL); i++) {
const auto wire_opcode = static_cast<WireOpCode>(i);
const auto& operands = wire_format.at(wire_opcode);
const auto tag_counts = std::count(operands.begin(), operands.end(), simulation::OperandType::TAG);
const auto& wire_instruction_spec = WIRE_INSTRUCTION_SPEC.at(wire_opcode);

if (wire_instruction_spec.tag_operand_idx.has_value()) {
EXPECT_EQ(tag_counts, 1);
if (wire_instruction_spec.tag_operand_idx.value() == 2) {
EXPECT_EQ(operands.at(2), simulation::OperandType::TAG);
} else {
EXPECT_EQ(operands.at(3), simulation::OperandType::TAG);
}
} else {
EXPECT_EQ(tag_counts, 0);
}
}
}

} // namespace
} // namespace bb::avm2
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@

namespace bb::avm2 {

// Adapt NUM_MEMORY_TAGS in fixtures.cpp if this enum is modified.
enum class MemoryTag {
FF,
U1,
Expand All @@ -15,6 +14,7 @@ enum class MemoryTag {
U32,
U64,
U128,
MAX = U128,
};

using MemoryAddress = uint32_t;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ using pc_abs_diff_positive_lookup = lookup_instr_fetching_pc_abs_diff_positive_r
using wire_instr_spec_lookup = lookup_instr_fetching_wire_instruction_info_relation<FF>;
using bc_decomposition_lookup = lookup_instr_fetching_bytes_from_bc_dec_relation<FF>;
using bytecode_size_bc_decomposition_lookup = lookup_instr_fetching_bytecode_size_from_bc_dec_relation<FF>;
using tag_validation_lookup = lookup_instr_fetching_tag_value_validation_relation<FF>;

using testing::random_bytes;

Expand Down Expand Up @@ -317,6 +318,7 @@ void check_all(const std::vector<InstructionFetchingEvent>& instr_events,
precomputed_builder.process_wire_instruction_spec(trace);
precomputed_builder.process_sel_range_8(trace);
precomputed_builder.process_sel_range_16(trace);
precomputed_builder.process_memory_tag_range(trace);
bytecode_builder.process_instruction_fetching(instr_events, trace);
bytecode_builder.process_decomposition(decomposition_events, trace);
range_check_builder.process(range_check_events, trace);
Expand All @@ -325,6 +327,7 @@ void check_all(const std::vector<InstructionFetchingEvent>& instr_events,
LookupIntoIndexedByClk<instr_abs_diff_positive_lookup::Settings>().process(trace);
LookupIntoDynamicTableGeneric<pc_abs_diff_positive_lookup::Settings>().process(trace);
LookupIntoIndexedByClk<wire_instr_spec_lookup::Settings>().process(trace);
LookupIntoIndexedByClk<tag_validation_lookup::Settings>().process(trace);
LookupIntoDynamicTableGeneric<bc_decomposition_lookup::Settings>().process(trace);
LookupIntoDynamicTableGeneric<bytecode_size_bc_decomposition_lookup::Settings>().process(trace);

Expand All @@ -336,6 +339,7 @@ void check_all(const std::vector<InstructionFetchingEvent>& instr_events,
check_interaction<wire_instr_spec_lookup>(trace);
check_interaction<bc_decomposition_lookup>(trace);
check_interaction<bytecode_size_bc_decomposition_lookup>(trace);
check_interaction<tag_validation_lookup>(trace);
}

// Positive test with 5 five bytecodes and bytecode_id = 0,1,2,3,4
Expand Down Expand Up @@ -528,6 +532,40 @@ TEST(InstrFetchingConstrainingTest, SingleInstructionOpcodeOutOfRange)
check_all(instr_events, gen_range_check_events(instr_events), decomposition_events);
}

// Positive test with one single instruction (SET_16) with error TAG_OUT_OF_RANGE.
// The bytecode consists into a serialized single instruction with pc = 0.
// The operand at index 1 is wrongly set to value 12
TEST(InstrFetchingConstrainingTest, SingleInstructionTagOutOfRange)
{
Instruction set_16_instruction = {
.opcode = WireOpCode::SET_16,
.indirect = 0,
.operands = { Operand::u16(0x1234), Operand::u8(12), Operand::u16(0x5678) },
};

std::vector<uint8_t> bytecode = set_16_instruction.serialize();
const auto bytecode_ptr = std::make_shared<std::vector<uint8_t>>(std::move(bytecode));

const std::vector<InstructionFetchingEvent> instr_events = {
{
.bytecode_id = 1,
.pc = 0,
.instruction = set_16_instruction,
.bytecode = bytecode_ptr,
.error = InstrDeserializationError::TAG_OUT_OF_RANGE,
},
};

const std::vector<BytecodeDecompositionEvent> decomposition_events = {
{
.bytecode_id = 1,
.bytecode = bytecode_ptr,
},
};

check_all(instr_events, gen_range_check_events(instr_events), decomposition_events);
}

// Negative interaction test with some values not matching the instruction spec table.
TEST(InstrFetchingConstrainingTest, NegativeWrongWireInstructionSpecInteractions)
{
Expand Down Expand Up @@ -556,14 +594,15 @@ TEST(InstrFetchingConstrainingTest, NegativeWrongWireInstructionSpecInteractions
ASSERT_EQ(trace.get(C::lookup_instr_fetching_wire_instruction_info_counts, static_cast<uint32_t>(opcode)), 1);
check_interaction<wire_instr_spec_lookup>(trace);

constexpr std::array<C, 20> mutated_cols = {
C::instr_fetching_exec_opcode, C::instr_fetching_instr_size, C::instr_fetching_sel_op_dc_0,
C::instr_fetching_sel_op_dc_1, C::instr_fetching_sel_op_dc_2, C::instr_fetching_sel_op_dc_3,
C::instr_fetching_sel_op_dc_4, C::instr_fetching_sel_op_dc_5, C::instr_fetching_sel_op_dc_6,
C::instr_fetching_sel_op_dc_7, C::instr_fetching_sel_op_dc_8, C::instr_fetching_sel_op_dc_9,
C::instr_fetching_sel_op_dc_10, C::instr_fetching_sel_op_dc_11, C::instr_fetching_sel_op_dc_12,
C::instr_fetching_sel_op_dc_13, C::instr_fetching_sel_op_dc_14, C::instr_fetching_sel_op_dc_15,
C::instr_fetching_sel_op_dc_16, C::instr_fetching_sel_op_dc_17,
constexpr std::array<C, 22> mutated_cols = {
C::instr_fetching_exec_opcode, C::instr_fetching_instr_size, C::instr_fetching_sel_has_tag,
C::instr_fetching_sel_tag_is_op2, C::instr_fetching_sel_op_dc_0, C::instr_fetching_sel_op_dc_1,
C::instr_fetching_sel_op_dc_2, C::instr_fetching_sel_op_dc_3, C::instr_fetching_sel_op_dc_4,
C::instr_fetching_sel_op_dc_5, C::instr_fetching_sel_op_dc_6, C::instr_fetching_sel_op_dc_7,
C::instr_fetching_sel_op_dc_8, C::instr_fetching_sel_op_dc_9, C::instr_fetching_sel_op_dc_10,
C::instr_fetching_sel_op_dc_11, C::instr_fetching_sel_op_dc_12, C::instr_fetching_sel_op_dc_13,
C::instr_fetching_sel_op_dc_14, C::instr_fetching_sel_op_dc_15, C::instr_fetching_sel_op_dc_16,
C::instr_fetching_sel_op_dc_17,
};

// Mutate execution opcode
Expand Down Expand Up @@ -702,6 +741,49 @@ TEST(InstrFetchingConstrainingTest, NegativeWrongBytecodeSizeBcDecompositionInte
}
}

// Negative interaction test for #[TAG_VALUE_VALIDATION] where tag_out_of_range is wrongly mutated
TEST(InstrFetchingConstrainingTest, NegativeWrongTagValidationInteractions)
{
TestTraceContainer trace;
BytecodeTraceBuilder bytecode_builder;
PrecomputedTraceBuilder precomputed_builder;

// Some chosen opcode with a tag. We limit to one as this unit test is costly.
// Test works if the following vector is extended to other opcodes though.
std::vector<WireOpCode> opcodes = { WireOpCode::SET_8 };

for (const auto& opcode : opcodes) {
TestTraceContainer trace;
const auto instr = testing::random_instruction(opcode);
bytecode_builder.process_instruction_fetching(
{ { .bytecode_id = 1,
.pc = 0,
.instruction = instr,
.bytecode = std::make_shared<std::vector<uint8_t>>(instr.serialize()) } },
trace);
precomputed_builder.process_memory_tag_range(trace);
precomputed_builder.process_sel_range_8(trace);
precomputed_builder.process_misc(trace, trace.get_num_rows()); // Limit to the number of rows we need.

LookupIntoIndexedByClk<tag_validation_lookup::Settings>().process(trace);

auto valid_trace = trace; // Keep original trace before lookup processing
check_interaction<tag_validation_lookup>(valid_trace);

// Mutate tag out-of-range error
auto mutated_trace = trace;
ASSERT_EQ(trace.get(C::instr_fetching_tag_out_of_range, 1), 0);
mutated_trace.set(C::instr_fetching_tag_out_of_range, 1, 1); // Mutate by toggling the error.

// We do not need to re-run LookupIntoIndexedByClk<tag_validation_lookup::Settings>().process(trace);
// because we never mutate the indexing column for this lookup (clk) and for this lookup
// find_in_dst only uses column C::instr_fetching_tag_value mapped to (clk). So, the counts are still valid.

EXPECT_THROW_WITH_MESSAGE(check_interaction<tag_validation_lookup>(mutated_trace),
"Relation.*TAG_VALUE_VALIDATION.* ACCUMULATION.* is non-zero");
}
}

// Negative test on not toggling instr_out_of_range when instr_size > bytes_to_read
TEST(InstrFetchingConstrainingTest, NegativeNotTogglingInstrOutOfRange)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ std::string render_pil(
: format("#[OP", static_cast<uint32_t>(i), "_BYTES_DECOMPOSITION]\n");
pil_equations += (i == 0) ? "indirect = " : format(OPERAND_PREFIX, static_cast<uint32_t>(i), " = ");

pil_equations += "(1 - parsing_err) * ("; // Error gating multiplicative term
pil_equations += "(1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * ("; // Error gating multiplicative term

std::vector<std::string> additive_terms;
for (const auto& sel_layout : sel_layout_breakdowns[i]) {
Expand Down
10 changes: 5 additions & 5 deletions barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp

Large diffs are not rendered by default.

10 changes: 7 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm2/generated/flavor.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -95,13 +95,13 @@ class AvmFlavor {
// This flavor would not be used with ZK Sumcheck
static constexpr bool HasZK = false;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 44;
static constexpr size_t NUM_WITNESS_ENTITIES = 923;
static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 47;
static constexpr size_t NUM_WITNESS_ENTITIES = 929;
static constexpr size_t NUM_SHIFTED_ENTITIES = 134;
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
// We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 1101;
static constexpr size_t NUM_ALL_ENTITIES = 1110;

// In the sumcheck univariate computation, we divide the trace in chunks and each chunk is
// evenly processed by all the threads. This constant defines the maximum number of rows
Expand Down Expand Up @@ -173,6 +173,7 @@ class AvmFlavor {
lookup_instr_fetching_bytes_from_bc_dec_relation<FF_>,
lookup_instr_fetching_instr_abs_diff_positive_relation<FF_>,
lookup_instr_fetching_pc_abs_diff_positive_relation<FF_>,
lookup_instr_fetching_tag_value_validation_relation<FF_>,
lookup_instr_fetching_wire_instruction_info_relation<FF_>,
lookup_merkle_check_merkle_poseidon2_relation<FF_>,
lookup_poseidon2_hash_poseidon2_perm_relation<FF_>,
Expand Down Expand Up @@ -459,7 +460,9 @@ class AvmFlavor {
this->precomputed_p_decomposition_radix = verification_key->precomputed_p_decomposition_radix;
this->precomputed_power_of_2 = verification_key->precomputed_power_of_2;
this->precomputed_sel_bitwise = verification_key->precomputed_sel_bitwise;
this->precomputed_sel_has_tag = verification_key->precomputed_sel_has_tag;
this->precomputed_sel_integral_tag = verification_key->precomputed_sel_integral_tag;
this->precomputed_sel_mem_tag_out_of_range = verification_key->precomputed_sel_mem_tag_out_of_range;
this->precomputed_sel_op_dc_0 = verification_key->precomputed_sel_op_dc_0;
this->precomputed_sel_op_dc_1 = verification_key->precomputed_sel_op_dc_1;
this->precomputed_sel_op_dc_10 = verification_key->precomputed_sel_op_dc_10;
Expand All @@ -482,6 +485,7 @@ class AvmFlavor {
this->precomputed_sel_range_16 = verification_key->precomputed_sel_range_16;
this->precomputed_sel_range_8 = verification_key->precomputed_sel_range_8;
this->precomputed_sel_sha256_compression = verification_key->precomputed_sel_sha256_compression;
this->precomputed_sel_tag_is_op2 = verification_key->precomputed_sel_tag_is_op2;
this->precomputed_sel_to_radix_safe_limbs = verification_key->precomputed_sel_to_radix_safe_limbs;
this->precomputed_sel_unary = verification_key->precomputed_sel_unary;
this->precomputed_sha256_compression_round_constant =
Expand Down
Loading