Cowrie Research

bit-length-precondition-omission

15 min read

Bit-Length Precondition Omission / Representation-Width Underconstraint

  • Name: bit-length precondition omission / representation-width underconstraint
  • Category: exploit pattern / zk-circuit semantic precondition failure / helper-gadget width-assumption omission / under-constrained arithmetic admission
  • Summary: This pattern appears when a proof circuit reuses a helper gadget whose soundness depends on an unstated width assumption — inputs must fit in n bits, limbs must stay in proper representation, a remainder must be range-bounded, an index must stay below a fixed bit length, or a signed value must stay inside an expected window — but the surrounding circuit never actually proves that assumption. The helper then returns a result that is only meaningful on the intended narrow domain while the prover is free to choose wider witness values. That lets attackers satisfy a range proof, ordering check, modulo relation, or nullifier derivation path with witness values the protocol would never have considered valid, turning locally reasonable helper reuse into a forged authorization, replayable right, or impossible state transition.
  • What it is:
    • A circuit uses a helper such as LessThan, Num2Bits, bigint division / modulo logic, an index-to-bits encoder, or some other gadget whose correctness is conditioned on inputs staying within a fixed bit width or canonical representation.
    • The outer circuit relies on the helper’s output as if that width condition were already enforced.
    • No separate constraint proves that the helper’s inputs or outputs actually live inside that intended width.
    • The proved statement is therefore weaker than the protocol author thinks: it says this helper relation holds algebraically for some field elements, not this helper relation holds for well-formed bounded-width values with the intended semantic meaning.
    • Attackers can then choose witnesses outside the intended width so overflow, wraparound, sign ambiguity, or non-canonical representation makes the helper accept an otherwise-invalid state transition.
  • Typical preconditions:
    • The circuit depends on a comparison, range proof, modulo reduction, index derivation, or bigint helper whose documentation assumes bounded-width inputs.
    • The surrounding circuit treats those width assumptions as obvious and does not restate them as constraints.
    • Security-critical logic depends on the helper result: location validity, replay prevention, nullifier uniqueness, bounded arithmetic, canonical remainders, note positions, or some other one-time right or authorization path.
    • The prover controls or influences the witness values entering the helper.
    • The system has no later canonicalization boundary that would reject the widened witness interpretation before value leaves or authority is consumed.
  • Common vulnerable surfaces:
    • LessThan(n) or similar comparator gadgets used as range proofs without separately proving the operands fit in n bits
    • bigint helper libraries where quotient, remainder, or limb arrays are constrained only partially, leaving one output in non-canonical representation
    • note-position, leaf-index, or path-index gadgets whose intended width is smaller than the host field but never explicitly bounded
    • replay-prevention or nullifier derivation circuits that hash or derive one semantic object from multiple witness encodings because the index / position / scalar input is wider than intended
    • arithmetic adapters that assume signed overflow, proper representation, or canonical limb decomposition but only constrain part of that representation family
    • zk-app game or state-transition circuits that treat inside allowed radius, inside valid range, or within bounded domain as a helper property rather than a full proved statement
  • Exploit sequence:
    1. The attacker identifies a helper gadget whose correctness depends on a width assumption the outer circuit never proves.
    2. They choose witness values that violate the intended width while still satisfying the circuit’s explicit constraints.
    3. Because the helper is now operating outside its semantic domain, its output no longer means what the protocol author thinks it means.
    4. The circuit still accepts the witness and proves a weaker statement than intended: an out-of-range coordinate looks in range, two spends derive different nullifiers from one semantic note, or a modulo / remainder output leaves canonical form.
    5. The application honors the proof and updates state, spends value, or mints authority on the assumption that the helper result represented a real bounded-domain fact.
  • Variants:
    • Comparator precondition omission — LessThan(bits) or a similar comparator is used as a range proof, but operands are never constrained to bits bits first, so overflow or wraparound invalidates the intended ordering claim.
    • Output canonicalization omission — a helper computes quotient and remainder or another decomposition pair, but only one output is range-constrained, so the other can leave canonical form and poison downstream arithmetic.
    • Index-width omission — note indices, Merkle positions, or path selectors exceed the intended bit width, letting one semantic object admit multiple derived identities or nullifiers.
    • Representation-family drift — a helper expects proper limb representation but the circuit allows a wider or signed-overflow representation, so downstream consumers interpret the same bigint object differently.

Three helper-width promotions healthy reviewers should not collapse

  1. A helper-shaped arithmetic object exists at all

    • A comparator got called, a bigint helper returned quotient/remainder arrays, an index was encoded, or a modulo relation held algebraically for some witness values.
    • This is only the existence question: some helper-valid-looking object showed up in the circuit trace.

  2. That object already counts as bounded-width or canonical semantic truth

    • The surrounding circuit treats the helper input or output as if width, limb form, signedness, and canonical representation have already all been proved tightly enough for the helper result to mean what the protocol thinks it means.
    • This is the semantic-promotion question: the helper-shaped arithmetic object is really the same bounded object the protocol meant to authorize.

  3. That accepted semantic object already deserves downstream authority

    • A coordinate is admitted as map truth, a nullifier/index becomes one-time-right identity, or a quotient/remainder object gets to influence spend, release, replay-prevention, or settlement logic.
    • This is the authority question: even if the helper relation holds, why was this accepted representation allowed to matter this much here?
  • Detection heuristics:
    • Treat every gadget parameter like bits, n, k, wordSize, maxAbsValue, or fieldBits as a suspicion magnet until you can point to the exact constraints that force inputs and outputs into that domain.
    • Read helper-library docs and source for hidden preconditions; many zk bugs come from correct gadget reuse under incorrect assumptions about what the gadget itself does not prove.
    • For comparators and range proofs, fuzz with boundary-adjacent witnesses that exceed the intended width while preserving the outer semantic claim and see whether proofs still verify.
    • For bigint helpers, inspect both inputs and outputs for canonical limb constraints; if a helper promises a = q*b + r, ask where r < b and r’s representation width are actually enforced.
    • Search for comments like expects n-bit inputs, proper representation, range proof, bounded index, or overflow protection and verify the corresponding constraints exist in the circuit rather than only in prose.
    • Keep an eye out for host-language reasoning imported into finite-field circuits. This integer is obviously small is not a proof once the prover controls witness values inside a large field.
  • Defenses:
    • Prove helper preconditions explicitly in the outer circuit; do not assume library gadgets constrain input width just because they are usually used that way.
    • Prefer helper wrappers that encode both the semantic relation and its width preconditions in one reusable checked primitive.
    • Constrain every decomposition output, not just the one currently consumed by a visible equality.
    • Add adversarial tests that exceed intended width or representation families: x, x + 2^n, non-canonical remainders, oversized indices, and alternate limb encodings should all fail.
    • Document gadget preconditions in protocol-level review notes so audits ask where is this proved? instead of stopping at where is this used?.
    • When width assumptions underpin replay prevention or custody logic, treat them as settlement-critical constraints rather than prover-side hygiene.

What sound design looks like

  • A healthy circuit keeps the three promotions separate on purpose: helper-shaped arithmetic object exists, that object is already the bounded-width / canonical semantic object we mean to trust, and that accepted object deserves spend, release, or replay-prevention authority here.
  • A healthy circuit does not rely on helper folklore. If a gadget is only sound for n-bit inputs or canonical limbs, the outer circuit proves those facts explicitly before treating the helper’s output as authorization truth.
  • Width assumptions should be visible at the same layer as the economic claim. Reviewers should be able to trace this proof authorizes a spend through the nullifier / index / remainder / coordinate was first proven well formed for the gadget that consumed it.
  • The cleanest engineering shape is a checked wrapper primitive: BoundedLessThan, CanonicalBigMod, BoundedIndexToNullifier, or similar helpers that fuse semantic relation and representation constraints instead of requiring callers to remember invisible side conditions.
  • Property tests should target the precondition boundary directly. If the protocol says out-of-range inputs are impossible, the test suite should not only try honest in-range cases; it should try the exact width-overflow witnesses that would make the helper lie.
  • The reviewer question is: where do we prove the witness object satisfies the width and canonical-representation assumptions that make this helper's output meaningful at all, and where do we stop that object from gaining downstream authority before that proof is complete?

Best concrete case studies

  • [[../../../incidents/proofs-verifiers/dark-forest-v0-3-rangeproof-lessthan-bit-length-precondition-omission-near-miss-2021-09-30|Dark Forest v0.3 RangeProof / LessThan(bits) bit-length precondition omission near miss (2021-09-30)]] — the clean comparator-domain exemplar. LessThan(bits) looked like a range proof for map coordinates, but the circuit had not yet proved the compared values actually lived in the comparator’s intended width domain, so an inside bounds statement weakened into inside bounds for honest-width witnesses.
  • [[../../../incidents/proofs-verifiers/zk-email-verify-revealsubstring-lessthan-exclusive-upper-bound-bit-width-omission-near-miss-2025-11-12|zk-email-verify RevealSubstring LessThan exclusive-upper-bound bit-width omission near miss (2025-11-12)]] — the clean bound itself is the out-of-domain comparator operand exemplar. The helper had visible substring bounds, but LessThan(log2Ceil(bound))([x, bound]) stopped one bit too early whenever the exclusive upper bound hit a power of two, so the range check no longer proved the exact boundary statement its callers assumed.
  • [[../../../incidents/proofs-verifiers/circom-ecdsa-bigmod-remainder-range-check-omission-noncanonical-remainder-near-miss-2022-03-30|circom-ecdsa BigMod remainder range-check omission / non-canonical remainder near miss (2022-03-30)]] — the canonical bigint-output exemplar. The quotient side already had Num2Bits(n) checks, which made the missing remainder-side width proof easy to miss in review, yet that was exactly the gap that let mod[] remain an arithmetic witness instead of a guaranteed proper-form remainder object.
  • The useful preserved boundary is that not every too-wide zk input bug belongs here. Semaphore-style groupId, external-nullifier, and zero-leaf issues usually do more analytical work under public-input-domain-mismatch because the decisive split is across the contract / verifier boundary. This note should stay focused on helpers whose own semantic domain assumptions were never fully proved inside the circuit that reused them.

Failure-prevention checklist

  • For every helper with a width parameter or canonical-representation requirement, list the exact constraints that prove those preconditions before the helper result is trusted.
  • Write review notes in promotion order: helper object exists, helper object became bounded-width semantic truth, accepted object gained authority. That makes it harder to stop at the comparator ran or the modulo relation held.
  • Wrap unsafe-by-default gadgets in project-local checked adapters so call sites cannot forget the width proof and still compile or review cleanly.
  • Add explicit width constraints to both inputs and outputs of decomposition, comparison, and bigint gadgets; do not assume one side being checked implies the other side is meaningful.
  • Fuzz and regression-test the just over the width boundary family: x + 2^n, oversized indices, alternate limb encodings, non-canonical remainders, and values that differ only by implied wraparound.
  • Treat comments like prevents overflow, ensures proper representation, or bounds the index as audit claims that must map to a concrete equality or bit-decomposition constraint.
  • Review helper-library upgrades, swaps, and copy-pastes with special care; teams often preserve the call site while losing the original surrounding width checks.
  • Make circuit tests assert semantic claims, not only satisfiability. If the statement is coordinate is within radius or nullifier is unique for one note, include negative tests using wider witness objects that would break that meaning.
  • Where a widened witness can reopen a spend or claim path, bind settlement code and circuit review together; replay prevention is unsafe if the proof can derive multiple helper-valid representations of one semantic right.
  • Keep a short inventory of gadgets with hidden preconditions in each repo so reviewers know where helper semantics depend on more than the visible function signature.
  • Prefer design patterns where malformed-width objects die at admission rather than surviving deep enough to influence state transitions, nullifier derivation, or payout logic.

Audit prompts

  • What exact width or canonical-representation assumption does this helper rely on, and where is that assumption proved in constraints rather than comments?
  • Am I accidentally promoting helper-shaped arithmetic witness exists into bounded semantic object exists without one explicit local proof step?
  • If I add 2^n, widen one limb, or choose a non-canonical remainder, does the helper still output the same acceptance bit or downstream identity?
  • Do all outputs of this decomposition or comparison helper stay in proper representation, or only the subset currently checked by surrounding code?
  • Is the circuit proving the intended semantic statement, or only a weaker field-arithmetic statement that happens to coincide with the intended meaning for honest in-range witnesses?
  • Which witness-controlled values feed into replay prevention, nullifier derivation, or one-time-right consumption, and what stops multiple width-distinct encodings of the same semantic object?
  • If a helper library says expects n-bit inputs, where is the matching Num2Bits / range proof / decomposition that actually enforces that expectation?
  • Could a caller satisfy inside bounds, valid index, proper modulo result, or unique nullifier with a witness that only works because the circuit silently accepted a wider representation family than intended?
  • After a refactor or library upgrade, what test proves the helper’s semantic preconditions are still fused to the call site instead of living only in stale documentation?

Lessons that should already be standard

  • Helper gadgets prove only what they constrain. Their names and common usage patterns are not additional constraints.
  • The helper ran is not the same claim as the bounded semantic object exists, and that is not the same claim as the object deserves downstream authority.
  • Width assumptions are part of the proved statement. If the circuit depends on n-bit meaning, the proof must establish n-bit well-formedness.
  • Prevents overflow is an economic claim once a proof authorizes movement, minting, or replay prevention. It needs adversarial tests, not just nice comments.
  • Canonical representation matters as much as algebraic equality. A quotient, remainder, index, or nullifier derived from a non-canonical witness can still poison downstream logic even if some top-level equality holds.
  • Many under-constrained zk bugs are really helper-boundary bugs: the circuit reused a correct gadget, but never proved the gadget’s semantic domain assumptions.
  • The safest circuit APIs make illegal width states unrepresentable at the call site rather than relying on every caller to remember invisible preconditions.

Where this pattern stops

  • Use validation-output-nonconsumption when the helper computes the right boolean validation result but the outer circuit never requires that result to equal 1. That family is about a dropped output bit. This family is about missing width and representation preconditions even when the output is consumed.
  • Use public-input-domain-mismatch when the verifier and host contract disagree about the domain of a public input across the proof boundary. This family can exist entirely inside the circuit even before any contract-domain mismatch appears.
  • Use witness-public-input-binding-failure when the sharper problem is that the circuit never bound witness-side state to the public object it claimed to authenticate. Here the narrower failure is that the helper’s semantic domain assumptions were never proven, weakening the statement from inside.
  • In short: this pattern begins when a helper’s output is only meaningful for bounded-width or canonical inputs the circuit never proved, and it stops once the sharper story is instead an unconsumed validation bit, a verifier/contract boundary mismatch, or a broader split statement.

Internal linkages

Control surface

  • The leverage sits in helper call sites where semantic domain assumptions stay implicit: comparators, bigint gadgets, decomposition helpers, index encoders, nullifier derivation inputs, and wrappers that translate protocol meaning into raw field arithmetic.

  • The recurring mistake is to read a gadget like LessThan(64) or BigMod as if its name also proved my values are valid 64-bit operands or my outputs are canonical, when the actual circuit never said that.

  • The dangerous promotion is usually not at one line of arithmetic alone, but at the seam where helper-shaped object exists silently becomes bounded semantic object exists and then silently becomes object with spend / release / replay-prevention authority exists.

  • Once a proof system treats width assumptions as comments instead of constraints, attackers can often turn one semantic object into multiple helper-valid witness encodings or make an invalid state transition look bounded and therefore authorized.

  • Sources:

  • Last reviewed: 2026-08-03 UTC

Graph View

Backlinks