search

Consensys / gnark

gnark is a fast zk-SNARK library that offers a high-level API to design circuits. The library is open source and developed under the Apache 2.0 license
https://hackmd.io/@gnark
Apache License 2.0
1.44k stars 369 forks source link

bug: pairing check failing in computeLines #1021

Closed hussein-aitlahcen closed 9 months ago

hussein-aitlahcen commented 9 months ago

Impossible to do a pairing check after hashing to curve in circuit

Description

Pairing check is failing if point is not reduced. Pairing check success if point is reduce, but the mulCheck is then failing.

Expected Behavior

Pairing check either succeed or fail depending on ?=1

Actual Behavior

The pairing check partially execute and fail when doing a division

                Error:          Received unexpected error:
                                [assertIsEqual] 13573084457088809626222208413653396691442628839211825728704817208597560688640 == 13573084457088809626222208413653396691442628839211825728718372491985233641471
                                emulated.(*Field[...]).rsh
                                        field_assert.go:56
                                emulated.(*Field[...]).assertLimbsEqualitySlow
                                        field_assert.go:35
                                emulated.(*Field[...]).AssertLimbsEquality
                                        field_assert.go:86
                                emulated.(*Field[...]).AssertIsEqual
                                        field_assert.go:144
                                fields_bn254.Ext2.AssertIsEqual
                                        e2.go:292
                                fields_bn254.Ext2.DivUnchecked
                                        e2.go:338
                                sw_bn254.Pairing.doubleAndAddStep
                                        pairing.go:525
                                sw_bn254.(*Pairing).computeLines
                                        precomputations.go:51
                                sw_bn254.Pairing.MillerLoop
                                        pairing.go:337
                                sw_bn254.Pairing.Pair
                                        pairing.go:235
                                sw_bn254.Pairing.PairingCheck
                                        pairing.go:248
                                bls.(*BlsAPI).VerifySignature
                                        api.go:87

Possible Fix

this is not a fix but a hack

Provide an already reduced point as input, assert non reduced in-circuit computed point = precomputed reduced point. Then use the reduced point in the pairing check.

Steps to Reproduce

Difficult to reproduce without sharing the circuit, which I unfortunately can't right now... But I have the limbs of the hashedMessage and circuit.HashedMessage which are supposed to be equal:

    api.Println(hashedMessage.P.X.A0.Limbs...)
    api.Println(hashedMessage.P.X.A1.Limbs...)
    api.Println(hashedMessage.P.Y.A0.Limbs...)
    api.Println(hashedMessage.P.Y.A1.Limbs...)
    api.Println(circuit.HashedMessage.P.X.A0.Limbs...)
    api.Println(circuit.HashedMessage.P.X.A1.Limbs...)
    api.Println(circuit.HashedMessage.P.Y.A0.Limbs...)
    api.Println(circuit.HashedMessage.P.Y.A1.Limbs...)
    emulatedAPI.AssertIsEqual(hashedMessage, &circuit.HashedMessage)
(test.engine) circuit.go:46 731357677393372949156035347812318951046982142424218836498362974 731357677393372949156035347812318951046982151724018355025173054 731357677393372949156035347812318951046982137688853674959032584 731357677393372949156035347812318951046982166735237619140699961 
(test.engine) circuit.go:47 1462715354786745898312070695624637902093964261711126733991492303 1462715354786745898312070695624637902093964400424641065979075866 1462715354786745898312070695624637902093964093851933721962378868 1462715354786745898312070695624637902093964285612166117565438195 
(test.engine) circuit.go:48 1225996432692711086686677621720247380894688177721744432 1225996432692711086686677621720247341543641161608247233 1225996432692711086686677621720247240858616188630742230 1225996432692711086686677621720247342023609896358217801 
(test.engine) circuit.go:49 1225996432692711086686677621720247354175014015613623455 1225996432692711086686677621720247337423881473139217565 1225996432692711086686677621720247223803978013039608155 1225996432692711086686677621720247345915149660392407871 
(test.engine) circuit.go:50 6100632540357070999 98655406553727371 15906860541925415677 2110505027010837885 
(test.engine) circuit.go:51 8494485320925336540 17735600162734044383 4496698748756625187 1693678401744332689 
(test.engine) circuit.go:52 14226504759626984327 12905112477811950811 16391525418439874834 660748936362181337 
(test.engine) circuit.go:53 1620957799948758703 16314972718574589737 4502439365283597625 1065290433593400741

Note: the emulated arithmetic don't reduce the G2 coordinate, if I manually reduce via emulated.Field[T].Reduce, the following error happen

    result.P.X.A0 = *e.field.Reduce(&result.P.X.A0)
    result.P.X.A1 = *e.field.Reduce(&result.P.X.A1)
    result.P.Y.A0 = *e.field.Reduce(&result.P.Y.A0)
    result.P.Y.A1 = *e.field.Reduce(&result.P.Y.A1)
                Error:          Received unexpected error:
                                [assertIsEqual] 17192346684490724479132753141438781808435158862270986513452613437186377923286 == 17624948470444647702376193208120835975715250400947484742758127258421773707776
                                emulated.(*mulCheck[...]).check
                                        field_mul.go:86
                                emulated.(*Field[...]).performMulChecks.func1
                                        field_mul.go:200
                                multicommit.(*multicommitter).commitAndCall
                                        nativecommit.go:101
                                nonadjacent.FuzzNonadjacent.func4
                                        circuit_test.go:324
                                reflect.Value.call
                                        value.go:596
                                reflect.Value.Call
                                        value.go:380
                                testing.(*F).Fuzz.func1.1
                                        fuzz.go:335
                                testing.tRunner
                                        testing.go:1595
                                runtime.goexit
                                        asm_amd64.s:1650

Your Environment

hussein-aitlahcen commented 9 months ago

@ivokub after investigation its perhaps a combination of #749 with the precomputed lines. As field.Mul no longer reduce, the point is not reduced when calling the pairing check and the subsequent line precomputation is failing. If I manually reduce the components before that, the pairing check successfully pass but I have an issue with the mulCheck later... I guess AssertIsEqual is still working because it still uses the old mul. Am I missing something obvious?

hussein-aitlahcen commented 9 months ago

I am able to fix the issue and reduce if I patch field.Reduce from: https://github.com/Consensys/gnark/blob/179023dd99e8783c69103c041f106897a7fcc87a/std/math/emulated/field_ops.go#L136-L148

To the previous version using the remainder without pushing a mulCheck:

// Reduce reduces a modulo the field order and returns it. Uses hint [RemHint].
func (f *Field[T]) Reduce(a *Element[T]) *Element[T] {
    f.enforceWidthConditional(a)
    if a.overflow == 0 {
        // fast path - already reduced, omit reduction.
        return a
    }
    // sanity check
    if _, aConst := f.constantValue(a); aConst {
        panic("trying to reduce a constant, which happen to have an overflow flag set")
    }

    // slow path - use hint to reduce value
    _, r, _, err := f.callMulHint(a, f.One())
    if err != nil {
        panic(fmt.Sprintf("reduction hint: %v", err))
    }
    f.AssertIsEqual(r, a)
    return r
}
ivokub commented 9 months ago

Now Field.Mul and Field.MulMod are equivalent with latter are only left for API compatibility and they both modreduce the result automatically. And you're right, f.AssertIsEqual uses old multiplication which is less susceptible to some kinds of bugs.

I think it should be sufficient to have limbs for debugging, but to confirm, the emulated G2 points are for BN254? And over what curve are you constructing the proof? Additionally, could you also give what is the value of the overflow field of the *Element? We use this field to track the max width of the limbs and there have previously been bugs with its computation on some edge cases. It is unexported though but I think that maybe you can use fmt.Printf with %+v to print the value?

It seems like a major bug indeed, I'll try to debug it in a few days. I still have a few things in backlog.

hussein-aitlahcen commented 9 months ago

Now Field.Mul and Field.MulMod are equivalent with latter are only left for API compatibility and they both modreduce the result automatically. And you're right, f.AssertIsEqual uses old multiplication which is less susceptible to some kinds of bugs.

I think it should be sufficient to have limbs for debugging, but to confirm, the emulated G2 points are for BN254? And over what curve are you constructing the proof? Additionally, could you also give what is the value of the overflow field of the *Element? We use this field to track the max width of the limbs and there have previously been bugs with its computation on some edge cases. It is unexported though but I think that maybe you can use fmt.Printf with %+v to print the value?

It seems like a major bug indeed, I'll try to debug it in a few days. I still have a few things in backlog.

It's BN254 on BN254 in Groth16, here is the dump of in-circuit hashedMessage that overflows and circuit.HashedMessage passed as public:

(test.engine) field_assert.go:211 Overflow:  147 
(test.engine) field_assert.go:212 Internal:  1 
(test.engine) field_assert.go:213 Limbs   : 
[+731357677393372949156035347812318951046982112975653444387794127 +731357677393372949156035347812318951046982158841205293597773323 +731357677393372949156035347812318951046982077668374614900268710 +731357677393372949156035347812318951046982121951598480347017066]
(test.engine) field_assert.go:211 Overflow:  148 
(test.engine) field_assert.go:212 Internal:  1 
(test.engine) field_assert.go:213 Limbs   : 
[+1462715354786745898312070695624637902093964181393946215859544207 +1462715354786745898312070695624637902093964195946379967022867391 +1462715354786745898312070695624637902093964030445854428435853522 +1462715354786745898312070695624637902093964230039617171585058601]
(test.engine) field_assert.go:211 Overflow:  118 
(test.engine) field_assert.go:212 Internal:  1 
(test.engine) field_assert.go:213 Limbs   : 
[+1225996432692711086686677621720247318812756641730443502 +1225996432692711086686677621720247361700411779813937251 +1225996432692711086686677621720247182320076968792456741 +1225996432692711086686677621720247335077927209076111906]
(test.engine) field_assert.go:211 Overflow:  118 
(test.engine) field_assert.go:212 Internal:  1 
(test.engine) field_assert.go:213 Limbs   : 
[+1225996432692711086686677621720247306918135218379411414 +1225996432692711086686677621720247444473235325305077797 +1225996432692711086686677621720247223821543200735648469 +1225996432692711086686677621720247351674909366319710493]
(test.engine) field_assert.go:211 Overflow:  0 
(test.engine) field_assert.go:212 Internal:  0 
(test.engine) field_assert.go:213 Limbs   : 
[+14529342401172481955 +1564503633662393986 +17861412406180373852 +2657843356655773641]
(test.engine) field_assert.go:211 Overflow:  0 
(test.engine) field_assert.go:212 Internal:  0 
(test.engine) field_assert.go:213 Limbs   : 
[+15945918816977440268 +6378069449133515859 +6015738085948802896 +1913101724611483743]
(test.engine) field_assert.go:211 Overflow:  0 
(test.engine) field_assert.go:212 Internal:  0 
(test.engine) field_assert.go:213 Limbs   : 
[+16150039187323650771 +18002643237554303636 +2862114174860530461 +689062782686016771]
(test.engine) field_assert.go:211 Overflow:  0 
(test.engine) field_assert.go:212 Internal:  0 
(test.engine) field_assert.go:213 Limbs   : 
[+5371694352563545247 +1766737984005257249 +9685556675414494812 +3338051872717732697]
ivokub commented 9 months ago

Thanks for the inputs.

One thing though -- I see from the stack trace that the inputs are obtained from a fuzzer, am I right? I'm not sure if we test by default that the inputs to the pairing computation are checked to be in G1 and G2. I'm not sure the pairing computation is complete in cases the inputs are not curve, maybe @yelhousni can confirm?

What happens if you assert tests pairing.AssertIsOnG1 and pairing.AssertIsOnG2 before calling pairing.PairingCheck? Does it still fail?

If indeed the failure is due to the G2 inputs not being in group then I guess we can add options to the Pairing and PairingCheck interfaces to perform the checks. We have omitted the checks before because in our use cases we are performing them separately and it impacts the constraint count significantly if we perform by default.

hussein-aitlahcen commented 9 months ago

Thanks for the inputs.

One thing though -- I see from the stack trace that the inputs are obtained from a fuzzer, am I right? I'm not sure if we test by default that the inputs to the pairing computation are checked to be in G1 and G2. I'm not sure the pairing computation is complete in cases the inputs are not curve, maybe @yelhousni can confirm?

What happens if you assert tests pairing.AssertIsOnG1 and pairing.AssertIsOnG2 before calling pairing.PairingCheck? Does it still fail?

If indeed the failure is due to the G2 inputs not being in group then I guess we can add options to the Pairing and PairingCheck interfaces to perform the checks. We have omitted the checks before because in our use cases we are performing them separately and it impacts the constraint count significantly if we perform by default.

It's a fuzzing test (golang fuzzing, gnark test is ran with NoFuzzing), but the fuzzing is only used to seed private keys, all points are correctly mapped as the VerifySignature function check them before executing the pairing, as follow:

func (b *BlsAPI) VerifySignature(publicKey *gadget.G1Affine, message *gadget.G2Affine, signature *gadget.G2Affine) error {
    pairing, err := gadget.NewPairing(b.api)
    if err != nil {
        return fmt.Errorf("new pairing: %w", err)
    }
    pairing.AssertIsOnG1(publicKey)
    pairing.AssertIsOnG2(message)
    pairing.AssertIsOnG2(signature)
    // Verify that the aggregated signature is correct
    err = pairing.PairingCheck(
        []*gadget.G1Affine{&b.negG1Gen, publicKey},
        []*gadget.G2Affine{signature, message},
    )
    if err != nil {
        return fmt.Errorf("pairing check: %w", err)
    }
    return nil
}

Note that I am even doing a pairing check out of circuit to verify before asserting the circuit to be solved by this inputs

yelhousni commented 9 months ago

@hussein-aitlahcen It's difficult to debug without reproducing in local but it seems that the pairing circuit fails at doubleAndAddStep in computeLines when the loopCounter bit is -1 (which happens only 11 times). Can you share the coordinates of the points G1 and G2 you're trying to do a pairing of? Can you also confirm at which iteration i it fails and at this point what is Qacc and QNeg? They must have the same x-coordinate at this iteration so that it fails but I need to understand why.

yelhousni commented 9 months ago

Also would you test with an earlier version of gnark? just to confirm if it is related to the pairing algorithm or the field emulation. I believe the pairing algorithm did not change (the code in computeLines was the exact same directly inside MillerLoop).

hussein-aitlahcen commented 9 months ago

@yelhousni the test cases are very involved but I managed to reproduce, I have few notes:

I also don't think it's the pairing check but more like the new way of doing mulMod.

Below is a reproducible case where points are correctly mapped but the message is non reduced:

// (test.engine) api.go:89 publicKey:
// (test.engine) api.go:90 11930982415540411953 12343092716136141065 1916072663178228420 554508045891390944
// (test.engine) api.go:91 13483673382317630327 9152802033415685860 5502605702594763507 2536091695916914633
// (test.engine) api.go:92 signature:
// (test.engine) api.go:93 11300806162194093623 11024472275762661616 713814731584471798 3398271227046419981
// (test.engine) api.go:94 17557010969439139012 12959726923681390654 6898571771715354335 1113685078429720673
// (test.engine) api.go:95 1605531702743565790 8699071956286069614 16002142271116031401 2499191488808805049
// (test.engine) api.go:96 9267720049247923974 305767022685043862 1595415380063926597 530773690523314188
// (test.engine) api.go:97 message:
// (test.engine) field.go:115 ===
// (test.engine) field.go:116 Internal:  1
// (test.engine) field.go:117 Overflow:  147
// (test.engine) field.go:118 731357677393372949156035347812318951046982142424218836498362974 731357677393372949156035347812318951046982151724018355025173054 731357677393372949156035347812318951046982137688853674959032584 731357677393372949156035347812318951046982166735237619140699961
// (test.engine) field.go:115 ===
// (test.engine) field.go:116 Internal:  1
// (test.engine) field.go:117 Overflow:  148
// (test.engine) field.go:118 1462715354786745898312070695624637902093964261711126733991492303 1462715354786745898312070695624637902093964400424641065979075866 1462715354786745898312070695624637902093964093851933721962378868 1462715354786745898312070695624637902093964285612166117565438195
// (test.engine) field.go:115 ===
// (test.engine) field.go:116 Internal:  1
// (test.engine) field.go:117 Overflow:  118
// (test.engine) field.go:118 1225996432692711086686677621720247380894688177721744432 1225996432692711086686677621720247341543641161608247233 1225996432692711086686677621720247240858616188630742230 1225996432692711086686677621720247342023609896358217801
// (test.engine) field.go:115 ===
// (test.engine) field.go:116 Internal:  1
// (test.engine) field.go:117 Overflow:  118
// (test.engine) field.go:118 1225996432692711086686677621720247354175014015613623455 1225996432692711086686677621720247337423881473139217565 1225996432692711086686677621720247223803978013039608155 1225996432692711086686677621720247345915149660392407871

type ReductionIssue struct {
    NonReduced gadget.G2Affine
    Signature  gadget.G2Affine
    PublicKey  gadget.G1Affine
}

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

        /* Assuming we have this backdoor for testing
           func (e*Element[T]) SetInternal(internal bool, overflow uint) {
                e.overflow = overflow
                e.internal = internal
            }
        */
    c.NonReduced.P.X.A0.SetInternal(true, 147)
    c.NonReduced.P.X.A1.SetInternal(true, 148)
    c.NonReduced.P.Y.A0.SetInternal(true, 118)
    c.NonReduced.P.Y.A1.SetInternal(true, 118)

    pairing.AssertIsOnG1(&c.PublicKey)
    pairing.AssertIsOnG2(&c.Signature)
    pairing.AssertIsOnG2(&c.NonReduced)

    _, _, g1Gen, _ := curve.Generators()
    var g1GenNeg curve.G1Affine
    g1GenNeg.Neg(&g1Gen)
    g1GenNegEmulated := gadget.NewG1Affine(g1GenNeg)

    err = pairing.PairingCheck(
        []*gadget.G1Affine{&g1GenNegEmulated, &c.PublicKey},
        []*gadget.G2Affine{&c.Signature, &c.NonReduced},
    )
    if err != nil {
        return fmt.Errorf("pairing check: %w", err)
    }
    return nil
}

func TestReduction(t *testing.T) {
    t.Parallel()
    publicKey := gadget.G1Affine{}
    publicKey.X.Limbs = []frontend.Variable{
        uint64(11930982415540411953),
        uint64(12343092716136141065),
        uint64(1916072663178228420),
        uint64(554508045891390944),
    }
    publicKey.Y.Limbs = []frontend.Variable{
        uint64(13483673382317630327),
        uint64(9152802033415685860),
        uint64(5502605702594763507),
        uint64(2536091695916914633),
    }

    signature := gadget.G2Affine{}
    signature.P.X.A0.Limbs = []frontend.Variable{
        uint64(11300806162194093623),
        uint64(11024472275762661616),
        uint64(713814731584471798),
        uint64(3398271227046419981),
    }
    signature.P.X.A1.Limbs = []frontend.Variable{
        uint64(17557010969439139012),
        uint64(12959726923681390654),
        uint64(6898571771715354335),
        uint64(1113685078429720673),
    }
    signature.P.Y.A0.Limbs = []frontend.Variable{
        uint64(1605531702743565790),
        uint64(8699071956286069614),
        uint64(16002142271116031401),
        uint64(2499191488808805049),
    }
    signature.P.Y.A1.Limbs = []frontend.Variable{
        uint64(9267720049247923974),
        uint64(305767022685043862),
        uint64(1595415380063926597),
        uint64(530773690523314188),
    }

    bigInt := func(x string) *big.Int {
        var b big.Int
        _, ok := b.SetString(x, 10)
        assert.True(t, ok)
        return &b
    }

    message := gadget.G2Affine{}
    message.P.X.A0.Limbs = []frontend.Variable{
        bigInt("731357677393372949156035347812318951046982142424218836498362974"),
        bigInt("731357677393372949156035347812318951046982151724018355025173054"),
        bigInt("731357677393372949156035347812318951046982137688853674959032584"),
        bigInt("731357677393372949156035347812318951046982166735237619140699961"),
    }
    message.P.X.A1.Limbs = []frontend.Variable{
        bigInt("1462715354786745898312070695624637902093964261711126733991492303"),
        bigInt("1462715354786745898312070695624637902093964400424641065979075866"),
        bigInt("1462715354786745898312070695624637902093964093851933721962378868"),
        bigInt("1462715354786745898312070695624637902093964285612166117565438195"),
    }
    message.P.Y.A0.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247380894688177721744432"),
        bigInt("1225996432692711086686677621720247341543641161608247233"),
        bigInt("1225996432692711086686677621720247240858616188630742230"),
        bigInt("1225996432692711086686677621720247342023609896358217801"),
    }
    message.P.Y.A1.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247354175014015613623455"),
        bigInt("1225996432692711086686677621720247337423881473139217565"),
        bigInt("1225996432692711086686677621720247223803978013039608155"),
        bigInt("1225996432692711086686677621720247345915149660392407871"),
    }
    err := test.IsSolved(
        &ReductionIssue{},
        &ReductionIssue{
            PublicKey:  publicKey,
            Signature:  signature,
            NonReduced: message,
        },
        ecc.BN254.ScalarField(),
    )
    assert.NoError(t, err)
}

type MulcheckIssue struct {
    NonReduced gadget.G2Affine
    Signature  gadget.G2Affine
    PublicKey  gadget.G1Affine
}

func (c *MulcheckIssue) Define(api frontend.API) error {
    ba, err := emulated.NewField[emulated.BN254Fp](api)
    if err != nil {
        return fmt.Errorf("new base api: %w", err)
    }
    pairing, err := gadget.NewPairing(api)
    if err != nil {
        return fmt.Errorf("new pairing: %w", err)
    }

    c.NonReduced.P.X.A0.SetInternal(true, 147)
    c.NonReduced.P.X.A1.SetInternal(true, 148)
    c.NonReduced.P.Y.A0.SetInternal(true, 118)
    c.NonReduced.P.Y.A1.SetInternal(true, 118)

    // Reduction allow the pairing check to be successful, at the expense of a mulCheck failure
    c.NonReduced.P.X.A0 = *ba.Reduce(&c.NonReduced.P.X.A0)
    c.NonReduced.P.X.A1 = *ba.Reduce(&c.NonReduced.P.X.A1)
    c.NonReduced.P.Y.A0 = *ba.Reduce(&c.NonReduced.P.Y.A0)
    c.NonReduced.P.Y.A1 = *ba.Reduce(&c.NonReduced.P.Y.A1)

    api.Println(c.NonReduced.P.X.A0.Limbs...)
    api.Println(c.NonReduced.P.X.A1.Limbs...)
    api.Println(c.NonReduced.P.Y.A0.Limbs...)
    api.Println(c.NonReduced.P.Y.A1.Limbs...)

    pairing.AssertIsOnG1(&c.PublicKey)
    pairing.AssertIsOnG2(&c.Signature)
    pairing.AssertIsOnG2(&c.NonReduced)

    _, _, g1Gen, _ := curve.Generators()
    var g1GenNeg curve.G1Affine
    g1GenNeg.Neg(&g1Gen)
    g1GenNegEmulated := gadget.NewG1Affine(g1GenNeg)

    err = pairing.PairingCheck(
        []*gadget.G1Affine{&g1GenNegEmulated, &c.PublicKey},
        []*gadget.G2Affine{&c.Signature, &c.NonReduced},
    )
    if err != nil {
        return fmt.Errorf("pairing check: %w", err)
    }
    return nil
}

func TestMulcheck(t *testing.T) {
    t.Parallel()
    publicKey := gadget.G1Affine{}
    publicKey.X.Limbs = []frontend.Variable{
        uint64(11930982415540411953),
        uint64(12343092716136141065),
        uint64(1916072663178228420),
        uint64(554508045891390944),
    }
    publicKey.Y.Limbs = []frontend.Variable{
        uint64(13483673382317630327),
        uint64(9152802033415685860),
        uint64(5502605702594763507),
        uint64(2536091695916914633),
    }

    signature := gadget.G2Affine{}
    signature.P.X.A0.Limbs = []frontend.Variable{
        uint64(11300806162194093623),
        uint64(11024472275762661616),
        uint64(713814731584471798),
        uint64(3398271227046419981),
    }
    signature.P.X.A1.Limbs = []frontend.Variable{
        uint64(17557010969439139012),
        uint64(12959726923681390654),
        uint64(6898571771715354335),
        uint64(1113685078429720673),
    }
    signature.P.Y.A0.Limbs = []frontend.Variable{
        uint64(1605531702743565790),
        uint64(8699071956286069614),
        uint64(16002142271116031401),
        uint64(2499191488808805049),
    }
    signature.P.Y.A1.Limbs = []frontend.Variable{
        uint64(9267720049247923974),
        uint64(305767022685043862),
        uint64(1595415380063926597),
        uint64(530773690523314188),
    }

    bigInt := func(x string) *big.Int {
        var b big.Int
        _, ok := b.SetString(x, 10)
        assert.True(t, ok)
        return &b
    }

    message := gadget.G2Affine{}
    message.P.X.A0.Limbs = []frontend.Variable{
        bigInt("731357677393372949156035347812318951046982142424218836498362974"),
        bigInt("731357677393372949156035347812318951046982151724018355025173054"),
        bigInt("731357677393372949156035347812318951046982137688853674959032584"),
        bigInt("731357677393372949156035347812318951046982166735237619140699961"),
    }
    message.P.X.A1.Limbs = []frontend.Variable{
        bigInt("1462715354786745898312070695624637902093964261711126733991492303"),
        bigInt("1462715354786745898312070695624637902093964400424641065979075866"),
        bigInt("1462715354786745898312070695624637902093964093851933721962378868"),
        bigInt("1462715354786745898312070695624637902093964285612166117565438195"),
    }
    message.P.Y.A0.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247380894688177721744432"),
        bigInt("1225996432692711086686677621720247341543641161608247233"),
        bigInt("1225996432692711086686677621720247240858616188630742230"),
        bigInt("1225996432692711086686677621720247342023609896358217801"),
    }
    message.P.Y.A1.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247354175014015613623455"),
        bigInt("1225996432692711086686677621720247337423881473139217565"),
        bigInt("1225996432692711086686677621720247223803978013039608155"),
        bigInt("1225996432692711086686677621720247345915149660392407871"),
    }
    err := test.IsSolved(
        &MulcheckIssue{},
        &MulcheckIssue{
            PublicKey:  publicKey,
            Signature:  signature,
            NonReduced: message,
        },
        ecc.BN254.ScalarField(),
    )
    assert.NoError(t, err)
}
hussein-aitlahcen commented 9 months ago

Oh, it's working if we recreate a point to reduce as stated in the doc here https://github.com/Consensys/gnark/blob/4c81525a048329c8cf0f4cd82cb05ff41a0ace47/std/math/emulated/field_mul.go#L18-L23 So the following is wrong because we reassign...

    // Reduction allow the pairing check to be successful, at the expense of a mulCheck failure
    c.NonReduced.P.X.A0 = *ba.Reduce(&c.NonReduced.P.X.A0)
    c.NonReduced.P.X.A1 = *ba.Reduce(&c.NonReduced.P.X.A1)
    c.NonReduced.P.Y.A0 = *ba.Reduce(&c.NonReduced.P.Y.A0)
    c.NonReduced.P.Y.A1 = *ba.Reduce(&c.NonReduced.P.Y.A1)

Yet I struggle to understand why we are forced to reduce to do the pairing while the rest of the API don't expected the reduction?

ivokub commented 9 months ago

Hmm, I think I understand now. The reason is a bit complicated to be honest, but I'll try to explain.

In the new modular multiplication approach we are considering the limbs of non-native element to be coefficients of a polynomial. Then, to show that the modular multiplication A * B = C + K*P holds we need to show it on the corresponding polynomials a(X) * b(X) = c(X) + k(X) * p(X) + e(X) (here e(X) is a fixed polynomial for carrying the carries). Normally, we would then sample a random challenge r and then check the polynomial evaluation on a random point: a(r) * b(r) == c(r) + k(r) * p(r) + e(r).

Now, if we notice that we actually have a lot of multiplication chains so c(X) from one multiplication check is an input to another multiplication (i.e. c_n(X) is a_{n+100}(X) in some other check). So, to make the multiplication checks more efficient we only evaluate such polynomials only one and then use the cached value wherever the same polynomial is in future checks.

Now, remembering that the polynomials are actually limbs in the non-native element, which is a structure:

type Element[T] struct {
    Limbs []frontend.Variable
    ....
    evaluationValue frontend.Variable // evaluated Limbs[0] + Limbs[1]*r + Limbs[2]*r^2+....
}

and the multiplication check (which are only called after Define of the circuit) are stored as:

type mulCheck struct {
    a, b, c, k, e *Element[T] // do not need to store p, it is the modulus of the emulated field

So, if we would overwrite Element stored at some pointer location *Element, then it affects the amortized multiplication check and we get undefined behaviour unfortunately.

And so, if for example we have a structure:

type Point struct {
    X, Y emulated.Element[T]

where X, Y are results of some computation which gets included in the multiplication checks and we would do something:

    p := Point{X: *f.Mul(a, b), Y: *f.Mul(c,d)}
    p.X = *f.Mul(&p.X, x)

then we are overwriting the emulated.Element value pointed at &p.X and we get undefined behaviour! It should instead be written as:

    p := Point{X: *f.Mul(a, b), Y: *f.Mul(c,d)}
    p = Point{X: *f.Mul(&p.X, x), Y: p.Y} // I'm not overwriting existing p.X but creating a new value

So, in short, can you check that in your code you are not dereferencing non-native operation result into an existing non-native element value?

On a bit unrelated note, I have tried figuring out how to add a canary to detect such modification of values, but I haven't come up with a good solution yet. The current behaviour is really unintuitive, and I'd definitely want to make it better (even by showing informative errors messages at least).

ivokub commented 9 months ago

I am trying to recreate the inputs and I'm not able to create native input for which the pairing check succeeds. From the given example I tried to reconstruct the hashed message:

type EqualityCircuit struct {
    WitnessMsg  gadget.G2Affine
    ComputedMsg gadget.G2Affine
}

func (c *EqualityCircuit) Define(api frontend.API) error {
    g2 := gadget.NewG2(api)
    c.ComputedMsg.P.X.A0.SetInternal(true, 147)
    c.ComputedMsg.P.X.A1.SetInternal(true, 148)
    c.ComputedMsg.P.Y.A0.SetInternal(true, 118)
    c.ComputedMsg.P.Y.A1.SetInternal(true, 118)
    g2.AssertIsEqual(&c.ComputedMsg, &c.WitnessMsg)
    return nil
}

func TestEquality(t *testing.T) {
    assert := test.NewAssert(t)
    var err error
    bigInt := func(x string) *big.Int {
        var b big.Int
        _, ok := b.SetString(x, 10)
        assert.True(ok)
        return &b
    }
    message := gadget.G2Affine{}
    message.P.X.A0.Limbs = []frontend.Variable{
        bigInt("731357677393372949156035347812318951046982142424218836498362974"),
        bigInt("731357677393372949156035347812318951046982151724018355025173054"),
        bigInt("731357677393372949156035347812318951046982137688853674959032584"),
        bigInt("731357677393372949156035347812318951046982166735237619140699961"),
    }
    message.P.X.A1.Limbs = []frontend.Variable{
        bigInt("1462715354786745898312070695624637902093964261711126733991492303"),
        bigInt("1462715354786745898312070695624637902093964400424641065979075866"),
        bigInt("1462715354786745898312070695624637902093964093851933721962378868"),
        bigInt("1462715354786745898312070695624637902093964285612166117565438195"),
    }
    message.P.Y.A0.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247380894688177721744432"),
        bigInt("1225996432692711086686677621720247341543641161608247233"),
        bigInt("1225996432692711086686677621720247240858616188630742230"),
        bigInt("1225996432692711086686677621720247342023609896358217801"),
    }
    message.P.Y.A1.Limbs = []frontend.Variable{
        bigInt("1225996432692711086686677621720247354175014015613623455"),
        bigInt("1225996432692711086686677621720247337423881473139217565"),
        bigInt("1225996432692711086686677621720247223803978013039608155"),
        bigInt("1225996432692711086686677621720247345915149660392407871"),
    }

    msgxa0, err := new(fp.Element).SetString("13247854767592044053073878812331037228887882218153485703259699078156704813207")
    assert.NoError(err)
    msgxa1, err := new(fp.Element).SetString("10631391634776290608147940298158866655851881467848437887363840283340335109084")
    assert.NoError(err)
    msgya0, err := new(fp.Element).SetString("4147588295093951967861280457974193623404677472891767418736712075704186465159")
    assert.NoError(err)
    msgya1, err := new(fp.Element).SetString("6686936429399965395982341866473029103409855157509626717226854381494853971631")
    assert.NoError(err)
    msg := curve.G2Affine{
        X: curve.E2{
            A0: *msgxa0,
            A1: *msgxa1,
        },
        Y: curve.E2{
            A0: *msgya0,
            A1: *msgya1,
        },
    }
    err = test.IsSolved(&EqualityCircuit{}, &EqualityCircuit{WitnessMsg: gadget.NewG2Affine(msg), ComputedMsg: message}, ecc.BN254.ScalarField())
    assert.NoError(err)
}

We see that G2 equality check succeeds, so the hashed message natively corresponds to your example. Now, when I'm trying to compute the pairing natively:

func TestNativePairing(t *testing.T) {
    assert := test.NewAssert(t)
    var err error
    msgxa0, err := new(fp.Element).SetString("13247854767592044053073878812331037228887882218153485703259699078156704813207")
    assert.NoError(err)
    msgxa1, err := new(fp.Element).SetString("10631391634776290608147940298158866655851881467848437887363840283340335109084")
    assert.NoError(err)
    msgya0, err := new(fp.Element).SetString("4147588295093951967861280457974193623404677472891767418736712075704186465159")
    assert.NoError(err)
    msgya1, err := new(fp.Element).SetString("6686936429399965395982341866473029103409855157509626717226854381494853971631")
    assert.NoError(err)
    msg := curve.G2Affine{
        X: curve.E2{
            A0: *msgxa0,
            A1: *msgxa1,
        },
        Y: curve.E2{
            A0: *msgya0,
            A1: *msgya1,
        },
    }
    sigxa0, err := new(fp.Element).SetString("13247854767592044053073878812331037228887882218153485703259699078156704813207")
    assert.NoError(err)
    sigxa1, err := new(fp.Element).SetString("10631391634776290608147940298158866655851881467848437887363840283340335109084")
    assert.NoError(err)
    sigya0, err := new(fp.Element).SetString("4147588295093951967861280457974193623404677472891767418736712075704186465159")
    assert.NoError(err)
    sigya1, err := new(fp.Element).SetString("6686936429399965395982341866473029103409855157509626717226854381494853971631")
    assert.NoError(err)
    sig := curve.G2Affine{
        X: curve.E2{
            A0: *sigxa0,
            A1: *sigxa1,
        },
        Y: curve.E2{
            A0: *sigya0,
            A1: *sigya1,
        },
    }

    pkx, err := new(fp.Element).SetString("3480703417150727311536067606215579789328636298792737855743736748610189516337")
    assert.NoError(err)
    pky, err := new(fp.Element).SetString("15919305585539815134658383098338055295787018379294663107586608899644086723447")
    assert.NoError(err)
    pk := curve.G1Affine{
        X: *pkx,
        Y: *pky,
    }

    _, _, g1aff, _ := curve.Generators()
    ng1aff := new(curve.G1Affine).Neg(&g1aff)

    ok, err := curve.PairingCheck([]curve.G1Affine{*ng1aff, pk}, []curve.G2Affine{sig, msg})
    assert.NoError(err)
    assert.True(ok)
}

it fails.

So it would seem there is some mismatch in the inputs? Can you check that the signature and public key I recovered from the example are correct? Would it be possible to provide such witness for which the native pairing check (using gnark-crypto) succeeds but fails for in-circuit?

hussein-aitlahcen commented 9 months ago

@ivokub I think I was not explaining correctly, let me rephrase: there was no input for which the native pairing check was successful but failing in circuit in the sense that the it's not ?=1 in circuit, when I was saying failing in circuit I was referring to the error in computesLines.

In the end, the issue is that the pairing API do no accept G2 points that are not reduced. So my final fix is to manually reduce (correctly by recreating a point and not mutating the existing one to avoid the mulcheck issue mentioned in the doc) before executing the check:

func (e *EmulatedAPI) Reduce(p *gadget.G2Affine) *gadget.G2Affine {
    reducedP := gadget.G2Affine{}
    reducedP.P.X.A0 = *e.field.Reduce(&p.P.X.A0)
    reducedP.P.X.A1 = *e.field.Reduce(&p.P.X.A1)
    reducedP.P.Y.A0 = *e.field.Reduce(&p.P.Y.A0)
    reducedP.P.Y.A1 = *e.field.Reduce(&p.P.Y.A1)
    return &reducedP
}

...

// https://datatracker.ietf.org/doc/html/rfc9380#name-encoding-byte-strings-to-el
func (e *EmulatedAPI) HashToG2(message frontend.Variable, dst frontend.Variable) (*gadget.G2Affine, error) {
    u, err := e.HashToField(message, dst)
    if err != nil {
        return nil, err
    }
    Q0 := e.MapToCurve(&fields_bn254.E2{
        A0: *u[0],
        A1: *u[1],
    })
    Q1 := e.MapToCurve(&fields_bn254.E2{
        A0: *u[2],
        A1: *u[3],
    })
    return e.Reduce(e.ClearCofactor(e.Add(Q0, Q1))), nil
}

Finally, to avoid allowing the user to mutate field elements, maybe we can make the coordinates private and provide getters/constructors.

ivokub commented 9 months ago

Indeed, I think you have found an edge case. In field emulation when the limbs overflow the field we do not always reduce back to range [0, p) but only if the arithmetic result overflows the native field. However it seems that for some path this is not taken. I'm able to reproduce with the following snippet:

func randomG1G2Affines() (curve.G1Affine, curve.G2Affine) {
    _, _, G1AffGen, G2AffGen := curve.Generators()
    mod := curve.ID.ScalarField()
    s1, err := rand.Int(rand.Reader, mod)
    if err != nil {
        panic(err)
    }
    s2, err := rand.Int(rand.Reader, mod)
    if err != nil {
        panic(err)
    }
    var p curve.G1Affine
    p.ScalarMultiplication(&G1AffGen, s1)
    var q curve.G2Affine
    q.ScalarMultiplication(&G2AffGen, s2)
    return p, q
}

type PairingCircuitNonReduced struct {
    In1G1 gadget.G1Affine
    In1G2 gadget.G2Affine
    In2G1 gadget.G1Affine
    In2G2 gadget.G2Affine
}

func (c *PairingCircuitNonReduced) Define(api frontend.API) error {
    pr, err := gadget.NewPairing(api)
    if err != nil {
        return err
    }

    // // works
    // err = pr.PairingCheck([]*gadget.G1Affine{&c.In1G1, &c.In2G1}, []*gadget.G2Affine{&c.In1G2, &c.In2G2})
    // if err != nil {
    //  return fmt.Errorf("pair: %w", err)
    // }

    // // also works
    // var in2 gadget.G2Affine
    // in2.P.X.A0 = c.In2G2.P.X.A0
    // in2.P.X.A1 = c.In2G2.P.X.A1
    // in2.P.Y.A0 = c.In2G2.P.Y.A0
    // in2.P.Y.A1 = c.In2G2.P.Y.A1
    // err = pr.PairingCheck([]*gadget.G1Affine{&c.In1G1, &c.In2G1}, []*gadget.G2Affine{&c.In1G2, &in2})
    // if err != nil {
    //  return fmt.Errorf("pair: %w", err)
    // }

    f, err := emulated.NewField[emparams.BN254Fp](api)
    if err != nil {
        return err
    }
    p := f.Modulus()
    in3XA0 := f.Add(&c.In2G2.P.X.A0, p)
    in3XA1 := f.Add(&c.In2G2.P.X.A1, p)
    in3YA0 := f.Add(&c.In2G2.P.Y.A0, p)
    in3YA1 := f.Add(&c.In2G2.P.Y.A1, p)
    for i := 0; i < 151; i++ {
        in3XA0 = f.Add(in3XA0, p)
        in3XA1 = f.Add(in3XA1, p)
        in3YA0 = f.Add(in3YA0, p)
        in3YA1 = f.Add(in3YA1, p)
    }
    var in3 gadget.G2Affine
    in3.P.X.A0 = *in3XA0
    in3.P.X.A1 = *in3XA1
    in3.P.Y.A0 = *in3YA0
    in3.P.Y.A1 = *in3YA1
    // doesnt work
    err = pr.PairingCheck([]*gadget.G1Affine{&c.In2G1, &c.In1G1}, []*gadget.G2Affine{&in3, &c.In1G2})
    if err != nil {
        return fmt.Errorf("pair: %w", err)
    }
    return nil
}

func TestPairingCheckNonReduced(t *testing.T) {
    assert := test.NewAssert(t)
    p1, q1 := randomG1G2Affines()
    var p2 curve.G1Affine
    p2.Neg(&p1)
    witness := PairingCircuitNonReduced{
        In1G1: gadget.NewG1Affine(p1),
        In1G2: gadget.NewG2Affine(q1),
        In2G1: gadget.NewG1Affine(p2),
        In2G2: gadget.NewG2Affine(q1),
    }
    err := test.IsSolved(&PairingCircuitNonReduced{}, &witness, ecc.BN254.ScalarField())
    assert.NoError(err)
}

The bug only appears when i < 151, if it is less then it doesn't.

And yes, currently I think your workaround to manually reduce works, but it is definitely bug in the field emulation to be fixed. It is a bit subtle though, and it is difficult to avoid creating new issues, so I'll take a bit time to think about it.

ivokub commented 9 months ago

Can you try with https://github.com/Consensys/gnark/pull/1026/commits/14816d5d35c958db8301cbb8fd391b0ba54c8e0e? You can use the version

go get github.com/consensys/gnark@14816d5d35c958db8301cbb8fd391b0ba54c8e0e
ivokub commented 9 months ago

Additionally, we have implemented manual reduction before computing the G2 lines just to be extra safe. But the core problem is still in the field emulation and we'll see if we merge #1026 as is or will improve on it to make AssertIsEqual more efficient (by losing bit shifting and comparison). Can you also check against https://github.com/Consensys/gnark/pull/1027/commits/05c8c62921057dedc8716429c89ca225fd8ff188 if it works?

hussein-aitlahcen commented 9 months ago

Can you try with 14816d5? You can use the version

go get github.com/consensys/gnark@14816d5d35c958db8301cbb8fd391b0ba54c8e0e

Oh wow it's working! Manual reduction is not needed anymore!

hussein-aitlahcen commented 9 months ago

Additionally, we have implemented manual reduction before computing the G2 lines just to be extra safe. But the core problem is still in the field emulation and we'll see if we merge #1026 as is or will improve on it to make AssertIsEqual more efficient (by losing bit shifting and comparison). Can you also check against 05c8c62 if it works?

Can confirm this fix is working as well :+1: