halo2_proofs/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 = selectors
74        .into_iter()
75        .filter(|selector| {
76            if selector.max_degree == 0 {
77                // This is a complex selector, or a selector that does not appear in any
78                // gate constraint.
79                let expression = allocate_fixed_column();
80
81                let combination_assignment = selector
82                    .activations
83                    .iter()
84                    .map(|b| if *b { F::one() } else { F::zero() })
85                    .collect::<Vec<_>>();
86                let combination_index = combination_assignments.len();
87                combination_assignments.push(combination_assignment);
88                selector_assignments.push(SelectorAssignment {
89                    selector: selector.selector,
90                    combination_index,
91                    expression,
92                });
93
94                false
95            } else {
96                true
97            }
98        })
99        .collect();
100
101    // All of the remaining `selectors` are simple. Let's try to combine them.
102    // First, we compute the exclusion matrix that has (j, k) = true if selector
103    // j and selector k conflict -- that is, they are both enabled on the same
104    // row. This matrix is symmetric and the diagonal entries are false, so we
105    // only need to store the lower triangular entries.
106    let mut exclusion_matrix = (0..selectors.len())
107        .map(|i| vec![false; i])
108        .collect::<Vec<_>>();
109
110    for (i, rows) in selectors
111        .iter()
112        .map(|selector| &selector.activations)
113        .enumerate()
114    {
115        // Loop over the selectors previous to this one
116        for (j, other_selector) in selectors.iter().enumerate().take(i) {
117            // Look at what selectors are active at the same row
118            if rows
119                .iter()
120                .zip(other_selector.activations.iter())
121                .any(|(l, r)| l & r)
122            {
123                // Mark them as incompatible
124                exclusion_matrix[i][j] = true;
125            }
126        }
127    }
128
129    // Simple selectors that we've added to combinations already.
130    let mut added = vec![false; selectors.len()];
131
132    for (i, selector) in selectors.iter().enumerate() {
133        if added[i] {
134            continue;
135        }
136        added[i] = true;
137        assert!(selector.max_degree <= max_degree);
138        // This is used to keep track of the largest degree gate involved in the
139        // combination so far. We subtract by one to omit the virtual selector
140        // which will be substituted by the caller with the expression we give
141        // them.
142        let mut d = selector.max_degree - 1;
143        let mut combination = vec![selector];
144        let mut combination_added = vec![i];
145
146        // Try to find other selectors that can join this one.
147        'try_selectors: for (j, selector) in selectors.iter().enumerate().skip(i + 1) {
148            if d + combination.len() == max_degree {
149                // Short circuit; nothing can be added to this
150                // combination.
151                break 'try_selectors;
152            }
153
154            // Skip selectors that have been added to previous combinations
155            if added[j] {
156                continue 'try_selectors;
157            }
158
159            // Is this selector excluded from co-existing in the same
160            // combination with any of the other selectors so far?
161            for &i in combination_added.iter() {
162                if exclusion_matrix[j][i] {
163                    continue 'try_selectors;
164                }
165            }
166
167            // Can the new selector join the combination? Reminder: we use
168            // selector.max_degree - 1 to omit the influence of the virtual
169            // selector on the degree, as it will be substituted.
170            let new_d = std::cmp::max(d, selector.max_degree - 1);
171            if new_d + combination.len() + 1 > max_degree {
172                // Guess not.
173                continue 'try_selectors;
174            }
175
176            d = new_d;
177            combination.push(selector);
178            combination_added.push(j);
179            added[j] = true;
180        }
181
182        // Now, compute the selector and combination assignments.
183        let mut combination_assignment = vec![F::zero(); n];
184        let combination_len = combination.len();
185        let combination_index = combination_assignments.len();
186        let query = allocate_fixed_column();
187
188        let mut assigned_root = F::one();
189        selector_assignments.extend(combination.into_iter().map(|selector| {
190            // Compute the expression for substitution. This produces an expression of the
191            // form
192            //     q * Prod[i = 1..=combination_len, i != assigned_root](i - q)
193            //
194            // which is non-zero only on rows where `combination_assignment` is set to
195            // `assigned_root`. In particular, rows set to 0 correspond to all selectors
196            // being disabled.
197            let mut expression = query.clone();
198            let mut root = F::one();
199            for _ in 0..combination_len {
200                if root != assigned_root {
201                    expression = expression * (Expression::Constant(root) - query.clone());
202                }
203                root += F::one();
204            }
205
206            // Update the combination assignment
207            for (combination, selector) in combination_assignment
208                .iter_mut()
209                .zip(selector.activations.iter())
210            {
211                // This will not overwrite another selector's activations because
212                // we have ensured that selectors are disjoint.
213                if *selector {
214                    *combination = assigned_root;
215                }
216            }
217
218            assigned_root += F::one();
219
220            SelectorAssignment {
221                selector: selector.selector,
222                combination_index,
223                expression,
224            }
225        }));
226        combination_assignments.push(combination_assignment);
227    }
228
229    (combination_assignments, selector_assignments)
230}
231
232#[cfg(test)]
233mod tests {
234    use super::*;
235    use crate::poly::Rotation;
236    use pasta_curves::Fp;
237    use proptest::collection::{vec, SizeRange};
238    use proptest::prelude::*;
239
240    prop_compose! {
241        fn arb_selector(assignment_size: usize, max_degree: usize)
242                       (degree in 0..max_degree,
243                        assignment in vec(any::<bool>(), assignment_size))
244                       -> (usize, Vec<bool>) {
245            (degree, assignment)
246        }
247    }
248
249    prop_compose! {
250        fn arb_selector_list(assignment_size: usize, max_degree: usize, num_selectors: impl Into<SizeRange>)
251                            (list in vec(arb_selector(assignment_size, max_degree), num_selectors))
252                            -> Vec<SelectorDescription>
253        {
254            list.into_iter().enumerate().map(|(i, (max_degree, activations))| {
255                SelectorDescription {
256                    selector: i,
257                    activations,
258                    max_degree,
259                }
260            }).collect()
261        }
262    }
263
264    prop_compose! {
265        fn arb_instance(max_assignment_size: usize,
266                        max_degree: usize,
267                        max_selectors: usize)
268                       (assignment_size in 1..max_assignment_size,
269                        degree in 1..max_degree,
270                        num_selectors in 1..max_selectors)
271                       (list in arb_selector_list(assignment_size, degree, num_selectors),
272                        degree in Just(degree))
273                       -> (Vec<SelectorDescription>, usize)
274        {
275            (list, degree)
276        }
277    }
278
279    proptest! {
280        #![proptest_config(ProptestConfig::with_cases(10000))]
281        #[test]
282        fn test_selector_combination((selectors, max_degree) in arb_instance(10, 10, 15)) {
283            let mut query = 0;
284            let (combination_assignments, selector_assignments) =
285                process::<Fp, _>(selectors.clone(), max_degree, || {
286                    let tmp = Expression::Fixed {
287                        query_index: query,
288                        column_index: query,
289                        rotation: Rotation::cur(),
290                    };
291                    query += 1;
292                    tmp
293                });
294
295            {
296                let mut selectors_seen = vec![];
297                assert_eq!(selectors.len(), selector_assignments.len());
298                for selector in &selector_assignments {
299                    // Every selector should be assigned to a combination
300                    assert!(selector.combination_index < combination_assignments.len());
301                    assert!(!selectors_seen.contains(&selector.selector));
302                    selectors_seen.push(selector.selector);
303                }
304            }
305
306            // Test that, for each selector, the provided expression
307            //  1. evaluates to zero on rows where the selector's activation is off
308            //  2. evaluates to nonzero on rows where the selector's activation is on
309            //  3. is of degree d such that d + (selector.max_degree - 1) <= max_degree
310            //     OR selector.max_degree is zero
311            for selector in selector_assignments {
312                assert_eq!(
313                    selectors[selector.selector].activations.len(),
314                    combination_assignments[selector.combination_index].len()
315                );
316                for (&activation, &assignment) in selectors[selector.selector]
317                    .activations
318                    .iter()
319                    .zip(combination_assignments[selector.combination_index].iter())
320                {
321                    let eval = selector.expression.evaluate(
322                        &|c| c,
323                        &|_| panic!("should not occur in returned expressions"),
324                        &|query_index, _, _| {
325                            // Should be the correct combination in the expression
326                            assert_eq!(selector.combination_index, query_index);
327                            assignment
328                        },
329                        &|_, _, _| panic!("should not occur in returned expressions"),
330                        &|_, _, _| panic!("should not occur in returned expressions"),
331                        &|a| -a,
332                        &|a, b| a + b,
333                        &|a, b| a * b,
334                        &|a, f| a * f,
335                    );
336
337                    if activation {
338                        assert!(!eval.is_zero_vartime());
339                    } else {
340                        assert!(eval.is_zero_vartime());
341                    }
342                }
343
344                let expr_degree = selector.expression.degree();
345                assert!(expr_degree <= max_degree);
346                if selectors[selector.selector].max_degree > 0 {
347                    assert!(
348                        (selectors[selector.selector].max_degree - 1) + expr_degree <= max_degree
349                    );
350                }
351            }
352        }
353    }
354}