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