binius_core/constraint_system/
constraint.rs

1// Copyright 2025 Irreducible Inc.
2use binius_utils::serialization::{DeserializeBytes, SerializationError, SerializeBytes};
3use bytes::{Buf, BufMut};
4
5use super::{ShiftedValueIndex, ValueIndex};
6
7/// Operand type.
8///
9/// An operand in Binius64 is a vector of shifted values. Each item in the vector represents a
10/// term in a XOR combination of shifted values.
11///
12/// To give a couple examples:
13///
14/// ```ignore
15/// vec![] == 0
16/// vec![1] == 1
17/// vec![1, 1] == 1 ^ 1
18/// vec![x >> 5, y << 5] = (x >> 5) ^ (y << 5)
19/// ```
20pub type Operand = Vec<ShiftedValueIndex>;
21
22/// AND constraint: `A & B = C`.
23///
24/// This constraint verifies that the bitwise AND of operands A and B equals operand C.
25/// Each operand is computed as the XOR of multiple shifted values from the value vector.
26#[derive(Debug, Clone, Default)]
27pub struct AndConstraint {
28	/// Operand A.
29	pub a: Operand,
30	/// Operand B.
31	pub b: Operand,
32	/// Operand C.
33	pub c: Operand,
34}
35
36impl AndConstraint {
37	/// Creates a new AND constraint from XOR combinations of the given unshifted values.
38	pub fn plain_abc(
39		a: impl IntoIterator<Item = ValueIndex>,
40		b: impl IntoIterator<Item = ValueIndex>,
41		c: impl IntoIterator<Item = ValueIndex>,
42	) -> AndConstraint {
43		AndConstraint {
44			a: a.into_iter().map(ShiftedValueIndex::plain).collect(),
45			b: b.into_iter().map(ShiftedValueIndex::plain).collect(),
46			c: c.into_iter().map(ShiftedValueIndex::plain).collect(),
47		}
48	}
49
50	/// Creates a new AND constraint from XOR combinations of the given shifted values.
51	pub fn abc(
52		a: impl IntoIterator<Item = ShiftedValueIndex>,
53		b: impl IntoIterator<Item = ShiftedValueIndex>,
54		c: impl IntoIterator<Item = ShiftedValueIndex>,
55	) -> AndConstraint {
56		AndConstraint {
57			a: a.into_iter().collect(),
58			b: b.into_iter().collect(),
59			c: c.into_iter().collect(),
60		}
61	}
62}
63
64impl SerializeBytes for AndConstraint {
65	fn serialize(&self, mut write_buf: impl BufMut) -> Result<(), SerializationError> {
66		self.a.serialize(&mut write_buf)?;
67		self.b.serialize(&mut write_buf)?;
68		self.c.serialize(write_buf)
69	}
70}
71
72impl DeserializeBytes for AndConstraint {
73	fn deserialize(mut read_buf: impl Buf) -> Result<Self, SerializationError>
74	where
75		Self: Sized,
76	{
77		let a = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
78		let b = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
79		let c = Vec::<ShiftedValueIndex>::deserialize(read_buf)?;
80
81		Ok(AndConstraint { a, b, c })
82	}
83}
84
85/// MUL constraint: `A * B = (HI << 64) | LO`.
86///
87/// 64-bit unsigned integer multiplication producing 128-bit result split into high and low 64-bit
88/// words.
89#[derive(Debug, Clone, Default)]
90pub struct MulConstraint {
91	/// A operand.
92	pub a: Operand,
93	/// B operand.
94	pub b: Operand,
95	/// HI operand.
96	///
97	/// The high 64 bits of the result of the multiplication.
98	pub hi: Operand,
99	/// LO operand.
100	///
101	/// The low 64 bits of the result of the multiplication.
102	pub lo: Operand,
103}
104
105impl SerializeBytes for MulConstraint {
106	fn serialize(&self, mut write_buf: impl BufMut) -> Result<(), SerializationError> {
107		self.a.serialize(&mut write_buf)?;
108		self.b.serialize(&mut write_buf)?;
109		self.hi.serialize(&mut write_buf)?;
110		self.lo.serialize(write_buf)
111	}
112}
113
114impl DeserializeBytes for MulConstraint {
115	fn deserialize(mut read_buf: impl Buf) -> Result<Self, SerializationError>
116	where
117		Self: Sized,
118	{
119		let a = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
120		let b = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
121		let hi = Vec::<ShiftedValueIndex>::deserialize(&mut read_buf)?;
122		let lo = Vec::<ShiftedValueIndex>::deserialize(read_buf)?;
123
124		Ok(MulConstraint { a, b, hi, lo })
125	}
126}
127
128#[cfg(test)]
129mod tests {
130	use super::*;
131
132	#[test]
133	fn test_and_constraint_serialization_round_trip() {
134		let constraint = AndConstraint::abc(
135			vec![ShiftedValueIndex::sll(ValueIndex(1), 5)],
136			vec![ShiftedValueIndex::srl(ValueIndex(2), 10)],
137			vec![
138				ShiftedValueIndex::sar(ValueIndex(3), 15),
139				ShiftedValueIndex::plain(ValueIndex(4)),
140			],
141		);
142
143		let mut buf = Vec::new();
144		constraint.serialize(&mut buf).unwrap();
145
146		let deserialized = AndConstraint::deserialize(&mut buf.as_slice()).unwrap();
147		assert_eq!(constraint.a.len(), deserialized.a.len());
148		assert_eq!(constraint.b.len(), deserialized.b.len());
149		assert_eq!(constraint.c.len(), deserialized.c.len());
150
151		for (orig, deser) in constraint.a.iter().zip(deserialized.a.iter()) {
152			assert_eq!(orig.value_index, deser.value_index);
153			assert_eq!(orig.amount, deser.amount);
154		}
155	}
156
157	#[test]
158	fn test_mul_constraint_serialization_round_trip() {
159		let constraint = MulConstraint {
160			a: vec![ShiftedValueIndex::plain(ValueIndex(0))],
161			b: vec![ShiftedValueIndex::srl(ValueIndex(1), 32)],
162			hi: vec![ShiftedValueIndex::plain(ValueIndex(2))],
163			lo: vec![ShiftedValueIndex::plain(ValueIndex(3))],
164		};
165
166		let mut buf = Vec::new();
167		constraint.serialize(&mut buf).unwrap();
168
169		let deserialized = MulConstraint::deserialize(&mut buf.as_slice()).unwrap();
170		assert_eq!(constraint.a.len(), deserialized.a.len());
171		assert_eq!(constraint.b.len(), deserialized.b.len());
172		assert_eq!(constraint.hi.len(), deserialized.hi.len());
173		assert_eq!(constraint.lo.len(), deserialized.lo.len());
174	}
175}
binius_core/constraint_system/constraint.rs

binius_core/constraint_system/
constraint.rs
