Improve connection between gate configuration and assignment

[str4d]

Currently, to use a custom gate (being a group of constraints), the circuit developer needs to do the following:

• At circuit config time:
  • Define the required columns and selectors for the gate.
  • Configure the gate by querying the columns at the appropriate rotations.
  • Store the columns in the circuit's config (or chip's config, if at that level).
• At circuit synthesis time:
  • Call Layouter::assign_region to create a region in which the gate can be used.
  • Obtain the gate's columns from the circuit config.
  • Activate the gate's selector(s) at some specific offset x.
  • Assign to the region's cells, in the columns required for the gate and at the correct rotations relative to x.

Note that the "definition" of the gate is not propagated from configuration to synthesis; the circuit developer just has to "remember" that definition and assign cells appropriately. On the one hand, this makes it easy to detect unintended double-assignments to cells, as the developer can assign once to a cell used in multiple overlapping gates. On the other hand, it's still on the developer to prevent those double-assignments, and it's more likely that the developer will get the assignments wrong due to needing to manually position the gate's "Tetris piece".

My idea for improving this (which I thought I'd already written down somewhere, but oh well) is that gates should be defined as structs with generic parameters:

// Here T represents an advice or fixed cell, and S represents a selector.
struct StandardPlonk<S, T> {
    a: T,
    b: T,
    c: T,
    sa: S,
    sb: S,
    sm: S,
    sc: S,
}

At configure time, each gate struct is constructed to contain "cell templates", which are then used to configure the gate with the constraint relations:

impl StandardPlonk<(Column<Any>, Rotation), Selector> {
    fn query(
        &self,
        meta: &mut ConstraintSystem,
    ) -> StandardPlonk<Expression<Fp>, Expression<Fp>> {
        StandardPlonk {
            a: meta.query_advice(self.a.0, self.a.1),
            b: meta.query_advice(self.b.0, self.b.1),
            c: meta.query_advice(self.c.0, self.c.1),
            sa: meta.query_selector(self.sa),
            sb: meta.query_selector(self.sb),
            sm: meta.query_selector(self.sm),
            sc: meta.query_selector(self.sc),
        }
    }
}

let advice = [
    meta.advice_column(),
    meta.advice_column(),
];
let sa = meta.selector();
let sb = meta.selector();
let sm = meta.selector();
let sc = meta.selector();

let foo: StandardPlonk<(Column<Any>, Rotation), Selector> = StandardPlonk {
    a: (advice[0], Rotation::cur()),
    b: (advice[1], Rotation::cur()),
    c: (advice[0], Rotation::next()),
    sa,
    sb,
    sm,
    sc,
};

// ConstraintSystem::create_gate internally calls StandardPlonk::query
// (probably via some Gate trait).
meta.create_gate("Standard PLONK", foo, |meta, gate| {
    let StandardPlonk {
        a, b, c, sa, sb, sm, sc,
    } = gate;
    sa * a + sb * b + sm * a * b = sc * c
});

The gate structs (foo in the above example) are then stored in the circuit config.

Each gate struct has assignment functions that can be called at synthesis time within a region, by providing the offset to assign the gate at, and the values that should be assigned:

impl StandardPlonk<(Column<Any>, Rotation), Selector> {
    fn assign_addition(
        &self,
        region: &mut Region,
        offset: usize,
        values: StandardPlonk<Option<Fp>, ()>,
    ) -> Result<(), Error> {
        self.sa.enable(&mut region, offset)?;
        self.sb.enable(&mut region, offset)?;
        self.sc.enable(&mut region, offset)?;
        region.assign_advice(|| "", self.a.0, offset + self.a.1.0, || values.a.ok_or(Error::SynthesisError))?;
        region.assign_advice(|| "", self.b.0, offset + self.b.1.0, || values.b.ok_or(Error::SynthesisError))?;
        region.assign_advice(|| "", self.c.0, offset + self.c.1.0, || values.c.ok_or(Error::SynthesisError))?;
    }
}

layouter.assign_region(|| "", |mut region| {
    config.foo.assign_addition(&mut region, 0, StandardPlonk {
        a: Some(2),
        b: Some(5),
        c: Some(7),
        sa: (),
        sb: (),
        sm: (),
        sc: (),
    })
})

The use of the same struct (template) for both the gate and its values, reduces the chance that developers miss any cell assignments. Reviewers would only need to look at StandardPlonk::assign_addition to understand that assignment, instead of in potentially-repeated untethered functions.

[str4d]

Actually, in the above sketch there's no need to reuse StandardPlonk for holding values; StandardPlonk::assign_addition is a concrete method, so it can just take the necessary values as parameters.

[str4d]

After discussing this more last week, I'm pretty sure that this would require several more changes from the above:

• Value assignments need to use closures rather than Option<_> to support side-effects (like pulling from iterators).
• As a result, gate structures need a separate type parameter for every queried cell, rather than sharing T and S above.
• We also need a fair bit of boilerplate to map over the various queried cells, since they are individual properties of the gate struct.

So I think the next step is to write a macro that produces the gate structs and associated boilerplate / mappings, and then try to use them for a few example circuits.

[str4d]

See also #509 (comment) wrt value assignments.

[str4d]

During Office Hours today, while trying to figure out how to assign table rows inside regions, we noted that a nice way to do overlapping gate assignments would be to use the Value type directly, and then after synthesis the backend does a pass to ensure that all queried gate cells were assigned. This would enable users doing tesselation to just assign values for the zero-rotation row of the gate (or whichever rotations are most convenient for the gate author), leaving the next gate to fill in the blanks (that are represented in the current gate by Value::unknown()), and then the first and/or last gate assignments handle the ends.