docs: sumcheck documentation

barretenberg/cpp/docs/src/honk.md

@@ -0,0 +1,17 @@
+# Honk
+
+Honk is a sumcheck-based SNARK protocol which is similar to HyperPlonk [HyperPlonk]. A theory paper, based on the thesis [H], is forthcoming. This spec described what is currently implemented in Barretenberg.
+
+The variants of Honk that we build will be heavily optimized. As a warm-up, we describe a basic, unoptimized version of the protocol [here](honk-outline.md).
+
+# Preliminaries
+
+# Flavors
+
+# Prover's algorithm
+This is outlined in `proof_system::honk::UltraProver::construct_proof()`:
+ \snippet cpp/src/barretenberg/ultra_honk/ultra_prover.cpp ConstructProof
+
+## Sumcheck
+Sumcheck protocol is a proof system allowing to efficiently prove claims about the sums of values of multilinear polynomials in \f$ d \f$ variables over the Boolean hypercube \f$ \{0,1\}^d \f$ as well as more elaborate relations between such polynomials. Our implementation of Sumcheck including is described [here](sumcheck-outline.md).
+# Verifier's algorithm

barretenberg/cpp/docs/src/sumcheck-outline.md

@@ -0,0 +1,3 @@
+# Sumcheck Implementation
+
+A template for Sumcheck outline. To be updated when we implement ZK. 

barretenberg/cpp/src/barretenberg/polynomials/pow.hpp

@@ -7,109 +7,67 @@
 #include <vector>
 namespace bb {
 
-/**
- * @brief Succinct representation of the `pow` polynomial that can be partially evaluated variable-by-variable.
- * pow_{\vec{β}}(X_0,X_1,..,X_{d-1}) = \prod_{0≤l<d} ((1−X_l) + X_l⋅β_l) for a vector {β_0,...,β_{d-1}} used in
-sumcheck.
- *
- * @details Let
- * - d be the number of variables
- * - l be the current Sumcheck round ( l ∈ {0, …, d-1} )
- * - u_0, ..., u_{l-1} the challenges sent by the verifier in rounds 0 to l-1.
- *
- * - pow_\vec{β}(X) = ∏_{0≤l<d} ((1−X_l) + X_l⋅β_l) is the multilinear polynomial whose evaluation at the i-th index
- *   of the full hypercube equals pow_\vec{β}(i) = ∏_{j ∈ bin(i), j = 1} β_j. More explicitly, the product contains the
-elements of \vec{β} whose
- *  indexes j represent bits set to 1 in the binary representation of i.
- *
- *  We can also see it as the multi-linear extension of the vector \vec{β}.
- *
- * - At round l, we iterate over a boolean hypercube of dimension (d-l).
- *   Let i = ∑_{l<k<d} i_k ⋅ 2^{k-(l+1)} be the index of the current edge over which we are evaluating the relation.
- *   We define the edge univariate for the pow polynomial as powˡᵢ( X_l ) and it can be represented as:
- *
- *   powˡᵢ( X_{l} ) = pow( u_{0}, ..., u_{l-1},
- *                         X_{l},
- *                         i_{l+1}, ..., i_{d-1})
- *                  = ∏_{0≤k<l} ( (1-u_k) + u_k⋅β_k )
- *                             ⋅( (1−X_l) + X_l⋅β_l )
- *                    ∏_{l<k<d} ( (1-i_k) + i_k⋅β_k )
- *
- * Product ∏_{0≤k<l} ( (1-u_k) + u_k⋅β_k ) gets updated at each round of sumcheck and represents the
- * partial_evaluation_result in the implementation. This is the pow polynomial, partially evaluated in the first l-1
- * variables as (X_{0}, ..., X_{l-1}) = (u_{0}, ...,u_{l-1}).
- *
- * As we iterate over the other points in the boolean hypercube (i_{l+1}, ..., i_{d-1}) ∈ {0,1}^{d-l-1},
- * the subproducts
- * ∏_{l<k<d} ( (1-i_k) + i_k⋅β_k ) represent the terms of pow(\vec{β}) that do not contain β_0,...,β_l. These appear in
- * the set {pow_\vec{β}(i)| i =0,..,2^{d}-1} at indices 2^{l+1} * p where p ≥ 1 and 2^{l+1} * p < 2^d
- *
- *
- * - Sˡᵢ( X_l ) is the univariate of the full relation at edge pair i
- * i.e. it is the alpha-linear-combination of the relations evaluated in the edge at index i.
- * If our composed Sumcheck relation is a multi-variate polynomial P(X_{0}, ..., X_{d-1}),
- * Then Sˡᵢ( X_l ) = P( u_{0}, ..., u_{l-1}, X_{l}, i_{l+1}, ..., i_{d-1} ).
- * The l-th univariate would then be Sˡ( X_l ) = ∑_{ 0 ≤ i < 2^{d-l-1} }  Sˡᵢ( X_l ) .
- *
- * We want to check that P(i)=0 for all i ∈ {0,1}^d. So we use Sumcheck over the polynomial
- * P'(X) = pow(X)⋅P(X).
- * The claimed sum is 0 and is equal to ∑_{i ∈ {0,1}^d} pow(i)⋅P(i).
- * If the Sumcheck passes, then with it must hold with high-probability that all P(i) are 0.
- *
- * Init:
- * - σ_0 <-- 0 // Claimed Sumcheck sum
- * - c_0  <-- 1 // Partial evaluation constant, before any evaluation
- *
- * Round 0≤l<d-1:
- * - σ_{ l } =?= S'ˡ(0) + S'ˡ(1) = Tˡ(0) + ζ_{l}⋅Tˡ(1)  // Check partial sum
- * - σ_{l+1} <-- ( (1−u_{l}) + u_{l}⋅β_{l} )⋅Tʲ(u_{l})  // Compute next partial sum
- * - c_{l+1} <-- ( (1−u_{l}) + u_{l}⋅β_{l} )⋅c_{l}      // Partially evaluate pow in u_{l}
- *
- * Final round l=d-1:
- * - σ_{d-1} =?= S'ᵈ⁻¹(0) + S'ᵈ⁻¹(1) = Tᵈ⁻¹(0) + β_{d-1}⋅Tᵈ⁻¹(1)    // Check partial sum
- * - σ_{ d } <-- ( (1−u_{d-1}) + u_{d-1}⋅ζ_{0} )⋅Tᵈ⁻¹(u_{d-1})      // Compute purported evaluation of P'(u)
- * - c_{ d } <-- ∏_{0≤l<d} ( (1-u_{l}) + u_{l}⋅β_{l} )
- *             = pow(u_{0}, ..., u_{d-1})                           // Full evaluation of pow
- * - σ_{ d } =?= c_{d}⋅P(u_{0}, ..., u_{d-1})                       // Compare against real evaluation of P'(u)
- */
-
 template <typename FF> struct PowPolynomial {
 
-    // \vec{β} = {β_0, β_1,.., β_{d-1}}
+    /**
+     * @brief The challenges \f$(\beta_0,\ldots, \beta_{d-1}) \f$
+     *
+     */
     std::vector<FF> betas;
 
-    // The values of pow_\vec{β}(i) for i=0,..,2^d - 1 for the given \vec{β}
+    /**
+     * @brief The consecutive evaluations \f$ pow_{\ell}(\beta) =  pow_{\beta}(\vec \ell) \f$ for \f$\vec \ell\f$
+     * identified with the integers \f$\ell = 0,\ldots, 2^d-1\f$
+     *
+     */
     std::vector<FF> pow_betas;
-
-    // At round l of sumcheck this will point to the l-th element in \vec{β}
+    /**
+     * @brief In Round \f$ i\f$ of Sumcheck, it points to the \f$ i \f$-th element in \f$ \vec \beta \f$
+     *
+     */
     size_t current_element_idx = 0;
-
-    // At round l of sumcheck, the periodicity represents the fixed interval at which elements not containing either of
-    // β_0,..,β_l appear in pow_betas
+    /**
+     * @brief In Round \f$ i\f$ of Sumcheck, the periodicity equals to \f$ 2^{i+1}\f$ and represents the fixed interval
+     * at which elements not containing either of \f$ (\beta_0,\ldots ,β_i)\f$ appear in #pow_betas.
+     *
+     */
     size_t periodicity = 2;
-
-    // The value c_l obtained by partially evaluating one variable in the power polynomial at each round. At the
-    // end of round l in the sumcheck protocol, variable X_l is replaced by a verifier challenge u_l. The partial
-    // evaluation result is updated to represent pow(u_0,.., u_{l-1}) = \prod_{0 ≤ k < l} ( (1-u_k) + u_k⋅β_k).
+    /**
+     * @brief  The value \f$c_i\f$ obtained by partially evaluating one variable in the power polynomial at each round.
+     * At the end of Round \f$ i \f$ in the sumcheck protocol, variable \f$X_i\f$ is replaced by the challenge \f$u_i
+     * \f$. The partial evaluation result is updated to represent \f$ pow_{\beta}(u_0,.., u_{i}) = \prod_{k=0}^{i} (
+     * (1-u_k) + u_k\cdot \beta_k) \f$.
+     *
+     */
     FF partial_evaluation_result = FF(1);
 
     explicit PowPolynomial(const std::vector<FF>& betas)
         : betas(betas)
     {}
-
+    /**
+     * @brief Retruns the element in #pow_betas at place #idx.
+     *
+     * @param idx
+     * @return FF const&
+     */
     FF const& operator[](size_t idx) const { return pow_betas[idx]; }
-
+    /**
+     * @brief Computes the component  at index #current_element_idx in #betas.
+     *
+     * @return FF
+     */
     FF current_element() const { return betas[current_element_idx]; }
 
     /**
-     * @brief Evaluate the monomial ((1−X_l) + X_l⋅β_l) in the challenge point X_l=u_l.
+     * @brief Evaluate  \f$ ((1−X_{i}) + X_{i}\cdot \beta_{i})\f$ at the challenge point \f$ X_{i}=u_{i} \f$.
      */
     FF univariate_eval(FF challenge) const { return (FF(1) + (challenge * (betas[current_element_idx] - FF(1)))); };
 
     /**
-     * @brief Parially evaluate the pow polynomial in X_l and updating the value c_l -> c_{l+1}.
-     *
-     * @param challenge l-th verifier challenge u_l
+     * @brief Partially evaluate the \f$pow_{\beta} \f$-polynomial at the new challenge and update \f$ c_i \f$
+     * @details Update the constant \f$c_{i} \to c_{i+1} \f$ multiplying it by \f$pow_{\beta}\f$'s factor \f$\left(
+     * (1-X_i) + X_i\cdot \beta_i\right)\vert_{X_i = u_i}\f$ computed by \ref univariate_eval.
+     * @param challenge \f$ i \f$-th verifier challenge \f$ u_{i}\f$
      */
     void partially_evaluate(FF challenge)
     {
@@ -120,7 +78,8 @@ template <typename FF> struct PowPolynomial {
     }
 
     /**
-     * @brief Given \vec{β} = {β_0,...,β_{d-1}} compute pow_\vec{β}(i) for i=0,...,2^{d}-1
+     * @brief Given \f$ \vec\beta = (\beta_0,...,\beta_{d-1})\f$ compute \f$ pow_{\ell}(\vec \beta) = pow_{\beta}(\vec
+     * \ell)\f$ for \f$ \ell =0,\ldots,2^{d}-1\f$.
      *
      */
     BB_PROFILE void compute_values()
@@ -158,4 +117,68 @@ template <typename FF> struct PowPolynomial {
         });
     }
 };
+/**<
+ * @struct PowPolynomial
+ * @brief Implementation of the methods for the \f$pow_{\ell}\f$-polynomials used in ProtoGalaxy and
+\f$pow_{\beta}\f$-polynomials used in Sumcheck.
+ *
+ * @details
+ * ## PowPolynomial in Protogalaxy
+ * For \f$0\leq \ell \leq 2^d-1 \f$, the \f$pow_{\ell} \f$-polynomials used in Protogalaxy is a multilinear polynomial
+defined by the formula
+ * \f{align} pow_{\ell}(X_0,\ldots, X_{d-1})
+          =    \prod_{k=0}^{d-1} ( ( 1-\ell_k ) + \ell_k \cdot X_k )
+          =      \prod_{k=0}^{d-1} X_{k}^{ \ell_k }
+     \f}
+ *where \f$(\ell_0,\ldots, \ell_{d-1})\f$ is the binary representation of \f$\ell \f$.
+ *
+ *
+  ## Pow-contributions to Round Univariates in Sumcheck
+ * For a fixed \f$ \vec \beta \in \mathbb{F}^d\f$, the map \f$ \ell \mapsto pow_{\ell} (\vec \beta)\f$ defines a
+multi-linear polynomial \f{align}{ pow_{\beta} (X_0,\ldots, X_{d-1}) = \prod_{k=0}^{d-1} (1- X_k + X_k \cdot \beta_k)
+ \f}
+such that \f$ pow_{\beta} (\vec \ell) = pow_{\ell} (\vec \beta) \f$ for any \f$0\leq \ell \leq 2^d-1 \f$ and any vector
+\f$(\beta_0,\ldots, \beta_{d-1})  \in \mathbb{F} ^d\f$.
+
+ * Let \f$ i \f$ be the current Sumcheck round, \f$ i \in \{0, …, d-1\}\f$ and \f$ u_{0}, ..., u_{i-1} \f$ be the
+challenges computed in Rounds \f$ 0 \f$ to \f$ i-1\f$.
+ *
+ * In Round \f$ i \f$, we iterate over the points \f$ (\ell_{i+1}, \ldots, \ell_{d-1}) \in
+\{0,1\}^{d-1-i}\f$. Define the edge univariate for the \f$ pow_\beta \f$ polynomial as \f$ pow^{i}_{\beta} (X_i, \vec
+\ell )\f$ and it can be represented as:
+ *   \f{align}{  pow_{\beta}^i =   pow_{\beta} ( u_{0}, ..., u_{i-1}, X_i, \ell_{i+1}, \ldots, \ell_{d-1})            =
+c_i \cdot ( (1−X_i) + X_i \cdot \beta_i ) \cdot \beta_{i+1}^{\ell_{i+1}}\cdot \cdots \cdot \beta_{d-1}^{\ell_{d-1}}, \f}
+ where \f$ c_i = \prod_{k=0}^{i-1} (1- u_k + u_k \cdot \beta_k) \f$.
+
+ ### Computing Sumcheck Round Univariates
+ * We identify \f$ \vec \ell = (\ell_{i+1}, \ldots, \ell_{d-1}) \in \{0,1\}^{d-1 - i}\f$ with the binary representation
+of the integer \f$ \ell \in \{0,\ldots, 2^{d-1-i}-1 \}\f$.
+ *
+ * Set
+  \f{align}{S^i_{\ell}( X_i ) = F( u_{0}, ..., u_{i-1}, X_{i},  \vec \ell ), \f}
+ * i.e. \f$ S^{i}_{\ell}( X_i ) \f$  is the univariate of the full relation \f$ F \f$ defined by its partial evaluation
+at \f$(u_0,\ldots,u_{i-1},  \ell_{i+1},\ldots, \ell_{d-1}) \f$
+ * which  is an alpha-linear-combination of the sub-relations evaluated at this point.
+ *
+ * In Round \f$i\f$, the prover \ref bb::SumcheckProverRound< Flavor >::compute_univariate "computes the univariate
+polynomial" for the relation defined by \f$ \tilde{F} (X_0,\ldots, X_{d-1}) = pow_{\beta}(X_0,\ldots, X_{d-1}) \cdot
+F\f$, namely
+ * \f{align}{
+    \tilde{S}^{i}(X_i) = \sum_{ \ell = 0} ^{2^{d-i-1}-1}  pow^i_\beta ( X_i, \ell_{i+1}, \ldots, \ell_{d-1} )
+S^i_{\ell}( X_i )
+ *        =  c_i \cdot ( (1−X_i) + X_i\cdot \beta_i )  \cdot \sum_{ \ell = 0} ^{2^{d-i-1}-1} \beta_{i+1}^{\ell_{i+1}}
+\cdot \ldots \cdot \beta_{d-1}^{\ell_{d-1}} \cdot S^i_{\ell}( X_i ) \f}
+ *
+ * Define
+ \f{align} T^{i}( X_i ) =  \sum_{\ell = 0}^{2^{d-i-1}-1} \beta_{i+1}^{\ell_{i+1}} \cdot \ldots \cdot
+\beta_{d-1}^{\ell_{d-1}} \cdot S^{i}_{\ell}( X_i ) \f} then \f$ \deg_{X_i} (T^i) \leq \deg_{X_i} S^i \f$.
+ ### Main Features of PowPolynomial Class:
+ - The factor \f$ c_i \f$ is contained in #partial_evaluation_result and updated by \ref partially_evaluate.
+ - The challenges \f$(\beta_0,\ldots, \beta_{d-1}) \f$ are recorded in #betas.
+ - The consecutive evaluations \f$ pow_{\ell}(\vec \beta) = pow_{\beta}(\vec \ell) \f$ for \f$\vec \ell\f$ identified
+with the integers \f$\ell = 0,\ldots, 2^d-1\f$ represented in binary are pre-computed by \ref compute_values and stored
+in #pow_betas.
+ *
+ */
+
 } // namespace bb