halo2_axiom/plonk/circuit/compress_selectors.rs
1use super::Expression;
2use ff::Field;
3
4/// This describes a selector and where it is activated.
5#[derive(Debug, Clone)]
6pub struct SelectorDescription {
7 /// The selector that this description references, by index.
8 pub selector: usize,
9
10 /// The vector of booleans defining which rows are active for this selector.
11 pub activations: Vec<bool>,
12
13 /// The maximum degree of a gate involving this selector, including the
14 /// virtual selector itself. This means this will be at least 1 for any
15 /// expression containing a simple selector, even if that selector is not
16 /// multiplied by anything.
17 pub max_degree: usize,
18}
19
20/// This describes the assigned combination of a particular selector as well as
21/// the expression it should be substituted with.
22#[derive(Debug, Clone)]
23pub struct SelectorAssignment<F> {
24 /// The selector that this structure references, by index.
25 pub selector: usize,
26
27 /// The combination this selector was assigned to
28 pub combination_index: usize,
29
30 /// The expression we wish to substitute with
31 pub expression: Expression<F>,
32}
33
34/// This function takes a vector that defines each selector as well as a closure
35/// used to allocate new fixed columns, and returns the assignment of each
36/// combination as well as details about each selector assignment.
37///
38/// This function takes
39/// * `selectors`, a vector of `SelectorDescription`s that describe each
40/// selector
41/// * `max_degree`, the maximum allowed degree of any gate
42/// * `allocate_fixed_columns`, a closure that constructs a new fixed column and
43/// queries it at Rotation::cur(), returning the expression
44///
45/// and returns `Vec<Vec<F>>` containing the assignment of each new fixed column
46/// (which each correspond to a combination) as well as a vector of
47/// `SelectorAssignment` that the caller can use to perform the necessary
48/// substitutions to the constraint system.
49///
50/// This function is completely deterministic.
51pub fn process<F: Field, E>(
52 mut selectors: Vec<SelectorDescription>,
53 max_degree: usize,
54 mut allocate_fixed_column: E,
55) -> (Vec<Vec<F>>, Vec<SelectorAssignment<F>>)
56where
57 E: FnMut() -> Expression<F>,
58{
59 if selectors.is_empty() {
60 // There is nothing to optimize.
61 return (vec![], vec![]);
62 }
63
64 // The length of all provided selectors must be the same.
65 let n = selectors[0].activations.len();
66 assert!(selectors.iter().all(|a| a.activations.len() == n));
67
68 let mut combination_assignments = vec![];
69 let mut selector_assignments = vec![];
70
71 // All provided selectors of degree 0 are assumed to be either concrete
72 // selectors or do not appear in a gate. Let's address these first.
73 selectors.retain(|selector| {
74 if selector.max_degree == 0 {
75 // This is a complex selector, or a selector that does not appear in any
76 // gate constraint.
77 let expression = allocate_fixed_column();
78
79 let combination_assignment = selector
80 .activations
81 .iter()
82 .map(|b| if *b { F::ONE } else { F::ZERO })
83 .collect::<Vec<_>>();
84 let combination_index = combination_assignments.len();
85 combination_assignments.push(combination_assignment);
86 selector_assignments.push(SelectorAssignment {
87 selector: selector.selector,
88 combination_index,
89 expression,
90 });
91
92 false
93 } else {
94 true
95 }
96 });
97
98 // All of the remaining `selectors` are simple. Let's try to combine them.
99 // First, we compute the exclusion matrix that has (j, k) = true if selector
100 // j and selector k conflict -- that is, they are both enabled on the same
101 // row. This matrix is symmetric and the diagonal entries are false, so we
102 // only need to store the lower triangular entries.
103 let mut exclusion_matrix = (0..selectors.len())
104 .map(|i| vec![false; i])
105 .collect::<Vec<_>>();
106
107 for (i, rows) in selectors
108 .iter()
109 .map(|selector| &selector.activations)
110 .enumerate()
111 {
112 // Loop over the selectors previous to this one
113 for (j, other_selector) in selectors.iter().enumerate().take(i) {
114 // Look at what selectors are active at the same row
115 if rows
116 .iter()
117 .zip(other_selector.activations.iter())
118 .any(|(l, r)| l & r)
119 {
120 // Mark them as incompatible
121 exclusion_matrix[i][j] = true;
122 }
123 }
124 }
125
126 // Simple selectors that we've added to combinations already.
127 let mut added = vec![false; selectors.len()];
128
129 for (i, selector) in selectors.iter().enumerate() {
130 if added[i] {
131 continue;
132 }
133 added[i] = true;
134 assert!(selector.max_degree <= max_degree);
135 // This is used to keep track of the largest degree gate involved in the
136 // combination so far. We subtract by one to omit the virtual selector
137 // which will be substituted by the caller with the expression we give
138 // them.
139 let mut d = selector.max_degree - 1;
140 let mut combination = vec![selector];
141 let mut combination_added = vec![i];
142
143 // Try to find other selectors that can join this one.
144 'try_selectors: for (j, selector) in selectors.iter().enumerate().skip(i + 1) {
145 if d + combination.len() == max_degree {
146 // Short circuit; nothing can be added to this
147 // combination.
148 break 'try_selectors;
149 }
150
151 // Skip selectors that have been added to previous combinations
152 if added[j] {
153 continue 'try_selectors;
154 }
155
156 // Is this selector excluded from co-existing in the same
157 // combination with any of the other selectors so far?
158 for &i in combination_added.iter() {
159 if exclusion_matrix[j][i] {
160 continue 'try_selectors;
161 }
162 }
163
164 // Can the new selector join the combination? Reminder: we use
165 // selector.max_degree - 1 to omit the influence of the virtual
166 // selector on the degree, as it will be substituted.
167 let new_d = std::cmp::max(d, selector.max_degree - 1);
168 if new_d + combination.len() + 1 > max_degree {
169 // Guess not.
170 continue 'try_selectors;
171 }
172
173 d = new_d;
174 combination.push(selector);
175 combination_added.push(j);
176 added[j] = true;
177 }
178
179 // Now, compute the selector and combination assignments.
180 let mut combination_assignment = vec![F::ZERO; n];
181 let combination_len = combination.len();
182 let combination_index = combination_assignments.len();
183 let query = allocate_fixed_column();
184
185 let mut assigned_root = F::ONE;
186 selector_assignments.extend(combination.into_iter().map(|selector| {
187 // Compute the expression for substitution. This produces an expression of the
188 // form
189 // q * Prod[i = 1..=combination_len, i != assigned_root](i - q)
190 //
191 // which is non-zero only on rows where `combination_assignment` is set to
192 // `assigned_root`. In particular, rows set to 0 correspond to all selectors
193 // being disabled.
194 let mut expression = query.clone();
195 let mut root = F::ONE;
196 for _ in 0..combination_len {
197 if root != assigned_root {
198 expression = expression * (Expression::Constant(root) - query.clone());
199 }
200 root += F::ONE;
201 }
202
203 // Update the combination assignment
204 for (combination, selector) in combination_assignment
205 .iter_mut()
206 .zip(selector.activations.iter())
207 {
208 // This will not overwrite another selector's activations because
209 // we have ensured that selectors are disjoint.
210 if *selector {
211 *combination = assigned_root;
212 }
213 }
214
215 assigned_root += F::ONE;
216
217 SelectorAssignment {
218 selector: selector.selector,
219 combination_index,
220 expression,
221 }
222 }));
223 combination_assignments.push(combination_assignment);
224 }
225
226 (combination_assignments, selector_assignments)
227}
228
229#[cfg(test)]
230mod tests {
231 use super::*;
232 use crate::{plonk::FixedQuery, poly::Rotation};
233 use halo2curves::pasta::Fp;
234 use proptest::collection::{vec, SizeRange};
235 use proptest::prelude::*;
236
237 prop_compose! {
238 fn arb_selector(assignment_size: usize, max_degree: usize)
239 (degree in 0..max_degree,
240 assignment in vec(any::<bool>(), assignment_size))
241 -> (usize, Vec<bool>) {
242 (degree, assignment)
243 }
244 }
245
246 prop_compose! {
247 fn arb_selector_list(assignment_size: usize, max_degree: usize, num_selectors: impl Into<SizeRange>)
248 (list in vec(arb_selector(assignment_size, max_degree), num_selectors))
249 -> Vec<SelectorDescription>
250 {
251 list.into_iter().enumerate().map(|(i, (max_degree, activations))| {
252 SelectorDescription {
253 selector: i,
254 activations,
255 max_degree,
256 }
257 }).collect()
258 }
259 }
260
261 prop_compose! {
262 fn arb_instance(max_assignment_size: usize,
263 max_degree: usize,
264 max_selectors: usize)
265 (assignment_size in 1..max_assignment_size,
266 degree in 1..max_degree,
267 num_selectors in 1..max_selectors)
268 (list in arb_selector_list(assignment_size, degree, num_selectors),
269 degree in Just(degree))
270 -> (Vec<SelectorDescription>, usize)
271 {
272 (list, degree)
273 }
274 }
275
276 proptest! {
277 #![proptest_config(ProptestConfig::with_cases(10000))]
278 #[test]
279 fn test_selector_combination((selectors, max_degree) in arb_instance(10, 10, 15)) {
280 let mut query = 0;
281 let (combination_assignments, selector_assignments) =
282 process::<Fp, _>(selectors.clone(), max_degree, || {
283 let tmp = Expression::Fixed(FixedQuery {
284 index: Some(query),
285 column_index: query,
286 rotation: Rotation::cur(),
287 });
288 query += 1;
289 tmp
290 });
291
292 {
293 let mut selectors_seen = vec![];
294 assert_eq!(selectors.len(), selector_assignments.len());
295 for selector in &selector_assignments {
296 // Every selector should be assigned to a combination
297 assert!(selector.combination_index < combination_assignments.len());
298 assert!(!selectors_seen.contains(&selector.selector));
299 selectors_seen.push(selector.selector);
300 }
301 }
302
303 // Test that, for each selector, the provided expression
304 // 1. evaluates to zero on rows where the selector's activation is off
305 // 2. evaluates to nonzero on rows where the selector's activation is on
306 // 3. is of degree d such that d + (selector.max_degree - 1) <= max_degree
307 // OR selector.max_degree is zero
308 for selector in selector_assignments {
309 assert_eq!(
310 selectors[selector.selector].activations.len(),
311 combination_assignments[selector.combination_index].len()
312 );
313 for (&activation, &assignment) in selectors[selector.selector]
314 .activations
315 .iter()
316 .zip(combination_assignments[selector.combination_index].iter())
317 {
318 let eval = selector.expression.evaluate(
319 &|c| c,
320 &|_| panic!("should not occur in returned expressions"),
321 &|query| {
322 // Should be the correct combination in the expression
323 assert_eq!(selector.combination_index, query.index.unwrap());
324 assignment
325 },
326 &|_| panic!("should not occur in returned expressions"),
327 &|_| panic!("should not occur in returned expressions"),
328 &|_| panic!("should not occur in returned expressions"),
329 &|a| -a,
330 &|a, b| a + b,
331 &|a, b| a * b,
332 &|a, f| a * f,
333 );
334
335 if activation {
336 assert!(!eval.is_zero_vartime());
337 } else {
338 assert!(eval.is_zero_vartime());
339 }
340 }
341
342 let expr_degree = selector.expression.degree();
343 assert!(expr_degree <= max_degree);
344 if selectors[selector.selector].max_degree > 0 {
345 assert!(
346 (selectors[selector.selector].max_degree - 1) + expr_degree <= max_degree
347 );
348 }
349 }
350 }
351 }
352}