@@ -1,9 +1,15 @@
 use ark_bls12_381::Fr;
-use ark_std::test_rng;
-use poly_iop::{PolyIOP, PolyIOPErrors, SumCheck, VirtualPolynomial, ZeroCheck};
-use std::time::Instant;
+use ark_poly::{DenseMultilinearExtension, MultilinearExtension};
+use ark_std::{test_rng, UniformRand};
+use poly_iop::{
+    identity_permutation_mle, PermutationCheck, PolyIOP, PolyIOPErrors, SumCheck, VPAuxInfo,
+    VirtualPolynomial, ZeroCheck,
+};
+use std::{marker::PhantomData, time::Instant};
 
 fn main() -> Result<(), PolyIOPErrors> {
+    bench_permutation_check()?;
+    println!("\n\n");
     bench_sum_check()?;
     println!("\n\n");
     bench_zero_check()
@@ -105,13 +111,14 @@ let start = Instant::now();
                 let mut transcript = <PolyIOP<Fr> as ZeroCheck<Fr>>::init_transcript();
                 transcript.append_message(b"testing", b"initializing transcript for testing")?;
                 let subclaim =
-                    <PolyIOP<Fr> as ZeroCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?.0;
+                    <PolyIOP<Fr> as ZeroCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?
+                        .sum_check_sub_claim;
                 assert!(
                     poly.evaluate(&subclaim.point)? == subclaim.expected_evaluation,
                     "wrong subclaim"
                 );
                 println!(
-                    "zero check verification time for {} variables and {} degree:: {} ns",
+                    "zero check verification time for {} variables and {} degree: {} ns",
                     nv,
                     degree,
                     start.elapsed().as_nanos() / repetition as u128
@@ -123,3 +130,84 @@ }
     }
     Ok(())
 }
+
+fn bench_permutation_check() -> Result<(), PolyIOPErrors> {
+    let mut rng = test_rng();
+
+    for nv in 4..20 {
+        let repetition = if nv < 10 {
+            100
+        } else if nv < 20 {
+            50
+        } else {
+            10
+        };
+
+        let w = DenseMultilinearExtension::rand(nv, &mut rng);
+
+        // s_perm is the identity map
+        let s_perm = identity_permutation_mle(nv);
+
+        let proof = {
+            let start = Instant::now();
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+
+            let mut challenge =
+                <PolyIOP<Fr> as PermutationCheck<Fr>>::generate_challenge(&mut transcript)?;
+
+            let prod_x_and_aux = <PolyIOP<Fr> as PermutationCheck<Fr>>::compute_products(
+                &challenge, &w, &w, &s_perm,
+            )?;
+
+            let prod_x_binding = mock_commit(&prod_x_and_aux[0]);
+
+            <PolyIOP<Fr> as PermutationCheck<Fr>>::update_challenge(
+                &mut challenge,
+                &mut transcript,
+                &prod_x_binding,
+            )?;
+
+            let proof = <PolyIOP<Fr> as PermutationCheck<Fr>>::prove(
+                &prod_x_and_aux,
+                &challenge,
+                &mut transcript,
+            )?;
+
+            println!(
+                "permutation check proving time for {} variables: {} ns",
+                nv,
+                start.elapsed().as_nanos() / repetition as u128
+            );
+            proof
+        };
+
+        {
+            let poly_info = VPAuxInfo {
+                max_degree: 2,
+                num_variables: nv,
+                phantom: PhantomData::default(),
+            };
+
+            let start = Instant::now();
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+            let _subclaim =
+                <PolyIOP<Fr> as PermutationCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?;
+            println!(
+                "permutation check verification time for {} variables: {} ns",
+                nv,
+                start.elapsed().as_nanos() / repetition as u128
+            );
+        }
+
+        println!("====================================");
+    }
+
+    Ok(())
+}
+
+fn mock_commit(_f: &DenseMultilinearExtension<Fr>) -> Fr {
+    let mut rng = test_rng();
+    Fr::rand(&mut rng)
+}

@@ -4,4 +4,5 @@
 Implements the following protocols
 
 - [x] sum checks
-- [x] zero checks+- [x] zero checks
+- [x] permutation checks

@@ -11,8 +11,12 @@ mod virtual_poly;
 mod zero_check;
 
 pub use errors::PolyIOPErrors;
+pub use perm_check::{
+    util::{identity_permutation_mle, random_permutation_mle},
+    PermutationCheck,
+};
 pub use sum_check::SumCheck;
-pub use virtual_poly::VirtualPolynomial;
+pub use virtual_poly::{VPAuxInfo, VirtualPolynomial};
 pub use zero_check::ZeroCheck;
 
 #[derive(Clone, Debug, Default, Copy)]

@@ -1,205 +1,618 @@
-//! This module implements the permutation check protocol.
+//! Main module for the Permutation Check protocol
 
-use crate::{utils::get_index, PolyIOPErrors};
+use crate::{
+    errors::PolyIOPErrors, perm_check::util::compute_prod_0, structs::IOPProof,
+    transcript::IOPTranscript, utils::get_index, PolyIOP, VirtualPolynomial, ZeroCheck,
+};
 use ark_ff::PrimeField;
 use ark_poly::DenseMultilinearExtension;
 use ark_std::{end_timer, start_timer};
+use std::rc::Rc;
 
-/// Compute `prod(0,x) := prod(0, x1, …, xn)` which is the MLE over the
-/// evaluations of the following polynomial on the boolean hypercube {0,1}^n:
+pub mod util;
+
+/// A PermutationCheck is derived from ZeroCheck.
 ///
-///  (w(x) + \beta s_id(x) + \gamma)/(w(x) + \beta s_perm(x) + \gamma)
+/// A Permutation Check IOP takes the following steps:
 ///
-/// where
-/// - beta and gamma are challenges
-/// - w(x), s_id(x), s_perm(x) are mle-s
+/// Inputs:
+/// - f(x)
+/// - g(x)
+/// - permutation s_perm(x)
 ///
-/// The caller needs to check num_vars matches in w/s_id/s_perm
-/// Cost: linear in N.
-#[allow(dead_code)]
-// TODO: remove
-fn compute_prod_0<F: PrimeField>(
-    beta: &F,
-    gamma: &F,
-    w: &DenseMultilinearExtension<F>,
-    s_id: &DenseMultilinearExtension<F>,
-    s_perm: &DenseMultilinearExtension<F>,
-) -> Result<DenseMultilinearExtension<F>, PolyIOPErrors> {
-    let start = start_timer!(|| "compute prod(1,x)");
-    let num_vars = w.num_vars;
-    let eval: Vec<F> = w
-        .iter()
-        .zip(s_id.iter().zip(s_perm.iter()))
-        .map(|(wi, (s_id_i, s_perm_i))| {
-            let tmp = *wi + *gamma;
-            (tmp + *beta * *s_id_i) / (tmp + *beta * *s_perm_i)
-        })
-        .collect();
+/// Steps:
+/// 1. `generate_challenge` from current transcript (generate beta, gamma)
+/// 2. `compute_product` to build `prod(x)` etc. from f, g and s_perm
+/// 3. push a commitment of `prod(x)` to the transcript (done by the snark
+/// caller)
+/// 4. `update_challenge` with the updated transcript (generate alpha)
+/// 5. `prove` to generate the proof
+pub trait PermutationCheck<F: PrimeField>: ZeroCheck<F> {
+    type PermutationCheckSubClaim;
+    type PermutationChallenge;
+
+    /// Initialize the system with a transcript
+    ///
+    /// This function is optional -- in the case where a PermutationCheck is
+    /// an building block for a more complex protocol, the transcript
+    /// may be initialized by this complex protocol, and passed to the
+    /// PermutationCheck prover/verifier.
+    fn init_transcript() -> Self::Transcript;
+
+    /// Step 1 of the IOP.
+    /// Generate challenge beta and gamma from a transcript.
+    fn generate_challenge(
+        transcript: &mut Self::Transcript,
+    ) -> Result<Self::PermutationChallenge, PolyIOPErrors>;
+
+    /// Step 4 of the IOP.
+    /// Update the challenge with alpha; returns an error if
+    /// alpha already exists.
+    fn update_challenge(
+        challenge: &mut Self::PermutationChallenge,
+        transcript: &mut Self::Transcript,
+        prod_x_binding: &F,
+    ) -> Result<(), PolyIOPErrors>;
+
+    /// Step 2 of the IOP.
+    /// Compute the following 7 polynomials
+    /// - prod(x)
+    /// - prod(0, x)
+    /// - prod(1, x)
+    /// - prod(x, 0)
+    /// - prod(x, 1)
+    /// - numerator
+    /// - denominator
+    ///
+    /// where
+    /// - `prod(0,x) := prod(0, x0, x1, …, xn)` which is the MLE over the
+    /// evaluations of the following polynomial on the boolean hypercube
+    /// {0,1}^n:
+    ///
+    ///  (f(x) + \beta s_id(x) + \gamma)/(g(x) + \beta s_perm(x) + \gamma)
+    ///
+    ///   where
+    ///   - beta and gamma are challenges
+    ///   - f(x), g(x), s_id(x), s_perm(x) are mle-s
+    ///
+    /// - `prod(1,x) := prod(x, 0) * prod(x, 1)`
+    /// - numerator is the MLE for `f(x) + \beta s_id(x) + \gamma`
+    /// - denominator is the MLE for `g(x) + \beta s_perm(x) + \gamma`
+    ///
+    /// The caller needs to check num_vars matches in f/g/s_id/s_perm
+    /// Cost: linear in N.
+    fn compute_products(
+        challenge: &Self::PermutationChallenge,
+        fx: &DenseMultilinearExtension<F>,
+        gx: &DenseMultilinearExtension<F>,
+        s_perm: &DenseMultilinearExtension<F>,
+    ) -> Result<[DenseMultilinearExtension<F>; 7], PolyIOPErrors>;
+
+    /// Step 5 of the IOP.
+    ///
+    /// Initialize the prover to argue that an MLE g(x) is a permutation of
+    /// MLE f(x) over a permutation given by s_perm.
+    /// Inputs:
+    /// - 7 MLEs from `Self::compute_products`
+    /// - challenge: `Self::Challenge` that has been updated
+    /// - transcript: a transcript that is used to generate the challenges beta
+    ///   and gamma
+    /// Cost: O(N)
+    fn prove(
+        prod_x_and_aux_info: &[DenseMultilinearExtension<F>; 7],
+        challenge: &Self::PermutationChallenge,
+        transcript: &mut IOPTranscript<F>,
+    ) -> Result<Self::Proof, PolyIOPErrors>;
+
+    /// Verify that an MLE g(x) is a permutation of
+    /// MLE f(x) over a permutation given by s_perm.
+    fn verify(
+        proof: &Self::Proof,
+        aux_info: &Self::VPAuxInfo,
+        transcript: &mut Self::Transcript,
+    ) -> Result<Self::PermutationCheckSubClaim, PolyIOPErrors>;
+}
+
+/// A permutation subclaim consists of
+/// - A zero check IOP subclaim for Q(x) is 0, consists of the following:
+///  (See `build_qx` for definition of Q(x).)
+///   - the SubClaim from the SumCheck
+///   - the initial challenge r which is used to build eq(x, r) in ZeroCheck
+/// - A final query for `prod(1, ..., 1, 0) = 1`.
+// Note that this final query is in fact a constant that
+// is independent from the proof. So we should avoid
+// (de)serialize it.
+#[derive(Clone, Debug, Default, PartialEq)]
+pub struct PermutationCheckSubClaim<F: PrimeField, ZC: ZeroCheck<F>> {
+    // the SubClaim from the ZeroCheck
+    zero_check_sub_claim: ZC::ZeroCheckSubClaim,
+    // final query which consists of
+    // - the vector `(1, ..., 1, 0)`
+    // - the evaluation `1`
+    final_query: (Vec<F>, F),
+}
 
-    let res = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval);
-    end_timer!(start);
-    Ok(res)
+pub struct PermutationChallenge<F: PrimeField> {
+    alpha: Option<F>,
+    beta: F,
+    gamma: F,
 }
 
-/// Compute the following 5 polynomials
-/// - prod(x)
-/// - prod(0, x)
-/// - prod(1, x)
-/// - prod(x, 0)
-/// - prod(x, 1)
+/// A PermutationCheck is derived from ZeroCheck.
 ///
-/// where
-/// - `prod(0,x) := prod(0, x0, x1, …, xn)` which is the MLE over the
-/// evaluations of the following polynomial on the boolean hypercube {0,1}^n:
+/// A Permutation Check IOP takes the following steps:
 ///
-///  (w(x) + \beta s_id(x) + \gamma)/(w(x) + \beta s_perm(x) + \gamma)
+/// Inputs:
+/// - f(x)
+/// - g(x)
+/// - permutation s_perm(x)
 ///
-///   where
-///   - beta and gamma are challenges
-///   - w(x), s_id(x), s_perm(x) are mle-s
-///
-/// - `prod(1,x) := prod(x, 0) * prod(x, 1)`
-///
-/// Returns an error when the num_vars in w/s_id/s_perm does not match
-/// Cost: linear in N.
-#[allow(dead_code)]
-// TODO: remove
-fn compute_products<F: PrimeField>(
-    beta: &F,
-    gamma: &F,
-    w: &DenseMultilinearExtension<F>,
-    s_id: &DenseMultilinearExtension<F>,
-    s_perm: &DenseMultilinearExtension<F>,
-) -> Result<[DenseMultilinearExtension<F>; 5], PolyIOPErrors> {
-    let start = start_timer!(|| "compute all prod polynomial");
+/// Steps:
+/// 1. `generate_challenge` from current transcript (generate beta, gamma)
+/// 2. `compute_product` to build `prod(x)` etc. from f, g and s_perm
+/// 3. push a commitment of `prod(x)` to the transcript (done by the snark
+/// caller)
+/// 4. `update_challenge` with the updated transcript (generate alpha)
+/// 5. `prove` to generate the proof
+impl<F: PrimeField> PermutationCheck<F> for PolyIOP<F> {
+    /// A Permutation SubClaim is indeed a ZeroCheck SubClaim that consists of
+    /// - the SubClaim from the SumCheck
+    /// - the initial challenge r which is used to build eq(x, r)
+    type PermutationCheckSubClaim = PermutationCheckSubClaim<F, Self>;
 
-    let num_vars = w.num_vars;
+    type PermutationChallenge = PermutationChallenge<F>;
+
+    /// Initialize the system with a transcript
+    ///
+    /// This function is optional -- in the case where a PermutationCheck is
+    /// an building block for a more complex protocol, the transcript
+    /// may be initialized by this complex protocol, and passed to the
+    /// PermutationCheck prover/verifier.
+    fn init_transcript() -> Self::Transcript {
+        IOPTranscript::<F>::new(b"Initializing PermutationCheck transcript")
+    }
 
-    if num_vars != s_id.num_vars || num_vars != s_perm.num_vars {
-        return Err(PolyIOPErrors::InvalidParameters(
-            "num of variables do not match".to_string(),
-        ));
+    /// Step 1 of the IOP.
+    /// Generate challenge beta and gamma from a transcript.
+    fn generate_challenge(
+        transcript: &mut Self::Transcript,
+    ) -> Result<Self::PermutationChallenge, PolyIOPErrors> {
+        Ok(Self::PermutationChallenge {
+            beta: transcript.get_and_append_challenge(b"beta")?,
+            gamma: transcript.get_and_append_challenge(b"gamma")?,
+            alpha: None,
+        })
     }
-    // ===================================
-    // prod(0, x)
-    // ===================================
-    let prod_0x = compute_prod_0(beta, gamma, w, s_id, s_perm)?;
+
+    /// Step 4 of the IOP.
+    /// Update the challenge with alpha; returns an error if
+    /// alpha already exists.
+    fn update_challenge(
+        challenge: &mut Self::PermutationChallenge,
+        transcript: &mut Self::Transcript,
+        prod_x_binding: &F,
+    ) -> Result<(), PolyIOPErrors> {
+        if challenge.alpha.is_some() {
+            return Err(PolyIOPErrors::InvalidTranscript(
+                "alpha should not be sampled at the current stage".to_string(),
+            ));
+        }
+        transcript.append_field_element(b"prod(x)", prod_x_binding)?;
+        challenge.alpha = Some(transcript.get_and_append_challenge(b"alpha")?);
+        Ok(())
+    }
+
+    /// Step 2 of the IOP.
+    /// Compute the following 7 polynomials
+    /// - prod(x)
+    /// - prod(0, x)
+    /// - prod(1, x)
+    /// - prod(x, 0)
+    /// - prod(x, 1)
+    /// - numerator
+    /// - denominator
+    ///
+    /// where
+    /// - `prod(0,x) := prod(0, x0, x1, …, xn)` which is the MLE over the
+    /// evaluations of the following polynomial on the boolean hypercube
+    /// {0,1}^n:
+    ///
+    ///  (f(x) + \beta s_id(x) + \gamma)/(g(x) + \beta s_perm(x) + \gamma)
+    ///
+    ///   where
+    ///   - beta and gamma are challenges
+    ///   - f(x), g(x), s_id(x), s_perm(x) are mle-s
+    ///
+    /// - `prod(1,x) := prod(x, 0) * prod(x, 1)`
+    /// - numerator is the MLE for `f(x) + \beta s_id(x) + \gamma`
+    /// - denominator is the MLE for `g(x) + \beta s_perm(x) + \gamma`
+    ///
+    /// The caller needs to check num_vars matches in f/g/s_id/s_perm
+    /// Cost: linear in N.
+    fn compute_products(
+        challenge: &Self::PermutationChallenge,
+        fx: &DenseMultilinearExtension<F>,
+        gx: &DenseMultilinearExtension<F>,
+        s_perm: &DenseMultilinearExtension<F>,
+    ) -> Result<[DenseMultilinearExtension<F>; 7], PolyIOPErrors> {
+        let start = start_timer!(|| "compute all prod polynomial");
+
+        if challenge.alpha.is_some() {
+            return Err(PolyIOPErrors::InvalidTranscript(
+                "alpha is already sampled".to_string(),
+            ));
+        }
+
+        let num_vars = fx.num_vars;
+
+        // ===================================
+        // prod(0, x)
+        // ===================================
+        let (prod_0x, numerator, denominator) =
+            compute_prod_0(&challenge.beta, &challenge.gamma, fx, gx, s_perm)?;
+
+        // ===================================
+        // prod(1, x)
+        // ===================================
+        //
+        // `prod(1, x)` can be computed via recursing the following formula for 2^n-1
+        // times
+        //
+        // `prod(1, x_1, ..., x_n) :=
+        //      prod(x_1, x_2, ..., x_n, 0) * prod(x_1, x_2, ..., x_n, 1)`
+        //
+        // At any given step, the right hand side of the equation
+        // is available via either eval_0x or the current view of eval_1x
+        let eval_0x = &prod_0x.evaluations;
+        let mut eval_1x = vec![];
+        for x in 0..(1 << num_vars) - 1 {
+            // sign will decide if the evaluation should be looked up from eval_0x or
+            // eval_1x; x_zero_index is the index for the evaluation (x_2, ..., x_n,
+            // 0); x_one_index is the index for the evaluation (x_2, ..., x_n, 1);
+            let (x_zero_index, x_one_index, sign) = get_index(x, num_vars);
+            if !sign {
+                eval_1x.push(eval_0x[x_zero_index] * eval_0x[x_one_index]);
+            } else {
+                // sanity check: if we are trying to look up from the eval_1x table,
+                // then the target index must already exist
+                if x_zero_index >= eval_1x.len() || x_one_index >= eval_1x.len() {
+                    return Err(PolyIOPErrors::ShouldNotArrive);
+                }
+                eval_1x.push(eval_1x[x_zero_index] * eval_1x[x_one_index]);
+            }
+        }
+        // prod(1, 1, ..., 1) := 0
+        eval_1x.push(F::zero());
 
-    // ===================================
-    // prod(1, x)
-    // ===================================
-    //
-    // `prod(1, x)` can be computed via recursing the following formula for 2^n-1
-    // times
-    //
-    // `prod(1, x_1, ..., x_n) :=
-    //      prod(x_1, x_2, ..., x_n, 0) * prod(x_1, x_2, ..., x_n, 1)`
-    //
-    // At any given step, the right hand side of the equation
-    // is available via either eval_0x or the current view of eval_1x
-    let eval_0x = &prod_0x.evaluations;
-    let mut eval_1x = vec![];
-    for x in 0..(1 << num_vars) - 1 {
-        // sign will decide if the evaluation should be looked up from eval_0x or
-        // eval_1x; x_zero_index is the index for the evaluation (x_2, ..., x_n,
-        // 0); x_one_index is the index for the evaluation (x_2, ..., x_n, 1);
-        let (x_zero_index, x_one_index, sign) = get_index(x, num_vars);
-        if !sign {
-            eval_1x.push(eval_0x[x_zero_index] * eval_0x[x_one_index]);
-        } else {
-            // sanity check: if we are trying to look up from the eval_1x table,
-            // then the target index must already exist
-            if x_zero_index >= eval_1x.len() || x_one_index >= eval_1x.len() {
-                return Err(PolyIOPErrors::ShouldNotArrive);
+        // ===================================
+        // prod(x)
+        // ===================================
+        // prod(x)'s evaluation is indeed `e := [eval_0x[..], eval_1x[..]].concat()`
+        let eval = [eval_0x.as_slice(), eval_1x.as_slice()].concat();
+
+        // ===================================
+        // prod(x, 0) and prod(x, 1)
+        // ===================================
+        //
+        // now we compute eval_x0 and eval_x1
+        // eval_0x will be the odd coefficients of eval
+        // and eval_1x will be the even coefficients of eval
+        let mut eval_x0 = vec![];
+        let mut eval_x1 = vec![];
+        for (x, &prod_x) in eval.iter().enumerate() {
+            if x & 1 == 0 {
+                eval_x0.push(prod_x);
+            } else {
+                eval_x1.push(prod_x);
             }
-            eval_1x.push(eval_1x[x_zero_index] * eval_1x[x_one_index]);
         }
+
+        let prod_1x = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_1x);
+        let prod_x0 = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_x0);
+        let prod_x1 = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_x1);
+        let prod = DenseMultilinearExtension::from_evaluations_vec(num_vars + 1, eval);
+
+        end_timer!(start);
+        Ok([
+            prod,
+            prod_0x,
+            prod_1x,
+            prod_x0,
+            prod_x1,
+            numerator,
+            denominator,
+        ])
     }
-    // prod(1, 1, ..., 1) := 0
-    eval_1x.push(F::zero());
 
-    // ===================================
-    // prod(x)
-    // ===================================
-    // prod(x)'s evaluation is indeed `e := [eval_0x[..], eval_1x[..]].concat()`
-    let eval = [eval_0x.as_slice(), eval_1x.as_slice()].concat();
+    /// Step 5 of the IOP.
+    ///
+    /// Generate a proof to argue that an MLE g(x) is a permutation of
+    /// MLE f(x) over a permutation given by s_perm.
+    /// Inputs:
+    /// - 7 MLEs from `Self::compute_products(*, f, g, s_perm)`
+    /// - challenge: `Self::Challenge` that has been updated
+    /// - transcript: a transcript that is used to generate the challenges beta
+    ///   and gamma
+    /// Cost: O(N)
+    fn prove(
+        prod_x_and_aux_info: &[DenseMultilinearExtension<F>; 7],
+        challenge: &Self::PermutationChallenge,
+        transcript: &mut IOPTranscript<F>,
+    ) -> Result<Self::Proof, PolyIOPErrors> {
+        let alpha = match challenge.alpha {
+            Some(p) => p,
+            None => {
+                return Err(PolyIOPErrors::InvalidTranscript(
+                    "alpha is not sampled yet".to_string(),
+                ))
+            },
+        };
 
-    // ===================================
-    // prod(x, 0) and prod(x, 1)
-    // ===================================
-    //
-    // now we compute eval_x0 and eval_x1
-    // eval_0x will be the odd coefficients of eval
-    // and eval_1x will be the even coefficients of eval
-    let mut eval_x0 = vec![];
-    let mut eval_x1 = vec![];
-    for (x, &prod_x) in eval.iter().enumerate() {
-        if x & 1 == 0 {
-            eval_x0.push(prod_x);
-        } else {
-            eval_x1.push(prod_x);
-        }
+        let (proof, _q_x) = prove_internal(prod_x_and_aux_info, &alpha, transcript)?;
+        Ok(proof)
+    }
+
+    /// Verify that an MLE g(x) is a permutation of an
+    /// MLE f(x) over a permutation given by s_perm.
+    fn verify(
+        proof: &Self::Proof,
+        aux_info: &Self::VPAuxInfo,
+        transcript: &mut Self::Transcript,
+    ) -> Result<Self::PermutationCheckSubClaim, PolyIOPErrors> {
+        let start = start_timer!(|| "Permutation check verify");
+
+        // invoke the zero check on the iop_proof
+        let zero_check_sub_claim = <Self as ZeroCheck<F>>::verify(proof, aux_info, transcript)?;
+
+        let mut final_query = vec![F::one(); aux_info.num_variables];
+        final_query[aux_info.num_variables - 1] = F::zero();
+        let final_eval = F::one();
+
+        end_timer!(start);
+
+        Ok(PermutationCheckSubClaim {
+            zero_check_sub_claim,
+            final_query: (final_query, final_eval),
+        })
     }
+}
+
+/// Step 5 of the IOP.
+///
+/// Generate a proof to argue that an MLE g(x) is a permutation of
+/// MLE f(x) over a permutation given by s_perm.
+/// Inputs:
+/// - 7 MLEs from `Self::compute_products(*, f, g, s_perm)`
+/// - challenge: `Self::Challenge` that has been updated
+/// - transcript: a transcript that is used to generate the challenges beta and
+///   gamma
+///
+/// Returns proof and Q(x) for testing purpose.
+///
+/// Cost: O(N)
+fn prove_internal<F: PrimeField>(
+    prod_x_and_aux_info: &[DenseMultilinearExtension<F>; 7],
+    alpha: &F,
+    transcript: &mut IOPTranscript<F>,
+) -> Result<(IOPProof<F>, VirtualPolynomial<F>), PolyIOPErrors> {
+    let start = start_timer!(|| "Permutation check prove");
 
-    let prod_1x = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_1x);
-    let prod_x0 = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_x0);
-    let prod_x1 = DenseMultilinearExtension::from_evaluations_vec(num_vars, eval_x1);
-    let prod = DenseMultilinearExtension::from_evaluations_vec(num_vars + 1, eval);
+    // prods consists of the following:
+    // - prod(x)
+    // - prod(0, x)
+    // - prod(1, x)
+    // - prod(x, 0)
+    // - prod(x, 1)
+    // - numerator
+    // - denominator
+    let prod_0x = Rc::new(prod_x_and_aux_info[1].clone());
+    let prod_1x = Rc::new(prod_x_and_aux_info[2].clone());
+    let prod_x1 = Rc::new(prod_x_and_aux_info[3].clone());
+    let prod_x0 = Rc::new(prod_x_and_aux_info[4].clone());
+    let numerator = Rc::new(prod_x_and_aux_info[5].clone());
+    let denominator = Rc::new(prod_x_and_aux_info[6].clone());
+
+    // compute (g(x) + beta * s_perm(x) + gamma) * prod(0, x) * alpha
+    // which is prods[6] * prod[1] * alpha
+    let mut q_x = VirtualPolynomial::new_from_mle(denominator, F::one());
+    q_x.mul_by_mle(prod_0x, *alpha)?;
+
+    //   (g(x) + beta * s_perm(x) + gamma) * prod(0, x) * alpha
+    // - (f(x) + beta * s_id(x)   + gamma) * alpha
+    q_x.add_mle_list([numerator], -*alpha)?;
+
+    // Q(x) := prod(1,x) - prod(x, 0) * prod(x, 1)
+    //       + alpha * (
+    //             (g(x) + beta * s_perm(x) + gamma) * prod(0, x)
+    //           - (f(x) + beta * s_id(x)   + gamma))
+    q_x.add_mle_list([prod_x0, prod_x1], -F::one())?;
+    q_x.add_mle_list([prod_1x], F::one())?;
+    let iop_proof = <PolyIOP<F> as ZeroCheck<F>>::prove(&q_x, transcript)?;
 
     end_timer!(start);
-    Ok([prod, prod_0x, prod_1x, prod_x0, prod_x1])
+    Ok((iop_proof, q_x))
 }
 
 #[cfg(test)]
 mod test {
-    use super::*;
-    use crate::utils::bit_decompose;
+
+    use super::PermutationCheck;
+    use crate::{
+        errors::PolyIOPErrors,
+        perm_check::{prove_internal, util::identity_permutation_mle},
+        random_permutation_mle,
+        structs::IOPProof,
+        utils::bit_decompose,
+        virtual_poly::VPAuxInfo,
+        PolyIOP, VirtualPolynomial,
+    };
     use ark_bls12_381::Fr;
-    use ark_ff::UniformRand;
-    use ark_poly::MultilinearExtension;
+    use ark_ff::{PrimeField, Zero};
+    use ark_poly::{DenseMultilinearExtension, MultilinearExtension};
     use ark_std::test_rng;
+    use std::marker::PhantomData;
 
-    /// An MLE that represent an identity permutation: `f(index) \mapto index`
-    fn identity_permutation_mle<F: PrimeField>(num_vars: usize) -> DenseMultilinearExtension<F> {
-        let s_id_vec = (0..1u64 << num_vars).map(|index| F::from(index)).collect();
-        DenseMultilinearExtension::from_evaluations_vec(num_vars, s_id_vec)
+    fn mock_commit<F: PrimeField>(_f: &DenseMultilinearExtension<F>) -> F {
+        let mut rng = test_rng();
+        F::rand(&mut rng)
+    }
+
+    fn test_permutation_check_helper(
+        f: &DenseMultilinearExtension<Fr>,
+        g: &DenseMultilinearExtension<Fr>,
+        s_perm: &DenseMultilinearExtension<Fr>,
+    ) -> Result<(IOPProof<Fr>, VirtualPolynomial<Fr>), PolyIOPErrors> {
+        let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+        transcript.append_message(b"testing", b"initializing transcript for testing")?;
+
+        let mut challenge =
+            <PolyIOP<Fr> as PermutationCheck<Fr>>::generate_challenge(&mut transcript)?;
+
+        let prod_x_and_aux =
+            <PolyIOP<Fr> as PermutationCheck<Fr>>::compute_products(&challenge, f, g, s_perm)?;
+
+        let prod_x_binding = mock_commit(&prod_x_and_aux[0]);
+
+        <PolyIOP<Fr> as PermutationCheck<Fr>>::update_challenge(
+            &mut challenge,
+            &mut transcript,
+            &prod_x_binding,
+        )?;
+        let alpha = challenge.alpha.unwrap();
+
+        prove_internal(&prod_x_and_aux, &alpha, &mut transcript)
     }
 
-    #[test]
-    fn test_compute_prod_0() -> Result<(), PolyIOPErrors> {
+    fn test_permutation_check(nv: usize) -> Result<(), PolyIOPErrors> {
         let mut rng = test_rng();
 
-        for num_vars in 2..6 {
-            let w_vec: Vec<Fr> = (0..(1 << num_vars)).map(|_| Fr::rand(&mut rng)).collect();
-            let w = DenseMultilinearExtension::from_evaluations_vec(num_vars, w_vec);
+        let poly_info = VPAuxInfo {
+            max_degree: 2,
+            num_variables: nv,
+            phantom: PhantomData::default(),
+        };
 
-            let s_id = identity_permutation_mle::<Fr>(num_vars);
+        {
+            // good path: w is a permutation of w itself under the identify map
+            let w = DenseMultilinearExtension::rand(nv, &mut rng);
+
+            // s_perm is the identity map
+            let s_perm = identity_permutation_mle(nv);
 
-            let s_perm_vec: Vec<Fr> = (0..(1 << num_vars)).map(|_| Fr::rand(&mut rng)).collect();
-            let s_perm = DenseMultilinearExtension::from_evaluations_vec(num_vars, s_perm_vec);
+            let (proof, q_x) = test_permutation_check_helper(&w, &w, &s_perm)?;
 
-            let beta = Fr::rand(&mut rng);
-            let gamma = Fr::rand(&mut rng);
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+            let subclaim =
+                <PolyIOP<Fr> as PermutationCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?
+                    .zero_check_sub_claim;
+            assert_eq!(
+                q_x.evaluate(&subclaim.sum_check_sub_claim.point).unwrap(),
+                subclaim.sum_check_sub_claim.expected_evaluation,
+                "wrong subclaim"
+            );
 
-            let prod_0 = compute_prod_0(&beta, &gamma, &w, &s_id, &s_perm)?;
+            // test q_x is a 0 over boolean hypercube
+            for i in 0..1 << nv {
+                let bit_sequence = bit_decompose(i, nv);
+                let eval: Vec<Fr> = bit_sequence.iter().map(|x| Fr::from(*x as u64)).collect();
+                let res = q_x.evaluate(&eval)?;
+                assert!(res.is_zero())
+            }
+        }
 
-            for i in 0..1 << num_vars {
-                let r: Vec<Fr> = bit_decompose(i, num_vars)
-                    .iter()
-                    .map(|&x| Fr::from(x))
-                    .collect();
+        {
+            // bad path 1: w is a not permutation of w itself under a random map
+            let w = DenseMultilinearExtension::rand(nv, &mut rng);
 
-                let eval = prod_0.evaluate(&r).unwrap();
+            // s_perm is a random map
+            let s_perm = random_permutation_mle(nv, &mut rng);
 
-                let w_eval = w.evaluate(&r).unwrap();
-                let s_id_eval = s_id.evaluate(&r).unwrap();
-                let s_perm_eval = s_perm.evaluate(&r).unwrap();
-                let eval_rec =
-                    (w_eval + beta * s_id_eval + gamma) / (w_eval + beta * s_perm_eval + gamma);
+            let (proof, q_x) = test_permutation_check_helper(&w, &w, &s_perm)?;
 
-                assert_eq!(eval, eval_rec);
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+            if nv != 1 {
+                assert!(<PolyIOP<Fr> as PermutationCheck<Fr>>::verify(
+                    &proof,
+                    &poly_info,
+                    &mut transcript
+                )
+                .is_err());
+            } else {
+                // a trivial poly is always a permutation of itself, so the zero check should
+                // pass
+                let subclaim = <PolyIOP<Fr> as PermutationCheck<Fr>>::verify(
+                    &proof,
+                    &poly_info,
+                    &mut transcript,
+                )?
+                .zero_check_sub_claim;
+
+                // the evaluation should fail because a different s_perm is used for proof and
+                // for w |-> w mapping
+                assert_ne!(
+                    q_x.evaluate(&subclaim.sum_check_sub_claim.point).unwrap(),
+                    subclaim.sum_check_sub_claim.expected_evaluation,
+                    "wrong subclaim"
+                );
             }
         }
+
+        {
+            // bad path 2: f is a not permutation of g under a identity map
+            let f = DenseMultilinearExtension::rand(nv, &mut rng);
+            let g = DenseMultilinearExtension::rand(nv, &mut rng);
+
+            // s_perm is the identity map
+            let s_perm = identity_permutation_mle(nv);
+
+            let (proof, q_x) = test_permutation_check_helper(&f, &g, &s_perm)?;
+
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+            if nv != 1 {
+                assert!(<PolyIOP<Fr> as PermutationCheck<Fr>>::verify(
+                    &proof,
+                    &poly_info,
+                    &mut transcript
+                )
+                .is_err());
+            } else {
+                // a trivial poly is always a permutation of itself, so the zero check should
+                // pass
+                let subclaim = <PolyIOP<Fr> as PermutationCheck<Fr>>::verify(
+                    &proof,
+                    &poly_info,
+                    &mut transcript,
+                )?
+                .zero_check_sub_claim;
+
+                // the evaluation should fail because a different s_perm is used for proof and
+                // for f |-> g mapping
+                assert_ne!(
+                    q_x.evaluate(&subclaim.sum_check_sub_claim.point).unwrap(),
+                    subclaim.sum_check_sub_claim.expected_evaluation,
+                    "wrong subclaim"
+                );
+            }
+        }
+
+        Ok(())
+    }
+
+    #[test]
+    fn test_trivial_polynomial() -> Result<(), PolyIOPErrors> {
+        test_permutation_check(1)
+    }
+    #[test]
+    fn test_normal_polynomial() -> Result<(), PolyIOPErrors> {
+        test_permutation_check(5)
+    }
+
+    #[test]
+    fn zero_polynomial_should_error() -> Result<(), PolyIOPErrors> {
+        assert!(test_permutation_check(0).is_err());
         Ok(())
     }
 
@@ -208,19 +621,20 @@ fn test_compute_prod() -> Result<(), PolyIOPErrors> {
         let mut rng = test_rng();
 
         for num_vars in 2..6 {
-            let w_vec: Vec<Fr> = (0..(1 << num_vars)).map(|_| Fr::rand(&mut rng)).collect();
-            let w = DenseMultilinearExtension::from_evaluations_vec(num_vars, w_vec);
+            let f = DenseMultilinearExtension::rand(num_vars, &mut rng);
+            let g = DenseMultilinearExtension::rand(num_vars, &mut rng);
 
             let s_id = identity_permutation_mle::<Fr>(num_vars);
+            let s_perm = random_permutation_mle(num_vars, &mut rng);
 
-            let s_perm_vec: Vec<Fr> = (0..(1 << num_vars)).map(|_| Fr::rand(&mut rng)).collect();
-            let s_perm = DenseMultilinearExtension::from_evaluations_vec(num_vars, s_perm_vec);
+            let mut transcript = <PolyIOP<Fr> as PermutationCheck<Fr>>::init_transcript();
+            transcript.append_message(b"testing", b"initializing transcript for testing")?;
+            let challenge =
+                <PolyIOP<Fr> as PermutationCheck<Fr>>::generate_challenge(&mut transcript)?;
 
-            let beta = Fr::rand(&mut rng);
-            let gamma = Fr::rand(&mut rng);
-
-            // TODO: also test other 4 polynomials
-            let res = compute_products(&beta, &gamma, &w, &s_id, &s_perm)?;
+            let res = <PolyIOP<Fr> as PermutationCheck<Fr>>::compute_products(
+                &challenge, &f, &g, &s_perm,
+            )?;
 
             for i in 0..1 << num_vars {
                 let r: Vec<Fr> = bit_decompose(i, num_vars)
@@ -230,11 +644,12 @@ .collect();
 
                 let eval = res[1].evaluate(&r).unwrap();
 
-                let w_eval = w.evaluate(&r).unwrap();
+                let f_eval = f.evaluate(&r).unwrap();
+                let g_eval = g.evaluate(&r).unwrap();
                 let s_id_eval = s_id.evaluate(&r).unwrap();
                 let s_perm_eval = s_perm.evaluate(&r).unwrap();
-                let eval_rec =
-                    (w_eval + beta * s_id_eval + gamma) / (w_eval + beta * s_perm_eval + gamma);
+                let eval_rec = (f_eval + challenge.beta * s_id_eval + challenge.gamma)
+                    / (g_eval + challenge.beta * s_perm_eval + challenge.gamma);
 
                 assert_eq!(eval, eval_rec);
             }

@@ -0,0 +1,143 @@
+//! This module implements useful functions for the permutation check protocol.
+
+use crate::PolyIOPErrors;
+use ark_ff::PrimeField;
+use ark_poly::DenseMultilinearExtension;
+use ark_std::{end_timer, rand::RngCore, start_timer};
+
+/// Returns three MLEs:
+/// - prod(0,x)
+/// - numerator
+/// - denominator
+///
+/// where
+/// - `prod(0,x) := prod(0, x1, …, xn)` which is the MLE over the
+/// evaluations of the following polynomial on the boolean hypercube {0,1}^n:
+///
+///  (f(x) + \beta s_id(x) + \gamma)/(g(x) + \beta s_perm(x) + \gamma)
+///
+///  where
+///  - beta and gamma are challenges
+///  - f(x), g(x), s_id(x), s_perm(x) are mle-s
+///
+/// - numerator is the MLE for `f(x) + \beta s_id(x) + \gamma`
+/// - denominator is the MLE for `g(x) + \beta s_perm(x) + \gamma`
+///
+/// The caller needs to check num_vars matches in f/g/s_id/s_perm
+/// Cost: linear in N.
+#[allow(clippy::type_complexity)]
+pub(super) fn compute_prod_0<F: PrimeField>(
+    beta: &F,
+    gamma: &F,
+    fx: &DenseMultilinearExtension<F>,
+    gx: &DenseMultilinearExtension<F>,
+    s_perm: &DenseMultilinearExtension<F>,
+) -> Result<
+    (
+        DenseMultilinearExtension<F>,
+        DenseMultilinearExtension<F>,
+        DenseMultilinearExtension<F>,
+    ),
+    PolyIOPErrors,
+> {
+    let start = start_timer!(|| "compute prod(1,x)");
+
+    let num_vars = fx.num_vars;
+    let mut prod_0x_evals = vec![];
+    let mut numerator_evals = vec![];
+    let mut denominator_evals = vec![];
+
+    let s_id = identity_permutation_mle::<F>(num_vars);
+
+    for (&fi, (&gi, (&s_id_i, &s_perm_i))) in
+        fx.iter().zip(gx.iter().zip(s_id.iter().zip(s_perm.iter())))
+    {
+        let numerator = fi + *beta * s_id_i + gamma;
+        let denominator = gi + *beta * s_perm_i + gamma;
+
+        prod_0x_evals.push(numerator / denominator);
+        numerator_evals.push(numerator);
+        denominator_evals.push(denominator);
+    }
+
+    let prod_0x = DenseMultilinearExtension::from_evaluations_vec(num_vars, prod_0x_evals);
+    let numerator = DenseMultilinearExtension::from_evaluations_vec(num_vars, numerator_evals);
+    let denominator = DenseMultilinearExtension::from_evaluations_vec(num_vars, denominator_evals);
+
+    end_timer!(start);
+    Ok((prod_0x, numerator, denominator))
+}
+
+/// An MLE that represent an identity permutation: `f(index) \mapto index`
+pub fn identity_permutation_mle<F: PrimeField>(num_vars: usize) -> DenseMultilinearExtension<F> {
+    let s_id_vec = (0..1u64 << num_vars).map(F::from).collect();
+    DenseMultilinearExtension::from_evaluations_vec(num_vars, s_id_vec)
+}
+
+/// An MLE that represent a random permutation
+pub fn random_permutation_mle<F: PrimeField, R: RngCore>(
+    num_vars: usize,
+    rng: &mut R,
+) -> DenseMultilinearExtension<F> {
+    let len = 1u64 << num_vars;
+    let mut s_id_vec: Vec<F> = (0..len).map(F::from).collect();
+    let mut s_perm_vec = vec![];
+    for _ in 0..len {
+        let index = rng.next_u64() as usize % s_id_vec.len();
+        s_perm_vec.push(s_id_vec.remove(index));
+    }
+    DenseMultilinearExtension::from_evaluations_vec(num_vars, s_perm_vec)
+}
+
+#[cfg(test)]
+mod test {
+    use super::*;
+    use crate::utils::bit_decompose;
+    use ark_bls12_381::Fr;
+    use ark_ff::UniformRand;
+    use ark_poly::MultilinearExtension;
+    use ark_std::test_rng;
+
+    #[test]
+    fn test_compute_prod_0() -> Result<(), PolyIOPErrors> {
+        let mut rng = test_rng();
+
+        for num_vars in 2..6 {
+            let f = DenseMultilinearExtension::rand(num_vars, &mut rng);
+            let g = DenseMultilinearExtension::rand(num_vars, &mut rng);
+
+            let s_id = identity_permutation_mle::<Fr>(num_vars);
+            let s_perm = random_permutation_mle(num_vars, &mut rng);
+
+            let beta = Fr::rand(&mut rng);
+            let gamma = Fr::rand(&mut rng);
+
+            let (prod_0, numerator, denominator) = compute_prod_0(&beta, &gamma, &f, &g, &s_perm)?;
+
+            for i in 0..1 << num_vars {
+                let r: Vec<Fr> = bit_decompose(i, num_vars)
+                    .iter()
+                    .map(|&x| Fr::from(x))
+                    .collect();
+
+                let prod_0_eval = prod_0.evaluate(&r).unwrap();
+                let numerator_eval = numerator.evaluate(&r).unwrap();
+                let denominator_eval = denominator.evaluate(&r).unwrap();
+
+                let f_eval = f.evaluate(&r).unwrap();
+                let g_eval = g.evaluate(&r).unwrap();
+                let s_id_eval = s_id.evaluate(&r).unwrap();
+                let s_perm_eval = s_perm.evaluate(&r).unwrap();
+
+                let numerator_eval_rec = f_eval + beta * s_id_eval + gamma;
+                let denominator_eval_rec = g_eval + beta * s_perm_eval + gamma;
+                let prod_0_eval_rec = numerator_eval_rec / denominator_eval_rec;
+
+                assert_eq!(numerator_eval, numerator_eval_rec);
+                assert_eq!(denominator_eval, denominator_eval_rec);
+                assert_eq!(prod_0_eval, prod_0_eval_rec);
+            }
+        }
+        Ok(())
+    }
+}

@@ -3,16 +3,6 @@
 use crate::VirtualPolynomial;
 use ark_ff::PrimeField;
 
-/// A Subclaim is a claim generated by the verifier at the end of verification
-/// when it is convinced.
-pub struct SubClaim<F: PrimeField> {
-    /// the multi-dimensional point that this multilinear extension is evaluated
-    /// to
-    pub point: Vec<F>,
-    /// the expected evaluation
-    pub expected_evaluation: F,
-}
-
 /// An IOP proof is a collections of messages from prover to verifier at each
 /// round through the interactive protocol.
 #[derive(Clone, Debug, Default, PartialEq)]

@@ -2,12 +2,13 @@ //! This module implements the sum check protocol.
 
 use crate::{
     errors::PolyIOPErrors,
-    structs::{IOPProof, IOPProverState, IOPVerifierState, SubClaim},
+    structs::{IOPProof, IOPProverState, IOPVerifierState},
     transcript::IOPTranscript,
     virtual_poly::{VPAuxInfo, VirtualPolynomial},
     PolyIOP,
 };
 use ark_ff::PrimeField;
+use ark_poly::DenseMultilinearExtension;
 use ark_std::{end_timer, start_timer};
 
 mod prover;
@@ -15,11 +16,13 @@ mod verifier;
 
 /// Trait for doing sum check protocols.
 pub trait SumCheck<F: PrimeField> {
-    type Proof;
     type VirtualPolynomial;
     type VPAuxInfo;
-    type SubClaim;
+    type MultilinearExtension;
+
+    type Proof;
     type Transcript;
+    type SumCheckSubClaim;
 
     /// Extract sum from the proof
     fn extract_sum(proof: &Self::Proof) -> F;
@@ -46,7 +49,7 @@ sum: F,
         proof: &Self::Proof,
         aux_info: &Self::VPAuxInfo,
         transcript: &mut Self::Transcript,
-    ) -> Result<Self::SubClaim, PolyIOPErrors>;
+    ) -> Result<Self::SumCheckSubClaim, PolyIOPErrors>;
 }
 
 /// Trait for sum check protocol prover side APIs.
@@ -77,7 +80,7 @@ type VPAuxInfo;
     type ProverMessage;
     type Challenge;
     type Transcript;
-    type SubClaim;
+    type SumCheckSubClaim;
 
     /// Initialize the verifier's state.
     fn verifier_init(index_info: &Self::VPAuxInfo) -> Self;
@@ -105,14 +108,26 @@ /// Larger field size guarantees smaller soundness error.
     fn check_and_generate_subclaim(
         &self,
         asserted_sum: &F,
-    ) -> Result<Self::SubClaim, PolyIOPErrors>;
+    ) -> Result<Self::SumCheckSubClaim, PolyIOPErrors>;
+}
+
+/// A SumCheckSubClaim is a claim generated by the verifier at the end of
+/// verification when it is convinced.
+#[derive(Clone, Debug, Default, PartialEq)]
+pub struct SumCheckSubClaim<F: PrimeField> {
+    /// the multi-dimensional point that this multilinear extension is evaluated
+    /// to
+    pub point: Vec<F>,
+    /// the expected evaluation
+    pub expected_evaluation: F,
 }
 
 impl<F: PrimeField> SumCheck<F> for PolyIOP<F> {
     type Proof = IOPProof<F>;
     type VirtualPolynomial = VirtualPolynomial<F>;
     type VPAuxInfo = VPAuxInfo<F>;
-    type SubClaim = SubClaim<F>;
+    type MultilinearExtension = DenseMultilinearExtension<F>;
+    type SumCheckSubClaim = SumCheckSubClaim<F>;
     type Transcript = IOPTranscript<F>;
 
     /// Extract sum from the proof
@@ -170,7 +185,7 @@ claimed_sum: F,
         proof: &Self::Proof,
         aux_info: &Self::VPAuxInfo,
         transcript: &mut Self::Transcript,
-    ) -> Result<Self::SubClaim, PolyIOPErrors> {
+    ) -> Result<Self::SumCheckSubClaim, PolyIOPErrors> {
         let start = start_timer!(|| "sum check verify");
 
         transcript.append_aux_info(aux_info)?;

@@ -1,9 +1,9 @@
 //! Verifier subroutines for a SumCheck protocol.
 
-use super::SumCheckVerifier;
+use super::{SumCheckSubClaim, SumCheckVerifier};
 use crate::{
     errors::PolyIOPErrors,
-    structs::{IOPProverMessage, IOPVerifierState, SubClaim},
+    structs::{IOPProverMessage, IOPVerifierState},
     transcript::IOPTranscript,
     virtual_poly::VPAuxInfo,
 };
@@ -18,7 +18,7 @@ type VPAuxInfo = VPAuxInfo<F>;
     type ProverMessage = IOPProverMessage<F>;
     type Challenge = F;
     type Transcript = IOPTranscript<F>;
-    type SubClaim = SubClaim<F>;
+    type SumCheckSubClaim = SumCheckSubClaim<F>;
 
     /// Initialize the verifier's state.
     fn verifier_init(index_info: &Self::VPAuxInfo) -> Self {
@@ -91,7 +91,7 @@ /// Larger field size guarantees smaller soundness error.
     fn check_and_generate_subclaim(
         &self,
         asserted_sum: &F,
-    ) -> Result<Self::SubClaim, PolyIOPErrors> {
+    ) -> Result<Self::SumCheckSubClaim, PolyIOPErrors> {
         let start = start_timer!(|| "sum check check and generate subclaim");
         if !self.finished {
             return Err(PolyIOPErrors::InvalidVerifier(
@@ -161,7 +161,7 @@ ));
             }
         }
         end_timer!(start);
-        Ok(SubClaim {
+        Ok(SumCheckSubClaim {
             point: self.challenges.clone(),
             // the last expected value (not checked within this function) will be included in the
             // subclaim
@@ -221,7 +221,7 @@ //  - for len >  33 with BigInt
     if p_i.len() <= 20 {
         let last_denominator = F::from(u64_factorial(len - 1));
         let mut ratio_numerator = 1i64;
-        let mut ratio_enumerator = 1u64;
+        let mut ratio_denominator = 1u64;
 
         for i in (0..len).rev() {
             let ratio_numerator_f = if ratio_numerator < 0 {
@@ -230,19 +230,19 @@ } else {
                 F::from(ratio_numerator as u64)
             };
 
-            res += p_i[i] * prod * F::from(ratio_enumerator)
+            res += p_i[i] * prod * F::from(ratio_denominator)
                 / (last_denominator * ratio_numerator_f * evals[i]);
 
             // compute denom for the next step is current_denom * (len-i)/i
             if i != 0 {
                 ratio_numerator *= -(len as i64 - i as i64);
-                ratio_enumerator *= i as u64;
+                ratio_denominator *= i as u64;
             }
         }
     } else if p_i.len() <= 33 {
         let last_denominator = F::from(u128_factorial(len - 1));
         let mut ratio_numerator = 1i128;
-        let mut ratio_enumerator = 1u128;
+        let mut ratio_denominator = 1u128;
 
         for i in (0..len).rev() {
             let ratio_numerator_f = if ratio_numerator < 0 {
@@ -251,13 +251,13 @@ } else {
                 F::from(ratio_numerator as u128)
             };
 
-            res += p_i[i] * prod * F::from(ratio_enumerator)
+            res += p_i[i] * prod * F::from(ratio_denominator)
                 / (last_denominator * ratio_numerator_f * evals[i]);
 
             // compute denom for the next step is current_denom * (len-i)/i
             if i != 0 {
                 ratio_numerator *= -(len as i128 - i as i128);
-                ratio_enumerator *= i as u128;
+                ratio_denominator *= i as u128;
             }
         }
     } else {

@@ -23,7 +23,7 @@ /// * Coefficient of ith product c_i = `polynomial.products[i].0`
 ///
 /// The resulting polynomial is
 ///
-/// $$\sum_{i=0}^{n} c_i \cdot \prod_{j=0}^{m_i} P_{ij} $$
+/// $$ \sum_{i=0}^{n} c_i \cdot \prod_{j=0}^{m_i} P_{ij} $$
 ///
 /// Example:
 ///  f = c0 * f0 * f1 * f2 + c1 * f3 * f4
@@ -60,7 +60,7 @@ /// number of variables of the polynomial
     pub num_variables: usize,
     /// Associated field
     #[doc(hidden)]
-    pub(crate) phantom: PhantomData<F>,
+    pub phantom: PhantomData<F>,
 }
 
 impl<F: PrimeField> Add for &VirtualPolynomial<F> {

@@ -1,22 +1,23 @@
 //! Main module for the ZeroCheck protocol.
 
-use crate::{
-    errors::PolyIOPErrors,
-    structs::{IOPProof, SubClaim},
-    sum_check::SumCheck,
-    transcript::IOPTranscript,
-    virtual_poly::{VPAuxInfo, VirtualPolynomial},
-    PolyIOP,
-};
+use crate::{errors::PolyIOPErrors, sum_check::SumCheck, transcript::IOPTranscript, PolyIOP};
 use ark_ff::PrimeField;
 use ark_std::{end_timer, start_timer};
 
-pub trait ZeroCheck<F: PrimeField> {
-    type Proof;
-    type VirtualPolynomial;
-    type VPAuxInfo;
-    type SubClaim;
-    type Transcript;
+/// A zero check IOP subclaim for \hat f(x) is 0, consists of the following:
+///   - the SubClaim from the SumCheck
+///   - the initial challenge r which is used to build eq(x, r) in ZeroCheck
+#[derive(Clone, Debug, Default, PartialEq)]
+pub struct ZeroCheckSubClaim<F: PrimeField, SC: SumCheck<F>> {
+    // the SubClaim from the SumCheck
+    pub sum_check_sub_claim: SC::SumCheckSubClaim,
+    // the initial challenge r which is used to build eq(x, r)
+    pub init_challenge: Vec<F>,
+}
+
+/// A ZeroCheck is derived from SumCheck.
+pub trait ZeroCheck<F: PrimeField>: SumCheck<F> {
+    type ZeroCheckSubClaim;
 
     /// Initialize the system with a transcript
     ///
@@ -38,19 +39,14 @@ fn verify(
         proof: &Self::Proof,
         aux_info: &Self::VPAuxInfo,
         transcript: &mut Self::Transcript,
-    ) -> Result<Self::SubClaim, PolyIOPErrors>;
+    ) -> Result<Self::ZeroCheckSubClaim, PolyIOPErrors>;
 }
 
 impl<F: PrimeField> ZeroCheck<F> for PolyIOP<F> {
-    type Proof = IOPProof<F>;
-    type VirtualPolynomial = VirtualPolynomial<F>;
-    type VPAuxInfo = VPAuxInfo<F>;
-
     /// A ZeroCheck SubClaim consists of
-    /// - the SubClaim from the ZeroCheck
+    /// - the SubClaim from the SumCheck
     /// - the initial challenge r which is used to build eq(x, r)
-    type SubClaim = (SubClaim<F>, Vec<F>);
-    type Transcript = IOPTranscript<F>;
+    type ZeroCheckSubClaim = ZeroCheckSubClaim<F, Self>;
 
     /// Initialize the system with a transcript
     ///
@@ -98,7 +94,7 @@ fn verify(
         proof: &Self::Proof,
         fx_aux_info: &Self::VPAuxInfo,
         transcript: &mut Self::Transcript,
-    ) -> Result<Self::SubClaim, PolyIOPErrors> {
+    ) -> Result<Self::ZeroCheckSubClaim, PolyIOPErrors> {
         let start = start_timer!(|| "zero check verify");
 
         // check that the sum is zero
@@ -120,7 +116,10 @@ let subclaim =
             <Self as SumCheck<F>>::verify(F::zero(), proof, &hat_fx_aux_info, transcript)?;
 
         end_timer!(start);
-        Ok((subclaim, r))
+        Ok(ZeroCheckSubClaim {
+            sum_check_sub_claim: subclaim,
+            init_challenge: r,
+        })
     }
 }
 
@@ -152,7 +151,8 @@ let poly_info = poly.aux_info.clone();
             let mut transcript = <PolyIOP<Fr> as ZeroCheck<Fr>>::init_transcript();
             transcript.append_message(b"testing", b"initializing transcript for testing")?;
             let subclaim =
-                <PolyIOP<Fr> as ZeroCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?.0;
+                <PolyIOP<Fr> as ZeroCheck<Fr>>::verify(&proof, &poly_info, &mut transcript)?
+                    .sum_check_sub_claim;
             assert!(
                 poly.evaluate(&subclaim.point)? == subclaim.expected_evaluation,
                 "wrong subclaim"