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