binius_core/constraint_system/value_table.rs
1// Copyright 2026 The Binius Developers
2
3use std::ops::Deref;
4
5use super::{ValueIndex, ValueVec, ValueVecLayout};
6use crate::word::Word;
7
8/// The witness for a batch of `2^k` independent instances of one circuit, in wire-major order.
9///
10/// Each wire's values across all instances are grouped together, one wire per row (wire-major):
11///
12/// ```text
13/// instance 0 instance 1 ... instance K-1
14/// wire 0 [ w | w | ... | w ] <- one row
15/// wire 1 [ w | w | ... | w ]
16/// ...
17/// ```
18///
19/// Each row is one wire and each column is one instance.
20/// So a batched interpreter can advance every instance of a wire in a single pass.
21///
22/// This is the batched counterpart of [`ValueVec`]: one instance read back out with
23/// [`Self::instance_value_vec`] is bit-for-bit the value vector populating that instance on its own
24/// would produce.
25///
26/// This table is specialized for the M4 accelerator setting, where the value vector splits with
27/// the inout values on the hidden side ([`InoutSegment::Hidden`](super::InoutSegment::Hidden)):
28///
29/// 1. **Inout wires are committed.** Every instance chooses its own inout words, so they are not
30/// one set of shared values a verifier can evaluate. They are committed with the private values
31/// instead, at the front of the hidden segment.
32/// 2. **Constants are not stored.** The constants live once on the constraint system as a
33/// `Vec<Word>`, not replicated per instance. Only the hidden segment — the inout, witness and
34/// internal words — is stored here. Reading an instance back takes the constants as an argument.
35///
36/// So the stored data holds exactly the hidden segment of every instance: `n_hidden_words` rows by
37/// `2^log_instances` columns.
38///
39/// The committed inout words are not tied to any value the verifier knows, so the statement a
40/// proof over this table makes is that *some* inout values complete every instance.
41///
42/// Populating one is the circuit frontend's business, since it takes a circuit to evaluate — see
43/// `Circuit::populate_batch`.
44///
45/// `Data` is the buffer backing the words. It defaults to [`Vec<Word>`], but the prover populates
46/// a table straight into a buffer drawn from its pool, so any `Deref<Target = [Word]>` will do.
47#[derive(Clone, Debug)]
48pub struct ValueTable<Data = Vec<Word>> {
49 /// The per-instance value layout, shared by every instance in the batch.
50 layout: ValueVecLayout,
51 /// The base-2 logarithm of the instance count.
52 log_instances: usize,
53 /// The number of hidden-word rows the proving protocol commits per instance.
54 ///
55 /// This is the inout values followed by the private ones, which is
56 /// [`ConstraintSystem::n_hidden_words`](super::ConstraintSystem::n_hidden_words) under
57 /// [`InoutSegment::Hidden`](super::InoutSegment::Hidden).
58 n_hidden_words: usize,
59 /// The hidden words of every wire, in wire-major order.
60 ///
61 /// Row `r` (for `r` in `0..n_hidden_words`) holds the `2^log_instances` values of hidden wire
62 /// `r` — inout value `r`, then private value `r - n_inout` — one per instance. The rows are
63 /// laid out contiguously, so the length is `n_hidden_words << log_instances`.
64 data: Data,
65}
66
67impl<Data: Deref<Target = [Word]>> ValueTable<Data> {
68 /// Builds a table from the hidden words of every instance, in wire-major order.
69 ///
70 /// `data` is what [`Self::as_words`] returns: the rows of the hidden segment laid out
71 /// contiguously, each holding one wire's value in every instance. The row count follows from
72 /// the layout, so it is not passed separately.
73 ///
74 /// This is the seam the frontend populates through; nothing in this crate can evaluate a
75 /// circuit to produce the words.
76 ///
77 /// # Panics
78 ///
79 /// Panics if `data` is not `n_hidden_words << log_instances` words long.
80 pub fn from_hidden_words(layout: ValueVecLayout, log_instances: usize, data: Data) -> Self {
81 let n_hidden_words = layout.combined_len() - layout.offset_inout();
82 assert_eq!(
83 data.len(),
84 n_hidden_words << log_instances,
85 "the data must hold one row per hidden word, one column per instance"
86 );
87 Self {
88 layout,
89 log_instances,
90 n_hidden_words,
91 data,
92 }
93 }
94
95 /// The base-2 logarithm of the number of instances.
96 pub const fn log_instances(&self) -> usize {
97 self.log_instances
98 }
99
100 /// The number of instances in the batch.
101 pub const fn n_instances(&self) -> usize {
102 1usize << self.log_instances
103 }
104
105 /// The per-instance value layout shared by every instance.
106 pub const fn layout(&self) -> &ValueVecLayout {
107 &self.layout
108 }
109
110 /// The number of hidden-word rows per instance, including the protocol's zero padding.
111 pub const fn n_hidden_words(&self) -> usize {
112 self.n_hidden_words
113 }
114
115 /// The whole batch as one flat, wire-major word buffer.
116 ///
117 /// Row `r` (hidden wire `r`) occupies `data[r << log_instances .. (r + 1) << log_instances]`,
118 /// holding that wire's value in every instance.
119 pub fn as_words(&self) -> &[Word] {
120 &self.data
121 }
122
123 /// Reconstructs one instance as a standalone single-instance value vector.
124 ///
125 /// Because the constants are not stored in the table, the caller supplies them (they live on
126 /// the constraint system). The result is bit-for-bit what populating this instance on its own
127 /// would produce, so it can be fed directly to single-instance constraint checking.
128 ///
129 /// # Panics
130 ///
131 /// Panics if the index is not below the instance count, or if `constants` does not match the
132 /// layout's constant count.
133 pub fn instance_value_vec(&self, instance: usize, constants: &[Word]) -> ValueVec {
134 assert!(instance < self.n_instances(), "instance index out of range");
135 assert_eq!(
136 constants.len(),
137 self.layout.n_const,
138 "constants length must match the layout's constant count"
139 );
140
141 // The constants are the whole public segment; the table stores everything after them.
142 let mut values = ValueVec::new(&self.layout);
143 for (i, &constant) in constants.iter().enumerate() {
144 values[ValueIndex::constant(i as u32)] = constant;
145 }
146
147 // Gather this instance's column of hidden values across every row, which the value vector
148 // holds from the first inout word onwards.
149 for row in 0..self.n_hidden_words {
150 *values.word_mut((self.layout.offset_inout() + row) as u32) =
151 self.data[(row << self.log_instances) + instance];
152 }
153
154 values
155 }
156}
157
158#[cfg(test)]
159mod tests {
160 use super::*;
161
162 /// A layout of one constant, two inout values and one private value.
163 fn layout() -> ValueVecLayout {
164 ValueVecLayout {
165 n_const: 1,
166 n_inout: 2,
167 n_witness: 1,
168 n_internal: 0,
169 n_scratch: 0,
170 }
171 }
172
173 /// A two-instance table whose hidden word `r` holds `0x10 * r + instance`.
174 fn table() -> ValueTable {
175 let n_hidden_words = layout().combined_len() - layout().offset_inout();
176 let data = (0..n_hidden_words)
177 .flat_map(|row| {
178 (0..2).map(move |instance| Word::from_u64(0x10 * row as u64 + instance))
179 })
180 .collect();
181 ValueTable::from_hidden_words(layout(), 1, data)
182 }
183
184 #[test]
185 fn the_row_count_follows_from_the_layout() {
186 let table = table();
187 assert_eq!(table.log_instances(), 1);
188 assert_eq!(table.n_instances(), 2);
189 // Three hidden words: two inout values and one private one.
190 assert_eq!(table.n_hidden_words(), 3);
191 assert_eq!(table.as_words().len(), 6);
192 }
193
194 #[test]
195 #[should_panic(expected = "one row per hidden word")]
196 fn a_buffer_of_the_wrong_length_is_rejected() {
197 ValueTable::from_hidden_words(layout(), 1, vec![Word::ZERO; 5]);
198 }
199
200 // An instance is the column at its index, behind the constants the table does not store.
201 #[test]
202 fn an_instance_reads_back_as_its_own_column() {
203 let table = table();
204 let constants = [Word::from_u64(0xc0)];
205
206 for instance in 0..2 {
207 let values = table.instance_value_vec(instance, &constants);
208 assert_eq!(values[ValueIndex::constant(0)], constants[0]);
209 assert_eq!(values[ValueIndex::inout(0)], Word::from_u64(instance as u64));
210 assert_eq!(values[ValueIndex::inout(1)], Word::from_u64(0x10 + instance as u64));
211 assert_eq!(values[ValueIndex::private(0)], Word::from_u64(0x20 + instance as u64));
212 }
213 }
214
215 #[test]
216 #[should_panic(expected = "instance index out of range")]
217 fn reading_past_the_last_instance_panics() {
218 table().instance_value_vec(2, &[Word::from_u64(0xc0)]);
219 }
220
221 #[test]
222 #[should_panic(expected = "constants length must match")]
223 fn the_wrong_number_of_constants_is_rejected() {
224 table().instance_value_vec(0, &[]);
225 }
226}