IT WORKS!

- Rework primary IO.
  - Return transcript and state hash
- Use correct Poseidon for sponge
- Impl `eq_native` methods for comparing allocated types
- Add ability to generate dummy proofs as initial input to the circuit
- Fix `AllocatedPoint::enforce_trivial`
- Impl CycleFold circuit
  - Ensure IO matches
  - Add Poseidon hashing of points
- Fix AllocatedBase
  - fix `big_int_to_limbs`
  - fix other limb issues
  - add test
- Fix `enforce_trivial` for `AllocatedBase` elements
- Fix r_bits to r conversion
- add recursive snark verification
- use sponge for hashing state due to variable size

src/parafold/circuit.rs

@@ -6,26 +6,27 @@ use crate::parafold::transcript::TranscriptConstants;
 use crate::supernova::StepCircuit;
 use crate::traits::CurveCycleEquipped;
 
-#[allow(unused)]
 pub fn synthesize_step<E, CS, SF>(
   mut cs: CS,
   ro_consts: &TranscriptConstants<E::Scalar>,
   proof: NIVCUpdateProof<E>,
   step_circuit: &SF,
-) -> Result<NIVCIO<E>, SynthesisError>
+) -> Result<(Option<NIVCIO<E>>, AllocatedNIVCState<E>), SynthesisError>
 where
   E: CurveCycleEquipped,
   CS: ConstraintSystem<E::Scalar>,
   SF: StepCircuit<E::Scalar>,
 {
   // Fold proof for previous state
-  let mut state = AllocatedNIVCState::from_proof(cs.namespace(|| "verify self"), ro_consts, proof)?;
+  let (mut state, transcript_state) =
+    AllocatedNIVCState::from_proof(cs.namespace(|| "verify self"), ro_consts, proof)?;
 
-  let io_native = state.update_io(cs.namespace(|| "step"), step_circuit);
+  let io = state.update_io(cs.namespace(|| "step"), step_circuit)?;
 
   state.inputize(cs.namespace(|| "inputize state"))?;
+  transcript_state.inputize(cs.namespace(|| "inputize transcript"))?;
 
-  io_native
+  Ok((io, state))
 }
 
 // /// Circuit

src/parafold/cycle_fold/gadgets/ecc.rs

@@ -1,13 +1,14 @@
 use bellpepper::gadgets::Assignment;
+use bellpepper_core::{ConstraintSystem, SynthesisError};
 use bellpepper_core::boolean::{AllocatedBit, Boolean};
 use bellpepper_core::num::AllocatedNum;
-
 use bellpepper_core::SynthesisError::AssignmentMissing;
-use bellpepper_core::{ConstraintSystem, SynthesisError};
 use ff::{Field, PrimeField};
-use neptune::circuit2::{Elt, PoseidonCircuit2};
+use neptune::circuit2::{Elt, poseidon_hash_allocated};
 use neptune::generic_array::typenum::U2;
+use neptune::hash_type::HashType;
 use neptune::poseidon::PoseidonConstants;
+use neptune::Strength;
 
 use crate::gadgets::utils::{
   alloc_num_equals, alloc_one, alloc_zero, conditionally_select, conditionally_select2,
@@ -52,10 +53,10 @@ impl<G: Group> AllocatedPoint<G> {
     // is_trivial => (is_identity == 1)
     // is_trivial == is_identity
     cs.enforce(
-      || "is_trivial - E.is_infinity = 0",
-      |lc| lc,
+      || "(is_trivial) * (1-is_infinity) = 0",
+      |_| is_trivial.lc(CS::one(), G::Base::ONE),
+      |lc| lc + CS::one() - self.is_infinity.get_variable(),
       |lc| lc,
-      |_| is_trivial.lc(CS::one(), G::Base::ONE) - self.is_infinity.get_variable(),
     );
   }
 
@@ -100,17 +101,17 @@ impl<G: Group> AllocatedPoint<G> {
   where
     CS: ConstraintSystem<G::Base>,
   {
-    let constants = PoseidonConstants::<G::Base, U2>::new();
-    let hash = PoseidonCircuit2::new(
-      vec![
-        Elt::Allocated(self.x.clone()),
-        Elt::Allocated(self.y.clone()),
-      ],
+    let constants = PoseidonConstants::<G::Base, U2>::new_with_strength_and_type(
+      Strength::Standard,
+      HashType::ConstantLength(2),
+    );
+    let hash = poseidon_hash_allocated(
+      cs.namespace(|| "hash"),
+      vec![self.x.clone(), self.y.clone()],
       &constants,
-    )
-    .hash_to_allocated(cs.namespace(|| "hash"))?;
+    )?;
 
-    let hash_final = AllocatedNum::alloc(cs.namespace(|| "alloc hash"), || {
+    let hash_final = AllocatedNum::alloc_input(cs.namespace(|| "alloc hash"), || {
       let is_infinity = self.is_infinity.get_value().ok_or(AssignmentMissing)?;
       if is_infinity == G::Base::ONE {
         Ok(G::Base::ZERO)
@@ -126,7 +127,7 @@ impl<G: Group> AllocatedPoint<G> {
       |lc| lc + hash.get_variable(),
       |lc| lc + hash_final.get_variable(),
     );
-    hash_final.inputize(cs.namespace(|| "inputize"))
+    Ok(())
   }
 
   /// Allocates a new point on the curve using coordinates provided by `coords`.
@@ -701,8 +702,8 @@ impl<G: Group> AllocatedPoint<G> {
   }
 }
 
-#[derive(Clone)]
 /// `AllocatedPoint` but one that is guaranteed to be not infinity
+#[derive(Clone)]
 pub struct AllocatedPointNonInfinity<G: Group> {
   x: AllocatedNum<G::Base>,
   y: AllocatedNum<G::Base>,

src/parafold/cycle_fold/gadgets/emulated.rs

@@ -1,18 +1,18 @@
 use std::marker::PhantomData;
-use std::ops::{BitAnd, Shr};
+use std::ops::BitAnd;
 
+use bellpepper_core::{ConstraintSystem, SynthesisError, Variable};
 use bellpepper_core::boolean::{AllocatedBit, Boolean};
 use bellpepper_core::num::{AllocatedNum, Num};
-use bellpepper_core::{ConstraintSystem, SynthesisError, Variable};
 use bellpepper_emulated::field_element::{
   EmulatedFieldElement, EmulatedFieldParams, EmulatedLimbs,
 };
 use bellpepper_emulated::util::bigint_to_scalar;
 use ff::{Field, PrimeField, PrimeFieldBits};
-use itertools::zip_eq;
+use itertools::{Itertools, zip_eq};
 use neptune::circuit2::Elt;
 use num_bigint::{BigInt, Sign};
-use num_traits::{Num as num_Num, One};
+use num_traits::{Num as num_Num, One, Zero};
 
 use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
 use crate::traits::CurveCycleEquipped;
@@ -40,21 +40,28 @@ impl<E: CurveCycleEquipped> EmulatedFieldParams for BaseParams<E> {
 }
 
 impl<E: CurveCycleEquipped> BaseParams<E> {
-  pub fn base_to_limb(base: E::Base) -> Vec<E::Scalar> {
+  pub fn base_to_limbs(base: &E::Base) -> Vec<E::Scalar> {
     Self::big_int_to_limbs(field_to_big_int(base))
   }
-  pub fn big_int_to_limbs(base: BigInt) -> Vec<E::Scalar> {
+
+  pub fn big_int_to_limbs(mut base: BigInt) -> Vec<E::Scalar> {
     let num_bits = BaseParams::<E>::bits_per_limb() as u32;
     let num_limbs = BaseParams::<E>::num_limbs() as u32;
     let mask = BigInt::from(2).pow(num_bits) - BigInt::one();
 
-    (0..num_limbs)
-      .map(|limb_index| {
-        let shift = (limb_index * num_bits) as u8;
-        let limb = base.clone().shr(shift).bitand(&mask);
+    let limbs = (0..num_limbs)
+      .map(|_| {
+        let limb = base.clone().bitand(&mask);
+        base >>= num_bits;
         bigint_to_scalar::<E::Scalar>(&limb)
       })
-      .collect()
+      .collect();
+    assert!(
+      base.is_zero(),
+      "input must be at most {} bits",
+      num_bits * num_limbs
+    );
+    limbs
   }
 }
 
@@ -67,6 +74,24 @@ impl<E: CurveCycleEquipped> AllocatedBase<E> {
     Self(EmulatedFieldElement::zero())
   }
 
+  pub fn enforce_zero<CS: ConstraintSystem<E::Scalar>>(&self, mut cs: CS, is_zero: &Boolean) {
+    for (i, limb) in self.as_preimage().into_iter().enumerate() {
+      cs.enforce(
+        || format!("limb {i} is zero"),
+        |_| is_zero.lc(CS::one(), E::Scalar::ONE),
+        |_| limb.lc(),
+        |lc| lc,
+      )
+    }
+  }
+
+  pub fn alloc_limbs<CS: ConstraintSystem<E::Scalar>>(mut cs: CS, limbs: Vec<E::Scalar>) -> Self {
+    let element = EmulatedFieldElement::new_internal_element(EmulatedLimbs::Constant(limbs), 0)
+      .allocate_field_element_unchecked(&mut cs.namespace(|| "alloc unchecked"))
+      .unwrap();
+    Self(element)
+  }
+
   pub fn from_bits_le(one: Variable, bits: &[Boolean]) -> Self {
     let limb_bases =
       std::iter::successors(Some(E::Scalar::ONE), |base: &E::Scalar| Some(base.double()))
@@ -109,12 +134,9 @@ impl<E: CurveCycleEquipped> AllocatedBase<E> {
     Self::from_bits_le(CS::one(), &base_bits)
   }
 
-  pub fn alloc_unchecked<CS: ConstraintSystem<E::Scalar>>(mut cs: CS, base: E::Base) -> Self {
-    let base = field_to_big_int(base);
-    let base = EmulatedFieldElement::from(&base)
-      .allocate_field_element_unchecked(&mut cs.namespace(|| "alloc unchecked"))
-      .unwrap();
-    Self(base)
+  pub fn alloc_unchecked<CS: ConstraintSystem<E::Scalar>>(cs: CS, base: E::Base) -> Self {
+    let limbs = BaseParams::<E>::base_to_limbs(&base);
+    Self::alloc_limbs(cs, limbs)
   }
 
   pub fn as_preimage(&self) -> impl IntoIterator<Item = Elt<E::Scalar>> {
@@ -126,9 +148,12 @@ impl<E: CurveCycleEquipped> AllocatedBase<E> {
       )
       .unwrap();
     let EmulatedLimbs::Allocated(limbs) = limbs else {
-      unreachable!()
+      panic!()
     };
-    limbs.into_iter().map(Elt::Num)
+    limbs
+      .into_iter()
+      .map(Elt::Num)
+      .pad_using(BaseParams::<E>::num_limbs(), |_| Elt::Num(Num::zero()))
   }
 
   pub fn add<CS: ConstraintSystem<E::Scalar>>(
@@ -167,7 +192,7 @@ impl<E: CurveCycleEquipped> AllocatedBase<E> {
     )?))
   }
 
-  fn to_big_int(self) -> BigInt {
+  pub fn to_big_int(&self) -> BigInt {
     (&self.0).into()
   }
 
@@ -188,9 +213,15 @@ impl<E: CurveCycleEquipped> AllocatedBase<E> {
       0,
     ))
   }
+
+  pub fn eq_native(&self, other: &E::Base) -> bool {
+    let lhs = self.to_big_int();
+    let rhs = field_to_big_int(other);
+    lhs == rhs
+  }
 }
 
-fn field_to_big_int<F: PrimeField>(f: F) -> BigInt {
+pub fn field_to_big_int<F: PrimeField>(f: &F) -> BigInt {
   let repr = f.to_repr();
   BigInt::from_bytes_le(Sign::Plus, repr.as_ref())
 }
@@ -215,9 +246,10 @@ mod tests {
 
   type Scalar = <E as Engine>::Scalar;
   type Base = <E as Engine>::Base;
+  type P = BaseParams<E>;
   type CS = TestConstraintSystem<Scalar>;
 
-  fn check_eq<F: PrimeField>(expected: F, actual: AllocatedBase<E>) {
+  fn check_eq<F: PrimeField>(expected: &F, actual: AllocatedBase<E>) {
     let value = actual.to_big_int();
     let expected = field_to_big_int(expected);
     assert_eq!(value, expected);
@@ -227,8 +259,8 @@ mod tests {
   fn test_alloc() {
     let cases = [Base::ZERO, Base::ONE, Base::ZERO - Base::ONE];
     let mut cs = CS::new();
-    for (i, base) in cases.into_iter().enumerate() {
-      let base_allocated = AllocatedBase::<E>::alloc(cs.namespace(|| format!("alloc {i}")), base);
+    for (i, base) in cases.iter().enumerate() {
+      let base_allocated = AllocatedBase::<E>::alloc(cs.namespace(|| format!("alloc {i}")), *base);
       check_eq(base, base_allocated);
     }
 
@@ -242,9 +274,9 @@ mod tests {
   fn test_from_bits() {
     let cases = [Scalar::ZERO, Scalar::ONE, Scalar::ZERO - Scalar::ONE];
     let mut cs = CS::new();
-    for (i, scalar) in cases.into_iter().enumerate() {
+    for (i, scalar) in cases.iter().enumerate() {
       let scalar_allocated =
-        AllocatedNum::alloc_infallible(cs.namespace(|| format!("alloc scalar {i}")), || scalar);
+        AllocatedNum::alloc_infallible(cs.namespace(|| format!("alloc scalar {i}")), || *scalar);
       let scalar_bits = scalar_allocated
         .to_bits_le_strict(cs.namespace(|| format!("to_bits {i}")))
         .unwrap();
@@ -348,7 +380,7 @@ mod tests {
     let result = a + r * b;
 
     // Add a multiple of the modulus while staying in the limb bounds
-    let b_bi = field_to_big_int(b) + BaseParams::<E>::modulus() * BigInt::from(4);
+    let b_bi = field_to_big_int(&b) + P::modulus() * BigInt::from(4);
 
     let mut cs = CS::new();
 
@@ -369,11 +401,31 @@ mod tests {
   fn test_alloc_big_int() {
     // let mut rng = ChaCha20Rng::from_seed([0u8; 32]);
 
-    let a = BaseParams::<E>::modulus().sub(BigInt::one());
+    let a = P::modulus().sub(BigInt::one());
 
     let mut cs = CS::new();
 
     let a_alloc = AllocatedBase::<E>::alloc_big_int(cs.namespace(|| "a"), a.clone());
     assert_eq!(a, a_alloc.to_big_int());
   }
+
+  #[test]
+  fn test_conversions() {
+    let mut rng = ChaCha20Rng::from_seed([0u8; 32]);
+
+    let mut cs = CS::new();
+
+    let base = Base::random(&mut rng);
+    let base_big_int = field_to_big_int(&base);
+    let base_limbs = P::base_to_limbs(&base);
+
+    let alloc_base_big_int =
+      AllocatedBase::<E>::alloc_big_int(cs.namespace(|| "big int"), base_big_int.clone());
+    let alloc_base_limbs = AllocatedBase::<E>::alloc_limbs(cs.namespace(|| "limbs"), base_limbs);
+
+    assert_eq!(alloc_base_big_int.to_big_int(), base_big_int);
+    assert_eq!(alloc_base_limbs.to_big_int(), base_big_int);
+
+    assert!(cs.is_satisfied());
+  }
 }

src/parafold/cycle_fold/gadgets/secondary_commitment.rs

@@ -1,11 +1,12 @@
-use bellpepper_core::boolean::Boolean;
 use bellpepper_core::{ConstraintSystem, SynthesisError};
+use bellpepper_core::boolean::Boolean;
+use bitvec::macros::internal::funty::Fundamental;
 use neptune::circuit2::Elt;
 
+use crate::Commitment;
 use crate::parafold::cycle_fold::gadgets::ecc::AllocatedPoint;
-use crate::traits::commitment::CommitmentTrait;
 use crate::traits::{CurveCycleEquipped, Engine};
-use crate::Commitment;
+use crate::traits::commitment::CommitmentTrait;
 
 #[derive(Debug, Clone)]
 pub struct AllocatedSecondaryCommitment<E: CurveCycleEquipped> {
@@ -77,4 +78,14 @@ impl<E: CurveCycleEquipped> AllocatedSecondaryCommitment<E> {
       .commitment
       .enforce_trivial(cs.namespace(|| "enforce trivial"), is_trivial)
   }
+
+  pub fn eq_native(&self, other: &Commitment<E::Secondary>) -> Option<bool> {
+    let (x, y, is_infinity) = other.to_coordinates();
+    let x_eq = self.commitment.x.get_value()? == x;
+    let y_eq = self.commitment.y.get_value()? == y;
+    let is_infinity_eq =
+      self.commitment.is_infinity.get_value()? == E::Scalar::from(is_infinity.as_u64());
+
+    Some(x_eq && y_eq && is_infinity_eq)
+  }
 }

src/parafold/cycle_fold/mod.rs

@@ -2,10 +2,11 @@ use bellpepper_core::ConstraintSystem;
 use digest::consts::U2;
 use ff::Field;
 use neptune::circuit2::Elt;
+use neptune::hash_type::HashType;
 use neptune::poseidon::PoseidonConstants;
-use neptune::Poseidon;
+use neptune::{Poseidon, Strength};
 
-use crate::parafold::cycle_fold::gadgets::emulated::AllocatedBase;
+use crate::parafold::cycle_fold::gadgets::emulated::{field_to_big_int, AllocatedBase};
 use crate::traits::commitment::CommitmentTrait;
 use crate::traits::CurveCycleEquipped;
 use crate::Commitment;
@@ -17,7 +18,10 @@ pub mod prover;
 
 pub fn hash_commitment<E: CurveCycleEquipped>(commitment: &Commitment<E>) -> E::Base {
   // TODO: Find a way to cache this
-  let constants = PoseidonConstants::<E::Base, U2>::new();
+  let constants = PoseidonConstants::<E::Base, U2>::new_with_strength_and_type(
+    Strength::Standard,
+    HashType::ConstantLength(2),
+  );
 
   let (x, y, infinity) = commitment.to_coordinates();
   if infinity {
@@ -82,4 +86,10 @@ impl<E: CurveCycleEquipped> AllocatedPrimaryCommitment<E> {
   pub fn as_preimage(&self) -> impl IntoIterator<Item = Elt<E::Scalar>> {
     self.hash.as_preimage()
   }
+
+  pub fn eq_native(&self, other: &Commitment<E>) -> bool {
+    let self_hash = self.hash.to_big_int();
+    let other_hash = field_to_big_int(&hash_commitment::<E>(other));
+    self_hash == other_hash
+  }
 }