Constraint Systems

How we capture problem statements systematically

At the center of our circuit programming API is the ConstraintSystem, which is shared between prover and verifier, and describes how the prover's witness data is constrained. After a brief look at the ConstraintSystem, we turn to how constraint systems and witnesses are created and used by the prover and verifier.

The prover and verifier invoke prove and verify functions which take the following inputs.

Prove: a constraint system and a witness.
Verify: a constraint system and boundary values.

The boundary values are integral to our arithmetization techniques and are introduced here. They are what allow the verifier to connect the proof received to the statement proven. While the prover doesn't need the boundary values, the prover must often help construct the boundary values and give them to the verifier as advice.

As a circuit programmer you won't need to access any fields of the ConstraintSystem directly, but it looks like this:

pub struct ConstraintSystem<F: TowerField> {
	pub oracles: MultilinearOracleSet<F>,
	pub table_constraints: Vec<ConstraintSet<F>>,
	pub non_zero_oracle_ids: Vec<OracleId>,
	pub flushes: Vec<Flush>,
	pub max_channel_id: ChannelId,
}

The ConstraintSystem constrains witness data in four ways:

Virtual oracles: These define relationships between columns that the verifier also knows about. An example of this is Shifted, which describes one column as a shift of another one.
Zero-check constraints: These assert that certain the rows across certain columns satisfy certain equations. We call them "zero-checks" because we express these equations as arithmetic expression on which the rows must vanish.
Nonzero oracles: These assert that certain columns are not allowed to contain any zeros.
Channel flushes: These require that all pushes/pulls to a channel must balance each other out. If the tuple (4, 5) is pushed to a channel, the tuple (4, 5) must also be pulled for the channel to be balanced.

Next we outline how to obtain a constrain system, a witness, and how to feed them to the prover and verifier.

Building the Constraint System

To build both the constraint system and the witness, we use a ConstraintSystemBuilder. The prover and verifier use a ConstraintSystemBuilder as follows. Let us suppose there is a black box function build which accepts the builder, and is responsible for building the entire constraint system as well as the witness. We suppress type parameters for readability.

Verifier: the verifier calls ConstraintSystemBuilder::new to create a builder. Upon passing the builder to our blackbox build function, we can extract out the constraint system by calling builder.build.

let mut builder = ConstraintSystemBuilder::new();
 
build(&mut builder)?;
 
let constraint_system = builder.build()?;

Provided boundary values, a proof from the prover, and log_inv_rate and security_bits parameters, the verifier can call

fn verify(
	constraint_system: &ConstraintSystem,
	log_inv_rate: usize,
	security_bits: usize,
	boundaries: Vec<Boundary>,
	proof: Proof,
) -> Result<(), Error>;

Prover: the prover calls ConstraintSystemBuilder::new_with_witness to create a builder, but must pass in an allocator. Currently we use the simple bump allocator bumpalo. The prover then calls our blackbox build function just as the verifier did, and afterwards extracts both the constraint system and the witness.
```
let allocator = bumpalo::Bump::new();
let mut builder = ConstraintSystemBuilder::new_with_witness(&allocator);
 
build(&mut builder)?;
 
let constraint_system = builder.build()?;
let witness = builder.take_witness()?;
```
Provided the same parameters as the verifier, as well as a domain factory and a backend, the prover can then obtain a proof by calling
```
fn prove(
	constraint_system: &ConstraintSystem,
	log_inv_rate: usize,
	security_bits: usize,
	witness: MultilinearExtensionIndex,
	domain_factory: DomainFactory,
	backend: &Backend,
) -> Result<Proof, Error>;
```
There is also a helper function validate_witness the prover can call to ensure the witness is valid with respect to the constraint system.
```
pub fn validate_witness(
	constraint_system: &ConstraintSystem,
	boundaries: &[Boundary],
	witness: &MultilinearExtensionIndex,
) -> Result<(), Error>;
```
This is a developer tool that can be helpful when building a constraint system to avoid the cost of generating and verifying a proof.

The Build Function

Within our blackbox build function, we must build both the constraint system and the witness. Since both the prover and verifier are calling build, yet only the prover is to build the witness, we must detect whether it is the prover or the verifier calling build. Recall that the prover and verifier instantiated the builder differently. The prover instantiated with an allocator for the witness and the verifier didn't. Calling builder.witness() we receive an Option that returns the witness (or rather the witness builder) if and only if the builder was instantiated by the prover.

Throughout our build function we can build up the witness in prover-only code blocks of the form

if let Some(witness) = builder.witness() {
	// add columns to the witness
}

Outside of these prover-only code blocks all logic is devoted to building the constraint system shared by the prover and verifier. Care must be taken to ensure the additional code executed by the prover doesn't cause the constraint systems to differ between the prover and verifier, otherwise proof verification will fail.

For details on how to create columns, constrain them, and let the prover populate them for the witness, see the basic pattern.