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.

Sign up for GitHub

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

Jump to bottom

Call synthesize in MockProver multiple times to behave same as real prover #129

Merged
merged 2 commits into from
Feb 9, 2023
Merged

Call synthesize in MockProver multiple times to behave same as real prover #129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9769487
feat: call synthesize in `MockProver` multiple times to behave same a…
han0110 Jan 19, 2023
a5b42f7
feat: check advice assignment consistency between different phases
han0110 Jan 31, 2023
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
110 changes: 90 additions & 20 deletions halo2_proofs/src/dev.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,11 @@ use crate::{
arithmetic::{FieldExt, Group},
circuit,
plonk::{
permutation, Advice, Any, Assigned, Assignment, Challenge, Circuit, Column, ColumnType,
ConstraintSystem, Error, Expression, Fixed, FloorPlanner, Instance, Phase, Selector,
VirtualCell,
permutation,
sealed::{self, SealedPhase},
Advice, Any, Assigned, Assignment, Challenge, Circuit, Column, ColumnType,
ConstraintSystem, Error, Expression, FirstPhase, Fixed, FloorPlanner, Instance, Phase,
Selector, VirtualCell,
},
poly::Rotation,
};
Expand Down Expand Up @@ -307,6 +309,14 @@ pub struct MockProver<F: Group + Field> {

// A range of available rows for assignment and copies.
usable_rows: Range<usize>,

current_phase: sealed::Phase,
}

impl<F: Field + Group> MockProver<F> {
fn in_phase<P: Phase>(&self, phase: P) -> bool {
self.current_phase == phase.to_sealed()
}
}

impl<F: Field + Group> Assignment<F> for MockProver<F> {
Expand All @@ -315,6 +325,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
NR: Into<String>,
N: FnOnce() -> NR,
{
if !self.in_phase(FirstPhase) {
return;
}
CPerezz marked this conversation as resolved.
Show resolved Hide resolved

assert!(self.current_region.is_none());
self.current_region = Some(Region {
name: name().into(),
Expand All @@ -327,6 +341,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
}

fn exit_region(&mut self) {
if !self.in_phase(FirstPhase) {
return;
}
CPerezz marked this conversation as resolved.
Show resolved Hide resolved

self.regions.push(self.current_region.take().unwrap());
}

Expand All @@ -335,6 +353,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if !self.in_phase(FirstPhase) {
return;
}

CPerezz marked this conversation as resolved.
Show resolved Hide resolved
if let Some(region) = self.current_region.as_mut() {
region
.annotations
Expand All @@ -347,6 +369,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if !self.in_phase(FirstPhase) {
return Ok(());
}

if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
Expand Down Expand Up @@ -395,25 +421,44 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
if self.in_phase(FirstPhase) {
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}

if let Some(region) = self.current_region.as_mut() {
region.update_extent(column.into(), row);
region
.cells
.entry((column.into(), row))
.and_modify(|count| *count += 1)
.or_default();
if let Some(region) = self.current_region.as_mut() {
region.update_extent(column.into(), row);
region
.cells
.entry((column.into(), row))
.and_modify(|count| *count += 1)
.or_default();
}
}

*self
.advice
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)? =
CellValue::Assigned(to().into_field().evaluate().assign()?);
match to().into_field().evaluate().assign() {
Ok(to) => {
let value = self
.advice
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)?;
if let CellValue::Assigned(value) = value {
// Inconsistent assignment between different phases.
han0110 marked this conversation as resolved.
Show resolved Hide resolved
if value != &to {
return Err(Error::Synthesis);
}
} else {
*value = CellValue::Assigned(to);
}
}
Err(err) => {
// Propagate `assign` error if the column is in current phase.
if self.in_phase(column.column_type().phase) {
return Err(err);
}
}
}

Ok(())
}
Expand All @@ -431,6 +476,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
A: FnOnce() -> AR,
AR: Into<String>,
{
if !self.in_phase(FirstPhase) {
return Ok(());
}

if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
Expand Down Expand Up @@ -461,6 +510,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
right_column: Column<Any>,
right_row: usize,
) -> Result<(), crate::plonk::Error> {
if !self.in_phase(FirstPhase) {
return Ok(());
}

if !self.usable_rows.contains(&left_row) || !self.usable_rows.contains(&right_row) {
return Err(Error::not_enough_rows_available(self.k));
}
Expand All @@ -475,6 +528,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
from_row: usize,
to: circuit::Value<Assigned<F>>,
) -> Result<(), Error> {
if !self.in_phase(FirstPhase) {
return Ok(());
}

if !self.usable_rows.contains(&from_row) {
return Err(Error::not_enough_rows_available(self.k));
}
Expand All @@ -487,6 +544,10 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
}

fn get_challenge(&self, challenge: Challenge) -> circuit::Value<F> {
if self.current_phase <= challenge.phase {
return circuit::Value::unknown();
}

circuit::Value::known(self.challenges[challenge.index()])
}

Expand Down Expand Up @@ -581,9 +642,18 @@ impl<F: FieldExt> MockProver<F> {
challenges,
permutation,
usable_rows: 0..usable_rows,
current_phase: FirstPhase.to_sealed(),
};

ConcreteCircuit::FloorPlanner::synthesize(&mut prover, circuit, config, constants)?;
for current_phase in prover.cs.phases() {
prover.current_phase = current_phase;
ConcreteCircuit::FloorPlanner::synthesize(
&mut prover,
circuit,
config.clone(),
constants.clone(),
)?;
}

let (cs, selector_polys) = prover.cs.compress_selectors(prover.selectors.clone());
prover.cs = cs;
Expand Down
8 changes: 7 additions & 1 deletion halo2_proofs/src/plonk/circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,12 @@ pub(crate) mod sealed {
}
}

impl SealedPhase for Phase {
fn to_sealed(self) -> Phase {
self
}
}

/// Sealed trait to help keep `Phase` private.
pub trait SealedPhase {
fn to_sealed(self) -> Phase;
Expand Down Expand Up @@ -496,7 +502,7 @@ impl TableColumn {
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Challenge {
index: usize,
phase: sealed::Phase,
pub(crate) phase: sealed::Phase,
}

impl Challenge {
Expand Down