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