1package plonky2_verifier
  2
  3import (
  4	"gnark-ed25519/field"
  5	. "gnark-ed25519/field"
  6	"gnark-ed25519/poseidon"
  7	"math"
  8
  9	"github.com/consensys/gnark/frontend"
 10)
 11
 12type FriOpeningBatch struct {
 13	values []QuadraticExtension
 14}
 15
 16type FriOpenings struct {
 17	Batches []FriOpeningBatch
 18}
 19
 20func (c *OpeningSet) ToFriOpenings() FriOpenings {
 21	values := c.Constants
 22	values = append(values, c.PlonkSigmas...)
 23	values = append(values, c.Wires...)
 24	values = append(values, c.PlonkZs...)
 25	values = append(values, c.PartialProducts...)
 26	values = append(values, c.QuotientPolys...)
 27	zetaBatch := FriOpeningBatch{values: values}
 28	zetaNextBatch := FriOpeningBatch{values: c.PlonkZsNext}
 29	return FriOpenings{Batches: []FriOpeningBatch{zetaBatch, zetaNextBatch}}
 30}
 31
 32type FriChip struct {
 33	api   frontend.API
 34	field frontend.API
 35	qe    *QuadraticExtensionAPI
 36
 37	poseidonChip *poseidon.PoseidonChip
 38
 39	friParams               *FriParams
 40	verifierOnlyCircuitData *VerifierOnlyCircuitData
 41}
 42
 43func NewFriChip(api frontend.API, field frontend.API, qe *QuadraticExtensionAPI, poseidonChip *poseidon.PoseidonChip, friParams *FriParams) *FriChip {
 44	return &FriChip{
 45		api:          api,
 46		field:        field,
 47		qe:           qe,
 48		poseidonChip: poseidonChip,
 49		friParams:    friParams,
 50	}
 51}
 52
 53func (f *FriChip) assertLeadingZeros(powWitness F, friConfig FriConfig) {
 54	// Asserts that powWitness'es big-endian bit representation has at least `leading_zeros` leading zeros.
 55	// Note that this is assuming that the Goldilocks field is being used.  Specfically that the
 56	// field is 64 bits long
 57	maxPowWitness := uint64(math.Pow(2, float64(64-friConfig.ProofOfWorkBits))) - 1
 58	f.field.AssertIsLessOrEqual(powWitness, field.NewFieldElement(maxPowWitness))
 59}
 60
 61func (f *FriChip) fromOpeningsAndAlpha(openings *FriOpenings, alpha QuadraticExtension) []QuadraticExtension {
 62	// One reduced opening for all openings evaluated at point Zeta.
 63	// Another one for all openings evaluated at point Zeta * Omega (which is only PlonkZsNext polynomial)
 64
 65	reducedOpenings := make([]QuadraticExtension, 0, 2)
 66	for _, batch := range openings.Batches {
 67		reducedOpenings = append(reducedOpenings, reduceWithPowers(f.qe, batch.values, alpha))
 68	}
 69
 70	return reducedOpenings
 71}
 72
 73func (f *FriChip) hashOrNoop(data []F) Hash {
 74	var elements Hash
 75	if len(data) <= 4 {
 76		// Pad the data to have a size of 4
 77		for i, inputElement := range data {
 78			elements[i] = inputElement
 79		}
 80		for i := len(data); i < 4; i++ {
 81			elements[i] = f.qe.ZERO_F
 82		}
 83
 84		return elements
 85	} else {
 86		hashOutput := f.poseidonChip.HashNToMNoPad(data, 4)
 87
 88		if len(hashOutput) != len(elements) {
 89			panic("The length of hashOutput and elements is different")
 90		}
 91
 92		for i, hashField := range hashOutput {
 93			elements[i] = hashField
 94		}
 95
 96		return elements
 97	}
 98}
 99
100func (f *FriChip) verifyMerkleProofToCapWithCapIndex(leafData []F, leafIndexBits []frontend.Variable, capIndex F, merkleCap MerkleCap, proof *MerkleProof) {
101	currentDigest := f.hashOrNoop(leafData)
102
103	if len(leafIndexBits) != len(proof.Siblings) {
104		panic("len(leafIndexBits) != len(proof.Siblings)")
105	}
106
107	fourZeros := [4]F{f.qe.ZERO_F, f.qe.ZERO_F, f.qe.ZERO_F, f.qe.ZERO_F}
108	for i, bit := range leafIndexBits {
109		sibling := proof.Siblings[i]
110
111		var leftSiblingState poseidon.PoseidonState
112		copy(leftSiblingState[0:4], sibling[0:4])
113		copy(leftSiblingState[4:8], currentDigest[0:4])
114		copy(leftSiblingState[8:12], fourZeros[0:4])
115		leftHash := f.poseidonChip.Poseidon(leftSiblingState)
116		leftHashCompress := leftHash[0:4]
117
118		var rightSiblingState poseidon.PoseidonState
119		copy(rightSiblingState[0:4], currentDigest[0:4])
120		copy(rightSiblingState[4:8], sibling[0:4])
121		copy(rightSiblingState[8:12], fourZeros[0:4])
122		rightHash := f.poseidonChip.Poseidon(rightSiblingState)
123		rightHashCompress := rightHash[0:4]
124
125		currentDigest = f.api.Select(bit, leftHashCompress, rightHashCompress).(Hash)
126	}
127}
128
129func (f *FriChip) verifyInitialProof(xIndexBits []frontend.Variable, proof *FriInitialTreeProof, initialMerkleCaps []MerkleCap, capIndex F) {
130	if len(proof.EvalsProofs) != len(initialMerkleCaps) {
131		panic("length of eval proofs in fri proof should equal length of initial merkle caps")
132	}
133
134	for i := 0; i < len(initialMerkleCaps); i++ {
135		evals := proof.EvalsProofs[i].Elements
136		merkleProof := proof.EvalsProofs[i].MerkleProof
137		cap := initialMerkleCaps[i]
138		f.verifyMerkleProofToCapWithCapIndex(evals, xIndexBits, capIndex, cap, &merkleProof)
139	}
140}
141
142// / We decompose FRI query indices into bits without verifying that the decomposition given by
143// / the prover is the canonical one. In particular, if `x_index < 2^field_bits - p`, then the
144// / prover could supply the binary encoding of either `x_index` or `x_index + p`, since they are
145// / congruent mod `p`. However, this only occurs with probability
146// /     p_ambiguous = (2^field_bits - p) / p
147// / which is small for the field that we use in practice.
148// /
149// / In particular, the soundness error of one FRI query is roughly the codeword rate, which
150// / is much larger than this ambiguous-element probability given any reasonable parameters.
151// / Thus ambiguous elements contribute a negligible amount to soundness error.
152// /
153// / Here we compare the probabilities as a sanity check, to verify the claim above.
154func (f *FriChip) assertNoncanonicalIndicesOK() {
155	numAmbiguousElems := uint64(math.MaxUint64) - EmulatedFieldModulus().Uint64() + 1
156	queryError := f.friParams.Config.rate()
157	pAmbiguous := float64(numAmbiguousElems) / float64(EmulatedFieldModulus().Uint64())
158	if pAmbiguous < queryError*1e-5 {
159		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.")
160	}
161}
162
163func (f *FriChip) verifyQueryRound(
164	challenges *FriChallenges,
165	precomputedReducedEval []QuadraticExtension,
166	initialMerkleCaps []MerkleCap,
167	proof *FriProof,
168	xIndex F,
169	n uint64,
170	roundProof *FriQueryRound,
171) {
172	nLog := log2Strict(uint(n))
173
174	f.assertNoncanonicalIndicesOK()
175	xIndexBits := f.qe.field.ToBinary(xIndex, nLog)
176	capIndex := f.qe.field.FromBinary(xIndexBits[len(xIndexBits)-int(f.friParams.Config.CapHeight):]...).(F)
177
178	f.verifyInitialProof(xIndexBits, &roundProof.InitialTreesProof, initialMerkleCaps, capIndex)
179}
180
181func (f *FriChip) VerifyFriProof(
182	openings FriOpenings,
183	friChallenges *FriChallenges,
184	initialMerkleCaps []MerkleCap,
185	friProof *FriProof,
186) {
187	// TODO:  Check fri config
188	/* if let Some(max_arity_bits) = params.max_arity_bits() {
189		self.check_recursion_config::<C>(max_arity_bits);
190	}
191
192	debug_assert_eq!(
193		params.final_poly_len(),
194		proof.final_poly.len(),
195		"Final polynomial has wrong degree."
196	); */
197
198	// Check POW
199	f.assertLeadingZeros(friChallenges.FriPowResponse, f.friParams.Config)
200
201	precomputedReducedEvals := f.fromOpeningsAndAlpha(&openings, friChallenges.FriAlpha)
202
203	// Size of the LDE domain.
204	n := uint64(math.Pow(2, float64(f.friParams.DegreeBits+f.friParams.Config.RateBits)))
205
206	if len(friChallenges.FriQueryIndicies) != len(precomputedReducedEvals) {
207		panic("Number of queryRoundProofs should equal number of precomputedReducedEvals")
208	}
209
210	for idx, xIndex := range friChallenges.FriQueryIndicies {
211		roundProof := friProof.QueryRoundProofs[idx]
212
213		f.verifyQueryRound(
214			friChallenges,
215			precomputedReducedEvals,
216			initialMerkleCaps,
217			friProof,
218			xIndex,
219			n,
220			&roundProof,
221		)
222	}
223}