Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sorry - can be ignored #375

Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 17 additions & 2 deletions halo2_frontend/src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ pub trait Chip<F: Field>: Sized {
}

/// Index of a region in a layouter
#[derive(Clone, Copy, Debug)]
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct RegionIndex(usize);

impl From<usize> for RegionIndex {
Expand Down Expand Up @@ -471,7 +471,7 @@ impl std::ops::Deref for RegionStart {
}

/// A pointer to a cell within a circuit.
#[derive(Clone, Copy, Debug)]
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct Cell {
/// Identifies the region in which this cell resides.
pub region_index: RegionIndex,
Expand All @@ -489,6 +489,21 @@ pub struct AssignedCell<V, F: Field> {
_marker: PhantomData<F>,
}

impl<V, F: Field> PartialEq for AssignedCell<V, F> {
fn eq(&self, other: &Self) -> bool {
self.cell == other.cell
}
}

impl<V, F: Field> Eq for AssignedCell<V, F> {}

use std::hash::{Hash, Hasher};
impl<V, F: Field> Hash for AssignedCell<V, F> {
fn hash<H: Hasher>(&self, state: &mut H) {
self.cell.hash(state)
}
}

impl<V, F: Field> AssignedCell<V, F> {
/// Returns the value of the [`AssignedCell`].
pub fn value(&self) -> Value<&V> {
Expand Down
76 changes: 75 additions & 1 deletion halo2_frontend/src/dev.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,11 @@ pub use tfp::TracingFloorPlanner;
#[cfg(feature = "dev-graph")]
mod graph;

use crate::plonk::circuit::constraint_system::VirtualCell;
#[cfg(feature = "dev-graph")]
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
pub use graph::{circuit_dot_graph, layout::CircuitLayout};
use halo2_middleware::poly::Rotation;

/// Region of assignments that are done during synthesis.
#[derive(Debug)]
Expand Down Expand Up @@ -830,7 +832,17 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
}
_ => {
// Check that it was assigned!
if r.cells.contains_key(&(cell.column, cell_row)) {
if r.cells.contains_key(&(cell.column, cell_row))
|| gate.polynomials().par_iter().all(
|expr| {
self.cell_is_irrelevant(
cell,
expr,
gate_row as usize,
)
},
)
{
None
} else {
Some(VerifyFailure::CellNotAssigned {
Expand Down Expand Up @@ -1177,6 +1189,68 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
}
}

// Checks if the given expression is guaranteed to be constantly zero at the given offset.
fn expr_is_constantly_zero(&self, expr: &Expression<F>, offset: usize) -> bool {
match expr {
Expression::Constant(constant) => constant.is_zero().into(),
Expression::Selector(selector) => !self.selectors[selector.0][offset],
Expression::Fixed(query) => match self.fixed[query.column_index][offset] {
CellValue::Assigned(value) => value.is_zero().into(),
_ => false,
},
Expression::Scaled(e, factor) => {
factor.is_zero().into() || self.expr_is_constantly_zero(e, offset)
}
Expression::Sum(e1, e2) => {
self.expr_is_constantly_zero(e1, offset) && self.expr_is_constantly_zero(e2, offset)
}
Expression::Product(e1, e2) => {
self.expr_is_constantly_zero(e1, offset) || self.expr_is_constantly_zero(e2, offset)
}
_ => false,
}
}
// Verify that the value of the given cell within the given expression is
// irrelevant to the evaluation of the expression. This may be because
// the cell is always multiplied by an expression that evaluates to 0, or
// because the cell is not being queried in the expression at all.
fn cell_is_irrelevant(&self, cell: &VirtualCell, expr: &Expression<F>, offset: usize) -> bool {
// Check if a given query (defined by its columnd and rotation, since we
// want this function to support different query types) is equal to `cell`.
let eq_query = |query_column: usize, query_rotation: Rotation, col_type: Any| {
cell.column.index == query_column
&& cell.column.column_type == col_type
&& query_rotation == cell.rotation
};
match expr {
Expression::Constant(_) | Expression::Selector(_) => true,
Expression::Fixed(query) => !eq_query(query.column_index, query.rotation(), Any::Fixed),
Expression::Advice(query) => !eq_query(
query.column_index,
query.rotation(),
Any::Advice,
),
Expression::Instance(query) => {
!eq_query(query.column_index, query.rotation(), Any::Instance)
}
Expression::Challenge(_) => true,
Expression::Negated(e) => self.cell_is_irrelevant(cell, e, offset),
Expression::Sum(e1, e2) => {
self.cell_is_irrelevant(cell, e1, offset)
&& self.cell_is_irrelevant(cell, e2, offset)
}
Expression::Product(e1, e2) => {
(self.expr_is_constantly_zero(e1, offset)
|| self.expr_is_constantly_zero(e2, offset))
|| (self.cell_is_irrelevant(cell, e1, offset)
&& self.cell_is_irrelevant(cell, e2, offset))
}
Expression::Scaled(e, factor) => {
factor.is_zero().into() || self.cell_is_irrelevant(cell, e, offset)
}
}
}

/// Panics if the circuit being checked by this `MockProver` is not satisfied.
///
/// Any verification failures will be pretty-printed to stderr before the function
Expand Down
62 changes: 60 additions & 2 deletions halo2_frontend/src/dev/cost_model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,19 @@ pub struct CostOptions {

/// 2^K bound on the number of rows.
pub k: usize,

/// Rows count, not including table rows and not accounting for compression
/// (where multiple regions can use the same rows).
pub rows_count: usize,

/// Table rows count, not accounting for compression (where multiple regions
/// can use the same rows), but not much if any compression can happen with
/// table rows anyway.
pub table_rows_count: usize,

/// Compressed rows count, accounting for compression (where multiple
/// regions can use the same rows).
pub compressed_rows_count: usize,
}

/// Structure holding polynomial related data for benchmarks
Expand All @@ -76,7 +89,7 @@ impl FromStr for Poly {
pub struct Lookup;

impl Lookup {
fn queries(&self) -> impl Iterator<Item = Poly> {
pub fn queries(&self) -> impl Iterator<Item = Poly> {
// - product commitments at x and \omega x
// - input commitments at x and x_inv
// - table commitments at x
Expand All @@ -98,7 +111,7 @@ pub struct Permutation {
}

impl Permutation {
fn queries(&self) -> impl Iterator<Item = Poly> {
pub fn queries(&self) -> impl Iterator<Item = Poly> {
// - product commitments at x and x_inv
// - polynomial commitments at x
let product = "0,-1".parse().unwrap();
Expand All @@ -108,6 +121,10 @@ impl Permutation {
.chain(Some(product))
.chain(iter::repeat(poly).take(self.columns))
}

pub fn nr_columns(&self) -> usize {
self.columns
}
}

/// Structure holding the [Shuffle] related data for circuit benchmarks.
Expand All @@ -128,6 +145,10 @@ impl Shuffle {
pub struct ModelCircuit {
/// Power-of-2 bound on the number of rows in the circuit.
pub k: usize,
/// Number of rows in the circuit (not including table rows).
pub rows: usize,
/// Number of table rows in the circuit.
pub table_rows: usize,
/// Maximum degree of the circuit.
pub max_deg: usize,
/// Number of advice columns.
Expand Down Expand Up @@ -228,6 +249,8 @@ impl CostOptions {

ModelCircuit {
k: self.k,
rows: self.rows_count,
table_rows: self.table_rows_count,
max_deg: self.max_degree,
advice_columns: self.advice.len(),
lookups: self.lookup.len(),
Expand Down Expand Up @@ -307,6 +330,38 @@ pub fn from_circuit_to_cost_model_options<F: Ord + Field + FromUniformBytes<64>,
.max()
.unwrap_or(0);

// Note that this computation does't assume that `regions` is already in
// order of increasing row indices.
let (rows_count, table_rows_count, compressed_rows_count) = {
let mut rows_count = 0;
let mut table_rows_count = 0;
let mut compressed_rows_count = 0;
for region in prover.regions {
// If `region.rows == None`, then that region has no rows.
if let Some((start, end)) = region.rows {
// Note that `end` is the index of the last column, so when
// counting rows this last column needs to be counted via `end +
// 1`.

// A region is a _table region_ if all of its columns are `Fixed`
// columns (see that [`plonk::circuit::TableColumn` is a wrapper
// around `Column<Fixed>`]). All of a table region's rows are
// counted towards `table_rows_count.`
if region
.columns
.iter()
.all(|c| *c.column_type() == halo2_middleware::circuit::Any::Fixed)
{
table_rows_count += (end + 1) - start;
} else {
rows_count += (end + 1) - start;
}
compressed_rows_count = std::cmp::max(compressed_rows_count, end + 1);
}
}
(rows_count, table_rows_count, compressed_rows_count)
};

let k = prover.k.try_into().unwrap();

CostOptions {
Expand All @@ -319,5 +374,8 @@ pub fn from_circuit_to_cost_model_options<F: Ord + Field + FromUniformBytes<64>,
permutation,
shuffle,
k,
rows_count,
table_rows_count,
compressed_rows_count,
}
}
2 changes: 1 addition & 1 deletion halo2_frontend/src/dev/util.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ pub(super) fn format_value<F: Field>(v: F) -> String {
// Format value as hex.
let s = format!("{v:?}");
// Remove leading zeroes.
let s = s.strip_prefix("0x").unwrap();
let s = s.splitn(2, "0x").nth(1).unwrap().splitn(2, ")").nth(0).unwrap();
let s = s.trim_start_matches('0');
format!("0x{s}")
}
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.78.0
1.80.0
Loading