Skip to main content

binius_prover/fold_word/
mod.rs

1// Copyright 2025 Irreducible Inc.
2// Copyright 2026 The Binius Developers
3
4//! Contracting a word list against weights, along either of its two axes.
5//!
6//! A `&[Word]` list is a matrix over GF(2): row `i` is word `i`, and column `b` is bit position
7//! `b` across every word.
8//!
9//! ```text
10//!     words[0]  b63 b62 ... b1 b0
11//!     words[1]  b63 b62 ... b1 b0
12//!       ...
13//!     words[n]  b63 b62 ... b1 b0
14//! ```
15//!
16//! Every fold here contracts one axis of that matrix against one weight per position of it.
17//!
18//! | contracts | weights | leaves |
19//! |---|---|---|
20//! | the bit axis, the columns | one per bit position | one element per word |
21//! | the word axis, the rows | an equality tensor over the rows | one element per bit position |
22//!
23//! Both use the [Method of Four Russians]: group eight weights, precompute all 256 of their subset
24//! sums, then let one byte of the matrix index eight positions' whole contribution at once.
25//!
26//! The two directions differ in one step. Folding the bit axis reads a byte of the word directly.
27//! Folding the word axis first transposes a group of eight rows, so that one byte carries eight
28//! rows' bits at a single column.
29//!
30//! Each axis is folded through a folder that owns its lookup tables. Building the folder is what
31//! costs, so a caller folding several lists against one point builds it once and reuses it.
32//!
33//! [Method of Four Russians]: <https://en.wikipedia.org/wiki/Method_of_Four_Russians>
34
35mod bit_axis;
36mod lookup;
37mod output;
38mod word_axis;
39
40use binius_core::word::Word;
41pub use bit_axis::BitAxisFolder;
42pub use word_axis::WordAxisFolder;
43
44use crate::bit_matrix::WEIGHTS_PER_TABLE;
45
46/// Number of words folded together within a single chunk.
47///
48/// One row-fold table covers one byte of a word, so a chunk spans every row those tables reach:
49/// eight tables of eight rows each. That this equals the bit width of a word is arithmetic, not
50/// definition.
51const CHUNK_SIZE: usize = Word::BYTES * WEIGHTS_PER_TABLE;
52/// Base-2 logarithm of the number of words folded together within a single chunk.
53const LOG_CHUNK_SIZE: usize = CHUNK_SIZE.ilog2() as usize;
54/// One 64-bit word with its bit axis expanded into full field elements.
55///
56/// Each bit position becomes one element, so the word is carried in oblong form.
57pub type FoldedWord<F> = [F; Word::BITS];