1package plonky2_verifier
  2
  3import (
  4	"gnark-ed25519/field"
  5	. "gnark-ed25519/field"
  6
  7	"github.com/consensys/gnark/frontend"
  8)
  9
 10type PlonkOracle struct {
 11	index    uint64
 12	blinding bool
 13}
 14
 15var CONSTANTS_SIGMAS = PlonkOracle{
 16	index:    0,
 17	blinding: false,
 18}
 19
 20var WIRES = PlonkOracle{
 21	index:    1,
 22	blinding: true,
 23}
 24
 25var ZS_PARTIAL_PRODUCTS = PlonkOracle{
 26	index:    2,
 27	blinding: true,
 28}
 29
 30var QUOTIENT = PlonkOracle{
 31	index:    3,
 32	blinding: true,
 33}
 34
 35type PlonkChip struct {
 36	api frontend.API
 37	qe  *QuadraticExtensionAPI
 38
 39	commonData      CommonCircuitData
 40	proofChallenges ProofChallenges
 41	openings        OpeningSet
 42
 43	DEGREE        F
 44	DEGREE_BITS_F F
 45	DEGREE_QE     QuadraticExtension
 46}
 47
 48func NewPlonkChip(api frontend.API, qe *QuadraticExtensionAPI, commonData CommonCircuitData) *PlonkChip {
 49	// TODO:  Should degreeBits be verified that it fits within the field and that degree is within uint64?
 50
 51	return &PlonkChip{
 52		api: api,
 53		qe:  qe,
 54
 55		commonData: commonData,
 56
 57		DEGREE:        NewFieldElement(1 << commonData.DegreeBits),
 58		DEGREE_BITS_F: NewFieldElement(commonData.DegreeBits),
 59		DEGREE_QE:     QuadraticExtension{NewFieldElement(1 << commonData.DegreeBits), field.ZERO_F},
 60	}
 61}
 62
 63func (p *PlonkChip) expPowerOf2Extension(x QuadraticExtension) QuadraticExtension {
 64	for i := uint64(0); i < p.commonData.DegreeBits; i++ {
 65		x = p.qe.SquareExtension(x)
 66	}
 67
 68	return x
 69}
 70
 71func (p *PlonkChip) evalL0(x QuadraticExtension, xPowN QuadraticExtension) QuadraticExtension {
 72	// L_0(x) = (x^n - 1) / (n * (x - 1))
 73	evalZeroPoly := p.qe.SubExtension(
 74		xPowN,
 75		p.qe.ONE_QE,
 76	)
 77	denominator := p.qe.SubExtension(
 78		p.qe.ScalarMulExtension(x, p.DEGREE),
 79		p.DEGREE_QE,
 80	)
 81	return p.qe.DivExtension(
 82		evalZeroPoly,
 83		denominator,
 84	)
 85}
 86
 87func (p *PlonkChip) checkPartialProducts(
 88	numerators []QuadraticExtension,
 89	denominators []QuadraticExtension,
 90	challengeNum uint64,
 91) []QuadraticExtension {
 92	numPartProds := p.commonData.NumPartialProducts
 93	quotDegreeFactor := p.commonData.QuotientDegreeFactor
 94
 95	productAccs := make([]QuadraticExtension, 0, numPartProds+2)
 96	productAccs = append(productAccs, p.openings.PlonkZs[challengeNum])
 97	productAccs = append(productAccs, p.openings.PartialProducts[challengeNum*numPartProds:(challengeNum+1)*numPartProds]...)
 98	productAccs = append(productAccs, p.openings.PlonkZsNext[challengeNum])
 99
100	partialProductChecks := make([]QuadraticExtension, 0, numPartProds)
101
102	for i := uint64(0); i <= numPartProds; i += 1 {
103		ppStartIdx := i * quotDegreeFactor
104		numeProduct := numerators[ppStartIdx]
105		denoProduct := denominators[ppStartIdx]
106		for j := uint64(1); j < quotDegreeFactor; j++ {
107			numeProduct = p.qe.MulExtension(numeProduct, numerators[ppStartIdx+j])
108			denoProduct = p.qe.MulExtension(denoProduct, denominators[ppStartIdx+j])
109		}
110
111		partialProductCheck := p.qe.SubExtension(
112			p.qe.MulExtension(productAccs[i], numeProduct),
113			p.qe.MulExtension(productAccs[i+1], denoProduct),
114		)
115
116		partialProductChecks = append(partialProductChecks, partialProductCheck)
117	}
118	return partialProductChecks
119}
120
121func (p *PlonkChip) evalVanishingPoly(zetaPowN QuadraticExtension) []QuadraticExtension {
122	// Calculate the k[i] * x
123	sIDs := make([]QuadraticExtension, p.commonData.Config.NumRoutedWires)
124
125	for i := uint64(0); i < p.commonData.Config.NumRoutedWires; i++ {
126		sIDs[i] = p.qe.ScalarMulExtension(p.proofChallenges.PlonkZeta, p.commonData.KIs[i])
127	}
128
129	// Calculate L_0(zeta)
130	l0Zeta := p.evalL0(p.proofChallenges.PlonkZeta, zetaPowN)
131
132	vanishingZ1Terms := make([]QuadraticExtension, 0, p.commonData.Config.NumChallenges)
133	vanishingPartialProductsTerms := make([]QuadraticExtension, 0, p.commonData.Config.NumChallenges*p.commonData.NumPartialProducts)
134	for i := uint64(0); i < p.commonData.Config.NumChallenges; i++ {
135		// L_0(zeta) (Z(zeta) - 1) = 0
136		z1_term := p.qe.MulExtension(
137			l0Zeta,
138			p.qe.SubExtension(p.openings.PlonkZs[i], p.qe.ONE_QE))
139		vanishingZ1Terms = append(vanishingZ1Terms, z1_term)
140
141		numeratorValues := make([]QuadraticExtension, 0, p.commonData.Config.NumRoutedWires)
142		denominatorValues := make([]QuadraticExtension, 0, p.commonData.Config.NumRoutedWires)
143		for j := uint64(0); j < p.commonData.Config.NumRoutedWires; j++ {
144			// The numerator is `beta * s_id + wire_value + gamma`, and the denominator is
145			// `beta * s_sigma + wire_value + gamma`.
146
147			wireValuePlusGamma := p.qe.AddExtension(
148				p.openings.Wires[j],
149				p.qe.FieldToQE(p.proofChallenges.PlonkGammas[i]),
150			)
151
152			numerator := p.qe.AddExtension(
153				p.qe.MulExtension(
154					p.qe.FieldToQE(p.proofChallenges.PlonkBetas[i]),
155					sIDs[j],
156				),
157				wireValuePlusGamma,
158			)
159
160			denominator := p.qe.AddExtension(
161				p.qe.MulExtension(
162					p.qe.FieldToQE(p.proofChallenges.PlonkBetas[i]),
163					p.openings.PlonkSigmas[j],
164				),
165				wireValuePlusGamma,
166			)
167
168			numeratorValues = append(numeratorValues, numerator)
169			denominatorValues = append(denominatorValues, denominator)
170		}
171
172		vanishingPartialProductsTerms = append(
173			vanishingPartialProductsTerms,
174			p.checkPartialProducts(numeratorValues, denominatorValues, i)...,
175		)
176	}
177
178	vanishingTerms := append(vanishingZ1Terms, vanishingPartialProductsTerms...)
179
180	reducedValues := make([]QuadraticExtension, p.commonData.Config.NumChallenges)
181	for i := uint64(0); i < p.commonData.Config.NumChallenges; i++ {
182		reducedValues[i] = p.qe.ZERO_QE
183	}
184
185	// TODO:  Enable this check once the custom gate evaluations are added to the
186	//        vanishingTerms array
187	/*
188		if len(vanishingTerms) != int(p.commonData.QuotientDegreeFactor) {
189			panic("evalVanishingPoly: len(vanishingTerms) != int(p.commonData.QuotientDegreeFactor)")
190		}
191	*/
192
193	// reverse iterate the vanishingPartialProductsTerms array
194	for i := len(vanishingTerms) - 1; i >= 0; i-- {
195		for j := uint64(0); j < p.commonData.Config.NumChallenges; j++ {
196			reducedValues[j] = p.qe.AddExtension(
197				vanishingTerms[i],
198				p.qe.ScalarMulExtension(
199					reducedValues[j],
200					p.proofChallenges.PlonkAlphas[j],
201				),
202			)
203		}
204	}
205
206	return reducedValues
207}
208
209func (p *PlonkChip) Verify() {
210	// Calculate zeta^n
211	zetaPowN := p.expPowerOf2Extension(p.proofChallenges.PlonkZeta)
212
213	vanishingPolysZeta := p.evalVanishingPoly(zetaPowN)
214
215	// Calculate Z(H)
216	zHZeta := p.qe.SubExtension(zetaPowN, p.qe.ONE_QE)
217
218	// `quotient_polys_zeta` holds `num_challenges * quotient_degree_factor` evaluations.
219	// Each chunk of `quotient_degree_factor` holds the evaluations of `t_0(zeta),...,t_{quotient_degree_factor-1}(zeta)`
220	// where the "real" quotient polynomial is `t(X) = t_0(X) + t_1(X)*X^n + t_2(X)*X^{2n} + ...`.
221	// So to reconstruct `t(zeta)` we can compute `reduce_with_powers(chunk, zeta^n)` for each
222	// `quotient_degree_factor`-sized chunk of the original evaluations.
223	for i := 0; i < len(p.openings.QuotientPolys); i += int(p.commonData.QuotientDegreeFactor) {
224		prod := p.qe.MulExtension(
225			zHZeta,
226			p.qe.ReduceWithPowers(
227				p.openings.QuotientPolys[i:i+int(p.commonData.QuotientDegreeFactor)],
228				zetaPowN,
229			),
230		)
231
232		// TODO: Uncomment this after adding in the custom gates evaluations
233		//p.api.AssertIsEqual(vanishingPolysZeta[i], prod)
234	}
235}