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