Add the missing check of in-circuit state against initial state for i=0

Author: winderica

crates/ivc/src/compilers/cyclefold/circuits.rs

@@ -2,9 +2,7 @@
 
 use ark_ff::PrimeField;
 use ark_r1cs_std::{
-    GR1CSVar,
-    alloc::AllocVar,
-    fields::{FieldVar, fp::FpVar},
+    GR1CSVar, alloc::AllocVar, eq::EqGadget, fields::{FieldVar, fp::FpVar}
 };
 use ark_relations::gr1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
 use sonobe_fs::{
@@ -99,6 +97,9 @@ where
         let cf_U = AllocVar::new_witness(cs.clone(), || Ok(cf_U))?;
         let cf_proofs = Vec::new_witness(cs.clone(), || Ok(cf_proofs))?;
 
+        // 0. Check initial state consistency
+        initial_state.conditional_enforce_equal(&current_state, &is_basecase)?;
+
         // 1. Fold primary instances.
         // 1.a. Derive the public input to the primary (augmented) circuit in
         //      the `i-1`-th step, which is `u.x = H(i, z_0, z_i, U, cf_U)`.

crates/primitives/src/circuits/mod.rs

@@ -1,7 +1,7 @@
 //! This module defines circuits and helpers used by Sonobe.
 
 use ark_ff::{Field, PrimeField};
-use ark_r1cs_std::{GR1CSVar, alloc::AllocVar, fields::fp::FpVar};
+use ark_r1cs_std::{GR1CSVar, alloc::AllocVar, eq::EqGadget, fields::fp::FpVar};
 use ark_relations::gr1cs::{
     ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError, SynthesisMode,
 };
@@ -74,7 +74,8 @@ pub trait FCircuit {
     /// implement the required traits for the corresponding variable type.
     type StateVar: GR1CSVar<Self::Field, Value = Self::State>
         + AllocVar<Self::State, Self::Field>
-        + AbsorbableVar<Self::Field>;
+        + AbsorbableVar<Self::Field>
+        + EqGadget<Self::Field>;
     /// [`FCircuit::ExternalInputs`] is the type of external inputs provided to
     /// each step of the circuit.
     type ExternalInputs;