Struct halo2_proofs::dev::MockProver

pub struct MockProver<F: Group + Field> { /* private fields */ }

A test prover for debugging circuits.

The normal proving process, when applied to a buggy circuit implementation, might return proofs that do not validate when they should, but it can’t indicate anything other than “something is invalid”. MockProver can be used to figure out why these are invalid: it stores all the private inputs along with the circuit internals, and then checks every constraint manually.

Examples

use halo2_proofs::{
    arithmetic::FieldExt,
    circuit::{Layouter, SimpleFloorPlanner, Value},
    dev::{FailureLocation, MockProver, VerifyFailure},
    plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
    poly::Rotation,
};
use halo2curves::pasta::Fp;
const K: u32 = 5;

#[derive(Copy, Clone)]
struct MyConfig {
    a: Column<Advice>,
    b: Column<Advice>,
    c: Column<Advice>,
    s: Selector,
}

#[derive(Clone, Default)]
struct MyCircuit {
    a: Value<u64>,
    b: Value<u64>,
}

impl<F: FieldExt> Circuit<F> for MyCircuit {
    type Config = MyConfig;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        Self::default()
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> MyConfig {
        let a = meta.advice_column();
        let b = meta.advice_column();
        let c = meta.advice_column();
        let s = meta.selector();

        meta.create_gate("R1CS constraint", |meta| {
            let a = meta.query_advice(a, Rotation::cur());
            let b = meta.query_advice(b, Rotation::cur());
            let c = meta.query_advice(c, Rotation::cur());
            let s = meta.query_selector(s);

            // BUG: Should be a * b - c
            Some(("buggy R1CS", s * (a * b + c)))
        });

        MyConfig { a, b, c, s }
    }

    fn synthesize(&self, config: MyConfig, mut layouter: impl Layouter<F>) -> Result<(), Error> {
        layouter.assign_region(|| "Example region", |mut region| {
            config.s.enable(&mut region, 0)?;
            region.assign_advice(|| "a", config.a, 0, || {
                self.a.map(F::from)
            })?;
            region.assign_advice(|| "b", config.b, 0, || {
                self.b.map(F::from)
            })?;
            region.assign_advice(|| "c", config.c, 0, || {
                (self.a * self.b).map(F::from)
            })?;
            Ok(())
        })
    }
}

// Assemble the private inputs to the circuit.
let circuit = MyCircuit {
    a: Value::known(2),
    b: Value::known(4),
};

// This circuit has no public inputs.
let instance = vec![];

let prover = MockProver::<Fp>::run(K, &circuit, instance).unwrap();
assert_eq!(
    prover.verify(),
    Err(vec![VerifyFailure::ConstraintNotSatisfied {
        constraint: ((0, "R1CS constraint").into(), 0, "buggy R1CS").into(),
        location: FailureLocation::InRegion {
            region: (0, "Example region").into(),
            offset: 0,
        },
        cell_values: vec![
            (((Any::advice(), 0).into(), 0).into(), "0x2".to_string()),
            (((Any::advice(), 1).into(), 0).into(), "0x4".to_string()),
            (((Any::advice(), 2).into(), 0).into(), "0x8".to_string()),
        ],
    }])
);

// If we provide a too-small K, we get an error.
assert!(matches!(
    MockProver::<Fp>::run(2, &circuit, vec![]).unwrap_err(),
    Error::NotEnoughRowsAvailable {
        current_k,
    } if current_k == 2,
));

Implementations

impl<F: FieldExt> MockProver<F>

pub fn run<ConcreteCircuit: Circuit<F>>(
    k: u32,
    circuit: &ConcreteCircuit,
    instance: Vec<Vec<F>>
) -> Result<Self, Error>

Runs a synthetic keygen-and-prove operation on the given circuit, collecting data about the constraints and their assignments.

pub fn verify(&self) -> Result<(), Vec<VerifyFailure>>

Returns Ok(()) if this MockProver is satisfied, or a list of errors indicating the reasons that the circuit is not satisfied.

pub fn verify_at_rows<I: Clone + Iterator<Item = usize>>(
    &self,
    gate_row_ids: I,
    lookup_input_row_ids: I
) -> Result<(), Vec<VerifyFailure>>

Returns Ok(()) if this MockProver is satisfied, or a list of errors indicating the reasons that the circuit is not satisfied. Constraints are only checked at gate_row_ids, and lookup inputs are only checked at lookup_input_row_ids

pub fn verify_par(&self) -> Result<(), Vec<VerifyFailure>>

Returns Ok(()) if this MockProver is satisfied, or a list of errors indicating the reasons that the circuit is not satisfied. Constraints and lookup are checked at usable_rows, parallelly.

pub fn verify_at_rows_par<I: Clone + Iterator<Item = usize>>(
    &self,
    gate_row_ids: I,
    lookup_input_row_ids: I
) -> Result<(), Vec<VerifyFailure>>

Returns Ok(()) if this MockProver is satisfied, or a list of errors indicating the reasons that the circuit is not satisfied. Constraints are only checked at gate_row_ids, and lookup inputs are only checked at lookup_input_row_ids, parallelly.

pub fn assert_satisfied(&self)

Panics if the circuit being checked by this MockProver is not satisfied.

Any verification failures will be pretty-printed to stderr before the function panics.

Apart from the stderr output, this method is equivalent to:

assert_eq!(prover.verify(), Ok(()));

pub fn assert_satisfied_par(&self)

Panics if the circuit being checked by this MockProver is not satisfied.

Any verification failures will be pretty-printed to stderr before the function panics.

Internally, this function uses a parallel aproach in order to verify the MockProver contents.

Apart from the stderr output, this method is equivalent to:

assert_eq!(prover.verify_par(), Ok(()));

Trait Implementations

impl<F: Field + Group> Assignment<F> for MockProver<F>

fn enter_region<NR, N>(&mut self, name: N)where
    NR: Into<String>,
    N: FnOnce() -> NR,

Creates a new region and enters into it.

fn exit_region(&mut self)

Exits the current region.

fn enable_selector<A, AR>(
    &mut self,
    _: A,
    selector: &Selector,
    row: usize
) -> Result<(), Error>where
    A: FnOnce() -> AR,
    AR: Into<String>,

Enables a selector at the given row.

fn query_instance(
    &self,
    column: Column<Instance>,
    row: usize
) -> Result<Value<F>, Error>

Queries the cell of an instance column at a particular absolute row.

fn assign_advice<'r, 'v>(
    &'r mut self,
    column: Column<Advice>,
    row: usize,
    to: Value<Assigned<F>>
) -> Result<Value<&'v Assigned<F>>, Error>

Assign an advice column value (witness)

fn assign_fixed(&mut self, column: Column<Fixed>, row: usize, to: Assigned<F>)

Assign a fixed value

fn copy(
    &mut self,
    left_column: Column<Any>,
    left_row: usize,
    right_column: Column<Any>,
    right_row: usize
)

Assign two cells to have the same value

fn fill_from_row(
    &mut self,
    col: Column<Fixed>,
    from_row: usize,
    to: Value<Assigned<F>>
) -> Result<(), Error>

Fills a fixed column starting from the given row with value to.

fn get_challenge(&self, challenge: Challenge) -> Value<F>

Queries the value of the given challenge.

fn push_namespace<NR, N>(&mut self, _: N)where
    NR: Into<String>,
    N: FnOnce() -> NR,

Creates a new (sub)namespace and enters into it.

fn pop_namespace(&mut self, _: Option<String>)

Exits out of the existing namespace.

fn next_phase(&mut self)

Commit advice columns in current phase and squeeze challenges. This can be called DURING synthesize.

impl<F: Debug + Group + Field> Debug for MockProver<F>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.