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}