zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #298 from zcash/297-per-region-gate-assignment 

MockProver: Check cell assignment per-region instead of globally
This commit is contained in:
ebfull 2021-06-18 14:20:39 -06:00 committed by GitHub
parent 236115917d 5f8a61cb24
commit ac68cee6de
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 99 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

144
src/dev.rs
View File

@ -32,10 +32,20 @@ fn cell_value<F: Field>(cell: Option<F>) -> F {
pub enum VerifyFailure {
/// A cell used in an active gate was not assigned to.
Cell {
/// The column in which this cell is located.
/// The index of the region in which this cell should be assigned. These indices
/// are assigned in the order in which `Layouter::assign_region` is called during
/// `Circuit::synthesize`.
region_index: usize,
/// The name of the region in which this cell should be assigned. This is
/// specified by the region creator (such as a chip implementation), and is not
/// enforced to be unique.
region_name: String,
/// The column in which this cell should be assigned.
column: Column<Any>,
/// The row in which this cell is located.
row: usize,
/// The offset (relative to the start of the region) at which this cell should be
/// assigned. This may be negative (for example, if a selector enables a gate at
/// offset 0, but the gate uses `Rotation::prev()`).
offset: isize,
/// The index of the active gate. These indices are assigned in the order in which
/// `ConstraintSystem::create_gate` is called during `Circuit::configure`.
gate_index: usize,
@ -90,15 +100,17 @@ impl fmt::Display for VerifyFailure {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Self::Cell {
region_index,
region_name,
column,
row,
offset,
gate_index,
gate_name,
} => {
write!(
f,
"Cell ({:?}, {}) was not assigned to, but it is used by active gate {} ('{}').",
column, row, gate_index, gate_name
"Region {} ('{}') uses gate {} ('{}'), which requires cell in column {:?} at offset {} to be assigned.",
region_index, region_name, gate_index, gate_name, column, offset
)
}
Self::Constraint {
@ -140,6 +152,32 @@ impl fmt::Display for VerifyFailure {
}
}
#[derive(Debug)]
struct Region {
/// The name of the region. Not required to be unique.
name: String,
/// The row that this region starts on, if known.
start: Option<usize>,
/// The selectors that have been enabled in this region. All other selectors are by
/// construction not enabled.
enabled_selectors: HashMap<Selector, Vec<usize>>,
/// The cells assigned in this region. We store this as a `Vec` so that if any cells
/// are double-assigned, they will be visibly darker.
cells: Vec<(Column<Any>, usize)>,
}
impl Region {
fn update_start(&mut self, row: usize) {
// The region start is the earliest row assigned to.
let mut start = self.start.unwrap_or(row);
if row < start {
// The first row assigned was not at start 0 within the region.
start = row;
}
self.start = Some(start);
}
}
/// A test prover for debugging circuits.
///
/// The normal proving process, when applied to a buggy circuit implementation, might
@ -234,9 +272,11 @@ pub struct MockProver<F: Group + Field> {
n: u32,
cs: ConstraintSystem<F>,
/// The selectors that have been enabled in the circuit. All other selectors are by
/// construction not enabled.
enabled_selectors: HashMap<Selector, Vec<usize>>,
/// The regions in the circuit.
regions: Vec<Region>,
/// The current region being assigned to. Will be `None` after the circuit has been
/// synthesized.
current_region: Option<Region>,
// The fixed cells in the circuit, arranged as [column][row].
fixed: Vec<Vec<Option<F>>>,
@ -249,14 +289,23 @@ pub struct MockProver<F: Group + Field> {
}
impl<F: Field + Group> Assignment<F> for MockProver<F> {
fn enter_region<NR, N>(&mut self, _: N)
fn enter_region<NR, N>(&mut self, name: N)
where
NR: Into<String>,
N: FnOnce() -> NR,
{
assert!(self.current_region.is_none());
self.current_region = Some(Region {
name: name().into(),
start: None,
enabled_selectors: HashMap::default(),
cells: vec![],
});
}
fn exit_region(&mut self) {}
fn exit_region(&mut self) {
self.regions.push(self.current_region.take().unwrap());
}
fn enable_selector<A, AR>(
&mut self,
@ -268,8 +317,12 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
// Track that this selector was enabled.
self.enabled_selectors
// Track that this selector was enabled. We require that all selectors are enabled
// inside some region (i.e. no floating selectors).
self.current_region
.as_mut()
.unwrap()
.enabled_selectors
.entry(*selector)
.or_default()
.push(row);
@ -290,6 +343,11 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if let Some(region) = self.current_region.as_mut() {
region.update_start(row);
region.cells.push((column.into(), row));
}
*self
.advice
.get_mut(column.index())
@ -311,6 +369,11 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if let Some(region) = self.current_region.as_mut() {
region.update_start(row);
region.cells.push((column.into(), row));
}
*self
.fixed
.get_mut(column.index())
@ -389,7 +452,8 @@ impl<F: FieldExt> MockProver<F> {
let mut prover = MockProver {
n,
cs,
enabled_selectors: HashMap::default(),
regions: vec![],
current_region: None,
fixed,
advice,
instance,
@ -406,14 +470,13 @@ impl<F: FieldExt> MockProver<F> {
pub fn verify(&self) -> Result<(), Vec<VerifyFailure>> {
let n = self.n as i32;
// Check that all cells used in instantiated gates have been assigned to.
let selector_errors = self
.cs
.gates
.iter()
.enumerate()
.flat_map(|(gate_index, gate)| {
gate.queried_selectors()
// Check that within each region, all cells used in instantiated gates have been
// assigned to.
let selector_errors = self.regions.iter().enumerate().flat_map(|(r_i, r)| {
r.enabled_selectors.iter().flat_map(move |(selector, at)| {
// Find the gates enabled by this selector
self.cs
.gates
.iter()
// Assume that if a queried selector is enabled, the user wants to use the
// corresponding gate in some way.
@ -422,8 +485,9 @@ impl<F: FieldExt> MockProver<F> {
// un-enabled keeps a gate enabled. We could alternatively require that
// every selector is explicitly enabled or disabled on every row? But that
// seems messy and confusing.
.filter_map(|s| self.enabled_selectors.get(&s))
.flat_map(move |at| {
.enumerate()
.filter(move |(_, g)| g.queried_selectors().contains(&selector))
.flat_map(move |(gate_index, gate)| {
at.iter().flat_map(move |selector_row| {
// Selectors are queried with no rotation.
let gate_row = *selector_row as i32;
@ -433,21 +497,14 @@ impl<F: FieldExt> MockProver<F> {
let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize;
// Check that it was assigned!
if match cell.column.column_type() {
Any::Advice => {
self.advice[cell.column.index()][cell_row].is_some()
}
Any::Fixed => {
self.fixed[cell.column.index()][cell_row].is_some()
}
// Instance column cells are assigned outside the circuit.
Any::Instance => true,
} {
if r.cells.contains(&(cell.column, cell_row)) {
None
} else {
Some(VerifyFailure::Cell {
region_index: r_i,
region_name: r.name.clone(),
column: cell.column,
row: cell_row,
offset: cell_row as isize - r.start.unwrap() as isize,
gate_index,
gate_name: gate.name(),
})
@ -455,7 +512,8 @@ impl<F: FieldExt> MockProver<F> {
})
})
})
});
})
});
// Check that all gates are satisfied for all rows.
let gate_errors =
@ -656,7 +714,6 @@ mod tests {
#[test]
fn unassigned_cell() {
const K: u32 = 4;
const FAULTY_ROW: usize = 2;
#[derive(Clone)]
struct FaultyCircuitConfig {
@ -696,15 +753,10 @@ mod tests {
|| "Faulty synthesis",
|mut region| {
// Enable the equality gate.
config.q.enable(&mut region, FAULTY_ROW)?;
config.q.enable(&mut region, 1)?;
// Assign a = 0.
region.assign_advice(
|| "a",
config.a,
FAULTY_ROW - 1,
|| Ok(Fp::zero()),
)?;
region.assign_advice(|| "a", config.a, 0, || Ok(Fp::zero()))?;
// BUG: Forget to assign b = 0! This could go unnoticed during
// development, because cell values default to zero, which in this
@ -719,8 +771,10 @@ mod tests {
assert_eq!(
prover.verify(),
Err(vec![VerifyFailure::Cell {
region_index: 0,
region_name: "Faulty synthesis".to_owned(),
column: Column::new(1, Any::Advice),
row: FAULTY_ROW,
offset: 1,
gate_index: 0,
gate_name: "Equality check"
}])