decaf377/ark_curve/r1cs/
fqvar_ext.rs

1use ark_r1cs_std::eq::EqGadget;
2use ark_r1cs_std::prelude::{AllocVar, Boolean, FieldVar};
3use ark_r1cs_std::select::CondSelectGadget;
4use ark_r1cs_std::{R1CSVar, ToBitsGadget};
5use ark_relations::r1cs::SynthesisError;
6
7use crate::ark_curve::{constants::ZETA, r1cs::FqVar};
8use crate::Fq;
9
10pub trait FqVarExtension: Sized {
11    fn isqrt(&self) -> Result<(Boolean<Fq>, FqVar), SynthesisError>;
12
13    // This is similar to the Sign trait in this crate,
14    // however: we need to return `Result<_, SynthesisError>`
15    // everywhere.
16    fn is_negative(&self) -> Result<Boolean<Fq>, SynthesisError>;
17    fn is_nonnegative(&self) -> Result<Boolean<Fq>, SynthesisError>;
18    fn abs(self) -> Result<Self, SynthesisError>;
19}
20
21impl FqVarExtension for FqVar {
22    /// Inverse square root in R1CS
23    ///
24    /// Cases:
25    /// - Case 1: `(true, sqrt(num/den))` if `num` and `den` are both nonzero and `num/den` is square;
26    /// - Case 2: `(true, 0)` if `num` is zero;
27    /// - Case 3: `(false, 0)` if `den` is zero;
28    /// - Case 4: `(false, sqrt(zeta*num/den))` if `num` and `den` are both nonzero and `num/den` is nonsquare;
29    fn isqrt(&self) -> Result<(Boolean<Fq>, FqVar), SynthesisError> {
30        // During mode `SynthesisMode::Setup`, value() will not provide a field element.
31        let den = self.value().unwrap_or(Fq::ONE);
32
33        // Out of circuit sqrt computation:
34        // Note: `num = 1`
35        // `y = sqrt(num/den)`
36        let (was_square, y) = Fq::sqrt_ratio_zeta(&Fq::ONE, &den);
37
38        let cs = self.cs();
39        let was_square_var = Boolean::new_witness(cs.clone(), || Ok(was_square))?;
40        let y_var = FqVar::new_witness(cs.clone(), || Ok(y))?;
41        // `y^2 = num/den`
42        let y_squared_var = y_var.square()?;
43
44        // The below is a flattened version of the four cases above, excluding case 2 since `num` is hardcoded
45        // to be one.
46        //
47        // Case 1: `(true, sqrt(num/den))` if `num` and `den` are both nonzero and `num/den` is square
48        let den_var_is_zero = self.is_eq(&FqVar::zero())?;
49        let den_var = FqVar::conditionally_select(&den_var_is_zero, &FqVar::one(), self)?;
50        let den_var_inv = den_var.inverse()?;
51        // Note we could be in case 1 or case 2 based on the constraint that `was_square = true`, but
52        // num is hardcoded to be one above, so we're in case 1.
53        let in_case_1 = was_square_var.clone();
54        // Certify the return value y is sqrt(1/den) when we're in case 1. This also certifies that we are not in case 2.
55        y_squared_var.conditional_enforce_equal(&den_var_inv, &in_case_1)?;
56
57        // Case 3: `(false, 0)` if `den` is zero
58        let was_not_square_var = was_square_var.not();
59        let in_case_3 = was_not_square_var.and(&den_var_is_zero)?;
60        // Certify the return value y is 0 when we're in case 3.
61        y_squared_var.conditional_enforce_equal(&FqVar::zero(), &in_case_3)?;
62
63        // Case 4: `(false, sqrt(zeta*num/den))` if `num` and `den` are both nonzero and `num/den` is nonsquare;
64        let zeta_var = FqVar::new_constant(cs, ZETA)?;
65        let zeta_times_one_over_den_var = zeta_var * den_var_inv;
66        let in_case_4 = was_not_square_var.and(&den_var_is_zero.not())?;
67        // Certify the return value y is sqrt(zeta * 1/den)
68        y_squared_var.conditional_enforce_equal(&zeta_times_one_over_den_var, &in_case_4)?;
69
70        // Ensure that we are in case 1, 3, or 4.
71        let in_case = in_case_1.or(&in_case_3)?.or(&in_case_4)?;
72        in_case.enforce_equal(&Boolean::TRUE)?;
73
74        Ok((was_square_var, y_var))
75    }
76
77    fn is_negative(&self) -> Result<Boolean<Fq>, SynthesisError> {
78        Ok(self.is_nonnegative()?.not())
79    }
80
81    fn is_nonnegative(&self) -> Result<Boolean<Fq>, SynthesisError> {
82        let bitvars = self.to_bits_le()?;
83
84        // bytes[0] & 1 == 0
85        let true_var = Boolean::<Fq>::TRUE;
86        let false_var = Boolean::<Fq>::FALSE;
87
88        // Check least significant bit
89        let lhs = bitvars[0].and(&true_var)?;
90        let is_nonnegative_var = lhs.is_eq(&false_var)?;
91
92        Ok(is_nonnegative_var)
93    }
94
95    fn abs(self) -> Result<Self, SynthesisError> {
96        let absolute_value =
97            FqVar::conditionally_select(&self.is_nonnegative()?, &self, &self.negate()?)?;
98        Ok(absolute_value)
99    }
100}
decaf377/ark_curve/r1cs/fqvar_ext.rs

decaf377/ark_curve/r1cs/
fqvar_ext.rs
