use std::cell::{Ref, RefCell, RefMut};
use std::rc::Rc;

use crate::zk::dot_product::{
    zk_dot_product_commitment, zk_dot_product_proof, ZkDotTotalProof, ZkVectorProverData,
};
use crate::zk::error_correcting_code::{RsFromCoefficients, RsInterpolation};
use crate::zk::hadamard_product::{
    zk_hadamard_and_dots_proof, zk_hadamard_product_commitment, ZkHadamardAndDotsTotalProof,
};
use derive_where::derive_where;
use rand::Rng;
use serde::{Deserialize, Serialize};
use slop_algebra::AbstractField;
use slop_alloc::CpuBackend;
use slop_challenger::{CanObserve, FieldChallenger};
use slop_merkle_tree::TensorCsProver;

use super::prover_transcript::ProverElement;
use super::transcript::{
    MleCommitmentIndex, PcsCommitmentEntry, PcsMultiEvalClaim, Point, ProofTranscript,
    TranscriptLinConstraint, TranscriptMulConstraint,
};
use super::{
    ConstraintContextInner, ProverLinExpression, ProverValue, TranscriptIndex, ZkExpression,
    ZkMerkleizer, ZkPcsProver,
};
use super::{ExpressionIndex, ZkIopCtx};

/// A zk-proof generated by the [`ZkProverContext`] at the end of the protocol.
///
/// Should be opened to a static [`ZkCnstrProof`] and mutable [`ZkVerificationContext`] before use by verifier.
#[derive_where(Clone; GC::PcsProof: Clone)]
#[derive(Serialize, Deserialize)]
#[serde(bound(
    serialize = "GC::PcsProof: Serialize",
    deserialize = "GC::PcsProof: serde::de::DeserializeOwned"
))]
pub struct ZkProof<GC: ZkIopCtx> {
    pub(in crate::zk::inner) proof: ZkCnstrProof<GC>,
    pub(in crate::zk::inner) transcript: ProofTranscript<GC::EF>,
    /// PCS commitment transcript: metadata for each committed MLE.
    pub(in crate::zk::inner) pcs_commitment_transcript: Vec<PcsCommitmentEntry<GC::Digest>>,
}

/// The static proof data from [`ZkProof`] needed to verify linear and multiplicative constraints.
/// The multiplicative part is optional. PCS proofs are included when PCS was used.
#[derive_where(Clone; GC::PcsProof: Clone)]
#[derive(Serialize, Deserialize)]
#[serde(bound(
    serialize = "GC::PcsProof: Serialize",
    deserialize = "GC::PcsProof: serde::de::DeserializeOwned"
))]
pub struct ZkCnstrProof<GC: ZkIopCtx> {
    pub mask_commitment: GC::Digest,
    pub zk_dot_product_proof: ZkDotTotalProof<GC, RsFromCoefficients<GC::EF>>,
    pub mul_proof_wrapper: Option<ZkMulCnstrProof<GC>>,
    /// PCS proofs for each evaluation claim (empty if no PCS was used).
    pub pcs_proofs: Vec<GC::PcsProof>,
}

/// Just the data for proving multiplicative constraints.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(bound(serialize = "", deserialize = ""))]
#[allow(clippy::type_complexity)]
pub struct ZkMulCnstrProof<GC: ZkIopCtx> {
    /// Single shared commitment for all three vectors (a, b, c)
    pub commitment: GC::Digest,
    pub mul_proof: ZkHadamardAndDotsTotalProof<GC, RsInterpolation<GC::EF>>,
}

/// Handle to a [`ZkProverContextInner`] that provides shared mutable access.
/// This is the main type users interact with for building zero-knowledge proofs.
///
/// The handle wraps the inner context in `Rc<RefCell<>>` to allow elements
/// returned from `add_values` to hold references back to the context.
///
/// # Type Parameters
/// * `GC` - The ZK IOP context type
/// * `MK` - The merkleizer type used for tensor commitments
/// * `PD` - The PCS prover data type (defaults to `()` when no PCS is used)
///
/// Contains a challenger which can be accessed using self.challenger()
#[derive_where(Clone; PD: Clone)]
pub struct ZkProverContext<GC: ZkIopCtx, MK: ZkMerkleizer<GC>, PD = ()> {
    inner: Rc<RefCell<ZkProverContextInner<GC, MK, PD>>>,
}

/// Tracks linear constraints during zero-knowledge proof generation.
/// Also tracks masking values and their dot-product commitment.
/// Consumed at the end to produce a [`ZkProof`].
#[allow(clippy::type_complexity)]
#[derive_where(Clone; <MK as TensorCsProver<GC, CpuBackend>>::ProverData: Clone, PD: Clone)]
pub struct ZkProverContextInner<GC: ZkIopCtx, MK: ZkMerkleizer<GC>, PD = ()> {
    /// The challenger for Fiat-Shamir (access via ZkProverContext::challenger())
    challenger: GC::Challenger,

    // transcript is represented as a jagged array, the breakpoints are the index starts of each piece
    transcript: ProofTranscript<GC::EF>,

    // Need to keep track of where in masks we are to generate the masked values
    masks: Vec<GC::EF>,
    masks_current_index: usize,

    // Linear combinations of values that need to equal 0
    // Each constraint is a vector of (coefficient, index in masked_values as a jagged array)
    lin_constraints: Vec<TranscriptLinConstraint<GC::EF>>,

    // Multiplicative constraints (if needed)
    // Each constraint is a vector of indices a,b,c where a*b=c
    mul_constraints: Option<Vec<TranscriptMulConstraint<GC::EF>>>,

    // Commitments generated on initialization
    mask_commitment: GC::Digest,
    prover_secret_data: ZkVectorProverData<
        GC,
        <MK as TensorCsProver<GC, CpuBackend>>::ProverData,
        RsFromCoefficients<GC::EF>,
    >,

    expressions: Vec<ZkExpression<GC::EF, ProverElement<GC::EF>>>,

    // PCS commitment entries with their prover data
    pcs_commitments: Vec<(PcsCommitmentEntry<GC::Digest>, PD)>,

    // PCS evaluation claims to be proven (each may batch multiple commitments at same point)
    pcs_eval_claims: Vec<PcsMultiEvalClaim<GC::EF, ProverValue<GC, MK, PD>>>,

    // Debug: constraint debugger (only present when sp1_debug_constraints is enabled)
    #[cfg(sp1_debug_constraints)]
    debugger: crate::zk::inner::debug::ConstraintDebugger,
}

impl<GC: ZkIopCtx, MK: ZkMerkleizer<GC>, PD> super::constraints::private::Sealed
    for ZkProverContext<GC, MK, PD>
{
}

impl<GC: ZkIopCtx, MK: ZkMerkleizer<GC>, PD: Clone> ConstraintContextInner<GC::EF>
    for ZkProverContext<GC, MK, PD>
{
    type Element = ProverElement<GC::EF>;

    fn add_lin_constraints(
        &mut self,
        constraints: impl IntoIterator<Item = TranscriptLinConstraint<GC::EF>>,
    ) {
        let mut inner = self.borrow_mut();
        let constraints: Vec<_> = constraints.into_iter().collect();
        #[cfg(sp1_debug_constraints)]
        inner.debugger.on_constraints_added(constraints.len());
        inner.lin_constraints.extend(constraints);
    }

    fn add_expr(
        &mut self,
        expr: ZkExpression<GC::EF, ProverElement<GC::EF>>,
    ) -> ProverValue<GC, MK, PD> {
        self.borrow_mut().expressions.push(expr);
        ExpressionIndex::new(self.borrow().expressions.len() - 1, self.clone())
    }

    fn get_expr(&self, index: usize) -> Option<ZkExpression<GC::EF, ProverElement<GC::EF>>> {
        self.borrow().expressions.get(index).cloned()
    }

    fn add_mul_constraints(
        &mut self,
        constraints: impl IntoIterator<Item = TranscriptMulConstraint<GC::EF>>,
    ) {
        let mut inner = self.borrow_mut();
        if let Some(mul_constraints) = &mut inner.mul_constraints {
            mul_constraints.extend(constraints);
        } else {
            panic!("Multiplicative constraints are not supported by this prover");
        }
    }

    #[cfg(sp1_debug_constraints)]
    fn name_last_lin_constraint_inner(&self, name: impl Into<String>) {
        self.borrow_mut().debugger.name_last(name);
    }

    fn materialize_prod(
        &mut self,
        a: ProverLinExpression<GC::EF>,
        b: ProverLinExpression<GC::EF>,
    ) -> Option<ProverElement<GC::EF>> {
        let elt = self.add_value_raw(a.value() * b.value());
        self.constrain_mul_triple(a, b, elt);
        Some(elt)
    }

    fn add_eval_claim(
        &mut self,
        commitment_indices: Vec<MleCommitmentIndex>,
        point: Point<GC::EF>,
        eval_exprs: Vec<ProverValue<GC, MK, PD>>,
    ) {
        self.borrow_mut().pcs_eval_claims.push(PcsMultiEvalClaim {
            commitment_indices,
            point,
            eval_exprs,
        });
    }
}

impl<GC: ZkIopCtx, MK: ZkMerkleizer<GC>, PD> ZkProverContext<GC, MK, PD> {
    /// Borrow the inner context mutably and return a guard.
    pub fn borrow_mut(&self) -> RefMut<'_, ZkProverContextInner<GC, MK, PD>> {
        self.inner.borrow_mut()
    }

    /// Borrow the inner context immutably and return a guard.
    pub fn borrow(&self) -> Ref<'_, ZkProverContextInner<GC, MK, PD>> {
        self.inner.borrow()
    }

    /// Access the challenger for Fiat-Shamir operations.
    pub fn challenger(&mut self) -> RefMut<'_, GC::Challenger> {
        RefMut::map(self.borrow_mut(), |inner| &mut inner.challenger)
    }

    /// Initializes a prover that supports only linear constraints.
    ///
    /// Generates random masks, commits to them, and sets up the Fiat-Shamir challenger.
    /// Adding multiplicative constraints to the returned context will panic;
    /// use [`Self::initialize`] if multiplicative constraints are needed.
    ///
    /// # Arguments
    /// * `length` - Upper bound on the number of transcript elements that will be added.
    /// * `rng` - Cryptographically secure random number generator.
    ///
    /// # Panics
    /// Later calls will panic if more than `length` transcript elements are added.
    /// Compile with `RUSTFLAGS="--cfg sp1_debug_constraints"` to detect over-allocation.
    pub fn initialize_only_lin_constraints<RNG: rand::CryptoRng + Rng>(
        length: usize,
        rng: &mut RNG,
    ) -> Self
    where
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
    {
        Self::initialize_inner(length, false, rng)
    }

    /// Initializes a prover that supports both linear and multiplicative constraints.
    ///
    /// Generates random masks (with extra padding for multiplicative constraint masking),
    /// commits to them, and sets up the Fiat-Shamir challenger.
    ///
    /// # Arguments
    /// * `length` - Upper bound on the number of transcript elements that will be added.
    /// * `rng` - Cryptographically secure random number generator.
    ///
    /// # Panics
    /// Later calls will panic if more than `length` transcript elements are added.
    /// Compile with `RUSTFLAGS="--cfg sp1_debug_constraints"` to detect over-allocation.
    pub fn initialize<RNG: rand::CryptoRng + Rng>(length: usize, rng: &mut RNG) -> Self
    where
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
    {
        Self::initialize_inner(length, true, rng)
    }

    /// Shared initialization logic for both `initialize` and `initialize_only_lin_constraints`.
    fn initialize_inner<RNG: rand::CryptoRng + Rng>(
        length: usize,
        with_mul_constraints: bool,
        rng: &mut RNG,
    ) -> Self
    where
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
    {
        let merkleizer = MK::default();
        let mut challenger = GC::default_challenger();

        // Length +1 to allow for the constant first value
        // and +6 to allow for padding to deal with multiplicative constraints (if needed)
        let mul_padding = if with_mul_constraints { 6 } else { 0 };
        let real_length = length + 1 + mul_padding;
        let masks: Vec<GC::EF> = std::iter::repeat_with(|| rng.gen()).take(real_length).collect();

        let (commitment, prover_secret_data) =
            zk_dot_product_commitment::<GC, MK, _, RsFromCoefficients<GC::EF>>(
                std::slice::from_ref(&masks),
                rng,
                &merkleizer,
            );

        challenger.observe(commitment);

        let mul_constraints = if with_mul_constraints { Some(vec![]) } else { None };

        let mut inner = ZkProverContextInner {
            challenger,
            transcript: ProofTranscript::new(real_length),
            masks,
            masks_current_index: 0,
            lin_constraints: vec![],
            mul_constraints,
            mask_commitment: commitment,
            prover_secret_data,
            expressions: vec![],
            pcs_commitments: vec![],
            pcs_eval_claims: vec![],
            #[cfg(sp1_debug_constraints)]
            debugger: super::debug::ConstraintDebugger::new(),
        };

        // Add a dummy constant value to allow for affine constraints
        inner.transcript.add_values(&[GC::EF::one() + inner.masks[0]]);
        inner.masks_current_index += 1;

        Self { inner: Rc::new(RefCell::new(inner)) }
    }

    fn add_values_raw(&mut self, new_values: &[GC::EF]) -> usize {
        let mut inner = self.borrow_mut();
        let masked: Vec<GC::EF> = new_values
            .iter()
            .enumerate()
            .map(|(i, &value)| value + inner.masks[inner.masks_current_index + i])
            .collect();

        let block_index = inner.transcript.next_block_index();

        inner.challenger.observe_ext_element_slice(&masked);
        inner.masks_current_index = inner.transcript.add_values(&masked);

        block_index
    }

    /// Adds new values to the proof and observes them for Fiat-Shamir.
    ///
    /// Returns the [`ExpressionIndex`]'s that these added values correspond to
    pub fn add_values(&mut self, new_values: &[GC::EF]) -> Vec<ProverValue<GC, MK, PD>>
    where
        PD: Clone,
    {
        let block_index = self.add_values_raw(new_values);
        new_values
            .iter()
            .enumerate()
            .map(|(i, &value)| {
                let elt = ProverElement::new(value, [block_index, i].into());
                self.add_expr(elt.into())
            })
            .collect()
    }

    fn add_value_raw(&mut self, value: GC::EF) -> ProverElement<GC::EF> {
        let block_index = self.add_values_raw(&[value]);
        ProverElement::new(value, [block_index, 0].into())
    }

    /// Adds a single value to the proof and observes it for Fiat-Shamir.
    ///
    /// Returns the [`ExpressionIndex`] that it corresponds to.
    pub fn add_value(&mut self, new_value: GC::EF) -> ProverValue<GC, MK, PD>
    where
        PD: Clone,
    {
        let elt = self.add_value_raw(new_value);
        self.add_expr(elt.into())
    }

    /// Returns the index of the next block to be added
    pub fn next_block_index(&self) -> usize {
        self.borrow().transcript.next_block_index()
    }

    /// Commits to a flat MLE and registers it in the context.
    ///
    /// This is the primary method for committing MLEs. It:
    /// 1. Calls the PCS prover to stack and generate the commitment
    /// 2. Observes the commitment digest in the Fiat-Shamir challenger
    /// 3. Stores the prover data for later proof generation
    ///
    /// # Arguments
    /// * `mle` — the flat (unstacked) MLE to commit to, with
    ///   `num_encoding_variables + log_num_polynomials` total variables.
    /// * `log_num_polynomials` — log2 of the number of stacked polynomials (tensor height).
    ///   The inferred `num_encoding_variables = mle.num_variables() - log_num_polynomials`
    ///   must match the value the PCS was initialized with.
    /// * `pcs_prover` — the PCS prover for generating commitments.
    /// * `rng` — cryptographically secure random number generator.
    ///
    /// # Returns
    /// An `MleCommitmentIndex` that can be used to reference this commitment
    /// when adding evaluation claims, or an error if commitment fails.
    pub fn commit_mle<P, RNG>(
        &mut self,
        mle: slop_multilinear::Mle<GC::F, slop_alloc::CpuBackend>,
        log_num_polynomials: usize,
        pcs_prover: &P,
        rng: &mut RNG,
    ) -> Result<MleCommitmentIndex, super::ZkPcsCommitmentError>
    where
        P: super::ZkPcsProver<GC, MK, ProverData = PD>,
        RNG: rand::CryptoRng + rand::Rng,
        rand::distributions::Standard: rand::distributions::Distribution<GC::F>,
    {
        // Compute num_vars from the flat MLE's total variables minus stacking height
        let num_vars = mle.num_variables() as usize - log_num_polynomials;
        let log_num_polys = log_num_polynomials;

        // Generate commitment using the PCS prover (stacking happens inside)
        let (digest, prover_data) = pcs_prover.commit_mle(mle, log_num_polynomials, rng)?;

        // Register the commitment internally
        Ok(self.register_commitment(digest, prover_data, num_vars, log_num_polys))
    }

    /// Registers a pre-committed MLE in the context.
    ///
    /// The commitment digest is observed in the Fiat-Shamir challenger.
    /// The prover data is stored internally for use during proof generation.
    ///
    /// Prefer using `commit_mle` which handles commitment generation automatically.
    /// This method is exposed for testing and advanced use cases where commitment
    /// is generated separately.
    pub(in crate::zk::inner) fn register_commitment(
        &mut self,
        digest: GC::Digest,
        prover_data: PD,
        num_vars: usize,
        log_num_polys: usize,
    ) -> MleCommitmentIndex {
        let mut inner = self.borrow_mut();

        // Observe the commitment digest in the Fiat-Shamir challenger
        inner.challenger.observe(digest);

        // Store the commitment entry with prover data
        let index = inner.pcs_commitments.len();
        let entry = PcsCommitmentEntry { digest, num_vars, log_num_polys };
        inner.pcs_commitments.push((entry, prover_data));

        MleCommitmentIndex::new(index)
    }

    /// Returns the PCS commitment entries registered so far (without prover data).
    pub fn pcs_commitments(&self) -> Vec<PcsCommitmentEntry<GC::Digest>> {
        self.borrow().pcs_commitments.iter().map(|(entry, _)| entry.clone()).collect()
    }

    /// Returns the PCS evaluation claims registered so far.
    pub fn pcs_eval_claims(&self) -> Vec<PcsMultiEvalClaim<GC::EF, ProverValue<GC, MK, PD>>>
    where
        PD: Clone,
    {
        self.borrow().pcs_eval_claims.clone()
    }

    /// Returns the prover data for a given commitment index.
    ///
    /// Returns `None` if the commitment index is out of bounds.
    pub fn get_prover_data(&self, index: MleCommitmentIndex) -> Option<PD>
    where
        PD: Clone,
    {
        self.borrow().pcs_commitments.get(index.index()).map(|(_, data)| data.clone())
    }

    /// Generates a zero-knowledge dot-product proof for the constraints.
    ///
    /// Consumes the builder. Call this after all constraints and values have been added.
    /// Creates a default merkleizer internally.
    ///
    /// # Arguments
    /// * `rng` - Cryptographically secure random number generator
    /// * `pcs_prover` - Optional PCS prover. If provided, generates evaluation proofs
    ///   for all registered PCS eval claims using the stored prover data.
    ///   If `None` and there are eval claims, this method will panic.
    ///
    /// # Returns
    /// A `ZkProof` containing all constraint proofs and PCS proofs.
    /// The PCS proofs vector inside is empty if no PCS prover was provided.
    ///
    /// # Type Parameters
    /// * `P` - The PCS prover type implementing `ZkPcsProver<GC>` with `ProverData = PD`
    pub fn prove<RNG, P>(mut self, rng: &mut RNG, pcs_prover: Option<&P>) -> ZkProof<GC>
    where
        RNG: rand::CryptoRng + rand::Rng,
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
        P: ZkPcsProver<GC, MK, ProverData = PD>,
        PD: Clone,
    {
        let merkleizer = MK::default();

        // Handle PCS evaluation claims first
        let pcs_proofs = self.generate_pcs_proofs(pcs_prover);

        // Handle multiplicative constraints
        let mul_proof = self.generate_mul_proof(&merkleizer, rng);

        // Debug checks
        #[cfg(sp1_debug_constraints)]
        {
            let inner = self.borrow();

            //check each linear constraint individually before RLC
            inner.debugger.check_and_report(
                &inner.transcript,
                &inner.masks,
                &inner.lin_constraints,
            );

            // Check if there were extra masks
            let structural_mask_length = if inner.mul_constraints.is_some() { 1 + 6 } else { 1 };
            if inner.masks_current_index < inner.masks.len() {
                eprintln!(
                    "WARNING: Not all masks were used. {} non-structural masks were generated but only {} were used.",
                    inner.masks.len() - structural_mask_length,
                    inner.masks_current_index - structural_mask_length
                );
            } else {
                eprintln!(
                    "All masks were used. {} non-structural masks were generated and used.",
                    inner.masks.len() - structural_mask_length
                );
            }
        }

        // Dot Product proof for linear constraints
        let rlc_coeff: GC::EF = self.borrow_mut().challenger.sample_ext_element();

        let dot_vec = {
            let inner = self.borrow();
            inner.transcript.generate_rlc_dot_vector(&inner.lin_constraints, rlc_coeff)
        };

        // Extract the inner context, cloning if there are still outstanding references
        // (e.g., from ProverElement instances that haven't been dropped yet)
        let mut inner = match Rc::try_unwrap(self.inner) {
            Ok(refcell) => refcell.into_inner(),
            Err(rc) => {
                eprintln!(
                    "WARNING: ZkProverContext has outstanding references (likely from ProverElements or ProverConstraints). \
                     Cloning inner context. Consider dropping ProverElements before calling into_proof."
                );
                rc.borrow().clone()
            }
        };

        let total_dot_proof = zk_dot_product_proof(
            &dot_vec,
            &inner.mask_commitment,
            inner.prover_secret_data,
            &mut inner.challenger,
            &merkleizer,
        );

        // Extract just the commitment entries (without prover data) for the proof
        let pcs_commitment_transcript =
            inner.pcs_commitments.into_iter().map(|(entry, _)| entry).collect();

        ZkProof {
            proof: ZkCnstrProof {
                mask_commitment: inner.mask_commitment,
                zk_dot_product_proof: total_dot_proof,
                mul_proof_wrapper: mul_proof,
                pcs_proofs,
            },
            transcript: inner.transcript,
            pcs_commitment_transcript,
        }
    }

    /// Helper method to generate PCS proofs for all evaluation claims.
    ///
    /// One proof is generated per claim. Panics if multiple claims exist for the same
    /// commitment, as this breaks zero-knowledge
    fn generate_pcs_proofs<P>(&mut self, pcs_prover: Option<&P>) -> Vec<GC::PcsProof>
    where
        P: ZkPcsProver<GC, MK, ProverData = PD>,
        PD: Clone,
    {
        let eval_claims = self.pcs_eval_claims();

        if eval_claims.is_empty() {
            return vec![];
        }

        // Check for duplicate commitment indices — multiple eval claims on the
        // same commitment would leak information and break zero-knowledge.
        let mut seen = std::collections::HashSet::new();
        for claim in &eval_claims {
            for idx in &claim.commitment_indices {
                if !seen.insert(*idx) {
                    panic!(
                        "Multiple eval claims on the same PCS commitment (index {}). \
                         This breaks zero-knowledge but not soundness.",
                        idx.index(),
                    );
                }
            }
        }

        let pcs_prover = pcs_prover.expect(
            "PCS evaluation claims exist but no PCS prover was provided. \
             Call prove with pcs_prover: Some(&prover) when using add_eval_claim.",
        );

        let mut pcs_proofs = Vec::with_capacity(eval_claims.len());
        for claim in eval_claims {
            let proof = pcs_prover.prove_multi_eval(self, claim);
            pcs_proofs.push(proof);
        }

        // Clear eval claims to drop ProverValue references before calling into_proof
        self.borrow_mut().pcs_eval_claims.clear();

        pcs_proofs
    }

    /// Helper method to generate multiplicative constraint proofs.
    fn generate_mul_proof<RNG>(
        &mut self,
        merkleizer: &MK,
        rng: &mut RNG,
    ) -> Option<ZkMulCnstrProof<GC>>
    where
        RNG: rand::CryptoRng + rand::Rng,
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
        PD: Clone,
    {
        self.borrow().mul_constraints.as_ref()?;

        // Pad the R1CS witness used by the Hadamard check by `(r, s, rs, r-1, t, (r-1)t)`
        // for i.i.d. uniform `r, s, t`, realizing the two tautological multiplicative
        // relations `r * s = rs` and `(r-1) * t = (r-1)t`.
        //
        // Note: the simulator's bijection requires `rlc_coeff ≠ 0` and `rlc_coeff ≠ -1`
        // (where `rlc_coeff` is sampled below). We do not condition the proof on these
        // holding, so the protocol is only statistically zero-knowledge against an
        // honest verifier. Because `rlc_coeff` is derived via Fiat-Shamir from the
        // transcript hash, the verifier behaves as honest and this does not affect
        // deployment.
        let r: GC::EF = rng.gen();
        let s: GC::EF = rng.gen();
        let t: GC::EF = rng.gen();
        let r_minus_1 = r - GC::EF::one();

        let padding_block = self.next_block_index();
        self.add_values_raw(&[r, s, r * s, r_minus_1, t, r_minus_1 * t]);

        self.constrain_mul_triple(
            TranscriptIndex::<GC::EF>::from([padding_block, 0]),
            TranscriptIndex::<GC::EF>::from([padding_block, 1]),
            TranscriptIndex::<GC::EF>::from([padding_block, 2]),
        );
        self.constrain_mul_triple(
            TranscriptIndex::<GC::EF>::from([padding_block, 3]),
            TranscriptIndex::<GC::EF>::from([padding_block, 4]),
            TranscriptIndex::<GC::EF>::from([padding_block, 5]),
        );

        // Extract mul_vecs and mul_len from the inner context
        let (mul_vecs, mul_len) = {
            let inner = self.borrow();
            let mul_constraints = inner.mul_constraints.as_ref().unwrap();
            let mul_len = mul_constraints.len();

            let mut mul_vecs: [Vec<GC::EF>; 3] = [vec![], vec![], vec![]];
            for constraint in mul_constraints.iter() {
                for (i, cnstr) in constraint.0.iter().enumerate() {
                    let value = cnstr.iter().fold(GC::EF::zero(), |acc, (coeff, index)| {
                        let fi = inner.transcript.to_flat_index(index);
                        acc + *coeff * (inner.transcript.values[fi] - inner.masks[fi])
                    });
                    mul_vecs[i].push(value);
                }
            }
            (mul_vecs, mul_len)
        };

        // Commit the vectors (returns single shared commitment)
        let (commitment, prover_data) = zk_hadamard_product_commitment::<
            GC,
            MK,
            _,
            RsInterpolation<GC::EF>,
        >(
            &mul_vecs[0], &mul_vecs[1], &mul_vecs[2], rng, merkleizer
        );

        // Sample RLC coefficient
        let rlc_coeff: GC::EF = {
            let mut inner = self.borrow_mut();
            inner.challenger.sample_ext_element()
        };

        // Compute dot_vec from RLC powers
        let dot_vec: Vec<GC::EF> = rlc_coeff.powers().take(mul_len).collect();

        // Generate combined hadamard + dot product proofs with shared indices
        let total_mul_proof = {
            let mut inner = self.borrow_mut();
            zk_hadamard_and_dots_proof::<GC, MK, RsInterpolation<GC::EF>>(
                commitment,
                &dot_vec,
                prover_data,
                &mut inner.challenger,
                merkleizer,
            )
        };

        // Build and add the new linear constraints
        let new_lin_constraints = {
            let dot_prods: [GC::EF; 3] =
                std::array::from_fn(|i| total_mul_proof.dot_claimed_dot_products()[i]);
            let inner = self.borrow();
            let mul_constraints = inner.mul_constraints.as_ref().unwrap();
            inner.transcript.pickout_lin_constraints_from_mul_constraints(
                mul_constraints,
                &dot_prods,
                rlc_coeff,
            )
        };

        self.add_lin_constraints(new_lin_constraints.to_vec());

        Some(ZkMulCnstrProof { commitment, mul_proof: total_mul_proof })
    }
}

/// A no-op PCS prover for when no PCS is needed.
///
/// This type is used as a default when calling `prove` without PCS support.
/// It produces no proofs and panics if actually asked to prove anything.
#[derive(Clone, Copy, Debug)]
pub struct NoPcsProver;

impl<GC: ZkIopCtx, MK: ZkMerkleizer<GC>> ZkPcsProver<GC, MK> for NoPcsProver {
    type ProverData = ();

    fn commit_mle<RNG: rand::CryptoRng + rand::Rng>(
        &self,
        _mle: slop_multilinear::Mle<GC::F, slop_alloc::CpuBackend>,
        _log_num_polynomials: usize,
        _rng: &mut RNG,
    ) -> Result<(GC::Digest, Self::ProverData), super::ZkPcsCommitmentError>
    where
        rand::distributions::Standard: rand::distributions::Distribution<GC::F>,
    {
        panic!("NoPcsProver::commit_mle should never be called")
    }

    fn prove_multi_eval(
        &self,
        _ctx: &mut ZkProverContext<GC, MK, ()>,
        _claim: PcsMultiEvalClaim<GC::EF, ProverValue<GC, MK, ()>>,
    ) -> GC::PcsProof {
        panic!("NoPcsProver::prove_multi_eval should never be called")
    }
}

impl<GC: ZkIopCtx, MK: ZkMerkleizer<GC>> ZkProverContext<GC, MK, ()> {
    /// Convenience method to generate a proof without PCS support.
    ///
    /// This is equivalent to calling `prove(rng, None::<&NoPcsProver>)`
    /// but with simpler syntax for the common case where no PCS is needed.
    ///
    /// # Panics
    /// Panics if there are any PCS evaluation claims registered.
    pub fn prove_without_pcs<RNG: rand::CryptoRng + rand::Rng>(self, rng: &mut RNG) -> ZkProof<GC>
    where
        rand::distributions::Standard: rand::distributions::Distribution<GC::EF>,
    {
        self.prove::<RNG, NoPcsProver>(rng, None)
    }
}
