From ecc6fe320c9e42e0eb92ebdf9650402ce27462e1 Mon Sep 17 00:00:00 2001
From: FlashW <flashwayne00@gmail.com>
Date: Mon, 28 Sep 2026 14:25:06 -0300
Subject: [PATCH] fix(sw_bls12377): accept the G1 point at infinity in the
 pairing

MillerLoop and PairingCheck compute DivUnchecked(1, P.Y), which has no
solution for the G1 point at infinity (0,0), so e(0,Q) = 1 can't be proven
with the native BLS12-377 pairing. Select yInv = 0 when Y is zero, which
makes the line evaluations for that point equal to 1.
---
 internal/stats/latest_stats.csv               |  4 +-
 std/algebra/native/sw_bls12377/pairing.go     | 13 +++++-
 .../native/sw_bls12377/pairing_test.go        | 43 +++++++++++++++++++
 3 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/internal/stats/latest_stats.csv b/internal/stats/latest_stats.csv
index 446f8949bd..14cd3f4b36 100644
--- a/internal/stats/latest_stats.csv
+++ b/internal/stats/latest_stats.csv
@@ -103,8 +103,8 @@ math/emulated/secp256k1_64,bn254,plonk,5136,5009
 math/emulated/secp256k1_64,bls12_377,plonk,5136,5009
 math/emulated/secp256k1_64,bls12_381,plonk,5136,5009
 math/emulated/secp256k1_64,bw6_761,plonk,4682,4567
-pairing_bls12377,bw6_761,groth16,12046,12046
-pairing_bls12377,bw6_761,plonk,38271,37663
+pairing_bls12377,bw6_761,groth16,12050,12050
+pairing_bls12377,bw6_761,plonk,38278,37670
 pairing_bls12381,bn254,groth16,1322686,2141587
 pairing_bls12381,bn254,plonk,4878525,4684904
 pairing_bn254,bn254,groth16,836345,1354248
diff --git a/std/algebra/native/sw_bls12377/pairing.go b/std/algebra/native/sw_bls12377/pairing.go
index 7a745492a6..556e0fe79f 100644
--- a/std/algebra/native/sw_bls12377/pairing.go
+++ b/std/algebra/native/sw_bls12377/pairing.go
@@ -59,7 +59,7 @@ func millerLoopLines(api frontend.API, P []G1Affine, lines []lineEvaluations) (G
 	yInv := make([]frontend.Variable, n)
 	xNegOverY := make([]frontend.Variable, n)
 	for k := 0; k < n; k++ {
-		yInv[k] = api.DivUnchecked(1, P[k].Y)
+		yInv[k] = invYWithInfinityGuard(api, P[k].Y)
 		xNegOverY[k] = api.Mul(P[k].X, yInv[k])
 		xNegOverY[k] = api.Neg(xNegOverY[k])
 	}
@@ -316,7 +316,7 @@ func PairingCheck(api frontend.API, P []G1Affine, Q []G2Affine) error {
 	yInv := make([]frontend.Variable, nP)
 	xNegOverY := make([]frontend.Variable, nP)
 	for k := 0; k < nP; k++ {
-		yInv[k] = api.DivUnchecked(1, P[k].Y)
+		yInv[k] = invYWithInfinityGuard(api, P[k].Y)
 		xNegOverY[k] = api.Mul(P[k].X, yInv[k])
 		xNegOverY[k] = api.Neg(xNegOverY[k])
 	}
@@ -511,3 +511,12 @@ func divE2WithZeroGuard(api frontend.API, n, d fields_bls12377.E2) fields_bls123
 	res.Select(api, dIsZero, zero, l)
 	return res
 }
+
+// invYWithInfinityGuard returns 1/y, or 0 when y is 0. The G1 point at infinity
+// is represented as (0,0) and setting yInv to 0 makes its line evaluations
+// equal to 1, so the point doesn't contribute to the Miller loop.
+func invYWithInfinityGuard(api frontend.API, y frontend.Variable) frontend.Variable {
+	isYZero := api.IsZero(y)
+	y = api.Select(isYZero, 1, y)
+	return api.Select(isYZero, 0, api.DivUnchecked(1, y))
+}
diff --git a/std/algebra/native/sw_bls12377/pairing_test.go b/std/algebra/native/sw_bls12377/pairing_test.go
index 62f9462325..40f03e4fe9 100644
--- a/std/algebra/native/sw_bls12377/pairing_test.go
+++ b/std/algebra/native/sw_bls12377/pairing_test.go
@@ -202,6 +202,49 @@ func TestPairingCheckBLS377(t *testing.T) {
 
 }
 
+type pairingG1InfinityBLS377 struct {
+	P1, P2 G1Affine
+	Q1, Q2 G2Affine
+	Res    GT
+}
+
+func (circuit *pairingG1InfinityBLS377) Define(api frontend.API) error {
+	res, err := Pair(api, []G1Affine{circuit.P1, circuit.P2}, []G2Affine{circuit.Q1, circuit.Q2})
+	if err != nil {
+		return fmt.Errorf("pair: %w", err)
+	}
+	res.AssertIsEqual(api, circuit.Res)
+	return nil
+}
+
+func TestPairingG1InfinityBLS377(t *testing.T) {
+	assert := test.NewAssert(t)
+	_, _, _, g2 := bls12377.Generators()
+	P, Q, _, _ := pairingData()
+	var infinity bls12377.G1Affine
+
+	// e(0,g2) * e(P,Q) == e(P,Q)
+	res, err := bls12377.Pair([]bls12377.G1Affine{infinity, P}, []bls12377.G2Affine{g2, Q})
+	assert.NoError(err)
+	witness := pairingG1InfinityBLS377{
+		P1:  NewG1Affine(infinity),
+		P2:  NewG1Affine(P),
+		Q1:  NewG2Affine(g2),
+		Q2:  NewG2Affine(Q),
+		Res: NewGTEl(res),
+	}
+	assert.CheckCircuit(&pairingG1InfinityBLS377{}, test.WithValidAssignment(&witness), test.WithCurves(ecc.BW6_761), test.NoProverChecks())
+
+	// e(0,g2) * e(0,Q) == 1
+	witnessCheck := pairingCheckBLS377{
+		P1: NewG1Affine(infinity),
+		P2: NewG1Affine(infinity),
+		Q1: NewG2Affine(g2),
+		Q2: NewG2Affine(Q),
+	}
+	assert.CheckCircuit(&pairingCheckBLS377{}, test.WithValidAssignment(&witnessCheck), test.WithCurves(ecc.BW6_761), test.NoProverChecks())
+}
+
 type groupMembership struct {
 	P G1Affine
 	Q G2Affine