From 7087cd065b06c079b9ad2829acdcef3254c3000f Mon Sep 17 00:00:00 2001
From: Ivo Kubjas <ivo.kubjas@consensys.net>
Date: Tue, 23 Jul 2024 13:34:35 +0200
Subject: [PATCH] refactor: separate fixed circuits used in zkevm (#1217)

---
 std/evmprecompiles/08-bnpairing.go | 73 ++++++++++++++++++++++++------
 1 file changed, 60 insertions(+), 13 deletions(-)

diff --git a/std/evmprecompiles/08-bnpairing.go b/std/evmprecompiles/08-bnpairing.go
index 3f4cac461..4a31e1f05 100644
--- a/std/evmprecompiles/08-bnpairing.go
+++ b/std/evmprecompiles/08-bnpairing.go
@@ -1,30 +1,33 @@
 package evmprecompiles
 
 import (
+	"fmt"
+
 	"github.com/consensys/gnark/frontend"
 	"github.com/consensys/gnark/std/algebra/emulated/sw_bn254"
 )
 
 // ECPair implements [ALT_BN128_PAIRING_CHECK] precompile contract at address 0x08.
 //
-// [ALT_BN128_PAIRING_CHECK]: https://ethereum.github.io/execution-specs/autoapi/ethereum/paris/vm/precompiled_contracts/alt_bn128/index.html#alt-bn128-pairing-check
-//
 // To have a fixed-circuit regardless of the number of inputs, we need 2 fixed circuits:
-// - MillerLoopAndMul:
-// 		A Miller loop of fixed size 1 followed by a multiplication in 𝔽p¹².
-// - MillerLoopAndFinalExpCheck:
-// 		A Miller loop of fixed size 1 followed by a multiplication in 𝔽p¹², and
-// 		a check that the result lies in the same equivalence class as the
-// 		reduced pairing purported to be 1. This check replaces the final
-// 		exponentiation step in-circuit and follows Section 4 of [On Proving
-// 		Pairings] paper by A.  Novakovic and L. Eagen.
-//
-// 		[On Proving Pairings]: https://eprint.iacr.org/2024/640.pdf
+//   - MillerLoopAndMul:
+//     A Miller loop of fixed size 1 followed by a multiplication in 𝔽p¹².
+//   - MillerLoopAndFinalExpCheck:
+//     A Miller loop of fixed size 1 followed by a multiplication in 𝔽p¹², and
+//     a check that the result lies in the same equivalence class as the
+//     reduced pairing purported to be 1. This check replaces the final
+//     exponentiation step in-circuit and follows Section 4 of [On Proving
+//     Pairings] paper by A. Novakovic and L. Eagen.
 //
 // N.B.: This is a sub-optimal routine but defines a fixed circuit regardless
 // of the number of inputs.  We can extend this routine to handle a 2-by-2
 // logic but we prefer a minimal number of circuits (2).
-
+//
+// See the methods [ECPairMillerLoopAndMul] and [ECPairMillerLoopAndFinalExpCheck] for the fixed circuits.
+// See the method [ECPairIsOnG2] for the check that Qᵢ are on G2.
+//
+// [ALT_BN128_PAIRING_CHECK]: https://ethereum.github.io/execution-specs/autoapi/ethereum/paris/vm/precompiled_contracts/alt_bn128/index.html#alt-bn128-pairing-check
+// [On Proving Pairings]: https://eprint.iacr.org/2024/640.pdf
 func ECPair(api frontend.API, P []*sw_bn254.G1Affine, Q []*sw_bn254.G2Affine) {
 	if len(P) != len(Q) {
 		panic("P and Q length mismatch")
@@ -56,3 +59,47 @@ func ECPair(api frontend.API, P []*sw_bn254.G1Affine, Q []*sw_bn254.G2Affine) {
 	// fixed circuit 2
 	pair.AssertMillerLoopAndFinalExpIsOne(P[n-1], Q[n-1], ml)
 }
+
+// ECPairIsOnG2 implements the fixed circuit for checking G2 membership and non-membership.
+func ECPairIsOnG2(api frontend.API, Q *sw_bn254.G2Affine, expectedIsOnG2 frontend.Variable) error {
+	pairing, err := sw_bn254.NewPairing(api)
+	if err != nil {
+		return err
+	}
+	isOnG2 := pairing.IsOnG2(Q)
+	api.AssertIsEqual(expectedIsOnG2, isOnG2)
+	return nil
+}
+
+// ECPairMillerLoopAndMul implements the fixed circuit for a Miller loop of
+// fixed size 1 followed by a multiplication with an accumulator in 𝔽p¹². It
+// asserts that the result corresponds to the expected result.
+func ECPairMillerLoopAndMul(api frontend.API, accumulator *sw_bn254.GTEl, P *sw_bn254.G1Affine, Q *sw_bn254.G2Affine, expected *sw_bn254.GTEl) error {
+	pairing, err := sw_bn254.NewPairing(api)
+	if err != nil {
+		return fmt.Errorf("new pairing: %w", err)
+	}
+	pairing.AssertIsOnG2(Q)
+	ml, err := pairing.MillerLoopAndMul(P, Q, accumulator)
+	if err != nil {
+		return fmt.Errorf("miller loop and mul: %w", err)
+	}
+	pairing.AssertIsEqual(expected, ml)
+	return nil
+}
+
+// ECPairMillerLoopAndFinalExpCheck implements the fixed circuit for a Miller
+// loop of fixed size 1 followed by a multiplication with an accumulator in
+// 𝔽p¹², and a check that the result corresponds to the expected result.
+func ECPairMillerLoopAndFinalExpCheck(api frontend.API, accumulator *sw_bn254.GTEl, P *sw_bn254.G1Affine, Q *sw_bn254.G2Affine, expectedIsSuccess frontend.Variable) error {
+	api.AssertIsBoolean(expectedIsSuccess)
+	pairing, err := sw_bn254.NewPairing(api)
+	if err != nil {
+		return fmt.Errorf("new pairing: %w", err)
+	}
+	pairing.AssertIsOnG2(Q)
+
+	isSuccess := pairing.IsMillerLoopAndFinalExpOne(P, Q, accumulator)
+	api.AssertIsEqual(expectedIsSuccess, isSuccess)
+	return nil
+}