openvm_pairing_guest/halo2curves_shims/bn254/
miller_loop.rs

1use alloc::vec::Vec;
2
3use halo2curves_axiom::bn256::{Fq, Fq12, Fq2, FROBENIUS_COEFF_FQ6_C1, XI_TO_Q_MINUS_1_OVER_2};
4use itertools::izip;
5use openvm_ecc_guest::{
6    algebra::{field::FieldExtension, DivUnsafe, Field},
7    AffinePoint,
8};
9
10use super::Bn254;
11use crate::pairing::{
12    Evaluatable, EvaluatedLine, LineMulDType, MillerStep, MultiMillerLoop, UnevaluatedLine,
13};
14
15pub const BN254_SEED: u64 = 0x44e992b44a6909f1;
16// Encodes 6x+2 where x is the BN254 seed.
17// 6*x+2 = sum_i BN254_PSEUDO_BINARY_ENCODING[i] * 2^i
18// where BN254_PSEUDO_BINARY_ENCODING[i] is in {-1, 0, 1}
19pub const BN254_PSEUDO_BINARY_ENCODING: [i8; 66] = [
20    0, 0, 0, 1, 0, 1, 0, -1, 0, 0, -1, 0, 0, 0, 1, 0, 0, -1, 0, -1, 0, 0, 0, 1, 0, -1, 0, 0, 0, 0,
21    -1, 0, 0, 1, 0, -1, 0, 0, 1, 0, 0, 0, 0, 0, -1, 0, 0, -1, 0, 1, 0, -1, 0, 0, 0, -1, 0, -1, 0,
22    0, 0, 1, 0, -1, 0, 1,
23];
24
25#[test]
26fn test_bn254_pseudo_binary_encoding() {
27    let mut x: i128 = 0;
28    let mut power_of_2 = 1;
29    for b in BN254_PSEUDO_BINARY_ENCODING.iter() {
30        x += (*b as i128) * power_of_2;
31        power_of_2 *= 2;
32    }
33    assert_eq!(x.unsigned_abs(), 6 * (BN254_SEED as u128) + 2);
34}
35
36impl MillerStep for Bn254 {
37    type Fp2 = Fq2;
38
39    /// Miller double step
40    fn miller_double_step(
41        s: &AffinePoint<Self::Fp2>,
42    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
43        let one = &Self::Fp2::ONE;
44        let two = &(one + one);
45        let three = &(one + two);
46
47        let x = &s.x;
48        let y = &s.y;
49        // λ = (3x^2) / (2y)
50        let lambda = &((three * x * x).div_unsafe(&(two * y)));
51        // x_2s = λ^2 - 2x
52        let x_2s = lambda * lambda - two * x;
53        // y_2s = λ(x - x_2s) - y
54        let y_2s = lambda * (x - x_2s) - y;
55        let two_s = AffinePoint { x: x_2s, y: y_2s };
56
57        // Tangent line
58        //   1 + b' (x_P / y_P) w^-1 + c' (1 / y_P) w^-3
59        // where
60        //   l_{\Psi(S),\Psi(S)}(P) = (λ * x_S - y_S) (1 / y_P)  - λ (x_P / y_P) w^2 + w^3
61        // x0 = λ * x_S - y_S
62        // x2 = - λ
63        let b = lambda.neg();
64        let c = lambda * x - y;
65
66        (two_s, UnevaluatedLine { b, c })
67    }
68
69    fn miller_add_step(
70        s: &AffinePoint<Self::Fp2>,
71        q: &AffinePoint<Self::Fp2>,
72    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
73        let x_s = &s.x;
74        let y_s = &s.y;
75        let x_q = &q.x;
76        let y_q = &q.y;
77
78        // λ1 = (y_s - y_q) / (x_s - x_q)
79        let x_delta = x_s - x_q;
80        let lambda = (y_s - y_q).div_unsafe(&x_delta);
81        let x_s_plus_q = lambda * lambda - x_s - x_q;
82        let y_s_plus_q = lambda * (x_q - x_s_plus_q) - y_q;
83
84        let s_plus_q = AffinePoint {
85            x: x_s_plus_q,
86            y: y_s_plus_q,
87        };
88
89        // l_{\Psi(S),\Psi(Q)}(P) = (λ_1 * x_S - y_S) (1 / y_P) - λ_1 (x_P / y_P) w^2 + w^3
90        let b = lambda.neg();
91        let c = lambda * x_s - y_s;
92
93        (s_plus_q, UnevaluatedLine { b, c })
94    }
95
96    /// Miller double and add step (2S + Q implemented as S + Q + S for efficiency)
97    #[allow(clippy::type_complexity)]
98    fn miller_double_and_add_step(
99        s: &AffinePoint<Self::Fp2>,
100        q: &AffinePoint<Self::Fp2>,
101    ) -> (
102        AffinePoint<Self::Fp2>,
103        UnevaluatedLine<Self::Fp2>,
104        UnevaluatedLine<Self::Fp2>,
105    ) {
106        let one = &Self::Fp2::ONE;
107        let two = &(one + one);
108
109        let x_s = &s.x;
110        let y_s = &s.y;
111        let x_q = &q.x;
112        let y_q = &q.y;
113
114        // λ1 = (y_s - y_q) / (x_s - x_q)
115        let lambda1 = &((y_s - y_q).div_unsafe(&(x_s - x_q)));
116        let x_s_plus_q = lambda1 * lambda1 - x_s - x_q;
117
118        // λ2 = -λ1 - 2y_s / (x_{s+q} - x_s)
119        let lambda2 = &(lambda1.neg() - (two * y_s).div_unsafe(&(x_s_plus_q - x_s)));
120        let x_s_plus_q_plus_s = lambda2 * lambda2 - x_s - x_s_plus_q;
121        let y_s_plus_q_plus_s = lambda2 * (x_s - x_s_plus_q_plus_s) - y_s;
122
123        let s_plus_q_plus_s = AffinePoint {
124            x: x_s_plus_q_plus_s,
125            y: y_s_plus_q_plus_s,
126        };
127
128        // l_{\Psi(S),\Psi(Q)}(P) = (λ_1 * x_S - y_S) (1 / y_P) - λ_1 (x_P / y_P) w^2 + w^3
129        let b0 = lambda1.neg();
130        let c0 = lambda1 * x_s - y_s;
131
132        // l_{\Psi(S+Q),\Psi(S)}(P) = (λ_2 * x_S - y_S) (1 / y_P) - λ_2 (x_P / y_P) w^2 + w^3
133        let b1 = lambda2.neg();
134        let c1 = lambda2 * x_s - y_s;
135
136        (
137            s_plus_q_plus_s,
138            UnevaluatedLine { b: b0, c: c0 },
139            UnevaluatedLine { b: b1, c: c1 },
140        )
141    }
142}
143
144#[allow(non_snake_case)]
145impl MultiMillerLoop for Bn254 {
146    type Fp = Fq;
147    type Fp12 = Fq12;
148
149    const SEED_ABS: u64 = BN254_SEED;
150    const PSEUDO_BINARY_ENCODING: &[i8] = &BN254_PSEUDO_BINARY_ENCODING;
151
152    fn evaluate_lines_vec(f: Fq12, lines: Vec<EvaluatedLine<Fq2>>) -> Fq12 {
153        let mut f = f;
154        let mut lines = lines;
155        if lines.len() % 2 == 1 {
156            f = Self::mul_by_013(&f, &lines.pop().unwrap());
157        }
158        for chunk in lines.chunks(2) {
159            if let [line0, line1] = chunk {
160                let prod = Self::mul_013_by_013(line0, line1);
161                f = Self::mul_by_01234(&f, &prod);
162            } else {
163                panic!("lines.len() % 2 should be 0 at this point");
164            }
165        }
166        f
167    }
168
169    fn pre_loop(
170        Q_acc: Vec<AffinePoint<Fq2>>,
171        _Q: &[AffinePoint<Fq2>],
172        c: Option<Fq12>,
173        xy_fracs: &[(Fq, Fq)],
174    ) -> (Fq12, Vec<AffinePoint<Fq2>>) {
175        let mut f = if let Some(mut c) = c {
176            c.square_assign();
177            c
178        } else {
179            Self::Fp12::ONE
180        };
181
182        let mut Q_acc = Q_acc;
183        let mut initial_lines = Vec::<EvaluatedLine<Fq2>>::new();
184
185        let (Q_out_double, lines_2S) = Q_acc
186            .into_iter()
187            .map(|Q| Self::miller_double_step(&Q))
188            .unzip::<_, _, Vec<_>, Vec<_>>();
189        Q_acc = Q_out_double;
190
191        let lines_iter = izip!(lines_2S.iter(), xy_fracs.iter());
192        for (line_2S, xy_frac) in lines_iter {
193            let line = line_2S.evaluate(xy_frac);
194            initial_lines.push(line);
195        }
196
197        f = Self::evaluate_lines_vec(f, initial_lines);
198
199        (f, Q_acc)
200    }
201
202    fn post_loop(
203        f: &Fq12,
204        Q_acc: Vec<AffinePoint<Fq2>>,
205        Q: &[AffinePoint<Fq2>],
206        _c: Option<Fq12>,
207        xy_fracs: &[(Fq, Fq)],
208    ) -> (Fq12, Vec<AffinePoint<Fq2>>) {
209        let mut Q_acc = Q_acc;
210        let mut lines = Vec::<EvaluatedLine<Fq2>>::new();
211
212        let x_to_q_minus_1_over_3 = FROBENIUS_COEFF_FQ6_C1[1];
213        let x_to_q_sq_minus_1_over_3 = FROBENIUS_COEFF_FQ6_C1[2];
214        let q1_vec = Q
215            .iter()
216            .map(|Q| {
217                let x = Q.x.frobenius_map(1);
218                let x = x * x_to_q_minus_1_over_3;
219                let y = Q.y.frobenius_map(1);
220                let y = y * XI_TO_Q_MINUS_1_OVER_2;
221                AffinePoint { x, y }
222            })
223            .collect::<Vec<_>>();
224
225        let (Q_out_add, lines_S_plus_Q) = Q_acc
226            .iter()
227            .zip(q1_vec.iter())
228            .map(|(Q_acc, q1)| Self::miller_add_step(Q_acc, q1))
229            .unzip::<_, _, Vec<_>, Vec<_>>();
230        Q_acc = Q_out_add;
231
232        let lines_iter = izip!(lines_S_plus_Q.iter(), xy_fracs.iter());
233        for (lines_S_plus_Q, xy_frac) in lines_iter {
234            let line = lines_S_plus_Q.evaluate(xy_frac);
235            lines.push(line);
236        }
237
238        let q2_vec = Q
239            .iter()
240            .map(|Q| {
241                // There is a frobenius mapping π²(Q) that we skip here since it is equivalent to
242                // the identity mapping
243                let x = Q.x * x_to_q_sq_minus_1_over_3;
244                AffinePoint { x, y: Q.y }
245            })
246            .collect::<Vec<_>>();
247
248        let (Q_out_add, lines_S_plus_Q) = Q_acc
249            .iter()
250            .zip(q2_vec.iter())
251            .map(|(Q_acc, q2)| Self::miller_add_step(Q_acc, q2))
252            .unzip::<_, _, Vec<_>, Vec<_>>();
253        Q_acc = Q_out_add;
254
255        let lines_iter = izip!(lines_S_plus_Q.iter(), xy_fracs.iter());
256        for (lines_S_plus_Q, xy_frac) in lines_iter {
257            let line = lines_S_plus_Q.evaluate(xy_frac);
258            lines.push(line);
259        }
260
261        let mut f = *f;
262        f = Self::evaluate_lines_vec(f, lines);
263
264        (f, Q_acc)
265    }
266}