Struct MockProver

pub struct MockProver<F>
where
    F: Field,
{
    k: u32,
    n: u32,
    cs: ConstraintSystem<F>,
    regions: Vec<Region>,
    current_region: Option<Region>,
    fixed: Vec<Vec<CellValue<F>>>,
    advice: Vec<Vec<CellValue<F>>>,
    instance: Vec<Vec<InstanceValue<F>>>,
    selectors: Vec<Vec<bool>>,
    permutation: Assembly,
    usable_rows: Range<usize>,
}

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 group::ff::PrimeField;
use halo2_proofs::{
    circuit::{Layouter, SimpleFloorPlanner, Value},
    dev::{FailureLocation, MockProver, VerifyFailure},
    pasta::Fp,
    plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
    poly::Rotation,
};
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![
            (((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,
));

Fields

k: u32

n: u32

cs: ConstraintSystem<F>

regions: Vec<Region>

current_region: Option<Region>

fixed: Vec<Vec<CellValue<F>>>

advice: Vec<Vec<CellValue<F>>>

instance: Vec<Vec<InstanceValue<F>>>

selectors: Vec<Vec<bool>>

permutation: Assembly

usable_rows: Range<usize>

Implementations

impl<F> MockProver<F>

where F: Field + 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 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 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(()));

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 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<V, VR, A, AR>( &mut self, _: 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, _: 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 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.