openvm_pairing_guest/pairing/
miller_step.rs

Help
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 solutions in Fp2.
51    /// The curve G1Affine and twist G2Affine are both chosen for bn254, bls12_381 so that this never happens.
52    fn miller_double_step(
53        s: &AffinePoint<Self::Fp2>,
54    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
55        let two: &Self::Fp2 = &<P as PairingIntrinsics>::FP2_TWO;
56        let three: &Self::Fp2 = &<P as PairingIntrinsics>::FP2_THREE;
57
58        let x = &s.x;
59        let y = &s.y;
60        // λ = (3x^2) / (2y)
61        let lambda = &((three * x * x).div_unsafe(&(two * y)));
62        // x_2s = λ^2 - 2x
63        let x_2s = lambda * lambda - two * x;
64        // y_2s = λ(x - x_2s) - y
65        let y_2s = lambda * &(x - &x_2s) - y;
66        let two_s = AffinePoint { x: x_2s, y: y_2s };
67
68        // l_{\Psi(S),\Psi(S)}(P)
69        let b = Self::Fp2::ZERO - lambda;
70        let c = lambda * x - y;
71
72        (two_s, UnevaluatedLine { b, c })
73    }
74
75    /// Miller add step.
76    /// Returns S+Q and a line in Fp12 passing through \Psi(S) and \Psi(Q).
77    fn miller_add_step(
78        s: &AffinePoint<Self::Fp2>,
79        q: &AffinePoint<Self::Fp2>,
80    ) -> (AffinePoint<Self::Fp2>, UnevaluatedLine<Self::Fp2>) {
81        let x_s = &s.x;
82        let y_s = &s.y;
83        let x_q = &q.x;
84        let y_q = &q.y;
85
86        // λ1 = (y_s - y_q) / (x_s - x_q)
87        let x_delta = x_s - x_q;
88        let lambda = &((y_s - y_q).div_unsafe(&x_delta));
89        let x_s_plus_q = lambda * lambda - x_s - x_q;
90        let y_s_plus_q = lambda * &(x_q - &x_s_plus_q) - y_q;
91
92        let s_plus_q = AffinePoint {
93            x: x_s_plus_q,
94            y: y_s_plus_q,
95        };
96
97        // l_{\Psi(S),\Psi(Q)}(P)
98        let b = Self::Fp2::ZERO - lambda;
99        let c = lambda * x_s - y_s;
100
101        (s_plus_q, UnevaluatedLine { b, c })
102    }
103
104    /// Miller double and add step (2S + Q implemented as S + Q + S for efficiency).
105    /// Returns 2S+Q, a line in Fp12 passing through S and Q, and a line in Fp12 passing through S+Q and S
106    /// Assumption: Q != +- S && (S+Q) != +-S, so that there is no division by zero.
107    /// The way this is used in miller loop, this is always satisfied.
108    fn miller_double_and_add_step(
109        s: &AffinePoint<Self::Fp2>,
110        q: &AffinePoint<Self::Fp2>,
111    ) -> (
112        AffinePoint<Self::Fp2>,
113        UnevaluatedLine<Self::Fp2>,
114        UnevaluatedLine<Self::Fp2>,
115    ) {
116        let two = &Self::FP2_TWO;
117
118        let x_s = &s.x;
119        let y_s = &s.y;
120        let x_q = &q.x;
121        let y_q = &q.y;
122
123        // λ1 = (y_s - y_q) / (x_s - x_q)
124        let lambda1 = &((y_s - y_q).div_unsafe(&(x_s - x_q)));
125        let x_s_plus_q = lambda1 * lambda1 - x_s - x_q;
126
127        // λ2 = -λ1 - 2y_s / (x_{s+q} - x_s)
128        let lambda2 =
129            &(Self::Fp2::ZERO - lambda1.clone() - (two * y_s).div_unsafe(&(&x_s_plus_q - x_s)));
130        let x_s_plus_q_plus_s = lambda2 * lambda2 - x_s - &x_s_plus_q;
131        let y_s_plus_q_plus_s = lambda2 * &(x_s - &x_s_plus_q_plus_s) - y_s;
132
133        let s_plus_q_plus_s = AffinePoint {
134            x: x_s_plus_q_plus_s,
135            y: y_s_plus_q_plus_s,
136        };
137
138        // l_{\Psi(S),\Psi(Q)}(P)
139        let b0 = Self::Fp2::ZERO - lambda1;
140        let c0 = lambda1 * x_s - y_s;
141
142        // l_{\Psi(S+Q),\Psi(S)}(P)
143        let b1 = Self::Fp2::ZERO - lambda2;
144        let c1 = lambda2 * x_s - y_s;
145
146        (
147            s_plus_q_plus_s,
148            UnevaluatedLine { b: b0, c: c0 },
149            UnevaluatedLine { b: b1, c: c1 },
150        )
151    }
152}
openvm_pairing_guest/pairing/miller_step.rs

openvm_pairing_guest/pairing/
miller_step.rs
