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 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 let lambda = &((three * x * x).div_unsafe(&(two * y)));
33 let x_2s = lambda * lambda - two * x;
35 let y_2s = lambda * (x - x_2s) - y;
37 let two_s = AffinePoint { x: x_2s, y: y_2s };
38
39 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 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 let b = lambda.neg();
73 let c = lambda * x_s - y_s;
74
75 (s_plus_q, UnevaluatedLine { b, c })
76 }
77
78 #[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 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 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 let b0 = lambda1.neg();
112 let c0 = lambda1 * x_s - y_s;
113
114 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 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}