gnark-plonky2-verifier/plonky2_verifier/fri.go
plonky2_verifier/fri.goRaw
1package plonky2_verifier
2
3import (
4 "fmt"
5 "gnark-ed25519/field"
6 . "gnark-ed25519/field"
7 "gnark-ed25519/poseidon"
8 "math"
9 "math/big"
10 "math/bits"
11
12 "github.com/consensys/gnark-crypto/field/goldilocks"
13 "github.com/consensys/gnark/frontend"
14)
15
16type FriChip struct {
17 api frontend.API
18 fieldAPI frontend.API
19 qeAPI *QuadraticExtensionAPI
20 hashAPI *HashAPI
21
22 poseidonChip *poseidon.PoseidonChip
23
24 friParams *FriParams
25 verifierOnlyCircuitData *VerifierOnlyCircuitData
26}
27
28func NewFriChip(
29 api frontend.API,
30 fieldAPI frontend.API,
31 qeAPI *QuadraticExtensionAPI,
32 hashAPI *HashAPI,
33 poseidonChip *poseidon.PoseidonChip,
34 friParams *FriParams,
35) *FriChip {
36 return &FriChip{
37 api: api,
38 fieldAPI: fieldAPI,
39 qeAPI: qeAPI,
40 hashAPI: hashAPI,
41 poseidonChip: poseidonChip,
42 friParams: friParams,
43 }
44}
45
46func (f *FriChip) assertLeadingZeros(powWitness F, friConfig FriConfig) {
47 // Asserts that powWitness'es big-endian bit representation has at least `leading_zeros` leading zeros.
48 // Note that this is assuming that the Goldilocks field is being used. Specfically that the
49 // field is 64 bits long
50 maxPowWitness := uint64(math.Pow(2, float64(64-friConfig.ProofOfWorkBits))) - 1
51 f.fieldAPI.AssertIsLessOrEqual(powWitness, field.NewFieldElement(maxPowWitness))
52}
53
54func (f *FriChip) fromOpeningsAndAlpha(openings *FriOpenings, alpha QuadraticExtension) []QuadraticExtension {
55 // One reduced opening for all openings evaluated at point Zeta.
56 // Another one for all openings evaluated at point Zeta * Omega (which is only PlonkZsNext polynomial)
57
58 reducedOpenings := make([]QuadraticExtension, 0, 2)
59 for _, batch := range openings.Batches {
60 reducedOpenings = append(reducedOpenings, f.qeAPI.ReduceWithPowers(batch.Values, alpha))
61 }
62
63 return reducedOpenings
64}
65
66func (f *FriChip) hashOrNoop(data []F) Hash {
67 var elements Hash
68 if len(data) <= 4 {
69 // Pad the data to have a size of 4
70 for i, inputElement := range data {
71 elements[i] = inputElement
72 }
73 for i := len(data); i < 4; i++ {
74 elements[i] = field.ZERO_F
75 }
76
77 return elements
78 } else {
79 hashOutput := f.poseidonChip.HashNToMNoPad(data, 4)
80
81 if len(hashOutput) != len(elements) {
82 panic("The length of hashOutput and elements is different")
83 }
84
85 for i, hashField := range hashOutput {
86 elements[i] = hashField
87 }
88
89 return elements
90 }
91}
92
93func (f *FriChip) verifyMerkleProofToCapWithCapIndex(leafData []F, leafIndexBits []frontend.Variable, capIndexBits []frontend.Variable, merkleCap MerkleCap, proof *MerkleProof) {
94 currentDigest := f.hashOrNoop(leafData)
95 fourZeros := [4]F{field.ZERO_F, field.ZERO_F, field.ZERO_F, field.ZERO_F}
96 for i, sibling := range proof.Siblings {
97 bit := leafIndexBits[i]
98
99 var leftSiblingState poseidon.PoseidonState
100 copy(leftSiblingState[0:4], sibling[0:4])
101 copy(leftSiblingState[4:8], currentDigest[0:4])
102 copy(leftSiblingState[8:12], fourZeros[0:4])
103
104 leftHash := f.poseidonChip.Poseidon(leftSiblingState)
105
106 var leftHashCompress Hash
107 leftHashCompress[0] = leftHash[0]
108 leftHashCompress[1] = leftHash[1]
109 leftHashCompress[2] = leftHash[2]
110 leftHashCompress[3] = leftHash[3]
111
112 var rightSiblingState poseidon.PoseidonState
113 copy(rightSiblingState[0:4], currentDigest[0:4])
114 copy(rightSiblingState[4:8], sibling[0:4])
115 copy(rightSiblingState[8:12], fourZeros[0:4])
116
117 rightHash := f.poseidonChip.Poseidon(rightSiblingState)
118
119 var rightHashCompress Hash
120 rightHashCompress[0] = rightHash[0]
121 rightHashCompress[1] = rightHash[1]
122 rightHashCompress[2] = rightHash[2]
123 rightHashCompress[3] = rightHash[3]
124
125 currentDigest = f.hashAPI.SelectHash(bit, leftHashCompress, rightHashCompress)
126 }
127
128 // We assume that the cap_height is 4. Create two levels of the Lookup2 circuit
129 if len(capIndexBits) != 4 || len(merkleCap) != 16 {
130 errorMsg, _ := fmt.Printf(
131 "capIndexBits length should be 4 and the merkleCap length should be 16. Actual values (capIndexBits: %d, merkleCap: %d)\n",
132 len(capIndexBits),
133 len(merkleCap),
134 )
135 panic(errorMsg)
136 }
137
138 const NUM_LEAF_LOOKUPS = 4
139 var leafLookups [NUM_LEAF_LOOKUPS]Hash
140 // First create the "leaf" lookup2 circuits
141 // The will use the least significant bits of the capIndexBits array
142 for i := 0; i < NUM_LEAF_LOOKUPS; i++ {
143 leafLookups[i] = f.hashAPI.Lookup2Hash(
144 capIndexBits[0], capIndexBits[1],
145 merkleCap[i*NUM_LEAF_LOOKUPS], merkleCap[i*NUM_LEAF_LOOKUPS+1], merkleCap[i*NUM_LEAF_LOOKUPS+2], merkleCap[i*NUM_LEAF_LOOKUPS+3],
146 )
147 }
148
149 // Use the most 2 significant bits of the capIndexBits array for the "root" lookup
150 merkleCapEntry := f.hashAPI.Lookup2Hash(capIndexBits[2], capIndexBits[3], leafLookups[0], leafLookups[1], leafLookups[2], leafLookups[3])
151 f.hashAPI.AssertIsEqualHash(currentDigest, merkleCapEntry)
152}
153
154func (f *FriChip) verifyInitialProof(xIndexBits []frontend.Variable, proof *FriInitialTreeProof, initialMerkleCaps []MerkleCap, capIndexBits []frontend.Variable) {
155 if len(proof.EvalsProofs) != len(initialMerkleCaps) {
156 panic("length of eval proofs in fri proof should equal length of initial merkle caps")
157 }
158
159 for i := 0; i < len(initialMerkleCaps); i++ {
160 evals := proof.EvalsProofs[i].Elements
161 merkleProof := proof.EvalsProofs[i].MerkleProof
162 cap := initialMerkleCaps[i]
163 f.verifyMerkleProofToCapWithCapIndex(evals, xIndexBits, capIndexBits, cap, &merkleProof)
164 }
165}
166
167// / We decompose FRI query indices into bits without verifying that the decomposition given by
168// / the prover is the canonical one. In particular, if `x_index < 2^field_bits - p`, then the
169// / prover could supply the binary encoding of either `x_index` or `x_index + p`, since they are
170// / congruent mod `p`. However, this only occurs with probability
171// / p_ambiguous = (2^field_bits - p) / p
172// / which is small for the field that we use in practice.
173// /
174// / In particular, the soundness error of one FRI query is roughly the codeword rate, which
175// / is much larger than this ambiguous-element probability given any reasonable parameters.
176// / Thus ambiguous elements contribute a negligible amount to soundness error.
177// /
178// / Here we compare the probabilities as a sanity check, to verify the claim above.
179func (f *FriChip) assertNoncanonicalIndicesOK() {
180 numAmbiguousElems := uint64(math.MaxUint64) - goldilocks.Modulus().Uint64() + 1
181 queryError := f.friParams.Config.rate()
182 pAmbiguous := float64(numAmbiguousElems) / float64(goldilocks.Modulus().Uint64())
183
184 // TODO: Check that pAmbiguous value is the same as the one in plonky2 verifier
185 if pAmbiguous >= queryError*1e-5 {
186 panic("A non-negligible portion of field elements are in the range that permits non-canonical encodings. Need to do more analysis or enforce canonical encodings.")
187 }
188}
189
190func (f *FriChip) expFromBitsConstBase(
191 base goldilocks.Element,
192 exponentBits []frontend.Variable,
193) F {
194 product := ONE_F
195 for i, bit := range exponentBits {
196 pow := int64(1 << i)
197 // If the bit is on, we multiply product by base^pow.
198 // We can arithmetize this as:
199 // product *= 1 + bit (base^pow - 1)
200 // product = (base^pow - 1) product bit + product
201 basePow := goldilocks.NewElement(0)
202 basePow.Exp(base, big.NewInt(pow))
203
204 basePowElement := NewFieldElement(basePow.Uint64() - 1)
205
206 product = f.fieldAPI.Add(
207 f.fieldAPI.Mul(
208 basePowElement,
209 product,
210 bit,
211 ),
212 product,
213 ).(F)
214 }
215
216 return product
217}
218
219func (f *FriChip) calculateSubgroupX(
220 xIndexBits []frontend.Variable,
221 nLog uint64,
222) F {
223 // Compute x from its index
224 // `subgroup_x` is `subgroup[x_index]`, i.e., the actual field element in the domain.
225 // TODO - Make these as global values
226 g := field.NewFieldElement(field.GOLDILOCKS_MULTIPLICATIVE_GROUP_GENERATOR.Uint64())
227 base := field.GoldilocksPrimitiveRootOfUnity(nLog)
228
229 // Create a reverse list of xIndexBits
230 xIndexBitsRev := make([]frontend.Variable, 0)
231 for i := len(xIndexBits) - 1; i >= 0; i-- {
232 xIndexBitsRev = append(xIndexBitsRev, xIndexBits[i])
233 }
234
235 product := f.expFromBitsConstBase(base, xIndexBitsRev)
236
237 return f.fieldAPI.Mul(g, product).(F)
238}
239
240func (f *FriChip) friCombineInitial(
241 instance FriInstanceInfo,
242 proof FriInitialTreeProof,
243 friAlpha QuadraticExtension,
244 subgroupX_QE QuadraticExtension,
245 precomputedReducedEval []QuadraticExtension,
246) QuadraticExtension {
247 sum := f.qeAPI.ZERO_QE
248
249 if len(instance.Batches) != len(precomputedReducedEval) {
250 panic("len(openings) != len(precomputedReducedEval)")
251 }
252
253 for i := 0; i < len(instance.Batches); i++ {
254 batch := instance.Batches[i]
255 reducedOpenings := precomputedReducedEval[i]
256
257 point := batch.Point
258 evals := make([]QuadraticExtension, 0)
259 for _, polynomial := range batch.Polynomials {
260 evals = append(
261 evals,
262 QuadraticExtension{proof.EvalsProofs[polynomial.OracleIndex].Elements[polynomial.PolynomialInfo], field.ZERO_F},
263 )
264 }
265
266 reducedEvals := f.qeAPI.ReduceWithPowers(evals, friAlpha)
267 numerator := f.qeAPI.SubExtension(reducedEvals, reducedOpenings)
268 denominator := f.qeAPI.SubExtension(subgroupX_QE, point)
269 sum = f.qeAPI.MulExtension(f.qeAPI.ExpU64Extension(friAlpha, uint64(len(evals))), sum)
270 sum = f.qeAPI.AddExtension(
271 f.qeAPI.DivExtension(
272 numerator,
273 denominator,
274 ),
275 sum,
276 )
277 }
278
279 return f.qeAPI.MulExtension(sum, subgroupX_QE)
280}
281
282func (f *FriChip) finalPolyEval(finalPoly PolynomialCoeffs, point QuadraticExtension) QuadraticExtension {
283 ret := f.qeAPI.ZERO_QE
284 for i := len(finalPoly.Coeffs) - 1; i >= 0; i-- {
285 ret = f.qeAPI.AddExtension(
286 f.qeAPI.MulExtension(
287 ret,
288 point,
289 ),
290 finalPoly.Coeffs[i],
291 )
292 }
293 return ret
294}
295
296func (f *FriChip) interpolate(x QuadraticExtension, xPoints []QuadraticExtension, yPoints []QuadraticExtension, barycentricWeights []QuadraticExtension) QuadraticExtension {
297 if len(xPoints) != len(yPoints) || len(xPoints) != len(barycentricWeights) {
298 panic("length of xPoints, yPoints, and barycentricWeights are inconsistent")
299 }
300
301 lX := f.qeAPI.ONE_QE
302 for i := 0; i < len(xPoints); i++ {
303 lX = f.qeAPI.MulExtension(
304 lX,
305 f.qeAPI.SubExtension(
306 x,
307 xPoints[i],
308 ),
309 )
310 }
311
312 sum := f.qeAPI.ZERO_QE
313 for i := 0; i < len(xPoints); i++ {
314 sum = f.qeAPI.AddExtension(
315 f.qeAPI.MulExtension(
316 f.qeAPI.DivExtension(
317 barycentricWeights[i],
318 f.qeAPI.SubExtension(
319 x,
320 xPoints[i],
321 ),
322 ),
323 yPoints[i],
324 ),
325 sum,
326 )
327 }
328
329 interpolation := f.qeAPI.MulExtension(lX, sum)
330
331 returnField := interpolation
332 // Now check if x is already within the xPoints
333 for i := 0; i < len(xPoints); i++ {
334 returnField = f.qeAPI.Select(
335 f.qeAPI.IsZero(f.qeAPI.SubExtension(x, xPoints[i])),
336 yPoints[i],
337 returnField,
338 )
339 }
340
341 return returnField
342}
343
344func (f *FriChip) computeEvaluation(
345 x F,
346 xIndexWithinCosetBits []frontend.Variable,
347 arityBits uint64,
348 evals []QuadraticExtension,
349 beta QuadraticExtension,
350) QuadraticExtension {
351 arity := 1 << arityBits
352 if (len(evals)) != arity {
353 panic("len(evals) ! arity")
354 }
355 if arityBits > 8 {
356 panic("currently assuming that arityBits is <= 8")
357 }
358
359 g := field.GoldilocksPrimitiveRootOfUnity(arityBits)
360 gInv := goldilocks.NewElement(0)
361 gInv.Exp(g, big.NewInt(int64(arity-1)))
362
363 // The evaluation vector needs to be reordered first. Permute the evals array such that each
364 // element's new index is the bit reverse of it's original index.
365 // TODO: Optimization - Since the size of the evals array should be constant (e.g. 2^arityBits),
366 // we can just hard code the permutation.
367 permutedEvals := make([]QuadraticExtension, len(evals))
368 for i := uint8(0); i < uint8(len(evals)); i++ {
369 newIndex := bits.Reverse8(i) >> arityBits
370 permutedEvals[newIndex] = evals[i]
371 }
372
373 // Want `g^(arity - rev_x_index_within_coset)` as in the out-of-circuit version. Compute it
374 // as `(g^-1)^rev_x_index_within_coset`.
375 revXIndexWithinCosetBits := make([]frontend.Variable, len(xIndexWithinCosetBits))
376 for i := 0; i < len(xIndexWithinCosetBits); i++ {
377 revXIndexWithinCosetBits[len(xIndexWithinCosetBits)-1-i] = xIndexWithinCosetBits[i]
378 }
379 start := f.expFromBitsConstBase(gInv, revXIndexWithinCosetBits)
380 cosetStart := f.fieldAPI.Mul(start, x).(F)
381
382 xPoints := make([]QuadraticExtension, len(evals))
383 yPoints := permutedEvals
384
385 // TODO: Make g_F a constant
386 g_F := f.qeAPI.FieldToQE(NewFieldElement(g.Uint64()))
387 xPoints[0] = f.qeAPI.FieldToQE(cosetStart)
388 for i := 1; i < len(evals); i++ {
389 xPoints[i] = f.qeAPI.MulExtension(xPoints[i-1], g_F)
390 }
391
392 // TODO: This is n^2. Is there a way to do this better?
393 // Compute the barycentric weights
394 barycentricWeights := make([]QuadraticExtension, len(xPoints))
395 for i := 0; i < len(xPoints); i++ {
396 barycentricWeights[i] = f.qeAPI.ONE_QE
397 for j := 0; j < len(xPoints); j++ {
398 if i != j {
399 barycentricWeights[i] = f.qeAPI.MulExtension(
400 f.qeAPI.SubExtension(xPoints[i], xPoints[j]),
401 barycentricWeights[i],
402 )
403 }
404 }
405 // Take the inverse of the barycentric weights
406 // TODO: Can provide a witness to this value
407 barycentricWeights[i] = f.qeAPI.InverseExtension(barycentricWeights[i])
408 }
409
410 return f.interpolate(beta, xPoints, yPoints, barycentricWeights)
411}
412
413func (f *FriChip) verifyQueryRound(
414 instance FriInstanceInfo,
415 challenges *FriChallenges,
416 precomputedReducedEval []QuadraticExtension,
417 initialMerkleCaps []MerkleCap,
418 proof *FriProof,
419 xIndex F,
420 n uint64,
421 nLog uint64,
422 roundProof *FriQueryRound,
423) {
424 f.assertNoncanonicalIndicesOK()
425 xIndexBits := f.fieldAPI.ToBinary(xIndex, int(nLog))
426 capIndexBits := xIndexBits[len(xIndexBits)-int(f.friParams.Config.CapHeight):]
427
428 f.verifyInitialProof(xIndexBits, &roundProof.InitialTreesProof, initialMerkleCaps, capIndexBits)
429
430 subgroupX := f.calculateSubgroupX(
431 xIndexBits,
432 nLog,
433 )
434
435 subgroupX_QE := QuadraticExtension{subgroupX, field.ZERO_F}
436
437 oldEval := f.friCombineInitial(
438 instance,
439 roundProof.InitialTreesProof,
440 challenges.FriAlpha,
441 subgroupX_QE,
442 precomputedReducedEval,
443 )
444
445 for i, arityBits := range f.friParams.ReductionArityBits {
446 evals := roundProof.Steps[i].Evals
447
448 cosetIndexBits := xIndexBits[arityBits:]
449 xIndexWithinCosetBits := xIndexBits[:arityBits]
450
451 // Assumes that the arity bits will be 4. That means that the range of
452 // xIndexWithCoset is [0,2^4-1]. This is based on plonky2's circuit recursive
453 // config: https://github.com/mir-protocol/plonky2/blob/main/plonky2/src/plonk/circuit_data.rs#L63
454 // Will use a two levels tree of 4-selector gadgets.
455 if arityBits != 4 {
456 panic("assuming arity bits is 4")
457 }
458
459 const NUM_LEAF_LOOKUPS = 4
460 var leafLookups [NUM_LEAF_LOOKUPS]QuadraticExtension
461 // First create the "leaf" lookup2 circuits
462 // The will use the least significant bits of the xIndexWithCosetBits array
463 for i := 0; i < NUM_LEAF_LOOKUPS; i++ {
464 leafLookups[i] = f.qeAPI.Lookup2(
465 xIndexWithinCosetBits[0],
466 xIndexWithinCosetBits[1],
467 evals[i*NUM_LEAF_LOOKUPS],
468 evals[i*NUM_LEAF_LOOKUPS+1],
469 evals[i*NUM_LEAF_LOOKUPS+2],
470 evals[i*NUM_LEAF_LOOKUPS+3],
471 )
472 }
473
474 // Use the most 2 significant bits of the xIndexWithCosetBits array for the "root" lookup
475 newEval := f.qeAPI.Lookup2(
476 xIndexWithinCosetBits[2],
477 xIndexWithinCosetBits[3],
478 leafLookups[0],
479 leafLookups[1],
480 leafLookups[2],
481 leafLookups[3],
482 )
483
484 f.qeAPI.AssertIsEqual(newEval, oldEval)
485
486 oldEval = f.computeEvaluation(
487 subgroupX,
488 xIndexWithinCosetBits,
489 arityBits,
490 evals,
491 challenges.FriBetas[i],
492 )
493
494 // Convert evals (array of QE) to fields by taking their 0th degree coefficients
495 fieldEvals := make([]F, 0, 2*len(evals))
496 for j := 0; j < len(evals); j++ {
497 fieldEvals = append(fieldEvals, evals[j][0])
498 fieldEvals = append(fieldEvals, evals[j][1])
499 }
500 f.verifyMerkleProofToCapWithCapIndex(
501 fieldEvals,
502 cosetIndexBits,
503 capIndexBits,
504 proof.CommitPhaseMerkleCaps[i],
505 &roundProof.Steps[i].MerkleProof,
506 )
507
508 // Update the point x to x^arity.
509 for j := uint64(0); j < arityBits; j++ {
510 subgroupX = f.fieldAPI.Mul(subgroupX, subgroupX).(F)
511 }
512
513 xIndexBits = cosetIndexBits
514 }
515
516 subgroupX_QE = f.qeAPI.FieldToQE(subgroupX)
517 finalPolyEval := f.finalPolyEval(proof.FinalPoly, subgroupX_QE)
518
519 f.qeAPI.AssertIsEqual(oldEval, finalPolyEval)
520}
521
522func (f *FriChip) VerifyFriProof(
523 instance FriInstanceInfo,
524 openings FriOpenings,
525 friChallenges *FriChallenges,
526 initialMerkleCaps []MerkleCap,
527 friProof *FriProof,
528) {
529 // TODO: Check fri config
530 /* if let Some(max_arity_bits) = params.max_arity_bits() {
531 self.check_recursion_config::<C>(max_arity_bits);
532 }
533
534 debug_assert_eq!(
535 params.final_poly_len(),
536 proof.final_poly.len(),
537 "Final polynomial has wrong degree."
538 ); */
539
540 // Check POW
541 f.assertLeadingZeros(friChallenges.FriPowResponse, f.friParams.Config)
542
543 precomputedReducedEvals := f.fromOpeningsAndAlpha(&openings, friChallenges.FriAlpha)
544
545 // Size of the LDE domain.
546 nLog := f.friParams.DegreeBits + f.friParams.Config.RateBits
547 n := uint64(math.Pow(2, float64(nLog)))
548
549 if len(friChallenges.FriQueryIndicies) != len(friProof.QueryRoundProofs) {
550 panic(fmt.Sprintf(
551 "Number of query indices (%d) should equal number of query round proofs (%d)",
552 len(friChallenges.FriQueryIndicies),
553 len(friProof.QueryRoundProofs),
554 ))
555 }
556
557 for idx, xIndex := range friChallenges.FriQueryIndicies {
558 roundProof := friProof.QueryRoundProofs[idx]
559
560 f.verifyQueryRound(
561 instance,
562 friChallenges,
563 precomputedReducedEvals,
564 initialMerkleCaps,
565 friProof,
566 xIndex,
567 n,
568 nLog,
569 &roundProof,
570 )
571 }
572}