Universal batch verifier circuit

The universal batch verifier circuit is specified in detail in spec/circuits/universal_batch_verifier.md. There is one discrepancy between the code and the specification that we pointed out in Discussion section ref↗ — for the purposes of the following description, we are going to assume that the endianess in the implementation is correct and assume a correspondingly fixed specification. We will also not mention the findings again here.

We will discuss how the specification corresponds to the implementation, starting from the highest level.

Entry points

The SafeCircuit implementation for UniversalBatchVerifyCircuit offers the main entry points keygen and prover to generate the verification keys and to prove the universal batch verifier circuit. They handle the appropriate settings and otherwise act as a wrapper around UniversalBatchVerifyCircuit::create_builder_and_instance. The prover method also uses BatchEntries::from_ubv_inputs_and_config to pad inputs appropriately. This corresponds to the "Preprocessing" step in the specification.

The circuit uses the halo2-lib builder pattern, and the GateThreadBuilder is created in UniversalBatchVerifyCircuit::create_builder_and_instance, which otherwise acts as a wrapper around the universal_batch_verify_circuit function, creating and passing on the necessary range and finite field chips.

Step 1: Assignment and checking proof points lie on curve and padding is correct

The UniversalBatchVerifierChip::assign_batch_entry function is called by universal_batch_verify_circuit and handles step 1 of the specification.

First, BatchVerifierChip::assign_proof is called, which assigns circuit variables for all the inputs and uses BatchVerifierChip::check_points_on_curve to verify that the proof points lie on the curve, corresponding to step 1b of the specification. Curve points are given in affine coordinates, and checking whether such a point lies on the curve is done using halo2_ecc::ecc::check_is_on_curve, which verifies the curve equation. The point at infinity is thus not representable for curve points.

Step 1a is handled by UniversalBatchVerifierChip::assign_batch_entry via a call to UniversalBatchVerifierChip::check_padding, in which the padding is constrained to be correct, using the method described in the specification.

Steps 2 and 3: Computation of circuit IDs and the challenge point

The UniversalBatchVerifierChip::verify function is called by universal_batch_verify_circuit and handles steps 2 through 7 of the specification, split up in three calls.

First, circuit IDs are computed by calling UniversalBatchVerifierChip::compute_vk_hash, which performs the required Poseidon hash calculation via a call to var_len_poseidon_no_len_check in utils/hashing.rs. This implements step 2 of the specification.

Second, the challenge point is computed by the function UniversalBatchVerifierChip::compute_r. The challenge point is given by another Poseidon hash, of the circuit IDs, proofs, and public inputs, and is calculated with the PoseidonHasher from utils/hashing.rs. This implements step 3 of the specification.

Third, UniversalBatchVerifierChip::verify_with_challenge is called to handle steps 4 through 7.

Precomputation for steps 4 and 5

The UniversalBatchVerifierChip::verify_with_challenge function calls UniversalBatchVerifierChip::prepare_proofs to handle steps 4 and 5.

As step 5 involves taking the scalar multiple of curve points with a power of the challenge point, these powers are first precomputed. This is done by BatchVerifierChip::scalar_powers. A call to UniversalBatchVerifierChip::compute_pairs then handles the actual steps 4 and 5.

Step 4: Computation of $S_i$ and the public input pairs

To perform step 4 of the specification, UniversalBatchVerifierChip::compute_pairs calls UniversalBatchVerifierChip::compute_pi_pairs, which uses halo2_ecc::ecc::EccChip::variable_base_msm and halo2_ecc::ecc::EccChip::sum to compute the linear combinations $S_i$.

Step 5: Scaling of pairs for the batched pairing check

Step 5 of the specification is performed by UniversalBatchVerifierChip::compute_pairs directly. In order to compute the relevant scalar products, BatchVerifierChip::scale_pairs is used, which replaces the first component of a pair with its scalar product with a scalar using halo2_ecc::ecc::scalar_multiply.

Step 6: Computation of the multipairing

To compute the multipairing of all the prepared pairs in the previous steps, UniversalBatchVerifierChip::verify_with_challenge calls BatchVerifierChip::multi_pairing, which uses the PairingChip from halo2_ecc::bn254::pairing to perform this calculation. This implements step 6 of the specification.

Step 7: Constraining the final result

For a valid batch of proofs, the result of the multipairing in the previous step should have been the neutral element of ${\mathbb{G}}_T$. This constraint is added by BatchVerifierChip::check_pairing_result, which is called by UniversalBatchVerifierChip::verify_with_challenge. This implements step 7 of the specification.