Skip to content

Run the BaseFold opening as a Libra-masked sumcheck over {0, ∞}^ℓ - #2523

Merged
jimpo merged 3 commits into
mainfrom
aj/binius-703-phase-a-libra-masked-batch-sumcheck-with-a-compiler
Nov 1, 2026
Merged

jimpo merged 3 commits into
mainfrom
aj/binius-703-phase-a-libra-masked-batch-sumcheck-with-a-compiler

Conversation

@benji-potamus

Copy link
Copy Markdown
Collaborator

Linear: BINIUS-703 (Phase A of BINIUS-696, binius.xyz#128 "Batched ZK BaseFold opening").

This replaces the σ/γ claim masking with Phase A. The compiler now commits its own Libra oracle for a masked opening: a round of its own after the schedule's, holding 2^{⌈log2 ℓ⌉ + 2} entries (pad_len = 0 until BINIUS-704). The batched claim is sumchecked over the infinity hypercube on f + α·h.

Scope: this also brings in the minimal Phase A′ and Phase B interleave round

Phase A can't land on its own; details are in the Linear comment:

  • β. Nothing checks β until Phase A′. Left unchecked, it would let the prover hit any f*, so the opening would accept any claims.
  • γ. With the σ-masking gone, the α_r are claims on M_r alone. Reaching the γ-fold that *_mlecheck_basefold opens needs the ω side, which is the interleave round.

So a masked opening runs:

  1. Phase A: Libra-masked batch sumcheck over {0, ∞}^ℓ. The prover sends α_r; the verifier checks Σ_r α_r · T_r^∞(ρ_{<ℓ_r}) = f*, getting T_r^∞ from the operand closures via the projective translation.
  2. Phase A′: unmasked infinity::batch_prove / batch_verify over the Libra round's m variables, moving every claim to prefixes of ρ''.
  3. Phase B: translates the claims to σ_j = ρ''_j / (1 + ρ''_j). In the interleave round the prover sends the polynomial at Y = 1, and γ is sampled after r'. Then today's *_mlecheck_basefold, whose signature is unchanged.

An unmasked opening commits no Libra oracle and samples neither α nor γ.

Left for BINIUS-705:

  • An inversion-free translation. This PR uses invert_or_zero, so the recursion circuit pays for the inverses.
  • Tests that tamper α'_r, β' and the interleave polynomial.
  • The measurement table.

ρ_j = 1 is not rejected explicitly. It has probability ℓ/|K|, which the soundness error already covers.

Commits

  1. Add the infinity-cube point translation and expose its product prover. Adds sumcheck::infinity::to_mle_point, and makes ProductProver public so the opening can drive unit-weight sums plus the mask.
  2. Run the BaseFold opening as a Libra-masked sumcheck.
    • New binius_iop::basefold::libra (layout, libra-eval table and its monomial evaluation) and the prover's LibraMask.
    • Verifier and prover openings rewritten.
    • Compiler appends the Libra layout.
    • New tests: tampered s_h / α_0 rejected, masked and unmasked compiler layouts.

Costs to look at

  • Proof size: the Spartan proof_size_test pin rises from 61680 to 77200. On that one-constraint circuit, most of the increase is the second round oracle's query openings.
  • Phase A copies each round oracle once, because ProductProver folds in place. It's marked with a ponytail: note.
  • Phase A′ makes one pass per round oracle, using hypercube::fold_highest_var::<InfCube> (Make fold_highest_var generic over the hypercube #2522).

Testing

  • cargo nextest run --workspace --release: 1956 passed. Doc tests pass.
  • cargo clippy --workspace --all-targets --all-features -D warnings: clean. Nightly fmt: clean.

🤖 Generated with Claude Code

to_mle_point translates a point of a sumcheck over {0, ∞}^n to the
Boolean hypercube, sigma_j = rho_j / (1 + rho_j), with the scales
prod_{j<k} (1 + rho_j) that relate u^∞ to the multilinear extension.

ProductProver becomes public so a caller can drive the round
polynomials with its own combination, as the BaseFold opening's
unit-weight, Libra-masked batch does.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@benji-potamus
benji-potamus requested a review from a team October 30, 2026 22:47
@linear-code

linear-code Bot commented Oct 30, 2026

Copy link
Copy Markdown

BINIUS-703

@jimpo jimpo left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Refactor to share more of the libra code with the ZK MLE-check in the spartan-prover and spartan-verifier crates. The Mask in zk_mlecheck looks very similar. This can be moved out to a libra in binius-ip/binius-ip-prover.

jimpo and others added 2 commits November 1, 2026 09:46
The ZK MLE-check's mask, its coefficient-table dimensions and the
libra-eval operand describe the Libra mask itself, not the MLE-check.
Move them to binius_ip::libra and binius_ip_prover::libra, where the
BaseFold opening's own Libra mask can share them. No behavior change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Replace the sigma/gamma claim masking with Phase A of the batched ZK
BaseFold opening (binius.xyz#128). The compiler commits a Libra oracle
for a masked opening, in a round of its own after the schedule's: the
coefficient table of a binius_ip_prover::libra::Mask of degree 2 on ℓ
variables, the mask the ZK MLE-check uses. The batched claim is
sumchecked over the infinity hypercube on f + α·h, leaving the
monomial evaluations α_r = M_r^∞(ρ_{<ℓ_r}) and the Libra query
β = h(ρ). The mask gains the round polynomials of that sumcheck, and
libra_eval takes the hypercube it evaluates over.

β is not an evaluation claim, so a masked opening also runs Phase A'
now: an unmasked sumcheck over the Libra round's m variables moves
every claim to prefixes of one point ρ''. Phase B translates the claims
to multilinear extensions at σ_j = ρ''_j / (1 + ρ''_j) and adds the
interleave round. The prover sends the round polynomial at Y = 1 and
the verifier samples γ after r'. Without it the claims, now on M_r
alone, could not reach the γ-fold the FRI opens.

An unmasked opening commits no Libra oracle and samples neither α nor
γ. The Spartan proof-size pin grows by the Libra oracle's openings.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@benji-potamus
benji-potamus force-pushed the aj/binius-703-phase-a-libra-masked-batch-sumcheck-with-a-compiler branch from 3a65293 to e02352f Compare November 1, 2026 09:54
@benji-potamus

Copy link
Copy Markdown
Collaborator Author

Addressed the review: the Libra code is now shared with the ZK MLE-check (pushed e02352f).

The stack is now three commits:

  1. Unchanged: to_mle_point and the public ProductProver.
  2. New, a pure move with no behavior change:
    • mask_buffer_dimensions and libra_eval move from binius_ip::mlecheck to binius_ip::libra.
    • Mask and expand_libra_eval move from binius_ip_prover::sumcheck::zk_mlecheck to binius_ip_prover::libra, along with their two tests.
    • Spartan's prover and verifier import them from the new modules.
  3. Phase A, now built on those modules. I deleted both BaseFold-local libra.rs files:
    • Mask type. The opening's mask is a Mask of degree 2. It gains evaluate, sum_over_infinity_cube and infinity_round_coeffs for the sumcheck over {0, ∞}^ℓ.
    • libra_eval. It now takes the hypercube it evaluates over: OneCube for the MLE-check's MLE, InfCube for Phase A′'s monomial evaluation. The prover's Phase A′ operand is expand_libra_eval.
    • Layout. The Libra round's layout moved into basefold::layout::libra_layout and is sized by mask_buffer_dimensions. When the ZK pad lands (BINIUS-704), it can pass the pad as n_extra_dof.
    • Table layout. The table now uses Mask's layout, j · 2^{m_d} + k, instead of my own.

Checks: the workspace passes (1956 tests, plus doc tests), and clippy with -D warnings and nightly fmt are clean. The proof-size pin is unchanged at 77200.

Comment thread crates/iop/src/basefold/compiler.rs Resolved
@benji-potamus

Copy link
Copy Markdown
Collaborator Author

@jimpo thanks for the approval. CI is green on e02352f. Could you add this to the merge queue? I can't reach it from here. The follow-up from your inline comment is BINIUS-708.

@jimpo
jimpo added this pull request to the merge queue Nov 1, 2026
Merged via the queue into main with commit 19b8f6f Nov 1, 2026
10 checks passed
@jimpo
jimpo deleted the aj/binius-703-phase-a-libra-masked-batch-sumcheck-with-a-compiler branch November 1, 2026 23:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants