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