openvm_pairing_guest/halo2curves_shims/bn254/
final_exp.rs

1use halo2curves_axiom::{
2    bn256::{Fq, Fq12, Fq2},
3    ff::Field,
4};
5use openvm_ecc_guest::{algebra::field::FieldExtension, AffinePoint};
6
7use super::{Bn254, EXP1, EXP2, M_INV, R_INV, U27_COEFF_0, U27_COEFF_1};
8use crate::pairing::{FinalExp, MultiMillerLoop};
9
10#[allow(non_snake_case)]
11impl FinalExp for Bn254 {
12    type Fp = Fq;
13    type Fp2 = Fq2;
14    type Fp12 = Fq12;
15
16    fn assert_final_exp_is_one(
17        f: &Self::Fp12,
18        P: &[AffinePoint<Self::Fp>],
19        Q: &[AffinePoint<Self::Fp2>],
20    ) {
21        let (c, u) = Self::final_exp_hint(f);
22        let c_inv = c.invert().unwrap();
23
24        // We follow Theorem 3 of https://eprint.iacr.org/2024/640.pdf to check that the pairing equals 1
25        // By the theorem, it suffices to provide c and u such that f * u == c^λ.
26        // Since λ = 6x + 2 + q^3 - q^2 + q, we will check the equivalent condition:
27        // f * c^-{6x + 2} * u * c^-{q^3 - q^2 + q} == 1
28        // This is because we can compute f * c^-{6x+2} by embedding the c^-{6x+2} computation in the miller loop.
29
30        // c_mul = c^-{q^3 - q^2 + q}
31        let c_q3_inv = FieldExtension::frobenius_map(&c_inv, 3);
32        let c_q2 = FieldExtension::frobenius_map(&c, 2);
33        let c_q_inv = FieldExtension::frobenius_map(&c_inv, 1);
34        let c_mul = c_q3_inv * c_q2 * c_q_inv;
35
36        // Pass c inverse into the miller loop so that we compute fc == f * c^-{6x + 2}
37        let fc = Self::multi_miller_loop_embedded_exp(P, Q, Some(c_inv));
38
39        assert_eq!(fc * c_mul * u, Fq12::ONE);
40    }
41
42    // Adapted from the Gnark implementation:
43    // https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/sw_bn254/hints.go#L23
44    // returns c (residueWitness) and u (cubicNonResiduePower)
45    // The Gnark implementation is based on https://eprint.iacr.org/2024/640.pdf
46    fn final_exp_hint(f: &Self::Fp12) -> (Self::Fp12, Self::Fp12) {
47        // Residue witness
48        let mut c;
49        // Cubic nonresidue power
50        let u;
51
52        // get the 27th root of unity
53        let u0 = U27_COEFF_0.to_u64_digits();
54        let u1 = U27_COEFF_1.to_u64_digits();
55        let u_coeffs = Fq2::from_coeffs([
56            Fq::from_raw([u0[0], u0[1], u0[2], u0[3]]),
57            Fq::from_raw([u1[0], u1[1], u1[2], u1[3]]),
58        ]);
59        let unity_root_27 = Fq12::from_coeffs([
60            Fq2::ZERO,
61            Fq2::ZERO,
62            u_coeffs,
63            Fq2::ZERO,
64            Fq2::ZERO,
65            Fq2::ZERO,
66        ]);
67        debug_assert_eq!(unity_root_27.pow([27]), Fq12::one());
68
69        if f.pow(EXP1.to_u64_digits()) == Fq12::ONE {
70            c = *f;
71            u = Fq12::ONE;
72        } else {
73            let f_mul_unity_root_27 = f * unity_root_27;
74            if f_mul_unity_root_27.pow(EXP1.to_u64_digits()) == Fq12::ONE {
75                c = f_mul_unity_root_27;
76                u = unity_root_27;
77            } else {
78                c = f_mul_unity_root_27 * unity_root_27;
79                u = unity_root_27.square();
80            }
81        }
82
83        // 1. Compute r-th root and exponentiate to rInv where
84        //   rInv = 1/r mod (p^12-1)/r
85        c = c.pow(R_INV.to_u64_digits());
86
87        // 2. Compute m-th root where
88        //   m = (6x + 2 + q^3 - q^2 +q)/3r
89        // Exponentiate to mInv where
90        //   mInv = 1/m mod p^12-1
91        c = c.pow(M_INV.to_u64_digits());
92
93        // 3. Compute cube root
94        // since gcd(3, (p^12-1)/r) != 1, we use a modified Tonelli-Shanks algorithm
95        // see Alg.4 of https://eprint.iacr.org/2024/640.pdf
96        // Typo in the paper: p^k-1 = 3^n * s instead of p-1 = 3^r * s
97        // where k=12 and n=3 here and exp2 = (s+1)/3
98        let mut x = c.pow(EXP2.to_u64_digits());
99
100        // 3^t is ord(x^3 / residueWitness)
101        let c_inv = c.invert().unwrap();
102        let mut x3 = x.square() * x * c_inv;
103        let mut t = 0;
104        let mut tmp = x3.square();
105
106        // Modified Tonelli-Shanks algorithm for computing the cube root
107        fn tonelli_shanks_loop(x3: &mut Fq12, tmp: &mut Fq12, t: &mut i32) {
108            while *x3 != Fq12::ONE {
109                *tmp = (*x3).square();
110                *x3 *= *tmp;
111                *t += 1;
112            }
113        }
114
115        tonelli_shanks_loop(&mut x3, &mut tmp, &mut t);
116
117        while t != 0 {
118            tmp = unity_root_27.pow(EXP2.to_u64_digits());
119            x *= tmp;
120
121            x3 = x.square() * x * c_inv;
122            t = 0;
123            tonelli_shanks_loop(&mut x3, &mut tmp, &mut t);
124        }
125
126        debug_assert_eq!(c, x * x * x);
127        // x is the cube root of the residue witness c
128        c = x;
129
130        (c, u)
131    }
132}