Skip to main content

prove

Function prove 

Source
pub fn prove<A, F, PChallenge, Channel, Data>(
    columns: [Data; 2],
    operands: &[OperandWitness<'_, F>],
    channel: &mut Channel,
    alloc: &A,
) -> AndCheckOutput<F>
where A: Allocator, F: BinaryField + From<Rijndael8b>, PChallenge: PackedField<Scalar = F>, Channel: IPProverChannel<F>, Data: Deref<Target = [Word]>,
Expand description

Proves the AND constraint reduction over the two operand columns A and B.

This wraps UnivariateRoundProver, the univariate-skip round, so both the single-instance prover and the M4 batch prover route their AND check through one entry point. Its multilinear rounds are one sumcheck with the operand-column MLE-checks of operands; see rerand::prove. The C operand is never passed: the reduction derives C = A & B word-by-word, which is sound because folding is F2-linear on word bits (see UnivariateRoundProver::compute_message).

The columns are generic over their backing store Data (anything that dereferences to [Word]), so pooled buffers and plain Vec<Word> are both accepted and moved into the kernel. The univariate-skip domain is built internally as BinarySubspace::<B8>::with_dim(Word::LOG_BITS + 1), matching the domain the shift reduction folds its bit axis over.

The two columns must have equal length, but that length need not be a power of two: the constraint axis is the next power of two and the rows past the columns’ end read as zero. Such a row forces the derived C = A & B to zero as well, so A * B - C vanishes on it and the reduction skips it rather than folding zeros. Passing an already-padded column is therefore equivalent, just slower.

See [binius_verifier::protocols::bitand] for the protocol specification and [AndCheckOutput] for the output shape.

§Panics

Panics if the two operand columns don’t have equal length.