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