openvm_pairing_guest/pairing/
miller_step.rs

1use core::ops::{Add, Mul, Neg, Sub};
2
3use openvm_algebra_guest::{DivUnsafe, Field};
4use openvm_ecc_guest::AffinePoint;
5
6use super::{PairingIntrinsics, UnevaluatedLine};
7
8/// Trait definition for Miller step opcodes
9pub trait MillerStep {
10    type Fp2;
11
12    /// Miller double step
13    fn miller_double_step(
14        s: &AffinePoint<Self::Fp2>,
15    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>);
16
17    /// Miller add step
18    fn miller_add_step(
19        s: &AffinePoint<Self::Fp2>,
20        q: &AffinePoint<Self::Fp2>,
21    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>);
22
23    /// Miller double and add step (2S + Q implemented as S + Q + S for efficiency)
24    #[allow(clippy::type_complexity)]
25    fn miller_double_and_add_step(
26        s: &AffinePoint<Self::Fp2>,
27        q: &AffinePoint<Self::Fp2>,
28    ) -> (
29        AffinePoint<Self::Fp2>,
30        UnevaluatedLine<Self::Fp2>,
31        UnevaluatedLine<Self::Fp2>,
32    );
33}
34
35impl<P> MillerStep for P
36where
37    P: PairingIntrinsics,
38    for<'a> &'a P::Fp2: Add<&'a P::Fp2, Output = P::Fp2>,
39    for<'a> &'a P::Fp2: Sub<&'a P::Fp2, Output = P::Fp2>,
40    for<'a> &'a P::Fp2: Mul<&'a P::Fp2, Output = P::Fp2>,
41    for<'a> &'a P::Fp2: Neg<Output = P::Fp2>,
42{
43    type Fp2 = <P as PairingIntrinsics>::Fp2;
44
45    /// Miller double step.
46    /// Returns 2S and a line in Fp12 tangent to \Psi(S).
47    /// Assumptions:
48    ///     - s is not point at infinity.
49    ///     - a in the curve equation is 0.
50    /// The case y = 0 does not happen as long as the curve satisfies that 0 = X^3 + b has no
51    /// solutions in Fp2. The curve G1Affine and twist G2Affine are both chosen for bn254,
52    /// bls12_381 so that this never happens.
53    fn miller_double_step(
54        s: &AffinePoint<Self::Fp2>,
55    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
56        let two: &Self::Fp2 = &<P as PairingIntrinsics>::FP2_TWO;
57        let three: &Self::Fp2 = &<P as PairingIntrinsics>::FP2_THREE;
58
59        let x = &s.x;
60        let y = &s.y;
61        // λ = (3x^2) / (2y)
62        let lambda = &((three * x * x).div_unsafe(&(two * y)));
63        // x_2s = λ^2 - 2x
64        let x_2s = lambda * lambda - two * x;
65        // y_2s = λ(x - x_2s) - y
66        let y_2s = lambda * &(x - &x_2s) - y;
67        let two_s = AffinePoint { x: x_2s, y: y_2s };
68
69        // l_{\Psi(S),\Psi(S)}(P)
70        let b = Self::Fp2::ZERO - lambda;
71        let c = lambda * x - y;
72
73        (two_s, UnevaluatedLine { b, c })
74    }
75
76    /// Miller add step.
77    /// Returns S+Q and a line in Fp12 passing through \Psi(S) and \Psi(Q).
78    fn miller_add_step(
79        s: &AffinePoint<Self::Fp2>,
80        q: &AffinePoint<Self::Fp2>,
81    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
82        let x_s = &s.x;
83        let y_s = &s.y;
84        let x_q = &q.x;
85        let y_q = &q.y;
86
87        // λ1 = (y_s - y_q) / (x_s - x_q)
88        let x_delta = x_s - x_q;
89        let lambda = &((y_s - y_q).div_unsafe(&x_delta));
90        let x_s_plus_q = lambda * lambda - x_s - x_q;
91        let y_s_plus_q = lambda * &(x_q - &x_s_plus_q) - y_q;
92
93        let s_plus_q = AffinePoint {
94            x: x_s_plus_q,
95            y: y_s_plus_q,
96        };
97
98        // l_{\Psi(S),\Psi(Q)}(P)
99        let b = Self::Fp2::ZERO - lambda;
100        let c = lambda * x_s - y_s;
101
102        (s_plus_q, UnevaluatedLine { b, c })
103    }
104
105    /// Miller double and add step (2S + Q implemented as S + Q + S for efficiency).
106    /// Returns 2S+Q, a line in Fp12 passing through S and Q, and a line in Fp12 passing through S+Q
107    /// and S Assumption: Q != +- S && (S+Q) != +-S, so that there is no division by zero.
108    /// The way this is used in miller loop, this is always satisfied.
109    fn miller_double_and_add_step(
110        s: &AffinePoint<Self::Fp2>,
111        q: &AffinePoint<Self::Fp2>,
112    ) -> (
113        AffinePoint<Self::Fp2>,
114        UnevaluatedLine<Self::Fp2>,
115        UnevaluatedLine<Self::Fp2>,
116    ) {
117        let two = &Self::FP2_TWO;
118
119        let x_s = &s.x;
120        let y_s = &s.y;
121        let x_q = &q.x;
122        let y_q = &q.y;
123
124        // λ1 = (y_s - y_q) / (x_s - x_q)
125        let lambda1 = &((y_s - y_q).div_unsafe(&(x_s - x_q)));
126        let x_s_plus_q = lambda1 * lambda1 - x_s - x_q;
127
128        // λ2 = -λ1 - 2y_s / (x_{s+q} - x_s)
129        let lambda2 =
130            &(Self::Fp2::ZERO - lambda1.clone() - (two * y_s).div_unsafe(&(&x_s_plus_q - x_s)));
131        let x_s_plus_q_plus_s = lambda2 * lambda2 - x_s - &x_s_plus_q;
132        let y_s_plus_q_plus_s = lambda2 * &(x_s - &x_s_plus_q_plus_s) - y_s;
133
134        let s_plus_q_plus_s = AffinePoint {
135            x: x_s_plus_q_plus_s,
136            y: y_s_plus_q_plus_s,
137        };
138
139        // l_{\Psi(S),\Psi(Q)}(P)
140        let b0 = Self::Fp2::ZERO - lambda1;
141        let c0 = lambda1 * x_s - y_s;
142
143        // l_{\Psi(S+Q),\Psi(S)}(P)
144        let b1 = Self::Fp2::ZERO - lambda2;
145        let c1 = lambda2 * x_s - y_s;
146
147        (
148            s_plus_q_plus_s,
149            UnevaluatedLine { b: b0, c: c0 },
150            UnevaluatedLine { b: b1, c: c1 },
151        )
152    }
153}
openvm_pairing_guest/pairing/miller_step.rs

openvm_pairing_guest/pairing/
miller_step.rs
