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