Emulated BW6-761 pairing

[ivokub]

This discussion is a continuation of the thread in #395.

@SherLzp, I have some code which helps debugging pairing implementation in-circuit. First, to use the debug code, you need to use the test engine (instead of compiling the circuit and solving it).

First, add the following functions (in field emulation std/math/emulated/debug.go):

func (f *Field[T]) String(a *Element[T]) (string, error) {
       // for debug only, if is not test engine then no-op
       var fp T
       blimbs := make([]*big.Int, len(a.Limbs))
       for i, v := range a.Limbs {
               switch vv := v.(type) {
               case *big.Int:
                       blimbs[i] = vv
               case big.Int:
                       blimbs[i] = &vv
               case int:
                       blimbs[i] = new(big.Int)
                       blimbs[i].SetInt64(int64(vv))
               case uint:
                       blimbs[i] = new(big.Int)
                       blimbs[i].SetUint64(uint64(vv))
               default:
                       return "", fmt.Errorf("not big int")
               }
       }
       res := new(big.Int)
       err := recompose(blimbs, fp.BitsPerLimb(), res)
       if err != nil {
               return "", fmt.Errorf("recompose: %w", err)
       }
       reduced := new(big.Int).Mod(res, fp.Modulus())
       return reduced.String(), nil
}

and (in std/algebra/pairing_bn254/debug.go):

func (e ext2) String(x *E2) string {
       x0, err := e.fp.String(&x.A0)
       if err != nil {
               x0 = "?"
       }
       x1, err := e.fp.String(&x.A1)
       if err != nil {
               x1 = "?"
       }
       return fmt.Sprintf("%s+%s*u", x0, x1)
}

func (e ext6) String(x *E6) string {
       return fmt.Sprintf("%s+(%s)*v+(%s)*v**2", e.ext2.String(&x.B0), e.ext2.String(&x.B1), e.ext2.String(&x.B2))
}

func (e ext12) String(x *E12) string {
       return fmt.Sprintf("%s+(%s)*w", e.ext6.String(&x.C0), e.ext6.String(&x.C1))
}

Now, you can print out the intermediate values by calling fmt.Println(pairing.ext12(gtEl)) in-circuit. The output corresponds to the output with calling .String() methods on field elements in gnark-crypto.

[SherLzp]

Hi Sir @ivokub , thanks for your comment, right now I can print out the data.

I already changed every Mul to MulMod and put every operation under e.fp. However, when I want to make a test for Expt, it still comes to the following error at this line: https://github.com/SherLzp/gnark/blob/develop/std/algebra/pairing_bw6761/e6_pairing.go#L58

 e6_pairing_test.go:60: 
        	Error Trace:	D:\Projects\mygo\src\Zecrey\SherLzp\gnark\std\algebra\pairing_bw6761\e6_pairing_test.go:60
        	Error:      	Received unexpected error:
        	            	[assertIsEqual] 45103312938095893 == 477448877165663509
        	            	bits.toBinary
        	            		conversion_binary.go:93
        	            	bits.ToBase
        	            		conversion.go:25
        	            	bits.ToBinary
        	            		conversion_binary.go:18
        	            	emulated.(*Field[...]).EnforceWidth
        	            		field_assert.go:135
        	            	emulated.(*Field[...]).PackLimbs
        	            		field.go:114
        	            	emulated.(*Field[...]).computeQuoHint
        	            		hints.go:141
        	            	emulated.(*Field[...]).AssertIsEqual
        	            		field_assert.go:158
        	            	emulated.(*Field[...]).Reduce
        	            		field_ops.go:226
        	            	pairing_bw6761.ext3.Set
        	            		e3.go:347
        	            	pairing_bw6761.ext6.Set
        	            		e6.go:360
        	            	pairing_bw6761.ext6.CyclotomicSquareCompressed
        	            		e6.go:127
        	            	pairing_bw6761.ext6.nSquareCompressed
        	            		e6_pairing.go:33
        	            	pairing_bw6761.ext6.Expt
        	            		e6_pairing.go:58
        	            	pairing_bw6761.(*e6Expt).Define
        	            		e6_pairing_test.go:41
        	Test:       	TestExptFp6
--- FAIL: TestExptFp6 (1.28s)

I check every operation in gnark-crypto and it seems no problem. In addition, I already make tests for each operation in Expt and everyhing is ok. Do you have any ideas about what happended here?

[SherLzp]

Hi sir, @ivokub , I think I finally found the problem. Could you tell me why these two methods will give different results?

z := fp.Add(x, x)
z = fp.Add(z, z)
z = fp.Neg(z)

nonResidue := emulated.NewElement[emulated.BW6761Fp](-4)
z := fp.Mul(x, &nonResidue)

[SherLzp]

Yes, it does reduce the constraints, but leads to the circuit being under-constrained. The method Reduce(a) computes b such that b = a mod p, but this computation is done using hints, where the prover provides the actual value to b during proving time, and then we assert that exists any k such that b + k*p = a (as integers). If we omit this line, then prover can essentially provide any b and we do not enforce that this reduction was correct.

So, this check definitely has to be there :) The equality assertion is expensive because as the limbs may have different overflows, we have to binary decompose all limbs and then check bit-by-bit, carrying over any overflow. We are looking into way to optimize this equality assertion using table lookups, but it is currently work-in-progress. It is quite high priority right now, because as you said, field emulation is quite costly still.

Got it. If I don't comment it, for BW6-761 pairing operation, especially nSquareCompressed in FinalExponentiation: https://github.com/SherLzp/gnark/blob/develop/std/algebra/pairing_bw6761/e6_pairing.go#L30
It will have the following error:

    pairing_test.go:130: 
        	Error Trace:	D:\Projects\mygo\src\Zecrey\SherLzp\gnark\std\algebra\pairing_bw6761\pairing_test.go:130
        	Error:      	Received unexpected error:
        	            	[assertIsEqual] 74313501244881661 == 1803695758155152125
        	            	bits.toBinary
        	            		conversion_binary.go:93
        	            	bits.ToBase
        	            		conversion.go:25
        	            	bits.ToBinary
        	            		conversion_binary.go:18
        	            	emulated.(*Field[...]).EnforceWidth
        	            		field_assert.go:135

        	            	emulated.(*Field[...]).PackLimbs
        	            		field.go:114
        	            	emulated.(*Field[...]).computeQuoHint
        	            		hints.go:141
        	            	emulated.(*Field[...]).AssertIsEqual
        	            		field_assert.go:160

        	            	emulated.(*Field[...]).Reduce
        	            		field_ops.go:226
        	            	emulated.(*Field[...]).reduceAndOp
        	            		field_ops.go:352
        	            	emulated.(*Field[...]).Mul
        	            		field_ops.go:104
        	            	emulated.(*Field[...]).MulMod
        	            		field_ops.go:110
        	            	pairing_bw6761.ext6.CyclotomicSquareCompressed
        	            		e6.go:131
        	            	pairing_bw6761.ext6.nSquareCompressed
        	            		e6_pairing.go:30
        	            	pairing_bw6761.ext6.Expt
        	            		e6_pairing.go:55
        	            	pairing_bw6761.Pairing.FinalExponentiation
        	            		pairing.go:101
        	            	pairing_bw6761.(*finalExponentiationBW6761).Define
        	            		pairing_test.go:93
        	Test:       	TestFinalExponentiationBW6761

[SherLzp]

Yes, it does reduce the constraints, but leads to the circuit being under-constrained. The method Reduce(a) computes b such that b = a mod p, but this computation is done using hints, where the prover provides the actual value to b during proving time, and then we assert that exists any k such that b + k*p = a (as integers). If we omit this line, then prover can essentially provide any b and we do not enforce that this reduction was correct.

So, this check definitely has to be there :) The equality assertion is expensive because as the limbs may have different overflows, we have to binary decompose all limbs and then check bit-by-bit, carrying over any overflow. We are looking into way to optimize this equality assertion using table lookups, but it is currently work-in-progress. It is quite high priority right now, because as you said, field emulation is quite costly still.

Sir, I remember you have mentioned about non-amortized reductions. How that works?

[ivokub]

Instead of doing fp.MulMod, you can do fp.Mul. Then the output of multiplication is not reduced modulo the emulated modulus.

[ivokub]

And for correctness:

• amortized reductions - we do not reduce by the modulus after very multiplication
• non-amortized - we do reduce.

[SherLzp]

What input for x causes the error? If I do:

type testCircuit struct {
	X emulated.Element[emulated.BW6761Fp]
}

func (c *testCircuit) Define(api frontend.API) error {
	F, err := emulated.NewField[emulated.BW6761Fp](api)
	if err != nil {
		return err
	}
	nonResidue := emulated.NewElement[emulated.BW6761Fp](-4)
	A := F.Mul(&c.X, &nonResidue)
	B := F.Add(&c.X, &c.X)
	B = F.Add(B, B)
	B = F.Neg(B)
	F.AssertIsEqual(A, B)
	return nil
}

func TestTestCircuit(t *testing.T) {
	assert := test.NewAssert(t)
	var x fp.Element // import fp  "github.com/consensys/gnark-crypto/ecc/bw6-761/fp"
	x.SetRandom()
	circuit := &testCircuit{}
	witness := &testCircuit{
		X: emulated.NewElement[emulated.BW6761Fp](x),
	}
	err := test.IsSolved(circuit, witness, testCurve.ScalarField())
	assert.NoError(err)
}

then I don't get error.

Yes, that's the strange thing. When I make unit tests, everything is ok. But when I want to do MillerLoop, it will have the problem. I think the test cannot fully describe it, because NewElement will always give the correct result.

Here is the test process: I run the test here: https://github.com/SherLzp/gnark/blob/develop/std/algebra/pairing_bw6761/pairing_test.go#L54 It will fail now. But when I change the method here: https://github.com/SherLzp/gnark/blob/develop/std/algebra/pairing_bw6761/pairing_test.go#L54 from:

z := fp.Add(x, x)
z = fp.Add(z, z)
z = fp.Neg(z)

to:

nonResidue := emulated.NewElement[emulated.BW6761Fp](-4)
z := fp.Mul(x, &nonResidue)

It will succeed.

And I finally find the difference is here: https://github.com/SherLzp/gnark/blob/develop/std/algebra/pairing_bw6761/e6.go#L109

But as mentioned before, this problem still exists.

[SherLzp]

And when I change the method to the following, sometimes it will give the same result:

z := fp.Neg(z)
z = fp.Add(z, z)
z = fp.Add(z, z)

[ivokub]

You can try this fix:

diff --git a/std/math/emulated/field_assert.go b/std/math/emulated/field_assert.go
index e068f11a..1bdcbbc4 100644
--- a/std/math/emulated/field_assert.go
+++ b/std/math/emulated/field_assert.go
@@ -125,10 +125,10 @@ func (f *Field[T]) EnforceWidth(a *Element[T]) {
                // TODO @gbotrel why check all the limbs here? if len(e.Limbs) <= modulus
                // && last limb <= bits[lastLimbs] modulus, we're good ?
                limbNbBits := int(f.fParams.BitsPerLimb())
-               if i == len(a.Limbs)-1 {
-                       // take only required bits from the most significant limb
-                       limbNbBits = ((f.fParams.Modulus().BitLen() - 1) % int(f.fParams.BitsPerLimb())) + 1
-               }
+               // if i == len(a.Limbs)-1 {
+               //      // take only required bits from the most significant limb
+               //      limbNbBits = ((f.fParams.Modulus().BitLen() - 1) % int(f.fParams.BitsPerLimb())) + 1
+               // }
                // bits.ToBinary restricts the least significant NbDigits to be equal to
                // the limb value. This is sufficient to restrict for the bitlength and
                // we can discard the bits themselves.

So when enforcing the widths of the limbs, I had assumed that I only enforce for the cases when the integer value is smaller than modulus. But actually for the coefficient k as mentioned previously may be larger than p due to the subtraction padding.

I will implement a proper fix later to separate between two cases (to save a few constraints), but I think that for now this should work for you and should be sound.

Now there is another error, but I think this is due to some other problem. Maybe you can spot it. But if it seems to be a problem in field emulation, then can have a look.

[SherLzp]

You can try this fix:

diff --git a/std/math/emulated/field_assert.go b/std/math/emulated/field_assert.go
index e068f11a..1bdcbbc4 100644
--- a/std/math/emulated/field_assert.go
+++ b/std/math/emulated/field_assert.go
@@ -125,10 +125,10 @@ func (f *Field[T]) EnforceWidth(a *Element[T]) {
                // TODO @gbotrel why check all the limbs here? if len(e.Limbs) <= modulus
                // && last limb <= bits[lastLimbs] modulus, we're good ?
                limbNbBits := int(f.fParams.BitsPerLimb())
-               if i == len(a.Limbs)-1 {
-                       // take only required bits from the most significant limb
-                       limbNbBits = ((f.fParams.Modulus().BitLen() - 1) % int(f.fParams.BitsPerLimb())) + 1
-               }
+               // if i == len(a.Limbs)-1 {
+               //      // take only required bits from the most significant limb
+               //      limbNbBits = ((f.fParams.Modulus().BitLen() - 1) % int(f.fParams.BitsPerLimb())) + 1
+               // }
                // bits.ToBinary restricts the least significant NbDigits to be equal to
                // the limb value. This is sufficient to restrict for the bitlength and
                // we can discard the bits themselves.

So when enforcing the widths of the limbs, I had assumed that I only enforce for the cases when the integer value is smaller than modulus. But actually for the coefficient k as mentioned previously may be larger than p due to the subtraction padding.

I will implement a proper fix later to separate between two cases (to save a few constraints), but I think that for now this should work for you and should be sound.

Now there is another error, but I think this is due to some other problem. Maybe you can spot it. But if it seems to be a problem in field emulation, then can have a look.

It works. Thanks sir.

[SherLzp]

Hi sir @ivokub ,

what's the usage of this method? Is that required?

https://github.com/ConsenSys/gnark/blob/develop/std/math/emulated/field.go#L114

[ivokub]

But I'm trying an idea using lookups which could reduce the constraint count a lot.

[SherLzp]

@ivokub That's amazing. Sir, do you have the estimated date for lookups implementation?

[ivokub]

I have tried range checks using lookups in pairings and ECDSA verification and for Groth16 it is about 4x-5x reduction in the constraint count. For plonk it is more difficult and I don't have an implementation yet.

That said, it is still a prototype and difficult to use correctly (we amortise range checks and it means have to finalise them somewhere but due to composability is difficult). I'm starting to work on this again next week and will be expecting to have some initial results by March. But this would be first-version-initial-implementation and subject to rewrites and polishing.

[ivokub]

@ivokub That's amazing. Sir, do you have the estimated date for lookups implementation?

@SherLzp - first draft PR available at #472. I think you can start trying to use it. Right now we only support Groth16, but in general know how to implement also for PLONK. But for PLONK if we have custom gates, then becomes a lot more efficient. Any feedback / bugreports greatly appreciated.

[SherLzp]

Thanks sir.