CVE-2026-46669

@@ -322,6 +322,14 @@ impl Bls12_381 {
         Q: &[AffinePoint<<Self as PairingCheck>::Fp2>],
     ) -> Option<Result<(), PairingCheckError>> {
         let (c, s) = Self::pairing_check_hint(P, Q);
+        // Hint is only honest if `s` lies in proper subfield Fp6. Matches <https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bls12381/e12_pairing.go#L413>
+        // The Fp6 representation is `fp6_c0 = [s.c[0], s.c[2], s.c[4]]` and `fp6_c1 = [s.c[1],
+        // s.c[3], s.c[5]]`.
+        for i in [1, 3, 5] {
+            if s.c[i] != Fp2::ZERO {
+                return None;
+            }
+        }
 
         // The gnark implementation checks that f * s = c^{q - x} where x is the curve seed.
         // We check an equivalent condition: f * c^x * s = c^q.

@@ -1,6 +1,7 @@
 use group::ff::Field;
 use halo2curves_axiom::bls12_381::{
-    Fq, Fq12, Fq2, Fq6, G1Affine, G2Affine, G2Prepared, MillerLoopResult, FROBENIUS_COEFF_FQ12_C1,
+    Fq, Fq12, Fq2, Fq6, Fr, G1Affine, G2Affine, G2Prepared, MillerLoopResult,
+    FROBENIUS_COEFF_FQ12_C1,
 };
 use num_bigint::BigUint;
 use num_traits::One;
@@ -300,6 +301,34 @@ fn test_bls12381_pairing_check_hint_host() {
     assert_eq!(s, s_cmp);
 }
 
+#[allow(non_snake_case)]
+#[test]
+fn test_bad_hint_fails_subfield_host() {
+    let S = G1Affine::generator();
+    let Q = G2Affine::generator();
+
+    let S_mul = [
+        G1Affine::from(S * Fr::from(1)),
+        G1Affine::from(S * Fr::from(2)),
+    ];
+    let Q_mul = [
+        G2Affine::from(Q * Fr::from(2)),
+        G2Affine::from(Q * Fr::from(1)),
+    ];
+
+    let s = S_mul.map(|s| AffinePoint::new(s.x, s.y));
+    let q = Q_mul.map(|p| AffinePoint::new(p.x, p.y));
+    // Pairing check should **not** pass for this
+    // We check that c = 1, s = f^{-1} will not pass the subfield check
+    let f =
+        openvm_pairing_guest::halo2curves_shims::bls12_381::Bls12_381::multi_miller_loop(&s, &q);
+    let s_halo2 = f.invert().unwrap();
+    let s = convert_bls12381_halo2_fq12_to_fp12(s_halo2);
+    let subfield_check = s.c[1] == Fp2::ZERO && s.c[3] == Fp2::ZERO && s.c[5] == Fp2::ZERO;
+    assert_eq!(subfield_check, bool::from(s_halo2.c1.is_zero()));
+    assert!(!subfield_check);
+}
+
 #[test]
 fn test_bls12381_final_exponent() {
     let final_exp = (BLS12_381_MODULUS.pow(12) - BigUint::one()) / BLS12_381_ORDER.clone();

@@ -356,6 +356,14 @@ impl Bn254 {
         if c == Fp12::ZERO {
             return None;
         }
+        // Hint is only honest if `u` lies in proper subfield Fp6. Matches <https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bn254/e12_pairing.go#L450>
+        // The Fp6 representation is `fp6_c0 = [s.c[0], s.c[2], s.c[4]]` and `fp6_c1 = [s.c[1],
+        // s.c[3], s.c[5]]`.
+        for i in [1, 3, 5] {
+            if u.c[i] != Fp2::ZERO {
+                return None;
+            }
+        }
         let c_inv = Fp12::ONE.div_unsafe(&c);
 
         // We follow Theorem 3 of https://eprint.iacr.org/2024/640.pdf to check that the pairing equals 1

@@ -1,6 +1,6 @@
 use group::{ff::Field, prime::PrimeCurveAffine};
 use halo2curves_axiom::bn256::{
-    Fq, Fq12, Fq2, Fq6, G1Affine, G2Affine, G2Prepared, Gt, FROBENIUS_COEFF_FQ12_C1,
+    Fq, Fq12, Fq2, Fq6, Fr, G1Affine, G2Affine, G2Prepared, Gt, FROBENIUS_COEFF_FQ12_C1,
     FROBENIUS_COEFF_FQ6_C1, XI_TO_Q_MINUS_1_OVER_2,
 };
 use num_bigint::BigUint;
@@ -287,6 +287,33 @@ fn test_bn254_pairing_check_hint_host() {
     assert_eq!(u, u_cmp);
 }
 
+#[allow(non_snake_case)]
+#[test]
+fn test_bad_hint_fails_subfield_host() {
+    let S = G1Affine::generator();
+    let Q = G2Affine::generator();
+
+    let S_mul = [
+        G1Affine::from(S * Fr::from(1)),
+        G1Affine::from(S * Fr::from(2)),
+    ];
+    let Q_mul = [
+        G2Affine::from(Q * Fr::from(2)),
+        G2Affine::from(Q * Fr::from(1)),
+    ];
+
+    let s = S_mul.map(|s| AffinePoint::new(s.x, s.y));
+    let q = Q_mul.map(|p| AffinePoint::new(p.x, p.y));
+    // Pairing check should **not** pass for this
+    // We check that c = 1, u = f^{-1} will not pass the subfield check
+    let f = openvm_pairing_guest::halo2curves_shims::bn254::Bn254::multi_miller_loop(&s, &q);
+    let u_halo2 = f.invert().unwrap();
+    let u = convert_bn254_halo2_fq12_to_fp12(u_halo2);
+    let subfield_check = u.c[1] == Fp2::ZERO && u.c[3] == Fp2::ZERO && u.c[5] == Fp2::ZERO;
+    assert_eq!(subfield_check, bool::from(u_halo2.c1.is_zero()));
+    assert!(!subfield_check);
+}
+
 #[test]
 fn test_bn254_final_exponent() {
     let final_exp = (BN254_MODULUS.pow(12) - BigUint::one()) / BN254_ORDER.clone();

@@ -61,30 +61,37 @@ mod bn254 {
             P: &[AffinePoint<<Self as PairingCheck>::Fp>],
             Q: &[AffinePoint<<Self as PairingCheck>::Fp2>],
         ) -> Option<Result<(), PairingCheckError>> {
-            let (c, s) = Self::pairing_check_hint(P, Q);
-
-            // f * s = c^{q - x}
-            // f * s = c^q * c^-x
-            // f * c^x * c^-q * s = 1,
-            //   where fc = f * c'^x (embedded Miller loop with c conjugate inverse),
-            //   and the curve seed x = -0xd201000000010000
-            //   the miller loop computation includes a conjugation at the end because the value of
-            // the   seed is negative, so we need to conjugate the miller loop input c
-            // as c'. We then substitute   y = -x to get c^-y and finally compute c'^-y
-            // as input to the miller loop: f * c'^-y * c^-q * s = 1
-            let c_q = FieldExtension::frobenius_map(&c, 1);
-            let c_conj = c.conjugate();
-            if c_conj == Fp12::ZERO {
+            let (c, u) = Self::pairing_check_hint(P, Q);
+            if c == Fp12::ZERO {
                 return None;
             }
-            let c_conj_inv = Fp12::ONE.div_unsafe(&c_conj);
+            // Hint is only honest if `u` lies in proper subfield Fp6. Matches <https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bn254/e12_pairing.go#L450>
+            // The Fp6 representation is `fp6_c0 = [s.c[0], s.c[2], s.c[4]]` and `fp6_c1 = [s.c[1],
+            // s.c[3], s.c[5]]`.
+            for i in [1, 3, 5] {
+                if u.c[i] != Fp2::ZERO {
+                    return None;
+                }
+            }
+            let c_inv = Fp12::ONE.div_unsafe(&c);
 
-            // fc = f_{Miller,x,Q}(P) * c^{x}
-            // where
-            //   fc = conjugate( f_{Miller,-x,Q}(P) * c'^{-x} ), with c' denoting the conjugate of c
-            let fc = Bn254::multi_miller_loop_embedded_exp(P, Q, Some(c_conj_inv));
+            // We follow Theorem 3 of https://eprint.iacr.org/2024/640.pdf to check that the pairing equals 1
+            // By the theorem, it suffices to provide c and u such that f * u == c^λ.
+            // Since λ = 6x + 2 + q^3 - q^2 + q, we will check the equivalent condition:
+            // f * c^-{6x + 2} * u * c^-{q^3 - q^2 + q} == 1
+            // This is because we can compute f * c^-{6x+2} by embedding the c^-{6x+2} computation
+            // in the miller loop.
 
-            if fc * s == c_q {
+            // c_mul = c^-{q^3 - q^2 + q}
+            let c_q3_inv = FieldExtension::frobenius_map(&c_inv, 3);
+            let c_q2 = FieldExtension::frobenius_map(&c, 2);
+            let c_q_inv = FieldExtension::frobenius_map(&c_inv, 1);
+            let c_mul = c_q3_inv * c_q2 * c_q_inv;
+
+            // Pass c inverse into the miller loop so that we compute fc == f * c^-{6x + 2}
+            let fc = Bn254::multi_miller_loop_embedded_exp(P, Q, Some(c_inv));
+
+            if fc * c_mul * u == Fp12::ONE {
                 Some(Ok(()))
             } else {
                 None
@@ -172,26 +179,33 @@ mod bls12_381 {
             Q: &[AffinePoint<<Self as PairingCheck>::Fp2>],
         ) -> Option<Result<(), PairingCheckError>> {
             let (c, s) = Self::pairing_check_hint(P, Q);
+            // Hint is only honest if `s` lies in proper subfield Fp6. Matches <https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bls12381/e12_pairing.go#L413>
+            // The Fp6 representation is `fp6_c0 = [s.c[0], s.c[2], s.c[4]]` and `fp6_c1 = [s.c[1],
+            // s.c[3], s.c[5]]`.
+            for i in [1, 3, 5] {
+                if s.c[i] != Fp2::ZERO {
+                    return None;
+                }
+            }
 
-            // f * s = c^{q - x}
-            // f * s = c^q * c^-x
-            // f * c^x * c^-q * s = 1,
-            //   where fc = f * c'^x (embedded Miller loop with c conjugate inverse),
-            //   and the curve seed x = -0xd201000000010000
-            //   the miller loop computation includes a conjugation at the end because the value of
-            // the   seed is negative, so we need to conjugate the miller loop input c
-            // as c'. We then substitute   y = -x to get c^-y and finally compute c'^-y
-            // as input to the miller loop: f * c'^-y * c^-q * s = 1
+            // The gnark implementation checks that f * s = c^{q - x} where x is the curve seed.
+            // We check an equivalent condition: f * c^x * s = c^q.
+            // This is because we can compute f * c^x by embedding the c^x computation in the miller
+            // loop.
+
+            // We compute c^q before c is consumed by conjugate() below
             let c_q = FieldExtension::frobenius_map(&c, 1);
+
+            // Since the Bls12_381 curve has a negative seed, the miller loop for Bls12_381 is
+            // computed as f_{Miller,x,Q}(P) = conjugate( f_{Miller,-x,Q}(P) * c^{-x} ).
+            // We will pass in the conjugate inverse of c into the miller loop so that we compute
+            // fc = conjugate( f_{Miller,-x,Q}(P) * c'^{-x} )  (where c' is the conjugate inverse of
+            // c)    = f_{Miller,x,Q}(P) * c^x
             let c_conj = c.conjugate();
             if c_conj == Fp12::ZERO {
                 return None;
             }
             let c_conj_inv = Fp12::ONE.div_unsafe(&c_conj);
-
-            // fc = f_{Miller,x,Q}(P) * c^{x}
-            // where
-            //   fc = conjugate( f_{Miller,-x,Q}(P) * c'^{-x} ), with c' denoting the conjugate of c
             let fc = Bls12_381::multi_miller_loop_embedded_exp(P, Q, Some(c_conj_inv));
 
             if fc * s == c_q {