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