feat: merge-train/avm (#22433)

BEGIN_COMMIT_OVERRIDE
chore(avm)!: Instruction Fetching pre-audit (#22221)
END_COMMIT_OVERRIDE

Author: AztecBot

barretenberg/cpp/pil/vm2/bytecode/bc_decomposition.pil

@@ -98,7 +98,7 @@ include "../precomputed.pil";
  *                --> bc_retrieval.pil                            --> precomputed.pil
  * This trace is looked up by:
  * - instr_fetching.pil: To constrain the bytecode size (#[BYTECODE_SIZE_FROM_BC_DEC]) and values (#[BYTES_FROM_BC_DEC]).
- * - bc_hashing.pil: To constrain the bytecode size (#[CHECK_FINAL_BYTES_REMAINING] and #[BYTECODE_LENGTH_BYTES]) and packed field values
+ * - bc_hashing.pil: To constrain the bytecode size (#[BYTECODE_LENGTH_BYTES]) and packed field values
  *                   (#[GET_PACKED_FIELD_i] for i = 0, 1, 2) via a multipermutation. It enforces that the id is the public bytecode commitment.
  *
  * This trace looks up:

barretenberg/cpp/pil/vm2/bytecode/instr_fetching.pil

@@ -2,46 +2,115 @@ include "bc_decomposition.pil";
 
 include "../range_check.pil";
 include "../constants_gen.pil";
-
-// Explanations
-// *****************************************************************************
-// The role of this subtrace is to fetch an instruction from the bytecode at a
-// position specified by pc. This subtrace copies the relevant bytecode portion
-// from subtrace specified in bc_decomposition.pil.
-// Note that instruction fetching will only be performed for the instructions
-// which are executed by the execution trace and only once, i.e., even if
-// the AVM executes several times a given instruction, the current sub-trace
-// will only produce one row per static instruction.
-// The main work performed by the current sub-trace consists in transforming
-// bytes into the operands of the corresponding instruction. This part is
-// expressed by the relations #[ADDRESSING_MODE_BYTES_DECOMPOSITION] and
-// #[OPXXX_BYTES_DECOMPOSITION]. They encode each operand based on relevant bytes
-// of the relative position to PC depending on each opcode. Each wire opcode has
-// a static specification in precomputed.pil (see WIRE INSTRUCTION SPEC table)
-// corresponding to the operand decomposition (sel_op_dc_XXX).
-// All the other relations deal with error handling (except lookups/interactions).
-// We handle 4 possible different errors and consolidate into a single one: sel_parsing_err.
-// Only sel_parsing_err is propagated to the execution trace.
-// List of errors:
-// 1) pc_out_of_range: pc is out-of-range if pc >= bytecode_size.
-//    - bytecode_size is retrieved from bc_decomposition.pil at pc == 0.
-// 2) opcode_out_of_range:
-//    - opcode is out-of-range if the byte at pc is not a valid wire opcode.
-//    - this information is retrieved from precomputed.pil.
-// 3) instr_out_of_range: remaing bytes in bytecode are less than instruction size.
-//    - instruction size (in bytes) is retrieved from precomputed.pil.
-//    - bytes_to_read (remaining bytes in bytecode) is retrieved from bc_decomposition.pil.
-// 4) tag_out_of_range:
-//    - tag is out-of-range if a tag operand is not a valid memory tag.
-//    - this information is retrieved from precomputed.pil.
-//
-// There is a hierarchy among these errors, in the sense that if any of them is encountered
-// the next ones are irrelevant. If pc is out of range, there is no instruction to consider.
-// If the opcode is invalid, we cannot consider any instruction. If the instruction is not
-// complete then there is no point to validate tag operands.
-// Thus, our witness generation will never toggle more than a single error. We will
-// enforce this constraint as it will help reducing the degrees of some relations.
-// Assuming disjoint erros, the consolidated error is simply the sum of the 4 errors.
+include "../precomputed.pil";
+
+/**
+ * This subtrace fetches and validates instructions from bytecode. It is used during execution
+ * at each active row, as long as the context's bytecode has been successfully retrieved.
+ * For our purposes an instruction can be thought of as:
+ *    - Opcode (exec_opcode, u8): The operation to perform encoded numerically as defined in our
+ *        instruction specification e.g. the SUB operation is mapped to 1.
+ *    - Operands ([op1, ..., op7], MemoryValue[]): The inputs and/or outputs of the operation. The
+ *        number of operands and their types differs per opcode e.g. FDIV has three; two FF inputs
+ *        and one FF output.
+ *    - Addressing Mode (addressing_mode, u16): The indirect and relative contributions of the operands
+ *        encoded as a u16. Each bit pair of the value represents whether the corresponding operand is
+ *        direct (00), indirect (01), or relative (10). See yarn-project/simulator/docs/avm/addressing.md
+ *        for the encoding breakdown and an example.
+ *
+ * The main work of this trace is to derive the decoded operands of an instruction from raw bytecode
+ * bytes and our opcode specification:
+ *    - addressing_mode: #[ADDRESSING_MODE_BYTES_DECOMPOSITION]
+ *    - [op1, op2, op3, op4, op5, op6, op7]: #[OPXXX_BYTES_DECOMPOSITION]
+ *
+ * It copies the relevant bytecode portion from bc_decomposition.pil (#[BYTES_FROM_BC_DEC]):
+ *   bd0 = bytecode[pc], bd1 = bytecode[pc+1], ..., bd36 = bytecode[pc+36],
+ * where bc_decomposition holds a 37 (= MAX_INSTRUCTION_SIZE) byte sliding window starting at the
+ * position specified by pc. The first byte (bd0) is the wire opcode and the remaining are raw operand bytes.
+ *
+ * The operands' encoding is determined per opcode by the WIRE_INSTRUCTION_SPEC in precomputed.pil.
+ * This specification provides: exec_opcode, instr_size, operand decomposition selectors (sel_op_dc_0..16)
+ * and tag metadata (sel_has_tag, sel_tag_is_op2). We use the decomposition selectors to transform the
+ * fetched bytecode bytes (bd0..36) into the operands (addressing_mode, op1..7)).
+ *
+ * The remaining work of this trace uses other specification data to handle errors (see ERROR HANDLING).
+ *
+ *
+ * PRECONDITIONS:
+ * - The bytecode identified by bytecode_id must already be decomposed in bc_decomposition.pil.
+ * - The [pc, bytecode_id] pairs present in this trace correspond to an instruction in a successfully
+ *   retrieved bytecode. This is enforced by execution.pil lookups.
+ *
+ * USAGE: Note that this subtrace is only designed to be used by execution, where it is accessed by
+ *        two separate lookups. This allows for error handling without having to constrain partial
+ *        instructions on parsing failure.
+ * To determine whether parsing succeeded (#[INSTRUCTION_FETCHING_RESULT] in execution.pil):
+ *      sel_bytecode_retrieval_success {
+ *             pc, bytecode_id, sel_instruction_fetching_failure
+ *      } in instr_fetching.sel {
+ *          instr_fetching.pc, instr_fetching.bytecode_id, instr_fetching.sel_parsing_err
+ *      };
+ *
+ * To retrieve the full decoded instruction, only when parsing succeeded (using
+ * sel_instruction_fetching_success == !sel_instruction_fetching_failure && sel_bytecode_retrieval_success
+ * to gate #[INSTRUCTION_FETCHING_BODY] in execution.pil):
+ *      sel_instruction_fetching_success {
+ *          pc, bytecode_id, exec_opcode,
+ *          instr_size, addressing_mode,
+ *          op[0], op[1], op[2], op[3], op[4],
+            op[5], op[6]
+ *      } in instr_fetching.sel {
+ *          instr_fetching.pc, instr_fetching.bytecode_id, instr_fetching.exec_opcode,
+ *          instr_fetching.instr_size, instr_fetching.addressing_mode,
+ *          instr_fetching.op1, instr_fetching.op2, instr_fetching.op3, instr_fetching.op4,
+ *          instr_fetching.op5, instr_fetching.op6, instr_fetching.op7
+ *      };
+ *
+ * ERROR HANDLING:
+ * The trace detects four (mutually exclusive) parsing errors, consolidated into sel_parsing_err:
+ *   1. pc_out_of_range:     pc >= bytecode_size.
+ *      Determined by #[PC_OUT_OF_RANGE_TOGGLE] where bytecode_size is looked up from bc_decomposition.
+ *   2. opcode_out_of_range: bd0 does not correspond to a valid wire opcode.
+ *      Determined by the precomputed table entry for bd0 (#[WIRE_INSTRUCTION_INFO]).
+ *   3. instr_out_of_range:  bytes_to_read < instr_size.
+ *      Determined by #[INSTR_OUT_OF_RANGE_TOGGLE] where bytes_to_read is looked up from
+ *      bc_decomposition and instr_size is from the precomputed table entry (#[WIRE_INSTRUCTION_INFO]).
+ *   4. tag_out_of_range:    a tag operand does not correspond to a valid memory tag.
+ *      Determined by the precomputed table entry for the tag operand (op2 or op3) (#[TAG_VALUE_VALIDATION]).
+ *
+ * The errors are hierarchical in the above order (see simulation -> deserialize_instruction()); if
+ * any are encountered, the following are irrelevant. Thus, witness generation sets at most one error flag,
+ * where disjointness is enforced by the definition of sel_parsing_err. Only sel_parsing_err is propagated to
+ * execution.pil.
+ *
+ * Note that decoded operands are enforced to be 0 when any of errors 1-3 are active (denoted by
+ * PARSING_ERROR_EXCEPT_TAG_ERROR == 1).
+ *
+ * TRACE SHAPE: One row per unique [pc, bytecode_id] pair. Note that simulation deduplicates
+ *   instructions that have already been processed i.e. when the same [pc, bytecode_id] pair is
+ *   retrieved multiple times in the same tx, only one event is emitted.
+ *   See InstructionFetchingEvent and DeduplicatingEventEmitter used in simulate_for_witgen.
+ *
+ * INTERACTIONS:
+ *  execution.pil --> instr_fetching.pil --> bc_decomposition.pil <-> bc_hashing.pil
+ *                                       --> precomputed.pil
+ *                                       --> range_check.pil
+ *
+ * This subtrace is looked up by:
+ * - execution.pil: To fetch the instruction at [pc, bytecode_id] and detect parse errors
+ *                  (#[INSTRUCTION_FETCHING_RESULT] and #[INSTRUCTION_FETCHING_BODY]).
+ *
+ * This subtrace looks up:
+ * - bc_decomposition.pil: To retrieve the bytecode size (#[BYTECODE_SIZE_FROM_BC_DEC]) and the
+ *                         encoded instruction bytes for [pc, bytecode_id] (#[BYTES_FROM_BC_DEC]).
+ * - precomputed.pil: To retrieve the wire instruction information for the opcode (#[WIRE_INSTRUCTION_INFO],
+ *                    by opcode byte bd0), to validate the tag operand if it exists
+ *                    (#[TAG_VALUE_VALIDATION]), and to enforce that instr_abs_diff is positive via
+ *                    a range check (#[INSTR_ABS_DIFF_POSITIVE]).
+ * - range_check.pil: To to enforce that pc_abs_diff is positve via a range check (#[PC_ABS_DIFF_POSITIVE]).
+ *
+ * Note that the latter two range checks are on 8 and 32 bit numbers resp., hence use different traces.
+ */
 
 namespace instr_fetching;
 
@@ -88,37 +157,34 @@ sel_parsing_err * (1 - sel_parsing_err) = 0; // enforces disjoint errors
 //                Handling pc_out_of_range error
 // ****************************************************************************
 
-// Retrieved from bc_decomposition.pil based on bytecode_id with pc == 0
+// Size of the bytecode in bytes (constrained by #[BYTECODE_SIZE_FROM_BC_DEC]).
 pol commit bytecode_size;
 
-// We have to enforce that: pc < bytecode_size <==> pc_out_of_range == 0
-// We use a specific absolute difference value to distinguish pc < bytecode_size
-// from pc >= bytecode_size.
-
-// pc - bytecode_size       if bytecode_size <= pc
+// Absolute difference variant where we compute:
+// pc - bytecode_size       if bytecode_size <= pc (pc_out_of_range == 1)
 // bytecode_size - pc - 1   if bytecode_size > pc
 pol commit pc_abs_diff;
+
+// From the following relation, we have: pc_abs_diff >= 0 ==> [pc >= bytecode_size <==> pc_out_of_range == 1]
 #[PC_OUT_OF_RANGE_TOGGLE]
 pc_abs_diff = sel * ((2 * pc_out_of_range - 1) * (pc - bytecode_size) - 1 + pc_out_of_range);
 
-// TODO: Remove this one once we support constant in lookup tuples
-// A column with the value 32 at each row.
+// Lookup constant support: Can be removed when we support constants in lookups.
 pol commit pc_size_in_bits;
 sel * (pc_size_in_bits - constants.AVM_PC_SIZE_IN_BITS) = 0;
 
 // pc_abs_diff is 32-bit long (pc is uint32_t)
-// Use constant AVM_PC_SIZE_IN_BITS once we support constants in lookup tuples.
 #[PC_ABS_DIFF_POSITIVE]
 sel { pc_abs_diff, pc_size_in_bits } in range_check.sel { range_check.value, range_check.rng_chk_bits };
 
 // ****************************************************************************
 //                Handling instr_out_of_range error
 // ****************************************************************************
 
-// Number of bytes which were read at a given pc. Retrieved from bc_decomposition.pil
+// Number of bytes which were read at a given pc (constrained by #[BYTES_FROM_BC_DEC]).
 pol commit bytes_to_read;
 
-// Instruction size in bytes. Copied from precomputed.pil
+// Instruction size in bytes (constrained by #[WIRE_INSTRUCTION_INFO]).
 pol commit instr_size;
 
 // Absolute difference variant where we compute:
@@ -138,17 +204,27 @@ sel { instr_abs_diff } in precomputed.sel_range_8 { precomputed.idx };
 //                Handling tag_out_of_range error
 // ****************************************************************************
 
-// Retrieved from precomputed.pil (instruction specification)
-pol commit sel_has_tag; // @boolean (by lookup only when sel_pc_in_range == 1) - With current instruction specs, tag can appear at op2 (SET_XXX) or op3 (CAST_8, CAST_16)
-pol commit sel_tag_is_op2; // @boolean (by lookup only when sel_pc_in_range == 1) - (sel_tag_is_op2 == 0 && sel_has_tag == 1) ==> op3 is a tag
+// Retrieved from precomputed.pil (instruction specification).
+// Whether this instruction has a tag. Constrained by the precomputed table (#[WIRE_INSTRUCTION_INFO])
+// to be 1 iff we have a wire opcode (represented by bd0) with a tag as defined in the instruction spec.
+pol commit sel_has_tag; // @boolean (by lookup only when sel_pc_in_range == 1)
+
+// Whether the tag exists at op2 (== 1) or op3, if exists (sel_tag_is_op2 == 0 && sel_has_tag == 1 ==> op3 is a tag).
+// Constrained, like sel_has_tag, by the precomputed table (#[WIRE_INSTRUCTION_INFO]) against the wire opcode.
+pol commit sel_tag_is_op2; // @boolean (by lookup only when sel_pc_in_range == 1)
 
-// Value to validate as tag. According to our instruction specifications, there is a maximum of one tag per instruction
-// and it appears only at op2 or op3.
+// Value to validate as tag. According to our current instruction specifications, there is a maximum of one
+// tag per instruction and it appears only at op2 (SET_XXX) or op3 (CAST_8, CAST_16).
+// Lookup constant support: Can be removed when we support constants in lookups.
 pol commit tag_value;
+// Note that (sel_has_tag - sel_tag_is_op2) cannot underflow (= p - 1) since the precomputed table enforces
+// that sel_tag_is_op2 == 1 ==> sel_has_tag == 1 (#[WIRE_INSTRUCTION_INFO]). When this lookup is skipped (sel_pc_in_range == 0)
+// we have pc_out_of_range == 1, meaning an error hierarchically higher than tag_out_of_range is activated, and we have
+// the same outcome of a sel_parsing_err to process anyway.
 #[TAG_VALUE]
 tag_value = (sel_has_tag - sel_tag_is_op2) * op3 + sel_tag_is_op2 * op2;
 
-// TODO: Investigate whether enforcing the tag checking in execution trace or in CAST/SET gadgets might be a better option.
+// TODO(#AVM-263): Investigate whether enforcing the tag checking in execution trace or in CAST/SET gadgets might be a better option.
 #[TAG_VALUE_VALIDATION]
 sel_has_tag { tag_value, tag_out_of_range } in precomputed.sel_range_8 { precomputed.idx, precomputed.sel_mem_tag_out_of_range };
 

barretenberg/cpp/pil/vm2/context.pil

@@ -242,9 +242,9 @@ namespace execution;
     //         PC and NEXT_PC
     // =============================
 
-    // `instr_length` is from execution.pil and constrained when `sel_instruction_fetching_success == 1`.
+    // `instr_size` is from execution.pil and constrained when `sel_instruction_fetching_success == 1`.
     #[NEXT_PC]
-    sel_instruction_fetching_success * (pc + instr_length - next_pc) = 0;
+    sel_instruction_fetching_success * (pc + instr_size - next_pc) = 0;
 
     // Initialization: enqueued_call_start = 1 ==> pc = 0;
     //                 sel_enter_call      = 1 ==> pc' = 0;

barretenberg/cpp/pil/vm2/execution.pil

@@ -196,19 +196,21 @@ sel_bytecode_retrieval_success = sel * (1 - sel_bytecode_retrieval_failure);
  *  Temporality group 2: Instruction fetching
  **************************************************************************************************/
 
-pol commit instr_length; // Need this for shift col on next_pc
+pol commit instr_size; // Need this for shift col on next_pc
 pol commit sel_instruction_fetching_failure; // @boolean (by definition below)
 
-pol commit ex_opcode;
+pol commit exec_opcode;
 pol commit addressing_mode;
 pol commit op[7];  // operands
 
 // We now proceed to fetch the instruction.
-// The handling is slightly subtle: suppose fetching fails, then in simulation/tracegen
-// we will NOT have the partial information of the instruction, and we prefer to leave
-// the instruction unconstrained here. Fixing this would require the partial instruction
-// result to execution.cpp which is not very elegant neither.
-// This is why we do 2 lookups instead of 1.
+
+// We separate the fetching into two lookups. This ensures that if fetching fails we constrain
+// the error cleanly without needing to feed execution partial and/or filler instruction values.
+//  1. #[INSTRUCTION_FETCHING_RESULT] - constrains the success or failure of fetching given we
+//      have retrieved the bytecode.
+//  2. #[INSTRUCTION_FETCHING_BODY] - constrains the instruction's addressing, operands, and
+//      size against the opcode, given we have retrieved the bytecode and parsed the instruction.
 
 // Note: the below lookups additionally constrain that the bytecode with bytecode_id has
 // been correctly hashed due to instr_fetching's lookups into bc_decomposition, where
@@ -232,8 +234,8 @@ sel_instruction_fetching_success = sel_bytecode_retrieval_success * (1 - sel_ins
 sel_instruction_fetching_success {
     pc,
     bytecode_id,
-    ex_opcode,
-    instr_length,
+    exec_opcode,
+    instr_size,
     addressing_mode,
     op[0],
     op[1],
@@ -265,7 +267,7 @@ sel_instruction_fetching_success {
 
 #[EXEC_SPEC_READ]
 sel_instruction_fetching_success {
-    ex_opcode,
+    exec_opcode,
     // in gas.pil.
     opcode_gas,
     base_da_gas,

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/exec_op_id.test.cpp

@@ -182,7 +182,7 @@ TEST(ExecOpIdConstrainingTest, InteractionWithExecInstructionSpec)
         trace.set(C::execution_sel_should_execute_opcode, static_cast<uint32_t>(i + 1), 1);
         trace.set(C::execution_sel_exec_dispatch_execution, static_cast<uint32_t>(i + 1), 1);
         trace.set(SELECTOR_COLUMNS.at(i), static_cast<uint32_t>(i + 1), 1);
-        trace.set(C::execution_ex_opcode,
+        trace.set(C::execution_exec_opcode,
                   static_cast<uint32_t>(i + 1),
                   static_cast<uint8_t>(events.at(i).wire_instruction.get_exec_opcode()));
     }