BN254 Pairing issue

[hussein-aitlahcen]

I upgraded our circuit from 9f74ad791b8c to latest develop branch commit and the BN254 pairing check is no longer working. I'm not sure whether it is related to the optimization made in this branch but the aggregation + pairing check is working on the previously mentioned commit.

[ivokub]

Does it also fail with https://github.com/ConsenSys/gnark/pull/603?

[hussein-aitlahcen]

Does it also fail with #603?

Yes. I can confirm the last working commit is a4d7b88d6a7d970f35cb95ba245b31fbfa4c6a36 from #566, looks like it's no longer working since #594

[ivokub]

Hmm. Unit tests are not failing (full Pairing and full multipairing). Aren't you by any chance doing only MillerLoop? It isn't 1-to-1 with the implementation in gnark-crypto anymore, but the FinalExponetiation cancels out the difference.

Can you post a minimal failing unit test for debugging?

[hussein-aitlahcen]

Hmm. Unit tests are not failing (full Pairing and full multipairing). Aren't you by any chance doing only MillerLoop? It isn't 1-to-1 with the implementation in gnark-crypto anymore, but the FinalExponetiation cancels out the difference.

Can you post a minimal failing unit test for debugging?

I'm using the Pair function and checking against 1GT:

    // Pairing check
    pairing, err := gadget.NewPairing(api)
    if err != nil {
        return fmt.Errorf("new pairing: %w", err)
    }

    var g1AffGenNeg curve.G1Affine
    g1AffGenNeg.Neg(&g1AffGen)
    negG1 := gadget.NewG1Affine(g1AffGenNeg)
    e, err := pairing.Pair([]*gadget.G1Affine{&negG1, &aggregatedPublicKey}, []*gadget.G2Affine{&circuit.Sig, &hm})
    if err != nil {
        return fmt.Errorf("pair: %w", err)
    }

    var oneN curve.GT
    oneN.SetOne()
    one := gadget.NewGTEl(oneN)

    pairing.AssertIsEqual(e, &one)

The public key aggregation is done in-circuit, I'm trying to extract a failing example. Note that the out of circuit pairing is working with the out of circuit aggregation.

[ivokub]

Great! Will wait for the case. It may be some edge case.

Pinging in @yelhousni.

[hussein-aitlahcen]

Alright, the following circuit is not passing on latest develop 8f89251cb228450b1cecfb4ac0d6418053e51d17, but working on a4d7b88d6a7d970f35cb95ba245b31fbfa4c6a36:

package main

import (
    "crypto/rand"
    "fmt"
    "math/big"
    "testing"

    "github.com/consensys/gnark-crypto/ecc"
    curve "github.com/consensys/gnark-crypto/ecc/bn254"
    "github.com/consensys/gnark/backend"
    "github.com/consensys/gnark/frontend"
    "github.com/consensys/gnark/test"

    gadget "github.com/consensys/gnark/std/algebra/emulated/sw_bn254"
)

type testCircuit struct {
        PK gadget.G1Affine
    Sig gadget.G2Affine
    HM gadget.G2Affine
}

func (c *testCircuit) Define(api frontend.API) error {
    pairing, err := gadget.NewPairing(api)
    if err != nil {
        return fmt.Errorf("new pairing: %w", err)
    }

    _, _, g1AffGen, _ := curve.Generators()
    var g1AffGenNeg curve.G1Affine
    g1AffGenNeg.Neg(&g1AffGen)
    negG1 := gadget.NewG1Affine(g1AffGenNeg)
    e, err := pairing.Pair([]*gadget.G1Affine{&negG1, &c.PK}, []*gadget.G2Affine{&c.Sig, &c.HM})
    if err != nil {
        return fmt.Errorf("pair: %w", err)
    }

    var oneN curve.GT
    oneN.SetOne()
    one := gadget.NewGTEl(oneN)

    pairing.AssertIsEqual(e, &one)

    return nil
}

func TestTest(t *testing.T) {
    genPriv := func() *big.Int {
        secret, err := rand.Int(rand.Reader, big.NewInt(0).Exp(big.NewInt(2), big.NewInt(130), nil))
        if err != nil {
            panic(err)
        }
        return secret
    }

    secret := genPriv()

    var PK curve.G1Affine
    PK.ScalarMultiplicationBase(secret)

    HM, err := curve.HashToG2([]byte("Hello, World!"), []byte("test"))
    if err != nil {
        panic(err)
    }

    var Sig curve.G2Affine
    Sig.ScalarMultiplication(&HM, secret)

    assert := test.NewAssert(t)
    assert.ProverSucceeded(&testCircuit{}, &testCircuit{
        PK: gadget.NewG1Affine(PK), Sig: gadget.NewG2Affine(Sig), HM: gadget.NewG2Affine(HM),
    }, test.WithBackends(backend.GROTH16), test.WithCurves(ecc.BN254))
}

Error logs:

[nix-shell:~/github/dnarthk]$ go test dude_test.go
--- FAIL: TestTest (38.34s)
    --- FAIL: TestTest/bn254/groth16 (32.38s)
        assert.go:515: 
                Error Trace:    /home/hussein/go/pkg/mod/github.com/consensys/gnark@v0.7.2-0.20230324144629-8f89251cb228/test/assert.go:515
                                                        /home/hussein/go/pkg/mod/github.com/consensys/gnark@v0.7.2-0.20230324144629-8f89251cb228/test/assert.go:136
                                                        /home/hussein/go/pkg/mod/github.com/consensys/gnark@v0.7.2-0.20230324144629-8f89251cb228/test/assert.go:144
                                                        /home/hussein/go/pkg/mod/github.com/consensys/gnark@v0.7.2-0.20230324144629-8f89251cb228/test/assert.go:74
                Error:          groth16(bn254): [assertIsEqual] 50216813883093446480573248228721441113507041834044321955840 == 50216813883093446480889237183057549727367382294244272427207
                                emulated.(*Field[...]).rsh
                                        field_assert.go:56
                                emulated.(*Field[...]).assertLimbsEqualitySlow
                                        field_assert.go:35
                                emulated.(*Field[...]).AssertLimbsEquality
                                        field_assert.go:88
                                emulated.(*Field[...]).AssertIsEqual
                                        field_assert.go:144
                                fields_bn254.Ext2.AssertIsEqual
                                        e2.go:279
                                fields_bn254.Ext6.AssertIsEqual
                                        e6.go:261
                                fields_bn254.Ext6.DivUnchecked
                                        e6.go:314
                                fields_bn254.Ext12.MulTorus
                                        e12_pairing.go:230
                                sw_bn254.Pairing.FinalExponentiationTorus
                                        pairing.go:123
                                sw_bn254.Pairing.FinalExponentiation
                                        pairing.go:77
                                sw_bn254.Pairing.Pair
                                        pairing.go:137
                                command-line-arguments.(*testCircuit).Define
                                        dude_test.go:34

                                witness:{"PK":{"X":{"Limbs":["1994150817481768610","1235247154095663860","2171890078265119104","2606583602725773584"]},"Y":{"Limbs":["10271509859365130892","9043516901281802768","16979713083157272735","2705352635320843033"]}},"Sig":{"X":{"A0":{"Limbs":["11219949897108690048","8550997954063542816","17757865678861127314","1471376415384361219"]},"A1":{"Limbs":["1501398245300977988","3701389754985560858","15522739702337502402","2579290147535710426"]}},"Y":{"A0":{"Limbs":["8849407380141025986","10185630694906073056","3144099018389735133","2117431379031521651"]},"A1":{"Limbs":["6217863759219764260","4838859492308665316","8456854986180169101","1487275514237539369"]}}},"HM":{"X":{"A0":{"Limbs":["15355298030077567241","9669948671603011633","9370267460866241311","680200344209813180"]},"A1":{"Limbs":["63318926566748825","9827603146311018670","15560527974064051958","1003938990945631013"]}},"Y":{"A0":{"Limbs":["13747433911198083926","6139727144073377004","11269494308936257083","2640120129429026842"]},"A1":{"Limbs":["1339737764024109054","13631583807732498276","9271178318250851169","2906268977234934276"]}}}}
                Test:           TestTest/bn254/groth16
FAIL
FAIL    command-line-arguments  38.493s
FAIL

[ivokub]

Yes, I'm able to reproduce. It seems that in https://github.com/ConsenSys/gnark/blob/967e64659278a6e7ac7bead7305a7a9d8f9f4347/std/algebra/emulated/sw_bn254/pairing.go#L90 we get a division by zero.

Simpler test case:

type smallTestCircuit struct{}

func (c *smallTestCircuit) Define(api frontend.API) error {
    pairing, err := sw_bn254.NewPairing(api)
    if err != nil {
        return err
    }
    curve, err := sw_emulated.New[emulated.BN254Fp, emulated.BN254Fr](api, sw_emulated.GetBN254Params())
    if err != nil {
        return err
    }

    _, _, g1aff, g2aff := bn254.Generators()
    var ng1aff bn254.G1Affine
    ng1aff.Neg(&g1aff)

    eg1aff := sw_bn254.NewG1Affine(g1aff)
    eng1aff := curve.Neg(&eg1aff)
    eg2aff := sw_bn254.NewG2Affine(g2aff)
    res, err := pairing.Pair([]*sw_bn254.G1Affine{&eg1aff, eng1aff}, []*sw_bn254.G2Affine{&eg2aff, &eg2aff})
    if err != nil {
        return err
    }
    f, err := emulated.NewField[emulated.BN254Fp](api)
    if err != nil {
        return err
    }
    ext12 := fields_bn254.NewExt12(f)
    o := ext12.One()
    pairing.AssertIsEqual(o, res)
    return nil
}

func TestSmall(t *testing.T) {
    assert := test.NewAssert(t)
    err = test.IsSolved(&smallTestCircuit{}, &smallTestCircuit{}, ecc.BN254.ScalarField())
    assert.NoError(err)
}

edit: we will look into it and try to fix, but it will take a bit of time, not my area of expertise :) I think meanwhile it should be possible to compute instead two pairings, compute the inverse and check equality a la

        res1, err := pairing.Pair([]*sw_bn254.G1Affine{&eg1aff}, []*sw_bn254.G2Affine{&eg2aff})
    if err != nil {
        return err
    }
    res2, err := pairing.Pair([]*sw_bn254.G1Affine{eng1aff}, []*sw_bn254.G2Affine{&eg2aff})
    if err != nil {
        return err
    }
    f, err := emulated.NewField[emulated.BN254Fp](api)
    if err != nil {
        return err
    }
    ext12 := fields_bn254.NewExt12(f)
    res2inv := ext12.Inverse(res2)
    ext12.AssertIsEqual(res2inv, res1)

[hussein-aitlahcen]

Yes, I'm able to reproduce. It seems that in

https://github.com/ConsenSys/gnark/blob/967e64659278a6e7ac7bead7305a7a9d8f9f4347/std/algebra/emulated/sw_bn254/pairing.go#L90

we get a division by zero. Simpler test case:

type smallTestCircuit struct{}

func (c *smallTestCircuit) Define(api frontend.API) error {
  pairing, err := sw_bn254.NewPairing(api)
  if err != nil {
      return err
  }
  curve, err := sw_emulated.New[emulated.BN254Fp, emulated.BN254Fr](api, sw_emulated.GetBN254Params())
  if err != nil {
      return err
  }

  _, _, g1aff, g2aff := bn254.Generators()
  var ng1aff bn254.G1Affine
  ng1aff.Neg(&g1aff)

  eg1aff := sw_bn254.NewG1Affine(g1aff)
  eng1aff := curve.Neg(&eg1aff)
  eg2aff := sw_bn254.NewG2Affine(g2aff)
  res, err := pairing.Pair([]*sw_bn254.G1Affine{&eg1aff, eng1aff}, []*sw_bn254.G2Affine{&eg2aff, &eg2aff})
  if err != nil {
      return err
  }
  f, err := emulated.NewField[emulated.BN254Fp](api)
  if err != nil {
      return err
  }
  ext12 := fields_bn254.NewExt12(f)
  o := ext12.One()
  pairing.AssertIsEqual(o, res)
  return nil
}

func TestSmall(t *testing.T) {
  assert := test.NewAssert(t)
  err = test.IsSolved(&smallTestCircuit{}, &smallTestCircuit{}, ecc.BN254.ScalarField())
  assert.NoError(err)
}

edit: we will look into it and try to fix, but it will take a bit of time, not my area of expertise :) I think meanwhile it should be possible to compute instead two pairings, compute the inverse and check equality a la

        res1, err := pairing.Pair([]*sw_bn254.G1Affine{&eg1aff}, []*sw_bn254.G2Affine{&eg2aff})
  if err != nil {
      return err
  }
  res2, err := pairing.Pair([]*sw_bn254.G1Affine{eng1aff}, []*sw_bn254.G2Affine{&eg2aff})
  if err != nil {
      return err
  }
  f, err := emulated.NewField[emulated.BN254Fp](api)
  if err != nil {
      return err
  }
  ext12 := fields_bn254.NewExt12(f)
  res2inv := ext12.Inverse(res2)
  ext12.AssertIsEqual(res2inv, res1)

Thanks for shrinking :)!

[yelhousni]

Thanks @hussein-aitlahcen for raising this issue. So for a single pairing, the implemented logic is correct. For a product of pairings, it seems there might be an edge case for which the verification fails. In fact, we perform now the final exponentiation in the algebraic torus T2(Fp6). So we need to compress an element e ∈ Fp12 to Fp6 which requires e.C1 ≠ 0. The e.C1=0 occurs only when e = 1 or -1 which cannot be the case after a Miller loop but it seems it can be the case after a product of Miller loops, in which case the final result would always be 1. I'm working on a fix.

[hussein-aitlahcen]

@yelhousni you're welcome, thanks for the quick answer! I would love to grasp everything you explained but I'm not at this level yet (otherwise I would have been more than happy to try fixing this). We've reverted to the previous version for now, it's all good.

[yelhousni]

Yes, I'm able to reproduce. It seems that in

https://github.com/ConsenSys/gnark/blob/967e64659278a6e7ac7bead7305a7a9d8f9f4347/std/algebra/emulated/sw_bn254/pairing.go#L90

we get a division by zero.

Actually this happens in the simpler proposed test by @ivokub but in the original test proposed by @hussein-aitlahcen we get the division by zero elsewhere, here: https://github.com/ConsenSys/gnark/blob/17e2743737b581311a00064ed559d67eea859762/std/algebra/emulated/sw_bn254/pairing.go#L123

However, it's the same issue but should be solved in two places. TL;DR the torus-based arithmetic does not work for elements in {-1,1}. For a single Miller loop this should never happen but for a product of Miller loops it might happen (as in the provided tests). For the simpler test e.C1 = 0 means e=1 (because the norm equation is 1). For the original test t0 = -t2 which also means that the product is 1 in the torus. In the PR #613 I proposed a fix that gets around these edge cases for both BN254 and BLS12-381. This adds 13k constraint however. We can also have a different path (orignal code) when MillerLoop size is 1 that saves these 13k in that case.

[hussein-aitlahcen]

Yes, I'm able to reproduce. It seems that in https://github.com/ConsenSys/gnark/blob/967e64659278a6e7ac7bead7305a7a9d8f9f4347/std/algebra/emulated/sw_bn254/pairing.go#L90

we get a division by zero.

Actually this happens in the simpler proposed test by @ivokub but in the original test proposed by @hussein-aitlahcen we get the division by zero elsewhere, here:

https://github.com/ConsenSys/gnark/blob/17e2743737b581311a00064ed559d67eea859762/std/algebra/emulated/sw_bn254/pairing.go#L123

However, it's the same issue but should be solved in two places. TL;DR the torus-based arithmetic does not work for elements in {-1,1}. For a single Miller loop this should never happen but for a product of Miller loops it might happen (as in the provided tests). For the simpler test e.C1 = 0 means e=1 (because the norm equation is 1). For the original test t0 = -t2 which also means that the product is 1 in the torus. In the PR #613 I proposed a fix that gets around these edge cases for both BN254 and BLS12-381. This adds 13k constraint however. We can also have a different path (orignal code) when MillerLoop size is 1 that saves these 13k in that case.

Fantastic, I'm upgrading to the PR right now :)

[hussein-aitlahcen]

Resolved by #613