fix(avm)!: missing input len column into poseidon2 hash start row is (#19971)

Linear issue:
[AVM-213](https://linear.app/aztec-labs/issue/AVM-213/missing-input-len-column-into-poseidon2-hash-start-row-is-not-sound)

Author: jeanmon

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

@@ -39,19 +39,19 @@ namespace address_derivation;
     pol commit partial_address_domain_separator;
     sel * (partial_address_domain_separator - constants.DOM_SEP__PARTIAL_ADDRESS) = 0;
 
-    // TODO: We need these temporarily while we dont allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit const_two;
     sel * (const_two - 2) = 0;
     pol commit const_three;
     sel * (const_three - 3) = 0;
     pol commit const_four;
     sel * (const_four - 4) = 0;
-    pol commit const_five;
-    sel * (const_five - 5) = 0;
+    pol commit const_thirteen;
+    sel * (const_thirteen - 13) = 0;
 
     #[SALTED_INITIALIZATION_HASH_POSEIDON2_0]
-    sel { partial_address_domain_separator, salt, init_hash, salted_init_hash, const_two }
-    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.num_perm_rounds_rem };
+    sel { partial_address_domain_separator, salt, init_hash, salted_init_hash, const_four }
+    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
 
     #[SALTED_INITIALIZATION_HASH_POSEIDON2_1]
     sel { deployer_addr, precomputed.zero, precomputed.zero, salted_init_hash }
@@ -63,8 +63,8 @@ namespace address_derivation;
     pol commit partial_address;
 
     #[PARTIAL_ADDRESS_POSEIDON2]
-    sel { sel /* =1 */, partial_address_domain_separator, class_id, salted_init_hash, partial_address }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    sel { partial_address_domain_separator, class_id, salted_init_hash, partial_address, const_three }
+    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
 
 
     // Hash the public keys
@@ -78,8 +78,8 @@ namespace address_derivation;
     // Remove all the 0s for is_infinite when removed from public_keys.nr
     // https://github.com/AztecProtocol/aztec-packages/issues/7529
     #[PUBLIC_KEYS_HASH_POSEIDON2_0]
-    sel { public_keys_hash_domain_separator, nullifier_key_x, nullifier_key_y, public_keys_hash, const_five }
-    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.num_perm_rounds_rem };
+    sel { public_keys_hash_domain_separator, nullifier_key_x, nullifier_key_y, public_keys_hash, const_thirteen }
+    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
 
     #[PUBLIC_KEYS_HASH_POSEIDON2_1]
     sel { precomputed.zero, incoming_viewing_key_x, incoming_viewing_key_y, public_keys_hash, const_four }
@@ -107,8 +107,8 @@ namespace address_derivation;
     sel * (preaddress_domain_separator - constants.DOM_SEP__CONTRACT_ADDRESS_V1) = 0;
 
     #[PREADDRESS_POSEIDON2]
-    sel { sel /* =1 */, preaddress_domain_separator, public_keys_hash, partial_address, preaddress }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    sel { preaddress_domain_separator, public_keys_hash, partial_address, preaddress, const_three }
+    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
 
 
     // Derive preaddress public key

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

@@ -23,13 +23,13 @@ namespace class_id_derivation;
     // TODO: We need these temporarily while we dont allow for aliases in the lookup tuple.
     pol commit gen_index_contract_class_id;
     sel * (gen_index_contract_class_id - constants.DOM_SEP__CONTRACT_CLASS_ID) = 0;
-    pol commit const_two;
-    sel * (const_two - 2) = 0;
+    pol commit const_four;
+    sel * (const_four - 4) = 0;
 
     // Since the inputs to poseidon2 have to be chunks of 3, we need two lookups if we want to do this in a single row
     #[CLASS_ID_POSEIDON2_0]
-    sel { gen_index_contract_class_id, artifact_hash, private_functions_root, class_id, const_two }
-    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.num_perm_rounds_rem };
+    sel { gen_index_contract_class_id, artifact_hash, private_functions_root, class_id, const_four }
+    in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
 
     #[CLASS_ID_POSEIDON2_1]
     sel { public_bytecode_commitment, precomputed.zero, precomputed.zero, class_id }

barretenberg/cpp/pil/vm2/bytecode/update_check.pil

@@ -41,7 +41,7 @@ namespace update_check;
     pol commit timestamp;
 
     // Get timestamp from public inputs
-    // TODO: Remove this as a column when we can lookup with constants
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit timestamp_pi_offset;
     timestamp_pi_offset = sel * constants.AVM_PUBLIC_INPUTS_GLOBAL_VARIABLES_TIMESTAMP_ROW_IDX;
     #[TIMESTAMP_FROM_PUBLIC_INPUTS]
@@ -54,20 +54,27 @@ namespace update_check;
     // ======== DELAYED PUBLIC MUTABLE HASH READ ========
 
     pol commit update_hash;
-    // TODO: Remove this as a column when we can lookup with constants
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit updated_class_ids_slot;
     sel * (constants.UPDATED_CLASS_IDS_SLOT - updated_class_ids_slot) = 0;
+    pol commit const_two;
+    sel * (const_two - 2) = 0;
 
     pol commit delayed_public_mutable_slot;
 
     #[DELAYED_PUBLIC_MUTABLE_SLOT_POSEIDON2]
-    sel { sel /* =1 */, updated_class_ids_slot, address, precomputed.zero, delayed_public_mutable_slot }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    sel {
+         updated_class_ids_slot, address, precomputed.zero,
+         delayed_public_mutable_slot, const_two
+    } in poseidon2_hash.start {
+         poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+         poseidon2_hash.output, poseidon2_hash.input_len
+    };
 
     pol commit delayed_public_mutable_hash_slot;
     sel * (delayed_public_mutable_slot + constants.UPDATES_DELAYED_PUBLIC_MUTABLE_VALUES_LEN - delayed_public_mutable_hash_slot) = 0;
 
-    // TODO: Remove this as a column when we can lookup with constants
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit deployer_protocol_contract_address;
     sel * (constants.CONTRACT_INSTANCE_REGISTRY_CONTRACT_ADDRESS - deployer_protocol_contract_address) = 0;
 
@@ -103,9 +110,18 @@ namespace update_check;
     pol commit update_preimage_pre_class_id;
     pol commit update_preimage_post_class_id;
 
+    // Lookup constant support: Can be removed when we support constants in lookups.
+    pol commit const_three;
+    sel * (const_three - 3) = 0;
+
     #[UPDATE_HASH_POSEIDON2]
-    hash_not_zero { sel /* =1 */, update_preimage_metadata, update_preimage_pre_class_id, update_preimage_post_class_id, update_hash }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    hash_not_zero {
+         update_preimage_metadata, update_preimage_pre_class_id, update_preimage_post_class_id,
+         update_hash, const_three
+    } in poseidon2_hash.start {
+         poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+         poseidon2_hash.output, poseidon2_hash.input_len
+    };
 
     // ======== TIMESTAMP OF CHANGE READ ========
 
@@ -114,10 +130,10 @@ namespace update_check;
     pol commit timestamp_of_change;
     pol commit update_hi_metadata;
     pol TWO_POW_32 = 2**32;
-    // TODO: Remove this as a column when we can lookup with constants
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit update_hi_metadata_bit_size;
     hash_not_zero * (constants.UPDATES_DELAYED_PUBLIC_MUTABLE_METADATA_BIT_SIZE - constants.TIMESTAMP_OF_CHANGE_BIT_SIZE - update_hi_metadata_bit_size) = 0;
-    // TODO: Remove this as a column when we can lookup with constants
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit timestamp_of_change_bit_size; // 32
     hash_not_zero * (constants.TIMESTAMP_OF_CHANGE_BIT_SIZE - timestamp_of_change_bit_size) = 0;
 

barretenberg/cpp/pil/vm2/poseidon2_hash.pil

@@ -4,27 +4,26 @@ include "precomputed.pil";
 /** Performs the poseidon2 full hash
  * === Usage Tips ===
  *    - SINGLE ROW: To constrain the result of a poseidon hash over a single row (i.e. 3 or fewer inputs), lookup the inputs,
- *      output, end (= 1), and start (= 1). This trace constrains that when start = end = 1, we have a single row.
+ *      output, input_len and use destination selector start (= 1). The caller will pass 1,2, or 3 for input_len. This follows
+ *      from the below constraints that `num_perm_rounds_rem == 1` and `end ==1`.
  *
  *      Example (nullifier_check.pil):
- *             should_silo { sel, siloing_separator, address, nullifier, siloed_nullifier }
- *   in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1,
- *                           poseidon2_hash.input_2, poseidon2_hash.output };
+ *             should_silo   { siloing_separator, address, nullifier, siloed_nullifier, const_three }
+ *   in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1,
+ *                           poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
  *
  *    - MULTIPLE ROWS:
  *       - Lookup the inputs and output values for each row.
  *       - Use num_perm_rounds_rem against the decrementing counter to ensure that each round is
  *         computed in the correct order (at end = 1, num_perm_rounds_rem is constrained to be 1 => can equivalently
- *         lookup the end selector for the final row).
- *       - Over multiple rows, lookup the start selector at the expected first row to ensure no extra rows are prepended.
- *         Note that input_len is only constrained at the start row, so it cannot be relied on for intermediate rows.
- *         Pass also `num_perm_rounds_rem` explicitly at the start row. // TODO(AVM-213): Require `input_len` explicitly
- *                                                                      // at the start row.
+ *         lookup the end selector for the final row). This can be omitted at the `start==1` row.
+ *       - Lookup the start selector at the expected first row to ensure no extra rows are prepended.
+ *         Pass `input_len` in the lookup at the start row, so that the IV is correctly computed.
  *
  *      Example (address_derivation.pil):
  *             // First row (removed prefix poseidon2_hash.** in destination tuple for presentation purposes)
- *             sel { public_keys_hash_domain_separator, nullifier_key_x, nullifier_key_y, public_keys_hash, const_five }
- *             in poseidon2_hash.start { input_0, input_1, input_2, output, num_perm_rounds_rem };
+ *             sel { public_keys_hash_domain_separator, nullifier_key_x, nullifier_key_y, public_keys_hash, const_thirteen }
+ *             in poseidon2_hash.start { input_0, input_1, input_2, output, ipnut_len };
  *
  *             sel { precomputed.zero, incoming_viewing_key_x, incoming_viewing_key_y, public_keys_hash, const_four }
  *             in poseidon2_hash.sel { input_0, input_1, input_2, output, num_perm_rounds_rem };
@@ -72,12 +71,27 @@ namespace poseidon2_hash;
     #[skippable_if]
     sel = 0;
 
-    // If the current row is not active, then there are no more active rows after that.
-    // Note that sel cannot be activated in the first row as sel' is defined.
-    // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
-    // the activated rows start from the second row and are contiguous.
+    // == Multi-row Computation Selectors ==
+    // We follow the recipe documented in:
+    // https://hackmd.io/moq6viBpRJeLpWrHAogCZw?view#Contiguous-Multi-Rows-Computation-Trace
+
+    // Start of a poseidon2 computation
+    pol commit start; // @boolean
+    start * (1 - start) = 0;
+    // The last row of hashing for the given input
+    pol commit end; // @boolean
+    end * (1 - end) = 0;
+
+    pol LATCH_CONDITION = end + precomputed.first_row;
+
+    #[SEL_ON_START_OR_END]
+    (start + end) * (1 - sel) = 0;
+
     #[TRACE_CONTINUITY]
-    (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+    (1 - LATCH_CONDITION) * (sel - sel') = 0;
+
+    #[START_AFTER_LATCH]
+    sel' * (start' - LATCH_CONDITION) = 0;
 
     // === Input Values ===
     // Unpadded Length of the inputs to be hashed
@@ -97,25 +111,6 @@ namespace poseidon2_hash;
     // The latch condition (see below for definition) will be on at the first_row (customary pil relations) or when num_perm_rounds_rem - 1 = 0
     (1 - LATCH_CONDITION) * (output' - output) = 0;
 
-    // === Control Flow within Subtrace ===
-    // Start of a poseidon2 computation
-    pol commit start; // @boolean
-    start * (1 - start) = 0;
-    // When we end a poseidon, the next row must naturally have a start
-    sel' * (start' - LATCH_CONDITION) = 0;
-
-    // The last row of hashing for the given input
-    pol commit end; // @boolean
-    end * (1 - end) = 0;
-
-    // Selector must be 1 in end row
-    #[SELECTOR_ON_START_OR_END]
-    (start + end) * (1 - sel) = 0;
-
-    // Our latch condition can either be the designated end of the computation or the first row
-    // The previous relation ensures they cannot both be 1
-    pol LATCH_CONDITION = end + precomputed.first_row;
-
     // === Permutation/Round Counting ===
     // We use the padded length to calculate the num of rounds to perform
     pol commit num_perm_rounds_rem;
@@ -144,6 +139,8 @@ namespace poseidon2_hash;
     // This cannot happen because to satisfy the current subtrace constraints, the attacker must decrement `num_perm_rounds_rem`
     // to `1` which would require ca. 2^250 rows. This implies that we will never reach legitimate `num_perm_rounds_rem` values
     // and that `end == 1` cannot be satisfied for this multi-row invocation.
+    // If we cannot reach `end == 1`, then we cannot satisfy the constraint  #[TRACE_CONTINUITY] on the
+    // last row of the trace.
 
     //=== Output Chaining ===
     // The permutation input values are represented by a_0, a_1, a_2, a_3

barretenberg/cpp/pil/vm2/trees/merkle_check.pil

@@ -198,19 +198,27 @@ namespace merkle_check;
     pol commit read_output_hash;
     pol commit write_output_hash;
 
+    // Lookup constant support: Can be removed when we support constants in lookups.
+    pol commit const_two;
+    sel * (const_two - 2) = 0;
+
     // Lookup to the full poseidon2 gadget
     #[MERKLE_POSEIDON2_READ]
     sel {
-        read_left_node, read_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ sel, read_output_hash
-    } in poseidon2_hash.end {
-        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output
+        read_left_node, read_right_node, /*input_2=*/ precomputed.zero,
+        read_output_hash, const_two
+    } in poseidon2_hash.start {
+        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+        poseidon2_hash.output, poseidon2_hash.input_len
     };
 
     #[MERKLE_POSEIDON2_WRITE]
     write {
-        write_left_node, write_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ write, write_output_hash
-    } in poseidon2_hash.end {
-        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output
+        write_left_node, write_right_node, /*input_2=*/ precomputed.zero,
+        write_output_hash, const_two
+    } in poseidon2_hash.start {
+        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+        poseidon2_hash.output, poseidon2_hash.input_len
     };
 
     // If we are not done, this row's output_hash is the next row's node

barretenberg/cpp/pil/vm2/trees/note_hash_tree_check.pil

@@ -78,14 +78,20 @@ namespace note_hash_tree_check;
     #[PASSTHROUGH_SILOING]
     sel * (1 - should_silo) * (note_hash - siloed_note_hash) = 0;
 
-    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit siloing_separator;
     sel * (constants.DOM_SEP__SILOED_NOTE_HASH - siloing_separator) = 0;
+    pol commit const_three;
+    sel * (const_three - 3) = 0;
 
     #[SILO_POSEIDON2]
-    should_silo { sel, siloing_separator, address, note_hash, siloed_note_hash }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
-
+    should_silo {
+         siloing_separator, address, note_hash,
+         siloed_note_hash, const_three
+    } in poseidon2_hash.start {
+         poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+         poseidon2_hash.output, poseidon2_hash.input_len
+    };
 
     // ====== UNIQUE ======
     // If reading we should pass an already unique note hash
@@ -96,7 +102,7 @@ namespace note_hash_tree_check;
     #[PASSTHROUGH_UNIQUENESS]
     sel * (1 - should_unique) * (siloed_note_hash - unique_note_hash) = 0;
 
-    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit first_nullifier_pi_index;
     sel * (constants.AVM_PUBLIC_INPUTS_PREVIOUS_NON_REVERTIBLE_ACCUMULATED_DATA_NULLIFIERS_ROW_IDX - first_nullifier_pi_index) = 0;
 
@@ -114,21 +120,31 @@ namespace note_hash_tree_check;
 
     pol commit nonce;
 
-    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit nonce_separator;
     sel * (constants.DOM_SEP__NOTE_HASH_NONCE - nonce_separator) = 0;
 
     #[NONCE_COMPUTATION_POSEIDON2]
-    should_unique { sel, nonce_separator, first_nullifier, note_hash_index, nonce }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    should_unique {
+         nonce_separator, first_nullifier, note_hash_index,
+         nonce, const_three
+    } in poseidon2_hash.start {
+         poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+         poseidon2_hash.output, poseidon2_hash.input_len
+    };
 
-    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit unique_note_hash_separator;
     sel * (constants.DOM_SEP__UNIQUE_NOTE_HASH - unique_note_hash_separator) = 0;
 
     #[UNIQUE_NOTE_HASH_POSEIDON2]
-    should_unique { sel, unique_note_hash_separator, nonce, siloed_note_hash, unique_note_hash }
-    in poseidon2_hash.end { poseidon2_hash.start, poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
+    should_unique {
+         unique_note_hash_separator, nonce, siloed_note_hash,
+         unique_note_hash, const_three
+    } in poseidon2_hash.start {
+         poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2,
+         poseidon2_hash.output, poseidon2_hash.input_len
+    };
 
     // ====== TREE CHECK ======
     pol commit prev_leaf_value;
@@ -142,7 +158,7 @@ namespace note_hash_tree_check;
     // If reading, next_leaf_value is unconstrained
     write * (unique_note_hash - next_leaf_value) = 0;
 
-    // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple
+    // Lookup constant support: Can be removed when we support constants in lookups.
     pol commit note_hash_tree_height;
     sel * (constants.NOTE_HASH_TREE_HEIGHT - note_hash_tree_height) = 0;