p3_sumcheck/layout/
mod.rs

1//! Stacked sumcheck layout.
2//!
3//! # Why stack
4//!
5//! - A WHIR commitment carries a fixed per-commitment overhead (FFT + Merkle).
6//! - Committing each table separately multiplies that overhead by the table count.
7//! - Stacking concatenates every table into one multilinear polynomial and
8//!   commits once, so a single commitment covers all tables.
9//! - WHIR natively supports multiple opening claims on the committed polynomial,
10//!   so no extra batching sumcheck is needed on top.
11//!
12//! # Layout of the stacked polynomial
13//!
14//! - Sort source tables by arity, largest first.
15//! - Lay columns out back-to-back on the boolean hypercube.
16//! - Each column takes a contiguous slot of size `2^arity`.
17//! - Pad with zeros up to the next power of two.
18//! - The concatenation is itself a multilinear polynomial.
19//!
20//! Example: three tables with `(4, 3, 2)` variables and one column each.
21//!
22//! ```text
23//!     +---- 16 ----+-- 8 --+-- 4 --+-- pad --+
24//!     |    P_1     |  P_2  |  P_3  |  zeros  |
25//!     +------------+-------+-------+---------+
26//!     0           16      24      28        32
27//! ```
28//!
29//! # Selectors: addressing a slot by a boolean prefix
30//!
31//! - Each column is reached by prefixing its local variables with a boolean
32//!   selector that picks the slot.
33//! - Local variables follow the selector bits.
34//!
35//! For the example above, with `P` the stacked polynomial:
36//!
37//! ```text
38//!     P_1(x_1, x_2, x_3, x_4) = P(0,       x_1, x_2, x_3, x_4)
39//!     P_2(x_1, x_2, x_3)      = P(1, 0,    x_1, x_2, x_3)
40//!     P_3(x_1, x_2)           = P(1, 1, 0, x_1, x_2)
41//! ```
42//!
43//! # Why selector lifts stay cheap in WHIR
44//!
45//! - The WHIR cost of adding an equality constraint `P(z) = y` scales as
46//!   `O(2^k)`, where `k` counts the coordinates of `z` that are not in `{0, 1}`.
47//! - Selector coordinates are always boolean, so they do not inflate `k`.
48//! - Lifting a local claim into a stacked claim therefore adds no asymptotic
49//!   cost beyond the original local coordinates.
50//!
51//! # Residual sumcheck: two binding modes
52//!
53//! After lifting, a batching challenge `alpha` collapses every recorded
54//! opening into one residual claim. The residual sumcheck can bind variables
55//! in two different orders:
56//!
57//! - Prefix-first binding: round one runs in SIMD-packed arithmetic, and the
58//!   remaining rounds drive a product polynomial.
59//! - Suffix-first binding: SVO accumulators are precomputed at claim-recording
60//!   time and folded round by round with Lagrange weights.
61//!
62//! Both modes end at the same residual product polynomial; the binding order
63//! only decides which fast-path tricks apply on the first rounds.
64//!
65//! # References
66//!
67//! - Stacking construction: "Minimal zkVM for Lean Ethereum", section 3.7.
68//! - WHIR proximity argument: ePrint 2024/1586.
69//! - SVO accumulators: ePrint 2025/1117, Algorithm 5.
70//! - Jagged PCS: ePrint 2025/0917.
71
72mod opening;
73mod plan;
74mod prover;
75mod verifier;
76mod witness;
77
78pub use opening::{
79    MultiClaim, Opening, ProverMultiClaim, ProverVirtualClaim, VerifierMultiClaim, VerifierOpening,
80    VerifierVirtualClaim,
81};
82pub use prover::{Layout, PrefixProver, SuffixProver};
83pub use verifier::Verifier;
84pub use witness::{Selector, Table, TablePlacement, Witness};
85
86use crate::strategy::VariableOrder;
87pub use crate::table::TableShape;
88
89/// Verifier-side metadata required to replay a committed layout.
90#[derive(Debug, Clone, Copy, PartialEq, Eq)]
91pub struct LayoutStrategy {
92    /// Whether selector bits are reversed and appended after local bits.
93    pub reverse_selectors: bool,
94    /// Variable order used by the residual WHIR/sumcheck rounds.
95    pub variable_order: VariableOrder,
96}
97
98impl LayoutStrategy {
99    pub const fn new(reverse_selectors: bool, variable_order: VariableOrder) -> Self {
100        Self {
101            reverse_selectors,
102            variable_order,
103        }
104    }
105}
106
107#[cfg(test)]
108mod tests {
109    use super::*;
110
111    #[test]
112    fn layout_strategy_new_stores_constructor_arguments_verbatim() {
113        // Invariant:
114        //     LayoutStrategy::new copies its two arguments into the matching
115        //     fields without mutation. The two reachable shapes — prefix
116        //     binding without selector reversal, and suffix binding with
117        //     selector reversal — are exercised exactly the same way.
118        //
119        // Fixture state:
120        //     case A: (reverse_selectors = false, Prefix)
121        //     case B: (reverse_selectors = true,  Suffix)
122        let case_a = LayoutStrategy::new(false, VariableOrder::Prefix);
123        let case_b = LayoutStrategy::new(true, VariableOrder::Suffix);
124
125        assert!(!case_a.reverse_selectors);
126        assert_eq!(case_a.variable_order, VariableOrder::Prefix);
127
128        assert!(case_b.reverse_selectors);
129        assert_eq!(case_b.variable_order, VariableOrder::Suffix);
130    }
131}
p3_sumcheck/layout/mod.rs

p3_sumcheck/layout/
mod.rs
