1package plonky2_verifier
  2
  3import (
  4	"fmt"
  5	"gnark-ed25519/field"
  6	. "gnark-ed25519/field"
  7	"gnark-ed25519/poseidon"
  8	"math"
  9
 10	"github.com/consensys/gnark/frontend"
 11)
 12
 13type FriOpeningBatch struct {
 14	values []QuadraticExtension
 15}
 16
 17type FriOpenings struct {
 18	Batches []FriOpeningBatch
 19}
 20
 21func (c *OpeningSet) ToFriOpenings() FriOpenings {
 22	values := c.Constants
 23	values = append(values, c.PlonkSigmas...)
 24	values = append(values, c.Wires...)
 25	values = append(values, c.PlonkZs...)
 26	values = append(values, c.PartialProducts...)
 27	values = append(values, c.QuotientPolys...)
 28	zetaBatch := FriOpeningBatch{values: values}
 29	zetaNextBatch := FriOpeningBatch{values: c.PlonkZsNext}
 30	return FriOpenings{Batches: []FriOpeningBatch{zetaBatch, zetaNextBatch}}
 31}
 32
 33type FriChip struct {
 34	api   frontend.API
 35	field frontend.API
 36	qe    *QuadraticExtensionAPI
 37
 38	poseidonChip *poseidon.PoseidonChip
 39
 40	friParams               *FriParams
 41	verifierOnlyCircuitData *VerifierOnlyCircuitData
 42}
 43
 44func NewFriChip(api frontend.API, field frontend.API, qe *QuadraticExtensionAPI, poseidonChip *poseidon.PoseidonChip, friParams *FriParams) *FriChip {
 45	return &FriChip{
 46		api:          api,
 47		field:        field,
 48		qe:           qe,
 49		poseidonChip: poseidonChip,
 50		friParams:    friParams,
 51	}
 52}
 53
 54func (f *FriChip) assertLeadingZeros(powWitness F, friConfig FriConfig) {
 55	// Asserts that powWitness'es big-endian bit representation has at least `leading_zeros` leading zeros.
 56	// Note that this is assuming that the Goldilocks field is being used.  Specfically that the
 57	// field is 64 bits long
 58	maxPowWitness := uint64(math.Pow(2, float64(64-friConfig.ProofOfWorkBits))) - 1
 59	f.field.AssertIsLessOrEqual(powWitness, field.NewFieldElement(maxPowWitness))
 60}
 61
 62func (f *FriChip) fromOpeningsAndAlpha(openings *FriOpenings, alpha QuadraticExtension) []QuadraticExtension {
 63	// One reduced opening for all openings evaluated at point Zeta.
 64	// Another one for all openings evaluated at point Zeta * Omega (which is only PlonkZsNext polynomial)
 65
 66	reducedOpenings := make([]QuadraticExtension, 0, 2)
 67	for _, batch := range openings.Batches {
 68		reducedOpenings = append(reducedOpenings, reduceWithPowers(f.qe, batch.values, alpha))
 69	}
 70
 71	return reducedOpenings
 72}
 73
 74func (f *FriChip) hashOrNoop(data []F) Hash {
 75	var elements Hash
 76	if len(data) <= 4 {
 77		// Pad the data to have a size of 4
 78		for i, inputElement := range data {
 79			elements[i] = inputElement
 80		}
 81		for i := len(data); i < 4; i++ {
 82			elements[i] = f.qe.ZERO_F
 83		}
 84
 85		return elements
 86	} else {
 87		hashOutput := f.poseidonChip.HashNToMNoPad(data, 4)
 88
 89		if len(hashOutput) != len(elements) {
 90			panic("The length of hashOutput and elements is different")
 91		}
 92
 93		for i, hashField := range hashOutput {
 94			elements[i] = hashField
 95		}
 96
 97		return elements
 98	}
 99}
100
101func (f *FriChip) verifyMerkleProofToCapWithCapIndex(leafData []F, leafIndexBits []frontend.Variable, capIndex F, merkleCap MerkleCap, proof *MerkleProof) {
102	currentDigest := f.hashOrNoop(leafData)
103	fourZeros := [4]F{f.qe.ZERO_F, f.qe.ZERO_F, f.qe.ZERO_F, f.qe.ZERO_F}
104	field.PrintHash(f.field, currentDigest)
105	for i, sibling := range proof.Siblings {
106		bit := leafIndexBits[i]
107
108		var leftSiblingState poseidon.PoseidonState
109		copy(leftSiblingState[0:4], sibling[0:4])
110		copy(leftSiblingState[4:8], currentDigest[0:4])
111		copy(leftSiblingState[8:12], fourZeros[0:4])
112
113		leftHash := f.poseidonChip.Poseidon(leftSiblingState)
114		var leftHashCompress Hash
115		leftHashCompress[0] = leftHash[0]
116		leftHashCompress[1] = leftHash[1]
117		leftHashCompress[2] = leftHash[2]
118		leftHashCompress[3] = leftHash[3]
119
120		var rightSiblingState poseidon.PoseidonState
121		copy(rightSiblingState[0:4], currentDigest[0:4])
122		copy(rightSiblingState[4:8], sibling[0:4])
123		copy(rightSiblingState[8:12], fourZeros[0:4])
124
125		rightHash := f.poseidonChip.Poseidon(rightSiblingState)
126		var rightHashCompress Hash
127		rightHashCompress[0] = rightHash[0]
128		rightHashCompress[1] = rightHash[1]
129		rightHashCompress[2] = rightHash[2]
130		rightHashCompress[3] = rightHash[3]
131
132		currentDigest = SelectHash(f.field, bit, leftHashCompress, rightHashCompress)
133		field.PrintHash(f.field, currentDigest)
134	}
135}
136
137func (f *FriChip) verifyInitialProof(xIndexBits []frontend.Variable, proof *FriInitialTreeProof, initialMerkleCaps []MerkleCap, capIndex F) {
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, capIndex, 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) - EmulatedFieldModulus().Uint64() + 1
164	queryError := f.friParams.Config.rate()
165	pAmbiguous := float64(numAmbiguousElems) / float64(EmulatedFieldModulus().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) verifyQueryRound(
174	challenges *FriChallenges,
175	precomputedReducedEval []QuadraticExtension,
176	initialMerkleCaps []MerkleCap,
177	proof *FriProof,
178	xIndex F,
179	n uint64,
180	nLog uint64,
181	roundProof *FriQueryRound,
182) {
183	f.assertNoncanonicalIndicesOK()
184	xIndexBits := f.qe.field.ToBinary(xIndex, int(nLog))
185	capIndex := f.qe.field.FromBinary(xIndexBits[len(xIndexBits)-int(f.friParams.Config.CapHeight):]...).(F)
186
187	f.verifyInitialProof(xIndexBits, &roundProof.InitialTreesProof, initialMerkleCaps, capIndex)
188}
189
190func (f *FriChip) VerifyFriProof(
191	openings FriOpenings,
192	friChallenges *FriChallenges,
193	initialMerkleCaps []MerkleCap,
194	friProof *FriProof,
195) {
196	// TODO:  Check fri config
197	/* if let Some(max_arity_bits) = params.max_arity_bits() {
198		self.check_recursion_config::<C>(max_arity_bits);
199	}
200
201	debug_assert_eq!(
202		params.final_poly_len(),
203		proof.final_poly.len(),
204		"Final polynomial has wrong degree."
205	); */
206
207	// Check POW
208	f.assertLeadingZeros(friChallenges.FriPowResponse, f.friParams.Config)
209
210	precomputedReducedEvals := f.fromOpeningsAndAlpha(&openings, friChallenges.FriAlpha)
211
212	// Size of the LDE domain.
213	nLog := f.friParams.DegreeBits + f.friParams.Config.RateBits
214	n := uint64(math.Pow(2, float64(nLog)))
215
216	if len(friChallenges.FriQueryIndicies) != len(friProof.QueryRoundProofs) {
217		panic(fmt.Sprintf(
218			"Number of query indices (%d) should equal number of query round proofs (%d)",
219			len(friChallenges.FriQueryIndicies),
220			len(friProof.QueryRoundProofs),
221		))
222	}
223
224	for idx, xIndex := range friChallenges.FriQueryIndicies {
225		roundProof := friProof.QueryRoundProofs[idx]
226
227		f.verifyQueryRound(
228			friChallenges,
229			precomputedReducedEvals,
230			initialMerkleCaps,
231			friProof,
232			xIndex,
233			n,
234			nLog,
235			&roundProof,
236		)
237	}
238}