diff --git a/algebra/src/to_field_vec.rs b/algebra/src/to_field_vec.rs index f65db70eb..bd3087894 100644 --- a/algebra/src/to_field_vec.rs +++ b/algebra/src/to_field_vec.rs @@ -1,3 +1,4 @@ +use num_traits::Zero; use crate::{ fields::{ Field, FpParameters, PrimeField, @@ -77,12 +78,15 @@ impl ToConstraintField fo x_fe.extend_from_slice(&y_fe); Ok(x_fe) } else { - // Otherwise, return the coordinates of the infinity representation in Jacobian - let mut x_fe = self.x.to_field_elements()?; - let y_fe = self.y.to_field_elements()?; + // Otherwise, serialize the point as the affine point x=0, y=0, + // which is for sure not on the curve unless b=0 (which should never happen in our case + // as if b=0 then the curve has non-prime order). + //ToDo: in case in the future we may need to employ curves with b=0, we can employ (0,1) + // as the affine representation of the infinity point + debug_assert!(!M::COEFF_B.is_zero()); + let mut x_fe = M::BaseField::zero().to_field_elements()?; + let y_fe = M::BaseField::zero().to_field_elements()?; x_fe.extend_from_slice(&y_fe); - let z_fe = self.z.to_field_elements()?; - x_fe.extend_from_slice(&z_fe); Ok(x_fe) } } @@ -101,12 +105,15 @@ impl ToConstraintField fo x_fe.extend_from_slice(&y_fe); Ok(x_fe) } else { - // Otherwise, return the coordinates of the infinity representation in Projective - let mut x_fe = self.x.to_field_elements()?; - let y_fe = self.y.to_field_elements()?; + // Otherwise, serialize the point as the affine point x=0, y=0, + // which is for sure not on the curve unless b=0 (which should never happen in our case + // as if b=0 then the curve has non-prime order). + //ToDo: in case in the future we may need to employ curves with b=0, we can employ (0,1) + // as the affine representation of the infinity point + debug_assert!(!M::COEFF_B.is_zero()); + let mut x_fe = M::BaseField::zero().to_field_elements()?; + let y_fe = M::BaseField::zero().to_field_elements()?; x_fe.extend_from_slice(&y_fe); - let z_fe = self.z.to_field_elements()?; - x_fe.extend_from_slice(&z_fe); Ok(x_fe) } } diff --git a/r1cs/gadgets/std/src/fields/fp.rs b/r1cs/gadgets/std/src/fields/fp.rs index 0c771cbf7..3be38e399 100644 --- a/r1cs/gadgets/std/src/fields/fp.rs +++ b/r1cs/gadgets/std/src/fields/fp.rs @@ -6,8 +6,9 @@ use r1cs_core::{ }; use std::borrow::Borrow; +use std::convert::TryInto; -use crate::{boolean::AllocatedBit, prelude::*, Assignment}; +use crate::{boolean::AllocatedBit, prelude::*, Assignment, FromGadget}; #[derive(Debug)] pub struct FpGadget { @@ -125,6 +126,66 @@ impl FpGadget { } } +impl TryInto for FpGadget { + type Error = SynthesisError; + + /// Convert an FpGadget `self` that is already constrained to be either 0 or 1 to a Boolean gadget. + /// Therefore, this function does not impose any additional constraint in the circuit to verify that + /// `self` is either 0 or 1, as calling this function with `self` not already being constrained + /// to be either 0 or 1 is considered a misuse of the function. + /// However, if `self.get_value() != None`, then the function will check that such value is + /// neither 0 nor 1, returning an error if this is not the case. + fn try_into(self) -> Result { + + let variable = match self.get_variable() { + Var(var) => var, + LC(_) => Err(SynthesisError::Other(String::from("cannot convert linear combination of variables to Boolean variable")))? + }; + let value = self.get_value().map(|val| if val.is_zero() { + Ok(Some(false)) + } else if val.is_one() { + Ok(Some(true)) + } else { + Err(SynthesisError::Other(String::from("converting field element other than 0 or 1 to Boolean"))) + }).unwrap_or(Ok(None))?; + let alloc_bit = AllocatedBit{ + variable, + value, + }; + Ok(Boolean::from(alloc_bit)) + } +} + +impl FromGadget for FpGadget { + fn from>(bit: Boolean, mut cs: CS) -> Result { + if bit.is_constant() { + return if bit.get_value().unwrap() { + Self::one(cs.ns(|| "alloc constant 1")) + } else { + Self::zero(cs.ns(|| "alloc constant 0")) + } + } + + let alloc_bit = match bit { + Boolean::Is(alloc_bit) | Boolean::Not(alloc_bit) => alloc_bit, + _ => unreachable!(), + }; + + let variable = ConstraintVar::::from(alloc_bit.get_variable()); + let value = bit.get_value().map(|bit_val| if bit_val { + F::one() + } else { + F::zero() + }); + + Ok( + Self{ + value, + variable, + }) + } +} + impl FieldGadget for FpGadget { type Variable = ConstraintVar; @@ -397,18 +458,25 @@ impl EqGadget for FpGadget { mut cs: CS, other: &Self, ) -> Result { - // The Boolean we want to constrain. - let v = Boolean::alloc(cs.ns(|| "alloc verdict"), || { + // The flag we want to constrain. Can be allocated as field element rather than a Boolean + // as the constraints already imposed that v is either 0 or 1 + let v = Self::alloc(cs.ns(|| "alloc verdict"), || { let self_val = self.get_value().get()?; let other_val = other.get_value().get()?; - Ok(self_val == other_val) + Ok( + if self_val == other_val { + F::one() + } else { + F::zero() + } + ) })?; // We allow the prover to choose c as he wishes when v = 1, but if c != 1/(x-y) when // v = 0, then the following constraints will fail let c = Self::alloc(cs.ns(|| "alloc c"), || { let v_val = v.get_value().get()?; - if v_val { + if v_val.is_one() { Ok(F::one()) //Just one random value } else { let self_val = self.get_value().get()?; @@ -422,17 +490,17 @@ impl EqGadget for FpGadget { // 0 = v * (x - y) // 1 - v = c * (x - y) - self.conditional_enforce_equal(cs.ns(|| "0 = v * (x - y)"), other, &v)?; - - let one = CS::one(); + //self.conditional_enforce_equal(cs.ns(|| "0 = v * (x - y)"), other, &v)?; + cs.enforce(|| "0 = v * (x - y)", |lc| &v.variable + lc, |lc| (&self.variable - &other.variable) + lc, |lc| lc); + let not_v = v.negate(cs.ns(|| "-v"))?.add_constant(cs.ns(|| "1-v"), &F::one())?; cs.enforce( || "1 - v = c * (x - y)", |lc| (&self.variable - &other.variable) + lc, |lc| &c.variable + lc, - |_| v.not().lc(one, F::one()), + |lc| ¬_v.variable + lc, ); - Ok(v) + Ok(v.try_into()?) } fn conditional_enforce_equal>( diff --git a/r1cs/gadgets/std/src/fields/mod.rs b/r1cs/gadgets/std/src/fields/mod.rs index 5e30affe5..e6c83d25e 100644 --- a/r1cs/gadgets/std/src/fields/mod.rs +++ b/r1cs/gadgets/std/src/fields/mod.rs @@ -1,9 +1,10 @@ +use std::convert::TryInto; // use std::ops::{Mul, MulAssign}; use algebra::{BitIterator, Field}; use r1cs_core::{ConstraintSystemAbstract, SynthesisError}; use std::fmt::Debug; -use crate::{prelude::*, Assignment}; +use crate::{prelude::*, Assignment, FromGadget}; pub mod cmp; pub mod fp; @@ -23,6 +24,8 @@ pub trait FieldGadget: + TwoBitLookupGadget + ThreeBitCondNegLookupGadget + Debug + + TryInto + + FromGadget { type Variable: Clone + Debug; @@ -754,7 +757,7 @@ pub(crate) mod tests { assert!(cs.is_satisfied()); //If a == b but the prover maliciously witness v as False, cs will not be satisfied - cs.set("a == b/alloc verdict/boolean", ConstraintF::zero()); + cs.set("a == b/alloc verdict/alloc", ConstraintF::zero()); assert!(!cs.is_satisfied()); assert_eq!( "a == b/1 - v = c * (x - y)", @@ -762,7 +765,7 @@ pub(crate) mod tests { ); //If a == b the prover can freely choose c without invalidating any constraint - cs.set("a == b/alloc verdict/boolean", ConstraintF::one()); //Let's bring back v to True + cs.set("a == b/alloc verdict/alloc", ConstraintF::one()); //Let's bring back v to True assert!(cs.is_satisfied()); //Situation should be back to positive case cs.set("a == b/alloc c/alloc", ConstraintF::rand(&mut rng)); //Let's choose a random v assert!(cs.is_satisfied()); @@ -786,15 +789,15 @@ pub(crate) mod tests { assert!(cs.is_satisfied()); //If a != b but the prover maliciously witness v as True, cs will not be satisfied - cs.set("a != b/alloc verdict/boolean", ConstraintF::one()); + cs.set("a != b/alloc verdict/alloc", ConstraintF::one()); assert!(!cs.is_satisfied()); assert_eq!( - "a != b/0 = v * (x - y)/conditional_equals", + "a != b/0 = v * (x - y)", cs.which_is_unsatisfied().unwrap() ); //If a != b the prover is forced to choose c as 1/(a-b) - cs.set("a != b/alloc verdict/boolean", ConstraintF::zero()); //Let's bring back v to False + cs.set("a != b/alloc verdict/alloc", ConstraintF::zero()); //Let's bring back v to False assert!(cs.is_satisfied()); //Situation should be back to normal cs.set("a != b/alloc c/alloc", ConstraintF::rand(&mut rng)); //Let's choose a random c assert!(!cs.is_satisfied()); diff --git a/r1cs/gadgets/std/src/fields/nonnative/nonnative_field_gadget.rs b/r1cs/gadgets/std/src/fields/nonnative/nonnative_field_gadget.rs index d0513901b..9939352db 100644 --- a/r1cs/gadgets/std/src/fields/nonnative/nonnative_field_gadget.rs +++ b/r1cs/gadgets/std/src/fields/nonnative/nonnative_field_gadget.rs @@ -29,6 +29,7 @@ use r1cs_core::{ConstraintSystemAbstract, SynthesisError}; use std::cmp::max; use std::marker::PhantomData; use std::{borrow::Borrow, vec, vec::Vec}; +use std::convert::TryInto; #[derive(Debug, Eq, PartialEq)] #[must_use] @@ -1226,6 +1227,20 @@ impl * The high-level functions for arithmetic mod p: Implementation of FieldGadget * * *****************************************************************************/ +impl TryInto for NonNativeFieldGadget { + type Error = SynthesisError; + + fn try_into(self) -> Result { + unimplemented!() + } +} + +impl FromGadget for NonNativeFieldGadget { + fn from>(_other: Boolean, _cs: CS) -> Result { + unimplemented!() + } +} + impl FieldGadget for NonNativeFieldGadget { diff --git a/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_jacobian.rs b/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_jacobian.rs index aa456f167..383531112 100644 --- a/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_jacobian.rs +++ b/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_jacobian.rs @@ -260,6 +260,7 @@ where /// Compute 2 * self + other. /// Incomplete, safe, addition: neither `self` nor `other` can be the neutral /// element, and other != ±self. + // // ToDo: evaluate if it may be worthy to make it complete pub fn double_and_add>( &self, cs: CS, @@ -334,8 +335,8 @@ where #[inline] fn zero>(mut cs: CS) -> Result { Ok(Self::new( - F::zero(cs.ns(|| "zero"))?, - F::one(cs.ns(|| "one"))?, + F::zero(cs.ns(|| "x=zero"))?, + F::zero(cs.ns(|| "y=zero"))?, Boolean::constant(true), )) } @@ -349,18 +350,129 @@ where } #[inline] - /// Incomplete, safe, addition: neither `self` nor `other` can be the neutral - /// element. + // Algorithm for complete addition ported in R1CS from zcash: https://github.com/ebfull/halo/blob/master/src/gadgets/ecc.rs#L357. + // The algorithm from zcash works only with Weierstrass curves y^2 = x^3+b, the algorithm here + // is modified to work with generic curves y^2 = x^3 +ax + b, for b != 0 (as if b=0 then the point + // (0,0), which is currently used to represent the identity point, will belong to the curve) + //ToDo: in case in the future we may need to use curves with b=0, then it should be possible to + // modify the function to employ the point (0,1) as the representation for the identity point fn add>( &self, - cs: CS, + mut cs: CS, other: &Self, ) -> Result { - self.add_internal(cs, other, true) + let zero = F::zero(cs.ns(|| "alloc constant 0"))?; + let is_same_x = F::alloc(cs.ns(|| "alloc x1 == x2"), + || Ok( + if self.x.get_value().get()? == other.x.get_value().get()? { + P::BaseField::one() + } else { + P::BaseField::zero() + }) + )?; + let not_is_same_x = is_same_x.negate(cs.ns(|| "-is_same_x"))?.add_constant(cs.ns(|| "1 - is_same_x"), &P::BaseField::one())?; + + let x2_minus_x1 = other.x.sub(cs.ns(|| "x2 - x1"), &self.x)?; + let inv = F::alloc(cs.ns(|| "alloc (x2-x1)^-1"), || + Ok( + x2_minus_x1.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ) + )?; + + // enforce that is_same_x = 0 if x2 != x1 + x2_minus_x1.mul_equals(cs.ns(|| "enforce (x2-x1)*is_same_x = 0"), &is_same_x, &zero)?; + // enforce that is_same_x = 1 if x2 == x1 + x2_minus_x1.mul_equals(cs.ns(|| "enforce (x2-x1)*(x2-x1)^-1 = 1-is_same_x"), &inv, ¬_is_same_x)?; + + // compute lambda_diff = (y2-y1)/(x2-x1+is_same_x), the value for lambda to be used in case x1 != x2 + let y2_minus_y1 = other.y.sub(cs.ns(|| "y2 - y1"), &self.y)?; + let x2_minus_x1_plus_x_same = x2_minus_x1.add(cs.ns(|| "x2 - x1 + x_is_same"), &is_same_x)?; + let lambda_diff = F::alloc(cs.ns(|| "alloc lambda_diff"), || Ok( + y2_minus_y1.get_value().get()?*x2_minus_x1_plus_x_same.get_value().get()?.inverse().unwrap() + // safe to unwrap inverse as x2_minus_x1_plus_x_same cannot be 0 by construction + ) + )?; + lambda_diff.mul_equals(cs.ns(|| "enforce lambda_diff = (y2-y1) div (x2-x1+is_same_x"), &x2_minus_x1_plus_x_same, &y2_minus_y1)?; + + // compute lambda_same = (3x1^2+a)/(2y1), the value for lambda to be used in case x1 = x2. + // The correct value of lambda_same can be enforced with the constraint + // 2y1*lambda_same = 3x1^2+a. + // Note that in case y1 = 0, then the value of lambda_same is unconstrained, as + // 2y1*lambda_same = 0 independently from the value of lambda_same; + // However, since we consider only curves with prime order, then there cannot be points with + // y1=0 besides the point at infinity, which is represented as x1=0, y1=0. + // Therefore, in case `self` is the identity (i.e., x1=,y1=0), then there are no values of + // lambda_same which would satisfy the constraint 2y1*lambda_same = 3x1^2+a, unless a == 0. + // Therefore, we modify the constraint as (2y1+self.infinity)*lambda_same = 3x1^2+a, which + // is satisfiable when y1=0 by simply choosing lambda_same=a + let infinity_flag_to_field = F::from(self.infinity, cs.ns(|| "self infinity to field element"))?; + let two_y1_plus_infinity_flag = self.y.double(cs.ns(|| "2y1"))?.add(cs.ns(|| "2y1+self.infinity"), &infinity_flag_to_field)?; + let three_times_x1_square_plus_a = self.x.square(cs.ns(|| "x1^2"))?.mul_by_constant(cs.ns(|| "3x1^2"), &P::BaseField::from(3u128))?.add_constant(cs.ns(|| "3x1^2+a"), &P::COEFF_A)?; + let lambda_same = F::alloc(cs.ns(|| "alloc lambda_same"), || Ok( + three_times_x1_square_plus_a.get_value().get()?*two_y1_plus_infinity_flag.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ))?; + lambda_same.mul_equals(cs.ns(|| "enforce lambda_same = (3x1^2+a) div 2y1"), &two_y1_plus_infinity_flag, &three_times_x1_square_plus_a)?; + + // set lambda to either lambda_same or lambda_diff depending on is_same_x flag + let lambda = F::alloc(cs.ns(|| "alloc lambda"), || Ok( + if is_same_x.get_value().get()?.is_one() { + lambda_same.get_value().get()? + } else { + lambda_diff.get_value().get()? + } + ))?; + let lambda_minus_diff = lambda.sub(cs.ns(|| "lambda - lambda_diff"), &lambda_diff)?; + let lambda_same_minus_diff = lambda_same.sub(cs.ns(|| "lambda_same - lambda_diff"), &lambda_diff)?; + lambda_same_minus_diff.mul_equals(cs.ns(|| "enforce (lambda-lambda_diff) = is_same_x*(lambda_same-lambda_diff)"), &is_same_x, &lambda_minus_diff)?; + + // x3 = lambda^2-x1-x2 + let x1_plus_x2 = self.x.add(cs.ns(|| "x1+x2"), &other.x)?; + let x3 = lambda.square(cs.ns(|| "lambda^2"))?.sub(cs.ns(|| "x3=lambda^2-x1-x2"), &x1_plus_x2)?; + // y3 = lambda*(x1-x3)-y1 + let x1_minus_x3 = self.x.sub(cs.ns(|| "x1-x3"), &x3)?; + let y3 = lambda.mul(cs.ns(|| "lambda*(x1-x3)"), &x1_minus_x3)?.sub(cs.ns(|| "y3=lambda*(x1-x3)-y1"), &self.y)?; + + // compute a flag is_sum_zero which is true iff self+other == identity + let y1_plus_y2 = self.y.add(cs.ns(|| "y1+y2"), &other.y)?; + let is_sum_zero = F::alloc(cs.ns(|| "alloc self+other == 0"), || Ok( + if y1_plus_y2.get_value().get()?.is_zero() { + is_same_x.get_value().get()? + } else { + P::BaseField::zero() + } + ))?; + // enforce sum_is_zero == 0 if y1+y2 != 0, that is if the sum is not the identity + y1_plus_y2.mul_equals(cs.ns(|| "enforce (y1+y2)*sum_is_zero=0"), &is_sum_zero, &zero)?; + let same_x_minus_sum_zero = is_same_x.sub(cs.ns(|| "is_same_x-sum_is_zero"), &is_sum_zero)?; + let inv = F::alloc(cs.ns(|| "alloc (y1+y2)^-1"), || Ok( + // set inv to is_same_x if y1+y2 !=0, otherwise we can set it to an arbitrary as it has no impact on the constraint + is_same_x.get_value().get()?*y1_plus_y2.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ))?; + + // enforce sum_is_zero == is_same_x if y1+y2 == 0, as in this case the sum is the identity iff the x-coordinates are the same + y1_plus_y2.mul_equals(cs.ns(|| "enforce (y1+y2)*(y1+y2)^-1=is_same_x-sum_is_zero"), &inv, &same_x_minus_sum_zero)?; + + // enforce that x4 = y4 = 0 if sum is zero + let is_sum_not_zero = is_sum_zero.negate(cs.ns(|| "-is_sum_zero"))?.add_constant(cs.ns(|| "1-is_sum_zero"), &P::BaseField::one())?; + let x4 = x3.mul(cs.ns(|| "x4 = x3*(1-is_sum_zero)"), &is_sum_not_zero)?; + let y4 = y3.mul(cs.ns(|| "y4 = y3*(1-is_sum_zero)"), &is_sum_not_zero)?; + + // deal with the case when self is the identity + let x5 = F::conditionally_select(cs.ns(|| "x5=x2 if self == 0, x4 otherwise"), &self.infinity, &other.x, &x4)?; + let y5 = F::conditionally_select(cs.ns(|| "y5=y2 if self == 0, y4 otherwise"), &self.infinity, &other.y, &y4)?; + + // deal with the case when other is the identity + let x_out = F::conditionally_select(cs.ns(|| "x_out=x1 if other == 0, x5 otherwise"), &other.infinity, &self.x, &x5)?; + let y_out = F::conditionally_select(cs.ns(|| "y_out=y1 if other == 0, y5 otherwise"), &other.infinity, &self.y, &y5)?; + + let infinity_out = F::try_into(is_sum_zero)?; + + Ok(Self::new(x_out, y_out, infinity_out)) } /// Incomplete addition: neither `self` nor `other` can be the neutral /// element. + // ToDo: make addition complete fn add_constant>( &self, mut cs: CS, @@ -805,7 +917,8 @@ where // Last chunk we must use safe add _ => { let adder: Self = Self::new(x, y, Boolean::constant(false)); - acc = acc.add(cs.ns(|| format!("Add_{}", i)), &adder)?; + // acc = acc.add(cs.ns(|| format!("Add_{}", i)), &adder)?; + acc = acc.add_internal(cs.ns(|| format!("Add_{}", i)), &adder, true)?; } } @@ -1210,7 +1323,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) @@ -1263,7 +1376,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) @@ -1372,7 +1485,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) diff --git a/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_projective.rs b/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_projective.rs index f47ff4e60..4a37f71e9 100644 --- a/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_projective.rs +++ b/r1cs/gadgets/std/src/groups/curves/short_weierstrass/short_weierstrass_projective.rs @@ -334,8 +334,8 @@ where #[inline] fn zero>(mut cs: CS) -> Result { Ok(Self::new( - F::zero(cs.ns(|| "zero"))?, - F::one(cs.ns(|| "one"))?, + F::zero(cs.ns(|| "x-zero"))?, + F::zero(cs.ns(|| "y-zero"))?, Boolean::constant(true), )) } @@ -349,14 +349,124 @@ where } #[inline] - /// Incomplete, safe, addition: neither `self` nor `other` can be the neutral - /// element. + // Algorithm for complete addition ported in R1CS from zcash: https://github.com/ebfull/halo/blob/master/src/gadgets/ecc.rs#L357 + // The algorithm from zcash works only with Weierstrass curves y^2 = x^3+b, the algorithm here + // is modified to work with generic curves y^2 = x^3 +ax + b, for b != 0 (as if b=0 then the point + // (0,0), which is currently used to represent the identity point, will belong to the curve) + //ToDo: in case in the future we may need to use curves with b=0, then it should be possible to + // modify the function to employ the point (0,1) as the representation for the identity point fn add>( &self, - cs: CS, + mut cs: CS, other: &Self, ) -> Result { - self.add_internal(cs, other, true) + let zero = F::zero(cs.ns(|| "alloc constant 0"))?; + let is_same_x = F::alloc(cs.ns(|| "alloc x1 == x2"), + || Ok( + if self.x.get_value().get()? == other.x.get_value().get()? { + P::BaseField::one() + } else { + P::BaseField::zero() + }) + )?; + let not_is_same_x = is_same_x.negate(cs.ns(|| "-is_same_x"))?.add_constant(cs.ns(|| "1 - is_same_x"), &P::BaseField::one())?; + + let x2_minus_x1 = other.x.sub(cs.ns(|| "x2 - x1"), &self.x)?; + let inv = F::alloc(cs.ns(|| "alloc (x2-x1)^-1"), || + Ok( + x2_minus_x1.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ) + )?; + + // enforce that is_same_x = 0 if x2 != x1 + x2_minus_x1.mul_equals(cs.ns(|| "enforce (x2-x1)*is_same_x = 0"), &is_same_x, &zero)?; + // enforce that is_same_x = 1 if x2 == x1 + x2_minus_x1.mul_equals(cs.ns(|| "enforce (x2-x1)*(x2-x1)^-1 = 1-is_same_x"), &inv, ¬_is_same_x)?; + + // compute lambda_diff = (y2-y1)/(x2-x1+is_same_x), the value for lambda to be used in case x1 != x2 + let y2_minus_y1 = other.y.sub(cs.ns(|| "y2 - y1"), &self.y)?; + let x2_minus_x1_plus_is_same_x = x2_minus_x1.add(cs.ns(|| "x2 - x1 + is_same_x"), &is_same_x)?; + let lambda_diff = F::alloc(cs.ns(|| "alloc lambda_diff"), || Ok( + y2_minus_y1.get_value().get()?* x2_minus_x1_plus_is_same_x.get_value().get()?.inverse().unwrap() + // safe to unwrap inverse as x2_minus_x1_plus_x_same cannot be 0 by construction + ) + )?; + lambda_diff.mul_equals(cs.ns(|| "enforce lambda_diff = (y2-y1) div (x2-x1+is_same_x"), &x2_minus_x1_plus_is_same_x, &y2_minus_y1)?; + + // compute lambda_same = (3x1^2+a)/(2y1), the value for lambda to be used in case x1 = x2. + // The correct value of lambda_same can be enforced with the constraint + // 2y1*lambda_same = 3x1^2+a. + // Note that in case y1 = 0, then the value of lambda_same is unconstrained, as + // 2y1*lambda_same = 0 independently from the value of lambda_same; + // However, since we consider only curves with prime order, then there cannot be points with + // y1=0 besides the point at infinity, which is represented as x1=0, y1=0. + // Therefore, in case `self` is the identity (i.e., x1=,y1=0), then there are no values of + // lambda_same which would satisfy the constraint 2y1*lambda_same = 3x1^2+a, unless a == 0. + // Therefore, we modify the constraint as (2y1+self.infinity)*lambda_same = 3x1^2+a, which + // is satisfiable when y1=0 by simply choosing lambda_same=a + let infinity_flag_to_field = F::from(self.infinity, cs.ns(|| "self infinity to field element"))?; + let two_y1_plus_infinity_flag = self.y.double(cs.ns(|| "2y1"))?.add(cs.ns(|| "2y1+self.infinity"), &infinity_flag_to_field)?; + let three_times_x1_square_plus_a = self.x.square(cs.ns(|| "x1^2"))?.mul_by_constant(cs.ns(|| "3x1^2"), &P::BaseField::from(3u128))?.add_constant(cs.ns(|| "3x1^2+a"), &P::COEFF_A)?; + let lambda_same = F::alloc(cs.ns(|| "alloc lambda_same"), || Ok( + three_times_x1_square_plus_a.get_value().get()?*two_y1_plus_infinity_flag.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ))?; + lambda_same.mul_equals(cs.ns(|| "enforce lambda_same = (3x1^2+a) div 2y1"), &two_y1_plus_infinity_flag, &three_times_x1_square_plus_a)?; + + // set lambda to either lambda_same or lambda_diff depending on is_same_x flag + let lambda = F::alloc(cs.ns(|| "alloc lambda"), || Ok( + if is_same_x.get_value().get()?.is_one() { + lambda_same.get_value().get()? + } else { + lambda_diff.get_value().get()? + } + ))?; + let lambda_minus_diff = lambda.sub(cs.ns(|| "lambda - lambda_diff"), &lambda_diff)?; + let lambda_same_minus_diff = lambda_same.sub(cs.ns(|| "lambda_same - lambda_diff"), &lambda_diff)?; + lambda_same_minus_diff.mul_equals(cs.ns(|| "enforce (lambda-lambda_diff) = is_same_x*(lambda_same-lambda_diff)"), &is_same_x, &lambda_minus_diff)?; + + // x3 = lambda^2-x1-x2 + let x1_plus_x2 = self.x.add(cs.ns(|| "x1+x2"), &other.x)?; + let x3 = lambda.square(cs.ns(|| "lambda^2"))?.sub(cs.ns(|| "x3=lambda^2-x1-x2"), &x1_plus_x2)?; + // y3 = lambda*(x1-x3)-y1 + let x1_minus_x3 = self.x.sub(cs.ns(|| "x1-x3"), &x3)?; + let y3 = lambda.mul(cs.ns(|| "lambda*(x1-x3)"), &x1_minus_x3)?.sub(cs.ns(|| "y3=lambda*(x1-x3)-y1"), &self.y)?; + + // compute a flag is_sum_zero which is true iff self+other == identity + let y1_plus_y2 = self.y.add(cs.ns(|| "y1+y2"), &other.y)?; + let is_sum_zero = F::alloc(cs.ns(|| "alloc self+other == 0"), || Ok( + if y1_plus_y2.get_value().get()?.is_zero() { + is_same_x.get_value().get()? + } else { + P::BaseField::zero() + } + ))?; + // enforce sum_is_zero == 0 if y1+y2 != 0, that is if the sum is not the identity + y1_plus_y2.mul_equals(cs.ns(|| "enforce (y1+y2)*sum_is_zero=0"), &is_sum_zero, &zero)?; + let same_x_minus_sum_zero = is_same_x.sub(cs.ns(|| "is_same_x-sum_is_zero"), &is_sum_zero)?; + let inv = F::alloc(cs.ns(|| "alloc (y1+y2)^-1"), || Ok( + // set inv to is_same_x if y1+y2 !=0, otherwise we can set it to an arbitrary as it has no impact on the constraint + is_same_x.get_value().get()?*y1_plus_y2.get_value().get()?.inverse().unwrap_or(P::BaseField::one()) + ))?; + + // enforce sum_is_zero == is_same_x if y1+y2 == 0, as in this case the sum is the identity iff the x-coordinates are the same + y1_plus_y2.mul_equals(cs.ns(|| "enforce (y1+y2)*(y1+y2)^-1=is_same_x-sum_is_zero"), &inv, &same_x_minus_sum_zero)?; + + // enforce that x4 = y4 = 0 if sum is zero + let is_sum_not_zero = is_sum_zero.negate(cs.ns(|| "-is_sum_zero"))?.add_constant(cs.ns(|| "1-is_sum_zero"), &P::BaseField::one())?; + let x4 = x3.mul(cs.ns(|| "x4 = x3*(1-is_sum_zero)"), &is_sum_not_zero)?; + let y4 = y3.mul(cs.ns(|| "y4 = y3*(1-is_sum_zero)"), &is_sum_not_zero)?; + + // deal with the case when self is the identity + let x5 = F::conditionally_select(cs.ns(|| "x5=x2 if self == 0, x4 otherwise"), &self.infinity, &other.x, &x4)?; + let y5 = F::conditionally_select(cs.ns(|| "y5=y2 if self == 0, y4 otherwise"), &self.infinity, &other.y, &y4)?; + + // deal with the case when other is the identity + let x_out = F::conditionally_select(cs.ns(|| "x_out=x1 if other == 0, x5 otherwise"), &other.infinity, &self.x, &x5)?; + let y_out = F::conditionally_select(cs.ns(|| "y_out=y1 if other == 0, y5 otherwise"), &other.infinity, &self.y, &y5)?; + + let infinity_out = F::try_into(is_sum_zero)?; + + Ok(Self::new(x_out, y_out, infinity_out)) } /// Incomplete addition: neither `self` nor `other` can be the neutral @@ -1210,7 +1320,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) @@ -1263,7 +1373,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) @@ -1372,7 +1482,7 @@ where Ok(ge) => { let ge = ge.borrow(); if ge.is_zero() { - (Ok(P::BaseField::zero()), Ok(P::BaseField::one()), Ok(true)) + (Ok(P::BaseField::zero()), Ok(P::BaseField::zero()), Ok(true)) } else { let ge = ge.into_affine().unwrap(); (Ok(ge.x), Ok(ge.y), Ok(false)) diff --git a/r1cs/gadgets/std/src/groups/mod.rs b/r1cs/gadgets/std/src/groups/mod.rs index 9c4743faf..4c15bcc3d 100644 --- a/r1cs/gadgets/std/src/groups/mod.rs +++ b/r1cs/gadgets/std/src/groups/mod.rs @@ -534,6 +534,11 @@ pub(crate) mod test { // a - a = 0 assert_eq!(a.sub(cs.ns(|| "a_minus_a"), &a).unwrap(), zero); + // 0 + b = b + assert_eq!(zero.add(cs.ns(|| "zero_plus_b"), &b).unwrap(), b); + // 0 - b = -b + assert_eq!(zero.sub(cs.ns(|| "zero_minus_b"), &b).unwrap(), b.negate(cs.ns(|| "-b")).unwrap()); + // a + b = b + a let a_b = a.add(cs.ns(|| "a_plus_b"), &b).unwrap(); let b_a = b.add(cs.ns(|| "b_plus_a"), &a).unwrap(); @@ -554,6 +559,11 @@ pub(crate) mod test { let b_b = b.add(cs.ns(|| "b + b"), &b).unwrap(); assert_eq!(b2, b_b); + // 0 + 0 = 0 + assert_eq!(zero.add(cs.ns(|| "0+0"), &zero).unwrap(), zero); + // 0 - 0 = 0 + assert_eq!(zero.sub(cs.ns(|| "0-0"), &zero).unwrap(), zero); + let _ = a.to_bytes(&mut cs.ns(|| "ToBytes")).unwrap(); let _ = a.to_bytes_strict(&mut cs.ns(|| "ToBytes Strict")).unwrap(); @@ -626,6 +636,9 @@ pub(crate) mod test { let _ = b .to_bytes_strict(&mut cs.ns(|| "b ToBytes Strict")) .unwrap(); + if !cs.is_satisfied() { + println!("{:?}", cs.which_is_unsatisfied()); + } assert!(cs.is_satisfied()); scalar_bits_to_constant_length_test::<::BasePrimeField, G>(); diff --git a/r1cs/gadgets/std/src/groups/nonnative/short_weierstrass/short_weierstrass_jacobian.rs b/r1cs/gadgets/std/src/groups/nonnative/short_weierstrass/short_weierstrass_jacobian.rs index 548be2834..9e041620c 100644 --- a/r1cs/gadgets/std/src/groups/nonnative/short_weierstrass/short_weierstrass_jacobian.rs +++ b/r1cs/gadgets/std/src/groups/nonnative/short_weierstrass/short_weierstrass_jacobian.rs @@ -56,6 +56,8 @@ where type Value = Jacobian

; type Variable = (); + /// Incomplete, safe, addition: neither `self` nor `other` can be the neutral + /// element. fn add>( &self, cs: CS, diff --git a/r1cs/gadgets/std/src/instantiated/tweedle/curves.rs b/r1cs/gadgets/std/src/instantiated/tweedle/curves.rs index 88f85f4a4..64714c61c 100644 --- a/r1cs/gadgets/std/src/instantiated/tweedle/curves.rs +++ b/r1cs/gadgets/std/src/instantiated/tweedle/curves.rs @@ -13,6 +13,7 @@ pub type TweedleDumGadget = AffineGadget; #[test] fn test_dee() { crate::groups::test::group_test_with_incomplete_add::<_, _, TweedleDeeGadget>(); + crate::groups::test::group_test::<_,_,TweedleDeeGadget>(); crate::groups::test::mul_bits_test::<_, _, TweedleDeeGadget>(); crate::groups::test::fixed_base_msm_test::<_, _, TweedleDeeGadget>(); crate::groups::test::endo_mul_test::<_, _, TweedleDeeGadget>(); @@ -21,6 +22,7 @@ fn test_dee() { #[test] fn test_dum() { crate::groups::test::group_test_with_incomplete_add::<_, _, TweedleDumGadget>(); + crate::groups::test::group_test::<_, _, TweedleDumGadget>(); crate::groups::test::mul_bits_test::<_, _, TweedleDumGadget>(); crate::groups::test::fixed_base_msm_test::<_, _, TweedleDeeGadget>(); crate::groups::test::endo_mul_test::<_, _, TweedleDumGadget>();