Merge branch 'logup-gkr' into al-gkr-periodic

.cargo/katex-header.html

@@ -11,6 +11,7 @@
         renderMathInElement(document.body, {
             fleqn: false,
             macros: {
+                "\\B": "\\mathbb{B}",
                 "\\F": "\\mathbb{F}",
                 "\\G": "\\mathbb{G}",
                 "\\O": "\\mathcal{O}",

CHANGELOG.md

@@ -1,7 +1,10 @@
 # Changelog
 
 ## 0.10.0 (2024-06-11) - `utils/maybe-async` crate only
-* [BREAKING] Refactored `maybe-async` macro into simpler `maybe-async` and `maybe-await` macros.
+- [BREAKING] Refactored `maybe-async` macro into simpler `maybe-async` and `maybe-await` macros.
+
+## 0.9.1 (2024-06-24) - `utils/core` crate only
+- Fixed `useize` serialization in `ByteWriter`.
 
 ## 0.9.0 (2024-05-09)
 - [BREAKING] Merged `TraceLayout` into `TraceInfo` (#245).

Cargo.toml

@@ -10,8 +10,8 @@ members = [
   "prover",
   "verifier",
   "winterfell",
-  "examples"
-, "sumcheck"]
+  "examples",
+  "sumcheck",]
 resolver = "2"
 
 [profile.release]

air/src/air/assertions/mod.rs

@@ -30,18 +30,18 @@ const NO_STRIDE: usize = 0;
 /// An assertion is always placed against a single column of an execution trace, but can cover
 /// multiple steps and multiple values. Specifically, there are three kinds of assertions:
 ///
-/// 1.  **Single** assertion - which requires that a value in a single cell of an execution trace
-///     is equal to the specified value.
-/// 2.  **Periodic** assertion - which requires that values in multiple cells of a single column
-///     are equal to the specified value. The cells must be evenly spaced at intervals with lengths
-///     equal to powers of two. For example, we can specify that values in a column must be equal
-///     to 0 at steps 0, 8, 16, 24, 32 etc. Steps can also start at some offset - e.g., 1, 9, 17,
-///     25, 33 is also a valid sequence of steps.
-/// 3.  **Sequence** assertion - which requires that multiple cells in a single column are equal
-///     to the values from the provided list. The cells must be evenly spaced at intervals with
-///     lengths equal to powers of two. For example, we can specify that values in a column must
-///     be equal to a sequence 1, 2, 3, 4 at steps 0, 8, 16, 24. That is, value at step 0 should be
-///     equal to 1, value at step 8 should be equal to 2 etc.
+/// 1. **Single** assertion - which requires that a value in a single cell of an execution trace
+///    is equal to the specified value.
+/// 2. **Periodic** assertion - which requires that values in multiple cells of a single column
+///    are equal to the specified value. The cells must be evenly spaced at intervals with lengths
+///    equal to powers of two. For example, we can specify that values in a column must be equal
+///    to 0 at steps 0, 8, 16, 24, 32 etc. Steps can also start at some offset - e.g., 1, 9, 17,
+///    25, 33 is also a valid sequence of steps.
+/// 3. **Sequence** assertion - which requires that multiple cells in a single column are equal
+///    to the values from the provided list. The cells must be evenly spaced at intervals with
+///    lengths equal to powers of two. For example, we can specify that values in a column must
+///    be equal to a sequence 1, 2, 3, 4 at steps 0, 8, 16, 24. That is, value at step 0 should be
+///    equal to 1, value at step 8 should be equal to 2 etc.
 ///
 /// Note that single and periodic assertions are succinct. That is, a verifier can evaluate them
 /// very efficiently. However, sequence assertions have liner complexity in the number of

air/src/air/aux.rs

@@ -1,34 +1,34 @@
+// Copyright (c) Facebook, Inc. and its affiliates.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+
 use alloc::vec::Vec;
 
 use math::{ExtensionOf, FieldElement};
 
-use super::{lagrange::LagrangeKernelRandElements, LogUpGkrOracle};
+use super::{LagrangeKernelRandElements, LogUpGkrOracle};
 
-/// Holds the randomly generated elements necessary to build the auxiliary trace.
+/// Holds the randomly generated elements used in defining the auxiliary segment of the trace.
 ///
-/// Specifically, [`AuxRandElements`] currently supports 3 types of random elements:
-/// - the ones needed to build the Lagrange kernel column (when using GKR to accelerate LogUp),
-/// - the ones needed to build the "s" auxiliary column (when using GKR to accelerate LogUp),
-/// - the ones needed to build all the other auxiliary columns
+/// Specifically, [`AuxRandElements`] currently supports 2 types of random elements:
+/// - the ones needed to build all the auxiliary columns except for the ones associated
+///   to LogUp-GKR.
+/// - the ones needed to build the "s" and Lagrange kernel auxiliary columns (when using GKR to
+///   accelerate LogUp). These also include additional information needed to evaluate constraints
+///   one these two columns.
 #[derive(Debug, Clone)]
 pub struct AuxRandElements<E: FieldElement> {
     rand_elements: Vec<E>,
     gkr: Option<GkrData<E>>,
 }
 
 impl<E: FieldElement> AuxRandElements<E> {
-    /// Creates a new [`AuxRandElements`], where the auxiliary trace doesn't contain a Lagrange
-    /// kernel column.
-    pub fn new(rand_elements: Vec<E>) -> Self {
-        Self { rand_elements, gkr: None }
-    }
-
-    /// Creates a new [`AuxRandElements`], where the auxiliary trace contains columns needed when
+    /// Creates a new [`AuxRandElements`], where the auxiliary segment may contain columns needed when
     /// using GKR to accelerate LogUp (i.e. a Lagrange kernel column and the "s" column).
-    pub fn new_with_gkr(rand_elements: Vec<E>, gkr: GkrData<E>) -> Self {
-        Self { rand_elements, gkr: Some(gkr) }
+    pub fn new(rand_elements: Vec<E>, gkr: Option<GkrData<E>>) -> Self {
+        Self { rand_elements, gkr }
     }
-
     /// Returns the random elements needed to build all columns other than the two GKR-related ones.
     pub fn rand_elements(&self) -> &[E] {
         &self.rand_elements
@@ -46,21 +46,35 @@ impl<E: FieldElement> AuxRandElements<E> {
         self.gkr.as_ref().map(|gkr| gkr.openings_combining_randomness.as_ref())
     }
 
+    /// Returns a collection of data necessary for implementing the univariate IOP for multi-linear
+    /// evaluations of [1] when LogUp-GKR is enabled, else returns a `None`.
+    ///
+    /// [1]: https://eprint.iacr.org/2023/1284
     pub fn gkr_data(&self) -> Option<GkrData<E>> {
         self.gkr.clone()
     }
 }
 
-/// Holds all the random elements needed when using GKR to accelerate LogUp.
+/// Holds all the data needed when using LogUp-GKR in order to build and verify the correctness of
+/// two extra auxiliary columns required for running the univariate IOP for multi-linear
+/// evaluations of [1].
 ///
-/// This consists of two sets of random values:
-/// 1. The Lagrange kernel random elements (expanded on in [`LagrangeKernelRandElements`]), and
+/// This consists of:
+/// 1. The Lagrange kernel random elements (expanded on in [`LagrangeKernelRandElements`]). These
+///    make up the evaluation point of the multi-linear extension polynomials underlying the oracles
+///    in point 4 below.
 /// 2. The "openings combining randomness".
+/// 3. The openings of the multi-linear extension polynomials of the main trace columns involved
+///    in LogUp.
+/// 4. A description of the each of the oracles involved in LogUp.
+///
+/// After verifying the LogUp-GKR circuit, the verifier is left with unproven claims provided
+/// by the prover about the evaluations of the MLEs of the main trace columns at the evaluation
+/// point defining the Lagrange kernel. Those claims are (linearly) batched into one using the
+/// openings combining randomness and checked against the batched oracles using univariate IOP
+/// for multi-linear evaluations of [1].
 ///
-/// After the verifying the LogUp-GKR circuit, the verifier is left with unproven claims provided
-/// nondeterministically by the prover about the evaluations of the MLE of the main trace columns at
-/// the Lagrange kernel random elements. Those claims are (linearly) combined into one using the
-/// openings combining randomness.
+/// [1]: https://eprint.iacr.org/2023/1284
 #[derive(Clone, Debug)]
 pub struct GkrData<E: FieldElement> {
     pub lagrange_kernel_eval_point: LagrangeKernelRandElements<E>,
@@ -116,7 +130,7 @@ impl<E: FieldElement> GkrData<E> {
                 .fold(E::ZERO, |acc, (a, b)| acc + *a * *b)
     }
 
-    pub fn compute_batched_query_<F>(&self, query: &[F]) -> E
+    pub fn compute_batched_query<F>(&self, query: &[F]) -> E
     where
         F: FieldElement<BaseField = E::BaseField>,
         E: ExtensionOf<F>,

air/src/air/boundary/mod.rs

@@ -58,8 +58,8 @@ impl<E: FieldElement> BoundaryConstraints<E> {
     ///   coefficients.
     /// * The specified assertions are not valid in the context of the computation (e.g., assertion
     ///   column index is out of bounds).
-    pub fn new(
-        context: &AirContext<E::BaseField>,
+    pub fn new<P>(
+        context: &AirContext<E::BaseField, P>,
         main_assertions: Vec<Assertion<E::BaseField>>,
         aux_assertions: Vec<Assertion<E>>,
         composition_coefficients: &[E],
@@ -88,7 +88,7 @@ impl<E: FieldElement> BoundaryConstraints<E> {
         );
 
         let trace_length = context.trace_info.length();
-        let main_trace_width = context.trace_info.main_trace_width();
+        let main_trace_width = context.trace_info.main_segment_width();
         let aux_trace_width = context.trace_info.aux_segment_width();
 
         // make sure the assertions are valid in the context of their respective trace segments;
@@ -151,9 +151,9 @@ impl<E: FieldElement> BoundaryConstraints<E> {
 
 /// Translates the provided assertions into boundary constraints, groups the constraints by their
 /// divisor, and sorts the resulting groups by the degree adjustment factor.
-fn group_constraints<F, E>(
+fn group_constraints<F, E, P>(
     assertions: Vec<Assertion<F>>,
-    context: &AirContext<F::BaseField>,
+    context: &AirContext<F::BaseField, P>,
     composition_coefficients: &[E],
     inv_g: F::BaseField,
     twiddle_map: &mut BTreeMap<usize, Vec<F::BaseField>>,

air/src/air/coefficients.rs

@@ -27,6 +27,13 @@ use math::FieldElement;
 ///
 /// The coefficients are separated into two lists: one for transition constraints and another one
 /// for boundary constraints. This separation is done for convenience only.
+///
+/// In addition to the above, and when LogUp-GKR is enabled, there are two extra sets of
+/// constraint composition coefficients that are used, namely for:
+///
+/// 1. Lagrange kernel constraints, which include both transition and boundary constraints.
+/// 2. S-column constraint, which is used in implementing the cohomological sum-check argument
+///    of https://eprint.iacr.org/2021/930
 #[derive(Debug, Clone)]
 pub struct ConstraintCompositionCoefficients<E: FieldElement> {
     pub transition: Vec<E>,
@@ -84,8 +91,9 @@ pub struct LagrangeConstraintsCompositionCoefficients<E: FieldElement> {
 ///    negligible increase in soundness error. The formula for the updated error can be found in
 ///    Theorem 8 of https://eprint.iacr.org/2022/1216.
 ///
-/// In the case when the trace polynomials contain a trace polynomial corresponding to a Lagrange
-/// kernel column, the above expression of $Y(x)$ includes the additional term given by
+/// In the case when LogUp-GKR is enabled, the trace polynomials contain an additional trace
+/// polynomial corresponding to a Lagrange kernel column and the above expression of $Y(x)$
+/// includes the additional term given by
 ///
 /// $$
 /// \gamma \cdot \frac{T_l(x) - p_S(x)}{Z_S(x)}
@@ -100,8 +108,13 @@ pub struct LagrangeConstraintsCompositionCoefficients<E: FieldElement> {
 /// 4. $p_S(X)$ is the polynomial of minimal degree interpolating the set ${(a, T_l(a)): a \in S}$.
 /// 5. $Z_S(X)$ is the polynomial of minimal degree vanishing over the set $S$.
 ///
-/// Note that, if a Lagrange kernel trace polynomial is present, then $\rho^{+}$ from above should
-/// be updated to be $\rho^{+} := \frac{\kappa + log_2(\nu) + 1}{\nu}$.
+/// Note that when LogUp-GKR is enabled, we also have to take into account an additional column,
+/// called s-column throughout, used in implementing the univariate IOP for multi-linear evaluation.
+/// This means that we need and additional random value, in addition to $\gamma$ above, when
+/// LogUp-GKR is enabled.
+///
+/// Note that, when LogUp-GKR is enabled, $\rho^{+}$ from above should be updated to be
+/// $\rho^{+} := \frac{\kappa + log_2(\nu) + 1}{\nu}$.
 #[derive(Debug, Clone)]
 pub struct DeepCompositionCoefficients<E: FieldElement> {
     /// Trace polynomial composition coefficients $\alpha_i$.
@@ -110,6 +123,6 @@ pub struct DeepCompositionCoefficients<E: FieldElement> {
     pub constraints: Vec<E>,
     /// Lagrange kernel trace polynomial composition coefficient $\gamma$.
     pub lagrange: Option<E>,
-    /// TODO
+    /// S-column trace polynomial composition coefficient.
     pub s_col: Option<E>,
 }

air/src/air/context.rs

@@ -14,9 +14,10 @@ use crate::{air::TransitionConstraintDegree, ProofOptions, TraceInfo};
 // ================================================================================================
 /// STARK parameters and trace properties for a specific execution of a computation.
 #[derive(Clone, PartialEq, Eq)]
-pub struct AirContext<B: StarkField> {
+pub struct AirContext<B: StarkField, P> {
     pub(super) options: ProofOptions,
     pub(super) trace_info: TraceInfo,
+    pub(super) pub_inputs: P,
     pub(super) main_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
     pub(super) aux_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
     pub(super) num_main_assertions: usize,
@@ -28,7 +29,7 @@ pub struct AirContext<B: StarkField> {
     pub(super) logup_gkr: bool,
 }
 
-impl<B: StarkField> AirContext<B> {
+impl<B: StarkField, P> AirContext<B, P> {
     // CONSTRUCTORS
     // --------------------------------------------------------------------------------------------
     /// Returns a new instance of [AirContext] instantiated for computations which require a single
@@ -48,6 +49,7 @@ impl<B: StarkField> AirContext<B> {
     /// * `trace_info` describes a multi-segment execution trace.
     pub fn new(
         trace_info: TraceInfo,
+        pub_inputs: P,
         transition_constraint_degrees: Vec<TransitionConstraintDegree>,
         num_assertions: usize,
         options: ProofOptions,
@@ -58,6 +60,7 @@ impl<B: StarkField> AirContext<B> {
         );
         Self::new_multi_segment(
             trace_info,
+            pub_inputs,
             transition_constraint_degrees,
             Vec::new(),
             num_assertions,
@@ -90,6 +93,7 @@ impl<B: StarkField> AirContext<B> {
     ///   of the specified transition constraints.
     pub fn new_multi_segment(
         trace_info: TraceInfo,
+        pub_inputs: P,
         main_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
         aux_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
         num_main_assertions: usize,
@@ -102,7 +106,7 @@ impl<B: StarkField> AirContext<B> {
         );
         assert!(num_main_assertions > 0, "at least one assertion must be specified");
 
-        if trace_info.is_multi_segment() && !trace_info.is_with_logup_gkr() {
+        if trace_info.is_multi_segment() && !trace_info.logup_gkr_enabled() {
             assert!(
              !aux_transition_constraint_degrees.is_empty(),
             "at least one transition constraint degree must be specified for the auxiliary trace segment"
@@ -150,6 +154,7 @@ impl<B: StarkField> AirContext<B> {
         AirContext {
             options,
             trace_info,
+            pub_inputs,
             main_transition_constraint_degrees,
             aux_transition_constraint_degrees,
             num_main_assertions,
@@ -164,6 +169,7 @@ impl<B: StarkField> AirContext<B> {
 
     pub fn with_logup_gkr(
         trace_info: TraceInfo,
+        pub_inputs: P,
         main_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
         aux_transition_constraint_degrees: Vec<TransitionConstraintDegree>,
         num_main_assertions: usize,
@@ -172,6 +178,7 @@ impl<B: StarkField> AirContext<B> {
     ) -> Self {
         let mut air_context = Self::new_multi_segment(
             trace_info,
+            pub_inputs,
             main_transition_constraint_degrees,
             aux_transition_constraint_degrees,
             num_main_assertions,
@@ -218,6 +225,10 @@ impl<B: StarkField> AirContext<B> {
         self.trace_info.length() * self.options.blowup_factor()
     }
 
+    pub fn public_inputs(&self) -> &P {
+        &self.pub_inputs
+    }
+
     /// Returns the number of transition constraints for a computation, excluding the Lagrange
     /// kernel transition constraints, which are managed separately.
     ///
@@ -239,17 +250,13 @@ impl<B: StarkField> AirContext<B> {
         self.aux_transition_constraint_degrees.len()
     }
 
-    /// Returns the index of the auxiliary column which implements the Lagrange kernel, if any
-    pub fn lagrange_kernel_aux_column_idx(&self) -> Option<usize> {
-        if self.is_with_logup_gkr() {
-            Some(self.trace_info().aux_segment_width() - 1)
-        } else {
-            None
-        }
+    /// Returns the index of the auxiliary column which implements the Lagrange kernel, if any.
+    pub fn lagrange_kernel_column_idx(&self) -> Option<usize> {
+        self.trace_info.lagrange_kernel_column_idx()
     }
 
     /// Returns true if LogUp-GKR is enabled.
-    pub fn is_with_logup_gkr(&self) -> bool {
+    pub fn logup_gkr_enabled(&self) -> bool {
         self.logup_gkr
     }
 
@@ -279,16 +286,27 @@ impl<B: StarkField> AirContext<B> {
     ///    transition constraint divisor divided by trace length.
     /// 2. `1`, because the constraint composition polynomial requires at least one column.
     ///
-    ///    Since the degree of a constraint `C(x)` can be computed as `[constraint.base +
-    ///    constraint.cycles.len()] * [trace_length - 1]` the degree of the constraint composition
-    ///    polynomial can be computed as: `([constraint.base + constraint.cycles.len()] * [trace_length
-    ///    - 1] - [trace_length - n])` where `constraint` is the constraint attaining the maximum and
-    ///    `n` is the number of exemption points. In the case `n = 1`, the expression simplifies to:
-    ///    `[constraint.base + constraint.cycles.len() - 1] * [trace_length - 1]` Thus, if each column
-    ///    is of length `trace_length`, we would need `[constraint.base + constraint.cycles.len() - 1]`
-    ///    columns to store the coefficients of the constraint composition polynomial. This means that
-    ///    if the highest constraint degree is equal to `5`, the constraint composition polynomial will
-    ///    require four columns and if the highest constraint degree is equal to `7`, it will require six columns to store.
+    /// Since the degree of a constraint `C(x)` can be computed as
+    ///
+    ///   `[constraint.base + constraint.cycles.len()] * [trace_length - 1]`
+    ///
+    /// the degree of the constraint composition polynomial can be computed as:
+    ///
+    ///   `([constraint.base + constraint.cycles.len()] * [trace_length - 1] - [trace_length - n])`
+    ///
+    /// where `constraint` is the constraint attaining the maximum and `n` is the number of
+    /// exemption points. In the case `n = 1`, the expression simplifies to:
+    ///
+    ///   `[constraint.base + constraint.cycles.len() - 1] * [trace_length - 1]`
+    ///
+    /// Thus, if each column is of length `trace_length`, we would need
+    ///
+    ///   `[constraint.base + constraint.cycles.len() - 1]`
+    ///
+    /// columns to store the coefficients of the constraint composition polynomial. This means that
+    /// if the highest constraint degree is equal to `5`, the constraint composition polynomial will
+    /// require four columns and if the highest constraint degree is equal to `7`, it will require
+    /// six columns to store.
     ///
     /// Note that the Lagrange kernel constraints require only 1 column, since the degree of the
     /// numerator is `trace_len - 1` for all transition constraints (i.e. the base degree is 1).