zcash / halo2

The Halo2 zero-knowledge proving system
https://zcash.github.io/halo2/
Other
728 stars 495 forks source link

Improve connection between gate configuration and assignment #365

Open str4d opened 3 years ago

str4d commented 3 years ago

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

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 commented 3 years ago

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 commented 2 years ago

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

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 commented 2 years ago

See also https://github.com/zcash/halo2/issues/509#issuecomment-1146025689 wrt value assignments.

str4d commented 2 years ago

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.