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