## 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 $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.