A Tutorial on Writing proofs with Plonky2 (Part II)

A deeper dive into plonky2 and recursion.

This is the second part in our series on how to write proofs using plonky2. In part I, we went over some basics and a toy non-recursive example of how to provide a mathematical mfunction.

Today we’ll cover how to write your own circuit and recursively compose individual plonky2 proofs. We’ll go into more technical details than before to help the reader better understand the plonky2 library APIs. While we won’t cover the entirety of our full implementation, we’ll look at key portions of the code.

Configuration

A CircuitConfigis passed in to instantiate a new plonky2 CircuitBuilder. We added some additional comments to the fields below as documentation.

#[derive(Clone, Debug)]
pub struct CircuitConfig {
    // Limits the number of columns/inputs a gate can have.
    pub num_wires: usize,
    // Limits the number of connectable wires a gate can have.
    // Routable wires are connected via copy constraints.
    pub num_routed_wires: usize,
    // Limits the number of constant columns/inputs a gate can have.
    pub num_constants: usize,
    /// Whether to use a dedicated gate for base field arithmetic, rather than using a single gate
    /// for both base field and extension field arithmetic.
    pub use_base_arithmetic_gate: bool,
    // Minimum number of FRI security bits which is dependent on the
    //   - number of query rounds
    //   - code rate (proportion of data that is not redundant)
    //   - proof of work bits (computes num of leading zeros in FRI pow challenges)
    pub security_bits: usize,
    /// The number of challenge points to generate, for IOPs that have soundness errors of (roughly)
    /// `degree / |F|`.
    pub num_challenges: usize,
    pub zero_knowledge: bool,
    /// A cap on the quotient polynomial's degree factor. The actual degree factor is derived
    /// systematically, but will never exceed this value.
    pub max_quotient_degree_factor: usize,
    pub fri_config: FriConfig,
}

Circuit Building

There are a few core operations we want to do when building a circuit. There is some overlap with the operations below.

• Add target wires for dynamic values
• Connect wires via copy constraints
• Associate gates with wires
• Use generators as an optimization for invertible functions

We’ll walk through how the operations above are actually applied when it comes to implementing a circuit for some logic.

EdDSA Signature Verification

The first example we’ll cover is the eddsa signature verification algorithm. To start, let’s visit what the steps of the algorithm looks like at a high level.

verify_eddsa_signature(msg, pubKey, signature { R, s } )
- Calculate h = hash(R + pubKey + msg) mod q
- Calculate P1 = s * G
- Calculate P2 = R + h * pubKey
- Return P1 == P2

Next, we’ll describe what this looks like using the Plonky2 circuit builder API starting with the h calculation.

• First we allocate enough bits to build a sha512 circuit to hash R + pubKey + msg together.
• We assign the msg as a sh512 circuit target directly. Then we add virtual bool targets (bits) for the signature, pubKey and message.
• Next, we connect() the signature and pubKey wires to the sha512 circuit wires.
• Lastly, we apply a few conversions to the hash digest to make the input work for the builder reduce() method which applies modulus the size of the finite field completing the h calculation.

use plonky2_sha512::circuit::{bits_to_biguint_target, make_circuits};

pub fn make_verify_circuits<F: RichField + Extendable<D>, const D: usize>(
    builder: &mut CircuitBuilder<F, D>,
    msg_len: usize,
) -> EDDSATargets {
    let msg_len_in_bits = msg_len * 8;
    let sha512_msg_len = msg_len_in_bits + 512;
    let sha512 = make_circuits(builder, sha512_msg_len as u128);

    let mut msg = Vec::new();
    let mut sig = Vec::new();
    let mut pk = Vec::new();
    for i in 0..msg_len_in_bits {
        msg.push(sha512.message[512 + i]);
    }
    for _ in 0..512 {
        sig.push(builder.add_virtual_bool_target());
    }
    for _ in 0..256 {
        pk.push(builder.add_virtual_bool_target());
    }
    for i in 0..256 {
        builder.connect(sha512.message[i].target, sig[i].target);
    }
    for i in 0..256 {
        builder.connect(sha512.message[256 + i].target, pk[i].target);
    }

    let digest_bits = bits_in_le(sha512.digest.clone());
    let hash = bits_to_biguint_target(builder, digest_bits);
    let h = builder.reduce(&hash);

Let’s look at the P1 calculation next.

• We need to multiply s in the signature by the generator point of the curve.
• We convert the s bits into a BigUintTarget and convert it to a NonNativeTarget which has additional methods for non native field arithmetic.
• Then we multiply s by the generator using a sliding 4 bit window.

    let s_bits = bits_in_le(sig[256..512].to_vec());
    let s_biguint = bits_to_biguint_target(builder, s_bits);
    let s = builder.biguint_to_nonnative(&s_biguint);
    let sb = fixed_base_curve_mul_circuit(
        builder, 
        Ed25519::GENERATOR_AFFINE, 
        &s,
    );

Last thing we need to do is to complete the P2 calculation.

• We take the pubKey bits and convert it to an affine point (x, y) through point_decompress().
• Then we multiply the point by the scalar h which we computed first.
• To add the R portion of the signature to the ha result, we once again convert its bits into an affine point and curve_add() the two points together.

    let pk_bits = bits_in_le(pk.clone());
    let a = builder.point_decompress(&pk_bits);
    let ha = builder.curve_scalar_mul_windowed(&a, &h);

    let r_bits = bits_in_le(sig[..256].to_vec());
    let r = builder.point_decompress(&r_bits);
    let rhs = builder.curve_add(&r, &ha);

To do the equality check we just connect the two points.

     builder.connect_affine_point(&sb, &rhs);

Using Generators

Generators are useful in places where we have invertible functions where the inverse of f is harder to compute than f.

Let’s see how this is done in code for point decompression.

• In the example below, CurvePointDecompressionGenerator computes the inverse of f in rust (outside of the circuit) and adds it to the witness table.
• We connect() the result of the generator p to a point compression circuit.
• Then we compare that result with the input of the point decompression expecting the two values to match.

fn point_decompress<C: Curve>(&mut self, pv: &Vec<BoolTarget>) -> AffinePointTarget<C> {
    assert_eq!(pv.len(), 256);
    let p = self.add_virtual_affine_point_target();

    self.add_simple_generator(CurvePointDecompressionGenerator::<F, D, C> {
        pv: pv.clone(),
        p: p.clone(),
        _phantom: PhantomData,
    });

    let pv2 = self.point_compress(&p);
    for i in 0..256 {
        self.connect(pv[i].target, pv2[i].target);
    }
    p
}

Recursion

To build a recursive circuit to compose proofs, we must first instantiate a new builder and witness.

let mut builder = CircuitBuilder::<F, D>::new(config.clone());
let mut pw = PartialWitness::new();

For each inner proof we do the following.

• Add virtual proof targets to the builder and witness.
• Connect the inner proof with the witness proof target.
• Create a VerifierCircuitTarget which is a dynamic target for use specifically in recursive circuits.
• Connect the verifier circuit data with the verifier circuit target.
• Verify the inner proof using a FRI proof.

/*
inner_proof: ProofWithPublicInputs<F, C, D>
inner_vd: VerifierOnlyCircuitData<C, D>
inner_cd: CommonCircuitData<F, C, D>
*/

let (inner_proof, inner_vd, inner_cd) = inner1;
let pt = builder.add_virtual_proof_with_pis(inner_cd);
pw.set_proof_with_pis_target(&pt, inner_proof);

let inner_data = VerifierCircuitTarget {
    constants_sigmas_cap: builder.add_virtual_cap(inner_cd.config.fri_config.cap_height),
};
pw.set_cap_target(
    &inner_data.constants_sigmas_cap,
    &inner_vd.constants_sigmas_cap,
);

builder.verify_proof(pt, &inner_data, inner_cd);

Note that we can do the above for every inner proof we want to compose. However, each additional proof added to the builder increases the size of the recursive verifier circuit.

In our implementation, we recursively compose two proofs at a time. As a final step, we build the recursive circuit and generate and verify a recursive proof.

let data = builder.build::<C>();
let proof = prove(&data.prover_only, &data.common, pw, &mut timing)?;
data.verify(proof.clone())?;