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
 11	"github.com/consensys/gnark-crypto/field/goldilocks"
 12	"github.com/consensys/gnark/frontend"
 13)
 14
 15type FriChip struct {
 16	api      frontend.API
 17	fieldAPI frontend.API
 18	qeAPI    *QuadraticExtensionAPI
 19
 20	poseidonChip *poseidon.PoseidonChip
 21
 22	friParams               *FriParams
 23	verifierOnlyCircuitData *VerifierOnlyCircuitData
 24}
 25
 26func NewFriChip(api frontend.API, fieldAPI frontend.API, qeAPI *QuadraticExtensionAPI, poseidonChip *poseidon.PoseidonChip, friParams *FriParams) *FriChip {
 27	return &FriChip{
 28		api:          api,
 29		fieldAPI:     fieldAPI,
 30		qeAPI:        qeAPI,
 31		poseidonChip: poseidonChip,
 32		friParams:    friParams,
 33	}
 34}
 35
 36func (f *FriChip) assertLeadingZeros(powWitness F, friConfig FriConfig) {
 37	// Asserts that powWitness'es big-endian bit representation has at least `leading_zeros` leading zeros.
 38	// Note that this is assuming that the Goldilocks field is being used.  Specfically that the
 39	// field is 64 bits long
 40	maxPowWitness := uint64(math.Pow(2, float64(64-friConfig.ProofOfWorkBits))) - 1
 41	f.fieldAPI.AssertIsLessOrEqual(powWitness, field.NewFieldElement(maxPowWitness))
 42}
 43
 44func (f *FriChip) fromOpeningsAndAlpha(openings *FriOpenings, alpha QuadraticExtension) []QuadraticExtension {
 45	// One reduced opening for all openings evaluated at point Zeta.
 46	// Another one for all openings evaluated at point Zeta * Omega (which is only PlonkZsNext polynomial)
 47
 48	reducedOpenings := make([]QuadraticExtension, 0, 2)
 49	for _, batch := range openings.Batches {
 50		reducedOpenings = append(reducedOpenings, reduceWithPowers(f.qeAPI, batch.values, alpha))
 51	}
 52
 53	return reducedOpenings
 54}
 55
 56func (f *FriChip) hashOrNoop(data []F) Hash {
 57	var elements Hash
 58	if len(data) <= 4 {
 59		// Pad the data to have a size of 4
 60		for i, inputElement := range data {
 61			elements[i] = inputElement
 62		}
 63		for i := len(data); i < 4; i++ {
 64			elements[i] = field.ZERO_F
 65		}
 66
 67		return elements
 68	} else {
 69		hashOutput := f.poseidonChip.HashNToMNoPad(data, 4)
 70
 71		if len(hashOutput) != len(elements) {
 72			panic("The length of hashOutput and elements is different")
 73		}
 74
 75		for i, hashField := range hashOutput {
 76			elements[i] = hashField
 77		}
 78
 79		return elements
 80	}
 81}
 82
 83func (f *FriChip) verifyMerkleProofToCapWithCapIndex(leafData []F, leafIndexBits []frontend.Variable, capIndexBits []frontend.Variable, merkleCap MerkleCap, proof *MerkleProof) {
 84	currentDigest := f.hashOrNoop(leafData)
 85	fourZeros := [4]F{field.ZERO_F, field.ZERO_F, field.ZERO_F, field.ZERO_F}
 86	for i, sibling := range proof.Siblings {
 87		bit := leafIndexBits[i]
 88
 89		var leftSiblingState poseidon.PoseidonState
 90		copy(leftSiblingState[0:4], sibling[0:4])
 91		copy(leftSiblingState[4:8], currentDigest[0:4])
 92		copy(leftSiblingState[8:12], fourZeros[0:4])
 93
 94		leftHash := f.poseidonChip.Poseidon(leftSiblingState)
 95		var leftHashCompress Hash
 96		leftHashCompress[0] = leftHash[0]
 97		leftHashCompress[1] = leftHash[1]
 98		leftHashCompress[2] = leftHash[2]
 99		leftHashCompress[3] = leftHash[3]
100
101		var rightSiblingState poseidon.PoseidonState
102		copy(rightSiblingState[0:4], currentDigest[0:4])
103		copy(rightSiblingState[4:8], sibling[0:4])
104		copy(rightSiblingState[8:12], fourZeros[0:4])
105
106		rightHash := f.poseidonChip.Poseidon(rightSiblingState)
107		var rightHashCompress Hash
108		rightHashCompress[0] = rightHash[0]
109		rightHashCompress[1] = rightHash[1]
110		rightHashCompress[2] = rightHash[2]
111		rightHashCompress[3] = rightHash[3]
112
113		currentDigest = SelectHash(f.fieldAPI, bit, leftHashCompress, rightHashCompress)
114	}
115
116	// We assume that the cap_height is 4.  Create two levels of the Lookup2 circuit
117	if len(capIndexBits) != 4 || len(merkleCap) != 16 {
118		panic("capIndexBits length should be 4 and the merkleCap length should be 16")
119	}
120
121	const NUM_LEAF_LOOKUPS = 4
122	var leafLookups [NUM_LEAF_LOOKUPS]Hash
123	// First create the "leaf" lookup2 circuits
124	// The will use the least significant bits of the capIndexBits array
125	for i := 0; i < NUM_LEAF_LOOKUPS; i++ {
126		leafLookups[i] = Lookup2Hash(
127			f.fieldAPI, capIndexBits[0], capIndexBits[1],
128			merkleCap[i*NUM_LEAF_LOOKUPS], merkleCap[i*NUM_LEAF_LOOKUPS+1], merkleCap[i*NUM_LEAF_LOOKUPS+2], merkleCap[i*NUM_LEAF_LOOKUPS+3],
129		)
130	}
131
132	// Use the most 2 significant bits of the capIndexBits array for the "root" lookup
133	merkleCapEntry := Lookup2Hash(f.fieldAPI, capIndexBits[2], capIndexBits[3], leafLookups[0], leafLookups[1], leafLookups[2], leafLookups[3])
134	AssertIsEqualHash(f.fieldAPI, currentDigest, merkleCapEntry)
135}
136
137func (f *FriChip) verifyInitialProof(xIndexBits []frontend.Variable, proof *FriInitialTreeProof, initialMerkleCaps []MerkleCap, capIndexBits []frontend.Variable) {
138	if len(proof.EvalsProofs) != len(initialMerkleCaps) {
139		panic("length of eval proofs in fri proof should equal length of initial merkle caps")
140	}
141
142	for i := 0; i < len(initialMerkleCaps); i++ {
143		evals := proof.EvalsProofs[i].Elements
144		merkleProof := proof.EvalsProofs[i].MerkleProof
145		cap := initialMerkleCaps[i]
146		f.verifyMerkleProofToCapWithCapIndex(evals, xIndexBits, capIndexBits, cap, &merkleProof)
147	}
148}
149
150// / We decompose FRI query indices into bits without verifying that the decomposition given by
151// / the prover is the canonical one. In particular, if `x_index < 2^field_bits - p`, then the
152// / prover could supply the binary encoding of either `x_index` or `x_index + p`, since they are
153// / congruent mod `p`. However, this only occurs with probability
154// /     p_ambiguous = (2^field_bits - p) / p
155// / which is small for the field that we use in practice.
156// /
157// / In particular, the soundness error of one FRI query is roughly the codeword rate, which
158// / is much larger than this ambiguous-element probability given any reasonable parameters.
159// / Thus ambiguous elements contribute a negligible amount to soundness error.
160// /
161// / Here we compare the probabilities as a sanity check, to verify the claim above.
162func (f *FriChip) assertNoncanonicalIndicesOK() {
163	numAmbiguousElems := uint64(math.MaxUint64) - goldilocks.Modulus().Uint64() + 1
164	queryError := f.friParams.Config.rate()
165	pAmbiguous := float64(numAmbiguousElems) / float64(goldilocks.Modulus().Uint64())
166
167	// TODO:  Check that pAmbiguous value is the same as the one in plonky2 verifier
168	if pAmbiguous >= queryError*1e-5 {
169		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.")
170	}
171}
172
173func (f *FriChip) calculateSubgroupX(
174	xIndexBits []frontend.Variable,
175	nLog uint64,
176) F {
177	// Compute x from its index
178	// `subgroup_x` is `subgroup[x_index]`, i.e., the actual field element in the domain.
179	// TODO - Make these as global values
180	g := field.NewFieldElement(field.GOLDILOCKS_MULTIPLICATIVE_GROUP_GENERATOR.Uint64())
181	base := field.GoldilocksPrimitiveRootOfUnity(nLog)
182
183	product := ONE_F
184	// Create a reverse list of xIndexBits
185	xIndexBitsRev := make([]frontend.Variable, 0)
186	for i := len(xIndexBits) - 1; i >= 0; i-- {
187		xIndexBitsRev = append(xIndexBitsRev, xIndexBits[i])
188	}
189
190	for i, bit := range xIndexBitsRev {
191		pow := int64(1 << i)
192		// If the bit is on, we multiply product by base^pow.
193		// We can arithmetize this as:
194		//     product *= 1 + bit (base^pow - 1)
195		//     product = (base^pow - 1) product bit + product
196		basePow := goldilocks.NewElement(0)
197		basePow.Exp(base, big.NewInt(pow))
198
199		basePowElement := NewFieldElement(basePow.Uint64() - 1)
200
201		product = f.fieldAPI.Add(
202			f.fieldAPI.Mul(
203				basePowElement,
204				product,
205				bit,
206			),
207			product,
208		).(F)
209	}
210
211	return f.fieldAPI.Mul(g, product).(F)
212}
213
214func (f *FriChip) friCombineInitial(
215	instance FriInstanceInfo,
216	proof FriInitialTreeProof,
217	friAlpha QuadraticExtension,
218	subgroupX_QE QuadraticExtension,
219	precomputedReducedEval []QuadraticExtension,
220) QuadraticExtension {
221	sum := f.qeAPI.ZERO_QE
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([]QuadraticExtension, 0)
233		for _, polynomial := range batch.Polynomials {
234			evals = append(
235				evals,
236				QuadraticExtension{proof.EvalsProofs[polynomial.OracleIndex].Elements[polynomial.PolynomialInfo], field.ZERO_F},
237			)
238		}
239
240		reducedEvals := reduceWithPowers(f.qeAPI, evals, friAlpha)
241		numerator := f.qeAPI.SubExtension(reducedEvals, reducedOpenings)
242		denominator := f.qeAPI.SubExtension(subgroupX_QE, point)
243		sum = f.qeAPI.MulExtension(f.qeAPI.ExpU64Extension(friAlpha, uint64(len(evals))), sum)
244		sum = f.qeAPI.AddExtension(
245			f.qeAPI.DivExtension(
246				numerator,
247				denominator,
248			),
249			sum,
250		)
251	}
252
253	return f.qeAPI.MulExtension(sum, subgroupX_QE)
254}
255
256func (f *FriChip) finalPolyEval(finalPoly PolynomialCoeffs, point QuadraticExtension) QuadraticExtension {
257	ret := f.qeAPI.ZERO_QE
258	for i := len(finalPoly.Coeffs) - 1; i >= 0; i-- {
259		ret = f.qeAPI.AddExtension(
260			f.qeAPI.MulExtension(
261				ret,
262				point,
263			),
264			finalPoly.Coeffs[i],
265		)
266	}
267	return ret
268}
269
270func (f *FriChip) verifyQueryRound(
271	instance FriInstanceInfo,
272	challenges *FriChallenges,
273	precomputedReducedEval []QuadraticExtension,
274	initialMerkleCaps []MerkleCap,
275	proof *FriProof,
276	xIndex F,
277	n uint64,
278	nLog uint64,
279	roundProof *FriQueryRound,
280) {
281	f.assertNoncanonicalIndicesOK()
282	xIndexBits := f.fieldAPI.ToBinary(xIndex, int(nLog))
283	capIndexBits := xIndexBits[len(xIndexBits)-int(f.friParams.Config.CapHeight):]
284
285	f.verifyInitialProof(xIndexBits, &roundProof.InitialTreesProof, initialMerkleCaps, capIndexBits)
286
287	subgroupX := f.calculateSubgroupX(
288		xIndexBits,
289		nLog,
290	)
291
292	subgroupX_QE := QuadraticExtension{subgroupX, field.ZERO_F}
293
294	oldEval := f.friCombineInitial(
295		instance,
296		roundProof.InitialTreesProof,
297		challenges.FriAlpha,
298		subgroupX_QE,
299		precomputedReducedEval,
300	)
301
302	finalPolyEval := f.finalPolyEval(proof.FinalPoly, subgroupX_QE)
303
304	f.fieldAPI.AssertIsEqual(oldEval[0], finalPolyEval[0])
305	f.fieldAPI.AssertIsEqual(oldEval[1], finalPolyEval[1])
306}
307
308func (f *FriChip) VerifyFriProof(
309	instance FriInstanceInfo,
310	openings FriOpenings,
311	friChallenges *FriChallenges,
312	initialMerkleCaps []MerkleCap,
313	friProof *FriProof,
314) {
315	// TODO:  Check fri config
316	/* if let Some(max_arity_bits) = params.max_arity_bits() {
317		self.check_recursion_config::<C>(max_arity_bits);
318	}
319
320	debug_assert_eq!(
321		params.final_poly_len(),
322		proof.final_poly.len(),
323		"Final polynomial has wrong degree."
324	); */
325
326	// Check POW
327	f.assertLeadingZeros(friChallenges.FriPowResponse, f.friParams.Config)
328
329	precomputedReducedEvals := f.fromOpeningsAndAlpha(&openings, friChallenges.FriAlpha)
330
331	// Size of the LDE domain.
332	nLog := f.friParams.DegreeBits + f.friParams.Config.RateBits
333	n := uint64(math.Pow(2, float64(nLog)))
334
335	if len(friChallenges.FriQueryIndicies) != len(friProof.QueryRoundProofs) {
336		panic(fmt.Sprintf(
337			"Number of query indices (%d) should equal number of query round proofs (%d)",
338			len(friChallenges.FriQueryIndicies),
339			len(friProof.QueryRoundProofs),
340		))
341	}
342
343	for idx, xIndex := range friChallenges.FriQueryIndicies {
344		roundProof := friProof.QueryRoundProofs[idx]
345
346		f.verifyQueryRound(
347			instance,
348			friChallenges,
349			precomputedReducedEvals,
350			initialMerkleCaps,
351			friProof,
352			xIndex,
353			n,
354			nLog,
355			&roundProof,
356		)
357	}
358}