openvm_pairing_guest/halo2curves_shims/bn254/
final_exp.rs

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

openvm_pairing_guest/halo2curves_shims/bn254/
final_exp.rs
