Differences in batch verification to integrate gnark proofs

The subject of this audit were the protocol- and implementation-level changes to the batch verifier circuit that support verification of gnark proofs.

The differences introduced for the integration of gnark proofs are summarized below.

Types

The struct AssignedVerificationKey is changed to include the verifying key for the Pedersen commitment.

pub struct AssignedVerificationKey<F: EccPrimeField> {
    pub alpha: G1InputPoint<F>,
    pub beta: G2InputPoint<F>,
    pub gamma: G2InputPoint<F>,
    pub delta: G2InputPoint<F>,
    pub s: Vec<G1InputPoint<F>>,
+    pub h1: G2InputPoint<F>,
+    pub h2: G2InputPoint<F>,
}

Analogously, the struct AssignedProof is extended to include the Pedersen commitment and proof of knowledge.

pub struct AssignedProof<F: EccPrimeField> {
    pub a: G1InputPoint<F>,
    pub b: G2InputPoint<F>,
    pub c: G1InputPoint<F>,
+    pub m: G1InputPoint<F>,
+    pub pok: G1InputPoint<F>,
}

The separation between vanilla Groth proofs and gnark proofs is handled at the AssignedBatchEntry level by including a has_commitment boolean flag. It also contains the hash of the commitment, which is constrained to be equal to the last public input of the entry.

pub struct AssignedBatchEntry<F: EccPrimeField> {
    /// Assigned length of the public inputs
    pub(super) len: AssignedValue<F>,
    /// Pedersen commitment flag. Constrained to boolean values.
+    pub(super) has_commitment: AssignedValue<F>,
    /// Assigned Verification Key
    pub(super) vk: AssignedVerificationKey<F>,
    /// Assigned Proof
    pub(super) proof: AssignedProof<F>,
    /// Assigned Public Inputs
    pub(super) public_inputs: AssignedPublicInputs<F>,
    /// Commitment Hash
+    pub(super) commitment_hash: AssignedValue<F>,
}

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

In step 1a, UniversalBatchVerifierChip::check_padding,

1. The number of nonpadding elements in the public inputs are checked against entry.len + entry.has_commitment to account for the extra public input, which is constrained to the Pedersen commitment's hash.

2. Also, UniversalBatchVerifierChip::check_padding calls UniversalBatchVerifierChip::check_vk_commitment_padding and UniversalBatchVerifierChip::check_proof_commitment_padding, which constrain vk.h1, vk.h2, proof.m, and proof.pok to be padding if entry.has_commitment is false.

For step 1b, the added elements in the proof and verification key are also checked to lie on the respective curves.

For step 1c, the last public input is constrained to be equal to the hash of the commitment in the proof through a call to UniversalBatchVerifierChip::constrain_commitment_hash.

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

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; UniversalBatchVerifierChip::compute_vk_hash now computes two hashes. One hashes the verifying key as normal, and the second adds the verifying key's commitment terms, h1 and h2, as extra terms before computing the digest. The output is then selected from the two using entry.has_commitment as the selector.

The Fiat-Shamir step for calculating the challenge point now also hashes Pedersen terms from the proofs and verifies keys from each entry.

Steps 4: Computation of 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$. The $S_i$ pairs are computed as before, but the dot product is extended so the computed sum now includes the term entry.has_commitment*proof.M.

Two extra pairs for the Pedersen commitments and corresponding knowledge proofs are now also computed at this stage by making a call to UniversalBatchVerifierChip::pedersen_pairs.

Step 5 to 7: Computation of multipairing and constraining the final result

These steps are largely unchanged — except the addition of m_pairs and pok_pairs computed from UniversalBatchVerifierChip::pedersen_pairs in the previous step are also included in the pairing computation.