Heavy use of custom gates can lead to a circuit defining many binary selectors, which would increase proof size and verification time.
This section describes an optimization, applied automatically by halo2, that combines binary selector columns into fewer fixed columns.
The basic idea is that if we have binary selectors labelled that are enabled on disjoint sets of rows, then under some additional conditions we can combine them into a single fixed column, say , such that:
However, the devil is in the detail.
The halo2 API allows defining some selectors to be "simple selectors", subject to the following condition:
Every polynomial constraint involving a simple selector must be of the form where is a polynomial involving no simple selectors.
Suppose that has label in some set of simple selectors that are combined into as above. Then this condition ensures that replacing by will not change the meaning of any constraints.
It would be possible to relax this condition by ensuring that every use of a binary selector is substituted by a precise interpolation of its value from the corresponding combined selector. However,
- the restriction simplifies the implementation, developer tooling, and human understanding and debugging of the resulting constraint system;
- the scope to apply the optimization is not impeded very much by this restriction for typical circuits.
Note that replacing by will increase the degree of constraints selected by by , and so we must choose the selectors that are combined in such a way that the maximum degree bound is not exceeded.
Identifying selectors that can be combined
We need a partition of the overall set of selectors into subsets (called "combinations"), such that no two selectors in a combination are enabled on the same row.
Labels must be unique within a combination, but they are not unique across combinations. Do not confuse a selector's index with its label.
Suppose that we are given , the degree bound of the circuit.
We use the following algorithm:
- Leave nonsimple selectors unoptimized, i.e. map each of them to a separate fixed column.
- Check (or ensure by construction) that all polynomial constraints involving each simple selector are of the form where do not involve any simple selectors. For each , record the maximum degree of any as .
- Compute a binary "exclusion matrix" such that is whenever
and and are enabled on the same row; and otherwise.
Since is symmetric and is zero on the diagonal, we can represent it by either its upper or lower triangular entries. The rest of the algorithm is guaranteed only to access only the entries where .
- Initialize a boolean array to all .
will record whether has been included in any combination.
- Iterate over the that have not yet been added to any combination:
- a. Add to a fresh combination , and set .
- b. Let mut .
is used to keep track of the largest degree, excluding the selector expression, of any gate involved in the combination so far.
- c. Iterate over all the selectors for that can potentially join ,
i.e. for which is false:
- i. (Optimization) If , break to the outer loop, since no more selectors can be added to .
- ii. Let .
- iii. If is for any in , or if
, break to the outer
is the maximum degree, including the selector expression, of any constraint that would result from adding to the combination .
- iv. Set .
- v. Add to and set .
- d. Allocate a fixed column , initialized to all-zeroes.
- e. For each selector :
- i. Label with a distinct index where .
- ii. Record that should be substituted with in all gate constraints.
- iii. For each row such that is enabled at , assign the value to at row .
The above algorithm is implemented in
This is used by the
compress_selectors function of
which does the actual substitutions.
Writing circuits to take best advantage of selector combining
For this optimization it is beneficial for a circuit to use simple selectors as far as possible, rather than fixed columns. It is usually not beneficial to do manual combining of selectors, because the resulting fixed columns cannot take part in the automatic combining. That means that to get comparable results you would need to do a global optimization manually, which would interfere with writing composable gadgets.
Whether two selectors are enabled on the same row (and so are inhibited from being combined) depends on how regions are laid out by the floor planner. The currently implemented floor planners do not attempt to take this into account. We suggest not worrying about it too much — the gains that can be obtained by cajoling a floor planner to shuffle around regions in order to improve combining are likely to be relatively small.