binius_core/constraint_system/
constraint.rs

1// Copyright 2025 Irreducible Inc.
2use std::array;
3
4use binius_utils::serialization::{DeserializeBytes, SerializationError, SerializeBytes};
5use bytes::{Buf, BufMut};
6
7use super::{ShiftedValueIndex, ValueIndex};
8
9/// Operand type.
10///
11/// An operand in Binius64 is a vector of shifted values. Each item in the vector represents a
12/// term in a XOR combination of shifted values.
13///
14/// To give a couple examples:
15///
16/// ```ignore
17/// vec![] == 0
18/// vec![1] == 1
19/// vec![1, 1] == 1 ^ 1
20/// vec![x >> 5, y << 5] = (x >> 5) ^ (y << 5)
21/// ```
22pub type Operand = Vec<ShiftedValueIndex>;
23
24/// Number of operands of an [`AndConstraint`].
25const AND_ARITY: usize = 3;
26/// Number of operands of an [`ImulConstraint`].
27const IMUL_ARITY: usize = 4;
28/// Number of operands of a [`BmulConstraint`].
29const BMUL_ARITY: usize = 6;
30
31/// Serializes the operands of a constraint in storage order.
32fn serialize_operands(
33	operands: &[Operand],
34	mut write_buf: impl BufMut,
35) -> Result<(), SerializationError> {
36	for operand in operands {
37		operand.serialize(&mut write_buf)?;
38	}
39	Ok(())
40}
41
42/// Deserializes the operands of a constraint of the given arity in storage order.
43fn deserialize_operands<const ARITY: usize>(
44	mut read_buf: impl Buf,
45) -> Result<[Operand; ARITY], SerializationError> {
46	let mut operands = array::from_fn::<_, ARITY, _>(|_| Operand::new());
47	for operand in &mut operands {
48		*operand = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
49	}
50	Ok(operands)
51}
52
53/// AND constraint: `A & B = C`.
54///
55/// This constraint verifies that the bitwise AND of operands A and B equals operand C.
56/// Each operand is computed as the XOR of multiple shifted values from the value vector.
57///
58/// The operands are stored in the order given by [`AndConstraint::OPERAND_NAMES`].
59#[derive(Debug, Clone, Default)]
60pub struct AndConstraint(pub [Operand; AND_ARITY]);
61
62impl AndConstraint {
63	/// Number of operands.
64	pub const ARITY: usize = AND_ARITY;
65	/// Names of the operands, in storage order.
66	pub const OPERAND_NAMES: [&'static str; AND_ARITY] = ["a", "b", "c"];
67
68	/// Creates a new AND constraint from XOR combinations of the given unshifted values.
69	pub fn plain_abc(
70		a: impl IntoIterator<Item = ValueIndex>,
71		b: impl IntoIterator<Item = ValueIndex>,
72		c: impl IntoIterator<Item = ValueIndex>,
73	) -> AndConstraint {
74		AndConstraint::abc(
75			a.into_iter().map(ShiftedValueIndex::plain),
76			b.into_iter().map(ShiftedValueIndex::plain),
77			c.into_iter().map(ShiftedValueIndex::plain),
78		)
79	}
80
81	/// Creates a new AND constraint from XOR combinations of the given shifted values.
82	pub fn abc(
83		a: impl IntoIterator<Item = ShiftedValueIndex>,
84		b: impl IntoIterator<Item = ShiftedValueIndex>,
85		c: impl IntoIterator<Item = ShiftedValueIndex>,
86	) -> AndConstraint {
87		AndConstraint([
88			a.into_iter().collect(),
89			b.into_iter().collect(),
90			c.into_iter().collect(),
91		])
92	}
93
94	/// Operand A.
95	pub const fn a(&self) -> &Operand {
96		&self.0[0]
97	}
98
99	/// Operand B.
100	pub const fn b(&self) -> &Operand {
101		&self.0[1]
102	}
103
104	/// Operand C.
105	pub const fn c(&self) -> &Operand {
106		&self.0[2]
107	}
108}
109
110impl AsRef<[Operand; AND_ARITY]> for AndConstraint {
111	fn as_ref(&self) -> &[Operand; AND_ARITY] {
112		&self.0
113	}
114}
115
116impl SerializeBytes for AndConstraint {
117	fn serialize(&self, write_buf: impl BufMut) -> Result<(), SerializationError> {
118		serialize_operands(&self.0, write_buf)
119	}
120}
121
122impl DeserializeBytes for AndConstraint {
123	fn deserialize(read_buf: impl Buf) -> Result<Self, SerializationError>
124	where
125		Self: Sized,
126	{
127		Ok(AndConstraint(deserialize_operands(read_buf)?))
128	}
129}
130
131/// IMUL constraint: `A * B = (HI << 64) | LO`.
132///
133/// 64-bit unsigned integer multiplication producing 128-bit result split into high and low 64-bit
134/// words.
135///
136/// The operands are stored in the order given by [`ImulConstraint::OPERAND_NAMES`].
137#[derive(Debug, Clone, Default)]
138pub struct ImulConstraint(pub [Operand; IMUL_ARITY]);
139
140impl ImulConstraint {
141	/// Number of operands.
142	pub const ARITY: usize = IMUL_ARITY;
143	/// Names of the operands, in storage order.
144	pub const OPERAND_NAMES: [&'static str; IMUL_ARITY] = ["a", "b", "lo", "hi"];
145
146	/// A operand.
147	pub const fn a(&self) -> &Operand {
148		&self.0[0]
149	}
150
151	/// B operand.
152	pub const fn b(&self) -> &Operand {
153		&self.0[1]
154	}
155
156	/// LO operand.
157	///
158	/// The low 64 bits of the result of the multiplication.
159	pub const fn lo(&self) -> &Operand {
160		&self.0[2]
161	}
162
163	/// HI operand.
164	///
165	/// The high 64 bits of the result of the multiplication.
166	pub const fn hi(&self) -> &Operand {
167		&self.0[3]
168	}
169}
170
171impl AsRef<[Operand; IMUL_ARITY]> for ImulConstraint {
172	fn as_ref(&self) -> &[Operand; IMUL_ARITY] {
173		&self.0
174	}
175}
176
177impl SerializeBytes for ImulConstraint {
178	fn serialize(&self, write_buf: impl BufMut) -> Result<(), SerializationError> {
179		serialize_operands(&self.0, write_buf)
180	}
181}
182
183impl DeserializeBytes for ImulConstraint {
184	fn deserialize(read_buf: impl Buf) -> Result<Self, SerializationError>
185	where
186		Self: Sized,
187	{
188		Ok(ImulConstraint(deserialize_operands(read_buf)?))
189	}
190}
191
192/// BMUL constraint: `A * B = C` in the GHASH field `GF(2^128)`.
193///
194/// Multiplication of two GHASH binary-field elements. Because a field element spans 128 bits while
195/// a word holds only 64, each operand is carried by a pair of words: the `lo` word supplies the low
196/// 64 coefficients (of `1, X, ..., X^63`) and the `hi` word the high 64 (of `X^64, ..., X^127`).
197///
198/// The operands are stored in the order given by [`BmulConstraint::OPERAND_NAMES`].
199#[derive(Debug, Clone, Default)]
200pub struct BmulConstraint(pub [Operand; BMUL_ARITY]);
201
202impl BmulConstraint {
203	/// Number of operands.
204	pub const ARITY: usize = BMUL_ARITY;
205	/// Names of the operands, in storage order.
206	pub const OPERAND_NAMES: [&'static str; BMUL_ARITY] =
207		["a_lo", "a_hi", "b_lo", "b_hi", "c_lo", "c_hi"];
208
209	/// Low word of the A operand.
210	pub const fn a_lo(&self) -> &Operand {
211		&self.0[0]
212	}
213
214	/// High word of the A operand.
215	pub const fn a_hi(&self) -> &Operand {
216		&self.0[1]
217	}
218
219	/// Low word of the B operand.
220	pub const fn b_lo(&self) -> &Operand {
221		&self.0[2]
222	}
223
224	/// High word of the B operand.
225	pub const fn b_hi(&self) -> &Operand {
226		&self.0[3]
227	}
228
229	/// Low word of the C (product) operand.
230	pub const fn c_lo(&self) -> &Operand {
231		&self.0[4]
232	}
233
234	/// High word of the C (product) operand.
235	pub const fn c_hi(&self) -> &Operand {
236		&self.0[5]
237	}
238}
239
240impl AsRef<[Operand; BMUL_ARITY]> for BmulConstraint {
241	fn as_ref(&self) -> &[Operand; BMUL_ARITY] {
242		&self.0
243	}
244}
245
246impl SerializeBytes for BmulConstraint {
247	fn serialize(&self, write_buf: impl BufMut) -> Result<(), SerializationError> {
248		serialize_operands(&self.0, write_buf)
249	}
250}
251
252impl DeserializeBytes for BmulConstraint {
253	fn deserialize(read_buf: impl Buf) -> Result<Self, SerializationError>
254	where
255		Self: Sized,
256	{
257		Ok(BmulConstraint(deserialize_operands(read_buf)?))
258	}
259}
260
261#[cfg(test)]
262mod tests {
263	use super::*;
264
265	#[test]
266	fn test_and_constraint_serialization_round_trip() {
267		let constraint = AndConstraint::abc(
268			vec![ShiftedValueIndex::sll(ValueIndex(1), 5)],
269			vec![ShiftedValueIndex::srl(ValueIndex(2), 10)],
270			vec![
271				ShiftedValueIndex::sar(ValueIndex(3), 15),
272				ShiftedValueIndex::plain(ValueIndex(4)),
273			],
274		);
275
276		let mut buf = Vec::new();
277		constraint.serialize(&mut buf).unwrap();
278
279		let deserialized = AndConstraint::deserialize(&mut buf.as_slice()).unwrap();
280		assert_eq!(constraint.a().len(), deserialized.a().len());
281		assert_eq!(constraint.b().len(), deserialized.b().len());
282		assert_eq!(constraint.c().len(), deserialized.c().len());
283
284		for (orig, deser) in constraint.a().iter().zip(deserialized.a().iter()) {
285			assert_eq!(orig.value_index, deser.value_index);
286			assert_eq!(orig.amount, deser.amount);
287		}
288	}
289
290	#[test]
291	fn test_imul_constraint_serialization_round_trip() {
292		let constraint = ImulConstraint([
293			vec![ShiftedValueIndex::plain(ValueIndex(0))],
294			vec![ShiftedValueIndex::srl(ValueIndex(1), 32)],
295			vec![ShiftedValueIndex::plain(ValueIndex(2))],
296			vec![ShiftedValueIndex::plain(ValueIndex(3))],
297		]);
298
299		let mut buf = Vec::new();
300		constraint.serialize(&mut buf).unwrap();
301
302		let deserialized = ImulConstraint::deserialize(&mut buf.as_slice()).unwrap();
303		assert_eq!(constraint.a().len(), deserialized.a().len());
304		assert_eq!(constraint.b().len(), deserialized.b().len());
305		assert_eq!(constraint.lo().len(), deserialized.lo().len());
306		assert_eq!(constraint.hi().len(), deserialized.hi().len());
307	}
308
309	#[test]
310	fn test_bmul_constraint_serialization_round_trip() {
311		let constraint = BmulConstraint([
312			vec![ShiftedValueIndex::plain(ValueIndex(0))],
313			vec![ShiftedValueIndex::srl(ValueIndex(1), 32)],
314			vec![ShiftedValueIndex::plain(ValueIndex(2))],
315			vec![ShiftedValueIndex::sll(ValueIndex(3), 5)],
316			vec![ShiftedValueIndex::plain(ValueIndex(4))],
317			vec![
318				ShiftedValueIndex::sar(ValueIndex(5), 15),
319				ShiftedValueIndex::plain(ValueIndex(6)),
320			],
321		]);
322
323		let mut buf = Vec::new();
324		constraint.serialize(&mut buf).unwrap();
325
326		let deserialized = BmulConstraint::deserialize(&mut buf.as_slice()).unwrap();
327		assert_eq!(constraint.a_lo().len(), deserialized.a_lo().len());
328		assert_eq!(constraint.a_hi().len(), deserialized.a_hi().len());
329		assert_eq!(constraint.b_lo().len(), deserialized.b_lo().len());
330		assert_eq!(constraint.b_hi().len(), deserialized.b_hi().len());
331		assert_eq!(constraint.c_lo().len(), deserialized.c_lo().len());
332		assert_eq!(constraint.c_hi().len(), deserialized.c_hi().len());
333	}
334}
binius_core/constraint_system/constraint.rs

binius_core/constraint_system/
constraint.rs
