jf_relation/gadgets/ecc/emulated/
short_weierstrass.rs

1// Copyright (c) 2022 Espresso Systems (espressosys.com)
2// This file is part of the Jellyfish library.
3
4// You should have received a copy of the MIT License
5// along with the Jellyfish library. If not, see <https://mit-license.org/>.
6
7//! Short Weierstrass curve point addition
8
9use crate::{
10    gadgets::{from_emulated_field, EmulatedVariable, EmulationConfig, SerializableEmulatedStruct},
11    BoolVar, Circuit, CircuitError, PlonkCircuit,
12};
13use ark_ec::short_weierstrass::{Affine, SWCurveConfig};
14use ark_ff::PrimeField;
15use ark_serialize::{CanonicalDeserialize, CanonicalSerialize};
16use ark_std::{vec, vec::Vec};
17
18/// An elliptic curve point in short Weierstrass affine form (x, y, infinity).
19#[derive(Debug, Eq, PartialEq, Copy, Clone, CanonicalSerialize, CanonicalDeserialize)]
20pub struct SWPoint<F: PrimeField>(pub F, pub F, pub bool);
21
22impl<F: PrimeField> Default for SWPoint<F> {
23    fn default() -> Self {
24        Self(F::zero(), F::zero(), true)
25    }
26}
27
28impl<F, P> From<Affine<P>> for SWPoint<F>
29where
30    F: PrimeField,
31    P: SWCurveConfig<BaseField = F>,
32{
33    fn from(p: Affine<P>) -> Self {
34        SWPoint(p.x, p.y, p.infinity)
35    }
36}
37
38impl<E, F> SerializableEmulatedStruct<F> for SWPoint<E>
39where
40    E: EmulationConfig<F>,
41    F: PrimeField,
42{
43    fn serialize_to_native_elements(&self) -> Vec<F> {
44        let mut result = from_emulated_field(self.0);
45        result.extend(from_emulated_field(self.1));
46        result.push(if self.2 { F::one() } else { F::zero() });
47        result
48    }
49}
50
51/// The variable represents an SW point in the emulated field.
52#[derive(Debug, Clone)]
53pub struct EmulatedSWPointVariable<E: PrimeField>(
54    pub EmulatedVariable<E>,
55    pub EmulatedVariable<E>,
56    pub BoolVar,
57);
58
59impl<F: PrimeField> PlonkCircuit<F> {
60    /// Return the witness point
61    pub fn emulated_sw_point_witness<E: EmulationConfig<F>>(
62        &self,
63        point_var: &EmulatedSWPointVariable<E>,
64    ) -> Result<SWPoint<E>, CircuitError> {
65        let x = self.emulated_witness(&point_var.0)?;
66        let y = self.emulated_witness(&point_var.1)?;
67        let infinity = self.witness(point_var.2 .0)? == F::one();
68        Ok(SWPoint(x, y, infinity))
69    }
70
71    /// Add a new emulated EC point (as witness)
72    pub fn create_emulated_sw_point_variable<E: EmulationConfig<F>>(
73        &mut self,
74        point: SWPoint<E>,
75    ) -> Result<EmulatedSWPointVariable<E>, CircuitError> {
76        let x = self.create_emulated_variable(point.0)?;
77        let y = self.create_emulated_variable(point.1)?;
78        let infinity = self.create_boolean_variable(point.2)?;
79        Ok(EmulatedSWPointVariable(x, y, infinity))
80    }
81
82    /// Add a new constant emulated EC point
83    pub fn create_constant_emulated_sw_point_variable<E: EmulationConfig<F>>(
84        &mut self,
85        point: SWPoint<E>,
86    ) -> Result<EmulatedSWPointVariable<E>, CircuitError> {
87        let x = self.create_constant_emulated_variable(point.0)?;
88        let y = self.create_constant_emulated_variable(point.1)?;
89        let infinity = BoolVar(if point.2 { self.one() } else { self.zero() });
90        Ok(EmulatedSWPointVariable(x, y, infinity))
91    }
92
93    /// Add a new public emulated EC point
94    pub fn create_public_emulated_sw_point_variable<E: EmulationConfig<F>>(
95        &mut self,
96        point: SWPoint<E>,
97    ) -> Result<EmulatedSWPointVariable<E>, CircuitError> {
98        let x = self.create_public_emulated_variable(point.0)?;
99        let y = self.create_public_emulated_variable(point.1)?;
100        let infinity = self.create_public_boolean_variable(point.2)?;
101        Ok(EmulatedSWPointVariable(x, y, infinity))
102    }
103
104    /// Obtain an emulated point variable of the conditional selection from 2
105    /// emulated point variables. `b` is a boolean variable that indicates
106    /// selection of P_b from (P0, P1).
107    /// Return error if invalid input parameters are provided.
108    pub fn binary_emulated_sw_point_vars_select<E: EmulationConfig<F>>(
109        &mut self,
110        b: BoolVar,
111        p0: &EmulatedSWPointVariable<E>,
112        p1: &EmulatedSWPointVariable<E>,
113    ) -> Result<EmulatedSWPointVariable<E>, CircuitError> {
114        let select_x = self.conditional_select_emulated(b, &p0.0, &p1.0)?;
115        let select_y = self.conditional_select_emulated(b, &p0.1, &p1.1)?;
116        let select_infinity = BoolVar(self.conditional_select(b, p0.2 .0, p1.2 .0)?);
117
118        Ok(EmulatedSWPointVariable::<E>(
119            select_x,
120            select_y,
121            select_infinity,
122        ))
123    }
124
125    /// Constrain two emulated point variables to be the same.
126    /// Return error if the input point variables are invalid.
127    pub fn enforce_emulated_sw_point_equal<E: EmulationConfig<F>>(
128        &mut self,
129        p0: &EmulatedSWPointVariable<E>,
130        p1: &EmulatedSWPointVariable<E>,
131    ) -> Result<(), CircuitError> {
132        self.enforce_emulated_var_equal(&p0.0, &p1.0)?;
133        self.enforce_emulated_var_equal(&p0.1, &p1.1)?;
134        self.enforce_equal(p0.2 .0, p1.2 .0)?;
135        Ok(())
136    }
137
138    /// Obtain a bool variable representing whether two input emulated point
139    /// variables are equal. Return error if variables are invalid.
140    pub fn is_emulated_sw_point_equal<E: EmulationConfig<F>>(
141        &mut self,
142        p0: &EmulatedSWPointVariable<E>,
143        p1: &EmulatedSWPointVariable<E>,
144    ) -> Result<BoolVar, CircuitError> {
145        let mut r0 = self.is_emulated_var_equal(&p0.0, &p1.0)?;
146        let r1 = self.is_emulated_var_equal(&p0.1, &p1.1)?;
147        let r2 = self.is_equal(p0.2 .0, p1.2 .0)?;
148        r0.0 = self.mul(r0.0, r1.0)?;
149        r0.0 = self.mul(r0.0, r2.0)?;
150        Ok(r0)
151    }
152
153    /// Constrain variable `p2` to be the point addition of `p0` and
154    /// `p1` over an elliptic curve.
155    /// Let p0 = (x0, y0, inf0), p1 = (x1, y1, inf1), p2 = (x2, y2, inf2)
156    /// The addition formula for affine points of sw curve is as follows:
157    ///
158    /// If either p0 or p1 is infinity, then p2 equals to another point.
159    ///   1. if p0 == p1
160    ///      - if y0 == 0 then inf2 = 1
161    ///      - Calculate s = (3 * x0^2 + a) / (2 * y0)
162    ///      - x2 = s^2 - x0 - x1
163    ///      - y2 = s(x0 - x2) - y0
164    ///   2. Otherwise
165    ///      - if x0 == x1 then inf2 = 1
166    ///      - Calculate s = (y0 - y1) / (x0 - x1)
167    ///      - x2 = s^2 - x0 - x1
168    ///      - y2 = s(x0 - x2) - y0
169    ///
170    /// The first case is equivalent to the following:
171    ///
172    /// - inf0 == 1 || inf1 == 1 || x0 != x1 || y0 != y1 || y0 != 0 || inf2 == 0
173    /// - (x0 + x1 + x2) * (y0 + y0)^2 == (3 * x0^2 + a)^2
174    /// - (y2 + y0) * (y0 + y0) == (3 * x0^2 + a) (x0 - x2)
175    ///
176    /// The second case is equivalent to the following:
177    ///
178    /// - inf0 == 1 || inf1 == 1 || x0 != x1 || y0 == y1 || inf2 == 0
179    /// - (x0 - x1)^2 (x0 + x1 + x2) == (y0 - y1)^2
180    /// - (x0 - x2) (y0 - y1) == (y0 + y2) (x0 - x1)
181    ///
182    /// First check in both cases can be combined into the following:
183    ///
184    /// inf0 == 1 || inf1 == 1 || inf2 == 0 || x0 != x1 || (y0 == y1 && y0 != 0)
185    ///
186    /// For the rest equality checks,
187    ///   - Both LHS and RHS must be multiplied with an indicator variable
188    ///     (!inf0 && !inf1). So that if either p0 or p1 is infinity, those
189    ///     checks will trivially pass.
190    ///   - For the first case (point doubling), both LHS and RHS must be
191    ///     multiplied with an indicator variable (y0 != 0 && x0 == x1 && y1 ==
192    ///     y0). So that when y0 == 0 || x0 != x1 || y0 != y1, these checks will
193    ///     trivially pass.
194    ///   - For the second case, both LHS and RHS must be multiplied with (x0 -
195    ///     x1). So that when x0 == x1, these checks will trivially pass.
196    pub fn emulated_sw_ecc_add_gate<E: EmulationConfig<F>>(
197        &mut self,
198        p0: &EmulatedSWPointVariable<E>,
199        p1: &EmulatedSWPointVariable<E>,
200        p2: &EmulatedSWPointVariable<E>,
201        a: E,
202    ) -> Result<(), CircuitError> {
203        let eq_p1_p2 = self.is_emulated_sw_point_equal(p1, p2)?;
204        let eq_p0_p2 = self.is_emulated_sw_point_equal(p0, p2)?;
205        // Case 1: either p0 or p1 is infinity
206        self.enforce_equal(p0.2 .0, eq_p1_p2.0)?;
207        self.enforce_equal(p1.2 .0, eq_p0_p2.0)?;
208
209        // infinity_mark is 1 iff either p0 or p1 is infinity
210        let infinity_mark = self.logic_or(p0.2, p1.2)?;
211        // is 1 iff both p0 and p1 are not infinity
212        let non_infinity_mark = self.logic_neg(infinity_mark)?;
213
214        // Case 2: p2 is infinity, while p0 and p1 are not.
215        // inf0 == 1 || inf1 == 1 || inf2 == 0 || x0 != x1 || (y0 == y1 && y0 != 0)
216        let non_inf_p2 = self.logic_neg(p2.2)?;
217        let eq_x0_x1 = self.is_emulated_var_equal(&p0.0, &p1.0)?;
218        let neq_x0_x1 = self.logic_neg(eq_x0_x1)?;
219        let eq_y0_y1 = self.is_emulated_var_equal(&p0.1, &p1.1)?;
220        let is_y0_zero = self.is_emulated_var_zero(&p0.1)?;
221        let not_y0_zero = self.logic_neg(is_y0_zero)?;
222        let t = self.logic_and(eq_y0_y1, not_y0_zero)?;
223        let t = self.logic_or(neq_x0_x1, t)?;
224        let t = self.logic_or(non_inf_p2, t)?;
225        self.logic_or_gate(infinity_mark, t)?;
226
227        // Case 3: point doubling
228        // doubling mark is 1 iff x0 == x1 and y0 == y1
229        let doubling_mark = self.mul(eq_x0_x1.0, eq_y0_y1.0)?;
230        let doubling_coef = self.mul(doubling_mark, non_infinity_mark.0)?;
231        let doubling_coef = self.mul(doubling_coef, not_y0_zero.0)?;
232        // forcefully convert Variable into EmulatedVariable
233        // safe because it's boolean
234        let mut v = vec![self.zero(); E::NUM_LIMBS];
235        v[0] = doubling_coef;
236        let doubling_coef = EmulatedVariable::<E>(v, core::marker::PhantomData);
237
238        // first equality (x0 + x1 + x2) * (y0 + y0)^2 == (3 * x1^2 + a)^2
239        let y0_times_2 = self.emulated_add(&p0.1, &p0.1)?;
240        let x0_plus_x1 = self.emulated_add(&p0.0, &p1.0)?;
241        let x0_plus_x1_plus_x2 = self.emulated_add(&p2.0, &x0_plus_x1)?;
242        let lhs = self.emulated_mul(&x0_plus_x1_plus_x2, &y0_times_2)?;
243        let lhs = self.emulated_mul(&lhs, &y0_times_2)?;
244        // s = 3 * x1^2 + a
245        let s = self.emulated_mul(&p0.0, &p0.0)?;
246        let s = self.emulated_mul_constant(&s, E::from(3u64))?;
247        let s = self.emulated_add_constant(&s, a)?;
248        let rhs = self.emulated_mul(&s, &s)?;
249
250        let lhs = self.emulated_mul(&lhs, &doubling_coef)?;
251        let rhs = self.emulated_mul(&rhs, &doubling_coef)?;
252        self.enforce_emulated_var_equal(&lhs, &rhs)?;
253
254        // second equality (y2 + y0) * (y0 + y0) == (3 * x1^2 + a) (x0 - x2)
255        let y2_plus_y0 = self.emulated_add(&p2.1, &p0.1)?;
256        let lhs = self.emulated_mul(&y2_plus_y0, &y0_times_2)?;
257        let x0_minus_x2 = self.emulated_sub(&p0.0, &p2.0)?;
258        let rhs = self.emulated_mul(&s, &x0_minus_x2)?;
259
260        let lhs = self.emulated_mul(&lhs, &doubling_coef)?;
261        let rhs = self.emulated_mul(&rhs, &doubling_coef)?;
262        self.enforce_emulated_var_equal(&lhs, &rhs)?;
263
264        // Case 4: point addition
265        let coef = self.mul(non_infinity_mark.0, neq_x0_x1.0)?;
266        // forcefully convert Variable into EmulatedVariable
267        // safe because it's boolean
268        let mut v = vec![self.zero(); E::NUM_LIMBS];
269        v[0] = coef;
270        let add_coef = EmulatedVariable::<E>(v, core::marker::PhantomData);
271
272        // first equality (x0 - x1)^2 (x0 + x1 + x2) == (y0 - y1)^2
273        let x0_minus_x1 = self.emulated_sub(&p0.0, &p1.0)?;
274        let lhs = self.emulated_mul(&x0_minus_x1, &x0_minus_x1)?;
275        let lhs = self.emulated_mul(&lhs, &x0_plus_x1_plus_x2)?;
276        let y0_minus_y1 = self.emulated_sub(&p0.1, &p1.1)?;
277        let rhs = self.emulated_mul(&y0_minus_y1, &y0_minus_y1)?;
278
279        let lhs = self.emulated_mul(&lhs, &add_coef)?;
280        let rhs = self.emulated_mul(&rhs, &add_coef)?;
281        self.enforce_emulated_var_equal(&lhs, &rhs)?;
282
283        // second equality (x0 - x2) (y0 - y1) == (y0 + y2) (x0 - x1)
284        let lhs = self.emulated_mul(&x0_minus_x2, &y0_minus_y1)?;
285        let y0_plus_y2 = self.emulated_add(&p0.1, &p2.1)?;
286        let rhs = self.emulated_mul(&y0_plus_y2, &x0_minus_x1)?;
287
288        let lhs = self.emulated_mul(&lhs, &add_coef)?;
289        let rhs = self.emulated_mul(&rhs, &add_coef)?;
290        self.enforce_emulated_var_equal(&lhs, &rhs)?;
291
292        Ok(())
293    }
294
295    /// Obtain a variable to the point addition result of `p0` + `p1`
296    pub fn emulated_sw_ecc_add<E: EmulationConfig<F>>(
297        &mut self,
298        p0: &EmulatedSWPointVariable<E>,
299        p1: &EmulatedSWPointVariable<E>,
300        a: E,
301    ) -> Result<EmulatedSWPointVariable<E>, CircuitError> {
302        let x0 = self.emulated_witness(&p0.0)?;
303        let y0 = self.emulated_witness(&p0.1)?;
304        let infinity0 = self.witness(p0.2 .0)? == F::one();
305        let x1 = self.emulated_witness(&p1.0)?;
306        let y1 = self.emulated_witness(&p1.1)?;
307        let infinity1 = self.witness(p1.2 .0)? == F::one();
308        let p2 = if infinity0 {
309            SWPoint(x1, y1, infinity1)
310        } else if infinity1 {
311            SWPoint(x0, y0, infinity0)
312        } else if x0 == x1 && y0 == y1 {
313            // point doubling
314            if y0.is_zero() {
315                SWPoint(E::zero(), E::zero(), true)
316            } else {
317                let s = (x0 * x0 * E::from(3u64) + a) / (y0 + y0);
318                let x2 = s * s - x0 - x1;
319                let y2 = s * (x0 - x2) - y0;
320                SWPoint(x2, y2, false)
321            }
322        } else {
323            // point addition
324            if x0 == x1 {
325                SWPoint(E::zero(), E::zero(), true)
326            } else {
327                let s = (y0 - y1) / (x0 - x1);
328                let x2 = s * s - x0 - x1;
329                let y2 = s * (x0 - x2) - y0;
330                SWPoint(x2, y2, false)
331            }
332        };
333        let p2 = self.create_emulated_sw_point_variable(p2)?;
334        self.emulated_sw_ecc_add_gate(p0, p1, &p2, a)?;
335        Ok(p2)
336    }
337}
338
339#[cfg(test)]
340mod tests {
341    use crate::{
342        gadgets::{ecc::conversion::*, EmulationConfig, SerializableEmulatedStruct},
343        Circuit, CircuitError, PlonkCircuit,
344    };
345    use ark_bls12_377::{g1::Config as Param377, Fq as Fq377};
346    use ark_bn254::{g1::Config as Param254, Fq as Fq254, Fr as Fr254};
347    use ark_ec::{
348        short_weierstrass::{Projective, SWCurveConfig},
349        CurveGroup, Group,
350    };
351    use ark_ff::{MontFp, PrimeField};
352    use ark_std::{UniformRand, Zero};
353
354    use super::{EmulatedSWPointVariable, SWPoint};
355
356    #[test]
357    fn test_emulated_sw_point_addition() {
358        let a: Fq377 = MontFp!("0");
359        test_emulated_sw_point_addition_helper::<Fq377, Fr254, Param377>(a);
360        let a: Fq254 = MontFp!("0");
361        test_emulated_sw_point_addition_helper::<Fq254, Fr254, Param254>(a);
362    }
363
364    fn ecc_add_and_check<E, F>(
365        circuit: &mut PlonkCircuit<F>,
366        p0: &EmulatedSWPointVariable<E>,
367        p1: &EmulatedSWPointVariable<E>,
368        a: E,
369        expected: &SWPoint<E>,
370    ) -> Result<EmulatedSWPointVariable<E>, CircuitError>
371    where
372        E: EmulationConfig<F> + SWToTEConParam,
373        F: PrimeField,
374    {
375        let result = circuit.emulated_sw_ecc_add(p0, p1, a)?;
376        assert_eq!(circuit.emulated_sw_point_witness(&result)?, *expected);
377        Ok(result)
378    }
379
380    fn test_emulated_sw_point_addition_helper<E, F, P>(a: E)
381    where
382        E: EmulationConfig<F> + SWToTEConParam,
383        F: PrimeField,
384        P: SWCurveConfig<BaseField = E>,
385    {
386        let mut rng = jf_utils::test_rng();
387        let neutral = Projective::<P>::zero().into_affine();
388        let p1 = Projective::<P>::rand(&mut rng).into_affine();
389        let p2 = Projective::<P>::rand(&mut rng).into_affine();
390        let expected = (p1 + p2).into_affine().into();
391        let wrong_result = (p1 + p2 + Projective::<P>::generator())
392            .into_affine()
393            .into();
394
395        let mut circuit = PlonkCircuit::<F>::new_ultra_plonk(20);
396
397        let var_p1 = circuit
398            .create_public_emulated_sw_point_variable(p1.into())
399            .unwrap();
400        let var_p2 = circuit
401            .create_emulated_sw_point_variable(p2.into())
402            .unwrap();
403        let var_neutral = circuit
404            .create_emulated_sw_point_variable(neutral.into())
405            .unwrap();
406        ecc_add_and_check::<E, F>(&mut circuit, &var_p1, &var_p2, a, &expected).unwrap();
407        ecc_add_and_check::<E, F>(&mut circuit, &var_p1, &var_neutral, a, &p1.into()).unwrap();
408        ecc_add_and_check::<E, F>(&mut circuit, &var_neutral, &var_p2, a, &p2.into()).unwrap();
409
410        // test point doubling
411        let double_p1 = (p1 + p1).into_affine().into();
412        ecc_add_and_check::<E, F>(&mut circuit, &var_p1, &var_p1, a, &double_p1).unwrap();
413        ecc_add_and_check::<E, F>(&mut circuit, &var_neutral, &var_neutral, a, &neutral.into())
414            .unwrap();
415
416        let public_inputs: SWPoint<E> = p1.into();
417        let public_inputs = public_inputs.serialize_to_native_elements();
418        let wrong_inputs: SWPoint<E> = neutral.into();
419        let wrong_inputs = wrong_inputs.serialize_to_native_elements();
420        assert!(circuit.check_circuit_satisfiability(&public_inputs).is_ok());
421        assert!(circuit.check_circuit_satisfiability(&wrong_inputs).is_err());
422
423        // fail path
424        let var_wrong_result = circuit
425            .create_emulated_sw_point_variable(wrong_result)
426            .unwrap();
427        circuit
428            .emulated_sw_ecc_add_gate(&var_p1, &var_p2, &var_wrong_result, a)
429            .unwrap();
430        assert!(circuit
431            .check_circuit_satisfiability(&public_inputs)
432            .is_err());
433    }
434}
jf_relation/gadgets/ecc/emulated/short_weierstrass.rs

jf_relation/gadgets/ecc/emulated/
short_weierstrass.rs
