diff --git a/core/src/cpu/air/mod.rs b/core/src/cpu/air/mod.rs
index fc3c96b8a3..7ffdab1df0 100644
--- a/core/src/cpu/air/mod.rs
+++ b/core/src/cpu/air/mod.rs
@@ -237,6 +237,9 @@ impl CpuChip {
         // Verify that the clk increments are correct.  Most clk increment should be 4, but for some
         // precompiles, there are additional cycles.
         let num_extra_cycles = self.get_num_extra_ecall_cycles::<AB>(local);
+
+        // We already assert that `local.clk < 2^24`. `num_extra_cycles` is an entry of a word and
+        // therefore less than `2^8`, this means that the sum cannot overflow in a 31 bit field.
         let expected_next_clk =
             local.clk + AB::Expr::from_canonical_u32(4) + num_extra_cycles.clone();
 
diff --git a/core/src/stark/chip.rs b/core/src/stark/chip.rs
index b792fb597c..3b82a51a8b 100644
--- a/core/src/stark/chip.rs
+++ b/core/src/stark/chip.rs
@@ -7,10 +7,10 @@ use p3_util::log2_ceil_usize;
 
 use crate::{
     air::{MachineAir, MultiTableAirBuilder, SP1AirBuilder},
-    lookup::{Interaction, InteractionBuilder},
+    lookup::{Interaction, InteractionBuilder, InteractionKind},
 };
 
-use super::{eval_permutation_constraints, generate_permutation_trace};
+use super::{eval_permutation_constraints, generate_permutation_trace, permutation_trace_width};
 
 /// An Air that encodes lookups based on interactions.
 pub struct Chip<F: Field, A> {
@@ -74,10 +74,21 @@ where
         }
     }
 
+    #[inline]
     pub fn num_interactions(&self) -> usize {
         self.sends.len() + self.receives.len()
     }
 
+    #[inline]
+    pub fn num_sends_by_kind(&self, kind: InteractionKind) -> usize {
+        self.sends.iter().filter(|i| i.kind == kind).count()
+    }
+
+    #[inline]
+    pub fn num_receives_by_kind(&self, kind: InteractionKind) -> usize {
+        self.receives.iter().filter(|i| i.kind == kind).count()
+    }
+
     pub fn generate_permutation_trace<EF: ExtensionField<F>>(
         &self,
         preprocessed: Option<&RowMajorMatrix<F>>,
@@ -98,6 +109,20 @@ where
         )
     }
 
+    #[inline]
+    pub fn permutation_width(&self) -> usize {
+        permutation_trace_width(
+            self.sends().len() + self.receives().len(),
+            self.logup_batch_size(),
+        )
+    }
+
+    #[inline]
+    pub fn quotient_width(&self) -> usize {
+        1 << self.log_quotient_degree
+    }
+
+    #[inline]
     pub fn logup_batch_size(&self) -> usize {
         // TODO: calculate by log_quotient_degree.
         2
diff --git a/core/src/stark/machine.rs b/core/src/stark/machine.rs
index 22f93de9da..a6dfe95b4d 100644
--- a/core/src/stark/machine.rs
+++ b/core/src/stark/machine.rs
@@ -288,7 +288,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> StarkMachine<SC, A> {
         vk: &StarkVerifyingKey<SC>,
         proof: &MachineProof<SC>,
         challenger: &mut SC::Challenger,
-    ) -> Result<(PublicValuesDigest, DeferredDigest), ProgramVerificationError>
+    ) -> Result<(PublicValuesDigest, DeferredDigest), ProgramVerificationError<SC>>
     where
         SC::Challenger: Clone,
         A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
@@ -522,16 +522,48 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> StarkMachine<SC, A> {
     }
 }
 
-#[derive(Debug)]
-pub enum ProgramVerificationError {
-    InvalidSegmentProof(VerificationError),
-    InvalidGlobalProof(VerificationError),
+pub enum ProgramVerificationError<SC: StarkGenericConfig> {
+    InvalidSegmentProof(VerificationError<SC>),
+    InvalidGlobalProof(VerificationError<SC>),
     NonZeroCumulativeSum,
     InvalidShardTransition(&'static str),
     InvalidPublicValuesDigest,
     DebugInteractionsFailed,
 }
 
+impl<SC: StarkGenericConfig> Debug for ProgramVerificationError<SC> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            ProgramVerificationError::InvalidSegmentProof(e) => {
+                write!(f, "Invalid segment proof: {:?}", e)
+            }
+            ProgramVerificationError::InvalidGlobalProof(e) => {
+                write!(f, "Invalid global proof: {:?}", e)
+            }
+            ProgramVerificationError::NonZeroCumulativeSum => {
+                write!(f, "Non-zero cumulative sum")
+            }
+            ProgramVerificationError::InvalidShardTransition(s) => {
+                write!(f, "Invalid shard transition: {}", s)
+            }
+            ProgramVerificationError::InvalidPublicValuesDigest => {
+                write!(f, "Invalid public values digest")
+            }
+            ProgramVerificationError::DebugInteractionsFailed => {
+                write!(f, "Debug interactions failed")
+            }
+        }
+    }
+}
+
+impl<SC: StarkGenericConfig> std::fmt::Display for ProgramVerificationError<SC> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        Debug::fmt(self, f)
+    }
+}
+
+impl<SC: StarkGenericConfig> std::error::Error for ProgramVerificationError<SC> {}
+
 #[cfg(test)]
 #[allow(non_snake_case)]
 pub mod tests {
diff --git a/core/src/stark/permutation.rs b/core/src/stark/permutation.rs
index 85325afb1b..85cc671662 100644
--- a/core/src/stark/permutation.rs
+++ b/core/src/stark/permutation.rs
@@ -71,6 +71,10 @@ pub fn populate_permutation_row<F: PrimeField, EF: ExtensionField<F>>(
     }
 }
 
+pub const fn permutation_trace_width(num_interactions: usize, batch_size: usize) -> usize {
+    (num_interactions + 1) / batch_size + 1
+}
+
 /// Generates the permutation trace for the given chip and main trace based on a variant of LogUp.
 ///
 /// The permutation trace has (N+1)*EF::NUM_COLS columns, where N is the number of interactions in
@@ -96,7 +100,7 @@ pub(crate) fn generate_permutation_trace<F: PrimeField, EF: ExtensionField<F>>(
     //
     // where f_{i, c_k} is the value at row i for column c_k. The computed value is essentially a
     // fingerprint for the interaction.
-    let permutation_trace_width = (sends.len() + receives.len() + 1) / batch_size + 1;
+    let permutation_trace_width = permutation_trace_width(sends.len() + receives.len(), batch_size);
     let height = main.height();
 
     let mut permutation_trace = RowMajorMatrix::new(
diff --git a/core/src/stark/prover.rs b/core/src/stark/prover.rs
index fc949e8c0b..8153530c3d 100644
--- a/core/src/stark/prover.rs
+++ b/core/src/stark/prover.rs
@@ -375,7 +375,7 @@ where
                         permutation_trace_on_quotient_domains,
                         &packed_perm_challenges,
                         alpha,
-                        shard_data.public_values.clone(),
+                        &shard_data.public_values,
                     )
                 })
                 .collect::<Vec<_>>()
@@ -505,7 +505,6 @@ where
             .collect::<Vec<_>>();
 
         ShardProof::<SC> {
-            index: shard_data.index,
             commitment: ShardCommitment {
                 main_commit: shard_data.main_commit.clone(),
                 permutation_commit,
diff --git a/core/src/stark/quotient.rs b/core/src/stark/quotient.rs
index 9483627943..4934df0b66 100644
--- a/core/src/stark/quotient.rs
+++ b/core/src/stark/quotient.rs
@@ -28,7 +28,7 @@ pub fn quotient_values<SC, A, Mat>(
     permutation_trace_on_quotient_domain: Mat,
     perm_challenges: &[PackedChallenge<SC>],
     alpha: SC::Challenge,
-    public_values: Vec<Val<SC>>,
+    public_values: &[Val<SC>],
 ) -> Vec<SC::Challenge>
 where
     A: for<'a> Air<ProverConstraintFolder<'a, SC>>,
@@ -116,7 +116,6 @@ where
                 .collect();
 
             let accumulator = PackedChallenge::<SC>::zero();
-            let public_values = public_values.to_vec();
             let mut folder = ProverConstraintFolder {
                 preprocessed: VerticalPair::new(
                     RowMajorMatrixView::new_row(&prep_local),
@@ -137,7 +136,7 @@ where
                 is_transition,
                 alpha,
                 accumulator,
-                public_values: &public_values,
+                public_values,
             };
             chip.eval(&mut folder);
 
diff --git a/core/src/stark/types.rs b/core/src/stark/types.rs
index b4cb257744..3fdd5aee64 100644
--- a/core/src/stark/types.rs
+++ b/core/src/stark/types.rs
@@ -131,7 +131,6 @@ pub const PROOF_MAX_NUM_PVS: usize = SP1_PROOF_NUM_PV_ELTS;
 #[derive(Serialize, Deserialize, Clone)]
 #[serde(bound = "")]
 pub struct ShardProof<SC: StarkGenericConfig> {
-    pub index: usize,
     pub commitment: ShardCommitment<Com<SC>>,
     pub opened_values: ShardOpenedValues<Challenge<SC>>,
     pub opening_proof: OpeningProof<SC>,
diff --git a/core/src/stark/verifier.rs b/core/src/stark/verifier.rs
index 308b27040e..fbde0f4267 100644
--- a/core/src/stark/verifier.rs
+++ b/core/src/stark/verifier.rs
@@ -1,9 +1,11 @@
 use core::fmt::Display;
+use std::fmt::Debug;
 use std::fmt::Formatter;
 use std::marker::PhantomData;
 
 use itertools::Itertools;
 use p3_air::Air;
+use p3_air::BaseAir;
 use p3_challenger::CanObserve;
 use p3_challenger::FieldChallenger;
 use p3_commit::LagrangeSelectors;
@@ -15,6 +17,7 @@ use p3_field::AbstractField;
 use super::folder::VerifierConstraintFolder;
 use super::types::*;
 use super::Domain;
+use super::OpeningError;
 use super::StarkGenericConfig;
 use super::StarkVerifyingKey;
 use super::Val;
@@ -31,7 +34,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
         chips: &[&MachineChip<SC, A>],
         challenger: &mut SC::Challenger,
         proof: &ShardProof<SC>,
-    ) -> Result<(), VerificationError>
+    ) -> Result<(), VerificationError<SC>>
     where
         A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
     {
@@ -41,6 +44,8 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             commitment,
             opened_values,
             opening_proof,
+            chip_ordering,
+            public_values,
             ..
         } = proof;
 
@@ -85,8 +90,8 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             .chip_information
             .iter()
             .map(|(name, domain, _)| {
-                let i = proof.chip_ordering[name];
-                let values = proof.opened_values.chips[i].preprocessed.clone();
+                let i = chip_ordering[name];
+                let values = opened_values.chips[i].preprocessed.clone();
                 (
                     *domain,
                     vec![
@@ -99,7 +104,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
 
         let main_domains_points_and_opens = trace_domains
             .iter()
-            .zip_eq(proof.opened_values.chips.iter())
+            .zip_eq(opened_values.chips.iter())
             .map(|(domain, values)| {
                 (
                     *domain,
@@ -113,7 +118,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
 
         let perm_domains_points_and_opens = trace_domains
             .iter()
-            .zip_eq(proof.opened_values.chips.iter())
+            .zip_eq(opened_values.chips.iter())
             .map(|(domain, values)| {
                 (
                     *domain,
@@ -166,7 +171,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
                 opening_proof,
                 challenger,
             )
-            .map_err(|_| VerificationError::InvalidopeningArgument)?;
+            .map_err(|e| VerificationError::InvalidopeningArgument(e))?;
 
         // Verify the constrtaint evaluations.
 
@@ -176,41 +181,114 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             quotient_chunk_domains,
             opened_values.chips.iter(),
         ) {
+            // Verify the shape of the opening arguments matches the expected values.
+            Self::verify_opening_shape(chip, values)
+                .map_err(|e| VerificationError::OpeningShapeError(chip.name(), e))?;
+            // Verify the constraint evaluation.
             Self::verify_constraints(
                 chip,
-                values.clone(),
+                values,
                 trace_domain,
                 qc_domains,
                 zeta,
                 alpha,
                 &permutation_challenges,
-                proof.public_values.clone(),
+                public_values,
             )
             .map_err(|_| VerificationError::OodEvaluationMismatch(chip.name()))?;
         }
         Ok(())
     }
 
+    fn verify_opening_shape(
+        chip: &MachineChip<SC, A>,
+        opening: &ChipOpenedValues<SC::Challenge>,
+    ) -> Result<(), OpeningShapeError> {
+        // Verify that the preprocessed width matches the expected value for the chip.
+        if opening.preprocessed.local.len() != chip.preprocessed_width() {
+            return Err(OpeningShapeError::PreprocessedWidthMismatch(
+                chip.preprocessed_width(),
+                opening.preprocessed.local.len(),
+            ));
+        }
+        if opening.preprocessed.next.len() != chip.preprocessed_width() {
+            return Err(OpeningShapeError::PreprocessedWidthMismatch(
+                chip.preprocessed_width(),
+                opening.preprocessed.next.len(),
+            ));
+        }
+
+        // Verify that the main width matches the expected value for the chip.
+        if opening.main.local.len() != chip.width() {
+            return Err(OpeningShapeError::MainWidthMismatch(
+                chip.width(),
+                opening.main.local.len(),
+            ));
+        }
+        if opening.main.next.len() != chip.width() {
+            return Err(OpeningShapeError::MainWidthMismatch(
+                chip.width(),
+                opening.main.next.len(),
+            ));
+        }
+
+        // Verify that the permutation width matches the expected value for the chip.
+        if opening.permutation.local.len() != chip.permutation_width() * SC::Challenge::D {
+            return Err(OpeningShapeError::PermutationWidthMismatch(
+                chip.permutation_width(),
+                opening.permutation.local.len(),
+            ));
+        }
+        if opening.permutation.next.len() != chip.permutation_width() * SC::Challenge::D {
+            return Err(OpeningShapeError::PermutationWidthMismatch(
+                chip.permutation_width(),
+                opening.permutation.next.len(),
+            ));
+        }
+
+        // Verift that the number of quotient chunks matches the expected value for the chip.
+        if opening.quotient.len() != chip.quotient_width() {
+            return Err(OpeningShapeError::QuotientWidthMismatch(
+                chip.quotient_width(),
+                opening.quotient.len(),
+            ));
+        }
+        // For each quotient chunk, verify that the number of elements is equal to the degree of the
+        // challenge extension field over the value field.
+        for slice in &opening.quotient {
+            if slice.len() != SC::Challenge::D {
+                return Err(OpeningShapeError::QuotientChunkSizeMismatch(
+                    SC::Challenge::D,
+                    slice.len(),
+                ));
+            }
+        }
+
+        Ok(())
+    }
+
     #[allow(clippy::too_many_arguments)]
     fn verify_constraints(
         chip: &MachineChip<SC, A>,
-        opening: ChipOpenedValues<SC::Challenge>,
+        opening: &ChipOpenedValues<SC::Challenge>,
         trace_domain: Domain<SC>,
         qc_domains: Vec<Domain<SC>>,
         zeta: SC::Challenge,
         alpha: SC::Challenge,
         permutation_challenges: &[SC::Challenge],
-        public_values: Vec<Val<SC>>,
+        public_values: &[Val<SC>],
     ) -> Result<(), OodEvaluationMismatch>
     where
         A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
     {
         let sels = trace_domain.selectors_at_point(zeta);
 
-        let quotient = Self::recompute_quotient(&opening, &qc_domains, zeta);
+        // Recompute the quotient at zeta from the chunks.
+        let quotient = Self::recompute_quotient(opening, &qc_domains, zeta);
+        // Calculate the evaluations of the constraints at zeta.
         let folded_constraints = Self::eval_constraints(
             chip,
-            &opening,
+            opening,
             &sels,
             alpha,
             permutation_challenges,
@@ -231,7 +309,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
         selectors: &LagrangeSelectors<SC::Challenge>,
         alpha: SC::Challenge,
         permutation_challenges: &[SC::Challenge],
-        public_values: Vec<Val<SC>>,
+        public_values: &[Val<SC>],
     ) -> SC::Challenge
     where
         A: for<'a> Air<VerifierConstraintFolder<'a, SC>>,
@@ -254,7 +332,6 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             next: unflatten(&opening.permutation.next),
         };
 
-        let public_values = public_values.to_vec();
         let mut folder = VerifierConstraintFolder::<SC> {
             preprocessed: opening.preprocessed.view(),
             main: opening.main.view(),
@@ -266,7 +343,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
             is_transition: selectors.is_transition,
             alpha,
             accumulator: SC::Challenge::zero(),
-            public_values: &public_values,
+            public_values,
             _marker: PhantomData,
         };
 
@@ -315,25 +392,104 @@ impl<SC: StarkGenericConfig, A: MachineAir<Val<SC>>> Verifier<SC, A> {
 
 pub struct OodEvaluationMismatch;
 
-#[derive(Debug)]
-pub enum VerificationError {
+pub enum OpeningShapeError {
+    PreprocessedWidthMismatch(usize, usize),
+    MainWidthMismatch(usize, usize),
+    PermutationWidthMismatch(usize, usize),
+    QuotientWidthMismatch(usize, usize),
+    QuotientChunkSizeMismatch(usize, usize),
+}
+
+pub enum VerificationError<SC: StarkGenericConfig> {
     /// opening proof is invalid.
-    InvalidopeningArgument,
+    InvalidopeningArgument(OpeningError<SC>),
     /// Out-of-domain evaluation mismatch.
     ///
     /// `constraints(zeta)` did not match `quotient(zeta) Z_H(zeta)`.
     OodEvaluationMismatch(String),
+    /// The shape of the opening arguments is invalid.
+    OpeningShapeError(String, OpeningShapeError),
+}
+
+impl Debug for OpeningShapeError {
+    fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
+        match self {
+            OpeningShapeError::PreprocessedWidthMismatch(expected, actual) => {
+                write!(
+                    f,
+                    "Preprocessed width mismatch: expected {}, got {}",
+                    expected, actual
+                )
+            }
+            OpeningShapeError::MainWidthMismatch(expected, actual) => {
+                write!(
+                    f,
+                    "Main width mismatch: expected {}, got {}",
+                    expected, actual
+                )
+            }
+            OpeningShapeError::PermutationWidthMismatch(expected, actual) => {
+                write!(
+                    f,
+                    "Permutation width mismatch: expected {}, got {}",
+                    expected, actual
+                )
+            }
+            OpeningShapeError::QuotientWidthMismatch(expected, actual) => {
+                write!(
+                    f,
+                    "Quotient width mismatch: expected {}, got {}",
+                    expected, actual
+                )
+            }
+            OpeningShapeError::QuotientChunkSizeMismatch(expected, actual) => {
+                write!(
+                    f,
+                    "Quotient chunk size mismatch: expected {}, got {}",
+                    expected, actual
+                )
+            }
+        }
+    }
+}
+
+impl Display for OpeningShapeError {
+    fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
+        // use the debug implementation
+        write!(f, "{:?}", self)
+    }
+}
+
+impl<SC: StarkGenericConfig> Debug for VerificationError<SC> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
+        match self {
+            VerificationError::InvalidopeningArgument(e) => {
+                write!(f, "Invalid opening argument: {:?}", e)
+            }
+            VerificationError::OodEvaluationMismatch(chip) => {
+                write!(f, "Out-of-domain evaluation mismatch on chip {}", chip)
+            }
+            VerificationError::OpeningShapeError(chip, e) => {
+                write!(f, "Invalid opening shape for chip {}: {:?}", chip, e)
+            }
+        }
+    }
 }
 
-impl Display for VerificationError {
+impl<SC: StarkGenericConfig> Display for VerificationError<SC> {
     fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
         match self {
-            VerificationError::InvalidopeningArgument => {
+            VerificationError::InvalidopeningArgument(_) => {
                 write!(f, "Invalid opening argument")
             }
             VerificationError::OodEvaluationMismatch(chip) => {
                 write!(f, "Out-of-domain evaluation mismatch on chip {}", chip)
             }
+            VerificationError::OpeningShapeError(chip, e) => {
+                write!(f, "Invalid opening shape for chip {}: {}", chip, e)
+            }
         }
     }
 }
+
+impl<SC: StarkGenericConfig> std::error::Error for VerificationError<SC> {}
diff --git a/core/src/utils/prove.rs b/core/src/utils/prove.rs
index 0a0f5f21b1..8cf625cb9e 100644
--- a/core/src/utils/prove.rs
+++ b/core/src/utils/prove.rs
@@ -32,7 +32,7 @@ pub fn get_cycles(program: Program) -> u64 {
 pub fn run_test_io(
     program: Program,
     inputs: SP1Stdin,
-) -> Result<SP1PublicValues, crate::stark::ProgramVerificationError> {
+) -> Result<SP1PublicValues, crate::stark::ProgramVerificationError<BabyBearBlake3>> {
     let runtime = tracing::info_span!("runtime.run(...)").in_scope(|| {
         let mut runtime = Runtime::new(program);
         runtime.write_vecs(&inputs.buffer);
@@ -46,7 +46,10 @@ pub fn run_test_io(
 
 pub fn run_test(
     program: Program,
-) -> Result<crate::stark::MachineProof<BabyBearBlake3>, crate::stark::ProgramVerificationError> {
+) -> Result<
+    crate::stark::MachineProof<BabyBearBlake3>,
+    crate::stark::ProgramVerificationError<BabyBearBlake3>,
+> {
     let runtime = tracing::info_span!("runtime.run(...)").in_scope(|| {
         let mut runtime = Runtime::new(program);
         runtime.run();
@@ -58,7 +61,10 @@ pub fn run_test(
 #[allow(unused_variables)]
 pub fn run_test_core(
     runtime: Runtime,
-) -> Result<crate::stark::MachineProof<BabyBearBlake3>, crate::stark::ProgramVerificationError> {
+) -> Result<
+    crate::stark::MachineProof<BabyBearBlake3>,
+    crate::stark::ProgramVerificationError<BabyBearBlake3>,
+> {
     let config = BabyBearBlake3::new();
     let machine = RiscvAir::machine(config);
     let (pk, vk) = machine.setup(runtime.program.as_ref());
diff --git a/prover/src/verify.rs b/prover/src/verify.rs
index 061742d5a3..5e8098d284 100644
--- a/prover/src/verify.rs
+++ b/prover/src/verify.rs
@@ -3,7 +3,7 @@ use sp1_core::stark::{MachineProof, ProgramVerificationError, RiscvAir, StarkGen
 use crate::{CoreSC, SP1CoreProof, SP1ReduceProof, SP1VerifyingKey};
 
 impl SP1CoreProof {
-    pub fn verify(&self, vk: &SP1VerifyingKey) -> Result<(), ProgramVerificationError> {
+    pub fn verify(&self, vk: &SP1VerifyingKey) -> Result<(), ProgramVerificationError<CoreSC>> {
         let core_machine = RiscvAir::machine(CoreSC::default());
         let mut challenger = core_machine.config().challenger();
         let machine_proof = MachineProof {
@@ -15,7 +15,7 @@ impl SP1CoreProof {
 }
 
 impl SP1ReduceProof<CoreSC> {
-    pub fn verify(&self, _vk: &SP1VerifyingKey) -> Result<(), ProgramVerificationError> {
+    pub fn verify(&self, _vk: &SP1VerifyingKey) -> Result<(), ProgramVerificationError<CoreSC>> {
         todo!()
     }
 }
diff --git a/recursion/circuit/src/types.rs b/recursion/circuit/src/types.rs
index c828992161..4e6ff000cc 100644
--- a/recursion/circuit/src/types.rs
+++ b/recursion/circuit/src/types.rs
@@ -12,7 +12,6 @@ use crate::DIGEST_SIZE;
 pub type OuterDigestVariable<C: Config> = [Var<C::N>; DIGEST_SIZE];
 
 pub struct RecursionShardProofVariable<C: Config> {
-    pub index: usize,
     pub commitment: ShardCommitment<OuterDigestVariable<C>>,
     pub opened_values: RecursionShardOpenedValuesVariable<C>,
     pub opening_proof: TwoAdicPcsProofVariable<C>,
diff --git a/recursion/circuit/src/witness.rs b/recursion/circuit/src/witness.rs
index 57e30e8ad3..bd5bda0837 100644
--- a/recursion/circuit/src/witness.rs
+++ b/recursion/circuit/src/witness.rs
@@ -305,7 +305,6 @@ impl Witnessable<C> for ShardProof<BabyBearPoseidon2Outer> {
         let public_values = builder.vec(public_values);
 
         RecursionShardProofVariable {
-            index: self.index,
             commitment,
             opened_values,
             opening_proof,
diff --git a/recursion/program/src/hints.rs b/recursion/program/src/hints.rs
index 464a4d85d5..b01eb42281 100644
--- a/recursion/program/src/hints.rs
+++ b/recursion/program/src/hints.rs
@@ -415,13 +415,11 @@ where
     type HintVariable = ShardProofVariable<C>;
 
     fn read(builder: &mut Builder<C>) -> Self::HintVariable {
-        let index = builder.hint_var();
         let commitment = ShardCommitment::read(builder);
         let opened_values = ShardOpenedValues::read(builder);
         let opening_proof = InnerPcsProof::read(builder);
         let public_values = Vec::<InnerVal>::read(builder);
         ShardProofVariable {
-            index,
             commitment,
             opened_values,
             opening_proof,
@@ -431,7 +429,6 @@ where
 
     fn write(&self) -> Vec<Vec<Block<<C as Config>::F>>> {
         let mut stream = Vec::new();
-        stream.extend(self.index.write());
         stream.extend(self.commitment.write());
         stream.extend(self.opened_values.write());
         stream.extend(self.opening_proof.write());
diff --git a/recursion/program/src/types.rs b/recursion/program/src/types.rs
index e994d445e3..ef143eec1f 100644
--- a/recursion/program/src/types.rs
+++ b/recursion/program/src/types.rs
@@ -13,7 +13,6 @@ use crate::fri::TwoAdicMultiplicativeCosetVariable;
 /// Reference: [sp1_core::stark::ShardProof]
 #[derive(DslVariable, Clone)]
 pub struct ShardProofVariable<C: Config> {
-    pub index: Var<C::N>,
     pub commitment: ShardCommitmentVariable<C>,
     pub opened_values: ShardOpenedValuesVariable<C>,
     pub opening_proof: TwoAdicPcsProofVariable<C>,
@@ -71,6 +70,13 @@ pub struct AirOpenedValuesVariable<C: Config> {
 }
 
 impl<C: Config> ChipOpening<C> {
+    /// Collect opening values from a dynamic array into vectors.
+    ///
+    /// This method is used to convert a `ChipOpenedValuesVariable` into a `ChipOpenedValues`, which
+    /// are the same values but with each opening converted from a dynamic array into a Rust vector.
+    ///
+    /// *Safety*: This method also verifies that the legnth of the dynamic arrays match the expected
+    /// length of the vectors.
     pub fn from_variable<A>(
         builder: &mut Builder<C>,
         chip: &Chip<C::F, A>,
@@ -83,8 +89,11 @@ impl<C: Config> ChipOpening<C> {
             local: vec![],
             next: vec![],
         };
-
         let preprocessed_width = chip.preprocessed_width();
+        // Assert that the length of the dynamic arrays match the expected length of the vectors.
+        builder.assert_usize_eq(preprocessed_width, opening.preprocessed.local.len());
+        builder.assert_usize_eq(preprocessed_width, opening.preprocessed.next.len());
+        // Collect the preprocessed values into vectors.
         for i in 0..preprocessed_width {
             preprocessed
                 .local
@@ -99,6 +108,10 @@ impl<C: Config> ChipOpening<C> {
             next: vec![],
         };
         let main_width = chip.width();
+        // Assert that the length of the dynamic arrays match the expected length of the vectors.
+        builder.assert_usize_eq(main_width, opening.main.local.len());
+        builder.assert_usize_eq(main_width, opening.main.next.len());
+        // Collect the main values into vectors.
         for i in 0..main_width {
             main.local.push(builder.get(&opening.main.local, i));
             main.next.push(builder.get(&opening.main.next, i));
@@ -108,8 +121,11 @@ impl<C: Config> ChipOpening<C> {
             local: vec![],
             next: vec![],
         };
-        let permutation_width =
-            C::EF::D * ((chip.num_interactions() + 1) / chip.logup_batch_size() + 1);
+        let permutation_width = C::EF::D * chip.permutation_width();
+        // Assert that the length of the dynamic arrays match the expected length of the vectors.
+        builder.assert_usize_eq(permutation_width, opening.permutation.local.len());
+        builder.assert_usize_eq(permutation_width, opening.permutation.next.len());
+        // Collect the permutation values into vectors.
         for i in 0..permutation_width {
             permutation
                 .local
@@ -120,10 +136,15 @@ impl<C: Config> ChipOpening<C> {
         }
 
         let num_quotient_chunks = 1 << chip.log_quotient_degree();
-
         let mut quotient = vec![];
+        // Assert that the length of the quotient chunk arrays match the expected length.
+        builder.assert_usize_eq(num_quotient_chunks, opening.quotient.len());
+        // Collect the quotient values into vectors.
         for i in 0..num_quotient_chunks {
             let chunk = builder.get(&opening.quotient, i);
+            // Assert that the chunk length matches the expected length.
+            builder.assert_usize_eq(C::EF::D, chunk.len());
+            // Collect the quotient values into vectors.
             let mut quotient_vals = vec![];
             for j in 0..C::EF::D {
                 let value = builder.get(&chunk, j);