Introduce checks about AllocatedPoint (#258)

* introduce checks on AllocatedPoint

* update version

* fix test_pp_digest

* optimize checks

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "nova-snark"
-version = "0.30.1"
+version = "0.31.0"
 authors = ["Srinath Setty <srinath@microsoft.com>"]
 edition = "2021"
 description = "Recursive zkSNARKs without trusted setup"

src/circuit.rs

@@ -172,6 +172,7 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> NovaAugmentedCircuit<'a, G, SC> {
         .as_ref()
         .and_then(|inputs| inputs.T.map(|T| T.to_coordinates())),
     )?;
+    T.check_on_curve(cs.namespace(|| "check T on curve"))?;
 
     Ok((params, i, z_0, z_i, U, u, T))
   }
@@ -452,7 +453,7 @@ mod tests {
     let ro_consts2: ROConstantsCircuit<PastaG1> = PoseidonConstantsCircuit::default();
 
     test_recursive_circuit_with::<PastaG1, PastaG2>(
-      &params1, &params2, ro_consts1, ro_consts2, 9815, 10347,
+      &params1, &params2, ro_consts1, ro_consts2, 9825, 10357,
     );
   }
 
@@ -468,7 +469,7 @@ mod tests {
     test_recursive_circuit_with::<
       provider::bn256_grumpkin::bn256::Point,
       provider::bn256_grumpkin::grumpkin::Point,
-    >(&params1, &params2, ro_consts1, ro_consts2, 9983, 10536);
+    >(&params1, &params2, ro_consts1, ro_consts2, 9993, 10546);
   }
 
   #[test]
@@ -483,6 +484,6 @@ mod tests {
     test_recursive_circuit_with::<
       provider::secp_secq::secp256k1::Point,
       provider::secp_secq::secq256k1::Point,
-    >(&params1, &params2, ro_consts1, ro_consts2, 10262, 10959);
+    >(&params1, &params2, ro_consts1, ro_consts2, 10272, 10969);
   }
 }

src/gadgets/ecc.rs

@@ -63,7 +63,53 @@ where
     Ok(AllocatedPoint { x, y, is_infinity })
   }
 
-  /// Allocates a default point on the curve.
+  /// checks if `self` is on the curve or if it is infinity
+  pub fn check_on_curve<CS>(&self, mut cs: CS) -> Result<(), SynthesisError>
+  where
+    CS: ConstraintSystem<G::Base>,
+  {
+    // check that (x,y) is on the curve if it is not infinity
+    // we will check that (1- is_infinity) * y^2 = (1-is_infinity) * (x^3 + Ax + B)
+    // note that is_infinity is already restricted to be in the set {0, 1}
+    let y_square = self.y.square(cs.namespace(|| "y_square"))?;
+    let x_square = self.x.square(cs.namespace(|| "x_square"))?;
+    let x_cube = self.x.mul(cs.namespace(|| "x_cube"), &x_square)?;
+
+    let rhs = AllocatedNum::alloc(cs.namespace(|| "rhs"), || {
+      if *self.is_infinity.get_value().get()? == G::Base::ONE {
+        Ok(G::Base::ZERO)
+      } else {
+        Ok(
+          *x_cube.get_value().get()?
+            + *self.x.get_value().get()? * G::get_curve_params().0
+            + G::get_curve_params().1,
+        )
+      }
+    })?;
+
+    cs.enforce(
+      || "rhs = (1-is_infinity) * (x^3 + Ax + B)",
+      |lc| {
+        lc + x_cube.get_variable()
+          + (G::get_curve_params().0, self.x.get_variable())
+          + (G::get_curve_params().1, CS::one())
+      },
+      |lc| lc + CS::one() - self.is_infinity.get_variable(),
+      |lc| lc + rhs.get_variable(),
+    );
+
+    // check that (1-infinity) * y_square = rhs
+    cs.enforce(
+      || "check that y_square * (1 - is_infinity) = rhs",
+      |lc| lc + y_square.get_variable(),
+      |lc| lc + CS::one() - self.is_infinity.get_variable(),
+      |lc| lc + rhs.get_variable(),
+    );
+
+    Ok(())
+  }
+
+  /// Allocates a default point on the curve, set to the identity point.
   pub fn default<CS>(mut cs: CS) -> Result<Self, SynthesisError>
   where
     CS: ConstraintSystem<G::Base>,

src/gadgets/r1cs.rs

@@ -33,11 +33,11 @@ impl<G: Group> AllocatedR1CSInstance<G> {
     mut cs: CS,
     u: Option<&R1CSInstance<G>>,
   ) -> Result<Self, SynthesisError> {
-    // Check that the incoming instance has exactly 2 io
     let W = AllocatedPoint::alloc(
       cs.namespace(|| "allocate W"),
       u.map(|u| u.comm_W.to_coordinates()),
     )?;
+    W.check_on_curve(cs.namespace(|| "check W on curve"))?;
 
     let X0 = alloc_scalar_as_base::<G, _>(cs.namespace(|| "allocate X[0]"), u.map(|u| u.X[0]))?;
     let X1 = alloc_scalar_as_base::<G, _>(cs.namespace(|| "allocate X[1]"), u.map(|u| u.X[1]))?;
@@ -72,6 +72,9 @@ impl<G: Group> AllocatedRelaxedR1CSInstance<G> {
     limb_width: usize,
     n_limbs: usize,
   ) -> Result<Self, SynthesisError> {
+    // We do not need to check that W or E are well-formed (e.g., on the curve) as we do a hash check
+    // in the Nova augmented circuit, which ensures that the relaxed instance
+    // came from a prior iteration of Nova.
     let W = AllocatedPoint::alloc(
       cs.namespace(|| "allocate W"),
       inst.map(|inst| inst.comm_W.to_coordinates()),
@@ -116,6 +119,9 @@ impl<G: Group> AllocatedRelaxedR1CSInstance<G> {
 
     let u = W.x.clone(); // In the default case, W.x = u = 0
 
+    // X0 and X1 are allocated and in the honest prover case set to zero
+    // If the prover is malicious, it can set to arbitrary values, but the resulting
+    // relaxed R1CS instance with the the checked default values of W, E, and u must still be satisfying
     let X0 = BigNat::alloc_from_nat(
       cs.namespace(|| "allocate x_default[0]"),
       || Ok(f_to_nat(&G::Scalar::ZERO)),
@@ -141,7 +147,7 @@ impl<G: Group> AllocatedRelaxedR1CSInstance<G> {
     limb_width: usize,
     n_limbs: usize,
   ) -> Result<Self, SynthesisError> {
-    let E = AllocatedPoint::default(cs.namespace(|| "allocate W"))?;
+    let E = AllocatedPoint::default(cs.namespace(|| "allocate default E"))?;
 
     let u = alloc_one(cs.namespace(|| "one"));
 

src/lib.rs

@@ -962,13 +962,13 @@ mod tests {
     test_pp_digest_with::<G1, G2, _, _>(
       &trivial_circuit1,
       &trivial_circuit2,
-      "117ac6f33d66d377346e420f0d8caa09f8f4ec7db0c336dcc65995bf3058bf01",
+      "cb581e2d5c4b2ef2ddbe2d6849e0da810352f59bcdaca51476dcf9e16072f100",
     );
 
     test_pp_digest_with::<G1, G2, _, _>(
       &cubic_circuit1,
       &trivial_circuit2,
-      "583c9964e180332e63a59450870a72b4cbf663ce0d274ac5bd0d052d4cd92903",
+      "3cc29bb864910463e0501bac84cdefc1d4327e9c2ef5b0fd6d45ad1741f1a401",
     );
 
     let trivial_circuit1_grumpkin = TrivialCircuit::<<bn256::Point as Group>::Scalar>::default();
@@ -978,12 +978,12 @@ mod tests {
     test_pp_digest_with::<bn256::Point, grumpkin::Point, _, _>(
       &trivial_circuit1_grumpkin,
       &trivial_circuit2_grumpkin,
-      "fb6805b7197f41ae2af71dc0130d4bfd1d28fa63b8221741b597dfbb2e48d603",
+      "c26cc841d42c19bf98bc2482e66cd30903922f2a923927b85d66f375a821f101",
     );
     test_pp_digest_with::<bn256::Point, grumpkin::Point, _, _>(
       &cubic_circuit1_grumpkin,
       &trivial_circuit2_grumpkin,
-      "684b2f7151031a79310f6fb553ab1480e290d73731fa34e74c27e004d589f102",
+      "4c484cab71e93dda69b420beb7276af969c2034a7ffb0ea8e6964e96a7e5a901",
     );
 
     let trivial_circuit1_secp = TrivialCircuit::<<secp256k1::Point as Group>::Scalar>::default();
@@ -993,12 +993,12 @@ mod tests {
     test_pp_digest_with::<secp256k1::Point, secq256k1::Point, _, _>(
       &trivial_circuit1_secp,
       &trivial_circuit2_secp,
-      "dbffd48ae0d05f3aeb217e971fbf3b2b7a759668221f6d6cb9032cfa0445aa01",
+      "b794d655fb39891eaf530ca3be1ec2a5ac97f72a0d07c45dbb84529d8a611502",
     );
     test_pp_digest_with::<secp256k1::Point, secq256k1::Point, _, _>(
       &cubic_circuit1_secp,
       &trivial_circuit2_secp,
-      "24e4e8044310e3167196276cc66b4f71b5d0e3e57701dddb17695ae968fba802",
+      "50e6acf363c31c2ac1c9c646b4494cb21aae6cb648c7b0d4c95015c811fba302",
     );
   }
 

src/r1cs/mod.rs

@@ -89,7 +89,7 @@ impl<G: Group> R1CS<G> {
   /// # Arguments
   ///
   /// * `S`: The shape of the R1CS matrices.
-  /// * `commitment_key_hint`: A function that provides a floor for the number of generators. A good function
+  /// * `ck_floor`: A function that provides a floor for the number of generators. A good function
   ///   to provide is the ck_floor field defined in the trait `RelaxedR1CSSNARKTrait`.
   ///
   pub fn commitment_key(S: &R1CSShape<G>, ck_floor: &CommitmentKeyHint<G>) -> CommitmentKey<G> {