provekit-r1cs-compiler 1.0.0

use {
    crate::{
        binops::add_combined_binop_constraints,
        digits::{add_digital_decomposition, DigitalDecompositionWitnessesBuilder},
        memory::{add_ram_checking, add_rom_checking, MemoryBlock, MemoryOperation},
        poseidon2::add_poseidon2_permutation,
        range_check::add_range_checks,
        sha256_compression::add_sha256_compression,
        spread::get_optimal_spread_width,
    },
    acir::{
        circuit::{
            opcodes::{
                BlackBoxFuncCall, BlockType, ConstantOrWitnessEnum as ConstantOrACIRWitness,
            },
            Circuit, Opcode,
        },
        native_types::{Expression, Witness as NoirWitness},
    },
    anyhow::{bail, Result},
    ark_ff::PrimeField,
    ark_std::One,
    provekit_common::{
        utils::noir_to_native,
        witness::{
            ConstantOrR1CSWitness, ConstantTerm, SumTerm, WitnessBuilder, BINOP_ATOMIC_BITS,
            NUM_DIGITS,
        },
        FieldElement, NoirElement, R1CS,
    },
    std::{collections::BTreeMap, num::NonZeroU32, ops::Neg},
};

/// Detailed breakdown of R1CS constraint and witness counts by circuit
/// component.
///
/// This struct tracks the exact contribution of each ACIR opcode type to the
/// final R1CS size, enabling precise analysis of circuit complexity.
#[derive(Debug, Clone, Default)]
pub struct R1CSBreakdown {
    /// Constraints from ACIR AssertZero opcodes
    pub assert_zero_constraints: usize,
    /// Witnesses added for AssertZero intermediate products
    pub assert_zero_witnesses:   usize,

    /// Constraints for ROM (read-only memory) checking
    pub memory_rom_constraints: usize,
    /// Witnesses for ROM checking
    pub memory_rom_witnesses:   usize,
    /// Constraints for RAM (read-write memory) checking
    pub memory_ram_constraints: usize,
    /// Witnesses for RAM checking
    pub memory_ram_witnesses:   usize,

    /// Constraints for combined AND/XOR binop operations
    pub binop_constraints:  usize,
    /// Witnesses for combined binop operations
    pub binop_witnesses:    usize,
    /// Total number of AND operations
    pub and_ops_total:      usize,
    /// Total number of XOR operations
    pub xor_ops_total:      usize,
    /// Optimal atomic width chosen for binop lookup table
    pub binop_atomic_width: Option<u32>,
    /// Constraints for batched range checks
    pub range_constraints:  usize,
    /// Witnesses for range checks
    pub range_witnesses:    usize,
    /// Total number of range check operations
    pub range_ops_total:    usize,
    /// Optimal base width chosen for range check decomposition
    pub range_base_width:   Option<u32>,

    /// Direct constraints from SHA256 compression (excluding batched ops)
    pub sha256_direct_constraints: usize,
    /// Direct witnesses from SHA256 compression
    pub sha256_direct_witnesses:   usize,
    /// Number of AND operations generated by SHA256
    pub sha256_and_ops:            usize,
    /// Number of XOR operations generated by SHA256
    pub sha256_xor_ops:            usize,
    /// Number of range checks generated by SHA256
    pub sha256_range_ops:          usize,
    /// Optimal spread table width chosen for SHA256 (None if no SHA256)
    pub spread_table_bits:         Option<u32>,

    /// Constraints from Poseidon2 permutation
    pub poseidon2_constraints: usize,
    /// Witnesses from Poseidon2 permutation
    pub poseidon2_witnesses:   usize,
}

/// Compiles an ACIR circuit into an [R1CS] instance, comprising of the A, B,
/// and C R1CS matrices, along with the witness vector.
pub(crate) struct NoirToR1CSCompiler {
    pub(crate) r1cs: R1CS,

    /// Indicates how to solve for each R1CS witness
    pub witness_builders: Vec<WitnessBuilder>,

    /// Maps indices of ACIR witnesses to indices of R1CS witnesses
    acir_to_r1cs_witness_map: BTreeMap<usize, usize>,

    /// Cache for deduplicating product witnesses: (min(a,b), max(a,b)) →
    /// product witness index
    product_cache: std::collections::HashMap<(usize, usize), usize>,

    /// The ACIR witness indices of the initial values of the memory blocks
    pub initial_memories: BTreeMap<usize, Vec<usize>>,
}

/// Compile a Noir circuit to an R1CS relation.
///
/// Returns the R1CS instance, a mapping from Noir witness indices to R1CS
/// witness indices, and the witness builders for solving.
pub fn noir_to_r1cs(
    circuit: &Circuit<NoirElement>,
) -> Result<(R1CS, Vec<Option<NonZeroU32>>, Vec<WitnessBuilder>)> {
    let mut compiler = NoirToR1CSCompiler::new();
    compiler.add_circuit(circuit)?;
    Ok(compiler.finalize())
}

pub fn noir_to_r1cs_with_breakdown(
    circuit: &Circuit<NoirElement>,
) -> Result<(
    R1CS,
    Vec<Option<NonZeroU32>>,
    Vec<WitnessBuilder>,
    R1CSBreakdown,
)> {
    let mut compiler = NoirToR1CSCompiler::new();
    let breakdown = compiler.add_circuit_with_breakdown(circuit)?;
    let (r1cs, map, builders) = compiler.finalize();
    Ok((r1cs, map, builders, breakdown))
}

impl NoirToR1CSCompiler {
    pub(crate) fn new() -> Self {
        let mut r1cs = R1CS::new();
        // Grow the matrices to account for the constant one witness.
        r1cs.add_witnesses(1);
        // We want to get the index of the witness_one index, which should be
        // the current number of witnesses minus one, meaning it is the only
        // witness that has been added so far.
        let witness_one_idx = r1cs.num_witnesses() - 1;
        assert_eq!(witness_one_idx, 0, "R1CS requires first witness to be 1");
        Self {
            r1cs,
            witness_builders: vec![WitnessBuilder::Constant(ConstantTerm(
                witness_one_idx,
                FieldElement::one(),
            ))],
            acir_to_r1cs_witness_map: BTreeMap::new(),
            product_cache: std::collections::HashMap::new(),
            initial_memories: BTreeMap::new(),
        }
    }

    /// Returns the R1CS and the witness map
    pub fn finalize(self) -> (R1CS, Vec<Option<NonZeroU32>>, Vec<WitnessBuilder>) {
        // Convert witness map to vector
        let len = self
            .acir_to_r1cs_witness_map
            .keys()
            .copied()
            .max()
            .map_or_else(|| 0, |i| i + 1);
        let mut map = vec![None; len];
        for (acir_witness_idx, r1cs_witness_idx) in self.acir_to_r1cs_witness_map {
            map[acir_witness_idx] =
                Some(NonZeroU32::new(r1cs_witness_idx as u32).expect("Index zero is reserved"));
        }
        (self.r1cs, map, self.witness_builders)
    }

    /// Index of the constant one witness
    pub const fn witness_one(&self) -> usize {
        0
    }

    /// The number of witnesses in the R1CS instance. This includes the constant
    /// one witness.
    pub fn num_witnesses(&self) -> usize {
        self.r1cs.num_witnesses()
    }

    // Add a new witness to the R1CS instance, returning its index. If the
    // witness builder implicitly maps an ACIR witness to an R1CS witness, then
    // record this.
    pub fn add_witness_builder(&mut self, witness_builder: WitnessBuilder) -> usize {
        let start_idx = self.num_witnesses();
        self.r1cs.add_witnesses(witness_builder.num_witnesses());
        // Add the witness to the mapping if it is an ACIR witness
        if let WitnessBuilder::Acir(r1cs_witness_idx, acir_witness) = &witness_builder {
            self.acir_to_r1cs_witness_map
                .insert(*acir_witness, *r1cs_witness_idx);
        }
        self.witness_builders.push(witness_builder);
        start_idx
    }

    // Return the R1CS witness index corresponding to the AcirWitness provided,
    // creating a new R1CS witness (and builder) if required.
    pub fn fetch_r1cs_witness_index(&mut self, acir_witness_index: NoirWitness) -> usize {
        self.acir_to_r1cs_witness_map
            .get(&acir_witness_index.as_usize())
            .copied()
            .unwrap_or_else(|| {
                self.add_witness_builder(WitnessBuilder::Acir(
                    self.num_witnesses(),
                    acir_witness_index.as_usize(),
                ))
            })
    }

    // Convert a ConstantOrACIRWitness into a ConstantOrR1CSWitness, creating a new
    // R1CS witness (and builder) if required.
    fn fetch_constant_or_r1cs_witness(
        &mut self,
        constant_or_witness: ConstantOrACIRWitness<NoirElement>,
    ) -> ConstantOrR1CSWitness {
        match constant_or_witness {
            ConstantOrACIRWitness::Constant(c) => {
                ConstantOrR1CSWitness::Constant(noir_to_native(c))
            }
            ConstantOrACIRWitness::Witness(w) => {
                let r1cs_witness = self.fetch_r1cs_witness_index(w);
                ConstantOrR1CSWitness::Witness(r1cs_witness)
            }
        }
    }

    /// Add a new witness representing the product of two existing witnesses,
    /// and add an R1CS constraint enforcing this. Returns a cached witness
    /// index if the same (a, b) pair was already computed.
    pub(crate) fn add_product(&mut self, operand_a: usize, operand_b: usize) -> usize {
        let key = (operand_a.min(operand_b), operand_a.max(operand_b));
        if let Some(&cached) = self.product_cache.get(&key) {
            return cached;
        }
        let product = self.add_witness_builder(WitnessBuilder::Product(
            self.num_witnesses(),
            operand_a,
            operand_b,
        ));
        self.r1cs.add_constraint(
            &[(FieldElement::one(), operand_a)],
            &[(FieldElement::one(), operand_b)],
            &[(FieldElement::one(), product)],
        );
        self.product_cache.insert(key, product);
        product
    }

    /// Add a new witness representing the sum of existing witnesses, and add an
    /// R1CS constraint enforcing this. Vector consists of (optional
    /// coefficient, witness index) tuples, one for each summand. The
    /// coefficient is optional, and if it is None, the coefficient is 1.
    pub(crate) fn add_sum(&mut self, summands: Vec<SumTerm>) -> usize {
        let sum =
            self.add_witness_builder(WitnessBuilder::Sum(self.num_witnesses(), summands.clone()));
        let az = summands
            .iter()
            .map(|SumTerm(coeff, witness_idx)| (coeff.unwrap_or(FieldElement::one()), *witness_idx))
            .collect::<Vec<_>>();
        self.r1cs
            .add_constraint(&az, &[(FieldElement::one(), self.witness_one())], &[(
                FieldElement::one(),
                sum,
            )]);
        sum
    }

    /// Add an ACIR assert zero constraint.
    pub fn add_acir_assert_zero(&mut self, expr: &Expression<NoirElement>) {
        // Create individual constraints for all the multiplication terms and collect
        // their outputs
        let mut linear: Vec<(FieldElement, usize)> = vec![];
        let mut a: Vec<(FieldElement, usize)> = vec![];
        let mut b: Vec<(FieldElement, usize)> = vec![];

        if !expr.mul_terms.is_empty() {
            // Process all except the last multiplication term
            linear = expr
                .mul_terms
                .iter()
                .take(expr.mul_terms.len() - 1)
                .map(|(coeff, acir_witness_a, acir_witness_b)| {
                    let a = self.fetch_r1cs_witness_index(*acir_witness_a);
                    let b = self.fetch_r1cs_witness_index(*acir_witness_b);
                    (-noir_to_native(*coeff), self.add_product(a, b))
                })
                .collect::<Vec<_>>();

            // Handle the last multiplication term directly
            let (final_coeff, final_acir_witness_a, final_acir_witness_b) =
                &expr.mul_terms[expr.mul_terms.len() - 1];
            a = vec![(
                noir_to_native(*final_coeff),
                self.fetch_r1cs_witness_index(*final_acir_witness_a),
            )];
            b = vec![(
                FieldElement::one(),
                self.fetch_r1cs_witness_index(*final_acir_witness_b),
            )];
        }

        // Extend with linear combinations
        linear.extend(expr.linear_combinations.iter().map(|term| {
            (
                noir_to_native(term.0).neg(),
                self.fetch_r1cs_witness_index(term.1),
            )
        }));

        // Add constant by multipliying with constant value one.
        linear.push((noir_to_native(expr.q_c).neg(), self.witness_one()));

        // Add a single linear constraint. We could avoid this by substituting
        // back into the last multiplication constraint.
        self.r1cs.add_constraint(&a, &b, &linear);
    }

    fn process_binop_opcode(
        &mut self,
        lhs: ConstantOrACIRWitness<NoirElement>,
        rhs: ConstantOrACIRWitness<NoirElement>,
        output: NoirWitness,
        target_ops: &mut Vec<(ConstantOrR1CSWitness, ConstantOrR1CSWitness, usize)>,
    ) {
        // Get the 32-bit witness indices
        let lhs_witness = match lhs {
            ConstantOrACIRWitness::Witness(w) => self.fetch_r1cs_witness_index(w),
            ConstantOrACIRWitness::Constant(lhs_c) => {
                // lhs is constant
                let lhs_c =
                    self.fetch_constant_or_r1cs_witness(ConstantOrACIRWitness::Constant(lhs_c));
                let ConstantOrR1CSWitness::Constant(lhs_fe) = lhs_c else {
                    unreachable!()
                };
                // Decompose lhs constant into bytes.
                //
                // v1's binop pipeline is hardcoded to 32-bit operands (see the
                // `(value as u32).to_le_bytes()` decomposition below), so any
                // constant wider than 32 bits would be silently truncated.
                // Reject up front rather than producing a wrong proof.
                let lhs_bigint = lhs_fe.into_bigint();
                assert!(
                    lhs_bigint.0[1..].iter().all(|&limb| limb == 0)
                        && lhs_bigint.0[0] <= u32::MAX as u64,
                    "AND/XOR constant lhs exceeds the 32-bit binop limit: {lhs_fe}"
                );
                let lhs_bytes: [u8; 4] = (lhs_bigint.0[0] as u32).to_le_bytes();

                let out_idx = self.fetch_r1cs_witness_index(output);
                let log_bases = vec![BINOP_ATOMIC_BITS; NUM_DIGITS];

                match rhs {
                    ConstantOrACIRWitness::Constant(rhs_c) => {
                        // Both lhs and rhs are constants
                        let rhs_c = self
                            .fetch_constant_or_r1cs_witness(ConstantOrACIRWitness::Constant(rhs_c));
                        let ConstantOrR1CSWitness::Constant(rhs_fe) = rhs_c else {
                            unreachable!()
                        };
                        // See lhs comment above: 32-bit binop limit.
                        let rhs_bigint = rhs_fe.into_bigint();
                        assert!(
                            rhs_bigint.0[1..].iter().all(|&limb| limb == 0)
                                && rhs_bigint.0[0] <= u32::MAX as u64,
                            "AND/XOR constant rhs exceeds the 32-bit binop limit: {rhs_fe}"
                        );
                        let rhs_bytes: [u8; 4] = (rhs_bigint.0[0] as u32).to_le_bytes();

                        let dd = add_digital_decomposition(self, log_bases, vec![out_idx]);
                        for byte_idx in 0..NUM_DIGITS {
                            let lhs_byte = ConstantOrR1CSWitness::Constant(FieldElement::from(
                                lhs_bytes[byte_idx] as u64,
                            ));
                            let rhs_byte = ConstantOrR1CSWitness::Constant(FieldElement::from(
                                rhs_bytes[byte_idx] as u64,
                            ));
                            let out_byte = dd.get_digit_witness_index(byte_idx, 0);
                            target_ops.push((lhs_byte, rhs_byte, out_byte));
                        }
                    }
                    ConstantOrACIRWitness::Witness(rhs_w) => {
                        // lhs constant, rhs witness - decompose rhs witness
                        let rhs_witness = self.fetch_r1cs_witness_index(rhs_w);
                        let dd =
                            add_digital_decomposition(self, log_bases, vec![rhs_witness, out_idx]);
                        for byte_idx in 0..NUM_DIGITS {
                            let lhs_byte = ConstantOrR1CSWitness::Constant(FieldElement::from(
                                lhs_bytes[byte_idx] as u64,
                            ));
                            let rhs_byte = ConstantOrR1CSWitness::Witness(
                                dd.get_digit_witness_index(byte_idx, 0),
                            );
                            let out_byte = dd.get_digit_witness_index(byte_idx, 1);
                            target_ops.push((lhs_byte, rhs_byte, out_byte));
                        }
                    }
                }
                return;
            }
        };
        let rhs_witness = match rhs {
            ConstantOrACIRWitness::Witness(w) => self.fetch_r1cs_witness_index(w),
            ConstantOrACIRWitness::Constant(rhs_c) => {
                // For rhs constant with witness lhs
                let rhs_c =
                    self.fetch_constant_or_r1cs_witness(ConstantOrACIRWitness::Constant(rhs_c));
                let out_idx = self.fetch_r1cs_witness_index(output);
                let log_bases = vec![BINOP_ATOMIC_BITS; NUM_DIGITS];
                let dd = add_digital_decomposition(self, log_bases, vec![lhs_witness, out_idx]);
                // Decompose rhs constant into bytes
                let rhs_bytes: [u8; 4] = if let ConstantOrR1CSWitness::Constant(rhs_fe) = rhs_c {
                    // See lhs comment above: 32-bit binop limit.
                    let rhs_bigint = rhs_fe.into_bigint();
                    assert!(
                        rhs_bigint.0[1..].iter().all(|&limb| limb == 0)
                            && rhs_bigint.0[0] <= u32::MAX as u64,
                        "AND/XOR constant rhs exceeds the 32-bit binop limit: {rhs_fe}"
                    );
                    (rhs_bigint.0[0] as u32).to_le_bytes()
                } else {
                    unreachable!()
                };
                for byte_idx in 0..NUM_DIGITS {
                    let lhs_byte =
                        ConstantOrR1CSWitness::Witness(dd.get_digit_witness_index(byte_idx, 0));
                    let rhs_byte = ConstantOrR1CSWitness::Constant(FieldElement::from(
                        rhs_bytes[byte_idx] as u64,
                    ));
                    let out_byte = dd.get_digit_witness_index(byte_idx, 1);
                    target_ops.push((lhs_byte, rhs_byte, out_byte));
                }
                return;
            }
        };
        let out_idx = self.fetch_r1cs_witness_index(output);

        // Decompose all three 32-bit values into bytes
        let log_bases = vec![BINOP_ATOMIC_BITS; NUM_DIGITS];
        let dd =
            add_digital_decomposition(self, log_bases, vec![lhs_witness, rhs_witness, out_idx]);

        for byte_idx in 0..NUM_DIGITS {
            let lhs_byte = ConstantOrR1CSWitness::Witness(dd.get_digit_witness_index(byte_idx, 0));
            let rhs_byte = ConstantOrR1CSWitness::Witness(dd.get_digit_witness_index(byte_idx, 1));
            let out_byte = dd.get_digit_witness_index(byte_idx, 2);
            target_ops.push((lhs_byte, rhs_byte, out_byte));
        }
    }

    fn add_circuit(&mut self, circuit: &Circuit<NoirElement>) -> Result<()> {
        self.add_circuit_with_breakdown(circuit)?;
        Ok(())
    }

    fn add_circuit_with_breakdown(
        &mut self,
        circuit: &Circuit<NoirElement>,
    ) -> Result<R1CSBreakdown> {
        // Read-only memory blocks (used for building the memory lookup constraints at
        // the end)

        let mut memory_blocks: BTreeMap<usize, MemoryBlock> = BTreeMap::new();
        // Mapping the log of the range size k to the vector of witness indices that
        // are to be constrained within the range [0..2^k].
        // These will be digitally decomposed into smaller ranges, if necessary.
        let mut range_checks: BTreeMap<u32, Vec<usize>> = BTreeMap::new();
        // (input, input, output) tuples for AND and XOR operations.
        // Inputs may be either constants or R1CS witnesses.
        // Outputs are always R1CS witnesses.
        // General ops from Noir blackbox calls (may be >8 bits, need decomposition)
        let mut and_ops = vec![];
        let mut xor_ops = vec![];
        let mut sha256_compression_ops = vec![];
        let mut poseidon2_ops = vec![];

        let mut breakdown = R1CSBreakdown::default();

        let constraints_before_assert = self.r1cs.num_constraints();
        let witnesses_before_assert = self.num_witnesses();

        for opcode in &circuit.opcodes {
            match opcode {
                Opcode::AssertZero(expr) => self.add_acir_assert_zero(expr),
                // Brillig is only for witness generation and does not produce constraints.
                Opcode::BrilligCall { .. } => {}
                Opcode::MemoryInit {
                    block_id,
                    init,
                    block_type,
                } => {
                    if *block_type != BlockType::Memory {
                        panic!("MemoryInit block type must be Memory")
                    }
                    let block_id = block_id.0 as usize;
                    assert!(
                        !memory_blocks.contains_key(&block_id),
                        "Memory block {} already initialized",
                        block_id
                    );
                    let acir_indices: Vec<usize> = init.iter().map(|w| w.0 as usize).collect();
                    self.initial_memories.insert(block_id, acir_indices);
                    let mut block = MemoryBlock::new();
                    init.iter().for_each(|acir_witness| {
                        let r1cs_witness = self.fetch_r1cs_witness_index(*acir_witness);
                        block.initial_value_witnesses.push(r1cs_witness);
                    });
                    memory_blocks.insert(block_id, block);
                }
                Opcode::MemoryOp {
                    block_id,
                    op,
                    predicate,
                } => {
                    // Panic if the predicate is set (according to Noir developers, predicate is
                    // always None and will soon be removed).
                    assert!(
                        predicate.is_none(),
                        "MemoryOp has unexpected predicate: {:?}",
                        predicate
                    );

                    let block_id = block_id.0 as usize;
                    assert!(
                        memory_blocks.contains_key(&block_id),
                        "Memory block {} not initialized before read",
                        block_id
                    );
                    let block = memory_blocks.get_mut(&block_id).unwrap();

                    // `op.index` is _always_ just a single ACIR witness, not a more complicated
                    // expression, and not a constant. See [here](https://discord.com/channels/1113924620781883405/1356865341065531446)
                    // Static reads are hard-wired into the circuit, or instead rendered as a
                    // dummy dynamic read by introducing a new witness constrained to have the value
                    // of the static address.
                    let addr = op.index.to_witness().map_or_else(
                        || {
                            unimplemented!(
                                "MemoryOp index must be a single witness, not a more general \
                                 Expression"
                            )
                        },
                        |acir_witness| self.fetch_r1cs_witness_index(acir_witness),
                    );
                    let op = if op.operation.is_zero() {
                        // Create a new (as yet unconstrained) witness `result_of_read` for the
                        // result of the read; it will be constrained by later memory block
                        // processing.
                        // "In read operations, [op.value] corresponds to the witness index at which
                        // the value from memory will be written." (from the Noir codebase)
                        // At R1CS solving time, only need to map over the value of the
                        // corresponding ACIR witness, whose value is already determined by the ACIR
                        // solver.
                        let result_of_read =
                            self.fetch_r1cs_witness_index(op.value.to_witness().unwrap());
                        MemoryOperation::Load(addr, result_of_read)
                    } else {
                        let new_value =
                            self.fetch_r1cs_witness_index(op.value.to_witness().unwrap());
                        MemoryOperation::Store(addr, new_value)
                    };
                    block.operations.push(op);
                }
                Opcode::BlackBoxFuncCall(black_box_func_call) => match black_box_func_call {
                    BlackBoxFuncCall::RANGE {
                        input: function_input,
                    } => {
                        let input = function_input.input();
                        let num_bits = function_input.num_bits();
                        let input_witness = match input {
                            ConstantOrACIRWitness::Constant(_) => {
                                panic!(
                                    "We should never be range-checking a constant value, as this \
                                     should already be done by the noir-ACIR compiler"
                                );
                            }
                            ConstantOrACIRWitness::Witness(witness) => {
                                self.fetch_r1cs_witness_index(witness)
                            }
                        };
                        range_checks
                            .entry(num_bits)
                            .or_default()
                            .push(input_witness);
                    }

                    // Binary operations:
                    // The inputs and outputs will have already been solved for by the ACIR solver.
                    // Noir blackbox AND/XOR operate on 32-bit values. We decompose into 4 bytes
                    // and add byte-level ops to leverage the combined byte-level lookup table.
                    BlackBoxFuncCall::AND { lhs, rhs, output } => {
                        self.process_binop_opcode(lhs.input(), rhs.input(), *output, &mut and_ops);
                    }
                    BlackBoxFuncCall::XOR { lhs, rhs, output } => {
                        self.process_binop_opcode(lhs.input(), rhs.input(), *output, &mut xor_ops);
                    }
                    BlackBoxFuncCall::Poseidon2Permutation {
                        inputs,
                        outputs,
                        len,
                    } => {
                        assert_eq!(inputs.len() as u32, *len, "Poseidon2: inputs.len != len");
                        assert_eq!(outputs.len() as u32, *len, "Poseidon2: outputs.len != len");
                        let t = *len;

                        // Only these widths are allowed for Poseidon2
                        assert!(
                            matches!(t, 2 | 3 | 4 | 8 | 12 | 16),
                            "Poseidon2: unsupported width {t}"
                        );

                        // Convert ACIR inputs to (Constant | Witness)
                        let in_wits: Vec<ConstantOrR1CSWitness> = inputs
                            .iter()
                            .map(|inp| self.fetch_constant_or_r1cs_witness(inp.input()))
                            .collect();
                        let out_wits: Vec<usize> = outputs
                            .iter()
                            .map(|&w| self.fetch_r1cs_witness_index(w))
                            .collect();
                        poseidon2_ops.push((t, in_wits, out_wits));
                    }
                    BlackBoxFuncCall::Sha256Compression {
                        inputs,
                        hash_values,
                        outputs,
                    } => {
                        let input_witnesses: Vec<ConstantOrR1CSWitness> = inputs
                            .iter()
                            .map(|input| self.fetch_constant_or_r1cs_witness(input.input()))
                            .collect();
                        let hash_witnesses: Vec<ConstantOrR1CSWitness> = hash_values
                            .iter()
                            .map(|hv| self.fetch_constant_or_r1cs_witness(hv.input()))
                            .collect();
                        let output_witnesses: Vec<usize> = outputs
                            .iter()
                            .map(|&output| self.fetch_r1cs_witness_index(output))
                            .collect();
                        sha256_compression_ops.push((
                            input_witnesses,
                            hash_witnesses,
                            output_witnesses,
                        ));
                    }
                    _ => {
                        unimplemented!("Other black box function: {:?}", black_box_func_call);
                    }
                },
                op => bail!("Unsupported Opcode {op}"),
            }
        }

        breakdown.assert_zero_constraints = self.r1cs.num_constraints() - constraints_before_assert;
        breakdown.assert_zero_witnesses = self.num_witnesses() - witnesses_before_assert;

        // Process ROM blocks first (read-only memory uses lookup constraints)
        let constraints_before_rom = self.r1cs.num_constraints();
        let witnesses_before_rom = self.num_witnesses();
        for (_, block) in memory_blocks.iter() {
            if block.is_read_only() {
                add_rom_checking(self, block);
            }
        }
        breakdown.memory_rom_constraints = self.r1cs.num_constraints() - constraints_before_rom;
        breakdown.memory_rom_witnesses = self.num_witnesses() - witnesses_before_rom;

        // Process RAM blocks second (read-write memory uses Spice offline memory
        // checking)
        let constraints_before_ram = self.r1cs.num_constraints();
        let witnesses_before_ram = self.num_witnesses();
        for (_, block) in memory_blocks.iter() {
            if !block.is_read_only() {
                // RAM checking returns witnesses that need range checks for timestamp
                // validation
                let (num_bits, witnesses_to_range_check) = add_ram_checking(self, block);
                let range_check = range_checks.entry(num_bits).or_default();
                witnesses_to_range_check
                    .iter()
                    .for_each(|value| range_check.push(*value));
            }
        }
        breakdown.memory_ram_constraints = self.r1cs.num_constraints() - constraints_before_ram;
        breakdown.memory_ram_witnesses = self.num_witnesses() - witnesses_before_ram;

        // SHA256 compression uses spread-based operations internally
        // (no contribution to batched AND/XOR/range ops)
        let constraints_before_sha256 = self.r1cs.num_constraints();
        let witnesses_before_sha256 = self.num_witnesses();

        let n_sha = sha256_compression_ops.len();
        let n_const_hash = sha256_compression_ops
            .iter()
            .filter(|(_, hash_values, _)| {
                hash_values
                    .iter()
                    .all(|hv| matches!(hv, ConstantOrR1CSWitness::Constant(_)))
            })
            .count();
        let spread_w = if n_sha > 0 {
            Some(get_optimal_spread_width(n_sha, n_const_hash))
        } else {
            None
        };
        let sha256_range_checks = if let Some(w) = spread_w {
            add_sha256_compression(self, sha256_compression_ops, w)
        } else {
            BTreeMap::new()
        };

        breakdown.sha256_direct_constraints =
            self.r1cs.num_constraints() - constraints_before_sha256;
        breakdown.sha256_direct_witnesses = self.num_witnesses() - witnesses_before_sha256;
        breakdown.sha256_and_ops = 0;
        breakdown.sha256_xor_ops = 0;
        breakdown.sha256_range_ops = sha256_range_checks.values().map(|v| v.len()).sum();
        breakdown.spread_table_bits = spread_w;

        // Merge spread sub-chunk range checks into global range checks
        for (bits, witnesses) in sha256_range_checks {
            range_checks.entry(bits).or_default().extend(witnesses);
        }

        breakdown.and_ops_total = and_ops.len();
        breakdown.xor_ops_total = xor_ops.len();
        let constraints_before_binop = self.r1cs.num_constraints();
        let witnesses_before_binop = self.num_witnesses();
        breakdown.binop_atomic_width = add_combined_binop_constraints(self, and_ops, xor_ops);
        breakdown.binop_constraints = self.r1cs.num_constraints() - constraints_before_binop;
        breakdown.binop_witnesses = self.num_witnesses() - witnesses_before_binop;
        let constraints_before_poseidon = self.r1cs.num_constraints();
        let witnesses_before_poseidon = self.num_witnesses();
        add_poseidon2_permutation(self, poseidon2_ops);
        breakdown.poseidon2_constraints = self.r1cs.num_constraints() - constraints_before_poseidon;
        breakdown.poseidon2_witnesses = self.num_witnesses() - witnesses_before_poseidon;

        breakdown.range_ops_total = range_checks.values().map(|v| v.len()).sum();
        let constraints_before_range = self.r1cs.num_constraints();
        let witnesses_before_range = self.num_witnesses();
        breakdown.range_base_width = add_range_checks(self, range_checks);
        breakdown.range_constraints = self.r1cs.num_constraints() - constraints_before_range;
        breakdown.range_witnesses = self.num_witnesses() - witnesses_before_range;

        Ok(breakdown)
    }
}