fix RO absorb counts

lurk-lang · Feb 7, 2024 · c88ab38 · c88ab38
1 parent 501a664
commit c88ab38
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 8 deletions.
diff --git a/src/constants.rs b/src/constants.rs
@@ -5,6 +5,7 @@ pub(crate) const BN_LIMB_WIDTH: usize = 64;
 pub(crate) const BN_N_LIMBS: usize = 4;
 pub(crate) const NUM_FE_WITHOUT_IO_FOR_CRHF: usize = 17;
 pub(crate) const NUM_FE_FOR_RO: usize = 9;
+pub(crate) const NUM_FE_IN_EMULATED_POINT: usize = 2 * BN_N_LIMBS + 1;
 
 /// Bit size of Nova field element hashes
 pub const NUM_HASH_BITS: usize = 250;
diff --git a/src/cyclefold/gadgets.rs b/src/cyclefold/gadgets.rs
@@ -64,7 +64,7 @@ pub mod emulated {
   use std::marker::PhantomData;
 
   use crate::{
-    constants::{NUM_CHALLENGE_BITS, NUM_FE_FOR_RO},
+    constants::{/*BN_N_LIMBS,*/ NUM_CHALLENGE_BITS, NUM_FE_IN_EMULATED_POINT, /*NUM_FE_FOR_RO*/},
     gadgets::{
       nonnative::{bignat::BigNat, util::f_to_nat},
       utils::{
@@ -383,7 +383,10 @@ pub mod emulated {
       comm_T: &AllocatedPoint<E1, E2>,
       ro_consts: ROConstantsCircuit<E1>,
     ) -> Result<Self, SynthesisError> {
-      let mut ro = E1::ROCircuit::new(ro_consts, NUM_FE_FOR_RO);
+      let mut ro = E1::ROCircuit::new(
+        ro_consts,
+        1 + NUM_FE_IN_EMULATED_POINT + 2 + NUM_FE_IN_EMULATED_POINT, // pp_digest + u.W + u.x + comm_T
+      );
 
       ro.absorb(pp_digest);
 

diff --git a/src/cyclefold/nova_circuit.rs b/src/cyclefold/nova_circuit.rs
@@ -1,7 +1,7 @@
 //! This module defines the Nova augmented circuit used for Cyclefold
 
 use crate::{
-  constants::{NUM_FE_WITHOUT_IO_FOR_CRHF, NUM_HASH_BITS},
+  constants::{NUM_FE_IN_EMULATED_POINT, NUM_FE_WITHOUT_IO_FOR_CRHF, NUM_HASH_BITS},
   gadgets::{
     r1cs::AllocatedRelaxedR1CSInstance,
     utils::{
@@ -304,7 +304,7 @@ where
     // Follows the outline written down here https://hackmd.io/@mpenciak/HybHrnNFT
     let mut ro_p = E1::ROCircuit::new(
       self.ro_consts.clone(),
-      NUM_FE_WITHOUT_IO_FOR_CRHF + 2 * arity,
+      2 + 2 * arity + 2 * NUM_FE_IN_EMULATED_POINT + 3,
     );
 
     ro_p.absorb(pp_digest);
@@ -331,6 +331,7 @@ where
     let mut ro_c = E1::ROCircuit::new(self.ro_consts.clone(), NUM_FE_WITHOUT_IO_FOR_CRHF);
 
     ro_c.absorb(pp_digest);
+    ro_c.absorb(i);
     data_c_1
       .U
       .absorb_in_ro(cs.namespace(|| "absorb U_c"), &mut ro_c)?;
@@ -361,15 +362,15 @@ where
     )?;
 
     // Calculate h_int = H(pp, U_c_int)
-    let mut ro_c_int = E1::ROCircuit::new(self.ro_consts.clone(), NUM_FE_WITHOUT_IO_FOR_CRHF);
+    let mut ro_c_int = E1::ROCircuit::new(self.ro_consts.clone(), NUM_FE_WITHOUT_IO_FOR_CRHF - 1);
     ro_c_int.absorb(pp_digest);
     U_int.absorb_in_ro(cs.namespace(|| "absorb U_c_int"), &mut ro_c_int)?;
     let h_c_int_bits =
       ro_c_int.squeeze(cs.namespace(|| "intermediate hash bits"), NUM_HASH_BITS)?;
     let h_c_int = le_bits_to_num(cs.namespace(|| "intermediate hash"), &h_c_int_bits)?;
 
     // Calculate h_1 = H(pp, U_c_1)
-    let mut ro_c_1 = E1::ROCircuit::new(self.ro_consts.clone(), NUM_FE_WITHOUT_IO_FOR_CRHF);
+    let mut ro_c_1 = E1::ROCircuit::new(self.ro_consts.clone(), NUM_FE_WITHOUT_IO_FOR_CRHF - 1);
     ro_c_1.absorb(pp_digest);
     data_c_2
       .U
@@ -418,7 +419,7 @@ where
     let arity = self.step_circuit.arity();
 
     let (pp_digest, i, z_0, z_i, data_p, data_c_1, data_c_2, E_new, W_new) =
-      self.alloc_witness(cs.namespace(|| "alloc_witness"), self.params.n_limbs)?;
+      self.alloc_witness(cs.namespace(|| "alloc_witness"), arity)?;
 
     let zero = alloc_zero(cs.namespace(|| "zero"));
     let is_base_case = alloc_num_equals(cs.namespace(|| "is base case"), &i, &zero)?;
@@ -496,7 +497,7 @@ where
 
     let mut ro_p = E1::ROCircuit::new(
       self.ro_consts.clone(),
-      NUM_FE_WITHOUT_IO_FOR_CRHF + 2 * arity,
+      2 + 2 * arity + 2 * NUM_FE_IN_EMULATED_POINT + 3,
     );
     ro_p.absorb(&pp_digest);
     ro_p.absorb(&i_new);
@@ -512,6 +513,7 @@ where
 
     let mut ro_c = E1::ROCircuit::new(self.ro_consts, NUM_FE_WITHOUT_IO_FOR_CRHF);
     ro_c.absorb(&pp_digest);
+    ro_c.absorb(&i_new);
     Unew_c.absorb_in_ro(cs.namespace(|| "absorb Unew_c"), &mut ro_c)?;
     let hash_c_bits = ro_c.squeeze(cs.namespace(|| "hash_c_bits"), NUM_HASH_BITS)?;
     let hash_c = le_bits_to_num(cs.namespace(|| "hash_c"), &hash_c_bits)?;
@@ -522,3 +524,52 @@ where
     Ok(z_next)
   }
 }
+
+#[cfg(test)]
+mod test {
+  use crate::{
+    bellpepper::test_shape_cs::TestShapeCS,
+    constants::{BN_LIMB_WIDTH, BN_N_LIMBS},
+    provider::{
+      Bn256Engine, GrumpkinEngine, PallasEngine, Secp256k1Engine, Secq256k1Engine, VestaEngine,
+    },
+    traits::circuit::TrivialCircuit,
+  };
+
+  use super::*;
+
+  fn test_circuit_size_with<E1, E2>()
+  where
+    E1: Engine<Base = <E2 as Engine>::Scalar>,
+    E2: Engine<Base = <E1 as Engine>::Scalar>,
+  {
+    let params = AugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS);
+
+    let ro_consts = ROConstantsCircuit::<E1>::default();
+
+    let step_circuit = TrivialCircuit::<E2::Scalar>::default();
+
+    let circuit = AugmentedCircuit::<E1, E2, TrivialCircuit<E2::Scalar>>::new(
+      &params,
+      ro_consts,
+      None,
+      &step_circuit,
+    );
+    let mut cs: TestShapeCS<E2> = TestShapeCS::default();
+
+    let _ = circuit.synthesize(&mut cs);
+
+    let num_constraints = cs.num_constraints();
+    let num_variables = cs.num_aux();
+
+    assert_eq!(num_constraints, 0);
+    assert_eq!(num_variables, 0);
+  }
+
+  #[test]
+  fn test_circuit_size() {
+    test_circuit_size_with::<PallasEngine, VestaEngine>();
+    test_circuit_size_with::<Secp256k1Engine, Secq256k1Engine>();
+    test_circuit_size_with::<Bn256Engine, GrumpkinEngine>();
+  }
+}