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