1//! Main module for the Permutation Check protocol
  2
  3use crate::{errors::PolyIOPErrors, transcript::IOPTranscript, VirtualPolynomial, ZeroCheck};
  4use ark_ff::PrimeField;
  5use ark_poly::DenseMultilinearExtension;
  6
  7/// A ProductCheck is derived from ZeroCheck.
  8///
  9/// A ProductCheck IOP takes the following steps:
 10///
 11/// Inputs:
 12/// - f(x)
 13///
 14/// Prover steps:
 15/// 1. `compute_product_poly` to build `prod(x0, ..., x_n)` from virtual
 16/// polynomial f
 17/// 2. push commitments of `f(x)`, `prod(x)` to the transcript
 18/// (done by the snark caller)
 19/// 3. `generate_challenge` from current transcript (generate alpha)
 20/// 4. `prove` to generate the zerocheck proof for the virtual polynomial
 21///     prod(1, x) - prod(x, 0) * prod(x, 1) + alpha * (f(x) - prod(0, x))
 22///
 23/// Verifier steps:
 24/// 1. Extract commitments of `f(x)`, `prod(x)` from the proof, push them to the
 25/// transcript (done by the snark caller)
 26/// 2. `generate_challenge` from current transcript (generate alpha)
 27/// 3. `verify` to verify the zerocheck proof and generate the subclaim for
 28/// polynomial evaluations
 29pub trait ProductCheck<F: PrimeField>: ZeroCheck<F> {
 30    type ProductCheckSubClaim;
 31    type ProductCheckChallenge;
 32
 33    /// Initialize the system with a transcript
 34    ///
 35    /// This function is optional -- in the case where a ProductCheck is
 36    /// an building block for a more complex protocol, the transcript
 37    /// may be initialized by this complex protocol, and passed to the
 38    /// ProductCheck prover/verifier.
 39    fn init_transcript() -> Self::Transcript;
 40
 41    /// Generate random challenge `alpha` from a transcript.
 42    fn generate_challenge(
 43        transcript: &mut Self::Transcript,
 44    ) -> Result<Self::ProductCheckChallenge, PolyIOPErrors>;
 45
 46    /// Compute the product polynomial `prod(x)` where
 47    ///
 48    ///  - `prod(0,x) := prod(0, x1, …, xn)` is the MLE over the
 49    /// evaluations of `f(x)` on the boolean hypercube {0,1}^n
 50    ///
 51    /// - `prod(1,x)` is a MLE over the evaluations of `prod(x, 0) * prod(x, 1)`
 52    /// on the boolean hypercube {0,1}^n
 53    ///
 54    /// The caller needs to check num_vars matches in f
 55    /// Cost: linear in N.
 56    fn compute_product_poly(
 57        fx: &VirtualPolynomial<F>,
 58    ) -> Result<DenseMultilinearExtension<F>, PolyIOPErrors>;
 59
 60    /// Initialize the prover to argue that for a virtual polynomial f(x),
 61    /// it holds that `s = \prod_{x \in {0,1}^n} f(x)`
 62    ///
 63    /// Inputs:
 64    /// - fx: the virtual polynomial
 65    /// - prod_x: the product polynomial
 66    /// - transcript: a transcript that is used to generate the challenges alpha
 67    /// - claimed_product: the claimed product value
 68    ///
 69    /// Cost: O(N)
 70    fn prove(
 71        fx: &VirtualPolynomial<F>,
 72        prod_x: &DenseMultilinearExtension<F>,
 73        transcript: &mut IOPTranscript<F>,
 74        claimed_product: F,
 75    ) -> Result<Self::Proof, PolyIOPErrors>;
 76
 77    /// Verify that for a witness virtual polynomial f(x),
 78    /// it holds that `s = \prod_{x \in {0,1}^n} f(x)`
 79    fn verify(
 80        proof: &Self::Proof,
 81        aux_info: &Self::VPAuxInfo,
 82        transcript: &mut Self::Transcript,
 83        claimed_product: F,
 84    ) -> Result<Self::ProductCheckSubClaim, PolyIOPErrors>;
 85}
 86
 87/// A product check subclaim consists of
 88/// - A zero check IOP subclaim for
 89/// `Q(x) = prod(1, x) - prod(x, 0) * prod(x, 1) + alpha * (f(x) - prod(0, x)`
 90/// is 0, consists of the following:
 91///   - the SubClaim from the SumCheck
 92///   - the initial challenge r which is used to build eq(x, r) in ZeroCheck
 93/// - A final query for `prod(1, ..., 1, 0) = claimed_product`.
 94// Note that this final query is in fact a constant that
 95// is independent from the proof. So we should avoid
 96// (de)serialize it.
 97#[derive(Clone, Debug, Default, PartialEq)]
 98pub struct ProductCheckSubClaim<F: PrimeField, ZC: ZeroCheck<F>> {
 99    // the SubClaim from the ZeroCheck
100    zero_check_sub_claim: ZC::ZeroCheckSubClaim,
101    // final query which consists of
102    // - the vector `(1, ..., 1, 0)`
103    // - the evaluation `claimed_product`
104    final_query: (Vec<F>, F),
105}
106
107/// The random challenges in a product check protocol
108#[allow(dead_code)]
109pub struct ProductCheckChallenge<F: PrimeField> {
110    alpha: F,
111}
112
113#[cfg(test)]
114mod test {}