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