mirror of
https://github.com/arnaucube/Nova.git
synced 2026-01-11 00:21:29 +01:00
optimize point add constraints (#106)
* optimize add constraints * optimize double by rewriting a constraint involving an inverted element
This commit is contained in:
@@ -412,7 +412,7 @@ mod tests {
|
|||||||
let mut cs: ShapeCS<G1> = ShapeCS::new();
|
let mut cs: ShapeCS<G1> = ShapeCS::new();
|
||||||
let _ = circuit1.synthesize(&mut cs);
|
let _ = circuit1.synthesize(&mut cs);
|
||||||
let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
|
let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
|
||||||
assert_eq!(cs.num_constraints(), 19739);
|
assert_eq!(cs.num_constraints(), 18967);
|
||||||
|
|
||||||
// Initialize the shape and gens for the secondary
|
// Initialize the shape and gens for the secondary
|
||||||
let circuit2: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
|
let circuit2: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
|
||||||
@@ -425,7 +425,7 @@ mod tests {
|
|||||||
let mut cs: ShapeCS<G2> = ShapeCS::new();
|
let mut cs: ShapeCS<G2> = ShapeCS::new();
|
||||||
let _ = circuit2.synthesize(&mut cs);
|
let _ = circuit2.synthesize(&mut cs);
|
||||||
let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
|
let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
|
||||||
assert_eq!(cs.num_constraints(), 20271);
|
assert_eq!(cs.num_constraints(), 19499);
|
||||||
|
|
||||||
// Execute the base case for the primary
|
// Execute the base case for the primary
|
||||||
let zero1 = <<G2 as Group>::Base as Field>::zero();
|
let zero1 = <<G2 as Group>::Base as Field>::zero();
|
||||||
|
|||||||
@@ -214,39 +214,24 @@ where
|
|||||||
&x_diff_is_actual,
|
&x_diff_is_actual,
|
||||||
)?;
|
)?;
|
||||||
|
|
||||||
let x_diff_inv = AllocatedNum::alloc(cs.namespace(|| "x diff inverse"), || {
|
let lambda = AllocatedNum::alloc(cs.namespace(|| "lambda"), || {
|
||||||
if *x_diff_is_actual.get_value().get()? == Fp::one() {
|
let x_diff_inv = if *x_diff_is_actual.get_value().get()? == Fp::one() {
|
||||||
// Set to default
|
// Set to default
|
||||||
Ok(Fp::one())
|
Fp::one()
|
||||||
} else {
|
} else {
|
||||||
// Set to the actual inverse
|
// Set to the actual inverse
|
||||||
let inv = (*other.x.get_value().get()? - *self.x.get_value().get()?).invert();
|
(*other.x.get_value().get()? - *self.x.get_value().get()?)
|
||||||
if inv.is_some().unwrap_u8() == 1 {
|
.invert()
|
||||||
Ok(inv.unwrap())
|
.unwrap()
|
||||||
} else {
|
};
|
||||||
Err(SynthesisError::DivisionByZero)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
})?;
|
|
||||||
|
|
||||||
cs.enforce(
|
Ok((*other.y.get_value().get()? - *self.y.get_value().get()?) * x_diff_inv)
|
||||||
|| "Check inverse",
|
|
||||||
|lc| lc + x_diff.get_variable(),
|
|
||||||
|lc| lc + x_diff_inv.get_variable(),
|
|
||||||
|lc| lc + CS::one(),
|
|
||||||
);
|
|
||||||
|
|
||||||
let lambda = AllocatedNum::alloc(cs.namespace(|| "lambda"), || {
|
|
||||||
Ok(
|
|
||||||
(*other.y.get_value().get()? - *self.y.get_value().get()?)
|
|
||||||
* x_diff_inv.get_value().get()?,
|
|
||||||
)
|
|
||||||
})?;
|
})?;
|
||||||
cs.enforce(
|
cs.enforce(
|
||||||
|| "Check that lambda is correct",
|
|| "Check that lambda is correct",
|
||||||
|lc| lc + other.y.get_variable() - self.y.get_variable(),
|
|
||||||
|lc| lc + x_diff_inv.get_variable(),
|
|
||||||
|lc| lc + lambda.get_variable(),
|
|lc| lc + lambda.get_variable(),
|
||||||
|
|lc| lc + x_diff.get_variable(),
|
||||||
|
|lc| lc + other.y.get_variable() - self.y.get_variable(),
|
||||||
);
|
);
|
||||||
|
|
||||||
//************************************************************************/
|
//************************************************************************/
|
||||||
@@ -358,37 +343,24 @@ where
|
|||||||
|
|
||||||
let tmp = select_one_or_num2(cs.namespace(|| "tmp"), &tmp_actual, &self.is_infinity)?;
|
let tmp = select_one_or_num2(cs.namespace(|| "tmp"), &tmp_actual, &self.is_infinity)?;
|
||||||
|
|
||||||
// Compute inv = tmp.invert
|
|
||||||
let tmp_inv = AllocatedNum::alloc(cs.namespace(|| "tmp inverse"), || {
|
|
||||||
if *self.is_infinity.get_value().get()? == Fp::one() {
|
|
||||||
// Return default value 1
|
|
||||||
Ok(Fp::one())
|
|
||||||
} else {
|
|
||||||
// Return the actual inverse
|
|
||||||
let inv = (*tmp.get_value().get()?).invert();
|
|
||||||
if inv.is_some().unwrap_u8() == 1 {
|
|
||||||
Ok(inv.unwrap())
|
|
||||||
} else {
|
|
||||||
Err(SynthesisError::DivisionByZero)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
})?;
|
|
||||||
cs.enforce(
|
|
||||||
|| "Check inverse",
|
|
||||||
|lc| lc + tmp.get_variable(),
|
|
||||||
|lc| lc + tmp_inv.get_variable(),
|
|
||||||
|lc| lc + CS::one(),
|
|
||||||
);
|
|
||||||
|
|
||||||
// Now compute lambda as (Fp::one() + Fp::one + Fp::one()) * self.x * self.x * tmp_inv
|
// Now compute lambda as (Fp::one() + Fp::one + Fp::one()) * self.x * self.x * tmp_inv
|
||||||
let prod_1 = AllocatedNum::alloc(cs.namespace(|| "alloc prod 1"), || {
|
let prod_1 = AllocatedNum::alloc(cs.namespace(|| "alloc prod 1"), || {
|
||||||
Ok(*tmp_inv.get_value().get()? * self.x.get_value().get()?)
|
let tmp_inv = if *self.is_infinity.get_value().get()? == Fp::one() {
|
||||||
|
// Return default value 1
|
||||||
|
Fp::one()
|
||||||
|
} else {
|
||||||
|
// Return the actual inverse
|
||||||
|
(*tmp.get_value().get()?).invert().unwrap()
|
||||||
|
};
|
||||||
|
|
||||||
|
Ok(tmp_inv * self.x.get_value().get()?)
|
||||||
})?;
|
})?;
|
||||||
|
|
||||||
cs.enforce(
|
cs.enforce(
|
||||||
|| "Check prod 1",
|
|| "Check prod 1",
|
||||||
|lc| lc + self.x.get_variable(),
|
|lc| lc + tmp.get_variable(),
|
||||||
|lc| lc + tmp_inv.get_variable(),
|
|
||||||
|lc| lc + prod_1.get_variable(),
|
|lc| lc + prod_1.get_variable(),
|
||||||
|
|lc| lc + self.x.get_variable(),
|
||||||
);
|
);
|
||||||
|
|
||||||
let prod_2 = AllocatedNum::alloc(cs.namespace(|| "alloc prod 2"), || {
|
let prod_2 = AllocatedNum::alloc(cs.namespace(|| "alloc prod 2"), || {
|
||||||
|
|||||||
Reference in New Issue
Block a user