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