binius_circuits/bignum/
reduce.rs

1// Copyright 2025 Irreducible Inc.
2use binius_core::word::Word;
3use binius_frontend::{CircuitBuilder, Wire};
4
5use super::{
6	addsub::{add, sub},
7	biguint::{BigUint, assert_eq, assert_eq_cond},
8	mul::{optimal_mul, textbook_mul},
9};
10
11/// Modular reduction verification for BigUint.
12///
13/// This circuit verifies that:
14///
15/// a = quotient * modulus + remainder
16pub struct ModReduce {
17	pub a: BigUint,
18	pub modulus: BigUint,
19	pub quotient: BigUint,
20	pub remainder: BigUint,
21}
22
23impl ModReduce {
24	/// Creates a new modular reduction verifier circuit.
25	///
26	/// # Arguments
27	/// * `builder` - Circuit builder for constraint generation
28	/// * `a` - The dividend
29	/// * `modulus` - The divisor
30	/// * `quotient` - The quotient
31	/// * `remainder` - The remainder
32	///
33	/// # Constraints
34	/// The circuit enforces that `a = quotient * modulus + remainder`
35	pub fn new(
36		builder: &CircuitBuilder,
37		a: BigUint,
38		modulus: BigUint,
39		quotient: BigUint,
40		remainder: BigUint,
41	) -> Self {
42		let zero = builder.add_constant(Word::ZERO);
43
44		let product = optimal_mul(builder, &quotient, &modulus);
45
46		let remainder_padded = remainder.pad_limbs_to(product.limbs.len(), zero);
47		let reconstructed = add(builder, &product, &remainder_padded);
48
49		let n_limbs = reconstructed.limbs.len().max(a.limbs.len());
50		assert_eq(
51			builder,
52			"modreduce_a_eq_reconstructed",
53			&reconstructed.pad_limbs_to(n_limbs, zero),
54			&a.pad_limbs_to(n_limbs, zero),
55		);
56
57		ModReduce {
58			a,
59			modulus,
60			quotient,
61			remainder,
62		}
63	}
64}
65
66/// Modular reduction verification for BigUint for pseudo Mersenne moduli.
67///
68/// This circuit verifies that:
69///
70/// a = quotient * (2^modulus_po2 - modulus_subtrahend) + remainder
71///
72/// where modulus_po2 is additionally restricted to be a multiple of limb size to only
73/// split BigUint at limb boundaries.
74///
75/// This algorithm is more efficient than `ModReduce` when `modulus_subtrahend` is a short
76/// compared to `modulus_po2`. This is the case for many practically interesting prime field.
77pub struct PseudoMersenneModReduce {
78	lhs: BigUint,
79	rhs: BigUint,
80}
81
82impl PseudoMersenneModReduce {
83	/// Creates a new pseudo Mersenne modular reduction verifier circuit.
84	///
85	/// # Arguments
86	/// * `builder` - Circuit builder for constraint generation
87	/// * `a` - The dividend
88	/// * `modulus_po2` - the power of two modulus minuend (has to be a multiple of `Word::BITS`)
89	/// * `modulus_subtrahend` - the value subtracted form `2^modulus_po2` to obtain modulus
90	/// * `quotient` - The quotient
91	/// * `remainder` - The remainder
92	///
93	/// # Constraints
94	/// The circuit enforces that `a = quotient * (2^modulus_po2 - modulus_subtrahend) + remainder`.
95	/// Remainder range check (`0 <= remainder < 2^modulus_po2 - modulus_subtrahend`) is _not_
96	/// enforced.
97	///
98	/// Note: This adds arithmetic constraints for computing intermediate values
99	/// (multiplication, addition, subtraction), but does NOT add the final equality
100	/// constraint. You must call `.constrain()` or `.constrain_cond()` to enforce
101	/// that the equation actually holds.
102	#[must_use]
103	pub fn new(
104		builder: &CircuitBuilder,
105		a: &BigUint,
106		modulus_po2: usize,
107		modulus_subtrahend: &BigUint,
108		quotient: &BigUint,
109		remainder: &BigUint,
110	) -> Self {
111		// a = quotient * (2^modulus_po2 - modulus_subtrahend) + remainder
112		// hi * 2^modulus_po2 + lo = quotient * (2^modulus_po2 - modulus_subtrahend) + remainder
113		// lo + quotient * modulus_subtrahend = remainder + 2^modulus_po2 * (quotient - hi)
114		// max(lo, remainder) < 2^modulus_po2
115		// quotient < |a/(2^modulus_po2 - modulus_subtrahend)|
116		// quotient >= hi
117		assert!(modulus_po2.is_multiple_of(Word::BITS));
118		assert!(modulus_subtrahend.limbs.len() * Word::BITS <= modulus_po2);
119		assert!(remainder.limbs.len() * Word::BITS <= modulus_po2);
120
121		let zero = builder.add_constant(Word::ZERO);
122
123		let n_lo_limbs = modulus_po2 / Word::BITS;
124
125		let (a_lo, a_hi) = a.pad_limbs_to(n_lo_limbs, zero).split_at_limbs(n_lo_limbs);
126
127		let rhs_hi = sub(builder, quotient, &a_hi.pad_limbs_to(quotient.limbs.len(), zero));
128		let rhs = remainder
129			.pad_limbs_to(n_lo_limbs, zero)
130			.concat_limbs(&rhs_hi);
131
132		let quotient_modulus_subtrahend = textbook_mul(builder, quotient, modulus_subtrahend);
133		let lhs_rhs_len = [
134			rhs.limbs.len(),
135			quotient_modulus_subtrahend.limbs.len() + 1,
136			a_lo.limbs.len() + 1,
137		]
138		.into_iter()
139		.max()
140		.expect("exactly 3 elements");
141
142		let lhs = add(
143			builder,
144			&a_lo.pad_limbs_to(lhs_rhs_len, zero),
145			&quotient_modulus_subtrahend.pad_limbs_to(lhs_rhs_len, zero),
146		);
147
148		let rhs = rhs.pad_limbs_to(lhs_rhs_len, zero);
149
150		Self { lhs, rhs }
151	}
152
153	/// Apply the reduction constraint unconditionally.
154	pub fn constrain(self, builder: &CircuitBuilder) {
155		assert_eq(builder, "modreduce_pseudo_mersenne", &self.lhs, &self.rhs);
156	}
157
158	/// Apply the reduction constraint conditionally based on the value of boolean `mask` wire.
159	pub fn constrain_cond(self, builder: &CircuitBuilder, cond: Wire) {
160		assert_eq_cond(builder, "modred_pseudo_mersenne", &self.lhs, &self.rhs, cond);
161	}
162}
binius_circuits/bignum/reduce.rs

binius_circuits/bignum/
reduce.rs
