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

This PR adds the requirements midnight_lib has to use halo2 library #9

Open
wants to merge 10 commits into
base: dev
Choose a base branch
from
23 changes: 0 additions & 23 deletions .github/workflows/coverage.yml

This file was deleted.

2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# halo2 [![codecov](https://codecov.io/github/privacy-scaling-explorations/halo2/graph/badge.svg?token=6WX7KBHFIP)](https://codecov.io/github/privacy-scaling-explorations/halo2)
# halo2

## [Documentation](https://privacy-scaling-explorations.github.io/halo2/halo2_proofs)

Expand Down
12 changes: 6 additions & 6 deletions halo2_backend/src/helpers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@ pub trait SerdeCurveAffine: CurveAffine + SerdeObject {
/// Reads an element from the buffer and parses it according to the `format`:
/// - `Processed`: Reads a compressed curve element and decompress it
/// - `RawBytes`: Reads an uncompressed curve element with coordinates in Montgomery form.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this intended?

/// - `RawBytesUnchecked`: Reads an uncompressed curve element with coordinates in Montgomery form;
/// does not perform any checks
/// does not perform any checks
fn read<R: io::Read>(reader: &mut R, format: SerdeFormat) -> io::Result<Self> {
match format {
SerdeFormat::Processed => <Self as CurveRead>::read(reader),
Expand Down Expand Up @@ -70,9 +70,9 @@ impl<C: CurveAffine + SerdeObject> SerdeCurveAffine for C {}
pub trait SerdePrimeField: PrimeField + SerdeObject {
/// Reads a field element as bytes from the buffer according to the `format`:
/// - `Processed`: Reads a field element in standard form, with endianness specified by the
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// - `RawBytes`: Reads a field element from raw bytes in its internal Montgomery representations,
/// and checks that the element is less than the modulus.
/// and checks that the element is less than the modulus.
/// - `RawBytesUnchecked`: Reads a field element in Montgomery form and performs no checks.
fn read<R: io::Read>(reader: &mut R, format: SerdeFormat) -> io::Result<Self> {
match format {
Expand All @@ -90,9 +90,9 @@ pub trait SerdePrimeField: PrimeField + SerdeObject {

/// Writes a field element as bytes to the buffer according to the `format`:
/// - `Processed`: Writes a field element in standard form, with endianness specified by the
/// `PrimeField` implementation.
/// `PrimeField` implementation.
/// - Otherwise: Writes a field element into raw bytes in its internal Montgomery representation,
/// WITHOUT performing the expensive Montgomery reduction.
/// WITHOUT performing the expensive Montgomery reduction.
fn write<W: io::Write>(&self, writer: &mut W, format: SerdeFormat) -> io::Result<()> {
match format {
SerdeFormat::Processed => writer.write_all(self.to_repr().as_ref()),
Expand Down
34 changes: 17 additions & 17 deletions halo2_backend/src/plonk.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,11 @@ where
///
/// Writes a curve element according to `format`:
/// - `Processed`: Writes a compressed curve element with coordinates in standard form.
/// Writes a field element in standard form, with endianness specified by the
/// `PrimeField` implementation.
/// Writes a field element in standard form, with endianness specified by the
/// `PrimeField` implementation.
/// - Otherwise: Writes an uncompressed curve element with coordinates in Montgomery form
/// Writes a field element into raw bytes in its internal Montgomery representation,
/// WITHOUT performing the expensive Montgomery reduction.
/// Writes a field element into raw bytes in its internal Montgomery representation,
/// WITHOUT performing the expensive Montgomery reduction.
pub fn write<W: io::Write>(&self, writer: &mut W, format: SerdeFormat) -> io::Result<()> {
// Version byte that will be checked on read.
writer.write_all(&[VERSION])?;
Expand All @@ -90,12 +90,12 @@ where
///
/// Reads a curve element from the buffer and parses it according to the `format`:
/// - `Processed`: Reads a compressed curve element and decompresses it.
/// Reads a field element in standard form, with endianness specified by the
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// Reads a field element in standard form, with endianness specified by the
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// - `RawBytes`: Reads an uncompressed curve element with coordinates in Montgomery form.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.
/// - `RawBytesUnchecked`: Reads an uncompressed curve element with coordinates in Montgomery form;
/// does not perform any checks
/// does not perform any checks
pub fn read<R: io::Read>(
reader: &mut R,
format: SerdeFormat,
Expand Down Expand Up @@ -302,12 +302,12 @@ where
///
/// Writes a curve element according to `format`:
/// - `Processed`: Writes a compressed curve element with coordinates in standard form.
/// Writes a field element in standard form, with endianness specified by the
/// `PrimeField` implementation.
/// Writes a field element in standard form, with endianness specified by the
/// `PrimeField` implementation.
/// - Otherwise: Writes an uncompressed curve element with coordinates in Montgomery form
/// Writes a field element into raw bytes in its internal Montgomery representation,
/// WITHOUT performing the expensive Montgomery reduction.
/// Does so by first writing the verifying key and then serializing the rest of the data (in the form of field polynomials)
/// Writes a field element into raw bytes in its internal Montgomery representation,
/// WITHOUT performing the expensive Montgomery reduction.
/// Does so by first writing the verifying key and then serializing the rest of the data (in the form of field polynomials)
pub fn write<W: io::Write>(&self, writer: &mut W, format: SerdeFormat) -> io::Result<()> {
self.vk.write(writer, format)?;
self.l0.write(writer, format)?;
Expand All @@ -325,12 +325,12 @@ where
///
/// Reads a curve element from the buffer and parses it according to the `format`:
/// - `Processed`: Reads a compressed curve element and decompresses it.
/// Reads a field element in standard form, with endianness specified by the
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// Reads a field element in standard form, with endianness specified by the
/// `PrimeField` implementation, and checks that the element is less than the modulus.
/// - `RawBytes`: Reads an uncompressed curve element with coordinates in Montgomery form.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.
/// Checks that field elements are less than modulus, and then checks that the point is on the curve.
/// - `RawBytesUnchecked`: Reads an uncompressed curve element with coordinates in Montgomery form;
/// does not perform any checks
/// does not perform any checks
pub fn read<R: io::Read>(
reader: &mut R,
format: SerdeFormat,
Expand Down
2 changes: 2 additions & 0 deletions halo2_backend/src/plonk/lookup/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ pub(in crate::plonk) struct Evaluated<C: CurveAffine> {
/// obtaining A' and S', and
/// - constructs [`Permuted<C>`] struct using permuted_input_value = A', and
/// permuted_table_expression = S'.
///
/// The [`Permuted<C>`] struct is used to update the Lookup, and is then returned.
#[allow(clippy::too_many_arguments)]
pub(in crate::plonk) fn lookup_commit_permuted<
Expand Down Expand Up @@ -404,6 +405,7 @@ type ExpressionPair<F> = (Polynomial<F, LagrangeCoeff>, Polynomial<F, LagrangeCo
/// - like values in A' are vertically adjacent to each other; and
/// - the first row in a sequence of like values in A' is the row
/// that has the corresponding value in S'.
///
/// This method returns (A', S') if no errors are encountered.
fn permute_expression_pair<C: CurveAffine, P: Params<C>, R: RngCore>(
pk: &ProvingKey<C>,
Expand Down
6 changes: 2 additions & 4 deletions halo2_backend/src/plonk/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -325,8 +325,6 @@
let params = self.params;
let meta = &self.pk.vk.cs;

let mut rng = &mut self.rng;

let advices = &mut self.advices;
let challenges = &mut self.challenges;

Expand Down Expand Up @@ -406,7 +404,7 @@
for (column_index, advice_values) in column_indices.iter().zip(&mut advice_values) {
if !unblinded_advice.contains(column_index) {
for cell in &mut advice_values[unusable_rows_start..] {
*cell = Scheme::Scalar::random(&mut rng);
*cell = Scheme::Scalar::random(&mut self.rng);
}
} else {
#[cfg(feature = "sanity-checks")]
Expand All @@ -423,7 +421,7 @@
if unblinded_advice.contains(i) {
Blind::default()
} else {
Blind(Scheme::Scalar::random(&mut rng))
Blind(Scheme::Scalar::random(&mut self.rng))
}
})
.collect();
Expand Down Expand Up @@ -501,7 +499,7 @@
/// - 10. Compute and hash instance evals for the circuit instance
/// - 11. Compute and hash fixed evals
/// - 12. Evaluate permutation, lookups and shuffles at x
/// - 13. Generate all queries ([`ProverQuery`])

Check warning on line 502 in halo2_backend/src/plonk/prover.rs

View workflow job for this annotation

GitHub Actions / Intra-doc links

public documentation for `create_proof` links to private item `ProverQuery`
/// - 14. Send the queries to the [`Prover`]
pub fn create_proof(mut self) -> Result<(), Error>
where
Expand Down
2 changes: 1 addition & 1 deletion halo2_debug/src/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use std::fmt;
/// - If the value is a power of two, format it as `2^k`
/// - If the value is smaller than 2^16, format it in decimal
/// - If the value is bigger than congruent -2^16, format it in decimal as the negative congruent
/// (between -2^16 and 0).
/// (between -2^16 and 0).
/// - Else format it in hex without leading zeros.
pub struct FDisp<'a, F: PrimeField>(pub &'a F);

Expand Down
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
14 changes: 0 additions & 14 deletions halo2_frontend/src/circuit/floor_planner/v1/strategy.rs
Original file line number Diff line number Diff line change
Expand Up @@ -214,22 +214,8 @@ pub(crate) fn slot_in_biggest_advice_first(
advice_cols * shape.row_count()
};

// This used to incorrectly use `sort_unstable_by_key` with non-unique keys, which gave
// output that differed between 32-bit and 64-bit platforms, and potentially between Rust
// versions.
// We now use `sort_by_cached_key` with non-unique keys, and rely on `region_shapes`
// being sorted by region index (which we also rely on below to return `RegionStart`s
// in the correct order).
#[cfg(not(feature = "floor-planner-v1-legacy-pdqsort"))]
sorted_regions.sort_by_cached_key(sort_key);

// To preserve compatibility, when the "floor-planner-v1-legacy-pdqsort" feature is enabled,
// we use a copy of the pdqsort implementation from the Rust 1.56.1 standard library, fixed
// to its behaviour on 64-bit platforms.
// https://github.com/rust-lang/rust/blob/1.56.1/library/core/src/slice/mod.rs#L2365-L2402
#[cfg(feature = "floor-planner-v1-legacy-pdqsort")]
halo2_legacy_pdqsort::sort::quicksort(&mut sorted_regions, |a, b| sort_key(a).lt(&sort_key(b)));

sorted_regions.reverse();

// Lay out the sorted regions.
Expand Down
78 changes: 74 additions & 4 deletions 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,15 @@ 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 @@ -911,9 +921,9 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
cell_values: util::cell_values(
gate,
poly,
&util::load(n, row, &self.cs.fixed_queries, &self.fixed),
&util::load(n, row, &self.cs.advice_queries, &self.advice),
&util::load_instance(
util::load(n, row, &self.cs.fixed_queries, &self.fixed),
util::load(n, row, &self.cs.advice_queries, &self.advice),
util::load_instance(
n,
row,
&self.cs.instance_queries,
Expand Down Expand Up @@ -1177,6 +1187,66 @@ 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
Loading
Loading