Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
honk_optimized_contract.hpp
Go to the documentation of this file.
1// === AUDIT STATUS ===
2// internal: { status: Planned, auditors: [], commit: }
3// external_1: { status: not started, auditors: [], commit: }
4// external_2: { status: not started, auditors: [], commit: }
5// =====================
6
7#pragma once
9#include <sstream>
10#include <vector>
11
12// Source code for the Ultrahonk Solidity verifier.
13// It's expected that the AcirComposer will inject a library which will load the verification key into memory.
14// NOLINTNEXTLINE(cppcoreguidelines-avoid-c-arrays)
15static const char HONK_CONTRACT_OPT_SOURCE[] = R"(
16// SPDX-License-Identifier: Apache-2.0
17// Copyright 2022 Aztec
18pragma solidity ^0.8.27;
19
20interface IVerifier {
21 function verify(bytes calldata _proof, bytes32[] calldata _publicInputs) external view returns (bool);
22}
23
24
25
26uint256 constant NUMBER_OF_SUBRELATIONS = 31;
27uint256 constant BATCHED_RELATION_PARTIAL_LENGTH = 8;
28uint256 constant ZK_BATCHED_RELATION_PARTIAL_LENGTH = 9;
29uint256 constant NUMBER_OF_ENTITIES = 41;
30uint256 constant NUMBER_UNSHIFTED = 36;
31uint256 constant NUMBER_TO_BE_SHIFTED = 5;
32uint256 constant PAIRING_POINTS_SIZE = 8;
33
34uint256 constant VK_HASH = {{ VK_HASH }};
35uint256 constant CIRCUIT_SIZE = {{ CIRCUIT_SIZE }};
36uint256 constant LOG_N = {{ LOG_CIRCUIT_SIZE }};
37uint256 constant NUMBER_PUBLIC_INPUTS = {{ NUM_PUBLIC_INPUTS }};
38uint256 constant REAL_NUMBER_PUBLIC_INPUTS = {{ REAL_NUM_PUBLIC_INPUTS }};
39uint256 constant PUBLIC_INPUTS_OFFSET = 5; // NUM_DISABLED_ROWS_IN_SUMCHECK + NUM_ZERO_ROWS = 4 + 1
40
41contract HonkVerifier is IVerifier {
42 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
43 /* SLAB ALLOCATION */
44 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
85 // {{ SECTION_START MEMORY_LAYOUT }}
86 // {{ SECTION_END MEMORY_LAYOUT }}
87
88 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
89 /* SUMCHECK - MEMORY ALIASES */
90 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
91 uint256 internal constant EC_X_1 = W2_EVAL_LOC;
92 uint256 internal constant EC_Y_1 = W3_EVAL_LOC;
93 uint256 internal constant EC_X_2 = W1_SHIFT_EVAL_LOC;
94 uint256 internal constant EC_Y_2 = W4_SHIFT_EVAL_LOC;
95 uint256 internal constant EC_Y_3 = W3_SHIFT_EVAL_LOC;
96 uint256 internal constant EC_X_3 = W2_SHIFT_EVAL_LOC;
97
98 // Aliases for selectors (Elliptic curve gadget)
99 uint256 internal constant EC_Q_SIGN = QL_EVAL_LOC;
100 uint256 internal constant EC_Q_IS_DOUBLE = QM_EVAL_LOC;
101
102 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
103 /* CONSTANTS */
104 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
105 uint256 internal constant GRUMPKIN_CURVE_B_PARAMETER_NEGATED = 17; // -(-17)
106
107 // Auxiliary relation constants
108 // In the Non Native Field Arithmetic Relation, large field elements are broken up into 4 LIMBs of 68 `LIMB_SIZE` bits each.
109 uint256 internal constant LIMB_SIZE = 0x100000000000000000; // 1<<68
110
111 // In the Delta Range Check Relation, there is a range checking relation that can validate 14-bit range checks with only 1
112 // extra relation in the execution trace.
113 // For large range checks, we decompose them into a collection of 14-bit range checks.
114 uint256 internal constant SUBLIMB_SHIFT = 0x4000; // 1<<14
115
116 // Poseidon2 internal constants
117 // https://github.com/HorizenLabs/poseidon2/blob/main/poseidon2_rust_params.sage - derivation code
118 uint256 internal constant POS_INTERNAL_MATRIX_D_0 =
119 0x10dc6e9c006ea38b04b1e03b4bd9490c0d03f98929ca1d7fb56821fd19d3b6e7;
120 uint256 internal constant POS_INTERNAL_MATRIX_D_1 =
121 0x0c28145b6a44df3e0149b3d0a30b3bb599df9756d4dd9b84a86b38cfb45a740b;
122 uint256 internal constant POS_INTERNAL_MATRIX_D_2 =
123 0x00544b8338791518b2c7645a50392798b21f75bb60e3596170067d00141cac15;
124 uint256 internal constant POS_INTERNAL_MATRIX_D_3 =
125 0x222c01175718386f2e2e82eb122789e352e105a3b8fa852613bc534433ee428b;
126
127 // Constants inspecting proof components
128 uint256 internal constant NUMBER_OF_UNSHIFTED_ENTITIES = 36;
129 // Shifted columns are columns that are duplicates of existing columns but right-shifted by 1
130 uint256 internal constant NUMBER_OF_SHIFTED_ENTITIES = 5;
131 uint256 internal constant TOTAL_NUMBER_OF_ENTITIES = 41;
132
133 // Constants for performing batch multiplication
134 uint256 internal constant ACCUMULATOR = 0x00;
135 uint256 internal constant ACCUMULATOR_2 = 0x40;
136 uint256 internal constant G1_LOCATION = 0x60;
137 uint256 internal constant G1_Y_LOCATION = 0x80;
138 uint256 internal constant SCALAR_LOCATION = 0xa0;
139
140 // Group order
141 uint256 internal constant Q = 21888242871839275222246405745257275088696311157297823662689037894645226208583; // EC group order
142
143 // Field order constants
144 // -1/2 mod p
145 uint256 internal constant NEG_HALF_MODULO_P = 0x183227397098d014dc2822db40c0ac2e9419f4243cdcb848a1f0fac9f8000000;
146 uint256 internal constant P = 21888242871839275222246405745257275088548364400416034343698204186575808495617;
147 uint256 internal constant P_SUB_1 = 21888242871839275222246405745257275088548364400416034343698204186575808495616;
148 uint256 internal constant P_SUB_2 = 21888242871839275222246405745257275088548364400416034343698204186575808495615;
149 uint256 internal constant P_SUB_3 = 21888242871839275222246405745257275088548364400416034343698204186575808495614;
150
151 // Barycentric evaluation constants
152 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_0 =
153 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593efffec51;
154 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_1 =
155 0x00000000000000000000000000000000000000000000000000000000000002d0;
156 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_2 =
157 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593efffff11;
158 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_3 =
159 0x0000000000000000000000000000000000000000000000000000000000000090;
160 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_4 =
161 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593efffff71;
162 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_5 =
163 0x00000000000000000000000000000000000000000000000000000000000000f0;
164 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_6 =
165 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593effffd31;
166 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_7 =
167 0x00000000000000000000000000000000000000000000000000000000000013b0;
168
169 // Constants for computing public input delta
170 uint256 internal constant PERMUTATION_ARGUMENT_VALUE_SEPARATOR = 1 << 28;
171
172 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
173 /* ERRORS */
174 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
175 // The errors match Errors.sol
176
177 bytes4 internal constant VALUE_GE_LIMB_MAX_SELECTOR = 0xeb73e0bd;
178 bytes4 internal constant VALUE_GE_GROUP_ORDER_SELECTOR = 0x607be13e;
179 bytes4 internal constant VALUE_GE_FIELD_ORDER_SELECTOR = 0x20a33589;
180 bytes4 internal constant SUMCHECK_FAILED_SELECTOR = 0x9fc3a218;
181 bytes4 internal constant SHPLEMINI_FAILED_SELECTOR = 0xa5d82e8a;
182
183 bytes4 internal constant PROOF_LENGTH_WRONG_WITH_LOG_N_SELECTOR = 0x59895a53;
184 bytes4 internal constant PUBLIC_INPUTS_LENGTH_WRONG_SELECTOR = 0xfa066593;
185
186 bytes4 internal constant MODEXP_FAILED_SELECTOR = 0xf442f163;
187
188 constructor() {}
189
190 function verify(
191 bytes calldata,
192 /*proof*/
193 bytes32[] calldata /*public_inputs*/
194 )
195 public
196 view
197 override
198 returns (bool)
199 {
200 // Load the proof from calldata in one large chunk
201 assembly {
202 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
203 /* LOAD VERIFCATION KEY */
204 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
205 // Write the verification key into memory
206 //
207 // Although defined at the top of the file, it is used towards the end of the algorithm when batching in the commitment scheme.
208 function loadVk() {
209 mstore(Q_L_X_LOC, {{ Q_L_X_LOC }})
210 mstore(Q_L_Y_LOC, {{ Q_L_Y_LOC }})
211 mstore(Q_R_X_LOC, {{ Q_R_X_LOC }})
212 mstore(Q_R_Y_LOC, {{ Q_R_Y_LOC }})
213 mstore(Q_O_X_LOC, {{ Q_O_X_LOC }})
214 mstore(Q_O_Y_LOC, {{ Q_O_Y_LOC }})
215 mstore(Q_4_X_LOC, {{ Q_4_X_LOC }})
216 mstore(Q_4_Y_LOC, {{ Q_4_Y_LOC }})
217 mstore(Q_M_X_LOC, {{ Q_M_X_LOC }})
218 mstore(Q_M_Y_LOC, {{ Q_M_Y_LOC }})
219 mstore(Q_C_X_LOC, {{ Q_C_X_LOC }})
220 mstore(Q_C_Y_LOC, {{ Q_C_Y_LOC }})
221 mstore(Q_LOOKUP_X_LOC, {{ Q_LOOKUP_X_LOC }})
222 mstore(Q_LOOKUP_Y_LOC, {{ Q_LOOKUP_Y_LOC }})
223 mstore(Q_ARITH_X_LOC, {{ Q_ARITH_X_LOC }})
224 mstore(Q_ARITH_Y_LOC, {{ Q_ARITH_Y_LOC }})
225 mstore(Q_DELTA_RANGE_X_LOC, {{ Q_DELTA_RANGE_X_LOC }})
226 mstore(Q_DELTA_RANGE_Y_LOC, {{ Q_DELTA_RANGE_Y_LOC }})
227 mstore(Q_ELLIPTIC_X_LOC, {{ Q_ELLIPTIC_X_LOC }})
228 mstore(Q_ELLIPTIC_Y_LOC, {{ Q_ELLIPTIC_Y_LOC }})
229 mstore(Q_MEMORY_X_LOC, {{ Q_MEMORY_X_LOC }})
230 mstore(Q_MEMORY_Y_LOC, {{ Q_MEMORY_Y_LOC }})
231 mstore(Q_NNF_X_LOC, {{ Q_NNF_X_LOC }})
232 mstore(Q_NNF_Y_LOC, {{ Q_NNF_Y_LOC }})
233 mstore(Q_POSEIDON_2_EXTERNAL_X_LOC, {{ Q_POSEIDON_2_EXTERNAL_X_LOC }})
234 mstore(Q_POSEIDON_2_EXTERNAL_Y_LOC, {{ Q_POSEIDON_2_EXTERNAL_Y_LOC }})
235 mstore(Q_POSEIDON_2_INTERNAL_X_LOC, {{ Q_POSEIDON_2_INTERNAL_X_LOC }})
236 mstore(Q_POSEIDON_2_INTERNAL_Y_LOC, {{ Q_POSEIDON_2_INTERNAL_Y_LOC }})
237 mstore(SIGMA_1_X_LOC, {{ SIGMA_1_X_LOC }})
238 mstore(SIGMA_1_Y_LOC, {{ SIGMA_1_Y_LOC }})
239 mstore(SIGMA_2_X_LOC, {{ SIGMA_2_X_LOC }})
240 mstore(SIGMA_2_Y_LOC, {{ SIGMA_2_Y_LOC }})
241 mstore(SIGMA_3_X_LOC, {{ SIGMA_3_X_LOC }})
242 mstore(SIGMA_3_Y_LOC, {{ SIGMA_3_Y_LOC }})
243 mstore(SIGMA_4_X_LOC, {{ SIGMA_4_X_LOC }})
244 mstore(SIGMA_4_Y_LOC, {{ SIGMA_4_Y_LOC }})
245 mstore(TABLE_1_X_LOC, {{ TABLE_1_X_LOC }})
246 mstore(TABLE_1_Y_LOC, {{ TABLE_1_Y_LOC }})
247 mstore(TABLE_2_X_LOC, {{ TABLE_2_X_LOC }})
248 mstore(TABLE_2_Y_LOC, {{ TABLE_2_Y_LOC }})
249 mstore(TABLE_3_X_LOC, {{ TABLE_3_X_LOC }})
250 mstore(TABLE_3_Y_LOC, {{ TABLE_3_Y_LOC }})
251 mstore(TABLE_4_X_LOC, {{ TABLE_4_X_LOC }})
252 mstore(TABLE_4_Y_LOC, {{ TABLE_4_Y_LOC }})
253 mstore(ID_1_X_LOC, {{ ID_1_X_LOC }})
254 mstore(ID_1_Y_LOC, {{ ID_1_Y_LOC }})
255 mstore(ID_2_X_LOC, {{ ID_2_X_LOC }})
256 mstore(ID_2_Y_LOC, {{ ID_2_Y_LOC }})
257 mstore(ID_3_X_LOC, {{ ID_3_X_LOC }})
258 mstore(ID_3_Y_LOC, {{ ID_3_Y_LOC }})
259 mstore(ID_4_X_LOC, {{ ID_4_X_LOC }})
260 mstore(ID_4_Y_LOC, {{ ID_4_Y_LOC }})
261 mstore(LAGRANGE_FIRST_X_LOC, {{ LAGRANGE_FIRST_X_LOC }})
262 mstore(LAGRANGE_FIRST_Y_LOC, {{ LAGRANGE_FIRST_Y_LOC }})
263 mstore(LAGRANGE_LAST_X_LOC, {{ LAGRANGE_LAST_X_LOC }})
264 mstore(LAGRANGE_LAST_Y_LOC, {{ LAGRANGE_LAST_Y_LOC }})
265 }
266
267 // Prime field order - placing on the stack
268 let p := P
269
270 {
271 let proof_ptr := add(calldataload(0x04), 0x24)
272
273 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
274 /* VALIDATE INPUT LENGTHS */
275 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
276 // Validate proof byte length matches expected size for this circuit's LOG_N.
277 // Expected = (8*2 + LOG_N*BATCHED_RELATION_PARTIAL_LENGTH + NUMBER_OF_ENTITIES
278 // + (LOG_N-1)*2 + LOG_N + 2*2 + PAIRING_POINTS_SIZE) * 32
279 {
280 let expected_proof_size := mul(
281 add(
282 add(
283 add(16, mul(LOG_N, BATCHED_RELATION_PARTIAL_LENGTH)),
284 add(NUMBER_OF_ENTITIES, mul(sub(LOG_N, 1), 2))
285 ),
286 add(add(LOG_N, 4), PAIRING_POINTS_SIZE)
287 ),
288 32
289 )
290 let proof_length := calldataload(add(calldataload(0x04), 0x04))
291 if iszero(eq(proof_length, expected_proof_size)) {
292 mstore(0x00, PROOF_LENGTH_WRONG_WITH_LOG_N_SELECTOR)
293 mstore(0x04, LOG_N)
294 mstore(0x24, proof_length)
295 mstore(0x44, expected_proof_size)
296 revert(0x00, 0x64)
297 }
298 }
299 // Validate public inputs array length matches expected count.
300 {
301 let pi_count := calldataload(add(calldataload(0x24), 0x04))
302 if iszero(eq(pi_count, REAL_NUMBER_PUBLIC_INPUTS)) {
303 mstore(0x00, PUBLIC_INPUTS_LENGTH_WRONG_SELECTOR)
304 revert(0x00, 0x04)
305 }
306 }
307
308 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
309 /* GENERATE CHALLENGES */
310 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
311 /*
312 * Proof points (affine coordinates) in the proof are in the following format, where offset is
313 * the offset in the entire proof until the first bit of the x coordinate
314 * offset + 0x00: x
315 * offset + 0x20: y
316 */
317
318 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
319 /* GENERATE ETA CHALLENGE */
320 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
321 /* Eta challenge participants
322 * - circuit size
323 * - number of public inputs
324 * - public inputs offset
325 * - w1
326 * - w2
327 * - w3
328 *
329 * Where circuit size, number of public inputs and public inputs offset are all 32 byte values
330 * and w1,w2,w3 are all proof points values
331 */
332
333 mstore(0x00, VK_HASH)
334
335 let public_inputs_start := add(calldataload(0x24), 0x24)
336 let public_inputs_size := mul(REAL_NUMBER_PUBLIC_INPUTS, 0x20)
337
338 // Copy the public inputs into the eta buffer
339 calldatacopy(0x20, public_inputs_start, public_inputs_size)
340
341 // Copy Pairing points into eta buffer
342 let public_inputs_end := add(0x20, public_inputs_size)
343
344 calldatacopy(public_inputs_end, proof_ptr, 0x100)
345
346 // 0x20 * 8 = 0x100 (8 pairing point limbs)
347 // End of public inputs + pairing points
348 calldatacopy(add(0x120, public_inputs_size), add(proof_ptr, 0x100), 0x100)
349
350 // 0x1e0 = 1 * 32 bytes + 3 * 64 bytes for (w1,w2,w3) + 0x100 for pairing points
351 let eta_input_length := add(0x1e0, public_inputs_size)
352
353 // Get eta and rom_logup_gamma, and compute eta powers (eta, eta², eta³)
354 let prev_challenge := mod(keccak256(0x00, eta_input_length), p)
355 let eta := prev_challenge
356 mstore(0x00, prev_challenge)
357 prev_challenge := mod(keccak256(0x00, 0x20), p)
358 mstore(0x00, prev_challenge)
359
360 let eta_two := mulmod(eta, eta, p)
361 let eta_three := mulmod(eta_two, eta, p)
362
363 mstore(ETA_CHALLENGE, eta)
364 mstore(ETA_TWO_CHALLENGE, eta_two)
365 mstore(ETA_THREE_CHALLENGE, eta_three)
366 mstore(ROM_LOGUP_GAMMA_CHALLENGE, prev_challenge)
367
368 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
369 /* LOAD PROOF INTO MEMORY */
370 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
371 // As all of our proof points are written in contiguous parts of memory, we call use a single
372 // calldatacopy to place all of our proof into the correct memory regions
373 // We copy the entire proof into memory as we must hash each proof section for challenge
374 // evaluation
375 // The last item in the proof, and the first item in the proof (pairing point 0)
376 let proof_size := sub(ETA_CHALLENGE, PAIRING_POINT_0_X_0_LOC)
377
378 calldatacopy(PAIRING_POINT_0_X_0_LOC, proof_ptr, proof_size)
379
380 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
381 /* VALIDATE PROOF INPUTS */
382 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
383 // Validate all proof elements are within their expected ranges.
384 // Pairing limbs: lo < 2^136, hi < 2^120. G1 coordinates < Q. Fr elements < P.
385 {
386 let valid := true
387 let lo_limb_max := shl(136, 1)
388 let hi_limb_max := shl(120, 1)
389 let q_mod := Q
390
391 // 1. Pairing limbs: lo < 2^136, hi < 2^120 (4 pairs, stride 0x40)
392 let ptr := PAIRING_POINT_0_X_0_LOC
393 for {} lt(ptr, W_L_X_LOC) { ptr := add(ptr, 0x40) } {
394 valid := and(valid, lt(mload(ptr), lo_limb_max))
395 valid := and(valid, lt(mload(add(ptr, 0x20)), hi_limb_max))
396 }
397 if iszero(valid) {
398 mstore(0x00, VALUE_GE_LIMB_MAX_SELECTOR)
399 revert(0x00, 0x04)
400 }
401
402 // 2. G1 coordinates: each < Q
403 // - Witness commitments: W_L through Z_PERM (16 slots)
404 for { ptr := W_L_X_LOC } lt(ptr, SUMCHECK_UNIVARIATE_0_0_LOC) { ptr := add(ptr, 0x20) } {
405 valid := and(valid, lt(mload(ptr), q_mod))
406 }
407 // - Gemini fold commitments (28 slots)
408 for { ptr := GEMINI_FOLD_UNIVARIATE_0_X_LOC } lt(ptr, GEMINI_A_EVAL_0) { ptr := add(ptr, 0x20) } {
409 valid := and(valid, lt(mload(ptr), q_mod))
410 }
411 // - Shplonk Q + KZG quotient (4 slots)
412 for { ptr := SHPLONK_Q_X_LOC } lt(ptr, ETA_CHALLENGE) { ptr := add(ptr, 0x20) } {
413 valid := and(valid, lt(mload(ptr), q_mod))
414 }
415 if iszero(valid) {
416 mstore(0x00, VALUE_GE_GROUP_ORDER_SELECTOR)
417 revert(0x00, 0x04)
418 }
419
420 // 2b. G1 points: identity (0,0) is accepted.
421 // Polynomial commitments to identically-zero polynomials are
422 // legitimately the identity, and the ecAdd/ecMul precompiles
423 // treat (0,0) as the additive identity per EIP-196. Soundness
424 // against (0,0) substitution for a non-zero commitment is upheld
425 // by sumcheck/Shplemini downstream.
426
427 // 3. Fr elements: each < P
428 // - Sumcheck univariates + evaluations (161 slots)
429 for { ptr := SUMCHECK_UNIVARIATE_0_0_LOC } lt(ptr, GEMINI_FOLD_UNIVARIATE_0_X_LOC) {
430 ptr := add(ptr, 0x20)
431 } {
432 valid := and(valid, lt(mload(ptr), p))
433 }
434 // - Gemini evaluations (15 slots)
435 for { ptr := GEMINI_A_EVAL_0 } lt(ptr, SHPLONK_Q_X_LOC) { ptr := add(ptr, 0x20) } {
436 valid := and(valid, lt(mload(ptr), p))
437 }
438 if iszero(valid) {
439 mstore(0x00, VALUE_GE_FIELD_ORDER_SELECTOR)
440 revert(0x00, 0x04)
441 }
442 }
443
444 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
445 /* GENERATE BETA and GAMMA CHALLENGE */
446 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
447
448 // Generate Beta and Gamma Challenges
449 // - prevChallenge
450 // - LOOKUP_READ_COUNTS
451 // - LOOKUP_READ_TAGS
452 // - W4
453 mcopy(0x20, LOOKUP_READ_COUNTS_X_LOC, 0xc0)
454
455 prev_challenge := mod(keccak256(0x00, 0xe0), p)
456 let beta := prev_challenge
457 mstore(0x00, prev_challenge)
458 prev_challenge := mod(keccak256(0x00, 0x20), p)
459 mstore(0x00, prev_challenge)
460 let gamma := prev_challenge
461
462 mstore(BETA_CHALLENGE, beta)
463 mstore(GAMMA_CHALLENGE, gamma)
464
465 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
466 /* ALPHA CHALLENGES */
467 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
468 // Generate Alpha challenges - non-linearise the gate contributions
469 //
470 // There are 31 total subrelations in this honk relation, we do not need to non linearise the first sub relation.
471 // There are 30 total gate contributions, a gate contribution is analogous to
472 // a custom gate, it is an expression which must evaluate to zero for each
473 // row in the constraint matrix
474 //
475 // If we do not non-linearise sub relations, then sub relations which rely
476 // on the same wire will interact with each other's sums.
477
478 mcopy(0x20, LOOKUP_INVERSES_X_LOC, 0x80)
479
480 prev_challenge := mod(keccak256(0x00, 0xa0), p)
481 mstore(0x00, prev_challenge)
482 let alpha := prev_challenge
483 mstore(ALPHA_CHALLENGE_0, alpha)
484
485 // Compute powers of alpha: alpha^2, alpha^3, ..., alpha^30
486 let alpha_off_set := ALPHA_CHALLENGE_1
487 for {} lt(alpha_off_set, add(ALPHA_CHALLENGE_29, 0x20)) {} {
488 let prev_alpha := mload(sub(alpha_off_set, 0x20))
489 mstore(alpha_off_set, mulmod(prev_alpha, alpha, p))
490 alpha_off_set := add(alpha_off_set, 0x20)
491 }
492
493 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
494 /* GATE CHALLENGES */
495 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
496
497 // Store the first gate challenge
498 prev_challenge := mod(keccak256(0x00, 0x20), p)
499 mstore(0x00, prev_challenge)
500 let gate_challenge := prev_challenge
501 mstore(GATE_CHALLENGE_0, gate_challenge)
502
503 let gate_off := GATE_CHALLENGE_1
504 for {} lt(gate_off, SUM_U_CHALLENGE_0) {} {
505 let prev := mload(sub(gate_off, 0x20))
506
507 mstore(gate_off, mulmod(prev, prev, p))
508 gate_off := add(gate_off, 0x20)
509 }
510
511 // Sumcheck Univariate challenges
512 // The algebraic relations of the Honk protocol are max degree-7.
513 // To prove satifiability, we multiply the relation by a random (POW) polynomial. We do this as we want all of our relations
514 // to be zero on every row - not for the sum of the relations to be zero. (Which is all sumcheck can do without this modification)
515 //
516 // As a result, in every round of sumcheck, the prover sends an degree-8 univariate polynomial.
517 // The sumcheck univariate challenge produces a challenge for each round of sumcheck, hashing the prev_challenge with
518 // a hash of the degree 8 univariate polynomial provided by the prover.
519 //
520 // 8 points are sent as it is enough to uniquely identify the polynomial
521 let read_off := SUMCHECK_UNIVARIATE_0_0_LOC
522 let write_off := SUM_U_CHALLENGE_0
523 for {} lt(read_off, SIGMA1_EVAL_LOC) {} {
524 // Increase by 20 * batched relation length (8)
525 // 0x20 * 0x8 = 0x100
526 mcopy(0x20, read_off, 0x100)
527
528 // Hash 0x100 + 0x20 (prev hash) = 0x120
529 prev_challenge := mod(keccak256(0x00, 0x120), p)
530 mstore(0x00, prev_challenge)
531
532 let sumcheck_u_challenge := prev_challenge
533 mstore(write_off, sumcheck_u_challenge)
534
535 // Progress read / write pointers
536 read_off := add(read_off, 0x100)
537 write_off := add(write_off, 0x20)
538 }
539
540 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
541 /* RHO CHALLENGES */
542 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
543 // The RHO challenge is the hash of the evaluations of all of the wire values
544 // As per usual, it includes the previous challenge
545 // Evaluations of the following wires and their shifts (for relevant wires):
546 // - QM
547 // - QC
548 // - Q1 (QL)
549 // - Q2 (QR)
550 // - Q3 (QO)
551 // - Q4
552 // - QLOOKUP
553 // - QARITH
554 // - QRANGE
555 // - QELLIPTIC
556 // - QMEMORY
557 // - QNNF (NNF = Non Native Field)
558 // - QPOSEIDON2_EXTERNAL
559 // - QPOSEIDON2_INTERNAL
560 // - SIGMA1
561 // - SIGMA2
562 // - SIGMA3
563 // - SIGMA4
564 // - ID1
565 // - ID2
566 // - ID3
567 // - ID4
568 // - TABLE1
569 // - TABLE2
570 // - TABLE3
571 // - TABLE4
572 // - W1 (WL)
573 // - W2 (WR)
574 // - W3 (WO)
575 // - W4
576 // - Z_PERM
577 // - LOOKUP_INVERSES
578 // - LOOKUP_READ_COUNTS
579 // - LOOKUP_READ_TAGS
580 // - W1_SHIFT
581 // - W2_SHIFT
582 // - W3_SHIFT
583 // - W4_SHIFT
584 // - Z_PERM_SHIFT
585 //
586 // Hash of all of the above evaluations
587 // Number of bytes to copy = 0x20 * NUMBER_OF_ENTITIES (41) = 0x520
588 mcopy(0x20, SIGMA1_EVAL_LOC, 0x520)
589 prev_challenge := mod(keccak256(0x00, 0x540), p)
590 mstore(0x00, prev_challenge)
591
592 let rho := prev_challenge
593
594 mstore(RHO_CHALLENGE, rho)
595
596 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
597 /* GEMINI R CHALLENGE */
598 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
599 // The Gemini R challenge contains a of all of commitments to all of the univariates
600 // evaluated in the Gemini Protocol
601 // So for multivariate polynomials in l variables, we will hash l - 1 commitments.
602 // For this implementation, we have logN number of of rounds and thus logN - 1 committments
603 // The format of these commitments are proof points, which are explained above
604 // 0x40 * (logN - 1)
605
606 mcopy(0x20, GEMINI_FOLD_UNIVARIATE_0_X_LOC, {{ GEMINI_FOLD_UNIVARIATE_LENGTH }})
607
608 prev_challenge := mod(keccak256(0x00, {{ GEMINI_FOLD_UNIVARIATE_HASH_LENGTH }}), p)
609 mstore(0x00, prev_challenge)
610
611 let geminiR := prev_challenge
612
613 mstore(GEMINI_R_CHALLENGE, geminiR)
614
615 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
616 /* SHPLONK NU CHALLENGE */
617 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
618 // The shplonk nu challenge hashes the evaluations of the above gemini univariates
619 // 0x20 * logN = 0x20 * 15 = 0x1e0
620
621 mcopy(0x20, GEMINI_A_EVAL_0, {{ GEMINI_EVALS_LENGTH }})
622 prev_challenge := mod(keccak256(0x00, {{ GEMINI_EVALS_HASH_LENGTH }}), p)
623 mstore(0x00, prev_challenge)
624
625 let shplonkNu := prev_challenge
626 mstore(SHPLONK_NU_CHALLENGE, shplonkNu)
627
628 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
629 /* SHPLONK Z CHALLENGE */
630 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
631 // Generate Shplonk Z
632 // Hash of the single shplonk Q commitment
633 mcopy(0x20, SHPLONK_Q_X_LOC, 0x40)
634 prev_challenge := mod(keccak256(0x00, 0x60), p)
635
636 let shplonkZ := prev_challenge
637 mstore(SHPLONK_Z_CHALLENGE, shplonkZ)
638
639 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
640 /* CHALLENGES COMPLETE */
641 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
642 }
643
644 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
645 /* PUBLIC INPUT DELTA */
646 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
675 {
676 let beta := mload(BETA_CHALLENGE)
677 let gamma := mload(GAMMA_CHALLENGE)
678 let pub_off := PUBLIC_INPUTS_OFFSET
679
680 let numerator_value := 1
681 let denominator_value := 1
682
683 let p_clone := p // move p to the front of the stack
684
685 // Assume offset is less than p
686 // numerator_acc = gamma + (beta * (PERMUTATION_ARGUMENT_VALUE_SEPARATOR + offset))
687 let numerator_acc :=
688 addmod(gamma, mulmod(beta, add(PERMUTATION_ARGUMENT_VALUE_SEPARATOR, pub_off), p_clone), p_clone)
689 // denominator_acc = gamma - (beta * (offset + 1))
690 let beta_x_off := mulmod(beta, add(pub_off, 1), p_clone)
691 let denominator_acc := addmod(gamma, sub(p_clone, beta_x_off), p_clone)
692
693 let valid_inputs := true
694 // Load the starting point of the public inputs (jump over the selector and the length of public inputs [0x24])
695 let public_inputs_ptr := add(calldataload(0x24), 0x24)
696
697 // endpoint_ptr = public_inputs_ptr + num_inputs * 0x20. // every public input is 0x20 bytes
698 let endpoint_ptr := add(public_inputs_ptr, mul(REAL_NUMBER_PUBLIC_INPUTS, 0x20))
699
700 for {} lt(public_inputs_ptr, endpoint_ptr) { public_inputs_ptr := add(public_inputs_ptr, 0x20) } {
701 // Get public inputs from calldata
702 let input := calldataload(public_inputs_ptr)
703
704 valid_inputs := and(valid_inputs, lt(input, p_clone))
705
706 numerator_value := mulmod(numerator_value, addmod(numerator_acc, input, p_clone), p_clone)
707 denominator_value := mulmod(denominator_value, addmod(denominator_acc, input, p_clone), p_clone)
708
709 numerator_acc := addmod(numerator_acc, beta, p_clone)
710 denominator_acc := addmod(denominator_acc, sub(p_clone, beta), p_clone)
711 }
712
713 // Revert if not all public inputs are field elements (i.e. < p)
714 if iszero(valid_inputs) {
715 mstore(0x00, VALUE_GE_FIELD_ORDER_SELECTOR)
716 revert(0x00, 0x04)
717 }
718
719 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
720 /* PUBLIC INPUT DELTA - Pairing points accum */
721 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
722 // Pairing points contribution to public inputs delta
723 let pairing_points_ptr := PAIRING_POINT_0_X_0_LOC
724 for {} lt(pairing_points_ptr, W_L_X_LOC) { pairing_points_ptr := add(pairing_points_ptr, 0x20) } {
725 let input := mload(pairing_points_ptr)
726
727 numerator_value := mulmod(numerator_value, addmod(numerator_acc, input, p_clone), p_clone)
728 denominator_value := mulmod(denominator_value, addmod(denominator_acc, input, p_clone), p_clone)
729
730 numerator_acc := addmod(numerator_acc, beta, p_clone)
731 denominator_acc := addmod(denominator_acc, sub(p_clone, beta), p_clone)
732 }
733
734 mstore(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE, numerator_value)
735 mstore(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE, denominator_value)
736
737 // PI delta denominator inversion is deferred to the barycentric
738 // batch inversion below.
739 }
740 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
741 /* PUBLIC INPUT DELTA - complete */
742 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
743
744 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
745 /* SUMCHECK */
746 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
747 //
748 // Sumcheck is used to prove that every relation 0 on each row of the witness.
749 //
750 // Given each of the columns of our trace is a multilinear polynomial 𝑃1,…,𝑃𝑁∈𝔽[𝑋0,…,𝑋𝑑−1]. We run sumcheck over the polynomial
751 //
752 // 𝐹̃ (𝑋0,…,𝑋𝑑−1)=𝑝𝑜𝑤𝛽(𝑋0,…,𝑋𝑑−1)⋅𝐹(𝑃1(𝑋0,…,𝑋𝑑−1),…,𝑃𝑁(𝑋0,…,𝑋𝑑−1))
753 //
754 // The Pow polynomial is a random polynomial that allows us to ceritify that the relations sum to 0 on each row of the witness,
755 // rather than the entire sum just targeting 0.
756 //
757 // Each polynomial P in our implementation are the polys in the proof and the verification key. (W_1, W_2, W_3, W_4, Z_PERM, etc....)
758 //
759 // We start with a LOG_N variate multilinear polynomial, each round fixes a variable to a challenge value.
760 // Each round the prover sends a round univariate poly, since the degree of our honk relations is 7 + the pow polynomial the prover
761 // sends a degree-8 univariate on each round.
762 // This is sent efficiently by sending 8 values, enough to represent a unique polynomial.
763 // Barycentric evaluation is used to evaluate the polynomial at any point on the domain, given these 8 unique points.
764 //
765 // In the sumcheck protocol, the target sum for each round is the sum of the round univariate evaluated on 0 and 1.
766 // 𝜎𝑖=?𝑆̃ 𝑖(0)+𝑆̃ 𝑖(1)
767 // This is efficiently checked as S(0) and S(1) are sent by the prover as values of the round univariate.
768 //
769 // We compute the next challenge by evaluating the round univariate at a random challenge value.
770 // 𝜎𝑖+1←𝑆̃ 𝑖(𝑢𝑖)
771 // This evaluation is performed via barycentric evaluation.
772 //
773 // Once we have reduced the multilinear polynomials into single dimensional polys, we check the entire sumcheck relation matches the target sum.
774 //
775 // Below this is composed of 8 relations:
776 // 1. Arithmetic relation - constrains arithmetic
777 // 2. Permutaiton Relation - efficiently encodes copy constraints
778 // 3. Log Derivative Lookup Relation - used for lookup operations
779 // 4. Delta Range Relation - used for efficient range checks
780 // 5. Memory Relation - used for efficient memory operations
781 // 6. NNF Relation - used for efficient Non Native Field operations
782 // 7. Poseidon2 External Relation - used for efficient in-circuit hashing
783 // 8. Poseidon2 Internal Relation - used for efficient in-circuit hashing
784 //
785 // These are batched together and evaluated at the same time using the alpha challenges.
786 //
787 {
788 // We write the barycentric domain values into memory
789 // These are written once per program execution, and reused across all
790 // sumcheck rounds
791 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_0_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_0)
792 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_1_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_1)
793 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_2_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_2)
794 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_3_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_3)
795 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_4_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_4)
796 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_5_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_5)
797 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_6_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_6)
798 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_7_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_7)
799
800 // Compute the target sums for each round of sumcheck
801 {
802 // This requires the barycentric inverses to be computed for each round
803 // Write all of the non inverted barycentric denominators into memory
804 let accumulator := 1
805 let temp := FOLD_POS_EVALUATIONS_{{ LOG_N_MINUS_ONE }}_LOC // we use fold pos evaluations as we add 0x20 immediately to get to `BARYCENTRIC_TEMP_0_LOC`
806 let bary_centric_inverses_off := BARYCENTRIC_DENOMINATOR_INVERSES_0_0_LOC
807 {
808 let round_challenge_off := SUM_U_CHALLENGE_0
809 for { let round := 0 } lt(round, LOG_N) { round := add(round, 1) } {
810 let round_challenge := mload(round_challenge_off)
811 let bary_lagrange_denominator_off := BARYCENTRIC_LAGRANGE_DENOMINATOR_0_LOC
812
813 // Unrolled as this loop as it only has 8 iterations - somehow this saves >10k gas
814 {
815 let bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
816 let pre_inv :=
817 mulmod(
818 bary_lagrange_denominator,
819 addmod(round_challenge, p, p), // sub(p, 0) = p
820 p
821 )
822 mstore(bary_centric_inverses_off, pre_inv)
823 temp := add(temp, 0x20)
824 mstore(temp, accumulator)
825 accumulator := mulmod(accumulator, pre_inv, p)
826
827 // increase offsets
828 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
829 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
830
831 // barycentric_index = 1
832 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
833 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 1), p), p)
834 mstore(bary_centric_inverses_off, pre_inv)
835 temp := add(temp, 0x20)
836 mstore(temp, accumulator)
837 accumulator := mulmod(accumulator, pre_inv, p)
838
839 // increase offsets
840 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
841 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
842
843 // barycentric_index = 2
844 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
845 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 2), p), p)
846 mstore(bary_centric_inverses_off, pre_inv)
847 temp := add(temp, 0x20)
848 mstore(temp, accumulator)
849 accumulator := mulmod(accumulator, pre_inv, p)
850
851 // increase offsets
852 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
853 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
854
855 // barycentric_index = 3
856 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
857 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 3), p), p)
858 mstore(bary_centric_inverses_off, pre_inv)
859 temp := add(temp, 0x20)
860 mstore(temp, accumulator)
861 accumulator := mulmod(accumulator, pre_inv, p)
862
863 // increase offsets
864 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
865 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
866
867 // barycentric_index = 4
868 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
869 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 4), p), p)
870 mstore(bary_centric_inverses_off, pre_inv)
871 temp := add(temp, 0x20)
872 mstore(temp, accumulator)
873 accumulator := mulmod(accumulator, pre_inv, p)
874
875 // increase offsets
876 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
877 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
878
879 // barycentric_index = 5
880 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
881 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 5), p), p)
882 mstore(bary_centric_inverses_off, pre_inv)
883 temp := add(temp, 0x20)
884 mstore(temp, accumulator)
885 accumulator := mulmod(accumulator, pre_inv, p)
886
887 // increase offsets
888 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
889 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
890
891 // barycentric_index = 6
892 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
893 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 6), p), p)
894 mstore(bary_centric_inverses_off, pre_inv)
895 temp := add(temp, 0x20)
896 mstore(temp, accumulator)
897 accumulator := mulmod(accumulator, pre_inv, p)
898
899 // increase offsets
900 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
901 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
902
903 // barycentric_index = 7
904 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
905 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 7), p), p)
906 mstore(bary_centric_inverses_off, pre_inv)
907 temp := add(temp, 0x20)
908 mstore(temp, accumulator)
909 accumulator := mulmod(accumulator, pre_inv, p)
910
911 // increase offsets
912 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
913 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
914 }
915 round_challenge_off := add(round_challenge_off, 0x20)
916 }
917 }
918
919 // Append PI delta denominator to the batch inversion
920 {
921 let pi_denom := mload(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE)
922 mstore(PUBLIC_INPUTS_DENOM_TEMP_LOC, accumulator)
923 accumulator := mulmod(accumulator, pi_denom, p)
924 }
925
926 // --- Phase 2: Shplemini forward pass ---
927 // Compute shplemini denominators and accumulate into the running product.
928 // Pre-inversion values stored in shplemini runtime memory
929 {
930 // Compute powers of evaluation challenge: gemini_r^{2^i}
931 let cache := mload(GEMINI_R_CHALLENGE)
932 mstore(POWERS_OF_EVALUATION_CHALLENGE_0_LOC, cache)
935
936 // Element 0: gemini_r (seed)
937 {
938 let val := mload(GEMINI_R_CHALLENGE)
939 mstore(GEMINI_R_INV_TEMP_LOC, accumulator)
940 accumulator := mulmod(accumulator, val, p)
941 }
942
943 // Elements 1..LOG_N: INVERTED_CHALLENGE_POW_MINUS_U
946
947 // Invert all elements (barycentric + PI delta + shplemini) as a single batch
948 {
949 {
950 mstore(0, 0x20)
951 mstore(0x20, 0x20)
952 mstore(0x40, 0x20)
953 mstore(0x60, accumulator)
954 mstore(0x80, P_SUB_2)
955 mstore(0xa0, p)
956 if iszero(staticcall(gas(), 0x05, 0x00, 0xc0, 0x00, 0x20)) {
957 mstore(0x00, MODEXP_FAILED_SELECTOR)
958 revert(0x00, 0x04)
959 }
960
961 accumulator := mload(0x00)
962 if iszero(accumulator) {
963 mstore(0x00, MODEXP_FAILED_SELECTOR)
964 revert(0x00, 0x04)
965 }
966 }
967
968 // --- Shplemini backward pass ---
969 // Extract shplemini inverses in strict reverse order.
972
973 // gemini_r inverse (staging[0])
974 {
975 let tmp := mulmod(accumulator, mload(GEMINI_R_INV_TEMP_LOC), p)
976 accumulator := mulmod(accumulator, mload(GEMINI_R_CHALLENGE), p)
977 mstore(GEMINI_R_INV_LOC, tmp) // 1/gemini_r at staging[0]
978 }
979 }
980
981 // Extract PI delta denominator inverse from the batch
982 {
983 let pi_delta_inv := mulmod(accumulator, mload(PUBLIC_INPUTS_DENOM_TEMP_LOC), p)
984 accumulator := mulmod(accumulator, mload(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE), p)
985
986 // Finalize: public_inputs_delta = numerator * (1/denominator)
987 mstore(
988 PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE,
989 mulmod(mload(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE), pi_delta_inv, p)
990 )
991 }
992
993 // Normalise as last loop will have incremented the offset
994 bary_centric_inverses_off := sub(bary_centric_inverses_off, 0x20)
995 for {} gt(bary_centric_inverses_off, BARYCENTRIC_LAGRANGE_DENOMINATOR_7_LOC) {
996 bary_centric_inverses_off := sub(bary_centric_inverses_off, 0x20)
997 } {
998 let tmp := mulmod(accumulator, mload(temp), p)
999 accumulator := mulmod(accumulator, mload(bary_centric_inverses_off), p)
1000 mstore(bary_centric_inverses_off, tmp)
1001
1002 temp := sub(temp, 0x20)
1003 }
1004 }
1005 }
1006
1007 let valid := true
1008 let round_target := 0
1009 let pow_partial_evaluation := 1
1010 let gate_challenge_off := GATE_CHALLENGE_0
1011 let round_univariates_off := SUMCHECK_UNIVARIATE_0_0_LOC
1012
1013 let challenge_off := SUM_U_CHALLENGE_0
1014 let bary_inverses_off := BARYCENTRIC_DENOMINATOR_INVERSES_0_0_LOC
1015
1016 for { let round := 0 } lt(round, LOG_N) { round := add(round, 1) } {
1017 let round_challenge := mload(challenge_off)
1018
1019 // Total sum = u[0] + u[1]
1020 let total_sum := addmod(mload(round_univariates_off), mload(add(round_univariates_off, 0x20)), p)
1021 valid := and(valid, eq(total_sum, round_target))
1022
1023 // Compute next target sum
1024 let numerator_value := round_challenge
1025 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 1), p), p)
1026 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 2), p), p)
1027 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 3), p), p)
1028 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 4), p), p)
1029 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 5), p), p)
1030 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 6), p), p)
1031 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 7), p), p)
1032
1033 // // Compute the next round target
1034 round_target := 0
1035 for { let i := 0 } lt(i, BATCHED_RELATION_PARTIAL_LENGTH) { i := add(i, 1) } {
1036 let term := mload(round_univariates_off)
1037 let inverse := mload(bary_inverses_off)
1038
1039 term := mulmod(term, inverse, p)
1040 round_target := addmod(round_target, term, p)
1041 round_univariates_off := add(round_univariates_off, 0x20)
1042 bary_inverses_off := add(bary_inverses_off, 0x20)
1043 }
1044
1045 round_target := mulmod(round_target, numerator_value, p)
1046
1047 // Partially evaluate POW
1048 let gate_challenge := mload(gate_challenge_off)
1049 let gate_challenge_minus_one := addmod(gate_challenge, sub(p, 1), p)
1050
1051 let univariate_evaluation := addmod(1, mulmod(round_challenge, gate_challenge_minus_one, p), p)
1052
1053 pow_partial_evaluation := mulmod(pow_partial_evaluation, univariate_evaluation, p)
1054
1055 gate_challenge_off := add(gate_challenge_off, 0x20)
1056 challenge_off := add(challenge_off, 0x20)
1057 }
1058
1059 if iszero(valid) {
1060 mstore(0x00, SUMCHECK_FAILED_SELECTOR)
1061 revert(0x00, 0x04)
1062 }
1063
1064 // The final sumcheck round; accumulating evaluations
1065 // Uses pow partial evaluation as the gate scaling factor
1066
1067 mstore(POW_PARTIAL_EVALUATION_LOC, pow_partial_evaluation)
1068 mstore(FINAL_ROUND_TARGET_LOC, round_target)
1069
1070 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1071 /* ARITHMETIC RELATION */
1072 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1073 {
1109 let w1q1 := mulmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
1110 let w2q2 := mulmod(mload(W2_EVAL_LOC), mload(QR_EVAL_LOC), p)
1111 let w3q3 := mulmod(mload(W3_EVAL_LOC), mload(QO_EVAL_LOC), p)
1112 let w4q3 := mulmod(mload(W4_EVAL_LOC), mload(Q4_EVAL_LOC), p)
1113
1114 let q_arith := mload(QARITH_EVAL_LOC)
1115 // w1w2qm := (w_1 . w_2 . q_m . (QARITH_EVAL_LOC - 3)) / 2
1116 let w1w2qm :=
1117 mulmod(
1118 mulmod(
1119 mulmod(mulmod(mload(W1_EVAL_LOC), mload(W2_EVAL_LOC), p), mload(QM_EVAL_LOC), p),
1120 addmod(q_arith, sub(p, 3), p),
1121 p
1122 ),
1123 NEG_HALF_MODULO_P,
1124 p
1125 )
1126
1127 // (w_1 . w_2 . q_m . (q_arith - 3)) / -2) + (w_1 . q_1) + (w_2 . q_2) + (w_3 . q_3) + (w_4 . q_4) + q_c
1128 let identity :=
1129 addmod(
1130 mload(QC_EVAL_LOC),
1131 addmod(w4q3, addmod(w3q3, addmod(w2q2, addmod(w1q1, w1w2qm, p), p), p), p),
1132 p
1133 )
1134
1135 // if q_arith == 3 we evaluate an additional mini addition gate (on top of the regular one), where:
1136 // w_1 + w_4 - w_1_omega + q_m = 0
1137 // we use this gate to save an addition gate when adding or subtracting non-native field elements
1138 // α * (q_arith - 2) * (w_1 + w_4 - w_1_omega + q_m)
1139 let extra_small_addition_gate_identity :=
1140 mulmod(
1141 addmod(q_arith, sub(p, 2), p),
1142 addmod(
1143 mload(QM_EVAL_LOC),
1144 addmod(
1145 sub(p, mload(W1_SHIFT_EVAL_LOC)),
1146 addmod(mload(W1_EVAL_LOC), mload(W4_EVAL_LOC), p),
1147 p
1148 ),
1149 p
1150 ),
1151 p
1152 )
1153
1154 // Split up the two relations
1155 let contribution_0 :=
1156 addmod(identity, mulmod(addmod(q_arith, sub(p, 1), p), mload(W4_SHIFT_EVAL_LOC), p), p)
1157 contribution_0 := mulmod(mulmod(contribution_0, q_arith, p), mload(POW_PARTIAL_EVALUATION_LOC), p)
1158 mstore(SUBRELATION_EVAL_6_LOC, contribution_0)
1159
1160 let contribution_1 := mulmod(extra_small_addition_gate_identity, addmod(q_arith, sub(p, 1), p), p)
1161 contribution_1 := mulmod(contribution_1, q_arith, p)
1162 contribution_1 := mulmod(contribution_1, mload(POW_PARTIAL_EVALUATION_LOC), p)
1163 mstore(SUBRELATION_EVAL_7_LOC, contribution_1)
1164 }
1165
1166 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1167 /* PERMUTATION RELATION */
1168 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1169 {
1170 let beta := mload(BETA_CHALLENGE)
1171 let gamma := mload(GAMMA_CHALLENGE)
1172
1181 let t1 :=
1182 mulmod(
1183 add(add(mload(W1_EVAL_LOC), gamma), mulmod(beta, mload(ID1_EVAL_LOC), p)),
1184 add(add(mload(W2_EVAL_LOC), gamma), mulmod(beta, mload(ID2_EVAL_LOC), p)),
1185 p
1186 )
1187 let t2 :=
1188 mulmod(
1189 add(add(mload(W3_EVAL_LOC), gamma), mulmod(beta, mload(ID3_EVAL_LOC), p)),
1190 add(add(mload(W4_EVAL_LOC), gamma), mulmod(beta, mload(ID4_EVAL_LOC), p)),
1191 p
1192 )
1193 let numerator := mulmod(t1, t2, p)
1194 t1 := mulmod(
1195 add(add(mload(W1_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA1_EVAL_LOC), p)),
1196 add(add(mload(W2_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA2_EVAL_LOC), p)),
1197 p
1198 )
1199 t2 := mulmod(
1200 add(add(mload(W3_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA3_EVAL_LOC), p)),
1201 add(add(mload(W4_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA4_EVAL_LOC), p)),
1202 p
1203 )
1204 let denominator := mulmod(t1, t2, p)
1205
1206 {
1207 let acc :=
1208 mulmod(addmod(mload(Z_PERM_EVAL_LOC), mload(LAGRANGE_FIRST_EVAL_LOC), p), numerator, p)
1209
1210 acc := addmod(
1211 acc,
1212 sub(
1213 p,
1214 mulmod(
1215 addmod(
1216 mload(Z_PERM_SHIFT_EVAL_LOC),
1217 mulmod(
1218 mload(LAGRANGE_LAST_EVAL_LOC),
1219 mload(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE),
1220 p
1221 ),
1222 p
1223 ),
1224 denominator,
1225 p
1226 )
1227 ),
1228 p
1229 )
1230
1231 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1232 mstore(SUBRELATION_EVAL_0_LOC, acc)
1233
1234 acc := mulmod(
1235 mulmod(mload(LAGRANGE_LAST_EVAL_LOC), mload(Z_PERM_SHIFT_EVAL_LOC), p),
1236 mload(POW_PARTIAL_EVALUATION_LOC),
1237 p
1238 )
1239 mstore(SUBRELATION_EVAL_1_LOC, acc)
1240 }
1241
1242 // Contribution 4: z_perm initialization (lagrange_first * z_perm = 0)
1243 {
1244 let acc := mulmod(
1245 mulmod(mload(LAGRANGE_FIRST_EVAL_LOC), mload(Z_PERM_EVAL_LOC), p),
1246 mload(POW_PARTIAL_EVALUATION_LOC),
1247 p
1248 )
1249 mstore(SUBRELATION_EVAL_2_LOC, acc)
1250 }
1251 }
1252
1253 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1254 /* LOGUP WIDGET EVALUATION */
1255 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1256 // Note: Using beta powers for column batching and gamma for offset ensures soundness
1257 // beta and gamma must be independent challenges (they come from splitting the same hash)
1258 {
1259 let gamma := mload(GAMMA_CHALLENGE)
1260 let beta := mload(BETA_CHALLENGE)
1261 // Compute beta powers inline (β², β³) for lookup column batching
1262 let beta_sqr := mulmod(beta, beta, p)
1263 let beta_cube := mulmod(beta_sqr, beta, p)
1264
1265 // table_term = table_1 + γ + table_2 * β + table_3 * β² + table_4 * β³
1266 let t0 :=
1267 addmod(addmod(mload(TABLE1_EVAL_LOC), gamma, p), mulmod(mload(TABLE2_EVAL_LOC), beta, p), p)
1268 let t1 :=
1269 addmod(
1270 mulmod(mload(TABLE3_EVAL_LOC), beta_sqr, p),
1271 mulmod(mload(TABLE4_EVAL_LOC), beta_cube, p),
1272 p
1273 )
1274 let table_term := addmod(t0, t1, p)
1275
1276 // lookup_term = derived_entry_1 + γ + derived_entry_2 * β + derived_entry_3 * β² + q_index * β³
1277 t0 := addmod(
1278 addmod(mload(W1_EVAL_LOC), gamma, p),
1279 mulmod(mload(QR_EVAL_LOC), mload(W1_SHIFT_EVAL_LOC), p),
1280 p
1281 )
1282 t1 := addmod(mload(W2_EVAL_LOC), mulmod(mload(QM_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p), p)
1283 let t2 := addmod(mload(W3_EVAL_LOC), mulmod(mload(QC_EVAL_LOC), mload(W3_SHIFT_EVAL_LOC), p), p)
1284
1285 let lookup_term := addmod(t0, mulmod(t1, beta, p), p)
1286 lookup_term := addmod(lookup_term, mulmod(t2, beta_sqr, p), p)
1287 lookup_term := addmod(lookup_term, mulmod(mload(QO_EVAL_LOC), beta_cube, p), p)
1288
1289 let lookup_inverse := mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), table_term, p)
1290 let table_inverse := mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), lookup_term, p)
1291
1292 let inverse_exists_xor := addmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), mload(QLOOKUP_EVAL_LOC), p)
1293 inverse_exists_xor := addmod(
1294 inverse_exists_xor,
1295 sub(p, mulmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), mload(QLOOKUP_EVAL_LOC), p)),
1296 p
1297 )
1298
1299 let accumulator_none := mulmod(mulmod(lookup_term, table_term, p), mload(LOOKUP_INVERSES_EVAL_LOC), p)
1300 accumulator_none := addmod(accumulator_none, sub(p, inverse_exists_xor), p)
1301 accumulator_none := mulmod(accumulator_none, mload(POW_PARTIAL_EVALUATION_LOC), p)
1302
1303 let accumulator_one := mulmod(mload(QLOOKUP_EVAL_LOC), lookup_inverse, p)
1304 accumulator_one := addmod(
1305 accumulator_one,
1306 sub(p, mulmod(mload(LOOKUP_READ_COUNTS_EVAL_LOC), table_inverse, p)),
1307 p
1308 )
1309
1310 let read_tag := mload(LOOKUP_READ_TAGS_EVAL_LOC)
1311 let read_tag_boolean_relation := mulmod(read_tag, addmod(read_tag, sub(p, 1), p), p)
1312 read_tag_boolean_relation := mulmod(read_tag_boolean_relation, mload(POW_PARTIAL_EVALUATION_LOC), p)
1313
1314 mstore(SUBRELATION_EVAL_3_LOC, accumulator_none)
1315 mstore(SUBRELATION_EVAL_4_LOC, accumulator_one)
1316 mstore(SUBRELATION_EVAL_5_LOC, read_tag_boolean_relation)
1317 }
1318
1319 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1320 /* DELTA RANGE RELATION */
1321 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1322 {
1323 let minus_one := P_SUB_1
1324 let minus_two := P_SUB_2
1325 let minus_three := P_SUB_3
1326
1327 let delta_1 := addmod(mload(W2_EVAL_LOC), sub(p, mload(W1_EVAL_LOC)), p)
1328 let delta_2 := addmod(mload(W3_EVAL_LOC), sub(p, mload(W2_EVAL_LOC)), p)
1329 let delta_3 := addmod(mload(W4_EVAL_LOC), sub(p, mload(W3_EVAL_LOC)), p)
1330 let delta_4 := addmod(mload(W1_SHIFT_EVAL_LOC), sub(p, mload(W4_EVAL_LOC)), p)
1331
1332 {
1333 let acc := delta_1
1334 acc := mulmod(acc, addmod(delta_1, minus_one, p), p)
1335 acc := mulmod(acc, addmod(delta_1, minus_two, p), p)
1336 acc := mulmod(acc, addmod(delta_1, minus_three, p), p)
1337 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1338 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1339 mstore(SUBRELATION_EVAL_8_LOC, acc)
1340 }
1341
1342 {
1343 let acc := delta_2
1344 acc := mulmod(acc, addmod(delta_2, minus_one, p), p)
1345 acc := mulmod(acc, addmod(delta_2, minus_two, p), p)
1346 acc := mulmod(acc, addmod(delta_2, minus_three, p), p)
1347 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1348 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1349 mstore(SUBRELATION_EVAL_9_LOC, acc)
1350 }
1351
1352 {
1353 let acc := delta_3
1354 acc := mulmod(acc, addmod(delta_3, minus_one, p), p)
1355 acc := mulmod(acc, addmod(delta_3, minus_two, p), p)
1356 acc := mulmod(acc, addmod(delta_3, minus_three, p), p)
1357 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1358 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1359 mstore(SUBRELATION_EVAL_10_LOC, acc)
1360 }
1361
1362 {
1363 let acc := delta_4
1364 acc := mulmod(acc, addmod(delta_4, minus_one, p), p)
1365 acc := mulmod(acc, addmod(delta_4, minus_two, p), p)
1366 acc := mulmod(acc, addmod(delta_4, minus_three, p), p)
1367 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1368 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1369 mstore(SUBRELATION_EVAL_11_LOC, acc)
1370 }
1371 }
1372
1373 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1374 /* ELLIPTIC CURVE RELATION */
1375 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1376 {
1377 // Contribution 10 point addition, x-coordinate check
1378 // q_elliptic * (x3 + x2 + x1)(x2 - x1)(x2 - x1) - y2^2 - y1^2 + 2(y2y1)*q_sign = 0
1379 let x_diff := addmod(mload(EC_X_2), sub(p, mload(EC_X_1)), p)
1380 let y1_sqr := mulmod(mload(EC_Y_1), mload(EC_Y_1), p)
1381 {
1382 let y2_sqr := mulmod(mload(EC_Y_2), mload(EC_Y_2), p)
1383 let y1y2 := mulmod(mulmod(mload(EC_Y_1), mload(EC_Y_2), p), mload(EC_Q_SIGN), p)
1384 let x_add_identity := addmod(mload(EC_X_3), addmod(mload(EC_X_2), mload(EC_X_1), p), p)
1385 x_add_identity := mulmod(mulmod(x_add_identity, x_diff, p), x_diff, p)
1386 x_add_identity := addmod(x_add_identity, sub(p, y2_sqr), p)
1387 x_add_identity := addmod(x_add_identity, sub(p, y1_sqr), p)
1388 x_add_identity := addmod(x_add_identity, y1y2, p)
1389 x_add_identity := addmod(x_add_identity, y1y2, p)
1390
1391 let eval := mulmod(x_add_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1392 eval := mulmod(eval, mload(QELLIPTIC_EVAL_LOC), p)
1393 eval := mulmod(eval, addmod(1, sub(p, mload(EC_Q_IS_DOUBLE)), p), p)
1394 mstore(SUBRELATION_EVAL_12_LOC, eval)
1395 }
1396
1397 {
1398 let y1_plus_y3 := addmod(mload(EC_Y_1), mload(EC_Y_3), p)
1399 let y_diff := mulmod(mload(EC_Y_2), mload(EC_Q_SIGN), p)
1400 y_diff := addmod(y_diff, sub(p, mload(EC_Y_1)), p)
1401 let y_add_identity := mulmod(y1_plus_y3, x_diff, p)
1402 y_add_identity := addmod(
1403 y_add_identity,
1404 mulmod(addmod(mload(EC_X_3), sub(p, mload(EC_X_1)), p), y_diff, p),
1405 p
1406 )
1407
1408 let eval := mulmod(y_add_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1409 eval := mulmod(eval, mload(QELLIPTIC_EVAL_LOC), p)
1410 eval := mulmod(eval, addmod(1, sub(p, mload(EC_Q_IS_DOUBLE)), p), p)
1411 mstore(SUBRELATION_EVAL_13_LOC, eval)
1412 }
1413
1414 {
1415 let x_pow_4 := mulmod(addmod(y1_sqr, GRUMPKIN_CURVE_B_PARAMETER_NEGATED, p), mload(EC_X_1), p)
1416 let y1_sqr_mul_4 := addmod(y1_sqr, y1_sqr, p)
1417 y1_sqr_mul_4 := addmod(y1_sqr_mul_4, y1_sqr_mul_4, p)
1418
1419 let x1_pow_4_mul_9 := mulmod(x_pow_4, 9, p)
1420
1421 let ep_x_double_identity := addmod(mload(EC_X_3), addmod(mload(EC_X_1), mload(EC_X_1), p), p)
1422 ep_x_double_identity := mulmod(ep_x_double_identity, y1_sqr_mul_4, p)
1423 ep_x_double_identity := addmod(ep_x_double_identity, sub(p, x1_pow_4_mul_9), p)
1424
1425 let acc := mulmod(ep_x_double_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1426 acc := mulmod(mulmod(acc, mload(QELLIPTIC_EVAL_LOC), p), mload(EC_Q_IS_DOUBLE), p)
1427 acc := addmod(acc, mload(SUBRELATION_EVAL_12_LOC), p)
1428
1429 // Add to existing contribution - and double check that numbers here
1430 mstore(SUBRELATION_EVAL_12_LOC, acc)
1431 }
1432
1433 {
1434 let x1_sqr_mul_3 :=
1435 mulmod(addmod(addmod(mload(EC_X_1), mload(EC_X_1), p), mload(EC_X_1), p), mload(EC_X_1), p)
1436 let y_double_identity :=
1437 mulmod(x1_sqr_mul_3, addmod(mload(EC_X_1), sub(p, mload(EC_X_3)), p), p)
1438 y_double_identity := addmod(
1439 y_double_identity,
1440 sub(
1441 p,
1442 mulmod(
1443 addmod(mload(EC_Y_1), mload(EC_Y_1), p),
1444 addmod(mload(EC_Y_1), mload(EC_Y_3), p),
1445 p
1446 )
1447 ),
1448 p
1449 )
1450
1451 let acc := mulmod(y_double_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1452 acc := mulmod(mulmod(acc, mload(QELLIPTIC_EVAL_LOC), p), mload(EC_Q_IS_DOUBLE), p)
1453 acc := addmod(acc, mload(SUBRELATION_EVAL_13_LOC), p)
1454
1455 // Add to existing contribution - and double check that numbers here
1456 mstore(SUBRELATION_EVAL_13_LOC, acc)
1457 }
1458 }
1459
1460 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1461 /* MEMORY RELATION */
1462 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1463 {
1464 {
1516 let memory_record_check := mulmod(mload(W3_EVAL_LOC), mload(ETA_THREE_CHALLENGE), p)
1517 memory_record_check := addmod(
1518 memory_record_check,
1519 mulmod(mload(W2_EVAL_LOC), mload(ETA_TWO_CHALLENGE), p),
1520 p
1521 )
1522 memory_record_check := addmod(
1523 memory_record_check,
1524 mulmod(mload(W1_EVAL_LOC), mload(ETA_CHALLENGE), p),
1525 p
1526 )
1527 memory_record_check := addmod(memory_record_check, mload(QC_EVAL_LOC), p)
1528
1529 let partial_record_check := memory_record_check
1530 memory_record_check := addmod(memory_record_check, sub(p, mload(W4_EVAL_LOC)), p)
1531
1532 mstore(AUX_MEMORY_CHECK_IDENTITY, memory_record_check)
1533
1549 // index_delta = w_1_omega - w_1
1550 let index_delta := addmod(mload(W1_SHIFT_EVAL_LOC), sub(p, mload(W1_EVAL_LOC)), p)
1551
1552 // record_delta = w_4_omega - w_4
1553 let record_delta := addmod(mload(W4_SHIFT_EVAL_LOC), sub(p, mload(W4_EVAL_LOC)), p)
1554
1555 // index_is_monotonically_increasing = index_delta * (index_delta - 1)
1556 let index_is_monotonically_increasing := mulmod(index_delta, addmod(index_delta, P_SUB_1, p), p)
1557
1558 // adjacent_values_match_if_adjacent_indices_match = record_delta * (1 - index_delta)
1559 let adjacent_values_match_if_adjacent_indices_match :=
1560 mulmod(record_delta, addmod(1, sub(p, index_delta), p), p)
1561
1562 mstore(
1563 SUBRELATION_EVAL_15_LOC,
1564 mulmod(
1565 adjacent_values_match_if_adjacent_indices_match,
1566 mulmod(
1567 mload(QL_EVAL_LOC),
1568 mulmod(
1569 mload(QR_EVAL_LOC),
1570 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1571 p
1572 ),
1573 p
1574 ),
1575 p
1576 )
1577 )
1578
1579 // ROM_CONSISTENCY_CHECK_2
1580 mstore(
1581 SUBRELATION_EVAL_16_LOC,
1582 mulmod(
1583 index_is_monotonically_increasing,
1584 mulmod(
1585 mload(QL_EVAL_LOC),
1586 mulmod(
1587 mload(QR_EVAL_LOC),
1588 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1589 p
1590 ),
1591 p
1592 ),
1593 p
1594 )
1595 )
1596
1597 mstore(
1598 AUX_ROM_CONSISTENCY_CHECK_IDENTITY,
1599 mulmod(memory_record_check, mulmod(mload(QL_EVAL_LOC), mload(QR_EVAL_LOC), p), p)
1600 )
1601
1602 {
1629 let next_gate_access_type := mulmod(mload(W3_SHIFT_EVAL_LOC), mload(ETA_THREE_CHALLENGE), p)
1630 next_gate_access_type := addmod(
1631 next_gate_access_type,
1632 mulmod(mload(W2_SHIFT_EVAL_LOC), mload(ETA_TWO_CHALLENGE), p),
1633 p
1634 )
1635 next_gate_access_type := addmod(
1636 next_gate_access_type,
1637 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(ETA_CHALLENGE), p),
1638 p
1639 )
1640 next_gate_access_type := addmod(mload(W4_SHIFT_EVAL_LOC), sub(p, next_gate_access_type), p)
1641
1642 // value_delta = w_3_omega - w_3
1643 let value_delta := addmod(mload(W3_SHIFT_EVAL_LOC), sub(p, mload(W3_EVAL_LOC)), p)
1644 // adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation = (1 - index_delta) * value_delta * (1 - next_gate_access_type);
1645
1646 let adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation :=
1647 mulmod(
1648 addmod(1, sub(p, index_delta), p),
1649 mulmod(value_delta, addmod(1, sub(p, next_gate_access_type), p), p),
1650 p
1651 )
1652
1653 // We can't apply the RAM consistency check identity on the final entry in the sorted list (the wires in the
1654 // next gate would make the identity fail). We need to validate that its 'access type' bool is correct. Can't
1655 // do with an arithmetic gate because of the `eta` factors. We need to check that the *next* gate's access
1656 // type is correct, to cover this edge case
1657 // deg 2 or 4
1663 let access_type := addmod(mload(W4_EVAL_LOC), sub(p, partial_record_check), p)
1664 let access_check := mulmod(access_type, addmod(access_type, P_SUB_1, p), p)
1665 let next_gate_access_type_is_boolean :=
1666 mulmod(next_gate_access_type, addmod(next_gate_access_type, P_SUB_1, p), p)
1667
1668 // scaled_activation_selector = q_arith * q_aux * alpha
1669 let scaled_activation_selector :=
1670 mulmod(
1671 mload(QO_EVAL_LOC),
1672 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1673 p
1674 )
1675
1676 mstore(
1677 SUBRELATION_EVAL_17_LOC,
1678 mulmod(
1679 adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation,
1680 scaled_activation_selector,
1681 p
1682 )
1683 )
1684
1685 mstore(
1686 SUBRELATION_EVAL_18_LOC,
1687 mulmod(index_is_monotonically_increasing, scaled_activation_selector, p)
1688 )
1689
1690 mstore(
1691 SUBRELATION_EVAL_19_LOC,
1692 mulmod(next_gate_access_type_is_boolean, scaled_activation_selector, p)
1693 )
1694
1695 mstore(AUX_RAM_CONSISTENCY_CHECK_IDENTITY, mulmod(access_check, mload(QO_EVAL_LOC), p))
1696 }
1697
1698 {
1699 // timestamp_delta = w_2_omega - w_2
1700 let timestamp_delta := addmod(mload(W2_SHIFT_EVAL_LOC), sub(p, mload(W2_EVAL_LOC)), p)
1701
1702 // RAM_timestamp_check_identity = (1 - index_delta) * timestamp_delta - w_3
1703 let RAM_TIMESTAMP_CHECK_IDENTITY :=
1704 addmod(
1705 mulmod(timestamp_delta, addmod(1, sub(p, index_delta), p), p),
1706 sub(p, mload(W3_EVAL_LOC)),
1707 p
1708 )
1709
1721 let memory_identity := mload(AUX_ROM_CONSISTENCY_CHECK_IDENTITY)
1722 memory_identity := addmod(
1723 memory_identity,
1724 mulmod(
1725 RAM_TIMESTAMP_CHECK_IDENTITY,
1726 mulmod(mload(Q4_EVAL_LOC), mload(QL_EVAL_LOC), p),
1727 p
1728 ),
1729 p
1730 )
1731
1732 memory_identity := addmod(
1733 memory_identity,
1734 mulmod(
1735 mload(AUX_MEMORY_CHECK_IDENTITY),
1736 mulmod(mload(QM_EVAL_LOC), mload(QL_EVAL_LOC), p),
1737 p
1738 ),
1739 p
1740 )
1741 memory_identity := addmod(memory_identity, mload(AUX_RAM_CONSISTENCY_CHECK_IDENTITY), p)
1742
1743 memory_identity := mulmod(
1744 memory_identity,
1745 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1746 p
1747 )
1748 mstore(SUBRELATION_EVAL_14_LOC, memory_identity)
1749 }
1750 }
1751 }
1752
1753 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1754 /* ROM LOGUP RELATION */
1755 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1756 {
1757 // Single-value ROM tables. Wire layout: (w_1, w_2, w_3, w_4) = (index, value, multiplicity,
1758 // inverse), q_c = array id. q_logup_table = q_2 * (1 - q_1), q_logup_read = q_4 * (1 - q_1).
1759 let one_minus_q1 := addmod(1, sub(p, mload(QL_EVAL_LOC)), p)
1760 let q_logup_table := mulmod(mload(QR_EVAL_LOC), one_minus_q1, p)
1761 let q_logup_read := mulmod(mload(Q4_EVAL_LOC), one_minus_q1, p)
1762
1763 // denom = rom_logup_gamma + w_1 + eta * w_2 + eta_two * q_c
1764 let denom := mload(ROM_LOGUP_GAMMA_CHALLENGE)
1765 denom := addmod(denom, mload(W1_EVAL_LOC), p)
1766 denom := addmod(denom, mulmod(mload(ETA_CHALLENGE), mload(W2_EVAL_LOC), p), p)
1767 denom := addmod(denom, mulmod(mload(ETA_TWO_CHALLENGE), mload(QC_EVAL_LOC), p), p)
1768
1769 // Inverse correctness: q_logup_any * (w_4 * denom - 1) * q_memory
1770 let inverse_correctness := addmod(mulmod(mload(W4_EVAL_LOC), denom, p), sub(p, 1), p)
1771 inverse_correctness := mulmod(addmod(q_logup_table, q_logup_read, p), inverse_correctness, p)
1772 inverse_correctness :=
1773 mulmod(
1774 inverse_correctness,
1775 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1776 p
1777 )
1778 mstore(SUBRELATION_EVAL_20_LOC, inverse_correctness)
1779
1780 // LogUp sum identity. Linearly dependent, so not scaled by the pow evaluation.
1781 let logup_sum := addmod(q_logup_read, sub(p, mulmod(q_logup_table, mload(W3_EVAL_LOC), p)), p)
1782 logup_sum := mulmod(logup_sum, mload(W4_EVAL_LOC), p)
1783 logup_sum := mulmod(logup_sum, mload(QMEMORY_EVAL_LOC), p)
1784 mstore(SUBRELATION_EVAL_21_LOC, logup_sum)
1785 }
1786
1787 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1788 /* NON NATIVE FIELD RELATION */
1789 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1790 {
1810 let limb_subproduct :=
1811 addmod(
1812 mulmod(mload(W1_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p),
1813 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(W2_EVAL_LOC), p),
1814 p
1815 )
1816
1817 let non_native_field_gate_2 :=
1818 addmod(
1819 addmod(
1820 mulmod(mload(W1_EVAL_LOC), mload(W4_EVAL_LOC), p),
1821 mulmod(mload(W2_EVAL_LOC), mload(W3_EVAL_LOC), p),
1822 p
1823 ),
1824 sub(p, mload(W3_SHIFT_EVAL_LOC)),
1825 p
1826 )
1827 non_native_field_gate_2 := mulmod(non_native_field_gate_2, LIMB_SIZE, p)
1828 non_native_field_gate_2 := addmod(non_native_field_gate_2, sub(p, mload(W4_SHIFT_EVAL_LOC)), p)
1829 non_native_field_gate_2 := addmod(non_native_field_gate_2, limb_subproduct, p)
1830 non_native_field_gate_2 := mulmod(non_native_field_gate_2, mload(Q4_EVAL_LOC), p)
1831
1832 limb_subproduct := mulmod(limb_subproduct, LIMB_SIZE, p)
1833 limb_subproduct := addmod(
1834 limb_subproduct,
1835 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p),
1836 p
1837 )
1838
1839 let non_native_field_gate_1 :=
1840 mulmod(
1841 addmod(limb_subproduct, sub(p, addmod(mload(W3_EVAL_LOC), mload(W4_EVAL_LOC), p)), p),
1842 mload(QO_EVAL_LOC),
1843 p
1844 )
1845
1846 let non_native_field_gate_3 :=
1847 mulmod(
1848 addmod(
1849 addmod(limb_subproduct, mload(W4_EVAL_LOC), p),
1850 sub(p, addmod(mload(W3_SHIFT_EVAL_LOC), mload(W4_SHIFT_EVAL_LOC), p)),
1851 p
1852 ),
1853 mload(QM_EVAL_LOC),
1854 p
1855 )
1856 let non_native_field_identity :=
1857 mulmod(
1858 addmod(
1859 addmod(non_native_field_gate_1, non_native_field_gate_2, p),
1860 non_native_field_gate_3,
1861 p
1862 ),
1863 mload(QR_EVAL_LOC),
1864 p
1865 )
1866
1867 mstore(AUX_NON_NATIVE_FIELD_IDENTITY, non_native_field_identity)
1868 }
1869
1870 {
1884 let limb_accumulator_1 := mulmod(mload(W2_SHIFT_EVAL_LOC), SUBLIMB_SHIFT, p)
1885 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W1_SHIFT_EVAL_LOC), p)
1886 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1887 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W3_EVAL_LOC), p)
1888 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1889 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W2_EVAL_LOC), p)
1890 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1891 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W1_EVAL_LOC), p)
1892 limb_accumulator_1 := addmod(limb_accumulator_1, sub(p, mload(W4_EVAL_LOC)), p)
1893 limb_accumulator_1 := mulmod(limb_accumulator_1, mload(Q4_EVAL_LOC), p)
1894
1908 let limb_accumulator_2 := mulmod(mload(W3_SHIFT_EVAL_LOC), SUBLIMB_SHIFT, p)
1909 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W2_SHIFT_EVAL_LOC), p)
1910 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1911 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W1_SHIFT_EVAL_LOC), p)
1912 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1913 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W4_EVAL_LOC), p)
1914 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1915 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W3_EVAL_LOC), p)
1916 limb_accumulator_2 := addmod(limb_accumulator_2, sub(p, mload(W4_SHIFT_EVAL_LOC)), p)
1917 limb_accumulator_2 := mulmod(limb_accumulator_2, mload(QM_EVAL_LOC), p)
1918
1919 let limb_accumulator_identity := addmod(limb_accumulator_1, limb_accumulator_2, p)
1920 limb_accumulator_identity := mulmod(limb_accumulator_identity, mload(QO_EVAL_LOC), p)
1921
1922 let nnf_identity := addmod(mload(AUX_NON_NATIVE_FIELD_IDENTITY), limb_accumulator_identity, p)
1923 nnf_identity := mulmod(
1924 nnf_identity,
1925 mulmod(mload(QNNF_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1926 p
1927 )
1928
1929 mstore(SUBRELATION_EVAL_22_LOC, nnf_identity)
1930 }
1931
1932 /*
1933 * Poseidon External Relation
1934 */
1935 {
1936 let s1 := addmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
1937 let s2 := addmod(mload(W2_EVAL_LOC), mload(QR_EVAL_LOC), p)
1938 let s3 := addmod(mload(W3_EVAL_LOC), mload(QO_EVAL_LOC), p)
1939 let s4 := addmod(mload(W4_EVAL_LOC), mload(Q4_EVAL_LOC), p)
1940
1941 // u1 := s1 * s1 * s1 * s1 * s1;
1942 let t0 := mulmod(s1, s1, p)
1943 let u1 := mulmod(t0, mulmod(t0, s1, p), p)
1944
1945 // u2 := s2 * s2 * s2 * s2 * s2;
1946 t0 := mulmod(s2, s2, p)
1947 let u2 := mulmod(t0, mulmod(t0, s2, p), p)
1948
1949 // u3 := s3 * s3 * s3 * s3 * s3;
1950 t0 := mulmod(s3, s3, p)
1951 let u3 := mulmod(t0, mulmod(t0, s3, p), p)
1952
1953 // u4 := s4 * s4 * s4 * s4 * s4;
1954 t0 := mulmod(s4, s4, p)
1955 let u4 := mulmod(t0, mulmod(t0, s4, p), p)
1956
1957 // matrix mul v = M_E * u with 14 additions
1958 t0 := addmod(u1, u2, p)
1959 let t1 := addmod(u3, u4, p)
1960
1961 let t2 := addmod(u2, u2, p)
1962 t2 := addmod(t2, t1, p)
1963
1964 let t3 := addmod(u4, u4, p)
1965 t3 := addmod(t3, t0, p)
1966
1967 let v4 := addmod(t1, t1, p)
1968 v4 := addmod(v4, v4, p)
1969 v4 := addmod(v4, t3, p)
1970
1971 let v2 := addmod(t0, t0, p)
1972 v2 := addmod(v2, v2, p)
1973 v2 := addmod(v2, t2, p)
1974
1975 let v1 := addmod(t3, v2, p)
1976 let v3 := addmod(t2, v4, p)
1977
1978 let q_pos_by_scaling :=
1979 mulmod(mload(QPOSEIDON2_EXTERNAL_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p)
1980
1981 mstore(
1982 SUBRELATION_EVAL_23_LOC,
1983 mulmod(q_pos_by_scaling, addmod(v1, sub(p, mload(W1_SHIFT_EVAL_LOC)), p), p)
1984 )
1985
1986 mstore(
1987 SUBRELATION_EVAL_24_LOC,
1988 mulmod(q_pos_by_scaling, addmod(v2, sub(p, mload(W2_SHIFT_EVAL_LOC)), p), p)
1989 )
1990
1991 mstore(
1992 SUBRELATION_EVAL_25_LOC,
1993 mulmod(q_pos_by_scaling, addmod(v3, sub(p, mload(W3_SHIFT_EVAL_LOC)), p), p)
1994 )
1995
1996 mstore(
1997 SUBRELATION_EVAL_26_LOC,
1998 mulmod(q_pos_by_scaling, addmod(v4, sub(p, mload(W4_SHIFT_EVAL_LOC)), p), p)
1999 )
2000 }
2001
2002 /*
2003 * Poseidon Internal Relation
2004 */
2005 {
2006 let s1 := addmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
2007
2008 // apply s-box round
2009 let t0 := mulmod(s1, s1, p)
2010 let u1 := mulmod(t0, mulmod(t0, s1, p), p)
2011 let u2 := mload(W2_EVAL_LOC)
2012 let u3 := mload(W3_EVAL_LOC)
2013 let u4 := mload(W4_EVAL_LOC)
2014
2015 // matrix mul v = M_I * u 4 muls and 7 additions
2016 let u_sum := addmod(u1, u2, p)
2017 u_sum := addmod(u_sum, addmod(u3, u4, p), p)
2018
2019 let q_pos_by_scaling :=
2020 mulmod(mload(QPOSEIDON2_INTERNAL_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p)
2021
2022 let v1 := addmod(mulmod(u1, POS_INTERNAL_MATRIX_D_0, p), u_sum, p)
2023
2024 mstore(
2025 SUBRELATION_EVAL_27_LOC,
2026 mulmod(q_pos_by_scaling, addmod(v1, sub(p, mload(W1_SHIFT_EVAL_LOC)), p), p)
2027 )
2028 let v2 := addmod(mulmod(u2, POS_INTERNAL_MATRIX_D_1, p), u_sum, p)
2029
2030 mstore(
2031 SUBRELATION_EVAL_28_LOC,
2032 mulmod(q_pos_by_scaling, addmod(v2, sub(p, mload(W2_SHIFT_EVAL_LOC)), p), p)
2033 )
2034 let v3 := addmod(mulmod(u3, POS_INTERNAL_MATRIX_D_2, p), u_sum, p)
2035
2036 mstore(
2037 SUBRELATION_EVAL_29_LOC,
2038 mulmod(q_pos_by_scaling, addmod(v3, sub(p, mload(W3_SHIFT_EVAL_LOC)), p), p)
2039 )
2040
2041 let v4 := addmod(mulmod(u4, POS_INTERNAL_MATRIX_D_3, p), u_sum, p)
2042 mstore(
2043 SUBRELATION_EVAL_30_LOC,
2044 mulmod(q_pos_by_scaling, addmod(v4, sub(p, mload(W4_SHIFT_EVAL_LOC)), p), p)
2045 )
2046 }
2047
2048 // Scale and batch subrelations by subrelation challenges
2049 // linear combination of subrelations
2050 let accumulator := mload(SUBRELATION_EVAL_0_LOC)
2051
2052 // Below is an unrolled variant of the following loop
2053 // for (uint256 i = 1; i < NUMBER_OF_SUBRELATIONS; ++i) {
2054 // accumulator = accumulator + evaluations[i] * subrelationChallenges[i - 1];
2055 // }
2056
2057 accumulator := addmod(
2058 accumulator,
2059 mulmod(mload(SUBRELATION_EVAL_1_LOC), mload(ALPHA_CHALLENGE_0), p),
2060 p
2061 )
2062 accumulator := addmod(
2063 accumulator,
2064 mulmod(mload(SUBRELATION_EVAL_2_LOC), mload(ALPHA_CHALLENGE_1), p),
2065 p
2066 )
2067 accumulator := addmod(
2068 accumulator,
2069 mulmod(mload(SUBRELATION_EVAL_3_LOC), mload(ALPHA_CHALLENGE_2), p),
2070 p
2071 )
2072 accumulator := addmod(
2073 accumulator,
2074 mulmod(mload(SUBRELATION_EVAL_4_LOC), mload(ALPHA_CHALLENGE_3), p),
2075 p
2076 )
2077 accumulator := addmod(
2078 accumulator,
2079 mulmod(mload(SUBRELATION_EVAL_5_LOC), mload(ALPHA_CHALLENGE_4), p),
2080 p
2081 )
2082 accumulator := addmod(
2083 accumulator,
2084 mulmod(mload(SUBRELATION_EVAL_6_LOC), mload(ALPHA_CHALLENGE_5), p),
2085 p
2086 )
2087 accumulator := addmod(
2088 accumulator,
2089 mulmod(mload(SUBRELATION_EVAL_7_LOC), mload(ALPHA_CHALLENGE_6), p),
2090 p
2091 )
2092 accumulator := addmod(
2093 accumulator,
2094 mulmod(mload(SUBRELATION_EVAL_8_LOC), mload(ALPHA_CHALLENGE_7), p),
2095 p
2096 )
2097 accumulator := addmod(
2098 accumulator,
2099 mulmod(mload(SUBRELATION_EVAL_9_LOC), mload(ALPHA_CHALLENGE_8), p),
2100 p
2101 )
2102 accumulator := addmod(
2103 accumulator,
2104 mulmod(mload(SUBRELATION_EVAL_10_LOC), mload(ALPHA_CHALLENGE_9), p),
2105 p
2106 )
2107 accumulator := addmod(
2108 accumulator,
2109 mulmod(mload(SUBRELATION_EVAL_11_LOC), mload(ALPHA_CHALLENGE_10), p),
2110 p
2111 )
2112 accumulator := addmod(
2113 accumulator,
2114 mulmod(mload(SUBRELATION_EVAL_12_LOC), mload(ALPHA_CHALLENGE_11), p),
2115 p
2116 )
2117 accumulator := addmod(
2118 accumulator,
2119 mulmod(mload(SUBRELATION_EVAL_13_LOC), mload(ALPHA_CHALLENGE_12), p),
2120 p
2121 )
2122 accumulator := addmod(
2123 accumulator,
2124 mulmod(mload(SUBRELATION_EVAL_14_LOC), mload(ALPHA_CHALLENGE_13), p),
2125 p
2126 )
2127 accumulator := addmod(
2128 accumulator,
2129 mulmod(mload(SUBRELATION_EVAL_15_LOC), mload(ALPHA_CHALLENGE_14), p),
2130 p
2131 )
2132 accumulator := addmod(
2133 accumulator,
2134 mulmod(mload(SUBRELATION_EVAL_16_LOC), mload(ALPHA_CHALLENGE_15), p),
2135 p
2136 )
2137 accumulator := addmod(
2138 accumulator,
2139 mulmod(mload(SUBRELATION_EVAL_17_LOC), mload(ALPHA_CHALLENGE_16), p),
2140 p
2141 )
2142 accumulator := addmod(
2143 accumulator,
2144 mulmod(mload(SUBRELATION_EVAL_18_LOC), mload(ALPHA_CHALLENGE_17), p),
2145 p
2146 )
2147 accumulator := addmod(
2148 accumulator,
2149 mulmod(mload(SUBRELATION_EVAL_19_LOC), mload(ALPHA_CHALLENGE_18), p),
2150 p
2151 )
2152 accumulator := addmod(
2153 accumulator,
2154 mulmod(mload(SUBRELATION_EVAL_20_LOC), mload(ALPHA_CHALLENGE_19), p),
2155 p
2156 )
2157 accumulator := addmod(
2158 accumulator,
2159 mulmod(mload(SUBRELATION_EVAL_21_LOC), mload(ALPHA_CHALLENGE_20), p),
2160 p
2161 )
2162 accumulator := addmod(
2163 accumulator,
2164 mulmod(mload(SUBRELATION_EVAL_22_LOC), mload(ALPHA_CHALLENGE_21), p),
2165 p
2166 )
2167 accumulator := addmod(
2168 accumulator,
2169 mulmod(mload(SUBRELATION_EVAL_23_LOC), mload(ALPHA_CHALLENGE_22), p),
2170 p
2171 )
2172 accumulator := addmod(
2173 accumulator,
2174 mulmod(mload(SUBRELATION_EVAL_24_LOC), mload(ALPHA_CHALLENGE_23), p),
2175 p
2176 )
2177 accumulator := addmod(
2178 accumulator,
2179 mulmod(mload(SUBRELATION_EVAL_25_LOC), mload(ALPHA_CHALLENGE_24), p),
2180 p
2181 )
2182 accumulator := addmod(
2183 accumulator,
2184 mulmod(mload(SUBRELATION_EVAL_26_LOC), mload(ALPHA_CHALLENGE_25), p),
2185 p
2186 )
2187 accumulator := addmod(
2188 accumulator,
2189 mulmod(mload(SUBRELATION_EVAL_27_LOC), mload(ALPHA_CHALLENGE_26), p),
2190 p
2191 )
2192 accumulator := addmod(
2193 accumulator,
2194 mulmod(mload(SUBRELATION_EVAL_28_LOC), mload(ALPHA_CHALLENGE_27), p),
2195 p
2196 )
2197 accumulator := addmod(
2198 accumulator,
2199 mulmod(mload(SUBRELATION_EVAL_29_LOC), mload(ALPHA_CHALLENGE_28), p),
2200 p
2201 )
2202 accumulator := addmod(
2203 accumulator,
2204 mulmod(mload(SUBRELATION_EVAL_30_LOC), mload(ALPHA_CHALLENGE_29), p),
2205 p
2206 )
2207
2208 let sumcheck_valid := eq(accumulator, mload(FINAL_ROUND_TARGET_LOC))
2209
2210 if iszero(sumcheck_valid) {
2211 mstore(0x00, SUMCHECK_FAILED_SELECTOR)
2212 revert(0x00, 0x04)
2213 }
2214 }
2215
2216 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
2217 /* SUMCHECK -- Complete */
2218 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
2219
2220 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
2221 /* SHPLEMINI */
2222 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
2223
2224 // ============= SHPLEMINI INVERSES ==============
2225 // Inverses were computed in the unified batch inversion above.
2226 let unshifted_scalar := 0
2227 let shifted_scalar := 0
2228 {
2229 // staging[0] = 1/gemini_r -- needed for shifted_scalar computation
2230 let gemini_r_inv := mload(GEMINI_R_INV_LOC)
2231
2232 // staging[1..3*LOG_N] maps contiguously to:
2233 // INVERTED_CHALLENGE_POW_MINUS_U_0..14
2234 // POS_INVERTED_DENOM_0..14
2235 // NEG_INVERTED_DENOM_0..14
2236 // Total: 3*LOG_N
2237
2238 // Compute unshifted_scalar and shifted_scalar using the copied inverses
2239 let pos_inverted_denominator := mload(POS_INVERTED_DENOM_0_LOC)
2240 let neg_inverted_denominator := mload(NEG_INVERTED_DENOM_0_LOC)
2241 let shplonk_nu := mload(SHPLONK_NU_CHALLENGE)
2242
2243 unshifted_scalar := addmod(pos_inverted_denominator, mulmod(shplonk_nu, neg_inverted_denominator, p), p)
2244
2245 shifted_scalar := mulmod(
2246 gemini_r_inv, // (1 / gemini_r_challenge) from staging[0]
2247 // (inverse_vanishing_evals[0]) - (shplonk_nu * inverse_vanishing_evals[1])
2248 addmod(
2249 pos_inverted_denominator,
2250 // - (shplonk_nu * inverse_vanishing_evals[1])
2251 sub(p, mulmod(shplonk_nu, neg_inverted_denominator, p)),
2252 p
2253 ),
2254 p
2255 )
2256 }
2257
2258 // Commitment Accumulation (MSM via sequential ecAdd/ecMul):
2259 // For each commitment C_i with batch scalar s_i, we compute:
2260 // accumulator += s_i * C_i
2261 // The commitments include: shplonk_Q, VK points, wire commitments,
2262 // lookup commitments, Z_PERM, gemini fold univariates.
2263 // The KZG quotient is handled separately.
2264 // The final accumulator is the LHS of the pairing equation.
2265
2266 // Accumulators
2267 let batching_challenge := 1
2268 let batched_evaluation := 0
2269
2270 let neg_unshifted_scalar := sub(p, unshifted_scalar)
2271 let neg_shifted_scalar := sub(p, shifted_scalar)
2272
2273 let rho := mload(RHO_CHALLENGE)
2274
2275 // Unrolled for the loop below - where NUMBER_UNSHIFTED = 36
2276 // for (uint256 i = 1; i <= NUMBER_UNSHIFTED; ++i) {
2277 // scalars[i] = mem.unshiftedScalar.neg() * mem.batchingChallenge;
2278 // mem.batchedEvaluation = mem.batchedEvaluation + (proof.sumcheckEvaluations[i - 1] * mem.batchingChallenge);
2279 // mem.batchingChallenge = mem.batchingChallenge * tp.rho;
2280 // }
2281
2282 // Iteration order matches UltraFlavor_Generated::EntityId. Scalar slot N = entity index N + 1
2283 // pairs with vk[N] in the batchMul block below.
2284
2285 // 0: SIGMA1_EVAL_LOC
2286 mstore(BATCH_SCALAR_1_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2287 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA1_EVAL_LOC), batching_challenge, p), p)
2288 batching_challenge := mulmod(batching_challenge, rho, p)
2289
2290 // 1: SIGMA2_EVAL_LOC
2291 mstore(BATCH_SCALAR_2_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2292 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA2_EVAL_LOC), batching_challenge, p), p)
2293 batching_challenge := mulmod(batching_challenge, rho, p)
2294
2295 // 2: SIGMA3_EVAL_LOC
2296 mstore(BATCH_SCALAR_3_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2297 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA3_EVAL_LOC), batching_challenge, p), p)
2298 batching_challenge := mulmod(batching_challenge, rho, p)
2299
2300 // 3: SIGMA4_EVAL_LOC
2301 mstore(BATCH_SCALAR_4_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2302 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA4_EVAL_LOC), batching_challenge, p), p)
2303 batching_challenge := mulmod(batching_challenge, rho, p)
2304
2305 // 4: ID1_EVAL_LOC
2306 mstore(BATCH_SCALAR_5_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2307 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID1_EVAL_LOC), batching_challenge, p), p)
2308 batching_challenge := mulmod(batching_challenge, rho, p)
2309
2310 // 5: ID2_EVAL_LOC
2311 mstore(BATCH_SCALAR_6_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2312 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID2_EVAL_LOC), batching_challenge, p), p)
2313 batching_challenge := mulmod(batching_challenge, rho, p)
2314
2315 // 6: ID3_EVAL_LOC
2316 mstore(BATCH_SCALAR_7_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2317 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID3_EVAL_LOC), batching_challenge, p), p)
2318 batching_challenge := mulmod(batching_challenge, rho, p)
2319
2320 // 7: ID4_EVAL_LOC
2321 mstore(BATCH_SCALAR_8_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2322 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID4_EVAL_LOC), batching_challenge, p), p)
2323 batching_challenge := mulmod(batching_challenge, rho, p)
2324
2325 // 8: LAGRANGE_FIRST_EVAL_LOC
2326 mstore(BATCH_SCALAR_9_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2327 batched_evaluation := addmod(batched_evaluation, mulmod(mload(LAGRANGE_FIRST_EVAL_LOC), batching_challenge, p), p)
2328 batching_challenge := mulmod(batching_challenge, rho, p)
2329
2330 // 9: LAGRANGE_LAST_EVAL_LOC
2331 mstore(BATCH_SCALAR_10_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2332 batched_evaluation := addmod(batched_evaluation, mulmod(mload(LAGRANGE_LAST_EVAL_LOC), batching_challenge, p), p)
2333 batching_challenge := mulmod(batching_challenge, rho, p)
2334
2335 // 10: QLOOKUP_EVAL_LOC
2336 mstore(BATCH_SCALAR_11_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2337 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QLOOKUP_EVAL_LOC), batching_challenge, p), p)
2338 batching_challenge := mulmod(batching_challenge, rho, p)
2339
2340 // 11: TABLE1_EVAL_LOC
2341 mstore(BATCH_SCALAR_12_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2342 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE1_EVAL_LOC), batching_challenge, p), p)
2343 batching_challenge := mulmod(batching_challenge, rho, p)
2344
2345 // 12: TABLE2_EVAL_LOC
2346 mstore(BATCH_SCALAR_13_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2347 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE2_EVAL_LOC), batching_challenge, p), p)
2348 batching_challenge := mulmod(batching_challenge, rho, p)
2349
2350 // 13: TABLE3_EVAL_LOC
2351 mstore(BATCH_SCALAR_14_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2352 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE3_EVAL_LOC), batching_challenge, p), p)
2353 batching_challenge := mulmod(batching_challenge, rho, p)
2354
2355 // 14: TABLE4_EVAL_LOC
2356 mstore(BATCH_SCALAR_15_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2357 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE4_EVAL_LOC), batching_challenge, p), p)
2358 batching_challenge := mulmod(batching_challenge, rho, p)
2359
2360 // 15: QM_EVAL_LOC
2361 mstore(BATCH_SCALAR_16_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2362 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QM_EVAL_LOC), batching_challenge, p), p)
2363 batching_challenge := mulmod(batching_challenge, rho, p)
2364
2365 // 16: QR_EVAL_LOC
2366 mstore(BATCH_SCALAR_17_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2367 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QR_EVAL_LOC), batching_challenge, p), p)
2368 batching_challenge := mulmod(batching_challenge, rho, p)
2369
2370 // 17: QO_EVAL_LOC
2371 mstore(BATCH_SCALAR_18_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2372 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QO_EVAL_LOC), batching_challenge, p), p)
2373 batching_challenge := mulmod(batching_challenge, rho, p)
2374
2375 // 18: QC_EVAL_LOC
2376 mstore(BATCH_SCALAR_19_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2377 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QC_EVAL_LOC), batching_challenge, p), p)
2378 batching_challenge := mulmod(batching_challenge, rho, p)
2379
2380 // 19: QL_EVAL_LOC
2381 mstore(BATCH_SCALAR_20_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2382 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QL_EVAL_LOC), batching_challenge, p), p)
2383 batching_challenge := mulmod(batching_challenge, rho, p)
2384
2385 // 20: Q4_EVAL_LOC
2386 mstore(BATCH_SCALAR_21_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2387 batched_evaluation := addmod(batched_evaluation, mulmod(mload(Q4_EVAL_LOC), batching_challenge, p), p)
2388 batching_challenge := mulmod(batching_challenge, rho, p)
2389
2390 // 21: QARITH_EVAL_LOC
2391 mstore(BATCH_SCALAR_22_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2392 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QARITH_EVAL_LOC), batching_challenge, p), p)
2393 batching_challenge := mulmod(batching_challenge, rho, p)
2394
2395 // 22: QRANGE_EVAL_LOC
2396 mstore(BATCH_SCALAR_23_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2397 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QRANGE_EVAL_LOC), batching_challenge, p), p)
2398 batching_challenge := mulmod(batching_challenge, rho, p)
2399
2400 // 23: QELLIPTIC_EVAL_LOC
2401 mstore(BATCH_SCALAR_24_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2402 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QELLIPTIC_EVAL_LOC), batching_challenge, p), p)
2403 batching_challenge := mulmod(batching_challenge, rho, p)
2404
2405 // 24: QMEMORY_EVAL_LOC
2406 mstore(BATCH_SCALAR_25_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2407 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QMEMORY_EVAL_LOC), batching_challenge, p), p)
2408 batching_challenge := mulmod(batching_challenge, rho, p)
2409
2410 // 25: QNNF_EVAL_LOC
2411 mstore(BATCH_SCALAR_26_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2412 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QNNF_EVAL_LOC), batching_challenge, p), p)
2413 batching_challenge := mulmod(batching_challenge, rho, p)
2414
2415 // 26: QPOSEIDON2_EXTERNAL_EVAL_LOC
2416 mstore(BATCH_SCALAR_27_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2417 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QPOSEIDON2_EXTERNAL_EVAL_LOC), batching_challenge, p), p)
2418 batching_challenge := mulmod(batching_challenge, rho, p)
2419
2420 // 27: QPOSEIDON2_INTERNAL_EVAL_LOC
2421 mstore(BATCH_SCALAR_28_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2422 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QPOSEIDON2_INTERNAL_EVAL_LOC), batching_challenge, p), p)
2423 batching_challenge := mulmod(batching_challenge, rho, p)
2424
2425 // 28: W1_EVAL_LOC
2426 mstore(BATCH_SCALAR_29_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2427 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W1_EVAL_LOC), batching_challenge, p), p)
2428 batching_challenge := mulmod(batching_challenge, rho, p)
2429
2430 // 29: W2_EVAL_LOC
2431 mstore(BATCH_SCALAR_30_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2432 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W2_EVAL_LOC), batching_challenge, p), p)
2433 batching_challenge := mulmod(batching_challenge, rho, p)
2434
2435 // 30: W3_EVAL_LOC
2436 mstore(BATCH_SCALAR_31_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2437 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W3_EVAL_LOC), batching_challenge, p), p)
2438 batching_challenge := mulmod(batching_challenge, rho, p)
2439
2440 // 31: W4_EVAL_LOC
2441 mstore(BATCH_SCALAR_32_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2442 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W4_EVAL_LOC), batching_challenge, p), p)
2443 batching_challenge := mulmod(batching_challenge, rho, p)
2444
2445 // 32: Z_PERM_EVAL_LOC
2446 mstore(BATCH_SCALAR_33_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2447 batched_evaluation := addmod(batched_evaluation, mulmod(mload(Z_PERM_EVAL_LOC), batching_challenge, p), p)
2448 batching_challenge := mulmod(batching_challenge, rho, p)
2449
2450 // 33: LOOKUP_INVERSES_EVAL_LOC
2451 mstore(BATCH_SCALAR_34_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2452 batched_evaluation := addmod(batched_evaluation, mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), batching_challenge, p), p)
2453 batching_challenge := mulmod(batching_challenge, rho, p)
2454
2455 // 34: LOOKUP_READ_COUNTS_EVAL_LOC
2456 mstore(BATCH_SCALAR_35_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2457 batched_evaluation := addmod(batched_evaluation, mulmod(mload(LOOKUP_READ_COUNTS_EVAL_LOC), batching_challenge, p), p)
2458 batching_challenge := mulmod(batching_challenge, rho, p)
2459
2460 // 35: LOOKUP_READ_TAGS_EVAL_LOC
2461 mstore(BATCH_SCALAR_36_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2462 batched_evaluation := addmod(batched_evaluation, mulmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), batching_challenge, p), p)
2463 batching_challenge := mulmod(batching_challenge, rho, p)
2464
2465 // Unrolled for NUMBER_OF_SHIFTED_ENTITIES = 5
2466 // for (uint256 i = NUMBER_UNSHIFTED + 1; i <= NUMBER_OF_ENTITIES; ++i) {
2467 // scalars[i] = mem.shiftedScalar.neg() * mem.batchingChallenge;
2468 // mem.batchedEvaluation = mem.batchedEvaluation + (proof.sumcheckEvaluations[i - 1] * mem.batchingChallenge);
2469 // mem.batchingChallenge = mem.batchingChallenge * tp.rho;
2470 // }
2471
2472 // 28: W1_EVAL_LOC
2473 mstore(
2474 BATCH_SCALAR_29_LOC,
2475 addmod(mload(BATCH_SCALAR_29_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2476 )
2477 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W1_SHIFT_EVAL_LOC), batching_challenge, p), p)
2478 batching_challenge := mulmod(batching_challenge, rho, p)
2479
2480 // 29: W2_EVAL_LOC
2481 mstore(
2482 BATCH_SCALAR_30_LOC,
2483 addmod(mload(BATCH_SCALAR_30_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2484 )
2485 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W2_SHIFT_EVAL_LOC), batching_challenge, p), p)
2486 batching_challenge := mulmod(batching_challenge, rho, p)
2487
2488 // 30: W3_EVAL_LOC
2489 mstore(
2490 BATCH_SCALAR_31_LOC,
2491 addmod(mload(BATCH_SCALAR_31_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2492 )
2493 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W3_SHIFT_EVAL_LOC), batching_challenge, p), p)
2494 batching_challenge := mulmod(batching_challenge, rho, p)
2495
2496 // 31: W4_EVAL_LOC
2497 mstore(
2498 BATCH_SCALAR_32_LOC,
2499 addmod(mload(BATCH_SCALAR_32_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2500 )
2501 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W4_SHIFT_EVAL_LOC), batching_challenge, p), p)
2502 batching_challenge := mulmod(batching_challenge, rho, p)
2503
2504 // 32: Z_PERM_EVAL_LOC
2505 mstore(
2506 BATCH_SCALAR_33_LOC,
2507 addmod(mload(BATCH_SCALAR_33_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2508 )
2509 batched_evaluation := addmod(
2510 batched_evaluation,
2511 mulmod(mload(Z_PERM_SHIFT_EVAL_LOC), batching_challenge, p),
2512 p
2513 )
2514 batching_challenge := mulmod(batching_challenge, rho, p)
2515
2516 // Compute fold pos evaluations
2517 {
2518 mstore(CHALL_POW_LOC, POWERS_OF_EVALUATION_CHALLENGE_{{ LOG_N_MINUS_ONE }}_LOC)
2519 mstore(SUMCHECK_U_LOC, SUM_U_CHALLENGE_{{ LOG_N_MINUS_ONE }})
2520 mstore(GEMINI_A_LOC, GEMINI_A_EVAL_{{ LOG_N_MINUS_ONE }})
2521 // Inversion of this value was included in batch inversion above
2522 let inverted_chall_pow_minus_u_loc := INVERTED_CHALLENGE_POW_MINUS_U_{{ LOG_N_MINUS_ONE }}_LOC
2523 let fold_pos_off := FOLD_POS_EVALUATIONS_{{ LOG_N_MINUS_ONE }}_LOC
2524
2525 let batchedEvalAcc := batched_evaluation
2526 for { let i := LOG_N } gt(i, 0) { i := sub(i, 1) } {
2527 let chall_pow := mload(mload(CHALL_POW_LOC))
2528 let sum_check_u := mload(mload(SUMCHECK_U_LOC))
2529
2530 // challengePower * batchedEvalAccumulator * 2
2531 let batchedEvalRoundAcc := mulmod(chall_pow, mulmod(batchedEvalAcc, 2, p), p)
2532 // (challengePower * (ONE - u) - u)
2533 let chall_pow_times_1_minus_u := mulmod(chall_pow, addmod(1, sub(p, sum_check_u), p), p)
2534
2535 batchedEvalRoundAcc := addmod(
2536 batchedEvalRoundAcc,
2537 sub(
2538 p,
2539 mulmod(
2540 mload(mload(GEMINI_A_LOC)),
2541 addmod(chall_pow_times_1_minus_u, sub(p, sum_check_u), p),
2542 p
2543 )
2544 ),
2545 p
2546 )
2547
2548 batchedEvalRoundAcc := mulmod(batchedEvalRoundAcc, mload(inverted_chall_pow_minus_u_loc), p)
2549
2550 batchedEvalAcc := batchedEvalRoundAcc
2551 mstore(fold_pos_off, batchedEvalRoundAcc)
2552
2553 mstore(CHALL_POW_LOC, sub(mload(CHALL_POW_LOC), 0x20))
2554 mstore(SUMCHECK_U_LOC, sub(mload(SUMCHECK_U_LOC), 0x20))
2555 mstore(GEMINI_A_LOC, sub(mload(GEMINI_A_LOC), 0x20))
2556 inverted_chall_pow_minus_u_loc := sub(inverted_chall_pow_minus_u_loc, 0x20)
2557 fold_pos_off := sub(fold_pos_off, 0x20)
2558 }
2559 }
2560
2561 let constant_term_acc := mulmod(mload(FOLD_POS_EVALUATIONS_0_LOC), mload(POS_INVERTED_DENOM_0_LOC), p)
2562 {
2563 let shplonk_nu := mload(SHPLONK_NU_CHALLENGE)
2564
2565 constant_term_acc := addmod(
2566 constant_term_acc,
2567 mulmod(mload(GEMINI_A_EVAL_0), mulmod(shplonk_nu, mload(NEG_INVERTED_DENOM_0_LOC), p), p),
2568 p
2569 )
2570
2571 let shplonk_nu_sqr := mulmod(shplonk_nu, shplonk_nu, p)
2572 batching_challenge := shplonk_nu_sqr
2573
2574 mstore(SS_POS_INV_DENOM_LOC, POS_INVERTED_DENOM_1_LOC)
2575 mstore(SS_NEG_INV_DENOM_LOC, NEG_INVERTED_DENOM_1_LOC)
2576
2577 mstore(SS_GEMINI_EVALS_LOC, GEMINI_A_EVAL_1)
2578 let fold_pos_evals_loc := FOLD_POS_EVALUATIONS_1_LOC
2579
2580 let scalars_loc := BATCH_SCALAR_37_LOC
2581
2582 for { let i := 0 } lt(i, sub(LOG_N, 1)) { i := add(i, 1) } {
2583 let scaling_factor_pos := mulmod(batching_challenge, mload(mload(SS_POS_INV_DENOM_LOC)), p)
2584 let scaling_factor_neg :=
2585 mulmod(batching_challenge, mulmod(shplonk_nu, mload(mload(SS_NEG_INV_DENOM_LOC)), p), p)
2586
2587 mstore(scalars_loc, addmod(sub(p, scaling_factor_neg), sub(p, scaling_factor_pos), p))
2588
2589 let accum_contribution := mulmod(scaling_factor_neg, mload(mload(SS_GEMINI_EVALS_LOC)), p)
2590 accum_contribution := addmod(
2591 accum_contribution,
2592 mulmod(scaling_factor_pos, mload(fold_pos_evals_loc), p),
2593 p
2594 )
2595
2596 constant_term_acc := addmod(constant_term_acc, accum_contribution, p)
2597
2598 batching_challenge := mulmod(batching_challenge, shplonk_nu_sqr, p)
2599
2600 mstore(SS_POS_INV_DENOM_LOC, add(mload(SS_POS_INV_DENOM_LOC), 0x20))
2601 mstore(SS_NEG_INV_DENOM_LOC, add(mload(SS_NEG_INV_DENOM_LOC), 0x20))
2602 mstore(SS_GEMINI_EVALS_LOC, add(mload(SS_GEMINI_EVALS_LOC), 0x20))
2603 fold_pos_evals_loc := add(fold_pos_evals_loc, 0x20)
2604 scalars_loc := add(scalars_loc, 0x20)
2605 }
2606 }
2607
2608 let precomp_success_flag := 1
2609 let q := Q // EC group order
2610 {
2611 // The initial accumulator = 1 * shplonk_q
2612 mcopy(ACCUMULATOR, SHPLONK_Q_X_LOC, 0x40)
2613 }
2614
2615 // Accumulate vk points
2616 loadVk()
2617 {
2618 // VK batchMul order matches UltraFlavor_Generated::EntityId precomputed layout.
2619 // Accumulator = accumulator + scalar[1] * vk[0] (sigma_1)
2620 mcopy(G1_LOCATION, SIGMA_1_X_LOC, 0x40)
2621 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_1_LOC))
2622 precomp_success_flag := and(
2623 precomp_success_flag,
2624 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2625 )
2626 precomp_success_flag := and(
2627 precomp_success_flag,
2628 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2629 )
2630
2631 // Accumulator = accumulator + scalar[2] * vk[1] (sigma_2)
2632 mcopy(G1_LOCATION, SIGMA_2_X_LOC, 0x40)
2633 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_2_LOC))
2634 precomp_success_flag := and(
2635 precomp_success_flag,
2636 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2637 )
2638 precomp_success_flag := and(
2639 precomp_success_flag,
2640 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2641 )
2642
2643 // Accumulator = accumulator + scalar[3] * vk[2] (sigma_3)
2644 mcopy(G1_LOCATION, SIGMA_3_X_LOC, 0x40)
2645 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_3_LOC))
2646 precomp_success_flag := and(
2647 precomp_success_flag,
2648 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2649 )
2650 precomp_success_flag := and(
2651 precomp_success_flag,
2652 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2653 )
2654
2655 // Accumulator = accumulator + scalar[4] * vk[3] (sigma_4)
2656 mcopy(G1_LOCATION, SIGMA_4_X_LOC, 0x40)
2657 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_4_LOC))
2658 precomp_success_flag := and(
2659 precomp_success_flag,
2660 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2661 )
2662 precomp_success_flag := and(
2663 precomp_success_flag,
2664 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2665 )
2666
2667 // Accumulator = accumulator + scalar[5] * vk[4] (id_1)
2668 mcopy(G1_LOCATION, ID_1_X_LOC, 0x40)
2669 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_5_LOC))
2670 precomp_success_flag := and(
2671 precomp_success_flag,
2672 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2673 )
2674 precomp_success_flag := and(
2675 precomp_success_flag,
2676 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2677 )
2678
2679 // Accumulator = accumulator + scalar[6] * vk[5] (id_2)
2680 mcopy(G1_LOCATION, ID_2_X_LOC, 0x40)
2681 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_6_LOC))
2682 precomp_success_flag := and(
2683 precomp_success_flag,
2684 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2685 )
2686 precomp_success_flag := and(
2687 precomp_success_flag,
2688 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2689 )
2690
2691 // Accumulator = accumulator + scalar[7] * vk[6] (id_3)
2692 mcopy(G1_LOCATION, ID_3_X_LOC, 0x40)
2693 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_7_LOC))
2694 precomp_success_flag := and(
2695 precomp_success_flag,
2696 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2697 )
2698 precomp_success_flag := and(
2699 precomp_success_flag,
2700 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2701 )
2702
2703 // Accumulator = accumulator + scalar[8] * vk[7] (id_4)
2704 mcopy(G1_LOCATION, ID_4_X_LOC, 0x40)
2705 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_8_LOC))
2706 precomp_success_flag := and(
2707 precomp_success_flag,
2708 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2709 )
2710 precomp_success_flag := and(
2711 precomp_success_flag,
2712 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2713 )
2714
2715 // Accumulator = accumulator + scalar[9] * vk[8] (lagrange_first)
2716 mcopy(G1_LOCATION, LAGRANGE_FIRST_X_LOC, 0x40)
2717 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_9_LOC))
2718 precomp_success_flag := and(
2719 precomp_success_flag,
2720 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2721 )
2722 precomp_success_flag := and(
2723 precomp_success_flag,
2724 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2725 )
2726
2727 // Accumulator = accumulator + scalar[10] * vk[9] (lagrange_last)
2728 mcopy(G1_LOCATION, LAGRANGE_LAST_X_LOC, 0x40)
2729 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_10_LOC))
2730 precomp_success_flag := and(
2731 precomp_success_flag,
2732 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2733 )
2734 precomp_success_flag := and(
2735 precomp_success_flag,
2736 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2737 )
2738
2739 // Accumulator = accumulator + scalar[11] * vk[10] (q_lookup)
2740 mcopy(G1_LOCATION, Q_LOOKUP_X_LOC, 0x40)
2741 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_11_LOC))
2742 precomp_success_flag := and(
2743 precomp_success_flag,
2744 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2745 )
2746 precomp_success_flag := and(
2747 precomp_success_flag,
2748 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2749 )
2750
2751 // Accumulator = accumulator + scalar[12] * vk[11] (table_1)
2752 mcopy(G1_LOCATION, TABLE_1_X_LOC, 0x40)
2753 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_12_LOC))
2754 precomp_success_flag := and(
2755 precomp_success_flag,
2756 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2757 )
2758 precomp_success_flag := and(
2759 precomp_success_flag,
2760 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2761 )
2762
2763 // Accumulator = accumulator + scalar[13] * vk[12] (table_2)
2764 mcopy(G1_LOCATION, TABLE_2_X_LOC, 0x40)
2765 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_13_LOC))
2766 precomp_success_flag := and(
2767 precomp_success_flag,
2768 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2769 )
2770 precomp_success_flag := and(
2771 precomp_success_flag,
2772 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2773 )
2774
2775 // Accumulator = accumulator + scalar[14] * vk[13] (table_3)
2776 mcopy(G1_LOCATION, TABLE_3_X_LOC, 0x40)
2777 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_14_LOC))
2778 precomp_success_flag := and(
2779 precomp_success_flag,
2780 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2781 )
2782 precomp_success_flag := and(
2783 precomp_success_flag,
2784 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2785 )
2786
2787 // Accumulator = accumulator + scalar[15] * vk[14] (table_4)
2788 mcopy(G1_LOCATION, TABLE_4_X_LOC, 0x40)
2789 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_15_LOC))
2790 precomp_success_flag := and(
2791 precomp_success_flag,
2792 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2793 )
2794 precomp_success_flag := and(
2795 precomp_success_flag,
2796 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2797 )
2798
2799 // Accumulator = accumulator + scalar[16] * vk[15] (q_m)
2800 mcopy(G1_LOCATION, Q_M_X_LOC, 0x40)
2801 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_16_LOC))
2802 precomp_success_flag := and(
2803 precomp_success_flag,
2804 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2805 )
2806 precomp_success_flag := and(
2807 precomp_success_flag,
2808 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2809 )
2810
2811 // Accumulator = accumulator + scalar[17] * vk[16] (q_r)
2812 mcopy(G1_LOCATION, Q_R_X_LOC, 0x40)
2813 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_17_LOC))
2814 precomp_success_flag := and(
2815 precomp_success_flag,
2816 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2817 )
2818 precomp_success_flag := and(
2819 precomp_success_flag,
2820 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2821 )
2822
2823 // Accumulator = accumulator + scalar[18] * vk[17] (q_o)
2824 mcopy(G1_LOCATION, Q_O_X_LOC, 0x40)
2825 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_18_LOC))
2826 precomp_success_flag := and(
2827 precomp_success_flag,
2828 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2829 )
2830 precomp_success_flag := and(
2831 precomp_success_flag,
2832 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2833 )
2834
2835 // Accumulator = accumulator + scalar[19] * vk[18] (q_c)
2836 mcopy(G1_LOCATION, Q_C_X_LOC, 0x40)
2837 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_19_LOC))
2838 precomp_success_flag := and(
2839 precomp_success_flag,
2840 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2841 )
2842 precomp_success_flag := and(
2843 precomp_success_flag,
2844 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2845 )
2846
2847 // Accumulator = accumulator + scalar[20] * vk[19] (q_l)
2848 mcopy(G1_LOCATION, Q_L_X_LOC, 0x40)
2849 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_20_LOC))
2850 precomp_success_flag := and(
2851 precomp_success_flag,
2852 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2853 )
2854 precomp_success_flag := and(
2855 precomp_success_flag,
2856 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2857 )
2858
2859 // Accumulator = accumulator + scalar[21] * vk[20] (q_4)
2860 mcopy(G1_LOCATION, Q_4_X_LOC, 0x40)
2861 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_21_LOC))
2862 precomp_success_flag := and(
2863 precomp_success_flag,
2864 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2865 )
2866 precomp_success_flag := and(
2867 precomp_success_flag,
2868 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2869 )
2870
2871 // Accumulator = accumulator + scalar[22] * vk[21] (q_arith)
2872 mcopy(G1_LOCATION, Q_ARITH_X_LOC, 0x40)
2873 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_22_LOC))
2874 precomp_success_flag := and(
2875 precomp_success_flag,
2876 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2877 )
2878 precomp_success_flag := and(
2879 precomp_success_flag,
2880 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2881 )
2882
2883 // Accumulator = accumulator + scalar[23] * vk[22] (q_delta_range)
2884 mcopy(G1_LOCATION, Q_DELTA_RANGE_X_LOC, 0x40)
2885 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_23_LOC))
2886 precomp_success_flag := and(
2887 precomp_success_flag,
2888 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2889 )
2890 precomp_success_flag := and(
2891 precomp_success_flag,
2892 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2893 )
2894
2895 // Accumulator = accumulator + scalar[24] * vk[23] (q_elliptic)
2896 mcopy(G1_LOCATION, Q_ELLIPTIC_X_LOC, 0x40)
2897 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_24_LOC))
2898 precomp_success_flag := and(
2899 precomp_success_flag,
2900 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2901 )
2902 precomp_success_flag := and(
2903 precomp_success_flag,
2904 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2905 )
2906
2907 // Accumulator = accumulator + scalar[25] * vk[24] (q_memory)
2908 mcopy(G1_LOCATION, Q_MEMORY_X_LOC, 0x40)
2909 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_25_LOC))
2910 precomp_success_flag := and(
2911 precomp_success_flag,
2912 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2913 )
2914 precomp_success_flag := and(
2915 precomp_success_flag,
2916 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2917 )
2918
2919 // Accumulator = accumulator + scalar[26] * vk[25] (q_nnf)
2920 mcopy(G1_LOCATION, Q_NNF_X_LOC, 0x40)
2921 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_26_LOC))
2922 precomp_success_flag := and(
2923 precomp_success_flag,
2924 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2925 )
2926 precomp_success_flag := and(
2927 precomp_success_flag,
2928 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2929 )
2930
2931 // Accumulator = accumulator + scalar[27] * vk[26] (q_poseidon2_external)
2932 mcopy(G1_LOCATION, Q_POSEIDON_2_EXTERNAL_X_LOC, 0x40)
2933 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_27_LOC))
2934 precomp_success_flag := and(
2935 precomp_success_flag,
2936 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2937 )
2938 precomp_success_flag := and(
2939 precomp_success_flag,
2940 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2941 )
2942
2943 // Accumulator = accumulator + scalar[28] * vk[27] (q_poseidon2_internal)
2944 mcopy(G1_LOCATION, Q_POSEIDON_2_INTERNAL_X_LOC, 0x40)
2945 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_28_LOC))
2946 precomp_success_flag := and(
2947 precomp_success_flag,
2948 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2949 )
2950 precomp_success_flag := and(
2951 precomp_success_flag,
2952 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2953 )
2954
2955 // Accumulator = accumulator + constant_term_acc * G (generator)
2956 mstore(G1_LOCATION, 0x01) // G1 generator x
2957 mstore(add(G1_LOCATION, 0x20), 0x02) // G1 generator y
2958 mstore(SCALAR_LOCATION, constant_term_acc)
2959 precomp_success_flag := and(
2960 precomp_success_flag,
2961 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2962 )
2963 precomp_success_flag := and(
2964 precomp_success_flag,
2965 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2966 )
2967
2968 // Accumulate proof points
2969 // Accumulator = accumulator + scalar[29] * w_l
2970 mcopy(G1_LOCATION, W_L_X_LOC, 0x40)
2971 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_29_LOC))
2972 precomp_success_flag := and(
2973 precomp_success_flag,
2974 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2975 )
2976 precomp_success_flag := and(
2977 precomp_success_flag,
2978 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2979 )
2980
2981 // Accumulator = accumulator + scalar[30] * w_r
2982 mcopy(G1_LOCATION, W_R_X_LOC, 0x40)
2983 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_30_LOC))
2984 precomp_success_flag := and(
2985 precomp_success_flag,
2986 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2987 )
2988 precomp_success_flag := and(
2989 precomp_success_flag,
2990 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2991 )
2992
2993 // Accumulator = accumulator + scalar[31] * w_o
2994 mcopy(G1_LOCATION, W_O_X_LOC, 0x40)
2995 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_31_LOC))
2996 precomp_success_flag := and(
2997 precomp_success_flag,
2998 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2999 )
3000 precomp_success_flag := and(
3001 precomp_success_flag,
3002 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3003 )
3004
3005 // Accumulator = accumulator + scalar[32] * w_4
3006 mcopy(G1_LOCATION, W_4_X_LOC, 0x40)
3007 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_32_LOC))
3008 precomp_success_flag := and(
3009 precomp_success_flag,
3010 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3011 )
3012 precomp_success_flag := and(
3013 precomp_success_flag,
3014 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3015 )
3016
3017 // Accumulator = accumulator + scalar[33] * z_perm
3018 mcopy(G1_LOCATION, Z_PERM_X_LOC, 0x40)
3019 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_33_LOC))
3020 precomp_success_flag := and(
3021 precomp_success_flag,
3022 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3023 )
3024 precomp_success_flag := and(
3025 precomp_success_flag,
3026 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3027 )
3028
3029 // Accumulator = accumulator + scalar[34] * lookup_inverses
3030 mcopy(G1_LOCATION, LOOKUP_INVERSES_X_LOC, 0x40)
3031 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_34_LOC))
3032 precomp_success_flag := and(
3033 precomp_success_flag,
3034 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3035 )
3036 precomp_success_flag := and(
3037 precomp_success_flag,
3038 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3039 )
3040
3041 // Accumulator = accumulator + scalar[35] * lookup_read_counts
3042 mcopy(G1_LOCATION, LOOKUP_READ_COUNTS_X_LOC, 0x40)
3043 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_35_LOC))
3044 precomp_success_flag := and(
3045 precomp_success_flag,
3046 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3047 )
3048 precomp_success_flag := and(
3049 precomp_success_flag,
3050 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3051 )
3052
3053 // Accumulator = accumulator + scalar[36] * lookup_read_tags
3054 mcopy(G1_LOCATION, LOOKUP_READ_TAGS_X_LOC, 0x40)
3055 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_36_LOC))
3056 precomp_success_flag := and(
3057 precomp_success_flag,
3058 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3059 )
3060 precomp_success_flag := and(
3061 precomp_success_flag,
3062 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3063 )
3064
3065 // Accumulate these LOG_N scalars with the gemini fold univariates
3066 {
3067 {
3070 }
3071 }
3072
3073 {
3074 // Accumulate final quotient commitment into shplonk check
3075 // Accumulator = accumulator + shplonkZ * quotient commitment
3076 mcopy(G1_LOCATION, KZG_QUOTIENT_X_LOC, 0x40)
3077
3078 mstore(SCALAR_LOCATION, mload(SHPLONK_Z_CHALLENGE))
3079 precomp_success_flag := and(
3080 precomp_success_flag,
3081 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3082 )
3083 precomp_success_flag := and(
3084 precomp_success_flag,
3085 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3086 )
3087 }
3088
3089 // All G1 points were validated on-curve during input validation.
3090 // precomp_success_flag now only tracks ecAdd/ecMul precompile success.
3091 if iszero(precomp_success_flag) {
3092 mstore(0x00, SHPLEMINI_FAILED_SELECTOR)
3093 revert(0x00, 0x04)
3094 }
3095
3096 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3097 /* SHPLEMINI - complete */
3098 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3099
3100 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3101 /* PAIRING CHECK */
3102 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3103 {
3104 // P_1
3105 mstore(0xc0, mload(KZG_QUOTIENT_X_LOC))
3106 mstore(0xe0, sub(q, mload(KZG_QUOTIENT_Y_LOC)))
3107
3108 // p_0_agg
3109 // 0x80 - p_0_agg x
3110 // 0xa0 - p_0_agg y
3111 mcopy(0x80, ACCUMULATOR, 0x40)
3112
3113 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3114 /* PAIRING AGGREGATION */
3115 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3116 // Read the pairing encoded in the first 8 field elements of the proof (2 limbs per coordinate)
3117 let p0_other_x := mload(PAIRING_POINT_0_X_0_LOC)
3118 p0_other_x := or(shl(136, mload(PAIRING_POINT_0_X_1_LOC)), p0_other_x)
3119
3120 let p0_other_y := mload(PAIRING_POINT_0_Y_0_LOC)
3121 p0_other_y := or(shl(136, mload(PAIRING_POINT_0_Y_1_LOC)), p0_other_y)
3122
3123 let p1_other_x := mload(PAIRING_POINT_1_X_0_LOC)
3124 p1_other_x := or(shl(136, mload(PAIRING_POINT_1_X_1_LOC)), p1_other_x)
3125
3126 let p1_other_y := mload(PAIRING_POINT_1_Y_0_LOC)
3127 p1_other_y := or(shl(136, mload(PAIRING_POINT_1_Y_1_LOC)), p1_other_y)
3128
3129 // Check if pairing points are default (all zero = infinity = no recursive verification)
3130 let pairing_points_are_default := iszero(or(or(p0_other_x, p0_other_y), or(p1_other_x, p1_other_y)))
3131
3132 let success := 1
3133 // Only aggregate if pairing points are non-default
3134 if iszero(pairing_points_are_default) {
3135 // Reconstructed coordinates must be < Q to prevent malleability
3136 if iszero(and(
3137 and(lt(p0_other_x, q), lt(p0_other_y, q)),
3138 and(lt(p1_other_x, q), lt(p1_other_y, q))
3139 )) {
3140 mstore(0x00, VALUE_GE_GROUP_ORDER_SELECTOR)
3141 revert(0x00, 0x04)
3142 }
3143
3144 // Validate p_0_other not point of infinity
3145 success := iszero(iszero(or(p0_other_x, p0_other_y)))
3146 // Validate p_1_other not point of infinity
3147 success := and(success, iszero(iszero(or(p1_other_x, p1_other_y))))
3148
3149 // p_0
3150 mstore(0x00, p0_other_x)
3151 mstore(0x20, p0_other_y)
3152
3153 // p_1
3154 mstore(0x40, p1_other_x)
3155 mstore(0x60, p1_other_y)
3156
3157 // p_1_agg is already in the correct location
3158
3159 let recursion_separator := keccak256(0x00, 0x100)
3160
3161 // Write separator back to scratch space
3162 mstore(0x00, p0_other_x)
3163
3164 mstore(0x40, recursion_separator)
3165 // recursion_separator * p_0_other
3166 success := and(success, staticcall(gas(), 0x07, 0x00, 0x60, 0x00, 0x40))
3167
3168 // (recursion_separator * p_0_other) + p_0_agg
3169 mcopy(0x40, 0x80, 0x40)
3170 // p_0 = (recursion_separator * p_0_other) + p_0_agg
3171 success := and(success, staticcall(gas(), 6, 0x00, 0x80, 0x00, 0x40))
3172
3173 mstore(0x40, p1_other_x)
3174 mstore(0x60, p1_other_y)
3175 mstore(0x80, recursion_separator)
3176
3177 success := and(success, staticcall(gas(), 7, 0x40, 0x60, 0x40, 0x40))
3178
3179 // Write p_1_agg back to scratch space
3180 mcopy(0x80, 0xc0, 0x40)
3181
3182 // 0xc0 - (recursion_separator * p_1_other) + p_1_agg
3183 success := and(success, staticcall(gas(), 6, 0x40, 0x80, 0xc0, 0x40))
3184 }
3185 // If default pairing points, use p_0_agg and p_1_agg directly (already at 0x80, 0xc0)
3186 if pairing_points_are_default {
3187 // Copy p_0_agg to 0x00 for pairing input
3188 mcopy(0x00, 0x80, 0x40)
3189 // p_1_agg stays at 0xc0
3190 }
3191
3192 // G2 [1]
3193 mstore(0x40, 0x198e9393920d483a7260bfb731fb5d25f1aa493335a9e71297e485b7aef312c2)
3194 mstore(0x60, 0x1800deef121f1e76426a00665e5c4479674322d4f75edadd46debd5cd992f6ed)
3195 mstore(0x80, 0x090689d0585ff075ec9e99ad690c3395bc4b313370b38ef355acdadcd122975b)
3196 mstore(0xa0, 0x12c85ea5db8c6deb4aab71808dcb408fe3d1e7690c43d37b4ce6cc0166fa7daa)
3197
3198 // G2 [x]
3199 mstore(0x100, 0x260e01b251f6f1c7e7ff4e580791dee8ea51d87a358e038b4efe30fac09383c1)
3200 mstore(0x120, 0x0118c4d5b837bcc2bc89b5b398b5974e9f5944073b32078b7e231fec938883b0)
3201 mstore(0x140, 0x04fc6369f7110fe3d25156c1bb9a72859cf2a04641f99ba4ee413c80da6a5fe4)
3202 mstore(0x160, 0x22febda3c0c0632a56475b4214e5615e11e6dd3f96e6cea2854a87d4dacc5e55)
3203
3204 let pairing_success := and(success, staticcall(gas(), 8, 0x00, 0x180, 0x00, 0x20))
3205 if iszero(and(pairing_success, mload(0x00))) {
3206 mstore(0x00, SHPLEMINI_FAILED_SELECTOR)
3207 revert(0x00, 0x04)
3208 }
3209
3210 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3211 /* PAIRING CHECK - Complete */
3212 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3213 }
3214 {
3215 mstore(0x00, 0x01)
3216 return(0x00, 0x20) // Proof succeeded!
3217 }
3218 }
3219 }
3220 }
3221}
3222)";
3223
3224inline std::string get_optimized_honk_solidity_verifier(auto const& verification_key)
3225{
3226 std::string template_str = HONK_CONTRACT_OPT_SOURCE;
3227
3228 apply_template_params(template_str, verification_key, /*is_zk=*/false);
3229
3230 // Replace UNROLL_SECTION blocks
3231 int log_n = static_cast<int>(verification_key->log_circuit_size);
3232 UnrollConfig unroll_config{
3233 .batch_scalar_offset = 37,
3234 };
3235
3236 replace_unroll_section(template_str, "POWERS_OF_EVALUATION_COMPUTATION", log_n, unroll_config);
3237 replace_unroll_section(template_str, "ACCUMULATE_INVERSES", log_n, unroll_config);
3238 replace_unroll_section(template_str, "COLLECT_INVERSES", log_n, unroll_config);
3239 replace_unroll_section(template_str, "ACCUMULATE_GEMINI_FOLD_UNIVARIATE", log_n, unroll_config);
3240
3241 MemoryLayoutConfig mem_config{
3243 .barycentric_domain_size = 8,
3244 .is_zk = false,
3245 };
3246 replace_memory_layout(template_str, log_n, mem_config);
3247
3248 return template_str;
3249}
void apply_template_params(std::string &template_str, VK const &verification_key, bool is_zk)
void replace_unroll_section(std::string &template_str, const std::string &section_name, int log_n, const UnrollConfig &config)
void replace_memory_layout(std::string &template_str, int log_n, const MemoryLayoutConfig &mem_config)
Find the memory layout tags then insert generated layout into the offsets.
std::string get_optimized_honk_solidity_verifier(auto const &verification_key)