str4d
commented
2 years ago Notes from the Office Hours session in which we discussed this issue:
Halo Office Hours notes
Dynamic tables
We probably need to just implement this from scratch rather than using the existing PRs.
How to improve the instance column API
We don't currently need circuit code when verifying a proof. Therefore, if we wanted to assign public inputs dynamically to instance cells, then the verifying key would need to include a mapping from logical public inputs to their cell positions.
Remember both the hashmap and the order of insertion into the column.
[YT: would we have to generate this mapping via synthesize? like assign_instance]
Motivation
Allow instance columns to be used directly in gates. Right now, if we want to bring in a table, we need to commit to the table column.
How would the rest of the API change?
Existing APIs for instance cell assignment must change or be disabled when using dynamic instance columns (for compatibility with existing circuits — the design constraint is that the circuit hashes must not change, even if the API does).
Maybe define two instance column types, e.g. AbsoluteInstance and DynamicInstance.
Diff of changes made to the codebase while figuring this out
diff --git a/halo2_proofs/examples/simple-example.rs b/halo2_proofs/examples/simple-example.rs
index 5691ba60..d171db25 100644
--- a/halo2_proofs/examples/simple-example.rs
+++ b/halo2_proofs/examples/simple-example.rs
@@ -77,6 +77,7 @@ impl<F: FieldExt> FieldChip<F> {
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
+ named_instance_var: InstanceVarName,
constant: Column<Fixed>,
) -> <Self as Chip<F>>::Config {
meta.enable_equality(instance);
@@ -91,16 +92,19 @@ impl<F: FieldExt> FieldChip<F> {
// To implement multiplication, we need three advice cells and a selector
// cell. We arrange them like so:
//
- // | a0 | a1 | s_mul |
- // |-----|-----|-------|
- // | lhs | rhs | s_mul |
- // | out | | |
+ // | i0 | a0 | a1 | s_mul |
+ // |-----|-----|-----|-------|
+ // | lhs | prev| rhs | |
+ // | lhz | | rhz | s_mul | <---
+ // | | out | | |
//
// Gates may refer to any relative offsets we want, but each distinct
// offset adds a cost to the proof. The most common offsets are 0 (the
// current row), 1 (the next row), and -1 (the previous row), for which
// `Rotation` has specific constructors.
- let lhs = meta.query_advice(advice[0], Rotation::cur());
+ //
+ // We still need to
+ let lhs = meta.query_dynamic_instance(named_instance_var, Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_selector(s_mul);
@@ -260,6 +264,18 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
// We also need an instance column to store public inputs.
let instance = meta.instance_column();
+ // Ideally we want the user to provide at proving/verification some slice &[I: Instances]
+ // where `trait Instances` enables converting the internally tracked instance variables
+ // to an iterator of NamedInstanceVars that the proving system can work with. To do this,
+ // the user needs to be able to identify:
+ // - The specific dynamic instance column that the name belongs in.
+ // - The name.
+ //
+ // We therefore need to specify both of these at configure time. Ideally these could be
+ // types rather than strings, for easier cross-usage.
+ let col = meta.dynamic_instance_column("baz");
+ let named_instance_var = col.named("foobar");
+
// Create a fixed column to load constants.
let constant = meta.fixed_column();
diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs
index 9436011f..889c5ee4 100644
--- a/halo2_proofs/src/circuit/layouter.rs
+++ b/halo2_proofs/src/circuit/layouter.rs
@@ -93,6 +93,24 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error>;
+ /// This tells the backend to position (a copy of) the named instance variable within
+ /// this region at the specified offset.
+ ///
+ /// The backend tracks each time this is called, and then once the regions are layed
+ /// out, it adds equality constraints between all of the copies of each named instance
+ /// variable (equivalent to what `assign_advice_from_instance` does for absolute
+ /// instance columns).
+ fn assign_instance_from_named_var<'v>(
+ &'v mut self,
+ annotation: &'v (dyn Fn() -> String + 'v),
+ // This might be strings, or user-defined types or something; need to figure out
+ // how the names-in-columns are tracked.
+ //
+ // The name type tracks its column internally.
+ name: InstanceVarName,
+ offset: usize,
+ ) -> Result<Cell, Error>;
+
/// Constrains a cell to have a constant value.
///
/// Returns an error if the cell is in a column where equality has not been enabled.
diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs
index 24128874..a3e3c321 100644
--- a/halo2_proofs/src/plonk/circuit.rs
+++ b/halo2_proofs/src/plonk/circuit.rs
@@ -721,11 +721,11 @@ pub(crate) struct PointIndex(pub usize);
/// within a custom gate.
#[derive(Clone, Debug)]
pub(crate) struct VirtualCell {
- pub(crate) column: Column<Any>,
+ pub(crate) column: Column<AnyRelative>,
pub(crate) rotation: Rotation,
}
-impl<Col: Into<Column<Any>>> From<(Col, Rotation)> for VirtualCell {
+impl<Col: Into<Column<AnyRelative>>> From<(Col, Rotation)> for VirtualCell {
fn from((column, rotation): (Col, Rotation)) -> Self {
VirtualCell {
column: column.into(),
@@ -1357,6 +1357,16 @@ impl<F: Field> ConstraintSystem<F> {
tmp
}
+ /// Allocate a new instance column that can be used in constraints.
+ pub fn dynamic_instance_column(&mut self, names) -> Column<DynamicInstance> {
+ let tmp = Column {
+ index: self.num_instance_columns,
+ column_type: Instance,
+ };
+ self.num_instance_columns += 1;
+ tmp
+ }
+
/// Compute the degree of the constraint system (the maximum degree of all
/// constraints).
pub fn degree(&self) -> usize {
@@ -1475,8 +1485,11 @@ impl<'a, F: Field> VirtualCells<'a, F> {
}
}
- /// Query an instance column at a relative position
- pub fn query_instance(&mut self, column: Column<Instance>, at: Rotation) -> Expression<F> {
+ /// Query an instance column at a relative position.
+ ///
+ /// This only works for instance columns declared dynamically (meaning their values
+ /// are referenced abstractly and the columns can be used in relative offsets).
+ pub fn query_instance(&mut self, column: Column<DynamicInstance>, at: Rotation) -> Expression<F> {
self.queried_cells.push((column, at).into());
Expression::Instance {
query_index: self.meta.query_instance_index(column, at),
@@ -1485,13 +1498,13 @@ impl<'a, F: Field> VirtualCells<'a, F> {
}
}
- /// Query an Any column at a relative position
- pub fn query_any<C: Into<Column<Any>>>(&mut self, column: C, at: Rotation) -> Expression<F> {
+ /// Query an Any column at a relative position.
+ pub fn query_any<C: Into<Column<AnyRelative>>>(&mut self, column: C, at: Rotation) -> Expression<F> {
let column = column.into();
match column.column_type() {
Any::Advice => self.query_advice(Column::<Advice>::try_from(column).unwrap(), at),
Any::Fixed => self.query_fixed(Column::<Fixed>::try_from(column).unwrap(), at),
- Any::Instance => self.query_instance(Column::<Instance>::try_from(column).unwrap(), at),
+ Any::DynamicInstance => self.query_instance(Column::<DynamicInstance>::try_from(column).unwrap(), at),
}
}
}
diff --git a/halo2_proofs/src/plonk/verifier.rs b/halo2_proofs/src/plonk/verifier.rs
index 8c6c984c..50a09414 100644
--- a/halo2_proofs/src/plonk/verifier.rs
+++ b/halo2_proofs/src/plonk/verifier.rs
@@ -64,6 +64,14 @@ impl<'params, C: CurveAffine> VerificationStrategy<'params, C> for SingleVerifie
}
}
+/// TODO: Need a deterministic column ordering for absolute vs dynamic.
+/// Would do this by adding DynamicInstance into the deterministic column
+/// Ord impl; circuits not using DynamicInstance would not be affected.
+struct Instances<'a, C> {
+ absolute: &'a [&'a [C::Scalar]],
+ dynamic: &'a [NamedInstanceVar],
+}
+
/// Returns a boolean indicating whether or not the proof is valid
pub fn verify_proof<
'params,
@@ -75,7 +83,7 @@ pub fn verify_proof<
params: &'params Params<C>,
vk: &VerifyingKey<C>,
strategy: V,
- instances: &[&[&[C::Scalar]]],
+ instances: &[Instances<'_>],
transcript: &mut T,
) -> Result<V::Output, Error> {
// Check that instances matches the expected number of instance columns
The current instance column API leaves a bit to be desired: instance columns are passed into the prover and verifier as
&[&[&[C::Scalar]]]. Breaking apart this monstrosity:Another problem is the interaction between instance columns and constraints. The API currently allows instance columns to be queried at relative offsets in constraints, but this is completely useless unless you also use a single region for your entire circuit (and give up any floor planning optimisations). This is because instance columns do not participate in region layouts, because unlike advice and fixed columns, the user needs to know how to construct the instance columns such that the instance variables are position in the correct cells, and the floor planning would make this positioning very hard to expose to the user. Instead, users currently just place their instance column values at the start of the columns, and use
assign_advice_from_instanceto bring them from the absolute instance column position into the relative advice column offset.We should add a second "dynamic instance column" notion, which flips the script. Users should be able to define "named instance variables" that are assigned in a specific column but in an unknown cell (or multiple unknown cells). Then
ConstraintSystem::query_instanceshould be changed to only allow querying these dynamic instance columns.