openvm_pairing_guest/halo2curves_shims/bls12_381/
final_exp.rs

1use halo2curves_axiom::bls12_381::{Fq, Fq12, Fq2};
2use num_bigint::BigUint;
3use openvm_ecc_guest::{
4    algebra::{ExpBytes, Field},
5    AffinePoint,
6};
7
8use super::{Bls12_381, FINAL_EXP_FACTOR, LAMBDA, POLY_FACTOR};
9use crate::pairing::{FinalExp, MultiMillerLoop};
10
11// The paper only describes the implementation for Bn254, so we use the gnark implementation for Bls12_381.
12#[allow(non_snake_case)]
13impl FinalExp for Bls12_381 {
14    type Fp = Fq;
15    type Fp2 = Fq2;
16    type Fp12 = Fq12;
17
18    // Adapted from the gnark implementation:
19    // https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bls12381/e12_pairing.go#L394C1-L395C1
20    fn assert_final_exp_is_one(
21        f: &Self::Fp12,
22        P: &[AffinePoint<Self::Fp>],
23        Q: &[AffinePoint<Self::Fp2>],
24    ) {
25        let (c, s) = Self::final_exp_hint(f);
26
27        // The gnark implementation checks that f * s = c^{q - x} where x is the curve seed.
28        // We check an equivalent condition: f * c^x * c^-q * s = 1.
29        // This is because we can compute f * c^x by embedding the c^x computation in the miller loop.
30
31        // Since the Bls12_381 curve has a negative seed, the miller loop for Bls12_381 is computed as
32        // f_{Miller,x,Q}(P) = conjugate( f_{Miller,-x,Q}(P) * c^{-x} ).
33        // We will pass in the conjugate inverse of c into the miller loop so that we compute
34        // fc = f_{Miller,x,Q}(P)
35        //    = conjugate( f_{Miller,-x,Q}(P) * c'^{-x} )  (where c' is the conjugate inverse of c)
36        //    = f_{Miller,x,Q}(P) * c^x
37        let c_conj_inv = c.conjugate().invert().unwrap();
38        let c_inv = c.invert().unwrap();
39        let c_q_inv = c_inv.frobenius_map();
40        let fc = Self::multi_miller_loop_embedded_exp(P, Q, Some(c_conj_inv));
41
42        assert_eq!(fc * c_q_inv * s, Fq12::ONE);
43    }
44
45    // Adapted from the gnark implementation:
46    // https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bls12381/hints.go#L273
47    // returns c (residueWitness) and s (scalingFactor)
48    // The Gnark implementation is based on https://eprint.iacr.org/2024/640.pdf
49    fn final_exp_hint(f: &Self::Fp12) -> (Self::Fp12, Self::Fp12) {
50        // 1. get p-th root inverse
51        let mut exp = FINAL_EXP_FACTOR.clone() * BigUint::from(27u32);
52        let mut root = f.exp_bytes(true, &exp.to_bytes_be());
53        let root_pth_inv: Fq12;
54        if root == Fq12::ONE {
55            root_pth_inv = Fq12::ONE;
56        } else {
57            let exp_inv = exp.modinv(&POLY_FACTOR.clone()).unwrap();
58            exp = exp_inv % POLY_FACTOR.clone();
59            root_pth_inv = root.exp_bytes(false, &exp.to_bytes_be());
60        }
61
62        // 2.1. get order of 3rd primitive root
63        let three = BigUint::from(3u32);
64        let mut order_3rd_power: u32 = 0;
65        exp = POLY_FACTOR.clone() * FINAL_EXP_FACTOR.clone();
66
67        root = f.exp_bytes(true, &exp.to_bytes_be());
68        let three_be = three.to_bytes_be();
69        // NOTE[yj]: we can probably remove this first check as an optimization since we initizlize order_3rd_power to 0
70        if root == Fq12::ONE {
71            order_3rd_power = 0;
72        }
73        root = root.exp_bytes(true, &three_be);
74        if root == Fq12::ONE {
75            order_3rd_power = 1;
76        }
77        root = root.exp_bytes(true, &three_be);
78        if root == Fq12::ONE {
79            order_3rd_power = 2;
80        }
81        root = root.exp_bytes(true, &three_be);
82        if root == Fq12::ONE {
83            order_3rd_power = 3;
84        }
85
86        // 2.2. get 27th root inverse
87        let root_27th_inv: Fq12;
88        if order_3rd_power == 0 {
89            root_27th_inv = Fq12::ONE;
90        } else {
91            let order_3rd = three.pow(order_3rd_power);
92            exp = POLY_FACTOR.clone() * FINAL_EXP_FACTOR.clone();
93            root = f.exp_bytes(true, &exp.to_bytes_be());
94            let exp_inv = exp.modinv(&order_3rd).unwrap();
95            exp = exp_inv % order_3rd;
96            root_27th_inv = root.exp_bytes(false, &exp.to_bytes_be());
97        }
98
99        // 2.3. shift the Miller loop result so that millerLoop * scalingFactor
100        // is of order finalExpFactor
101        let s = root_pth_inv * root_27th_inv;
102        let f = f * s;
103
104        // 3. get the witness residue
105        // lambda = q - u, the optimal exponent
106        exp = LAMBDA.clone().modinv(&FINAL_EXP_FACTOR.clone()).unwrap();
107        let c = f.exp_bytes(true, &exp.to_bytes_be());
108
109        (c, s)
110    }
111}