openvm_pairing_guest/halo2curves_shims/bls12_381/
miller_loop.rs

1use alloc::vec::Vec;
2
3use halo2curves_axiom::bls12_381::{Fq, Fq12, Fq2};
4use itertools::izip;
5use openvm_ecc_guest::{
6    algebra::{DivUnsafe, Field},
7    AffinePoint,
8};
9
10use super::Bls12_381;
11use crate::pairing::{
12    Evaluatable, EvaluatedLine, LineMulMType, MillerStep, MultiMillerLoop, UnevaluatedLine,
13};
14
15pub const BLS12_381_SEED_ABS: u64 = 0xd201000000010000;
16// Encodes the Bls12_381 seed, x.
17// x = sum_i BLS12_381_PSEUDO_BINARY_ENCODING[i] * 2^i
18// where BLS12_381_PSEUDO_BINARY_ENCODING[i] is in {-1, 0, 1}
19pub const BLS12_381_PSEUDO_BINARY_ENCODING: [i8; 64] = [
20    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
21    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 1,
22];
23
24#[test]
25fn test_bls12381_pseudo_binary_encoding() {
26    let mut x: i128 = 0;
27    let mut power_of_2 = 1;
28    for b in BLS12_381_PSEUDO_BINARY_ENCODING.iter() {
29        x += (*b as i128) * power_of_2;
30        power_of_2 *= 2;
31    }
32    assert_eq!(x.unsigned_abs(), BLS12_381_SEED_ABS as u128);
33}
34
35impl MillerStep for Bls12_381 {
36    type Fp2 = Fq2;
37
38    /// Miller double step
39    fn miller_double_step(
40        s: &AffinePoint<Self::Fp2>,
41    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
42        let one = &Self::Fp2::ONE;
43        let two = &(one + one);
44        let three = &(one + two);
45
46        let x = &s.x;
47        let y = &s.y;
48        // λ = (3x^2) / (2y)
49        let lambda = &((three * x * x).div_unsafe(&(two * y)));
50        // x_2s = λ^2 - 2x
51        let x_2s = lambda * lambda - two * x;
52        // y_2s = λ(x - x_2s) - y
53        let y_2s = lambda * (x - x_2s) - y;
54        let two_s = AffinePoint { x: x_2s, y: y_2s };
55
56        // Tangent line
57        //   1 + b' (x_P / y_P) w^-1 + c' (1 / y_P) w^-3
58        // where
59        //   l_{\Psi(S),\Psi(S)}(P) = (λ * x_S - y_S) (1 / y_P)  - λ (x_P / y_P) w^2 + w^3
60        // x0 = λ * x_S - y_S
61        // x2 = - λ
62        let b = lambda.neg();
63        let c = lambda * x - y;
64
65        (two_s, UnevaluatedLine { b, c })
66    }
67
68    fn miller_add_step(
69        s: &AffinePoint<Self::Fp2>,
70        q: &AffinePoint<Self::Fp2>,
71    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
72        let x_s = &s.x;
73        let y_s = &s.y;
74        let x_q = &q.x;
75        let y_q = &q.y;
76
77        // λ1 = (y_s - y_q) / (x_s - x_q)
78        let x_delta = x_s - x_q;
79        let lambda = (y_s - y_q).div_unsafe(&x_delta);
80        let x_s_plus_q = lambda * lambda - x_s - x_q;
81        let y_s_plus_q = lambda * (x_q - x_s_plus_q) - y_q;
82
83        let s_plus_q = AffinePoint {
84            x: x_s_plus_q,
85            y: y_s_plus_q,
86        };
87
88        // l_{\Psi(S),\Psi(Q)}(P) = (λ_1 * x_S - y_S) (1 / y_P) - λ_1 (x_P / y_P) w^2 + w^3
89        let b = lambda.neg();
90        let c = lambda * x_s - y_s;
91
92        (s_plus_q, UnevaluatedLine { b, c })
93    }
94
95    /// Miller double and add step (2S + Q implemented as S + Q + S for efficiency)
96    #[allow(clippy::type_complexity)]
97    fn miller_double_and_add_step(
98        s: &AffinePoint<Self::Fp2>,
99        q: &AffinePoint<Self::Fp2>,
100    ) -> (
101        AffinePoint<Self::Fp2>,
102        UnevaluatedLine<Self::Fp2>,
103        UnevaluatedLine<Self::Fp2>,
104    ) {
105        let one = &Self::Fp2::ONE;
106        let two = &(one + one);
107
108        let x_s = &s.x;
109        let y_s = &s.y;
110        let x_q = &q.x;
111        let y_q = &q.y;
112
113        // λ1 = (y_s - y_q) / (x_s - x_q)
114        let lambda1 = &((y_s - y_q).div_unsafe(&(x_s - x_q)));
115        let x_s_plus_q = lambda1 * lambda1 - x_s - x_q;
116
117        // λ2 = -λ1 - 2y_s / (x_{s+q} - x_s)
118        let lambda2 = &(lambda1.neg() - (two * y_s).div_unsafe(&(x_s_plus_q - x_s)));
119        let x_s_plus_q_plus_s = lambda2 * lambda2 - x_s - x_s_plus_q;
120        let y_s_plus_q_plus_s = lambda2 * (x_s - x_s_plus_q_plus_s) - y_s;
121
122        let s_plus_q_plus_s = AffinePoint {
123            x: x_s_plus_q_plus_s,
124            y: y_s_plus_q_plus_s,
125        };
126
127        // l_{\Psi(S),\Psi(Q)}(P) = (λ_1 * x_S - y_S) (1 / y_P) - λ_1 (x_P / y_P) w^2 + w^3
128        let b0 = lambda1.neg();
129        let c0 = lambda1 * x_s - y_s;
130
131        // l_{\Psi(S+Q),\Psi(S)}(P) = (λ_2 * x_S - y_S) (1 / y_P) - λ_2 (x_P / y_P) w^2 + w^3
132        let b1 = lambda2.neg();
133        let c1 = lambda2 * x_s - y_s;
134
135        (
136            s_plus_q_plus_s,
137            UnevaluatedLine { b: b0, c: c0 },
138            UnevaluatedLine { b: b1, c: c1 },
139        )
140    }
141}
142
143#[allow(non_snake_case)]
144impl MultiMillerLoop for Bls12_381 {
145    type Fp = Fq;
146    type Fp12 = Fq12;
147
148    const SEED_ABS: u64 = BLS12_381_SEED_ABS;
149    const PSEUDO_BINARY_ENCODING: &[i8] = &BLS12_381_PSEUDO_BINARY_ENCODING;
150
151    fn evaluate_lines_vec(f: Fq12, lines: Vec<EvaluatedLine<Fq2>>) -> Fq12 {
152        let mut f = f;
153        let mut lines = lines;
154        if lines.len() % 2 == 1 {
155            f = Self::mul_by_023(&f, &lines.pop().unwrap());
156        }
157        for chunk in lines.chunks(2) {
158            if let [line0, line1] = chunk {
159                let prod = Self::mul_023_by_023(line0, line1);
160                f = Self::mul_by_02345(&f, &prod);
161            } else {
162                panic!("lines.len() % 2 should be 0 at this point");
163            }
164        }
165        f
166    }
167
168    /// The expected output of this function when running the Miller loop with embedded exponent is
169    /// c^3 * l_{3Q}
170    fn pre_loop(
171        Q_acc: Vec<AffinePoint<Fq2>>,
172        Q: &[AffinePoint<Fq2>],
173        c: Option<Fq12>,
174        xy_fracs: &[(Fq, Fq)],
175    ) -> (Fq12, Vec<AffinePoint<Fq2>>) {
176        let mut f = if let Some(mut c) = c {
177            // for the miller loop with embedded exponent, f will be set to c at the beginning of
178            // the function, and we will multiply by c again due to the last two values
179            // of the pseudo-binary encoding (BN12_381_PBE) being 1. Therefore, the
180            // final value of f at the end of this block is c^3.
181            let mut c3 = c;
182            c.square_assign();
183            c3 *= &c;
184            c3
185        } else {
186            Self::Fp12::ONE
187        };
188
189        let mut Q_acc = Q_acc;
190
191        // Special case the first iteration of the Miller loop with pseudo_binary_encoding = 1:
192        // this means that the first step is a double and add, but we need to separate the two steps
193        // since the optimized `miller_double_and_add_step` will fail because Q_acc is equal
194        // to Q_signed on the first iteration
195        let (Q_out_double, lines_2S) = Q_acc
196            .into_iter()
197            .map(|Q| Self::miller_double_step(&Q))
198            .unzip::<_, _, Vec<_>, Vec<_>>();
199        Q_acc = Q_out_double;
200
201        let mut initial_lines = Vec::<EvaluatedLine<Fq2>>::new();
202
203        let lines_iter = izip!(lines_2S.iter(), xy_fracs.iter());
204        for (line_2S, xy_frac) in lines_iter {
205            let line = line_2S.evaluate(xy_frac);
206            initial_lines.push(line);
207        }
208
209        let (Q_out_add, lines_S_plus_Q) = Q_acc
210            .iter()
211            .zip(Q.iter())
212            .map(|(Q_acc, Q)| Self::miller_add_step(Q_acc, Q))
213            .unzip::<_, _, Vec<_>, Vec<_>>();
214        Q_acc = Q_out_add;
215
216        let lines_iter = izip!(lines_S_plus_Q.iter(), xy_fracs.iter());
217        for (lines_S_plus_Q, xy_frac) in lines_iter {
218            let line = lines_S_plus_Q.evaluate(xy_frac);
219            initial_lines.push(line);
220        }
221
222        f = Self::evaluate_lines_vec(f, initial_lines);
223
224        (f, Q_acc)
225    }
226
227    /// After running the main body of the Miller loop, we conjugate f due to the curve seed x being
228    /// negative.
229    fn post_loop(
230        f: &Fq12,
231        Q_acc: Vec<AffinePoint<Fq2>>,
232        _Q: &[AffinePoint<Fq2>],
233        _c: Option<Fq12>,
234        _xy_fracs: &[(Fq, Fq)],
235    ) -> (Fq12, Vec<AffinePoint<Fq2>>) {
236        // Conjugate for negative component of the seed
237        // Explanation:
238        // The general Miller loop formula implies that f_{-x} = 1/f_x. To avoid an inversion, we
239        // use the fact that for the final exponentiation, we only need the Miller loop
240        // result up to multiplication by some proper subfield of Fp12. Using the fact that
241        // Fp12 is a quadratic extension of Fp6, we have that f_x * conjugate(f_x) * 1/f_x lies in
242        // Fp6. Therefore we conjugate f_x instead of taking the inverse.
243        let f = f.conjugate();
244        (f, Q_acc)
245    }
246}
openvm_pairing_guest/halo2curves_shims/bls12_381/miller_loop.rs

openvm_pairing_guest/halo2curves_shims/bls12_381/
miller_loop.rs
