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