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