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