arnaucube
arnaucube/gnark-plonky2-verifierPublic Self-hosted repository
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 threshold maximum number of bits at which we must reduce the element.
 42var REDUCE_NB_BITS_THRESHOLD uint8 = 254 - 64
 43
 44// The number of bits to use for range checks on inner products of field elements.
 45var RANGE_CHECK_NB_BITS int = 140
 46
 47// Registers the hint functions with the solver.
 48func init() {
 49	solver.RegisterHint(MulAddHint)
 50	solver.RegisterHint(ReduceHint)
 51	solver.RegisterHint(InverseHint)
 52	solver.RegisterHint(SplitLimbsHint)
 53}
 54
 55// A type alias used to represent Goldilocks field elements.
 56type Variable struct {
 57	Limb frontend.Variable
 58}
 59
 60// Creates a new Goldilocks field element from an existing variable. Assumes that the element is
 61// already reduced.
 62func NewVariable(x frontend.Variable) Variable {
 63	return Variable{Limb: x}
 64}
 65
 66// The zero element in the Golidlocks field.
 67func Zero() Variable {
 68	return NewVariable(0)
 69}
 70
 71// The one element in the Goldilocks field.
 72func One() Variable {
 73	return NewVariable(1)
 74}
 75
 76// The negative one element in the Goldilocks field.
 77func NegOne() Variable {
 78	return NewVariable(MODULUS.Uint64() - 1)
 79}
 80
 81// The chip used for Goldilocks field operations.
 82type Chip struct {
 83	api          frontend.API
 84	rangeChecker frontend.Rangechecker
 85}
 86
 87// Creates a new Goldilocks Chip.
 88func New(api frontend.API) *Chip {
 89	rangeChecker := rangecheck.New(api)
 90	return &Chip{api: api, rangeChecker: rangeChecker}
 91}
 92
 93// Adds two field elements such that x + y = z within the Golidlocks field.
 94func (p *Chip) Add(a Variable, b Variable) Variable {
 95	return p.MulAdd(a, NewVariable(1), b)
 96}
 97
 98// Adds two field elements such that x + y = z within the Golidlocks field without reducing.
 99func (p *Chip) AddNoReduce(a Variable, b Variable) Variable {
100	return NewVariable(p.api.Add(a.Limb, b.Limb))
101}
102
103// Subtracts two field elements such that x + y = z within the Golidlocks field.
104func (p *Chip) Sub(a Variable, b Variable) Variable {
105	return p.MulAdd(b, NewVariable(MODULUS.Uint64()-1), a)
106}
107
108// Subtracts two field elements such that x + y = z within the Golidlocks field without reducing.
109func (p *Chip) SubNoReduce(a Variable, b Variable) Variable {
110	return NewVariable(p.api.Add(a.Limb, p.api.Mul(b.Limb, MODULUS.Uint64()-1)))
111}
112
113// Multiplies two field elements such that x * y = z within the Golidlocks field.
114func (p *Chip) Mul(a Variable, b Variable) Variable {
115	return p.MulAdd(a, b, Zero())
116}
117
118// Multiplies two field elements such that x * y = z within the Golidlocks field without reducing.
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 such that x * y + z = c within the
124// Golidlocks 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	lhs := p.api.MulAcc(c.Limb, a.Limb, b.Limb)
135	rhs := p.api.MulAcc(remainder.Limb, MODULUS, quotient.Limb)
136	p.api.AssertIsEqual(lhs, rhs)
137
138	p.RangeCheck(quotient)
139	p.RangeCheck(remainder)
140	return remainder
141}
142
143// Multiplies two field elements and adds a field element such that x * y + z = c within the
144// Golidlocks field without reducing.
145func (p *Chip) MulAddNoReduce(a Variable, b Variable, c Variable) Variable {
146	return NewVariable(p.api.MulAcc(c.Limb, a.Limb, b.Limb))
147}
148
149// The hint used to compute MulAdd.
150func MulAddHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
151	if len(inputs) != 3 {
152		panic("MulAddHint expects 3 input operands")
153	}
154
155	for _, operand := range inputs {
156		if operand.Cmp(MODULUS) >= 0 {
157			panic(fmt.Sprintf("%s is not in the field", operand.String()))
158		}
159	}
160
161	product := new(big.Int).Mul(inputs[0], inputs[1])
162	sum := new(big.Int).Add(product, inputs[2])
163	quotient := new(big.Int).Div(sum, MODULUS)
164	remainder := new(big.Int).Rem(sum, MODULUS)
165
166	results[0] = quotient
167	results[1] = remainder
168
169	return nil
170}
171
172// Reduces a field element x such that x % MODULUS = y.
173func (p *Chip) Reduce(x Variable) Variable {
174	// Witness a `quotient` and `remainder` such that:
175	//
176	// 		MODULUS * quotient + remainder = x
177	//
178	// Must check that offset \in [0, MODULUS) and carry \in [0, 2^RANGE_CHECK_NB_BITS) to ensure
179	// that this computation does not overflow. We use 2^RANGE_CHECK_NB_BITS to reduce the cost of the range check
180	//
181	// In other words, we assume that we at most compute a a dot product with dimension at most RANGE_CHECK_NB_BITS - 128.
182
183	result, err := p.api.Compiler().NewHint(ReduceHint, 2, x.Limb)
184	if err != nil {
185		panic(err)
186	}
187
188	quotient := result[0]
189	p.rangeChecker.Check(quotient, RANGE_CHECK_NB_BITS)
190
191	remainder := NewVariable(result[1])
192	p.RangeCheck(remainder)
193
194	p.api.AssertIsEqual(x, p.api.Add(p.api.Mul(quotient, MODULUS), remainder.Limb))
195
196	return remainder
197}
198
199// Reduces a field element x such that x % MODULUS = y.
200func (p *Chip) ReduceWithMaxBits(x Variable, maxNbBits uint64) Variable {
201	// Witness a `quotient` and `remainder` such that:
202	//
203	// 		MODULUS * quotient + remainder = x
204	//
205	// Must check that remainder \in [0, MODULUS) and quotient \in [0, 2^maxNbBits) to ensure that this
206	// computation does not overflow.
207
208	result, err := p.api.Compiler().NewHint(ReduceHint, 2, x.Limb)
209	if err != nil {
210		panic(err)
211	}
212
213	quotient := result[0]
214	p.rangeChecker.Check(quotient, int(maxNbBits))
215
216	remainder := NewVariable(result[1])
217	p.RangeCheck(remainder)
218	return remainder
219}
220
221// The hint used to compute Reduce.
222func ReduceHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
223	if len(inputs) != 1 {
224		panic("ReduceHint expects 1 input operand")
225	}
226	input := inputs[0]
227	quotient := new(big.Int).Div(input, MODULUS)
228	remainder := new(big.Int).Rem(input, MODULUS)
229	results[0] = quotient
230	results[1] = remainder
231	return nil
232}
233
234// Computes the inverse of a field element x such that x * x^-1 = 1.
235func (p *Chip) Inverse(x Variable) Variable {
236	result, err := p.api.Compiler().NewHint(InverseHint, 1, x.Limb)
237	if err != nil {
238		panic(err)
239	}
240
241	inverse := NewVariable(result[0])
242	p.RangeCheck(inverse)
243
244	product := p.Mul(inverse, x)
245	p.api.AssertIsEqual(product.Limb, frontend.Variable(1))
246	return inverse
247}
248
249// The hint used to compute Inverse.
250func InverseHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
251	if len(inputs) != 1 {
252		panic("InverseHint expects 1 input operand")
253	}
254
255	input := inputs[0]
256	if input.Cmp(MODULUS) == 0 || input.Cmp(MODULUS) == 1 {
257		panic("Input is not in the field")
258	}
259
260	inputGl := goldilocks.NewElement(input.Uint64())
261	resultGl := goldilocks.NewElement(0)
262	resultGl.Inverse(&inputGl)
263
264	result := big.NewInt(0)
265	results[0] = resultGl.BigInt(result)
266
267	return nil
268}
269
270// Computes a field element raised to some power.
271func (p *Chip) Exp(x Variable, k *big.Int) Variable {
272	if k.IsUint64() && k.Uint64() == 0 {
273		return One()
274	}
275
276	e := k
277	if k.Sign() == -1 {
278		panic("Unsupported negative exponent. Need to implement inversion.")
279	}
280
281	z := x
282	for i := e.BitLen() - 2; i >= 0; i-- {
283		z = p.Mul(z, z)
284		if e.Bit(i) == 1 {
285			z = p.Mul(z, x)
286		}
287	}
288
289	return z
290}
291
292// The hint used to split a GoldilocksVariable into 2 32 bit limbs.
293func SplitLimbsHint(_ *big.Int, inputs []*big.Int, results []*big.Int) error {
294	if len(inputs) != 1 {
295		panic("SplitLimbsHint expects 1 input operand")
296	}
297
298	// The Goldilocks field element
299	input := inputs[0]
300
301	if input.Cmp(MODULUS) == 0 || input.Cmp(MODULUS) == 1 {
302		return fmt.Errorf("input is not in the field")
303	}
304
305	two_32 := big.NewInt(int64(math.Pow(2, 32)))
306
307	// The most significant bits
308	results[0] = new(big.Int).Quo(input, two_32)
309	// The least significant bits
310	results[1] = new(big.Int).Rem(input, two_32)
311
312	return nil
313}
314
315// Range checks a field element x to be less than the Golidlocks modulus 2 ^ 64 - 2 ^ 32 + 1.
316func (p *Chip) RangeCheck(x Variable) {
317	// The Goldilocks' modulus is 2^64 - 2^32 + 1, which is:
318	//
319	// 		1111111111111111111111111111111100000000000000000000000000000001
320	//
321	// in big endian binary. This function will first verify that x is at most 64 bits wide. Then it
322	// checks that if the bits[0:31] (in big-endian) are all 1, then bits[32:64] are all zero.
323
324	result, err := p.api.Compiler().NewHint(SplitLimbsHint, 2, x.Limb)
325	if err != nil {
326		panic(err)
327	}
328
329	// We check that this is a valid decomposition of the Goldilock's element and range-check each limb.
330	mostSigLimb := result[0]
331	leastSigLimb := result[1]
332	p.api.AssertIsEqual(
333		p.api.Add(
334			p.api.Mul(mostSigLimb, uint64(math.Pow(2, 32))),
335			leastSigLimb,
336		),
337		x.Limb,
338	)
339	p.rangeChecker.Check(mostSigLimb, 32)
340	p.rangeChecker.Check(leastSigLimb, 32)
341
342	// If the most significant bits are all 1, then we need to check that the least significant bits are all zero
343	// in order for element to be less than the Goldilock's modulus.
344	// Otherwise, we don't need to do any checks, since we already know that the element is less than the Goldilocks modulus.
345	shouldCheck := p.api.IsZero(p.api.Sub(mostSigLimb, uint64(math.Pow(2, 32))-1))
346	p.api.AssertIsEqual(
347		p.api.Select(
348			shouldCheck,
349			leastSigLimb,
350			frontend.Variable(0),
351		),
352		frontend.Variable(0),
353	)
354}
355
356func (p *Chip) AssertIsEqual(x, y Variable) {
357	p.api.AssertIsEqual(x.Limb, y.Limb)
358}
359
360// Computes the n'th primitive root of unity for the Goldilocks field.
361func PrimitiveRootOfUnity(nLog uint64) goldilocks.Element {
362	if nLog > TWO_ADICITY {
363		panic("nLog is greater than TWO_ADICITY")
364	}
365	res := goldilocks.NewElement(POWER_OF_TWO_GENERATOR.Uint64())
366	for i := 0; i < int(TWO_ADICITY-nLog); i++ {
367		res.Square(&res)
368	}
369	return res
370}
371
372func TwoAdicSubgroup(nLog uint64) []goldilocks.Element {
373	if nLog > TWO_ADICITY {
374		panic("nLog is greater than GOLDILOCKS_TWO_ADICITY")
375	}
376
377	var res []goldilocks.Element
378	rootOfUnity := PrimitiveRootOfUnity(nLog)
379	res = append(res, goldilocks.NewElement(1))
380
381	for i := 0; i < (1 << nLog); i++ {
382		lastElement := res[len(res)-1]
383		res = append(res, *lastElement.Mul(&lastElement, &rootOfUnity))
384	}
385
386	return res
387}