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