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