11include "poseidon2_perm.pil";
2-
3- // Performs the poseidon2 full hash
4- // It is **mostly** well-constrained
5- // === Usage Tips ===
6- // - To constrain the result of a poseidon hash over a single row (i.e. 3 or fewer inputs), lookup the inputs,
7- // output, end (= 1), and start (= 1). This trace constrains that when start = end = 1, we have a single row.
8- // - Over multiple rows, use num_perm_rounds_rem against the decrementing counter to ensure that each round is
9- // computed in the correct order (at end = 1, num_perm_rounds_rem is constrained to be 1 => can equivalently
10- // lookup the end selector for the final row).
11- // - Over multiple rows, lookup the start selector at the expected first row to ensure no extra rows are prepended.
12- // Note that input_len is only constrained at the start row, so it cannot be relied on for intermediate rows.
2+ include "precomputed.pil";
3+
4+ /** Performs the poseidon2 full hash
5+ * === Usage Tips ===
6+ * - SINGLE ROW: To constrain the result of a poseidon hash over a single row (i.e. 3 or fewer inputs), lookup the inputs,
7+ * output, input_len and use destination selector start (= 1). The caller will pass 1,2, or 3 for input_len. This follows
8+ * from the below constraints that `num_perm_rounds_rem == 1` and `end ==1`.
9+ *
10+ * Example (nullifier_check.pil):
11+ * should_silo { siloing_separator, address, nullifier, siloed_nullifier, const_three }
12+ * in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1,
13+ * poseidon2_hash.input_2, poseidon2_hash.output, poseidon2_hash.input_len };
14+ *
15+ * - MULTIPLE ROWS:
16+ * - Lookup the inputs and output values for each row.
17+ * - Use num_perm_rounds_rem against the decrementing counter to ensure that each round is
18+ * computed in the correct order (at end = 1, num_perm_rounds_rem is constrained to be 1 => can equivalently
19+ * lookup the end selector for the final row). This can be omitted at the `start==1` row.
20+ * - Lookup the start selector at the expected first row to ensure no extra rows are prepended.
21+ * Pass `input_len` in the lookup at the start row, so that the IV is correctly computed.
22+ *
23+ * Example (address_derivation.pil):
24+ * // First row (removed prefix poseidon2_hash.** in destination tuple for presentation purposes)
25+ * sel { public_keys_hash_domain_separator, nullifier_key_x, nullifier_key_y, public_keys_hash, const_thirteen }
26+ * in poseidon2_hash.start { input_0, input_1, input_2, output, ipnut_len };
27+ *
28+ * sel { precomputed.zero, incoming_viewing_key_x, incoming_viewing_key_y, public_keys_hash, const_four }
29+ * in poseidon2_hash.sel { input_0, input_1, input_2, output, num_perm_rounds_rem };
30+ * .....
31+ *
32+ * sel { precomputed.zero, precomputed.zero, precomputed.zero, public_keys_hash }
33+ * in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };
34+ *
35+ *
36+ * === Trace Shape ===
37+ * This subtrace is a multi-rows computation. The trace shape is as follows (where `unc` denotes an unconstrained value):
38+ *
39+ * +------+-------+-----+--------+-----------+---------------------+
40+ * | sel | start | end |padding | input_len | num_perm_rounds_rem |
41+ * +------+-------+-----+--------+-----------+---------------------+
42+ * | 1 | 1 | 0 | 2 | 22 | 8 |
43+ * | 1 | 0 | 0 | unc | unc | 7 |
44+ * .................................................................
45+ * | 1 | 1 | 1 | unc | unc | 1 |
46+ * +------+-------+--------------+-----------+---------------------+
47+ *
48+ * The number of rows for a computation is ceil(input_len/3) rows.
49+ *
50+ * No errors are expected in this subtrace.
51+ *
52+ * This subtrace interacts with the poseidon2_perm.pil subtrace and is used by many other subtraces:
53+ * - address_derivation.pil
54+ * - bc_hashing.pil
55+ * - calldata_hashing.pil
56+ * - class_id_derivation.pil
57+ * - merkle_check.pil
58+ * - note_hash_tree_check.pil
59+ * - nullifier_check.pil
60+ * - public_data_check.pil
61+ * - retrieved_bytecodes_tree_check.pil
62+ * - tx.pil
63+ * - update_check.pil
64+ * - written_public_data_slots_tree_check.pil
65+ */
1366namespace poseidon2_hash;
1467
15- pol commit sel;
68+ pol commit sel; // @boolean
1669 sel * (1 - sel) = 0;
1770
1871 #[skippable_if]
1972 sel = 0;
2073
21- // If the current row is not active, then there are no more active rows after that.
22- // Note that sel cannot be activated in the first row as sel' is defined.
23- // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
24- // the activated rows start from the second row and are contiguous.
74+ // == Multi-row Computation Selectors ==
75+ // We follow the recipe documented in:
76+ // https://hackmd.io/moq6viBpRJeLpWrHAogCZw?view#Contiguous-Multi-Rows-Computation-Trace
77+
78+ // Start of a poseidon2 computation
79+ pol commit start; // @boolean
80+ start * (1 - start) = 0;
81+ // The last row of hashing for the given input
82+ pol commit end; // @boolean
83+ end * (1 - end) = 0;
84+
85+ pol LATCH_CONDITION = end + precomputed.first_row;
86+
87+ #[SEL_ON_START_OR_END]
88+ (start + end) * (1 - sel) = 0;
89+
2590 #[TRACE_CONTINUITY]
26- (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
91+ (1 - LATCH_CONDITION) * (sel - sel') = 0;
92+
93+ #[START_AFTER_LATCH]
94+ sel' * (start' - LATCH_CONDITION) = 0;
2795
2896 // === Input Values ===
2997 // Unpadded Length of the inputs to be hashed
@@ -41,26 +109,7 @@ namespace poseidon2_hash;
41109 pol commit output;
42110 // We enforce that the output has to be kept the same per row until we hit the "end" of the computation
43111 // 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
44- sel * (1 - LATCH_CONDITION) * (output' - output) = 0;
45-
46- // === Control Flow within Subtrace ===
47- // Start of a poseidon2 computation
48- pol commit start;
49- start * (1 - start) = 0;
50- // When we end a poseidon, the next row must naturally have a start
51- sel' * (start' - LATCH_CONDITION) = 0;
52-
53- // The last row of hashing for the given input
54- pol commit end;
55- end * (1 - end) = 0;
56-
57- // Selector must be 1 in end row
58- #[SELECTOR_ON_END]
59- end * (1 - sel) = 0;
60-
61- // Our latch condition can either be the designated end of the computation or the first row
62- // The previous relation ensures they cannot both be 1
63- pol LATCH_CONDITION = end + precomputed.first_row;
112+ (1 - LATCH_CONDITION) * (output' - output) = 0;
64113
65114 // === Permutation/Round Counting ===
66115 // We use the padded length to calculate the num of rounds to perform
@@ -69,16 +118,29 @@ namespace poseidon2_hash;
69118 // The amount of padding can be 0, 1 or 2.
70119 // Note the padded values are not enforced to be zero here, the calling function SHOULD enforce this
71120 padding * (padding - 1) * (padding - 2) = 0;
121+
72122 pol PADDED_LEN = input_len + padding;
73123 // Check that the PADDED_LEN = num_rounds * 3 at the start of the computation
74- sel * start * (num_perm_rounds_rem * 3 - PADDED_LEN) = 0;
75- // If we still have rounds to perform, the num_perm_rounds_rem is decremented
124+ start * (num_perm_rounds_rem * 3 - PADDED_LEN) = 0;
125+
126+ // If we still have rounds to perform, `num_perm_rounds_rem` is decremented.
76127 sel * (1 - LATCH_CONDITION) * (num_perm_rounds_rem' - num_perm_rounds_rem + 1) = 0;
77- // Need an additional helper that holds the inverse of the num_perm_rounds_rem;
78- pol commit num_perm_rounds_rem_inv ;
128+ // Need an additional helper that holds the inverse of num_perm_rounds_rem - 1.
129+ pol commit num_perm_rounds_rem_min_one_inv ;
79130 pol NEXT_ROUND_COUNT = num_perm_rounds_rem - 1;
80- // end == 1 when the (num_perm_rounds_rem - 1) == 0
81- sel * (NEXT_ROUND_COUNT * (end * (1 - num_perm_rounds_rem_inv) + num_perm_rounds_rem_inv) - 1 + end) = 0;
131+ // end == 1 <==> (num_perm_rounds_rem - 1) == 0
132+ sel * (NEXT_ROUND_COUNT * (end * (1 - num_perm_rounds_rem_min_one_inv) + num_perm_rounds_rem_min_one_inv) - 1 + end) = 0;
133+
134+ // Prevention of an invalid padding:
135+ // Note that in a finite field, we can always divide by 3. For any padding value (0,1,2), we can set
136+ // `num_perm_rounds_rem := 3^(-1) * PADDED_LEN`. Hence, a malicious prover can set an incorrect padding value,
137+ // setting `padding` so that `PADDED_LEN` is not a multiple of 3 over the integers. If this happens,
138+ // on `start == 1`, `num_perm_rounds_rem` must be huge, i.e., larger than p/3 (more than 250 bits).
139+ // This cannot happen because to satisfy the current subtrace constraints, the attacker must decrement `num_perm_rounds_rem`
140+ // to `1` which would require ca. 2^250 rows. This implies that we will never reach legitimate `num_perm_rounds_rem` values
141+ // and that `end == 1` cannot be satisfied for this multi-row invocation.
142+ // If we cannot reach `end == 1`, then we cannot satisfy the constraint #[TRACE_CONTINUITY] on the
143+ // last row of the trace.
82144
83145 //=== Output Chaining ===
84146 // The permutation input values are represented by a_0, a_1, a_2, a_3
@@ -91,14 +153,14 @@ namespace poseidon2_hash;
91153 pol commit a_2;
92154 pol commit a_3;
93155
94- sel * start * (a_0 - input_0) = 0;
95- sel * (1 - LATCH_CONDITION) * (a_0' - b_0 - input_0') = 0;
96- sel * start * (a_1 - input_1) = 0;
97- sel * (1 - LATCH_CONDITION) * (a_1' - b_1 - input_1') = 0;
98- sel * start * (a_2 - input_2) = 0;
99- sel * (1 - LATCH_CONDITION) * (a_2' - b_2 - input_2') = 0;
100- sel * start * (a_3 - IV) = 0; // IV is placed in the last slot if this is the start
101- sel * (1 - LATCH_CONDITION) * (a_3' - b_3) = 0;
156+ start * (a_0 - input_0) = 0;
157+ (1 - LATCH_CONDITION) * (a_0' - b_0 - input_0') = 0;
158+ start * (a_1 - input_1) = 0;
159+ (1 - LATCH_CONDITION) * (a_1' - b_1 - input_1') = 0;
160+ start * (a_2 - input_2) = 0;
161+ (1 - LATCH_CONDITION) * (a_2' - b_2 - input_2') = 0;
162+ start * (a_3 - IV) = 0; // IV is placed in the last slot if this is the start
163+ (1 - LATCH_CONDITION) * (a_3' - b_3) = 0;
102164
103165 // The Hash output value represented by b_0
104166 pol commit b_0;
@@ -107,7 +169,7 @@ namespace poseidon2_hash;
107169 pol commit b_3;
108170
109171 // The final result of the output of the hash should match the output from the last permutation (b_0)
110- sel * LATCH_CONDITION * (output - b_0) = 0;
172+ end * (output - b_0) = 0;
111173
112174 #[POSEIDON2_PERM]
113175 sel { a_0, a_1, a_2, a_3, b_0, b_1, b_2, b_3 }
0 commit comments