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