decaf377/ark_curve/r1cs/
inner.rs

1#![allow(non_snake_case)]
2use core::borrow::Borrow;
3use core::ops::{Add, AddAssign, Sub, SubAssign};
4
5use ark_ec::{twisted_edwards::TECurveConfig, AffineRepr};
6use ark_r1cs_std::{
7    alloc::AllocVar, eq::EqGadget, groups::curves::twisted_edwards::AffineVar, prelude::*, R1CSVar,
8};
9use ark_relations::ns;
10use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError};
11use ark_std::vec::Vec;
12
13use crate::ark_curve::{
14    constants::ZETA, edwards::EdwardsAffine, r1cs::fqvar_ext::FqVarExtension, r1cs::FqVar,
15    AffinePoint, Decaf377EdwardsConfig, Element,
16};
17use crate::Fq;
18
19pub(crate) type Decaf377EdwardsVar = AffineVar<Decaf377EdwardsConfig, FqVar>;
20
21#[derive(Clone, Debug)]
22/// Represents the R1CS equivalent of a `decaf377::Element`
23///
24/// Generally the suffix -`Var` will indicate that the type or variable
25/// represents in R1CS.
26pub struct ElementVar {
27    /// Inner type is an alias for `AffineVar<EdwardsConfig, FqVar>`
28    pub(crate) inner: Decaf377EdwardsVar,
29}
30
31impl ElementVar {
32    /// R1CS equivalent of `Element::vartime_compress_to_field`
33    pub fn compress_to_field(&self) -> Result<FqVar, SynthesisError> {
34        // We have affine x, y but our compression formulae are in projective.
35        let affine_x_var = &self.inner.x;
36        let affine_y_var = &self.inner.y;
37
38        let X_var = affine_x_var;
39        // We treat Z at a constant.
40        let Y_var = affine_y_var;
41        let Z_var = FqVar::one();
42        let T_var = X_var * Y_var;
43
44        let A_MINUS_D_VAR = FqVar::new_constant(
45            self.cs(),
46            Decaf377EdwardsConfig::COEFF_A - Decaf377EdwardsConfig::COEFF_D,
47        )?;
48
49        // 1.
50        let u_1_var = (X_var.clone() + T_var.clone()) * (X_var.clone() - T_var.clone());
51
52        // 2.
53        let den_var = u_1_var.clone() * A_MINUS_D_VAR.clone() * X_var.square()?;
54        let (_, v_var) = den_var.isqrt()?;
55
56        // 3.
57        let u_2_var: FqVar = (v_var.clone() * u_1_var).abs()?;
58
59        // 4.
60        let u_3_var = u_2_var * Z_var - T_var;
61
62        // 5.
63        let s_var = (A_MINUS_D_VAR * v_var * u_3_var * X_var).abs()?;
64
65        Ok(s_var)
66    }
67
68    /// R1CS equivalent of `Encoding::vartime_decompress`
69    pub fn decompress_from_field(s_var: FqVar) -> Result<ElementVar, SynthesisError> {
70        let D4: Fq = Decaf377EdwardsConfig::COEFF_D * Fq::from(4u32);
71        let D4_VAR = FqVar::constant(D4);
72
73        // 1. We do not check if canonically encoded here since we know FqVar is already
74        // a valid Fq field element.
75
76        // 2. Reject if negative.
77        let is_nonnegative_var = s_var.is_nonnegative()?;
78        is_nonnegative_var.enforce_equal(&Boolean::TRUE)?;
79
80        // 3. u_1 <- 1 - s^2
81        let ss_var = s_var.square()?;
82        let u_1_var = FqVar::one() - ss_var.clone();
83
84        // 4. u_2 <- u_1^2 - 4d s^2
85        let u_2_var = u_1_var.square()? - D4_VAR * ss_var.clone();
86
87        // 5. sqrt
88        let den_var = u_2_var.clone() * u_1_var.square()?;
89        let (was_square_var, mut v_var) = den_var.isqrt()?;
90        was_square_var.enforce_equal(&Boolean::TRUE)?;
91
92        // 6. Sign check
93        let two_s_u_1_var = (FqVar::one() + FqVar::one()) * s_var * u_1_var.clone();
94        let check_var = two_s_u_1_var.clone() * v_var.clone();
95        v_var = FqVar::conditionally_select(&check_var.is_negative()?, &v_var.negate()?, &v_var)?;
96
97        // 7. (Extended) Coordinates
98        let x_var = two_s_u_1_var * v_var.square()? * u_2_var;
99        let y_var = (FqVar::one() + ss_var) * v_var * u_1_var;
100        // // let z = FqVar::one();
101        // let t = x.clone() * y.clone();
102
103        // Note that the above are in extended, but we need affine coordinates
104        // for forming `AffineVar` where x = X/Z, y = Y/Z. However Z is
105        // hardcoded to be 1 above, so we can use x and y as is.
106        Ok(ElementVar {
107            inner: AffineVar::new(x_var, y_var),
108        })
109    }
110
111    /// R1CS equivalent of `Element::elligator_map`
112    pub(crate) fn elligator_map(r_0_var: &FqVar) -> Result<ElementVar, SynthesisError> {
113        let cs = r_0_var.cs();
114
115        let A_VAR = FqVar::new_constant(cs.clone(), Decaf377EdwardsConfig::COEFF_A)?;
116        let D_VAR = FqVar::new_constant(cs.clone(), Decaf377EdwardsConfig::COEFF_D)?;
117        let ZETA_VAR = FqVar::new_constant(cs, ZETA)?;
118
119        let r_var = ZETA_VAR * r_0_var.square()?;
120
121        let den_var = (D_VAR.clone() * r_var.clone() - (D_VAR.clone() - A_VAR.clone()))
122            * ((D_VAR.clone() - A_VAR.clone()) * r_var.clone() - D_VAR.clone());
123        let num_var = (r_var.clone() + FqVar::one())
124            * (A_VAR.clone() - (FqVar::one() + FqVar::one()) * D_VAR.clone());
125
126        let x_var = num_var.clone() * den_var;
127        let (iss_var, mut isri_var) = x_var.isqrt()?;
128
129        // Case 1: iss is true, then sgn and twiddle are both 1
130        // Case 2: iss is false, then sgn is -1 and twiddle is r_0
131        let sgn_var =
132            FqVar::conditionally_select(&iss_var, &FqVar::one(), &(FqVar::one()).negate()?)?;
133        let twiddle_var = FqVar::conditionally_select(&iss_var, &FqVar::one(), r_0_var)?;
134
135        isri_var *= twiddle_var;
136
137        let mut s_var = isri_var.clone() * num_var;
138        let t_var = sgn_var.negate()?
139            * isri_var
140            * s_var.clone()
141            * (r_var - FqVar::one())
142            * (A_VAR.clone() - (FqVar::one() + FqVar::one()) * D_VAR).square()?
143            - FqVar::one();
144
145        let is_negative_var = s_var.is_negative()?;
146        let cond_negate = is_negative_var.is_eq(&iss_var)?;
147        // if s.is_negative() == iss { s = -s }
148        s_var = FqVar::conditionally_select(&cond_negate, &s_var.negate()?, &s_var)?;
149
150        // Convert to affine from Jacobi quartic
151        // See commit cce38644d3343d9f7c46772dc2b945a9d17756d7
152        let affine_x_num = (FqVar::one() + FqVar::one()) * s_var.clone();
153        let affine_x_den = FqVar::one() + A_VAR.clone() * s_var.square()?;
154        let affine_x_var = affine_x_num * affine_x_den.inverse()?;
155        let affine_y_num = FqVar::one() - A_VAR * s_var.square()?;
156        let affine_y_den = t_var;
157        let affine_y_var = affine_y_num * affine_y_den.inverse()?;
158
159        Ok(ElementVar {
160            inner: AffineVar::new(affine_x_var, affine_y_var),
161        })
162    }
163}
164
165impl EqGadget<Fq> for ElementVar {
166    fn is_eq(&self, other: &Self) -> Result<Boolean<Fq>, SynthesisError> {
167        // Section 4.5 of Decaf paper: X_1 * Y_2 = X_2 * Y_1
168        // in extended coordinates, but note that x, y are affine here:
169        let X_1 = &self.inner.x;
170        let Y_1 = &self.inner.y;
171        let X_2 = &other.inner.x;
172        let Y_2 = &other.inner.y;
173        let lhs = X_1 * Y_2;
174        let rhs = X_2 * Y_1;
175        lhs.is_eq(&rhs)
176    }
177
178    fn conditional_enforce_equal(
179        &self,
180        other: &Self,
181        should_enforce: &Boolean<Fq>,
182    ) -> Result<(), SynthesisError> {
183        // should_enforce = true
184        //      return self == other
185        // should_enforce = false
186        //      return true
187        self.is_eq(other)?
188            .conditional_enforce_equal(&Boolean::constant(true), should_enforce)
189    }
190
191    fn conditional_enforce_not_equal(
192        &self,
193        other: &Self,
194        should_enforce: &Boolean<Fq>,
195    ) -> Result<(), SynthesisError> {
196        self.is_eq(other)?
197            .conditional_enforce_equal(&Boolean::constant(false), should_enforce)
198    }
199}
200
201impl R1CSVar<Fq> for ElementVar {
202    type Value = Element;
203
204    fn cs(&self) -> ConstraintSystemRef<Fq> {
205        self.inner.cs()
206    }
207
208    fn value(&self) -> Result<Self::Value, SynthesisError> {
209        let (x, y) = (self.inner.x.value()?, self.inner.y.value()?);
210        let result = EdwardsAffine::new(x, y);
211        Ok(Element {
212            inner: result.into(),
213        })
214    }
215}
216
217impl CondSelectGadget<Fq> for ElementVar {
218    fn conditionally_select(
219        cond: &Boolean<Fq>,
220        true_value: &Self,
221        false_value: &Self,
222    ) -> Result<Self, SynthesisError> {
223        let x = cond.select(&true_value.inner.x, &false_value.inner.x)?;
224        let y = cond.select(&true_value.inner.y, &false_value.inner.y)?;
225
226        Ok(ElementVar {
227            inner: Decaf377EdwardsVar::new(x, y),
228        })
229    }
230}
231
232// This lets us use `new_constant`, `new_input` (public), or `new_witness` to add
233// decaf elements to an R1CS constraint system.
234impl AllocVar<Element, Fq> for ElementVar {
235    fn new_variable<T: core::borrow::Borrow<Element>>(
236        cs: impl Into<ark_relations::r1cs::Namespace<Fq>>,
237        f: impl FnOnce() -> Result<T, SynthesisError>,
238        mode: AllocationMode,
239    ) -> Result<Self, SynthesisError> {
240        let ns = cs.into();
241        let cs = ns.cs();
242        let f = || Ok(*f()?.borrow());
243        let group_projective_point = f()?;
244
245        // `new_variable` should *not* allocate any new variables or constraints in `cs` when
246        // the mode is `AllocationMode::Constant` (see `AllocVar::new_constant`).
247        //
248        // Compare this with the implementation of this trait for `EdwardsVar`
249        // where they check that the point is in the right subgroup prior to witnessing.
250        match mode {
251            AllocationMode::Constant => Ok(Self {
252                inner: Decaf377EdwardsVar::new_variable_omit_prime_order_check(
253                    cs,
254                    || Ok(group_projective_point.inner),
255                    mode,
256                )?,
257            }),
258            AllocationMode::Input => {
259                unreachable!()
260            }
261            AllocationMode::Witness => {
262                let P_var = AffineVar::new_variable_omit_prime_order_check(
263                    ns!(cs, "P_affine"),
264                    || Ok(group_projective_point.inner),
265                    mode,
266                )?;
267
268                // At this point `P_var` might not be a valid representative of a decaf point.
269                //
270                // One way that is secure but provides stronger constraints than we need:
271                //
272                // 1. Encode (out of circuit) to an Fq
273                let field_element = group_projective_point.vartime_compress_to_field();
274
275                // 2. Witness the encoded value
276                let compressed_P_var = FqVar::new_witness(cs, || Ok(field_element))?;
277
278                // 3. Decode (in circuit)
279                let decoded_var = ElementVar::decompress_from_field(compressed_P_var)?;
280
281                let P_element_var = Self { inner: P_var };
282                decoded_var.enforce_equal(&P_element_var)?;
283
284                Ok(decoded_var)
285            }
286        }
287    }
288}
289
290impl AllocVar<AffinePoint, Fq> for ElementVar {
291    fn new_variable<T: Borrow<AffinePoint>>(
292        cs: impl Into<ark_relations::r1cs::Namespace<Fq>>,
293        f: impl FnOnce() -> Result<T, SynthesisError>,
294        mode: AllocationMode,
295    ) -> Result<Self, SynthesisError> {
296        Self::new_variable(cs, || f().map(|b| b.borrow().into_group()), mode)
297    }
298}
299
300impl ToBitsGadget<Fq> for ElementVar {
301    fn to_bits_le(&self) -> Result<Vec<Boolean<Fq>>, SynthesisError> {
302        let compressed_fq = self.inner.to_bits_le()?;
303        let encoded_bits = compressed_fq.to_bits_le()?;
304        Ok(encoded_bits)
305    }
306}
307
308impl ToBytesGadget<Fq> for ElementVar {
309    fn to_bytes(&self) -> Result<Vec<UInt8<Fq>>, SynthesisError> {
310        let compressed_fq = self.inner.to_bytes()?;
311        let encoded_bytes = compressed_fq.to_bytes()?;
312        Ok(encoded_bytes)
313    }
314}
315
316impl Add for ElementVar {
317    type Output = ElementVar;
318
319    fn add(self, other: ElementVar) -> Self::Output {
320        ElementVar {
321            inner: self.inner.add(other.inner),
322        }
323    }
324}
325
326impl<'a> Add<&'a ElementVar> for ElementVar {
327    type Output = ElementVar;
328
329    fn add(self, other: &'a ElementVar) -> Self::Output {
330        ElementVar {
331            inner: self.inner.add(other.inner.clone()),
332        }
333    }
334}
335
336impl AddAssign for ElementVar {
337    fn add_assign(&mut self, rhs: ElementVar) {
338        self.inner.add_assign(rhs.inner);
339    }
340}
341
342impl<'a> AddAssign<&'a ElementVar> for ElementVar {
343    fn add_assign(&mut self, rhs: &'a ElementVar) {
344        self.inner.add_assign(rhs.inner.clone())
345    }
346}
347
348impl Sub for ElementVar {
349    type Output = ElementVar;
350
351    fn sub(self, other: ElementVar) -> Self::Output {
352        ElementVar {
353            inner: self.inner.sub(other.inner),
354        }
355    }
356}
357
358impl<'a> Sub<&'a ElementVar> for ElementVar {
359    type Output = ElementVar;
360
361    fn sub(self, other: &'a ElementVar) -> Self::Output {
362        ElementVar {
363            inner: self.inner.sub(other.inner.clone()),
364        }
365    }
366}
367
368impl SubAssign for ElementVar {
369    fn sub_assign(&mut self, rhs: ElementVar) {
370        self.inner.sub_assign(rhs.inner)
371    }
372}
373
374impl<'a> SubAssign<&'a ElementVar> for ElementVar {
375    fn sub_assign(&mut self, rhs: &'a ElementVar) {
376        self.inner.sub_assign(rhs.inner.clone())
377    }
378}
379
380impl Sub<Element> for ElementVar {
381    type Output = ElementVar;
382
383    fn sub(self, other: Element) -> Self::Output {
384        ElementVar {
385            inner: self.inner.sub(other.inner),
386        }
387    }
388}
389
390impl SubAssign<Element> for ElementVar {
391    fn sub_assign(&mut self, rhs: Element) {
392        self.inner.sub_assign(rhs.inner)
393    }
394}
395
396impl Add<Element> for ElementVar {
397    type Output = ElementVar;
398
399    fn add(self, other: Element) -> Self::Output {
400        ElementVar {
401            inner: self.inner.add(other.inner),
402        }
403    }
404}
405
406impl AddAssign<Element> for ElementVar {
407    fn add_assign(&mut self, rhs: Element) {
408        self.inner.add_assign(rhs.inner)
409    }
410}
411
412impl<'a> GroupOpsBounds<'a, Element, ElementVar> for ElementVar {}
413
414impl CurveVar<Element, Fq> for ElementVar {
415    fn zero() -> Self {
416        Self {
417            inner: AffineVar::<Decaf377EdwardsConfig, FqVar>::zero(),
418        }
419    }
420
421    fn constant(other: Element) -> Self {
422        Self {
423            inner: AffineVar::<Decaf377EdwardsConfig, FqVar>::constant(other.inner),
424        }
425    }
426
427    fn new_variable_omit_prime_order_check(
428        cs: impl Into<ark_relations::r1cs::Namespace<Fq>>,
429        f: impl FnOnce() -> Result<Element, SynthesisError>,
430        mode: AllocationMode,
431    ) -> Result<Self, SynthesisError> {
432        let ns = cs.into();
433        let cs = ns.cs();
434
435        match f() {
436            Ok(ge) => {
437                let P = AffineVar::new_variable_omit_prime_order_check(cs, || Ok(ge.inner), mode)?;
438                Ok(Self { inner: P })
439            }
440            _ => Err(SynthesisError::AssignmentMissing),
441        }
442    }
443
444    fn enforce_prime_order(&self) -> Result<(), SynthesisError> {
445        // This is decaf
446        Ok(())
447    }
448
449    fn double_in_place(&mut self) -> Result<(), SynthesisError> {
450        self.inner.double_in_place()?;
451        Ok(())
452    }
453
454    fn negate(&self) -> Result<Self, SynthesisError> {
455        let negated = self.inner.negate()?;
456        Ok(Self { inner: negated })
457    }
458}
decaf377/ark_curve/r1cs/inner.rs

decaf377/ark_curve/r1cs/
inner.rs
