gnark-plonky2-verifier/goldilocks/base.go
goldilocks/base.goRaw
1// This package implements efficient Golidlocks arithmetic operations within Gnark. We do not use
2// the emulated field arithmetic API, because it is too slow for our purposes. Instead, we use
3// an efficient reduction method that leverages the fact that the modulus is a simple
4// linear combination of powers of two.
5package goldilocks
6
7// In general, methods whose name do not contain `NoReduce` can be used without any extra mental
8// overhead. These methods act exactly as you would expect a normal field would operate.
9//
10// However, if you want to aggressively optimize the number of constraints in your circuit, it can
11// be very beneficial to use the no reduction methods and keep track of the maximum number of bits
12// your computation uses.
13
14// This implementation is based on the following plonky2 implementation of Goldilocks
15// Available here: https://github.com/0xPolygonZero/plonky2/blob/main/field/src/goldilocks_field.rs#L70
16
17import (
18 "fmt"
19 "math"
20 "math/big"
21
22 "github.com/consensys/gnark-crypto/field/goldilocks"
23 "github.com/consensys/gnark/constraint/solver"
24 "github.com/consensys/gnark/frontend"
25 "github.com/consensys/gnark/std/math/emulated"
26 "github.com/consensys/gnark/std/rangecheck"
27)
28
29// The multiplicative group generator of the field.
30var MULTIPLICATIVE_GROUP_GENERATOR goldilocks.Element = goldilocks.NewElement(7)
31
32// The two adicity of the field.
33var TWO_ADICITY uint64 = 32
34
35// The power of two generator of the field.
36var POWER_OF_TWO_GENERATOR goldilocks.Element = goldilocks.NewElement(1753635133440165772)
37
38// The modulus of the field.
39var MODULUS *big.Int = emulated.Goldilocks{}.Modulus()
40
41// The number of bits to use for range checks on inner products of field elements.
42var RANGE_CHECK_NB_BITS int = 140
43
44// Registers the hint functions with the solver.
45func init() {
46 solver.RegisterHint(MulAddHint)
47 solver.RegisterHint(ReduceHint)
48 solver.RegisterHint(InverseHint)
49 solver.RegisterHint(SplitLimbsHint)
50}
51
52// A type alias used to represent Goldilocks field elements.
53type Variable struct {
54 Limb frontend.Variable
55}
56
57// Creates a new Goldilocks field element from an existing variable. Assumes that the element is
58// already reduced.
59func NewVariable(x frontend.Variable) Variable {
60 return Variable{Limb: x}
61}
62
63// The zero element in the Golidlocks field.
64func Zero() Variable {
65 return NewVariable(0)
66}
67
68// The one element in the Goldilocks field.
69func One() Variable {
70 return NewVariable(1)
71}
72
73// The negative one element in the Goldilocks field.
74func NegOne() Variable {
75 return NewVariable(MODULUS.Uint64() - 1)
76}
77
78// The chip used for Goldilocks field operations.
79type Chip struct {
80 api frontend.API
81 rangeChecker frontend.Rangechecker
82}
83
84// Creates a new Goldilocks Chip.
85func New(api frontend.API) *Chip {
86 rangeChecker := rangecheck.New(api)
87 return &Chip{api: api, rangeChecker: rangeChecker}
88}
89
90// Adds two goldilocks field elements and returns a value within the goldilocks field.
91func (p *Chip) Add(a Variable, b Variable) Variable {
92 return p.MulAdd(a, NewVariable(1), b)
93}
94
95// Adds two goldilocks field elements and returns a value that may not be within the goldilocks field
96// (e.g. the sum is not reduced).
97func (p *Chip) AddNoReduce(a Variable, b Variable) Variable {
98 return NewVariable(p.api.Add(a.Limb, b.Limb))
99}
100
101// Subracts two goldilocks field elements and returns a value within the goldilocks field.
102func (p *Chip) Sub(a Variable, b Variable) Variable {
103 return p.MulAdd(b, NegOne(), a)
104}
105
106// Subracts two goldilocks field elements and returns a value that may not be within the goldilocks field
107// (e.g. the difference is not reduced).
108func (p *Chip) SubNoReduce(a Variable, b Variable) Variable {
109 return NewVariable(p.api.Add(a.Limb, p.api.Mul(b.Limb, NegOne().Limb)))
110}
111
112// Multiplies two goldilocks field elements and returns a value within the goldilocks field.
113func (p *Chip) Mul(a Variable, b Variable) Variable {
114 return p.MulAdd(a, b, Zero())
115}
116
117// Multiplies two goldilocks field elements and returns a value that may not be within the goldilocks field
118// (e.g. the product is not reduced).
119func (p *Chip) MulNoReduce(a Variable, b Variable) Variable {
120 return NewVariable(p.api.Mul(a.Limb, b.Limb))
121}
122
123// Multiplies two field elements and adds a field element (e.g. computes a * b + c). The returned value
124// will be within the goldilocks field.
125func (p *Chip) MulAdd(a Variable, b Variable, c Variable) Variable {
126 result, err := p.api.Compiler().NewHint(MulAddHint, 2, a.Limb, b.Limb, c.Limb)
127 if err != nil {
128 panic(err)
129 }
130
131 quotient := NewVariable(result[0])
132 remainder := NewVariable(result[1])
133
134 cLimbCopy := p.api.Mul(c.Limb, 1)
135 lhs := p.api.MulAcc(cLimbCopy, a.Limb, b.Limb)
136 rhs := p.api.MulAcc(remainder.Limb, MODULUS, quotient.Limb)
137 p.api.AssertIsEqual(lhs, rhs)
138
139 p.RangeCheck(quotient)
140 p.RangeCheck(remainder)
141 return remainder
142}
143
144// Multiplies two field elements and adds a field element (e.g. computes a * b + c). The returned value
145// may no be within the goldilocks field (e.g. the result is not reduced).
146func (p *Chip) MulAddNoReduce(a Variable, b Variable, c Variable) Variable {
147 cLimbCopy := p.api.Mul(c.Limb, 1)
148 return NewVariable(p.api.MulAcc(cLimbCopy, a.Limb, b.Limb))
149}
150
151// The hint used to compute MulAdd.
152func MulAddHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
153 if len(inputs) != 3 {
154 panic("MulAddHint expects 3 input operands")
155 }
156
157 for _, operand := range inputs {
158 if operand.Cmp(MODULUS) >= 0 {
159 panic(fmt.Sprintf("%s is not in the field", operand.String()))
160 }
161 }
162
163 product := new(big.Int).Mul(inputs[0], inputs[1])
164 sum := new(big.Int).Add(product, inputs[2])
165 quotient := new(big.Int).Div(sum, MODULUS)
166 remainder := new(big.Int).Rem(sum, MODULUS)
167
168 results[0] = quotient
169 results[1] = remainder
170
171 return nil
172}
173
174// Reduces a field element x such that x % MODULUS = y.
175func (p *Chip) Reduce(x Variable) Variable {
176 // Witness a `quotient` and `remainder` such that:
177 //
178 // MODULUS * quotient + remainder = x
179 //
180 // Must check that offset \in [0, MODULUS) and carry \in [0, 2^RANGE_CHECK_NB_BITS) to ensure
181 // that this computation does not overflow. We use 2^RANGE_CHECK_NB_BITS to reduce the cost of the range check
182 //
183 // In other words, we assume that we at most compute a a dot product with dimension at most RANGE_CHECK_NB_BITS - 128.
184 return p.ReduceWithMaxBits(x, uint64(RANGE_CHECK_NB_BITS))
185}
186
187// Reduces a field element x such that x % MODULUS = y.
188func (p *Chip) ReduceWithMaxBits(x Variable, maxNbBits uint64) Variable {
189 // Witness a `quotient` and `remainder` such that:
190 //
191 // MODULUS * quotient + remainder = x
192 //
193 // Must check that remainder \in [0, MODULUS) and quotient \in [0, 2^maxNbBits) to ensure that this
194 // computation does not overflow.
195
196 result, err := p.api.Compiler().NewHint(ReduceHint, 2, x.Limb)
197 if err != nil {
198 panic(err)
199 }
200
201 quotient := result[0]
202 p.rangeChecker.Check(quotient, int(maxNbBits))
203
204 remainder := NewVariable(result[1])
205 p.RangeCheck(remainder)
206
207 p.api.AssertIsEqual(x.Limb, p.api.Add(p.api.Mul(quotient, MODULUS), remainder.Limb))
208
209 return remainder
210}
211
212// The hint used to compute Reduce.
213func ReduceHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
214 if len(inputs) != 1 {
215 panic("ReduceHint expects 1 input operand")
216 }
217 input := inputs[0]
218 quotient := new(big.Int).Div(input, MODULUS)
219 remainder := new(big.Int).Rem(input, MODULUS)
220 results[0] = quotient
221 results[1] = remainder
222 return nil
223}
224
225// Computes the inverse of a field element x such that x * x^-1 = 1.
226func (p *Chip) Inverse(x Variable) (Variable, frontend.Variable) {
227 result, err := p.api.Compiler().NewHint(InverseHint, 2, x.Limb)
228 if err != nil {
229 panic(err)
230 }
231
232 inverse := NewVariable(result[0])
233 hasInv := frontend.Variable(result[1])
234 p.RangeCheck(inverse)
235
236 product := p.Mul(inverse, x)
237 productToCheck := p.api.Select(hasInv, product.Limb, frontend.Variable(1))
238 p.api.AssertIsEqual(productToCheck, frontend.Variable(1))
239
240 return inverse, hasInv
241}
242
243// The hint used to compute Inverse.
244func InverseHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
245 if len(inputs) != 1 {
246 panic("InverseHint expects 1 input operand")
247 }
248
249 input := inputs[0]
250 if input.Cmp(MODULUS) == 0 || input.Cmp(MODULUS) == 1 {
251 panic("Input is not in the field")
252 }
253
254 inputGl := goldilocks.NewElement(input.Uint64())
255 resultGl := goldilocks.NewElement(0)
256
257 // Will set resultGL if inputGL == 0
258 resultGl.Inverse(&inputGl)
259
260 result := big.NewInt(0)
261 results[0] = resultGl.BigInt(result)
262
263 hasInvInt64 := int64(0)
264 if !inputGl.IsZero() {
265 hasInvInt64 = 1
266 }
267 results[1] = big.NewInt(hasInvInt64)
268
269 return nil
270}
271
272// Computes a field element raised to some power.
273func (p *Chip) Exp(x Variable, k *big.Int) Variable {
274 if k.IsUint64() && k.Uint64() == 0 {
275 return One()
276 }
277
278 e := k
279 if k.Sign() == -1 {
280 panic("Unsupported negative exponent. Need to implement inversion.")
281 }
282
283 z := x
284 for i := e.BitLen() - 2; i >= 0; i-- {
285 z = p.Mul(z, z)
286 if e.Bit(i) == 1 {
287 z = p.Mul(z, x)
288 }
289 }
290
291 return z
292}
293
294// The hint used to split a GoldilocksVariable into 2 32 bit limbs.
295func SplitLimbsHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
296 if len(inputs) != 1 {
297 panic("SplitLimbsHint expects 1 input operand")
298 }
299
300 // The Goldilocks field element
301 input := inputs[0]
302
303 if input.Cmp(MODULUS) == 0 || input.Cmp(MODULUS) == 1 {
304 return fmt.Errorf("input is not in the field")
305 }
306
307 two_32 := big.NewInt(int64(math.Pow(2, 32)))
308
309 // The most significant bits
310 results[0] = new(big.Int).Quo(input, two_32)
311 // The least significant bits
312 results[1] = new(big.Int).Rem(input, two_32)
313
314 return nil
315}
316
317// Range checks a field element x to be less than the Golidlocks modulus 2 ^ 64 - 2 ^ 32 + 1.
318func (p *Chip) RangeCheck(x Variable) {
319 // The Goldilocks' modulus is 2^64 - 2^32 + 1, which is:
320 //
321 // 1111111111111111111111111111111100000000000000000000000000000001
322 //
323 // in big endian binary. This function will first verify that x is at most 64 bits wide. Then it
324 // checks that if the bits[0:31] (in big-endian) are all 1, then bits[32:64] are all zero.
325
326 result, err := p.api.Compiler().NewHint(SplitLimbsHint, 2, x.Limb)
327 if err != nil {
328 panic(err)
329 }
330
331 // We check that this is a valid decomposition of the Goldilock's element and range-check each limb.
332 mostSigLimb := result[0]
333 leastSigLimb := result[1]
334 p.api.AssertIsEqual(
335 p.api.Add(
336 p.api.Mul(mostSigLimb, uint64(math.Pow(2, 32))),
337 leastSigLimb,
338 ),
339 x.Limb,
340 )
341 p.rangeChecker.Check(mostSigLimb, 32)
342 p.rangeChecker.Check(leastSigLimb, 32)
343
344 // If the most significant bits are all 1, then we need to check that the least significant bits are all zero
345 // in order for element to be less than the Goldilock's modulus.
346 // Otherwise, we don't need to do any checks, since we already know that the element is less than the Goldilocks modulus.
347 shouldCheck := p.api.IsZero(p.api.Sub(mostSigLimb, uint64(math.Pow(2, 32))-1))
348 p.api.AssertIsEqual(
349 p.api.Select(
350 shouldCheck,
351 leastSigLimb,
352 frontend.Variable(0),
353 ),
354 frontend.Variable(0),
355 )
356}
357
358func (p *Chip) AssertIsEqual(x, y Variable) {
359 p.api.AssertIsEqual(x.Limb, y.Limb)
360}
361
362// Computes the n'th primitive root of unity for the Goldilocks field.
363func PrimitiveRootOfUnity(nLog uint64) goldilocks.Element {
364 if nLog > TWO_ADICITY {
365 panic("nLog is greater than TWO_ADICITY")
366 }
367 res := goldilocks.NewElement(POWER_OF_TWO_GENERATOR.Uint64())
368 for i := 0; i < int(TWO_ADICITY-nLog); i++ {
369 res.Square(&res)
370 }
371 return res
372}
373
374func TwoAdicSubgroup(nLog uint64) []goldilocks.Element {
375 if nLog > TWO_ADICITY {
376 panic("nLog is greater than GOLDILOCKS_TWO_ADICITY")
377 }
378
379 var res []goldilocks.Element
380 rootOfUnity := PrimitiveRootOfUnity(nLog)
381 res = append(res, goldilocks.NewElement(1))
382
383 for i := 0; i < (1<<nLog)-1; i++ {
384 lastElement := res[len(res)-1]
385 res = append(res, *lastElement.Mul(&lastElement, &rootOfUnity))
386 }
387
388 return res
389}