Enable floor planners to configure columns

[str4d]

Currently, every time ConstraintSystem::advice_column etc is called, it allocates a fresh column. Chips require two kinds of columns:

• "Bus" columns that it uses to communicate with other chips (passing values around).
• Internal columns that they only use inside the instructions they implement.

If we only have a single chip in the circuit, then it doesn't matter where the columns are allocated; the Layouter is sufficient to lay out a circuit efficiently.

If we have two chips (cores?) in the same circuit that need to communicate, we allocate the bus columns at the circuit level and then explicitly pass them into each chip. However, the internal columns will be allocated independently, resulting in poor laying out of regions.

Instead, we should add namespacing to ConstraintSystem, to enable it to reason about what kinds of regions will use what kinds of columns. This could then be used by a floor planner to decide how to allocate concrete columns, in the same way that the Layouter decides how to assign concrete rows.

[daira]

As I'd imagined it, there would be only one place in the code where you allocate columns for a given circuit. In that place, you also instantiate the cores and pass whatever columns are needed into each core. Cores never allocate columns themselves (as you say, they can't do so efficiently).

The reason to do it this way is that sharing columns between cores is necessarily a global optimization. In general, you don't have enough information to do it efficiently unless you know all the cores you're using.

Now, you may argue that this means a circuit has to know too much about implementation details of the cores it depends on. In practice it's fine, though. It doesn't matter if circuit configuration code is not very reusable, or if it has to change when the column usage of the cores it depends on changes, because it's a relatively small amount of simple code. It's just no big deal, as least for now and for this layer of the API.

In the glorious future where we have a compiler from a high-level language, it will be able to infer how to share columns. But it's a hard problem and we have no need to solve it yet.

[str4d]

I've generalised this issue to be about enabling floor planners to perform horizontal optimizations - both deciding how many columns (of each kind) to allocate, and how to distribute them amongst the configured chips. Existing floor planners would be updated in a way that just requires circuits to retain the existing manually-configured logic.

[str4d]

In a pairing between @daira, @therealyingtong and myself, we had some discussion about this.

• Circuit::configure needs to take something like impl ConstraintSystem (except not named ConstraintSystem but naming is hard), so that we can call it twice: once to collect the columns that the circuit developer wants to use, and again to construct the gate Expressions using the real columns.
  • Pin: is this necessary? Or is doing replacement passes over the Expressions (like we currently do for selector combining) sufficient?
• We had a discussion about what kinds of optimisations would be permitted.
  • Obviously column merging is okay (we do this for selector combining). The floor planner would determine how columns are used by regions, and if it can prove that the regions in two columns are non-interacting, it can merge them.
  • This implies that all gates, lookups etc. involving the columns are fully controlled by selector expressions (that the backend can reason about, which might place restrictions on their complexity), so that the floor planner can prove disjointness.
  • Adding new columns is also okay.
  • e.g. currently users must specify sufficient fixed columns to fit global constants into, or the compiler complains. Instead the floor planner could pick such columns itself, with the existing user specification overriding it.
  • Splitting existing columns is likely workable.
  • The floor planner can examine regions that share a (logical) column (tracking (region_index, column)), determine that a better fit would be to place them in distinct columns, and then map usages of the logical column to the concrete column it has selected.
  • There is a potential UX issue here: if a chip has been configured with a particular column, and a chip instruction creates two regions using that same column, there is no guarantee that they with actually use the same column. However, that can be somewhat implied by the definition of a Region: the two regions cannot interact locally, and must interact via equality constraints, so it is unlikely (but should be confirmed) that there can't be long-range interactions between the regions that the chip developer is relying on (instead they should only be implementing interactions within a single region).
  • If a column to be split is equality-enabled, the resulting concrete columns must also all be equality-enabled. If a column to be split is not equality-enabled, no restrictions (of this form) apply (the columns can be "mixed"). Split columns obviously all need to be the same type (e.g. advice).
  • The floor planner, when deciding to split, would need to carefully reason about gates, because a gate is defined relative to a specific concrete column. In the above example:
    • if the chip developer used the same column in two regions and the same gate within those two regions, then the floor planner would need to split the columns and duplicate the gate constraints (splitting its selector expression potentially, which becomes a huge problem, so this would probably only apply to gates defined with simple boolean selectors); or
    • if the floor planner can prove that the two regions use disjoint sets of gates involving the column in question, then it can instead just configure those gates with the corresponding split-out concrete column.
    • This approach blocks on having typed gate information, because the floor planner needs to be able to link gate definitions in Circuit::configure with gate activations in Circuit::synthesize (#365).

[str4d]

Had another short discussion about this today with @daira and @therealyingtong. In order for efficient optimisers to be written, we need to give bounds on the rows and columns. This is effectively what we already do for the layouter: users specify their desired k value, and then the layouter optimises vertically to reduce the actual number of rows it consumes. But the circuit won't fully take advantage of that improvement unless the user lowers their k value. The same could be done with columns: the user configures the "maximum" (actual) number of columns to use, and the optimiser minimises within that (or perhaps uses all those columns in exchange to reducing rows further, depending on its settings).

Note that we only need for advice columns and non-selector fixed columns. Selector columns would not need a bound, because they serve a different role than a true fixed column. Users only ever enable selectors, they never set arbitrary values. Ergo the optimiser can just compress selectors as much as it wants.