BINIUS-114: switch multilinears to the monomial (infinity hypercube) basis#1565
Closed
benji-potamus wants to merge 3 commits into
Closed
BINIUS-114: switch multilinears to the monomial (infinity hypercube) basis#1565benji-potamus wants to merge 3 commits into
benji-potamus wants to merge 3 commits into
Conversation
…oes not work under unchanged verifier) Tests jimpo's proposed alternative for the broken non-homogeneous mul-gate MLE-check: instead of one QuadraticMleCheckProver for A*B - C, split into a quadratic prover for the homogeneous product A*B and a separate prover for the multilinear C, driven in lockstep like batch_prove_mle but combined with hardcoded weights +1/-1 instead of a random batch coefficient. The verifier is the unchanged single degree-2 mlecheck::verify. run_split_mul_gate_experiment is a non-panicking harness parameterized over the C sub-prover framing (degree-1 MultilinearEvalProver vs degree-2-framed QuadraticMleCheckProver) and the C claim (evaluate(C,point) vs c[0]). test_split_mul_gate_experiment_matrix tabulates outcomes: MultilinearEvalProver (deg1) | claim_C=evaluate(C) | n=1:FAIL n=2:FAIL n=3:FAIL n=8:FAIL QuadraticMleCheckProver (deg2)| claim_C=c[0] | n=1:PASS n=2:FAIL n=3:FAIL n=8:FAIL Conclusion: the split does not rescue the protocol under the unchanged degree-2 verifier. The verifier's per-round identity eval = R(0) + alpha*R(inf) extracts exactly one infinity coefficient (the degree-2 leading = the product's a1*b1). A lower-degree term like -C carries infinity-hypercube mass through its own degree-1 leading coefficient, for which the degree-2 framing has no slot: framing C at degree 2 zeroes that mass (reproducing the original multi-round bug — deg2 + c[0] passes only at n=1, then matches the single prover), and framing C at degree 1 makes the carried claim over-count C's infinity mass so the verifier's single infinity slot cannot carry it (fails even at n=1). The fix must live in the round polynomial / verifier identity (e.g. the eq-weighted degree-(d+1) form), not in how provers are composed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft — work in progress, opened for early review of BINIUS-114. Per the issue, this is one large change split by commit, and some commits are intentionally red. Not all tests pass yet — see "Open question" below; there's an active discussion on the Linear issue.
Switches the multilinear polynomial representation from the {0,1} evaluation (Lagrange) basis to the monomial basis — i.e. evaluation on the infinity hypercube
{0,∞}ⁿ, where a multilinear's value list is its monomial-coefficient vector. Grounded in eprint 2026/762 and the companion spec PR binius-zk/binius.xyz#117.Commits
1.
eqindicator + multilinearfold→ monomial basis (crates/math/src/multilinear/{eq,fold,evaluate}.rs)eq̃(X,Y) = 1 + XY(not the char-21+X+Y); tensor factor(1−xᵢ, xᵢ) → (1, xᵢ);eq_ind_zero→ identically 1;eq_ind_truncate_low→ prefix truncation.fold_highest_var_inplace:zero += r·(one−zero)→zero += r·one(the two halves are now the coefficients[c0, c1]). Same change to the scalar evaluator.eq_ind_partial_evalnow returns monomial coefficients, so it is no longereq_indat literal {0,1} vertices (only under projective {0,∞} evaluation);evaluate(an inner product with that tensor) stays correct unchanged. Unit tests rewritten to the monomial-coefficient / zeta-transform invariants.-D warningsclean.2. sumcheck & MLE-check round identities → monomial basis (
crates/ip/src/{sumcheck/common,mlecheck}.rs,crates/ip-prover/src/sumcheck/*)R(0)+R(∞)=s;recover→a_d = s − a₀.M(1)=lo+hi,M(∞)=hi),interpolate_eq→y₀ = s − α·y_inf(the(1−α)⁻¹drops out),recover→a₀ = eval − α·a_d,round_coeffs_by_eq→prime·(1+αX),lerp_over_endpoints→r₀ + α·r_inf.gruen32needs no change.test_bivariate_product_sumcheck, and the homogeneous degree-2 MLE-checks (a*b,(a+b)(c+d)) at all sizes.Open question (blocking the rest)
Non-homogeneous / lower-degree composites —
a+band the mul gatea*b − c— reduce correctly at one round but fail across multiple rounds (the degree-2 framing's∞ = X²-coeff doesn't match the carried claim for the lower-degree terms). I've asked on the Linear issue whether the MLE-check round poly should be the bare prime (degreed, current) or the eq-weighted degree-(d+1)poly with∞extractingx^{d+1}, and whether a degree-1 composition should use a degree-1 prover.Still to come (after the above resolves)
🤖 Generated with Claude Code