mirror of https://github.com/zcash/halo2.git
dev: Enable `VerifyFailure::Lookup` to point to region offsets
This commit is contained in:
parent
8cedfe89de
commit
3843c11e82
11
CHANGELOG.md
11
CHANGELOG.md
|
@ -6,6 +6,9 @@ and this project adheres to Rust's notion of
|
||||||
[Semantic Versioning](https://semver.org/spec/v2.0.0.html).
|
[Semantic Versioning](https://semver.org/spec/v2.0.0.html).
|
||||||
|
|
||||||
## [Unreleased]
|
## [Unreleased]
|
||||||
|
### Added
|
||||||
|
- `halo2::dev::LookupFailure` (used in `VerifyFailure::Lookup`)
|
||||||
|
|
||||||
### Changed
|
### Changed
|
||||||
- `halo2::plonk::Error` has been overhauled:
|
- `halo2::plonk::Error` has been overhauled:
|
||||||
- `Error` now implements `std::fmt::Display` and `std::error::Error`.
|
- `Error` now implements `std::fmt::Display` and `std::error::Error`.
|
||||||
|
@ -19,8 +22,12 @@ and this project adheres to Rust's notion of
|
||||||
underlying `io::Error`.
|
underlying `io::Error`.
|
||||||
- `halo2::dev::CircuitLayout::render` now takes `k` as a `u32`, matching the
|
- `halo2::dev::CircuitLayout::render` now takes `k` as a `u32`, matching the
|
||||||
regular parameter APIs.
|
regular parameter APIs.
|
||||||
- `halo2::dev::VerifyFailure::ConstraintNotSatisfied` now has a `cell_values`
|
- `halo2::dev::VerifyFailure` has been overhauled:
|
||||||
field, storing the values of the cells used in the unsatisfied constraint.
|
- `VerifyFailure::ConstraintNotSatisfied` now has a `cell_values` field,
|
||||||
|
storing the values of the cells used in the unsatisfied constraint.
|
||||||
|
- The `row` field of `VerifyFailure::Lookup` has been replaced by a `location`
|
||||||
|
field, which can now indicate whether the location falls within an assigned
|
||||||
|
region.
|
||||||
- `halo2::plonk::ConstraintSystem::enable_equality` and
|
- `halo2::plonk::ConstraintSystem::enable_equality` and
|
||||||
`halo2::plonk::ConstraintSystem::query_any` now take `Into<Column<Any>>` instead
|
`halo2::plonk::ConstraintSystem::query_any` now take `Into<Column<Any>>` instead
|
||||||
of `Column<Any>` as a parameter to avoid excesive `.into()` usage.
|
of `Column<Any>` as a parameter to avoid excesive `.into()` usage.
|
||||||
|
|
157
src/dev.rs
157
src/dev.rs
|
@ -33,6 +33,29 @@ mod graph;
|
||||||
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
|
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
|
||||||
pub use graph::{circuit_dot_graph, layout::CircuitLayout};
|
pub use graph::{circuit_dot_graph, layout::CircuitLayout};
|
||||||
|
|
||||||
|
/// The location at which a particular lookup is not satisfied.
|
||||||
|
#[derive(Debug, PartialEq)]
|
||||||
|
pub enum LookupFailure {
|
||||||
|
/// A location inside a region. This may be due to the intentional use of a lookup
|
||||||
|
/// (if its inputs are conditional on a complex selector), or an unintentional lookup
|
||||||
|
/// constraint that overlaps the region (indicating that the lookup's inputs should be
|
||||||
|
/// made conditional).
|
||||||
|
InRegion {
|
||||||
|
/// The region in which the lookup's input expressions were evaluated.
|
||||||
|
region: metadata::Region,
|
||||||
|
/// The offset (relative to the start of the region) at which the lookup's input
|
||||||
|
/// expressions were evaluated.
|
||||||
|
offset: usize,
|
||||||
|
},
|
||||||
|
/// A location outside of a region. This most likely means the input expressions do
|
||||||
|
/// not correctly constrain a default value that exists in the table when the lookup
|
||||||
|
/// is not being used.
|
||||||
|
OutsideRegion {
|
||||||
|
/// The circuit row on which this lookup is not satisfied.
|
||||||
|
row: usize,
|
||||||
|
},
|
||||||
|
}
|
||||||
|
|
||||||
/// The reasons why a particular circuit is not satisfied.
|
/// The reasons why a particular circuit is not satisfied.
|
||||||
#[derive(Debug, PartialEq)]
|
#[derive(Debug, PartialEq)]
|
||||||
pub enum VerifyFailure {
|
pub enum VerifyFailure {
|
||||||
|
@ -69,8 +92,8 @@ pub enum VerifyFailure {
|
||||||
/// the order in which `ConstraintSystem::lookup` is called during
|
/// the order in which `ConstraintSystem::lookup` is called during
|
||||||
/// `Circuit::configure`.
|
/// `Circuit::configure`.
|
||||||
lookup_index: usize,
|
lookup_index: usize,
|
||||||
/// The row on which this lookup is not satisfied.
|
/// The location at which the lookup is not satisfied.
|
||||||
row: usize,
|
location: LookupFailure,
|
||||||
},
|
},
|
||||||
/// A permutation did not preserve the original value of a cell.
|
/// A permutation did not preserve the original value of a cell.
|
||||||
Permutation {
|
Permutation {
|
||||||
|
@ -114,9 +137,19 @@ impl fmt::Display for VerifyFailure {
|
||||||
constraint
|
constraint
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
Self::Lookup { lookup_index, row } => {
|
Self::Lookup {
|
||||||
write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row)
|
lookup_index,
|
||||||
}
|
location,
|
||||||
|
} => match location {
|
||||||
|
LookupFailure::InRegion { region, offset } => write!(
|
||||||
|
f,
|
||||||
|
"Lookup {} is not satisfied in {} at offset {}",
|
||||||
|
lookup_index, region, offset
|
||||||
|
),
|
||||||
|
LookupFailure::OutsideRegion { row } => {
|
||||||
|
write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row)
|
||||||
|
}
|
||||||
|
},
|
||||||
Self::Permutation { column, row } => {
|
Self::Permutation { column, row } => {
|
||||||
write!(
|
write!(
|
||||||
f,
|
f,
|
||||||
|
@ -817,7 +850,9 @@ impl<F: FieldExt> MockProver<F> {
|
||||||
} else {
|
} else {
|
||||||
Some(VerifyFailure::Lookup {
|
Some(VerifyFailure::Lookup {
|
||||||
lookup_index,
|
lookup_index,
|
||||||
row: input_row as usize,
|
location: LookupFailure::OutsideRegion {
|
||||||
|
row: input_row as usize,
|
||||||
|
},
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
})
|
})
|
||||||
|
@ -891,10 +926,10 @@ impl<F: FieldExt> MockProver<F> {
|
||||||
mod tests {
|
mod tests {
|
||||||
use pasta_curves::Fp;
|
use pasta_curves::Fp;
|
||||||
|
|
||||||
use super::{MockProver, VerifyFailure};
|
use super::{LookupFailure, MockProver, VerifyFailure};
|
||||||
use crate::{
|
use crate::{
|
||||||
circuit::{Layouter, SimpleFloorPlanner},
|
circuit::{Layouter, SimpleFloorPlanner},
|
||||||
plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
|
plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector, TableColumn},
|
||||||
poly::Rotation,
|
poly::Rotation,
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -969,4 +1004,110 @@ mod tests {
|
||||||
}])
|
}])
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn bad_lookup() {
|
||||||
|
const K: u32 = 4;
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
|
struct FaultyCircuitConfig {
|
||||||
|
a: Column<Advice>,
|
||||||
|
q: Selector,
|
||||||
|
table: TableColumn,
|
||||||
|
}
|
||||||
|
|
||||||
|
struct FaultyCircuit {}
|
||||||
|
|
||||||
|
impl Circuit<Fp> for FaultyCircuit {
|
||||||
|
type Config = FaultyCircuitConfig;
|
||||||
|
type FloorPlanner = SimpleFloorPlanner;
|
||||||
|
|
||||||
|
fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
|
||||||
|
let a = meta.advice_column();
|
||||||
|
let q = meta.complex_selector();
|
||||||
|
let table = meta.lookup_table_column();
|
||||||
|
|
||||||
|
meta.lookup(|cells| {
|
||||||
|
let a = cells.query_advice(a, Rotation::cur());
|
||||||
|
let q = cells.query_selector(q);
|
||||||
|
|
||||||
|
// If q is enabled, a must be in the table.
|
||||||
|
// Zero is in the table, which satisfies the disabled case.
|
||||||
|
vec![(q * a, table)]
|
||||||
|
});
|
||||||
|
|
||||||
|
FaultyCircuitConfig { a, q, table }
|
||||||
|
}
|
||||||
|
|
||||||
|
fn without_witnesses(&self) -> Self {
|
||||||
|
Self {}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn synthesize(
|
||||||
|
&self,
|
||||||
|
config: Self::Config,
|
||||||
|
mut layouter: impl Layouter<Fp>,
|
||||||
|
) -> Result<(), Error> {
|
||||||
|
layouter.assign_table(
|
||||||
|
|| "Doubling table",
|
||||||
|
|mut table| {
|
||||||
|
(0..(1 << (K - 1)))
|
||||||
|
.map(|i| {
|
||||||
|
table.assign_cell(
|
||||||
|
|| format!("table[{}] = {}", i, 2 * i),
|
||||||
|
config.table,
|
||||||
|
i,
|
||||||
|
|| Ok(Fp::from(2 * i as u64)),
|
||||||
|
)
|
||||||
|
})
|
||||||
|
.fold(Ok(()), |acc, res| acc.and(res))
|
||||||
|
},
|
||||||
|
)?;
|
||||||
|
|
||||||
|
layouter.assign_region(
|
||||||
|
|| "Good synthesis",
|
||||||
|
|mut region| {
|
||||||
|
// Enable the lookup on rows 0 and 1.
|
||||||
|
config.q.enable(&mut region, 0)?;
|
||||||
|
config.q.enable(&mut region, 1)?;
|
||||||
|
|
||||||
|
// Assign a = 2 and a = 6.
|
||||||
|
region.assign_advice(|| "a = 2", config.a, 0, || Ok(Fp::from(2)))?;
|
||||||
|
region.assign_advice(|| "a = 6", config.a, 1, || Ok(Fp::from(6)))?;
|
||||||
|
|
||||||
|
Ok(())
|
||||||
|
},
|
||||||
|
)?;
|
||||||
|
|
||||||
|
layouter.assign_region(
|
||||||
|
|| "Faulty synthesis",
|
||||||
|
|mut region| {
|
||||||
|
// Enable the lookup on rows 0 and 1.
|
||||||
|
config.q.enable(&mut region, 0)?;
|
||||||
|
config.q.enable(&mut region, 1)?;
|
||||||
|
|
||||||
|
// Assign a = 4.
|
||||||
|
region.assign_advice(|| "a = 4", config.a, 0, || Ok(Fp::from(4)))?;
|
||||||
|
|
||||||
|
// BUG: Assign a = 5, which doesn't exist in the table!
|
||||||
|
region.assign_advice(|| "a = 5", config.a, 1, || Ok(Fp::from(5)))?;
|
||||||
|
|
||||||
|
Ok(())
|
||||||
|
},
|
||||||
|
)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap();
|
||||||
|
assert_eq!(
|
||||||
|
prover.verify(),
|
||||||
|
Err(vec![VerifyFailure::Lookup {
|
||||||
|
lookup_index: 0,
|
||||||
|
location: LookupFailure::InRegion {
|
||||||
|
region: (2, "Faulty synthesis".to_owned()).into(),
|
||||||
|
offset: 1,
|
||||||
|
}
|
||||||
|
}])
|
||||||
|
);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue