Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
honk_zk_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
8
10#include <sstream>
11#include <vector>
12
13// Source code for the ZK optimized Ultrahonk Solidity verifier.
14// It's expected that the AcirComposer will inject a library which will load the verification key into memory.
15// NOLINTNEXTLINE(cppcoreguidelines-avoid-c-arrays)
16static const char HONK_ZK_CONTRACT_OPT_SOURCE[] = R"(
17// SPDX-License-Identifier: Apache-2.0
18// Copyright 2022 Aztec
19pragma solidity ^0.8.27;
20
21interface IVerifier {
22 function verify(bytes calldata _proof, bytes32[] calldata _publicInputs) external view returns (bool);
23}
24
25
26
27uint256 constant NUMBER_OF_SUBRELATIONS = 29;
28uint256 constant BATCHED_RELATION_PARTIAL_LENGTH = 9;
29uint256 constant ZK_BATCHED_RELATION_PARTIAL_LENGTH = 9;
30uint256 constant NUMBER_OF_ENTITIES = 42;
31uint256 constant NUMBER_UNSHIFTED = 37;
32uint256 constant NUMBER_TO_BE_SHIFTED = 5;
33uint256 constant PAIRING_POINTS_SIZE = 8;
34
35uint256 constant VK_HASH = {{ VK_HASH }};
36uint256 constant CIRCUIT_SIZE = {{ CIRCUIT_SIZE }};
37uint256 constant LOG_N = {{ LOG_CIRCUIT_SIZE }};
38uint256 constant NUMBER_PUBLIC_INPUTS = {{ NUM_PUBLIC_INPUTS }};
39uint256 constant REAL_NUMBER_PUBLIC_INPUTS = {{ REAL_NUM_PUBLIC_INPUTS }};
40uint256 constant PUBLIC_INPUTS_OFFSET = 5; // NUM_DISABLED_ROWS_IN_SUMCHECK + NUM_ZERO_ROWS = 4 + 1
41
42contract HonkVerifier is IVerifier {
43 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
44 /* SLAB ALLOCATION */
45 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
102 // {{ SECTION_START MEMORY_LAYOUT }}
103 // {{ SECTION_END MEMORY_LAYOUT }}
104
105 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
106 /* SUMCHECK - MEMORY ALIASES */
107 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
108 uint256 internal constant EC_X_1 = W2_EVAL_LOC;
109 uint256 internal constant EC_Y_1 = W3_EVAL_LOC;
110 uint256 internal constant EC_X_2 = W1_SHIFT_EVAL_LOC;
111 uint256 internal constant EC_Y_2 = W4_SHIFT_EVAL_LOC;
112 uint256 internal constant EC_Y_3 = W3_SHIFT_EVAL_LOC;
113 uint256 internal constant EC_X_3 = W2_SHIFT_EVAL_LOC;
114
115 // Aliases for selectors (Elliptic curve gadget)
116 uint256 internal constant EC_Q_SIGN = QL_EVAL_LOC;
117 uint256 internal constant EC_Q_IS_DOUBLE = QM_EVAL_LOC;
118
119 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
120 /* CONSTANTS */
121 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
122 uint256 internal constant GRUMPKIN_CURVE_B_PARAMETER_NEGATED = 17; // -(-17)
123
124 // Auxiliary relation constants
125 // In the Non Native Field Arithmetic Relation, large field elements are broken up into 4 LIMBs of 68 `LIMB_SIZE` bits each.
126 uint256 internal constant LIMB_SIZE = 0x100000000000000000; // 2<<68
127
128 // In the Delta Range Check Relation, there is a range checking relation that can validate 14-bit range checks with only 1
129 // extra relation in the execution trace.
130 // For large range checks, we decompose them into a collection of 14-bit range checks.
131 uint256 internal constant SUBLIMB_SHIFT = 0x4000; // 2<<14
132
133 // Poseidon2 internal constants
134 // https://github.com/HorizenLabs/poseidon2/blob/main/poseidon2_rust_params.sage - derivation code
135 uint256 internal constant POS_INTERNAL_MATRIX_D_0 =
136 0x10dc6e9c006ea38b04b1e03b4bd9490c0d03f98929ca1d7fb56821fd19d3b6e7;
137 uint256 internal constant POS_INTERNAL_MATRIX_D_1 =
138 0x0c28145b6a44df3e0149b3d0a30b3bb599df9756d4dd9b84a86b38cfb45a740b;
139 uint256 internal constant POS_INTERNAL_MATRIX_D_2 =
140 0x00544b8338791518b2c7645a50392798b21f75bb60e3596170067d00141cac15;
141 uint256 internal constant POS_INTERNAL_MATRIX_D_3 =
142 0x222c01175718386f2e2e82eb122789e352e105a3b8fa852613bc534433ee428b;
143
144 // Constants inspecting proof components
145 uint256 internal constant NUMBER_OF_UNSHIFTED_ENTITIES = 37;
146 // Shifted columns are columes that are duplicates of existing columns but right-shifted by 1
147 uint256 internal constant NUMBER_OF_SHIFTED_ENTITIES = 5;
148 uint256 internal constant TOTAL_NUMBER_OF_ENTITIES = 42;
149
150 // Constants for performing batch multiplication
151 uint256 internal constant ACCUMULATOR = 0x00;
152 uint256 internal constant ACCUMULATOR_2 = 0x40;
153 uint256 internal constant G1_LOCATION = 0x60;
154 uint256 internal constant G1_Y_LOCATION = 0x80;
155 uint256 internal constant SCALAR_LOCATION = 0xa0;
156
157 uint256 internal constant LOWER_127_MASK = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
158
159 // Group order
160 uint256 internal constant Q = 21888242871839275222246405745257275088696311157297823662689037894645226208583; // EC group order
161
162 // Field order constants
163 // -1/2 mod p
164 uint256 internal constant NEG_HALF_MODULO_P = 0x183227397098d014dc2822db40c0ac2e9419f4243cdcb848a1f0fac9f8000000;
165 uint256 internal constant P = 21888242871839275222246405745257275088548364400416034343698204186575808495617;
166 uint256 internal constant P_SUB_1 = 21888242871839275222246405745257275088548364400416034343698204186575808495616;
167 uint256 internal constant P_SUB_2 = 21888242871839275222246405745257275088548364400416034343698204186575808495615;
168 uint256 internal constant P_SUB_3 = 21888242871839275222246405745257275088548364400416034343698204186575808495614;
169
170 // Barycentric evaluation constants
171 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_0 =
172 0x0000000000000000000000000000000000000000000000000000000000009d80;
173 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_1 =
174 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593efffec51;
175 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_2 =
176 0x00000000000000000000000000000000000000000000000000000000000005a0;
177 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_3 =
178 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593effffd31;
179 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_4 =
180 0x0000000000000000000000000000000000000000000000000000000000000240;
181 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_5 =
182 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593effffd31;
183 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_6 =
184 0x00000000000000000000000000000000000000000000000000000000000005a0;
185 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_7 =
186 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593efffec51;
187 uint256 internal constant BARYCENTRIC_LAGRANGE_DENOMINATOR_8 =
188 0x0000000000000000000000000000000000000000000000000000000000009d80;
189
190 // ZK-specific constants
191 uint256 internal constant SUBGROUP_SIZE = 256;
192 uint256 internal constant SUBGROUP_GENERATOR = 0x07b0c561a6148404f086204a9f36ffb0617942546750f230c893619174a57a76;
193 uint256 internal constant SUBGROUP_GENERATOR_INVERSE = 0x204bd3277422fad364751ad938e2b5e6a54cf8c68712848a692c553d0329f5d6;
194 uint256 internal constant LIBRA_COMMITMENTS = 3;
195 uint256 internal constant LIBRA_EVALUATIONS = 4;
196 uint256 internal constant SHIFTED_COMMITMENTS_START = 30;
197
198 // Constants for computing public input delta
199 uint256 internal constant PERMUTATION_ARGUMENT_VALUE_SEPARATOR = 1 << 28;
200
201 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
202 /* ERRORS */
203 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
204 // The errors match Errors.sol
205
206 bytes4 internal constant VALUE_GE_LIMB_MAX_SELECTOR = 0xeb73e0bd;
207 bytes4 internal constant VALUE_GE_GROUP_ORDER_SELECTOR = 0x607be13e;
208 bytes4 internal constant VALUE_GE_FIELD_ORDER_SELECTOR = 0x20a33589;
209 bytes4 internal constant SUMCHECK_FAILED_SELECTOR = 0x9fc3a218;
210 bytes4 internal constant SHPLEMINI_FAILED_SELECTOR = 0xa5d82e8a;
211
212 bytes4 internal constant PROOF_LENGTH_WRONG_WITH_LOG_N_SELECTOR = 0x59895a53;
213 bytes4 internal constant PUBLIC_INPUTS_LENGTH_WRONG_SELECTOR = 0xfa066593;
214
215 bytes4 internal constant MODEXP_FAILED_SELECTOR = 0xf442f163;
216 bytes4 internal constant CONSISTENCY_CHECK_FAILED_SELECTOR = 0xa2a2ac83;
217 bytes4 internal constant GEMINI_CHALLENGE_IN_SUBGROUP_SELECTOR = 0x835eb8f7;
218
219 constructor() {}
220
221 function verify(
222 bytes calldata,
223 /*proof*/
224 bytes32[] calldata /*public_inputs*/
225 )
226 public
227 view
228 override
229 returns (bool)
230 {
231 // Load the proof from calldata in one large chunk
232 assembly {
233 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
234 /* LOAD VERIFCATION KEY */
235 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
236 // Write the verification key into memory
237 //
238 // Although defined at the top of the file, it is used towards the end of the algorithm when batching in the commitment scheme.
239 function loadVk() {
240 mstore(Q_L_X_LOC, {{ Q_L_X_LOC }})
241 mstore(Q_L_Y_LOC, {{ Q_L_Y_LOC }})
242 mstore(Q_R_X_LOC, {{ Q_R_X_LOC }})
243 mstore(Q_R_Y_LOC, {{ Q_R_Y_LOC }})
244 mstore(Q_O_X_LOC, {{ Q_O_X_LOC }})
245 mstore(Q_O_Y_LOC, {{ Q_O_Y_LOC }})
246 mstore(Q_4_X_LOC, {{ Q_4_X_LOC }})
247 mstore(Q_4_Y_LOC, {{ Q_4_Y_LOC }})
248 mstore(Q_M_X_LOC, {{ Q_M_X_LOC }})
249 mstore(Q_M_Y_LOC, {{ Q_M_Y_LOC }})
250 mstore(Q_C_X_LOC, {{ Q_C_X_LOC }})
251 mstore(Q_C_Y_LOC, {{ Q_C_Y_LOC }})
252 mstore(Q_LOOKUP_X_LOC, {{ Q_LOOKUP_X_LOC }})
253 mstore(Q_LOOKUP_Y_LOC, {{ Q_LOOKUP_Y_LOC }})
254 mstore(Q_ARITH_X_LOC, {{ Q_ARITH_X_LOC }})
255 mstore(Q_ARITH_Y_LOC, {{ Q_ARITH_Y_LOC }})
256 mstore(Q_DELTA_RANGE_X_LOC, {{ Q_DELTA_RANGE_X_LOC }})
257 mstore(Q_DELTA_RANGE_Y_LOC, {{ Q_DELTA_RANGE_Y_LOC }})
258 mstore(Q_ELLIPTIC_X_LOC, {{ Q_ELLIPTIC_X_LOC }})
259 mstore(Q_ELLIPTIC_Y_LOC, {{ Q_ELLIPTIC_Y_LOC }})
260 mstore(Q_MEMORY_X_LOC, {{ Q_MEMORY_X_LOC }})
261 mstore(Q_MEMORY_Y_LOC, {{ Q_MEMORY_Y_LOC }})
262 mstore(Q_NNF_X_LOC, {{ Q_NNF_X_LOC }})
263 mstore(Q_NNF_Y_LOC, {{ Q_NNF_Y_LOC }})
264 mstore(Q_POSEIDON_2_EXTERNAL_X_LOC, {{ Q_POSEIDON_2_EXTERNAL_X_LOC }})
265 mstore(Q_POSEIDON_2_EXTERNAL_Y_LOC, {{ Q_POSEIDON_2_EXTERNAL_Y_LOC }})
266 mstore(Q_POSEIDON_2_INTERNAL_X_LOC, {{ Q_POSEIDON_2_INTERNAL_X_LOC }})
267 mstore(Q_POSEIDON_2_INTERNAL_Y_LOC, {{ Q_POSEIDON_2_INTERNAL_Y_LOC }})
268 mstore(SIGMA_1_X_LOC, {{ SIGMA_1_X_LOC }})
269 mstore(SIGMA_1_Y_LOC, {{ SIGMA_1_Y_LOC }})
270 mstore(SIGMA_2_X_LOC, {{ SIGMA_2_X_LOC }})
271 mstore(SIGMA_2_Y_LOC, {{ SIGMA_2_Y_LOC }})
272 mstore(SIGMA_3_X_LOC, {{ SIGMA_3_X_LOC }})
273 mstore(SIGMA_3_Y_LOC, {{ SIGMA_3_Y_LOC }})
274 mstore(SIGMA_4_X_LOC, {{ SIGMA_4_X_LOC }})
275 mstore(SIGMA_4_Y_LOC, {{ SIGMA_4_Y_LOC }})
276 mstore(TABLE_1_X_LOC, {{ TABLE_1_X_LOC }})
277 mstore(TABLE_1_Y_LOC, {{ TABLE_1_Y_LOC }})
278 mstore(TABLE_2_X_LOC, {{ TABLE_2_X_LOC }})
279 mstore(TABLE_2_Y_LOC, {{ TABLE_2_Y_LOC }})
280 mstore(TABLE_3_X_LOC, {{ TABLE_3_X_LOC }})
281 mstore(TABLE_3_Y_LOC, {{ TABLE_3_Y_LOC }})
282 mstore(TABLE_4_X_LOC, {{ TABLE_4_X_LOC }})
283 mstore(TABLE_4_Y_LOC, {{ TABLE_4_Y_LOC }})
284 mstore(ID_1_X_LOC, {{ ID_1_X_LOC }})
285 mstore(ID_1_Y_LOC, {{ ID_1_Y_LOC }})
286 mstore(ID_2_X_LOC, {{ ID_2_X_LOC }})
287 mstore(ID_2_Y_LOC, {{ ID_2_Y_LOC }})
288 mstore(ID_3_X_LOC, {{ ID_3_X_LOC }})
289 mstore(ID_3_Y_LOC, {{ ID_3_Y_LOC }})
290 mstore(ID_4_X_LOC, {{ ID_4_X_LOC }})
291 mstore(ID_4_Y_LOC, {{ ID_4_Y_LOC }})
292 mstore(LAGRANGE_FIRST_X_LOC, {{ LAGRANGE_FIRST_X_LOC }})
293 mstore(LAGRANGE_FIRST_Y_LOC, {{ LAGRANGE_FIRST_Y_LOC }})
294 mstore(LAGRANGE_LAST_X_LOC, {{ LAGRANGE_LAST_X_LOC }})
295 mstore(LAGRANGE_LAST_Y_LOC, {{ LAGRANGE_LAST_Y_LOC }})
296 }
297
298 // Prime field order - placing on the stack
299 let p := P
300
301 {
302 let proof_ptr := add(calldataload(0x04), 0x24)
303
304 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
305 /* VALIDATE INPUT LENGTHS */
306 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
307 // Validate proof byte length matches expected size for this circuit's LOG_N (ZK variant).
308 // ZK proof has: 9 witness G1 (18) + 3 libra G1 (6) + LOG_N*9 univariates + 42 evals
309 // + 2 (libraSum,libraEval) + LOG_N gemini evals + 4 libra poly evals
310 // + (LOG_N-1)*2 gemini fold G1 + 2*2 (shplonkQ,kzg) + 8 pairing = (82 + 12*LOG_N) * 32
311 {
312 let expected_proof_size := mul(
313 add(
314 add(
315 add(24, mul(LOG_N, BATCHED_RELATION_PARTIAL_LENGTH)),
316 add(add(NUMBER_OF_ENTITIES, 2), mul(sub(LOG_N, 1), 2))
317 ),
318 add(add(LOG_N, LIBRA_EVALUATIONS), add(4, PAIRING_POINTS_SIZE))
319 ),
320 32
321 )
322 let proof_length := calldataload(add(calldataload(0x04), 0x04))
323 if iszero(eq(proof_length, expected_proof_size)) {
324 mstore(0x00, PROOF_LENGTH_WRONG_WITH_LOG_N_SELECTOR)
325 mstore(0x04, LOG_N)
326 mstore(0x24, proof_length)
327 mstore(0x44, expected_proof_size)
328 revert(0x00, 0x64)
329 }
330 }
331 // Validate public inputs array length matches expected count.
332 {
333 let pi_count := calldataload(add(calldataload(0x24), 0x04))
334 if iszero(eq(pi_count, REAL_NUMBER_PUBLIC_INPUTS)) {
335 mstore(0x00, PUBLIC_INPUTS_LENGTH_WRONG_SELECTOR)
336 revert(0x00, 0x04)
337 }
338 }
339
340 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
341 /* GENERATE CHALLENGES */
342 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
343 /*
344 * Proof points (affine coordinates) in the proof are in the following format, where offset is
345 * the offset in the entire proof until the first bit of the x coordinate
346 * offset + 0x00: x
347 * offset + 0x20: y
348 */
349
350 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
351 /* GENERATE ETA CHALLENGE */
352 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
353 /* ZK Eta challenge participants
354 * - VK_HASH
355 * - public inputs
356 * - pairing point limbs (8)
357 * - geminiMaskingPoly (G1) <- ZK addition
358 * - w1, w2, w3 (G1)
359 */
360
361 mstore(0x00, VK_HASH)
362
363 let public_inputs_start := add(calldataload(0x24), 0x24)
364 let public_inputs_size := mul(REAL_NUMBER_PUBLIC_INPUTS, 0x20)
365
366 // Copy the public inputs into the eta buffer
367 calldatacopy(0x20, public_inputs_start, public_inputs_size)
368
369 // Copy Pairing points into eta buffer
370 let public_inputs_end := add(0x20, public_inputs_size)
371
372 calldatacopy(public_inputs_end, proof_ptr, 0x100)
373
374 // 0x20 * 8 = 0x100 (8 pairing point limbs)
375 // End of public inputs + pairing points
376 // ZK: Copy geminiMaskingPoly(0x40) + w1,w2,w3(0xC0) = 0x100 bytes from proof after pairing
377 calldatacopy(add(0x120, public_inputs_size), add(proof_ptr, 0x100), 0x100)
378
379 // 0x220 = 0x20 (VK_HASH) + 0x100 (pairing) + 0x40 (geminiMaskingPoly) + 0xC0 (w1,w2,w3)
380 let eta_input_length := add(0x220, public_inputs_size)
381
382 // Get single eta challenge and compute powers (eta, eta², eta³)
383 let prev_challenge := mod(keccak256(0x00, eta_input_length), p)
384 mstore(0x00, prev_challenge)
385
386 let eta := and(prev_challenge, LOWER_127_MASK)
387 let eta_two := mulmod(eta, eta, p)
388 let eta_three := mulmod(eta_two, eta, p)
389
390 mstore(ETA_CHALLENGE, eta)
391 mstore(ETA_TWO_CHALLENGE, eta_two)
392 mstore(ETA_THREE_CHALLENGE, eta_three)
393
394 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
395 /* LOAD PROOF INTO MEMORY */
396 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
397 // As all of our proof points are written in contiguous parts of memory, we call use a single
398 // calldatacopy to place all of our proof into the correct memory regions
399 // We copy the entire proof into memory as we must hash each proof section for challenge
400 // evaluation
401 // The last item in the proof, and the first item in the proof (pairing point 0)
402 let proof_size := sub(ETA_CHALLENGE, PAIRING_POINT_0_X_0_LOC)
403
404 calldatacopy(PAIRING_POINT_0_X_0_LOC, proof_ptr, proof_size)
405
406 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
407 /* VALIDATE PROOF INPUTS */
408 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
409 // Validate all proof elements are within their expected ranges.
410 // Pairing limbs: lo < 2^136, hi < 2^120. G1 coordinates < Q. Fr elements < P.
411 {
412 let valid := true
413 let lo_limb_max := shl(136, 1)
414 let hi_limb_max := shl(120, 1)
415 let q_mod := Q
416
417 // 1. Pairing limbs: lo < 2^136, hi < 2^120 (4 pairs, stride 0x40)
418 let ptr := PAIRING_POINT_0_X_0_LOC
419 for {} lt(ptr, GEMINI_MASKING_POLY_X_LOC) { ptr := add(ptr, 0x40) } {
420 valid := and(valid, lt(mload(ptr), lo_limb_max))
421 valid := and(valid, lt(mload(add(ptr, 0x20)), hi_limb_max))
422 }
423 if iszero(valid) {
424 mstore(0x00, VALUE_GE_LIMB_MAX_SELECTOR)
425 revert(0x00, 0x04)
426 }
427
428 // 2. G1 coordinates: each < Q
429 // - geminiMaskingPoly + witness commitments + libraConcat (20 slots)
430 for { ptr := GEMINI_MASKING_POLY_X_LOC } lt(ptr, LIBRA_SUM_LOC) { ptr := add(ptr, 0x20) } {
431 valid := and(valid, lt(mload(ptr), q_mod))
432 }
433 // - Libra grand product + quotient (4 slots)
434 for { ptr := LIBRA_GRAND_PRODUCT_X_LOC } lt(ptr, GEMINI_FOLD_UNIVARIATE_0_X_LOC) {
435 ptr := add(ptr, 0x20)
436 } {
437 valid := and(valid, lt(mload(ptr), q_mod))
438 }
439 // - Gemini fold commitments (28 slots)
440 for { ptr := GEMINI_FOLD_UNIVARIATE_0_X_LOC } lt(ptr, GEMINI_A_EVAL_0) { ptr := add(ptr, 0x20) } {
441 valid := and(valid, lt(mload(ptr), q_mod))
442 }
443 // - Shplonk Q + KZG quotient (4 slots)
444 for { ptr := SHPLONK_Q_X_LOC } lt(ptr, ETA_CHALLENGE) { ptr := add(ptr, 0x20) } {
445 valid := and(valid, lt(mload(ptr), q_mod))
446 }
447 if iszero(valid) {
448 mstore(0x00, VALUE_GE_GROUP_ORDER_SELECTOR)
449 revert(0x00, 0x04)
450 }
451
452 // 2b. G1 points: identity (0,0) is accepted.
453 // Polynomial commitments to identically-zero polynomials are
454 // legitimately the identity, and the ecAdd/ecMul precompiles
455 // treat (0,0) as the additive identity per EIP-196. Soundness
456 // against (0,0) substitution for a non-zero commitment is upheld
457 // by sumcheck/Shplemini downstream.
458
459 // 3. Fr elements: each < P
460 // - libraSum + sumcheck univariates + evals + libraEvaluation (179 slots)
461 for { ptr := LIBRA_SUM_LOC } lt(ptr, LIBRA_GRAND_PRODUCT_X_LOC) {
462 ptr := add(ptr, 0x20)
463 } {
464 valid := and(valid, lt(mload(ptr), p))
465 }
466 // - Gemini evaluations + libra poly evals (19 slots)
467 for { ptr := GEMINI_A_EVAL_0 } lt(ptr, SHPLONK_Q_X_LOC) { ptr := add(ptr, 0x20) } {
468 valid := and(valid, lt(mload(ptr), p))
469 }
470 if iszero(valid) {
471 mstore(0x00, VALUE_GE_FIELD_ORDER_SELECTOR)
472 revert(0x00, 0x04)
473 }
474 }
475
476 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
477 /* GENERATE BETA and GAMMAA CHALLENGE */
478 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
479
480 // Generate Beta and Gamma Chalenges
481 // - prevChallenge
482 // - LOOKUP_READ_COUNTS
483 // - LOOKUP_READ_TAGS
484 // - W4
485 mcopy(0x20, LOOKUP_READ_COUNTS_X_LOC, 0xc0)
486
487 prev_challenge := mod(keccak256(0x00, 0xe0), p)
488 mstore(0x00, prev_challenge)
489 let beta := and(prev_challenge, LOWER_127_MASK)
490 let gamma := shr(127, prev_challenge)
491
492 mstore(BETA_CHALLENGE, beta)
493 mstore(GAMMA_CHALLENGE, gamma)
494
495 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
496 /* ALPHA CHALLENGES */
497 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
498 // Generate Alpha challenges - non-linearise the gate contributions
499 //
500 // There are 26 total subrelations in this honk relation, we do not need to non linearise the first sub relation.
501 // There are 25 total gate contributions, a gate contribution is analogous to
502 // a custom gate, it is an expression which must evaluate to zero for each
503 // row in the constraint matrix
504 //
505 // If we do not non-linearise sub relations, then sub relations which rely
506 // on the same wire will interact with each other's sums.
507
508 mcopy(0x20, LOOKUP_INVERSES_X_LOC, 0x80)
509
510 // Generate single alpha challenge and compute its powers
511 prev_challenge := mod(keccak256(0x00, 0xa0), p)
512 mstore(0x00, prev_challenge)
513 let alpha := and(prev_challenge, LOWER_127_MASK)
514 mstore(ALPHA_CHALLENGE_0, alpha)
515
516 // Compute powers of alpha: alpha^2, alpha^3, ..., alpha^27
517 let alpha_off_set := ALPHA_CHALLENGE_1
518 for {} lt(alpha_off_set, add(ALPHA_CHALLENGE_27, 0x20)) {} {
519 let prev_alpha := mload(sub(alpha_off_set, 0x20))
520 mstore(alpha_off_set, mulmod(prev_alpha, alpha, p))
521 alpha_off_set := add(alpha_off_set, 0x20)
522 }
523
524 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
525 /* GATE CHALLENGES */
526 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
527
528 // Store the first gate challenge
529 prev_challenge := mod(keccak256(0x00, 0x20), p)
530 mstore(0x00, prev_challenge)
531 let gate_challenge := and(prev_challenge, LOWER_127_MASK)
532 mstore(GATE_CHALLENGE_0, gate_challenge)
533
534 let gate_off := GATE_CHALLENGE_1
535 for {} lt(gate_off, LIBRA_CHALLENGE) {} {
536 let prev := mload(sub(gate_off, 0x20))
537
538 mstore(gate_off, mulmod(prev, prev, p))
539 gate_off := add(gate_off, 0x20)
540 }
541
542 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
543 /* LIBRA CHALLENGE */
544 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
545 // Generate Libra challenge: hash(prevChallenge, libraConcat.x, libraConcat.y, libraSum)
546 // libraConcat (0x40) + libraSum (0x20) = 0x60 bytes of proof data
547 mcopy(0x20, LIBRA_CONCAT_X_LOC, 0x60)
548
549 prev_challenge := mod(keccak256(0x00, 0x80), p)
550 mstore(0x00, prev_challenge)
551 let libraChallenge := and(prev_challenge, LOWER_127_MASK)
552 mstore(LIBRA_CHALLENGE, libraChallenge)
553
554 // Sumcheck Univariate challenges (ZK variant)
555 // The algebraic relations of the Honk protocol are max degree-7.
556 // To prove satifiability, we multiply the relation by a random (POW) polynomial + masking.
557 // As a result, in every round of sumcheck, the prover sends a degree-9 univariate polynomial.
558 // 9 points are sent as it is enough to uniquely identify the polynomial.
559 let read_off := SUMCHECK_UNIVARIATE_0_0_LOC
560 let write_off := SUM_U_CHALLENGE_0
561 for {} lt(read_off, GEMINI_MASKING_EVAL_LOC) {} {
562 // 0x20 * 9 = 0x120 bytes per round
563 mcopy(0x20, read_off, 0x120)
564
565 // Hash 0x120 + 0x20 (prev hash) = 0x140
566 prev_challenge := mod(keccak256(0x00, 0x140), p)
567 mstore(0x00, prev_challenge)
568
569 let sumcheck_u_challenge := and(prev_challenge, LOWER_127_MASK)
570 mstore(write_off, sumcheck_u_challenge)
571
572 // Progress read / write pointers
573 read_off := add(read_off, 0x120)
574 write_off := add(write_off, 0x20)
575 }
576
577 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
578 /* RHO CHALLENGES */
579 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
580 // The RHO challenge is the hash of the evaluations of all of the wire values
581 // As per usual, it includes the previous challenge
582 // Evaluations of the following wires and their shifts (for relevant wires):
583 // - QM
584 // - QC
585 // - Q1 (QL)
586 // - Q2 (QR)
587 // - Q3 (QO)
588 // - Q4
589 // - QLOOKUP
590 // - QARITH
591 // - QRANGE
592 // - QELLIPTIC
593 // - QMEMORY
594 // - QNNF (NNF = Non Native Field)
595 // - QPOSEIDON2_EXTERNAL
596 // - QPOSEIDON2_INTERNAL
597 // - SIGMA1
598 // - SIGMA2
599 // - SIGMA3
600 // - SIGMA4
601 // - ID1
602 // - ID2
603 // - ID3
604 // - ID4
605 // - TABLE1
606 // - TABLE2
607 // - TABLE3
608 // - TABLE4
609 // - W1 (WL)
610 // - W2 (WR)
611 // - W3 (WO)
612 // - W4
613 // - Z_PERM
614 // - LOOKUP_INVERSES
615 // - LOOKUP_READ_COUNTS
616 // - LOOKUP_READ_TAGS
617 // - W1_SHIFT
618 // - W2_SHIFT
619 // - W3_SHIFT
620 // - W4_SHIFT
621 // - Z_PERM_SHIFT
622 //
623 // Hash all evaluations + libraEvaluation + 2 libra commitments (G1)
624 // ZK: 42 evals (GEMINI_MASKING_EVAL through Z_PERM_SHIFT) + libraEval + libraGrandProduct(G1) + libraQuotient(G1)
625 // = 42*0x20 + 0x20 + 2*0x40 = 0x5e0 bytes
626 mcopy(0x20, GEMINI_MASKING_EVAL_LOC, 0x5e0)
627 prev_challenge := mod(keccak256(0x00, 0x600), p)
628 mstore(0x00, prev_challenge)
629
630 let rho := and(prev_challenge, LOWER_127_MASK)
631
632 mstore(RHO_CHALLENGE, rho)
633
634 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
635 /* GEMINI R CHALLENGE */
636 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
637 // The Gemini R challenge contains a of all of commitments to all of the univariates
638 // evaluated in the Gemini Protocol
639 // So for multivariate polynomials in l variables, we will hash l - 1 commitments.
640 // For this implementation, we have logN number of of rounds and thus logN - 1 committments
641 // The format of these commitments are proof points, which are explained above
642 // 0x40 * (logN - 1)
643
644 mcopy(0x20, GEMINI_FOLD_UNIVARIATE_0_X_LOC, {{ GEMINI_FOLD_UNIVARIATE_LENGTH }})
645
646 prev_challenge := mod(keccak256(0x00, {{ GEMINI_FOLD_UNIVARIATE_HASH_LENGTH }}), p)
647 mstore(0x00, prev_challenge)
648
649 let geminiR := and(prev_challenge, LOWER_127_MASK)
650
651 mstore(GEMINI_R_CHALLENGE, geminiR)
652
653 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
654 /* SHPLONK NU CHALLENGE */
655 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
656 // The shplonk nu challenge hashes gemini A evaluations + libra poly evaluations
657 // ZK: 0x20 * (logN + 4) = 0x20 * 19 = 0x260
658
659 mcopy(0x20, GEMINI_A_EVAL_0, {{ GEMINI_EVALS_LENGTH }})
660 prev_challenge := mod(keccak256(0x00, {{ GEMINI_EVALS_HASH_LENGTH }}), p)
661 mstore(0x00, prev_challenge)
662
663 let shplonkNu := and(prev_challenge, LOWER_127_MASK)
664 mstore(SHPLONK_NU_CHALLENGE, shplonkNu)
665
666 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
667 /* SHPLONK Z CHALLENGE */
668 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
669 // Generate Shplonk Z
670 // Hash of the single shplonk Q commitment
671 mcopy(0x20, SHPLONK_Q_X_LOC, 0x40)
672 prev_challenge := mod(keccak256(0x00, 0x60), p)
673
674 let shplonkZ := and(prev_challenge, LOWER_127_MASK)
675 mstore(SHPLONK_Z_CHALLENGE, shplonkZ)
676
677 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
678 /* CHALLENGES COMPLETE */
679 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
680 }
681
682 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
683 /* PUBLIC INPUT DELTA */
684 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
713 {
714 let beta := mload(BETA_CHALLENGE)
715 let gamma := mload(GAMMA_CHALLENGE)
716 let pub_off := PUBLIC_INPUTS_OFFSET
717
718 let numerator_value := 1
719 let denominator_value := 1
720
721 let p_clone := p // move p to the front of the stack
722
723 // Assume offset is less than p
724 // numerator_acc = gamma + (beta * (PERMUTATION_ARGUMENT_VALUE_SEPARATOR + offset))
725 let numerator_acc :=
726 addmod(gamma, mulmod(beta, add(PERMUTATION_ARGUMENT_VALUE_SEPARATOR, pub_off), p_clone), p_clone)
727 // demonimator_acc = gamma - (beta * (offset + 1))
728 let beta_x_off := mulmod(beta, add(pub_off, 1), p_clone)
729 let denominator_acc := addmod(gamma, sub(p_clone, beta_x_off), p_clone)
730
731 let valid_inputs := true
732 // Load the starting point of the public inputs (jump over the selector and the length of public inputs [0x24])
733 let public_inputs_ptr := add(calldataload(0x24), 0x24)
734
735 // endpoint_ptr = public_inputs_ptr + num_inputs * 0x20. // every public input is 0x20 bytes
736 let endpoint_ptr := add(public_inputs_ptr, mul(REAL_NUMBER_PUBLIC_INPUTS, 0x20))
737
738 for {} lt(public_inputs_ptr, endpoint_ptr) { public_inputs_ptr := add(public_inputs_ptr, 0x20) } {
739 // Get public inputs from calldata
740 let input := calldataload(public_inputs_ptr)
741
742 valid_inputs := and(valid_inputs, lt(input, p_clone))
743
744 numerator_value := mulmod(numerator_value, addmod(numerator_acc, input, p_clone), p_clone)
745 denominator_value := mulmod(denominator_value, addmod(denominator_acc, input, p_clone), p_clone)
746
747 numerator_acc := addmod(numerator_acc, beta, p_clone)
748 denominator_acc := addmod(denominator_acc, sub(p_clone, beta), p_clone)
749 }
750
751 // Revert if not all public inputs are field elements (i.e. < p)
752 if iszero(valid_inputs) {
753 mstore(0x00, VALUE_GE_FIELD_ORDER_SELECTOR)
754 revert(0x00, 0x04)
755 }
756
757 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
758 /* PUBLIC INPUT DELTA - Pairing points accum */
759 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
760 // Pairing points contribution to public inputs delta
761 let pairing_points_ptr := PAIRING_POINT_0_X_0_LOC
762 for {} lt(pairing_points_ptr, GEMINI_MASKING_POLY_X_LOC) { pairing_points_ptr := add(pairing_points_ptr, 0x20) } {
763 let input := mload(pairing_points_ptr)
764
765 numerator_value := mulmod(numerator_value, addmod(numerator_acc, input, p_clone), p_clone)
766 denominator_value := mulmod(denominator_value, addmod(denominator_acc, input, p_clone), p_clone)
767
768 numerator_acc := addmod(numerator_acc, beta, p_clone)
769 denominator_acc := addmod(denominator_acc, sub(p_clone, beta), p_clone)
770 }
771
772 mstore(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE, numerator_value)
773 mstore(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE, denominator_value)
774
775 // PI delta denominator inversion is deferred to the barycentric
776 // batch inversion below.
777 }
778 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
779 /* PUBLIC INPUT DELTA - complete */
780 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
781
782 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
783 /* SUMCHECK */
784 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
785 //
786 // Sumcheck is used to prove that every relation 0 on each row of the witness.
787 //
788 // Given each of the columns of our trace is a multilinear polynomial 𝑃1,…,𝑃𝑁∈𝔽[𝑋0,…,𝑋𝑑−1]. We run sumcheck over the polynomial
789 //
790 // 𝐹̃ (𝑋0,…,𝑋𝑑−1)=𝑝𝑜𝑤𝛽(𝑋0,…,𝑋𝑑−1)⋅𝐹(𝑃1(𝑋0,…,𝑋𝑑−1),…,𝑃𝑁(𝑋0,…,𝑋𝑑−1))
791 //
792 // The Pow polynomial is a random polynomial that allows us to ceritify that the relations sum to 0 on each row of the witness,
793 // rather than the entire sum just targeting 0.
794 //
795 // 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....)
796 //
797 // We start with a LOG_N variate multilinear polynomial, each round fixes a variable to a challenge value.
798 // Each round the prover sends a round univariate poly, since the degree of our honk relations is 7 + the pow polynomial the prover
799 // sends a degree-8 univariate on each round.
800 // This is sent efficiently by sending 8 values, enough to represent a unique polynomial.
801 // Barycentric evaluation is used to evaluate the polynomial at any point on the domain, given these 8 unique points.
802 //
803 // In the sumcheck protocol, the target sum for each round is the sum of the round univariate evaluated on 0 and 1.
804 // 𝜎𝑖=?𝑆̃ 𝑖(0)+𝑆̃ 𝑖(1)
805 // This is efficiently checked as S(0) and S(1) are sent by the prover as values of the round univariate.
806 //
807 // We compute the next challenge by evaluating the round univariate at a random challenge value.
808 // 𝜎𝑖+1←𝑆̃ 𝑖(𝑢𝑖)
809 // This evaluation is performed via barycentric evaluation.
810 //
811 // Once we have reduced the multilinear polynomials into single dimensional polys, we check the entire sumcheck relation matches the target sum.
812 //
813 // Below this is composed of 8 relations:
814 // 1. Arithmetic relation - constrains arithmetic
815 // 2. Permutaiton Relation - efficiently encodes copy constraints
816 // 3. Log Derivative Lookup Relation - used for lookup operations
817 // 4. Delta Range Relation - used for efficient range checks
818 // 5. Memory Relation - used for efficient memory operations
819 // 6. NNF Relation - used for efficient Non Native Field operations
820 // 7. Poseidon2 External Relation - used for efficient in-circuit hashing
821 // 8. Poseidon2 Internal Relation - used for efficient in-circuit hashing
822 //
823 // These are batched together and evaluated at the same time using the alpha challenges.
824 //
825 {
826 // We write the barycentric domain values into memory
827 // These are written once per program execution, and reused across all
828 // sumcheck rounds
829 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_0_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_0)
830 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_1_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_1)
831 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_2_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_2)
832 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_3_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_3)
833 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_4_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_4)
834 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_5_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_5)
835 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_6_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_6)
836 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_7_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_7)
837 mstore(BARYCENTRIC_LAGRANGE_DENOMINATOR_8_LOC, BARYCENTRIC_LAGRANGE_DENOMINATOR_8)
838
839 // Compute the target sums for each round of sumcheck
840 {
841 // This requires the barycentric inverses to be computed for each round
842 // Write all of the non inverted barycentric denominators into memory
843 let accumulator := 1
844 let temp := FOLD_POS_EVALUATIONS_{{ LOG_N_MINUS_ONE }}_LOC // we use fold pos evaluations as we add 0x20 immediately to the pointer to get `BARYCENTRIC_TEMP_0_LOC`
845 let bary_centric_inverses_off := BARYCENTRIC_DENOMINATOR_INVERSES_0_0_LOC
846 {
847 let round_challenge_off := SUM_U_CHALLENGE_0
848 for { let round := 0 } lt(round, LOG_N) { round := add(round, 1) } {
849 let round_challenge := mload(round_challenge_off)
850 let bary_lagrange_denominator_off := BARYCENTRIC_LAGRANGE_DENOMINATOR_0_LOC
851
852 // Unrolled as this loop only has 9 iterations (ZK)
853 {
854 let bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
855 let pre_inv :=
856 mulmod(
857 bary_lagrange_denominator,
858 addmod(round_challenge, p, p), // sub(p, 0) = p
859 p
860 )
861 mstore(bary_centric_inverses_off, pre_inv)
862 temp := add(temp, 0x20)
863 mstore(temp, accumulator)
864 accumulator := mulmod(accumulator, pre_inv, p)
865
866 // increase offsets
867 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
868 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
869
870 // barycentric_index = 1
871 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
872 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 1), p), p)
873 mstore(bary_centric_inverses_off, pre_inv)
874 temp := add(temp, 0x20)
875 mstore(temp, accumulator)
876 accumulator := mulmod(accumulator, pre_inv, p)
877
878 // increase offsets
879 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
880 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
881
882 // barycentric_index = 2
883 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
884 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 2), p), p)
885 mstore(bary_centric_inverses_off, pre_inv)
886 temp := add(temp, 0x20)
887 mstore(temp, accumulator)
888 accumulator := mulmod(accumulator, pre_inv, p)
889
890 // increase offsets
891 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
892 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
893
894 // barycentric_index = 3
895 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
896 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 3), p), p)
897 mstore(bary_centric_inverses_off, pre_inv)
898 temp := add(temp, 0x20)
899 mstore(temp, accumulator)
900 accumulator := mulmod(accumulator, pre_inv, p)
901
902 // increase offsets
903 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
904 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
905
906 // barycentric_index = 4
907 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
908 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 4), p), p)
909 mstore(bary_centric_inverses_off, pre_inv)
910 temp := add(temp, 0x20)
911 mstore(temp, accumulator)
912 accumulator := mulmod(accumulator, pre_inv, p)
913
914 // increase offsets
915 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
916 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
917
918 // barycentric_index = 5
919 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
920 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 5), p), p)
921 mstore(bary_centric_inverses_off, pre_inv)
922 temp := add(temp, 0x20)
923 mstore(temp, accumulator)
924 accumulator := mulmod(accumulator, pre_inv, p)
925
926 // increase offsets
927 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
928 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
929
930 // barycentric_index = 6
931 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
932 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 6), p), p)
933 mstore(bary_centric_inverses_off, pre_inv)
934 temp := add(temp, 0x20)
935 mstore(temp, accumulator)
936 accumulator := mulmod(accumulator, pre_inv, p)
937
938 // increase offsets
939 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
940 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
941
942 // barycentric_index = 7
943 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
944 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 7), p), p)
945 mstore(bary_centric_inverses_off, pre_inv)
946 temp := add(temp, 0x20)
947 mstore(temp, accumulator)
948 accumulator := mulmod(accumulator, pre_inv, p)
949
950 // increase offsets
951 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
952 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
953
954 // barycentric_index = 8 (ZK)
955 bary_lagrange_denominator := mload(bary_lagrange_denominator_off)
956 pre_inv := mulmod(bary_lagrange_denominator, addmod(round_challenge, sub(p, 8), p), p)
957 mstore(bary_centric_inverses_off, pre_inv)
958 temp := add(temp, 0x20)
959 mstore(temp, accumulator)
960 accumulator := mulmod(accumulator, pre_inv, p)
961
962 // increase offsets
963 bary_lagrange_denominator_off := add(bary_lagrange_denominator_off, 0x20)
964 bary_centric_inverses_off := add(bary_centric_inverses_off, 0x20)
965 }
966 round_challenge_off := add(round_challenge_off, 0x20)
967 }
968 }
969
970 // Append PI delta denominator to the batch inversion
971 {
972 let pi_denom := mload(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE)
973 mstore(PUBLIC_INPUTS_DENOM_TEMP_LOC, accumulator)
974 accumulator := mulmod(accumulator, pi_denom, p)
975 }
976
977 // --- Phase 2: Shplemini forward pass ---
978 // Compute shplemini denominators and accumulate into the running product.
979 // Pre-inversion values stored at designated addresses (0x6800+),
980 // which don't overlap with barycentric storage.
981 {
982 // Compute powers of evaluation challenge: gemini_r^{2^i}
983 let cache := mload(GEMINI_R_CHALLENGE)
984 mstore(POWERS_OF_EVALUATION_CHALLENGE_0_LOC, cache)
987
988 // Element 0: gemini_r (seed)
989 {
990 let val := mload(GEMINI_R_CHALLENGE)
991 mstore(GEMINI_R_INV_TEMP_LOC, accumulator)
992 accumulator := mulmod(accumulator, val, p)
993 }
994
995 // Append Libra Subgroup Denominator calculation to batch inversion
996 {
997 let val := addmod(
998 mload(SHPLONK_Z_CHALLENGE),
999 sub(p, mulmod(SUBGROUP_GENERATOR, mload(GEMINI_R_CHALLENGE), p)),
1000 p
1001 )
1002 mstore(LIBRA_SUBGROUP_DENOM_LOC, val)
1003 mstore(LIBRA_SUBGROUP_DENOM_TEMP_LOC, accumulator)
1004 accumulator := mulmod(accumulator, val, p)
1005 }
1006
1007 // Elements 1..LOG_N: INVERTED_CHALLENGE_POW_MINUS_U
1008 // Elements LOG_N+1..2*LOG_N: POS_INVERTED_DENOM
1009 // Elements 2*LOG_N+1..3*LOG_N: NEG_INVERTED_DENOM
1012 }
1013
1014 // Invert all elements (barycentric + PI delta + shplemini) as a single batch
1015 {
1016 {
1017 mstore(0, 0x20)
1018 mstore(0x20, 0x20)
1019 mstore(0x40, 0x20)
1020 mstore(0x60, accumulator)
1021 mstore(0x80, P_SUB_2)
1022 mstore(0xa0, p)
1023 if iszero(staticcall(gas(), 0x05, 0x00, 0xc0, 0x00, 0x20)) {
1024 mstore(0x00, MODEXP_FAILED_SELECTOR)
1025 revert(0x00, 0x04)
1026 }
1027 accumulator := mload(0x00)
1028 if iszero(accumulator) {
1029 mstore(0x00, MODEXP_FAILED_SELECTOR)
1030 revert(0x00, 0x04)
1031 }
1032 }
1033
1034 // --- Shplemini backward pass ---
1035 // Extract shplemini inverses in strict reverse order.
1036 {
1039
1040 // libra subgroup denom
1041 {
1042 let tmp := mulmod(accumulator, mload(LIBRA_SUBGROUP_DENOM_TEMP_LOC), p)
1043 accumulator := mulmod(accumulator, mload(LIBRA_SUBGROUP_DENOM_LOC), p)
1044 mstore(LIBRA_SUBGROUP_DENOM_LOC, tmp)
1045 }
1046
1047 // gemini_r inverse
1048 {
1049 let tmp := mulmod(accumulator, mload(GEMINI_R_INV_TEMP_LOC), p)
1050 accumulator := mulmod(accumulator, mload(GEMINI_R_CHALLENGE), p)
1051 mstore(GEMINI_R_INV_LOC, tmp)
1052 }
1053 }
1054
1055 // Extract PI delta denominator inverse from the batch
1056 {
1057 let pi_delta_inv := mulmod(accumulator, mload(PUBLIC_INPUTS_DENOM_TEMP_LOC), p)
1058 accumulator := mulmod(accumulator, mload(PUBLIC_INPUTS_DELTA_DENOMINATOR_CHALLENGE), p)
1059
1060 // Finalize: public_inputs_delta = numerator * (1/denominator)
1061 mstore(
1062 PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE,
1063 mulmod(mload(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE), pi_delta_inv, p)
1064 )
1065 }
1066
1067 // Normalise as last loop will have incremented the offset
1068 bary_centric_inverses_off := sub(bary_centric_inverses_off, 0x20)
1069 for {} gt(bary_centric_inverses_off, BARYCENTRIC_LAGRANGE_DENOMINATOR_{{ BATCHED_RELATION_PARTIAL_LENGTH_MINUS_ONE }}_LOC) {
1070 bary_centric_inverses_off := sub(bary_centric_inverses_off, 0x20)
1071 } {
1072 let tmp := mulmod(accumulator, mload(temp), p)
1073 accumulator := mulmod(accumulator, mload(bary_centric_inverses_off), p)
1074 mstore(bary_centric_inverses_off, tmp)
1075
1076 temp := sub(temp, 0x20)
1077 }
1078 }
1079 }
1080
1081 let valid := true
1082 // ZK: initial round target = libraChallenge * libraSum
1083 let round_target := mulmod(mload(LIBRA_CHALLENGE), mload(LIBRA_SUM_LOC), p)
1084 let pow_partial_evaluation := 1
1085 let gate_challenge_off := GATE_CHALLENGE_0
1086 let round_univariates_off := SUMCHECK_UNIVARIATE_0_0_LOC
1087
1088 let challenge_off := SUM_U_CHALLENGE_0
1089 let bary_inverses_off := BARYCENTRIC_DENOMINATOR_INVERSES_0_0_LOC
1090
1091 for { let round := 0 } lt(round, LOG_N) { round := add(round, 1) } {
1092 let round_challenge := mload(challenge_off)
1093
1094 // Total sum = u[0] + u[1]
1095 let total_sum := addmod(mload(round_univariates_off), mload(add(round_univariates_off, 0x20)), p)
1096 valid := and(valid, eq(total_sum, round_target))
1097
1098 // Compute next target sum (ZK: 9-element domain)
1099 let numerator_value := round_challenge
1100 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 1), p), p)
1101 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 2), p), p)
1102 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 3), p), p)
1103 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 4), p), p)
1104 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 5), p), p)
1105 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 6), p), p)
1106 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 7), p), p)
1107 numerator_value := mulmod(numerator_value, addmod(round_challenge, sub(p, 8), p), p)
1108
1109 // // Compute the next round target
1110 round_target := 0
1111 for { let i := 0 } lt(i, BATCHED_RELATION_PARTIAL_LENGTH) { i := add(i, 1) } {
1112 let term := mload(round_univariates_off)
1113 let inverse := mload(bary_inverses_off)
1114
1115 term := mulmod(term, inverse, p)
1116 round_target := addmod(round_target, term, p)
1117 round_univariates_off := add(round_univariates_off, 0x20)
1118 bary_inverses_off := add(bary_inverses_off, 0x20)
1119 }
1120
1121 round_target := mulmod(round_target, numerator_value, p)
1122
1123 // Partially evaluate POW
1124 let gate_challenge := mload(gate_challenge_off)
1125 let gate_challenge_minus_one := sub(gate_challenge, 1)
1126
1127 let univariate_evaluation := addmod(1, mulmod(round_challenge, gate_challenge_minus_one, p), p)
1128
1129 pow_partial_evaluation := mulmod(pow_partial_evaluation, univariate_evaluation, p)
1130
1131 gate_challenge_off := add(gate_challenge_off, 0x20)
1132 challenge_off := add(challenge_off, 0x20)
1133 }
1134
1135 if iszero(valid) {
1136 mstore(0x00, SUMCHECK_FAILED_SELECTOR)
1137 revert(0x00, 0x04)
1138 }
1139
1140 // The final sumcheck round; accumulating evaluations
1141 // Uses pow partial evaluation as the gate scaling factor
1142
1143 mstore(POW_PARTIAL_EVALUATION_LOC, pow_partial_evaluation)
1144 mstore(FINAL_ROUND_TARGET_LOC, round_target)
1145
1146 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1147 /* LOGUP RELATION */
1148 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1149 {
1185 let w1q1 := mulmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
1186 let w2q2 := mulmod(mload(W2_EVAL_LOC), mload(QR_EVAL_LOC), p)
1187 let w3q3 := mulmod(mload(W3_EVAL_LOC), mload(QO_EVAL_LOC), p)
1188 let w4q3 := mulmod(mload(W4_EVAL_LOC), mload(Q4_EVAL_LOC), p)
1189
1190 let q_arith := mload(QARITH_EVAL_LOC)
1191 // w1w2qm := (w_1 . w_2 . q_m . (QARITH_EVAL_LOC - 3)) / 2
1192 let w1w2qm :=
1193 mulmod(
1194 mulmod(
1195 mulmod(mulmod(mload(W1_EVAL_LOC), mload(W2_EVAL_LOC), p), mload(QM_EVAL_LOC), p),
1196 addmod(q_arith, P_SUB_3, p),
1197 p
1198 ),
1199 NEG_HALF_MODULO_P,
1200 p
1201 )
1202
1203 // (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
1204 let identity :=
1205 addmod(
1206 mload(QC_EVAL_LOC),
1207 addmod(w4q3, addmod(w3q3, addmod(w2q2, addmod(w1q1, w1w2qm, p), p), p), p),
1208 p
1209 )
1210
1211 // if q_arith == 3 we evaluate an additional mini addition gate (on top of the regular one), where:
1212 // w_1 + w_4 - w_1_omega + q_m = 0
1213 // we use this gate to save an addition gate when adding or subtracting non-native field elements
1214 // α * (q_arith - 2) * (w_1 + w_4 - w_1_omega + q_m)
1215 let extra_small_addition_gate_identity :=
1216 mulmod(
1217 addmod(q_arith, P_SUB_2, p),
1218 addmod(
1219 mload(QM_EVAL_LOC),
1220 addmod(
1221 sub(p, mload(W1_SHIFT_EVAL_LOC)),
1222 addmod(mload(W1_EVAL_LOC), mload(W4_EVAL_LOC), p),
1223 p
1224 ),
1225 p
1226 ),
1227 p
1228 )
1229
1230 // Split up the two relations
1231 let contribution_0 :=
1232 addmod(identity, mulmod(addmod(q_arith, P_SUB_1, p), mload(W4_SHIFT_EVAL_LOC), p), p)
1233 contribution_0 := mulmod(mulmod(contribution_0, q_arith, p), mload(POW_PARTIAL_EVALUATION_LOC), p)
1234 mstore(SUBRELATION_EVAL_0_LOC, contribution_0)
1235
1236 let contribution_1 := mulmod(extra_small_addition_gate_identity, addmod(q_arith, P_SUB_1, p), p)
1237 contribution_1 := mulmod(contribution_1, q_arith, p)
1238 contribution_1 := mulmod(contribution_1, mload(POW_PARTIAL_EVALUATION_LOC), p)
1239 mstore(SUBRELATION_EVAL_1_LOC, contribution_1)
1240 }
1241
1242 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1243 /* PERMUTATION RELATION */
1244 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1245 {
1246 let beta := mload(BETA_CHALLENGE)
1247 let gamma := mload(GAMMA_CHALLENGE)
1248
1257 let t1 :=
1258 mulmod(
1259 add(add(mload(W1_EVAL_LOC), gamma), mulmod(beta, mload(ID1_EVAL_LOC), p)),
1260 add(add(mload(W2_EVAL_LOC), gamma), mulmod(beta, mload(ID2_EVAL_LOC), p)),
1261 p
1262 )
1263 let t2 :=
1264 mulmod(
1265 add(add(mload(W3_EVAL_LOC), gamma), mulmod(beta, mload(ID3_EVAL_LOC), p)),
1266 add(add(mload(W4_EVAL_LOC), gamma), mulmod(beta, mload(ID4_EVAL_LOC), p)),
1267 p
1268 )
1269 let numerator := mulmod(t1, t2, p)
1270 t1 := mulmod(
1271 add(add(mload(W1_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA1_EVAL_LOC), p)),
1272 add(add(mload(W2_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA2_EVAL_LOC), p)),
1273 p
1274 )
1275 t2 := mulmod(
1276 add(add(mload(W3_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA3_EVAL_LOC), p)),
1277 add(add(mload(W4_EVAL_LOC), gamma), mulmod(beta, mload(SIGMA4_EVAL_LOC), p)),
1278 p
1279 )
1280 let denominator := mulmod(t1, t2, p)
1281
1282 {
1283 let acc :=
1284 mulmod(addmod(mload(Z_PERM_EVAL_LOC), mload(LAGRANGE_FIRST_EVAL_LOC), p), numerator, p)
1285
1286 acc := addmod(
1287 acc,
1288 sub(
1289 p,
1290 mulmod(
1291 addmod(
1292 mload(Z_PERM_SHIFT_EVAL_LOC),
1293 mulmod(
1294 mload(LAGRANGE_LAST_EVAL_LOC),
1295 mload(PUBLIC_INPUTS_DELTA_NUMERATOR_CHALLENGE),
1296 p
1297 ),
1298 p
1299 ),
1300 denominator,
1301 p
1302 )
1303 ),
1304 p
1305 )
1306
1307 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1308 mstore(SUBRELATION_EVAL_2_LOC, acc)
1309
1310 acc := mulmod(
1311 mulmod(mload(LAGRANGE_LAST_EVAL_LOC), mload(Z_PERM_SHIFT_EVAL_LOC), p),
1312 mload(POW_PARTIAL_EVALUATION_LOC),
1313 p
1314 )
1315 mstore(SUBRELATION_EVAL_3_LOC, acc)
1316
1317
1318 // zperm initialization (lagrange_first * z_perm = 0)
1319 acc := mulmod(
1320 mulmod(
1321 mload(LAGRANGE_FIRST_EVAL_LOC),
1322 mload(Z_PERM_EVAL_LOC),
1323 p),
1324 mload(POW_PARTIAL_EVALUATION_LOC),
1325 p)
1326 mstore(SUBRELATION_EVAL_4_LOC, acc)
1327 }
1328 }
1329
1330 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1331 /* LOGUP WIDGET EVALUATION */
1332 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1333 // Note: Using beta powers for column batching and gamma for offset ensures soundness
1334 // beta and gamma must be independent challenges (they come from splitting the same hash)
1335 {
1336 let gamma := mload(GAMMA_CHALLENGE)
1337 let beta := mload(BETA_CHALLENGE)
1338 // Compute beta powers inline (β², β³) for lookup column batching
1339 let beta_sqr := mulmod(beta, beta, p)
1340 let beta_cube := mulmod(beta_sqr, beta, p)
1341
1342 // table_term = table_1 + γ + table_2 * β + table_3 * β² + table_4 * β³
1343 let t0 :=
1344 addmod(addmod(mload(TABLE1_EVAL_LOC), gamma, p), mulmod(mload(TABLE2_EVAL_LOC), beta, p), p)
1345 let t1 :=
1346 addmod(
1347 mulmod(mload(TABLE3_EVAL_LOC), beta_sqr, p),
1348 mulmod(mload(TABLE4_EVAL_LOC), beta_cube, p),
1349 p
1350 )
1351 let table_term := addmod(t0, t1, p)
1352
1353 // lookup_term = derived_entry_1 + γ + derived_entry_2 * β + derived_entry_3 * β² + q_index * β³
1354 t0 := addmod(
1355 addmod(mload(W1_EVAL_LOC), gamma, p),
1356 mulmod(mload(QR_EVAL_LOC), mload(W1_SHIFT_EVAL_LOC), p),
1357 p
1358 )
1359 t1 := addmod(mload(W2_EVAL_LOC), mulmod(mload(QM_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p), p)
1360 let t2 := addmod(mload(W3_EVAL_LOC), mulmod(mload(QC_EVAL_LOC), mload(W3_SHIFT_EVAL_LOC), p), p)
1361
1362 let lookup_term := addmod(t0, mulmod(t1, beta, p), p)
1363 lookup_term := addmod(lookup_term, mulmod(t2, beta_sqr, p), p)
1364 lookup_term := addmod(lookup_term, mulmod(mload(QO_EVAL_LOC), beta_cube, p), p)
1365
1366 let lookup_inverse := mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), table_term, p)
1367 let table_inverse := mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), lookup_term, p)
1368
1369 let inverse_exists_xor := addmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), mload(QLOOKUP_EVAL_LOC), p)
1370 inverse_exists_xor := addmod(
1371 inverse_exists_xor,
1372 sub(p, mulmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), mload(QLOOKUP_EVAL_LOC), p)),
1373 p
1374 )
1375
1376 let accumulator_none := mulmod(mulmod(lookup_term, table_term, p), mload(LOOKUP_INVERSES_EVAL_LOC), p)
1377 accumulator_none := addmod(accumulator_none, sub(p, inverse_exists_xor), p)
1378 accumulator_none := mulmod(accumulator_none, mload(POW_PARTIAL_EVALUATION_LOC), p)
1379
1380 let accumulator_one := mulmod(mload(QLOOKUP_EVAL_LOC), lookup_inverse, p)
1381 accumulator_one := addmod(
1382 accumulator_one,
1383 sub(p, mulmod(mload(LOOKUP_READ_COUNTS_EVAL_LOC), table_inverse, p)),
1384 p
1385 )
1386
1387 let read_tag := mload(LOOKUP_READ_TAGS_EVAL_LOC)
1388 let read_tag_boolean_relation := mulmod(read_tag, addmod(read_tag, P_SUB_1, p), p)
1389 read_tag_boolean_relation := mulmod(read_tag_boolean_relation, mload(POW_PARTIAL_EVALUATION_LOC), p)
1390
1391 mstore(SUBRELATION_EVAL_5_LOC, accumulator_none)
1392 mstore(SUBRELATION_EVAL_6_LOC, accumulator_one)
1393 mstore(SUBRELATION_EVAL_7_LOC, read_tag_boolean_relation)
1394 }
1395
1396 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1397 /* DELTA RANGE RELATION */
1398 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1399 {
1400 let minus_one := P_SUB_1
1401 let minus_two := P_SUB_2
1402 let minus_three := P_SUB_3
1403
1404 let delta_1 := addmod(mload(W2_EVAL_LOC), sub(p, mload(W1_EVAL_LOC)), p)
1405 let delta_2 := addmod(mload(W3_EVAL_LOC), sub(p, mload(W2_EVAL_LOC)), p)
1406 let delta_3 := addmod(mload(W4_EVAL_LOC), sub(p, mload(W3_EVAL_LOC)), p)
1407 let delta_4 := addmod(mload(W1_SHIFT_EVAL_LOC), sub(p, mload(W4_EVAL_LOC)), p)
1408
1409 {
1410 let acc := delta_1
1411 acc := mulmod(acc, addmod(delta_1, minus_one, p), p)
1412 acc := mulmod(acc, addmod(delta_1, minus_two, p), p)
1413 acc := mulmod(acc, addmod(delta_1, minus_three, p), p)
1414 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1415 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1416 mstore(SUBRELATION_EVAL_8_LOC, acc)
1417 }
1418
1419 {
1420 let acc := delta_2
1421 acc := mulmod(acc, addmod(delta_2, minus_one, p), p)
1422 acc := mulmod(acc, addmod(delta_2, minus_two, p), p)
1423 acc := mulmod(acc, addmod(delta_2, minus_three, p), p)
1424 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1425 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1426 mstore(SUBRELATION_EVAL_9_LOC, acc)
1427 }
1428
1429 {
1430 let acc := delta_3
1431 acc := mulmod(acc, addmod(delta_3, minus_one, p), p)
1432 acc := mulmod(acc, addmod(delta_3, minus_two, p), p)
1433 acc := mulmod(acc, addmod(delta_3, minus_three, p), p)
1434 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1435 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1436 mstore(SUBRELATION_EVAL_10_LOC, acc)
1437 }
1438
1439 {
1440 let acc := delta_4
1441 acc := mulmod(acc, addmod(delta_4, minus_one, p), p)
1442 acc := mulmod(acc, addmod(delta_4, minus_two, p), p)
1443 acc := mulmod(acc, addmod(delta_4, minus_three, p), p)
1444 acc := mulmod(acc, mload(QRANGE_EVAL_LOC), p)
1445 acc := mulmod(acc, mload(POW_PARTIAL_EVALUATION_LOC), p)
1446 mstore(SUBRELATION_EVAL_11_LOC, acc)
1447 }
1448 }
1449
1450 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1451 /* ELLIPTIC CURVE RELATION */
1452 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1453 {
1454 // Contribution 10 point addition, x-coordinate check
1455 // q_elliptic * (x3 + x2 + x1)(x2 - x1)(x2 - x1) - y2^2 - y1^2 + 2(y2y1)*q_sign = 0
1456 let x_diff := addmod(mload(EC_X_2), sub(p, mload(EC_X_1)), p)
1457 let y1_sqr := mulmod(mload(EC_Y_1), mload(EC_Y_1), p)
1458 {
1459 let y2_sqr := mulmod(mload(EC_Y_2), mload(EC_Y_2), p)
1460 let y1y2 := mulmod(mulmod(mload(EC_Y_1), mload(EC_Y_2), p), mload(EC_Q_SIGN), p)
1461 let x_add_identity := addmod(mload(EC_X_3), addmod(mload(EC_X_2), mload(EC_X_1), p), p)
1462 x_add_identity := mulmod(mulmod(x_add_identity, x_diff, p), x_diff, p)
1463 x_add_identity := addmod(x_add_identity, sub(p, y2_sqr), p)
1464 x_add_identity := addmod(x_add_identity, sub(p, y1_sqr), p)
1465 x_add_identity := addmod(x_add_identity, y1y2, p)
1466 x_add_identity := addmod(x_add_identity, y1y2, p)
1467
1468 let eval := mulmod(x_add_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1469 eval := mulmod(eval, mload(QELLIPTIC_EVAL_LOC), p)
1470 eval := mulmod(eval, addmod(1, sub(p, mload(EC_Q_IS_DOUBLE)), p), p)
1471 mstore(SUBRELATION_EVAL_12_LOC, eval)
1472 }
1473
1474 {
1475 let y1_plus_y3 := addmod(mload(EC_Y_1), mload(EC_Y_3), p)
1476 let y_diff := mulmod(mload(EC_Y_2), mload(EC_Q_SIGN), p)
1477 y_diff := addmod(y_diff, sub(p, mload(EC_Y_1)), p)
1478 let y_add_identity := mulmod(y1_plus_y3, x_diff, p)
1479 y_add_identity := addmod(
1480 y_add_identity,
1481 mulmod(addmod(mload(EC_X_3), sub(p, mload(EC_X_1)), p), y_diff, p),
1482 p
1483 )
1484
1485 let eval := mulmod(y_add_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1486 eval := mulmod(eval, mload(QELLIPTIC_EVAL_LOC), p)
1487 eval := mulmod(eval, addmod(1, sub(p, mload(EC_Q_IS_DOUBLE)), p), p)
1488 mstore(SUBRELATION_EVAL_13_LOC, eval)
1489 }
1490
1491 {
1492 let x_pow_4 := mulmod(addmod(y1_sqr, GRUMPKIN_CURVE_B_PARAMETER_NEGATED, p), mload(EC_X_1), p)
1493 let y1_sqr_mul_4 := addmod(y1_sqr, y1_sqr, p)
1494 y1_sqr_mul_4 := addmod(y1_sqr_mul_4, y1_sqr_mul_4, p)
1495
1496 let x1_pow_4_mul_9 := mulmod(x_pow_4, 9, p)
1497
1498 let ep_x_double_identity := addmod(mload(EC_X_3), addmod(mload(EC_X_1), mload(EC_X_1), p), p)
1499 ep_x_double_identity := mulmod(ep_x_double_identity, y1_sqr_mul_4, p)
1500 ep_x_double_identity := addmod(ep_x_double_identity, sub(p, x1_pow_4_mul_9), p)
1501
1502 let acc := mulmod(ep_x_double_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1503 acc := mulmod(mulmod(acc, mload(QELLIPTIC_EVAL_LOC), p), mload(EC_Q_IS_DOUBLE), p)
1504 acc := addmod(acc, mload(SUBRELATION_EVAL_12_LOC), p)
1505
1506 // Add to existing contribution
1507 mstore(SUBRELATION_EVAL_12_LOC, acc)
1508 }
1509
1510 {
1511 let x1_sqr_mul_3 :=
1512 mulmod(addmod(addmod(mload(EC_X_1), mload(EC_X_1), p), mload(EC_X_1), p), mload(EC_X_1), p)
1513 let y_double_identity :=
1514 mulmod(x1_sqr_mul_3, addmod(mload(EC_X_1), sub(p, mload(EC_X_3)), p), p)
1515 y_double_identity := addmod(
1516 y_double_identity,
1517 sub(
1518 p,
1519 mulmod(
1520 addmod(mload(EC_Y_1), mload(EC_Y_1), p),
1521 addmod(mload(EC_Y_1), mload(EC_Y_3), p),
1522 p
1523 )
1524 ),
1525 p
1526 )
1527
1528 let acc := mulmod(y_double_identity, mload(POW_PARTIAL_EVALUATION_LOC), p)
1529 acc := mulmod(mulmod(acc, mload(QELLIPTIC_EVAL_LOC), p), mload(EC_Q_IS_DOUBLE), p)
1530 acc := addmod(acc, mload(SUBRELATION_EVAL_13_LOC), p)
1531
1532 // Add to existing contribution
1533 mstore(SUBRELATION_EVAL_13_LOC, acc)
1534 }
1535 }
1536
1537 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1538 /* MEMORY RELATION */
1539 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1540 {
1541 {
1593 let memory_record_check := mulmod(mload(W3_EVAL_LOC), mload(ETA_THREE_CHALLENGE), p)
1594 memory_record_check := addmod(
1595 memory_record_check,
1596 mulmod(mload(W2_EVAL_LOC), mload(ETA_TWO_CHALLENGE), p),
1597 p
1598 )
1599 memory_record_check := addmod(
1600 memory_record_check,
1601 mulmod(mload(W1_EVAL_LOC), mload(ETA_CHALLENGE), p),
1602 p
1603 )
1604 memory_record_check := addmod(memory_record_check, mload(QC_EVAL_LOC), p)
1605
1606 let partial_record_check := memory_record_check
1607 memory_record_check := addmod(memory_record_check, sub(p, mload(W4_EVAL_LOC)), p)
1608
1609 mstore(AUX_MEMORY_CHECK_IDENTITY, memory_record_check)
1610
1626 // index_delta = w_1_omega - w_1
1627 let index_delta := addmod(mload(W1_SHIFT_EVAL_LOC), sub(p, mload(W1_EVAL_LOC)), p)
1628
1629 // record_delta = w_4_omega - w_4
1630 let record_delta := addmod(mload(W4_SHIFT_EVAL_LOC), sub(p, mload(W4_EVAL_LOC)), p)
1631
1632 // index_is_monotonically_increasing = index_delta * (index_delta - 1)
1633 let index_is_monotonically_increasing := mulmod(index_delta, addmod(index_delta, P_SUB_1, p), p)
1634
1635 // adjacent_values_match_if_adjacent_indices_match = record_delta * (1 - index_delta)
1636 let adjacent_values_match_if_adjacent_indices_match :=
1637 mulmod(record_delta, addmod(1, sub(p, index_delta), p), p)
1638
1639 mstore(
1640 SUBRELATION_EVAL_15_LOC,
1641 mulmod(
1642 adjacent_values_match_if_adjacent_indices_match,
1643 mulmod(
1644 mload(QL_EVAL_LOC),
1645 mulmod(
1646 mload(QR_EVAL_LOC),
1647 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1648 p
1649 ),
1650 p
1651 ),
1652 p
1653 )
1654 )
1655
1656 // ROM_CONSISTENCY_CHECK_2
1657 mstore(
1658 SUBRELATION_EVAL_16_LOC,
1659 mulmod(
1660 index_is_monotonically_increasing,
1661 mulmod(
1662 mload(QL_EVAL_LOC),
1663 mulmod(
1664 mload(QR_EVAL_LOC),
1665 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1666 p
1667 ),
1668 p
1669 ),
1670 p
1671 )
1672 )
1673
1674 mstore(
1675 AUX_ROM_CONSISTENCY_CHECK_IDENTITY,
1676 mulmod(memory_record_check, mulmod(mload(QL_EVAL_LOC), mload(QR_EVAL_LOC), p), p)
1677 )
1678
1679 {
1706 let next_gate_access_type := mulmod(mload(W3_SHIFT_EVAL_LOC), mload(ETA_THREE_CHALLENGE), p)
1707 next_gate_access_type := addmod(
1708 next_gate_access_type,
1709 mulmod(mload(W2_SHIFT_EVAL_LOC), mload(ETA_TWO_CHALLENGE), p),
1710 p
1711 )
1712 next_gate_access_type := addmod(
1713 next_gate_access_type,
1714 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(ETA_CHALLENGE), p),
1715 p
1716 )
1717 next_gate_access_type := addmod(mload(W4_SHIFT_EVAL_LOC), sub(p, next_gate_access_type), p)
1718
1719 // value_delta = w_3_omega - w_3
1720 let value_delta := addmod(mload(W3_SHIFT_EVAL_LOC), sub(p, mload(W3_EVAL_LOC)), p)
1721 // adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation = (1 - index_delta) * value_delta * (1 - next_gate_access_type);
1722
1723 let adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation :=
1724 mulmod(
1725 addmod(1, sub(p, index_delta), p),
1726 mulmod(value_delta, addmod(1, sub(p, next_gate_access_type), p), p),
1727 p
1728 )
1729
1730 // We can't apply the RAM consistency check identity on the final entry in the sorted list (the wires in the
1731 // next gate would make the identity fail). We need to validate that its 'access type' bool is correct. Can't
1732 // do with an arithmetic gate because of the `eta` factors. We need to check that the *next* gate's access
1733 // type is correct, to cover this edge case
1734 // deg 2 or 4
1740 let access_type := addmod(mload(W4_EVAL_LOC), sub(p, partial_record_check), p)
1741 let access_check := mulmod(access_type, addmod(access_type, P_SUB_1, p), p)
1742 let next_gate_access_type_is_boolean :=
1743 mulmod(next_gate_access_type, addmod(next_gate_access_type, P_SUB_1, p), p)
1744
1745 // scaled_activation_selector = q_arith * q_aux * alpha
1746 let scaled_activation_selector :=
1747 mulmod(
1748 mload(QO_EVAL_LOC),
1749 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1750 p
1751 )
1752
1753 mstore(
1754 SUBRELATION_EVAL_17_LOC,
1755 mulmod(
1756 adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation,
1757 scaled_activation_selector,
1758 p
1759 )
1760 )
1761
1762 mstore(
1763 SUBRELATION_EVAL_18_LOC,
1764 mulmod(index_is_monotonically_increasing, scaled_activation_selector, p)
1765 )
1766
1767 mstore(
1768 SUBRELATION_EVAL_19_LOC,
1769 mulmod(next_gate_access_type_is_boolean, scaled_activation_selector, p)
1770 )
1771
1772 mstore(AUX_RAM_CONSISTENCY_CHECK_IDENTITY, mulmod(access_check, mload(QO_EVAL_LOC), p))
1773 }
1774
1775 {
1776 // timestamp_delta = w_2_omega - w_2
1777 let timestamp_delta := addmod(mload(W2_SHIFT_EVAL_LOC), sub(p, mload(W2_EVAL_LOC)), p)
1778
1779 // RAM_timestamp_check_identity = (1 - index_delta) * timestamp_delta - w_3
1780 let RAM_TIMESTAMP_CHECK_IDENTITY :=
1781 addmod(
1782 mulmod(timestamp_delta, addmod(1, sub(p, index_delta), p), p),
1783 sub(p, mload(W3_EVAL_LOC)),
1784 p
1785 )
1786
1798 let memory_identity := mload(AUX_ROM_CONSISTENCY_CHECK_IDENTITY)
1799 memory_identity := addmod(
1800 memory_identity,
1801 mulmod(
1802 RAM_TIMESTAMP_CHECK_IDENTITY,
1803 mulmod(mload(Q4_EVAL_LOC), mload(QL_EVAL_LOC), p),
1804 p
1805 ),
1806 p
1807 )
1808
1809 memory_identity := addmod(
1810 memory_identity,
1811 mulmod(
1812 mload(AUX_MEMORY_CHECK_IDENTITY),
1813 mulmod(mload(QM_EVAL_LOC), mload(QL_EVAL_LOC), p),
1814 p
1815 ),
1816 p
1817 )
1818 memory_identity := addmod(memory_identity, mload(AUX_RAM_CONSISTENCY_CHECK_IDENTITY), p)
1819
1820 memory_identity := mulmod(
1821 memory_identity,
1822 mulmod(mload(QMEMORY_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1823 p
1824 )
1825 mstore(SUBRELATION_EVAL_14_LOC, memory_identity)
1826 }
1827 }
1828 }
1829
1830 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
1831 /* NON NATIVE FIELD RELATION */
1832 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
1833 {
1853 let limb_subproduct :=
1854 addmod(
1855 mulmod(mload(W1_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p),
1856 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(W2_EVAL_LOC), p),
1857 p
1858 )
1859
1860 let non_native_field_gate_2 :=
1861 addmod(
1862 addmod(
1863 mulmod(mload(W1_EVAL_LOC), mload(W4_EVAL_LOC), p),
1864 mulmod(mload(W2_EVAL_LOC), mload(W3_EVAL_LOC), p),
1865 p
1866 ),
1867 sub(p, mload(W3_SHIFT_EVAL_LOC)),
1868 p
1869 )
1870 non_native_field_gate_2 := mulmod(non_native_field_gate_2, LIMB_SIZE, p)
1871 non_native_field_gate_2 := addmod(non_native_field_gate_2, sub(p, mload(W4_SHIFT_EVAL_LOC)), p)
1872 non_native_field_gate_2 := addmod(non_native_field_gate_2, limb_subproduct, p)
1873 non_native_field_gate_2 := mulmod(non_native_field_gate_2, mload(Q4_EVAL_LOC), p)
1874
1875 limb_subproduct := mulmod(limb_subproduct, LIMB_SIZE, p)
1876 limb_subproduct := addmod(
1877 limb_subproduct,
1878 mulmod(mload(W1_SHIFT_EVAL_LOC), mload(W2_SHIFT_EVAL_LOC), p),
1879 p
1880 )
1881
1882 let non_native_field_gate_1 :=
1883 mulmod(
1884 addmod(limb_subproduct, sub(p, addmod(mload(W3_EVAL_LOC), mload(W4_EVAL_LOC), p)), p),
1885 mload(QO_EVAL_LOC),
1886 p
1887 )
1888
1889 let non_native_field_gate_3 :=
1890 mulmod(
1891 addmod(
1892 addmod(limb_subproduct, mload(W4_EVAL_LOC), p),
1893 sub(p, addmod(mload(W3_SHIFT_EVAL_LOC), mload(W4_SHIFT_EVAL_LOC), p)),
1894 p
1895 ),
1896 mload(QM_EVAL_LOC),
1897 p
1898 )
1899 let non_native_field_identity :=
1900 mulmod(
1901 addmod(
1902 addmod(non_native_field_gate_1, non_native_field_gate_2, p),
1903 non_native_field_gate_3,
1904 p
1905 ),
1906 mload(QR_EVAL_LOC),
1907 p
1908 )
1909
1910 mstore(AUX_NON_NATIVE_FIELD_IDENTITY, non_native_field_identity)
1911 }
1912
1913 {
1927 let limb_accumulator_1 := mulmod(mload(W2_SHIFT_EVAL_LOC), SUBLIMB_SHIFT, p)
1928 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W1_SHIFT_EVAL_LOC), p)
1929 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1930 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W3_EVAL_LOC), p)
1931 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1932 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W2_EVAL_LOC), p)
1933 limb_accumulator_1 := mulmod(limb_accumulator_1, SUBLIMB_SHIFT, p)
1934 limb_accumulator_1 := addmod(limb_accumulator_1, mload(W1_EVAL_LOC), p)
1935 limb_accumulator_1 := addmod(limb_accumulator_1, sub(p, mload(W4_EVAL_LOC)), p)
1936 limb_accumulator_1 := mulmod(limb_accumulator_1, mload(Q4_EVAL_LOC), p)
1937
1951 let limb_accumulator_2 := mulmod(mload(W3_SHIFT_EVAL_LOC), SUBLIMB_SHIFT, p)
1952 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W2_SHIFT_EVAL_LOC), p)
1953 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1954 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W1_SHIFT_EVAL_LOC), p)
1955 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1956 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W4_EVAL_LOC), p)
1957 limb_accumulator_2 := mulmod(limb_accumulator_2, SUBLIMB_SHIFT, p)
1958 limb_accumulator_2 := addmod(limb_accumulator_2, mload(W3_EVAL_LOC), p)
1959 limb_accumulator_2 := addmod(limb_accumulator_2, sub(p, mload(W4_SHIFT_EVAL_LOC)), p)
1960 limb_accumulator_2 := mulmod(limb_accumulator_2, mload(QM_EVAL_LOC), p)
1961
1962 let limb_accumulator_identity := addmod(limb_accumulator_1, limb_accumulator_2, p)
1963 limb_accumulator_identity := mulmod(limb_accumulator_identity, mload(QO_EVAL_LOC), p)
1964
1965 let nnf_identity := addmod(mload(AUX_NON_NATIVE_FIELD_IDENTITY), limb_accumulator_identity, p)
1966 nnf_identity := mulmod(
1967 nnf_identity,
1968 mulmod(mload(QNNF_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p),
1969 p
1970 )
1971
1972 mstore(SUBRELATION_EVAL_20_LOC, nnf_identity)
1973 }
1974
1975 /*
1976 * Poseidon External Relation
1977 */
1978 {
1979 let s1 := addmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
1980 let s2 := addmod(mload(W2_EVAL_LOC), mload(QR_EVAL_LOC), p)
1981 let s3 := addmod(mload(W3_EVAL_LOC), mload(QO_EVAL_LOC), p)
1982 let s4 := addmod(mload(W4_EVAL_LOC), mload(Q4_EVAL_LOC), p)
1983
1984 // u1 := s1 * s1 * s1 * s1 * s1;
1985 let t0 := mulmod(s1, s1, p)
1986 let u1 := mulmod(t0, mulmod(t0, s1, p), p)
1987
1988 // u2 := s2 * s2 * s2 * s2 * s2;
1989 t0 := mulmod(s2, s2, p)
1990 let u2 := mulmod(t0, mulmod(t0, s2, p), p)
1991
1992 // u3 := s3 * s3 * s3 * s3 * s3;
1993 t0 := mulmod(s3, s3, p)
1994 let u3 := mulmod(t0, mulmod(t0, s3, p), p)
1995
1996 // u4 := s4 * s4 * s4 * s4 * s4;
1997 t0 := mulmod(s4, s4, p)
1998 let u4 := mulmod(t0, mulmod(t0, s4, p), p)
1999
2000 // matrix mul v = M_E * u with 14 additions
2001 t0 := addmod(u1, u2, p)
2002 let t1 := addmod(u3, u4, p)
2003
2004 let t2 := addmod(u2, u2, p)
2005 t2 := addmod(t2, t1, p)
2006
2007 let t3 := addmod(u4, u4, p)
2008 t3 := addmod(t3, t0, p)
2009
2010 let v4 := addmod(t1, t1, p)
2011 v4 := addmod(v4, v4, p)
2012 v4 := addmod(v4, t3, p)
2013
2014 let v2 := addmod(t0, t0, p)
2015 v2 := addmod(v2, v2, p)
2016 v2 := addmod(v2, t2, p)
2017
2018 let v1 := addmod(t3, v2, p)
2019 let v3 := addmod(t2, v4, p)
2020
2021 let q_pos_by_scaling :=
2022 mulmod(mload(QPOSEIDON2_EXTERNAL_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p)
2023
2024 mstore(
2025 SUBRELATION_EVAL_21_LOC,
2026 mulmod(q_pos_by_scaling, addmod(v1, sub(p, mload(W1_SHIFT_EVAL_LOC)), p), p)
2027 )
2028
2029 mstore(
2030 SUBRELATION_EVAL_22_LOC,
2031 mulmod(q_pos_by_scaling, addmod(v2, sub(p, mload(W2_SHIFT_EVAL_LOC)), p), p)
2032 )
2033
2034 mstore(
2035 SUBRELATION_EVAL_23_LOC,
2036 mulmod(q_pos_by_scaling, addmod(v3, sub(p, mload(W3_SHIFT_EVAL_LOC)), p), p)
2037 )
2038
2039 mstore(
2040 SUBRELATION_EVAL_24_LOC,
2041 mulmod(q_pos_by_scaling, addmod(v4, sub(p, mload(W4_SHIFT_EVAL_LOC)), p), p)
2042 )
2043 }
2044
2045 /*
2046 * Poseidon Internal Relation
2047 */
2048 {
2049 let s1 := addmod(mload(W1_EVAL_LOC), mload(QL_EVAL_LOC), p)
2050
2051 // apply s-box round
2052 let t0 := mulmod(s1, s1, p)
2053 let u1 := mulmod(t0, mulmod(t0, s1, p), p)
2054 let u2 := mload(W2_EVAL_LOC)
2055 let u3 := mload(W3_EVAL_LOC)
2056 let u4 := mload(W4_EVAL_LOC)
2057
2058 // matrix mul v = M_I * u 4 muls and 7 additions
2059 let u_sum := addmod(u1, u2, p)
2060 u_sum := addmod(u_sum, addmod(u3, u4, p), p)
2061
2062 let q_pos_by_scaling :=
2063 mulmod(mload(QPOSEIDON2_INTERNAL_EVAL_LOC), mload(POW_PARTIAL_EVALUATION_LOC), p)
2064
2065 let v1 := addmod(mulmod(u1, POS_INTERNAL_MATRIX_D_0, p), u_sum, p)
2066
2067 mstore(
2068 SUBRELATION_EVAL_25_LOC,
2069 mulmod(q_pos_by_scaling, addmod(v1, sub(p, mload(W1_SHIFT_EVAL_LOC)), p), p)
2070 )
2071 let v2 := addmod(mulmod(u2, POS_INTERNAL_MATRIX_D_1, p), u_sum, p)
2072
2073 mstore(
2074 SUBRELATION_EVAL_26_LOC,
2075 mulmod(q_pos_by_scaling, addmod(v2, sub(p, mload(W2_SHIFT_EVAL_LOC)), p), p)
2076 )
2077 let v3 := addmod(mulmod(u3, POS_INTERNAL_MATRIX_D_2, p), u_sum, p)
2078
2079 mstore(
2080 SUBRELATION_EVAL_27_LOC,
2081 mulmod(q_pos_by_scaling, addmod(v3, sub(p, mload(W3_SHIFT_EVAL_LOC)), p), p)
2082 )
2083
2084 let v4 := addmod(mulmod(u4, POS_INTERNAL_MATRIX_D_3, p), u_sum, p)
2085 mstore(
2086 SUBRELATION_EVAL_28_LOC,
2087 mulmod(q_pos_by_scaling, addmod(v4, sub(p, mload(W4_SHIFT_EVAL_LOC)), p), p)
2088 )
2089 }
2090
2091 // Scale and batch subrelations by subrelation challenges
2092 // linear combination of subrelations
2093 let accumulator := mload(SUBRELATION_EVAL_0_LOC)
2094
2095 // Below is an unrolled variant of the following loop
2096 // for (uint256 i = 1; i < NUMBER_OF_SUBRELATIONS; ++i) {
2097 // accumulator = accumulator + evaluations[i] * subrelationChallenges[i - 1];
2098 // }
2099
2100 accumulator := addmod(
2101 accumulator,
2102 mulmod(mload(SUBRELATION_EVAL_1_LOC), mload(ALPHA_CHALLENGE_0), p),
2103 p
2104 )
2105 accumulator := addmod(
2106 accumulator,
2107 mulmod(mload(SUBRELATION_EVAL_2_LOC), mload(ALPHA_CHALLENGE_1), p),
2108 p
2109 )
2110 accumulator := addmod(
2111 accumulator,
2112 mulmod(mload(SUBRELATION_EVAL_3_LOC), mload(ALPHA_CHALLENGE_2), p),
2113 p
2114 )
2115 accumulator := addmod(
2116 accumulator,
2117 mulmod(mload(SUBRELATION_EVAL_4_LOC), mload(ALPHA_CHALLENGE_3), p),
2118 p
2119 )
2120 accumulator := addmod(
2121 accumulator,
2122 mulmod(mload(SUBRELATION_EVAL_5_LOC), mload(ALPHA_CHALLENGE_4), p),
2123 p
2124 )
2125 accumulator := addmod(
2126 accumulator,
2127 mulmod(mload(SUBRELATION_EVAL_6_LOC), mload(ALPHA_CHALLENGE_5), p),
2128 p
2129 )
2130 accumulator := addmod(
2131 accumulator,
2132 mulmod(mload(SUBRELATION_EVAL_7_LOC), mload(ALPHA_CHALLENGE_6), p),
2133 p
2134 )
2135 accumulator := addmod(
2136 accumulator,
2137 mulmod(mload(SUBRELATION_EVAL_8_LOC), mload(ALPHA_CHALLENGE_7), p),
2138 p
2139 )
2140 accumulator := addmod(
2141 accumulator,
2142 mulmod(mload(SUBRELATION_EVAL_9_LOC), mload(ALPHA_CHALLENGE_8), p),
2143 p
2144 )
2145 accumulator := addmod(
2146 accumulator,
2147 mulmod(mload(SUBRELATION_EVAL_10_LOC), mload(ALPHA_CHALLENGE_9), p),
2148 p
2149 )
2150 accumulator := addmod(
2151 accumulator,
2152 mulmod(mload(SUBRELATION_EVAL_11_LOC), mload(ALPHA_CHALLENGE_10), p),
2153 p
2154 )
2155 accumulator := addmod(
2156 accumulator,
2157 mulmod(mload(SUBRELATION_EVAL_12_LOC), mload(ALPHA_CHALLENGE_11), p),
2158 p
2159 )
2160 accumulator := addmod(
2161 accumulator,
2162 mulmod(mload(SUBRELATION_EVAL_13_LOC), mload(ALPHA_CHALLENGE_12), p),
2163 p
2164 )
2165 accumulator := addmod(
2166 accumulator,
2167 mulmod(mload(SUBRELATION_EVAL_14_LOC), mload(ALPHA_CHALLENGE_13), p),
2168 p
2169 )
2170 accumulator := addmod(
2171 accumulator,
2172 mulmod(mload(SUBRELATION_EVAL_15_LOC), mload(ALPHA_CHALLENGE_14), p),
2173 p
2174 )
2175 accumulator := addmod(
2176 accumulator,
2177 mulmod(mload(SUBRELATION_EVAL_16_LOC), mload(ALPHA_CHALLENGE_15), p),
2178 p
2179 )
2180 accumulator := addmod(
2181 accumulator,
2182 mulmod(mload(SUBRELATION_EVAL_17_LOC), mload(ALPHA_CHALLENGE_16), p),
2183 p
2184 )
2185 accumulator := addmod(
2186 accumulator,
2187 mulmod(mload(SUBRELATION_EVAL_18_LOC), mload(ALPHA_CHALLENGE_17), p),
2188 p
2189 )
2190 accumulator := addmod(
2191 accumulator,
2192 mulmod(mload(SUBRELATION_EVAL_19_LOC), mload(ALPHA_CHALLENGE_18), p),
2193 p
2194 )
2195 accumulator := addmod(
2196 accumulator,
2197 mulmod(mload(SUBRELATION_EVAL_20_LOC), mload(ALPHA_CHALLENGE_19), p),
2198 p
2199 )
2200 accumulator := addmod(
2201 accumulator,
2202 mulmod(mload(SUBRELATION_EVAL_21_LOC), mload(ALPHA_CHALLENGE_20), p),
2203 p
2204 )
2205 accumulator := addmod(
2206 accumulator,
2207 mulmod(mload(SUBRELATION_EVAL_22_LOC), mload(ALPHA_CHALLENGE_21), p),
2208 p
2209 )
2210 accumulator := addmod(
2211 accumulator,
2212 mulmod(mload(SUBRELATION_EVAL_23_LOC), mload(ALPHA_CHALLENGE_22), p),
2213 p
2214 )
2215 accumulator := addmod(
2216 accumulator,
2217 mulmod(mload(SUBRELATION_EVAL_24_LOC), mload(ALPHA_CHALLENGE_23), p),
2218 p
2219 )
2220 accumulator := addmod(
2221 accumulator,
2222 mulmod(mload(SUBRELATION_EVAL_25_LOC), mload(ALPHA_CHALLENGE_24), p),
2223 p
2224 )
2225 accumulator := addmod(
2226 accumulator,
2227 mulmod(mload(SUBRELATION_EVAL_26_LOC), mload(ALPHA_CHALLENGE_25), p),
2228 p
2229 )
2230 accumulator := addmod(
2231 accumulator,
2232 mulmod(mload(SUBRELATION_EVAL_27_LOC), mload(ALPHA_CHALLENGE_26), p),
2233 p
2234 )
2235 accumulator := addmod(
2236 accumulator,
2237 mulmod(mload(SUBRELATION_EVAL_28_LOC), mload(ALPHA_CHALLENGE_27), p),
2238 p
2239 )
2240
2241 // ZK final check: grandHonkRelationSum * (1 - evaluation) + libraEvaluation * libraChallenge == roundTargetSum
2242 // where evaluation = product(u[2] * u[3] * ... * u[LOG_N - 1])
2243 {
2244 // Row-disabling polynomial: 1 - ∏_{i≥2}(1 - u_i)
2245 let evaluation := 1
2246 let u_off := SUM_U_CHALLENGE_2
2247 for { let i := 2 } lt(i, LOG_N) { i := add(i, 1) } {
2248 // evaluation = evaluation * (1 - sumCheckUChallenges[i])
2249 let one_minus_u := addmod(1, sub(p, mload(u_off)), p)
2250 evaluation := mulmod(evaluation, one_minus_u, p)
2251 u_off := add(u_off, 0x20)
2252 }
2253
2254 // adjustedSum = accumulator * (1 - evaluation) + libraEvaluation * libraChallenge
2255 let one_minus_eval := addmod(1, sub(p, evaluation), p)
2256 let adjusted_sum := addmod(
2257 mulmod(accumulator, one_minus_eval, p),
2258 mulmod(mload(LIBRA_EVALUATION_LOC), mload(LIBRA_CHALLENGE), p),
2259 p
2260 )
2261
2262 let sumcheck_valid := eq(adjusted_sum, mload(FINAL_ROUND_TARGET_LOC))
2263
2264 if iszero(sumcheck_valid) {
2265 mstore(0x00, SUMCHECK_FAILED_SELECTOR)
2266 revert(0x00, 0x04)
2267 }
2268 }
2269 }
2270
2271 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
2272 /* SUMCHECK -- Complete */
2273 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
2274
2275 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
2276 /* SHPLEMINI */
2277 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
2278
2279 // ============= SHPLEMINI INVERSES ==============
2280 // Inverses are already at their designated addresses from batch inversion.
2281 let unshifted_scalar := 0
2282 let shifted_scalar := 0
2283 {
2284 let gemini_r_inv := mload(GEMINI_R_INV_LOC)
2285
2286 // Compute unshifted_scalar and shifted_scalar using the copied inverses
2287 let pos_inverted_denominator := mload(POS_INVERTED_DENOM_0_LOC)
2288 let neg_inverted_denominator := mload(NEG_INVERTED_DENOM_0_LOC)
2289 let shplonk_nu := mload(SHPLONK_NU_CHALLENGE)
2290
2291 unshifted_scalar := addmod(pos_inverted_denominator, mulmod(shplonk_nu, neg_inverted_denominator, p), p)
2292
2293 shifted_scalar := mulmod(
2294 gemini_r_inv, // (1 / gemini_r_challenge)
2295 // (inverse_vanishing_evals[0]) - (shplonk_nu * inverse_vanishing_evals[1])
2296 addmod(
2297 pos_inverted_denominator,
2298 // - (shplonk_nu * inverse_vanishing_evals[1])
2299 sub(p, mulmod(shplonk_nu, neg_inverted_denominator, p)),
2300 p
2301 ),
2302 p
2303 )
2304 }
2305
2306 // Commitment Accumulation (MSM via sequential ecAdd/ecMul):
2307 // For each commitment C_i with batch scalar s_i, we compute:
2308 // accumulator += s_i * C_i
2309 // The commitments include: shplonk_Q, gemini_masking (ZK), VK points,
2310 // wire commitments, lookup commitments, Z_PERM, libra (ZK),
2311 // gemini fold univariates. The KZG quotient is handled separately.
2312 // The final accumulator is the LHS of the pairing equation.
2313
2314 // Accumulators
2315 let batching_challenge := 1
2316 let batched_evaluation := 0
2317
2318 let neg_unshifted_scalar := sub(p, unshifted_scalar)
2319 let neg_shifted_scalar := sub(p, shifted_scalar)
2320
2321 let rho := mload(RHO_CHALLENGE)
2322
2323 // Unrolled for the loop below - where NUMBER_UNSHIFTED = 37 (ZK: includes gemini_masking_poly)
2324 // For ZK: evaluations array is [gemini_masking_poly, qm, qc, ql, qr, ...]
2325 // for (uint256 i = 1; i <= NUMBER_UNSHIFTED; ++i) {
2326 // scalars[i] = mem.unshiftedScalar.neg() * mem.batchingChallenge;
2327 // mem.batchedEvaluation = mem.batchedEvaluation + (proof.sumcheckEvaluations[i - NUM_MASKING_POLYNOMIALS] * mem.batchingChallenge);
2328 // mem.batchingChallenge = mem.batchingChallenge * tp.rho;
2329 // }
2330
2331 // Calculate the scalars and batching challenge for the unshifted entities
2332 // 0: GEMINI_MASKING_EVAL_LOC (ZK entity index 0)
2333 mstore(BATCH_SCALAR_1_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2334 batched_evaluation := addmod(batched_evaluation, mulmod(mload(GEMINI_MASKING_EVAL_LOC), batching_challenge, p), p)
2335 batching_challenge := mulmod(batching_challenge, rho, p)
2336
2337 // 1: QM_EVAL_LOC
2338 mstore(BATCH_SCALAR_2_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2339 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QM_EVAL_LOC), batching_challenge, p), p)
2340 batching_challenge := mulmod(batching_challenge, rho, p)
2341
2342 // 2: QC_EVAL_LOC
2343 mstore(BATCH_SCALAR_3_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2344 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QC_EVAL_LOC), batching_challenge, p), p)
2345 batching_challenge := mulmod(batching_challenge, rho, p)
2346
2347 // 3: QL_EVAL_LOC
2348 mstore(BATCH_SCALAR_4_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2349 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QL_EVAL_LOC), batching_challenge, p), p)
2350 batching_challenge := mulmod(batching_challenge, rho, p)
2351
2352 // 4: QR_EVAL_LOC
2353 mstore(BATCH_SCALAR_5_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2354 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QR_EVAL_LOC), batching_challenge, p), p)
2355 batching_challenge := mulmod(batching_challenge, rho, p)
2356
2357 // 5: QO_EVAL_LOC
2358 mstore(BATCH_SCALAR_6_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2359 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QO_EVAL_LOC), batching_challenge, p), p)
2360 batching_challenge := mulmod(batching_challenge, rho, p)
2361
2362 // 6: Q4_EVAL_LOC
2363 mstore(BATCH_SCALAR_7_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2364 batched_evaluation := addmod(batched_evaluation, mulmod(mload(Q4_EVAL_LOC), batching_challenge, p), p)
2365 batching_challenge := mulmod(batching_challenge, rho, p)
2366
2367 // 7: QLOOKUP_EVAL_LOC
2368 mstore(BATCH_SCALAR_8_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2369 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QLOOKUP_EVAL_LOC), batching_challenge, p), p)
2370 batching_challenge := mulmod(batching_challenge, rho, p)
2371
2372 // 8: QARITH_EVAL_LOC
2373 mstore(BATCH_SCALAR_9_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2374 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QARITH_EVAL_LOC), batching_challenge, p), p)
2375 batching_challenge := mulmod(batching_challenge, rho, p)
2376
2377 // 9: QRANGE_EVAL_LOC
2378 mstore(BATCH_SCALAR_10_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2379 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QRANGE_EVAL_LOC), batching_challenge, p), p)
2380 batching_challenge := mulmod(batching_challenge, rho, p)
2381
2382 // 10: QELLIPTIC_EVAL_LOC
2383 mstore(BATCH_SCALAR_11_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2384 batched_evaluation := addmod(
2385 batched_evaluation,
2386 mulmod(mload(QELLIPTIC_EVAL_LOC), batching_challenge, p),
2387 p
2388 )
2389 batching_challenge := mulmod(batching_challenge, rho, p)
2390
2391 // 11: QMEMORY_EVAL_LOC
2392 mstore(BATCH_SCALAR_12_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2393 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QMEMORY_EVAL_LOC), batching_challenge, p), p)
2394 batching_challenge := mulmod(batching_challenge, rho, p)
2395
2396 // 12: QNNF_EVAL_LOC
2397 mstore(BATCH_SCALAR_13_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2398 batched_evaluation := addmod(batched_evaluation, mulmod(mload(QNNF_EVAL_LOC), batching_challenge, p), p)
2399 batching_challenge := mulmod(batching_challenge, rho, p)
2400
2401 // 13: QPOSEIDON2_EXTERNAL_EVAL_LOC
2402 mstore(BATCH_SCALAR_14_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2403 batched_evaluation := addmod(
2404 batched_evaluation,
2405 mulmod(mload(QPOSEIDON2_EXTERNAL_EVAL_LOC), batching_challenge, p),
2406 p
2407 )
2408 batching_challenge := mulmod(batching_challenge, rho, p)
2409
2410 // 14: QPOSEIDON2_INTERNAL_EVAL_LOC
2411 mstore(BATCH_SCALAR_15_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2412 batched_evaluation := addmod(
2413 batched_evaluation,
2414 mulmod(mload(QPOSEIDON2_INTERNAL_EVAL_LOC), batching_challenge, p),
2415 p
2416 )
2417 batching_challenge := mulmod(batching_challenge, rho, p)
2418
2419 // 15: SIGMA1_EVAL_LOC
2420 mstore(BATCH_SCALAR_16_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2421 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA1_EVAL_LOC), batching_challenge, p), p)
2422 batching_challenge := mulmod(batching_challenge, rho, p)
2423
2424 // 16: SIGMA2_EVAL_LOC
2425 mstore(BATCH_SCALAR_17_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2426 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA2_EVAL_LOC), batching_challenge, p), p)
2427 batching_challenge := mulmod(batching_challenge, rho, p)
2428
2429 // 17: SIGMA3_EVAL_LOC
2430 mstore(BATCH_SCALAR_18_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2431 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA3_EVAL_LOC), batching_challenge, p), p)
2432 batching_challenge := mulmod(batching_challenge, rho, p)
2433
2434 // 18: SIGMA4_EVAL_LOC
2435 mstore(BATCH_SCALAR_19_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2436 batched_evaluation := addmod(batched_evaluation, mulmod(mload(SIGMA4_EVAL_LOC), batching_challenge, p), p)
2437 batching_challenge := mulmod(batching_challenge, rho, p)
2438
2439 // 19: ID1_EVAL_LOC
2440 mstore(BATCH_SCALAR_20_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2441 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID1_EVAL_LOC), batching_challenge, p), p)
2442 batching_challenge := mulmod(batching_challenge, rho, p)
2443
2444 // 20: ID2_EVAL_LOC
2445 mstore(BATCH_SCALAR_21_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2446 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID2_EVAL_LOC), batching_challenge, p), p)
2447 batching_challenge := mulmod(batching_challenge, rho, p)
2448
2449 // 21: ID3_EVAL_LOC
2450 mstore(BATCH_SCALAR_22_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2451 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID3_EVAL_LOC), batching_challenge, p), p)
2452 batching_challenge := mulmod(batching_challenge, rho, p)
2453
2454 // 22: ID4_EVAL_LOC
2455 mstore(BATCH_SCALAR_23_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2456 batched_evaluation := addmod(batched_evaluation, mulmod(mload(ID4_EVAL_LOC), batching_challenge, p), p)
2457 batching_challenge := mulmod(batching_challenge, rho, p)
2458
2459 // 23: TABLE1_EVAL_LOC
2460 mstore(BATCH_SCALAR_24_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2461 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE1_EVAL_LOC), batching_challenge, p), p)
2462 batching_challenge := mulmod(batching_challenge, rho, p)
2463
2464 // 24: TABLE2_EVAL_LOC
2465 mstore(BATCH_SCALAR_25_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2466 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE2_EVAL_LOC), batching_challenge, p), p)
2467 batching_challenge := mulmod(batching_challenge, rho, p)
2468
2469 // 25: TABLE3_EVAL_LOC
2470 mstore(BATCH_SCALAR_26_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2471 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE3_EVAL_LOC), batching_challenge, p), p)
2472 batching_challenge := mulmod(batching_challenge, rho, p)
2473
2474 // 26: TABLE4_EVAL_LOC
2475 mstore(BATCH_SCALAR_27_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2476 batched_evaluation := addmod(batched_evaluation, mulmod(mload(TABLE4_EVAL_LOC), batching_challenge, p), p)
2477 batching_challenge := mulmod(batching_challenge, rho, p)
2478
2479 // 27: LAGRANGE_FIRST_EVAL_LOC
2480 mstore(BATCH_SCALAR_28_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2481 batched_evaluation := addmod(
2482 batched_evaluation,
2483 mulmod(mload(LAGRANGE_FIRST_EVAL_LOC), batching_challenge, p),
2484 p
2485 )
2486 batching_challenge := mulmod(batching_challenge, rho, p)
2487
2488 // 28: LAGRANGE_LAST_EVAL_LOC
2489 mstore(BATCH_SCALAR_29_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2490 batched_evaluation := addmod(
2491 batched_evaluation,
2492 mulmod(mload(LAGRANGE_LAST_EVAL_LOC), batching_challenge, p),
2493 p
2494 )
2495 batching_challenge := mulmod(batching_challenge, rho, p)
2496
2497 // 29: W1_EVAL_LOC
2498 mstore(BATCH_SCALAR_30_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2499 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W1_EVAL_LOC), batching_challenge, p), p)
2500 batching_challenge := mulmod(batching_challenge, rho, p)
2501
2502 // 30: W2_EVAL_LOC
2503 mstore(BATCH_SCALAR_31_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2504 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W2_EVAL_LOC), batching_challenge, p), p)
2505 batching_challenge := mulmod(batching_challenge, rho, p)
2506
2507 // 31: W3_EVAL_LOC
2508 mstore(BATCH_SCALAR_32_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2509 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W3_EVAL_LOC), batching_challenge, p), p)
2510 batching_challenge := mulmod(batching_challenge, rho, p)
2511
2512 // 32: W4_EVAL_LOC
2513 mstore(BATCH_SCALAR_33_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2514 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W4_EVAL_LOC), batching_challenge, p), p)
2515 batching_challenge := mulmod(batching_challenge, rho, p)
2516
2517 // 33: Z_PERM_EVAL_LOC
2518 mstore(BATCH_SCALAR_34_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2519 batched_evaluation := addmod(batched_evaluation, mulmod(mload(Z_PERM_EVAL_LOC), batching_challenge, p), p)
2520 batching_challenge := mulmod(batching_challenge, rho, p)
2521
2522 // 34: LOOKUP_INVERSES_EVAL_LOC
2523 mstore(BATCH_SCALAR_35_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2524 batched_evaluation := addmod(
2525 batched_evaluation,
2526 mulmod(mload(LOOKUP_INVERSES_EVAL_LOC), batching_challenge, p),
2527 p
2528 )
2529 batching_challenge := mulmod(batching_challenge, rho, p)
2530
2531 // 35: LOOKUP_READ_COUNTS_EVAL_LOC
2532 mstore(BATCH_SCALAR_36_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2533 batched_evaluation := addmod(
2534 batched_evaluation,
2535 mulmod(mload(LOOKUP_READ_COUNTS_EVAL_LOC), batching_challenge, p),
2536 p
2537 )
2538 batching_challenge := mulmod(batching_challenge, rho, p)
2539
2540 // 36: LOOKUP_READ_TAGS_EVAL_LOC
2541 mstore(BATCH_SCALAR_37_LOC, mulmod(neg_unshifted_scalar, batching_challenge, p))
2542 batched_evaluation := addmod(
2543 batched_evaluation,
2544 mulmod(mload(LOOKUP_READ_TAGS_EVAL_LOC), batching_challenge, p),
2545 p
2546 )
2547 batching_challenge := mulmod(batching_challenge, rho, p)
2548
2549 // Unrolled for NUMBER_OF_SHIFTED_ENTITIES = 5
2550 // for (uint256 i = NUMBER_UNSHIFTED + 1; i <= NUMBER_OF_ENTITIES; ++i) {
2551 // scalars[i] = mem.shiftedScalar.neg() * mem.batchingChallenge;
2552 // mem.batchedEvaluation = mem.batchedEvaluation + (proof.sumcheckEvaluations[i - 1] * mem.batchingChallenge);
2553 // mem.batchingChallenge = mem.batchingChallenge * tp.rho;
2554 // }
2555
2556 // Shifted entities: SHIFTED_COMMITMENTS_START = 30
2557 // scalars[scalarOff] += mem.shiftedScalar.neg() * mem.batchingChallenge
2558 // 30: W1 (shifted)
2559 mstore(
2560 BATCH_SCALAR_30_LOC,
2561 addmod(mload(BATCH_SCALAR_30_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2562 )
2563 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W1_SHIFT_EVAL_LOC), batching_challenge, p), p)
2564 batching_challenge := mulmod(batching_challenge, rho, p)
2565
2566 // 31: W2 (shifted)
2567 mstore(
2568 BATCH_SCALAR_31_LOC,
2569 addmod(mload(BATCH_SCALAR_31_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2570 )
2571 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W2_SHIFT_EVAL_LOC), batching_challenge, p), p)
2572 batching_challenge := mulmod(batching_challenge, rho, p)
2573
2574 // 32: W3 (shifted)
2575 mstore(
2576 BATCH_SCALAR_32_LOC,
2577 addmod(mload(BATCH_SCALAR_32_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2578 )
2579 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W3_SHIFT_EVAL_LOC), batching_challenge, p), p)
2580 batching_challenge := mulmod(batching_challenge, rho, p)
2581
2582 // 33: W4 (shifted)
2583 mstore(
2584 BATCH_SCALAR_33_LOC,
2585 addmod(mload(BATCH_SCALAR_33_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2586 )
2587 batched_evaluation := addmod(batched_evaluation, mulmod(mload(W4_SHIFT_EVAL_LOC), batching_challenge, p), p)
2588 batching_challenge := mulmod(batching_challenge, rho, p)
2589
2590 // 34: Z_PERM (shifted)
2591 mstore(
2592 BATCH_SCALAR_34_LOC,
2593 addmod(mload(BATCH_SCALAR_34_LOC), mulmod(neg_shifted_scalar, batching_challenge, p), p)
2594 )
2595 batched_evaluation := addmod(
2596 batched_evaluation,
2597 mulmod(mload(Z_PERM_SHIFT_EVAL_LOC), batching_challenge, p),
2598 p
2599 )
2600 batching_challenge := mulmod(batching_challenge, rho, p)
2601
2602 // Compute fold pos evaluations
2603 {
2604 mstore(CHALL_POW_LOC, POWERS_OF_EVALUATION_CHALLENGE_{{ LOG_N_MINUS_ONE }}_LOC)
2605 mstore(SUMCHECK_U_LOC, SUM_U_CHALLENGE_{{ LOG_N_MINUS_ONE }})
2606 mstore(GEMINI_A_LOC, GEMINI_A_EVAL_{{ LOG_N_MINUS_ONE }})
2607
2608 // Inversion of this value was included in batch inversion above
2609 let inverted_chall_pow_minus_u_loc := INVERTED_CHALLENGE_POW_MINUS_U_{{ LOG_N_MINUS_ONE }}_LOC
2610 let fold_pos_off := FOLD_POS_EVALUATIONS_{{ LOG_N_MINUS_ONE }}_LOC
2611
2612 let batchedEvalAcc := batched_evaluation
2613 for { let i := LOG_N } gt(i, 0) { i := sub(i, 1) } {
2614 let chall_pow := mload(mload(CHALL_POW_LOC))
2615 let sum_check_u := mload(mload(SUMCHECK_U_LOC))
2616
2617 // challengePower * batchedEvalAccumulator * 2
2618 let batchedEvalRoundAcc := mulmod(chall_pow, mulmod(batchedEvalAcc, 2, p), p)
2619 // (challengePower * (ONE - u) - u)
2620 let chall_pow_times_1_minus_u := mulmod(chall_pow, addmod(1, sub(p, sum_check_u), p), p)
2621
2622 batchedEvalRoundAcc := addmod(
2623 batchedEvalRoundAcc,
2624 sub(
2625 p,
2626 mulmod(
2627 mload(mload(GEMINI_A_LOC)),
2628 addmod(chall_pow_times_1_minus_u, sub(p, sum_check_u), p),
2629 p
2630 )
2631 ),
2632 p
2633 )
2634
2635 batchedEvalRoundAcc := mulmod(batchedEvalRoundAcc, mload(inverted_chall_pow_minus_u_loc), p)
2636
2637 batchedEvalAcc := batchedEvalRoundAcc
2638 mstore(fold_pos_off, batchedEvalRoundAcc)
2639
2640 mstore(CHALL_POW_LOC, sub(mload(CHALL_POW_LOC), 0x20))
2641 mstore(SUMCHECK_U_LOC, sub(mload(SUMCHECK_U_LOC), 0x20))
2642 mstore(GEMINI_A_LOC, sub(mload(GEMINI_A_LOC), 0x20))
2643 inverted_chall_pow_minus_u_loc := sub(inverted_chall_pow_minus_u_loc, 0x20)
2644 fold_pos_off := sub(fold_pos_off, 0x20)
2645 }
2646 }
2647
2648 let constant_term_acc := mulmod(mload(FOLD_POS_EVALUATIONS_0_LOC), mload(POS_INVERTED_DENOM_0_LOC), p)
2649 {
2650 let shplonk_nu := mload(SHPLONK_NU_CHALLENGE)
2651
2652 constant_term_acc := addmod(
2653 constant_term_acc,
2654 mulmod(mload(GEMINI_A_EVAL_0), mulmod(shplonk_nu, mload(NEG_INVERTED_DENOM_0_LOC), p), p),
2655 p
2656 )
2657
2658 let shplonk_nu_sqr := mulmod(shplonk_nu, shplonk_nu, p)
2659 batching_challenge := shplonk_nu_sqr
2660
2661 mstore(SS_POS_INV_DENOM_LOC, POS_INVERTED_DENOM_1_LOC)
2662 mstore(SS_NEG_INV_DENOM_LOC, NEG_INVERTED_DENOM_1_LOC)
2663
2664 mstore(SS_GEMINI_EVALS_LOC, GEMINI_A_EVAL_1)
2665 let fold_pos_evals_loc := FOLD_POS_EVALUATIONS_1_LOC
2666
2667 let scalars_loc := BATCH_SCALAR_38_LOC
2668
2669 for { let i := 0 } lt(i, sub(LOG_N, 1)) { i := add(i, 1) } {
2670 let scaling_factor_pos := mulmod(batching_challenge, mload(mload(SS_POS_INV_DENOM_LOC)), p)
2671 let scaling_factor_neg :=
2672 mulmod(batching_challenge, mulmod(shplonk_nu, mload(mload(SS_NEG_INV_DENOM_LOC)), p), p)
2673
2674 mstore(scalars_loc, addmod(sub(p, scaling_factor_neg), sub(p, scaling_factor_pos), p))
2675
2676 let accum_contribution := mulmod(scaling_factor_neg, mload(mload(SS_GEMINI_EVALS_LOC)), p)
2677 accum_contribution := addmod(
2678 accum_contribution,
2679 mulmod(scaling_factor_pos, mload(fold_pos_evals_loc), p),
2680 p
2681 )
2682
2683 constant_term_acc := addmod(constant_term_acc, accum_contribution, p)
2684
2685 batching_challenge := mulmod(batching_challenge, shplonk_nu_sqr, p)
2686
2687 mstore(SS_POS_INV_DENOM_LOC, add(mload(SS_POS_INV_DENOM_LOC), 0x20))
2688 mstore(SS_NEG_INV_DENOM_LOC, add(mload(SS_NEG_INV_DENOM_LOC), 0x20))
2689 mstore(SS_GEMINI_EVALS_LOC, add(mload(SS_GEMINI_EVALS_LOC), 0x20))
2690 fold_pos_evals_loc := add(fold_pos_evals_loc, 0x20)
2691 scalars_loc := add(scalars_loc, 0x20)
2692 }
2693 }
2694
2695 // Libra polynomial batching (ZK addition)
2696 // denominators[0] = 1/(shplonkZ - geminiR) = POS_INVERTED_DENOM_0 (already computed)
2697 // denominators[1] = 1/(shplonkZ - SUBGROUP_GENERATOR * geminiR) (new, compute inline)
2698 // denominators[2] = denominators[0]
2699 // denominators[3] = denominators[0]
2700 {
2701 let shplonk_nu := mload(SHPLONK_NU_CHALLENGE)
2702
2703 let libra_denom_0 := mload(POS_INVERTED_DENOM_0_LOC)
2704
2705 // 1/(shplonkZ - SUBGROUP_GENERATOR * geminiR)
2706 // Already batch-inverted in the shplemini batch inversion above
2707 let libra_denom_1 := mload(LIBRA_SUBGROUP_DENOM_LOC)
2708
2709 // i=0: denom[0], libraPolyEvals[0]
2710 let scaling_factor := mulmod(libra_denom_0, batching_challenge, p)
2711 let libra_scalar_0 := sub(p, scaling_factor)
2712 constant_term_acc := addmod(constant_term_acc, mulmod(scaling_factor, mload(LIBRA_POLY_EVAL_0_LOC), p), p)
2713 batching_challenge := mulmod(batching_challenge, shplonk_nu, p)
2714
2715 // i=1: denom[1], libraPolyEvals[1]
2716 scaling_factor := mulmod(libra_denom_1, batching_challenge, p)
2717 let libra_scalar_1 := sub(p, scaling_factor)
2718 constant_term_acc := addmod(constant_term_acc, mulmod(scaling_factor, mload(LIBRA_POLY_EVAL_1_LOC), p), p)
2719 batching_challenge := mulmod(batching_challenge, shplonk_nu, p)
2720
2721 // i=2: denom[0], libraPolyEvals[2]
2722 scaling_factor := mulmod(libra_denom_0, batching_challenge, p)
2723 let libra_scalar_2 := sub(p, scaling_factor)
2724 constant_term_acc := addmod(constant_term_acc, mulmod(scaling_factor, mload(LIBRA_POLY_EVAL_2_LOC), p), p)
2725 batching_challenge := mulmod(batching_challenge, shplonk_nu, p)
2726
2727 // i=3: denom[0], libraPolyEvals[3]
2728 scaling_factor := mulmod(libra_denom_0, batching_challenge, p)
2729 let libra_scalar_3 := sub(p, scaling_factor)
2730 constant_term_acc := addmod(constant_term_acc, mulmod(scaling_factor, mload(LIBRA_POLY_EVAL_3_LOC), p), p)
2731
2732 // Store commitment scalars:
2733 // scalars[52] = batchingScalars[0] (for libraCommitments[0] = libraConcat)
2734 mstore(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_0 }}_LOC, libra_scalar_0)
2735 // scalars[53] = batchingScalars[1] + batchingScalars[2] (for libraCommitments[1] = libraGrandProduct)
2736 mstore(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_1 }}_LOC, addmod(libra_scalar_1, libra_scalar_2, p))
2737 // scalars[54] = batchingScalars[3] (for libraCommitments[2] = libraQuotient)
2738 mstore(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_2 }}_LOC, libra_scalar_3)
2739 }
2740
2741 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
2742 /* ZK: checkEvalsConsistency */
2743 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
2744 // Validates Libra polynomial evaluations using small subgroup IPA
2745 {
2746 let gemini_r := mload(GEMINI_R_CHALLENGE)
2747
2748 // Step 1: Compute vanishingPolyEval = geminiR^SUBGROUP_SIZE - 1
2749 // SUBGROUP_SIZE = 256 = 2^8, so 8 squarings instead of modexp precompile
2750 let v := mulmod(gemini_r, gemini_r, p) // r^2
2751 v := mulmod(v, v, p) // r^4
2752 v := mulmod(v, v, p) // r^8
2753 v := mulmod(v, v, p) // r^16
2754 v := mulmod(v, v, p) // r^32
2755 v := mulmod(v, v, p) // r^64
2756 v := mulmod(v, v, p) // r^128
2757 v := mulmod(v, v, p) // r^256
2758 let vanishing_poly_eval := addmod(v, sub(p, 1), p)
2759
2760 // Require vanishingPolyEval != 0 (geminiR not in subgroup)
2761 if iszero(vanishing_poly_eval) {
2762 mstore(0x00, GEMINI_CHALLENGE_IN_SUBGROUP_SELECTOR)
2763 revert(0x00, 0x04)
2764 }
2765
2766 // Step 2: Build challengePolyLagrange[0..255]
2767 // Memory layout: CHALLENGE_POLY_LAGRANGE_BASE + idx * 0x20
2768 // Zero-initialize all 256 entries (only 1 + 9*LOG_N = 136 will be non-zero)
2769
2770 mstore(CHALLENGE_POLY_LAGRANGE_BASE_0, 1) // [0] = 1
2771
2772 {
2773 let u_loc := SUM_U_CHALLENGE_0
2774 let challenge_base := CHALLENGE_POLY_LAGRANGE_BASE_1
2775 // Upper bound of this loop is LIBRA_UNIVARIATES_LENGTH * LOG_N - this is inserted in code templating depending on LOG_N
2776 for { } lt(challenge_base, CHALLENGE_POLY_LAGRANGE_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}) { } {
2777 let u_round := mload(u_loc)
2778
2779 // [currIdx] = 1
2780 mstore(challenge_base, 1)
2781 challenge_base := add(challenge_base, 0x20)
2782
2783 // Calc memory offset inner loop should break at
2784 let loop_target := add(challenge_base, mul(0x20, LIBRA_UNIVARIATES_LENGTH_MINUS_ONE))
2785
2786 // [currIdx+1..currIdx+8] = u^1, u^2, ..., u^8
2787 let prev_val := 1
2788 for { } lt(challenge_base, loop_target) { } {
2789 prev_val := mulmod(prev_val, u_round, p)
2790 mstore(challenge_base, prev_val)
2791 challenge_base := add(challenge_base, 0x20)
2792 }
2793
2794 u_loc := add(u_loc, 0x20)
2795 }
2796 }
2797
2798 // Step 3: Compute the active challenge-poly denominators and L_|H|(r)'s denominator.
2799 {
2800 let challenge_poly_denom_end := add(CONSISTENCY_DENOMINATORS_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}, 0x20)
2801 let root_power := 1
2802 let consistency_base := CONSISTENCY_DENOMINATORS_BASE_0
2803 for { } lt(consistency_base, challenge_poly_denom_end) { } {
2804 let denom := addmod(mulmod(root_power, gemini_r, p), sub(p, 1), p)
2805 mstore(consistency_base, denom)
2806 root_power := mulmod(root_power, SUBGROUP_GENERATOR_INVERSE, p)
2807 consistency_base := add(consistency_base, 0x20)
2808 }
2809 mstore(
2810 challenge_poly_denom_end,
2811 addmod(mulmod(SUBGROUP_GENERATOR, gemini_r, p), sub(p, 1), p)
2812 )
2813 }
2814
2815 // Step 4: Batch invert the active denominators plus L_|H|(r)'s denominator.
2816 {
2817 let final_product_pointer := add(CONSISTENCY_PRODUCTS_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}, 0x20)
2818 let batch_product_end := add(final_product_pointer, 0x20)
2819
2820 // Forward pass: accumulate products
2821 let product_pointer := CONSISTENCY_PRODUCTS_BASE_0
2822 let next_product_pointer := CONSISTENCY_PRODUCTS_BASE_1
2823 let denom_pointer := CONSISTENCY_DENOMINATORS_BASE_1
2824 mstore(CONSISTENCY_PRODUCTS_BASE_0, mload(CONSISTENCY_DENOMINATORS_BASE_0))
2825 for { } lt(next_product_pointer, batch_product_end) { } {
2826 mstore(
2827 next_product_pointer,
2828 mulmod(
2829 mload(product_pointer),
2830 mload(denom_pointer),
2831 p
2832 )
2833 )
2834 product_pointer := next_product_pointer
2835 next_product_pointer := add(next_product_pointer, 0x20)
2836 denom_pointer := add(denom_pointer, 0x20)
2837 }
2838
2839 // Invert the final product
2840 let final_prod := mload(final_product_pointer)
2841 mstore(0x00, 0x20)
2842 mstore(0x20, 0x20)
2843 mstore(0x40, 0x20)
2844 mstore(0x60, final_prod)
2845 mstore(0x80, sub(p, 2))
2846 mstore(0xa0, p)
2847 if iszero(staticcall(gas(), 5, 0x00, 0xc0, 0x00, 0x20)) {
2848 mstore(0x00, CONSISTENCY_CHECK_FAILED_SELECTOR)
2849 revert(0x00, 0x04)
2850 }
2851 let accumulator := mload(0x00)
2852 if iszero(accumulator) {
2853 mstore(0x00, MODEXP_FAILED_SELECTOR)
2854 revert(0x00, 0x04)
2855 }
2856
2857 // Backward pass: compute individual inverses
2858 let products_pointer := CONSISTENCY_PRODUCTS_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}
2859 let denoms_pointer := add(CONSISTENCY_DENOMINATORS_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}, 0x20)
2860 for { } gt(denoms_pointer, CONSISTENCY_DENOMINATORS_BASE_0) { } {
2861 let val := mulmod(
2862 accumulator,
2863 mload(products_pointer),
2864 p
2865 )
2866 accumulator := mulmod(
2867 accumulator,
2868 mload(denoms_pointer),
2869 p
2870 )
2871 mstore(denoms_pointer, val)
2872
2873 products_pointer := sub(products_pointer, 0x20)
2874 denoms_pointer := sub(denoms_pointer, 0x20)
2875 }
2876 // idx=0: running_inv is the inverse of denom[0]
2877 mstore(CONSISTENCY_DENOMINATORS_BASE_0, accumulator)
2878 }
2879
2880 // Step 5: Compute challengePolyEval = sum(lagrange[i] * invDenom[i]) * numerator
2881 let challenge_poly_eval := 0
2882 let challenge_poly_lagrange_end := add(CHALLENGE_POLY_LAGRANGE_BASE_{{ NUMBER_OF_LAGRANGE_BASES }}, 0x20)
2883 let lagrange_pointer := CHALLENGE_POLY_LAGRANGE_BASE_0
2884 let denom_pointer := CONSISTENCY_DENOMINATORS_BASE_0
2885 for { } lt(lagrange_pointer, challenge_poly_lagrange_end) { } {
2886 challenge_poly_eval := addmod(
2887 challenge_poly_eval,
2888 mulmod(
2889 mload(lagrange_pointer),
2890 mload(denom_pointer),
2891 p
2892 ),
2893 p
2894 )
2895 lagrange_pointer := add(lagrange_pointer, 0x20)
2896 denom_pointer := add(denom_pointer, 0x20)
2897 }
2898
2899 // numerator = vanishingPolyEval / SUBGROUP_SIZE
2900 let numerator := mulmod(vanishing_poly_eval, INV_SUBGROUP_SIZE, p)
2901 challenge_poly_eval := mulmod(challenge_poly_eval, numerator, p)
2902
2903 let lagrange_first := mulmod(mload(CONSISTENCY_DENOMINATORS_BASE_0), numerator, p)
2904 let lagrange_last := mulmod(
2905 mload(CONSISTENCY_DENOMINATORS_BASE_{{ NUMBER_OF_LAGRANGE_BASES_PLUS_ONE }}),
2906 numerator,
2907 p
2908 )
2909
2910 // Step 6: Compute diff and verify == 0
2911 // diff = lagrangeFirst * libraPolyEvals[2]
2912 let diff := mulmod(lagrange_first, mload(LIBRA_POLY_EVAL_2_LOC), p)
2913
2914 // diff += (geminiR - SUBGROUP_GENERATOR_INVERSE) *
2915 // (libraPolyEvals[1] - libraPolyEvals[2] - libraPolyEvals[0] * challengePolyEval)
2916 {
2917 let inner := addmod(
2918 mload(LIBRA_POLY_EVAL_1_LOC),
2919 sub(
2920 p,
2921 addmod(
2922 mload(LIBRA_POLY_EVAL_2_LOC),
2923 mulmod(mload(LIBRA_POLY_EVAL_0_LOC), challenge_poly_eval, p),
2924 p
2925 )
2926 ),
2927 p
2928 )
2929 let factor := addmod(gemini_r, sub(p, SUBGROUP_GENERATOR_INVERSE), p)
2930 diff := addmod(diff, mulmod(factor, inner, p), p)
2931 }
2932
2933 // diff += lagrangeLast * (libraPolyEvals[2] - libraEval)
2934 diff := addmod(
2935 diff,
2936 mulmod(
2937 lagrange_last,
2938 addmod(mload(LIBRA_POLY_EVAL_2_LOC), sub(p, mload(LIBRA_EVALUATION_LOC)), p),
2939 p
2940 ),
2941 p
2942 )
2943
2944 // diff -= vanishingPolyEval * libraPolyEvals[3]
2945 diff := addmod(
2946 diff,
2947 sub(p, mulmod(vanishing_poly_eval, mload(LIBRA_POLY_EVAL_3_LOC), p)),
2948 p
2949 )
2950
2951 if diff {
2952 mstore(0x00, CONSISTENCY_CHECK_FAILED_SELECTOR)
2953 revert(0x00, 0x04)
2954 }
2955 }
2956
2957 let precomp_success_flag := 1
2958 let q := Q // EC group order
2959 {
2960 // The initial accumulator = 1 * shplonk_q
2961 mcopy(ACCUMULATOR, SHPLONK_Q_X_LOC, 0x40)
2962 }
2963
2964 // Accumulate geminiMaskingPoly (ZK commitment[1])
2965 {
2966 mcopy(G1_LOCATION, GEMINI_MASKING_POLY_X_LOC, 0x40)
2967 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_1_LOC))
2968 precomp_success_flag := and(
2969 precomp_success_flag,
2970 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
2971 )
2972 precomp_success_flag := and(
2973 precomp_success_flag,
2974 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
2975 )
2976 }
2977
2978 // Accumulate vk points
2979 loadVk()
2980 {
2981 // Accumulator = accumulator + scalar[2] * vk[0] (Q_M)
2982 mcopy(G1_LOCATION, Q_M_X_LOC, 0x40)
2983 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_2_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[2] * vk[1]
2994 mcopy(G1_LOCATION, Q_C_X_LOC, 0x40)
2995 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_3_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[3] * vk[2]
3006 mcopy(G1_LOCATION, Q_L_X_LOC, 0x40)
3007 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_4_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[4] * vk[3]
3018 mcopy(G1_LOCATION, Q_R_X_LOC, 0x40)
3019 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_5_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[5] * vk[4]
3030 mcopy(G1_LOCATION, Q_O_X_LOC, 0x40)
3031 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_6_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[6] * vk[5]
3042 mcopy(G1_LOCATION, Q_4_X_LOC, 0x40)
3043 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_7_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[7] * vk[6]
3054 mcopy(G1_LOCATION, Q_LOOKUP_X_LOC, 0x40)
3055 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_8_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 // Accumulator = accumulator + scalar[8] * vk[7]
3066 mcopy(G1_LOCATION, Q_ARITH_X_LOC, 0x40)
3067 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_9_LOC))
3068 precomp_success_flag := and(
3069 precomp_success_flag,
3070 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3071 )
3072 precomp_success_flag := and(
3073 precomp_success_flag,
3074 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3075 )
3076
3077 // Accumulator = accumulator + scalar[9] * vk[8]
3078 mcopy(G1_LOCATION, Q_DELTA_RANGE_X_LOC, 0x40)
3079 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_10_LOC))
3080 precomp_success_flag := and(
3081 precomp_success_flag,
3082 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3083 )
3084 precomp_success_flag := and(
3085 precomp_success_flag,
3086 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3087 )
3088
3089 // Accumulator = accumulator + scalar[10] * vk[9]
3090 mcopy(G1_LOCATION, Q_ELLIPTIC_X_LOC, 0x40)
3091 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_11_LOC))
3092 precomp_success_flag := and(
3093 precomp_success_flag,
3094 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3095 )
3096 precomp_success_flag := and(
3097 precomp_success_flag,
3098 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3099 )
3100
3101 // Accumulator = accumulator + scalar[11] * vk[10]
3102 mcopy(G1_LOCATION, Q_MEMORY_X_LOC, 0x40)
3103 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_12_LOC))
3104 precomp_success_flag := and(
3105 precomp_success_flag,
3106 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3107 )
3108 precomp_success_flag := and(
3109 precomp_success_flag,
3110 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3111 )
3112
3113 // Accumulator = accumulator + scalar[12] * vk[11]
3114 mcopy(G1_LOCATION, Q_NNF_X_LOC, 0x40)
3115 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_13_LOC))
3116 precomp_success_flag := and(
3117 precomp_success_flag,
3118 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3119 )
3120 precomp_success_flag := and(
3121 precomp_success_flag,
3122 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3123 )
3124
3125 // Accumulator = accumulator + scalar[13] * vk[12]
3126 mcopy(G1_LOCATION, Q_POSEIDON_2_EXTERNAL_X_LOC, 0x40)
3127 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_14_LOC))
3128 precomp_success_flag := and(
3129 precomp_success_flag,
3130 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3131 )
3132 precomp_success_flag := and(
3133 precomp_success_flag,
3134 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3135 )
3136
3137 // Accumulator = accumulator + scalar[14] * vk[13]
3138 mcopy(G1_LOCATION, Q_POSEIDON_2_INTERNAL_X_LOC, 0x40)
3139 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_15_LOC))
3140 precomp_success_flag := and(
3141 precomp_success_flag,
3142 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3143 )
3144 precomp_success_flag := and(
3145 precomp_success_flag,
3146 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3147 )
3148
3149 // Accumulator = accumulator + scalar[15] * vk[14]
3150 mcopy(G1_LOCATION, SIGMA_1_X_LOC, 0x40)
3151 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_16_LOC))
3152 precomp_success_flag := and(
3153 precomp_success_flag,
3154 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3155 )
3156 precomp_success_flag := and(
3157 precomp_success_flag,
3158 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3159 )
3160
3161 // Accumulator = accumulator + scalar[16] * vk[15]
3162 mcopy(G1_LOCATION, SIGMA_2_X_LOC, 0x40)
3163 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_17_LOC))
3164 precomp_success_flag := and(
3165 precomp_success_flag,
3166 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3167 )
3168 precomp_success_flag := and(
3169 precomp_success_flag,
3170 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3171 )
3172
3173 // Accumulator = accumulator + scalar[17] * vk[16]
3174 mcopy(G1_LOCATION, SIGMA_3_X_LOC, 0x40)
3175 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_18_LOC))
3176 precomp_success_flag := and(
3177 precomp_success_flag,
3178 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3179 )
3180 precomp_success_flag := and(
3181 precomp_success_flag,
3182 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3183 )
3184
3185 // Accumulator = accumulator + scalar[18] * vk[17]
3186 mcopy(G1_LOCATION, SIGMA_4_X_LOC, 0x40)
3187 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_19_LOC))
3188 precomp_success_flag := and(
3189 precomp_success_flag,
3190 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3191 )
3192 precomp_success_flag := and(
3193 precomp_success_flag,
3194 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3195 )
3196
3197 // Accumulator = accumulator + scalar[19] * vk[18]
3198 mcopy(G1_LOCATION, ID_1_X_LOC, 0x40)
3199 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_20_LOC))
3200 precomp_success_flag := and(
3201 precomp_success_flag,
3202 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3203 )
3204 precomp_success_flag := and(
3205 precomp_success_flag,
3206 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3207 )
3208
3209 // Accumulator = accumulator + scalar[20] * vk[19]
3210 mcopy(G1_LOCATION, ID_2_X_LOC, 0x40)
3211 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_21_LOC))
3212 precomp_success_flag := and(
3213 precomp_success_flag,
3214 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3215 )
3216 precomp_success_flag := and(
3217 precomp_success_flag,
3218 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3219 )
3220
3221 // Accumulator = accumulator + scalar[21] * vk[20]
3222 mcopy(G1_LOCATION, ID_3_X_LOC, 0x40)
3223 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_22_LOC))
3224 precomp_success_flag := and(
3225 precomp_success_flag,
3226 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3227 )
3228 precomp_success_flag := and(
3229 precomp_success_flag,
3230 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3231 )
3232
3233 // Accumulator = accumulator + scalar[22] * vk[21]
3234 mcopy(G1_LOCATION, ID_4_X_LOC, 0x40)
3235 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_23_LOC))
3236 precomp_success_flag := and(
3237 precomp_success_flag,
3238 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3239 )
3240 precomp_success_flag := and(
3241 precomp_success_flag,
3242 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3243 )
3244
3245 // Accumulator = accumulator + scalar[23] * vk[22]
3246 mcopy(G1_LOCATION, TABLE_1_X_LOC, 0x40)
3247 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_24_LOC))
3248 precomp_success_flag := and(
3249 precomp_success_flag,
3250 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3251 )
3252 precomp_success_flag := and(
3253 precomp_success_flag,
3254 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3255 )
3256
3257 // Accumulator = accumulator + scalar[24] * vk[23]
3258 mcopy(G1_LOCATION, TABLE_2_X_LOC, 0x40)
3259 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_25_LOC))
3260 precomp_success_flag := and(
3261 precomp_success_flag,
3262 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3263 )
3264 precomp_success_flag := and(
3265 precomp_success_flag,
3266 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3267 )
3268
3269 // Accumulator = accumulator + scalar[25] * vk[24]
3270 mcopy(G1_LOCATION, TABLE_3_X_LOC, 0x40)
3271 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_26_LOC))
3272 precomp_success_flag := and(
3273 precomp_success_flag,
3274 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3275 )
3276 precomp_success_flag := and(
3277 precomp_success_flag,
3278 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3279 )
3280
3281 // Accumulator = accumulator + scalar[26] * vk[25]
3282 mcopy(G1_LOCATION, TABLE_4_X_LOC, 0x40)
3283 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_27_LOC))
3284 precomp_success_flag := and(
3285 precomp_success_flag,
3286 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3287 )
3288 precomp_success_flag := and(
3289 precomp_success_flag,
3290 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3291 )
3292
3293 // Accumulator = accumulator + scalar[27] * vk[26]
3294 mcopy(G1_LOCATION, LAGRANGE_FIRST_X_LOC, 0x40)
3295 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_28_LOC))
3296 precomp_success_flag := and(
3297 precomp_success_flag,
3298 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3299 )
3300 precomp_success_flag := and(
3301 precomp_success_flag,
3302 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3303 )
3304
3305 // Accumulator = accumulator + constant_term_acc * G (generator)
3306 mstore(G1_LOCATION, 0x01) // G1 generator x
3307 mstore(G1_Y_LOCATION, 0x02) // G1 generator y
3308 mstore(SCALAR_LOCATION, constant_term_acc)
3309 precomp_success_flag := and(
3310 precomp_success_flag,
3311 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3312 )
3313 precomp_success_flag := and(
3314 precomp_success_flag,
3315 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3316 )
3317
3318 // Accumulator = accumulator + scalar[28] * vk[27]
3319 mcopy(G1_LOCATION, LAGRANGE_LAST_X_LOC, 0x40)
3320 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_29_LOC))
3321 precomp_success_flag := and(
3322 precomp_success_flag,
3323 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3324 )
3325 precomp_success_flag := and(
3326 precomp_success_flag,
3327 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3328 )
3329
3330 // Accumulate proof points
3331 // Accumulator = accumulator + scalar[29] * w_l
3332 mcopy(G1_LOCATION, W_L_X_LOC, 0x40)
3333 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_30_LOC))
3334 precomp_success_flag := and(
3335 precomp_success_flag,
3336 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3337 )
3338 precomp_success_flag := and(
3339 precomp_success_flag,
3340 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3341 )
3342
3343 // Accumulator = accumulator + scalar[30] * w_r
3344 mcopy(G1_LOCATION, W_R_X_LOC, 0x40)
3345 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_31_LOC))
3346 precomp_success_flag := and(
3347 precomp_success_flag,
3348 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3349 )
3350 precomp_success_flag := and(
3351 precomp_success_flag,
3352 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3353 )
3354
3355 // Accumulator = accumulator + scalar[31] * w_o
3356 mcopy(G1_LOCATION, W_O_X_LOC, 0x40)
3357 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_32_LOC))
3358 precomp_success_flag := and(
3359 precomp_success_flag,
3360 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3361 )
3362 precomp_success_flag := and(
3363 precomp_success_flag,
3364 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3365 )
3366
3367 // Accumulator = accumulator + scalar[32] * w_4
3368 mcopy(G1_LOCATION, W_4_X_LOC, 0x40)
3369 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_33_LOC))
3370 precomp_success_flag := and(
3371 precomp_success_flag,
3372 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3373 )
3374 precomp_success_flag := and(
3375 precomp_success_flag,
3376 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3377 )
3378
3379 // Accumulator = accumulator + scalar[33] * z_perm
3380 mcopy(G1_LOCATION, Z_PERM_X_LOC, 0x40)
3381 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_34_LOC))
3382 precomp_success_flag := and(
3383 precomp_success_flag,
3384 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3385 )
3386 precomp_success_flag := and(
3387 precomp_success_flag,
3388 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3389 )
3390
3391 // Accumulator = accumulator + scalar[34] * lookup_inverses
3392 mcopy(G1_LOCATION, LOOKUP_INVERSES_X_LOC, 0x40)
3393 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_35_LOC))
3394 precomp_success_flag := and(
3395 precomp_success_flag,
3396 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3397 )
3398 precomp_success_flag := and(
3399 precomp_success_flag,
3400 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3401 )
3402
3403 // Accumulator = accumulator + scalar[35] * lookup_read_counts
3404 mcopy(G1_LOCATION, LOOKUP_READ_COUNTS_X_LOC, 0x40)
3405 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_36_LOC))
3406 precomp_success_flag := and(
3407 precomp_success_flag,
3408 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3409 )
3410 precomp_success_flag := and(
3411 precomp_success_flag,
3412 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3413 )
3414
3415 // Accumulator = accumulator + scalar[36] * lookup_read_tags
3416 mcopy(G1_LOCATION, LOOKUP_READ_TAGS_X_LOC, 0x40)
3417 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_37_LOC))
3418 precomp_success_flag := and(
3419 precomp_success_flag,
3420 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3421 )
3422 precomp_success_flag := and(
3423 precomp_success_flag,
3424 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3425 )
3426
3427 // Accumulate these LOG_N scalars with the gemini fold univariates
3428 {
3429 {
3432 }
3433 }
3434
3435 // Accumulate libra commitments (ZK)
3436 {
3437 // scalar[52] * libraConcat (libraCommitments[0])
3438 mcopy(G1_LOCATION, LIBRA_CONCAT_X_LOC, 0x40)
3439 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_0 }}_LOC))
3440 precomp_success_flag := and(
3441 precomp_success_flag,
3442 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3443 )
3444 precomp_success_flag := and(
3445 precomp_success_flag,
3446 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3447 )
3448
3449 // scalar[53] * libraGrandProduct (libraCommitments[1])
3450 mcopy(G1_LOCATION, LIBRA_GRAND_PRODUCT_X_LOC, 0x40)
3451 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_1 }}_LOC))
3452 precomp_success_flag := and(
3453 precomp_success_flag,
3454 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3455 )
3456 precomp_success_flag := and(
3457 precomp_success_flag,
3458 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3459 )
3460
3461 // scalar[54] * libraQuotient (libraCommitments[2])
3462 mcopy(G1_LOCATION, LIBRA_QUOTIENT_X_LOC, 0x40)
3463 mstore(SCALAR_LOCATION, mload(BATCH_SCALAR_{{ LIBRA_BATCH_SCALAR_2 }}_LOC))
3464 precomp_success_flag := and(
3465 precomp_success_flag,
3466 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3467 )
3468 precomp_success_flag := and(
3469 precomp_success_flag,
3470 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3471 )
3472 }
3473
3474 {
3475 // Accumlate final quotient commitment into shplonk check
3476 // Accumulator = accumulator + shplonkZ * quotient commitment
3477 mcopy(G1_LOCATION, KZG_QUOTIENT_X_LOC, 0x40)
3478
3479 mstore(SCALAR_LOCATION, mload(SHPLONK_Z_CHALLENGE))
3480 precomp_success_flag := and(
3481 precomp_success_flag,
3482 staticcall(gas(), 7, G1_LOCATION, 0x60, ACCUMULATOR_2, 0x40)
3483 )
3484 precomp_success_flag := and(
3485 precomp_success_flag,
3486 staticcall(gas(), 6, ACCUMULATOR, 0x80, ACCUMULATOR, 0x40)
3487 )
3488 }
3489
3490 // All G1 points were validated on-curve during input validation.
3491 // precomp_success_flag now only tracks ecAdd/ecMul precompile success.
3492 if iszero(precomp_success_flag) {
3493 mstore(0x00, SHPLEMINI_FAILED_SELECTOR)
3494 revert(0x00, 0x04)
3495 }
3496
3497 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3498 /* SHPLEMINI - complete */
3499 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3500
3501 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3502 /* PAIRING CHECK */
3503 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3504 {
3505 // P_1
3506 mstore(0xc0, mload(KZG_QUOTIENT_X_LOC))
3507 mstore(0xe0, sub(q, mload(KZG_QUOTIENT_Y_LOC)))
3508
3509 // p_0_agg
3510 // 0x80 - p_0_agg x
3511 // 0xa0 - p_0_agg y
3512 mcopy(0x80, ACCUMULATOR, 0x40)
3513
3514 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3515 /* PAIRING AGGREGATION */
3516 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3517 // Read the pairing encoded in the first 8 field elements of the proof (2 limbs per coordinate)
3518 let p0_other_x := mload(PAIRING_POINT_0_X_0_LOC)
3519 p0_other_x := or(shl(136, mload(PAIRING_POINT_0_X_1_LOC)), p0_other_x)
3520
3521 let p0_other_y := mload(PAIRING_POINT_0_Y_0_LOC)
3522 p0_other_y := or(shl(136, mload(PAIRING_POINT_0_Y_1_LOC)), p0_other_y)
3523
3524 let p1_other_x := mload(PAIRING_POINT_1_X_0_LOC)
3525 p1_other_x := or(shl(136, mload(PAIRING_POINT_1_X_1_LOC)), p1_other_x)
3526
3527 let p1_other_y := mload(PAIRING_POINT_1_Y_0_LOC)
3528 p1_other_y := or(shl(136, mload(PAIRING_POINT_1_Y_1_LOC)), p1_other_y)
3529
3530 // Check if pairing points are default (all zero = infinity = no recursive verification)
3531 let pairing_points_are_default := iszero(or(or(p0_other_x, p0_other_y), or(p1_other_x, p1_other_y)))
3532
3533 let success := 1
3534 // Only aggregate if pairing points are non-default
3535 if iszero(pairing_points_are_default) {
3536 // Reconstructed coordinates must be < Q to prevent malleability
3537 if iszero(and(
3538 and(lt(p0_other_x, q), lt(p0_other_y, q)),
3539 and(lt(p1_other_x, q), lt(p1_other_y, q))
3540 )) {
3541 mstore(0x00, VALUE_GE_GROUP_ORDER_SELECTOR)
3542 revert(0x00, 0x04)
3543 }
3544
3545 // Validate p_0_other not point of infinity
3546 success := iszero(iszero(or(p0_other_x, p0_other_y)))
3547 // Validate p_1_other not point of infinity
3548 success := and(success, iszero(iszero(or(p1_other_x, p1_other_y))))
3549
3550 // p_0
3551 mstore(0x00, p0_other_x)
3552 mstore(0x20, p0_other_y)
3553
3554 // p_1
3555 mstore(0x40, p1_other_x)
3556 mstore(0x60, p1_other_y)
3557
3558 // p_1_agg is already in the correct location
3559
3560 let recursion_separator := keccak256(0x00, 0x100)
3561
3562 // Write separator back to scratch space
3563 mstore(0x00, p0_other_x)
3564
3565 mstore(0x40, recursion_separator)
3566 // recursion_separator * p_0_other
3567 success := and(success, staticcall(gas(), 0x07, 0x00, 0x60, 0x00, 0x40))
3568
3569 // (recursion_separator * p_0_other) + p_0_agg
3570 mcopy(0x40, 0x80, 0x40)
3571 // p_0 = (recursion_separator * p_0_other) + p_0_agg
3572 success := and(success, staticcall(gas(), 6, 0x00, 0x80, 0x00, 0x40))
3573
3574 mstore(0x40, p1_other_x)
3575 mstore(0x60, p1_other_y)
3576 mstore(0x80, recursion_separator)
3577
3578 success := and(success, staticcall(gas(), 7, 0x40, 0x60, 0x40, 0x40))
3579
3580 // Write p_1_agg back to scratch space
3581 mcopy(0x80, 0xc0, 0x40)
3582
3583 // 0xc0 - (recursion_separator * p_1_other) + p_1_agg
3584 success := and(success, staticcall(gas(), 6, 0x40, 0x80, 0xc0, 0x40))
3585 }
3586 // If default pairing points, use p_0_agg and p_1_agg directly (already at 0x80, 0xc0)
3587 if pairing_points_are_default {
3588 // Copy p_0_agg to 0x00 for pairing input
3589 mcopy(0x00, 0x80, 0x40)
3590 // p_1_agg stays at 0xc0
3591 }
3592
3593 // G2 [1]
3594 mstore(0x40, 0x198e9393920d483a7260bfb731fb5d25f1aa493335a9e71297e485b7aef312c2)
3595 mstore(0x60, 0x1800deef121f1e76426a00665e5c4479674322d4f75edadd46debd5cd992f6ed)
3596 mstore(0x80, 0x090689d0585ff075ec9e99ad690c3395bc4b313370b38ef355acdadcd122975b)
3597 mstore(0xa0, 0x12c85ea5db8c6deb4aab71808dcb408fe3d1e7690c43d37b4ce6cc0166fa7daa)
3598
3599 // G2 [x]
3600 mstore(0x100, 0x260e01b251f6f1c7e7ff4e580791dee8ea51d87a358e038b4efe30fac09383c1)
3601 mstore(0x120, 0x0118c4d5b837bcc2bc89b5b398b5974e9f5944073b32078b7e231fec938883b0)
3602 mstore(0x140, 0x04fc6369f7110fe3d25156c1bb9a72859cf2a04641f99ba4ee413c80da6a5fe4)
3603 mstore(0x160, 0x22febda3c0c0632a56475b4214e5615e11e6dd3f96e6cea2854a87d4dacc5e55)
3604
3605 let pairing_success := and(success, staticcall(gas(), 8, 0x00, 0x180, 0x00, 0x20))
3606 if iszero(and(pairing_success, mload(0x00))) {
3607 mstore(0x00, SHPLEMINI_FAILED_SELECTOR)
3608 revert(0x00, 0x04)
3609 }
3610
3611 /*´:°•.°+.*•´.*:˚.°*.˚•´.°:°•.°•.*•´.*:˚.°*.˚•´.°:°•.°+.*•´.*:*/
3612 /* PAIRING CHECK - Complete */
3613 /*.•°:°.´+˚.*°.˚:*.´•*.+°.•°:´*.´•*.•°.•°:°.´:•˚°.*°.˚:*.´+°.•*/
3614 }
3615 {
3616 mstore(0x00, 0x01)
3617 return(0x00, 0x20) // Proof succeeded!
3618 }
3619 }
3620 }
3621 }
3622}
3623)";
3624
3625inline std::string get_optimized_honk_zk_solidity_verifier(auto const& verification_key)
3626{
3627 std::string template_str = HONK_ZK_CONTRACT_OPT_SOURCE;
3628
3629 apply_template_params(template_str, verification_key, /*is_zk=*/true);
3630
3631 // Replace UNROLL_SECTION blocks
3632 int log_n = static_cast<int>(verification_key->log_circuit_size);
3633 UnrollConfig unroll_config{
3634 .batch_scalar_offset = 38,
3635 };
3636
3637 replace_unroll_section(template_str, "POWERS_OF_EVALUATION_COMPUTATION", log_n, unroll_config);
3638 replace_unroll_section(template_str, "ACCUMULATE_INVERSES", log_n, unroll_config);
3639 replace_unroll_section(template_str, "COLLECT_INVERSES", log_n, unroll_config);
3640 replace_unroll_section(template_str, "ACCUMULATE_GEMINI_FOLD_UNIVARIATE", log_n, unroll_config);
3641
3642 MemoryLayoutConfig mem_config{
3644 .barycentric_domain_size = 9,
3645 .is_zk = true,
3646 };
3647 replace_memory_layout(template_str, log_n, mem_config);
3648 // Replace Memory Layout
3649 {
3650 std::string::size_type start_pos = template_str.find("// {{ SECTION_START MEMORY_LAYOUT }}");
3651 std::string::size_type end_pos = template_str.find("// {{ SECTION_END MEMORY_LAYOUT }}");
3652 if (start_pos != std::string::npos && end_pos != std::string::npos) {
3653 std::string::size_type start_line_end = template_str.find("\n", start_pos);
3654 std::string generated_code = generate_memory_offsets(log_n, mem_config);
3655 template_str = template_str.substr(0, start_line_end + 1) + generated_code + template_str.substr(end_pos);
3656 }
3657 }
3658
3659 return template_str;
3660}
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)
std::string generate_memory_offsets(int log_n, const MemoryLayoutConfig &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_zk_solidity_verifier(auto const &verification_key)