Skip to main content

Module booleanity

Module booleanity 

Source
Expand description

Booleanity (binary-polynomial lookup) argument.

Proves that every coefficient of every witness binary-polynomial column is a bit $\in \{0,1\}$. The committed-witness path is structured as a MultiDegreeSumcheckGroup of degree 3, batched alongside the existing CPR group with shared randomness, and emits bit-slice claims at the multi-degree sumcheck output point $r^\star$ for the protocol layer’s $\alpha’$ bridge into multipoint-eval (see “Soundness bridge” below). Affine virtual booleanity targets use a generic degree-3 group without the BinaryPoly round-1 fast path.

§Relation

For each witness binary-poly column $u_j \in (F_q^{<D}[X])^n$ with $n = 2^\mu$, decompose row-wise as

$$ {u_j}b = \sum_{i=0}^{D-1} v_{j,i,b} * X^i $$

The booleanity claim is:

$$ \forall j, i, b: v_{j,i,b} \in \{0,1\} $$

Equivalently, the MLE statement $\widetilde{v_{j,i}}(b)*(\widetilde{v_{j,i}}(b)-1) = 0$ for all $b \in {0,1}^\mu$. The protocol reduces this to a single batched sumcheck

$$ \sum_{b in {0,1}^\mu} eq(r, b) * \sum_{k=0}^{N*D-1} \alpha^k * \widetilde{v_k}(b) * (\widetilde{v_k}(b) - 1) = 0 $$

with a single batching challenge $\alpha$ over the flat $(j\text{-major}, i\text{-minor})$ index $k = j \cdot D + i$, and zerocheck point $r$. After the sumcheck reaches $r^\star$, the prover sends bit_slice_evals $= (\widetilde{v_{j,i}}(r^\star))$ to the verifier.

§Soundness bridge to multipoint-eval ($\alpha’$)

Booleanity does not itself close the bit-decomposition consistency at $r^\star$. The protocol-layer caller squeezes a fresh challenge $\alpha’$ from the transcript after bit_slice_evals are absorbed (the absorption is performed by BooleanityChecker::finalize_prover / finalize_verifier), then, for each witness binary-poly column $u_j$, appends one extra column to the multipoint-eval input list:

  • an extra MLE $\widetilde{\psi_{\alpha’}(u_j)}$ (the prover-side $\alpha’$-projection of $u_j$), and
  • an extra up-eval scalar $c’j ;:=; \sum{i=0}^{D-1} b_{j,i},\alpha’^{,i}$ (where $b_{j,i} = \widetilde{v_{j,i}}(r^\star)$ from bit_slice_evals).

No ShiftSpec references the appended slot, so down-evals / shifts pass through unchanged: row-shifted projections of witness binary-poly columns inherit booleanity from the un-shifted, $\psi_a$-projected slot they already reference in the multipoint-eval sumcheck.

Multipoint-eval / PCS is $\psi$-oblivious, so the appended slot combined with the lifted-evals step evaluating the corresponding $\bar u_j$ at $\alpha’$ enforces $\widetilde{\psi_{\alpha’}(u_j)}(r^\star) = c’_j$ via the PCS chain. By Schwartz–Zippel on the indeterminate $X$, if bit_slice_evals are not the true bit-decomposition then equality fails with probability $\le (D-1)/|F|$, so the verifier rejects.

For an unshifted affine virtual, the protocol collapses its bit-slice claims at the same $\alpha’$ and compares the result directly with the declared affine combination of source-column collapses at $r^\star$. Public source collapses are recomputed from the public trace; witness source collapses are the committed-column values bound through the MP/PCS chain above. Shifted affine terms require a separate row-shift opening and are rejected when affine specs are attached to the UAIR signature until that binding is implemented.

Structs§

BoolProverAncillary
Ancillary data produced by BooleanityChecker::prepare_sumcheck_group and consumed by BooleanityChecker::finalize_prover.
BoolVerifierAncillary
Ancillary data produced by BooleanityChecker::prepare_verifier and consumed by BooleanityChecker::finalize_verifier.
BoolVerifierSubclaim
Subclaim emitted by BooleanityChecker::finalize_verifier.
BooleanityChecker
Booleanity sumcheck group constructor / verifier.
BooleanityProof
Proof produced by the booleanity prover.

Enums§

BooleanityError
Errors from the booleanity subprotocol.

Functions§

build_affine_virtual_bit_slice_mles
Build per-bit-slice MLEs for affine virtual booleanity targets.