openvm_pairing_guest/bls12_381/
pairing.rs

1use alloc::vec::Vec;
2
3use itertools::izip;
4use openvm_algebra_guest::{
5    field::{ComplexConjugate, FieldExtension},
6    DivUnsafe, Field,
7};
8use openvm_ecc_guest::AffinePoint;
9#[cfg(target_os = "zkvm")]
10use {
11    crate::{PairingBaseFunct7, OPCODE, PAIRING_FUNCT3},
12    core::mem::MaybeUninit,
13    openvm_platform::custom_insn_r,
14    openvm_rv32im_guest,
15    openvm_rv32im_guest::hint_buffer_u32,
16};
17
18use super::{Bls12_381, Fp, Fp12, Fp2, BLS12_381_PSEUDO_BINARY_ENCODING, BLS12_381_SEED_ABS};
19use crate::pairing::{
20    exp_check_fallback, Evaluatable, EvaluatedLine, FromLineMType, LineMulMType, MillerStep,
21    MultiMillerLoop, PairingCheck, PairingCheckError, PairingIntrinsics, UnevaluatedLine,
22};
23#[cfg(all(feature = "halo2curves", not(target_os = "zkvm")))]
24use crate::{
25    bls12_381::utils::{
26        convert_bls12381_fp2_to_halo2_fq2, convert_bls12381_fp_to_halo2_fq,
27        convert_bls12381_halo2_fq12_to_fp12,
28    },
29    halo2curves_shims::bls12_381::Bls12_381 as Halo2CurvesBls12_381,
30    pairing::FinalExp,
31};
32
33impl Evaluatable<Fp, Fp2> for UnevaluatedLine<Fp2> {
34    fn evaluate(&self, xy_frac: &(Fp, Fp)) -> EvaluatedLine<Fp2> {
35        let (x_over_y, y_inv) = xy_frac;
36        // Represents the line L(x,y) = 1 + b (x/y) w^-1 + c (1/y) w^-3
37        EvaluatedLine {
38            b: self.b.mul_base(x_over_y),
39            c: self.c.mul_base(y_inv),
40        }
41    }
42}
43
44impl FromLineMType<Fp2> for Fp12 {
45    // Since multiplying by w^3 doesn't change the miller loop result, we transform the line
46    // into L_new(x,y) = w^3 L(x,y) = w^3 + b (x/y) w^2 + c (1/y)
47    fn from_evaluated_line_m_type(line: EvaluatedLine<Fp2>) -> Fp12 {
48        Fp12::from_coeffs([line.c, Fp2::ZERO, line.b, Fp2::ONE, Fp2::ZERO, Fp2::ZERO])
49    }
50}
51
52// TODO[jpw]: make this into a macro depending on P::PAIRING_IDX when we have more curves
53impl LineMulMType<Fp2, Fp12> for Bls12_381 {
54    /// Multiplies two lines in 023-form to get an element in 02345-form
55    fn mul_023_by_023(l0: &EvaluatedLine<Fp2>, l1: &EvaluatedLine<Fp2>) -> [Fp2; 5] {
56        // l0 = c0 + b0 w^2 + w^3
57        let b0 = &l0.b;
58        let c0 = &l0.c;
59        // l1 = c1 + b1 w^2 + w^3
60        let b1 = &l1.b;
61        let c1 = &l1.c;
62
63        // where w⁶ = xi
64        // l0 * l1 = c0c1 + (c0b1 + c1b0)w² + (c0 + c1)w³ + (b0b1)w⁴ + (b0 +b1)w⁵ + w⁶
65        //         = (c0c1 + xi) + (c0b1 + c1b0)w² + (c0 + c1)w³ + (b0b1)w⁴ + (b0 + b1)w⁵
66        let x0 = c0 * c1 + Bls12_381::XI;
67        let x2 = c0 * b1 + c1 * b0;
68        let x3 = c0 + c1;
69        let x4 = b0 * b1;
70        let x5 = b0 + b1;
71
72        [x0, x2, x3, x4, x5]
73    }
74
75    /// Multiplies a line in 02345-form with a Fp12 element to get an Fp12 element
76    fn mul_by_023(f: &Fp12, l: &EvaluatedLine<Fp2>) -> Fp12 {
77        // this is only used if the number of lines is odd, which doesn't happen for our
78        // applications right now, so we can use this suboptimal implementation
79        Fp12::from_evaluated_line_m_type(l.clone()) * f
80    }
81
82    /// Multiplies a line in 02345-form with a Fp12 element to get an Fp12 element
83    fn mul_by_02345(f: &Fp12, x: &[Fp2; 5]) -> Fp12 {
84        // we update the order of the coefficients to match the Fp12 coefficient ordering:
85        // Fp12 {
86        //   c0: Fp6 {
87        //     c0: x0,
88        //     c1: x2,
89        //     c2: x4,
90        //   },
91        //   c1: Fp6 {
92        //     c0: x1,
93        //     c1: x3,
94        //     c2: x5,
95        //   },
96        // }
97        let o0 = &x[0]; // coeff x0
98        let o1 = &x[1]; // coeff x2
99        let o2 = &x[3]; // coeff x4
100        let o4 = &x[2]; // coeff x3
101        let o5 = &x[4]; // coeff x5
102
103        let xi = &Bls12_381::XI;
104
105        let self_coeffs = &f.c;
106        let s0 = &self_coeffs[0];
107        let s1 = &self_coeffs[2];
108        let s2 = &self_coeffs[4];
109        let s3 = &self_coeffs[1];
110        let s4 = &self_coeffs[3];
111        let s5 = &self_coeffs[5];
112
113        // NOTE[yj]: Hand-calculated multiplication for Fp12 * 02345 ∈ Fp2; this is likely not the
114        // most efficient implementation c00 = cs0co0 + xi(cs1co2 + cs2co1 + cs3co5 +
115        // cs4co4) c01 = cs0co1 + cs1co0 + xi(cs2co2 + cs4co5 + cs5co4)
116        // c02 = cs0co2 + cs1co1 + cs2co0 + cs3co4 + xi(cs5co5)
117        // c10 = cs3co0 + xi(cs1co5 + cs2co4 + cs4co2 + cs5co1)
118        // c11 = cs0co4 + cs3co1 + cs4co0 + xi(cs2co5 + cs5co2)
119        // c12 = cs0co5 + cs1co4 + cs3co2 + cs4co1 + cs5co0
120        //   where cs*: self.c*
121        let c00 = s0 * o0 + xi * &(s1 * o2 + s2 * o1 + s3 * o5 + s4 * o4);
122        let c01 = s0 * o1 + s1 * o0 + xi * &(s2 * o2 + s4 * o5 + s5 * o4);
123        let c02 = s0 * o2 + s1 * o1 + s2 * o0 + s3 * o4 + xi * &(s5 * o5);
124        let c10 = s3 * o0 + xi * &(s1 * o5 + s2 * o4 + s4 * o2 + s5 * o1);
125        let c11 = s0 * o4 + s3 * o1 + s4 * o0 + xi * &(s2 * o5 + s5 * o2);
126        let c12 = s0 * o5 + s1 * o4 + s3 * o2 + s4 * o1 + s5 * o0;
127
128        Fp12::from_coeffs([c00, c10, c01, c11, c02, c12])
129    }
130}
131
132#[allow(non_snake_case)]
133impl MultiMillerLoop for Bls12_381 {
134    type Fp = Fp;
135    type Fp12 = Fp12;
136
137    const SEED_ABS: u64 = BLS12_381_SEED_ABS;
138    const PSEUDO_BINARY_ENCODING: &[i8] = &BLS12_381_PSEUDO_BINARY_ENCODING;
139
140    fn evaluate_lines_vec(f: Self::Fp12, lines: Vec<EvaluatedLine<Self::Fp2>>) -> Self::Fp12 {
141        let mut f = f;
142        let mut lines = lines;
143        if lines.len() % 2 == 1 {
144            f = Self::mul_by_023(&f, &lines.pop().unwrap());
145        }
146        for chunk in lines.chunks(2) {
147            if let [line0, line1] = chunk {
148                let prod = Self::mul_023_by_023(line0, line1);
149                f = Self::mul_by_02345(&f, &prod);
150            } else {
151                panic!("lines.len() % 2 should be 0 at this point");
152            }
153        }
154        f
155    }
156
157    /// The expected output of this function when running the Miller loop with embedded exponent is
158    /// c^3 * l_{3Q}
159    fn pre_loop(
160        Q_acc: Vec<AffinePoint<Self::Fp2>>,
161        Q: &[AffinePoint<Self::Fp2>],
162        c: Option<Self::Fp12>,
163        xy_fracs: &[(Self::Fp, Self::Fp)],
164    ) -> (Self::Fp12, Vec<AffinePoint<Self::Fp2>>) {
165        let mut f = if let Some(mut c) = c {
166            // for the miller loop with embedded exponent, f will be set to c at the beginning of
167            // the function, and we will multiply by c again due to the last two values
168            // of the pseudo-binary encoding (BLS12_381_PSEUDO_BINARY_ENCODING) being 1.
169            // Therefore, the final value of f at the end of this block is c^3.
170            let mut c3 = c.clone();
171            c.square_assign();
172            c3 *= &c;
173            c3
174        } else {
175            Self::Fp12::ONE
176        };
177
178        let mut Q_acc = Q_acc;
179
180        // Special case the first iteration of the Miller loop with pseudo_binary_encoding = 1:
181        // this means that the first step is a double and add, but we need to separate the two steps
182        // since the optimized `miller_double_and_add_step` will fail because Q_acc is equal
183        // to Q_signed on the first iteration
184        let (Q_out_double, lines_2S) = Q_acc
185            .into_iter()
186            .map(|Q| Self::miller_double_step(&Q))
187            .unzip::<_, _, Vec<_>, Vec<_>>();
188        Q_acc = Q_out_double;
189
190        let mut initial_lines = Vec::<EvaluatedLine<Self::Fp2>>::new();
191
192        let lines_iter = izip!(lines_2S.iter(), xy_fracs.iter());
193        for (line_2S, xy_frac) in lines_iter {
194            let line = line_2S.evaluate(xy_frac);
195            initial_lines.push(line);
196        }
197
198        let (Q_out_add, lines_S_plus_Q) = Q_acc
199            .iter()
200            .zip(Q.iter())
201            .map(|(Q_acc, Q)| Self::miller_add_step(Q_acc, Q))
202            .unzip::<_, _, Vec<_>, Vec<_>>();
203        Q_acc = Q_out_add;
204
205        let lines_iter = izip!(lines_S_plus_Q.iter(), xy_fracs.iter());
206        for (lines_S_plus_Q, xy_frac) in lines_iter {
207            let line = lines_S_plus_Q.evaluate(xy_frac);
208            initial_lines.push(line);
209        }
210
211        f = Self::evaluate_lines_vec(f, initial_lines);
212
213        (f, Q_acc)
214    }
215
216    /// After running the main body of the Miller loop, we conjugate f due to the curve seed x being
217    /// negative.
218    fn post_loop(
219        f: &Self::Fp12,
220        Q_acc: Vec<AffinePoint<Self::Fp2>>,
221        _Q: &[AffinePoint<Self::Fp2>],
222        _c: Option<Self::Fp12>,
223        _xy_fracs: &[(Self::Fp, Self::Fp)],
224    ) -> (Self::Fp12, Vec<AffinePoint<Self::Fp2>>) {
225        // Conjugate for negative component of the seed
226        // By Lemma 1 from https://www.iacr.org/archive/eurocrypt2011/66320047/66320047.pdf f_{x,Q} = conjugate( f_{|x|,Q} )
227        let mut f = f.clone();
228        f.conjugate_assign();
229        (f, Q_acc)
230    }
231}
232
233#[allow(non_snake_case)]
234impl PairingCheck for Bls12_381 {
235    type Fp = Fp;
236    type Fp2 = Fp2;
237    type Fp12 = Fp12;
238
239    #[allow(unused_variables)]
240    fn pairing_check_hint(
241        P: &[AffinePoint<Self::Fp>],
242        Q: &[AffinePoint<Self::Fp2>],
243    ) -> (Self::Fp12, Self::Fp12) {
244        #[cfg(not(target_os = "zkvm"))]
245        {
246            #[cfg(not(feature = "halo2curves"))]
247            panic!("`halo2curves` feature must be enabled to use pairing check hint on host");
248
249            #[cfg(feature = "halo2curves")]
250            {
251                let p_halo2 = P
252                    .iter()
253                    .map(|p| {
254                        AffinePoint::new(
255                            convert_bls12381_fp_to_halo2_fq(p.x.clone()),
256                            convert_bls12381_fp_to_halo2_fq(p.y.clone()),
257                        )
258                    })
259                    .collect::<Vec<_>>();
260                let q_halo2 = Q
261                    .iter()
262                    .map(|q| {
263                        AffinePoint::new(
264                            convert_bls12381_fp2_to_halo2_fq2(q.x.clone()),
265                            convert_bls12381_fp2_to_halo2_fq2(q.y.clone()),
266                        )
267                    })
268                    .collect::<Vec<_>>();
269                let fq12 = Halo2CurvesBls12_381::multi_miller_loop(&p_halo2, &q_halo2);
270                let (c_fq12, s_fq12) = Halo2CurvesBls12_381::final_exp_hint(&fq12);
271                let c = convert_bls12381_halo2_fq12_to_fp12(c_fq12);
272                let s = convert_bls12381_halo2_fq12_to_fp12(s_fq12);
273                (c, s)
274            }
275        }
276        #[cfg(target_os = "zkvm")]
277        {
278            let hint = MaybeUninit::<(Fp12, Fp12)>::uninit();
279            // We do not rely on the slice P's memory layout since rust does not guarantee it across
280            // compiler versions.
281            let p_fat_ptr = (P.as_ptr() as u32, P.len() as u32);
282            let q_fat_ptr = (Q.as_ptr() as u32, Q.len() as u32);
283            unsafe {
284                custom_insn_r!(
285                    opcode = OPCODE,
286                    funct3 = PAIRING_FUNCT3,
287                    funct7 = ((Bls12_381::PAIRING_IDX as u8) * PairingBaseFunct7::PAIRING_MAX_KINDS + PairingBaseFunct7::HintFinalExp as u8),
288                    rd = Const "x0",
289                    rs1 = In &p_fat_ptr,
290                    rs2 = In &q_fat_ptr
291                );
292                let ptr = hint.as_ptr() as *const u8;
293                hint_buffer_u32!(ptr, (48 * 12 * 2) / 4);
294                hint.assume_init()
295            }
296        }
297    }
298
299    fn pairing_check(
300        P: &[AffinePoint<Self::Fp>],
301        Q: &[AffinePoint<Self::Fp2>],
302    ) -> Result<(), PairingCheckError> {
303        Self::try_honest_pairing_check(P, Q).unwrap_or_else(|| {
304            let f = Self::multi_miller_loop(P, Q);
305            exp_check_fallback(&f, &Self::FINAL_EXPONENT)
306        })
307    }
308}
309
310#[allow(non_snake_case)]
311impl Bls12_381 {
312    // The paper only describes the implementation for Bn254, so we use the gnark implementation for
313    // Bls12_381. Adapted from the gnark implementation:
314    // https://github.com/Consensys/gnark/blob/af754dd1c47a92be375930ae1abfbd134c5310d8/std/algebra/emulated/fields_bls12381/e12_pairing.go#L394C1-L395C1
315    fn try_honest_pairing_check(
316        P: &[AffinePoint<<Self as PairingCheck>::Fp>],
317        Q: &[AffinePoint<<Self as PairingCheck>::Fp2>],
318    ) -> Option<Result<(), PairingCheckError>> {
319        let (c, s) = Self::pairing_check_hint(P, Q);
320
321        // The gnark implementation checks that f * s = c^{q - x} where x is the curve seed.
322        // We check an equivalent condition: f * c^x * s = c^q.
323        // This is because we can compute f * c^x by embedding the c^x computation in the miller
324        // loop.
325
326        // We compute c^q before c is consumed by conjugate() below
327        let c_q = FieldExtension::frobenius_map(&c, 1);
328
329        // Since the Bls12_381 curve has a negative seed, the miller loop for Bls12_381 is computed
330        // as f_{Miller,x,Q}(P) = conjugate( f_{Miller,-x,Q}(P) * c^{-x} ).
331        // We will pass in the conjugate inverse of c into the miller loop so that we compute
332        // fc = conjugate( f_{Miller,-x,Q}(P) * c'^{-x} )  (where c' is the conjugate inverse of c)
333        //    = f_{Miller,x,Q}(P) * c^x
334        let c_conj = c.conjugate();
335        if c_conj == Fp12::ZERO {
336            return None;
337        }
338        let c_conj_inv = Fp12::ONE.div_unsafe(&c_conj);
339        let fc = Self::multi_miller_loop_embedded_exp(P, Q, Some(c_conj_inv));
340
341        if fc * s == c_q {
342            Some(Ok(()))
343        } else {
344            None
345        }
346    }
347}