table-aware constraint system

This is the last PR in the series that implements
[CRY-363: Table-Aware Constraint System](https://linear.app/irreducible/issue/CRY-363/table-aware-constraint-system)

In this PR we introduce a structure called SymbolicMultilinearOracleSet. This
structure is very similar to MultilinearOracleSet with the exception that it
does not have any information about the sizes (n_vars) of the declared
multilinears.

This symbolic representation is what defines the ConstraintSystem, instead of
the concrete one. That, and other changes in this PR, make constraint system
serialization independent of the sizes of tables.

This PR avoids making large changes to the proving path and to achieve that I
decided to take the strategy in which the multilinears for zero-sized tables
are not created at all.

Author: pepyakin

crates/core/src/constraint_system/channel.rs

@@ -129,9 +129,8 @@ where
 			ref selectors,
 			multiplicity,
 			table_id,
-			log_values_per_row,
+			log_values_per_row: _,
 		} = flush;
-		let _ = log_values_per_row;
 
 		if channel_id > max_channel_id {
 			return Err(Error::ChannelIdOutOfRange {
@@ -141,6 +140,9 @@ where
 		}
 
 		let table_size = table_sizes[table_id];
+		if table_size == 0 {
+			continue;
+		}
 
 		// We check the variables only of OracleOrConst::Oracle variant oracles being the same.
 		let non_const_polys = oracles

crates/core/src/constraint_system/mod.rs

@@ -20,7 +20,7 @@ use exp::Exp;
 pub use prove::prove;
 pub use verify::verify;
 
-use crate::oracle::{ConstraintSet, MultilinearOracleSet, OracleId};
+use crate::oracle::{ConstraintSet, OracleId, SymbolicMultilinearOracleSet};
 
 /// Contains the 3 things that place constraints on witness data in Binius
 /// - virtual oracles
@@ -32,7 +32,7 @@ use crate::oracle::{ConstraintSet, MultilinearOracleSet, OracleId};
 #[derive(Debug, Clone, SerializeBytes, DeserializeBytes)]
 #[deserialize_bytes(eval_generics(F = BinaryField128b))]
 pub struct ConstraintSystem<F: TowerField> {
-	pub oracles: MultilinearOracleSet<F>,
+	pub oracles: SymbolicMultilinearOracleSet<F>,
 	pub table_constraints: Vec<ConstraintSet<F>>,
 	pub non_zero_oracle_ids: Vec<OracleId>,
 	pub flushes: Vec<Flush<F>>,

crates/core/src/constraint_system/prove.rs

@@ -108,11 +108,11 @@ where
 	let fast_domain_factory = IsomorphicEvaluationDomainFactory::<FFastExt<Tower>>::default();
 
 	let ConstraintSystem {
-		mut oracles,
+		oracles,
 		table_constraints,
 		mut flushes,
 		mut exponents,
-		non_zero_oracle_ids,
+		mut non_zero_oracle_ids,
 		channel_count,
 		table_size_specs,
 	} = constraint_system.clone();
@@ -155,6 +155,33 @@ where
 	let mut writer = transcript.message();
 	writer.write_slice(table_sizes);
 
+	let mut oracles = oracles.instantiate(table_sizes)?;
+
+	// Prepare the constraint system for proving:
+	//
+	// - Trim all the zero sized oracles.
+	// - Canonicalize the ordering.
+
+	flushes.retain(|flush| table_sizes[flush.table_id] > 0);
+	flushes.sort_by_key(|flush| flush.channel_id);
+
+	non_zero_oracle_ids.retain(|oracle| !oracles.is_zero_sized(*oracle));
+	exponents.retain(|exp| !oracles.is_zero_sized(exp.exp_result_id));
+
+	let mut table_constraints = table_constraints
+		.into_iter()
+		.filter_map(|u| {
+			if table_sizes[u.table_id] == 0 {
+				None
+			} else {
+				let n_vars = u.log_values_per_row + log2_ceil_usize(table_sizes[u.table_id]);
+				Some(SizedConstraintSet::new(n_vars, u))
+			}
+		})
+		.collect::<Vec<_>>();
+	// Stable sort constraint sets in ascending order by number of variables.
+	table_constraints.sort_by_key(|constraint_set| constraint_set.n_vars);
+
 	reorder_exponents(&mut exponents, &oracles);
 
 	let witness_span = tracing::info_span!(
@@ -177,20 +204,6 @@ where
 
 	drop(witness_span);
 
-	let mut table_constraints = table_constraints
-		.into_iter()
-		.filter_map(|u| {
-			if table_sizes[u.table_id] == 0 {
-				None
-			} else {
-				let n_vars = u.log_values_per_row + log2_ceil_usize(table_sizes[u.table_id]);
-				Some(SizedConstraintSet::new(n_vars, u))
-			}
-		})
-		.collect::<Vec<_>>();
-	// Stable sort constraint sets in ascending order by number of variables.
-	table_constraints.sort_by_key(|constraint_set| constraint_set.n_vars);
-
 	// Commit polynomials
 	let merkle_prover = BinaryMerkleTreeProver::<_, Hash, _>::new(Compress::default());
 	let merkle_scheme = merkle_prover.scheme();

crates/core/src/constraint_system/validate.rs

@@ -12,6 +12,7 @@ use super::{
 	error::Error,
 };
 use crate::{
+	constraint_system::TableSizeSpec,
 	oracle::{
 		ConstraintPredicate, MultilinearOracleSet, MultilinearPolyOracle, MultilinearPolyVariant,
 		ShiftVariant,
@@ -31,8 +32,58 @@ where
 	P: PackedField<Scalar = F> + PackedExtension<BinaryField1b>,
 	F: TowerField,
 {
+	let ConstraintSystem {
+		oracles,
+		table_constraints,
+		non_zero_oracle_ids,
+		flushes,
+		channel_count,
+		table_size_specs,
+		exponents: _,
+	} = constraint_system;
+
+	if table_sizes.len() != table_size_specs.len() {
+		return Err(Error::TableSizesLenMismatch {
+			expected: table_size_specs.len(),
+			got: table_sizes.len(),
+		});
+	}
+	for (table_id, (&table_size, table_size_spec)) in
+		table_sizes.iter().zip(table_size_specs.iter()).enumerate()
+	{
+		match table_size_spec {
+			TableSizeSpec::PowerOfTwo => {
+				if !table_size.is_power_of_two() {
+					return Err(Error::TableSizePowerOfTwoRequired {
+						table_id,
+						size: table_size,
+					});
+				}
+			}
+			TableSizeSpec::Fixed { log_size } => {
+				if table_size != 1 << log_size {
+					return Err(Error::TableSizeFixedRequired {
+						table_id,
+						size: table_size,
+					});
+				}
+			}
+			TableSizeSpec::Arbitrary => (),
+		}
+	}
+
+	let unsized_oracles = oracles;
+	let oracles = unsized_oracles.instantiate(table_sizes)?;
+
 	// Check the constraint sets
-	for constraint_set in &constraint_system.table_constraints {
+	for constraint_set in table_constraints {
+		if table_sizes[constraint_set.table_id] == 0 {
+			continue;
+		}
+		if constraint_set.oracle_ids.is_empty() {
+			continue;
+		}
+
 		let multilinears = constraint_set
 			.oracle_ids
 			.iter()
@@ -56,25 +107,15 @@ where
 	}
 
 	// Check that nonzero oracles are non-zero over the entire hypercube
-	nonzerocheck::validate_witness(
-		witness,
-		&constraint_system.oracles,
-		&constraint_system.non_zero_oracle_ids,
-	)?;
+	nonzerocheck::validate_witness(witness, &oracles, non_zero_oracle_ids)?;
 
 	// Check that the channels balance with flushes and boundaries
-	channel::validate_witness(
-		witness,
-		&constraint_system.flushes,
-		boundaries,
-		table_sizes,
-		constraint_system.channel_count,
-	)?;
+	channel::validate_witness(witness, flushes, boundaries, table_sizes, *channel_count)?;
 
 	// Check consistency of virtual oracle witnesses (eg. that shift polynomials are actually
 	// shifts).
-	for oracle in constraint_system.oracles.polys() {
-		validate_virtual_oracle_witness(oracle, &constraint_system.oracles, witness)?;
+	for oracle in oracles.polys() {
+		validate_virtual_oracle_witness(oracle, &oracles, witness)?;
 	}
 
 	Ok(())
@@ -321,6 +362,9 @@ pub mod nonzerocheck {
 		F: TowerField,
 	{
 		oracle_ids.into_par_iter().try_for_each(|id| {
+			if oracles.is_zero_sized(*id) {
+				return Ok(());
+			}
 			let multilinear = witness.get_multilin_poly(*id)?;
 			(0..(1 << multilinear.n_vars()))
 				.into_par_iter()

crates/core/src/constraint_system/verify.rs

@@ -59,12 +59,11 @@ where
 	Compress: PseudoCompressionFunction<Output<Hash>, 2> + Default + Sync,
 	Challenger_: Challenger + Default,
 {
-	let _ = constraint_system_digest;
 	let ConstraintSystem {
-		mut oracles,
+		oracles,
 		table_constraints,
 		mut flushes,
-		non_zero_oracle_ids,
+		mut non_zero_oracle_ids,
 		channel_count,
 		mut exponents,
 		table_size_specs,
@@ -107,6 +106,14 @@ where
 		}
 	}
 
+	let mut oracles = oracles.instantiate(&table_sizes)?;
+
+	flushes.retain(|flush| table_sizes[flush.table_id] > 0);
+	flushes.sort_by_key(|flush| flush.channel_id);
+
+	non_zero_oracle_ids.retain(|oracle| !oracles.is_zero_sized(*oracle));
+	exponents.retain(|exp| !oracles.is_zero_sized(exp.exp_result_id));
+
 	let mut table_constraints = table_constraints
 		.into_iter()
 		.filter_map(|u| {

crates/core/src/oracle/constraint.rs

@@ -63,7 +63,6 @@ impl<F: Field> SizedConstraintSet<F> {
 pub struct ConstraintSet<F: Field> {
 	pub table_id: TableId,
 	pub log_values_per_row: usize,
-	pub n_vars: usize,
 	pub oracle_ids: Vec<OracleId>,
 	pub constraints: Vec<Constraint<F>>,
 }

crates/core/src/oracle/error.rs

@@ -1,6 +1,6 @@
 // Copyright 2024-2025 Irreducible Inc.
 
-use crate::oracle::OracleId;
+use crate::{constraint_system::TableId, oracle::OracleId};
 
 #[derive(Debug, thiserror::Error)]
 pub enum Error {
@@ -32,4 +32,6 @@ pub enum Error {
 		"expected constraint set to contain only constraints with n_vars={expected}, but found n_vars={got}"
 	)]
 	ConstraintSetNvarsMismatch { got: usize, expected: usize },
+	#[error("table size for table {table_id} is missing")]
+	TableSizeMissing { table_id: TableId },
 }

crates/core/src/oracle/mod.rs

@@ -11,9 +11,11 @@ mod constraint;
 mod error;
 mod multilinear;
 mod oracle_id;
+mod symbolic;
 
 pub use composite::*;
 pub use constraint::*;
 pub use error::Error;
 pub use multilinear::*;
 pub use oracle_id::*;
+pub use symbolic::*;

crates/core/src/oracle/multilinear.rs

@@ -353,32 +353,42 @@ impl<F: TowerField> MultilinearOracleSetAddition<'_, F> {
 #[derive(Default, Debug, Clone, SerializeBytes, DeserializeBytes)]
 #[deserialize_bytes(eval_generics(F = BinaryField128b))]
 pub struct MultilinearOracleSet<F: TowerField> {
-	oracles: Vec<MultilinearPolyOracle<F>>,
+	/// The vector of oracles.
+	///
+	/// During sizing, an oracle could be skipped. In which case, the entry corresponding to the
+	/// oracle will be `None`.
+	oracles: Vec<Option<MultilinearPolyOracle<F>>>,
+	/// The number of non-`None` entries in `oracles`.
+	size: usize,
 }
 
 impl<F: TowerField> MultilinearOracleSet<F> {
 	pub const fn new() -> Self {
 		Self {
 			oracles: Vec::new(),
+			size: 0,
 		}
 	}
 
 	pub fn size(&self) -> usize {
-		self.oracles.len()
+		self.size
 	}
 
 	pub fn polys(&self) -> impl Iterator<Item = &MultilinearPolyOracle<F>> + '_ {
-		(0..self.oracles.len()).map(|index| &self[OracleId::from_index(index)])
+		self.iter().map(|(_, poly)| poly)
 	}
 
 	pub fn ids(&self) -> impl Iterator<Item = OracleId> {
-		(0..self.oracles.len()).map(OracleId::from_index)
+		self.iter().map(|(id, _)| id)
 	}
 
 	pub fn iter(&self) -> impl Iterator<Item = (OracleId, &MultilinearPolyOracle<F>)> + '_ {
-		(0..self.oracles.len()).map(|index| {
-			let oracle_id = OracleId::from_index(index);
-			(oracle_id, &self[oracle_id])
+		(0..self.oracles.len()).filter_map(|index| match self.oracles[index] {
+			Some(ref oracle) => {
+				let oracle_id = OracleId::from_index(index);
+				Some((oracle_id, oracle))
+			}
+			None => None,
 		})
 	}
 
@@ -400,15 +410,23 @@ impl<F: TowerField> MultilinearOracleSet<F> {
 		id.index() < self.oracles.len()
 	}
 
-	fn add_to_set(
+	pub(crate) fn add_to_set(
 		&mut self,
 		oracle: impl FnOnce(OracleId) -> MultilinearPolyOracle<F>,
 	) -> OracleId {
 		let id = OracleId::from_index(self.oracles.len());
-		self.oracles.push(oracle(id));
+		self.oracles.push(Some(oracle(id)));
+		self.size += 1;
 		id
 	}
 
+	/// Instead of adding a concrete oracle adds a skip mark, essentially just reserving an
+	/// [`OracleId`]. Accessing such oracle, with some exceptions, is an error.
+	pub(crate) fn add_skip(&mut self) {
+		self.oracles.push(None);
+		// don't increment size
+	}
+
 	pub fn add_transparent(
 		&mut self,
 		poly: impl MultivariatePoly<F> + 'static,
@@ -515,13 +533,21 @@ impl<F: TowerField> MultilinearOracleSet<F> {
 	pub fn tower_level(&self, id: OracleId) -> usize {
 		self[id].binary_tower_level()
 	}
+
+	/// Returns `true` if the given [`OracleId`] refers to an oracle that was skipped during the
+	/// instantiation of the symbolic multilinear oracle set.
+	pub fn is_zero_sized(&self, id: OracleId) -> bool {
+		self.oracles[id.index()].is_none()
+	}
 }
 
 impl<F: TowerField> std::ops::Index<OracleId> for MultilinearOracleSet<F> {
 	type Output = MultilinearPolyOracle<F>;
 
 	fn index(&self, id: OracleId) -> &Self::Output {
-		&self.oracles[id.index()]
+		self.oracles[id.index()]
+			.as_ref()
+			.expect("tried to access skipped oracle")
 	}
 }