feat: merge-train/avm

barretenberg/cpp/pil/vm2/alu.pil

@@ -142,10 +142,10 @@ pol commit ic_tag;
 // Common helper selectors
 pol commit sel_is_ff; // @boolean (whether input a is a field)
 pol commit sel_is_u128; // @boolean (whether input a is a u128)
-pol IS_NOT_FF = 1 - sel_is_ff; // @boolean Follows from definition.
-pol IS_NOT_U128 = 1 - sel_is_u128; // @boolean Follows from definition.
-pol SHIFT_OPS = sel_op_shl + sel_op_shr; // @boolean Follows from definition and mutual exclusion.
-pol DIV_OPS = sel_op_div + sel_op_fdiv; // @boolean Follows from definition and mutual exclusion.
+pol IS_NOT_FF = 1 - sel_is_ff; // @boolean (by definition)
+pol IS_NOT_U128 = 1 - sel_is_u128; // @boolean (by definition)
+pol SHIFT_OPS = sel_op_shl + sel_op_shr; // @boolean (by definition and mutual exclusion)
+pol DIV_OPS = sel_op_div + sel_op_fdiv; // @boolean (by definition and mutual exclusion)
 
 // Note that #[OP_ID_CHECK] ensures selectors are mutually exclusive.
 // Therefore, SHIFT_OPS and DIV_OPS are boolean.
@@ -173,8 +173,8 @@ sel * (TAG_U128_DIFF * (sel_is_u128 * (1 - tag_u128_diff_inv) + tag_u128_diff_in
 /******************************************************************************
 * Error Handling
 ******************************************************************************/
-pol commit sel_err; // @boolean Follows from definition (see #[ERR_CHECK]).
-pol commit sel_tag_err; // @boolean Follows from definition (see #[TAG_ERR_CHECK]).
+pol commit sel_err; // @boolean (by definition, see #[ERR_CHECK])
+pol commit sel_tag_err; // @boolean (by definition, see #[TAG_ERR_CHECK])
 pol commit sel_ab_tag_mismatch; // @boolean
 pol commit sel_div_0_err; // @boolean
 
@@ -280,7 +280,7 @@ pol SEL_DIV_U128 = sel_div_no_err * sel_is_u128;
 * BIT DECOMPOSITION (Common helper for MUL, DIV, SHL, SHR)
 ******************************************************************************/
 // We use the below to prove correct decomposition of some values into limbs. Currently used by MUL, DIV, SHL, and SHR.
-pol commit sel_decompose_a; // @boolean by definition and mutual exclusion of opcode selectors.
+pol commit sel_decompose_a; // @boolean (by definition and mutual exclusion of opcode selectors)
 sel_decompose_a = (1 - sel_err) * (sel_mul_div_u128 + SHIFT_OPS);
 // Currently, sel_decompose_b would just equal sel_mul_div_u128, so no need for another column.
 pol commit a_lo, a_hi, b_lo, b_hi; // Limbs of the decomposed value. Range values defined by LIMB_SIZE.
@@ -372,23 +372,23 @@ SEL_MUL_U128 * (
     ) = 0;
 
 // We need to range check c_hi < 2^64 for non-FF values and when there is no error.
-pol commit sel_mul_no_err_non_ff; // @boolean Follows from definition.
+pol commit sel_mul_no_err_non_ff; // @boolean (by definition)
 sel_mul_no_err_non_ff = IS_NOT_FF * (1 - sel_err) * sel_op_mul;
 #[RANGE_CHECK_MUL_C_HI]
 sel_mul_no_err_non_ff { c_hi, constant_64 } in range_check.sel_alu { range_check.value, range_check.rng_chk_bits };
 
 // ------------------------------------------------------------
 // DIV & FDIV
 // ------------------------------------------------------------
-pol commit sel_div_no_err; // @boolean Follows from definition.
+pol commit sel_div_no_err; // @boolean (by definition)
 sel_div_no_err = sel_op_div * (1 - sel_err);
 // We need to show that remainder < b (remainder stored in helper1)
 // We use #[INT_GT] below (see LT/LTE) by setting gt_input_a = b, gt_input_b = helper1, gt_result_c = 1 (gated by sel_div_no_err).
 
 // DIV - u128
 
 // Using this to switch on the range checks for decomposed u128 integers (#[OP_ID_CHECK] ensures selectors are mutually exclusive)
-pol commit sel_mul_div_u128; // @boolean Follows from definition.
+pol commit sel_mul_div_u128; // @boolean (by definition)
 // SEL_MUL_U128 || SEL_DIV_U128
 sel_mul_div_u128 = SEL_MUL_U128 + SEL_DIV_U128;
 
@@ -452,11 +452,11 @@ sel_op_eq * (1 - sel_err) * (DIFF * (ic * (1 - ab_diff_inv) + ab_diff_inv) - 1 +
 // ------------------------------------------------------------
 pol SEL_LT_OPS = (1 - sel_err) * (sel_op_lt + sel_op_lte);
 
-pol commit sel_ff_gt; // @boolean Follows from definition.
+pol commit sel_ff_gt; // @boolean (by definition)
 // sel_is_ff & SEL_LT_OPS:
 sel_ff_gt = sel_is_ff * SEL_LT_OPS;
 
-pol commit sel_int_gt; // @boolean Follows from definition.
+pol commit sel_int_gt; // @boolean (by definition)
 // (!sel_is_ff & SEL_LT_OPS) || sel_div_no_err:
 sel_int_gt = IS_NOT_FF * SEL_LT_OPS + sel_div_no_err;
 
@@ -623,7 +623,7 @@ sel_trunc_lt_128 * (1 - sel_trunc_lt_128) = 0;
 
 // Truncation separation case
 // Mutually exclusive due to sel_op_truncate being boolean
-pol commit sel_trunc_non_trivial; // @boolean Follows from definition. TODO: Aliases this once lookups support aliases for selectors.
+pol commit sel_trunc_non_trivial; // @boolean (by definition) TODO: Aliases this once lookups support aliases for selectors.
 
 #[SEL_TRUNC_NON_TRIVIAL]
 sel_trunc_non_trivial = sel_trunc_gte_128 + sel_trunc_lt_128;

barretenberg/cpp/pil/vm2/bitwise.pil

@@ -49,7 +49,7 @@ sel * (1 - sel) = 0;
 #[skippable_if]
 sel = 0;
 
-pol commit start; // Identifies when we want to capture the output to the main trace.
+pol commit start; // @boolean Identifies when we want to capture the output to the main trace.
 // Must be constrained as a boolean as any selector used in a lookup/permutation.
 start * (1 - start) = 0;
 
@@ -68,16 +68,16 @@ start_sha256 * (1 - start_sha256) = 0;
 pol commit ctr;
 
 // The error flags for this subtrace
-pol commit sel_tag_ff_err;
+pol commit sel_tag_ff_err; // @boolean
 sel_tag_ff_err * (1 - sel_tag_ff_err) = 0;
-pol commit sel_tag_mismatch_err;
+pol commit sel_tag_mismatch_err; // @boolean
 sel_tag_mismatch_err * (1 - sel_tag_mismatch_err) = 0;
 
 // Consolidated error flag
-pol commit err;
+pol commit err; // @boolean (by definition)
 err = 1 - (1 - sel_tag_mismatch_err) * (1 - sel_tag_ff_err);
 // last is a boolean which serves to mark the end of the computation (end of latch)
-pol commit last;
+pol commit last; // @boolean
 last * (1 - last) = 0;
 #[LAST_ON_ERROR] // last = 1 if err = 1
 err * (last - 1) = 0;

barretenberg/cpp/pil/vm2/bytecode/address_derivation.pil

@@ -6,7 +6,7 @@ include "../scalar_mul.pil";
 
 namespace address_derivation;
 
-    pol commit sel;
+    pol commit sel; // @boolean
     sel * (1 - sel) = 0;
 
     #[skippable_if]

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

@@ -9,7 +9,7 @@ include "../precomputed.pil";
 
 namespace bc_decomposition;
 
-pol commit sel;
+pol commit sel; // @boolean
 sel * (1 - sel) = 0;
 // No relations will be checked if this identity is satisfied.
 #[skippable_if]
@@ -29,7 +29,7 @@ pol commit bytes_remaining;
 
 // This column should be 1 iff the contract is switching, i.e., this row is the last one
 // of a contract bytecode. This is equivalent to bytes_remaining == 1.
-pol commit last_of_contract;
+pol commit last_of_contract; // @boolean
 last_of_contract * (1 - last_of_contract) = 0;
 
 // This is the most important column. It contains the bytecode one byte at a time on each row.
@@ -132,12 +132,12 @@ pol commit bytes_pc_plus_1, bytes_pc_plus_2, bytes_pc_plus_3, bytes_pc_plus_4, b
 //   39 |               1 |             1 |   0xD | 0x0 | 0x0 | ...
 
 pol commit bytes_to_read;
-pol commit sel_windows_gt_remaining;
+pol commit sel_windows_gt_remaining; // @boolean
 sel_windows_gt_remaining * (1 - sel_windows_gt_remaining) = 0;
 // We need to constrain bytes_to_read = min(WINDOW_SIZE, bytes_remaining) which is equal to
 // bytes_remaining if bytes_remaining <= WINDOW_SIZE and WINDOW_SIZE otherwise.
 
-pol commit is_windows_eq_remaining;
+pol commit is_windows_eq_remaining; // @boolean
 pol commit windows_min_remaining_inv;
 is_windows_eq_remaining * (1 - is_windows_eq_remaining) = 0;
 
@@ -224,11 +224,11 @@ bytes_pc_plus_36 = (1 - LATCH_CONDITION) * bytes_pc_plus_35';
 // We will have a selector for the PCs that are packed. This only needs to happen
 // for PCs 0, 31, 62, ...
 
-pol commit sel_packed;
+pol commit sel_packed; // @boolean
 sel_packed * (1 - sel_packed) = 0;
 
 // Permutation selectors (bc_hashing.pil).
-pol commit sel_packed_read[3];
+pol commit sel_packed_read[3]; // @boolean
 sel_packed_read[0] * (1 - sel_packed_read[0]) = 0;
 sel_packed_read[1] * (1 - sel_packed_read[1]) = 0;
 sel_packed_read[2] * (1 - sel_packed_read[2]) = 0;

barretenberg/cpp/pil/vm2/bytecode/bc_hashing.pil

@@ -47,7 +47,7 @@ include "../constants_gen.pil";
 
 namespace bc_hashing;
 
-    pol commit sel;
+    pol commit sel; // @boolean
     sel * (1 - sel) = 0;
 
     // Skippable
@@ -63,7 +63,7 @@ namespace bc_hashing;
 
     // Triggers the lookup to the address derivation subtrace, signifies the row that contains the final bytecode hash for this id
     // The sequencer can decide where to put this latch.
-    pol commit latch;
+    pol commit latch; // @boolean
     latch * (1 - latch) = 0;
 
     // latch == 1 ==> sel == 1
@@ -75,11 +75,11 @@ namespace bc_hashing;
     pol LATCH_CONDITION = latch + precomputed.first_row;
 
     // The start of a new bytecode id and new set of hashing runs:
-    pol commit start;
+    pol commit start; // @boolean
     start * (1 - start) = 0;
 
     // Needs to be a committed column as it is used in the lookup:
-    pol commit sel_not_start;
+    pol commit sel_not_start; // @boolean (by definition)
     sel_not_start = sel * (1 - start);
 
     // If the current row is a latch or the first row, the next row should be a start (if it's active):
@@ -132,7 +132,8 @@ namespace bc_hashing;
     // Note: packed_fields[0] must never be a padding value and padding can only occur at the last row (i.e. latch = 1).
 
     // Needs to be committed columns as they are used in the lookups
-    pol commit sel_not_padding_1, sel_not_padding_2;
+    pol commit sel_not_padding_1; // @boolean
+    pol commit sel_not_padding_2; // @boolean
     sel_not_padding_1 * (1 - sel_not_padding_1) = 0;
     sel_not_padding_2 * (1 - sel_not_padding_2) = 0;
 

barretenberg/cpp/pil/vm2/bytecode/bc_retrieval.pil

@@ -20,7 +20,7 @@ include "../constants_gen.pil";
 
 namespace bc_retrieval;
 
-pol commit sel;
+pol commit sel; // @boolean
 sel * (1 - sel) = 0;
 
 // No relations will be checked if this identity is satisfied.
@@ -68,7 +68,7 @@ pol commit prev_retrieved_bytecodes_tree_size;
 pol commit next_retrieved_bytecodes_tree_root;
 pol commit next_retrieved_bytecodes_tree_size;
 
-pol commit instance_exists;
+pol commit instance_exists; // @boolean
 instance_exists * (1 - instance_exists) = 0;
 
 #[CONTRACT_INSTANCE_RETRIEVAL]
@@ -86,7 +86,7 @@ sel {
     contract_instance_retrieval.nullifier_tree_root
 };
 
-pol commit no_remaining_bytecodes;
+pol commit no_remaining_bytecodes; // @boolean
 no_remaining_bytecodes * (1 - no_remaining_bytecodes) = 0;
 
 // The tree size is 1 (AVM_RETRIEVED_BYTECODES_TREE_INITIAL_SIZE) + retrieved_bytecodes_count
@@ -97,7 +97,7 @@ pol commit remaining_bytecodes_inv;
 #[NO_REMAINING_BYTECODES]
 sel * (REMAINING_BYTECODES * (no_remaining_bytecodes * (1 - remaining_bytecodes_inv) + remaining_bytecodes_inv) - 1 + no_remaining_bytecodes) = 0;
 
-pol commit is_new_class;
+pol commit is_new_class; // @boolean (by lookup into retrieved_bytecodes_tree_check when instance_exists == 1; constrained to 0 when instance_exists == 0)
 
 #[IS_NEW_CLASS_CHECK]
 instance_exists {
@@ -111,14 +111,14 @@ instance_exists {
 };
 
 // Enforce is_new_class == 0 if the instance does not exist.
-sel * (1 - instance_exists) * is_new_class = 0;
+(1 - instance_exists) * is_new_class = 0;
 
 pol TOO_MANY_BYTECODES = no_remaining_bytecodes * is_new_class;
 
 // We error if instance doesn't exist or if we have too many bytecodes.
 sel * (instance_exists * (1 - TOO_MANY_BYTECODES) - (1 - error)) = 0;
 
-pol commit should_retrieve;
+pol commit should_retrieve; // @boolean (by definition; sel gating enforces zero on non-active rows)
 should_retrieve = sel * (1 - error);
 
 // Observe the following also connects the current_class_id of the instance to the class members.

barretenberg/cpp/pil/vm2/bytecode/class_id_derivation.pil

@@ -6,7 +6,7 @@ include "../precomputed.pil";
 
 namespace class_id_derivation;
 
-    pol commit sel;
+    pol commit sel; // @boolean
     sel * (1 - sel) = 0;
 
     #[skippable_if]

barretenberg/cpp/pil/vm2/bytecode/contract_instance_retrieval.pil

@@ -42,7 +42,7 @@ include "../ff_gt.pil";
  */
 namespace contract_instance_retrieval;
 
-    pol commit sel;
+    pol commit sel; // @boolean
     sel * (1 - sel) = 0;
 
     // No relations will be checked if this identity is satisfied.
@@ -52,7 +52,8 @@ namespace contract_instance_retrieval;
     ////////////////////////////////////////////////////////////////////////////
     // I/O
     pol commit address; // contract address.
-    pol commit exists; // the contract instance exists (its address nullifier exists)
+    pol commit exists; // @boolean the contract instance exists (its address nullifier exists)
+    exists * (1 - exists) = 0;
 
     // address instance members.
     // See barretenberg/cpp/src/barretenberg/vm2/common/aztec_types.hpp
@@ -87,7 +88,8 @@ namespace contract_instance_retrieval;
     sel * (constants.CONTRACT_INSTANCE_REGISTRY_CONTRACT_ADDRESS - deployer_protocol_contract_address) = 0;
 
     // Indicates if the instance belongs to a protocol contract
-    pol commit is_protocol_contract;
+    pol commit is_protocol_contract; // @boolean (by lookup on active rows)
+    // TODO: review safety of is_protocol_contract being underconstrained on inactive rows
 
     // Canonical Addresses can be in the range of 1 <= address <= MAX_PROTOCOL_CONTRACTS
     pol commit max_protocol_contracts;
@@ -123,7 +125,7 @@ namespace contract_instance_retrieval;
 
     // Constrain exists and derived address for non-protocol contracts via nullifier check
 
-    pol commit should_check_nullifier;
+    pol commit should_check_nullifier; // @boolean (by definition)
     // Protocol contracts do not have an address nullifier in the nullifier tree.
     should_check_nullifier = sel * (1 - is_protocol_contract);
 
@@ -193,7 +195,7 @@ namespace contract_instance_retrieval;
 
     // Enforce that the class id provided is the _current_ one (only when nullifier exists)
     // If the address nullifier doesn't exist (which excludes protocol contract instances), there is no need to check!
-    pol commit should_check_for_update;
+    pol commit should_check_for_update; // @boolean (by definition)
     should_check_for_update = should_check_nullifier * exists;
     #[UPDATE_CHECK]
     should_check_for_update {