1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
//! Ring switching at a bit alphabet.
//!
//! The reduction beside this one is generic over a field and an extension.
//! It cannot be instantiated at `F_2`, because its basis accessor borrows.
//! A borrowed slice cannot hold 128 coefficients of one bit each.
//!
//! # What changes at a bit alphabet
//!
//! Two things about the same construction stop being incidental.
//!
//! A coefficient is one bit, so a product by one is a conditional add:
//!
//! ```text
//! general alphabet -> d multiplications per point
//! bit alphabet -> the set bits, added
//! ```
//!
//! And the tensor element is a `d x d` bit matrix, one `EF` element per row:
//!
//! ```text
//! one byte per coefficient -> 16 KB at d = 128
//! one bit per coefficient -> 2 KB
//! ```
//!
//! That matters because the element crosses the wire, so it is held by rows.
//! The two readings of the matrix are then a transpose apart.
//!
//! # The pieces
//!
//! ```text
//! Coefficients the F_2-coordinates of one element
//! BitPacking a bit witness read as the multilinear a commitment holds
//! BitTensor an element of EF (x) EF, as a bit matrix
//! BitRingSwitch one reduction, before the batching draw
//! BitRingSwitchBatch the same reduction, after it
//! SuccessorTensors the two elements a successor view adds past one element's rows
//! BitRingSwitchClaims several claims at their own points, one sumcheck for all
//! ```
//!
//! The reduction owns the two sides that run it, as methods over its own transcript.
//! The module beside this one exposes free functions because it has no such type.
//!
//! Booleanity comes from the packing itself, not from the wrapper.
//! At a byte-aligned level a packed multilinear unpacks to one bit witness.
//!
//! The reduction is split where the protocol splits.
//! The batching challenge is drawn after the tensor element is bound.
//! A type taking it up front would invite the unsound order.
//!
//! # The basis
//!
//! A tower level may hold its elements in any `F_2`-basis.
//! This module fixes the one its byte representation already defines.
//! Coefficient `j` is bit `j` of the little-endian bytes, so `beta_0 = 1`.
//!
//! Nothing depends on which basis that is, only on both sides agreeing.
//! The payoff is that packing becomes a reinterpretation, not a computation.
pub use Coefficients;
pub use ;
pub use ;
pub use ;
pub use ;
pub use ;