Audit of OpenVM 2.0

Description. The deferral aggregation root is not a canonical commitment to the proved deferral IO list. A malicious prover can make an absent padding child contribute an attacker-chosen digest to the aggregation root, and the hook layer can then interpret that same digest as a valid IO leaf.

The immediate AIR bug is that DeferralAggPvsAir does not enforce that padding children use a canonical padding value. The child-specific constraints are gated by is_present (crates/continuations/src/circuit/deferral/inner/def_pvs/air.rs:94-126), so when is_present = 0, the child’s values are mostly unconstrained. However, the parent aggregation hash still includes next.merkle_commit (crates/continuations/src/circuit/deferral/inner/def_pvs/air.rs:206-214):

self.poseidon2_bus.lookup_key(
    builder,
    Poseidon2CompressMessage {
        input: digests_to_poseidon2_input(local.merkle_commit, next.merkle_commit)
            .map(Into::into),
        output: merkle_commit.map(Into::into),
    },
    is_first_of_two_rows,
);

The honest trace generator fills the absent row slot with canonical padding (crates/continuations/src/circuit/deferral/inner/def_pvs/trace.rs:79-84), but the AIR does not require a malicious prover to do the same. This lets an attacker produce a valid aggregation proof with a public root of the form R = H(real_child_merkle_commit, attacker_chosen_padding) while still reporting num_def_circuit_proofs = 1.

The count check does not prevent this. num_def_circuit_proofs counts the number of present deferral proofs, but it does not bind the Merkle tree shape or role of the resulting root. A two-row aggregation node with one present child and one absent child still reports one real proof. The hook can therefore decommit the same root R as a one-leaf IO Merkle tree where input_commit = real_child_merkle_commit, output_commit = attacker_chosen_padding, and leaf_hash = H(input_commit, output_commit). The hook decommit layer only sends leaves marked by send_commits (crates/continuations/src/circuit/deferral/hook/decommit/air.rs:61-97), and the hook verifier checks that the number of onion-hashed leaves equals num_def_circuit_proofs (crates/continuations/src/circuit/deferral/hook/verifier/air.rs:257-264). Since both views contain exactly one real item, the count check does not detect that an aggregation internal node is being interpreted as a hook IO leaf.

This reinterpretation is possible because the same Poseidon2 compression format is used for aggregation internal nodes and hook IO leaves. There is no domain-separation tag distinguishing H(left_child_root, right_child_root) from H(input_commit, output_commit).

Impact. The verifier accepts a proof claiming a valid deferred call synthetic_input_commit -> attacker_chosen_output_commit even though the real underlying deferral proof was for an unrelated computation.

We confirmed this with a test against the production root verifier. The PoC attack constructs a malicious deferral aggregation by mutating the absent padding child’s merkle_commit to encode a desired forged output commitment, routes the resulting padded aggregation root through the deferral hook layer and the full VM/deferral continuation aggregation up to the root prover, and confirms that the final root verifier accepts the resulting proof. Using a small guest that reads an input commit and an expected output (a pattern similar to crates/continuations/programs/examples/multiple.rs and analogous in style to crates/sdk/programs/examples/verify-stark.rs), the PoC produces two independently verifying root proofs for the same guest binary and same claimed input commit, accepting two different outputs.

Recommendation.

The immediate fix is to ensure absent children cannot contribute unconstrained data. In DeferralAggPvsAir, constrain every non-present child row’s merkle_commit to the depth-appropriate canonical padding digest already used by the honest trace generator. The important property is that the public aggregation root must be a deterministic function of the present children and the canonical tree shape, not of prover-chosen padding columns.

As additional hardening, bind the Merkle tree shape/depth to num_def_circuit_proofs so that a root produced as an internal aggregation node cannot be decommitted later as a one-leaf IO tree with the same count. Finally, add domain separation between aggregation leaf hashes, aggregation internal hashes, hook IO leaf hashes, and hook internal hashes, for example by including a role tag in the Poseidon2 input.

Client response. PR #2815 partially fixes this issue by constraining absent deferral aggregation padding to the canonical zero hash and adding Merkle depth to the deferral aggregation public values. This addresses the direct attacker-chosen-padding primitive and adds shape/depth accounting. Additionally, domain separation between the input and output commitments compression and internal compression has been implemented in PR #2857, which solves this class of reinterpretation issues altogether.

Description. The host VmStarkProof verifier accepts deferral_flag = 0 by checking only that the deferral public values are unset: def_hook_commit, initial_acc_hash, final_acc_hash, and depth are zero values.

// Deferral verification
if let Some(expected_def_hook_commit) = vk.baseline.expected_def_hook_commit {
    let &VerifierDefPvs {
        deferral_flag,
        def_hook_commit,
    } = verifier_def_pvs_slice.borrow();

    let &DeferralPvs {
        initial_acc_hash,
        final_acc_hash,
        depth,
    } = proof.inner.public_values[DEF_PVS_AIR_ID]
        .as_slice()
        .borrow();

    if deferral_flag == F::ZERO {
        if !is_unset(&def_hook_commit) {
            return Err(VerifyStarkError::DefHookCommitSet {
                actual: def_hook_commit,
            });
        } else if !is_unset(&initial_acc_hash) {
            return Err(VerifyStarkError::DefInitialAccHashCommitSet {
                actual: initial_acc_hash,
            });
        } else if !is_unset(&final_acc_hash) {
            return Err(VerifyStarkError::DefFinalAccHashCommitSet {
                actual: final_acc_hash,
            });
        } else if depth != F::ZERO {
            return Err(VerifyStarkError::DefDepthSet { actual: depth });
        }
    } ...

However, these checks were not enough because they do not prove that the DEFERRAL_AS memory subtree stayed untouched throughout VM execution.

This also differs from the root verifier AIR. In the root circuit, even when the deferrals are unset, the deferral Merkle path still proves that the deferral address space did not change by enforcing the equality between the initial and final path nodes inside DEFERRAL_AS:

assert_array_eq(
    &mut builder.when(and(local.is_within_deferral_as, local.is_unset)),
    local.initial_node_commit,
    local.final_node_commit,
);

As a result, a malicious prover can produce a valid VmStarkProof whose execution uses deferral CALL instructions and mutates deferral memory by setting deferral_flag = 0 and omitting the deferral Merkle proof, causing the verifier to skip the deferral Merkle opening entirely.

Impact. A malicious prover can make native SDK verification accept a VM proof that consumed forged or unproven deferred inputs and/or outputs. The VM proof remains internally valid, and its final_root commits to the mutated deferral memory, but the verifier never checks that the mutation is represented by initial_acc_hash / final_acc_hash. Practically, this can forge a proof guarded by the guest-level verify_stark function that relies on deferred verification.

Note that this only affects VmStarkProof SDK verification and does not affect EVM verification, since the root circuit should reject the same condition.

Recommendation. Even if deferral_flag == 0, the verifier should enforce the Merkle opening check that requires all initial/final nodes inside DEFERRAL_AS are equal, mirroring the root verifier AIR constraints.

Client response. PR #2817 addresses this finding. The host verifier now requires and verifies deferral Merkle proofs whenever deferrals are enabled, regardless of the deferral_flag value.

Description. The host deferral verifier checks the initial and final deferral accumulator paths (initial_acc_hash and final_acc_hash) independently using the supplied Merkle proofs, such that it recomputes:

• initial_acc_hash $\Rightarrow$ initial_root
• final_acc_hash $\Rightarrow$ final_root

However, it never checks that initial_merkle_proof[level] == final_merkle_proof[level] for a level that is inside DEFERRAL_AS memory but outside the aggregated deferral subtree. This means that if there are 2 deferrals at the same tree level and only one of them is aggregated, the other deferral (the sibling node) is not enforced to remain unchanged throughout the VM execution. The simplified tree is depicted below:

This is in contrast with the root verifier AIR, which explicitly enforces this missing invariant: while the path is still inside DEFERRAL_AS, it requires the initial and final siblings to be equal, proving that all deferral accumulator subtrees not covered by the aggregate were unchanged:

assert_array_eq(
    &mut builder.when(local.is_within_deferral_as),
    local.initial_sibling,
    local.final_sibling,
);

Impact. This effectively allows a malicious prover to forge the effect of a deferral hook proof for an omitted deferral subtree: the VM can consume a deferred input/output at that index, while the verification accepts without any corresponding hook proof being aggregated.

As a proof of concept, consider the following guest program which has two deferred verify_stark calls:

#![cfg_attr(target_os = "zkvm", no_main)]
#![cfg_attr(target_os = "zkvm", no_std)]

extern crate alloc;

use alloc::vec::Vec;

use openvm::io::read;
use openvm_deferral_guest::Commit;
use openvm_verify_stark_guest::{verify_stark, ProofOutput};

openvm::entry!(main);

fn read_expected() -> (ProofOutput, Commit) {
    let app_exe_commit: Commit = read();
    let app_vm_commit: Commit = read();
    let user_public_values: Vec<u8> = read();
    let input_commit: Commit = read();

    (
        ProofOutput {
            app_exe_commit,
            app_vm_commit,
            user_public_values,
        },
        input_commit,
    )
}

pub fn main() {
    let (expected_0, input_commit_0) = read_expected();
    verify_stark::<0>(&input_commit_0, &expected_0);

    let (expected_1, input_commit_1) = read_expected();
    verify_stark::<1>(&input_commit_1, &expected_1);
}

An SDK prover can execute the guest program, while supplying a hook proof for only one of them. The second deferral’s input/output can still be supplied through the VM execution deferral state, so the guest observes it as if it came from deferred verification, but the host verifier only checks the aggregate for the first deferral, as seen in the following snippet:

// Honest child proof for deferral index 0.
let honest_child_vk = VmStarkVerifyingKey {
    mvk: child_agg_vk,
    baseline: child_baseline,
};

let honest_state = get_deferral_state(
    &honest_child_vk,
    from_ref(&honest_child_proof),
    0,
)?;

// Forged deferral result for index 1.
// This output is chosen by the malicious prover and is not backed by a hook proof.
let fake_state = DeferralState::new(generate_deferral_results(
    vec![RawDeferralResult {
        input: fake_input_commit.to_vec(),
        output_raw: fake_output_raw, // app_exe_commit || app_vm_commit || user_public_values
    }],
    1, // deferral index 1
    &deferral_poseidon2_chip::<F>(),
));

// Guest stdin contains the expected values that the guest will compare against
// the two deferred outputs.
let mut stdin = StdIn::default();
stdin.write(&honest_app_exe_commit);
stdin.write(&honest_app_vm_commit);
stdin.write(&honest_user_public_values);
stdin.write(&honest_input_commit);

stdin.write(&fake_app_exe_commit);
stdin.write(&fake_app_vm_commit);
stdin.write(&fake_user_public_values);
stdin.write(&fake_input_commit);

// VM execution sees both deferrals.
stdin.deferrals = vec![honest_state, fake_state];

// But the deferral proof path receives only the honest child proof for idx0.
let def_input = DeferralInput::from_inputs(from_ref(&honest_child_proof));

// Host aggregation proof is generated with one hook proof,
// while VM execution used two deferral states.
let (proof, _) = prover.prove(stdin, from_ref(&def_input))?;

// Vulnerable acceptance: host verification accepts because it checks the
// covered aggregate path, but does not prove the omitted sibling stayed unchanged.
Sdk::verify_proof(agg_vk, baseline, &proof)?;

Note that this only affects VmStarkProof SDK verification and does not affect EVM verification, since the root circuit should reject the same condition.

Recommendation. The host verifier should enforce the equality of the initial and final siblings for every Merkle tree level inside DEFERRAL_AS that is outside the aggregated subtree, mirroring the root verifier AIR invariant.

Client response. PR #2817 addresses this finding. The host verifier now checks that the deferral address space outside the claimed aggregated subtree is unchanged.

Description. The recursive aggregation depth is unbounded, so a malicious prover can perform any polynomial number of aggregation steps. This is not inherently a problem for Merkle claims: a Merkle root remains binding for polynomial-length paths. However, some aggregation metadata is accumulated as native field elements rather than as bounded integers.

Two such values are:

• The depth used in memory Merkle aggregation, which is incremented as a field element.
• num_def_circuit_proofs, which is read from child proofs and summed into the parent proof.

Because the BabyBear field is relatively small, these counters can wrap around. For the memory Merkle depth, an overflow would require $O(|𝔽|)$ aggregation steps. This could let a prover craft, for example, a root with depth = 0 or a pseudo-random root with depth = 1, but we did not identify an immediate soundness issue from this path alone.

For num_def_circuit_proofs, overflow is more practical. At each binary aggregation step, the counter can double, so wrapping the counter only requires $O(\log |𝔽|)$ aggregation steps. By aggregating trees of different heights, the prover can effectively choose the overflowed value using a double-and-add strategy. In particular, the prover can make the overflowed num_def_circuit_proofs equal to 1, which lets the hook layer interpret the aggregated Merkle root as if it contained a single real IO leaf right below the root.

This has the same shape as the padded-root reinterpretation issue: an aggregation internal node can be opened as a hook IO leaf. The root cause is different from arbitrary padding, but the issue relies on the same lack of separation between leaf hashes and internal-node hashes.

Impact. A malicious prover can use counter overflow to make an aggregated deferral tree appear to contain a different number of deferral circuit proofs than it actually contains. With the concrete num_def_circuit_proofs = 1 case, this enables the same kind of Merkle-root reinterpretation as the padded deferral aggregation issue.

Recommendation. Treat aggregation counters as bounded integers, not unconstrained field accumulators. Enforce range bounds or structural constraints that prevent depth and num_def_circuit_proofs from wrapping, and bind num_def_circuit_proofs to the aggregation tree shape. As hardening, domain-separate leaf hashes from internal-node hashes so that an aggregation root cannot be reinterpreted as a hook IO leaf.

Client Response. This issue has been addressed in PRs #2815 and #2838. The circuits now keep track of the Merkle depth and range-check it against MAX_DEF_AGG_MERKLE_DEPTH, set to 20. Additionally, domain separation between the input and output commitments compression and internal compression has been implemented in PR #2857, which solves this class of reinterpretation issues altogether.

Description. Interaction hashing adds 1 to interaction.bus_index, but BusIndex is a u16.

let num = evaluator.eval_expr(&interaction.count);
let denom = interaction
    .message
    .iter()
    .map(|expr| evaluator.eval_expr(expr))
    .chain(std::iter::once(SC::EF::from_u16(interaction.bus_index + 1)))
    .zip(beta_logup.powers())
    .fold(SC::EF::ZERO, |acc, (x, y)| acc + x * y);
(num, denom)

In release builds, this addition can wrap around, so interaction.bus_index = 2^16 - 1 is mapped to 0 instead of 2^16. As a result, a user defining an AIR with interactions on bus 2^16 - 1 can cause the verifier to hash the zero bus value, which would completely break soundness for interactions and allow arbitrary forged interactions.

The documentation for BusIndex states that all valid instantiations of BusIndex are safe, which suggests that the verifier should not be performing arithmetic on bus indices that can overflow.

// Must be a type smaller than u32 to make BusIndex p - 1 unrepresentable.
pub type BusIndex = u16;

// ...

/// The bus index specifying the bus to send the message over. All valid instantiations of
/// `BusIndex` are safe.
pub bus_index: BusIndex,

However, the current hashing logic computes +1 over u16, which breaks this expectation at the maximal value. This is particularly relevant because the low-level AIR builder allows interactions to be pushed to arbitrary bus indices by circuit designers, including 2^16 - 1.

Impact. A user can define a circuit using bus index 2^16 - 1 for which the verifier computes the wrong message hash. This can enable forged interactions and breaks soundness for such circuits.

Recommendation. Perform the increment after widening the bus index to a larger integer or directly to a field element. For example, compute the bus index as SC::EF::from_u16(interaction.bus_index) + SC::EF::ONE. Alternatively, reject 2^16 - 1 as an invalid bus index at key generation time.

Client response. This issue has been fixed in PR #312 by computing the increment after casting the bus index to a field element, avoiding overflow.

Description. The proof codec admits multiple distinct byte encodings for the same logical proof through two independent decoding issues.

First, trace_vdata presence flags are encoded as a bitmap in Proof::encode. When the number of AIRs is not a multiple of 8, the final bitmap byte contains unused padding bits. During decoding, those bits are ignored rather than required to be zero:

for byte in bitmap {
    for i in 0u8..8 {
        if trace_vdata.len() >= num_airs {
            break;
        }
        if byte & (1u8 << i) != 0 {
            trace_vdata.push(Some(TraceVData::decode(reader)?));
        } else {
            trace_vdata.push(None);
        }
    }
}

As a result, an attacker can flip the unused high bits of the last bitmap byte without changing the decoded Proof.

Second, BabyBearBn254Poseidon2Config canonically encodes BN254 digest elements, but its decoder accepts non-canonical 32-byte encodings:

let big = BigUint::from_bytes_be(&buf);
*val = Bn254Scalar::from_biguint(big)
    .ok_or_else(|| io::Error::other("invalid Bn254 element"))?;

Bn254Scalar::from_biguint does not enforce that the input is strictly less than the BN254 modulus, so distinct byte strings such as x and x + p may decode to the same field element. Since digests appear throughout proof decoding, including commitments and Merkle proof siblings, this also creates alternative serialized forms of the same proof.

Together, these issues make the proof encoding non-canonical.

Impact. Given a valid proof $\pi$, anyone can produce a distinct proof ${\pi }^{\prime }$ by either modifying ignored trace_vdata bitmap padding bits or replacing canonical BN254 digest encodings with non-canonical ones.

Recommendation. Enforce canonical proof decoding in both places. In Proof::decode, reject any non-zero padding bits in the final trace_vdata bitmap byte. In BabyBearBn254Poseidon2Config::decode_digest, reject any 32-byte integer greater than or equal to the BN254 modulus instead of accepting it via from_biguint.

Client Response. This issue has been acknowledged and fixed in PR #356.

Description. The proof codec does not enforce full consumption of the input byte slice when decoding a standalone proof. The generic helper Decode::decode_from_bytes wraps the input in a Cursor and returns after a single decode call:

fn decode_from_bytes(bytes: &[u8]) -> Result<Self> {
    let mut reader = Cursor::new(bytes);
    Self::decode(&mut reader)
}

At the top level, Proof::decode reconstructs a proof from the reader and returns immediately after decoding the expected fields:

Ok(Self {
    common_main_commit,
    trace_vdata,
    public_values,
    gkr_proof: GkrProof::decode(reader)?,
    batch_constraint_proof: BatchConstraintProof::decode(reader)?,
    stacking_proof: StackingProof::decode(reader)?,
    whir_proof: WhirProof::decode(reader)?,
})

No check is performed to ensure that the reader has reached EOF. As a result, if a proof is decoded from a standalone byte blob, any arbitrary suffix appended after a valid proof is ignored. Distinct byte strings of the form proof || suffix therefore decode to the same Proof object.

Impact. Given a valid serialized proof, anyone can append extra trailing bytes to produce a different proof blob that still decodes to the same proof and verifies successfully. This makes proof bytes non-canonical and can break systems that compare, hash, or deduplicate proofs by raw bytes.

Recommendation. After Proof::decode finishes decoding the expected proof fields, check that the input stream is at EOF and reject the input if any bytes remain. This ensures that only exact proof encodings are accepted and prevents arbitrary trailing-byte malleability.

Client Response. This issue has been acknowledged and fixed in PR #356.

Description. The fractional sumcheck GKR verification is supposed to handle zero-interaction AIRs by asserting that q0_claim is exactly one.

if total_rounds == 0 {
    // Proof shape asserts that `proof.claims_per_layer` and `proof.sumcheck_polys` are empty.
    debug_assert!(proof.claims_per_layer.is_empty());
    debug_assert!(proof.sumcheck_polys.is_empty());
    if proof.q0_claim != SC::EF::ONE {
        return Err(GkrVerificationError::InvalidZeroRoundValue {
            actual: proof.q0_claim,
        });
    }
    return Ok((SC::EF::ZERO, SC::EF::ONE, vec![]));
}

However, this check is incorrect and unreachable because of the following:

1. This check can only be reached if total_rounds == 0, which is unreachable as long as l_skip > 0, since if the total_interactions == 0, then total_rounds = l_skip + n_logup = l_skip + 0.
2. This check should return (0, alpha_logup) instead of (0, 1) to satisfy the downstream denominator check.
3. In the higher function call, there is an additional conditional statement that guards the verify_gkr function, which is only called if total_interactions is more than zero:

if total_interactions > 0 {
    (p_xi_claim, q_xi_claim, xi) =
        verify_gkr::<SC, TS>(gkr_proof, transcript, l_skip + n_logup)?;
    debug_assert_eq!(xi.len(), l_skip + n_logup);
}

As a result, q0_claim is never checked, so it is freely malleable and can be mutated to any arbitrary field element while the modified proof still passes verification.

Impact. Given a valid proof $\pi$, anyone can produce a distinct proof ${\pi }^{\prime }$ by changing q0_claim to any value in the extension field. While the soundness of statement verification itself is not affected, the ability to generate multiple valid proof representations has concrete implications for systems built on top of the verifier, such as bypassing proof-based replay protection mechanisms.

Recommendation. Make the early return inside verify_gkr reachable when there are no interactions, and remove the outer if total_interactions > 0 guard so that verify_gkr runs unconditionally. The early return value should also be corrected from (0, 1) into (0, alpha_logup) to satisfy the downstream denominator check.

Client Response. This issue has been acknowledged and fixed in PR #326.

Description. The host verifier checks the validity of the public values (UserPublicValuesProof) by deriving the public values subtree height from the prover-supplied length instead of checking it against the publicly configured num_user_pvs. The underlying check in UserPublicValuesProof::verify() only requires the supplied length to be a power-of-two multiple of CHUNK:

let pvs = &self.public_values;
if !pvs.len().is_multiple_of(CHUNK) || !(pvs.len() / CHUNK).is_power_of_two() {
    return Err(UserPublicValuesProofError::UnexpectedLength(pvs.len()));
}
let pv_height = log2_strict_usize(pvs.len() / CHUNK);
let proof_len = memory_dimensions.overall_height() - pv_height;

As a result, the values in proof.user_pvs_proof can be malleated in two possible ways:

1. Truncation: The adversary truncates public_values with shorter values, recomputes public_values_commit for the shorter vector, and adds the Merkle root of the removed values to the proof. See the diagram below for the concrete attack example.
2. Extension: The adversary appends public_values from the adjacent authenticated subtree, recomputes public_values_commit for the larger vector, and removes the Merkle sibling that previously represented those appended values from proof. Note that the appended values cannot be arbitrary since they must match the adjacent memory subtree already authenticated by the original Merkle path.

Impact. Given a valid proof $\pi$ and public statement $x$, anyone can produce a distinct statement $x^{\prime }$ by truncating or extending the attached user public values vector from $x$, as long as the mutated vector still Merkle-opens to the same final memory root.

While the extension is possible, the public values vector can only be extended with values that match the adjacent authenticated memory subtree already committed by the original Merkle path. In practice, this is usually only feasible for known subtrees such as unused zero-filled memory. So, truncation is the main practical impact here.

This issue affects both the SDK verification of ContinuationVmProof and VmStarkProof.

Recommendation. We suggest pinning num_user_pvs in every host verifier entry point. It is recommended that num_user_pvs be added to VerificationBaseline so that it is tied to the verifier configuration material.

Client response. PR #2817 addresses this finding for VmStarkProof verification. VerificationBaseline now records the expected number of raw user public values, and the host verifier rejects proofs whose user public value proof length does not match the baseline.

Since the same issue also affects SDK verification of ContinuationVmProof, this is addressed separately in PR #2835, as it is outside the scope of this phase.

Description. DeferralPvs.depth controls how many low Merkle levels are skipped before initial_acc_hash and final_acc_hash are opened against the VM memory roots. The host verifier checks that depth is not larger than the overall memory tree height, but it does not require nonzero depths to satisfy depth <= memory_dimensions.address_height, which is the height of the deferral address-space subtree. As a result, an oversized depth can move the opening above DEFERRAL_AS.

In DeferralMerkleProofs::verify, the only validation on the proof shape is that each Merkle proof has length overall_height(); depth is then passed straight through as the number of skipped levels (crates/verify/src/deferral.rs:53-68):

let overall_height = memory_dimensions.overall_height();
if self.initial_merkle_proof.len() != overall_height {
    return Err(VerifyStarkError::DeferralMerkleProofLengthMismatch { /* ... */ });
}
// ... same check for final_merkle_proof ...

let is_unset = depth == 0;
let skip_depth = if is_unset { 0 } else { depth };
let idx_prefix =
    usize::try_from(memory_dimensions.label_to_index((DEFERRAL_AS, 0))).unwrap();

skip_depth is used directly in merkle_path_root, which skips the first skip_depth siblings and walks the remaining levels to the root (crates/verify/src/deferral.rs:110-131). There is no constraint relating depth to address_height, so any depth in [1, overall_height] is accepted, including values that skip past the deferral subtree boundary.

This is reachable through the full public-value verifier: depth is read from DeferralPvs and forwarded into DeferralMerkleProofs::verify with no bound check (crates/verify/src/lib.rs:275-317).

This was confirmed with proof-of-concept tests. One sets depth = address_height + 1 (greater than address_height, still within overall_height) and shows the Merkle-path check accepts it. Another drives the full public-value verifier with an oversized depth whose opened subtree also covers PUBLIC_VALUES_AS, and the verifier accepts.

Impact. The binding between the deferral hook’s accumulator claims and the VM’s actual deferral accumulator memory is weakened. Instead of proving that the accumulator lives inside the deferral region, the proof may authenticate a larger subtree that also includes unrelated memory regions (for example PUBLIC_VALUES_AS). A direct end-to-end exploit is not obvious without another way to make the accumulator public values match such an oversized subtree root, but the verifier is checking the wrong invariant: the opening should be pinned to the DEFERRAL_AS subtree.

Recommendation. Enforce 1 <= depth <= memory_dimensions.address_height so the deferral opening always terminates at the root of the DEFERRAL_AS subtree and cannot be raised into sibling address spaces. This bound should be enforced consistently in both the native host verifier (crates/verify) and the root AIR (crates/continuations/src/circuit/root/def_paths).

Client response. PR #2817 addresses this finding. It adds the missing bound in both the native verifier and the root AIR path logic.

Description. The verifier absorbs proof-derived BabyBear wires into the Fiat-Shamir transcript, and hashes them into WHIR Merkle leaves, without first reducing them to a canonical representative. The wires it absorbs are loaded from the proof by load_witness, which only range-checks the magnitude to 31 bits:

pub fn load_witness(&self, ctx: &mut Context<Fr>, value: BabyBear) -> BabyBearWire {
    let value = ctx.load_witness(Fr::from(PrimeField64::as_canonical_u64(&value)));
    self.range.range_check(ctx, value, BABYBEAR_MAX_BITS); // BABYBEAR_MAX_BITS = 31
    BabyBearWire { value, max_bits: BABYBEAR_MAX_BITS }
}

A prover-supplied wire is therefore constrained only to lie in $[0,2^{31})$, not in the canonical range $[0,p)$ with $p=p_{BB}=\mathtt{0}\mathtt{x}\mathtt{78000001}$. Since $p<2^{31}$, the interval $[0,2^{31})$ contains non-canonical representatives: for every $x<2^{31}-p$ both $x$ and $x+p$ are valid 31-bit witnesses, distinct cells, but equal as BabyBear elements. The arithmetic gadgets route everything through signed_div_mod and so only ever compare values modulo $p$; the two cells are interchangeable for every algebraic constraint.

The transcript and the Merkle leaf hash, on the other hand, consume the raw cell, packed in base $2^{31}$:

/// Result = values[0] + values[1]*2^31 + values[2]*2^62 + ...
fn pack_base_2_31(ctx, gate, values: &[BabyBearWire]) -> AssignedValue<Fr> {
    gate.inner_product(ctx, values.iter().map(|v| v.value),
        gate.pow_of_two().iter().step_by(BABY_BEAR_BITS).take(values.len()).copied().map(Constant))
}

observe buffers up to NUM_OBS_PER_WORD = 8 wires and packs them this way; WHIR Merkle leaves are loaded with the same 31-bit load_witness (stages/whir/mod.rs:108-147) and hashed by hash_babybear_slice_to_digest, which packs identically (hash/poseidon2.rs:204). The packed word, and hence every transcript challenge and every Merkle digest, is a function of the raw 31-bit limbs, not of the BabyBear field elements they represent.

Concretely: replacing any absorbed value $x<2^{31}-p$ by $x+p$ leaves every algebraic constraint satisfied (they all reduce modulo $p$) but changes the packed word, and therefore the transcript from that point on. Exactly $2^{31}-p=\mathtt{0}\mathtt{x}\mathtt{7}\mathtt{f}\mathtt{f}\mathtt{f}\mathtt{f}\mathtt{f}\mathtt{f}$ field elements admit such a second encoding (one in sixteen of the field), so the values the verifier absorbs are frequently not bound to a unique encoding.

Impact. The transcript and the WHIR Merkle commitment do not canonically bind the field-element content of the values the live verifier absorbs. The concrete consequence is challenge grinding. A malicious prover can swap any absorbed value below $2^{31}-p$ for its non-canonical representative $x+p$ without disturbing a single algebraic constraint (they all reduce modulo $p$); each swap changes the packed word, and therefore the transcript from that point on, hence every subsequent challenge: sumcheck challenges, WHIR folding and query challenges, and the proof-of-work check. The prover thereby obtains re-randomizations of the challenges for free, outside the soundness and PoW analysis, lowering the cost of steering the transcript toward a state that accepts a false statement.

The same ambiguity makes proofs non-unique: a given statement has many distinct accepting proofs, since each absorbed value with a second representative yields another valid transcript, so a proof cannot be treated as a unique token. This is a grinding and uniqueness weakness, not a cheap proof rewrite. Re-encoding an absorbed value cascades through the Fiat-Shamir transcript, so every later challenge changes; and under a fixed commitment the Merkle path binds the exact raw leaf, so the digest cannot be reopened to a different representative. Any alternative proof must be produced by re-running the prover.

Unlike the companion finding “Observation is not sound for arbitrary BabyBear wires”, this weakness is reachable on the live absorb paths. The wires fed into observe, observe_ext, and the leaf hash in the actual verifier (public values, sumcheck claims, codeword and out-of-domain openings, and so on) are exactly the load_witness outputs above; none of them is canonicalized before being hashed. The values are non-negative in $[0,2^{31})$, so the signed-limb collisions of the companion finding do not arise here, but the non-canonical representatives do.

Recommendation. Fully reduce every BabyBearWire to its canonical range $[0,p)$ before it is absorbed into the transcript or hashed into a Merkle leaf, rather than only bounding max_bits. Once each limb is in $[0,p)$ with $p<2^{31}$, the base-$2^{31}$ packing is injective and canonical, and both the grinding and the malleability above disappear. Asserting max_bits <= 31 is not sufficient: it does not remove the non-canonical representatives.

reduce already produces a canonical representative; signed_div_mod constrains its remainder to $[0,p)$. The robust fix is to lift this into the type system: introduce a ReducedBabyBearWire newtype, constructible only through reduce, exposing AsRef<BabyBearWire> so it can be used anywhere a wire is expected, and have observe, observe_ext, pack_base_2_31, and the Merkle leaf hash accept only this type. Absorbing a raw, possibly non-canonical wire then becomes a compile error. The codebase already has the underlying primitive, used on sampled digits in constrain_base_baby_bear_decomposition:

range.check_less_than_safe(ctx, digit.value, BABY_BEAR_MODULUS_U64);

Apply the same check_less_than_safe(_, _, BABY_BEAR_MODULUS_U64) to proof field elements at load time (cleanest inside the proof-data loader), or reduce each wire to a canonical representative immediately before pack_base_2_31 and before leaf hashing.

Client Response. This issue has been addressed in PR #2848 by introducing reduced BabyBear newtypes and requiring them on transcript absorption and Merkle leaf hashing paths. The reduced witness loaders range-check values against the BabyBear modulus before they can be packed.

Description. On target_os = "zkvm", the openvm-org/tiny-keccak fork patches tiny_keccak::Keccak to wrap openvm_keccak256::Keccak256, whose finalize_ptr always writes exactly KECCAK_OUTPUT_SIZE = 32 bytes regardless of the caller’s buffer length:

// zkvm_impl.rs
core::ptr::copy_nonoverlapping(self.state.0.as_ptr(), output, KECCAK_OUTPUT_SIZE);

The fork’s finalize guards only the too-small case:

// keccak.rs (zkvm path)
assert!(output.len() >= 32, "output buffer too small");
unsafe { self.state.finalize(output) };

The assert! covers memory safety (output.len() < 32) but not output.len() > 32. The host and upstream Keccak::finalize squeeze output.len() bytes (Keccak-256’s rate is 136, so squeezing up to 136 bytes from one permutation is well-defined). So for any output.len() > 32, the zkVM build writes 32 correct bytes and leaves output[32..] stale, while the host build and the Keccak spec produce a full output.len()-byte squeeze. The path is reachable without triggering the fork’s non-256 panic: Keccak::v256() is the supported constructor, and finalize(&mut [0u8; N]) with N > 32 then silently truncates.

Impact. Medium. A guest using tiny_keccak::Keccak::v256 as a short extendable-output function (for example a 48 or 64 byte derivation) computes a value in the zkVM that differs from the host build and from the Keccak specification, silently: the first 32 bytes are correct, the rest are stale buffer bytes. A program that relies on those bytes (key or seed derivation, multi-value expansion) would compute a wrong value in the zkVM and still pass native tests. This is not a circuit-soundness break (the proof faithfully attests to whatever the guest computed), but it is a real guest-library correctness and compatibility bug. Likelihood is low, since Keccak-256 is overwhelmingly used as a 32-byte digest and the main ecosystem consumer routes through the fixed-32 native_keccak256 path, but the failure is silent and correctness-affecting.

Recommendation. On the zkVM target, make the contract explicit instead of silently truncating: either reject output.len() != 32 (failing loudly, matching the spirit of the non-256 panic) or fall back to the software KeccakState squeeze for output.len() != 32 so the full squeeze matches upstream. Document that on the zkVM target tiny_keccak::Keccak supports only the 32-byte Keccak-256 digest.

Client Response. The issue is fixed in PR #2872, by adding an exact check to enforce an output size of 32 bytes in finalize, and in PR #7 of the tiny-keccak fork, by replacing the wrapper that caused the truncation so arbitrary output lengths are squeezed correctly.

Description. The sample_bits method samples a random field element, interprets it as an integer, and then reduces it modulo 2^bits. Since the field modulus is not a power of two, this does not sample uniformly from [0, 2^bits): values below a threshold determined by the modulus occur slightly more often than values above it.

This affects at least two uses of sample_bits:

• In the PoW check, the sampled value is required to be zero. For example, when requesting a 30-bit PoW challenge, the success probability is 2/p rather than exactly 2^-30, which corresponds to approximately 29.91 bits of work rather than 30.
• The WHIR verifier uses sample_bits to derive query indices. As a result, these indices are also not sampled uniformly from the intended range, and lower indices are selected with a slight preference over higher ones.

If x is sampled uniformly from F_p and y = x mod 2^bits, then letting t = p mod 2^bits, the output distribution satisfies

and

In particular, the PoW check succeeds when sample_bits(bits) == 0, so its success probability is

For the modulus p used here, some representative examples are:

The following Python snippet reproduces these probabilities:

from math import log2

p = 2**31 - 2**27 + 1

for bits in [8, 16, 24, 27, 28, 29, 30]:
    threshold = p % 2**bits
    p_below = (p // 2**bits + 1) / p
    p_above = (p // 2**bits) / p
    print(
        f"{bits} bits: threshold={threshold}, "
        f"log2(p_below)={log2(p_below):.18g}, "
        f"log2(p_above)={log2(p_above):.18g}"
    )

Impact. The induced bias is small, but it means that values returned by sample_bits are not distributed exactly as assumed by idealized soundness and PoW calculations. In particular, the actual PoW success probability is slightly higher than the uniform 2^-bits target, and WHIR queries exhibit a slight preference toward low-index positions.

Recommendation. If uniform sampling over [0, 2^bits) is required, implement sample_bits using rejection sampling instead of truncating a uniformly sampled field element. Otherwise, document the bias explicitly and account for it in any soundness or PoW parameter calculations that rely on sample_bits.

Client response. The OpenVM team is aware of this bias. Since it is relatively small, especially when sampling less than 27 bits, the team is not planning to change the sampling method. The soundness calculator was updated to account for this bias in PR #357.

Description. The design of the FiatShamirTranscript trait forces the protocol to use the same hash function to implement the Fiat-Shamir transform and to enforce proof-of-work (PoW) challenges. In particular, the associated function check_witness shown below forces the proof-of-work bits to be derived from self:

    fn check_witness(&mut self, bits: usize, witness: SC::F) -> bool {
        if bits == 0 {
            return true;
        }
        self.observe(witness);
        self.sample_bits(bits) == 0
    }

Impact. This design limits flexibility for parameter setting and may cause a degradation in the overall security level when changing hash functions. For example, the BLAKE3 hash function is a valid choice to implement the Fiat-Shamir transcript but is substantially faster to compute than SHA-3 or Poseidon2. This means that $n$ bits of PoW using BLAKE3 provides much less security than $n$ bits of PoW using Poseidon2 (as used in the current parameter config).

Recommendation. We give two orthogonal recommendations. The first is what we consider to be best practice, while the second is more immediate and avoids changes to the codebase.

• (best practice). We recommend “separating responsibilities” of the hash functions. Concretely, one could modify the check_witness function above by replacing self.sample_bits(bits) with a call to another PoW-specialized hash function. This modification removes a potential foot-gun and allows for future configurations using more elaborate PoW functions (for example using memory-hard functions to defend against malicious provers that use custom and highly-parallel hardware).

• (simpler mitigation). Alternatively, this issue can be mitigated by clearly documenting this fact and encouraging anyone modifying the configuration parameters to think about adjusting the PoW difficulty for their chosen hash function.

Client Response. The client has included new documentation for this behavior in the soundness calculator in PR #357.

Description. In GkrInputAir, when the GKR proof has no interactions (n_logup = 0), the q0_claim column is completely unconstrained. In contrast, the native verifier (in the verify_gkr function) contains a corresponding check that enforces q0_claim == 1 when there are no interactions, which the recursive verifier does not replicate.

As a result, besides the inconsistency, the prover can set q0_claim to any arbitrary extension field element without affecting the verification in the same way as the related finding in the native verifier.

Impact. As in the native verifier, the unconstrained q0_claim allows proof malleability. But unlike the native verifier, where the malleable field is directly in the proof struct and exploitable by any external party, the recursive verifier’s q0_claim is a witness column inside the recursion circuit’s trace (i.e., witness malleability rather than proof malleability). Although the practical impact is negligible and very limited, it might still warrant a correction to increase robustness and keep consistency with the native verifier.

Recommendation. Add a constraint in GkrInputAir that pins q0_claim to the canonical value one in the extension field ([1, 0, 0, 0]) when there are no interactions.

Client Response. This issue has been acknowledged and fixed in PR #2742.

Description. The Decode trait (codec.rs, lines 28-35) provides an interface to produce proof structures from an untrusted reader (or byte stream). The trait is implemented for SWIRL proofs and its constituent components in proof.rs (lines 421-692).

As part of the decoding process, the implementations must allocate vectors of variable sizes. The sizes are directly taken from the reader without sanitization or bounding (beyond what the type system enforces). We highlight an example from the implementation of Decode for BatchConstraintProof (specifically, lines 532-533) and list all occurrences of similar cases:

    let n_max = usize::decode(reader)?;
    let mut sumcheck_round_polys = Vec::with_capacity(n_max);

Impact. A malicious prover could abuse this lack of sanitization to force the verifier to allocate arbitrarily large vectors. Depending on the hardware and OS running the verifier, this could cause resource exhaustion. Note, however, that all these sizes are later checked by verify_proof_shape() and therefore do not cause soundness issues.

Recommendation. It is good practice to sanitize inputs before allocating vectors.

Client Response. This issue has been acknowledged and fixed in PR #356.

Description. The deferral CALL opcode writes an OutputKey into guest heap memory containing both output_commit and output_len, laid out as one contiguous write [output_commit || output_len_le] (extensions/deferral/circuit/src/call/air.rs:55-67). Only output_commit is bound into the deferral accumulators; output_len is not.

In DeferralCallCoreAir::eval, the accumulator update hashes only the two commits:

let input_f_commit = byte_commit_to_f(&cols.reads.input_commit);
let output_f_commit = byte_commit_to_f(&cols.writes.output_commit);

self.poseidon2_bus
    .lookup(
        cols.reads.old_input_acc,
        input_f_commit,
        cols.writes.new_input_acc,
        AB::Expr::ONE,
    )
    .eval(builder, cols.is_valid);

self.poseidon2_bus
    .lookup(
        cols.reads.old_output_acc,
        output_f_commit,
        cols.writes.new_output_acc,
        AB::Expr::ONE,
    )
    .eval(builder, cols.is_valid);

output_len never enters any accumulator. The only constraints applied to it are range checks: a byte-pair range check (extensions/deferral/circuit/src/call/air.rs:151-155) and a top-byte < 2^address_bits check in the adapter (extensions/deferral/circuit/src/call/air.rs:342-347). The AIR does not constrain output_len to equal the length of the output that produced output_commit. (The DeferralCallWrites doc comment states output_len “must be divisible by DIGEST_SIZE”, but this is not enforced at CALL either.)

The true output length is bound, but inside output_commit, not in the separate field. The output commitment is an onion hash seeded with the real length (extensions/deferral/circuit/src/def_fn.rs:84-85):

let mut state = [F::ZERO; POSEIDON2_WIDTH];
state[0] = F::from_u32(deferral_idx);
state[1] = F::from_usize(output_ref.len());

That binding is only re-derived and checked by the OUTPUT opcode, which reads the full [output_commit || output_len] pair from memory, rebuilds the sponge initial state [deferral_idx, output_len, 0, ...], and on the last row requires both that the recomputed hash equals output_commit and that output_len == section_idx * DIGEST_SIZE (extensions/deferral/circuit/src/output/air.rs:196-223). Consequently, output_len as written by CALL is an unauthenticated prover hint: a malicious prover can write any range-valid output_len into the OutputKey while keeping the genuine output_commit, and the CALL proof still verifies. This is demonstrated by the test poc_deferral_call_accepts_forged_output_len (extensions/deferral/circuit/src/call/tests.rs:478-609), which keeps the real output_commit for an 8-byte output but writes output_len = 16, and the trace verifies.

A subsequent OUTPUT call on the full (output_commit, output_len) pair detects the mismatch, because the genuine commit was computed with the real length and the forged pair fails the hash and section_idx * DIGEST_SIZE checks. The risk is therefore confined to guest code that consumes output_len before (or without) an OUTPUT that authenticates it. The current examples do this. single.rs asserts on the CALL-returned length before fetching the output:

let output_key_0 = deferred_compute::<0>(&INPUT_COMMIT_0);
assert_eq!(output_key_0.output_len as usize, EXPECTED_OUTPUT_0.len());

(extensions/deferral/tests/programs/examples/single.rs:16-18). And verify_stark_unchecked branches on the hint before calling get_deferred_output (which is what emits OUTPUT):

let output_key = deferred_compute::<DEF_IDX>(input_commit);
let output_len = output_key.output_len as usize;

const MIN_OUTPUT_BYTES: usize = 2 * COMMIT_NUM_BYTES;
if output_len < MIN_OUTPUT_BYTES {
    panic!("output_len too small for a ProofOutput");
}

(guest-libs/verify-stark/guest/src/lib.rs:16-26).

Impact. By contract, output_len is a hint that becomes authenticated only when OUTPUT is invoked with the matching output_commit. The soundness of the deferral framework itself is not affected: OUTPUT binds the pair. However, guest code that branches on output_len, allocates based on it, meters based on it, or exposes it as part of verified state before OUTPUT succeeds can be misled by a forged length. The convention is implicit and is not followed by the shipped examples, which makes the footgun easy to reproduce in downstream guest programs.

Recommendation. Make the intended contract explicit in the documentation: OutputKey.output_len is an unauthenticated prover hint until an OUTPUT call authenticates it against output_commit.

In addition to the docs, adjust the examples to model the safe pattern:

• For fixed-size outputs, allocate the expected-size buffer directly and immediately pass the full (output_commit, output_len) pair to OUTPUT, without first branching on CALL’s returned output_len.
• For dynamic-size outputs, treat output_len only as an unauthenticated allocation hint: first check it against an application-defined maximum, allocate the buffer, and immediately call OUTPUT. Any further logic based on the output (such as parsing, minimum length checks, or branching) should happen only after OUTPUT has succeeded.

Client response. The client confirmed that OutputKey.output_len returned by CALL is intended to be treated as an unauthenticated allocation hint that becomes authenticated only when OUTPUT consumes the full (output_commit, output_len) pair. The client plans to update the documentation and examples to model safe deferral extension usage. No circuit-level binding of the CALL-returned output_len to the committed output length is included in the reviewed fixes. Extensive documentation has been added in PR #2866.

Description. There are two low-severity canonicality and consistency issues in the deferral tree/path machinery.

First, in crates/continuations/src/circuit/inner/def_pvs/air.rs, a two-row aggregation with exactly one real child and one absent child lets the prover-controlled single_present_is_right bit decide whether the real child is hashed on the left or the right. The absent child is still constrained to represent an unchanged subtree, so this is not an arbitrary absent-subtree forgery. The AIR checks the one-present-child case around lines 116-122 and uses single_present_is_right in the parent hash selection around lines 234-265, but does not bind that bit to a canonical tree position. This is mainly a malleability issue: we confirmed by testing that the same underlying child proof/public values can produce two different valid parent roots depending only on this position bit.

Second, there is a small inconsistency in how depth == 0 (unset Merkle paths) are represented. The root AIR’s unset path forces the first branch bit to the right in crates/continuations/src/circuit/root/def_paths/air.rs:147-151, so its effective path anchors at (DEFERRAL_AS, 1), while the depth == 0 branch in DeferralMerkleProofs::verify uses label_to_index((DEFERRAL_AS, 0)) in crates/verify/src/deferral.rs:67-74. The native deferral_flag == 0 verifier flow does not call this helper branch; it only checks that the deferral public values are unset in crates/verify/src/lib.rs:283-299. The helper branch would matter only in a deferral_flag == 2 && depth == 0 corner, which does not appear reachable for valid root-AIR proofs because set deferral paths require positive depth. We confirmed the convention mismatch with a trace/unit test showing that the root AIR unset trace maps to (DEFERRAL_AS, 1) while the native helper convention maps to (DEFERRAL_AS, 0).

Impact. These are canonicality and consistency issues rather than direct soundness breaks. The single-child position bit gives a prover one bit of root malleability at each single-child aggregation step, but does not let the prover choose an arbitrary root or bypass child-proof verification. The unset-path mismatch appears to be a convention mismatch in an edge/helper path rather than a live native/root verifier divergence.

Recommendation. Canonicalize the single-present-child case by carrying or deriving constrained tree-position metadata and requiring the real child to occupy that position. For the unset path, either align the native helper branch with the root AIR convention or document why the root AIR intentionally anchors the unset case at block 1.

Client response. PR #2817 aligns the native unset-path convention with the root AIR by requiring deferral Merkle proofs even in the deferral_flag == 0 case and by using the same depth-zero right-child convention. Additionally, PR #2862 makes each deferral proof carry its position in the deferral memory subtree, enforcing that the deferral index corresponds to the position in memory.

Description. There is an AIR/native-verifier consistency mismatch in the verify-stark in-circuit verifier. In guest-libs/verify-stark/circuit/src/verifier/air.rs, the check def_hook_commit == expected_def_hook_commit was gated by deferral_flag, while the no-deferral branch only zeroed depth, initial_acc_hash, and final_acc_hash, leaving def_hook_commit unconstrained when deferral_flag == 0. The native verifier, by contrast, explicitly rejects non-zero def_hook_commit in the deferral_flag == 0 path.

In other words, the in-circuit verifier could accept malformed child public values that the native verifier rejects:

native_verifier(child_proof) = reject

but:

prove_and_verify(verify_stark_circuit(child_proof)) = accept

Impact. This is a consistency mismatch, but def_hook_commit does not appear to flow into verify-stark outputs in the no-deferral path, so we did not identify a concrete exploit.

Recommendation. Add an assert_zeros constraint for def_hook_commit in the no-deferral branch anywhere deferral_flag == 0 is allowed.

Client response. The client reported this as a known issue and fixed it in PR #2817 before reporting. The fix adds an assert_zeros constraint for def_hook_commit in the no-deferral branch of the verify-stark AIR, matching the native verifier’s deferral_flag == 0 behavior. The same PR applies the analogous zeroing fix to the root continuation verifier AIR.

Description. CommitBytes::new accepts arbitrary 32-byte values, but converting CommitBytes into a BabyBear [F; 8] digest is not injective. The conversion interprets the bytes as a big integer and decomposes it modulo the BabyBear modulus across 8 limbs, effectively reducing the value modulo p^8. As a result, multiple distinct 32-byte strings can map to the same field digest. In practice, most [F; 8] digests have 429 valid byte encodings, and some have 430. For example, 0x00..00 and the 32-byte encoding of p^8 both decode to the same [F; 8] value.

Impact. In the current code, this affects byte-ingestion paths such as VerificationBaselineJson, where commitment fields are deserialized as raw 32-byte CommitBytes and then converted into field digests for verification. This means the same valid proof can verify against multiple distinct raw commitment strings for fields such as app_exe_commit, VK commit components, or expected_def_hook_commit, as long as those strings decode to the same [F; 8]. This does not appear to be a soundness break or a cryptographic hash collision, but it creates byte-level statement malleability and can confuse downstream systems that use raw commitment bytes as app/VK identity.

Recommendation. Enforce a single canonical byte representation for CommitBytes values before they are used as BabyBear digests. In particular, external byte-ingestion paths should reject or normalize non-canonical encodings.

Client response. PR #2839 addresses this finding by enforcing canonical CommitBytes encodings. CommitBytes::new now validates that supplied bytes round-trip through the BabyBear digest encoding, limb-based conversions check canonical field bounds, and the Bn254 -> CommitBytes path uses the same checked constructor.

Description. BabyBearChip::div constrains a = b * c (mod p) by forming diff = a - b*c and calling assert_zero on it. Before doing so it pre-reduces its operands, and then tags the difference with a max_bits that adds one carry bit:

let mut c = self.load_witness(ctx, a.to_baby_bear() * b_inv_val);
if a.max_bits > Fr::CAPACITY as usize - RESERVED_HIGH_BITS {
    a = self.reduce(ctx, a);
}
if b.max_bits + c.max_bits > Fr::CAPACITY as usize - RESERVED_HIGH_BITS {
    b = self.reduce(ctx, b);
}
if b.max_bits + c.max_bits > Fr::CAPACITY as usize - RESERVED_HIGH_BITS {
    c = self.reduce(ctx, c);
}
let diff = self.gate().sub_mul(ctx, a.value, b.value, c.value);
let max_bits = a.max_bits.max(b.max_bits + c.max_bits) + 1;
self.assert_zero(ctx, BabyBearWire { value: diff, max_bits });

With RESERVED_HIGH_BITS = 2 and Fr::CAPACITY = 253, the threshold is 251. Observe that the pre-reduction guards use a strict >, so an operand sitting exactly at the boundary is left untouched: if a.max_bits == 251, or b.max_bits + c.max_bits == 251, neither reduction fires. The subsequent + 1 then pushes max_bits to 252. But assert_zero opens by asserting the wire respects the invariant:

assert!(a.max_bits <= Fr::CAPACITY as usize - RESERVED_HIGH_BITS);

i.e. assert!(252 <= 251), which panics. The bug is that the pre-reduction test omits the carry bit that the final max_bits accounts for. Contrast add and sub, which fold the + 1 into the same comparison:

if a.max_bits.max(b.max_bits) + 1 > Fr::CAPACITY as usize - RESERVED_HIGH_BITS {

A minimal reproduction:

let a = BabyBearWire { value: ctx.load_witness(Fr::from(1)), max_bits: 251 };
let b = chip.load_constant(ctx, BabyBear::ONE);
chip.div(ctx, a, b); // a.max_bits == 251 is not reduced; assert_zero panics

Impact. This is a completeness defect, not a soundness one: the prover panics during witness generation and cannot produce a proof for the affected operands. A wire only reaches max_bits == 251 through a deliberate sequence of unreduced operations, so I am not aware of an in-tree call site that triggers it today; the guard is nonetheless off-by-one and will fail closed on a panic rather than silently miscompute.

Recommendation. Fold the carry bit into the pre-reduction guards, mirroring add/sub: reduce when a.max_bits + 1 > Fr::CAPACITY - RESERVED_HIGH_BITS and when b.max_bits + c.max_bits + 1 > Fr::CAPACITY - RESERVED_HIGH_BITS, so that diff.max_bits never exceeds the assert_zero bound.

Client Response. This issue has been addressed by PR #2858 by adding the carry bit to the div pre-reduction guards. At the boundary case, operands are reduced before assert_zero, so diff.max_bits stays within the allowed bound.

Description. observe enforces no bound on its input at all:

pub fn observe(&mut self, ctx: &mut Context<Fr>, value: &BabyBearWire) {
    self.invalidate_samples();
    self.observe_buf.push(*value);
    if self.observe_buf.len() == NUM_OBS_PER_WORD { self.flush_observe_buf(ctx); }
}

So the packed word is whatever raw cells the caller supplies. This matters because a BabyBearWire is a BN254 cell that logically holds a signed integer, with the invariant documented on the type:

/// Logically `value` is a signed integer represented as `Bn254`.
/// Invariants:
/// - `|value|` never overflows `Bn254`
/// - `|value| < 2^max_bits` and `max_bits <= Fr::CAPACITY - RESERVED_HIGH_BITS`

The transcript and the Merkle leaf hash, on the other hand, do not look at the field elements; they pack the raw signed cells in base $2^{31}$. The transcript buffers up to NUM_OBS_PER_WORD = 8 wires and packs them with pack_base_2_31, and hash_babybear_slice_to_digest packs each leaf chunk the same way with pack_base_2_31_cells (base $2^{31}$). In both cases the absorbed word is the linear combination:

where each $x_i$ is the raw signed BN254 cell of the $i$-th wire and $k\le 8$. Soundness of the transcript and the commitment requires $\mathsf{p}\mathsf{a}\mathsf{c}\mathsf{k}$ to be injective on the BabyBear vectors being absorbed; otherwise distinct field content can produce the same word, and the prover is free to move between the preimages.

The map $\mathsf{p}\mathsf{a}\mathsf{c}\mathsf{k}$ is injective only when each limb $x_i$ is confined to a set of residues of width strictly less than the base $2^{31}$. The canonical range $[0,p)$ is such a set: with $p<2^{31}$, the map is ordinary base-$2^{31}$ positional notation, the limbs never overlap, and distinct BabyBear vectors give distinct integers and hence distinct words. observe guarantees nothing of the sort. Two ways the injectivity fails for the wires observe accepts:

• Oversized limbs. For a wire with max_bits > 31 the cell can exceed $2^{31}$ and spill into the next limb’s place outright, so the encoding is trivially ambiguous.

• Signed limbs. Even within the type’s nominal 31-bit width the cell is signed, and the signed range is wider than the base. The key observation is that $L$ has a nontrivial kernel over such limbs: the carry vector $c_i=2^{31}{e}_i-e_{i+1}$ (with $e_i$ the $i$-th unit vector) satisfies:

Adding $c_i$ to a limb vector therefore leaves the absorbed word unchanged while changing the underlying field vector. Hence over the domain observe accepts, the transcript and the WHIR Merkle commitment are not binding on field content; the hashing is genuinely not collision-resistant.

Unsound even for max_bits-reduced wires

The natural mitigation is to reduce each wire before observing it. That is not enough. reduce_max_bits only reduces a wire whose max_bits exceeds 31; it leaves any wire with max_bits <= 31 untouched, sign included:

pub fn reduce_max_bits(&self, ctx: &mut Context<Fr>, a: BabyBearWire) -> BabyBearWire {
    if a.max_bits > BABYBEAR_MAX_BITS { self.reduce(ctx, a) } else { a }
}

So a max_bits-reduced wire still ranges over the signed interval $(-2^{31},2^{31})$, an interval of width $2^{32}$, which is twice the packing base $2^{31}$. The carry vector $c_i$ from above stays inside this box, so the collision survives. Take the two-limb example:

Here $w=v+c_0$, so both pack to the same value, since:

But coordinate-wise modulo $p$ they are the distinct vectors $(0,0)$ and $(2^{31}-p,p-1)$. Both limbs of $v$ and $w$ lie in $(-2^{31},2^{31})$, so both are legal max_bits-reduced inputs to observe. The collision is confirmed by cvc5 over the signed-limb model:

(set-logic QF_LIA)
(define-fun B () Int 2147483648)  ; 2^31
(define-fun P () Int 2013265921)  ; BabyBear modulus = 0x78000001
(declare-fun v0 () Int) (declare-fun v1 () Int)
(declare-fun w0 () Int) (declare-fun w1 () Int)
(define-fun signed_31 ((x Int)) Bool (and (< (- B) x) (< x B)))
(assert (and (signed_31 v0) (signed_31 v1) (signed_31 w0) (signed_31 w1)))
; the two vectors differ as BabyBear vectors (coordinate-wise mod p)
(assert (or (not (= (mod v0 P) (mod w0 P))) (not (= (mod v1 P) (mod w1 P)))))
; but pack to the same raw base-2^31 value
(assert (= (+ v0 (* v1 B)) (+ w0 (* w1 B))))
(check-sat)

sat
((v0 (- 2013265921)) (v1 0) (w0 134217727) (w1 (- 1)))
(mod: v = (0, 0)   w = (134217727, 2013265920))

Reducing max_bits to 31 is therefore not the same as canonicalizing to $[0,p)$, and asserting max_bits <= 31 (or even == 31) is likewise insufficient: neither removes the signed range, and the carry collision survives. Only confining each limb to $[0,p)$, where $p<2^{31}$ and the limbs cannot overlap, makes $\mathsf{p}\mathsf{a}\mathsf{c}\mathsf{k}$ injective.

Impact. In the reviewed code these collisions are not reachable. Every wire that actually reaches observe, observe_ext, or the leaf hash is loaded via load_witness and is therefore non-negative in $[0,2^{31})$; no signed limb and no oversized wire is ever absorbed. The non-canonical-representative weakness that is reachable on those non-negative inputs is the subject of the companion finding “Unreduced BabyBear wires are absorbed into the transcript”.

The finding here is about the API contract rather than a demonstrated forgery. observe accepts an arbitrary BabyBearWire, and a signed wire is the documented, legal state of the type. It silently produces a non-binding encoding for such a wire, with no guard and no compile-time or run-time signal that anything is wrong. A future caller that observes a signed wire, or a wire with max_bits > 31, would reintroduce the grinding weakness of the companion finding, and, because signed limbs genuinely collide, a true binding failure of the commitment.

Recommendation. The transcript and leaf-hash paths should canonicalize every input to $[0,p)$ before packing, rather than trusting the caller to pass a wire in a particular sub-range. With each limb in $[0,p)$ and $p<2^{31}$, the limbs cannot overlap and $\mathsf{p}\mathsf{a}\mathsf{c}\mathsf{k}$ is injective, which removes both the signed-limb carry collisions and the oversized-limb overlap. As shown above, neither asserting max_bits <= 31 nor calling reduce_max_bits achieves this: the former keeps the signed range, the latter is a no-op at max_bits <= 31.

reduce already produces a canonical representative; signed_div_mod constrains its remainder to $[0,p)$. The robust fix is to make non-reduced absorption unrepresentable: introduce a ReducedBabyBearWire newtype, constructible only through reduce, exposing AsRef<BabyBearWire> so it can stand in wherever a wire is expected, and have observe, observe_ext, and the leaf hash accept only this type. The compiler then rejects any attempt to absorb a raw, possibly non-canonical or signed BabyBearWire, closing both this finding and its companion at the type level.

Client Response. This issue has been addressed in PR #2848 by introducing reduced BabyBear newtypes and making observe, observe_ext, and leaf hashing accept only those reduced types. Raw BabyBearWires, including signed or oversized ones, no longer reach the base-$2^{31}$ packing interface.

Description. signed_div_mod introduces witnesses div and rem with div * b + rem ≡ a (mod p) and 0 <= rem < b, where b is the BabyBear order. To range-check div it relies on the following argument in the proof-of-correctness comment:

// Logically we want `div = a // b`. Because (2) and `a` could be negative, `div` could
// be negative. Therefore, we have `|div| = |a // b| = |a| // b < 2^max_bits // b = bound` and
// we can say `shifted_div = div + bound` is in `[0, 2 * bound)`.

The middle identity |a // b| = |a| // b is false for negative a: floor division and absolute value do not commute. Take $a=-1$ and $b=p_{BB}$:

So |div| = 1 while |a| // b = 0; the claimed bound underestimates |div|. This is not merely a comment defect, because the code computes bound from exactly that quantity:

// Constrain that `abs(div) <= 2 ** (2 ** a_num_bits / b).bits()`.
let bound = (BigUint::from(1u32) << (a_num_bits as u32)) / &b;
let shifted_div = range.gate().add(ctx, div, QuantumCell::Constant(biguint_to_fe(&bound)));
range.range_check(ctx, shifted_div, (bound * 2u32 + 1u32).bits() as usize);

For a negative value with a tight width, e.g. a = -1 with a_num_bits = 1 (which is what neg(one) produces: value = -1, max_bits = 1), we get bound $=\lfloor 2^1/p_{BB}\rfloor =0$. Then div = -1 and shifted_div = div + bound = -1, which the range check to (2*bound + 1).bits() = 1 bit rejects: it expects shifted_div in [0, 2*bound], but -1 reduces modulo Fr to a large element. The constraint is unsatisfiable, so the prover cannot complete signed_div_mod for such an input.

Impact. A completeness edge, not a soundness one. signed_div_mod backs reduce, assert_zero, and assert_equal, so any of these is unprovable on a small negative value carrying a tight a_num_bits. In practice the gadget is reached with a_num_bits = BABYBEAR_MAX_BITS = 31, where bound >= 1 and the negative quotient is covered, so the live code does not appear to hit it; the documented invariant is wrong regardless, and the safe range is narrower than the comment claims.

Recommendation. Derive bound so that it covers the floor-division of negative dividends rather than routing through |a| // b: the magnitude of div $=\lfloor a/b\rfloor$ for $|a|<2^{a\_num\_bits}$ is at most $\lceil (2^{a\_num\_bits}-1)/b\rceil$, so use that (or equivalently bound $=\lfloor 2^{a\_num\_bits}/b\rfloor$ together with an asserted lower bound a_num_bits >= BABYBEAR_ORDER_BITS). At minimum, correct the proof comment and document that the gadget must only be called with a_num_bits large enough that bound covers the negative quotient.

Client Response. This issue has been addressed in PR #2860 by changing the quotient bound to ceil((2^a_num_bits - 1) / b). The tight negative case is now inside the shifted-div range check.

Description. The XORIN circuit can absorb at most 136 bytes per call: its columns are sized to KECCAK_RATE_BYTES = 136 (34 four-byte chunks), and the AIR enforces len = 4 * (#non-padding) <= 136. A single XORIN therefore supports any per-block absorb length in {0, 4, ..., 136}. The limit is purely the absorb width; KECCAKF permutes the full 200-byte state, so the permutation itself is rate-agnostic.

native_xorin is an exported low-level intrinsic whose documented contract only mentions pointer validity. It rounds len up to a multiple of four (adjusted_len = len.next_multiple_of(4)) and emits the instruction with no check that adjusted_len <= 136. A caller passing len = 140 emits len = 140, which the circuit cannot represent: pure execution proceeds, then preflight or trace generation panics (140 bytes need 35 chunks versus 34 slots). The patched RustCrypto sha3 fork routes all generic block absorption through native_xorin(state, block, block.len()), so honest use of any variant whose rate exceeds 136 bytes calls the intrinsic with len > 136.

A sponge function is circuit-provable through this path if and only if its rate is at most 136 bytes (state 1600 bits = 200 bytes; rate = 200 - capacity):

So the dividing line is capacity at least 512 bits, equivalently rate at most 136. The unprovable set is the 128-bit-security XOF family (rate 168) plus SHA3-224 / Keccak-224 (rate 144).

Impact. Low (honest-prover completeness and API compatibility, not soundness). Honest guest programs using the affected low-level API, or affected RustCrypto sha3 APIs under the OpenVM fork, can execute but fail to prove (preflight or trace-generation panic). Note the limit is the absorb width, not the variant per se: SHA3-384 and SHA3-512 (rates 104 and 72) are provable through the fork, while SHA3-224 and SHAKE128 are not.

Recommendation. Never emit an unprovable XORIN, and never fail late. Harden native_xorin to reject len.next_multiple_of(4) > 136 at the API boundary, so misuse fails loudly there rather than deep in trace generation, and document the alignment and length limit. For sponge integrations whose rate exceeds 136 (the sha3 fork’s SHA3-224, SHAKE128, cSHAKE128, and so on), fall back to a software absorb for the oversized block while still using the native KECCAKF for the permutation; since the permutation dominates proving cost, the de-accelerated absorb is nearly free and the variant stays usable. Preferred ordering of options: software fallback over compile-time error over runtime panic.

Client Response. The issue has been fixed in PR #2845, PR #13 of the hashes fork, and PR #7 of the tiny-keccak fork. native_xorin explicitly rejects lengths over the limit, and the patched hash functions do not emit XORIN instructions exceeding it.

Description. On target_os = "zkvm", the openvm-org/tiny-keccak fork rejects every non-256 variant at runtime in Keccak::new:

#[cfg(target_os = "zkvm")]
fn new(bits: usize) -> Keccak {
    if bits != 256 {
        panic!("Only Keccak256 is supported for ZKVM");
    }
    ...
}

So the public constructors Keccak::v384() and Keccak::v512() still compile cleanly for the zkVM target but panic when the guest actually runs. Crucially, these two variants have rates 104 and 72 bytes respectively, both at most 136, so they are within the XORIN circuit’s absorb capability (see the related rate finding): the limitation is an artifact of the fork wrapping the fixed-rate, fixed-output Keccak256 type, not a circuit constraint. (Keccak-224, rate 144 > 136, is genuinely unprovable and is covered separately.)

Impact. Low (API compatibility and late, runtime failure). A guest constructing Keccak::v384() or Keccak::v512() builds successfully and then panics at execution time, a target-specific failure that does not exist on the host build and surfaces only when the program is run or proved. For these circuit-capable rates the failure is doubly unfortunate, because the variant could have been supported.

Recommendation. Since v384 and v512 fit the XORIN width (rates 104 and 72 at most 136), the proper fix is to support them by absorbing at their own rate instead of hardcoding Keccak-256’s 136. If the fork chooses not to implement them, it should at least fail at compile time rather than runtime: on the zkVM target, #[cfg]-gate the constructors so that using Keccak::v384() is a compile error rather than a runtime panic. (For the genuinely unprovable v224, rate 144, use the software-absorb fallback recommended in the related rate finding, not a compile-time rejection, since it remains a usable hash.)

Client Response. The issue has been fixed in PR #7 of the tiny-keccak fork. When a variant’s absorb rate exceeds the XORIN width, the block is now absorbed in chunks. This allows all variants, even v224, to use the XORIN intrinsic instead of being rejected.

Description. The SWIRL whitepaper and soundness calculator in soundness.rs treat the GKR fractional sumcheck and the ZeroCheck as fully independent protocols, respectively computing their error probabilities and security bits separately. The paper takes a maximum over the error probabilities and, accordingly, the soundness calculator takes a minimum across all components (soundness.rs:143-149). To avoid confusion, we will only write in terms of error probabilities (and therefore taking the maximum when rounds are independent).

In contrast to the above calculations, several challenges are shared or co-derived, which means their error probabilities should be combined via a union bound (summation of the failure probabilities) rather than treated independently. We identify three specific issues:

1. Shared challenge xi between GKR and ZeroCheck. The evaluation point xi produced by verify_gkr() (batch_constraints.rs:97-98) is reused directly as the evaluation point for the ZeroCheck. A malicious prover succeeds if xi is a bad challenge for either protocol. Therefore, the correct error for this round is a union bound over the probability of getting a “bad” challenge for the GKR round and for the ZeroCheck.
2. Incremental construction of xi. The point xi is not sampled atomically. It is built incrementally during the GKR sumcheck: each layer’s sub-rounds sample one coordinate via the mu challenges (fractional_sumcheck_gkr.rs:108, fractional_sumcheck_gkr.rs:144). If n_global > n_logup, additional coordinates are sampled afterward (batch_constraints.rs:104-106). This incremental construction complicates the round-by-round analysis: the GKR soundness for each sub-round is entangled with the eventual use of xi in the ZeroCheck, and the current soundness model does not account for this. We do not know how to prove round-by-round soundness in this case.
3. lambda and final coordinates of xi are sampled from the same transcript state. When n_global > n_logup, the final coordinates of xi and lambda are derived from the same transcript state with no intervening prover message. They cannot be treated as separate rounds in an RBR analysis; their error probabilities should be combined via a union bound.

Impact. The RBR error in certain rounds is slightly higher than shown in the paper and soundness calculator. In particular, (1) above approximately doubles the error associated with the sampling of xi ($1$-bit security loss). Similarly, assuming that the errors associated with xi and lambda are comparable, taking a union over both events as in (3) leads to another $1$-bit reduction in security level. The impact of (2) is yet to be determined; it is unclear to us whether existing theory is enough to give RBR soundness guarantees or to indicate a possible attack.

Recommendation. With respect to (1) and (3), we recommend revising the RBR soundness analysis. (2) is likely to warrant further investigation.

Client Response. The client acknowledged the issue and presented our team with a new draft of the SWIRL paper updating the relevant theorems. In particular, the revised theorems account for the incremental construction of xi, the multiple uses of the xi value and the fact that lambda is sampled alongside the final coordinates of xi. The soundness calculator was updated to reflect the paper changes in PR #357.

Description. The recursive verifier uses stacking_module_bus to carry the transcript index from the batch-constraint sumcheck module into the stacked-opening module. The bus message contains only a single field, tidx, so the consumer distinguishes messages only by the value of the transcript index and by the global balance of sends and receives.

The same bus is used for two semantically different handoffs:

• UnivariateSumcheckAir sends the transcript index immediately after the univariate sumcheck round, i.e. the initial tidx for MultilinearSumcheckAir.
• MultilinearSumcheckAir, when it has non-zero rounds, receives that tidx, performs its transcript observations and challenges, and sends the transcript index immediately before column openings.
• StackingOpeningAir receives the transcript index immediately before column openings.

This overloading is done to enable the zero-round multilinear sumcheck case. When MultilinearSumcheckAir has no rounds, its trace contains a dummy row and its stacking_module_bus receive/send constraints are disabled. In that case, the message sent by UnivariateSumcheckAir is consumed directly by StackingOpeningAir, because the transcript index before the multilinear sumcheck is also the transcript index before column openings.

There is currently no concrete message-confusion attack. If the prover tries to swap the non-zero-round and zero-round handoffs, the surrounding transcript constraints cause some transcript operations to be consumed twice or not consumed at all. Still, the bus does not encode which module boundary a message belongs to, so the intended protocol sequencing is implicit rather than reflected in the bus domain.

Recommendation. Consider adding semantic separation between the two handoffs. For example, MultilinearSumcheckAir could always receive the tidx from UnivariateSumcheckAir, including on rows where is_dummy = 1, and then forward the same tidx to StackingOpeningAir on a distinct bus when there are zero multilinear rounds. This would make the protocol stages explicit while preserving the current zero-round behavior.

Client Response. The client has decided not to address this comment.

Description. While auditing the recursive verifier AIRs, several constraints were found to be redundant: they are either fully implied by other constraints in the same AIR or by stricter constraints that fire on a superset of rows. Removing them does not weaken the AIR but reduces the constraint count (and therefore prover work and verifier degree-bounding cost).

The redundant constraints identified so far are listed below. Each item names the location, restates the constraint, and gives the reason it is implied.

1. GKR AIRs - transition-gated dummy-row constraints (crates/recursion/src/gkr/layer/air.rs:153-159, crates/recursion/src/gkr/sumcheck/air.rs:171-178, crates/recursion/src/gkr/xi_sampler/air.rs:115-122). In each of the three AIRs the same pair of transition constraints on local.is_dummy is already implied by the singleton-row constraints immediately below them (is_dummy –> is_first=1 and is_last=1, plus the analogous round/layer flags in the sumcheck case), which already make any dummy row a singleton segment with no internal transition.

2. Univariate eq-AIR - boolean check on local_is_last (crates/recursion/src/batch_constraint/eq_airs/eq_uni/air.rs:95-96). assert_bool(next.is_first + not(next.is_valid)) only excludes is_first = 1 and is_valid = 0, which is already unreachable via the existing is_first –> is_valid invariant.

Client Response. This issue has been acknowledged, and the client has decided not to address it for the moment.

Description. The OUTPUT opcode enforces the local relation “these raw bytes hash to this supplied OutputKey”, but it does not prove that the supplied OutputKey was previously produced by a CALL. The intended usage is documented: the guest calls deferred_compute, receives an OutputKey, and then passes that same key to get_deferred_output (docs/vocs/docs/pages/book/acceleration-using-extensions/deferral.mdx:11-12, docs/vocs/docs/pages/specs/openvm/isa.mdx:448). In the AIR, however, CALL folds the returned output_commit into the output accumulator (extensions/deferral/circuit/src/call/air.rs:157-181), while OUTPUT independently proves only that (deferral_idx, output_len, output_raw) reconstructs the supplied output_commit (extensions/deferral/circuit/src/output/air.rs:193-223). The DeferralCircuitCountBus validates the deferral index, but not that this particular key came from a prior CALL. In addition, OutputKey::new is public in extensions/deferral/guest/src/lib.rs:32-39.

Impact. This is primarily a guest API contract footgun. A guest that manually constructs or accepts an OutputKey from untrusted input can call OUTPUT and authenticate bytes against that arbitrary key without proving that the key came from a deferred computation. If all trusted code uses the intended pattern:

let key = deferred_compute::<IDX>(&input_commit);
get_deferred_output::<IDX>(&mut output, &key);

then the key comes from CALL and the deferral accumulators bind it to the deferred computation path.

Recommendation. Either document very explicitly that manually constructed OutputKeys are not trusted deferral results, or harden the circuit/API so OUTPUT consumes a key that is linked to a prior CALL. A circuit-level fix would require a lookup/bus relation such as CALL sending (deferral_idx, output_commit, output_len) and OUTPUT receiving it, with a clear multiplicity rule for whether outputs can be read once or multiple times.

Client response. The client indicated that deferral opcode usage should be heavily restricted to the provided guest libraries. Extensive documentation has been added in PR #2866.

Description. We observed several low-risk verify-stark API and hygiene issues.

• UserPvsCommitValuesAir::new relies on debug_assert! for configuration shape checks. In guest-libs/verify-stark/circuit/src/commit/air.rs:35-48, the constructor expects num_user_pvs >= DIGEST_SIZE, num_user_pvs % DIGEST_SIZE == 0, and (num_user_pvs / DIGEST_SIZE).is_power_of_two(), but these checks are debug-only. In release builds, malformed configurations could pass construction and fail later in less obvious ways.

• DeferredVerifyCircuitProver’s generic DeferralCircuitProver::prove path always uses prove_no_def. In guest-libs/verify-stark/circuit/src/prover/mod.rs:253-270, prove(&self, input_bytes) decodes a VmStarkProof and calls self.prover.prove_no_def(...). This means the trait path does not appear to support proving child STARKs that themselves require deferral Merkle inputs, even though the verifier machinery has deferral-aware concepts. This may be intended, but then the trait path should be documented as no-deferral-only.

• row_idx_flags in UserPvsCommitValuesAir appears dead. guest-libs/verify-stark/circuit/src/commit/air.rs:80-83 slices row_idx_flags from the row after MerkleTreeCols, but the AIR width is exactly MerkleTreeCols::<u8>::width() at lines 62-65, and debug_assert_eq!(row_idx_flags.len(), 0) at line 102 confirms it is always empty.

Impact. These do not appear to be soundness issues. They can cause configuration failures to be delayed or opaque, can surprise users who expect the verify-stark deferral prover trait path to support child proofs with deferrals, and leave minor dead code in the AIR.

Recommendation. Replace the debug-only configuration checks with ordinary assertions or fallible constructor errors. Document whether DeferralCircuitProver::prove is intentionally no-deferral-only for verify-stark, or add a deferral-aware trait path if that use case is supported. Remove the dead row_idx_flags slice.

Client response. The DeferredVerifyCircuitProver::prove item is present in the audited snapshot at commit f01c912, but it had already been fixed on another development line by PR #2717 and thus it is fixed in the later rc branches. The remaining API/hygiene notes have been addressed in PR #2837.

Description. This finding collects some low-impact observations made during the review. None of them are soundness issues in the code as it stands; they are defense-in-depth hardening, contract hygiene, and code-quality suggestions, grouped by theme.

Canonical form and range invariants

The core soundness problem in this area, that non-canonical 31-bit BabyBear representatives are absorbed into the transcript and Merkle leaves, is written up separately as a Medium finding (“Non-canonical BabyBear representatives produce multiple transcript and Merkle encodings of the same field element”). The remaining items here are orthogonal hardening:

• pack_base_2_31_cells (hash/poseidon2.rs:204) does not assert values.len() <= MULTI_FIELD32_NUM_F_ELMS. With too many limbs the base-2^31 packing exceeds the field and stops being an injective encoding; I recommend asserting the bound (the canonicality of each limb is covered by the Medium finding above).

• load_base_baby_bear_decomposition_witness (transcript/mod.rs:74) constructs BabyBearWire { value: digit, max_bits: BABY_BEAR_BITS } and only range-checks the digits afterwards in constrain_base_baby_bear_decomposition (which does enforce < BABY_BEAR_MODULUS_U64, so these particular wires end up canonical). The type’s range invariant should nonetheless hold by construction: I suggest returning the raw AssignedValues here and only minting a BabyBearWire where a range check accompanies it, so the type is never observable in an unchecked state.

• hash_babybear_slice_to_digest (hash/poseidon2.rs:219) is an unpadded sponge with no length domain separation, so it is not collision-resistant across variable-length inputs: trailing zero limbs are absorbed identically, giving Hash(a) = Hash(a || 0) when the extra zero falls in the same rate block. The current callers hash fixed-shape data, so this is latent; worth a note (or a length tag) to avoid future misuse.

Type-safety preconditions

• BabyBearChip::select (base.rs:340) and BabyBearExt4Chip::select (field/baby_bear/extension.rs) take the condition as a raw AssignedValue<Fr> and forward it to gate().select, which is only a branch selection when cond ∈ {0,1}. The wrapper adds no boolean constraint; soundness rests on the caller having constrained cond. In-tree callers do (bits from num_to_bits, or SafeBool), so there is no live bug, but the API is unsafe. I recommend taking a SafeBool (or a boolean new-type) for cond.

• eval_var (stages/batch_constraints/mod.rs:479) maps a symbolic entry’s rotation offset with if offset == 0 { value.local } else { value.next }, so any offset >= 2 silently resolves to value.next. This is correct only for AIRs whose rotations are limited to current/next. I suggest a typed Offset enum (Cur/Next) or a match with _ => unreachable!() so an unexpected offset fails loudly.

API and contract hygiene

• prove_verify_stark_constraints_only (prover.rs:99) proves with instance_columns == 0, so it does not export the verifier’s public inputs and cannot be used as a real verifier; it exists for integration tests. The constraints-only path should be clearly marked test-only (in name and/or docs) so it is not mistaken for a statement-binding proof.

Suggested refactors and code-quality nits

These are stylistic and do not affect correctness:

• gkr-proof-wire (GkrProofWire): claims_per_layer is always four claims; Vec<[BabyBearExtWire; 4]> would encode that.
• whir-proof-wire-struct (WhirProofWire): whir_sumcheck_polys always has 2 evals per round; Vec<[BabyBearExtWire; 2]> would encode that.
• verify-final-residual: let r = ext_chip.sub(final_acc, final_claim); assert_equal(r, zero) is just ext_chip.assert_equal(final_acc, final_claim).
• query-root-from-bits-helper: the inline “select a power of omega or one, then wrap in a BabyBearWire” should be a select_constant helper on the BabyBear chip rather than open-coded.
• binary-k-fold-loop, eval-lagrange-on-integer-grid, eval-eq-mle-ef-f-assigned: each open-codes an extension-field +/- base-field operation by mutating .0[0]; these belong behind dedicated Ext ± Base methods on the extension chip.
• eval-eq-mle-assigned: the cost comment is inaccurate, since y is also an extension-field element.
• tree-compress-helper: takes ext_chip: &BabyBearExtChip but does nothing field-specific; it should take gate: &impl GateInstructions<F>.
• invert-base-helper, ext-to-coeffs-helper: these helpers logically belong in the baby_bear module.
• digest-to-fr-helper: could be an Into implementation.
• babybear-ext4-from-base-const: the explicit caching is redundant; the base layer already caches in BabyBearChip::load_constant.
• poseidon2-babybear-rate-ratio: the rate constants are defined by division; defining BABY_BEAR_PER_BN256 and deriving the rate from it reads more clearly.
• constrain-batch-gkr-cubic-subrounds: the repeated cubic sumcheck rounds could share a sumcheck subroutine.
• wrapper-generate-circuit-object-for-proving-block: introduce a named constant for the accumulator size (12).
• BabyBearChip::special_inner_product can be simplified by noting that range and other_range are always equal. The function actually computes the s-th term of a convolution. The function also hardcodes a magic number rather than using the extension degree (constant).

Client Response. This issue has been addressed by PRs #2868 and #2909, which cover the concrete defense-in-depth items: packing bounds, typed boolean selects, rotation checks, fixed proof shapes, test-only prover cleanup, and delayed BabyBearWire construction until after range checks. The finding remains partially resolved because the length-agnostic hash_babybear_slice_to_digest note and some style refactors are still open.

Description. This finding collects some low-impact observations made during the review that may improve performance.

Unused and duplicate code

Some sections of the code are either unused, unreachable, or duplicated:

• Functions for packing BabyBear elements into Fr elements appear twice: pack_base_2_31 (in transcript.rs) and pack_base_2_31_cells (in poseidon2.rs). The only difference is whether the input is the assigned value or the wire. For both of these functions, the caller has access to both representations.
• add, sub, mul, mul_add in BabyBearChip all implement an additional max_bits check on the output c, even though this is already guaranteed not to overflow.
• The select method of Poseidon2State is unused.

The duplicate packing and redundant output checks produce additional and unnecessary constraints.

Equality checks

The chips BabyBearChip and BabyBearExt4Chip both expose assert_zero and assert_equal functions, where the latter works by performing a subtraction and an internal call to assert_zero.

However, we have observed the following patterns in the code:

• Using assert_equal with a fixed $0$ instead of using assert_zero (example 1, example 2).
• Performing a subtraction followed by an assert_equal with a fixed $0$, instead of using assert_equal in the first place (example 1, example 2, example 3).

Operand ordering affects number of constraints

add and sub in BabyBearChip are cheaper if the first operand is larger. mul avoids this with a mem::swap pattern. This same pattern could be replicated in add and sub to potentially save on reduce operations.

Client Response. This issue has been addressed by PR #2868, which resolves the duplicate packing, unused selector, redundant output reductions, and equality-check items. The add/sub operand-ordering optimization was implemented in #2868 but reverted in PR #2909 for clarity, so that suggestion was not adopted.

Description. The soundness of signed_div_mod rests on an upper bound on the input width. BabyBearWire documents the invariant, and signed_div_mod repeats it as an explicit assumption:

/// ## Assumptions
/// * `a_max_bits < F::CAPACITY = F::NUM_BITS - RESERVED_HIGH_BITS`
///   * Unsafe behavior if `a_max_bits >= F::CAPACITY`

The overflow argument in signed_div_mod (that |div * b + rem| does not wrap modulo Fr) depends on this bound. Yet neither reduce nor signed_div_mod enforces it. reduce forwards a.max_bits straight through, checking only the value under a debug-only guard:

pub fn reduce(&self, ctx: &mut Context<Fr>, a: BabyBearWire) -> BabyBearWire {
    guarded_debug_assert!(fe_to_bigint(a.value.value()).bits() as usize <= a.max_bits);
    let (_, r) = signed_div_mod(&self.range, ctx, a.value, a.max_bits);
    ...
}

and signed_div_mod itself only asserts a_val.bits() <= a_num_bits, never a_num_bits <= Fr::CAPACITY - RESERVED_HIGH_BITS. Recall that assert_zero, which performs the same shifted-quotient range check, does guard the width:

assert!(a.max_bits <= Fr::CAPACITY as usize - RESERVED_HIGH_BITS);

So a wire carrying an oversized max_bits tag flows into signed_div_mod through reduce without the gadget failing closed.

Impact. Defense in depth. max_bits is circuit-generation metadata rather than prover-controlled witness data, and no in-tree caller constructs a BabyBearWire violating the invariant, so there is no concrete attack. The concern is that reduce and signed_div_mod are public over the field module and do not reject an input that breaks the assumption their soundness relies on.

Recommendation. Add the same guard reduce (and/or signed_div_mod) already documents, mirroring assert_zero:

assert!(a.max_bits <= Fr::CAPACITY as usize - RESERVED_HIGH_BITS);

Client Response. This issue has been addressed in PR #2860, which adds the precondition assertion in signed_div_mod, and in PR #2868, which adds the same guard in reduce. PR #2909 removes a duplicate assertion, leaving both checks in final code.

Description. sample_bits short-circuits when asked for zero bits:

pub fn sample_bits(&mut self, ctx: &mut Context<Fr>, bits: usize) -> AssignedValue<Fr> {
    ...
    if bits == 0 {
        return ctx.load_zero();
    }
    let sampled = self.sample(ctx);
    ...
}

Recall that a real sample goes through sample, which first flushes any buffered observations and then squeezes the sponge:

pub fn sample(&mut self, ctx: &mut Context<Fr>) -> BabyBearWire {
    if let Some(val) = self.sample_buf.pop() { return val; }
    self.flush_observe_buf(ctx);
    let squeezed = self.sponge_squeeze(ctx);
    ...
}

sponge_squeeze is what flips the duplex sponge from absorb to squeeze mode: when absorb_idx != 0 it permutes the state and resets absorb_idx/sample_idx. The zero-bit path does neither; it does not flush observe_buf, does not call sponge_squeeze, and returns a freshly loaded zero. The native out-of-circuit transcript performs the squeeze transition on every sample (the sponge tracking here is documented to “match DuplexSponge::absorb/squeeze”). Hence an in-circuit sample_bits(0) issued while the sponge is still in absorb mode (or with observations buffered) leaves the in-circuit Fiat-Shamir state one transition behind the native verifier, and every challenge drawn afterwards diverges.

Impact. Informational. sample_bits(0) is not reached in the current verifier with a non-trivial sponge state: check_witness already returns early for bits == 0 before it would sample, and no other call site requests zero bits. The behavior cannot produce a soundness issue as the code stands; I am flagging it as a latent transcript-fidelity gap that would bite if a future call site sampled zero bits mid-transcript.

Recommendation. Make the zero-bit path perform the same sponge transition as a genuine sample, flushing the observe buffer and squeezing once (discarding the result), so the in-circuit transcript matches the native one unconditionally; alternatively assert bits > 0 if zero is never an intended argument.

Client Response. This issue has been addressed in PR #2868 by sampling before the zero-bit early return. sample_bits(0) now runs the same sample path as a non-zero request, keeping the transcript in sync.

Description. signed_div_mod is a crucial component of the field arithmetic emulation. It is also one of the most complex functions in the BabyBearChip. The documentation comment justifies why this function is mathematically sound. As noted in a previous finding, some of the claims there are not correct. Furthermore, the code does not actually implement the checks written in the documentation string.

Impact. As it stands, it is unclear why the implemented function is sound.

Recommendation. Revise the documentation comment to match the implemented checks.

Client Response. This issue has been addressed by PR #2860, which rewrites the signed_div_mod proof comment to match the implemented checks. Additionally, PR #2909 addresses our follow-up comment by replacing the stale assert_zero cross-reference with an exact-remainder explanation.

Description. The top-level SHA-2 and Keccak soundness theorems in the openvm-fv repository are conditional on hypotheses stating that the relevant AIR constraints and bus interactions hold, but those hypotheses are not presented through one uniform, extraction-native interface across AIRs. The raw extraction files provide a mechanical low-level surface (per-row predicates Foo.extraction.constraint_i and a bus predicate Foo.extraction.constrain_interactions), yet the theorem-facing assumptions are aggregated ad hoc per AIR:

• SHA-2 uses handwritten structures (mainTraceConstraints, blockHasherConstraints) whose fields store extracted interactions and row or group constraints;
• the Keccak permutation and XORIN define extracted row lists and allHold predicates bridged to simplified theorem-facing predicates via rfl;
• KeccakfOp’s main theorem consumes allHold_simplified, packaging extracted interactions with a simplified row_constraint_list.

This is not evidence of a false theorem; the bridges are mostly kernel-checked and many are definitional. The problem is auditability: a reviewer must inspect each AIR’s bespoke aggregation layer to confirm the top-level theorem assumes exactly the extracted Rust AIR constraints and interactions, and not a strengthened, weakened, omitted, duplicated, or otherwise ad-hoc set. A soundness theorem stated over a simplified aggregate can be true while silently failing to apply to the actual extracted AIR if the aggregate diverges from the raw extraction output.

Impact. Informational (formal-verification hygiene and auditability). The risk of FV integration mistakes is increased and audit review is made materially harder. The guarantee a reader most wants, namely that a theorem’s hypotheses are precisely the extracted AIR’s constraints and interactions, is not directly expressible against the current interfaces.

Recommendation. Provide a uniform final theorem or corollary per verified AIR whose assumptions are entirely derived from raw extraction output: define a canonical extraction-level aggregate (for example Foo.extraction.constrain_row_all := constraint_0 and ... and constraint_N) and state the public soundness corollary against bounded extraction hypotheses (constrain_interactions plus for all row <= air.last_row, constrain_row_all air row). Simplified constraints and semantic bundles can remain internal proof conveniences, but the auditor-facing theorem should have extraction-native assumptions. Prefer bounded row quantification over unbounded for all row, since the verifier only enforces constraints over the finite trace.

Client Response. The client has acknowledged the recommendation and is evaluating it for adoption in a future update.

Description. Pointer bounding in the SHA-2 main chip and the Keccak XORIN chip is done by range-checking only the top limb of the pointer: high_limb * 2^(32 - ptr_max_bits) < 2^8. For ptr_max_bits >= 24 this correctly enforces pointer < 2^ptr_max_bits. For ptr_max_bits < 24 it only forces the top byte toward zero, i.e. it enforces the weaker bound pointer < 2^24, under-constraining the pointer relative to the documented precondition.

KeccakfOpAir asserts ptr_max_bits >= RV32_CELL_BITS * (RV32_REGISTER_NUM_LIMBS - 1) at construction time. Sha2MainAir (eval_instruction) and XorinVmAir document the same precondition but do not assert it. The shipped default (POINTER_MAX_BITS = 29) satisfies the precondition, so honest configurations are safe.

Impact. Informational. Honest pointers always satisfy the precondition, so there is no completeness impact, and the shipped default configuration is sound. The issue is a latent, silent soundness weakening that would only manifest if a non-default configuration set ptr_max_bits < 24, in which case the pointer would be under-constrained rather than bounded as documented.

Recommendation. Add the same construction-time assertion that KeccakfOpAir uses to Sha2MainAir and XorinVmAir, so the documented precondition is enforced rather than assumed. Consider also asserting an explicit upper bound, since ptr_max_bits >= 31 raises a separate field-aliasing concern.

Client Response. The issue has been addressed in PR #2845 with explicit assertions in Sha2MainAir and XorinVmAir, as recommended.

Description. The architecture designates four system AIRs as required: SystemConfig::is_required_air_id returns true for PROGRAM, CONNECTOR, BOUNDARY, and MERKLE. The backend enforces requiredness as a proof-shape check (the verifier asserts vk.is_required implies is_air_present, via ProofShapeVDataError::RequiredAirNoVData), so a properly keyed verifying key rejects proofs that omit any of those AIRs.

VirtualMachine::new_with_keygen honors this, calling add_required_air exactly when is_required_air_id(air_id). The SDK path does not: AppProvingKey::keygen calls app_engine.keygen(&airs) directly, and the default StarkEngine::keygen does for air in airs { add_air(air) }, never add_required_air. So the SDK app verifying key marks nothing required, and the backend’s is_required enforcement does not apply.

verify_segments partially compensates, but asymmetrically: it explicitly checks program_air_present, connector_air_present, and merkle_air_present, but has no boundary_air_present check; the boundary AIR falls into the generic branch that only asserts empty public values. So three of the four required system AIRs are re-checked and the boundary is conspicuously omitted. Under an SDK-generated verifying key, boundary-AIR presence is enforced by neither the backend is_required flag (not set) nor verify_segments (not checked); it rests solely on memory-bus balance. A follow-up proof-of-concept confirmed that a degenerate terminate-only (no-memory) execution can omit PersistentBoundaryAir and pass both engine.verify and verify_segments.

Impact. Informational; no current security impact. A boundary-omitting proof can only exist for a no-memory execution: any memory access (registers are address space 1 on the same bus) leaves the memory bus unbalanced, which the GKR/LogUp zero-sum check rejects. A no-memory execution forces initial_root = final_root = default_root, so exe_commit = H(program_commit, default_root, initial_pc) matches only a trivial app with default initial memory; for any real app the degenerate proof’s exe_commit does not match and is rejected. So no meaningful statement can be forged. The finding is a deviation from the architecture’s intended proof-shape invariant: soundness here currently relies on bus balance rather than the explicit required-AIR mechanism the design specifies, which is exactly the kind of latent gap that becomes load-bearing if a future change weakens the bus argument or introduces a self-balancing system AIR.

Recommendation. Two independent halves, both warranted:

1. Root cause: make SDK app keygen mirror new_with_keygen, building via MultiStarkKeygenBuilder and calling add_required_air whenever config.as_ref().is_required_air_id(air_id). Add a regression test asserting that AppProvingKey::keygen(...) marks Program, Connector, Boundary, and Merkle as required.
2. Defense in depth: add an explicit boundary_air_present check to verify_segments, matching the existing Program, Connector, and Merkle checks, so the host-level system-AIR set is symmetric.

Client Response. The observation has been acknowledged and addressed in PR #2847, with SDK app keygen now mirroring new_with_keygen and marking the required AIRs, and verify_segments explicitly checking that the AIRs are present.

Description. OpenVM’s BN254 and BLS12-381 pairing checks in the guest-libraries implement the Novakovic-Eagon optimization. The main idea of the optimization is that, since verifying $e(P,Q)=1$ is dominated by the final exponentiation $f^{(p^{12}-1)/r}=1$ (where $f$ is the output of the Miller loop and $p$, $r$ are the base-field characteristic and the prime subgroup order of the curve, respectively), we can avoid this operation in favor of a much cheaper algebraic identity verified against a prover-supplied hint. The prover sends a witness $(c,u)$ and the verifier checks the small-exponent equation $f·u=c^{\lambda }$, where $\lambda$ is the optimal exponent for the curve ($\lambda =6x+2+q^3-q^2+q$ for BN254, $\lambda =q-x$ for BLS12-381) and is several orders of magnitude smaller than $(p^{12}-1)/r$. The $c^{\lambda }$ term can be folded into the Miller loop almost for free by passing $c^{-1}$ as the embedded exponent.

The soundness of this relation rests on Theorem 3 of the paper, which states: $e(P,Q)=1$ if and only if there exists $(c,u)$ such that $f·u=c^{\lambda }$ and $u^{d^i}=1$, where $d^i$ is the order of a specific residue subgroup of ${𝔽}_{p^{12}}^{*}$ dictated by the curve (for BN254, $d^i=27$, i.e. the honest hint always satisfies $u^{27}=1$). The latter constraint, however, is missing from this implementation: Bn254::try_honest_pairing_check performs no subgroup check on $u$ at all, and Bls12_381::try_honest_pairing_check enforces only a partial check on its scaling factor $s$ while leaving the residue witness $c$ unconstrained.

Notably, because $u$ is underconstrained, the algebraic identity $f·u=c^{\lambda }$ collapses into a single equation in ${𝔽}_{p^{12}}$ with two free unknowns and is therefore trivially satisfiable for any $(P,Q)$, regardless of whether $e(P,Q)=1$ actually holds. A malicious prover simply sets $c=1$ (so $c^{\lambda }=1$) and solves $u=f^{-1}$, where $f$ is the Miller-loop output computed from the (possibly invalid) input pair. The forged hint $(1,f^{-1})$ then passes the verifier’s check identically to an honest hint.

As a simple proof of concept, a malicious prover can apply the following diff to the host-side phantom executor that produces the hint, causing the zkVM to emit a valid proof for any Bls12_381::pairing_check.

diff --git a/extensions/pairing/circuit/src/pairing_extension.rs b/extensions/pairing/circuit/src/pairing_extension.rs
index b5de43ca4..1305ff614 100644
--- a/extensions/pairing/circuit/src/pairing_extension.rs
+++ b/extensions/pairing/circuit/src/pairing_extension.rs
@@ -251,8 +251,10 @@ pub(crate) mod phantom {
                     })
                     .collect::<eyre::Result<Vec<_>>>()?;

-                let f: Fq12 = Bls12_381::multi_miller_loop(&p, &q);
-                let (c, u) = Bls12_381::final_exp_hint(&f);
+                let c = Fq12::one();
+                let c_inv = Fq12::one();
+                let fc = Bls12_381::multi_miller_loop_embedded_exp(&p, &q, Some(c_inv));
+                let u = fc.invert().unwrap();
                 hint_stream.clear();
                 hint_stream.extend(
                     c.to_coeffs()

The resulting proof verifies under the unmodified verifying key, so the forgery is indistinguishable from an honest proof to any downstream verifier that consumes it.

Note: this issue is already known to the client, having been reported by a zkSecurity member via responsible disclosure prior to the audit. It is included here for completeness since it is still in scope and has not been fixed during the audit.

Impact. A malicious prover can forge successful pairing checks for false pairing equations. Any guest program relying on openvm-pairing pairing verification as a dependency can be made to accept invalid cryptographic proofs or commitments inside the zkVM. This breaks soundness of the proven statement.

Recommendation. Before accepting the hinted relation, enforce the missing Theorem 3 subgroup condition $u^{d^i}=1$ on the residue witness.

Client Response. This issue has been acknowledged and fixed by rebasing from v1.6.0.