binius_m3/builder/
table.rs

1// Copyright 2025 Irreducible Inc.
2
3use std::{ops::Index, sync::Arc};
4
5pub use binius_core::constraint_system::TableId;
6use binius_core::{
7	constraint_system::{
8		TableSizeSpec,
9		channel::{ChannelId, FlushDirection},
10	},
11	oracle::ShiftVariant,
12	transparent::MultilinearExtensionTransparent,
13};
14use binius_field::{
15	ExtensionField, TowerField,
16	arch::OptimalUnderlier,
17	as_packed_field::{PackScalar, PackedType},
18	packed::pack_slice,
19};
20use binius_math::ArithCircuit;
21use binius_utils::{
22	checked_arithmetics::{checked_log_2, log2_ceil_usize, log2_strict_usize},
23	sparse_index::SparseIndex,
24};
25
26use super::{
27	B1, ColumnIndex, ColumnPartitionIndex, FlushOpts,
28	channel::Flush,
29	column::{Col, ColumnDef, ColumnId, ColumnInfo, ColumnShape},
30	expr::{Expr, ZeroConstraint},
31	stat::TableStat,
32	structured::StructuredDynSize,
33	types::B128,
34	upcast_col,
35};
36
37#[derive(Debug)]
38pub struct TableBuilder<'a, F: TowerField = B128> {
39	namespace: Option<String>,
40	table: &'a mut Table<F>,
41}
42
43impl<'a, F: TowerField> TableBuilder<'a, F> {
44	/// Returns a new `TableBuilder` for the given table.
45	pub fn new(table: &'a mut Table<F>) -> Self {
46		Self {
47			namespace: None,
48			table,
49		}
50	}
51
52	/// Declares that the table's size must be a power of two.
53	///
54	/// The table's size is decided by the prover, but it must be a power of two.
55	///
56	/// ## Pre-conditions
57	///
58	/// This cannot be called if [`Self::require_power_of_two_size`] or
59	/// [`Self::require_fixed_size`] has already been called.
60	pub fn require_power_of_two_size(&mut self) {
61		assert!(matches!(self.table.table_size_spec, TableSizeSpec::Arbitrary));
62		self.table.table_size_spec = TableSizeSpec::PowerOfTwo;
63	}
64
65	/// Declares that the table's size must be a fixed power of two.
66	///
67	/// ## Pre-conditions
68	///
69	/// This cannot be called if [`Self::require_power_of_two_size`] or
70	/// [`Self::require_fixed_size`] has already been called.
71	pub fn require_fixed_size(&mut self, log_size: usize) {
72		assert!(matches!(self.table.table_size_spec, TableSizeSpec::Arbitrary));
73		self.table.table_size_spec = TableSizeSpec::Fixed { log_size };
74	}
75
76	/// Returns a new `TableBuilder` with the specified namespace.
77	///
78	/// A namespace is a prefix that will be prepended to all column names and zero constraints
79	/// created by this builder. The new namespace is nested within the current builder's namespace
80	/// (if any exists). When nesting namespaces, they are joined with "::" separators, creating a
81	/// hierarchical naming structure.
82	///
83	/// # Note
84	///
85	/// This method doesn't modify the original builder. It returns a new builder that shares
86	/// the underlying table but has its own namespace configuration that builds upon the
87	/// original builder's namespace.
88	///
89	/// # Examples
90	///
91	/// ```
92	/// # use binius_m3::builder::{B128, Col, Table, TableBuilder};
93	/// let mut table = Table::<B128>::new(0, "table");
94	/// let mut tb = TableBuilder::new(&mut table);
95	///
96	/// // Create a builder with namespace "arithmetic"
97	/// let mut arithmetic_tb = tb.with_namespace("arithmetic");
98	/// let add_col: Col<B128> = arithmetic_tb.add_committed("add"); // Column name: "arithmetic::add"
99	///
100	/// // Create a nested namespace "arithmetic::mul"
101	/// let mut mul_tb = arithmetic_tb.with_namespace("mul");
102	/// let result_col: Col<B128> = mul_tb.add_committed("result"); // Column name: "arithmetic::mul::result"
103	/// ```
104	pub fn with_namespace(&mut self, namespace: impl ToString) -> TableBuilder<'_, F> {
105		TableBuilder {
106			namespace: Some(self.namespaced_name(namespace)),
107			table: self.table,
108		}
109	}
110
111	/// Returns the [`TableId`] of the underlying table.
112	pub fn id(&self) -> TableId {
113		self.table.id()
114	}
115
116	pub fn add_committed<FSub, const VALUES_PER_ROW: usize>(
117		&mut self,
118		name: impl ToString,
119	) -> Col<FSub, VALUES_PER_ROW>
120	where
121		FSub: TowerField,
122		F: ExtensionField<FSub>,
123	{
124		self.table.new_column(
125			self.namespaced_name(name),
126			ColumnDef::Committed {
127				tower_level: FSub::TOWER_LEVEL,
128			},
129		)
130	}
131
132	pub fn add_committed_multiple<FSub, const VALUES_PER_ROW: usize, const N: usize>(
133		&mut self,
134		name: impl ToString,
135	) -> [Col<FSub, VALUES_PER_ROW>; N]
136	where
137		FSub: TowerField,
138		F: ExtensionField<FSub>,
139	{
140		std::array::from_fn(|i| self.add_committed(format!("{}[{}]", name.to_string(), i)))
141	}
142
143	pub fn add_shifted<FSub, const VALUES_PER_ROW: usize>(
144		&mut self,
145		name: impl ToString,
146		col: Col<FSub, VALUES_PER_ROW>,
147		log_block_size: usize,
148		offset: usize,
149		variant: ShiftVariant,
150	) -> Col<FSub, VALUES_PER_ROW>
151	where
152		FSub: TowerField,
153		F: ExtensionField<FSub>,
154	{
155		assert!(log_block_size <= log2_strict_usize(VALUES_PER_ROW));
156		assert!(offset <= 1 << log_block_size);
157		self.table.new_column(
158			self.namespaced_name(name),
159			ColumnDef::Shifted {
160				col: col.id(),
161				offset,
162				log_block_size,
163				variant,
164			},
165		)
166	}
167
168	pub fn add_packed<FSubSub, const VALUES_PER_ROW_SUB: usize, FSub, const VALUES_PER_ROW: usize>(
169		&mut self,
170		name: impl ToString,
171		col: Col<FSubSub, VALUES_PER_ROW_SUB>,
172	) -> Col<FSub, VALUES_PER_ROW>
173	where
174		FSub: TowerField + ExtensionField<FSubSub>,
175		FSubSub: TowerField,
176		F: ExtensionField<FSub>,
177	{
178		assert!(FSubSub::TOWER_LEVEL < FSub::TOWER_LEVEL);
179		assert!(VALUES_PER_ROW_SUB > VALUES_PER_ROW);
180		assert_eq!(
181			FSub::TOWER_LEVEL + log2_strict_usize(VALUES_PER_ROW),
182			FSubSub::TOWER_LEVEL + log2_strict_usize(VALUES_PER_ROW_SUB)
183		);
184		self.table.new_column(
185			self.namespaced_name(name),
186			ColumnDef::Packed {
187				col: col.id(),
188				log_degree: FSub::TOWER_LEVEL - FSubSub::TOWER_LEVEL,
189			},
190		)
191	}
192
193	/// Adds a derived column that is computed as an expression over other columns in the table.
194	///
195	/// The derived column has the same vertical stacking factor as the input columns and its
196	/// values are computed independently. The cost of the column's evaluations are proportional
197	/// to the polynomial degree of the expression. When the expression is linear, the column's
198	/// cost is minimal. When the expression is non-linear, the column is committed and the
199	/// expression is asserted to be zero against the committed column.
200	pub fn add_computed<FSub, const V: usize>(
201		&mut self,
202		name: impl ToString + Clone,
203		expr: Expr<FSub, V>,
204	) -> Col<FSub, V>
205	where
206		FSub: TowerField,
207		F: ExtensionField<FSub>,
208	{
209		if expr.degree() <= 1 {
210			let expr_circuit = ArithCircuit::from(expr.expr());
211			// Indices within the partition.
212			let indices_within_partition = expr_circuit
213				.vars_usage()
214				.iter()
215				.enumerate()
216				.filter(|(_, used)| **used)
217				.map(|(i, _)| i)
218				.collect::<Vec<_>>();
219			let partition = &self.table.partitions[partition_id::<V>()];
220			let cols = indices_within_partition
221				.iter()
222				.map(|&partition_index| partition.columns[partition_index])
223				.collect::<Vec<_>>();
224
225			let mut var_remapping = vec![0; expr_circuit.n_vars()];
226			for (new_index, &old_index) in indices_within_partition.iter().enumerate() {
227				var_remapping[old_index] = new_index;
228			}
229			let remapped_expr = expr_circuit
230				.convert_field()
231				.remap_vars(&var_remapping)
232				.expect("var_remapping should be large enough");
233
234			self.table.new_column(
235				self.namespaced_name(name),
236				ColumnDef::Computed {
237					cols,
238					expr: remapped_expr,
239				},
240			)
241		} else {
242			let col: Col<FSub, V> = self.add_committed(name.clone());
243			self.assert_zero(name, expr - col);
244			col
245		}
246	}
247
248	/// Add a derived column that selects a single value from a vertically stacked column.
249	///
250	/// The virtual column is derived from another column in the table passed as `col`, which we'll
251	/// call the "inner" column. The inner column has `V` values vertically stacked per table cell.
252	/// The `index` is in the range `0..V`, and it selects the `index`-th value from the inner
253	/// column.
254	pub fn add_selected<FSub, const V: usize>(
255		&mut self,
256		name: impl ToString,
257		col: Col<FSub, V>,
258		index: usize,
259	) -> Col<FSub, 1>
260	where
261		FSub: TowerField,
262		F: ExtensionField<FSub>,
263	{
264		assert!(index < V);
265		self.table.new_column(
266			self.namespaced_name(name),
267			ColumnDef::Selected {
268				col: col.id(),
269				index,
270				index_bits: log2_strict_usize(V),
271			},
272		)
273	}
274
275	/// Add a derived column that selects a subrange of values from a vertically stacked column.
276	///
277	/// The virtual column is derived from another column in the table passed as `col`, which we'll
278	/// call the "inner" column. The inner column has `V` values vertically stacked per table cell.
279	/// The `index` is in the range `0..(V - NEW_V)`, and it selects the values
280	/// `(i * NEW_V)..((i + 1) * NEW_V)` from the inner column.
281	pub fn add_selected_block<FSub, const V: usize, const NEW_V: usize>(
282		&mut self,
283		name: impl ToString,
284		col: Col<FSub, V>,
285		index: usize,
286	) -> Col<FSub, NEW_V>
287	where
288		FSub: TowerField,
289		F: ExtensionField<FSub>,
290	{
291		assert!(V.is_power_of_two());
292		assert!(NEW_V.is_power_of_two());
293		assert!(NEW_V < V);
294
295		let log_values_per_row = log2_strict_usize(V);
296		// This is also the value of the start_index.
297		let log_new_values_per_row = log2_strict_usize(NEW_V);
298		// Get the log size of the query.
299		let log_query_size = log_values_per_row - log_new_values_per_row;
300
301		self.table.new_column(
302			self.namespaced_name(name),
303			ColumnDef::Projected {
304				col: col.id(),
305				start_index: log_new_values_per_row,
306				query_size: log_query_size,
307				query_bits: index,
308			},
309		)
310	}
311
312	/// Given the representation at a tower level FSub (with `VALUES_PER_ROW` variables),
313	/// returns the representation at a higher tower level F (with `NEW_VALUES_PER_ROW` variables)
314	/// by left padding each FSub element with zeroes.
315	pub fn add_zero_pad_upcast<FSub, const VALUES_PER_ROW: usize, const NEW_VALUES_PER_ROW: usize>(
316		&mut self,
317		name: impl ToString,
318		col: Col<FSub, VALUES_PER_ROW>,
319	) -> Col<FSub, NEW_VALUES_PER_ROW>
320	where
321		FSub: TowerField,
322		F: ExtensionField<FSub>,
323	{
324		assert!(VALUES_PER_ROW.is_power_of_two());
325		assert!(NEW_VALUES_PER_ROW.is_power_of_two());
326		assert!(NEW_VALUES_PER_ROW > VALUES_PER_ROW);
327		let log_new_values_per_row = log2_strict_usize(NEW_VALUES_PER_ROW);
328		let log_values_per_row = log2_strict_usize(VALUES_PER_ROW);
329		let n_pad_vars = log_new_values_per_row - log_values_per_row;
330		let nonzero_index = (1 << n_pad_vars) - 1;
331		self.table.new_column(
332			self.namespaced_name(name),
333			ColumnDef::ZeroPadded {
334				col: col.id(),
335				n_pad_vars,
336				start_index: log_values_per_row,
337				nonzero_index,
338			},
339		)
340	}
341
342	/// Given the representation at a tower level FSub (with `VALUES_PER_ROW` variables),
343	/// returns the representation at a higher tower level F (with `NEW_VALUES_PER_ROW` variables).
344	/// This is done by keeping the `nonzero-index`-th FSub element, and setting all the others to
345	/// 0. Note that `0 <= nonzero_index < NEW_VALUES_PER_ROW / VALUES_PER_ROW`.
346	pub fn add_zero_pad<FSub, const VALUES_PER_ROW: usize, const NEW_VALUES_PER_ROW: usize>(
347		&mut self,
348		name: impl ToString,
349		col: Col<FSub, VALUES_PER_ROW>,
350		nonzero_index: usize,
351	) -> Col<FSub, NEW_VALUES_PER_ROW>
352	where
353		FSub: TowerField,
354		F: ExtensionField<FSub>,
355	{
356		assert!(VALUES_PER_ROW.is_power_of_two());
357		assert!(NEW_VALUES_PER_ROW.is_power_of_two());
358		assert!(NEW_VALUES_PER_ROW > VALUES_PER_ROW);
359		let log_new_values_per_row = log2_strict_usize(NEW_VALUES_PER_ROW);
360		let log_values_per_row = log2_strict_usize(VALUES_PER_ROW);
361		let n_pad_vars = log_new_values_per_row - log_values_per_row;
362		assert!(nonzero_index < 1 << n_pad_vars);
363
364		self.table.new_column(
365			self.namespaced_name(name),
366			ColumnDef::ZeroPadded {
367				col: col.id(),
368				n_pad_vars,
369				start_index: log_values_per_row,
370				nonzero_index,
371			},
372		)
373	}
374
375	/// Adds a column to the table with a constant cell value.
376	///
377	/// The cell is repeated for each row in the table, but the values stacked vertically within
378	/// the cell are not necessarily all equal.
379	pub fn add_constant<FSub, const V: usize>(
380		&mut self,
381		name: impl ToString,
382		constants: [FSub; V],
383	) -> Col<FSub, V>
384	where
385		FSub: TowerField,
386		F: ExtensionField<FSub>,
387		OptimalUnderlier: PackScalar<FSub> + PackScalar<F>,
388	{
389		let namespaced_name = self.namespaced_name(name);
390		let n_vars = log2_strict_usize(V);
391		let packed_values: Vec<PackedType<OptimalUnderlier, FSub>> = pack_slice(&constants);
392		let mle = MultilinearExtensionTransparent::<
393			PackedType<OptimalUnderlier, FSub>,
394			PackedType<OptimalUnderlier, F>,
395			_,
396		>::from_values_and_mu(packed_values, n_vars)
397		.unwrap();
398		self.table.new_column(
399			namespaced_name,
400			ColumnDef::Constant {
401				poly: Arc::new(mle),
402				data: constants.map(|f_sub| f_sub.into()).to_vec(),
403			},
404		)
405	}
406
407	/// Adds field exponentiation column with a fixed base
408	///
409	/// ## Parameters
410	/// - `name`: Name for the column
411	/// - `pow_bits`: The bits of exponent columns from LSB to MSB
412	/// - `base`: The base to exponentiate. The field used in exponentiation will be `FSub`
413	///
414	/// ## Preconditions
415	/// * `pow_bits.len()` must be less than or equal to the width of the field `FSub`
416	///
417	/// ## NOTE
418	/// * The witness generation for the return column will be done inside gkr_gpa *
419	pub fn add_static_exp<FExpBase>(
420		&mut self,
421		name: impl ToString,
422		pow_bits: &[Col<B1>],
423		base: FExpBase,
424	) -> Col<FExpBase>
425	where
426		FExpBase: TowerField,
427		F: ExtensionField<FExpBase>,
428	{
429		assert!(pow_bits.len() <= (1 << FExpBase::TOWER_LEVEL));
430
431		// TODO: Add check for F, FSub, VALUES_PER_ROW
432		let namespaced_name = self.namespaced_name(name);
433		let bit_cols = pow_bits
434			.iter()
435			.enumerate()
436			.map(|(index, bit)| {
437				assert_eq!(
438					self.table.id(),
439					bit.id().table_id,
440					"passed foreign table column at index={index}"
441				);
442				bit.id()
443			})
444			.collect();
445		self.table.new_column(
446			namespaced_name,
447			ColumnDef::StaticExp {
448				bit_cols,
449				base: base.into(),
450				base_tower_level: FExpBase::TOWER_LEVEL,
451			},
452		)
453	}
454
455	/// Adds field exponentiation column with a base from another column
456	///
457	/// ## Parameters
458	/// - `name`: Name for the column
459	/// - `pow_bits`: The bits of exponent columns from LSB to MSB
460	/// - `base`: The column of base to exponentiate. The field used in exponentiation will be
461	///   `FSub`
462	///
463	/// ## Preconditions
464	/// * `pow_bits.len()` must be less than or equal to the width of field `FSub`
465	///
466	/// ## NOTE
467	/// * The witness generation for the return column will be done inside gkr_gpa *
468	pub fn add_dynamic_exp<FExpBase>(
469		&mut self,
470		name: impl ToString,
471		pow_bits: &[Col<B1>],
472		base: Col<FExpBase>,
473	) -> Col<FExpBase>
474	where
475		FExpBase: TowerField,
476		F: ExtensionField<FExpBase>,
477	{
478		assert!(pow_bits.len() <= (1 << FExpBase::TOWER_LEVEL));
479
480		// TODO: Add check for F, FSub, VALUES_PER_ROW
481		let namespaced_name = self.namespaced_name(name);
482		let bit_cols = pow_bits
483			.iter()
484			.enumerate()
485			.map(|(index, bit)| {
486				assert_eq!(
487					self.table.id(),
488					bit.id().table_id,
489					"passed foreign table column at index={index}"
490				);
491				bit.id()
492			})
493			.collect();
494		self.table.new_column(
495			namespaced_name,
496			ColumnDef::DynamicExp {
497				bit_cols,
498				base: base.id(),
499				base_tower_level: FExpBase::TOWER_LEVEL,
500			},
501		)
502	}
503
504	/// Add a structured column to a table.
505	///
506	/// A structured column is one that has sufficient structure that its multilinear extension
507	/// can be evaluated succinctly. See [`StructuredDynSize`] for more information.
508	pub fn add_structured<FSub>(
509		&mut self,
510		name: impl ToString,
511		variant: StructuredDynSize,
512	) -> Col<FSub>
513	where
514		FSub: TowerField,
515		F: ExtensionField<FSub>,
516	{
517		assert!(
518			self.table.requires_any_po2_size(),
519			"Structured dynamic size columns may only be added to tables that are power of two sized"
520		);
521		let namespaced_name = self.namespaced_name(name);
522		self.table
523			.new_column(namespaced_name, ColumnDef::StructuredDynSize(variant))
524	}
525
526	/// Add a structured fixed-size column to a table.
527	pub fn add_fixed<FSub>(&mut self, name: impl ToString, expr: ArithCircuit<F>) -> Col<FSub>
528	where
529		FSub: TowerField,
530		F: ExtensionField<FSub>,
531	{
532		assert!(
533			matches!(self.table.table_size_spec, TableSizeSpec::Fixed { log_size } if log_size == expr.n_vars()),
534			"Structured fixed-size columns may only be added to tables with a fixed log_size that matches the n_vars of the expression"
535		);
536
537		let namespaced_name = self.namespaced_name(name);
538		self.table
539			.new_column(namespaced_name, ColumnDef::StructuredFixedSize { expr })
540	}
541
542	/// Constrains that an expression computed over the table columns is zero.
543	///
544	/// The zero constraint applies to all values stacked vertically within the column cells. That
545	/// means that the expression is evaluated independently `V` times per row, and each evaluation
546	/// in the stack must be zero.
547	pub fn assert_zero<FSub, const V: usize>(&mut self, name: impl ToString, expr: Expr<FSub, V>)
548	where
549		FSub: TowerField,
550		F: ExtensionField<FSub>,
551	{
552		let namespaced_name = self.namespaced_name(name);
553		self.table
554			.partition_mut(V)
555			.assert_zero(namespaced_name, expr)
556	}
557
558	/// Constrains that all values contained in this column are non-zero.
559	pub fn assert_nonzero<FSub, const V: usize>(&mut self, expr: Col<FSub, V>)
560	where
561		FSub: TowerField,
562		F: ExtensionField<FSub>,
563	{
564		assert_eq!(expr.table_id, self.id());
565		assert!(expr.table_index.0 < self.table.columns.len());
566
567		self.table.columns[expr.table_index.0].is_nonzero = true;
568	}
569
570	pub fn pull<FSub>(&mut self, channel: ChannelId, cols: impl IntoIterator<Item = Col<FSub>>)
571	where
572		FSub: TowerField,
573		F: ExtensionField<FSub>,
574	{
575		self.pull_with_opts(channel, cols, FlushOpts::default());
576	}
577
578	pub fn push<FSub>(&mut self, channel: ChannelId, cols: impl IntoIterator<Item = Col<FSub>>)
579	where
580		FSub: TowerField,
581		F: ExtensionField<FSub>,
582	{
583		self.push_with_opts(channel, cols, FlushOpts::default());
584	}
585
586	pub fn pull_with_opts<FSub>(
587		&mut self,
588		channel: ChannelId,
589		cols: impl IntoIterator<Item = Col<FSub>>,
590		opts: FlushOpts,
591	) where
592		FSub: TowerField,
593		F: ExtensionField<FSub>,
594	{
595		self.table.partition_mut(1).flush(
596			channel,
597			FlushDirection::Pull,
598			cols.into_iter().map(upcast_col),
599			opts,
600		);
601	}
602
603	pub fn push_with_opts<FSub>(
604		&mut self,
605		channel: ChannelId,
606		cols: impl IntoIterator<Item = Col<FSub>>,
607		opts: FlushOpts,
608	) where
609		FSub: TowerField,
610		F: ExtensionField<FSub>,
611	{
612		self.table.partition_mut(1).flush(
613			channel,
614			FlushDirection::Push,
615			cols.into_iter().map(upcast_col),
616			opts,
617		);
618	}
619
620	/// Reads a group of columns from a specified lookup table.
621	///
622	/// This method enforces that the values of the provided columns are obtained from a lookup
623	/// table through the specified lookup channel. The lookup channel identifies the target
624	/// table for retrieving values.
625	///
626	/// # Parameters
627	///
628	/// - `lookup_chan`: The channel ID that specifies the lookup table through which the values
629	///   will be constrained.
630	/// - `cols`: An iterable of columns (`Col`) that will be constrained based on the lookup
631	///   values.
632	///
633	/// # Type Parameters
634	///
635	/// - `FSub`: The field type used for the column values.
636	/// - `V`: The number of stacked values (vertical stacking factor) per cell of each column.
637	pub fn read<FSub, const V: usize>(
638		&mut self,
639		lookup_chan: ChannelId,
640		cols: impl IntoIterator<Item = Col<FSub, V>>,
641	) where
642		FSub: TowerField,
643		F: ExtensionField<FSub>,
644	{
645		let partition = self.table.partition_mut(V);
646		let columns = cols
647			.into_iter()
648			.map(|col| {
649				assert_eq!(col.table_id, partition.table_id);
650				col.id()
651			})
652			.collect();
653
654		partition.flushes.push(Flush {
655			columns,
656			channel_id: lookup_chan,
657			direction: FlushDirection::Pull,
658			multiplicity: 1,
659			selectors: vec![],
660		});
661	}
662
663	fn namespaced_name(&self, name: impl ToString) -> String {
664		let name = name.to_string();
665		match &self.namespace {
666			Some(namespace) => format!("{namespace}::{name}"),
667			None => name.to_string(),
668		}
669	}
670}
671
672/// A table in an M3 constraint system.
673///
674/// ## Invariants
675///
676/// * All expressions in `zero_constraints` have a number of variables less than or equal to the
677///   number of table columns (the length of `column_info`).
678/// * All flushes in `flushes` contain column indices less than the number of table columns (the
679///   length of `column_info`).
680#[derive(Debug)]
681pub struct Table<F: TowerField = B128> {
682	pub id: TableId,
683	pub name: String,
684	pub columns: Vec<ColumnInfo<F>>,
685	/// the size specification of a table
686	table_size_spec: TableSizeSpec,
687	pub(super) partitions: SparseIndex<TablePartition<F>>,
688}
689
690/// A table partition describes a part of a table where everything has the same pack factor (as well
691/// as height) Tower level does not need to be the same.
692///
693/// Zerocheck constraints can only be defined within table partitions.
694#[derive(Debug)]
695pub(super) struct TablePartition<F: TowerField = B128> {
696	pub table_id: TableId,
697	pub values_per_row: usize,
698	pub flushes: Vec<Flush>,
699	pub columns: Vec<ColumnId>,
700	pub zero_constraints: Vec<ZeroConstraint<F>>,
701}
702
703impl<F: TowerField> TablePartition<F> {
704	fn new(table_id: TableId, values_per_row: usize) -> Self {
705		Self {
706			table_id,
707			values_per_row,
708			flushes: Vec::new(),
709			columns: Vec::new(),
710			zero_constraints: Vec::new(),
711		}
712	}
713
714	fn assert_zero<FSub, const VALUES_PER_ROW: usize>(
715		&mut self,
716		name: impl ToString,
717		expr: Expr<FSub, VALUES_PER_ROW>,
718	) where
719		FSub: TowerField,
720		F: ExtensionField<FSub>,
721	{
722		self.zero_constraints.push(ZeroConstraint {
723			tower_level: FSub::TOWER_LEVEL,
724			name: name.to_string(),
725			expr: ArithCircuit::from(expr.expr()).convert_field(),
726		});
727	}
728
729	fn flush(
730		&mut self,
731		channel_id: ChannelId,
732		direction: FlushDirection,
733		cols: impl IntoIterator<Item = Col<F>>,
734		opts: FlushOpts,
735	) {
736		let columns = cols
737			.into_iter()
738			.map(|col| {
739				assert_eq!(col.table_id, self.table_id);
740				col.id()
741			})
742			.collect();
743		let selectors = opts
744			.selectors
745			.iter()
746			.map(|selector| {
747				assert_eq!(selector.table_id, self.table_id);
748				selector.id()
749			})
750			.collect::<Vec<_>>();
751		self.flushes.push(Flush {
752			columns,
753			channel_id,
754			direction,
755			multiplicity: opts.multiplicity,
756			selectors,
757		});
758	}
759}
760
761impl<F: TowerField> Table<F> {
762	pub fn new(id: TableId, name: impl ToString) -> Self {
763		Self {
764			id,
765			name: name.to_string(),
766			columns: Vec::new(),
767			table_size_spec: TableSizeSpec::Arbitrary,
768			partitions: SparseIndex::new(),
769		}
770	}
771
772	pub fn id(&self) -> TableId {
773		self.id
774	}
775
776	fn new_column<FSub, const V: usize>(
777		&mut self,
778		name: impl ToString,
779		col: ColumnDef<F>,
780	) -> Col<FSub, V>
781	where
782		FSub: TowerField,
783		F: ExtensionField<FSub>,
784	{
785		let table_id = self.id;
786		let table_index = ColumnIndex(self.columns.len());
787		let partition = self.partition_mut(V);
788		let id = ColumnId {
789			table_id,
790			table_index,
791		};
792		let info = ColumnInfo {
793			id,
794			col,
795			name: name.to_string(),
796			shape: ColumnShape {
797				tower_height: FSub::TOWER_LEVEL,
798				log_values_per_row: log2_strict_usize(V),
799			},
800			is_nonzero: false,
801		};
802
803		let partition_index = ColumnPartitionIndex(partition.columns.len());
804		partition.columns.push(id);
805		self.columns.push(info);
806		Col::new(id, partition_index)
807	}
808
809	fn partition_mut(&mut self, values_per_row: usize) -> &mut TablePartition<F> {
810		self.partitions
811			.entry(log2_strict_usize(values_per_row))
812			.or_insert_with(|| TablePartition::new(self.id, values_per_row))
813	}
814
815	/// Returns true if this table requires to have any power-of-two size.
816	pub fn requires_any_po2_size(&self) -> bool {
817		matches!(self.table_size_spec, TableSizeSpec::PowerOfTwo)
818	}
819
820	/// Returns the size constraint of this table.
821	pub(crate) fn size_spec(&self) -> TableSizeSpec {
822		self.table_size_spec
823	}
824
825	pub fn stat(&self) -> TableStat {
826		TableStat::new(self)
827	}
828}
829
830impl<F: TowerField> Index<ColumnIndex> for Table<F> {
831	type Output = ColumnInfo<F>;
832
833	fn index(&self, index: ColumnIndex) -> &Self::Output {
834		&self.columns[index.0]
835	}
836}
837
838impl<F: TowerField> Index<ColumnId> for Table<F> {
839	type Output = ColumnInfo<F>;
840
841	fn index(&self, index: ColumnId) -> &Self::Output {
842		assert_eq!(index.table_id, self.id());
843		&self.columns[index.table_index.0]
844	}
845}
846
847const fn partition_id<const V: usize>() -> usize {
848	checked_log_2(V)
849}
850
851/// Returns the binary logarithm of the table capacity required to accommodate the given number
852/// of rows.
853///
854/// The table capacity must be a power of two (in order to be compatible with the multilinear
855/// proof system, which associates each table index with a vertex of a boolean hypercube).
856/// This is be the next power of two greater than the table size.
857pub fn log_capacity(table_size: usize) -> usize {
858	log2_ceil_usize(table_size)
859}
860
861#[cfg(test)]
862mod tests {
863	use binius_compute::cpu::alloc::CpuComputeAllocator;
864	use binius_field::{arch::OptimalUnderlier, as_packed_field::PackedType};
865
866	use super::{B128, Table, TableBuilder};
867	use crate::builder::{
868		B8, ConstraintSystem, FlushOpts, WitnessIndex,
869		test_utils::validate_system_witness_with_prove_verify,
870	};
871
872	#[test]
873	fn namespace_nesting() {
874		let mut table = Table::<B128>::new(0, "table");
875		let mut tb = TableBuilder::new(&mut table);
876		let mut tb_ns_1 = tb.with_namespace("ns1");
877		let tb_ns_2 = tb_ns_1.with_namespace("ns2");
878		assert_eq!(tb_ns_2.namespaced_name("column"), "ns1::ns2::column");
879	}
880
881	// Test that the `read` method works correctly.
882	#[test]
883	fn test_read_method() {
884		let mut cs = ConstraintSystem::<B128>::new();
885		let lookup_chan = cs.add_channel("lookup");
886		let mut read_table = cs.add_table("stacked_reads");
887		let read_table_id = read_table.id();
888		const LOG_STACKING_FACTOR: usize = 3;
889		const LOG_READ_TABLE_SIZE: usize = 3;
890		let read_col =
891			read_table.add_constant("constant_reads", [B8::new(3); 1 << LOG_STACKING_FACTOR]);
892		read_table.require_fixed_size(LOG_READ_TABLE_SIZE);
893
894		read_table.read(lookup_chan, [read_col]);
895		drop(read_table);
896		let mut write_table = cs.add_table("packed_write");
897		let write_table_id = write_table.id();
898		write_table.require_fixed_size(LOG_READ_TABLE_SIZE);
899		let write_col = write_table.add_constant("constant_writes", [B8::new(3)]);
900		write_table.push_with_opts(
901			lookup_chan,
902			[write_col],
903			FlushOpts {
904				multiplicity: 1 << LOG_STACKING_FACTOR as u32,
905				selectors: vec![],
906			},
907		);
908
909		let mut allocator = CpuComputeAllocator::new(1 << 12);
910		let alloc = allocator.into_bump_allocator();
911		let mut witness: WitnessIndex<PackedType<OptimalUnderlier, B128>> =
912			WitnessIndex::new(&cs, &alloc);
913		witness
914			.init_table(read_table_id, 1 << LOG_READ_TABLE_SIZE)
915			.unwrap();
916		witness
917			.init_table(write_table_id, 1 << LOG_READ_TABLE_SIZE)
918			.unwrap();
919		witness.fill_constant_cols().unwrap();
920
921		let boundaries = vec![];
922
923		// We only want to validate the channel balancing
924		validate_system_witness_with_prove_verify::<OptimalUnderlier>(
925			&cs, witness, boundaries, false,
926		);
927	}
928}
binius_m3/builder/table.rs

binius_m3/builder/
table.rs
