feat: add protocol support for list decoding regime

[jonathanpwang]

Closes INT-5791

PR: WHIR List Decoding Regime & Round-by-Round Soundness

Overview

Adds list decoding support to the WHIR proximity gap analysis, implements the BCHKS25/TR25-169 Theorem 1.5 bounds, restructures soundness accounting to use round-by-round (RBR) error composition, and provides documented production parameter presets in stark-sdk.

Previously, only unique decoding was supported (list size l = 1). This PR generalizes all soundness components to account for l > 1, propagating the list size through every Schwartz-Zippel and batching bound.

---

1. WhirProximityStrategy and ProximityRegime (stark-backend/src/config.rs)

New enum: WhirProximityStrategy controls which proximity regime each WHIR round uses:

Variant	Behavior
UniqueDecoding	Unique decoding in every round
SplitUniqueList { m, list_start_round }	Unique decoding for rounds < list_start_round, then list decoding with multiplicity m
ListDecoding { m }	List decoding with multiplicity m in every round

ProximityRegime (per-round) gains a ListDecoding { m } variant. The whir_query_security_bits method now uses the Johnson bound sqrt(rho * (1 + 1/m)) for list decoding max agreement instead of (1 + rho) / 2 (unique decoding).

WhirParams expanded with three new fields (previously hardcoded constants):

• folding_pow_bits -- grinding bits per folding step
• mu_pow_bits -- grinding bits for the mu batching challenge
• proximity: WhirProximityStrategy

These are also stored on WhirConfig so the soundness calculator can access them.

---

2. BCHKS25 Proximity Gap Bounds (stark-backend/src/soundness.rs)

whir_proximity_gap_security now returns ProximityGapSecurity { log2_err, log2_list_size } instead of a single f64.

For ListDecoding { m }:

• Computes log2(a) from BCHKS25 Lemma 3.1 / Equation (13) using degree parameters D_X, D_Y, D_Z.
• Reference (closed-form) degrees from Lemma 3.1 are in bchks25_reference_log2_degrees.
• An optional brute-force optimizer (feature-gated behind soundness-bchks25-optimized) searches for tighter (D_X, D_Y, D_Z) that still satisfy all proof conditions (Equation 11 n_vars > n_eqs, D_X >= k*D_Y, D_Z >= D_Y, Section 3.2 precondition).

Brute-force module (bchks25_brute_force_params, behind feature flag)

• Scans D_Y from max(1, m-1) up to a scaled reference upper bound.
• For each D_Y, samples candidate D_X values (base k*D_Y, near the slope crossover, and a coarse grid up to the Section 3.2 limit).
• Solves for minimal valid D_Z via the closed-form linear inequality A_v*(d_z+1) - B_v > A_e*(d_z+1) - B_e.
• Picks the (D_X, D_Y, D_Z) minimizing log2(a).

---

3. Round-by-Round Soundness Restructuring (stark-backend/src/soundness.rs)

WhirSoundnessCalculator fields restructured to reflect the WHIR paper's Theorem 5.2 / Claim 5.4 error composition:

Old field	New field(s)	Description
query_bits	query_bits (detail)	Unchanged, kept for per-component analysis
proximity_gaps_bits	proximity_gaps_bits (detail)	Unchanged
sumcheck_bits	sumcheck_bits (detail)	Unchanged
ood_bits	ood_rbr_bits	Now includes l^2 factor: `
gamma_batching_bits	gamma_batching_bits (detail)	Now `
(new)	fold_rbr_bits	min_round(combine(sumcheck, prox_gaps)) -- per Theorem 5.2 epsilon_fold
(new)	shift_rbr_bits	min_round(combine(query, gamma)) -- per Claim 5.4 epsilon_shift/epsilon_fin
(new)	mu_batching_bits	Initial mu batching, now includes proximity gap error + grinding

Overall WHIR security is now min(mu_batching, fold_rbr, ood_rbr, shift_rbr) instead of min(each_component_independently).

List size propagation

All non-WHIR Schwartz-Zippel bounds now add log2_list_size (from the initial round's proximity gap) to their security:

• calculate_logup_soundness
• calculate_zerocheck_sumcheck_soundness
• calculate_constraint_batching_soundness
• calculate_stacked_reduction_soundness

The SoundnessCalculator::calculate signature drops the proximity_regime: ProximityRegime parameter (now read from params.whir.proximity).

---

4. Production Parameter Presets (stark-sdk/src/config/mod.rs)

New public functions defining documented production configurations:

Function	Config
app_params_with_100_bits_security(log_stacked_height)	l_skip=4, log_blowup=1, w_stack=2048, SplitUniqueList{m:2, start:1}, fold_pow=20, mu_pow=15
leaf_params_with_100_bits_security()	l_skip=2, n_stack=18, log_blowup=2, w_stack=1024, SplitUniqueList{m:3, start:1}, fold_pow=20, mu_pow=13
internal_params_with_100_bits_security()	l_skip=2, n_stack=17, log_blowup=2, w_stack=1024, SplitUniqueList{m:3, start:1}, fold_pow=20, mu_pow=13
compression_params_with_100_bits_security()	l_skip=2, n_stack=20, log_blowup=4, w_stack=16, ListDecoding{m:1}, fold_pow=20, mu_pow=20

Each function has a doc comment listing the circuit parameter upper bounds (max AIRs, constraints, trace columns, etc.) under which 100-bit security is proven.

SystemParams::new(...) constructor added for building params from these primitives (hardcodes k_whir=4, max_constraint_degree=4, query_phase_pow_bits=20).

---

5. Production Soundness Tests Moved to Integration Test (stark-backend/tests/soundness.rs)

The production configuration tests (test_app_vm_security, test_leaf_aggregation_security, etc.) were moved from unit tests in soundness.rs to a new integration test file. This avoids a circular dependency: these tests now import the preset functions from stark-sdk rather than duplicating the parameter definitions.

---

6. Example Simplification (stark-sdk/examples/keccakf.rs, cuda-backend/examples/keccakf.rs)

Both keccakf examples replace ~20 lines of manual SystemParams / WhirConfig construction with a single call to app_params_with_100_bits_security(21).

---

7. Bug Fixes (from earlier commits in the branch)

• Out-of-domain sampling error: OOD error formula now uses m_i (log degree after folding, i.e., at the start of the next round) instead of m_i + k (log degree before folding).
• Gamma batching error: Uses list_size * t instead of t - 1 to match Theorem 5.6.
• Proximity regime mismatch: Fixed inconsistency where the regime used for query count selection didn't match the regime used in soundness analysis.

[jonathanpwang]

attn: @zlangley

[jonathanpwang]

make sure to check this - I had it wrong in a previous version

[jonathanpwang]

the theorem states these combined, not a separate RBR errors

[jonathanpwang]

Theorem states them combined