1use super::*;
  2
  3/// An affine representation of a prime order curve point that is guaranteed
  4/// to *not* be the point at infinity.
  5#[derive(Derivative)]
  6#[derivative(Debug, Clone)]
  7#[must_use]
  8pub struct NonZeroAffineVar<
  9    P: SWModelParameters,
 10    F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
 11> where
 12    for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 13{
 14    /// The x-coordinate.
 15    pub x: F,
 16    /// The y-coordinate.
 17    pub y: F,
 18    #[derivative(Debug = "ignore")]
 19    _params: PhantomData<P>,
 20}
 21
 22impl<P, F> NonZeroAffineVar<P, F>
 23where
 24    P: SWModelParameters,
 25    F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
 26    for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 27{
 28    pub fn new(x: F, y: F) -> Self {
 29        Self {
 30            x,
 31            y,
 32            _params: PhantomData,
 33        }
 34    }
 35
 36    /// Converts self into a non-zero projective point.
 37    #[tracing::instrument(target = "r1cs", skip(self))]
 38    pub fn into_projective(&self) -> ProjectiveVar<P, F> {
 39        ProjectiveVar::new(self.x.clone(), self.y.clone(), F::one())
 40    }
 41
 42    /// Performs an addition without checking that other != ±self.
 43    #[tracing::instrument(target = "r1cs", skip(self, other))]
 44    pub fn add_unchecked(&self, other: &Self) -> Result<Self, SynthesisError> {
 45        if [self, other].is_constant() {
 46            let result =
 47                (self.value()?.into_projective() + other.value()?.into_projective()).into_affine();
 48            Ok(Self::new(F::constant(result.x), F::constant(result.y)))
 49        } else {
 50            let (x1, y1) = (&self.x, &self.y);
 51            let (x2, y2) = (&other.x, &other.y);
 52            // Then,
 53            // slope lambda := (y2 - y1)/(x2 - x1);
 54            // x3 = lambda^2 - x1 - x2;
 55            // y3 = lambda * (x1 - x3) - y1
 56            let numerator = y2 - y1;
 57            let denominator = x2 - x1;
 58            // It's okay to use `unchecked` here, because the precondition of `add_unchecked` is that
 59            // self != ±other, which means that `numerator` and `denominator` are both non-zero.
 60            let lambda = numerator.mul_by_inverse_unchecked(&denominator)?;
 61            let x3 = lambda.square()? - x1 - x2;
 62            let y3 = lambda * &(x1 - &x3) - y1;
 63            Ok(Self::new(x3, y3))
 64        }
 65    }
 66
 67    /// Doubles `self`. As this is a prime order curve point,
 68    /// the output is guaranteed to not be the point at infinity.
 69    #[tracing::instrument(target = "r1cs", skip(self))]
 70    pub fn double(&self) -> Result<Self, SynthesisError> {
 71        if [self].is_constant() {
 72            let result = self.value()?.into_projective().double().into_affine();
 73            // Panic if the result is zero.
 74            assert!(!result.is_zero());
 75            Ok(Self::new(F::constant(result.x), F::constant(result.y)))
 76        } else {
 77            let (x1, y1) = (&self.x, &self.y);
 78            let x1_sqr = x1.square()?;
 79            // Then,
 80            // tangent lambda := (3 * x1^2 + a) / (2 * y1);
 81            // x3 = lambda^2 - 2x1
 82            // y3 = lambda * (x1 - x3) - y1
 83            let numerator = x1_sqr.double()? + &x1_sqr + P::COEFF_A;
 84            let denominator = y1.double()?;
 85            // It's okay to use `unchecked` here, because the precondition of `double` is that
 86            // self != zero.
 87            let lambda = numerator.mul_by_inverse_unchecked(&denominator)?;
 88            let x3 = lambda.square()? - x1.double()?;
 89            let y3 = lambda * &(x1 - &x3) - y1;
 90            Ok(Self::new(x3, y3))
 91        }
 92    }
 93
 94    /// Computes `(self + other) + self`. This method requires only 5 constraints,
 95    /// less than the 7 required when computing via `self.double() + other`.
 96    ///
 97    /// This follows the formulae from [\[ELM03\]](https://arxiv.org/abs/math/0208038).
 98    #[tracing::instrument(target = "r1cs", skip(self))]
 99    pub fn double_and_add_unchecked(&self, other: &Self) -> Result<Self, SynthesisError> {
100        if [self].is_constant() || other.is_constant() {
101            self.double()?.add_unchecked(other)
102        } else {
103            // It's okay to use `unchecked` the precondition is that `self != ±other` (i.e. same logic as in `add_unchecked`)
104            let (x1, y1) = (&self.x, &self.y);
105            let (x2, y2) = (&other.x, &other.y);
106
107            // Calculate self + other:
108            // slope lambda := (y2 - y1)/(x2 - x1);
109            // x3 = lambda^2 - x1 - x2;
110            // y3 = lambda * (x1 - x3) - y1
111            let numerator = y2 - y1;
112            let denominator = x2 - x1;
113            let lambda_1 = numerator.mul_by_inverse_unchecked(&denominator)?;
114
115            let x3 = lambda_1.square()? - x1 - x2;
116
117            // Calculate final addition slope:
118            let lambda_2 =
119                (lambda_1 + y1.double()?.mul_by_inverse_unchecked(&(&x3 - x1))?).negate()?;
120
121            let x4 = lambda_2.square()? - x1 - x3;
122            let y4 = lambda_2 * &(x1 - &x4) - y1;
123            Ok(Self::new(x4, y4))
124        }
125    }
126
127    /// Doubles `self` in place.
128    #[tracing::instrument(target = "r1cs", skip(self))]
129    pub fn double_in_place(&mut self) -> Result<(), SynthesisError> {
130        *self = self.double()?;
131        Ok(())
132    }
133}
134
135impl<P, F> R1CSVar<<P::BaseField as Field>::BasePrimeField> for NonZeroAffineVar<P, F>
136where
137    P: SWModelParameters,
138    F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
139    for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
140{
141    type Value = SWAffine<P>;
142
143    fn cs(&self) -> ConstraintSystemRef<<P::BaseField as Field>::BasePrimeField> {
144        self.x.cs().or(self.y.cs())
145    }
146
147    fn value(&self) -> Result<SWAffine<P>, SynthesisError> {
148        Ok(SWAffine::new(self.x.value()?, self.y.value()?, false))
149    }
150}
151
152impl<P, F> CondSelectGadget<<P::BaseField as Field>::BasePrimeField> for NonZeroAffineVar<P, F>
153where
154    P: SWModelParameters,
155    F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
156    for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
157{
158    #[inline]
159    #[tracing::instrument(target = "r1cs")]
160    fn conditionally_select(
161        cond: &Boolean<<P::BaseField as Field>::BasePrimeField>,
162        true_value: &Self,
163        false_value: &Self,
164    ) -> Result<Self, SynthesisError> {
165        let x = cond.select(&true_value.x, &false_value.x)?;
166        let y = cond.select(&true_value.y, &false_value.y)?;
167
168        Ok(Self::new(x, y))
169    }
170}
171
172impl<P, F> EqGadget<<P::BaseField as Field>::BasePrimeField> for NonZeroAffineVar<P, F>
173where
174    P: SWModelParameters,
175    F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
176    for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
177{
178    #[tracing::instrument(target = "r1cs")]
179    fn is_eq(
180        &self,
181        other: &Self,
182    ) -> Result<Boolean<<P::BaseField as Field>::BasePrimeField>, SynthesisError> {
183        let x_equal = self.x.is_eq(&other.x)?;
184        let y_equal = self.y.is_eq(&other.y)?;
185        x_equal.and(&y_equal)
186    }
187
188    #[inline]
189    #[tracing::instrument(target = "r1cs")]
190    fn conditional_enforce_equal(
191        &self,
192        other: &Self,
193        condition: &Boolean<<P::BaseField as Field>::BasePrimeField>,
194    ) -> Result<(), SynthesisError> {
195        let x_equal = self.x.is_eq(&other.x)?;
196        let y_equal = self.y.is_eq(&other.y)?;
197        let coordinates_equal = x_equal.and(&y_equal)?;
198        coordinates_equal.conditional_enforce_equal(&Boolean::Constant(true), condition)?;
199        Ok(())
200    }
201
202    #[inline]
203    #[tracing::instrument(target = "r1cs")]
204    fn enforce_equal(&self, other: &Self) -> Result<(), SynthesisError> {
205        self.x.enforce_equal(&other.x)?;
206        self.y.enforce_equal(&other.y)?;
207        Ok(())
208    }
209
210    #[inline]
211    #[tracing::instrument(target = "r1cs")]
212    fn conditional_enforce_not_equal(
213        &self,
214        other: &Self,
215        condition: &Boolean<<P::BaseField as Field>::BasePrimeField>,
216    ) -> Result<(), SynthesisError> {
217        let is_equal = self.is_eq(other)?;
218        is_equal
219            .and(condition)?
220            .enforce_equal(&Boolean::Constant(false))
221    }
222}
223
224#[cfg(test)]
225mod test_non_zero_affine {
226    use crate::alloc::AllocVar;
227    use crate::eq::EqGadget;
228    use crate::fields::fp::{AllocatedFp, FpVar};
229    use crate::groups::curves::short_weierstrass::non_zero_affine::NonZeroAffineVar;
230    use crate::groups::curves::short_weierstrass::ProjectiveVar;
231    use crate::groups::CurveVar;
232    use crate::R1CSVar;
233    use ark_ec::{ProjectiveCurve, SWModelParameters};
234    use ark_relations::r1cs::ConstraintSystem;
235    use ark_std::{vec::Vec, One};
236    use ark_test_curves::bls12_381::{g1::Parameters as G1Parameters, Fq};
237
238    #[test]
239    fn correctness_test_1() {
240        let cs = ConstraintSystem::<Fq>::new_ref();
241
242        let x = FpVar::Var(
243            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
244                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.0)
245            })
246            .unwrap(),
247        );
248        let y = FpVar::Var(
249            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
250                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.1)
251            })
252            .unwrap(),
253        );
254
255        // The following code uses `double` and `add` (`add_unchecked`) to compute
256        // (1 + 2 + ... + 2^9) G
257
258        let sum_a = {
259            let mut a = ProjectiveVar::<G1Parameters, FpVar<Fq>>::new(
260                x.clone(),
261                y.clone(),
262                FpVar::Constant(Fq::one()),
263            );
264
265            let mut double_sequence = Vec::new();
266            double_sequence.push(a.clone());
267
268            for _ in 1..10 {
269                a = a.double().unwrap();
270                double_sequence.push(a.clone());
271            }
272
273            let mut sum = double_sequence[0].clone();
274            for elem in double_sequence.iter().skip(1) {
275                sum = sum + elem;
276            }
277
278            let sum = sum.value().unwrap().into_affine();
279            (sum.x, sum.y)
280        };
281
282        let sum_b = {
283            let mut a = NonZeroAffineVar::<G1Parameters, FpVar<Fq>>::new(x, y);
284
285            let mut double_sequence = Vec::new();
286            double_sequence.push(a.clone());
287
288            for _ in 1..10 {
289                a = a.double().unwrap();
290                double_sequence.push(a.clone());
291            }
292
293            let mut sum = double_sequence[0].clone();
294            for elem in double_sequence.iter().skip(1) {
295                sum = sum.add_unchecked(&elem).unwrap();
296            }
297
298            (sum.x.value().unwrap(), sum.y.value().unwrap())
299        };
300
301        assert_eq!(sum_a.0, sum_b.0);
302        assert_eq!(sum_a.1, sum_b.1);
303    }
304
305    #[test]
306    fn correctness_test_2() {
307        let cs = ConstraintSystem::<Fq>::new_ref();
308
309        let x = FpVar::Var(
310            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
311                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.0)
312            })
313            .unwrap(),
314        );
315        let y = FpVar::Var(
316            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
317                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.1)
318            })
319            .unwrap(),
320        );
321
322        // The following code tests `double_and_add`.
323        let sum_a = {
324            let a = ProjectiveVar::<G1Parameters, FpVar<Fq>>::new(
325                x.clone(),
326                y.clone(),
327                FpVar::Constant(Fq::one()),
328            );
329
330            let mut cur = a.clone();
331            cur.double_in_place().unwrap();
332            for _ in 1..10 {
333                cur.double_in_place().unwrap();
334                cur = cur + &a;
335            }
336
337            let sum = cur.value().unwrap().into_affine();
338            (sum.x, sum.y)
339        };
340
341        let sum_b = {
342            let a = NonZeroAffineVar::<G1Parameters, FpVar<Fq>>::new(x, y);
343
344            let mut cur = a.double().unwrap();
345            for _ in 1..10 {
346                cur = cur.double_and_add_unchecked(&a).unwrap();
347            }
348
349            (cur.x.value().unwrap(), cur.y.value().unwrap())
350        };
351
352        assert!(cs.is_satisfied().unwrap());
353        assert_eq!(sum_a.0, sum_b.0);
354        assert_eq!(sum_a.1, sum_b.1);
355    }
356
357    #[test]
358    fn correctness_test_eq() {
359        let cs = ConstraintSystem::<Fq>::new_ref();
360
361        let x = FpVar::Var(
362            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
363                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.0)
364            })
365            .unwrap(),
366        );
367        let y = FpVar::Var(
368            AllocatedFp::<Fq>::new_witness(cs.clone(), || {
369                Ok(G1Parameters::AFFINE_GENERATOR_COEFFS.1)
370            })
371            .unwrap(),
372        );
373
374        let a = NonZeroAffineVar::<G1Parameters, FpVar<Fq>>::new(x, y);
375
376        let n = 10;
377
378        let a_multiples: Vec<NonZeroAffineVar<G1Parameters, FpVar<Fq>>> =
379            std::iter::successors(Some(a.clone()), |acc| Some(acc.add_unchecked(&a).unwrap()))
380                .take(n)
381                .collect();
382
383        let all_equal: Vec<NonZeroAffineVar<G1Parameters, FpVar<Fq>>> = (0..n / 2)
384            .map(|i| {
385                a_multiples[i]
386                    .add_unchecked(&a_multiples[n - i - 1])
387                    .unwrap()
388            })
389            .collect();
390
391        for i in 0..n - 1 {
392            a_multiples[i]
393                .enforce_not_equal(&a_multiples[i + 1])
394                .unwrap();
395        }
396        for i in 0..all_equal.len() - 1 {
397            all_equal[i].enforce_equal(&all_equal[i + 1]).unwrap();
398        }
399
400        assert!(cs.is_satisfied().unwrap());
401    }
402}