Documentation ¶
Overview ¶
Package emulated implements operations over any modulus.
Non-native computation in circuit ¶
Usually, the computations in a SNARK circuit are performed in the 'native' field of the curve. The native field is defined by the scalar field of the underlying curve. This package implements non-native arithmetic on top of the native field to emulate operations in any field and ring.
This package does this by splitting the element into smaller limbs. The parameters for splitting the limb and defining the modulus are stored in types implementing FieldParams type. The elements are parametrized by those types to make compile-time distinction between different emulated fields.
This package defines Element type which stores the element value in split limbs. On top of the Element instance, this package defines typical arithmetic as addition, multiplication and subtraction. If the modulus is a prime (i.e. defines a finite field), then inversion and division operations are also possible.
The results of the operations are not always reduced to be less than the modulus. For consecutive operations it is necessary to manually reduce the value using Field.Reduce method. The number of operations which can be performed without reduction depends when the operations result starts overflowing the limbs.
Element representation ¶
We operate in the scalar field of the SNARK curve (native field). Denote the modulus of the native field as 'q'. Representing the modulus of the native field requires 'n' bits. We wish to emulate operations over modulus 'r'. Modulus r may or may not be a prime. If r is not prime, then we do not have inversion and division operations (the corresponding methods panic). Let the bitlength of r be 'm'. We note that r may be smaller, larger or equal to q.
To represent an element x ∈ N_r, we choose the limb width 'w' such that
w ≤ (m-1)/2
and write its integer representation as
x = ∑_{i=0}^k x_i 2^{w i}.
Here, the variable 'x_i' is the w bits of x starting from 2^{w i}, 'k' is the number of limbs and is computed as
k = (n+w-1)/w, // NB! integer division
and 'i' is the limb index. In this representation the element is represented in little-endian (least significant limbs first) order. We do not necessarily require that the limb values x_i are less than 2^w. This may happen if the limb values are obtained as a result of arithmetic operations between elements. If we know that the limb values do not overflow 2^w, then we say that the element is in normal form.
In the implementation, we have two functions for splitting an element into limbs and composing an element from limbs -- [decompose] and [recompose]. The [recompose] function also accepts element in non-normal form.
Elements in non-normal form ¶
When an element is initialized, the limbs are in normal form, i.e. the values of the limbs have bitwidth strictly less than w. As addition and multiplication are performed on limbs natively, then the bitwidths of the limbs of the result may be larger than w. We track the number of bits which may exceed the initial width of the limbs. We denote the number of such excess bits as 'f' and call it overflow. The total maximal bitwidth of the limbs is then
w+f.
Keep in mind that parameter w is global for all emulated elements and f is individual for every individual element.
To compute the overflow for the operations, we consider the arithmetic operations which affect the overflow. In this implementation only addition is done natively (limb-wise addition). When adding two elements, the bitwidth of the result is up to one bit wider than the width of the widest element.
In the context of overflows, if the overflows of the addends are f_0 and f_1 then the overflow value f' for the sum is computed as
f' = max(f_0, f_1)+1.
Multiplication ¶
The complexity of native limb-wise multiplication is k^2. This translates directly to the complexity in the number of constraints in the constraint system. However, alternatively, when instead computing the limb values off-circuit and constructing a system of k linear equations, we can ensure that the product was computed correctly.
Let the factors be
x = ∑_{i=0}^k x_i 2^{w i}
and
y = ∑_{i=0}^k y_i 2^{w i}.
For computing the product, we compute off-circuit the limbs
z_i = ∑_{j, j'>0, j+j'=i, j+j'≤2k-2} x_{j} y_{j'}, // in MultiplicationHint()
and assert in-circuit
∑_{i=0}^{2k-2} z_i c^i = (∑_{i=0}^k x_i) (∑_{i=0}^k y_i), ∀ c ∈ {1, ..., 2k-1}.
Computing the overflow for the multiplication result is slightly more complicated. The overflow for
x_{j} y_{j'}
is
w+f+f'+1.
Naively, as the limbs of the result are summed over all 0 ≤ i ≤ 2k-2, then the overflow of the limbs should be
w+f+f'+2k-1.
For computing the number of bits and thus in the overflow, we can instead look at the maximal possible value. This can be computed by
(2^{2w+f+f'+2}-1)*(2k-1).
Its bitlength is
2w+f+f'+1+log_2(2k-1),
which leads to maximal overflow of
w+f+f'+1+log_2(2k-1).
Subtraction ¶
We perform subtraction limb-wise between the elements x and y. However, we have to ensure than any limb in the result does not result in overflow, i.e.
x_i ≥ y_i, ∀ 0≤i<k.
As this does not hold in general, then we need to pad x such that every limb x_i is strictly larger than y_i.
The additional padding 'u' has to be divisible by the emulated modulus r and every limb u_i must be larger than x_i-y_i. Let f' be the overflow of y. We first compute the limbs u'_i as
u'_i = 1 << (w+f'), ∀ 0≤i<k.
Now, as u' is not divisible by r, we need to compensate for it:
u'' = u' + regroup(r - (u' % r)),
where regroup() regroups the argument so that it is in normal form (i.e. first applies recompose() and then decompose() method).
We see that u” is now such that it is divisible by r and its every limb is larger than every limb of b. The subtraction is performed as
z_i = x_i + u''_i - y_i, ∀ 0≤i<k.
Equality checking ¶
The package provides two ways to check equality -- limb-wise equality check and checking equality by value.
In the limb-wise equality check we check that the integer values of the elements x and y are equal. We have to carry the excess using bit decomposition (which makes the computation fairly inefficient). To reduce the number of bit decompositions, we instead carry over the excess of the difference of the limbs instead. As we take the difference, then similarly as computing the padding in subtraction algorithm, we need to add padding to the limbs before subtracting limb-wise to avoid underflows. However, the padding in this case is slightly different -- we do not need the padding to be divisible by the modulus, but instead need that the limb padding is larger than the limb which is being subtracted.
Lets look at the algorithm itself. We assume that the overflow f of x is larger than y. If overflow of y is larger, then we can just swap the arguments and apply the same argumentation. Let
maxValue = 1 << (k+f), // padding for limbs maxValueShift = 1 << f. // carry part of the padding
For every limb we compute the difference as
diff_0 = maxValue+x_0-y_0, diff_i = maxValue+carry_i+x_i-y_i-maxValueShift.
We check that the normal part of the difference is zero and carry the rest over to next limb:
diff_i[0:k] == 0, carry_{i+1} = diff_i[k:k+f+1] // we also carry over the padding bit.
Finally, after we have compared all the limbs, we still need to check that the final carry corresponds to the padding. We add final check:
carry_k == maxValueShift.
We can further optimise the limb-wise equality check by first regrouping the limbs. The idea is to group several limbs so that the result would still fit into the scalar field. If
x = ∑_{i=0}^k x_i 2^{w i},
then we can instead take w' divisible by w such that
x = ∑_{i=0}^(k/(w'/w)) x'_i 2^{w' i},
where
x'_j = ∑_{i=0}^(w'/w) x_{j*w'/w+i} 2^{w i}.
For element value equality check, we check that two elements x and y are equal modulo r and for that we need to show that r divides x-y. As mentioned in the subtraction section, we add sufficient padding such that x-y does not underflow and its integer value is always larger than 0. We use hint function to compute z such that
x-y = z*r,
compute z*r and use limbwise equality checking to show that
x-y == z*r.
Bitwidth enforcement ¶
When element is computed using hints, we need to ensure that every limb is not wider than k bits. For that, we perform bitwise decomposition of every limb and check that k lower bits are equal to the whole limb. We omit the bitwidth enforcement for multiplication as the correctness of the limbs is ensured using the corresponding system of linear equations.
Additionally, we apply bitwidth enforcement for elements initialized from integers.
Modular reduction ¶
To reduce the integer value of element x to be less than the modulus, we compute the remainder x' of x modulo r using hint, enforce the bitwidth of x' and assert that
x' == x
using element equality checking.
Values computed using hints ¶
We additionally define functions for computing inverse of an element and ratio of two elements. Both function compute the actual value using hint and then assert the correctness of the operation using multiplication.
Constant values ¶
The package currently does not explicitly differentiate between constant and variable elements. The builder may track some elements as being constants. Some operations have a fast track path for cases when all inputs are constants. There is Field.MulConst, which provides variable by constant multiplication.
Index ¶
- func DivHint(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error
- func GetHints() []hint.Function
- func InverseHint(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error
- func MultiplicationHint(mod *big.Int, inputs []*big.Int, outputs []*big.Int) error
- func NBitsShifted(_ *big.Int, inputs []*big.Int, results []*big.Int) error
- func QuoHint(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error
- func RemHint(_ *big.Int, inputs []*big.Int, outputs []*big.Int) error
- type BLS12377Fp
- type BN254Fp
- type BN254Fr
- type Element
- type Field
- func (f *Field[T]) Add(a, b *Element[T]) *Element[T]
- func (f *Field[T]) AssertIsEqual(a, b *Element[T])
- func (f *Field[T]) AssertIsLessOrEqual(e, a *Element[T])
- func (f *Field[T]) AssertLimbsEquality(a, b *Element[T])
- func (f *Field[T]) Div(a, b *Element[T]) *Element[T]
- func (f *Field[T]) FromBits(bs ...frontend.Variable) *Element[T]
- func (f *Field[T]) Inverse(a *Element[T]) *Element[T]
- func (f *Field[T]) Lookup2(b0, b1 frontend.Variable, a, b, c, d *Element[T]) *Element[T]
- func (f *Field[T]) Modulus() *Element[T]
- func (f *Field[T]) Mul(a, b *Element[T]) *Element[T]
- func (f *Field[T]) MulConst(a *Element[T], c *big.Int) *Element[T]
- func (f *Field[T]) MulMod(a, b *Element[T]) *Element[T]
- func (f *Field[T]) Neg(a *Element[T]) *Element[T]
- func (f *Field[T]) NewElement(v interface{}) *Element[T]
- func (f *Field[T]) One() *Element[T]
- func (f *Field[T]) Reduce(a *Element[T]) *Element[T]
- func (f *Field[T]) Select(selector frontend.Variable, a, b *Element[T]) *Element[T]
- func (f *Field[T]) Sub(a, b *Element[T]) *Element[T]
- func (f *Field[T]) ToBits(a *Element[T]) []frontend.Variable
- func (f *Field[T]) Zero() *Element[T]
- type FieldParams
- type Goldilocks
- type Secp256k1Fp
- type Secp256k1Fr
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func InverseHint ¶
InverseHint computes the inverse x^-1 for the input x and stores it in outputs.
func MultiplicationHint ¶
MultiplicationHint unpacks the factors and parameters from inputs, computes the product and stores it in output. See internal method computeMultiplicationHint for the input packing.
func NBitsShifted ¶
NBitsShifted returns the first bits of the input, with a shift. The number of returned bits is defined by the length of the results slice.
Types ¶
type BLS12377Fp ¶
type BLS12377Fp struct{}
BLS12377Fp provide type parametrization for emulated field on 6 limb of width 64bits for modulus 0x1ae3a4617c510eac63b05c06ca1493b1a22d9f300f5138f1ef3622fba094800170b5d44300000008508c00000000001. This is the base field of the BLS12-377 curve.
func (BLS12377Fp) BitsPerLimb ¶
func (fp BLS12377Fp) BitsPerLimb() uint
func (BLS12377Fp) IsPrime ¶
func (fp BLS12377Fp) IsPrime() bool
func (BLS12377Fp) Modulus ¶
func (fp BLS12377Fp) Modulus() *big.Int
func (BLS12377Fp) NbLimbs ¶
func (fp BLS12377Fp) NbLimbs() uint
type BN254Fp ¶
type BN254Fp struct{}
BN254Fp provide type parametrization for emulated field on 4 limb of width 64bits for modulus 0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47. This is the base field of the BN254 curve.
func (BN254Fp) BitsPerLimb ¶
type BN254Fr ¶
type BN254Fr struct{}
BN254Fr provides type parametrisation for emulated field on 4 limbs of width 64bits for modulus 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001. This is the scalar field of the BN254 curve.
func (BN254Fr) BitsPerLimb ¶
type Element ¶
type Element[T FieldParams] struct { // Limbs is the decomposition of the integer value into limbs in the native // field. To enforce that the limbs are of expected width, use Pack... // methods on the Field. Uses little-endian (least significant limb first) // encoding. Limbs []frontend.Variable // contains filtered or unexported fields }
Element defines an element in the ring of integers modulo n. The integer value of the element is split into limbs of nbBits lengths and represented as a slice of limbs. The type parameter defines the field this element belongs to.
func ValueOf ¶
func ValueOf[T FieldParams](constant interface{}) Element[T]
ValueOf returns an Element[T] from a constant value. The input is converted to *big.Int and decomposed into limbs and packed into new Element[T].
func (*Element[T]) GnarkInitHook ¶
func (e *Element[T]) GnarkInitHook()
GnarkInitHook describes how to initialise the element.
type Field ¶
type Field[T FieldParams] struct { // contains filtered or unexported fields }
Field holds the configuration for non-native field operations. The field parameters (modulus, number of limbs) is given by FieldParams type parameter. If [FieldParams.IsPrime] is true, then allows inverse and division operations.
Example ¶
Example of using Field instance. The witness elements must be Element type.
package main import ( "fmt" "github.com/BeratOz01/gnark/backend" "github.com/BeratOz01/gnark/backend/groth16" "github.com/BeratOz01/gnark/frontend" "github.com/BeratOz01/gnark/frontend/cs/r1cs" "github.com/BeratOz01/gnark/std/math/emulated" "github.com/consensys/gnark-crypto/ecc" ) type ExampleFieldCircuit[T emulated.FieldParams] struct { In1 emulated.Element[T] In2 emulated.Element[T] Res emulated.Element[T] } func (c *ExampleFieldCircuit[T]) Define(api frontend.API) error { f, err := emulated.NewField[T](api) if err != nil { return fmt.Errorf("new field: %w", err) } res := f.Mul(&c.In1, &c.In2) // non-reducing res = f.Reduce(res) f.AssertIsEqual(res, &c.Res) return nil } // Example of using [Field] instance. The witness elements must be [Element] // type. func main() { circuit := ExampleFieldCircuit[emulated.BN254Fp]{} witness := ExampleFieldCircuit[emulated.BN254Fp]{ In1: emulated.ValueOf[emulated.BN254Fp](3), In2: emulated.ValueOf[emulated.BN254Fp](5), Res: emulated.ValueOf[emulated.BN254Fp](15), } ccs, err := frontend.Compile(ecc.BN254.ScalarField(), r1cs.NewBuilder, &circuit) if err != nil { panic(err) } else { fmt.Println("compiled") } witnessData, err := frontend.NewWitness(&witness, ecc.BN254.ScalarField()) if err != nil { panic(err) } else { fmt.Println("secret witness parsed") } publicWitnessData, err := witnessData.Public() if err != nil { panic(err) } else { fmt.Println("public witness parsed") } pk, vk, err := groth16.Setup(ccs) if err != nil { panic(err) } else { fmt.Println("setup done") } proof, err := groth16.Prove(ccs, pk, witnessData, backend.WithHints(emulated.GetHints()...)) if err != nil { panic(err) } else { fmt.Println("proved") } err = groth16.Verify(proof, vk, publicWitnessData) if err != nil { panic(err) } else { fmt.Println("verified") } }
Output: compiled secret witness parsed public witness parsed setup done proved verified
func NewField ¶
func NewField[T FieldParams](native frontend.API) (*Field[T], error)
NewField returns an object to be used in-circuit to perform emulated arithmetic over the field defined by type parameter FieldParams. The operations on this type are defined on Element. There is also another type [FieldAPI] implementing frontend.API which can be used in place of native API for existing circuits.
This is an experimental feature and performing emulated arithmetic in-circuit is extremly costly. See package doc for more info.
func (*Field[T]) Add ¶
Add computes a+b and returns it. If the result wouldn't fit into Element, then first reduces the inputs (larger first) and tries again. Doesn't mutate inputs.
func (*Field[T]) AssertIsEqual ¶
AssertIsEqual ensures that a is equal to b modulo the modulus.
func (*Field[T]) AssertIsLessOrEqual ¶
AssertIsLessOrEqual ensures that e is less or equal than a.
func (*Field[T]) AssertLimbsEquality ¶
AssertLimbsEquality asserts that the limbs represent a same integer value. This method does not ensure that the values are equal modulo the field order. For strict equality, use AssertIsEqual.
func (*Field[T]) Inverse ¶
Inverse compute 1/a and returns it. It uses InverseHint.
func (*Field[T]) Lookup2 ¶
Lookup2 performs two-bit lookup between a, b, c, d based on lookup bits b1 and b2 such that:
- if b0=0 and b1=0, sets to a,
- if b0=1 and b1=0, sets to b,
- if b0=0 and b1=1, sets to c,
- if b0=1 and b1=1, sets to d.
The number of the limbs and overflow in the result is the maximum of the inputs'. If the inputs are very unbalanced, then reduce the result.
func (*Field[T]) Mul ¶
Mul computes a*b and returns it. It doesn't reduce the output and it may be larger than the modulus. The returned Element has as many limbs as the inputs together. If the result wouldn't fit into Element, then locally reduces the inputs first. Doesn't mutate inputs.
Even though this method skips reduction and allows for multiplication chains, then in most cases it is more efficient to use [Field[T].MulMod] as reducing Element with 2 times the limbs is 2 times more expensive.
For multiplying by a constant, use [Field[T].MulConst] method which is more efficient.
Uses MultiplicationHint.
func (*Field[T]) MulConst ¶
MulConst multiplies a by a constant c and returns it. We assume that the input constant is "small", so that we can compute the product by multiplying all individual limbs with the constant. If it is not small, then use the general [Field[T].Mul] or [Field[T].MulMod] with creating new Element from the constant on-the-fly.
func (*Field[T]) MulMod ¶
Mul computes a*b and reduces it modulo the field order. The returned Element has default number of limbs and zero overflow.
func (*Field[T]) NewElement ¶
NewElement builds a new Element[T] from input v.
- if v is a Element[T] or *Element[T] it clones it
- if v is a constant this is equivalent to calling emulated.ValueOf[T]
- if this methods interpret v (frontend.Variable or []frontend.Variable) as being the limbs; and constrain the limbs following the parameters of the Field.
func (*Field[T]) Reduce ¶
Reduce reduces a modulo the field order and returns it. Uses hint RemHint.
func (*Field[T]) Select ¶
Select sets e to a if selector == 0 and to b otherwise. Sets the number of limbs and overflow of the result to be the maximum of the limb lengths and overflows. If the inputs are strongly unbalanced, then it would better to reduce the result after the operation.
func (*Field[T]) Sub ¶
Sub subtracts b from a and returns it. Reduces locally if wouldn't fit into Element. Doesn't mutate inputs.
func (*Field[T]) ToBits ¶
ToBits returns the bit representation of the Element in little-endian (LSB first) order. The returned bits are constrained to be 0-1. The number of returned bits is nbLimbs*nbBits+overflow. To obtain the bits of the canonical representation of Element, reduce Element first and take less significant bits corresponding to the bitwidth of the emulated modulus.
type FieldParams ¶
type FieldParams interface { NbLimbs() uint // number of limbs to represent field element BitsPerLimb() uint // number of bits per limb. Top limb may contain less than limbSize bits. IsPrime() bool // indicates if the modulus is prime Modulus() *big.Int // returns modulus. Do not modify. }
FieldParams describes the emulated field characteristics
type Goldilocks ¶
type Goldilocks struct{}
Goldilocks provide type parametrization for emulated field on 1 limb of width 64bits for modulus 0xffffffff00000001
func (Goldilocks) BitsPerLimb ¶
func (fp Goldilocks) BitsPerLimb() uint
func (Goldilocks) IsPrime ¶
func (fp Goldilocks) IsPrime() bool
func (Goldilocks) Modulus ¶
func (fp Goldilocks) Modulus() *big.Int
func (Goldilocks) NbLimbs ¶
func (fp Goldilocks) NbLimbs() uint
type Secp256k1Fp ¶
type Secp256k1Fp struct{}
Secp256k1Fp provide type parametrization for emulated field on 4 limb of width 64bits for modulus 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f. This is the base field of secp256k1 curve
func (Secp256k1Fp) BitsPerLimb ¶
func (fp Secp256k1Fp) BitsPerLimb() uint
func (Secp256k1Fp) IsPrime ¶
func (fp Secp256k1Fp) IsPrime() bool
func (Secp256k1Fp) Modulus ¶
func (fp Secp256k1Fp) Modulus() *big.Int
func (Secp256k1Fp) NbLimbs ¶
func (fp Secp256k1Fp) NbLimbs() uint
type Secp256k1Fr ¶
type Secp256k1Fr struct{}
Secp256k1Fr provides type parametrization for emulated field on 4 limbs of width 64bits for modulus 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141. This is the scalar field of secp256k1 curve.
func (Secp256k1Fr) BitsPerLimb ¶
func (fp Secp256k1Fr) BitsPerLimb() uint
func (Secp256k1Fr) IsPrime ¶
func (fp Secp256k1Fr) IsPrime() bool
func (Secp256k1Fr) Modulus ¶
func (fp Secp256k1Fr) Modulus() *big.Int
func (Secp256k1Fr) NbLimbs ¶
func (fp Secp256k1Fr) NbLimbs() uint