midnight-zk-stdlib 2.1.0

// This file is part of MIDNIGHT-ZK.
// Copyright (C) Midnight Foundation
// SPDX-License-Identifier: Apache-2.0
// Licensed under the Apache License, Version 2.0 (the "License");
// You may not use this file except in compliance with the License.
// You may obtain a copy of the License at
// http://www.apache.org/licenses/LICENSE-2.0
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#![doc = include_str!("../README.md")]
//!
//! ## Implementation Details
//!
//! This library uses a fixed configuration, meaning that regardless of what one
//! uses, it will always consist of the same columns, lookups, permutation
//! enabled columns, or gates. The motivation for this is twofold:
//!
//! * It facilitates recursion (we always aggregate circuits that have the same
//!   verification logic).
//!
//! * We could optimise the verifier, who can store part of the circuit
//!   description in memory and does not need to reproduce it everytime it
//!   receives a new proof.

mod external;
pub mod utils;

use std::{cell::RefCell, cmp::max, convert::TryInto, fmt::Debug, io, rc::Rc};

use bincode::{config::standard, Decode, Encode};
use blake2b::blake2b::{
    blake2b_chip::{Blake2bChip, Blake2bConfig},
    NB_BLAKE2B_ADVICE_COLS,
};
use ff::{Field, PrimeField};
use group::{prime::PrimeCurveAffine, Group};
use keccak_sha3::packed_chip::{PackedChip, PackedConfig, PACKED_ADVICE_COLS, PACKED_FIXED_COLS};
use midnight_circuits::{
    biguint::biguint_gadget::BigUintGadget,
    ecc::{
        foreign::{
            edwards_chip::{
                nb_foreign_edwards_chip_columns, ForeignEdwardsEccChip, ForeignEdwardsEccConfig,
            },
            weierstrass_chip::{
                nb_foreign_ecc_chip_columns, ForeignWeierstrassEccChip, ForeignWeierstrassEccConfig,
            },
        },
        hash_to_curve::HashToCurveGadget,
        native::{EccChip, EccConfig, NB_EDWARDS_COLS},
    },
    field::{
        decomposition::{
            chip::{P2RDecompositionChip, P2RDecompositionConfig},
            pow2range::Pow2RangeChip,
        },
        foreign::{
            nb_field_chip_columns, params::MultiEmulationParams as MEP, FieldChip, FieldChipConfig,
        },
        native::{NB_ARITH_COLS, NB_ARITH_FIXED_COLS},
        NativeChip, NativeConfig, NativeGadget,
    },
    hash::{
        poseidon::{
            constants::RATE, PoseidonChip, PoseidonConfig, VarLenPoseidonGadget,
            NB_POSEIDON_ADVICE_COLS, NB_POSEIDON_FIXED_COLS,
        },
        sha256::{
            Sha256Chip, Sha256Config, VarLenSha256Gadget, NB_SHA256_ADVICE_COLS,
            NB_SHA256_FIXED_COLS,
        },
        sha512::{Sha512Chip, Sha512Config, NB_SHA512_ADVICE_COLS, NB_SHA512_FIXED_COLS},
    },
    instructions::{
        hash::VarHashInstructions, public_input::CommittedInstanceInstructions,
        vector::VectorBounds, *,
    },
    map::map_gadget::MapGadget,
    parsing::{
        self,
        scanner::{ScannerChip, ScannerConfig, NB_SCANNER_ADVICE_COLS, NB_SCANNER_FIXED_COLS},
        Base64Chip, Base64Config, ParserGadget, NB_BASE64_ADVICE_COLS,
    },
    types::{
        AssignedBit, AssignedByte, AssignedNative, AssignedNativePoint, ComposableChip, InnerValue,
        Instantiable,
    },
    vec::{vector_gadget::VectorGadget, AssignedVector, Vectorizable},
    verifier::{BlstrsEmulation, VerifierGadget},
};
use midnight_curves::{
    curve25519::{self as curve25519_mod, Curve25519},
    k256::{self as k256_mod, K256},
    p256::{self as p256_mod, P256},
    Fq, G1Affine, G1Projective,
};
use midnight_proofs::{
    circuit::{Layouter, SimpleFloorPlanner, Value},
    dev::cost_model::{circuit_model, CircuitModel},
    plonk::{
        self, keygen_vk_with_k, prepare, Circuit, ConstraintSystem, Error, ProvingKey, VerifyingKey,
    },
    poly::{
        commitment::{Guard, Params},
        kzg::{
            params::{ParamsKZG, ParamsVerifierKZG},
            KZGCommitmentScheme,
        },
    },
    transcript::{CircuitTranscript, Hashable, Sampleable, Transcript, TranscriptHash},
    utils::SerdeFormat,
};
use num_bigint::BigUint;
use rand::{CryptoRng, RngCore};

use crate::{
    external::{blake2b::Blake2bWrapper, keccak_sha3::KeccakSha3Wrapper},
    utils::plonk_api::BlstPLONK,
};

type C = midnight_curves::JubjubExtended;
type F = midnight_curves::Fq;

// Type aliases, for readability.
type NG = NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>;
type Secp256k1BaseChip = FieldChip<F, k256_mod::Fp, MEP, NG>;
type Secp256k1ScalarChip = FieldChip<F, k256_mod::Fq, MEP, NG>;
type Secp256k1Chip = ForeignWeierstrassEccChip<F, K256, MEP, Secp256k1ScalarChip, NG>;
type P256BaseChip = FieldChip<F, p256_mod::Fp, MEP, NG>;
type P256ScalarChip = FieldChip<F, p256_mod::Fq, MEP, NG>;
type P256Chip = ForeignWeierstrassEccChip<F, P256, MEP, P256ScalarChip, NG>;
type Bls12381BaseChip = FieldChip<F, midnight_curves::Fp, MEP, NG>;
type Bls12381Chip = ForeignWeierstrassEccChip<
    F,
    midnight_curves::G1Projective,
    midnight_curves::G1Projective,
    NG,
    NG,
>;
type Curve25519BaseChip = FieldChip<F, curve25519_mod::Fp, MEP, NG>;
type Curve25519ScalarChip = FieldChip<F, curve25519_mod::Scalar, MEP, NG>;
type Curve25519Chip = ForeignEdwardsEccChip<F, Curve25519, MEP, Curve25519ScalarChip, NG>;

const ZKSTD_VERSION: u32 = 2;

/// Byte size of a serialized BLS12-381 G1 commitment (compressed).
const COMMITMENT_BYTE_SIZE: usize = 48;

/// Byte size of a serialized BLS12-381 scalar.
const SCALAR_BYTE_SIZE: usize = 32;

/// Architecture of the standard library. Specifies what chips need to be
/// configured.
#[derive(Clone, Copy, Debug, Eq, PartialEq, Encode, Decode)]
pub struct ZkStdLibArch {
    /// Enable the Jubjub chip?
    pub jubjub: bool,

    /// Enable the Poseidon chip?
    pub poseidon: bool,

    /// Enable the SHA256 chip?
    pub sha2_256: bool,

    /// Enable the SHA512 chip?
    pub sha2_512: bool,

    /// Enable the Keccak chip? (third-party implementation)
    ///
    /// Note: is configured using the same columns and tables as sha3_256,
    /// meaning enabling either of the two, or both, requires the same
    /// configuration resources.
    pub keccak_256: bool,

    /// Enable the Sha3 chip? (third-party implementation)
    ///
    /// Note: is configured using the same columns and tables as keccak_256,
    /// meaning enabling either of the two, or both, requires the same
    /// configuration resources.
    pub sha3_256: bool,

    /// Enable the Blake2b chip? (third-party implementation)
    pub blake2b: bool,

    /// Enable the Secp256k1 chip?
    pub secp256k1: bool,

    /// Enable the P256 chip?
    pub p256: bool,

    /// Enable BLS12-381 chip?
    pub bls12_381: bool,

    /// Enable Curve25519 chip?
    pub curve25519: bool,

    /// Enable base64 chip?
    pub base64: bool,

    /// Enable scanner chip (automaton-based parsing and substring checks)?
    pub automaton: bool,

    /// Number of parallel lookups for range checks.
    pub nr_pow2range_cols: u8,
}

impl Default for ZkStdLibArch {
    fn default() -> Self {
        ZkStdLibArch {
            jubjub: false,
            poseidon: false,
            sha2_256: false,
            sha2_512: false,
            sha3_256: false,
            keccak_256: false,
            blake2b: false,
            secp256k1: false,
            p256: false,
            bls12_381: false,
            curve25519: false,
            base64: false,
            automaton: false,
            nr_pow2range_cols: 1,
        }
    }
}

/// Serialized layout of [`ZkStdLibArch`] as it existed in
/// `midnight-zk-stdlib` v1.0.0 (ZKSTD_VERSION 1). Used only for migration
/// when reading old serialized verifying keys.
#[derive(Decode)]
struct ZkStdLibArchV1 {
    jubjub: bool,
    poseidon: bool,
    sha2_256: bool,
    sha2_512: bool,
    keccak_256: bool,
    sha3_256: bool,
    blake2b: bool,
    secp256k1: bool,
    bls12_381: bool,
    base64: bool,
    automaton: bool,
    nr_pow2range_cols: u8,
}

impl From<ZkStdLibArchV1> for ZkStdLibArch {
    fn from(v1: ZkStdLibArchV1) -> Self {
        ZkStdLibArch {
            jubjub: v1.jubjub,
            poseidon: v1.poseidon,
            sha2_256: v1.sha2_256,
            sha2_512: v1.sha2_512,
            keccak_256: v1.keccak_256,
            sha3_256: v1.sha3_256,
            blake2b: v1.blake2b,
            secp256k1: v1.secp256k1,
            p256: false,
            bls12_381: v1.bls12_381,
            curve25519: false,
            base64: v1.base64,
            automaton: v1.automaton,
            nr_pow2range_cols: v1.nr_pow2range_cols,
        }
    }
}

impl ZkStdLibArch {
    /// Writes the ZKStd architecture to a buffer.
    pub fn write<W: io::Write>(&self, writer: &mut W) -> io::Result<()> {
        writer.write_all(&ZKSTD_VERSION.to_le_bytes())?;
        bincode::encode_into_std_write(self, writer, standard())
            .map(|_| ())
            .map_err(io::Error::other)
    }

    /// Reads the ZkStd architecture from a buffer.
    pub fn read<R: io::Read>(reader: &mut R) -> io::Result<Self> {
        let mut version = [0u8; 4];
        reader.read_exact(&mut version)?;
        let version = u32::from_le_bytes(version);
        match version {
            1 => bincode::decode_from_std_read::<ZkStdLibArchV1, _, _>(reader, standard())
                .map(ZkStdLibArch::from)
                .map_err(|e| io::Error::new(io::ErrorKind::InvalidData, e)),
            2 => bincode::decode_from_std_read(reader, standard())
                .map_err(|e| io::Error::new(io::ErrorKind::InvalidData, e)),
            _ => Err(io::Error::new(
                io::ErrorKind::InvalidData,
                format!("Unsupported ZKStd version: {}", version),
            )),
        }
    }

    /// Reads the ZkStdArchitecture from a buffer where a MidnightVK was
    /// serialized. This enables the reader to know the architecture without
    /// the need of deserializing the full verifying key.
    pub fn read_from_serialized_vk<R: io::Read>(reader: &mut R) -> io::Result<Self> {
        // The current serialization of the verifying key places the architecture at
        // the beginning.
        Self::read(reader)
    }
}

#[derive(Debug, Clone)]
/// Configured chips for [ZkStdLib].
pub struct ZkStdLibConfig {
    native_config: NativeConfig,
    core_decomposition_config: P2RDecompositionConfig,
    jubjub_config: Option<EccConfig>,
    sha2_256_config: Option<Sha256Config>,
    sha2_512_config: Option<Sha512Config>,
    poseidon_config: Option<PoseidonConfig<midnight_curves::Fq>>,
    secp256k1_scalar_config: Option<FieldChipConfig>,
    secp256k1_config: Option<ForeignWeierstrassEccConfig<K256>>,
    p256_scalar_config: Option<FieldChipConfig>,
    p256_config: Option<ForeignWeierstrassEccConfig<P256>>,
    bls12_381_config: Option<ForeignWeierstrassEccConfig<midnight_curves::G1Projective>>,
    curve25519_scalar_config: Option<FieldChipConfig>,
    curve25519_config: Option<ForeignEdwardsEccConfig<Curve25519>>,
    base64_config: Option<Base64Config>,
    scanner_config: Option<ScannerConfig>,

    // Configuration of external libraries.
    keccak_sha3_config: Option<PackedConfig>,
    blake2b_config: Option<Blake2bConfig>,
}

/// The `ZkStdLib` exposes all tools that are used in circuit generation.
#[derive(Clone, Debug)]
#[allow(clippy::type_complexity)]
pub struct ZkStdLib {
    // Internal chips and gadgets.
    native_gadget: NG,
    core_decomposition_chip: P2RDecompositionChip<F>,
    jubjub_chip: Option<EccChip<C>>,
    sha2_256_chip: Option<Sha256Chip<F>>,
    varlen_sha2_256_gadget: Option<VarLenSha256Gadget<F>>,
    sha2_512_chip: Option<Sha512Chip<F>>,
    poseidon_gadget: Option<PoseidonChip<F>>,
    varlen_poseidon_gadget: Option<VarLenPoseidonGadget<F>>,
    htc_gadget: Option<HashToCurveGadget<F, C, AssignedNative<F>, PoseidonChip<F>, EccChip<C>>>,
    map_gadget: Option<MapGadget<F, NG, PoseidonChip<F>>>,
    biguint_gadget: BigUintGadget<F, NG>,
    secp256k1_chip: Option<Secp256k1Chip>,
    p256_chip: Option<P256Chip>,
    bls12_381_chip: Option<Bls12381Chip>,
    curve25519_chip: Option<Curve25519Chip>,
    base64_chip: Option<Base64Chip<F>>,
    parser_gadget: ParserGadget<F, NG>,
    scanner_chip: Option<ScannerChip<F>>,
    vector_gadget: VectorGadget<F>,
    verifier_gadget: Option<VerifierGadget<BlstrsEmulation>>,

    // Third-party chips.
    keccak_sha3_chip: Option<KeccakSha3Wrapper<F>>,
    blake2b_chip: Option<Blake2bWrapper<F>>,

    // Flags that indicate if certain chips have been used. This way we can load the tables only
    // when necessary (thus reducing the min_k in some cases).
    // Such a usage flag has to be added and updated correctly for each new chip using tables.
    used_sha2_256: Rc<RefCell<bool>>,
    used_sha2_512: Rc<RefCell<bool>>,
    used_secp256k1: Rc<RefCell<bool>>,
    used_p256: Rc<RefCell<bool>>,
    used_bls12_381: Rc<RefCell<bool>>,
    used_curve25519: Rc<RefCell<bool>>,
    used_base64: Rc<RefCell<bool>>,
    used_scanner: Rc<RefCell<bool>>,
    used_keccak_or_sha3: Rc<RefCell<bool>>,
    used_blake2b: Rc<RefCell<bool>>,
}

impl ZkStdLib {
    /// Creates a new [ZkStdLib] given its config.
    pub fn new(config: &ZkStdLibConfig, max_bit_len: usize) -> Self {
        let native_chip = NativeChip::new(&config.native_config, &());
        let core_decomposition_chip =
            P2RDecompositionChip::new(&config.core_decomposition_config, &max_bit_len);
        let native_gadget = NativeGadget::new(core_decomposition_chip.clone(), native_chip.clone());
        let jubjub_chip = (config.jubjub_config.as_ref())
            .map(|jubjub_config| EccChip::new(jubjub_config, &native_gadget));
        let sha2_256_chip = (config.sha2_256_config.as_ref())
            .map(|sha256_config| Sha256Chip::new(sha256_config, &native_gadget));
        let varlen_sha2_256_gadget = sha2_256_chip.as_ref().map(VarLenSha256Gadget::new);
        let sha2_512_chip = (config.sha2_512_config.as_ref())
            .map(|sha512_config| Sha512Chip::new(sha512_config, &native_gadget));
        let poseidon_gadget = (config.poseidon_config.as_ref())
            .map(|poseidon_config| PoseidonChip::new(poseidon_config, &native_chip));
        let varlen_poseidon_gadget = (poseidon_gadget.as_ref())
            .map(|poseidon| VarLenPoseidonGadget::new(poseidon, &native_gadget));
        let htc_gadget = (jubjub_chip.as_ref())
            .zip(poseidon_gadget.as_ref())
            .map(|(ecc_chip, poseidon_gadget)| HashToCurveGadget::new(poseidon_gadget, ecc_chip));
        let biguint_gadget = BigUintGadget::new(&native_gadget);
        let map_gadget = poseidon_gadget
            .as_ref()
            .map(|poseidon_gadget| MapGadget::new(&native_gadget, poseidon_gadget));
        let secp256k1_scalar_chip = (config.secp256k1_scalar_config.as_ref())
            .map(|scalar_config| FieldChip::new(scalar_config, &native_gadget));
        let secp256k1_chip = (config.secp256k1_config.as_ref())
            .zip(secp256k1_scalar_chip.as_ref())
            .map(|(curve_config, scalar_chip)| {
                ForeignWeierstrassEccChip::new(curve_config, &native_gadget, scalar_chip)
            });
        let p256_scalar_chip = (config.p256_scalar_config.as_ref())
            .map(|scalar_config| FieldChip::new(scalar_config, &native_gadget));
        let p256_chip = (config.p256_config.as_ref()).zip(p256_scalar_chip.as_ref()).map(
            |(curve_config, scalar_chip)| {
                ForeignWeierstrassEccChip::new(curve_config, &native_gadget, scalar_chip)
            },
        );
        let bls12_381_chip = (config.bls12_381_config.as_ref()).map(|curve_config| {
            ForeignWeierstrassEccChip::new(curve_config, &native_gadget, &native_gadget)
        });
        let curve25519_scalar_chip = (config.curve25519_scalar_config.as_ref())
            .map(|scalar_config| FieldChip::new(scalar_config, &native_gadget));
        let curve25519_chip = (config.curve25519_config.as_ref())
            .zip(curve25519_scalar_chip.as_ref())
            .map(|(curve_config, scalar_chip)| {
                ForeignEdwardsEccChip::new(curve_config, &native_gadget, scalar_chip)
            });

        let base64_chip = (config.base64_config.as_ref())
            .map(|base64_config| Base64Chip::new(base64_config, &native_gadget));

        let parser_gadget = ParserGadget::new(&native_gadget);
        let scanner_chip =
            config.scanner_config.as_ref().map(|c| ScannerChip::new(c, &native_gadget));
        let vector_gadget = VectorGadget::new(&native_gadget);

        let verifier_gadget = bls12_381_chip.as_ref().zip(poseidon_gadget.as_ref()).map(
            |(curve_chip, sponge_chip)| {
                VerifierGadget::<BlstrsEmulation>::new(curve_chip, &native_gadget, sponge_chip)
            },
        );

        let keccak_sha3_chip = config
            .keccak_sha3_config
            .as_ref()
            .map(|sha3_config| KeccakSha3Wrapper::new(sha3_config, &native_gadget));
        let blake2b_chip = config
            .blake2b_config
            .as_ref()
            .map(|blake2b_config| Blake2bWrapper::new(blake2b_config, &native_gadget));

        Self {
            native_gadget,
            core_decomposition_chip,
            jubjub_chip,
            sha2_256_chip,
            varlen_sha2_256_gadget,
            sha2_512_chip,
            poseidon_gadget,
            varlen_poseidon_gadget,
            map_gadget,
            htc_gadget,
            biguint_gadget,
            secp256k1_chip,
            p256_chip,
            bls12_381_chip,
            curve25519_chip,
            base64_chip,
            parser_gadget,
            scanner_chip,
            vector_gadget,
            verifier_gadget,
            keccak_sha3_chip,
            blake2b_chip,
            used_sha2_256: Rc::new(RefCell::new(false)),
            used_sha2_512: Rc::new(RefCell::new(false)),
            used_secp256k1: Rc::new(RefCell::new(false)),
            used_p256: Rc::new(RefCell::new(false)),
            used_bls12_381: Rc::new(RefCell::new(false)),
            used_curve25519: Rc::new(RefCell::new(false)),
            used_base64: Rc::new(RefCell::new(false)),
            used_scanner: Rc::new(RefCell::new(false)),
            used_keccak_or_sha3: Rc::new(RefCell::new(false)),
            used_blake2b: Rc::new(RefCell::new(false)),
        }
    }

    /// Configure [ZkStdLib] from scratch.
    pub fn configure(
        meta: &mut ConstraintSystem<F>,
        (arch, max_bit_len): (ZkStdLibArch, u8),
    ) -> ZkStdLibConfig {
        let nb_advice_cols = [
            NB_ARITH_COLS,
            arch.nr_pow2range_cols as usize,
            arch.jubjub as usize * NB_EDWARDS_COLS,
            arch.poseidon as usize * NB_POSEIDON_ADVICE_COLS,
            arch.sha2_256 as usize * NB_SHA256_ADVICE_COLS,
            arch.sha2_512 as usize * NB_SHA512_ADVICE_COLS,
            arch.secp256k1 as usize
                * max(
                    nb_field_chip_columns::<F, k256_mod::Fq, MEP>(),
                    nb_foreign_ecc_chip_columns::<F, K256, MEP, k256_mod::Fq>(),
                ),
            arch.p256 as usize
                * max(
                    nb_field_chip_columns::<F, p256_mod::Fq, MEP>(),
                    nb_foreign_ecc_chip_columns::<F, P256, MEP, p256_mod::Fq>(),
                ),
            arch.bls12_381 as usize
                * max(
                    nb_field_chip_columns::<F, midnight_curves::Fp, MEP>(),
                    nb_foreign_ecc_chip_columns::<
                        F,
                        midnight_curves::G1Projective,
                        MEP,
                        midnight_curves::Fp,
                    >(),
                ),
            arch.curve25519 as usize
                * max(
                    nb_field_chip_columns::<F, curve25519_mod::Scalar, MEP>(),
                    nb_foreign_edwards_chip_columns::<F, Curve25519, MEP>(),
                ),
            arch.base64 as usize * NB_BASE64_ADVICE_COLS,
            arch.automaton as usize * NB_SCANNER_ADVICE_COLS,
            (arch.keccak_256 || arch.sha3_256) as usize * PACKED_ADVICE_COLS,
            arch.blake2b as usize * NB_BLAKE2B_ADVICE_COLS,
        ]
        .into_iter()
        .max()
        .unwrap_or(0);

        let nb_fixed_cols = [
            NB_ARITH_FIXED_COLS,
            arch.poseidon as usize * NB_POSEIDON_FIXED_COLS,
            arch.sha2_256 as usize * NB_SHA256_FIXED_COLS,
            arch.sha2_512 as usize * NB_SHA512_FIXED_COLS,
            (arch.keccak_256 || arch.sha3_256) as usize * PACKED_FIXED_COLS,
            arch.automaton as usize * NB_SCANNER_FIXED_COLS,
        ]
        .into_iter()
        .max()
        .unwrap_or(0);

        let advice_columns = (0..nb_advice_cols).map(|_| meta.advice_column()).collect::<Vec<_>>();
        let fixed_columns = (0..nb_fixed_cols).map(|_| meta.fixed_column()).collect::<Vec<_>>();
        let committed_instance_column = meta.instance_column();
        let instance_column = meta.instance_column();

        let native_config = NativeChip::configure(
            meta,
            &(
                advice_columns[..NB_ARITH_COLS].try_into().unwrap(),
                fixed_columns[..NB_ARITH_FIXED_COLS].try_into().unwrap(),
                [committed_instance_column, instance_column],
            ),
        );

        let nb_parallel_range_checks = arch.nr_pow2range_cols as usize;
        let max_bit_len = max_bit_len as u32;

        let pow2range_config =
            Pow2RangeChip::configure(meta, &advice_columns[1..=arch.nr_pow2range_cols as usize]);

        let core_decomposition_config =
            P2RDecompositionChip::configure(meta, &(native_config.clone(), pow2range_config));

        let jubjub_config = arch.jubjub.then(|| {
            EccChip::<C>::configure(meta, &advice_columns[..NB_EDWARDS_COLS].try_into().unwrap())
        });

        let sha2_256_config = arch.sha2_256.then(|| {
            Sha256Chip::configure(
                meta,
                &(
                    advice_columns[..NB_SHA256_ADVICE_COLS].try_into().unwrap(),
                    fixed_columns[..NB_SHA256_FIXED_COLS].try_into().unwrap(),
                ),
            )
        });

        let sha2_512_config = arch.sha2_512.then(|| {
            Sha512Chip::configure(
                meta,
                &(
                    advice_columns[..NB_SHA512_ADVICE_COLS].try_into().unwrap(),
                    fixed_columns[..NB_SHA512_FIXED_COLS].try_into().unwrap(),
                ),
            )
        });

        let poseidon_config = arch.poseidon.then(|| {
            PoseidonChip::configure(
                meta,
                &(
                    advice_columns[..NB_POSEIDON_ADVICE_COLS].try_into().unwrap(),
                    fixed_columns[..NB_POSEIDON_FIXED_COLS].try_into().unwrap(),
                ),
            )
        });

        let secp256k1_scalar_config = arch.secp256k1.then(|| {
            Secp256k1ScalarChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let secp256k1_config = arch.secp256k1.then(|| {
            let base_config = Secp256k1BaseChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            );
            Secp256k1Chip::configure(
                meta,
                &base_config,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let p256_scalar_config = arch.p256.then(|| {
            P256ScalarChip::configure(meta, &advice_columns, nb_parallel_range_checks, max_bit_len)
        });

        let p256_config = arch.p256.then(|| {
            let base_config = P256BaseChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            );
            P256Chip::configure(
                meta,
                &base_config,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let bls12_381_config = arch.bls12_381.then(|| {
            let base_config = Bls12381BaseChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            );
            Bls12381Chip::configure(
                meta,
                &base_config,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let curve25519_scalar_config = arch.curve25519.then(|| {
            Curve25519ScalarChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let curve25519_config = arch.curve25519.then(|| {
            let base_config = Curve25519BaseChip::configure(
                meta,
                &advice_columns,
                nb_parallel_range_checks,
                max_bit_len,
            );
            Curve25519Chip::configure(
                meta,
                &base_config,
                &advice_columns,
                &fixed_columns,
                nb_parallel_range_checks,
                max_bit_len,
            )
        });

        let base64_config = arch.base64.then(|| {
            Base64Chip::configure(
                meta,
                advice_columns[..NB_BASE64_ADVICE_COLS].try_into().unwrap(),
            )
        });

        let scanner_config = arch.automaton.then(|| {
            ScannerChip::configure(
                meta,
                &(
                    advice_columns[..NB_SCANNER_ADVICE_COLS].try_into().unwrap(),
                    fixed_columns[0],
                    parsing::spec_library(),
                ),
            )
        });

        let constant_column =
            (arch.keccak_256 || arch.sha3_256 || arch.blake2b).then(|| meta.fixed_column());

        let keccak_sha3_config = (arch.keccak_256 || arch.sha3_256).then(|| {
            PackedChip::configure(
                meta,
                constant_column.unwrap(),
                advice_columns[..PACKED_ADVICE_COLS].try_into().unwrap(),
                fixed_columns[..PACKED_FIXED_COLS].try_into().unwrap(),
            )
        });

        let blake2b_config = arch.blake2b.then(|| {
            Blake2bChip::configure(
                meta,
                constant_column.unwrap(),
                advice_columns[0],
                advice_columns[1..NB_BLAKE2B_ADVICE_COLS].try_into().unwrap(),
            )
        });

        ZkStdLibConfig {
            native_config,
            core_decomposition_config,
            jubjub_config,
            sha2_256_config,
            sha2_512_config,
            poseidon_config,
            secp256k1_scalar_config,
            secp256k1_config,
            p256_scalar_config,
            p256_config,
            bls12_381_config,
            curve25519_scalar_config,
            curve25519_config,
            base64_config,
            scanner_config,
            keccak_sha3_config,
            blake2b_config,
        }
    }
}

impl ZkStdLib {
    /// Native EccChip.
    pub fn jubjub(&self) -> &EccChip<C> {
        self.jubjub_chip.as_ref().expect("ZkStdLibArch must enable jubjub")
    }

    /// Gadget for performing in-circuit big-unsigned integer operations.
    pub fn biguint(&self) -> &BigUintGadget<F, NG> {
        &self.biguint_gadget
    }

    /// Gadget for performing map and non-map checks
    pub fn map_gadget(&self) -> &MapGadget<F, NG, PoseidonChip<F>> {
        self.map_gadget
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable poseidon"))
    }

    /// Chip for performing in-circuit operations over the Secp256k1 curve, its
    /// scalar field or its base field.
    pub fn secp256k1(&self) -> &Secp256k1Chip {
        *self.used_secp256k1.borrow_mut() = true;
        self.secp256k1_chip
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable secp256k1"))
    }

    /// Chip for performing in-circuit operations over the P256 curve, its
    /// scalar field or its base field.
    pub fn p256(&self) -> &P256Chip {
        *self.used_p256.borrow_mut() = true;
        self.p256_chip
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable p256"))
    }

    /// Chip for performing in-circuit operations over the BLS12-381 curve, its
    /// scalar field or its base field.
    pub fn bls12_381(&self) -> &Bls12381Chip {
        *self.used_bls12_381.borrow_mut() = true;
        self.bls12_381_chip
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable bls12_381"))
    }

    /// Chip for performing in-circuit operations over Curve25519.
    pub fn curve25519(&self) -> &Curve25519Chip {
        *self.used_curve25519.borrow_mut() = true;
        self.curve25519_chip
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable curve25519"))
    }

    /// Chip for performing in-circuit base64 decoding.
    pub fn base64(&self) -> &Base64Chip<F> {
        *self.used_base64.borrow_mut() = true;
        self.base64_chip
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable base64"))
    }

    /// Gadget for column-free parsing helpers (fetch_bytes, date_to_int, etc.).
    /// Always available (no arch flag needed).
    pub fn parser(&self) -> &ParserGadget<F, NG> {
        &self.parser_gadget
    }

    /// Chip for various scanning functions based on lookups. This includes
    /// automaton-based parsing ([`ScannerChip::parse`]) and substring checks
    /// ([`ScannerChip::check_subsequence`], [`ScannerChip::check_bytes`]).
    ///
    /// Returns the scanner chip for automaton-based parsing and substring
    /// checks. The static automaton table is loaded automatically when
    /// `parse` is called with a `Static(..)` variant.
    pub fn scanner(&self) -> &ScannerChip<F> {
        *self.used_scanner.borrow_mut() = true;
        (self.scanner_chip.as_ref()).unwrap_or_else(|| panic!("ZkStdLibArch must enable automaton"))
    }

    /// Chip for performing in-circuit verification of proofs
    /// (generated with Poseidon as the Fiat-Shamir transcript hash).
    pub fn verifier(&self) -> &VerifierGadget<BlstrsEmulation> {
        *self.used_bls12_381.borrow_mut() = true;
        self.verifier_gadget
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable bls12_381 & poseidon"))
    }

    /// Assert that a given assigned bit is true.
    ///
    /// ```
    /// # midnight_zk_stdlib::run_test_stdlib!(chip, layouter, 13, {
    /// let input: AssignedBit<F> = chip.assign_fixed(layouter, true)?;
    /// chip.assert_true(layouter, &input)?;
    /// # });
    /// ```
    pub fn assert_true(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedBit<F>,
    ) -> Result<(), Error> {
        self.native_gadget.assert_equal_to_fixed(layouter, input, true)
    }

    /// Assert that a given assigned bit is false
    pub fn assert_false(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedBit<F>,
    ) -> Result<(), Error> {
        self.native_gadget.assert_equal_to_fixed(layouter, input, false)
    }

    /// Returns `1` iff `x < y`.
    ///
    /// ```
    /// # midnight_zk_stdlib::run_test_stdlib!(chip, layouter, 13, {
    /// let x: AssignedNative<F> = chip.assign_fixed(layouter, F::from(127))?;
    /// let y: AssignedNative<F> = chip.assign_fixed(layouter, F::from(212))?;
    /// let condition = chip.lower_than(layouter, &x, &y, 8)?;
    ///
    /// chip.assert_true(layouter, &condition)?;
    /// # });
    /// ```
    ///
    /// # Unsatisfiable Circuit
    ///
    /// If `x` or `y` are not in the range `[0, 2^n)`.
    ///
    /// ```should_panic
    /// # midnight_zk_stdlib::run_test_stdlib!(chip, layouter, 13, {
    /// let x: AssignedNative<F> = chip.assign_fixed(layouter, F::from(127))?;
    /// let y: AssignedNative<F> = chip.assign_fixed(layouter, F::from(212))?;
    /// let _condition = chip.lower_than(layouter, &x, &y, 7)?;
    /// # });
    /// ```
    ///
    /// Setting `n > (F::NUM_BITS - 1) / 2` will result in a compile-time
    /// error.
    pub fn lower_than(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        y: &AssignedNative<F>,
        n: u32,
    ) -> Result<AssignedBit<F>, Error> {
        let bounded_x = self.native_gadget.bounded_of_element(layouter, n as usize, x)?;
        let bounded_y = self.native_gadget.bounded_of_element(layouter, n as usize, y)?;
        self.native_gadget.lower_than(layouter, &bounded_x, &bounded_y)
    }

    /// Poseidon hash from a slice of native values into a native value.
    ///
    /// ```
    /// # midnight_zk_stdlib::run_test_stdlib!(chip, layouter, 13, {
    /// let x: AssignedNative<F> = chip.assign_fixed(layouter, F::from(127))?;
    /// let y: AssignedNative<F> = chip.assign_fixed(layouter, F::from(212))?;
    ///
    /// let _hash = chip.poseidon(layouter, &[x, y])?;
    /// # });
    /// ```
    pub fn poseidon(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedNative<F>],
    ) -> Result<AssignedNative<F>, Error> {
        self.poseidon_gadget
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable poseidon"))
            .hash(layouter, input)
    }

    /// Poseidon hash over a payload whose element count can vary between
    /// proofs.
    ///
    /// Unlike [`poseidon`](Self::poseidon), which takes a plain slice whose
    /// length is structurally fixed in the circuit (the same for every proof),
    /// this variant takes an [`AssignedVector`]: a specialized structure for
    /// carrying data of varying length, up to a maximum capacity of `M`
    /// elements.
    ///
    /// `M` must be a multiple of 2 (the Poseidon absorption rate).
    pub fn poseidon_varlen<const M: usize>(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedVector<F, AssignedNative<F>, M, RATE>,
    ) -> Result<AssignedNative<F>, Error> {
        assert!(
            M.is_multiple_of(RATE),
            "poseidon_varlen only supports assigned vector whose maxlen M is a multiple of {RATE} (here M = {M})"
        );
        self.varlen_poseidon_gadget
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable poseidon"))
            .poseidon_varlen(layouter, input)
    }

    /// Hashes a slice of assigned values into `(x, y)` coordinates which are
    /// guaranteed to be in the curve `C`. For usage, see [HashToCurveGadget].
    pub fn hash_to_curve(
        &self,
        layouter: &mut impl Layouter<F>,
        inputs: &[AssignedNative<F>],
    ) -> Result<AssignedNativePoint<C>, Error> {
        self.htc_gadget
            .as_ref()
            .unwrap_or_else(|| panic!("ZkStdLibArch must enable poseidon and jubjub"))
            .hash_to_curve(layouter, inputs)
    }

    /// SHA2-256.
    /// Takes as input a slice of assigned bytes and returns the assigned
    /// input/output in bytes.
    /// We assume the field uses little endian encoding.
    /// ```
    /// # midnight_zk_stdlib::run_test_stdlib!(chip, layouter, 13, {
    /// let input = chip.assign_many(
    ///     layouter,
    ///     &[
    ///         Value::known(13),
    ///         Value::known(226),
    ///         Value::known(119),
    ///         Value::known(5),
    ///     ],
    /// )?;
    ///
    /// let _hash = chip.sha2_256(layouter, &input)?;
    /// # });
    /// ```
    pub fn sha2_256(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>], // F -> decompose_bytes -> hash
    ) -> Result<[AssignedByte<F>; 32], Error> {
        *self.used_sha2_256.borrow_mut() = true;
        self.sha2_256_chip
            .as_ref()
            .expect("ZkStdLibArch must enable sha256")
            .hash(layouter, input)
    }

    /// SHA-256 hash over a payload whose byte count can vary between proofs.
    ///
    /// Unlike [`sha2_256`](Self::sha2_256), which takes a plain slice whose
    /// length is structurally fixed in the circuit (the same for every proof),
    /// this variant takes an [`AssignedVector`]: a specialized structure for
    /// carrying data of varying length, up to a maximum capacity of `M` bytes.
    ///
    /// `M` must be a multiple of 64 (the SHA-256 block size).
    pub fn sha2_256_varlen<const M: usize>(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedVector<F, AssignedByte<F>, M, 64>,
    ) -> Result<[AssignedByte<F>; 32], Error> {
        *self.used_sha2_256.borrow_mut() = true;
        assert!(
            M.is_multiple_of(64),
            "sha2_256_varlen only supports assigned vector whose maxlen M is a multiple of 64 (here M = {M})"
        );
        self.varlen_sha2_256_gadget
            .as_ref()
            .expect("ZkStdLibArch must enable sha256")
            .varhash(layouter, input)
    }

    /// SHA2-512 hash.
    pub fn sha2_512(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>], // F -> decompose_bytes -> hash
    ) -> Result<[AssignedByte<F>; 64], Error> {
        *self.used_sha2_512.borrow_mut() = true;
        self.sha2_512_chip
            .as_ref()
            .expect("ZkStdLibArch must enable sha512")
            .hash(layouter, input)
    }

    /// SHA3-256 hash (third-party implementation).
    pub fn sha3_256(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>],
    ) -> Result<[AssignedByte<Fq>; 32], Error> {
        *self.used_keccak_or_sha3.borrow_mut() = true;
        let chip = self
            .keccak_sha3_chip
            .as_ref()
            .expect("ZkStdLibArch must enable sha3 (or keccak)");
        chip.sha3_256_digest(layouter, input)
    }

    /// Keccak-256 hash (third-party implementation).
    pub fn keccak_256(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>],
    ) -> Result<[AssignedByte<Fq>; 32], Error> {
        *self.used_keccak_or_sha3.borrow_mut() = true;
        let chip = self
            .keccak_sha3_chip
            .as_ref()
            .expect("ZkStdLibArch must enable keccak (or sha3)");
        chip.keccak_256_digest(layouter, input)
    }

    /// Blake2b hash with a 256-bit output, unkeyed (third-party
    /// implementation).
    pub fn blake2b_256(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>],
    ) -> Result<[AssignedByte<F>; 32], Error> {
        *self.used_blake2b.borrow_mut() = true;
        let chip = self.blake2b_chip.as_ref().expect("ZkStdLibArch must enable blake2b");
        chip.blake2b_256_digest(layouter, input)
    }

    /// Blake2b hash with a 512-bit output, unkeyed (third-party
    /// implementation).
    pub fn blake2b_512(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &[AssignedByte<F>],
    ) -> Result<[AssignedByte<F>; 64], Error> {
        *self.used_blake2b.borrow_mut() = true;
        let chip = self.blake2b_chip.as_ref().expect("ZkStdLibArch must enable blake2b");
        chip.blake2b_512_digest(layouter, input)
    }
}

impl<T> AssignmentInstructions<F, T> for ZkStdLib
where
    T: InnerValue,
    T::Element: Clone,
    NG: AssignmentInstructions<F, T>,
{
    fn assign(
        &self,
        layouter: &mut impl Layouter<F>,
        value: Value<T::Element>,
    ) -> Result<T, Error> {
        self.native_gadget.assign(layouter, value)
    }

    fn assign_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        constant: T::Element,
    ) -> Result<T, Error> {
        self.native_gadget.assign_fixed(layouter, constant)
    }

    fn assign_many(
        &self,
        layouter: &mut impl Layouter<F>,
        values: &[Value<T::Element>],
    ) -> Result<Vec<T>, Error> {
        self.native_gadget.assign_many(layouter, values)
    }
}

impl<T> PublicInputInstructions<F, T> for ZkStdLib
where
    T: Instantiable<F>,
    T::Element: Clone,
    NG: PublicInputInstructions<F, T>,
{
    fn as_public_input(
        &self,
        layouter: &mut impl Layouter<F>,
        assigned: &T,
    ) -> Result<Vec<AssignedNative<F>>, Error> {
        self.native_gadget.as_public_input(layouter, assigned)
    }

    fn constrain_as_public_input(
        &self,
        layouter: &mut impl Layouter<F>,
        assigned: &T,
    ) -> Result<(), Error> {
        self.native_gadget.constrain_as_public_input(layouter, assigned)
    }

    fn assign_as_public_input(
        &self,
        layouter: &mut impl Layouter<F>,
        value: Value<<T>::Element>,
    ) -> Result<T, Error> {
        self.native_gadget.assign_as_public_input(layouter, value)
    }
}

impl<T> CommittedInstanceInstructions<F, T> for ZkStdLib
where
    F: PrimeField,
    T: Instantiable<F>,
    NG: CommittedInstanceInstructions<F, T>,
{
    fn constrain_as_committed_public_input(
        &self,
        layouter: &mut impl Layouter<F>,
        assigned: &T,
    ) -> Result<(), Error> {
        self.native_gadget.constrain_as_committed_public_input(layouter, assigned)
    }
}

impl<T> AssertionInstructions<F, T> for ZkStdLib
where
    T: InnerValue,
    NG: AssertionInstructions<F, T>,
{
    fn assert_equal(&self, layouter: &mut impl Layouter<F>, x: &T, y: &T) -> Result<(), Error> {
        self.native_gadget.assert_equal(layouter, x, y)
    }

    fn assert_not_equal(&self, layouter: &mut impl Layouter<F>, x: &T, y: &T) -> Result<(), Error> {
        self.native_gadget.assert_not_equal(layouter, x, y)
    }

    fn assert_equal_to_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        constant: T::Element,
    ) -> Result<(), Error> {
        self.native_gadget.assert_equal_to_fixed(layouter, x, constant)
    }

    fn assert_not_equal_to_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        constant: T::Element,
    ) -> Result<(), Error> {
        self.native_gadget.assert_not_equal_to_fixed(layouter, x, constant)
    }
}

impl<T> EqualityInstructions<F, T> for ZkStdLib
where
    T: InnerValue,
    NG: EqualityInstructions<F, T>,
{
    fn is_equal(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        y: &T,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.is_equal(layouter, x, y)
    }

    fn is_not_equal(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        y: &T,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.is_not_equal(layouter, x, y)
    }

    fn is_equal_to_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        constant: T::Element,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.is_equal_to_fixed(layouter, x, constant)
    }

    fn is_not_equal_to_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &T,
        constant: T::Element,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.is_not_equal_to_fixed(layouter, x, constant)
    }
}

impl<T1, T2> ConversionInstructions<F, T1, T2> for ZkStdLib
where
    T1: InnerValue,
    T2: InnerValue,
    NG: ConversionInstructions<F, T1, T2>,
{
    fn convert_value(&self, x: &T1::Element) -> Option<T2::Element> {
        ConversionInstructions::<_, T1, T2>::convert_value(&self.native_gadget, x)
    }

    fn convert(&self, layouter: &mut impl Layouter<F>, x: &T1) -> Result<T2, Error> {
        self.native_gadget.convert(layouter, x)
    }
}

impl CanonicityInstructions<F, AssignedNative<F>> for ZkStdLib {
    fn le_bits_lower_than(
        &self,
        layouter: &mut impl Layouter<F>,
        bits: &[AssignedBit<F>],
        bound: BigUint,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.le_bits_lower_than(layouter, bits, bound)
    }

    fn le_bits_geq_than(
        &self,
        layouter: &mut impl Layouter<F>,
        bits: &[AssignedBit<F>],
        bound: BigUint,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.le_bits_geq_than(layouter, bits, bound)
    }
}

impl DecompositionInstructions<F, AssignedNative<F>> for ZkStdLib {
    fn assigned_to_le_bits(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        nb_bits: Option<usize>,
        enforce_canonical: bool,
    ) -> Result<Vec<AssignedBit<F>>, Error> {
        self.native_gadget.assigned_to_le_bits(layouter, x, nb_bits, enforce_canonical)
    }

    fn assigned_to_le_bytes(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        nb_bytes: Option<usize>,
    ) -> Result<Vec<AssignedByte<F>>, Error> {
        self.native_gadget.assigned_to_le_bytes(layouter, x, nb_bytes)
    }

    fn assigned_to_le_chunks(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        nb_bits_per_chunk: usize,
        nb_chunks: Option<usize>,
    ) -> Result<Vec<AssignedNative<F>>, Error> {
        self.native_gadget
            .assigned_to_le_chunks(layouter, x, nb_bits_per_chunk, nb_chunks)
    }

    fn sgn0(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.sgn0(layouter, x)
    }
}

impl ArithInstructions<F, AssignedNative<F>> for ZkStdLib {
    fn linear_combination(
        &self,
        layouter: &mut impl Layouter<F>,
        terms: &[(F, AssignedNative<F>)],
        constant: F,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.linear_combination(layouter, terms, constant)
    }

    fn mul(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        y: &AssignedNative<F>,
        multiplying_constant: Option<F>,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.mul(layouter, x, y, multiplying_constant)
    }

    fn div(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        y: &AssignedNative<F>,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.div(layouter, x, y)
    }

    fn inv(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.inv(layouter, x)
    }

    fn inv0(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.inv0(layouter, x)
    }
}

impl ZeroInstructions<F, AssignedNative<F>> for ZkStdLib {}

impl<Assigned> ControlFlowInstructions<F, Assigned> for ZkStdLib
where
    Assigned: InnerValue,
    NG: ControlFlowInstructions<F, Assigned>,
{
    fn select(
        &self,
        layouter: &mut impl Layouter<F>,
        cond: &AssignedBit<F>,
        x: &Assigned,
        y: &Assigned,
    ) -> Result<Assigned, Error> {
        self.native_gadget.select(layouter, cond, x, y)
    }

    fn cond_swap(
        &self,
        layouter: &mut impl Layouter<F>,
        cond: &AssignedBit<F>,
        x: &Assigned,
        y: &Assigned,
    ) -> Result<(Assigned, Assigned), Error> {
        self.native_gadget.cond_swap(layouter, cond, x, y)
    }
}

impl FieldInstructions<F, AssignedNative<F>> for ZkStdLib {
    fn order(&self) -> BigUint {
        self.native_gadget.order()
    }
}

impl RangeCheckInstructions<F, AssignedNative<F>> for ZkStdLib {
    fn assign_lower_than_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        value: Value<F>,
        bound: &BigUint,
    ) -> Result<AssignedNative<F>, Error> {
        self.native_gadget.assign_lower_than_fixed(layouter, value, bound)
    }

    fn assert_lower_than_fixed(
        &self,
        layouter: &mut impl Layouter<F>,
        x: &AssignedNative<F>,
        bound: &BigUint,
    ) -> Result<(), Error> {
        self.native_gadget.assert_lower_than_fixed(layouter, x, bound)
    }
}

impl DivisionInstructions<F, AssignedNative<F>> for ZkStdLib {}

impl BinaryInstructions<F> for ZkStdLib {
    fn and(
        &self,
        layouter: &mut impl Layouter<F>,
        bits: &[AssignedBit<F>],
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.and(layouter, bits)
    }

    fn or(
        &self,
        layouter: &mut impl Layouter<F>,
        bits: &[AssignedBit<F>],
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.or(layouter, bits)
    }

    fn xor(
        &self,
        layouter: &mut impl Layouter<F>,
        bits: &[AssignedBit<F>],
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.xor(layouter, bits)
    }

    fn not(
        &self,
        layouter: &mut impl Layouter<F>,
        bit: &AssignedBit<F>,
    ) -> Result<AssignedBit<F>, Error> {
        self.native_gadget.not(layouter, bit)
    }
}

impl BitwiseInstructions<F, AssignedNative<F>> for ZkStdLib {}

impl<const M: usize, const A: usize, T> VectorInstructions<F, T, M, A> for ZkStdLib
where
    T: Vectorizable,
    T::Element: Copy,
    NG: AssignmentInstructions<F, T> + ControlFlowInstructions<F, T>,
{
    fn trim_beginning(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedVector<F, T, M, A>,
        n_elems: usize,
    ) -> Result<AssignedVector<F, T, M, A>, Error> {
        self.vector_gadget.trim_beginning(layouter, input, n_elems)
    }

    fn padding_flag(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedVector<F, T, M, A>,
    ) -> Result<(Box<[AssignedBit<F>; M]>, VectorBounds<F>), Error> {
        self.vector_gadget.padding_flag(layouter, input)
    }

    fn get_limits(
        &self,
        layouter: &mut impl Layouter<F>,
        input: &AssignedVector<F, T, M, A>,
    ) -> Result<VectorBounds<F>, Error> {
        self.vector_gadget.get_limits(layouter, input)
    }

    fn resize<const L: usize>(
        &self,
        layouter: &mut impl Layouter<F>,
        input: AssignedVector<F, T, M, A>,
    ) -> Result<AssignedVector<F, T, L, A>, Error> {
        self.vector_gadget.resize(layouter, input)
    }

    fn assign_with_filler(
        &self,
        layouter: &mut impl Layouter<F>,
        value: Value<Vec<<T>::Element>>,
        filler: Option<<T>::Element>,
    ) -> Result<AssignedVector<F, T, M, A>, Error> {
        self.vector_gadget.assign_with_filler(layouter, value, filler)
    }
}

/// Circuit structure which is used to create any circuit that can be compiled
/// into keys using the ZK standard library.
#[derive(Clone, Debug)]
pub struct MidnightCircuit<'a, R: Relation> {
    relation: &'a R,
    k: u32,
    instance: Value<R::Instance>,
    witness: Value<R::Witness>,
    nb_public_inputs: Rc<RefCell<Option<usize>>>,
    circuit_error: Rc<RefCell<Option<R::Error>>>,
}

impl<'a, R: Relation> MidnightCircuit<'a, R> {
    /// A MidnightCircuit with unknown instance-witness for the given relation.
    /// `k` is the log2 of the circuit size (i.e. the circuit has `2^k` rows).
    /// If `k` is `None`, the optimal value is computed automatically.
    pub fn from_relation(relation: &'a R, k: Option<u32>) -> Self {
        MidnightCircuit::new(relation, Value::unknown(), Value::unknown(), k)
    }

    /// Creates a new MidnightCircuit for the given relation.
    /// `k` is the log2 of the circuit size (i.e. the circuit has `2^k` rows).
    /// If `k` is `None`, the optimal value is computed automatically.
    pub fn new(
        relation: &'a R,
        instance: Value<R::Instance>,
        witness: Value<R::Witness>,
        k: Option<u32>,
    ) -> Self {
        let k = k.unwrap_or_else(|| optimal_k(relation));
        MidnightCircuit {
            relation,
            k,
            instance,
            witness,
            nb_public_inputs: Rc::new(RefCell::new(None)),
            circuit_error: Rc::new(RefCell::new(None)),
        }
    }

    /// Returns the log2 of the circuit size.
    pub fn k(&self) -> u32 {
        self.k
    }

    /// Takes the circuit error stashed during synthesis, if any.
    pub fn take_error(&self) -> Option<R::Error> {
        self.circuit_error.take()
    }
}

/// A verifier key of a Midnight circuit.
#[derive(Clone, Debug)]
pub struct MidnightVK {
    architecture: ZkStdLibArch,
    k: u8,
    nb_public_inputs: usize,
    vk: VerifyingKey<midnight_curves::Fq, KZGCommitmentScheme<midnight_curves::Bls12>>,
}

impl MidnightVK {
    /// Writes a verifying key to a buffer.
    ///
    /// Depending on the `format`:
    /// - `Processed`: Takes less space, but more time to read.
    /// - `RawBytes`: Takes more space, but faster to read.
    ///
    /// Using `RawBytesUnchecked` will have the same effect as `RawBytes`,
    /// but it is not recommended.
    pub fn write<W: io::Write>(&self, writer: &mut W, format: SerdeFormat) -> io::Result<()> {
        self.architecture.write(writer)?;

        writer.write_all(&[self.k])?;

        writer.write_all(&(self.nb_public_inputs as u32).to_le_bytes())?;

        self.vk.write(writer, format)
    }

    /// Reads a verification key from a buffer.
    ///
    /// The `format` must match the one that was used when writing the key.
    /// If the key was written with `RawBytes`, it can be read with `RawBytes`
    /// or `RawBytesUnchecked` (which is faster).
    ///
    /// # WARNING
    /// Use `RawBytesUnchecked` only if you trust the party who wrote the key.
    pub fn read<R: io::Read>(reader: &mut R, format: SerdeFormat) -> io::Result<Self> {
        let architecture = ZkStdLibArch::read(reader)?;

        let mut byte = [0u8; 1];
        reader.read_exact(&mut byte)?;
        let k = byte[0];

        let mut bytes = [0u8; 4];
        reader.read_exact(&mut bytes)?;
        let nb_public_inputs = u32::from_le_bytes(bytes) as usize;

        let mut cs = ConstraintSystem::default();
        let _config = ZkStdLib::configure(&mut cs, (architecture, k - 1));

        let vk = VerifyingKey::read_from_cs::<R>(reader, format, cs)?;

        Ok(MidnightVK {
            architecture,
            k,
            nb_public_inputs,
            vk,
        })
    }

    /// The size of the domain associated to this verifying key.
    pub fn k(&self) -> u8 {
        self.k
    }

    /// The underlying midnight-proofs verifying key.
    pub fn vk(
        &self,
    ) -> &VerifyingKey<midnight_curves::Fq, KZGCommitmentScheme<midnight_curves::Bls12>> {
        &self.vk
    }
}

/// A proving key of a Midnight circuit.
#[derive(Clone, Debug)]
pub struct MidnightPK<R: Relation> {
    k: u8,
    relation: R,
    pk: ProvingKey<midnight_curves::Fq, KZGCommitmentScheme<midnight_curves::Bls12>>,
}

impl<Rel: Relation> MidnightPK<Rel> {
    /// Writes a proving key to a buffer.
    ///
    /// Depending on the `format`:
    /// - `Processed`: Takes less space, but more time to read.
    /// - `RawBytes`: Takes more space, but faster to read.
    ///
    /// Using `RawBytesUnchecked` will have the same effect as `RawBytes`,
    /// but it is not recommended.
    pub fn write<W: io::Write>(&self, writer: &mut W, format: SerdeFormat) -> io::Result<()> {
        writer.write_all(&[self.k])?;

        Rel::write_relation(&self.relation, writer)?;

        self.pk.write(writer, format)
    }

    /// Reads a proving key from a buffer.
    ///
    /// The `format` must match the one that was used when writing the key.
    /// If the key was written with `RawBytes`, it can be read with `RawBytes`
    /// or `RawBytesUnchecked` (which is faster).
    ///
    /// # WARNING
    /// Use `RawBytesUnchecked` only if you trust the party who wrote the key.
    pub fn read<R: io::Read>(reader: &mut R, format: SerdeFormat) -> io::Result<Self> {
        let mut byte = [0u8; 1];

        reader.read_exact(&mut byte)?;
        let k = byte[0];

        let relation = Rel::read_relation(reader)?;

        let pk = ProvingKey::read::<R, MidnightCircuit<Rel>>(
            reader,
            format,
            MidnightCircuit::new(
                &relation,
                Value::unknown(),
                Value::unknown(),
                Some(k as u32),
            )
            .params(),
        )?;

        Ok(MidnightPK { k, relation, pk })
    }

    /// The size of the domain associated to this proving key.
    pub fn k(&self) -> u8 {
        self.k
    }

    /// The underlying midnight-proofs proving key.
    pub fn pk(
        &self,
    ) -> &ProvingKey<midnight_curves::Fq, KZGCommitmentScheme<midnight_curves::Bls12>> {
        &self.pk
    }
}

/// Helper trait, used to abstract the circuit developer from Halo2's
/// boilerplate.
///
/// `Relation` has a default implementation for loading only the tables
/// needed for the requested chips. The developer needs to implement the
/// function [Relation::circuit], which essentially contains the
/// statement of the proof we are creating.
///
/// # Important note
///
/// The API provided here guarantees that the number of public inputs
/// used during verification matches the number of public inputs (as raw
/// scalars) declared in [Relation::circuit] through the
/// [PublicInputInstructions] interface. Proof verification will fail if
/// this requirement is not met.
///
/// # Example
///
/// ```
/// # use midnight_circuits::{
/// #     instructions::{AssignmentInstructions, PublicInputInstructions},
/// #     types::{AssignedByte, Instantiable},
/// # };
/// # use midnight_zk_stdlib::{utils::plonk_api::filecoin_srs, Relation, ZkStdLib, ZkStdLibArch};
/// # use midnight_proofs::{
/// #     circuit::{Layouter, Value},
/// #     plonk::Error,
/// # };
/// # use rand::{rngs::OsRng, Rng, SeedableRng};
/// # use rand_chacha::ChaCha8Rng;
/// # use sha2::Digest;
/// #
/// type F = midnight_curves::Fq;
///
/// #[derive(Clone, Default)]
/// struct ShaPreImageCircuit;
///
/// impl Relation for ShaPreImageCircuit {
///     // When defining a circuit, one must clearly state the instance and the witness
///     // of the underlying NP-relation.
///     type Instance = [u8; 32];
///     type Witness = [u8; 24]; // 192 = 24 * 8
///     type Error = Error;
///
///     // We must specify how the instance is converted into raw field elements to
///     // be process by the prover/verifier. The order here must be consistent with
///     // the order in which public inputs are constrained/assigned in [circuit].
///     fn format_instance(instance: &Self::Instance) -> Result<Vec<F>, Error> {
///         Ok(instance.iter().flat_map(AssignedByte::<F>::as_public_input).collect())
///     }
///
///     // Define the logic of the NP-relation being proved.
///     fn circuit(
///         &self,
///         std_lib: &ZkStdLib,
///         layouter: &mut impl Layouter<F>,
///         _instance: Value<Self::Instance>,
///         witness: Value<Self::Witness>,
///     ) -> Result<(), Error> {
///         let assigned_input = std_lib.assign_many(layouter, &witness.transpose_array())?;
///         let output = std_lib.sha2_256(layouter, &assigned_input)?;
///         output.iter().try_for_each(|b| std_lib.constrain_as_public_input(layouter, b))
///     }
///
///     fn used_chips(&self) -> ZkStdLibArch {
///         ZkStdLibArch {
///             sha2_256: true,
///             ..ZkStdLibArch::default()
///         }
///     }
///
///     fn write_relation<W: std::io::Write>(&self, _writer: &mut W) -> std::io::Result<()> {
///         Ok(())
///     }
///
///     fn read_relation<R: std::io::Read>(_reader: &mut R) -> std::io::Result<Self> {
///         Ok(ShaPreImageCircuit)
///     }
/// }
///
/// const K: u32 = 13;
/// let mut srs = filecoin_srs(K);
///
/// let relation = ShaPreImageCircuit;
///
/// let vk = midnight_zk_stdlib::setup_vk(&srs, &relation);
/// let pk = midnight_zk_stdlib::setup_pk(&relation, &vk);
///
/// let mut rng = ChaCha8Rng::from_entropy();
/// let witness: [u8; 24] = core::array::from_fn(|_| rng.gen());
/// let instance = sha2::Sha256::digest(witness).into();
///
/// let proof = midnight_zk_stdlib::prove::<ShaPreImageCircuit, blake2b_simd::State>(
///     &srs, &pk, &relation, &instance, witness, OsRng,
/// )
/// .expect("Proof generation should not fail");
///
/// assert!(
///     midnight_zk_stdlib::verify::<ShaPreImageCircuit, blake2b_simd::State>(
///         &srs.verifier_params(),
///         &vk,
///         &instance,
///         None,
///         &proof
///     )
///     .is_ok()
/// )
/// ```
pub trait Relation: Clone {
    /// The instance of the NP-relation described by this circuit.
    type Instance: Clone;

    /// The witness of the NP-relation described by this circuit.
    type Witness: Clone;

    /// The error type returned by [Self::circuit] and [Self::format_instance].
    type Error: From<plonk::Error>;

    /// Produces a vector of field elements in PLONK format representing the
    /// given [Self::Instance].
    fn format_instance(instance: &Self::Instance) -> Result<Vec<F>, Self::Error>;

    /// Produces a vector of field elements in PLONK format representing the
    /// data inside the committed instance.
    fn format_committed_instances(_witness: &Self::Witness) -> Vec<F> {
        vec![]
    }

    /// Defines the circuit's logic.
    fn circuit(
        &self,
        std_lib: &ZkStdLib,
        layouter: &mut impl Layouter<F>,
        instance: Value<Self::Instance>,
        witness: Value<Self::Witness>,
    ) -> Result<(), Self::Error>;

    /// Specifies what chips are enabled in the standard library. A chip needs
    /// to be enabled if it is used in [Self::circuit], but it can also be
    /// enabled even if it is not used (possibly to share the same architecture
    /// with other circuits).
    ///
    /// The blanket implementation enables none of them.
    fn used_chips(&self) -> ZkStdLibArch {
        ZkStdLibArch::default()
    }

    /// Writes a relation to a buffer.
    fn write_relation<W: io::Write>(&self, writer: &mut W) -> io::Result<()>;

    /// Reads a relation from a buffer.
    fn read_relation<R: io::Read>(reader: &mut R) -> io::Result<Self>;
}

impl<R: Relation> Circuit<F> for MidnightCircuit<'_, R> {
    type Config = ZkStdLibConfig;

    // FIXME: this could be parametrised by MidnightCircuit.
    type FloorPlanner = SimpleFloorPlanner;

    type Params = (ZkStdLibArch, u8);

    fn without_witnesses(&self) -> Self {
        unreachable!()
    }

    fn params(&self) -> Self::Params {
        (self.relation.used_chips(), (self.k - 1) as u8)
    }

    fn configure_with_params(
        meta: &mut ConstraintSystem<F>,
        params: (ZkStdLibArch, u8),
    ) -> Self::Config {
        ZkStdLib::configure(meta, params)
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        ZkStdLib::configure(meta, (ZkStdLibArch::default(), 8))
    }

    fn synthesize(
        &self,
        config: Self::Config,
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        let max_bit_len = (self.k - 1) as usize;
        let zk_std_lib = ZkStdLib::new(&config, max_bit_len);

        self.relation
            .circuit(
                &zk_std_lib,
                &mut layouter.namespace(|| "Running logic circuit"),
                self.instance.clone(),
                self.witness.clone(),
            )
            .map_err(|e| {
                *self.circuit_error.borrow_mut() = Some(e);
                Error::Synthesis("Relation::circuit error".into())
            })?;

        // After the circuit function has been called, we can update the expected
        // number of raw public inputs in [Self] (via a RefCell). This number will
        // be stored in the MidnightVK so that we can make sure it matches the number of
        // public inputs provided during verification.
        *self.nb_public_inputs.borrow_mut() =
            Some(zk_std_lib.native_gadget.native_chip.nb_public_inputs());

        // We load the tables at the end, once we have figured out what chips/gadgets
        // were actually used.
        zk_std_lib.core_decomposition_chip.load(&mut layouter)?;

        if let Some(sha256_chip) = zk_std_lib.sha2_256_chip {
            if *zk_std_lib.used_sha2_256.borrow() {
                sha256_chip.load(&mut layouter)?;
            }
        }

        if let Some(sha512_chip) = zk_std_lib.sha2_512_chip {
            if *zk_std_lib.used_sha2_512.borrow() {
                sha512_chip.load(&mut layouter)?;
            }
        }

        if let Some(b64_chip) = zk_std_lib.base64_chip {
            if *zk_std_lib.used_base64.borrow() {
                b64_chip.load(&mut layouter)?;
            }
        }

        if let Some(scanner_chip) = zk_std_lib.scanner_chip {
            if *zk_std_lib.used_scanner.borrow() {
                scanner_chip.load(&mut layouter)?;
            }
        }

        if let Some(keccak_sha3_chip) = zk_std_lib.keccak_sha3_chip {
            if *zk_std_lib.used_keccak_or_sha3.borrow() {
                keccak_sha3_chip.load(&mut layouter)?;
            }
        }

        if let Some(blake2b_chip) = zk_std_lib.blake2b_chip {
            if *zk_std_lib.used_blake2b.borrow() {
                blake2b_chip.load(&mut layouter)?;
            }
        }

        Ok(())
    }
}

/// Generates a verifying key for a `MidnightCircuit<R>` circuit.
///
/// The log2 of the circuit size (`k`) is derived from the SRS parameters.
/// For optimal performance, downsize the SRS to the circuit's optimal `k`
/// beforehand (see [optimal_k]). Otherwise, the circuit will use the full
/// size of the SRS, which may be unnecessarily large.
pub fn setup_vk<R: Relation>(
    params: &ParamsKZG<midnight_curves::Bls12>,
    relation: &R,
) -> MidnightVK {
    let k = params.max_k();
    let circuit = MidnightCircuit::from_relation(relation, Some(k));
    let vk = keygen_vk_with_k(params, &circuit, k).expect("keygen_vk should not fail");

    // During the call to [setup_vk] the circuit RefCell on public inputs has been
    // mutated with the correct value. The following [unwrap] is safe here.
    let nb_public_inputs = circuit.nb_public_inputs.clone().borrow().unwrap();

    MidnightVK {
        architecture: relation.used_chips(),
        k: circuit.k as u8,
        nb_public_inputs,
        vk,
    }
}

/// Generates a proving key for a `MidnightCircuit<R>` circuit.
pub fn setup_pk<R: Relation>(relation: &R, vk: &MidnightVK) -> MidnightPK<R> {
    let circuit = MidnightCircuit::new(
        relation,
        Value::unknown(),
        Value::unknown(),
        Some(vk.k() as u32),
    );
    let pk = BlstPLONK::<MidnightCircuit<R>>::setup_pk(&circuit, &vk.vk);
    MidnightPK {
        k: vk.k(),
        relation: relation.clone(),
        pk,
    }
}

/// Produces a proof of relation `R` for the given instance (using the given
/// proving key and witness).
pub fn prove<R: Relation, H: TranscriptHash>(
    params: &ParamsKZG<midnight_curves::Bls12>,
    pk: &MidnightPK<R>,
    relation: &R,
    instance: &R::Instance,
    witness: R::Witness,
    rng: impl RngCore + CryptoRng,
) -> Result<Vec<u8>, R::Error>
where
    G1Projective: Hashable<H>,
    F: Hashable<H> + Sampleable<H>,
{
    let pi = R::format_instance(instance)?;
    let com_inst = R::format_committed_instances(&witness);
    let circuit = MidnightCircuit::new(
        relation,
        Value::known(instance.clone()),
        Value::known(witness),
        Some(pk.k as u32),
    );
    BlstPLONK::<MidnightCircuit<R>>::prove::<H>(
        params,
        &pk.pk,
        &circuit,
        1,
        &[com_inst.as_slice(), &pi],
        rng,
    )
    .map_err(|e| circuit.take_error().unwrap_or_else(|| e.into()))
}

/// Verifies the given proof of relation `R` with respect to the given instance.
/// Returns `Ok(())` if the proof is valid.
pub fn verify<R: Relation, H: TranscriptHash>(
    params_verifier: &ParamsVerifierKZG<midnight_curves::Bls12>,
    vk: &MidnightVK,
    instance: &R::Instance,
    committed_instance: Option<G1Affine>,
    proof: &[u8],
) -> Result<(), R::Error>
where
    G1Projective: Hashable<H>,
    F: Hashable<H> + Sampleable<H>,
{
    let pi = R::format_instance(instance)?;
    let committed_pi = committed_instance.unwrap_or(G1Affine::identity());
    if pi.len() != vk.nb_public_inputs {
        return Err(Error::InvalidInstances.into());
    }
    Ok(BlstPLONK::<MidnightCircuit<R>>::verify::<H>(
        params_verifier,
        &vk.vk,
        &[committed_pi],
        &[&pi],
        proof,
    )?)
}

/// Verifies a batch of proofs with respect to their corresponding vk.
/// This method does not need to know the `Relation` the proofs are associated
/// to and, indeed, it can verify proofs from different `Relation`s.
/// For that, this function does not take `instance`s, but public inputs
/// in raw format (`Vec<F>`).
///
/// Returns `Ok(())` if all proofs are valid.
pub fn batch_verify<H: TranscriptHash + Send + Sync>(
    params_verifier: &ParamsVerifierKZG<midnight_curves::Bls12>,
    vks: &[MidnightVK],
    pis: &[Vec<F>],
    proofs: &[Vec<u8>],
) -> Result<(), Error>
where
    G1Projective: Hashable<H>,
    F: Hashable<H> + Sampleable<H>,
{
    use rayon::prelude::*;

    // TODO: For the moment, committed instances are not supported.
    let n = vks.len();
    if pis.len() != n || proofs.len() != n {
        // TODO: have richer types in halo2
        return Err(Error::InvalidInstances);
    }

    let prepared: Vec<(_, F)> = vks
        .par_iter()
        .zip(pis.par_iter())
        .zip(proofs.par_iter())
        .map(|((vk, pi), proof)| {
            if pi.len() != vk.nb_public_inputs {
                return Err(Error::InvalidInstances);
            }

            let mut transcript = CircuitTranscript::init_from_bytes(proof);
            let dual_msm = prepare::<
                midnight_curves::Fq,
                KZGCommitmentScheme<midnight_curves::Bls12>,
                CircuitTranscript<H>,
            >(
                &vk.vk,
                &[&[midnight_curves::G1Projective::identity()]],
                // TODO: We could batch here proofs with the same vk.
                &[&[pi]],
                &mut transcript,
            )?;
            let summary: F = transcript.squeeze_challenge();
            transcript.assert_empty().map_err(|_| Error::Opening)?;
            Ok((dual_msm, summary))
        })
        .collect::<Result<Vec<_>, Error>>()?;

    let mut r_transcript = CircuitTranscript::init();
    let mut guards = Vec::with_capacity(n);
    for (guard, summary) in prepared {
        r_transcript.common(&summary)?;
        guards.push(guard);
    }
    let r: F = r_transcript.squeeze_challenge();

    let n_guards = guards.len();
    let powers: Vec<F> =
        std::iter::successors(Some(F::ONE), |p| Some(*p * r)).take(n_guards).collect();
    guards.par_iter_mut().enumerate().for_each(|(i, guard)| guard.scale(powers[i]));

    // Phase 4: add scaled guards sequentially.
    let Some(mut acc_guard) = guards.pop() else {
        return Ok(());
    };
    for guard in guards {
        acc_guard.add_msm(guard);
    }
    // TODO: Have richer error types
    acc_guard.verify(params_verifier).map_err(|_| Error::Opening)
}

/// Cost model of the given relation for the given `k`.
/// `k` is the log2 of the circuit size. If `None`, the optimal value is
/// computed automatically.
pub fn cost_model<R: Relation>(relation: &R, k: Option<u32>) -> CircuitModel {
    let circuit = MidnightCircuit::from_relation(relation, k);
    circuit_model::<_, COMMITMENT_BYTE_SIZE, SCALAR_BYTE_SIZE>(&circuit)
}

/// Finds the optimal `k` (log2 of the circuit size) for the given relation.
/// Tries different values of `k` (9..=25) and picks the smallest one where
/// the circuit fits. The pow2range table uses `max_bit_len = k - 1`.
pub fn optimal_k<R: Relation>(relation: &R) -> u32 {
    let mut best_k = u32::MAX;

    for k in 9..=25 {
        let model = cost_model(relation, Some(k));

        if model.k < best_k {
            best_k = model.k;
        }

        // Stop when the pow2range table (2^k rows) becomes the bottleneck.
        if model.rows < (1 << k) {
            break;
        }
    }

    best_k
}