Struct halo2_proofs::dev::MockProver

pub struct MockProver<F>
where
    F: 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_frontend::{
    circuit::{Layouter, SimpleFloorPlanner, Value},
    dev::{FailureLocation, MockProver, VerifyFailure},
    plonk::{circuit::Column, Circuit, ConstraintSystem, Error, Advice, Selector},
};
use halo2_middleware::circuit::{Any, ColumnMid};
use halo2_middleware::poly::Rotation;
use halo2_middleware::ff::PrimeField;
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: PrimeField> Circuit<F> for MyCircuit {
    type Config = MyConfig;
    type FloorPlanner = SimpleFloorPlanner;
    #[cfg(feature = "circuit-params")]
    type Params = ();

    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![
            ((ColumnMid::new(Any::Advice, 0), 0).into(), "0x2".to_string()),
            ((ColumnMid::new(Any::Advice, 1), 0).into(), "0x4".to_string()),
            ((ColumnMid::new(Any::Advice, 2), 0).into(), "0x8".to_string()),
        ],
    }])
);

// If we provide a too-small K, we get a panic.
use std::panic;
let result = panic::catch_unwind(|| {
    MockProver::<Fp>::run(2, &circuit, vec![]).unwrap_err()
});
assert_eq!(
    result.unwrap_err().downcast_ref::<String>().unwrap(),
    "n=4, minimum_rows=8, k=2"
);

Implementations

impl<F> MockProver<F>

where F: Field,

pub fn advice_mut(&mut self, column_index: usize) -> &mut [CellValue<F>]

Return the content of an advice column as mutable

pub fn instance_mut(&mut self, column_index: usize) -> &mut [InstanceValue<F>]

Return the content of an instance column as mutable

impl<F> MockProver<F>

where F: FromUniformBytes<64> + Ord,

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

where ConcreteCircuit: Circuit<F>,

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

pub fn advice_values(&self, column: Column<Advice>) -> &[CellValue<F>]

Return the content of an advice column as assigned by the circuit.

pub fn fixed_values(&self, column: Column<Fixed>) -> &[CellValue<F>]

Return the content of a fixed column as assigned by the circuit.

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. Constraints and lookup are checked at usable_rows, parallelly.

pub fn verify_at_rows<I>( &self, gate_row_ids: I, lookup_input_row_ids: I ) -> Result<(), Vec<VerifyFailure>>

where I: Clone + Iterator<Item = usize>,

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_at_rows<I>( &self, gate_row_ids: I, lookup_input_row_ids: I )

where I: Clone + Iterator<Item = usize>,

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.

Constraints are only checked at gate_row_ids, and lookup inputs are only checked at lookup_input_row_ids, parallelly.

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

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

pub fn cs(&self) -> &ConstraintSystem<F>

Returns the constraint system

pub fn usable_rows(&self) -> &Range<usize>

Returns the usable rows

pub fn advice(&self) -> &Vec<Vec<CellValue<F>>>

Returns the list of Advice Columns used within a MockProver instance and the associated values contained on each Cell.

pub fn fixed(&self) -> &Vec<Vec<CellValue<F>>>

Returns the list of Fixed Columns used within a MockProver instance and the associated values contained on each Cell.

pub fn selectors(&self) -> &Vec<Vec<bool>>

Returns the list of Selector Columns used within a MockProver instance and the associated values contained on each Cell.

pub fn instance(&self) -> &Vec<Vec<InstanceValue<F>>>

Returns the list of Instance Columns used within a MockProver instance and the associated values contained on each Cell.

Trait Implementations

impl<F> Assignment<F> for MockProver<F>

where F: Field,

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 annotate_column<A, AR>(&mut self, annotation: A, column: Column<Any>)

where A: FnOnce() -> AR, AR: Into<String>,

Allows the developer to include an annotation for an specific column within a Region.

fn enable_selector<A, AR>( &mut self, desc: 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<V, VR, A, AR>( &mut self, desc: A, column: Column<Advice>, row: usize, to: V ) -> Result<(), Error>

where V: FnOnce() -> Value<VR>, VR: Into<Assigned<F>>, A: FnOnce() -> AR, AR: Into<String>,

Assign an advice column value (witness)

fn assign_fixed<V, VR, A, AR>( &mut self, desc: A, column: Column<Fixed>, row: usize, to: V ) -> Result<(), Error>

where V: FnOnce() -> Value<VR>, VR: Into<Assigned<F>>, A: FnOnce() -> AR, AR: Into<String>,

Assign a fixed value

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

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.

impl<F> Debug for MockProver<F>

where F: Debug + Field,

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

Formats the value using the given formatter.