binius_prover/protocols/bitand/
prove.rs

1// Copyright 2025 Irreducible Inc.
2// Copyright 2026 The Binius Developers
3
4use std::ops::Deref;
5
6use binius_compute::Allocator;
7use binius_core::word::Word;
8use binius_field::{BinaryField, PackedField, Rijndael8b as B8};
9use binius_ip_prover::channel::IPProverChannel;
10use binius_math::{BinarySubspace, univariate::EvaluationDomain};
11use binius_utils::checked_arithmetics::log2_ceil_usize;
12use binius_verifier::{
13	config::PROVER_SMALL_FIELD_ZEROCHECK_CHALLENGES, protocols::bitand::AndCheckOutput,
14};
15
16use super::prover::UnivariateRoundProver;
17use crate::protocols::rerand::{self, OperandWitness};
18
19/// Proves the AND constraint reduction over the two operand columns `A` and `B`.
20///
21/// This wraps [`UnivariateRoundProver`], the univariate-skip round, so both the
22/// single-instance prover and the M4 batch prover route their AND check through one entry point.
23/// Its multilinear rounds are one sumcheck with the operand-column MLE-checks of `operands`; see
24/// [`rerand::prove`].
25/// The `C` operand is never passed: the reduction derives `C = A & B` word-by-word, which is sound
26/// because folding is F2-linear on word bits (see [`UnivariateRoundProver::compute_message`]).
27///
28/// The columns are generic over their backing store `Data` (anything that dereferences to
29/// `[Word]`), so pooled buffers and plain `Vec<Word>` are both accepted and moved into the kernel.
30/// The univariate-skip domain is built internally as
31/// `BinarySubspace::<B8>::with_dim(Word::LOG_BITS + 1)`, matching the domain the shift reduction
32/// folds its bit axis over.
33///
34/// The two columns must have equal length, but that length need not be a power of two: the
35/// constraint axis is the next power of two and the rows past the columns' end read as zero. Such a
36/// row forces the derived `C = A & B` to zero as well, so `A * B - C` vanishes on it and the
37/// reduction skips it rather than folding zeros. Passing an already-padded column is therefore
38/// equivalent, just slower.
39///
40/// See [`binius_verifier::protocols::bitand`] for the protocol specification and
41/// [`AndCheckOutput`] for the output shape.
42///
43/// # Panics
44///
45/// Panics if the two operand columns don't have equal length.
46pub fn prove<A, F, PChallenge, Channel, Data>(
47	columns: [Data; 2],
48	operands: &[OperandWitness<'_, F>],
49	channel: &mut Channel,
50	alloc: &A,
51) -> AndCheckOutput<F>
52where
53	A: Allocator,
54	F: BinaryField + From<B8>,
55	PChallenge: PackedField<Scalar = F>,
56	Channel: IPProverChannel<F>,
57	Data: Deref<Target = [Word]>,
58{
59	// The univariate-skip domain spans one dimension above the 64-bit word.
60	let prover_message_domain = BinarySubspace::<B8>::with_dim(Word::LOG_BITS + 1);
61	let [a, b] = columns;
62
63	// The column length is the row count: one row per constraint for the single-instance prover,
64	// one per (instance, constraint) pair for the M4 batch prover. The constraint axis rounds that
65	// count up to a power of two, and the rows in between read as zero.
66	assert_eq!(a.len(), b.len(), "the operand columns must have equal length");
67	let log_constraint_count = log2_ceil_usize(a.len());
68
69	// Pin the first few zerocheck coordinates to fixed small-field elements (friendly challenges),
70	// and draw the rest from the large field. The prover and verifier pin and draw the same split,
71	// in the same order.
72	let n_extra_zerocheck_challenges =
73		log_constraint_count.saturating_sub(PROVER_SMALL_FIELD_ZEROCHECK_CHALLENGES.len());
74	let big_field_zerocheck_challenges = channel.sample_many(n_extra_zerocheck_challenges);
75
76	let prover = UnivariateRoundProver::<_, _>::compute_message(
77		log_constraint_count,
78		a,
79		b,
80		big_field_zerocheck_challenges,
81		&prover_message_domain,
82	);
83
84	channel.send_many(prover.round_message());
85	let z_challenge = channel.sample();
86	let claim = prover.univariate_claim(z_challenge);
87
88	let bitand = tracing::debug_span!("Fold univariate round")
89		.in_scope(|| prover.fold::<PChallenge, _>(alloc, z_challenge));
90	// The operand columns fold over the 64-point domain: the skip domain less its top dimension.
91	let lagrange = prover_message_domain
92		.isomorphic::<F>()
93		.reduce_dim(Word::LOG_BITS)
94		.lagrange_evals(&z_challenge);
95	let rerand =
96		rerand::prove::<_, PChallenge, _, _>(bitand, claim, &lagrange, operands, channel, alloc);
97	AndCheckOutput {
98		z_challenge,
99		rerand,
100	}
101}
102
103#[cfg(test)]
104mod tests {
105	use std::{array, iter::repeat_with};
106
107	use binius_compute::GlobalAllocator;
108	use binius_field::arch::OptimalPackedB128;
109	use binius_transcript::{ProverTranscript, VerifierTranscript};
110	use binius_verifier::{
111		config::{B128, StdChallenger},
112		verify_bitand_reduction,
113	};
114	use rand::prelude::*;
115
116	use super::*;
117
118	// A column whose length is not a power of two reduces exactly as the same column zero-padded up
119	// to one: byte-identical transcript, identical reduced claim, and the claim still verifies
120	// against the padded row count the verifier derives from the constraint system.
121	//
122	// This is the guarantee that lets the M4 prover stop materializing the padding rows
123	// (BINIUS-388) without moving anything on the wire.
124	#[test]
125	fn unpadded_columns_reduce_identically_to_padded_ones() {
126		let mut rng = StdRng::seed_from_u64(0);
127
128		// Row counts crossing the round-1 window of 128 words and the fold's packed width: inside a
129		// single window, one word past a whole window, and several windows plus a partial one.
130		for n_rows in [3, 100, 129, 1000] {
131			let [a, b] = array::from_fn(|_| {
132				repeat_with(|| Word(rng.random()))
133					.take(n_rows)
134					.collect::<Vec<_>>()
135			});
136
137			let log_rows = log2_ceil_usize(n_rows);
138			let pad = |words: &[Word]| {
139				let mut padded = words.to_vec();
140				padded.resize(1 << log_rows, Word::ZERO);
141				padded
142			};
143
144			// One proof per shape, each from a fresh transcript over the same challenger seed.
145			let run = |columns: [Vec<Word>; 2]| {
146				let mut transcript = ProverTranscript::new(StdChallenger::default());
147				let output = prove::<_, B128, OptimalPackedB128, _, _>(
148					columns,
149					&[],
150					&mut transcript,
151					&GlobalAllocator,
152				);
153				(output, transcript.finalize())
154			};
155			let (unpadded_output, unpadded_proof) = run([a.clone(), b.clone()]);
156			let (padded_output, padded_proof) = run([pad(&a), pad(&b)]);
157
158			assert_eq!(unpadded_output, padded_output, "claim differs at n_rows = {n_rows}");
159			assert_eq!(unpadded_proof, padded_proof, "transcript differs at n_rows = {n_rows}");
160
161			let mut verifier_transcript =
162				VerifierTranscript::new(StdChallenger::default(), unpadded_proof);
163			let verify_output = verify_bitand_reduction(
164				log_rows,
165				&BinarySubspace::<B8>::with_dim(Word::LOG_BITS + 1).isomorphic::<B128>(),
166				&[],
167				&mut verifier_transcript,
168			)
169			.unwrap();
170			verifier_transcript
171				.finalize()
172				.expect("no trailing proof data");
173			assert_eq!(unpadded_output, verify_output, "verifier disagrees at n_rows = {n_rows}");
174		}
175	}
176}
binius_prover/protocols/bitand/prove.rs

binius_prover/protocols/bitand/
prove.rs
