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