diff --git a/src/ivc/cyclefold/sfc/input/assigned.rs b/src/ivc/cyclefold/sfc/input/assigned.rs
index 76ba3556..d679e6c4 100644
--- a/src/ivc/cyclefold/sfc/input/assigned.rs
+++ b/src/ivc/cyclefold/sfc/input/assigned.rs
@@ -13,8 +13,8 @@ type BigUint<F> = Vec<AssignedValue<F>>;
 
 #[derive(Clone)]
 pub struct BigUintPoint<F: PrimeField> {
-    x_limbs: BigUint<F>,
-    y_limbs: BigUint<F>,
+    pub x_limbs: BigUint<F>,
+    pub y_limbs: BigUint<F>,
 }
 
 impl<F: PrimeField> BigUintPoint<F> {
@@ -141,9 +141,10 @@ impl<F: PrimeField> ProtoGalaxyAccumulatorInstance<F> {
     }
 }
 
+#[derive(Debug, Clone)]
 pub struct ProtogalaxyProof<F: PrimeField> {
-    poly_F: Vec<AssignedValue<F>>,
-    poly_K: Vec<AssignedValue<F>>,
+    pub poly_F: Vec<AssignedValue<F>>,
+    pub poly_K: Vec<AssignedValue<F>>,
 }
 
 impl<F: PrimeField> ProtogalaxyProof<F> {
diff --git a/src/ivc/cyclefold/sfc/mod.rs b/src/ivc/cyclefold/sfc/mod.rs
index 14fb3058..4fa7af61 100644
--- a/src/ivc/cyclefold/sfc/mod.rs
+++ b/src/ivc/cyclefold/sfc/mod.rs
@@ -1,20 +1,29 @@
 use std::num::NonZeroUsize;
 
+use itertools::Itertools;
+use tracing::error;
+
 use crate::{
     halo2_proofs::{
         circuit::{Layouter, SimpleFloorPlanner},
         halo2curves::CurveAffine,
         plonk::{Circuit, ConstraintSystem, Error as Halo2PlonkError},
     },
-    ivc::{cyclefold, StepCircuit},
+    ivc::{
+        cyclefold::{self, ro_chip},
+        protogalaxy::{self, verify_chip},
+        StepCircuit,
+    },
     main_gate::{MainGate, MainGateConfig, RegionCtx},
+    polynomial::univariate::UnivariatePoly,
     poseidon::ROTrait,
 };
 
 mod input;
-use halo2_proofs::halo2curves::ff::{FromUniformBytes, PrimeField, PrimeFieldBits};
 pub use input::Input;
 
+use crate::halo2_proofs::halo2curves::ff::{FromUniformBytes, PrimeField, PrimeFieldBits};
+
 const T_MAIN_GATE: usize = 5;
 
 /// 'SCC' here is 'Step Circuit Config'
@@ -63,6 +72,8 @@ where
 
 impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> Circuit<C::ScalarExt>
     for StepFoldingCircuit<'_, ARITY, C, SC>
+where
+    C::ScalarExt: PrimeFieldBits + FromUniformBytes<64>,
 {
     type Config = Config<SC::Config>;
     type FloorPlanner = SimpleFloorPlanner;
@@ -86,16 +97,64 @@ impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> C
         config: Self::Config,
         mut layouter: impl Layouter<C::ScalarExt>,
     ) -> Result<(), Halo2PlonkError> {
-        layouter.assign_region(
-            || "sfc main",
+        let input = layouter.assign_region(
+            || "sfc input",
             |region| {
                 let mut region = RegionCtx::new(region, 0);
 
-                let _input = input::assigned::Input::assign_advice_from(
+                input::assigned::Input::assign_advice_from(&mut region, &self.input, &config.mg)
+            },
+        )?;
+
+        let z_out = self
+            .sc
+            .synthesize_step(config.sc, &mut layouter, &input.z_i)
+            .map_err(|err| {
+                error!("while synthesize_step: {err:?}");
+                Halo2PlonkError::Synthesis
+            })?;
+
+        let _self_acc_out = layouter.assign_region(
+            || "sfc protogalaxy",
+            |region| {
+                let mut region = RegionCtx::new(region, 0);
+
+                protogalaxy::verify_chip::verify(
                     &mut region,
-                    &self.input,
-                    &config.mg,
-                )?;
+                    config.mg.clone(),
+                    ro_chip(config.mg.clone()),
+                    verify_chip::AssignedVerifierParam {
+                        pp_digest: input.pp_digest.clone(),
+                    },
+                    input.self_trace.input_accumulator.clone().into(),
+                    &[input.self_trace.incoming.clone().into()],
+                    input.self_trace.proof.clone().into(),
+                )
+                .map_err(|err| {
+                    error!("while protogalaxy::verify: {err:?}");
+                    Halo2PlonkError::Synthesis
+                })
+            },
+        )?;
+
+        layouter.assign_region(
+            || "sfc out",
+            |region| {
+                let mut region = RegionCtx::new(region, 0);
+
+                let mg = MainGate::new(config.mg.clone());
+                let is_zero_step = mg.is_zero_term(&mut region, input.step.clone())?;
+
+                let _z_out: [_; ARITY] = input
+                    .z_0
+                    .iter()
+                    .zip_eq(z_out.iter())
+                    .map(|(z_0_i, z_out_i)| {
+                        mg.conditional_select(&mut region, z_0_i, z_out_i, &is_zero_step)
+                    })
+                    .collect::<Result<Vec<_>, _>>()?
+                    .try_into()
+                    .unwrap();
 
                 Ok(())
             },
@@ -104,3 +163,67 @@ impl<const ARITY: usize, C: CurveAffine, SC: StepCircuit<ARITY, C::ScalarExt>> C
         todo!()
     }
 }
+
+impl<F: PrimeField> From<input::assigned::ProtoGalaxyAccumulatorInstance<F>>
+    for verify_chip::AssignedAccumulatorInstance<F>
+{
+    fn from(value: input::assigned::ProtoGalaxyAccumulatorInstance<F>) -> Self {
+        use self::input::assigned::{NativePlonkInstance, ProtoGalaxyAccumulatorInstance};
+
+        let ProtoGalaxyAccumulatorInstance {
+            ins:
+                NativePlonkInstance {
+                    W_commitments,
+                    instances,
+                    challenges,
+                },
+            betas,
+            e,
+        } = value;
+
+        Self {
+            betas,
+            e,
+            ins: verify_chip::AssignedPlonkInstance {
+                instances,
+                challenges,
+                W_commitments: W_commitments
+                    .into_iter()
+                    .map(|W_commitment| (W_commitment.x_limbs, W_commitment.y_limbs))
+                    .collect(),
+            },
+        }
+    }
+}
+
+impl<F: PrimeField> From<input::assigned::ProtogalaxyProof<F>> for verify_chip::AssignedProof<F> {
+    fn from(value: input::assigned::ProtogalaxyProof<F>) -> Self {
+        let input::assigned::ProtogalaxyProof { poly_F, poly_K } = value;
+
+        verify_chip::AssignedProof {
+            poly_F: verify_chip::AssignedUnivariatePoly(UnivariatePoly(poly_F.into_boxed_slice())),
+            poly_K: verify_chip::AssignedUnivariatePoly(UnivariatePoly(poly_K.into_boxed_slice())),
+        }
+    }
+}
+
+impl<F: PrimeField> From<input::assigned::NativePlonkInstance<F>>
+    for verify_chip::AssignedPlonkInstance<F>
+{
+    fn from(value: input::assigned::NativePlonkInstance<F>) -> Self {
+        let input::assigned::NativePlonkInstance {
+            W_commitments,
+            instances,
+            challenges,
+        } = value;
+
+        Self {
+            instances,
+            challenges,
+            W_commitments: W_commitments
+                .into_iter()
+                .map(|W_commitment| (W_commitment.x_limbs, W_commitment.y_limbs))
+                .collect(),
+        }
+    }
+}
diff --git a/src/ivc/protogalaxy/mod.rs b/src/ivc/protogalaxy/mod.rs
index 6efb54cb..913ae5d5 100644
--- a/src/ivc/protogalaxy/mod.rs
+++ b/src/ivc/protogalaxy/mod.rs
@@ -7,7 +7,6 @@ pub mod verify_chip {
     use crate::{
         gadgets::nonnative::bn::big_uint,
         halo2_proofs::{
-            arithmetic::Field,
             circuit::{AssignedCell, Chip, Value as Halo2Value},
             halo2curves::{
                 ff::{FromUniformBytes, PrimeField, PrimeFieldBits},
@@ -63,9 +62,9 @@ pub mod verify_chip {
 
     /// Assigned version of [`crate::plonk::PlonkInstance`]
     pub struct AssignedPlonkInstance<F: PrimeField> {
-        W_commitments: Vec<BigUintPoint<AssignedValue<F>>>,
-        instances: Vec<Vec<AssignedValue<F>>>,
-        challenges: Vec<AssignedValue<F>>,
+        pub W_commitments: Vec<BigUintPoint<AssignedValue<F>>>,
+        pub instances: Vec<Vec<AssignedValue<F>>>,
+        pub challenges: Vec<AssignedValue<F>>,
     }
 
     fn to_bn<C: CurveAffine>(v: &C) -> Result<BigUintPoint<C::ScalarExt>, big_uint::Error> {
@@ -168,9 +167,9 @@ pub mod verify_chip {
 
     /// Assigned version of [`crate::nifs::protogalaxy::accumulator::AccumulatorInstance`]
     pub struct AssignedAccumulatorInstance<F: PrimeField> {
-        ins: AssignedPlonkInstance<F>,
-        betas: Box<[AssignedValue<F>]>,
-        e: AssignedValue<F>,
+        pub ins: AssignedPlonkInstance<F>,
+        pub betas: Box<[AssignedValue<F>]>,
+        pub e: AssignedValue<F>,
     }
 
     impl<F: PrimeField> AssignedAccumulatorInstance<F> {
@@ -276,7 +275,7 @@ pub mod verify_chip {
     }
 
     /// Assigned version of [`crate::polynomial::univariate::UnivariatePoly`]
-    pub struct AssignedUnivariatePoly<F: PrimeField>(UnivariatePoly<AssignedValue<F>>);
+    pub struct AssignedUnivariatePoly<F: PrimeField>(pub UnivariatePoly<AssignedValue<F>>);
 
     impl<F: PrimeField> AssignedUnivariatePoly<F> {
         pub fn assign<const T: usize>(
@@ -407,8 +406,8 @@ pub mod verify_chip {
 
     /// Assigned version of [`crate::nifs::protogalaxy::Proof]
     pub struct AssignedProof<F: PrimeField> {
-        poly_F: AssignedUnivariatePoly<F>,
-        poly_K: AssignedUnivariatePoly<F>,
+        pub poly_F: AssignedUnivariatePoly<F>,
+        pub poly_K: AssignedUnivariatePoly<F>,
     }
 
     impl<F: PrimeField> AssignedProof<F> {
@@ -556,11 +555,11 @@ pub mod verify_chip {
         .collect::<Result<Box<[_]>, Halo2PlonkError>>()
     }
 
-    fn calculate_betas_stroke<C: CurveAffine, const T: usize>(
-        region: &mut RegionCtx<C::ScalarExt>,
-        main_gate: &MainGate<C::ScalarExt, T>,
-        cha: PolyChallenges<AssignedCell<C::ScalarExt, C::ScalarExt>>,
-    ) -> Result<Box<[AssignedCell<C::ScalarExt, C::ScalarExt>]>, Error> {
+    fn calculate_betas_stroke<F: PrimeField, const T: usize>(
+        region: &mut RegionCtx<F>,
+        main_gate: &MainGate<F, T>,
+        cha: PolyChallenges<AssignedValue<F>>,
+    ) -> Result<Box<[AssignedValue<F>]>, Error> {
         let deltas =
             calculate_exponentiation_sequence(region, main_gate, cha.delta, cha.betas.len())
                 .map_err(|err| Error::Deltas { err })?;
@@ -795,18 +794,17 @@ pub mod verify_chip {
     ///
     /// 5. **Fold the Instance:**
     ///     - [`ProtoGalaxy::fold_instance`]
-    pub fn verify<C: CurveAffine, const L: usize, const T: usize>(
-        region: &mut RegionCtx<C::ScalarExt>,
+    pub fn verify<F, const L: usize, const T: usize>(
+        region: &mut RegionCtx<F>,
         main_gate_config: MainGateConfig<T>,
-        ro_circuit: impl ROCircuitTrait<C::ScalarExt>,
-        vp: AssignedVerifierParam<C::ScalarExt>,
-        accumulator: AssignedAccumulatorInstance<C::ScalarExt>,
-        incoming: &[AssignedPlonkInstance<C::ScalarExt>; L],
-        proof: AssignedProof<C::ScalarExt>,
-    ) -> Result<AssignedAccumulatorInstance<C::ScalarExt>, Error>
+        ro_circuit: impl ROCircuitTrait<F>,
+        vp: AssignedVerifierParam<F>,
+        accumulator: AssignedAccumulatorInstance<F>,
+        incoming: &[AssignedPlonkInstance<F>; L],
+        proof: AssignedProof<F>,
+    ) -> Result<AssignedAccumulatorInstance<F>, Error>
     where
-        C::ScalarExt: FromUniformBytes<64> + PrimeFieldBits,
-        C::ScalarExt: FromUniformBytes<64> + PrimeFieldBits,
+        F: FromUniformBytes<64> + PrimeFieldBits,
     {
         let AssignedChallanges {
             delta,
@@ -817,7 +815,7 @@ pub mod verify_chip {
 
         let main_gate = MainGate::new(main_gate_config);
 
-        let betas = calculate_betas_stroke::<C, T>(
+        let betas = calculate_betas_stroke::<F, T>(
             region,
             &main_gate,
             PolyChallenges {
@@ -831,7 +829,7 @@ pub mod verify_chip {
             .assign_advice(
                 || "one",
                 main_gate.config().state[0],
-                Halo2Value::known(C::ScalarExt::ONE),
+                Halo2Value::known(F::ONE),
             )
             .map_err(|err| Error::Assign {
                 annotation: "one",
@@ -842,7 +840,7 @@ pub mod verify_chip {
         let mut gamma_powers = ValuePowers::new(one.clone(), gamma);
         let mut alpha_powers = ValuePowers::new(one, alpha);
 
-        let e = calculate_e::<C::ScalarExt, T, L>(
+        let e = calculate_e::<F, T, L>(
             region,
             &main_gate,
             &proof,
@@ -1069,7 +1067,7 @@ pub mod verify_chip {
                         let main_gate = MainGate::<Scalar, T>::new(main_gate_config.clone());
 
                         Ok(
-                            calculate_betas_stroke::<Affine1, T>(&mut region, &main_gate, cha)
+                            calculate_betas_stroke::<Scalar, T>(&mut region, &main_gate, cha)
                                 .unwrap(),
                         )
                     },